diff --git a/router/dataplane.go b/router/dataplane.go
index 50d39b906..41cc9db3c 100644
--- 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
index a1dad4192..66bd97734 100644
--- 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
index 2b29310c7..de46a69ac 100644
--- 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