diff --git a/router/dataplane.go b/router/dataplane.go
index f786b4213..46b34d21a 100644
--- a/router/dataplane.go
+++ b/router/dataplane.go
@@ -1029,13 +1029,16 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 				// @ 	msgs[i].GetN() <= len(msgs[i].GetFstBuffer())
 				// @ assert forall i int :: { &msgs[i] } 0 <= i && i < pkts ==>
 				// @ 	MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]
+				// @ fold MsgsMem(msgs, 0, pkts, ingressID, ioValSeq)
 
 				// (VerifiedSCION) using regular for loop instead of range loop to avoid unnecessary
 				// complications with permissions
 				// @ invariant acc(&scmpErr)
-				// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==> msgs[i].Mem()
-				// @ invariant forall j int :: { &msgs[j] } 0 <= j && j < len(msgs) ==>
-				// @ 	sl.Bytes(msgs[j].GetFstBuffer(), 0, len(msgs[j].GetFstBuffer()))
+				// (VerifiedSCION) the six quantified invariants that described the batch
+				// - two permissions and the four pure facts only they can frame - are
+				// bundled into this predicate, so that the exhale at the end of the body
+				// hands over one chunk. 'TakeMsg' and 'PutMsg' open and close it.
+				// @ invariant MsgsMem(msgs, i0, pkts, ingressID, ioValSeq)
 				// @ invariant writeMsgInv(writeMsgs)
 				// @ invariant acc(dPtr, _) && *dPtr === d
 				// @ invariant acc(d.Mem(), _) && d.WellConfigured()
@@ -1046,12 +1049,6 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 				// @ invariant acc(rd.Mem(), _)
 				// @ invariant pkts <= len(msgs)
 				// @ invariant 0 <= i0 && i0 <= pkts
-				// @ invariant forall i int :: { &msgs[i] } i0 <= i && i < len(msgs) ==>
-				// @ 	msgs[i].HasActiveAddr()
-				// @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==>
-				// @ 	typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr]
-				// @ invariant forall i int :: { &msgs[i] } 0 <= i && i < pkts ==>
-				// @ 	msgs[i].GetN() <= len(msgs[i].GetFstBuffer())
 				// @ invariant processor.sInit() && processor.sInitD() === d
 				// @ invariant let ubuf := processor.sInitBufferUBuf() in
 				// @	acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm)
@@ -1062,12 +1059,14 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 				// @ invariant ioIngressID == path.IfsToIO_ifs(ingressID)
 				// @ invariant acc(ioLock.LockP(), _)
 				// @ invariant ioLock.LockInv() == SharedInv{dp, ioSharedArg}
-				// @ invariant forall i int :: { &msgs[i] } i0 <= i && i < pkts ==>
-				// @ 	MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]
 				// @ invariant MultiElemWitnessWithIndex(ioSharedArg.IBufY, ioIngressID, ioValSeq, i0)
 				// @ decreases pkts - i0
 				for i0 := 0; i0 < pkts; i0++ {
 					// @ assert &msgs[:pkts][i0] == &msgs[i0]
+					// (VerifiedSCION) take this message out of the batch. Doing it with a
+					// lemma rather than an 'unfold' keeps the quantified reasoning over the
+					// batch out of this body, which is the whole point of the predicate.
+					// @ ghost excl := TakeMsg(msgs, i0, pkts, ingressID, ioValSeq)
 					// @ preserves 0 <= i0 && i0 < pkts && pkts <= len(msgs)
 					// @ preserves acc(msgs[i0].Mem(), R1)
 					// @ ensures   p === msgs[:pkts][i0].GetMessage()
@@ -1113,11 +1112,6 @@ 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 {
@@ -1149,6 +1143,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 						// @ assert 0 <= m.N
 						// @ msgs[:pkts][i0].IsActive = false
 						// @ fold msgs[:pkts][i0].Mem()
+						// @ PutMsg(msgs, i0, pkts, ingressID, ioValSeq, excl)
 						log.Debug("Error processing packet", "err", err)
 						// @ assert acc(inputCounters.DroppedPacketsTotal.Mem(), _)
 						// @ prometheus.CounterMemImpliesNonNil(inputCounters.DroppedPacketsTotal)
@@ -1164,6 +1159,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 						// @ sl.CombineRange_Bytes(p.Buffers[0], 0, p.N, writePerm)
 						// @ msgs[:pkts][i0].IsActive = false
 						// @ fold msgs[:pkts][i0].Mem()
+						// @ PutMsg(msgs, i0, pkts, ingressID, ioValSeq, excl)
 						continue
 					}
 
@@ -1215,6 +1211,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 					// @ sl.CombineRange_Bytes(p.Buffers[0], 0, p.N, writePerm)
 					// @ msgs[:pkts][i0].IsActive = false
 					// @ fold msgs[:pkts][i0].Mem()
+					// @ PutMsg(msgs, i0, pkts, ingressID, ioValSeq, excl)
 					// @ fold writeMsgInv(writeMsgs)
 					if err != nil {
 						// @ requires err != nil && err.ErrorMem()
@@ -1254,6 +1251,9 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 					outputCounters.OutputBytesTotal.Add(float64(len(result.OutPkt)))
 					// @ )
 				}
+				// (VerifiedSCION) the batch goes back to the outer loop, and to the next
+				// ReadBatch, as the two quantified permissions they are stated with.
+				// @ unfold MsgsMem(msgs, pkts, pkts, ingressID, ioValSeq)
 			}
 		}
 	// @ unfold acc(d.Mem(), R1)
@@ -1744,7 +1744,13 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte,
 		// @ assert reveal p.scionLayer.EqPathType(p.rawPkt)
 		// @ assert path.Type(slayers.GetPathType(p.rawPkt)) != epic.PathType
 		// @ assert AbsIO_val(p.rawPkt, p.ingressID) == oldAbsVal
-		v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ )
+		// (VerifiedSCION) pack the last layer away for the whole of 'process':
+		// it is folded here, where it was just decoded and the facts about it are
+		// still immediate, rather than inside 'process', where re-deriving them
+		// from the ghost parameters costs far more than it saves.
+		// @ fold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd)
+		v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub, llStart, llEnd, ioLock, ioSharedArg, dp @*/ )
+		// @ unfold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd)
 		// @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer)
 		// @ fold p.sInit()
 		return v1, v2 /*@, addrAliasesPkt, newAbsPkt @*/
@@ -1764,7 +1770,13 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte,
 		// @ assert unfolding acc(p.scionLayer.Mem(p.rawPkt), R56) in slayers.CmnHdrLen <= len(p.rawPkt)
 		// @ assert typeOf(p.scionLayer.GetPath(p.rawPkt)) == *epic.Path ==>
 		// @ 	p.scionLayer.EqAbsHeader(p.rawPkt) && p.scionLayer.ValidScionInitSpec(p.rawPkt)
-		v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processEPIC( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ )
+		// (VerifiedSCION) pack the last layer away for the whole of 'process':
+		// it is folded here, where it was just decoded and the facts about it are
+		// still immediate, rather than inside 'process', where re-deriving them
+		// from the ghost parameters costs far more than it saves.
+		// @ fold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd)
+		v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processEPIC( /*@ p.rawPkt, ub, llStart, llEnd, ioLock, ioSharedArg, dp @*/ )
+		// @ unfold p.LastLayerMem(p.rawPkt, ub, llStart, llEnd)
 		// @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer)
 		// @ fold p.sInit()
 		return v1, v2 /*@, addrAliasesPkt, newAbsPkt @*/
@@ -1900,14 +1912,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) {
 // @ requires  sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
 // @ requires  acc(&p.ingressID, R10)
 // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _)
-// @ preserves acc(&p.lastLayer, R10)
-// @ preserves p.lastLayer != nil
-// @ preserves (p.lastLayer !== &p.scionLayer && llIsNil) ==>
-// @ 	acc(p.lastLayer.Mem(nil), R10)
-// @ preserves (p.lastLayer !== &p.scionLayer && !llIsNil) ==>
-// @ 	acc(p.lastLayer.Mem(ub[startLL:endLL]), R10)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	!llIsNil && startLL == 0 && endLL == len(ub)
+// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL)
 // @ preserves acc(&p.infoField)
 // @ preserves acc(&p.hopField)
 // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem()
@@ -1962,7 +1967,7 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) {
 // @ 		path.IfsToIO_ifs(p.ingressID),
 // @ 		newAbsPkt.ValPkt_1)
 // @ decreases 0 if sync.IgnoreBlockingForTermination()
-func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) {
+func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) {
 
 	var ok bool
 	// @ unfold acc(p.scionLayer.Mem(ub), R20)
@@ -1976,7 +1981,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil
 		return processResult{}, malformedPath /*@ , false, io.ValUnit{} @*/
 	}
 	// @ assert p.path === p.scionLayer.GetScionPath(ub)
-	return p.process( /*@ ub, llIsNil, startLL, endLL , ioLock, ioSharedArg, dp @*/ )
+	return p.process( /*@ ub, ubLL, startLL, endLL , ioLock, ioSharedArg, dp @*/ )
 }
 
 // @ requires  0 <= startLL && startLL <= endLL && endLL <= len(ub)
@@ -1993,14 +1998,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil
 // @ requires  sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
 // @ requires  acc(&p.ingressID, R10)
 // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _)
-// @ preserves acc(&p.lastLayer, R10)
-// @ preserves p.lastLayer != nil
-// @ preserves (p.lastLayer !== &p.scionLayer && llIsNil) ==>
-// @ 	acc(p.lastLayer.Mem(nil), R10)
-// @ preserves (p.lastLayer !== &p.scionLayer && !llIsNil) ==>
-// @ 	acc(p.lastLayer.Mem(ub[startLL:endLL]), R10)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	!llIsNil && startLL == 0 && endLL == len(ub)
+// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL)
 // @ preserves acc(&p.infoField)
 // @ preserves acc(&p.hopField)
 // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem()
@@ -2057,7 +2055,7 @@ func (p *scionPacketProcessor) processSCION( /*@ ghost ub []byte, ghost llIsNil
 // @ 		path.IfsToIO_ifs(p.ingressID),
 // @ 		newAbsPkt.ValPkt_1)
 // @ decreases 0 if sync.IgnoreBlockingForTermination()
-func (p *scionPacketProcessor) processEPIC( /*@ ghost ub []byte, ghost llIsNil bool, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) {
+func (p *scionPacketProcessor) processEPIC( /*@ ghost ub []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int, ghost ioLock gpointer[gsync.GhostMutex], ghost ioSharedArg SharedArg, ghost dp io.DataPlaneSpec @*/ ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) {
 	// @ unfold acc(p.scionLayer.Mem(ub), R10)
 	epicPath, ok := p.scionLayer.Path.(*epic.Path)
 	if !ok {
@@ -2093,7 +2091,7 @@ func (p *scionPacketProcessor) processEPIC( /*@ ghost ub []byte, ghost llIsNil b
 	// @ assert p.path === p.scionLayer.GetScionPath(ub)
 	// @ assert p.scionLayer.UBPath(ub) === ubPath
 
-	result, err /*@ , addrAliases, newAbsPkt0 @*/ := p.process( /*@ ub, llIsNil, startLL, endLL, ioLock, ioSharedArg, dp @*/ )
+	result, err /*@ , addrAliases, newAbsPkt0 @*/ := p.process( /*@ ub, ubLL, startLL, endLL, ioLock, ioSharedArg, dp @*/ )
 	if err != nil {
 		return result, err /*@ , addrAliases, newAbsPkt0 @*/
 	}
@@ -2225,12 +2223,7 @@ type macBuffersT struct {
 // @ requires  acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem()
 // @ requires  sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
 // @ requires  cause != nil ==> cause.ErrorMem()
-// @ preserves ubLL == nil || ubLL === ub[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ub === ubLL
+// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL)
 // @ ensures   acc(&p.d, R50) && acc(p.d.Mem(), _)
 // @ ensures   acc(p.scionLayer.Mem(ub), R4)
 // @ ensures   sl.Bytes(ub, 0, len(ub))
@@ -2254,6 +2247,10 @@ func (p *scionPacketProcessor) packSCMP(
 	// @ ghost startLL int,
 	// @ ghost endLL int,
 ) (respr processResult, reserr error) {
+	// (VerifiedSCION) this member reads the last layer, so it opens the
+	// predicate that carries it; the checks that only hand it on do not.
+	// @ unfold p.LastLayerMem(ub, ubLL, startLL, endLL)
+	// @ defer fold p.LastLayerMem(ub, ubLL, startLL, endLL)
 	// @ ghost llIsScmp := false
 	// @ ghost scmpPldIsNil := false
 	// @ ghost maybeStartPld := 0
@@ -2429,12 +2426,7 @@ func (p *scionPacketProcessor) parsePath( /*@ ghost ub []byte @*/ ) (respr proce
 // pres for IO:
 // @ requires  slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL)
 // @ requires  AbsPkt(ubScionL).PathNotFullyTraversed()
-// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ubScionL === ubLL
+// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 // @ preserves acc(&p.infoField, R20)
 // @ preserves acc(&p.hopField, R20)
 // @ preserves acc(&p.ingressID, R20)
@@ -2518,12 +2510,7 @@ func (p *scionPacketProcessor) validateHopExpiry( /*@ ghost ubScionL []byte, gho
 // @ requires  acc(&p.hopField, R20)
 // @ requires  acc(&p.infoField, R20)
 // @ requires  acc(&p.d, R50) && acc(p.d.Mem(), _)
-// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL]
-// @ preserves  acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves  &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves  &p.scionLayer === p.lastLayer ==>
-// @ 	ubScionL === ubLL
+// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 // @ ensures   acc(&p.d, R50)
 // @ ensures   acc(&p.path, R20)
 // @ ensures   acc(&p.infoField, R20)
@@ -2595,12 +2582,7 @@ func (p *scionPacketProcessor) validateIngressID( /*@ ghost ubScionL []byte, gho
 // @ requires  sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
 // @ requires  acc(&p.d, R50) && acc(p.d.Mem(), _)
 // @ preserves acc(&p.ingressID, R21)
-// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ubScionL === ubLL
+// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 // @ ensures   acc(p.scionLayer.Mem(ubScionL), R2)
 // @ ensures   acc(&p.path, R20)
 // @ ensures   acc(&p.d, R50) && acc(p.d.Mem(), _)
@@ -2708,12 +2690,7 @@ func (p *scionPacketProcessor) validateSrcDstIA( /*@ ghost ubScionL []byte, ghos
 // @ requires  sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
 // @ requires  acc(&p.d, R50) && acc(p.d.Mem(), _)
 // @ preserves acc(&p.ingressID, R40)
-// @ preserves ubLL == nil || ubLL === ub[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ub === ubLL
+// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL)
 // @ ensures   acc(&p.d, R50) && acc(p.d.Mem(), _)
 // @ ensures   acc(&p.path, R20)
 // @ ensures   acc(p.scionLayer.Mem(ub), R3)
@@ -2758,12 +2735,7 @@ func (p *scionPacketProcessor) invalidSrcIA(
 // @ requires  sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
 // @ requires  acc(&p.d, R50) && acc(p.d.Mem(), _)
 // @ preserves acc(&p.ingressID, R40)
-// @ preserves ubLL == nil || ubLL === ub[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ub === ubLL
+// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL)
 // @ ensures   acc(&p.d, R50) && acc(p.d.Mem(), _)
 // @ ensures   acc(&p.path, R20)
 // @ ensures   acc(p.scionLayer.Mem(ub), R3)
@@ -2893,12 +2865,7 @@ func (p *scionPacketProcessor) validateTransitUnderlaySrc( /*@ ghost ub []byte @
 // @ requires  acc(&p.ingressID, R21)
 // @ requires  acc(&p.infoField, R20)
 // @ requires  acc(&p.hopField, R20)
-// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ubScionL === ubLL
+// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 // @ ensures   acc(&p.infoField, R20)
 // @ ensures   acc(&p.hopField, R20)
 // @ ensures   acc(&p.ingressID, R21)
@@ -3218,12 +3185,7 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/
 // @ preserves acc(&p.macBuffers.scionInput, R20)
 // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 // @ preserves acc(&p.cachedMac)
-// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ubScionL === ubLL
+// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 // @ ensures   acc(&p.path, R20)
 // @ ensures   acc(&p.infoField, R20)
 // @ ensures   acc(&p.hopField,  R20)
@@ -3323,12 +3285,7 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec,
 // @ requires  slayers.ValidPktMetaHdr(ubScionL) && p.scionLayer.EqAbsHeader(ubScionL)
 // @ requires  AbsPkt(ubScionL).PathNotFullyTraversed()
 // @ preserves acc(&p.ingressID, R40)
-// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ubScionL === ubLL
+// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 // @ ensures   acc(&p.d, R15) && acc(p.d.Mem(), _)
 // @ requires  p.d.getValSvc() != nil
 // @ ensures   p.d.validResult(respr, addrAliasesUb)
@@ -3749,12 +3706,7 @@ func (p *scionPacketProcessor) egressInterface( /*@ ghost oldPkt io.Pkt @*/ ) (e
 // @ requires  AbsPkt(ub).PathNotFullyTraversed()
 // @ requires  p.EqAbsInfoField(AbsPkt(ub))
 // @ requires  p.EqAbsHopField(AbsPkt(ub))
-// @ preserves ubLL == nil || ubLL === ub[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ub === ubLL
+// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL)
 // @ ensures   acc(&p.infoField, R20)
 // @ ensures   acc(&p.hopField, R20)
 // @ ensures   acc(&p.ingressID, R21)
@@ -3833,12 +3785,7 @@ func (p *scionPacketProcessor) validateEgressUp(
 // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 // @ preserves acc(&p.cachedMac)
 // @ ensures   p.cachedMac === old(p.cachedMac)
-// @ preserves ubLL == nil || ubLL === ub[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ub === ubLL
+// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL)
 // @ ensures   acc(&p.ingressID, R21)
 // @ ensures   acc(&p.path, R20)
 // @ ensures   acc(&p.infoField, R20)
@@ -3969,12 +3916,7 @@ func (p *scionPacketProcessor) ingressRouterAlertFlag() (res *bool) {
 // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 // @ preserves acc(&p.cachedMac)
 // @ ensures   p.cachedMac === old(p.cachedMac)
-// @ preserves ubLL == nil || ubLL === ub[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ub === ubLL
+// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL)
 // @ ensures   acc(&p.ingressID, R21)
 // @ ensures   acc(&p.path, R20)
 // @ ensures   acc(&p.infoField, R20)
@@ -4106,12 +4048,7 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) {
 // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 // @ preserves acc(&p.cachedMac)
 // @ ensures   p.cachedMac === old(p.cachedMac)
-// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ubScionL === ubLL
+// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 // @ ensures   acc(&p.path, R20)
 // @ ensures   acc(&p.infoField, R20)
 // @ ensures   acc(&p.hopField,  R20)
@@ -4141,16 +4078,23 @@ func (p *scionPacketProcessor) egressRouterAlertFlag() (res *bool) {
 // @ decreases
 func (p *scionPacketProcessor) handleSCMPTraceRouteRequest(
 	interfaceID uint16 /*@, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/) (respr processResult, reserr error) {
+	// (VerifiedSCION) this member reads the last layer, so it opens the
+	// predicate that carries it; the checks that only hand it on do not. It is
+	// closed again as soon as the two reads below are done - the pure facts it
+	// carries stay known, and 'packSCMP' wants it folded.
+	// @ unfold p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 	// @ ghost llIsScmp := false
 	// @ ghost scionPldIsNil := false
 	// @ ghost maybeStartPld := 0
 	// @ ghost maybeEndPld := 0
 	if p.lastLayer.NextLayerType( /*@ ubLL @*/ ) != slayers.LayerTypeSCMP {
 		log.Debug("Packet with router alert, but not SCMP")
+		// @ fold p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 		// @ fold p.d.validResult(processResult{}, false)
 		return processResult{}, nil
 	}
 	scionPld /*@ , start, end @*/ := p.lastLayer.LayerPayload( /*@ ubLL @*/ )
+	// @ fold p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 	// @ sl.SplitRange_Bytes(ubScionL, startLL, endLL, R1)
 	// @ maybeStartPld = start
 	// @ maybeEndPld = end
@@ -4222,12 +4166,7 @@ func (p *scionPacketProcessor) handleSCMPTraceRouteRequest(
 // @ requires  sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
 // @ requires  acc(&p.d, R50) && acc(p.d.Mem(), _)
 // @ preserves acc(&p.ingressID, R20)
-// @ preserves ubLL == nil || ubLL === ubScionL[startLL:endLL]
-// @ preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
-// @ preserves &p.scionLayer !== p.lastLayer ==>
-// @ 	acc(p.lastLayer.Mem(ubLL), R15)
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	ubScionL === ubLL
+// @ preserves p.LastLayerMem(ubScionL, ubLL, startLL, endLL)
 // @ ensures   acc(&p.d, R50) && acc(p.d.Mem(), _)
 // @ ensures   acc(&p.path, R20)
 // @ ensures   acc(p.scionLayer.Mem(ubScionL), R3)
@@ -4287,13 +4226,7 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost
 // @ requires  acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem()
 // @ requires  sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
 // @ preserves acc(&p.srcAddr, R10) && acc(p.srcAddr.Mem(), _)
-// @ preserves acc(&p.lastLayer, R10)
-// @ preserves p.lastLayer != nil
-// @ preserves p.lastLayer !== &p.scionLayer ==>
-// @ 	(llIsNil ==> acc(p.lastLayer.Mem(nil), R10)) &&
-// @ 	(!llIsNil ==> acc(p.lastLayer.Mem(ub[startLL:endLL]), R10))
-// @ preserves &p.scionLayer === p.lastLayer ==>
-// @ 	!llIsNil && startLL == 0 && endLL == len(ub)
+// @ preserves p.LastLayerMem(ub, ubLL, startLL, endLL)
 // @ preserves acc(&p.infoField)
 // @ preserves acc(&p.hopField)
 // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem()
@@ -4354,14 +4287,13 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost
 // @ #backend[stateConsolidationMode(6)]
 func (p *scionPacketProcessor) process(
 // @ 	ghost ub []byte,
-// @ 	ghost llIsNil bool,
+// @ 	ghost ubLL []byte,
 // @ 	ghost startLL int,
 // @ 	ghost endLL int,
 // @ 	ghost ioLock gpointer[gsync.GhostMutex],
 // @ 	ghost ioSharedArg SharedArg,
 // @ 	ghost dp io.DataPlaneSpec,
 ) (respr processResult, reserr error /*@, ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) {
-	// @ ghost ubLL := llIsNil ? ([]byte)(nil) : ub[startLL:endLL]
 	// @ assert p.path === p.scionLayer.GetScionPath(ub)
 	if r, err := p.parsePath( /*@ ub @*/ ); err != nil {
 		// @ p.scionLayer.DowngradePerm(ub)
diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra
index 0623531b0..37d34f2a4 100644
--- a/router/dataplane_spec.gobra
+++ b/router/dataplane_spec.gobra
@@ -203,6 +203,28 @@ func liftForwardingMetricsNonInjectiveMem(v forwardingMetrics, id uint16) {
 	fold acc(forwardingMetricsMem(v, id), _)
 }
 
+// (VerifiedSCION) The last layer that was decoded out of the packet, which is
+// what 'packSCMP' reads when a check answers with an SCMP message. Every check
+// that 'process' performs has to carry it, even though almost none of them look
+// at it: they only hand it on to 'packSCMP'.
+//
+// Spelled out, this is four clauses - two of them impure implications, which
+// Silicon branches on and re-joins at every exhale and every inhale - repeated
+// in the contract of fourteen members and exchanged twice at each of the
+// seventeen calls along 'process's path. As a predicate it is a single chunk,
+// and only the two members that read it - 'packSCMP' and
+// 'handleSCMPTraceRouteRequest' - ever unfold it.
+//
+// 'ubLL' is the last layer's buffer, 'nil' when there is none; it is a slice of
+// 'ub' and coincides with it when the last layer is the SCION layer itself.
+pred (p *scionPacketProcessor) LastLayerMem(ub []byte, ubLL []byte, startLL int, endLL int) {
+	0 <= startLL && startLL <= endLL && endLL <= len(ub)                &&
+	acc(&p.lastLayer, R10) && p.lastLayer != nil                        &&
+	(ubLL == nil || ubLL === ub[startLL:endLL])                         &&
+	(&p.scionLayer !== p.lastLayer ==> acc(p.lastLayer.Mem(ubLL), R10)) &&
+	(&p.scionLayer === p.lastLayer ==> ub === ubLL)
+}
+
 pred (p *scionPacketProcessor) initMem() {
 	acc(&p.d)                                    &&
 	acc(&p.ingressID)                            &&
diff --git a/router/msgs-spec.gobra b/router/msgs-spec.gobra
new file mode 100644
index 000000000..532637665
--- /dev/null
+++ b/router/msgs-spec.gobra
@@ -0,0 +1,134 @@
+// Copyright 2025 ETH Zurich
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//   http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// +gobra
+
+package router
+
+import (
+	"net"
+
+	"golang.org/x/net/ipv4"
+
+	"verification/io"
+	sl "verification/utils/slices"
+	. "verification/utils/definitions"
+)
+
+// (VerifiedSCION) The per-message resources of one read batch, as the loop that
+// processes the batch carries them.
+//
+// Measuring the packet loop says that half of its cost is a single step:
+// exhaling the twenty-five invariants of the inner loop on the fall-through
+// path at the end of its body, over everything that body has accumulated by
+// then. Six of those invariants are quantified over the whole 64-message batch,
+// and they are what make that exhale expensive: two carry permission, and the
+// other four are pure facts that only the first two can frame, so they have to
+// travel together. Bundled here, the exhale hands over one chunk.
+//
+// 'i0' is the index the loop is about to process. Messages before it have been
+// consumed - their address is no longer guaranteed live, and their abstraction
+// no longer has to agree with the IO specification - while messages from 'i0'
+// on are still exactly as 'ReadBatch' left them.
+pred MsgsMem(msgs []ipv4.Message, i0 int, pkts int, ingressID uint16, ioValSeq seq[io.Val]) {
+	0 <= i0 && i0 <= pkts && pkts <= len(msgs) && pkts <= len(ioValSeq) &&
+	(forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
+		msgs[i].Mem()) &&
+	(forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
+		sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer()))) &&
+	(forall i int :: { &msgs[i] } i0 <= i && i < len(msgs) ==>
+		msgs[i].HasActiveAddr()) &&
+	(forall i int :: { &msgs[i] } i0 <= i && i < pkts ==>
+		typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr]) &&
+	(forall i int :: { &msgs[i] } 0 <= i && i < pkts ==>
+		msgs[i].GetN() <= len(msgs[i].GetFstBuffer())) &&
+	(forall i int :: { &msgs[i] } i0 <= i && i < pkts ==>
+		MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i])
+}
+
+// The same, with message 'i0' taken out. This is what the body of the loop
+// holds on to while it works on that one message.
+//
+// 'excl' is that message's buffer, and the last conjunct is the only reason the
+// predicate needs it. Both quantified permissions above are keyed on
+// 'msgs[i].GetFstBuffer()', so folding either one obliges Silicon to show that
+// no two messages share a buffer. Inside the batch that fact comes for free -
+// '--assumeInjectivityOnInhale' asserts it every time the quantified permission
+// is inhaled - but the message that has been taken out is no longer part of any
+// such inhale, so putting it back would leave its buffer unrelated to the rest.
+// Naming the buffer here carries the one missing inequality across the hole.
+pred MsgsMemHole(msgs []ipv4.Message, i0 int, pkts int, ingressID uint16, ioValSeq seq[io.Val], excl []byte) {
+	0 <= i0 && i0 < pkts && pkts <= len(msgs) && pkts <= len(ioValSeq) &&
+	(forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) && i != i0 ==>
+		msgs[i].Mem()) &&
+	(forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) && i != i0 ==>
+		sl.Bytes(msgs[i].GetFstBuffer(), 0, len(msgs[i].GetFstBuffer()))) &&
+	(forall i int :: { &msgs[i] } i0 <= i && i < len(msgs) && i != i0 ==>
+		msgs[i].HasActiveAddr()) &&
+	(forall i int :: { &msgs[i] } i0 <= i && i < pkts && i != i0 ==>
+		typeOf(msgs[i].GetAddr()) == type[*net.UDPAddr]) &&
+	(forall i int :: { &msgs[i] } 0 <= i && i < pkts && i != i0 ==>
+		msgs[i].GetN() <= len(msgs[i].GetFstBuffer())) &&
+	(forall i int :: { &msgs[i] } i0 <= i && i < pkts && i != i0 ==>
+		MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]) &&
+	(forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) && i != i0 ==>
+		msgs[i].GetFstBuffer() !== excl)
+}
+
+// Take message 'i0' out of the batch.
+//
+// The point of doing this in a lemma rather than with an 'unfold' in the loop
+// body is that the quantified reasoning then happens here, in a member whose
+// state holds nothing but the batch, instead of in the body, where it would run
+// over the packet's split byte ranges, the write-message permissions and the
+// IO-spec place and state as well. Unfolding the predicate in the body would
+// give back exactly the six invariants this is meant to replace.
+ghost
+requires MsgsMem(msgs, i0, pkts, ingressID, ioValSeq)
+requires 0 <= i0 && i0 < pkts && pkts <= len(msgs) && pkts <= len(ioValSeq)
+ensures  MsgsMemHole(msgs, i0, pkts, ingressID, ioValSeq, excl)
+ensures  msgs[i0].Mem()
+ensures  sl.Bytes(msgs[i0].GetFstBuffer(), 0, len(msgs[i0].GetFstBuffer()))
+ensures  excl === msgs[i0].GetFstBuffer()
+ensures  msgs[i0].HasActiveAddr()
+ensures  typeOf(msgs[i0].GetAddr()) == type[*net.UDPAddr]
+ensures  msgs[i0].GetN() <= len(msgs[i0].GetFstBuffer())
+ensures  MsgToAbsVal(&msgs[i0], ingressID) == ioValSeq[i0]
+decreases
+func TakeMsg(msgs []ipv4.Message, i0 int, pkts int, ingressID uint16, ioValSeq seq[io.Val]) (excl []byte) {
+	unfold MsgsMem(msgs, i0, pkts, ingressID, ioValSeq)
+	excl = msgs[i0].GetFstBuffer()
+	fold MsgsMemHole(msgs, i0, pkts, ingressID, ioValSeq, excl)
+}
+
+// Put message 'i0' back and move on to the next one.
+//
+// What comes back is deliberately weaker than what 'TakeMsg' handed out: the
+// loop body consumes the message's address and forwards its bytes, so neither
+// 'HasActiveAddr' nor the agreement with 'ioValSeq' still holds for 'i0'. That
+// is exactly why the predicate is indexed by 'i0': those two facts are only
+// claimed from the current index on.
+ghost
+requires MsgsMemHole(msgs, i0, pkts, ingressID, ioValSeq, excl)
+requires 0 <= i0 && i0 < pkts && pkts <= len(msgs) && pkts <= len(ioValSeq)
+requires msgs[i0].Mem()
+requires sl.Bytes(msgs[i0].GetFstBuffer(), 0, len(msgs[i0].GetFstBuffer()))
+requires excl === msgs[i0].GetFstBuffer()
+requires msgs[i0].GetN() <= len(msgs[i0].GetFstBuffer())
+ensures  MsgsMem(msgs, i0+1, pkts, ingressID, ioValSeq)
+decreases
+func PutMsg(msgs []ipv4.Message, i0 int, pkts int, ingressID uint16, ioValSeq seq[io.Val], excl []byte) {
+	unfold MsgsMemHole(msgs, i0, pkts, ingressID, ioValSeq, excl)
+	fold MsgsMem(msgs, i0+1, pkts, ingressID, ioValSeq)
+}
diff --git a/verification/PERFORMANCE.md b/verification/PERFORMANCE.md
new file mode 100644
index 000000000..ec80290f3
--- /dev/null
+++ b/verification/PERFORMANCE.md
@@ -0,0 +1,379 @@
+# Where the router's verification time goes
+
+`router/` is by far the most expensive package to verify: the CI gives it a six
+hour budget, while every other package gets between five and thirty minutes.
+Most of that budget is consumed by a handful of members. This note records how
+the cost is distributed, what was measured, and which changes are likely to pay
+off, so that the next person to look at this does not have to rediscover it.
+
+Everything below was measured with `verification/scripts/verify-member.py`,
+which verifies **one member at a time** using Gobra's isolation
+(`-i router/dataplane.go@<line>`, after which the chopper keeps only the slice
+of the program that the member needs) and the options that the CI uses. Numbers
+are wall clock for the whole Gobra run on a 4-core machine; roughly 140 s of
+each of them is Gobra's front end, which the isolated runs cannot avoid.
+
+## Cost per member
+
+| member | isolated run | of which: the contract alone |
+|---|---|---|
+| `Run` itself, for reference | 2.8 min | — |
+| `processOHP` | 5.5 min | — |
+| `processPkt` | 5.7 min | — |
+| `doXover` | 12 min | 6 min |
+| the `rc` closure of `Run` (`closureCall$rc_Run…`) | 26 min | 2.5 min |
+| `process` | 109 min | 4 min |
+
+(`process` and `rc` are now 62 min and 6.4 min — see the two *What did work*
+sections below. The rest of the table, and the whole analysis, describes the
+state before those changes.)
+
+The "contract alone" column comes from cutting the body at its first statement
+(see below): it is what the run still costs when the member has no body left.
+Since the front end alone is ~2.5 min, `Run` and `processPkt`/`processOHP` are
+in fact only a couple of minutes of solving each; the cost is concentrated in
+`process`, in the `rc` closure and, to a lesser extent, in `doXover`. That `Run`
+itself is cheap while the closure it declares is not is expected: `Run`'s body
+is broken up by seven `outline` blocks, and the packet loop lives in `rc`.
+
+## The backend options are not the problem
+
+Every deviation from what `router/gobra.json` already asks for made things
+worse, so the slowness is not a misconfiguration:
+
+| change | effect |
+|---|---|
+| `mce_mode: "od"` instead of `"on"` (the module default) | `processOHP` still running when the baseline had finished |
+| `#backend[moreJoins()]` on `doXover`, i.e. join every branch | more than twice as slow |
+| `#backend[moreJoins()]` on `process` | ≥ 8446 s against a 7737 s baseline under the same load |
+| `#backend[exhaleModeQP(2)]` on `doXover` | no improvement |
+
+Joining is the interesting one, because the profile below says `process` explores
+its whole tail once per side of the `IsXover` branch. Joining does remove that
+duplication — and still loses, because merging two copies of a heap this
+fragmented costs more than exploring it twice.
+
+`mce_mode: "on"` in particular is not a leftover: with on-demand exhale, Silicon
+first tries a greedy exhale and only retries with the complete one when that
+fails. In this package the greedy attempt fails often enough that the retries
+cost more than always being complete. Note also that Gobra never passes
+`--exhaleModeQP`, and Silicon's default for it is the complete mode regardless
+of `--exhaleMode`, so quantified permissions are always exhaled completely.
+
+## Where the time goes inside a member
+
+The body of a member can be cut short by inserting `TODO()` (which is
+`ensures false`), making everything after the cut unreachable. Timing a sequence
+of cuts gives a profile of the member. For `doXover`:
+
+| what runs | s |
+|---|---|
+| nothing (contract only) | 351 |
+| … up to the range splits and `XoverLemma` | 417 |
+| … up to and including `IncPath` | 465 |
+| … including the block of 14 assertions | 464 |
+| … including both hop/info field decodings | 458 |
+| the whole body, without the final `return` | 566 |
+| the whole member | 707 |
+
+And for `process`:
+
+| what runs | s |
+|---|---|
+| nothing (contract only) | 237 |
+| … `parsePath` | 307 |
+| … the next four validators | 446 |
+| … `verifyCurrentMAC`, `handleIngressRouterAlert` | 487 |
+| … the whole inbound branch, `InternalEnterEvent` included | 630 |
+| … the whole xover branch, `doXover` included | 1319 |
+| the whole member | 6548 |
+
+Four fifths of `process` is therefore in its last 130 lines: `validateEgressUp`,
+`egressInterface`, the two egress branches with their IO-spec events, the three
+`reveal PktUpdate(…)`/`reveal absIO_val(…)`, and the three exits. That tail sits
+after the `if p.path.IsXover(…)` branch, which *rejoins*; since `more_joins:
+"impure"` does not join `if` statements, everything in the tail is explored once
+per side of that branch, and again per side of each `ghost if
+slayers.IsSupportedPkt(ub)` and `ghost if !p.segmentChange` inside it.
+
+Back to `doXover`: two things stand out. The block of assertions in the middle
+and the two field decodings are free — the facts they restate are already in the path condition.
+And after subtracting the front end, roughly 60 % of the remaining time is spent
+on `doXover`'s *own contract*: ~210 s proving that its 26 `ensures` clauses are
+well defined before the body starts, and at least ~140 s exhaling them at the
+single successful exit. Dropping any one clause changes little (removing the
+largest one saves 4 %); the cost is spread evenly over clauses that each mention
+`absPkt(ub)` or `old(absPkt(ub))` and therefore drag in
+`CurrSeg`/`LeftSeg`/`MidSeg`/`RightSeg` → `segment` → the recursive `hopFields`,
+all of which have to be framed against the current `sl.Bytes(ub, …)` snapshot.
+
+`process` is expensive for the opposite reason: its contract costs about 100 s
+of solver time out of 109 minutes. Its body calls seventeen methods whose
+specifications total
+**568 clauses**, each of which is exhaled and then inhaled again over a heap
+that holds `p.scionLayer.Mem(ub)`, a fragmented `sl.Bytes(ub, …)` and the
+`absPkt(ub)` function stack. Nine of those callees share eleven *literally
+identical* clauses (permission to `p.d`, `p.path`, `p.buffer`,
+`p.buffer.UBuf()`, `p.lastLayer`, and `p.d.validResult`).
+
+The `rc` closure has no postcondition at all, and cutting its body away brings
+its run down to the front end alone (152 s), so all of its time is in the two
+nested loops. Cutting inside them says exactly where:
+
+| what runs | s |
+|---|---|
+| the outer loop entered, its body skipped | 178 |
+| the outer body, up to the inner loop entered with its body skipped | 177 |
+| … the inner body up to the `processPkt` call | 229 |
+| … including the `processPkt` call | 230 |
+| … up to `WriteBatch` | 432 |
+| the whole inner body, but not the invariant exhale that follows it | 1027 |
+| the whole closure | 2186 |
+
+Three things follow, and the first two are the opposite of what one would guess.
+
+**The invariants are cheap to establish and cheap to inhale.** The outer loop's
+eighteen and the inner loop's twenty-five together cost nothing measurable: the
+run with both loops entered and both bodies skipped is still at the front-end
+floor. So is the whole read-batch block, with its prophecy variable, its
+`MultiReadBio` unfoldings and its four quantified assertions over the batch.
+
+**The call to `processPkt` is free** — 229 s before it, 230 s after it — even
+though its contract is one of the largest in the package. Inhaling a big
+postcondition into a state this small is not what costs.
+
+**One exhale accounts for half of the closure.** The difference between the last
+two rows, ~1160 s, is a single step: exhaling the inner loop's twenty-five
+invariants on the fall-through path at the end of the body. The same exhale on
+the four `continue` paths, which happen earlier and in a smaller state, is
+included in the rows above it and is far cheaper. Seven of those invariants are
+quantified over the 64-message batch — `msgs[i].Mem()`,
+`sl.Bytes(msgs[i].GetFstBuffer(), …)`, and five pure facts about `msgs[i]`
+including `MsgToAbsVal(&msgs[i], ingressID) == ioValSeq[i]`, which unfolds the
+whole packet abstraction for every message — and they have to be re-established
+over everything the body has accumulated by then: the packet's byte ranges split
+and recombined, the write-message permissions, the IO-spec place and state.
+
+## Contributing factors
+
+* **Permission fragmentation.** `p.scionLayer.Mem(..)` is used at 18 distinct
+  permission amounts in `dataplane.go`, `p.scionLayer.Path.Mem(..)` at 11,
+  `d.Mem(..)` at 8. There are 136 calls to the `sl.*_Bytes` split/combine
+  lemmas at 11 distinct amounts. Each of them folds or unfolds a predicate whose
+  body is a quantified `forall i :: acc(&s[i])`, so each creates or consumes
+  quantified-permission chunks. Under the complete exhale that this package
+  needs, every subsequent heap lookup summarises all of them.
+* **Branches are not joined.** `more_joins: "impure"` only joins impure
+  conditionals inside assertions; `if` statements are only joined under
+  `moreJoins(all)`, which `Run` and `rc` opt into and the others do not. So
+  `process`'s seventeen error exits each exhale its postcondition (25 `ensures`
+  plus 11 `preserves`, so 36 clauses once encoded) separately, and — far more
+  expensive — its whole tail is explored once per side of the `IsXover` branch
+  that precedes it. Joining is not a free win: on `doXover` it was more than
+  twice as slow.
+* **`old(...)` in leaf contracts.** The contracts of the members that `process`
+  calls contain 61 `old(...)` applications and 88 applications of `absPkt`,
+  which forces Silicon to keep querying the pre-state heap as well.
+
+## What was tried, and did not work
+
+Rewriting the specifications locally does not help either. Each of these was
+implemented, verified (0 errors) and timed:
+
+| change | result |
+|---|---|
+| delete the assertions `doXover` repeats (`p.path === …GetScionPath(ub)` 6×, `…GetBase(ubScionPath) == nextBase` 5×) | no change; the profile says they were already free |
+| replace `doXover`'s eight repeated `ghost if typeOf(…) == *epic.Path` by one local ghost boolean | 841 s against a 707 s solo baseline — worse |
+| thread the abstract packet through ghost parameters in `doXover`, removing nine `absPkt(ub)` and five `old(absPkt(ub))` from its contract | 892 s vs 915 s in a fair A/B — a wash |
+| give `XoverEvent` and `ExternalEnterOrExitEvent` the intermediate abstract packets as parameters, instead of writing `AbsUpdateNonConsDirIngressSegID(oldPkt, ingressID)` nine times and `AbsDoXover(…)` five times inside it | `process` 7537 s with the machine to itself, against a 6548 s baseline that shared it — no gain |
+
+The last two are the informative failures. Silicon evaluates a heap-dependent
+function once per heap snapshot, not once per mention, so collapsing repeated
+applications buys nothing; what the contract costs is the *number of distinct
+states* in which its clauses have to be framed, and the `unfolding`-heavy
+accessors (`UBPath`, `UBScionPath`, `GetPath`, `GetScionPath`,
+`ValidPathMetaData`, `EqAbsHeader`, …) that each open `p.scionLayer.Mem(ub)`
+again.
+
+Taken together with the backend options above: six interventions, none of which
+moved the number. The cost is spread thinly over a very large number of
+individually expensive queries, and it is the *size and fragmentation of the
+symbolic state* that makes each of them expensive. Anything that leaves the
+state alone — reordering clauses, naming subterms, deleting assertions, changing
+how branches are explored — leaves the cost alone too. The next section is what
+happens when the state itself gets smaller.
+
+A corollary worth keeping in mind before the next attempt: measure in pairs.
+Several of the differences above are smaller than the effect of sharing the
+machine with a second Gobra run (a second run inflates a `process` measurement
+from 6548 s to 7737 s), so a variant timed on its own against a baseline timed
+under load will look like a win that is not there.
+
+## What did work: `LastLayerMem`
+
+Shrinking the state does move the number. `process` went from **7854 s to
+3729 s — 2.1× — in a paired A/B**, both arms reporting 0 errors.
+
+The change is `(p *scionPacketProcessor).LastLayerMem(ub, ubLL, startLL, endLL)`
+in `dataplane_spec.gobra`. It bundles the description of the last decoded layer,
+which used to be spelled out as four clauses in the contract of fourteen
+members:
+
+```
+preserves ubLL == nil || ubLL === ubScionL[startLL:endLL]
+preserves acc(&p.lastLayer, R55) && p.lastLayer != nil
+preserves &p.scionLayer !== p.lastLayer ==> acc(p.lastLayer.Mem(ubLL), R15)
+preserves &p.scionLayer === p.lastLayer ==> ubScionL === ubLL
+```
+
+Two of those are impure implications, which Silicon branches on and re-joins at
+every exhale and every inhale. `process` carries the same thing in an even
+worse spelling — an implication nested inside an implication, keyed on a
+`llIsNil` flag — and exchanges it twice at each of the seventeen calls along its
+path. As a predicate it is one chunk each way, and only `packSCMP`, the one
+member that actually reads the last layer, ever unfolds it.
+
+Nothing is proved that was not proved before: the predicate body is the same
+conjunction, and the `llIsNil` case split was only a second spelling of
+`p.lastLayer.Mem(ubLL)` with `ubLL == nil` folded into the flag. The one clause
+that was dropped rather than moved is `startLL == 0 && endLL == len(ub)` in
+`process`'s SCION-layer case, which no caller used.
+
+**Where the fold goes is the whole trick.** Folding inside `process` — the
+obvious place, since that is who holds the resources across the calls — costs
+about 1200 s on its own, because the predicate then has to be re-derived from
+the `llIsNil` parameterisation, including a slice identity `ub[0:len(ub)] === ub`.
+Folding in `processPkt` instead, right after `decodeLayers` has produced the
+layer and the facts about it are still immediate, is free (350 s against a
+342 s baseline). `process`, `processSCION` and `processEPIC` then just take the
+predicate as a parameter and never open it.
+
+## The same recipe on the SCMP buffer: no gain, and why
+
+The obvious next target was the other thing every validator carries and almost
+none of them touches: the buffer that `packSCMP` serialises an SCMP reply into.
+It is four clauses — two `requires`, two `ensures` — in the contract of
+seventeen members:
+
+```
+requires acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem()
+requires sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
+ensures  acc(&p.buffer, R50) && p.buffer != nil && p.buffer.Mem()
+ensures  sl.Bytes(p.buffer.UBuf(), 0, len(p.buffer.UBuf()))
+```
+
+This was implemented as `SCMPBufMem()` plus an `OutBuf()` getter, all seventeen
+members verified with 0 errors, and it bought **nothing**: 2497 s against 2490 s
+for `process` in a paired A/B. It was reverted (`e0d004b`). Two things are worth
+knowing before anyone tries it again.
+
+**Only the implications were ever the cost.** `LastLayerMem` won because two of
+the four clauses it absorbed were impure implications, which Silicon branches on
+and re-joins at every exhale *and* every inhale. The buffer clauses are plain
+conjunctions: one field chunk, one predicate chunk. Turning them into a single
+predicate chunk changes the constant, not the shape, and the measurement says
+the constant is not where the time is. This is the same lesson as the failures
+above, in a case where the change did shrink the contract: the number of clauses
+is not the cost — the number of *branches* is.
+
+**The permission to the bytes cannot move into a predicate at all.** Postconditions
+such as
+
+```
+ensures respr.OutPkt != nil ==> !slayers.IsSupportedPkt(respr.OutPkt)
+ensures reserr != nil && respr.OutPkt != nil ==>
+	absIO_val(respr.OutPkt, respr.EgressID).isValUnsupported
+```
+
+are stated over the *result*, which aliases the buffer, and both `IsSupportedPkt`
+and `absIO_val` require `sl.Bytes(raw, 0, len(raw))` at write permission. A
+predicate cannot frame a clause stated outside itself, so hiding
+`sl.Bytes(p.buffer.UBuf(), …)` inside `SCMPBufMem()` makes those clauses
+ill-defined at fifteen sites — which is what the first attempt did, and it fails
+with `Precondition of call slayers.IsSupportedPkt(respr.OutPkt) might not hold`.
+Restating each of them under `unfolding p.SCMPBufMem() in …` would work and
+would cost more than the bundling saves. The permission therefore has to stay a
+contract clause, which by itself caps how much of the buffer's footprint can be
+bundled.
+
+## What did work: `MsgsMem`
+
+Same recipe, applied where the profile said the money was, and it paid: the `rc`
+closure went from **1538 s to 384 s - 4.0x - in a paired A/B**, both arms
+reporting 0 errors.
+
+`MsgsMem(msgs, i0, pkts, ingressID, ioValSeq)` in `msgs-spec.gobra` bundles the
+six invariants of the inner loop that are quantified over the 64-message batch:
+the two permissions, `msgs[i].Mem()` and `sl.Bytes(msgs[i].GetFstBuffer(), ...)`,
+and the four pure facts that only those permissions can frame. The one expensive
+exhale now hands over a single chunk.
+
+**The lemmas are the point, not the predicate.** Opening the batch with an
+`unfold` at the top of the loop body and closing it with a `fold` at the bottom
+would buy nothing: the fold would re-do the same quantified work in the same
+large state, which is precisely what the invariant exhale was doing. `TakeMsg`
+and `PutMsg` are lemmas, so the loop body exchanges two predicate chunks and the
+quantified reasoning happens inside members whose state holds nothing but the
+batch. Entering and leaving the loop is a plain `fold`/`unfold`, which is free -
+the profile above shows the whole region around `ReadBatch` at the front-end
+floor.
+
+**`PutMsg` gives back less than `TakeMsg` handed out.** The body consumes the
+message's address and forwards its bytes, so neither `HasActiveAddr` nor the
+agreement with `ioValSeq` still holds for that message. That is what the index
+`i0` is for: those two facts are claimed only from the current position on, and
+`PutMsg` closes the predicate at `i0+1`. It also retires the assertion that was
+marked "crucial to keep verification stable" - it existed only to re-establish
+the invariant for the next iteration, which `PutMsg` now proves.
+
+**Taking a message out breaks buffer injectivity, and that has to be repaired
+explicitly.** Both quantified permissions are keyed on `msgs[i].GetFstBuffer()`,
+so every fold obliges Silicon to show that no two messages share a buffer.
+Inside the batch that fact is free, because `--assumeInjectivityOnInhale`
+asserts it whenever the quantified permission is inhaled - but the message that
+has been taken out is no longer part of any such inhale, so putting it back
+leaves its buffer unrelated to the rest and `PutMsg`'s fold fails with
+`Quantified resource ... might not be injective`. `MsgsMemHole` therefore takes
+the extracted buffer as a parameter and carries the one missing inequality
+across the hole.
+
+An earlier attempt keyed the permissions on `&msgs[i]` instead, by bundling
+`Mem()` and the bytes into a per-element `MsgAndBuf` predicate. That is injective
+by construction and `PutMsg` goes through - but the obligation simply moves to
+the lemma that has to convert back for the next `ReadBatch`, which is stated in
+terms of the buffer-keyed quantifiers. Naming the buffer is the shorter way out.
+
+## What is left to try
+
+1. **Reduce the number of distinct permission amounts.** `p.scionLayer.Mem(..)`
+   is currently used at 18 of them, and the `unfold acc(P, 1-R55)` /
+   `unfold acc(P, R55)` idiom exists only so that a pure function can be
+   evaluated in between. Every extra fraction is another chunk for the complete
+   exhale to summarise.
+2. **Outline the branches of `process`.** `Run` uses seven `outline` blocks;
+   `process` and `processPkt` use none. An outlined block is verified as its own
+   Viper method, so the state that the rest of `process` carries past it is
+   whatever the outline's contract says, not everything the branch touched.
+
+## Reproducing
+
+```sh
+export GOBRA=/path/to/gobra.jar Z3_EXE=/path/to/z3
+./verification/scripts/verify-member.py --list router          # member -> line
+./verification/scripts/verify-member.py router doXover
+./verification/scripts/verify-member.py router rc              # a closure of Run
+```
+
+Two Gobra limitations get in the way and are worth fixing upstream:
+
+* Member isolation cannot be expressed in the JSON configuration that the CI now
+  uses. `input_files` makes Gobra abort with
+  `Logic error: the configuration mode should be one of file, package, recursive
+  or config` (`InputConfig.fromVerificationJobCfg` fills in `input` but not
+  `cutInputWithIdxs`, which is what `InputConfig.rawConfig` dispatches on), and
+  `-i` inside `other` is rejected outright. Hence the script builds a full
+  command line instead.
+* `gobra --config router` from the repository root fails with
+  `Could not find module configuration file gobra-mod.json …`, because the
+  search for the module config walks `getParentFile()` on the *relative* path
+  and stops immediately. An absolute path works.
diff --git a/verification/scripts/verify-member.py b/verification/scripts/verify-member.py
new file mode 100755
index 000000000..d949f684a
--- /dev/null
+++ b/verification/scripts/verify-member.py
@@ -0,0 +1,202 @@
+#!/usr/bin/env python3
+"""Verify a single member of a package, instead of the whole package.
+
+Gobra can be told to verify only the members declared on a given line of a file
+(``-i <file>@<line>``); the chopper then keeps only the slice of the program that
+those members need.  That is the only practical way of attributing the run time
+of a package to individual functions, which is what one needs when a package
+takes hours to verify.
+
+The line numbers are a poor interface, so this script resolves a member *name*
+to the line on which it is declared, and reconstructs the options that the CI
+uses from ``gobra-mod.json`` and the package's ``gobra.json``.
+
+    ./verification/scripts/verify-member.py router doXover
+    ./verification/scripts/verify-member.py router rc            # a closure of Run
+    ./verification/scripts/verify-member.py --list router
+
+Note that isolation cannot currently be expressed in the JSON configuration:
+``input_files`` makes Gobra fail with an internal error and ``-i`` is rejected
+inside ``other``.  The script therefore assembles a full command line itself,
+mirroring what the configuration files say.
+
+The Gobra binary is taken from ``$GOBRA``; it may be either an executable or a
+``.jar`` (in which case it is run with ``java -jar``).  ``$Z3_EXE`` is forwarded
+to Gobra when it is set, and ``$GOBRA_HEAP`` overrides the JVM heap size (8g by
+default) - useful when running several members at once, since each of them can
+take several gigabytes.
+"""
+
+import argparse
+import json
+import os
+import re
+import shlex
+import subprocess
+import sys
+import time
+from pathlib import Path
+
+REPO = Path(__file__).resolve().parents[2]
+MODULE_CFG = REPO / "gobra-mod.json"
+JOB_CFG_NAME = "gobra.json"
+
+# Files that Gobra reads for a package: the sources with a `// +gobra` header
+# plus the specification files.  Test files are skipped, exactly as Gobra's own
+# package resolver does.
+SOURCE_SUFFIXES = (".go", ".gobra")
+
+
+def package_files(pkg: Path):
+    files = []
+    for f in sorted(pkg.iterdir()):
+        if f.suffix not in SOURCE_SUFFIXES or f.name.endswith("_test.go"):
+            continue
+        head = f.read_text(errors="replace")[:4096]
+        if re.search(r"^//\s*\+gobra\s*$", head, re.M):
+            files.append(f)
+    return files
+
+
+# A top-level declaration, e.g.
+#   func (p *scionPacketProcessor) doXover( ... )
+#   func newPacketProcessor( ... )
+# or a named function literal, e.g.
+#   func /*@ rc @*/ (ingressID uint16, ...)
+DECL = re.compile(r"^\s*func\s+(?:\([^)]*\)\s*)?(\w+)\s*[({]")
+CLOSURE = re.compile(r"^\s*func\s*/\*@\s*(\w+)\s*@\*/")
+
+
+def members(files):
+    """Map member name -> list of (file, line number)."""
+    found = {}
+    for f in files:
+        for n, line in enumerate(f.read_text(errors="replace").split("\n"), start=1):
+            m = CLOSURE.match(line) or DECL.match(line)
+            if m:
+                found.setdefault(m.group(1), []).append((f, n))
+    return found
+
+
+def merged_config(pkg: Path):
+    """Merge the module-level defaults with the package's own job config.
+
+    Mirrors Gobra's precedence: the job config wins over the module config.
+    Relative paths are resolved against the directory of the file that
+    declares them.
+    """
+    module = json.loads(MODULE_CFG.read_text()).get("default_job_cfg", {})
+    job_path = pkg / JOB_CFG_NAME
+    job = json.loads(job_path.read_text()) if job_path.exists() else {}
+
+    def resolve(cfg, base):
+        cfg = dict(cfg)
+        if "includes" in cfg:
+            cfg["includes"] = [str((base / p).resolve()) for p in cfg["includes"]]
+        return cfg
+
+    merged = resolve(module, MODULE_CFG.parent)
+    merged.update(resolve(job, pkg))
+    # `other` is concatenated rather than overwritten, like Gobra's merge does.
+    merged["other"] = module.get("other", []) + job.get("other", [])
+    return merged
+
+
+# JSON field -> how it becomes a command-line option.
+FLAGS = {
+    "assert_timeout": lambda v: ["--assertTimeout", str(v)],
+    "backend": lambda v: ["--backend", v],
+    "chop": lambda v: ["--chop", str(v)],
+    "mce_mode": lambda v: ["--mceMode", v],
+    "module": lambda v: ["-m", v],
+    "more_joins": lambda v: ["--moreJoins", v],
+    "includes": lambda v: ["-I"] + list(v),
+    "assume_injectivity_inhale": lambda v: ["--assumeInjectivityOnInhale" if v
+                                            else "--noassumeInjectivityOnInhale"],
+    "overflow": lambda v: ["--overflow" if v else "--nooverflow"],
+    "check_consistency": lambda v: ["--checkConsistency"] if v else [],
+    "conditionalize_permissions": lambda v: ["--conditionalizePermissions"] if v else [],
+    "only_files_with_header": lambda v: ["--onlyFilesWithHeader"] if v else [],
+    "parallelize_branches": lambda v: ["--parallelizeBranches"] if v else [],
+    "print_vpr": lambda v: ["--printVpr"] if v else [],
+    "require_triggers": lambda v: ["--requireTriggers"] if v else [],
+}
+
+
+def options(cfg):
+    opts = []
+    for key, value in cfg.items():
+        if key == "other":
+            opts += list(value)
+        elif key in FLAGS:
+            opts += FLAGS[key](value)
+        # `project_root` is deliberately dropped: Gobra rejects it together with
+        # `-i`, and it would withdraw the friend permissions granted to
+        # `pkg/slayers`.
+    return opts
+
+
+def gobra_command():
+    binary = os.environ.get("GOBRA")
+    if not binary:
+        sys.exit("Set $GOBRA to the Gobra executable or to gobra.jar.")
+    if binary.endswith(".jar"):
+        return ["java", "-Xss1g", "-Xmx" + os.environ.get("GOBRA_HEAP", "8g"), "-jar", binary]
+    return [binary]
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__,
+                                     formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("package", help="package directory, e.g. 'router'")
+    parser.add_argument("member", nargs="?",
+                        help="name of the member to verify; the whole package if omitted")
+    parser.add_argument("--list", action="store_true", help="list the members and exit")
+    parser.add_argument("--dry-run", action="store_true", help="print the command and exit")
+    parser.add_argument("rest", nargs=argparse.REMAINDER,
+                        help="further options, passed on to Gobra verbatim")
+    args = parser.parse_args()
+
+    pkg = (REPO / args.package).resolve()
+    if not pkg.is_dir():
+        sys.exit("no such package: %s" % pkg)
+    files = package_files(pkg)
+    if not files:
+        sys.exit("no files with a '+gobra' header in %s" % pkg)
+
+    declared = members(files)
+    if args.list:
+        for name in sorted(declared):
+            for f, line in declared[name]:
+                print("%-40s %s:%d" % (name, f.relative_to(REPO), line))
+        return
+
+    inputs = [str(f) for f in files]
+    if args.member:
+        hits = declared.get(args.member)
+        if not hits:
+            sys.exit("no member named %r; use --list to see the candidates"
+                     % args.member)
+        if len(hits) > 1:
+            sys.exit("%r is declared %d times: %s" %
+                     (args.member, len(hits),
+                      ", ".join("%s:%d" % (f.relative_to(REPO), l) for f, l in hits)))
+        target, line = hits[0]
+        inputs = [str(f) + ("@%d" % line if f == target else "") for f in files]
+
+    cmd = gobra_command() + ["-i"] + inputs + options(merged_config(pkg))
+    if os.environ.get("Z3_EXE"):
+        cmd += ["--z3Exe", os.environ["Z3_EXE"]]
+    cmd += [a for a in args.rest if a != "--"]
+
+    print(" ".join(shlex.quote(c) for c in cmd), flush=True)
+    if args.dry_run:
+        return
+    start = time.time()
+    rc = subprocess.call(cmd, cwd=REPO)
+    print("\nfinished in %.0f s (exit code %d)" % (time.time() - start, rc))
+    sys.exit(rc)
+
+
+if __name__ == "__main__":
+    main()