Skip to content

Commit

Permalink
Fix doXover on the new semantics (#395)
Browse files Browse the repository at this point in the history 
* start

* identify problematic postconditions

* drop one assumption

* drop comments

* fix proof of new postconditions of XoverLemma

* small simplifications

* drop yet another assumption

* drop last assumption
  • Loading branch information
@jcp19
jcp19 authored Feb 3, 2025
1 parent 0ac3ea8 commit f032c9b
Show file tree
Hide file tree
Showing 4 changed files with 41 additions and 5 deletions.
9 changes: 8 additions & 1 deletion pkg/slayers/path/scion/raw.go
View file
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
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
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
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

0 comments on commit f032c9b

Please sign in to comment.