Specify package-level invariants

.github/workflows/gobra.yml

@@ -21,7 +21,10 @@ env:
   checkConsistency: '1'
   imageVersion: 'latest'
   mceMode: 'od'
-  requireTriggers: '1'
+  # disabled for now, as it is unclear which triggers to
+  # provide to monoset in a way that it does not severely
+  # affect perf.
+  requireTriggers: '0'
   useZ3API: '0'
   viperBackend: 'SILICON'
   disableNL: '0'

pkg/addr/host.go

@@ -15,9 +15,16 @@
 
 // +gobra
 
-// @ initEnsures ErrBadHostAddrType.ErrorMem()
-// @ initEnsures ErrMalformedHostAddrType.ErrorMem()
-// @ initEnsures ErrUnsupportedSVCAddress.ErrorMem()
+// @ dup pkgInvariant ErrBadHostAddrType != nil              &&
+// @ 	ErrMalformedHostAddrType != nil                      &&
+// @ 	ErrUnsupportedSVCAddress != nil                      &&
+// @ 	acc(ErrBadHostAddrType.ErrorMem(), _)                &&
+// @ 	acc(ErrMalformedHostAddrType.ErrorMem(), _)          &&
+// @ 	acc(ErrUnsupportedSVCAddress.ErrorMem(), _)          &&
+// @ 	ErrBadHostAddrType.IsDuplicableMem()                 &&
+// @ 	ErrMalformedHostAddrType.IsDuplicableMem()           &&
+// @ 	ErrUnsupportedSVCAddress.IsDuplicableMem()
+
 package addr
 
 import (
@@ -206,7 +213,7 @@ func (h HostIPv4) IP() (res net.IP) {
 func (h HostIPv4) Copy() (res HostAddr) {
 	//@ unfold acc(h.Mem(), R13)
 	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
-	var tmp HostIPv4 = HostIPv4(append( /*@ R13, @*/ net.IP(nil), h...))
+	tmp := HostIPv4(append( /*@ R13, @*/ net.IP(nil), h...))
 	//@ fold acc(sl.Bytes(h, 0, len(h)), R13)
 	//@ fold sl.Bytes(tmp, 0, len(tmp))
 	//@ fold acc(h.Mem(), R13)
@@ -274,7 +281,7 @@ func (h HostIPv6) IP() (res net.IP) {
 func (h HostIPv6) Copy() (res HostAddr) {
 	//@ unfold acc(h.Mem(), R13)
 	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
-	var tmp HostIPv6 = HostIPv6(append( /*@ R13, @*/ net.IP(nil), h...))
+	tmp := HostIPv6(append( /*@ R13, @*/ net.IP(nil), h...))
 	//@ fold acc(sl.Bytes(h, 0, len(h)), R13)
 	//@ fold sl.Bytes(tmp, 0, len(tmp))
 	//@ fold acc(h.Mem(), R13)

pkg/addr/host_spec.gobra

@@ -19,6 +19,7 @@ package addr
 import (
 	"net"
 
+	"github.com/scionproto/scion/verification/utils/errors"
 	"github.com/scionproto/scion/verification/utils/slices"
 )
 
@@ -70,3 +71,27 @@ pure func sizeOfHostAddrType(htype HostAddrType) (res int) {
 		HostLenIPv4 : htype == HostTypeIPv6 ?
 		HostLenIPv6 : HostLenSVC
 }
+
+ghost
+ensures ErrBadHostAddrType.ErrorMem()
+decreases
+func EstablishErrBadHostAddrTypeMem() {
+	openDupPkgInv
+	errors.DupErrorsCanBePromoted(ErrBadHostAddrType)
+}
+
+ghost
+ensures ErrMalformedHostAddrType.ErrorMem()
+decreases
+func EstablishErrMalformedHostAddrTypeMem() {
+	openDupPkgInv
+	errors.DupErrorsCanBePromoted(ErrMalformedHostAddrType)
+}
+
+ghost
+ensures ErrUnsupportedSVCAddress.ErrorMem()
+decreases
+func EstablishErrUnsupportedSVCAddressMem() {
+	openDupPkgInv
+	errors.DupErrorsCanBePromoted(ErrUnsupportedSVCAddress)
+}

pkg/experimental/epic/epic.go

@@ -14,7 +14,7 @@
 
 // +gobra
 
-// @ initEnsures acc(postInitInvariant(), _)
+// @ dup pkgInvariant acc(postInitInvariant(), _)
 package epic
 
 import (

pkg/experimental/epic/epic_spec.gobra

@@ -26,7 +26,8 @@ pred postInitInvariant() {
 
 // learn the invariant established by init
 ghost
-trusted // TODO: drop after init invs are added
 ensures acc(postInitInvariant(), _)
 decreases _
-func establishPostInitInvariant()
+func establishPostInitInvariant() {
+	openDupPkgInv
+}

pkg/slayers/layertypes_spec.gobra

@@ -18,16 +18,11 @@
 // +gobra
 
 // To be added on a per-need basis
-initEnsures LayerTypeSCION == 1000
+dup pkgInvariant LayerTypeSCION == 1000
 package slayers
 
 import (
 	"github.com/google/gopacket"
-
-	// the following comes from gopacket/layers instead of gopacket
-	importRequires gopacket.LayerTypesMem()
-	importRequires forall t gopacket.LayerType :: { gopacket.Registered(t) } 1000 <= t ==>
-		!gopacket.Registered(t)
 	"github.com/google/gopacket/layers"
 )
 
@@ -60,20 +55,23 @@ var (
 
 // post init properties
 ghost
+trusted
 ensures res === LayerClassSCION
 ensures res != nil
 ensures res == (gopacket.LayerClass)(gopacket.LayerType(1000))
 decreases
 func LayerClassSCIONIsLayerType() (res gopacket.LayerClass)
 
 ghost
+trusted
 ensures res === LayerClassSCMP
 ensures res != nil
 ensures res == (gopacket.LayerClass)(gopacket.LayerType(1002))
 decreases
 func LayerClassSCMPIsLayerType() (res gopacket.LayerClass)
 
 ghost
+trusted
 ensures res === LayerClassHopByHopExtn
 ensures res != nil
 ensures res == (gopacket.LayerClass)(gopacket.LayerType(1003))

pkg/slayers/path/empty/empty.go

@@ -26,12 +26,10 @@ const PathLen = 0
 
 const PathType path.Type = 0
 
-// @ requires path.PathPackageMem()
-// @ requires !path.Registered(PathType)
-// @ ensures  path.PathPackageMem()
-// @ ensures  forall t path.Type :: { old(path.Registered(t)) }{ path.Registered(t) } 0 <= t && t < path.MaxPathType ==>
-// @ 	t != PathType ==> old(path.Registered(t)) == path.Registered(t)
-// @ ensures  path.Registered(PathType)
+// @ requires path.PkgMem()
+// @ requires path.RegisteredTypes().DoesNotContain(int64(PathType))
+// @ ensures  path.PkgMem()
+// @ ensures  path.RegisteredTypes().Contains(int64(PathType))
 // @ decreases
 func RegisterPath() {
 	tmp := path.Metadata{
@@ -48,7 +46,7 @@ func RegisterPath() {
 		},
 	}
 	//@ proof tmp.New implements path.NewPathSpec {
-	//@		return tmp.New() as newPath
+	//@ 	return tmp.New() as newPath
 	//@ }
 	path.RegisterPath(tmp)
 }

pkg/slayers/path/epic/epic.go

@@ -41,12 +41,10 @@ const (
 )
 
 // RegisterPath registers the EPIC path type globally.
-// @ requires path.PathPackageMem()
-// @ requires !path.Registered(PathType)
-// @ ensures  path.PathPackageMem()
-// @ ensures  forall t path.Type :: { old(path.Registered(t)) }{ path.Registered(t) } 0 <= t && t < path.MaxPathType ==>
-// @ 	t != PathType ==> old(path.Registered(t)) == path.Registered(t)
-// @ ensures  path.Registered(PathType)
+// @ requires path.PkgMem()
+// @ requires path.RegisteredTypes().DoesNotContain(int64(PathType))
+// @ ensures  path.PkgMem()
+// @ ensures  path.RegisteredTypes().Contains(int64(PathType))
 // @ decreases
 func RegisterPath() {
 	tmp := path.Metadata{
@@ -65,7 +63,7 @@ func RegisterPath() {
 		},
 	}
 	//@ proof tmp.New implements path.NewPathSpec {
-	//@		return tmp.New() as newPath
+	//@ 	return tmp.New() as newPath
 	//@ }
 	path.RegisterPath(tmp)
 }

pkg/slayers/path/onehop/onehop.go

@@ -29,12 +29,10 @@ const PathLen = path.InfoLen + 2*path.HopLen
 
 const PathType path.Type = 2
 
-// @ requires path.PathPackageMem()
-// @ requires !path.Registered(PathType)
-// @ ensures  path.PathPackageMem()
-// @ ensures  forall t path.Type :: { old(path.Registered(t)) }{ path.Registered(t) } 0 <= t && t < path.MaxPathType ==>
-// @ 	t != PathType ==> old(path.Registered(t)) == path.Registered(t)
-// @ ensures  path.Registered(PathType)
+// @ requires path.PkgMem()
+// @ requires path.RegisteredTypes().DoesNotContain(int64(PathType))
+// @ ensures  path.PkgMem()
+// @ ensures  path.RegisteredTypes().Contains(int64(PathType))
 // @ decreases
 func RegisterPath() {
 	tmp := path.Metadata{
@@ -51,7 +49,7 @@ func RegisterPath() {
 		},
 	}
 	//@ proof tmp.New implements path.NewPathSpec {
-	//@		return tmp.New() as newPath
+	//@ 	return tmp.New() as newPath
 	//@ }
 	path.RegisterPath(tmp)
 }

pkg/slayers/path/path.go

@@ -14,18 +14,21 @@
 
 // +gobra
 
-// @ initEnsures PathPackageMem()
-// Skipped the following post-condition due to performance reasons
-// initEnsures forall t Type :: 0 <= t && t < maxPathType ==> !Registered(t)
-// Instead, we have:
-// @ initEnsures !Registered(0) && !Registered(1) && !Registered(2) && !Registered(3)
 package path
 
+// @ friendPkg "github.com/scionproto/scion/pkg/slayers" PkgMem()
+// We have a non-quantified friendPkg clause below to avoid perf. issues.
+// @ friendPkg "github.com/scionproto/scion/pkg/slayers" RegisteredTypes().DoesNotContain(0) &&
+// @ 	RegisteredTypes().DoesNotContain(1) &&
+// @ 	RegisteredTypes().DoesNotContain(2) &&
+// @ 	RegisteredTypes().DoesNotContain(3)
+
 import (
 	"fmt"
 
 	"github.com/scionproto/scion/pkg/private/serrors"
 	//@ . "github.com/scionproto/scion/verification/utils/definitions"
+	//@ "github.com/scionproto/scion/verification/utils/monoset"
 	//@ sl "github.com/scionproto/scion/verification/utils/slices"
 )
 
@@ -37,22 +40,24 @@ var (
 	strictDecoding/*@@@*/ bool = true
 )
 
+// @ ghost var registeredKeys monoset.BoundedMonotonicSet = monoset.Alloc(0, int64(maxPathType))
+
 func init() {
 	// (VerifiedSCION) ghost initialization code to establish the PathPackageMem predicate.
 	// @ assert acc(&registeredPaths)
 	// @ assert acc(&strictDecoding)
-	// @ fold PathPackageMem()
+	// @ fold PkgMem()
 }
 
 // Type indicates the type of the path contained in the SCION header.
 type Type uint8
 
 // @ requires 0 <= t && t < maxPathType
-// @ preserves acc(PathPackageMem(), R20)
+// @ preserves acc(PkgMem(), R20)
 // @ decreases
 func (t Type) String() string {
-	//@ unfold acc(PathPackageMem(), R20)
-	//@ ghost defer fold acc(PathPackageMem(), R20)
+	//@ unfold acc(PkgMem(), R20)
+	//@ ghost defer fold acc(PkgMem(), R20)
 	pm := registeredPaths[t]
 	if !pm.inUse {
 		return fmt.Sprintf("UNKNOWN (%d)", t)
@@ -144,23 +149,24 @@ type Metadata struct {
 // RegisterPath registers a new SCION path type globally.
 // The PathType passed in must be unique, or a runtime panic will occur.
 // @ requires 0 <= pathMeta.Type && pathMeta.Type < maxPathType
-// @ requires PathPackageMem()
-// @ requires !Registered(pathMeta.Type)
+// @ requires PkgMem()
+// @ requires RegisteredTypes().DoesNotContain(int64(pathMeta.Type))
 // @ requires pathMeta.New implements NewPathSpec
-// @ ensures  PathPackageMem()
-// @ ensures  forall t Type :: { old(Registered(t)) }{ Registered(t) } 0 <= t && t < maxPathType ==>
-// @ 	t != pathMeta.Type ==> old(Registered(t)) == Registered(t)
-// @ ensures  Registered(pathMeta.Type)
+// @ ensures  PkgMem()
+// @ ensures  RegisteredTypes().Contains(int64(pathMeta.Type))
 // @ decreases
 func RegisterPath(pathMeta Metadata) {
-	//@ unfold PathPackageMem()
+	//@ unfold PkgMem()
 	pm := registeredPaths[pathMeta.Type]
+	// @ RegisteredTypes().DoesNotContainImpliesNotFContains(int64(pathMeta.Type))
 	if pm.inUse {
 		panic("path type already registered")
 	}
+	// @ RegisteredTypes().Add(int64(pathMeta.Type))
 	registeredPaths[pathMeta.Type].inUse = true
 	registeredPaths[pathMeta.Type].Metadata = pathMeta
-	//@ fold PathPackageMem()
+	// @ RegisteredTypes().ContainsImpliesFContains(int64(pathMeta.Type))
+	//@ fold PkgMem()
 }
 
 // StrictDecoding enables or disables strict path decoding. If enabled, unknown
@@ -170,23 +176,23 @@ func RegisterPath(pathMeta Metadata) {
 // Strict parsing is enabled by default.
 //
 // Experimental: This function is experimental and might be subject to change.
-// @ requires PathPackageMem()
-// @ ensures  PathPackageMem()
+// @ requires PkgMem()
+// @ ensures  PkgMem()
 // @ decreases
 func StrictDecoding(strict bool) {
-	//@ unfold PathPackageMem()
+	//@ unfold PkgMem()
 	strictDecoding = strict
-	//@ fold PathPackageMem()
+	//@ fold PkgMem()
 }
 
 // NewPath returns a new path object of pathType.
 // @ requires 0 <= pathType && pathType < maxPathType
-// @ requires acc(PathPackageMem(), _)
+// @ requires acc(PkgMem(), _)
 // @ ensures  e != nil ==> e.ErrorMem()
 // @ ensures  e == nil ==> p != nil && p.NonInitMem()
 // @ decreases
 func NewPath(pathType Type) (p Path, e error) {
-	//@ unfold acc(PathPackageMem(), _)
+	//@ unfold acc(PkgMem(), _)
 	pm := registeredPaths[pathType]
 	if !pm.inUse {
 		if strictDecoding {