Merge branch 'master' into drop_fractions_functions

viperproject · Dec 19, 2024 · 6a1b5b1 · 6a1b5b1
2 parents 400ceb7 + 0fc3d49
commit 6a1b5b1
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 {