Skip to content

Commit

Permalink
Merge branch 'joao-uncomment-packSCMP' into markus-packscmp-new-inv
Browse files Browse the repository at this point in the history
  • Loading branch information
@jcp19
jcp19 authored Aug 29, 2024
2 parents fa8c6b1 + 320a1fb commit 5187f87
Show file tree
Hide file tree
Showing 5 changed files with 179 additions and 144 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/gobra.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -265,7 +265,7 @@ jobs:
uses: viperproject/gobra-action@main
with:
packages: 'pkg/slayers/path/scion'
timeout: 5m
timeout: 30m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
Expand Down
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
78 changes: 59 additions & 19 deletions pkg/slayers/path/scion/raw.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -557,32 +557,72 @@ func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/)
// https://github.com/viperproject/gobra/issues/192
//@ assume 0 <= tmpHopField.ConsIngress && 0 <= tmpHopField.ConsEgress
//@ fold acc(tmpHopField.Mem(), R9)
//@ unfold acc(s.Mem(ubuf), R20)
//@ unfold acc(s.Base.Mem(), R20)
//@ reveal validPktMetaHdr(ubuf)
//@ unfold acc(s.Mem(ubuf), R50)
//@ unfold acc(s.Base.Mem(), R50)
//@ ghost currInfIdx := int(s.PathMeta.CurrINF)
//@ ghost currHfIdx := int(s.PathMeta.CurrHF)
//@ ghost seg1Len := int(s.PathMeta.SegLen[0])
//@ ghost seg2Len := int(s.PathMeta.SegLen[1])
//@ ghost seg3Len := int(s.PathMeta.SegLen[2])
//@ ghost segLens := io.CombineSegLens(seg1Len, seg2Len, seg3Len)
//@ ghost segLen := segLens.LengthOfCurrSeg(idx)
//@ ghost prevSegLen := segLens.LengthOfPrevSeg(idx)
//@ ghost offset := HopFieldOffset(s.Base.NumINF, prevSegLen, MetaLen)
//@ ghost hopfieldOffset := MetaLen + s.NumINF*path.InfoLen
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)

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

//@ ValidPktMetaHdrSublice(ubuf, MetaLen)
//@ ghost inf := path.BytesToAbsInfoField(InfofieldByteSlice(ubuf, currInfIdx), 0)
//@ ghost hfIdxSeg := idx-prevSegLen
//@ ghost 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)
//@ EstablishBytesStoreCurrSeg(currHopfields, hfIdxSeg, segLen, inf)
//@ SplitHopfields(currHopfields, hfIdxSeg, segLen, R0)
//@ } 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(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)
// (VerifiedSCION) The proof for these assumptions is provided in PR #361
// (https://github.com/viperproject/VerifiedSCION/pull/361), which will
// be merged once the performance issues are resolved.
//@ TemporaryAssumeForIO(validPktMetaHdr(ubuf) && s.GetBase(ubuf).EqAbsHeader(ubuf))
//@ TemporaryAssumeForIO(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)
//@ 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)
//@ EstablishBytesStoreCurrSeg(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:])
//@ } 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
Loading

0 comments on commit 5187f87

Please sign in to comment.