New assertion in Run() to resolve verification error (#388)

* assertion in run * Update router/dataplane.go --------- Co-authored-by: João Pereira <[email protected]>
viperproject · Dec 19, 2024 · 0fc3d49 · 0fc3d49
1 parent 2aebfb2
commit 0fc3d49
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/router/dataplane.go b/router/dataplane.go
@@ -1032,6 +1032,11 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 					// @ assert sl.Bytes(tmpBuf, 0, p.N)
 					// @ assert sl.Bytes(tmpBuf, 0, len(tmpBuf))
 					result, err /*@ , addrAliasesPkt, newAbsPkt @*/ := processor.processPkt(tmpBuf, srcAddr /*@, ioLock, ioSharedArg, dp @*/)
+					// (VerifiedSCION) This assertion is crucial to keep verification stable. Without it,
+					// the fold operation in the branch protected by the condition `result.OutConn == nil`
+					// may fail non-deterministically.
+					// @ assert forall i int :: { &msgs[i] } i0 < i && i < pkts ==>
+					// @ 	MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]
 					// @ fold scmpErr.Mem()
 
 					switch {