Skip to content

Commit

Permalink
renaming
Browse files Browse the repository at this point in the history
  • Loading branch information
@mlimbeck
mlimbeck committed Jun 27, 2024
1 parent 3c10372 commit c408dbc
Showing 1 changed file with 65 additions and 65 deletions.
130 changes: 65 additions & 65 deletions pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -552,21 +552,21 @@ ghost
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), R50)
requires let offset_curr := currHfIdx * path.HopLen in
let offset_next := offset_curr + path.HopLen in
acc(sl.Bytes(hopfields[:offset_curr], 0, offset_curr), R50) &&
acc(sl.Bytes(hopfields[offset_curr:offset_next], 0, path.HopLen), R50) &&
acc(sl.Bytes(hopfields[offset_next:], 0, (segLen - currHfIdx - 1) * path.HopLen), R50)
requires let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
acc(sl.Bytes(hopfields[:currHfStart], 0, currHfStart), R50) &&
acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), R50) &&
acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), R50)
decreases
pure func BytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf io.AbsInfoField) bool {
return let currseg := CurrSegWithInfo(hopfields, currHfIdx, segLen, inf) in
let offset_curr := currHfIdx * path.HopLen in
let offset_next := offset_curr + path.HopLen in
let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
len(currseg.Future) > 0 &&
currseg.Future[0] == path.BytesToIO_HF(hopfields[offset_curr:offset_next], 0, 0, path.HopLen) &&
currseg.Future[1:] == hopFields(hopfields[offset_next:], 0, 0, (segLen - currHfIdx - 1)) &&
currseg.Past == segPast(hopFields(hopfields[:offset_curr], 0, 0, currHfIdx)) &&
currseg.History == segHistory(hopFields(hopfields[:offset_curr], 0, 0, currHfIdx)) &&
currseg.Future[0] == path.BytesToIO_HF(hopfields[currHfStart:currHfEnd], 0, 0, path.HopLen) &&
currseg.Future[1:] == hopFields(hopfields[currHfEnd:], 0, 0, (segLen - currHfIdx - 1)) &&
currseg.Past == segPast(hopFields(hopfields[:currHfStart], 0, 0, currHfIdx)) &&
currseg.History == segHistory(hopFields(hopfields[:currHfStart], 0, 0, currHfIdx)) &&
currseg.AInfo == inf.AInfo &&
currseg.UInfo == inf.UInfo &&
currseg.ConsDir == inf.ConsDir &&
Expand All @@ -582,32 +582,32 @@ ghost
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
preserves acc(sl.Bytes(hopfields, 0, len(hopfields)), R49)
preserves let offset_curr := currHfIdx * path.HopLen in
let offset_next := offset_curr + path.HopLen in
acc(sl.Bytes(hopfields[:offset_curr], 0, offset_curr), R49) &&
acc(sl.Bytes(hopfields[offset_curr:offset_next], 0, path.HopLen), R49) &&
acc(sl.Bytes(hopfields[offset_next:], 0, (segLen - currHfIdx - 1) * path.HopLen), R49)
preserves let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
acc(sl.Bytes(hopfields[:currHfStart], 0, currHfStart), R49) &&
acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), R49) &&
acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), R49)
ensures BytesStoreCurrSeg(hopfields, currHfIdx, segLen, inf)
decreases
func EstablishBytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf io.AbsInfoField) {
currseg := reveal CurrSegWithInfo(hopfields, currHfIdx, segLen, inf)
offset_curr := currHfIdx * path.HopLen
offset_next := offset_curr + path.HopLen
currHfStart := currHfIdx * path.HopLen
currHfEnd := currHfStart + path.HopLen
unfold acc(sl.Bytes(hopfields, 0, len(hopfields)), R56)
unfold acc(sl.Bytes(hopfields[offset_curr:offset_next], 0, path.HopLen), 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[offset_curr:offset_next], 0, 0, path.HopLen)
assert currseg.Future[0] == path.BytesToIO_HF(hopfields[currHfStart:currHfEnd], 0, 0, path.HopLen)
splitHopFieldsInPastAndFuture(hopfields, currHfIdx, segLen)
assert currseg.Past == segPast(hopFields(hopfields[:offset_curr], 0, 0, currHfIdx))
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[offset_next:], 0, 0, (segLen - currHfIdx- 1))
assert currseg.History == segHistory(hopFields(hopfields[:offset_curr], 0, 0, currHfIdx))
fold acc(sl.Bytes(hopfields[offset_curr:offset_next], 0, path.HopLen), R56)
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)
}

Expand All @@ -620,34 +620,34 @@ 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 offset_curr := currHfIdx * path.HopLen in
let offset_next := offset_curr + path.HopLen in
acc(sl.Bytes(hopfields[:offset_curr], 0, offset_curr), R50) &&
acc(sl.Bytes(hopfields[offset_next:], 0, (segLen - currHfIdx - 1) * path.HopLen), R50)
ensures let offset_curr := currHfIdx * path.HopLen in
let offset_next := offset_curr + path.HopLen in
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[:offset_curr], 0, 0, currHfIdx) &&
hopFields(hopfields, 0, 0, segLen)[offset_next:] ==
hopFields(hopfields[offset_next:], 0, 0, (segLen - currHfIdx - 1))
hopFields(hopfields[:currHfStart], 0, 0, currHfIdx) &&
hopFields(hopfields, 0, 0, segLen)[currHfEnd:] ==
hopFields(hopfields[currHfEnd:], 0, 0, (segLen - currHfIdx - 1))
decreases
func splitHopFieldsInPastAndFuture(hopfields []byte, currHfIdx int, segLen int) {
offset_curr := currHfIdx * path.HopLen
offset_next := offset_curr + path.HopLen
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)
widenHopFields(hopfields, 0, 0, currHfIdx, 0, offset_curr, R52)
widenHopFields(hopfields, 0, 0, currHfIdx, 0, currHfStart, R52)

hfFuture := hopFields(hopfields, offset_next, 0, segLen - currHfIdx - 1)
hopFieldsBytePositionsLemma(hopfields, offset_next, 0, segLen - currHfIdx - 1, R54)
reveal hopFieldsBytePositions(hopfields, offset_next, 0, segLen - currHfIdx - 1, hfFuture)
widenHopFields(hopfields, offset_next, 0, segLen - currHfIdx - 1,
offset_next, segLen*path.HopLen, 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)
}

// `SplitHopfields` splits the permission to the raw bytes of a segment into the permission
Expand All @@ -658,20 +658,20 @@ requires 0 < p
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), p)
ensures let offset_curr := currHfIdx * path.HopLen in
let offset_next := offset_curr + path.HopLen in
acc(sl.Bytes(hopfields[:offset_curr], 0, offset_curr), p) &&
acc(sl.Bytes(hopfields[offset_curr:offset_next], 0, path.HopLen), p) &&
acc(sl.Bytes(hopfields[offset_next:], 0, (segLen - currHfIdx - 1) * path.HopLen), p)
ensures let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
acc(sl.Bytes(hopfields[:currHfStart], 0, currHfStart), p) &&
acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), p) &&
acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), p)
decreases
func SplitHopfields(hopfields []byte, currHfIdx int, segLen int, p perm) {
offset_curr := currHfIdx * path.HopLen
offset_next := offset_curr + path.HopLen
sl.SplitByIndex_Bytes(hopfields, 0, len(hopfields), offset_curr, p)
sl.SplitByIndex_Bytes(hopfields, offset_curr, len(hopfields), offset_next, p)
sl.Reslice_Bytes(hopfields, 0, offset_curr, p)
sl.Reslice_Bytes(hopfields, offset_curr, offset_next, p)
sl.Reslice_Bytes(hopfields, offset_next, len(hopfields), p)
currHfStart := currHfIdx * path.HopLen
currHfEnd := currHfStart + path.HopLen
sl.SplitByIndex_Bytes(hopfields, 0, len(hopfields), currHfStart, p)
sl.SplitByIndex_Bytes(hopfields, currHfStart, len(hopfields), currHfEnd, p)
sl.Reslice_Bytes(hopfields, 0, currHfStart, p)
sl.Reslice_Bytes(hopfields, currHfStart, currHfEnd, p)
sl.Reslice_Bytes(hopfields, currHfEnd, len(hopfields), p)
}

// `CombineHopfields` combines the permissions to the slices of bytes storing the past hopfields,
Expand All @@ -681,19 +681,19 @@ ghost
requires 0 < p
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires let offset_curr := currHfIdx * path.HopLen in
let offset_next := offset_curr + path.HopLen in
acc(sl.Bytes(hopfields[:offset_curr], 0, offset_curr), p) &&
acc(sl.Bytes(hopfields[offset_curr:offset_next], 0, path.HopLen), p) &&
acc(sl.Bytes(hopfields[offset_next:], 0, (segLen - currHfIdx - 1) * path.HopLen), p)
requires let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
acc(sl.Bytes(hopfields[:currHfStart], 0, currHfStart), p) &&
acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), p) &&
acc(sl.Bytes(hopfields[currHfEnd:], 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) {
offset_curr := currHfIdx * path.HopLen
offset_next := offset_curr + path.HopLen
sl.Unslice_Bytes(hopfields, offset_next, len(hopfields), p)
sl.Unslice_Bytes(hopfields, offset_curr, offset_next, p)
sl.Unslice_Bytes(hopfields, 0, offset_curr, p)
sl.CombineAtIndex_Bytes(hopfields, offset_curr, len(hopfields), offset_next, p)
sl.CombineAtIndex_Bytes(hopfields, 0, len(hopfields), offset_curr, p)
currHfStart := currHfIdx * path.HopLen
currHfEnd := currHfStart + path.HopLen
sl.Unslice_Bytes(hopfields, currHfEnd, len(hopfields), p)
sl.Unslice_Bytes(hopfields, currHfStart, currHfEnd, p)
sl.Unslice_Bytes(hopfields, 0, currHfStart, p)
sl.CombineAtIndex_Bytes(hopfields, currHfStart, len(hopfields), currHfEnd, p)
sl.CombineAtIndex_Bytes(hopfields, 0, len(hopfields), currHfStart, p)
}

0 comments on commit c408dbc

Please sign in to comment.