Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* 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]>
- Loading branch information
6 people
authored
Aug 29, 2024
1 parent
c6f1d95
commit f0da265