Skip to content
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

Proof of SetHopField #361

Merged
merged 31 commits into from
Aug 16, 2024
Merged

Proof of SetHopField #361

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
dcd5cca
proof of sethopfield and io-assumptions
mlimbeck Jun 19, 2024
48d5b63
fix syntax errors
mlimbeck Jun 19, 2024
10f95f0
fix termination measure
mlimbeck Jun 19, 2024
ec1769e
fix verification errors
mlimbeck Jun 19, 2024
3252934
simplifications and comments
mlimbeck Jun 20, 2024
1aee59c
fix syntax error
mlimbeck Jun 20, 2024
ca32450
feedback
mlimbeck Jun 27, 2024
3c10372
fix verification error
mlimbeck Jun 27, 2024
c408dbc
renaming
mlimbeck Jun 27, 2024
d7ad54a
space between arithmetic operands
mlimbeck Jun 27, 2024
6f7a7fd
increase timeout of path/scion
mlimbeck Jun 27, 2024
9d8d5a7
fix verification error
mlimbeck Jun 27, 2024
88aee17
Merge branch 'master' into markus-io-spec-setHopField-proof
mlimbeck Jul 9, 2024
575faee
test: parallelizeBranches for dependencies
mlimbeck Jul 9, 2024
1b74394
test: increase timeout for scion package to 20 min
mlimbeck Jul 9, 2024
76be847
test: increase timeout for scion package to 1h
mlimbeck Jul 9, 2024
b5def37
use parallelizeBranches only for scion package
mlimbeck Jul 9, 2024
580c387
stronger precondition for setHopfield
mlimbeck Jul 9, 2024
06e22bb
Revert "stronger precondition for setHopfield"
mlimbeck Jul 9, 2024
712cd18
test: scion pkg without parallelizeBranches
mlimbeck Jul 11, 2024
886876e
Revert "test: scion pkg without parallelizeBranches"
mlimbeck Jul 11, 2024
9c73a2d
Merge branch 'master' into markus-io-spec-setHopField-proof
mlimbeck Jul 11, 2024
d92ae1d
fix merging mistake
mlimbeck Jul 11, 2024
49d47fd
Merge branch 'master' into markus-io-spec-setHopField-proof
mlimbeck Jul 15, 2024
c85afa0
fix merge mistakes
mlimbeck Jul 15, 2024
2adfbe3
fix verification error
mlimbeck Jul 15, 2024
c18c7c9
Merge branch 'master' into markus-io-spec-setHopField-proof
jcp19 Jul 23, 2024
e3023ce
Drop `TemporaryAssumeForIO`
jcp19 Jul 23, 2024
5f5c334
Merge branch 'master' into markus-io-spec-setHopField-proof
jcp19 Aug 2, 2024
903dfc3
Apply suggestions from code review
jcp19 Aug 16, 2024
561902e
Update .github/workflows/gobra.yml
jcp19 Aug 16, 2024
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
24 changes: 7 additions & 17 deletions pkg/slayers/path/hopfield.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,16 +114,13 @@ func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
// @ preserves acc(h.Mem(), R10)
// @ preserves sl.Bytes(b, 0, HopLen)
// @ ensures err == nil
// @ ensures unfolding acc(h.Mem(), R10) in
// @ BytesToIO_HF(b, 0, 0, HopLen) == h.ToIO_HF()
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
// @ decreases
func (h *HopField) SerializeTo(b []byte) (err error) {
if len(b) < HopLen {
return serrors.New("buffer for HopField too short", "expected", MacLen, "actual", len(b))
}
//@ requires len(b) >= HopLen
//@ preserves acc(h.Mem(), R11)
//@ preserves sl.Bytes(b, 0, HopLen)
//@ decreases
//@ outline(
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
//@ unfold sl.Bytes(b, 0, HopLen)
//@ unfold acc(h.Mem(), R11)
b[0] = 0
Expand All @@ -139,24 +136,17 @@ func (h *HopField) SerializeTo(b []byte) (err error) {
//@ assert &b[4:6][0] == &b[4] && &b[4:6][1] == &b[5]
binary.BigEndian.PutUint16(b[4:6], h.ConsEgress)
//@ assert forall i int :: { &b[i] } 0 <= i && i < HopLen ==> acc(&b[i])
//@ fold sl.Bytes(b, 0, HopLen)
//@ fold acc(h.Mem(), R11)
//@ )
//@ requires len(b) >= HopLen
//@ preserves acc(h.Mem(), R11)
//@ preserves sl.Bytes(b, 0, HopLen)
//@ decreases
//@ outline(
//@ unfold sl.Bytes(b, 0, HopLen)
//@ unfold acc(h.Mem(), R11)
//@ assert forall i int :: { &h.Mac[:][i] } 0 <= i && i < len(h.Mac) ==>
//@ &h.Mac[i] == &h.Mac[:][i]
//@ assert forall i int :: { &b[6:6+MacLen][i] }{ &b[i+6] } 0 <= i && i < MacLen ==>
//@ &b[6:6+MacLen][i] == &b[i+6]
copy(b[6:6+MacLen], h.Mac[:] /*@, R11 @*/)
copy(b[6:6+MacLen], h.Mac[:] /*@, R47 @*/)
//@ assert forall i int :: {&h.Mac[:][i]} 0 <= i && i < MacLen ==> h.Mac[:][i] == b[6:6+MacLen][i]
//@ assert forall i int :: {&h.Mac[i]} 0 <= i && i < MacLen ==> h.Mac[:][i] == h.Mac[i]
//@ EqualBytesImplyEqualMac(b[6:6+MacLen], h.Mac)
//@ fold sl.Bytes(b, 0, HopLen)
//@ assert h.ToIO_HF() == BytesToIO_HF(b, 0, 0, HopLen)
//@ fold acc(h.Mem(), R11)
//@ )
return nil
}

Expand Down
128 changes: 126 additions & 2 deletions pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ func CombineBytesFromSegments(raw []byte, segs io.SegLens, p perm) {
ghost
requires 0 < p
requires segs.Valid()
requires PktLen(segs, MetaLen) <= len(raw)
requires MetaLen + numInf*path.InfoLen <= len(raw)
requires numInf == segs.NumInfoFields()
requires acc(sl.Bytes(raw, 0, len(raw)), p)
ensures acc(sl.Bytes(raw[:MetaLen], 0, MetaLen), p)
Expand Down Expand Up @@ -184,7 +184,7 @@ func SliceBytesIntoInfoFields(raw []byte, numInf int, segs io.SegLens, p perm) {
ghost
requires 0 < p
requires segs.Valid()
requires PktLen(segs, MetaLen) <= len(raw)
requires MetaLen + numInf*path.InfoLen <= len(raw)
requires numInf == segs.NumInfoFields()
requires acc(sl.Bytes(raw[:MetaLen], 0, MetaLen), p)
requires acc(sl.Bytes(InfofieldByteSlice(raw, 0), 0, path.InfoLen), p)
Expand Down Expand Up @@ -543,4 +543,128 @@ func MidSegEquality(raw []byte, currInfIdx int, segs io.SegLens) {
} else {
reveal MidSegWithInfo(nil, currInfIdx, segs, none[io.AbsInfoField])
}
}

// UpdateCurrSegHF specifies the relationship between different parts of the hopfield's raw bytes
// and their corresponding future, past and history segments in the abstract representation.
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
ghost
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), R50)
requires acc(sl.Bytes(hopfields[:currHfIdx*path.HopLen], 0, currHfIdx*path.HopLen), R50)
requires acc(sl.Bytes(hopfields[currHfIdx*path.HopLen:(currHfIdx+1)*path.HopLen], 0, path.HopLen), R50)
requires acc(sl.Bytes(hopfields[(currHfIdx+1)*path.HopLen:], 0, (segLen-(currHfIdx+1))*path.HopLen), R50)
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
decreases
pure func UpdateCurrSegHF(hopfields []byte, currHfIdx int, segLen int, inf io.AbsInfoField) bool {
return let currseg := CurrSegWithInfo(hopfields, currHfIdx, segLen, inf) in
len(currseg.Future) > 0 &&
currseg.Future[0] == path.BytesToIO_HF(hopfields[currHfIdx*path.HopLen:(currHfIdx+1)*path.HopLen], 0, 0, path.HopLen) &&
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
currseg.Future[1:] == hopFields(hopfields[(currHfIdx+1)*path.HopLen:], 0, 0, (segLen-(currHfIdx+1))) &&
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
currseg.Past == segPast(hopFields(hopfields[:currHfIdx*path.HopLen], 0, 0, currHfIdx)) &&
currseg.History == segHistory(hopFields(hopfields[:currHfIdx*path.HopLen], 0, 0, currHfIdx)) &&
currseg.AInfo == inf.AInfo &&
currseg.UInfo == inf.UInfo &&
currseg.ConsDir == inf.ConsDir &&
currseg.Peer == inf.Peer
}
jcp19 marked this conversation as resolved.
Show resolved Hide resolved

// SplitCurrSegHF verifies that the relationships defined in UpdateCurrSegHF hold
// for the current segment.
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
ghost
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
preserves acc(sl.Bytes(hopfields, 0, len(hopfields)), R49)
preserves acc(sl.Bytes(hopfields[:currHfIdx*path.HopLen], 0, currHfIdx*path.HopLen), R49)
preserves acc(sl.Bytes(hopfields[currHfIdx*path.HopLen:(currHfIdx+1)*path.HopLen], 0, path.HopLen), R49)
preserves acc(sl.Bytes(hopfields[(currHfIdx+1)*path.HopLen:], 0, (segLen-(currHfIdx+1))*path.HopLen), R49)
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
ensures UpdateCurrSegHF(hopfields, currHfIdx, segLen, inf)
decreases
func SplitCurrSegHFs(hopfields []byte, currHfIdx int, segLen int, inf io.AbsInfoField) {
currseg := reveal CurrSegWithInfo(hopfields, currHfIdx, segLen, inf)
unfold acc(sl.Bytes(hopfields, 0, len(hopfields)), R56)
unfold acc(sl.Bytes(hopfields[currHfIdx*path.HopLen:(currHfIdx+1)*path.HopLen], 0, path.HopLen), R56)
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
hf := hopFields(hopfields, 0, 0, segLen)
hopFieldsBytePositionsLemma(hopfields, 0, 0, segLen, R54)
reveal hopFieldsBytePositions(hopfields, 0, 0, segLen, hf)
assert len(currseg.Future) > 0
assert currseg.Future[0] == path.BytesToIO_HF(hopfields[currHfIdx*path.HopLen:(currHfIdx+1)*path.HopLen], 0, 0, path.HopLen)
HopFieldHelperLemma(hopfields, currHfIdx, segLen)
assert currseg.Past == segPast(hopFields(hopfields[:currHfIdx*path.HopLen], 0, 0, currHfIdx))
assert currseg.Future[0] == hf[currHfIdx]
assert hf[currHfIdx:][1:] == hf[currHfIdx+1:]
assert currseg.Future == hf[currHfIdx:]
assert currseg.Future[1:] == hopFields(hopfields[(currHfIdx+1)*path.HopLen:], 0, 0, (segLen-(currHfIdx+1)))
assert currseg.History == segHistory(hopFields(hopfields[:currHfIdx*path.HopLen], 0, 0, currHfIdx))
fold acc(sl.Bytes(hopfields[currHfIdx*path.HopLen:(currHfIdx+1)*path.HopLen], 0, path.HopLen), R56)
fold acc(sl.Bytes(hopfields, 0, len(hopfields)), R56)
}

// HopFieldHelperLemma verifies that we can split the abstract representation of hopfields into
// its future and past hopfields. This simplification helps in proving that the future and past
// hopfields remain unchanged when the current hopfield is modified.
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
ghost
requires 0 < segLen
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
preserves acc(sl.Bytes(hopfields, 0, len(hopfields)), R50)
preserves acc(sl.Bytes(hopfields[:currHfIdx*path.HopLen], 0, currHfIdx*path.HopLen), R50)
preserves acc(sl.Bytes(hopfields[(currHfIdx+1)*path.HopLen:], 0, (segLen-(currHfIdx+1))*path.HopLen), R50)
ensures hopFields(hopfields, 0, 0, segLen)[:currHfIdx] ==
hopFields(hopfields[:currHfIdx*path.HopLen], 0, 0, currHfIdx)
ensures hopFields(hopfields, 0, 0, segLen)[(currHfIdx+1):] ==
hopFields(hopfields[(currHfIdx+1)*path.HopLen:], 0, 0, (segLen-(currHfIdx+1)))
decreases
func HopFieldHelperLemma(hopfields []byte, currHfIdx int, segLen int) {
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
hf := hopFields(hopfields, 0, 0, segLen)
hopFieldsBytePositionsLemma(hopfields, 0, 0, segLen, R54)
reveal hopFieldsBytePositions(hopfields, 0, 0, segLen, hf)

hfPast := hopFields(hopfields, 0, 0, currHfIdx)
hopFieldsBytePositionsLemma(hopfields, 0, 0, currHfIdx, R54)
reveal hopFieldsBytePositions(hopfields, 0, 0, currHfIdx, hfPast)
widenHopFields(hopfields, 0, 0, currHfIdx, 0, currHfIdx*path.HopLen, R52)

hfFuture := hopFields(hopfields, (currHfIdx+1)*path.HopLen, 0, segLen-(currHfIdx+1))
hopFieldsBytePositionsLemma(hopfields, (currHfIdx+1)*path.HopLen, 0, segLen-(currHfIdx+1), R54)
reveal hopFieldsBytePositions(hopfields, (currHfIdx+1)*path.HopLen, 0, segLen-(currHfIdx+1), hfFuture)
widenHopFields(hopfields, (currHfIdx+1)*path.HopLen, 0, segLen-(currHfIdx+1),
(currHfIdx+1)*path.HopLen, segLen*path.HopLen, R52)
}

// SplitHopfields splits the raw bytes of a segment into its past hopfields,
// future hopfields and current hopfield.
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
ghost
requires 0 < p
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), p)
ensures acc(sl.Bytes(hopfields[:currHfIdx*path.HopLen], 0, currHfIdx*path.HopLen), p)
ensures acc(sl.Bytes(hopfields[currHfIdx*path.HopLen:(currHfIdx+1)*path.HopLen], 0, path.HopLen), p)
ensures acc(sl.Bytes(hopfields[(currHfIdx+1)*path.HopLen:], 0, (segLen-currHfIdx-1)*path.HopLen), p)
decreases
func SplitHopfields(hopfields []byte, currHfIdx int, segLen int, p perm) {
sl.SplitByIndex_Bytes(hopfields, 0, len(hopfields), currHfIdx*path.HopLen, p)
sl.SplitByIndex_Bytes(hopfields, currHfIdx*path.HopLen, len(hopfields), (currHfIdx+1)*path.HopLen, p)
sl.Reslice_Bytes(hopfields, 0, currHfIdx*path.HopLen, p)
sl.Reslice_Bytes(hopfields, currHfIdx*path.HopLen, (currHfIdx+1)*path.HopLen, p)
sl.Reslice_Bytes(hopfields, (currHfIdx+1)*path.HopLen, len(hopfields), p)
}

// CombineHopfields combines the past hopfields, future hopfields and current hopfield of a packet
// into a single slice of bytes.
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
ghost
requires 0 < p
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields[:currHfIdx*path.HopLen], 0, currHfIdx*path.HopLen), p)
requires acc(sl.Bytes(hopfields[currHfIdx*path.HopLen:(currHfIdx+1)*path.HopLen], 0, path.HopLen), p)
requires acc(sl.Bytes(hopfields[(currHfIdx+1)*path.HopLen:], 0, (segLen-currHfIdx-1)*path.HopLen), p)
ensures acc(sl.Bytes(hopfields, 0, len(hopfields)), p)
decreases
func CombineHopfields(hopfields []byte, currHfIdx int, segLen int, p perm) {
sl.Unslice_Bytes(hopfields, (currHfIdx+1)*path.HopLen, len(hopfields), p)
sl.Unslice_Bytes(hopfields, currHfIdx*path.HopLen, (currHfIdx+1)*path.HopLen, p)
sl.Unslice_Bytes(hopfields, 0, currHfIdx*path.HopLen, p)
sl.CombineAtIndex_Bytes(hopfields, currHfIdx*path.HopLen, len(hopfields), (currHfIdx+1)*path.HopLen, p)
sl.CombineAtIndex_Bytes(hopfields, 0, len(hopfields), currHfIdx*path.HopLen, p)
}
102 changes: 84 additions & 18 deletions pkg/slayers/path/scion/raw.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -530,34 +530,100 @@ func (s *Raw) GetCurrentHopField( /*@ ghost ubuf []byte @*/ ) (res path.HopField

// SetHopField updates the HopField at a given index.
// @ requires 0 <= idx
// @ preserves acc(s.Mem(ubuf), R20)
// @ preserves sl.Bytes(ubuf, 0, len(ubuf))
// @ ensures r != nil ==> r.ErrorMem()
// @ requires acc(s.Mem(ubuf), R20)
// @ requires sl.Bytes(ubuf, 0, len(ubuf))
// pres for IO:
// @ requires validPktMetaHdr(ubuf)
// @ requires s.GetBase(ubuf).EqAbsHeader(ubuf)
// @ requires len(s.absPkt(ubuf).CurrSeg.Future) > 0
mlimbeck marked this conversation as resolved.
Show resolved Hide resolved
// @ ensures acc(s.Mem(ubuf), R20)
// @ ensures sl.Bytes(ubuf, 0, len(ubuf))
// @ ensures r != nil ==> r.ErrorMem()
// posts for IO:
Copy link
Contributor

Choose a reason for hiding this comment

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

I'm starting to feel like these "posts for IO" annotations are a bit misleading, mostly because they are not about the IO behaviour, but instead about functional properties of the function. It just so happens that the correctness of the IO behaviour is predicated on the functional correctness of the packet processing. @Dspil would you be ok with us dropping these annotations, or do you think that it will still be useful for you to have the comments here?

// @ ensures r == nil ==>
// @ validPktMetaHdr(ubuf) &&
// @ s.GetBase(ubuf).EqAbsHeader(ubuf)
// @ ensures r == nil && idx == int(old(s.GetCurrHF(ubuf))) ==>
// @ let oldPkt := old(s.absPkt(ubuf)) in
// @ let newPkt := oldPkt.UpdateHopField(hop.ToIO_HF()) in
// @ s.absPkt(ubuf) == newPkt
// @ decreases
// @ #backend[exhaleMode(1)]
func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/) (r error) {
//@ share hop
// (VerifiedSCION) Due to an incompleteness (https://github.com/viperproject/gobra/issues/770),
// we introduce a temporary variable to be able to call `path.AbsMacArrayCongruence()`.
tmpHopField /*@@@*/ := hop
//@ path.AbsMacArrayCongruence(hop.Mac, tmpHopField.Mac)
// (VerifiedSCION) Cannot assert bounds of uint:
// https://github.com/viperproject/gobra/issues/192
//@ assume 0 <= hop.ConsIngress && 0 <= hop.ConsEgress
//@ fold hop.Mem()
//@ unfold acc(s.Mem(ubuf), R20)
//@ unfold acc(s.Base.Mem(), R20)
//@ assume 0 <= tmpHopField.ConsIngress && 0 <= tmpHopField.ConsEgress
//@ fold acc(tmpHopField.Mem(), R9)
//@ reveal validPktMetaHdr(ubuf)
//@ unfold acc(s.Mem(ubuf), R50)
//@ unfold acc(s.Base.Mem(), R50)
//@ currInfIdx := int(s.PathMeta.CurrINF)
//@ currHfIdx := int(s.PathMeta.CurrHF)
//@ seg1Len := int(s.PathMeta.SegLen[0])
//@ seg2Len := int(s.PathMeta.SegLen[1])
//@ seg3Len := int(s.PathMeta.SegLen[2])
//@ segLens := io.CombineSegLens(seg1Len, seg2Len, seg3Len)
//@ segLen := segLens.LengthOfCurrSeg(idx)
//@ prevSegLen := segLens.LengthOfPrevSeg(idx)
//@ offset := HopFieldOffset(s.Base.NumINF, prevSegLen, MetaLen)
//@ hopfieldOffset := MetaLen + s.NumINF*path.InfoLen
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
if idx >= s.NumHops {
// (VerifiedSCION) introduced `err`
err := serrors.New("HopField index out of bounds", "max", s.NumHops-1, "actual", idx)
//@ fold acc(s.Base.Mem(), R20)
//@ fold acc(s.Mem(ubuf), R20)
//@ fold acc(s.Base.Mem(), R50)
//@ fold acc(s.Mem(ubuf), R50)
return err
}
hopOffset := MetaLen + s.NumINF*path.InfoLen + idx*path.HopLen
//@ sl.SplitRange_Bytes(ubuf, 0, len(s.Raw), writePerm)
//@ assert sl.Bytes(s.Raw, 0, len(s.Raw))
//@ sl.SplitRange_Bytes(s.Raw, hopOffset, hopOffset+path.HopLen, writePerm)
ret := hop.SerializeTo(s.Raw[hopOffset : hopOffset+path.HopLen])
//@ sl.CombineRange_Bytes(s.Raw, hopOffset, hopOffset+path.HopLen, writePerm)
//@ sl.CombineRange_Bytes(ubuf, 0, len(s.Raw), writePerm)
//@ fold acc(s.Base.Mem(), R20)
//@ fold acc(s.Mem(ubuf), R20)

//@ SliceBytesIntoSegments(ubuf, segLens, HalfPerm)
//@ SliceBytesIntoInfoFields(ubuf[:hopfieldOffset], s.NumINF, segLens, R40)

//@ ValidPktMetaHdrSublice(ubuf, MetaLen)
//@ inf := path.BytesToAbsInfoField(InfofieldByteSlice(ubuf, currInfIdx), 0)
//@ hfIdxSeg := idx-prevSegLen
//@ currHopfields := HopfieldsByteSlice(ubuf, currInfIdx, segLens)
//@ ghost if idx == currHfIdx {
//@ CurrSegEquality(ubuf, offset, currInfIdx, hfIdxSeg, segLen)
//@ LeftSegEquality(ubuf, currInfIdx+1, segLens)
//@ MidSegEquality(ubuf, currInfIdx+2, segLens)
//@ RightSegEquality(ubuf, currInfIdx-1, segLens)
//@ reveal s.absPkt(ubuf)
//@ SplitHopfields(currHopfields, hfIdxSeg, segLen, R0)
//@ SplitCurrSegHFs(currHopfields, hfIdxSeg, segLen, inf)
//@ SplitHopfields(currHopfields, hfIdxSeg, segLen, R0)
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
//@ } else {
//@ sl.SplitRange_Bytes(ubuf[offset:offset+segLen*path.HopLen], hfIdxSeg*path.HopLen,
//@ (hfIdxSeg+1)*path.HopLen, HalfPerm)
//@ }
//@ sl.SplitRange_Bytes(ubuf, hopOffset, hopOffset+path.HopLen, HalfPerm)
ret := tmpHopField.SerializeTo(s.Raw[hopOffset : hopOffset+path.HopLen])
//@ sl.CombineRange_Bytes(ubuf, hopOffset, hopOffset+path.HopLen, HalfPerm)
//@ ValidPktMetaHdrSublice(ubuf, MetaLen)
//@ assert reveal validPktMetaHdr(ubuf)
//@ ghost if idx == currHfIdx {
//@ CombineHopfields(currHopfields, hfIdxSeg, segLen, R0)
//@ SplitCurrSegHFs(currHopfields, hfIdxSeg, segLen, inf)
//@ CombineHopfields(currHopfields, hfIdxSeg, segLen, R0)
//@ CurrSegEquality(ubuf, offset, currInfIdx, hfIdxSeg, segLen)
//@ LeftSegEquality(ubuf, currInfIdx+1, segLens)
//@ MidSegEquality(ubuf, currInfIdx+2, segLens)
//@ RightSegEquality(ubuf, currInfIdx-1, segLens)
//@ reveal s.absPkt(ubuf)
//@ assert s.absPkt(ubuf).CurrSeg.Future ==
//@ seq[io.IO_HF]{tmpHopField.ToIO_HF()} ++ old(s.absPkt(ubuf).CurrSeg.Future[1:])
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
//@ } else {
//@ sl.CombineRange_Bytes(ubuf[offset:offset+segLen*path.HopLen], hfIdxSeg*path.HopLen,
//@ (hfIdxSeg+1)*path.HopLen, HalfPerm)
//@ }
//@ CombineBytesFromInfoFields(ubuf[:hopfieldOffset], s.NumINF, segLens, R40)
//@ CombineBytesFromSegments(ubuf, segLens, HalfPerm)
//@ fold acc(s.Base.Mem(), R50)
//@ fold acc(s.Mem(ubuf), R50)
return ret
}

Expand Down
43 changes: 18 additions & 25 deletions pkg/slayers/path/scion/raw_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -232,31 +232,21 @@ pure func hopFields(
}

ghost
requires -1 <= currHfIdx && currHfIdx < len(hopfields)
ensures len(res) == currHfIdx + 1
decreases currHfIdx + 1
pure func segPast(hopfields seq[io.IO_HF], currHfIdx int) (res seq[io.IO_HF]) {
return currHfIdx == -1 ?
seq[io.IO_HF]{} :
seq[io.IO_HF]{hopfields[currHfIdx]} ++ segPast(hopfields, currHfIdx - 1)
ensures len(res) == len(hopfields)
decreases len(hopfields)
pure func segPast(hopfields seq[io.IO_HF]) (res seq[io.IO_HF]) {
return len(hopfields) == 0 ? seq[io.IO_HF]{} :
seq[io.IO_HF]{hopfields[len(hopfields)-1]} ++ segPast(
hopfields[:len(hopfields)-1])
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
seq[io.IO_HF]{hopfields[len(hopfields)-1]} ++ segPast(
hopfields[:len(hopfields)-1])
seq[io.IO_HF]{hopfields[len(hopfields)-1]} ++ segPast(hopfields[:len(hopfields)-1])

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

There's an interesting feature in Gobra: the ++ operator cannot be at the beginning or the end of a line. Given that the entire line is quite long, this is the best place to split it.

}

ghost
requires 0 <= currHfIdx && currHfIdx <= len(hopfields)
ensures len(res) == len(hopfields) - currHfIdx
decreases len(hopfields) - currHfIdx
pure func segFuture(hopfields seq[io.IO_HF], currHfIdx int) (res seq[io.IO_HF]) {
return currHfIdx == len(hopfields) ? seq[io.IO_HF]{} :
seq[io.IO_HF]{hopfields[currHfIdx]} ++ segFuture(hopfields, currHfIdx + 1)
}

ghost
requires -1 <= currHfIdx && currHfIdx < len(hopfields)
ensures len(res) == currHfIdx + 1
decreases currHfIdx + 1
pure func segHistory(hopfields seq[io.IO_HF], currHfIdx int) (res seq[io.IO_ahi]) {
return currHfIdx == -1 ? seq[io.IO_ahi]{} :
seq[io.IO_ahi]{hopfields[currHfIdx].Toab()} ++ segHistory(hopfields, currHfIdx - 1)
ensures len(res) == len(hopfields)
decreases len(hopfields)
pure func segHistory(hopfields seq[io.IO_HF]) (res seq[io.IO_ahi]) {
return len(hopfields) == 0 ? seq[io.IO_ahi]{} :
seq[io.IO_ahi]{hopfields[len(hopfields)-1].Toab()} ++ segHistory(
hopfields[:len(hopfields)-1])
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
seq[io.IO_ahi]{hopfields[len(hopfields)-1].Toab()} ++ segHistory(
hopfields[:len(hopfields)-1])
seq[io.IO_ahi]{hopfields[len(hopfields)-1].Toab()} ++ segHistory(hopfields[:len(hopfields)-1])

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

There's an interesting feature in Gobra: the ++ operator cannot be at the beginning or the end of a line. Given that the entire line is quite long, this is the best place to split it.

}

ghost
Expand All @@ -283,9 +273,9 @@ pure func segment(raw []byte,
UInfo : uinfo,
ConsDir : consDir,
Peer : peer,
Past : segPast(hopfields, currHfIdx - 1),
Future : segFuture(hopfields, currHfIdx),
History : segHistory(hopfields, currHfIdx - 1),
Past : segPast(hopfields[:currHfIdx]),
Future : hopfields[currHfIdx:],
History : segHistory(hopfields[:currHfIdx]),
}
}

Expand Down Expand Up @@ -754,6 +744,9 @@ decreases
func IncCurrSeg(raw []byte, offset int, currInfIdx int, currHfIdx int, segLen int) {
currseg := reveal CurrSeg(raw, offset, currInfIdx, currHfIdx, segLen, 0)
incseg := reveal CurrSeg(raw, offset, currInfIdx, currHfIdx+1, segLen, 0)
hf := hopFields(raw, offset, 0, segLen)
hfPast := hf[:currHfIdx+1]
assert hfPast[:len(hfPast)-1] == hf[:currHfIdx]
assert currseg.AInfo == incseg.AInfo
assert currseg.UInfo == incseg.UInfo
assert currseg.ConsDir == incseg.ConsDir
Expand Down
Loading
Loading