Refactored Widen-lemma #327
Merged
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
…roject/VerifiedSCION into disable-conditionalizePermissions
jcp19
approved these changes
Apr 18, 2024
Co-authored-by: João Pereira <joaopereira.19@gmail.com>
Co-authored-by: João Pereira <joaopereira.19@gmail.com>
jcp19
added a commit
that referenced
this pull request
Aug 29, 2024
* 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 <139873336+jiceatscion@users.noreply.github.com> * 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 <32896454+Dspil@users.noreply.github.com> * Apply suggestions from code review Co-authored-by: João Pereira <joaopereira.19@gmail.com> * 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 <joaopereira.19@gmail.com> * 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 <dennisspiliopoylos@gmail.com> Co-authored-by: João Pereira <joaopereira.19@gmail.com> * 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 <joaopereira.19@gmail.com> * 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 <joaopereira.19@gmail.com> * 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 <dennisspiliopoylos@gmail.com> * backup * adapt to the new syntax of backend annotations * clean-up * changes according to feedback --------- Co-authored-by: João Pereira <joaopereira.19@gmail.com> Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com> Co-authored-by: Dspil <dennisspiliopoylos@gmail.com> * 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 <joaopereira.19@gmail.com> * 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 <joaopereira.19@gmail.com> * Drop unnecessary function `hopFieldsNotConsDir` (#303) * reverse hopFieldsNotConsDir once * remove hopfieldsNotConsDir * hopFieldsConsDir => hopFields --------- Co-authored-by: João Pereira <joaopereira.19@gmail.com> * 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 <joaopereira.19@gmail.com> * fmt --------- Co-authored-by: MLETHZ <mlimbeck@student.ethz.ch> Co-authored-by: Markus Limbeck <92801626+mlimbeck@users.noreply.github.com> Co-authored-by: João Pereira <joaopereira.19@gmail.com> * 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 <mlimbeck@student.ethz.ch> Co-authored-by: Dspil <dennisspiliopoylos@gmail.com> * 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 <joaopereira.19@gmail.com> * Update router/widen-lemma.gobra Co-authored-by: João Pereira <joaopereira.19@gmail.com> * joao * indent --------- Co-authored-by: João Pereira <joaopereira.19@gmail.com> Co-authored-by: Dspil <dennisspiliopoylos@gmail.com> Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com> * enable chop 10 in the CI (#328) * drop assumption in processPkt (#318) Co-authored-by: João Pereira <joaopereira.19@gmail.com> * 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 <joaopereira.19@gmail.com> --------- Co-authored-by: João Pereira <joaopereira.19@gmail.com> Co-authored-by: Dspil <dennisspiliopoylos@gmail.com> Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com> * router: forbid bouncing packets internally (#4502) (#332) Brings changes from scion pr 4502 Co-authored-by: Matthias Frei <matzf@scion.org> * 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 <joaopereira.19@gmail.com> * fmt of widen-lemma * further fmt * feedback * add comment * Update router/dataplane.go * Apply suggestions from code review --------- Co-authored-by: João Pereira <joaopereira.19@gmail.com> * 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 <joaopereira.19@gmail.com> * add quantifier to GetCurrentHopField() and GetCurrentInfoField() to avoid code changes * Apply suggestions from code review Co-authored-by: João Pereira <joaopereira.19@gmail.com> * formatting * simplify onehop * improve io_msgterm_spec.gobra --------- Co-authored-by: João Pereira <joaopereira.19@gmail.com> * Drop assumption in parsePath (#348) * drop assumption in parsePath * Update router/dataplane.go Co-authored-by: João Pereira <joaopereira.19@gmail.com> * rename arrayCongruence() to AbsMacArrayCongruence() --------- Co-authored-by: João Pereira <joaopereira.19@gmail.com> * 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 <joaopereira.19@gmail.com> * refactoring * fix verification error * fixed LeftSegEquality() * formatting * Apply suggestions from code review Co-authored-by: João Pereira <joaopereira.19@gmail.com> * feedback * renaming AbsSlice_Bytes to Bytes * adding documentation --------- Co-authored-by: João Pereira <joaopereira.19@gmail.com> * 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 <joaopereira.19@gmail.com> Co-authored-by: Dionysios Spiliopoulos <32896454+Dspil@users.noreply.github.com> Co-authored-by: jiceatscion <139873336+jiceatscion@users.noreply.github.com> Co-authored-by: Dspil <dennisspiliopoylos@gmail.com> Co-authored-by: Matthias Frei <matzf@scion.org>
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.
No description provided.