packSCMP Continued (#373)

* fix missing precondition for packSCMP

* progress scmp

* further progress

* further scmp fixes

* fix syntax error and strengthen spec of erros.Is function

* fix verification error

* fix verification errors in process()

* drop last scmp assumption

* fix verification errors in process()

* add missing postconditions to resolveInbound

* fix p.d permissions

* remove wrong precondition from validateEgressUp()

* clean up

* feedback

* Update router/dataplane.go

---------

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

pkg/private/serrors/serrors_spec.gobra

@@ -76,12 +76,12 @@ func Wrap(msg, cause error, errCtx ...interface{}) (res error)
 // Elements of errCtx are limited to "primitive types" at the moment.
 // This is a safe but strict under-approximation of what can be done
 // with this method.
-requires cause.ErrorMem()
+requires cause != nil ==> cause.ErrorMem()
 preserves forall i int :: { &errCtx[i] } 0 <= i && i < len(errCtx) ==> acc(&errCtx[i], R15)
 // The following precondition cannot be adequately captured in Gobra.
 // requires forall i int :: 0 <= i && i < len(errCtx) ==> IsOfPrimitiveType(errCtx[i])
 ensures res != nil && res.ErrorMem()
-ensures res.ErrorMem() --* cause.ErrorMem()
+ensures cause != nil ==> (res.ErrorMem() --* cause.ErrorMem())
 decreases
 func WrapStr(msg string, cause error, errCtx ...interface{}) (res error)
 

router/assumptions.gobra

@@ -15,7 +15,7 @@
 // +gobra
 
 // This file is used for declaring assumptions which we cannot currenlty do
-// away with, due to Gobra's incompletnesses or lack of support for 
+// away with, due to Gobra's incompletnesses or lack of support for
 // specific features, like post-initialization invariants or because
 // Gobra does not currently infer that 'x' != nil if 'x.Mem()' holds,
 // where 'x' is of an interface type.