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>

.github/workflows/gobra.yml

@@ -424,7 +424,7 @@ jobs:
           requireTriggers: ${{ env.requireTriggers }}
           overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
-          disableNL: ${{ env.disableNL }}
+          disableNL: '0'
           viperBackend: ${{ env.viperBackend }}
-          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          unsafeWildcardOptimization: '0'
 

pkg/slayers/path/scion/raw_spec.gobra

@@ -579,7 +579,7 @@ pure func (s *Raw) absPkt(dp io.DataPlaneSpec, raw []byte) (res io.IO_pkt2) {
 // the return type.
 ghost
 requires MetaLen <= len(raw)
-requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) 
+requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56)
 decreases
 pure func RawBytesToMetaHdr(raw []byte) MetaHdr {
 	return unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), R56) in