Skip to content

refactor prepareSCMP #425

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
jcp19 wants to merge 19 commits into
base: master
Choose a base branch
from
+1,673 −87
Draft

refactor prepareSCMP #425

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
84d03bc
Add verification plan for prepareSCMP (dropping the TODO())
claude Jul 9, 2026
2aac6cb
Rework prepareSCMP plan for the annotations-only constraint
claude Jul 10, 2026
b477295
Implement M1 of the prepareSCMP plan: fresh mode for BaseLayer.Mem
claude Jul 10, 2026
e006e0d
Strengthen SerializeTo error-case postconditions (M4, partial)
claude Jul 10, 2026
2a0ca0d
Implement M2 (design v2): MemSerialize for fresh SCION headers
claude Jul 10, 2026
202d480
Strengthen address-setter contracts for the fresh-header flow
claude Jul 10, 2026
2c2b53e
Fix well-formedness of the SerializeLayers contract
claude Jul 12, 2026
ce5ea3b
Fix SetDstAddr wand shape and adapt testDstSetter
claude Jul 12, 2026
8c27094
Revert SetDstAddr contract change; carve dst bytes caller-side instead
claude Jul 12, 2026
41261fa
Implement M5: drop the TODO() in prepareSCMP
claude Jul 13, 2026
0bba8cd
Work around Gobra desugarer crash on nil in seq literal
claude Jul 13, 2026
c0688d4
Unfold wildcard IP address resources before component-wise calls
claude Jul 13, 2026
2609596
Fix the four remaining router errors in the prepareSCMP proof
claude Jul 13, 2026
85ec14e
Prove the decoded path's length bound via an explicit lemma
claude Jul 13, 2026
12762f5
Re-trigger CI after GitHub Actions infrastructure failure
claude Jul 13, 2026
22588c8
Bridge interface and concrete path length in the quote bound proof
claude Jul 13, 2026
fbd27d6
Make LenSpecBound fractional to keep LenSpec stable across it
claude Jul 13, 2026
34d6943
Minimize LenSpecBound to fit the scion package's time budget
claude Jul 13, 2026
3450274
Use writePerm for the reallocating quote append
claude Jul 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
777 changes: 777 additions & 0 deletions doc/verification/prepareSCMP.md
View file
Open in desktop

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions pkg/addr/host.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -360,6 +360,7 @@ func (h HostSVC) Pack() (res []byte) {

// @ requires pad >= 0
// @ ensures acc(res)
// @ ensures len(res) == HostLenSVC + pad
// @ decreases
func (h HostSVC) PackWithPad(pad int) (res []byte) {
out := make([]byte, HostLenSVC+pad)
Expand Down
6 changes: 4 additions & 2 deletions pkg/slayers/extn.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -309,7 +309,8 @@ func (h *HopByHopExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.Layer
// @ preserves acc(h.Mem(ub), R20)
// @ ensures 0 <= start && start <= end && end <= len(ub)
// @ ensures len(res) == end - start
// @ ensures res === ub[start:end]
// @ ensures ub != nil ==> res === ub[start:end]
// @ ensures ub == nil ==> (res == nil && start == 0 && end == 0)
// @ decreases
func (h *HopByHopExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ , ghost start int, ghost end int @*/) {
// @ unfold acc(h.Mem(ub), R20)
Expand Down Expand Up @@ -458,7 +459,8 @@ func (e *EndToEndExtn) NextLayerType( /*@ ghost ubuf []byte @*/ ) gopacket.Layer
// @ preserves acc(e.Mem(ub), R20)
// @ ensures 0 <= start && start <= end && end <= len(ub)
// @ ensures len(res) == end - start
// @ ensures res === ub[start:end]
// @ ensures ub != nil ==> res === ub[start:end]
// @ ensures ub == nil ==> (res == nil && start == 0 && end == 0)
// @ decreases
func (e *EndToEndExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ , ghost start int, ghost end int @*/) {
// @ unfold acc(e.Mem(ub), R20)
Expand Down
10 changes: 8 additions & 2 deletions pkg/slayers/extn_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,10 @@ pred (e *extnBase) Mem(ubuf []byte) {
acc(&e.NextHdr) &&
acc(&e.ExtLen) &&
acc(&e.ActualLen) &&
// In fresh mode (ubuf == nil, cf. BaseLayer.Mem), ActualLen must be 0.
// This preserves the facts that were derivable from BaseLayer.Mem's
// old definition (breakPoint <= len(ubuf)) for a nil buffer.
(ubuf == nil ==> e.ActualLen == 0) &&
e.BaseLayer.Mem(ubuf, e.ActualLen)
}

Expand Down Expand Up @@ -96,7 +100,8 @@ func (h *HopByHopExtnSkipper) LayerContents() (res []byte) {
preserves acc(h.Mem(ub), R20)
ensures 0 <= start && start <= end && end <= len(ub)
ensures len(res) == end - start
ensures res === ub[start:end]
ensures ub != nil ==> res === ub[start:end]
ensures ub == nil ==> (res == nil && start == 0 && end == 0)
decreases
func (h *HopByHopExtnSkipper) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) {
unfold acc(h.Mem(ub), R20)
Expand Down Expand Up @@ -186,7 +191,8 @@ func (e *EndToEndExtnSkipper) LayerContents() (res []byte) {
preserves acc(e.Mem(ub), R20)
ensures 0 <= start && start <= end && end <= len(ub)
ensures len(res) == end - start
ensures res === ub[start:end]
ensures ub != nil ==> res === ub[start:end]
ensures ub == nil ==> (res == nil && start == 0 && end == 0)
decreases
func (e *EndToEndExtnSkipper) LayerPayload(ghost ub []byte) (res []byte, ghost start int, ghost end int) {
unfold acc(e.Mem(ub), R20)
Expand Down
37 changes: 37 additions & 0 deletions pkg/slayers/path/scion/decoded_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,4 +200,41 @@ func (d *Decoded) Widen(ubuf1, ubuf2 []byte) {
fold d.Mem(ubuf2)
}

// LenSpecBound surfaces the upper bound on a decoded path's serialized
// length that follows from the bounds stored in Base.Mem (NumINF <=
// MaxINFs, NumHops <= MaxHops). It exists because the bound is buried two
// predicate unfoldings deep and is not derivable from LenSpec's
// definition alone at call sites.
// The lemma takes only a fraction so that the caller's retained fraction
// anchors the predicate snapshot: the value of LenSpec then provably
// survives the unfold/refold inside this lemma (cf. Len, which relates
// its result to LenSpec under the same fraction). The body is kept
// minimal because pkg/slayers/path/scion is close to its verification
// time budget: InfoLen and HopLen are compile-time constants, so the two
// exposed predicate bounds (NumINF <= MaxINFs, NumHops <= MaxHops)
// discharge the postcondition without nonlinear reasoning.
ghost
preserves acc(d.Mem(ub), R50)
ensures d.LenSpec(ub) <= MetaLen + MaxINFs*path.InfoLen + MaxHops*path.HopLen
decreases
func (d *Decoded) LenSpecBound(ghost ub []byte) {
unfold acc(d.Mem(ub), R50)
unfold acc(d.Base.Mem(), R50)
fold acc(d.Base.Mem(), R50)
fold acc(d.Mem(ub), R50)
}

// The resources captured by Mem are independent of the buffer parameter,
// so a Decoded path can be re-associated with an arbitrary other buffer,
// in particular with nil. This is used to serialize a decoded path
// without an underlying buffer (cf. prepareSCMP in the router).
ghost
requires d.Mem(ubuf1)
ensures d.Mem(ubuf2)
decreases
func (d *Decoded) ChangeUbuf(ubuf1, ubuf2 []byte) {
unfold d.Mem(ubuf1)
fold d.Mem(ubuf2)
}

/**** End of Lemmas ****/
106 changes: 72 additions & 34 deletions pkg/slayers/scion.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,9 +104,10 @@ func (b *BaseLayer) LayerContents() (res []byte) {

// LayerPayload returns the bytes contained within the packet layer.
// @ preserves acc(b.Mem(ub, bp), R20)
// @ ensures len(res) == len(ub) - bp
// @ ensures 0 <= bp && bp <= len(ub)
// @ ensures res === ub[bp:]
// @ ensures ub != nil ==> len(res) == len(ub) - bp
// @ ensures ub != nil ==> (0 <= bp && bp <= len(ub))
// @ ensures ub != nil ==> res === ub[bp:]
// @ ensures ub == nil ==> res == nil
// @ decreases
func (b *BaseLayer) LayerPayload( /*@ ghost ub []byte, ghost bp int @*/ ) (res []byte) {
// @ unfold acc(b.Mem(ub, bp), R20)
Expand Down Expand Up @@ -650,6 +651,8 @@ func (s *SCION) DstAddr() (res net.Addr, err error) {
// @ ensures err == nil ==>
// @ let rawSrcAddr := s.RawSrcAddr in
// @ (acc(res.Mem(), R15) --* acc(sl.Bytes(rawSrcAddr, 0, len(rawSrcAddr)), R15))
// @ ensures err == nil && typeOf(res) == type[*net.IPAddr] ==>
// @ unfolding acc(res.Mem(), R15) in len(res.(*net.IPAddr).IP) == len(s.RawSrcAddr)
// @ ensures err != nil ==>
// @ acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R15)
// @ ensures err != nil ==> err.ErrorMem()
Expand Down Expand Up @@ -683,10 +686,18 @@ func (s *SCION) SrcAddr() (res net.Addr, err error) {
// @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (!isIPv4(dst) && !isIPv6(dst) ==> len(dst.(*net.IPAddr).IP) == len(s.RawDstAddr)))
// @ ensures res == nil && !wildcard && isIP(dst) ==> (unfolding acc(dst.Mem(), R20) in (isIPv6(dst) && !isConvertibleToIPv4(dst) ==> len(dst.(*net.IPAddr).IP) == len(s.RawDstAddr)))
// @ ensures (res == nil) == (typeOf(dst) == type[*net.IPAddr] || typeOf(dst) == type[addr.HostSVC])
// @ ensures res == nil && isIP(dst) && s.DstAddrType == T4Ip ==> len(s.RawDstAddr) == 4
// @ ensures res == nil ==> s.DstAddrType.Has3Bits()
// @ ensures res == nil && isHostSVC(dst) ==> len(s.RawDstAddr) == 4
// @ decreases
func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res error) {
var err error
var verScionTmp []byte
// (VerifiedSCION) packAddr takes the resources of wildcard IP
// addresses component-wise (cf. its precondition).
// @ ghost if wildcard && isIP(dst) {
// @ unfold acc(dst.Mem(), _)
// @ }
s.DstAddrType, verScionTmp, err = packAddr(dst /*@ , wildcard @*/)
// @ ghost if !wildcard && err == nil && isIP(dst) {
// @ apply acc(sl.Bytes(verScionTmp, 0, len(verScionTmp)), R20) --* acc(dst.Mem(), R20)
Expand All @@ -700,7 +711,11 @@ func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res erro
// Changes to src might leave the layer in an inconsistent state.
// @ requires acc(&s.RawSrcAddr)
// @ requires acc(&s.SrcAddrType)
// @ requires wildcard ==> acc(src.Mem(), _)
// (VerifiedSCION) See the corresponding remark on packAddr.
// @ requires wildcard && isIP(src) ==> acc(&src.(*net.IPAddr).IP, _) &&
// @ (forall i int :: { &src.(*net.IPAddr).IP[i] } 0 <= i && i < len(src.(*net.IPAddr).IP) ==>
// @ acc(&src.(*net.IPAddr).IP[i], _))
// @ requires wildcard && !isIP(src) ==> acc(src.Mem(), _)
// @ requires !wildcard ==> acc(src.Mem(), R18)
// @ ensures isIP(src) ==> res == nil
// @ ensures isHostSVC(src) ==> res == nil
Expand All @@ -720,6 +735,11 @@ func (s *SCION) SetDstAddr(dst net.Addr /*@ , ghost wildcard bool @*/) (res erro
// @ ensures res == nil && !wildcard && isIP(src) ==> (unfolding acc(src.Mem(), R20) in (!isIPv4(src) && !isIPv6(src) ==> len(src.(*net.IPAddr).IP) == len(s.RawSrcAddr)))
// @ ensures res == nil && !wildcard && isIP(src) ==> (unfolding acc(src.Mem(), R20) in (isIPv6(src) && !isConvertibleToIPv4(src) ==> len(src.(*net.IPAddr).IP) == len(s.RawSrcAddr)))
// @ ensures (res == nil) == (typeOf(src) == type[*net.IPAddr] || typeOf(src) == type[addr.HostSVC])
// @ ensures res == nil && isIP(src) && s.SrcAddrType == T4Ip ==> len(s.RawSrcAddr) == 4
// @ ensures res == nil ==> s.SrcAddrType.Has3Bits()
// @ ensures res == nil && isHostSVC(src) ==> len(s.RawSrcAddr) == 4
// @ ensures res == nil && wildcard && isIP(src) && s.SrcAddrType == T16Ip ==>
// @ len(s.RawSrcAddr) == old(len(src.(*net.IPAddr).IP))
// @ decreases
func (s *SCION) SetSrcAddr(src net.Addr /*@, ghost wildcard bool @*/) (res error) {
var err error
Expand All @@ -738,6 +758,8 @@ func (s *SCION) SetSrcAddr(src net.Addr /*@, ghost wildcard bool @*/) (res error
// @ ensures err == nil ==> typeOf(res) == *net.IPAddr || typeOf(res) == addr.HostSVC
// @ ensures err == nil ==>
// @ (acc(res.Mem(), R15) --* acc(sl.Bytes(raw, 0, len(raw)), R15))
// @ ensures err == nil && typeOf(res) == type[*net.IPAddr] ==>
// @ unfolding acc(res.Mem(), R15) in len(res.(*net.IPAddr).IP) == len(raw)
// @ ensures err != nil ==> acc(sl.Bytes(raw, 0, len(raw)), R15)
// @ ensures err != nil ==> err.ErrorMem()
// @ decreases
Expand Down Expand Up @@ -775,7 +797,15 @@ func parseAddr(addrType AddrType, raw []byte) (res net.Addr, err error) {
"type", addrType, "len", addrType.Length())
}

// @ requires wildcard ==> acc(hostAddr.Mem(), _)
// (VerifiedSCION) In wildcard mode, the resources of an IP-typed address
// are taken component-wise instead of as a folded Mem() predicate: the
// caller may hold the bytes of the underlying IP only at wildcard amount
// (e.g. the router's internal IP), in which case Mem() cannot be folded
// at any concrete amount.
// @ requires wildcard && isIP(hostAddr) ==> acc(&hostAddr.(*net.IPAddr).IP, _) &&
// @ (forall i int :: { &hostAddr.(*net.IPAddr).IP[i] } 0 <= i && i < len(hostAddr.(*net.IPAddr).IP) ==>
// @ acc(&hostAddr.(*net.IPAddr).IP[i], _))
// @ requires wildcard && !isIP(hostAddr) ==> acc(hostAddr.Mem(), _)
// @ requires !wildcard ==> acc(hostAddr.Mem(), R19)
// @ ensures !wildcard ==> acc(hostAddr.Mem(), R20)
// @ ensures hostAddr === old(hostAddr)
Expand All @@ -798,13 +828,18 @@ func parseAddr(addrType AddrType, raw []byte) (res net.Addr, err error) {
// @ ensures err == nil && !wildcard && isIP(hostAddr) ==> (unfolding acc(hostAddr.Mem(), R20) in (!isIPv4(hostAddr) && !isIPv6(hostAddr) ==> len(hostAddr.(*net.IPAddr).IP) == len(b)))
// @ ensures err == nil && !wildcard && isIP(hostAddr) ==> (unfolding acc(hostAddr.Mem(), R20) in (isIPv6(hostAddr) && !isConvertibleToIPv4(hostAddr) ==> len(hostAddr.(*net.IPAddr).IP) == len(b)))
// @ ensures (err == nil) == (typeOf(hostAddr) == type[*net.IPAddr] || typeOf(hostAddr) == type[addr.HostSVC])
// @ ensures err == nil && isIP(hostAddr) && addrtyp == T4Ip ==> len(b) == 4
// @ ensures err == nil ==> addrtyp.Has3Bits()
// @ ensures err == nil && isHostSVC(hostAddr) ==> len(b) == 4
// @ ensures err == nil && wildcard && isIP(hostAddr) && addrtyp == T16Ip ==>
// @ len(b) == old(len(hostAddr.(*net.IPAddr).IP))
// @ decreases
func packAddr(hostAddr net.Addr /*@ , ghost wildcard bool @*/) (addrtyp AddrType, b []byte, err error) {
switch a := hostAddr.(type) {
case *net.IPAddr:
// @ ghost if wildcard {
// @ unfold acc(hostAddr.Mem(), _)
// @ } else {
// (VerifiedSCION) In wildcard mode the resources are already
// available component-wise (cf. the precondition).
// @ ghost if !wildcard {
// @ unfold acc(hostAddr.Mem(), R20)
// @ }
if ip := a.IP.To4( /*@ wildcard @*/ ); ip != nil {
Expand Down Expand Up @@ -977,16 +1012,19 @@ func (s *SCION) DecodeAddrHdr(data []byte) (res error) {
}

// computeChecksum computes the checksum with the SCION pseudo header.
// @ requires acc(&s.RawSrcAddr, R20) && acc(&s.RawDstAddr, R20)
// (VerifiedSCION) The permission amounts for the raw addresses are chosen
// so that they can be supplied from an unfolded ChecksumMem instance (which
// holds them at R25, resp. at wildcard amount for RawSrcAddr's bytes).
// @ requires acc(&s.RawSrcAddr, R30) && acc(&s.RawDstAddr, R30)
// @ requires len(s.RawSrcAddr) % 2 == 0 && len(s.RawDstAddr) % 2 == 0
// @ requires acc(&s.SrcIA, R20) && acc(&s.DstIA, R20)
// @ requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ requires acc(&s.SrcIA, R30) && acc(&s.DstIA, R30)
// @ requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)
// @ requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30)
// @ preserves acc(sl.Bytes(upperLayer, 0, len(upperLayer)), R20)
// @ ensures acc(&s.RawSrcAddr, R20) && acc(&s.RawDstAddr, R20)
// @ ensures acc(&s.SrcIA, R20) && acc(&s.DstIA, R20)
// @ ensures acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ ensures acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ ensures acc(&s.RawSrcAddr, R30) && acc(&s.RawDstAddr, R30)
// @ ensures acc(&s.SrcIA, R30) && acc(&s.DstIA, R30)
// @ ensures acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)
// @ ensures acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30)
// @ ensures s == nil ==> err != nil
// @ ensures len(s.RawDstAddr) == 0 ==> err != nil
// @ ensures len(s.RawSrcAddr) == 0 ==> err != nil
Expand All @@ -1006,15 +1044,15 @@ func (s *SCION) computeChecksum(upperLayer []byte, protocol uint8) (res uint16,
return folded, nil
}

// @ requires acc(&s.RawSrcAddr, R20) && acc(&s.RawDstAddr, R20)
// @ requires acc(&s.RawSrcAddr, R30) && acc(&s.RawDstAddr, R30)
// @ requires len(s.RawSrcAddr) % 2 == 0 && len(s.RawDstAddr) % 2 == 0
// @ requires acc(&s.SrcIA, R20) && acc(&s.DstIA, R20)
// @ requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ ensures acc(&s.RawSrcAddr, R20) && acc(&s.RawDstAddr, R20)
// @ ensures acc(&s.SrcIA, R20) && acc(&s.DstIA, R20)
// @ ensures acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ ensures acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ requires acc(&s.SrcIA, R30) && acc(&s.DstIA, R30)
// @ requires acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)
// @ requires acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30)
// @ ensures acc(&s.RawSrcAddr, R30) && acc(&s.RawDstAddr, R30)
// @ ensures acc(&s.SrcIA, R30) && acc(&s.DstIA, R30)
// @ ensures acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)
// @ ensures acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30)
// @ ensures len(s.RawDstAddr) == 0 ==> err != nil
// @ ensures len(s.RawSrcAddr) == 0 ==> err != nil
// @ ensures err != nil ==> err.ErrorMem()
Expand Down Expand Up @@ -1044,43 +1082,43 @@ func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (res uint32, er
}
// Address length is guaranteed to be a multiple of 2 by the protocol.
// @ ghost var rawSrcAddrLen int = len(s.RawSrcAddr)
// @ invariant acc(&s.RawSrcAddr, R20) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ invariant acc(&s.RawSrcAddr, R30) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)
// @ invariant len(s.RawSrcAddr) == rawSrcAddrLen
// @ invariant len(s.RawSrcAddr) % 2 == 0
// @ invariant i % 2 == 0
// @ invariant 0 <= i && i <= len(s.RawSrcAddr)
// @ decreases len(s.RawSrcAddr) - i
for i := 0; i < len(s.RawSrcAddr); i += 2 {
// @ requires acc(&s.RawSrcAddr, R20) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ requires acc(&s.RawSrcAddr, R30) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)
// @ requires 0 <= i && i < len(s.RawSrcAddr) && i % 2 == 0 && len(s.RawSrcAddr) % 2 == 0
// @ ensures acc(&s.RawSrcAddr, R20) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ ensures acc(&s.RawSrcAddr, R30) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)
// @ ensures s.RawSrcAddr === before(s.RawSrcAddr)
// @ decreases
// @ outline(
// @ unfold acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ unfold acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)
csum += uint32(s.RawSrcAddr[i]) << 8
csum += uint32(s.RawSrcAddr[i+1])
// @ fold acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ fold acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _)
// @ )
}
// @ ghost var rawDstAddrLen int = len(s.RawDstAddr)
// @ invariant acc(&s.RawDstAddr, R20) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ invariant acc(&s.RawDstAddr, R30) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30)
// @ invariant len(s.RawDstAddr) == rawDstAddrLen
// @ invariant len(s.RawDstAddr) % 2 == 0
// @ invariant i % 2 == 0
// @ invariant 0 <= i && i <= len(s.RawDstAddr)
// @ decreases len(s.RawDstAddr) - i
for i := 0; i < len(s.RawDstAddr); i += 2 {
// @ requires acc(&s.RawDstAddr, R20) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ requires acc(&s.RawDstAddr, R30) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30)
// @ requires 0 <= i && i < len(s.RawDstAddr) && i % 2 == 0 && len(s.RawDstAddr) % 2 == 0
// @ ensures acc(&s.RawDstAddr, R20) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ ensures acc(&s.RawDstAddr, R30) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30)
// @ ensures s.RawDstAddr === before(s.RawDstAddr)
// @ decreases
// @ outline(
// @ unfold acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ unfold acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30)
csum += uint32(s.RawDstAddr[i]) << 8
csum += uint32(s.RawDstAddr[i+1])
// @ fold acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ fold acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R30)
// @ )
}
l := uint32(length)
Expand Down
Loading
Loading