Use new support for invariants

router/dataplane_concurrency_model.gobra

@@ -17,7 +17,6 @@
 package router
 
 import (
-	gsync "verification/utils/ghost_sync"
 	"verification/utils/resalgebra"
 	io "verification/io"
 )
@@ -38,35 +37,36 @@ pred SharedInv(ghost dp io.DataPlaneSpec, ghost y SharedArg) {
 // initialize the shared invariant:
 ghost
 requires io.IOToken(p) && dp.Dp3s_iospec_ordered(s, p)
-ensures  m.LockP() && m.LockInv() == SharedInv{dp, y}
+ensures  Invariant(SharedInv{dp, y})
 decreases
 func InitSharedInv(
 	dp io.DataPlaneSpec,
 	p io.Place,
-	s io.Dp3sStateLocal) (m gpointer[gsync.GhostMutex], y SharedArg) {
-	mV@ := gsync.GhostMutex{}
-	m = &mV
+	s io.Dp3sStateLocal) (y SharedArg) {
 	pE@ := p
 	sE@ := s
 	yI := InitElemAuth(s.Ibuf)
 	yO := InitElemAuth(s.Obuf)
 	y := SharedArg{&pE, &sE, yI, yO}
 	fold SharedInv{dp, y}()
-	m.SetInv(SharedInv{dp, y})
+	EstablishInvariant(SharedInv{dp, y})
+	return y
 }
 
-/////////////////////////////////////// Prophecies ///////////////////////////////////////
-// To establish permission for incoming packets, we need to predict the quantity.
-// The return value of AllocProphecy is assumed to be identical to the actual number
-// of received packets.
-pred Prophecy(int)
-
-ghost
-ensures 0 <= expectedPkts && Prophecy(expectedPkts)
-decreases
-func AllocProphecy() (expectedPkts int)
-
 /////////////////////////////////////// MultiBio ///////////////////////////////////////
+// The definitions in this section describe the effect that receiving a batch of
+// `expectedPkts` packets has on the state of the model: `MultiReadBio` is the permission to
+// perform that many consecutive `recv` transitions, `MultiReadBioNext` and `MultiReadBioUpd`
+// compute the place and the local state that result from performing them, and
+// `MultiReadBioIO_val` collects the abstract values of the packets that are received.
+//
+// Because Gobra does not allow interface methods to be marked as `atomic`, these transitions
+// can no longer be performed by the caller of `BatchConn.ReadBatch` while holding the shared
+// invariant open; they are instead assumed to be performed inside `ReadBatch` itself (see the
+// comment on its contract). These definitions remain here because they specify precisely the
+// effect that `ReadBatch` is assumed to have on the shared invariant, and because
+// `ExtractRecvPermissions` below discharges every part of that effect that does not require
+// physically receiving a packet.
 
 pred MultiReadBio(ghost t io.Place, ghost expectedPkts int) {
 	(expectedPkts > 0 ==> io.CBioIO_bio3s_recv(t) &&
@@ -190,6 +190,49 @@ func MultiUpdateElemWitness(
 	}
 }
 
+// Shows that the permission to receive an arbitrary number `n` of packets can always be
+// extracted from the IO permissions of the shared invariant. Given the contents of
+// `SharedInv{dp, y}` for the place `t` and the local state `s`, this lemma yields the permission
+// to perform `n` consecutive `recv` transitions, the abstract values `ioValSeq` of the packets
+// that are received, the place `tN` and the local state `sN` that result from performing them,
+// and, provided that all of these packets are received from the interface `k`, a witness for
+// every one of them. Notice that the invariant cannot be closed again by this lemma, as the IO
+// token is still at the place `t`; that is why the lemma operates on the contents of the
+// invariant instead of on `Invariant(SharedInv{dp, y})` itself.
+//
+// This lemma is the proof obligation underlying the IO specification that is assumed for
+// `BatchConn.ReadBatch` (cf. the comment on its contract): every part of the effect that
+// `ReadBatch` is assumed to have on the shared invariant follows from the invariant alone,
+// with the single exception of advancing the IO token from `t` to `tN`, which is the physical
+// reception of the packets and thus cannot be discharged by a ghost lemma. The lemma is not
+// applied by the router itself, because `ReadBatch` may not be marked as `atomic` and thus
+// performs all of these steps internally.
+ghost
+requires 0 <= n
+requires dp.Dp3s_iospec_ordered(s, t)
+requires ElemAuth(s.Ibuf, y.IBufY) && ElemAuth(s.Obuf, y.OBufY)
+ensures  MultiReadBio(t, n)
+ensures  sN == MultiReadBioUpd(t, n, s)
+ensures  tN == MultiReadBioNext(t, n)
+ensures  ioValSeq == MultiReadBioIO_val(t, n) && len(ioValSeq) == n
+ensures  dp.Dp3s_iospec_ordered(sN, tN)
+ensures  ElemAuth(sN.Ibuf, y.IBufY) && ElemAuth(sN.Obuf, y.OBufY)
+ensures  MultiReadBioCorrectIfs(t, n, k) ==> MultiElemWitness(y.IBufY, k, ioValSeq)
+decreases
+func ExtractRecvPermissions(
+	dp io.DataPlaneSpec,
+	t io.Place,
+	n int,
+	s io.Dp3sStateLocal,
+	k Key,
+	y SharedArg) (ioValSeq seq[io.Val], sN io.Dp3sStateLocal, tN io.Place) {
+	ExtractMultiReadBio(dp, t, n, s)
+	MultiUpdateElemWitness(t, n, k, s, y)
+	ioValSeq = MultiReadBioIO_val(t, n)
+	sN = MultiReadBioUpd(t, n, s)
+	tN = MultiReadBioNext(t, n)
+}
+
 // Every well-formed packet is accompanied by a witness. Establishing the MultiElemWitness
 // predicate recursively is easier, but working with an index is more convenient.
 pred MultiElemWitness(ghost y ElemRA, ghost k Key, ghost es seq[io.Val]) {

router/gobra.json

@@ -3,5 +3,6 @@
   "mce_mode": "on",
   "more_joins": "impure",
   "conditionalize_permissions": true,
-  "parallelize_branches": false
+  "parallelize_branches": false,
+  "assert_timeout": 120000
 }

router/io-spec-abstract-transitions.gobra

@@ -22,7 +22,6 @@ import (
 	"github.com/scionproto/scion/pkg/slayers"
 	. "verification/utils/definitions"
 	io "verification/io"
-	gsync "verification/utils/ghost_sync"
 	sl "verification/utils/slices"
 )
 
@@ -199,6 +198,7 @@ pure func PktUpdate(pkt io.Pkt, ingressID option[io.Ifs], egressID option[io.Ifs
 // from a different AS (ingressID != none[io.Ifs])
 // and will be forwarded to another border router within the AS (egressID == none[io.Ifs])
 ghost
+opensInvariants
 requires  dp.Valid()
 requires  ingressID != none[io.Ifs]
 requires  egressID == none[io.Ifs]
@@ -208,18 +208,17 @@ requires  newPkt == AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)
 requires  AbsValidateIngressIDConstraint(oldPkt, ingressID)
 requires  AbsVerifyCurrentMACConstraint(newPkt, dp)
 requires  len(newPkt.CurrSeg.Future) == 1 || AbsValidateEgressIDConstraint(newPkt, true, dp)
-preserves acc(ioLock.LockP(), _)
-preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
+preserves Invariant(SharedInv{dp, ioSharedArg})
 ensures   ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
 decreases
-func InternalEnterEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+func InternalEnterEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
 	reveal AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)
 	reveal AbsValidateIngressIDConstraint(oldPkt, ingressID)
 	reveal AbsVerifyCurrentMACConstraint(newPkt, dp)
 	if(len(newPkt.CurrSeg.Future) != 1) {
 		reveal AbsValidateEgressIDConstraint(newPkt, true, dp)
 	}
-	AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)
+	AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioSharedArg, dp)
 }
 
 // Either this executes the IO enter event whenever a pkt was received
@@ -229,6 +228,7 @@ func InternalEnterEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt,
 // within the AS (ingressID == none[io.Ifs])
 // and will leave the AS (egressID != none[io.Ifs])
 ghost
+opensInvariants
 requires  dp.Valid()
 requires  egressID != none[io.Ifs]
 requires  get(egressID) elem domain(dp.GetNeighborIAs())
@@ -239,11 +239,10 @@ requires  AbsVerifyCurrentMACConstraint(AbsUpdateNonConsDirIngressSegID(oldPkt,
 requires  AbsValidateEgressIDConstraint(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID), (ingressID != none[io.Ifs]), dp)
 requires  AbsEgressInterfaceConstraint(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID), egressID)
 requires  newPkt == AbsProcessEgress(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID))
-preserves acc(ioLock.LockP(), _)
-preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
+preserves Invariant(SharedInv{dp, ioSharedArg})
 ensures   ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
 decreases
-func ExternalEnterOrExitEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+func ExternalEnterOrExitEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
 	reveal dp.Valid()
 	nextPkt := reveal AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)
 	reveal AbsValidateIngressIDConstraint(oldPkt, ingressID)
@@ -252,16 +251,17 @@ func ExternalEnterOrExitEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io
 	reveal AbsValidateEgressIDConstraint(nextPkt, (ingressID != none[io.Ifs]), dp)
 	reveal AbsProcessEgress(nextPkt)
 	if(ingressID == none[io.Ifs]){
-		AtomicExit(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)
+		AtomicExit(oldPkt, ingressID, newPkt, egressID, ioSharedArg, dp)
 	} else {
-		AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)
+		AtomicEnter(oldPkt, ingressID, newPkt, egressID, ioSharedArg, dp)
 	}
 }
 
 // This executes the IO xover event whenever a pkt was received
 // from a different AS (ingressID != none[io.Ifs])
 // and a segment switch was performed.
 ghost
+opensInvariants
 requires  dp.Valid()
 requires  ingressID != none[io.Ifs]
 requires  oldPkt.PathNotFullyTraversed()
@@ -280,11 +280,10 @@ requires  egressID == none[io.Ifs] ==>
 	newPkt == AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID))
 requires  egressID != none[io.Ifs] ==>
 	newPkt == AbsProcessEgress(AbsDoXover(AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)))
-preserves acc(ioLock.LockP(), _)
-preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
+preserves Invariant(SharedInv{dp, ioSharedArg})
 ensures   ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
 decreases
-func XoverEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+func XoverEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
 	reveal dp.Valid()
 	intermediatePkt1 := reveal AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)
 	intermediatePkt2 := reveal AbsDoXover(intermediatePkt1)
@@ -296,5 +295,5 @@ func XoverEvent(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID
 		reveal AbsEgressInterfaceConstraint(intermediatePkt2, egressID)
 		reveal AbsProcessEgress(intermediatePkt2)
 	}
-	AtomicXover(oldPkt, ingressID, newPkt, egressID, ioLock, ioSharedArg, dp)
+	AtomicXover(oldPkt, ingressID, newPkt, egressID, ioSharedArg, dp)
 }

router/io-spec-atomic-events.gobra

@@ -15,21 +15,16 @@
 // +gobra
 
 // This file contains the definition of operations that perform the atomic transitions of state
-// in the IO spec. They all take a gpointer[gsync.GhostMutex], which acts as a logical invariant, because Gobra
-// does not support invariants natively. As such, we can only get access to the invariants if we
-// first lock the mutex. Even though all these operations are
-// terminating, Gobra cannot currently prove this and thus, we assume termination for all methods
-// in this file.
+// in the IO spec.
 
 package router
 
 import (
-	"sync"
 	io "verification/io"
-	gsync "verification/utils/ghost_sync"
 )
 
 ghost
+opensInvariants
 requires  dp.Valid()
 requires  ingressID != none[io.Ifs]
 requires  len(oldPkt.CurrSeg.Future) > 0
@@ -51,60 +46,60 @@ requires  dp.Dp3s_forward(
 	},
 	newPkt,
 	egressID)
-preserves acc(ioLock.LockP(), _)
-preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
+preserves Invariant(SharedInv{dp, ioSharedArg})
 ensures   ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
-decreases _
-func AtomicEnter(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
-	ghost ioLock.Lock()
-	unfold SharedInv{dp, ioSharedArg}()
-	t, s := *ioSharedArg.Place, *ioSharedArg.State
-	ApplyElemWitness(s.Ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
-	ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID})
-	assert dp.Dp3s_iospec_bio3s_enter_guard(s, t, pkt_internal)
-	unfold dp.Dp3s_iospec_ordered(s, t)
-	unfold dp.Dp3s_iospec_bio3s_enter(s, t)
-	io.TriggerBodyIoEnter(pkt_internal)
-	tN := io.CBio_IN_bio3s_enter_T(t, pkt_internal)
-	io.Enter(t, pkt_internal) //Event
-	UpdateElemWitness(s.Obuf, ioSharedArg.OBufY, egressID, newPkt)
-	ghost *ioSharedArg.State = io.Dp3s_add_obuf(s, egressID, newPkt)
-	ghost *ioSharedArg.Place = tN
-	fold SharedInv{dp, ioSharedArg}()
-	ghost ioLock.Unlock()
+decreases
+func AtomicEnter(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+	critical SharedInv{dp, ioSharedArg} (
+		unfold SharedInv{dp, ioSharedArg}()
+		t, s := *ioSharedArg.Place, *ioSharedArg.State
+		ApplyElemWitness(s.Ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
+		ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID})
+		assert dp.Dp3s_iospec_bio3s_enter_guard(s, t, pkt_internal)
+		unfold dp.Dp3s_iospec_ordered(s, t)
+		unfold dp.Dp3s_iospec_bio3s_enter(s, t)
+		io.TriggerBodyIoEnter(pkt_internal)
+		ghost tN := io.CBio_IN_bio3s_enter_T(t, pkt_internal)
+		io.Enter(t, pkt_internal) //Event
+		UpdateElemWitness(s.Obuf, ioSharedArg.OBufY, egressID, newPkt)
+		ghost *ioSharedArg.State = io.Dp3s_add_obuf(s, egressID, newPkt)
+		ghost *ioSharedArg.Place = tN
+		fold SharedInv{dp, ioSharedArg}()
+	)
 }
 
 ghost
+opensInvariants
 requires  dp.Valid()
 requires  ingressID == none[io.Ifs]
 requires  egressID != none[io.Ifs]
 requires  len(oldPkt.CurrSeg.Future) > 0
 requires  ElemWitness(ioSharedArg.IBufY, ingressID, oldPkt)
 requires  dp.Dp3s_forward_ext(oldPkt, newPkt, get(egressID))
-preserves acc(ioLock.LockP(), _)
-preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
+preserves Invariant(SharedInv{dp, ioSharedArg})
 ensures   ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
-decreases _
-func AtomicExit(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
-	ghost ioLock.Lock()
-	unfold SharedInv{dp, ioSharedArg}()
-	t, s := *ioSharedArg.Place, *ioSharedArg.State
-	ApplyElemWitness(s.Ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
-	ghost pkt_internal := io.Val(io.ValInternal2{oldPkt, newPkt, get(egressID)})
-	assert dp.Dp3s_iospec_bio3s_exit_guard(s, t, pkt_internal)
-	unfold dp.Dp3s_iospec_ordered(s, t)
-	unfold dp.Dp3s_iospec_bio3s_exit(s, t)
-	io.TriggerBodyIoExit(pkt_internal)
-	tN := io.Dp3s_iospec_bio3s_exit_T(t, pkt_internal)
-	io.Exit(t, pkt_internal) //Event
-	UpdateElemWitness(s.Obuf, ioSharedArg.OBufY, egressID, newPkt)
-	ghost *ioSharedArg.State = io.Dp3s_add_obuf(s, egressID, newPkt)
-	ghost *ioSharedArg.Place = tN
-	fold SharedInv{dp, ioSharedArg}()
-	ghost ioLock.Unlock()
+decreases
+func AtomicExit(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+	critical SharedInv{dp, ioSharedArg} (
+		unfold SharedInv{dp, ioSharedArg}()
+		t, s := *ioSharedArg.Place, *ioSharedArg.State
+		ApplyElemWitness(s.Ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
+		ghost pkt_internal := io.Val(io.ValInternal2{oldPkt, newPkt, get(egressID)})
+		assert dp.Dp3s_iospec_bio3s_exit_guard(s, t, pkt_internal)
+		unfold dp.Dp3s_iospec_ordered(s, t)
+		unfold dp.Dp3s_iospec_bio3s_exit(s, t)
+		io.TriggerBodyIoExit(pkt_internal)
+		ghost tN := io.Dp3s_iospec_bio3s_exit_T(t, pkt_internal)
+		io.Exit(t, pkt_internal) //Event
+		UpdateElemWitness(s.Obuf, ioSharedArg.OBufY, egressID, newPkt)
+		ghost *ioSharedArg.State = io.Dp3s_add_obuf(s, egressID, newPkt)
+		ghost *ioSharedArg.Place = tN
+		fold SharedInv{dp, ioSharedArg}()
+	)
 }
 
 ghost
+opensInvariants
 requires  dp.Valid()
 requires  oldPkt.LeftSeg != none[io.Seg]
 requires  len(oldPkt.CurrSeg.Future) > 0
@@ -136,25 +131,24 @@ requires  dp.Dp3s_forward_xover(
 	},
 	newPkt,
 	egressID)
-preserves acc(ioLock.LockP(), _)
-preserves ioLock.LockInv() == SharedInv{dp, ioSharedArg}
+preserves Invariant(SharedInv{dp, ioSharedArg})
 ensures   ElemWitness(ioSharedArg.OBufY, egressID, newPkt)
-decreases _
-func AtomicXover(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
-	ghost ioLock.Lock()
-	unfold SharedInv{dp, ioSharedArg}()
-	t, s := *ioSharedArg.Place, *ioSharedArg.State
-	ApplyElemWitness(s.Ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
-	ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID})
-	assert dp.Dp3s_iospec_bio3s_xover_guard(s, t, pkt_internal)
-	unfold dp.Dp3s_iospec_ordered(s, t)
-	unfold dp.Dp3s_iospec_bio3s_xover(s, t)
-	io.TriggerBodyIoXover(pkt_internal)
-	tN := io.Dp3s_iospec_bio3s_xover_T(t, pkt_internal)
-	io.Xover(t, pkt_internal) //Event
-	UpdateElemWitness(s.Obuf, ioSharedArg.OBufY, egressID, newPkt)
-	ghost *ioSharedArg.State = io.Dp3s_add_obuf(s, egressID, newPkt)
-	ghost *ioSharedArg.Place = tN
-	fold SharedInv{dp, ioSharedArg}()
-	ghost ioLock.Unlock()
-}
+decreases
+func AtomicXover(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressID option[io.Ifs], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+	critical SharedInv{dp, ioSharedArg} (
+		unfold SharedInv{dp, ioSharedArg}()
+		t, s := *ioSharedArg.Place, *ioSharedArg.State
+		ApplyElemWitness(s.Ibuf, ioSharedArg.IBufY, ingressID, oldPkt)
+		ghost pkt_internal := io.Val(io.ValInternal1{oldPkt, get(ingressID), newPkt, egressID})
+		assert dp.Dp3s_iospec_bio3s_xover_guard(s, t, pkt_internal)
+		unfold dp.Dp3s_iospec_ordered(s, t)
+		unfold dp.Dp3s_iospec_bio3s_xover(s, t)
+		io.TriggerBodyIoXover(pkt_internal)
+		ghost tN := io.Dp3s_iospec_bio3s_xover_T(t, pkt_internal)
+		io.Xover(t, pkt_internal) //Event
+		UpdateElemWitness(s.Obuf, ioSharedArg.OBufY, egressID, newPkt)
+		ghost *ioSharedArg.State = io.Dp3s_add_obuf(s, egressID, newPkt)
+		ghost *ioSharedArg.Place = tN
+		fold SharedInv{dp, ioSharedArg}()
+	)
+}