Adapt to new version of z3 (4.16) and Viper (2026.09) (#438)

Author: jcp19

gobra-mod.json

@@ -1,6 +1,7 @@
 {
   "default_job_cfg": {
     "module": "github.com/scionproto/scion",
+    "assert_timeout": 45000,
     "includes": ["", "verification/dependencies"],
     "only_files_with_header": true,
     "assume_injectivity_inhale": true,

pkg/slayers/path/scion/raw_spec.gobra

@@ -451,6 +451,11 @@ func ValidPktMetaHdrSublice(raw []byte, idx int) {
 	unfold acc(sl.Bytes(raw[:idx], 0, idx), R56)
 	assert forall i int :: { &raw[:MetaLen][i] } 0 <= i && i < MetaLen ==>
 		&raw[:MetaLen][i] == &raw[:idx][:MetaLen][i]
+	// Sharing the locations is not enough: the two calls of RawBytesToMetaHdr
+	// read the meta header through different sl.Bytes predicates, so their
+	// snapshots must be related on those bytes as well.
+	assert forall i int :: { &raw[:MetaLen][i] } 0 <= i && i < MetaLen ==>
+		raw[:MetaLen][i] == raw[:idx][:MetaLen][i]
 	fold acc(sl.Bytes(raw, 0, len(raw)), R56)
 	fold acc(sl.Bytes(raw[:idx], 0, idx), R56)
 }

pkg/slayers/scion_spec.gobra

@@ -394,10 +394,10 @@ ensures  acc(sl.Bytes(ub, 0, length), R55)
 ensures  s.ValidHeaderOffset(ub, len(ub))
 decreases
 func (s *SCION) ValidHeaderOffsetFromSubSliceLemma(ub []byte, length int) {
-	reveal s.ValidHeaderOffset(ub, len(ub))
+	reveal s.ValidHeaderOffset(ub, length)
 	unfold acc(sl.Bytes(ub, 0, len(ub)), R56)
 	unfold acc(sl.Bytes(ub, 0, length), R56)
-	assert reveal s.ValidHeaderOffset(ub, length)
+	assert reveal s.ValidHeaderOffset(ub, len(ub))
 	fold acc(sl.Bytes(ub, 0, len(ub)), R56)
 	fold acc(sl.Bytes(ub, 0, length), R56)
 }
@@ -532,6 +532,12 @@ decreases
 func IsSupportedPktSubslice(raw []byte, idx int) {
 	unfold acc(sl.Bytes(raw, 0, len(raw)), R56)
 	unfold acc(sl.Bytes(raw[:idx], 0, idx), R56)
+	// The two calls of IsSupportedPkt read the next header and the path type
+	// through different sl.Bytes predicates. Reading both locations through
+	// both slices while the predicates are unfolded is what makes their
+	// snapshots agree on them.
+	assert raw[:idx][4] == raw[4]
+	assert raw[:idx][8] == raw[8]
 	reveal IsSupportedPkt(raw)
 	reveal IsSupportedPkt(raw[:idx])
 	fold acc(sl.Bytes(raw, 0, len(raw)), R56)
@@ -547,6 +553,9 @@ decreases
 func GetPathTypeSubslice(raw []byte, idx int) {
 	unfold acc(sl.Bytes(raw, 0, len(raw)), R56)
 	unfold acc(sl.Bytes(raw[:idx], 0, idx), R56)
+	// Relates the two sl.Bytes snapshots on the byte holding the path type,
+	// which is the only one the two calls of GetPathType read.
+	assert raw[:idx][8] == raw[8]
 	fold acc(sl.Bytes(raw, 0, len(raw)), R56)
 	fold acc(sl.Bytes(raw[:idx], 0, idx), R56)
 }

router/dataplane.go

@@ -1376,6 +1376,11 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 // @ ensures   d.DpAgreesWithSpec(dp)
 // @ ensures   d.getValForwardingMetrics() != nil
 // @ decreases
+// The postcondition of this method cannot be exhaled under the package-wide
+// more complete exhale: Silicon summarises the whole heap once per lookup and
+// per consumed conjunct, and the prover grows until it is killed. On demand is
+// enough here, so it is requested for this member alone.
+// @ #backend[exhaleMode(2)]
 func (d *DataPlane) initMetrics( /*@ ghost dp io.DataPlaneSpec @*/ ) {
 	// @ assert reveal d.PreWellConfigured()
 	// @ reveal d.getDomExternal()