Prove three of the four assumptions in parsePath
#316
Conversation
Co-authored-by: Dionysios Spiliopoulos <[email protected]>
* progress updating the IO-spec * finish updating new IO-spec
* start fixing pres of processSCION * backup * backup * Drop unnecessary assertions * tiny fmt
* io-spec update * proof of link logic * fix verification errors * drop assumption in validateSrcDstIA() * fix verification error * Update pkg/slayers/path/scion/raw.go
|
To guarantee that this does not fall out of sync with the main code, we should soon merge master here and try to merge this on master soon. I will add few preliminary comments in case that helps |
| // @ requires len(raw) >= HopLen | ||
| // @ preserves acc(h) | ||
| // @ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46) | ||
| // @ ensures h.ConsIngress >= 0 | ||
| // @ ensures h.ConsEgress >= 0 | ||
| // @ ensures let h1 := BytesToIO_HF(raw, 0, 0, HopLen) in | ||
| // @ let h2 := h.ToIO_HF() in | ||
| // @ h1.InIF2 == h2.InIF2 && | ||
| // @ h1.EgIF2 == h2.EgIF2 | ||
| // @ decreases | ||
| // @ outline( | ||
| // @ unfold acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R46) |
There was a problem hiding this comment.
Considering all the effort that went into making Gobra/silicon faster in the last few months, I think that these outline blocks are now unnecessary because
- this package is not problematic in the first place
- we can afford it now, even if this is ever so slightly slower (which probably is not the case anymore), and the annotation overhead is not worth it
| requires acc(slices.AbsSlice_Bytes(raw, start, end), _) | ||
| decreases | ||
| pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) { | ||
| return unfolding acc(slices.AbsSlice_Bytes(raw, start, end), _) in BytesToIO_HF_Helper(raw, start, middle, end) |
There was a problem hiding this comment.
I know that you still will refine the code, but as a heads-up, please try to keep lines shorter (e.g., by introducing line-breaks after in)
| decreases | ||
| pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) { | ||
| pure func BytesToIO_HF_Helper(raw [] byte, start int, middle int, end int) (io.IO_HF) { |
There was a problem hiding this comment.
These names are getting more and more unidiomatic :D I think calling these functions BytesToHfSpec and BytesToHfSpecUnfolded would be fine
router/dataplane.go
Outdated
| // TemporaryAssumeForIO(slayers.ValidPktMetaHdr(ub)) | ||
| // TemporaryAssumeForIO(len(absPkt(dp, ub).CurrSeg.Future) > 0) | ||
| // TemporaryAssumeForIO(p.EqAbsHopField(absPkt(dp, ub))) |
There was a problem hiding this comment.
If you haven't started the proof for the fourth assumption, maybe it is a good idea to do that on a separate PR, so that we can keep the PRs small and easy to review
| let idx := int(s.PathMeta.CurrHF) in | ||
| let hopOffset := MetaLen + s.NumINF*path.InfoLen + idx*path.HopLen in | ||
| let _ := Assuming(idx >= 0) in // Gobra can't figure this out from the type system at the moment |
There was a problem hiding this comment.
Hopefully, this will not be a problem soon because I intend to fix the overflow checking of Gobra soon and to make it generate the necessary obligations here.
At any rate, I would like to avoid introduce assumptions in pure functions due to their "global" nature. I would rather have a precondition in this method requiring s.PathMeta.CurrHF to be non-negative and introducing an assumption in the caller (if it is a non-pure function) or a precondition (if it is a pure function). I think that opening a precedent where we introduce assumptions in the bodies of pure functions is a bad idea
router/io-spec-lemmas.gobra
Outdated
| ensures len(absPkt(dp, ub).CurrSeg.Future) > 0 | ||
| ensures p.EqAbsHopField(absPkt(dp, ub)) | ||
| decreases | ||
| func (p *scionPacketProcessor) CurrentHopFieldBytesLemma(dp io.DataPlaneSpec , ub []byte, ubPath []byte) |
There was a problem hiding this comment.
you probably don't need dp in this function anymore, and in a few other functions that you introduced in this PR (check #341)
There was a problem hiding this comment.
Also, is this the only proof obligation that is missing?
|
|
||
| ghost | ||
| ensures b | ||
| decreases | ||
| pure func Assuming(b bool) bool |
There was a problem hiding this comment.
I would drop this function for the reasons stated above
| ensures s.absPktFutureBytePosition(dp, raw) | ||
| decreases | ||
| func (s *Raw) absPktFutureBytePositionLemma(dp io.DataPlaneSpec, raw []byte) (res io.IO_pkt2) { | ||
| _ := reveal validPktMetaHdr(raw) |
There was a problem hiding this comment.
| _ := reveal validPktMetaHdr(raw) | |
| reveal validPktMetaHdr(raw) |
jcp19
changed the title
parsePath
|
This PR is superseded by PR #345 |
No description provided.