* redo short-circuiting operations

* Undo change

* Update router/dataplane.go

* experiment with disabling NL

* enable the wildcard optimization for when NL is disabled

* Apply suggestions from code review

* drop unnecessary annotations

* fix precond error

* fix verification error

* cleanup

* fix tiny error

* start overflow checking

* backup

* fix flags

* Apply suggestions from code review

* disable checks in all packages for now

* Update .github/workflows/gobra.yml

* R40

* epic

* extn

* onehop

* reduce permission amount of decode layers

* cherry-pick 4483

* undo change to test due to the use of (yet) undefined symbols

* fix verification error

---------

Co-authored-by: jiceatscion <[email protected]>

* first batch of changes from the IO spec

* Apply suggestions from code review

* adapt config options

* add termination checking if we ignore locking

* add termination checks modulo locking

* backup

* fix termination measure

* fix verification errors

* fix verification error

* 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]>

* minor renaming and merging of functions

* further renaming

* cleanup unnecessary code in the stdlib formalization

* replace occurrences of names with 'VerifiedSCION'

* backup

* remove more

* 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]>

* 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]>

Co-authored-by: João Pereira <[email protected]>

* change triggers in abspktwidenlemma

* triggers

* remove quantifiers

* 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]>

Brings changes from scion pr 4502

Co-authored-by: Matthias Frei <[email protected]>

* proof of scionfix #4502

* feedback

* drop assume in processOHP()

* change getDomExternal()   to opaque

* fix comment

* verification fix and simplification

* fix verification errors

* feedback

* drop trusted from method

* progress open io-lemmas

* fix verification errors

* refactoring

* fix verification error

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.

* drop DataPlaneSpec param from absPkt

* headerOffset change in absPkt

* fix syntax error

* fix verification errors

* fix verification errors

* fix LastHopLemma

* 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]>

* 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

* Update router/dataplane.go

Co-authored-by: João Pereira <[email protected]>

* rename arrayCongruence()  to AbsMacArrayCongruence()

---------

Co-authored-by: João Pereira <[email protected]>

* 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 a few outparams

* backup

* 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]>

* simplification of SegLens

* remove preconditions on CombineSegLens

* fix verification error

* renaming

* fmt

* fmt

* 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

…`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

* 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

* 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()

* make hf_valid opaque

* backup

* backup

* might have to reverse this

* backup

* backup

* Update router/io-spec-abstract-transitions.gobra