dp.Valid() as opaque

mlimbeck · Feb 19, 2024 · 7df48b8 · 7df48b8
1 parent 9258b54
commit 7df48b8
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 1 deletion.
diff --git a/router/dataplane.go b/router/dataplane.go
@@ -1137,6 +1137,9 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 	// @ invariant d.getValForwardingMetrics() != nil
 	// @ invariant 0 in d.getDomForwardingMetrics()
 	// @ invariant d.macFactory != nil
+	// @ invariant dp.Valid()
+	// @ invariant d.dpSpecWellConfigured(dp)
+	// @ invariant acc(ioLockRun.LockP(), _) && ioLockRun.LockInv() == SharedInv!< dp, ioSharedArgRun !>;
 	// @ decreases len(externals) - len(visited)
 	for ifID, v := range externals /*@ with visited @*/ {
 		cl :=

diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra
@@ -43,6 +43,7 @@ type AsIfsPair struct {
 }
 
 ghost
+opaque
 decreases
 pure func (dp DataPlaneSpec) Valid() bool {
 	return (forall ifs IO_ifs :: {ifs in domain(dp.neighborIAs)} ifs in domain(dp.neighborIAs)  ==> 

diff --git a/verification/io/router.gobra b/verification/io/router.gobra
@@ -121,7 +121,7 @@ pure func insert(buf dict[option[IO_ifs]](set[IO_pkt3]), k option[IO_ifs], v IO_
 
 ghost
 requires len(m.CurrSeg.Future) > 0
-requires dp.Valid()
+requires reveal dp.Valid()
 decreases
 pure func (dp DataPlaneSpec) dp3s_forward_ext(m IO_pkt3, newpkt IO_pkt3, nextif IO_ifs) bool {
 	return let currseg := m.CurrSeg in