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 43 commits into
base: master
Choose a base branch
from
Draft

refactor prepareSCMP #425

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
43 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
00c875c
Prove RawSrcAddr evenness for the checksum fold
claude Jul 15, 2026
f632c76
Handle the nil internal-IP case in the RawSrcAddr evenness proof
claude Jul 16, 2026
295087d
Expose IsSupportedSerialization through the fold lemma
claude Jul 16, 2026
15ca603
Establish the non-nil layers quantifier for SerializeLayers
claude Jul 16, 2026
d31ee69
Restructure SerializeLayers spec to per-index preconditions
claude Jul 16, 2026
54e4ffb
Capture the payload layer in an interface-typed ghost for append iden…
claude Jul 16, 2026
53bba13
Drop payload Mem requirement from SerializeLayers to avoid append boxing
claude Jul 22, 2026
827a059
Re-trigger CI after a Gobra engine crash on verify-router
claude Jul 22, 2026
99d6c34
Flatten layerBufs construction to perturb the Gobra evaluator
claude Jul 22, 2026
5bee81a
Recover only MemSerialize post-serialization; leak ChecksumMem
claude Jul 22, 2026
266b2ce
Re-trigger CI after another transient Gobra engine crash
claude Jul 22, 2026
fa98c1b
Apply the SrcAddr wand with its exact stored shape
claude Jul 22, 2026
8094afb
Match the SrcAddr wand via a stable captured ghost term
claude Jul 22, 2026
f2c5f62
prepareSCMP: capture rawDst as stable ghost term for ExtractIPBytes wand
claude Jul 22, 2026
0795633
prepareSCMP: recover ChecksumMem's dst-addr fraction after serialize
claude Jul 22, 2026
3bcfd7a
prepareSCMP: reclaim dst-addr bytes via preserved MemSerialize, drop …
claude Jul 22, 2026
b24b459
gopacket: assert layers[0] != nil in SerializeLayers post for Seriali…
claude Jul 22, 2026
a5551b3
prepareSCMP: keep two empty-byte folds for SerializeLayers buffer mat…
claude Jul 22, 2026
307cd1a
prepareSCMP: materialize write-buffer bytes before SerializeLayers
claude Jul 22, 2026
d509f15
prepareSCMP: drop over-strict buffer assert, keep two empty-byte folds
claude Jul 22, 2026
8798db2
prepareSCMP: capture cleared buffer as ghost to reconnect SerializeLa…
claude Jul 22, 2026
beb0649
prepareSCMP: move MemSerialize unfold into isolated lemma to cut proo…
claude Jul 22, 2026
6780a7f
prepareSCMP: move IsSupportedPkt reveal bridge into isolated slayers …
claude Jul 22, 2026
e45b423
prepareSCMP: cut router verification time by hiding proof information
claude Jul 23, 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 ****/
113 changes: 79 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,17 @@ 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 && isIP(src) ==> s.SrcAddrType == T4Ip || s.SrcAddrType == T16Ip
// @ 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))
// (VerifiedSCION) An even-length source IP yields an even-length raw
// address (T4Ip gives length 4; T16Ip preserves the input length). Used
// by the router's prepareSCMP to fold the checksum predicate.
// @ ensures res == nil && wildcard && isIP(src) && old(len(src.(*net.IPAddr).IP)) % 2 == 0 ==>
// @ len(s.RawSrcAddr) % 2 == 0
// @ decreases
func (s *SCION) SetSrcAddr(src net.Addr /*@, ghost wildcard bool @*/) (res error) {
var err error
Expand All @@ -738,6 +764,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 +803,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 +834,19 @@ 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 && isIP(hostAddr) ==> addrtyp == T4Ip || addrtyp == T16Ip
// @ 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 +1019,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)), _)

@jcp19 jcp19 Aug 10, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

how can this verift later on if we pass _ as the permission amount here? Don't we have to recover that permission in order to reestablish the onwership of the entire raw pkt later on?

// @ 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 +1051,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 +1089,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