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.

Sign up for GitHub

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

Fix doXover on the new semantics #395

Merged
merged 10 commits into from
Feb 3, 2025
Merged

Fix doXover on the new semantics #395

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
93e4539
start
jcp19 Feb 2, 2025
2af170c
identify problematic postconditions
jcp19 Feb 2, 2025
d126ba2
drop one assumption
jcp19 Feb 2, 2025
3d280b7
drop comments
jcp19 Feb 2, 2025
dff7255
fix proof of new postconditions of XoverLemma
jcp19 Feb 2, 2025
8b91b34
small simplifications
jcp19 Feb 2, 2025
e0ed95d
drop yet another assumption
jcp19 Feb 2, 2025
d0fa499
drop last assumption
jcp19 Feb 2, 2025
706e614
Merge branch 'master' into fix-doxover
jcp19 Feb 2, 2025
47cdd56
Merge branch 'drop_fractions_functions' into fix-doxover
jcp19 Feb 2, 2025
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
9 changes: 8 additions & 1 deletion pkg/slayers/path/scion/raw.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -234,11 +234,18 @@ func (s *Raw) ToDecoded( /*@ ghost ubuf []byte @*/ ) (d *Decoded, err error) {
// @ ensures r != nil ==> s.NonInitMem()
// @ ensures r != nil ==> r.ErrorMem()
// post for IO:
// @ ensures r == nil ==> s.GetBase(ubuf).EqAbsHeader(ubuf) && validPktMetaHdr(ubuf)
// @ ensures r == nil ==>
// @ s.GetBase(ubuf).EqAbsHeader(ubuf) && validPktMetaHdr(ubuf)
// @ ensures r == nil && old(s.GetBase(ubuf).IsXoverSpec()) ==>
// @ s.absPkt(ubuf) == AbsXover(old(s.absPkt(ubuf)))
// @ ensures r == nil && !old(s.GetBase(ubuf).IsXoverSpec()) ==>
// @ s.absPkt(ubuf) == AbsIncPath(old(s.absPkt(ubuf)))
// (VerifiedSCION) the following post is technically redundant,
// as it conveys information that could, in principle, be conveyed
// with the previous posts. We should at some point revisit all
// abstractions we use for paths and potentially unify them.
// @ ensures r == nil ==>
// @ s.GetBase(ubuf) == old(s.GetBase(ubuf).IncPathSpec())
// @ decreases
func (s *Raw) IncPath( /*@ ghost ubuf []byte @*/ ) (r error) {
//@ unfold s.Mem(ubuf)
Expand Down
9 changes: 8 additions & 1 deletion pkg/slayers/path/scion/raw_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,13 +290,16 @@ requires 0 < segLen
requires offset + path.HopLen * segLen <= len(raw)
requires 0 <= currHfIdx && currHfIdx <= segLen
requires 0 <= currInfIdx && currInfIdx < 3
ensures len(res.Future) == segLen - currHfIdx
ensures len(res.History) == currHfIdx
ensures len(res.Past) == currHfIdx
decreases
pure func CurrSeg(raw []byte,
offset int,
currInfIdx int,
currHfIdx int,
segLen int,
headerOffset int) io.IO_seg3 {
headerOffset int) (res io.IO_seg3) {
return let ainfo := path.Timestamp(raw, currInfIdx, headerOffset) in
let consDir := path.ConsDir(raw, currInfIdx, headerOffset) in
let peer := path.Peer(raw, currInfIdx, headerOffset) in
Expand Down Expand Up @@ -621,6 +624,8 @@ preserves validPktMetaHdr(ubuf)
preserves s.GetBase(ubuf).EqAbsHeader(ubuf)
ensures s.absPkt(ubuf).LeftSeg != none[io.IO_seg2]
ensures len(s.absPkt(ubuf).CurrSeg.Future) == 1
ensures len(get(s.absPkt(ubuf).LeftSeg).Future) > 0
ensures len(get(s.absPkt(ubuf).LeftSeg).History) == 0
decreases
func (s *Raw) XoverLemma(ubuf []byte) {
reveal validPktMetaHdr(ubuf)
Expand All @@ -640,6 +645,8 @@ func (s *Raw) XoverLemma(ubuf []byte) {
assert pkt.LeftSeg == reveal LeftSeg(ubuf, currInfIdx + 1, segs, MetaLen)
assert len(pkt.CurrSeg.Future) == 1
assert pkt.LeftSeg != none[io.IO_seg2]
assert len(get(s.absPkt(ubuf).LeftSeg).History) == 0
assert len(get(pkt.LeftSeg).Future) > 0
}

ghost
Expand Down
25 changes: 22 additions & 3 deletions router/dataplane.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3115,8 +3115,8 @@ func (p *scionPacketProcessor) processEgress( /*@ ghost ub []byte @*/ ) (reserr
// @ let ubPath := p.scionLayer.UBPath(ub) in
// @ (unfolding acc(p.scionLayer.Mem(ub), _) in
// @ p.path === p.scionLayer.GetPath(ub) &&
// @ p.path.GetBase(ubPath) == currBase.IncPathSpec() &&
// @ currBase.IncPathSpec().Valid())
// @ p.path.GetBase(ubPath) == currBase.IncPathSpec())
// @ ensures reserr == nil ==> currBase.IncPathSpec().Valid()
// @ ensures reserr == nil ==>
// @ p.scionLayer.ValidPathMetaData(ub) == old(p.scionLayer.ValidPathMetaData(ub))
// @ decreases
Expand All @@ -3131,14 +3131,19 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost currBase scio
// @ sl.SplitByIndex_Bytes(ub, 0, startP, slayers.CmnHdrLen, R54)
// @ sl.Reslice_Bytes(ub, 0, slayers.CmnHdrLen, R54)
// @ slayers.IsSupportedPktSubslice(ub, slayers.CmnHdrLen)
// @ assert p.path == p.scionLayer.GetPath(ub)
// @ p.AbsPktToSubSliceAbsPkt(ub, startP, endP)
// @ assert p.path == p.scionLayer.GetPath(ub)
// @ p.scionLayer.ValidHeaderOffsetToSubSliceLemma(ub, startP)
// @ ghost preAbsPkt := p.path.absPkt(ubPath)
// @ p.path.XoverLemma(ubPath)
// @ reveal p.EqAbsInfoField(absPkt(ub))
// @ reveal p.EqAbsHopField(absPkt(ub))
// @ sl.SplitRange_Bytes(ub, startP, endP, HalfPerm)
// @ reveal p.scionLayer.ValidHeaderOffset(ub, startP)
// @ unfold acc(p.scionLayer.Mem(ub), R55)
// @ assert p.path.GetBase(ubPath) == currBase
// @ ghost nextBase := currBase.IncPathSpec()
if err := p.path.IncPath( /*@ ubPath @*/ ); err != nil {
// TODO parameter problem invalid path
// (VerifiedSCION) we currently expose a lot of internal information from slayers here. Can we avoid it?
Expand All @@ -3150,18 +3155,28 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost currBase scio
// @ fold p.scionLayer.NonInitMem()
return processResult{}, serrors.WrapStr("incrementing path", err)
}
// @ assert p.path.GetBase(ubPath) == nextBase
// @ assert p.path.absPkt(ubPath) == scion.AbsXover(preAbsPkt)
// @ fold acc(p.scionLayer.Mem(ub), R55)
// @ assert reveal p.scionLayer.ValidHeaderOffset(ub, startP)
// @ ghost sl.CombineRange_Bytes(ub, startP, endP, HalfPerm)
// @ slayers.IsSupportedPktSubslice(ub, slayers.CmnHdrLen)
// @ sl.Unslice_Bytes(ub, 0, slayers.CmnHdrLen, R54)
// @ sl.CombineAtIndex_Bytes(ub, 0, startP, slayers.CmnHdrLen, R54)
// @ assert p.path == p.scionLayer.GetPath(ub)
// @ p.scionLayer.ValidHeaderOffsetFromSubSliceLemma(ub, startP)
// @ assert p.scionLayer.ValidHeaderOffset(ub, len(ub))
// @ assert p.path == p.scionLayer.GetPath(ub)
// @ p.SubSliceAbsPktToAbsPkt(ub, startP, endP)
// @ assert p.scionLayer.ValidHeaderOffset(ub, len(ub))
// @ assert p.path == p.scionLayer.GetPath(ub)
// @ assert p.path.GetBase(ubPath) == nextBase
// @ assert len(get(old(absPkt(ub)).LeftSeg).Future) > 0
// @ assert len(get(old(absPkt(ub)).LeftSeg).History) == 0
// @ assert slayers.ValidPktMetaHdr(ub) && p.scionLayer.EqAbsHeader(ub)
// @ assert absPkt(ub) == reveal AbsDoXover(old(absPkt(ub)))
// @ assert p.path == p.scionLayer.GetPath(ub)
// @ assert p.path.GetBase(ubPath) == nextBase
var err error
// (VerifiedSCION) Due to an incompleteness (https://github.com/viperproject/gobra/issues/770),
// we introduce a temporary variable to be able to call `path.AbsMacArrayCongruence()`.
Expand All @@ -3173,6 +3188,7 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost currBase scio
// TODO parameter problem invalid path
return processResult{}, err
}
// @ assert p.path.GetBase(ubPath) == nextBase
p.hopField = tmpHopField
// @ path.AbsMacArrayCongruence(p.hopField.Mac, tmpHopField.Mac)
// @ assert p.hopField.ToIO_HF() == tmpHopField.ToIO_HF()
Expand All @@ -3185,15 +3201,18 @@ func (p *scionPacketProcessor) doXover( /*@ ghost ub []byte, ghost currBase scio
// TODO parameter problem invalid path
return processResult{}, err
}
// @ ghost sl.CombineRange_Bytes(ub, startP, endP, HalfPerm)
// @ assert p.path.GetBase(ubPath) == nextBase
// @ p.SubSliceAbsPktToAbsPkt(ub, startP, endP)
// @ ghost sl.CombineRange_Bytes(ub, startP, endP, HalfPerm/2)
// @ absPktFutureLemma(ub)
// @ p.path.DecodingLemma(ubPath, p.infoField, p.hopField)
// @ assert reveal p.path.EqAbsInfoField(p.path.absPkt(ubPath), p.infoField.ToAbsInfoField())
// @ assert reveal p.path.EqAbsHopField(p.path.absPkt(ubPath), p.hopField.ToIO_HF())
// @ assert reveal p.EqAbsHopField(absPkt(ub))
// @ assert reveal p.EqAbsInfoField(absPkt(ub))
// @ ghost sl.CombineRange_Bytes(ub, startP, endP, HalfPerm/2)
// @ fold acc(p.scionLayer.Mem(ub), 1-R55)
// @ assert currBase.IncPathSpec().Valid()
return processResult{}, nil
}

Expand Down
3 changes: 3 additions & 0 deletions router/io-spec-lemmas.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -263,6 +263,7 @@ ensures end == p.scionLayer.PathEndIdx(ub)
ensures scion.validPktMetaHdr(ub[start:end])
ensures p.path.GetBase(ub[start:end]).EqAbsHeader(ub[start:end])
ensures p.scionLayer.ValidHeaderOffset(ub, len(ub))
ensures p.path === p.scionLayer.GetPath(ub)
ensures absPkt(ub) == p.path.absPkt(ub[start:end])
decreases
func (p* scionPacketProcessor) AbsPktToSubSliceAbsPkt(ub []byte, start int, end int) {
Expand Down Expand Up @@ -324,7 +325,9 @@ ensures start == p.scionLayer.PathStartIdx(ub)
ensures end == p.scionLayer.PathEndIdx(ub)
ensures scion.validPktMetaHdr(ub[start:end])
ensures p.scionLayer.EqAbsHeader(ub)
ensures p.path === p.scionLayer.GetPath(ub)
ensures absPkt(ub) == p.path.absPkt(ub[start:end])
ensures p.scionLayer.ValidHeaderOffset(ub, len(ub))
decreases
func (p* scionPacketProcessor) SubSliceAbsPktToAbsPkt(ub []byte, start int, end int){
unfold acc(sl.Bytes(ub, 0, len(ub)), R56)
Expand Down
Loading