processEpic Continued

.github/workflows/gobra.yml

@@ -23,6 +23,10 @@ env:
   mceMode: 'od'
   requireTriggers: '1'
   useZ3API: '0'
+  viperBackend: 'SILICON'
+  disableNL: '0'
+  unsafeWildcardOptimization: '1'
+  overflow: '0'
 
 jobs:
   verify-deps:
@@ -60,7 +64,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/addr'
         uses: viperproject/gobra-action@main
         with:
@@ -76,12 +84,16 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/experimental/epic'
         uses: viperproject/gobra-action@main
         with:
           packages: 'pkg/experimental/epic'
-          timeout: 5m
+          timeout: 7m
           headerOnly: ${{ env.headerOnly }}
           module: ${{ env.module }}
           includePaths: ${{ env.includePaths }}
@@ -91,7 +103,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/log'
         uses: viperproject/gobra-action@main
         with:
@@ -106,7 +122,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/private/serrors'
         uses: viperproject/gobra-action@main
         with:
@@ -121,7 +141,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/scrypto'
         uses: viperproject/gobra-action@main
         with:
@@ -136,7 +160,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/slayers'
         uses: viperproject/gobra-action@main
         with:
@@ -151,7 +179,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/slayers/path'
         uses: viperproject/gobra-action@main
         with:
@@ -166,7 +198,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/slayers/path/empty'
         uses: viperproject/gobra-action@main
         with:
@@ -181,7 +217,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/slayers/path/epic'
         uses: viperproject/gobra-action@main
         with:
@@ -197,7 +237,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/slayers/path/onehop'
         uses: viperproject/gobra-action@main
         with:
@@ -212,7 +256,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'pkg/slayers/path/scion'
         uses: viperproject/gobra-action@main
         with:
@@ -227,7 +275,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'private/topology'
         uses: viperproject/gobra-action@main
         with:
@@ -242,7 +294,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'private/topology/underlay'
         uses: viperproject/gobra-action@main
         with:
@@ -257,7 +313,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'private/underlay/conn'
         uses: viperproject/gobra-action@main
         with:
@@ -272,7 +332,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'private/underlay/sockctrl'
         uses: viperproject/gobra-action@main
         with:
@@ -287,7 +351,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'router/bfd'
         uses: viperproject/gobra-action@main
         with:
@@ -302,7 +370,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Verify package 'router/control'
         uses: viperproject/gobra-action@main
         with:
@@ -317,7 +389,11 @@ jobs:
           imageVersion: ${{ env.imageVersion }}
           mceMode: ${{ env.mceMode }}
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
+          disableNL: ${{ env.disableNL }}
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
       - name: Upload the verification report
         uses: actions/upload-artifact@v2
         with:
@@ -339,12 +415,20 @@ jobs:
           includePaths: ${{ env.includePaths }}
           assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
           checkConsistency: ${{ env.checkConsistency }}
+          # Due to a bug introduced in https://github.com/viperproject/gobra/pull/776,
+          # we must currently disable the chopper, otherwise we well-founded orders
+          # for termination checking are not available at the chopped Viper parts.
+          # We should reenable it whenever possible, as it reduces verification time in
+          # ~8 min (20%).
+          # chop: 10
           parallelizeBranches: '1'
-          # The following flag has a significant influence on the number of branches verified.
-          # Without it, verification would take a lot longer.
           conditionalizePermissions: '1'
+          moreJoins: 'impure'
           imageVersion: ${{ env.imageVersion }}
           mceMode: 'on'
           requireTriggers: ${{ env.requireTriggers }}
+          overflow: ${{ env.overflow }}
           useZ3API: ${{ env.useZ3API }}
-
+          disableNL: '0'
+          viperBackend: ${{ env.viperBackend }}
+          unsafeWildcardOptimization: '0'

README.md

@@ -1,6 +1,6 @@
 # VerifiedSCION
 
-This package contains the **verified** implementation of the
+This package contains the **verified** implementation of the router from the
 [SCION](http://www.scion-architecture.net) protocol, a future Internet architecture.
 SCION is the first
 clean-slate Internet architecture designed to provide route control, failure
@@ -10,7 +10,7 @@ isolation, and explicit trust information for end-to-end communication.
 
 To find out more about the project, please visit the [official project page](https://www.pm.inf.ethz.ch/research/verifiedscion.html).
 
-> We are currently in the process of migrating the specifications and other annotations from the [original VerifiedSCION repository](https://github.com/jcp19/VerifiedSCION) to this one. This repository contains an up-to-date version of SCION (which we plan to keep updated), as well as improvements resulting from our experience from our first efforts on verifying SCION.
+> This repository contains a recent version of SCION (which we plan to keep updated), as well as fixes to the bugs we report as a result of verifying the SCION router from the mainline SCION repository.
 
 ## Methodology
 We focus on verifying the main implementation of SCION, written in the *Go* programming language.

pkg/addr/host.go

@@ -28,7 +28,7 @@ import (
 
 	"github.com/scionproto/scion/pkg/private/serrors"
 	//@ . "github.com/scionproto/scion/verification/utils/definitions"
-	//@ "github.com/scionproto/scion/verification/utils/slices"
+	//@ sl "github.com/scionproto/scion/verification/utils/slices"
 )
 
 type HostAddrType uint8
@@ -196,7 +196,7 @@ func (h HostIPv4) Pack() (res []byte) {
 func (h HostIPv4) IP() (res net.IP) {
 	// XXX(kormat): ensure the reply is the 4-byte representation.
 	//@ unfold acc(h.Mem(), R13)
-	//@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
 	return net.IP(h).To4( /*@ false @*/ )
 }
 
@@ -205,10 +205,10 @@ func (h HostIPv4) IP() (res net.IP) {
 // @ decreases
 func (h HostIPv4) Copy() (res HostAddr) {
 	//@ unfold acc(h.Mem(), R13)
-	//@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
 	var tmp HostIPv4 = HostIPv4(append( /*@ R13, @*/ net.IP(nil), h...))
-	//@ fold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
-	//@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+	//@ fold acc(sl.Bytes(h, 0, len(h)), R13)
+	//@ fold sl.Bytes(tmp, 0, len(tmp))
 	//@ fold acc(h.Mem(), R13)
 	//@ fold tmp.Mem()
 	return tmp
@@ -231,7 +231,7 @@ func (h HostIPv4) Equal(o HostAddr) bool {
 func (h HostIPv4) String() string {
 	//@ assert unfolding acc(h.Mem(), R13) in len(h) == HostLenIPv4
 	//@ ghost defer fold acc(h.Mem(), R13)
-	//@ ghost defer fold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+	//@ ghost defer fold acc(sl.Bytes(h, 0, len(h)), R13)
 	return h.IP().String()
 }
 
@@ -254,7 +254,7 @@ func (h HostIPv6) Type() HostAddrType {
 // @ decreases
 func (h HostIPv6) Pack() (res []byte) {
 	//@ unfold acc(h.Mem(), R13)
-	//@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
 	return []byte(h)[:HostLenIPv6]
 }
 
@@ -264,7 +264,7 @@ func (h HostIPv6) Pack() (res []byte) {
 // @ decreases
 func (h HostIPv6) IP() (res net.IP) {
 	//@ unfold acc(h.Mem(), R13)
-	//@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
 	return net.IP(h)
 }
 
@@ -273,10 +273,10 @@ func (h HostIPv6) IP() (res net.IP) {
 // @ decreases
 func (h HostIPv6) Copy() (res HostAddr) {
 	//@ unfold acc(h.Mem(), R13)
-	//@ unfold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
 	var tmp HostIPv6 = HostIPv6(append( /*@ R13, @*/ net.IP(nil), h...))
-	//@ fold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
-	//@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+	//@ fold acc(sl.Bytes(h, 0, len(h)), R13)
+	//@ fold sl.Bytes(tmp, 0, len(tmp))
 	//@ fold acc(h.Mem(), R13)
 	//@ fold tmp.Mem()
 	return tmp
@@ -299,7 +299,7 @@ func (h HostIPv6) Equal(o HostAddr) bool {
 func (h HostIPv6) String() string {
 	//@ assert unfolding acc(h.Mem(), R13) in len(h) == HostLenIPv6
 	//@ ghost defer fold acc(h.Mem(), R13)
-	//@ ghost defer fold acc(slices.AbsSlice_Bytes(h, 0, len(h)), R13)
+	//@ ghost defer fold acc(sl.Bytes(h, 0, len(h)), R13)
 	return h.IP().String()
 }
 
@@ -442,7 +442,7 @@ func HostFromRaw(b []byte, htype HostAddrType) (res HostAddr, err error) {
 		}
 		//@ assert forall i int :: { &b[:HostLenIPv4][i] } 0 <= i && i < len(b[:HostLenIPv4]) ==> &b[:HostLenIPv4][i] == &b[i]
 		tmp := HostIPv4(b[:HostLenIPv4])
-		//@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+		//@ fold sl.Bytes(tmp, 0, len(tmp))
 		//@ fold tmp.Mem()
 		return tmp, nil
 	case HostTypeIPv6:
@@ -451,7 +451,7 @@ func HostFromRaw(b []byte, htype HostAddrType) (res HostAddr, err error) {
 		}
 		//@ assert forall i int :: { &b[:HostLenIPv4][i] } 0 <= i && i < len(b[:HostLenIPv4]) ==> &b[:HostLenIPv4][i] == &b[i]
 		tmp := HostIPv6(b[:HostLenIPv6])
-		//@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+		//@ fold sl.Bytes(tmp, 0, len(tmp))
 		//@ fold tmp.Mem()
 		return tmp, nil
 	case HostTypeSVC:
@@ -473,12 +473,12 @@ func HostFromRaw(b []byte, htype HostAddrType) (res HostAddr, err error) {
 func HostFromIP(ip net.IP) (res HostAddr) {
 	if ip4 := ip.To4( /*@ false @*/ ); ip4 != nil {
 		tmp := HostIPv4(ip4)
-		//@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+		//@ fold sl.Bytes(tmp, 0, len(tmp))
 		//@ fold tmp.Mem()
 		return tmp
 	}
 	tmp := HostIPv6(ip)
-	//@ fold slices.AbsSlice_Bytes(tmp, 0, len(tmp))
+	//@ fold sl.Bytes(tmp, 0, len(tmp))
 	//@ fold tmp.Mem()
 	return tmp
 }