Skip to content

Commit

Permalink
Simplification of segLens (#356)
Browse files Browse the repository at this point in the history 
* simplification of SegLens

* remove preconditions on CombineSegLens

* fix verification error

* renaming
  • Loading branch information
@mlimbeck
mlimbeck authored Jun 14, 2024
1 parent b10cb4c commit 89fd7b6
Show file tree
Hide file tree
Showing 9 changed files with 412 additions and 431 deletions.
362 changes: 181 additions & 181 deletions pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
View file

Large diffs are not rendered by default.

43 changes: 22 additions & 21 deletions pkg/slayers/path/scion/raw.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -250,8 +250,9 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
//@ oldSeg1Len := int(s.PathMeta.SegLen[0])
//@ oldSeg2Len := int(s.PathMeta.SegLen[1])
//@ oldSeg3Len := int(s.PathMeta.SegLen[2])
//@ oldSegLen := LengthOfCurrSeg(oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ oldPrevSegLen := LengthOfPrevSeg(oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ oldSegs := io.CombineSegLens(oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ oldSegLen := oldSegs.LengthOfCurrSeg(oldCurrHfIdx)
//@ oldPrevSegLen := oldSegs.LengthOfPrevSeg(oldCurrHfIdx)
//@ oldOffset := HopFieldOffset(s.Base.NumINF, oldPrevSegLen, 0)
//@ fold acc(s.Base.Mem(), R56)
if err := s.Base.IncPath(); err != nil {
Expand All @@ -267,9 +268,9 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
//@ oldHfIdxSeg := oldCurrHfIdx-oldPrevSegLen
//@ WidenCurrSeg(ubuf, oldOffset + MetaLen, oldCurrInfIdx, oldHfIdxSeg,
//@ oldSegLen, MetaLen, MetaLen, len(ubuf))
//@ WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenRightSeg(ubuf, oldCurrInfIdx - 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSegs, MetaLen, MetaLen, len(ubuf))
//@ WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSegs, MetaLen, MetaLen, len(ubuf))
//@ WidenRightSeg(ubuf, oldCurrInfIdx - 1, oldSegs, MetaLen, MetaLen, len(ubuf))
//@ LenCurrSeg(tail, oldOffset, oldCurrInfIdx, oldHfIdxSeg, oldSegLen)
//@ oldAbsPkt := reveal s.absPkt(ubuf)
//@ sl.SplitRange_Bytes(ubuf, 0, MetaLen, HalfPerm)
Expand Down Expand Up @@ -297,24 +298,24 @@ func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
//@ IncCurrSeg(tail, oldOffset, oldCurrInfIdx, oldHfIdxSeg, oldSegLen)
//@ WidenCurrSeg(ubuf, oldOffset + MetaLen, oldCurrInfIdx, oldHfIdxSeg + 1,
//@ oldSegLen, MetaLen, MetaLen, len(ubuf))
//@ WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenRightSeg(ubuf, oldCurrInfIdx - 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenLeftSeg(ubuf, oldCurrInfIdx + 1, oldSegs, MetaLen, MetaLen, len(ubuf))
//@ WidenMidSeg(ubuf, oldCurrInfIdx + 2, oldSegs, MetaLen, MetaLen, len(ubuf))
//@ WidenRightSeg(ubuf, oldCurrInfIdx - 1, oldSegs, MetaLen, MetaLen, len(ubuf))
//@ assert reveal s.absPkt(ubuf) == AbsIncPath(oldAbsPkt)
//@ } else {
//@ segLen := LengthOfCurrSeg(currHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ prevSegLen := LengthOfPrevSeg(currHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ segLen := oldSegs.LengthOfCurrSeg(currHfIdx)
//@ prevSegLen := oldSegs.LengthOfPrevSeg(currHfIdx)
//@ offsetWithHops := HopFieldOffset(s.Base.NumINF, prevSegLen, MetaLen)
//@ hfIdxSeg := currHfIdx-prevSegLen
//@ XoverSegNotNone(tail, oldCurrInfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ XoverCurrSeg(tail, oldCurrInfIdx + 1, oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ XoverLeftSeg(tail, oldCurrInfIdx + 2, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ XoverMidSeg(tail, oldCurrInfIdx - 1, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ XoverRightSeg(tail, oldCurrInfIdx, oldCurrHfIdx, oldSeg1Len, oldSeg2Len, oldSeg3Len)
//@ XoverSegNotNone(tail, oldCurrInfIdx, oldSegs)
//@ XoverCurrSeg(tail, oldCurrInfIdx + 1, oldCurrHfIdx, oldSegs)
//@ XoverLeftSeg(tail, oldCurrInfIdx + 2, oldSegs)
//@ XoverMidSeg(tail, oldCurrInfIdx - 1, oldSegs)
//@ XoverRightSeg(tail, oldCurrInfIdx, oldCurrHfIdx, oldSegs)
//@ WidenCurrSeg(ubuf, offsetWithHops, currInfIdx, hfIdxSeg, segLen, MetaLen, MetaLen, len(ubuf))
//@ WidenLeftSeg(ubuf, currInfIdx + 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenMidSeg(ubuf, currInfIdx + 2, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenRightSeg(ubuf, currInfIdx - 1, oldSeg1Len, oldSeg2Len, oldSeg3Len, MetaLen, MetaLen, len(ubuf))
//@ WidenLeftSeg(ubuf, currInfIdx + 1, oldSegs, MetaLen, MetaLen, len(ubuf))
//@ WidenMidSeg(ubuf, currInfIdx + 2, oldSegs, MetaLen, MetaLen, len(ubuf))
//@ WidenRightSeg(ubuf, currInfIdx - 1, oldSegs, MetaLen, MetaLen, len(ubuf))
//@ assert reveal s.absPkt(ubuf) == AbsXover(oldAbsPkt)
//@ }

Expand Down Expand Up @@ -416,11 +417,11 @@ func (s *Raw) SetInfoField(info path.InfoField, idx int /*@, ghost ubuf []byte @
//@ seg1Len := int(s.PathMeta.SegLen[0])
//@ seg2Len := int(s.PathMeta.SegLen[1])
//@ seg3Len := int(s.PathMeta.SegLen[2])
//@ segLen := LengthOfCurrSeg(currHfIdx, seg1Len, seg2Len, seg3Len)
//@ prevSegLen := LengthOfPrevSeg(currHfIdx, seg1Len, seg2Len, seg3Len)
//@ segLens := io.CombineSegLens(seg1Len, seg2Len, seg3Len)
//@ segLen := segLens.LengthOfCurrSeg(currHfIdx)
//@ prevSegLen := segLens.LengthOfPrevSeg(currHfIdx)
//@ offset := HopFieldOffset(s.Base.NumINF, prevSegLen, MetaLen)
//@ hopfieldOffset := MetaLen + s.NumINF*path.InfoLen
//@ segLens := io.CombineSegLens(seg1Len, seg2Len, seg3Len)
if idx >= s.NumINF {
err := serrors.New("InfoField index out of bounds", "max", s.NumINF-1, "actual", idx)
//@ fold acc(s.Base.Mem(), R50)
Expand Down
Loading

0 comments on commit 89fd7b6

Please sign in to comment.