Skip to content

Commit

Permalink
Stabilize path/scion (#370)
Browse files Browse the repository at this point in the history 
* test

* replace hopFieldsBytePositions and by recursive functions

* renaming and public lemmas without perm param

* fix mistake

* Apply suggestions from code review

Co-authored-by: João Pereira <[email protected]>

* space around arith. operators

---------

Co-authored-by: mlimbeck <[email protected]>
Co-authored-by: Markus Limbeck <[email protected]>
  • Loading branch information
@jcp19 @mlimbeck
3 people authored Aug 27, 2024
1 parent 97c98ff commit 445bbad
Show file tree
Hide file tree
Showing 2 changed files with 119 additions and 119 deletions.
59 changes: 6 additions & 53 deletions pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -593,61 +593,14 @@ func EstablishBytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf
currseg := reveal CurrSegWithInfo(hopfields, currHfIdx, segLen, inf)
currHfStart := currHfIdx * path.HopLen
currHfEnd := currHfStart + path.HopLen
unfold acc(sl.Bytes(hopfields, 0, len(hopfields)), R56)
unfold acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), R56)
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[currHfStart:currHfEnd], 0, 0, path.HopLen)
splitHopFieldsInPastAndFuture(hopfields, currHfIdx, segLen)
assert currseg.Past == segPast(hopFields(hopfields[:currHfStart], 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[currHfEnd:], 0, 0, (segLen - currHfIdx- 1))
assert currseg.History == segHistory(hopFields(hopfields[:currHfStart], 0, 0, currHfIdx))
fold acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), R56)
fold acc(sl.Bytes(hopfields, 0, len(hopfields)), R56)
}

// `splitHopFieldsInPastAndFuture` shows that the raw bytes containing all hopfields
// can be split into two slices, one that exclusively contains all past hopfields and another
// that exclusively contains all future ones. This helps in proving that the future and past
// hopfields remain unchanged when the current hopfield is modified.
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 let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
acc(sl.Bytes(hopfields[:currHfStart], 0, currHfStart), R50) &&
acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), R50)
ensures let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
hopFields(hopfields, 0, 0, segLen)[:currHfIdx] ==
hopFields(hopfields[:currHfStart], 0, 0, currHfIdx) &&
hopFields(hopfields, 0, 0, segLen)[currHfIdx + 1:] ==
hopFields(hopfields[currHfEnd:], 0, 0, segLen - currHfIdx - 1)
decreases
func splitHopFieldsInPastAndFuture(hopfields []byte, currHfIdx int, segLen int) {
currHfStart := currHfIdx * path.HopLen
currHfEnd := currHfStart + path.HopLen
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)
HopsFromSuffixOfRawMatchSuffixOfHops(hopfields, 0, 0, segLen, currHfIdx)
AlignHopsOfRawWithOffsetAndIndex(hopfields, 0, currHfIdx + 1, segLen, currHfIdx + 1)
HopsFromPrefixOfRawMatchPrefixOfHops(hopfields, 0, 0, segLen, currHfIdx + 1)
HopsFromPrefixOfRawMatchPrefixOfHops(hopfields, 0, 0, segLen, currHfIdx)
widenHopFields(hopfields, 0, 0, currHfIdx, 0, currHfStart, R52)

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

// `SplitHopfields` splits the permission to the raw bytes of a segment into the permission
Expand Down
179 changes: 113 additions & 66 deletions pkg/slayers/path/scion/raw_spec.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -237,17 +237,17 @@ 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])
seq[io.IO_HF]{hopfields[len(hopfields) - 1]} ++ segPast(
hopfields[:len(hopfields) - 1])
}

ghost
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])
seq[io.IO_ahi]{hopfields[len(hopfields) - 1].Toab()} ++ segHistory(
hopfields[:len(hopfields) - 1])
}

ghost
Expand Down Expand Up @@ -385,7 +385,7 @@ pure func (s *Raw) absPkt(raw []byte) (res io.IO_pkt2) {
let numINF := segs.NumInfoFields() in
let offset := HopFieldOffset(numINF, prevSegLen, MetaLen) in
io.IO_Packet2 {
CurrSeg : CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen),
CurrSeg : CurrSeg(raw, offset, currInfIdx, currHfIdx - prevSegLen, segLen, MetaLen),
LeftSeg : LeftSeg(raw, currInfIdx + 1, segs, MetaLen),
MidSeg : MidSeg(raw, currInfIdx + 2, segs, MetaLen),
RightSeg : RightSeg(raw, currInfIdx - 1, segs, MetaLen),
Expand Down Expand Up @@ -536,7 +536,7 @@ pure func (s *Raw) CorrectlyDecodedInfWithIdx(ub []byte, idx int, info path.Info
return unfolding acc(s.Mem(ub), _) in
unfolding acc(s.Base.Mem(), _) in
let infOffset := MetaLen + idx*path.InfoLen in
infOffset+path.InfoLen <= len(ub) &&
infOffset + path.InfoLen <= len(ub) &&
info.ToAbsInfoField() ==
reveal path.BytesToAbsInfoField(ub, infOffset)
}
Expand All @@ -550,8 +550,8 @@ decreases
pure func (s *Raw) CorrectlyDecodedInf(ub []byte, info path.InfoField) bool {
return unfolding acc(s.Mem(ub), _) in
unfolding acc(s.Base.Mem(), _) in
let infOffset := MetaLen + int(s.Base.PathMeta.CurrINF)*path.InfoLen in
infOffset+path.InfoLen <= len(ub) &&
let infOffset := MetaLen + int(s.Base.PathMeta.CurrINF) * path.InfoLen in
infOffset + path.InfoLen <= len(ub) &&
info.ToAbsInfoField() ==
reveal path.BytesToAbsInfoField(ub, infOffset)
}
Expand All @@ -565,8 +565,8 @@ decreases
pure func (s *Raw) CorrectlyDecodedHfWithIdx(ub []byte, idx int, hop path.HopField) bool {
return unfolding acc(s.Mem(ub), _) in
unfolding acc(s.Base.Mem(), _) in
let hopOffset := MetaLen + int(s.NumINF)*path.InfoLen + idx*path.HopLen in
hopOffset+path.HopLen <= len(ub) &&
let hopOffset := MetaLen + int(s.NumINF) * path.InfoLen + idx * path.HopLen in
hopOffset + path.HopLen <= len(ub) &&
hop.ToIO_HF() == path.BytesToIO_HF(ub, 0, hopOffset, len(ub))
}

Expand All @@ -579,9 +579,9 @@ decreases
pure func (s *Raw) CorrectlyDecodedHf(ub []byte, hop path.HopField) bool {
return unfolding acc(s.Mem(ub), _) in
unfolding acc(s.Base.Mem(), _) in
let hopOffset := MetaLen + int(s.NumINF)*path.InfoLen +
int(s.Base.PathMeta.CurrHF)*path.HopLen in
hopOffset+path.HopLen <= len(ub) &&
let hopOffset := MetaLen + int(s.NumINF) * path.InfoLen +
int(s.Base.PathMeta.CurrHF) * path.HopLen in
hopOffset + path.HopLen <= len(ub) &&
hop.ToIO_HF() == path.BytesToIO_HF(ub, 0, hopOffset, len(ub))
}

Expand All @@ -607,7 +607,7 @@ func (s *Raw) LastHopLemma(ubuf []byte) {
numINF := segs.NumInfoFields()
offset := HopFieldOffset(numINF, prevSegLen, MetaLen)
pkt := reveal s.absPkt(ubuf)
assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen)
assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset, currInfIdx, currHfIdx - prevSegLen, segLen, MetaLen)
assert len(pkt.CurrSeg.Future) == 1
}

Expand All @@ -634,7 +634,7 @@ func (s *Raw) XoverLemma(ubuf []byte) {
numINF := segs.NumInfoFields()
offset := HopFieldOffset(numINF, prevSegLen, MetaLen)
pkt := reveal s.absPkt(ubuf)
assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset, currInfIdx, currHfIdx-prevSegLen, segLen, MetaLen)
assert pkt.CurrSeg == reveal CurrSeg(ubuf, offset, currInfIdx, currHfIdx - prevSegLen, segLen, MetaLen)
assert pkt.LeftSeg == reveal LeftSeg(ubuf, currInfIdx + 1, segs, MetaLen)
assert len(pkt.CurrSeg.Future) == 1
assert pkt.LeftSeg != none[io.IO_seg2]
Expand Down Expand Up @@ -686,18 +686,12 @@ func (s *Raw) DecodingLemma(ubuf []byte, info path.InfoField, hop path.HopField)
prevSegLen := segs.LengthOfPrevSeg(currHfIdx)
numINF := segs.NumInfoFields()
offset := HopFieldOffset(numINF, prevSegLen, MetaLen)
hfIdxSeg := currHfIdx-prevSegLen
hfIdxSeg := currHfIdx - prevSegLen
reveal s.CorrectlyDecodedInf(ubuf, info)
reveal s.CorrectlyDecodedHf(ubuf, hop)
pkt := reveal s.absPkt(ubuf)
currseg := reveal CurrSeg(ubuf, offset, currInfIdx, hfIdxSeg, segLen, MetaLen)
hopFields := hopFields(ubuf, offset, 0, segLen)
hopFieldsBytePositionsLemma(ubuf, offset, 0, segLen, R54)
reveal hopFieldsBytePositions(ubuf, offset, 0, segLen, hopFields)
assert currseg.Future[0] == hopFields[hfIdxSeg]
assert hopFields[hfIdxSeg] ==
path.BytesToIO_HF(ubuf, 0, offset + path.HopLen * hfIdxSeg, len(ubuf))
assert currseg.Future[0] == path.BytesToIO_HF(ubuf, 0, offset + path.HopLen * hfIdxSeg, len(ubuf))
reveal s.absPkt(ubuf)
reveal CurrSeg(ubuf, offset, currInfIdx, hfIdxSeg, segLen, MetaLen)
HopsFromPrefixOfRawMatchPrefixOfHops(ubuf, offset, 0, segLen, hfIdxSeg)
assert reveal s.EqAbsInfoField(s.absPkt(ubuf), info.ToAbsInfoField())
assert reveal s.EqAbsHopField(s.absPkt(ubuf), hop.ToIO_HF())
}
Expand All @@ -722,11 +716,11 @@ requires PktLen(segs, 0) <= len(raw)
requires 0 <= currInfIdx && currInfIdx < 2
requires 1 <= currInfIdx ==> 0 < segs.Seg3Len
preserves acc(sl.Bytes(raw, 0, len(raw)), R56)
ensures LeftSeg(raw, currInfIdx+1, segs, 0) != none[io.IO_seg3]
ensures LeftSeg(raw, currInfIdx + 1, segs, 0) != none[io.IO_seg3]
ensures RightSeg(raw, currInfIdx, segs, 0) != none[io.IO_seg3]
decreases
func XoverSegNotNone(raw []byte, currInfIdx int, segs io.SegLens) {
reveal LeftSeg(raw, currInfIdx+1, segs, 0)
reveal LeftSeg(raw, currInfIdx + 1, segs, 0)
reveal RightSeg(raw, currInfIdx, segs, 0)
}

Expand All @@ -738,15 +732,15 @@ requires 0 <= currHfIdx && currHfIdx < segLen
requires 0 <= currInfIdx && currInfIdx < 3
preserves acc(sl.Bytes(raw, 0, len(raw)), R56)
preserves len(CurrSeg(raw, offset, currInfIdx, currHfIdx, segLen, 0).Future) > 0
ensures CurrSeg(raw, offset, currInfIdx, currHfIdx+1, segLen, 0) ==
ensures CurrSeg(raw, offset, currInfIdx, currHfIdx + 1, segLen, 0) ==
absIncPathSeg(CurrSeg(raw, offset, currInfIdx, currHfIdx, segLen, 0))
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)
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]
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 All @@ -762,22 +756,22 @@ requires segs.Valid()
requires 0 < segs.Seg2Len
requires PktLen(segs, 0) <= len(raw)
requires 1 <= currInfIdx && currInfIdx < 3
requires 1 == currInfIdx ==> currHfIdx+1 == segs.Seg1Len
requires 2 == currInfIdx ==> 0 < segs.Seg3Len && currHfIdx+1 == segs.Seg1Len + segs.Seg2Len
requires 1 == currInfIdx ==> currHfIdx + 1 == segs.Seg1Len
requires 2 == currInfIdx ==> 0 < segs.Seg3Len && currHfIdx + 1 == segs.Seg1Len + segs.Seg2Len
requires PktLen(segs, 0) <= len(raw)
preserves acc(sl.Bytes(raw, 0, len(raw)), R56)
preserves LeftSeg(raw, currInfIdx, segs, 0) != none[io.IO_seg3]
ensures
let prevSegLen := segs.LengthOfPrevSeg(currHfIdx+1) in
let segLen := segs.LengthOfCurrSeg(currHfIdx+1) in
let prevSegLen := segs.LengthOfPrevSeg(currHfIdx + 1) in
let segLen := segs.LengthOfCurrSeg(currHfIdx + 1) in
let numInf := segs.NumInfoFields() in
let offset := HopFieldOffset(numInf, prevSegLen, 0) in
CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen+1, segLen, 0) ==
CurrSeg(raw, offset, currInfIdx, currHfIdx - prevSegLen + 1, segLen, 0) ==
get(LeftSeg(raw, currInfIdx, segs, 0))
decreases
func XoverCurrSeg(raw []byte, currInfIdx int, currHfIdx int, segs io.SegLens) {
prevSegLen := segs.LengthOfPrevSeg(currHfIdx+1)
segLen := segs.LengthOfCurrSeg(currHfIdx+1)
prevSegLen := segs.LengthOfPrevSeg(currHfIdx + 1)
segLen := segs.LengthOfCurrSeg(currHfIdx + 1)
numInf := segs.NumInfoFields()
offset := HopFieldOffset(numInf, prevSegLen, 0)
currseg := reveal CurrSeg(raw, offset, currInfIdx, 0, segLen, 0)
Expand Down Expand Up @@ -806,11 +800,11 @@ requires PktLen(segs, 0) <= len(raw)
requires -1 <= currInfIdx && currInfIdx < 1
requires 0 == currInfIdx ==> 0 < segs.Seg3Len
preserves acc(sl.Bytes(raw, 0, len(raw)), R56)
ensures MidSeg(raw, currInfIdx+4, segs, 0) ==
ensures MidSeg(raw, currInfIdx + 4, segs, 0) ==
RightSeg(raw, currInfIdx, segs, 0)
decreases
func XoverMidSeg(raw []byte, currInfIdx int, segs io.SegLens) {
midseg := reveal MidSeg(raw, currInfIdx+4, segs, 0)
midseg := reveal MidSeg(raw, currInfIdx + 4, segs, 0)
rightseg := reveal RightSeg(raw, currInfIdx, segs, 0)
assert midseg == rightseg
}
Expand All @@ -820,8 +814,8 @@ requires segs.Valid()
requires 0 < segs.Seg2Len
requires PktLen(segs, 0) <= len(raw)
requires 0 <= currInfIdx && currInfIdx < 2
requires 0 == currInfIdx ==> currHfIdx+1 == segs.Seg1Len
requires 1 == currInfIdx ==> 0 < segs.Seg3Len && currHfIdx+1 == segs.Seg1Len + segs.Seg2Len
requires 0 == currInfIdx ==> currHfIdx + 1 == segs.Seg1Len
requires 1 == currInfIdx ==> 0 < segs.Seg3Len && currHfIdx + 1 == segs.Seg1Len + segs.Seg2Len
requires PktLen(segs, 0) <= len(raw)
preserves acc(sl.Bytes(raw, 0, len(raw)), R56)
preserves RightSeg(raw, currInfIdx, segs, 0) != none[io.IO_seg3]
Expand All @@ -830,7 +824,7 @@ ensures
let segLen := segs.LengthOfCurrSeg(currHfIdx) in
let numInf := segs.NumInfoFields() in
let offset := HopFieldOffset(numInf, prevSegLen, 0) in
let currseg := CurrSeg(raw, offset, currInfIdx, currHfIdx-prevSegLen, segLen, 0) in
let currseg := CurrSeg(raw, offset, currInfIdx, currHfIdx - prevSegLen, segLen, 0) in
len(currseg.Future) > 0 &&
get(RightSeg(raw, currInfIdx, segs, 0)) == absIncPathSeg(currseg)
decreases
Expand All @@ -850,38 +844,91 @@ func XoverRightSeg(raw []byte, currInfIdx int, currHfIdx int, segs io.SegLens) {
}

ghost
opaque
requires 0 <= offset
requires 0 <= currHFIdx && currHFIdx <= segLen
requires len(hops) == segLen - currHFIdx
requires 0 <= currHfIdx && currHfIdx <= end
requires end <= segLen
requires offset + path.HopLen * segLen <= len(raw)
requires acc(sl.Bytes(raw, 0, len(raw)), R56)
preserves acc(sl.Bytes(raw, 0, len(raw)), R54)
ensures hopFields(raw, offset, currHfIdx, segLen)[:end - currHfIdx] ==
hopFields(raw, offset, currHfIdx, end)
decreases
pure func hopFieldsBytePositions(raw []byte, offset int, currHFIdx int, segLen int, hops seq[io.IO_HF]) bool {
return forall i int :: { hops[i] } 0 <= i && i < len(hops) ==>
hops[i] == path.BytesToIO_HF(raw, 0, offset + path.HopLen * (currHFIdx + i), len(raw))
func HopsFromSuffixOfRawMatchSuffixOfHops(raw []byte, offset int, currHfIdx int, segLen int, end int) {
hopsFromSuffixOfRawMatchSuffixOfHops(raw, offset, currHfIdx, segLen, end, R54)
}

ghost
requires R55 < p
requires 0 <= offset
requires 0 <= currHFIdx && currHFIdx <= segLen
requires 0 <= currHfIdx && currHfIdx <= end
requires end <= segLen
requires offset + path.HopLen * segLen <= len(raw)
preserves acc(sl.Bytes(raw, 0, len(raw)), p)
ensures hopFieldsBytePositions(raw, offset, currHFIdx, segLen, hopFields(raw, offset, currHFIdx, segLen))
decreases segLen - currHFIdx
func hopFieldsBytePositionsLemma(
raw []byte,
offset int,
currHFIdx int,
segLen int,
p perm) {
newP := (p + R55)/2
hopfields := hopFields(raw, offset, currHFIdx, segLen)
if (currHFIdx != segLen) {
hopFieldsBytePositionsLemma(raw, offset, currHFIdx + 1, segLen, newP)
hopfieldsInc := hopFields(raw, offset, currHFIdx + 1, segLen)
assert reveal hopFieldsBytePositions(raw, offset, currHFIdx + 1, segLen, hopfieldsInc)
ensures hopFields(raw, offset, currHfIdx, segLen)[:end - currHfIdx] ==
hopFields(raw, offset, currHfIdx, end)
decreases end - currHfIdx
func hopsFromSuffixOfRawMatchSuffixOfHops(raw []byte, offset int, currHfIdx int, segLen int, end int, p perm) {
if (currHfIdx != end) {
newP := (p + R55)/2
hopsFromSuffixOfRawMatchSuffixOfHops(raw, offset, currHfIdx + 1, segLen, end, newP)
}
}

ghost
requires 0 <= offset
requires 0 <= start
requires 0 <= currHfIdx && currHfIdx <= segLen - start
requires offset + path.HopLen * segLen <= len(raw)
preserves acc(sl.Bytes(raw, 0, len(raw)), R54)
ensures hopFields(raw, offset, currHfIdx, segLen)[start:] ==
hopFields(raw, offset, currHfIdx + start, segLen)
decreases
func HopsFromPrefixOfRawMatchPrefixOfHops(raw []byte, offset int, currHfIdx int, segLen int, start int) {
hopsFromPrefixOfRawMatchPrefixOfHops(raw, offset, currHfIdx, segLen, start, R54)
}

ghost
requires R55 < p
requires 0 <= offset
requires 0 <= start
requires 0 <= currHfIdx && currHfIdx <= segLen - start
requires offset + path.HopLen * segLen <= len(raw)
preserves acc(sl.Bytes(raw, 0, len(raw)), p)
ensures hopFields(raw, offset, currHfIdx, segLen)[start:] ==
hopFields(raw, offset, currHfIdx + start, segLen)
decreases start
func hopsFromPrefixOfRawMatchPrefixOfHops(raw []byte, offset int, currHfIdx int, segLen int, start int, p perm) {
if (start != 0) {
newP := (p + R55)/2
hopsFromPrefixOfRawMatchPrefixOfHops(raw, offset, currHfIdx, segLen, start - 1, newP)
}
}

ghost
requires 0 <= offset
requires 0 <= start && start <= currHfIdx
requires 0 <= currHfIdx && currHfIdx <= segLen
requires offset + path.HopLen * segLen <= len(raw)
preserves acc(sl.Bytes(raw, 0, len(raw)), R54)
ensures hopFields(raw, offset, currHfIdx, segLen) ==
hopFields(raw, offset + start * path.HopLen, currHfIdx - start, segLen - start)
decreases
func AlignHopsOfRawWithOffsetAndIndex(raw []byte, offset int, currHfIdx int, segLen int, start int) {
alignHopsOfRawWithOffsetAndIndex(raw, offset, currHfIdx, segLen, start, R54)
}

ghost
requires R55 < p
requires 0 <= offset
requires 0 <= start && start <= currHfIdx
requires 0 <= currHfIdx && currHfIdx <= segLen
requires offset + path.HopLen * segLen <= len(raw)
preserves acc(sl.Bytes(raw, 0, len(raw)), p)
ensures hopFields(raw, offset, currHfIdx, segLen) ==
hopFields(raw, offset + start * path.HopLen, currHfIdx - start, segLen - start)
decreases segLen - currHfIdx
func alignHopsOfRawWithOffsetAndIndex(raw []byte, offset int, currHfIdx int, segLen int, start int, p perm) {
if (currHfIdx != segLen) {
newP := (p + R55)/2
alignHopsOfRawWithOffsetAndIndex(raw, offset, currHfIdx + 1, segLen, start, newP)
}
assert reveal hopFieldsBytePositions(raw, offset, currHFIdx, segLen, hopfields)
}

0 comments on commit 445bbad

Please sign in to comment.