processEpic
#261
Draft
processEpic
#261
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Open
3 tasks
jcp19
commented
Mar 1, 2024
pkg/experimental/epic/epic.go
Outdated
| // @ ensures reserr != nil ==> sl.AbsSlice_Bytes(buffer, 0, len(buffer)) | ||
| // @ ensures reserr == nil ==> | ||
| // @ sl.AbsSlice_Bytes(res, 0, len(res)) && | ||
| // @ (sl.AbsSlice_Bytes(res, 0, len(res)) --* sl.AbsSlice_Bytes(buffer, 0, len(buffer))) |
There was a problem hiding this comment.
cannot be proven, even though we are able to assert this wand right at the end of the method
This was referenced Mar 1, 2024
Closed
jcp19
added a commit
that referenced
this pull request
Mar 4, 2024
3 tasks
* Undo workaround with short-circuiting operations (#269) * redo short-circuiting operations * Undo change * Update router/dataplane.go * increase timeout for epic (#278) * experiment with disabling NL (#265) * experiment with disabling NL * enable the wildcard optimization for when NL is disabled * Apply suggestions from code review * Drop unnecessary annotations in `Run` (#279) * drop unnecessary annotations * fix precond error * fix verification error * cleanup * fix tiny error * bring changes to the io spec to speed things a little (#281) * Add config for overflow in the CI (#247) * start overflow checking * backup * fix flags * Apply suggestions from code review * disable checks in all packages for now * Update .github/workflows/gobra.yml * Reduce permission amount to buffer for decodeFromLayers (#285) * R40 * epic * extn * onehop * reduce permission amount of decode layers * cosmetic changes (#286) * Fix warning in the CI (#288) * Update gobra.yml to disableNL (#289) * simplify Decoded.Reverse (#295) * Cherry-pick #4483 from `scionproto/scion` (#292) * cherry-pick 4483 * undo change to test due to the use of (yet) undefined symbols * fix verification error --------- Co-authored-by: jiceatscion <[email protected]> * change permissions amount for decode SCMPTraceRoute (#299) * First batch of changes from PR #248 (#306) * first batch of changes from the IO spec * Apply suggestions from code review * adapt config options * Add checks for termination modulo blocking (#309) * add termination checking if we ignore locking * add termination checks modulo locking * backup * fix termination measure * fix verification errors * fix verification error * Verify the IO behavior (a.k.a., basis PR) (#248) * manually trigger workflow * manually trigger workflow * raw byte to spec for segments and hopfields * bugfix * import fix * bugfix after gobra update * spec to pkt (currSeg) * spec to pkt (left, mid, right) * spec to pkt (termination) * code clean up * clean up * improvements * instantiate abstract functions with bodies * progress io spec * formatting * specification fixes * IO-spec to pkt rewritten * clean up * improve readability * rename of function lengthOfCurrSeg * extract asid-seqence from raw pkt * missing trigger * quick fix * Update router/dataplane_spec.gobra Co-authored-by: Dionysios Spiliopoulos <[email protected]> * Apply suggestions from code review Co-authored-by: João Pereira <[email protected]> * readability improvements * further improvements * replace 4 by its constant InfoLen * readability improvement * constant for metaLen in package path * Update router/io-spec.gobra Co-authored-by: João Pereira <[email protected]> * minor improvements * move validMetaLenInPath() to test file * io-spec in Run * add body to absIO_val * fix merge mistake * fix merge mistake * fix typo * io-spec skeleton for processPkt and processSCION * import fix * Update router/io-spec.gobra * unit * well formdness * relate dataplane with dataplaneSpec * various fixes * Update verification/io/values.gobra * permission fix for dpSpecWellConfigured * permission fix in rc * fix verification error * dp.Valid() as opaque * backup * format spacing * improve perf; drop assumption * fix formatting * Update router/dataplane.go * formatting postconditions of processPkt, processSCION * fix extra permission * typo * processSCION had the same issue * ingressID is preseved intead of sInit * Revert "ingressID is preseved intead of sInit" This reverts commit 88db3fd. * Revert "processSCION had the same issue" This reverts commit 71aadfe. * Updated IO-Spec-Function to Correlate Bytes with Terms (#262) * fixes in the asid extraction functions * pre-/postconditions for process * fix formatting * fix same issue in processSCION * fix var names * precondition changes in hopfield and asidFromIfs * prostcondition fix in process and processSCION * update imports links * Apply suggestions from code review --------- Co-authored-by: Dspil <[email protected]> Co-authored-by: João Pereira <[email protected]> * made absIO_val opaque * use artificial triggers for quantifiers inside IO resources (#280) * AbsPkt improvements (#270) * absPkt opaque and other improvements * quick fixes * changed permission from R55 to R56 * added missing permission amount in ReadBatch * fixed pre/postconditions of processPkt, processSCION and process * fixed opaque format --------- Co-authored-by: João Pereira <[email protected]> * Verify send guard in Run (#263) * remove send operation * lemma for smaller buffer result in same abstract pkt * progress send guard * progress send guard * Fix incompleteness and continue with send guard (#273) * backup * backup * backup * backup * backup * drop space * pick better triggers * add necessary lemma and call to it; contains an assume false that needs to be dropped * backup * backup * add missing loop invariant about ingressID * backup * backup * fix verification error * try out a simpler trigger * widen lemma for absIO_val (#268) * widen lemma for abspkt (non termianting) * abspkt proven * renamed io-spec-lemmas * io val also proven * cleanup * merged markus' abspkt improvements * consdir lemma * proved * reinstate lemma4 * fix verification error * Simplify widen lemma from #268 (#282) * start simplifying * continue simplifying * continue simplifying stuff * continue simplifying * continue simplifying * simplify further * finish for now * Update router/io-spec.gobra --------- Co-authored-by: João Pereira <[email protected]> * Continue send (#283) * widen lemma for abspkt (non termianting) * abspkt proven * renamed io-spec-lemmas * io val also proven * cleanup * merged markus' abspkt improvements * consdir lemma * proved * reinstate lemma4 * fix verification error * Simplify widen lemma from #268 (#282) * start simplifying * continue simplifying * continue simplifying stuff * continue simplifying * continue simplifying * simplify further * finish for now * Update router/io-spec.gobra * finish send in Run * propagate changes to processSCION --------- Co-authored-by: Dspil <[email protected]> * backup * adapt to the new syntax of backend annotations * clean-up * changes according to feedback --------- Co-authored-by: João Pereira <[email protected]> Co-authored-by: Dionysios Spiliopoulos <[email protected]> Co-authored-by: Dspil <[email protected]> * IO specification skeleton in process (#284) * absPkt opaque and other improvements * tests for local enter guard * new approach for absPkt * tests with GetIngressIDNotZero() * fix verification error * progress io-skeleton in process * progress Xover * progress io-spec skeleton in process * removed dulicate of lemma * fix verification error * removed old concurrency test * refactored absPkt * continue refactoring of absPkt * fixed postcondition in process * progress lemmas for io-spec * addressed feedback * progress in updateNonConsDirIngressSegID * fix verification errors * Prove IO lemmas in `path/scion` (#290) * try to prove lemma * backup * fix incompletness via additional lemma * fix verification error * fix verification errors and clean up * fix verification errors introduced in the latest changes to the PR * fix consistency error * add lemmas for updateNonConsDirIngressSegID() * Change to EQAbsHeader (#293) * changed EQAbsHeader * readbility improvements * progress in handleRouterAlerts methods * Fix verification errors in dependencies (#291) * backup * backup * backup * simplify Decoded.Reverse * clean-up * add section header * drop comment * fix verification errors in processEgress and DoXover addressing feedback clean up --------- Co-authored-by: João Pereira <[email protected]> * Add functional spec to `InfoField.SerializeTo` (#300) * absPkt opaque and other improvements * tests for local enter guard * new approach for absPkt * tests with GetIngressIDNotZero() * fix verification error * progress io-skeleton in process * progress Xover * progress io-spec skeleton in process * removed dulicate of lemma * fix verification error * removed old concurrency test * refactored absPkt * continue refactoring of absPkt * fixed postcondition in process * progress lemmas for io-spec * addressed feedback * progress in updateNonConsDirIngressSegID * fix verification errors * Prove IO lemmas in `path/scion` (#290) * try to prove lemma * backup * fix incompletness via additional lemma * fix verification error * fix verification errors and clean up * fix verification errors introduced in the latest changes to the PR * fix consistency error * add lemmas for updateNonConsDirIngressSegID() * backup * Change to EQAbsHeader (#293) * changed EQAbsHeader * readbility improvements * backup * backup * simplify Decoded.Reverse * progress in handleRouterAlerts methods * clean-up * add section header * drop comment * Fix verification errors in dependencies (#291) * backup * backup * backup * simplify Decoded.Reverse * clean-up * add section header * drop comment * backup * backup * fix verification errors in processEgress and DoXover addressing feedback clean up * backup * drop one assume * readability improvements * backup * backup * simplify proof * adapt lemmas * verify spec for SerializeTo of infofield * Missing Postcondition in Process (#301) * absPkt opaque and other improvements * tests for local enter guard * new approach for absPkt * tests with GetIngressIDNotZero() * fix verification error * progress io-skeleton in process * progress Xover * progress io-spec skeleton in process * removed dulicate of lemma * fix verification error * removed old concurrency test * refactored absPkt * continue refactoring of absPkt * fixed postcondition in process * progress lemmas for io-spec * addressed feedback * progress in updateNonConsDirIngressSegID * fix verification errors * Prove IO lemmas in `path/scion` (#290) * try to prove lemma * backup * fix incompletness via additional lemma * fix verification error * fix verification errors and clean up * fix verification errors introduced in the latest changes to the PR * fix consistency error * add lemmas for updateNonConsDirIngressSegID() * Change to EQAbsHeader (#293) * changed EQAbsHeader * readbility improvements * Revert "Update gobra.yml to disableNL (#289)" This reverts commit 1e60830. * progress in handleRouterAlerts methods * Fix verification errors in dependencies (#291) * backup * backup * backup * simplify Decoded.Reverse * clean-up * add section header * drop comment * fix verification errors in processEgress and DoXover addressing feedback clean up * fix verification error * changed postcondition in process * fix verification error * fix verification error * Update gobra.yml * added postcondition to packSCMP --------- Co-authored-by: João Pereira <[email protected]> * Drop unnecessary function `hopFieldsNotConsDir` (#303) * reverse hopFieldsNotConsDir once * remove hopfieldsNotConsDir * hopFieldsConsDir => hopFields --------- Co-authored-by: João Pereira <[email protected]> * Update IO-spec to drop the `xover_core` event (#302) * progress updating the IO-spec * finish updating new IO-spec * Fix precondition of `processSCION` (#307) * start fixing pres of processSCION * backup * backup * Drop unnecessary assertions * tiny fmt * streamline msgterm assumptions (#308) * improve verification time of processPkt * IO-spec update for link check logic (#310) * io-spec update * proof of link logic * fix verification errors * drop assumption in validateSrcDstIA() * fix verification error * Update pkg/slayers/path/scion/raw.go * Pre/Post conditions of processPkt (#312) * progress with pre and post conditions for io-spec in processPkt * fix verification error * changes in process * additional temporary assumptions in process() * cleanup --------- Co-authored-by: João Pereira <[email protected]> * fmt --------- Co-authored-by: MLETHZ <[email protected]> Co-authored-by: Markus Limbeck <[email protected]> Co-authored-by: João Pereira <[email protected]> * Update names of functions according to the changes in the IO-spec (#314) * minor renaming and merging of functions * further renaming * Cleanup unnecessary code in the stdlib formalization (#315) * cleanup unnecessary code in the stdlib formalization * replace occurrences of names with 'VerifiedSCION' * backup (#324) * Remove more names (#325) * backup * remove more * Disable conditionalizePermissions (#319) * Update gobra.yml * Update gobra.yml * fix verification error * fixed precondition of XoverEvent * enable moreJoins impure (#321) * invariant strengthening * undo change to the state consolidator --------- Co-authored-by: mlimbeck <[email protected]> Co-authored-by: Dspil <[email protected]> * Refactored Widen-lemma (#327) * Update gobra.yml * Update gobra.yml * fix verification error * fixed precondition of XoverEvent * enable moreJoins impure (#321) * invariant strengthening * progress widen-lemma proof * fix verification error * proven? * fix * bugfix * Update router/widen-lemma.gobra Co-authored-by: João Pereira <[email protected]> * Update router/widen-lemma.gobra Co-authored-by: João Pereira <[email protected]> * joao * indent --------- Co-authored-by: João Pereira <[email protected]> Co-authored-by: Dspil <[email protected]> Co-authored-by: Dionysios Spiliopoulos <[email protected]> * enable chop 10 in the CI (#328) * drop assumption in processPkt (#318) Co-authored-by: João Pereira <[email protected]> * fix termination measuer (#329) * change triggers in absPktWidenLemma (#330) * change triggers in abspktwidenlemma * triggers * remove quantifiers * Drop Assumption in validateEgressID (#326) * Update gobra.yml * Update gobra.yml * fix verification error * fixed precondition of XoverEvent * enable moreJoins impure (#321) * drop assumption in validateEgressID and process * clean up * invariant strengthening * undo change to the state consolidator * refactored wellConfigured assumptions * finish proof of EgressIDNotZeroLemma * Apply suggestions from code review * removed TopologySpec * minor fmt * fix verification error * removed comments Co-authored-by: João Pereira <[email protected]> --------- Co-authored-by: João Pereira <[email protected]> Co-authored-by: Dspil <[email protected]> Co-authored-by: Dionysios Spiliopoulos <[email protected]> * router: forbid bouncing packets internally (#4502) (#332) Brings changes from scion pr 4502 Co-authored-by: Matthias Frei <[email protected]> * Proof of Internal Packet Bouncing fix (#4502) (#333) * proof of scionfix #4502 * feedback * drop assume in processOHP() * change getDomExternal() to opaque * fix comment * verification fix and simplification * fix verification errors * feedback * bring changes from #243 (#335) * Drop `trusted` annotation in method (#339) * drop trusted from method * IO-spec lemmas (#334) * progress open io-lemmas * fix verification errors * refactoring * fix verification error * Enable `conditionalizePermissions` for the `router` (#340) Marco observed that a long time is spent on (sequential) pure function verification in the router package. He also suggested that using `conditionalizePermissions` might reduce the number of branches in these functions (`moreJoins 1` does not have any effect on pure functions), which might speed up verification. * Refactoring of absPkt (#341) * drop DataPlaneSpec param from absPkt * headerOffset change in absPkt * fix syntax error * fix verification errors * fix verification errors * fix LastHopLemma * Proof of incPath (#344) * progress incPath proof * Apply suggestions from code review Co-authored-by: João Pereira <[email protected]> * fmt of widen-lemma * further fmt * feedback * add comment * Update router/dataplane.go * Apply suggestions from code review --------- Co-authored-by: João Pereira <[email protected]> * simplify path/scion (#346) * Verify assumptions in SCION.DecodeFromBytes (#345) * progress scion- decodeFromBytes * revert change of call s.Path.DecodeFromBytes() * fix verification error * fix permission in rawPath * establish validPktHeader in parsePath * fix verification errors * fixed permission and refactored EqAbsHeader * fixed syntax errors * fix verification error * fix permission * introduces additional spec to the Path interface * remove unnecessary preconditions * proof of parse path assumption * simplification in epic.DecodeFromBytes * feedback * Update pkg/slayers/path/scion/raw.go Co-authored-by: João Pereira <[email protected]> * add quantifier to GetCurrentHopField() and GetCurrentInfoField() to avoid code changes * Apply suggestions from code review Co-authored-by: João Pereira <[email protected]> * formatting * simplify onehop * improve io_msgterm_spec.gobra --------- Co-authored-by: João Pereira <[email protected]> * Drop assumption in parsePath (#348) * drop assumption in parsePath * Update router/dataplane.go Co-authored-by: João Pereira <[email protected]> * rename arrayCongruence() to AbsMacArrayCongruence() --------- Co-authored-by: João Pereira <[email protected]> * Use Gobra's built-in ghost fields (#337) * add ghost fields * fix type errors so far * backup * clean-up * convert more adt types to structs * make read not trusted * Update router/dataplane_concurrency_model.gobra * cleanup * change equality * rever changes to === * clean-up * Fix ghostness of output params (#349) * fix ghostness of a few outparams * backup * fix fmt (#351) * big clean-up (#354) * Drop Assumption in SetInfoField (#350) * proof setInfoField * fix verification errors * fix syntax error * fix verification errors * formatting * simplification attempt * Apply suggestions from code review Co-authored-by: João Pereira <[email protected]> * refactoring * fix verification error * fixed LeftSegEquality() * formatting * Apply suggestions from code review Co-authored-by: João Pereira <[email protected]> * feedback * renaming AbsSlice_Bytes to Bytes * adding documentation --------- Co-authored-by: João Pereira <[email protected]> * small clean-up (#355) * Simplification of segLens (#356) * simplification of SegLens * remove preconditions on CombineSegLens * fix verification error * renaming * make Len impure and add LenSpec (#357) * Format `info_hop_setter_lemmas.gobra` (#359) * fmt * fmt * Simplify validity criteria of paths (#352) * backup * backup * continue refactor * backup * Update pkg/slayers/path/epic/epic_spec_test.gobra * backup * merge with master * backup * fix verification error * backup * simplify preconditions * drop unnecessary method * fix annotation * fix verification error * minor fixes in styling * fix verification errors * proof of IsSupportedPkt (#363) * Drop two assumptions and merge validity criteria `StronglyValid` and `FullyValid` (#366) * backup * backup * fix verification error * fix test * fix another verification error * fix verification error * drop StronglyValid criteria * cleanup * Update gobra.yml * Update .github/workflows/gobra.yml * Update .github/workflows/gobra.yml * Drop SetHopfield related assumptions (#368) * proof of sethopfield and io-assumptions * fix syntax errors * fix termination measure * fix verification errors * simplifications and comments * fix syntax error * feedback * fix verification error * renaming * space between arithmetic operands * increase timeout of path/scion * fix verification error * test: parallelizeBranches for dependencies * test: increase timeout for scion package to 20 min * test: increase timeout for scion package to 1h * use parallelizeBranches only for scion package * stronger precondition for setHopfield * Revert "stronger precondition for setHopfield" * test: scion pkg without parallelizeBranches * Revert "test: scion pkg without parallelizeBranches" * fix merging mistake * assume postconditions in setHopfield * add comment to IO assumptions * increase timeout for scion package * revert timeout increase * feedback * Drop IO-assumptions in processOHP (#369) * move assumption from processOHP to updateSCIONLayer * proof of assumptions in processOHP * test: moreJoins for SerializeTo in slayers * fix verification error * feedback * add moreJoins to SerializeTo() * fix sytnax errors * fix some verification errors * make `hf_valid` opaque (#372) * make hf_valid opaque * backup * backup * might have to reverse this * backup * backup * Update router/io-spec-abstract-transitions.gobra * Update README.md * progress with verification errors --------- Co-authored-by: João Pereira <[email protected]> Co-authored-by: Dionysios Spiliopoulos <[email protected]> Co-authored-by: jiceatscion <[email protected]> Co-authored-by: Dspil <[email protected]> Co-authored-by: Matthias Frei <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I will continue this after we merge #243
This PR adds the proof of mem. safety of
processEPIC, as well as its corresponding path inprocessPkt, and makes the necessary changes in the other functions. Furthermore, it verifies the correctness of the remaining functions inlibepic. Because this introduces big slow-downs, I will wait with merging this PR until the IO proof is done for theSCIONcase (this PR is irrelevant for that case anyway. Instead, it affects only theUnsupported_pathtype.The changes inlibepicmay be merged already to guarantee that they do not fall out of syncTODO:
VerifyHVFinlibepicreport magic wand issue in libepic that forces one of the methods to betrustedprocessPkt, for some reason it is now much slowerTODO()inprocessEpic