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.

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

Drop SetHopfield related assumptions #368

Merged
merged 28 commits into from
Jul 15, 2024
Merged
Changes from 1 commit
Commits
Show all changes
28 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
21e317c
assume postconditions in setHopfield
mlimbeck Jul 11, 2024
0e68b71
add comment to IO assumptions
mlimbeck Jul 11, 2024
ca49646
increase timeout for scion package
mlimbeck Jul 11, 2024
c8f7991
revert timeout increase
mlimbeck Jul 15, 2024
90614e7
feedback
mlimbeck Jul 15, 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
Prev Previous commit
Next Next commit
space between arithmetic operands
mlimbeck committed Jun 27, 2024
commit d7ad54aa2bb817dfe768ebc34564a2a7f4d24354
54 changes: 27 additions & 27 deletions pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
Original file line number Diff line number Diff line change
@@ -45,7 +45,7 @@ pure func InfofieldByteSlice(raw []byte, currInfIdx int) ([]byte) {
return let infOffset := currInfIdx == 4 ?
path.InfoFieldOffset(0, MetaLen) :
path.InfoFieldOffset(currInfIdx, MetaLen) in
raw[infOffset:infOffset+path.InfoLen]
raw[infOffset:infOffset + path.InfoLen]
}

// HopfieldsStartIdx returns index of the first byte of the hopfields of a segment
@@ -61,8 +61,8 @@ pure func HopfieldsStartIdx(currInfIdx int, segs io.SegLens) int {
return let numInf := segs.NumInfoFields() in
let infOffset := path.InfoFieldOffset(numInf, MetaLen) in
(currInfIdx == 0 || currInfIdx == 4) ? infOffset :
currInfIdx == 1 ? infOffset+segs.Seg1Len*path.HopLen :
infOffset+(segs.Seg1Len+segs.Seg2Len)*path.HopLen
currInfIdx == 1 ? infOffset + segs.Seg1Len * path.HopLen :
infOffset + (segs.Seg1Len + segs.Seg2Len) * path.HopLen
}

// HopfieldsStartIdx returns index of the last byte of the hopfields of a segment
@@ -77,9 +77,9 @@ decreases
pure func HopfieldsEndIdx(currInfIdx int, segs io.SegLens) int {
return let numInf := segs.NumInfoFields() in
let infOffset := path.InfoFieldOffset(numInf, MetaLen) in
(currInfIdx == 0 || currInfIdx == 4) ? infOffset+segs.Seg1Len*path.HopLen :
currInfIdx == 1 ? infOffset+(segs.Seg1Len+segs.Seg2Len)*path.HopLen :
infOffset+(segs.Seg1Len+segs.Seg2Len+segs.Seg3Len)*path.HopLen
(currInfIdx == 0 || currInfIdx == 4) ? infOffset + segs.Seg1Len * path.HopLen :
currInfIdx == 1 ? infOffset + (segs.Seg1Len + segs.Seg2Len) * path.HopLen :
infOffset + (segs.Seg1Len + segs.Seg2Len + segs.Seg3Len) * path.HopLen
}

// HopfieldsStartIdx returns returns the byte slice of the hopfields of a segment
@@ -107,9 +107,9 @@ requires segs.Valid()
requires PktLen(segs, MetaLen) <= len(raw)
requires acc(sl.Bytes(raw, 0, len(raw)), p)
ensures acc(sl.Bytes(raw[:HopfieldsStartIdx(0, segs)], 0, HopfieldsStartIdx(0, segs)), p)
ensures acc(sl.Bytes(HopfieldsByteSlice(raw, 0, segs), 0, segs.Seg1Len*path.HopLen), p)
ensures acc(sl.Bytes(HopfieldsByteSlice(raw, 1, segs), 0, segs.Seg2Len*path.HopLen), p)
ensures acc(sl.Bytes(HopfieldsByteSlice(raw, 2, segs), 0, segs.Seg3Len*path.HopLen), p)
ensures acc(sl.Bytes(HopfieldsByteSlice(raw, 0, segs), 0, segs.Seg1Len * path.HopLen), p)
ensures acc(sl.Bytes(HopfieldsByteSlice(raw, 1, segs), 0, segs.Seg2Len * path.HopLen), p)
ensures acc(sl.Bytes(HopfieldsByteSlice(raw, 2, segs), 0, segs.Seg3Len * path.HopLen), p)
ensures acc(sl.Bytes(raw[HopfieldsEndIdx(2, segs):], 0, len(raw[HopfieldsEndIdx(2, segs):])), p)
decreases
func SliceBytesIntoSegments(raw []byte, segs io.SegLens, p perm) {
@@ -152,7 +152,7 @@ func CombineBytesFromSegments(raw []byte, segs io.SegLens, p perm) {
ghost
requires 0 < p
requires segs.Valid()
requires MetaLen + numInf*path.InfoLen <= 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)
@@ -184,7 +184,7 @@ func SliceBytesIntoInfoFields(raw []byte, numInf int, segs io.SegLens, p perm) {
ghost
requires 0 < p
requires segs.Valid()
requires MetaLen + numInf*path.InfoLen <= 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)
@@ -220,7 +220,7 @@ ghost
opaque
requires 0 < SegLen
requires 0 <= currHfIdx && currHfIdx <= SegLen
requires SegLen*path.HopLen == len(hopfields)
requires SegLen * path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), R56)
decreases
pure func CurrSegWithInfo(hopfields []byte, currHfIdx int, SegLen int, inf io.AbsInfoField) io.IO_seg3 {
@@ -240,7 +240,7 @@ requires (currInfIdx == 1 && segs.Seg2Len > 0) ||
let start := HopfieldsStartIdx(currInfIdx, segs) in
let end := HopfieldsEndIdx(currInfIdx, segs) in
inf != none[io.AbsInfoField] &&
len(hopfields) == end-start &&
len(hopfields) == end - start &&
acc(sl.Bytes(hopfields, 0, len(hopfields)), R49)
decreases
pure func LeftSegWithInfo(
@@ -267,7 +267,7 @@ requires (currInfIdx == 0 && segs.Seg2Len > 0) ||
let start := HopfieldsStartIdx(currInfIdx, segs) in
let end := HopfieldsEndIdx(currInfIdx, segs) in
inf != none[io.AbsInfoField] &&
len(hopfields) == end-start &&
len(hopfields) == end - start &&
acc(sl.Bytes(hopfields, 0, len(hopfields)), R49)
decreases
pure func RightSegWithInfo(
@@ -294,7 +294,7 @@ requires (segs.Seg2Len > 0 && segs.Seg3Len > 0 &&
let start := HopfieldsStartIdx(currInfIdx, segs) in
let end := HopfieldsEndIdx(currInfIdx, segs) in
inf != none[io.AbsInfoField] &&
len(hopfields) == end-start &&
len(hopfields) == end - start &&
acc(sl.Bytes(hopfields, 0, len(hopfields)), R49)
decreases
pure func MidSegWithInfo(
@@ -318,10 +318,10 @@ requires offset + path.HopLen * SegLen <= len(raw)
requires 0 <= currHfIdx && currHfIdx <= SegLen
requires 0 <= currInfIdx && currInfIdx < 3
preserves acc(sl.Bytes(raw, 0, len(raw)), R50)
preserves acc(sl.Bytes(raw[offset:offset+SegLen*path.HopLen], 0, SegLen*path.HopLen), R50)
preserves acc(sl.Bytes(raw[offset:offset + SegLen * path.HopLen], 0, SegLen * path.HopLen), R50)
preserves acc(sl.Bytes(InfofieldByteSlice(raw, currInfIdx), 0, path.InfoLen), R50)
ensures let inf := path.BytesToAbsInfoField(InfofieldByteSlice(raw, currInfIdx), 0) in
CurrSegWithInfo(raw[offset:offset+SegLen*path.HopLen], currHfIdx, SegLen, inf) ==
CurrSegWithInfo(raw[offset:offset + SegLen * path.HopLen], currHfIdx, SegLen, inf) ==
CurrSeg(raw, offset, currInfIdx, currHfIdx, SegLen, MetaLen)
decreases
func CurrSegEquality(raw []byte, offset int, currInfIdx int, currHfIdx int, SegLen int) {
@@ -333,19 +333,19 @@ func CurrSegEquality(raw []byte, offset int, currInfIdx int, currHfIdx int, SegL
assert reveal path.BytesToAbsInfoField(raw, infOffset) ==
reveal path.BytesToAbsInfoField(infoBytes, 0)
reveal CurrSeg(raw, offset, currInfIdx, currHfIdx, SegLen, MetaLen)
reveal CurrSegWithInfo(raw[offset:offset+SegLen*path.HopLen], currHfIdx, SegLen, inf)
reveal CurrSegWithInfo(raw[offset:offset + SegLen * path.HopLen], currHfIdx, SegLen, inf)
fold acc(sl.Bytes(raw, 0, len(raw)), R56)
fold acc(sl.Bytes(infoBytes, 0, path.InfoLen), R56)
widenSegment(raw, offset, currHfIdx, inf.AInfo, inf.UInfo, inf.ConsDir,
inf.Peer, SegLen, offset, offset+SegLen*path.HopLen)
inf.Peer, SegLen, offset, offset + SegLen * path.HopLen)
}

// UpdateCurrSegInfo proves that updating the infofield from inf1 to inf2 does not alter the hopfields
// of the current segment.
ghost
requires 0 < SegLen
requires 0 <= currHfIdx && currHfIdx <= SegLen
requires SegLen*path.HopLen == len(raw)
requires SegLen * path.HopLen == len(raw)
preserves acc(sl.Bytes(raw, 0, len(raw)), R50)
ensures CurrSegWithInfo(raw, currHfIdx, SegLen, inf1).UpdateCurrSeg(inf2) ==
CurrSegWithInfo(raw, currHfIdx, SegLen, inf2)
@@ -550,7 +550,7 @@ func MidSegEquality(raw []byte, currInfIdx int, segs io.SegLens) {
// `currHfIdx`-th hop (out of `segLen` hops in total).
ghost
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires segLen * path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), R50)
requires let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
@@ -580,7 +580,7 @@ pure func BytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf io.
// current hopfield is modified.
ghost
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires segLen * path.HopLen == len(hopfields)
preserves acc(sl.Bytes(hopfields, 0, len(hopfields)), R49)
preserves let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
@@ -603,7 +603,7 @@ func EstablishBytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf
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 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))
@@ -618,7 +618,7 @@ func EstablishBytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf
ghost
requires 0 < segLen
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
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
@@ -647,7 +647,7 @@ func splitHopFieldsInPastAndFuture(hopfields []byte, currHfIdx int, segLen int)
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)
currHfEnd, segLen * path.HopLen, R52)
}

// `SplitHopfields` splits the permission to the raw bytes of a segment into the permission
@@ -656,7 +656,7 @@ func splitHopFieldsInPastAndFuture(hopfields []byte, currHfIdx int, segLen int)
ghost
requires 0 < p
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires segLen * path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), p)
ensures let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
@@ -680,7 +680,7 @@ func SplitHopfields(hopfields []byte, currHfIdx int, segLen int, p perm) {
ghost
requires 0 < p
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen*path.HopLen == len(hopfields)
requires segLen * path.HopLen == len(hopfields)
requires let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
acc(sl.Bytes(hopfields[:currHfStart], 0, currHfStart), p) &&