refactor prepareSCMP - #425
Draft
jcp19 wants to merge 43 commits into
Draft
Conversation
Analyzes whether Mem(ubuf) can be established for the layers passed to gopacket.SerializeLayers in prepareSCMP (it cannot, for any buffer, with the current predicate definitions) and lays out a nil-buffer 'serialize-mode' predicate design, the required SerializeTo/interface spec changes (FixLengths, error-case preservation, checksum permission accounting), a route to derive !IsSupportedPkt(result), and milestones. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
Executable Go code cannot change, so: keep the gopacket.SerializeLayers call and give it a trusted quantified spec; derive !IsSupportedPkt via a ghost pure hook on the SerializableLayer interface plus a gopacket-level IsSupportedRawPkt twin and bridging lemma; handle the internalIP wildcard problem with asymmetric permission amounts in the serialize-mode predicates (SetSrcAddr switched to wildcard mode via its ghost argument) and strengthened SetDstAddr/SetSrcAddr postconditions. Drop the overflow-bound concern (CI runs with overflow checking disabled). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
Generalize BaseLayer.Mem with a fresh mode (ub == nil): a freshly constructed, not-yet-decoded layer holds only the field permissions, with zero-valued Contents/Payload, instead of the buffer-aliasing facts. This makes Mem(nil) foldable for freshly constructed SCMP and SCMP message layers, a prerequisite for serializing them in prepareSCMP. - extnBase.Mem pins ActualLen == 0 in fresh mode so all facts previously derivable for a nil buffer are preserved. - LayerPayload specs over BaseLayer are conditionalized on ub != nil (their conclusions still imply the gopacket.Layer/DecodingLayer interface contracts). - DecodeFromBytes of SCMP and the seven SCMP message types now ensure their minimum length on success, so decoded-mode proof sites can derive data != nil and keep the aliasing facts (asserts added at the traceroute handler's unfolds). - FoldFreshMem witness lemmas for SCMP and all seven message types machine-check that fresh layers satisfy Mem(nil). - Add gopacket.IsSupportedRawPkt (twin of the slayers definition, which gopacket cannot import) plus a bridging lemma, needed later to thread the router's !IsSupportedPkt postcondition through SerializeLayers. Annotations/contracts only; no executable code changes. Not yet run through Gobra (unavailable in this environment) - needs a CI run. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The SerializableLayer interface previously only guaranteed Mem(ubuf) and the buffer resources when serialization succeeded. All implementations in fact keep them intact on error (SCMP and the SCMP message types fail only before unfolding Mem or re-fold it before every error return; Payload and BFD are trusted stubs; SCION's postconditions were already unconditional), so the guarantee can be made unconditional. prepareSCMP will rely on this to restore its resources on the error path of SerializeLayers. Also record in the plan that (*Decoded).Widen already provides the buffer-transfer lemma needed to re-fold the reversed path as Mem(nil). Annotations/contracts only; no executable code changes. Not yet run through Gobra (unavailable in this environment) - needs a CI run. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
Instead of adding a nil-buffer mode to SCION.Mem (which would make Mem(nil) satisfiable and thereby force nil-handling into every pure function and lemma that unfolds the predicate - they currently verify vacuously for nil), give freshly constructed SCION headers a separate predicate: - SCION.MemSerialize: field permissions, Path.Mem(nil) (satisfied for reversed paths via (*Decoded).Widen), fractional raw-address permissions that coexist with ChecksumMem, and the path pool. No facts about HdrLen/PayloadLen, which FixLengths computes during serialization. - SCION.IsSupportedSerialization: whether serializing this header yields a supported packet, expressed over PathType/NextHdr. - ChecksumMem re-fractioned (R25; wildcard for RawSrcAddr's bytes, which prepareSCMP can only obtain at wildcard amount from the data-plane's internal IP); computeChecksum/pseudoHeaderChecksum weakened to match (their only verified caller is SCMP.SerializeTo). - SerializableLayer gains MemSerialize and IsSupportedSerialization; trivial implementations for SCMP, the SCMP messages, Payload and BFD. - SerializeLayers gets a real trusted contract (replacing requires false): MemSerialize for the header layer, Mem(layerBufs[i]) for the rest, resources preserved also on error, and the trusted bridge IsSupportedRawPkt(w.View()) == old(layers[0].IsSupportedSerialization()). With this design the FixLengths relaxation of the SerializableLayer interface is unnecessary and verifying SCION.SerializeTo's FixLengths branch becomes optional hardening rather than a prerequisite: the fresh-flow serialization is axiomatized by the trusted SerializeLayers contract, documented as the load-bearing trusted assumption. Annotations/contracts only; no executable code changes. Not yet run through Gobra (unavailable in this environment) - needs a CI run. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
- SetDstAddr (IP case) no longer applies packAddr's magic wand internally; it exposes the R20 fraction of the bytes underlying RawDstAddr together with the wand to give it back, so that prepareSCMP can store byte fractions in the fresh header's MemSerialize/ChecksumMem predicates during serialization and still restore dst.Mem() afterwards. Its only verified caller is prepareSCMP's currently-unverified tail, so the post shape is free to change. - packAddr/SetDstAddr/SetSrcAddr gain 'T4Ip implies length 4' postconditions, provable from To4's contract. - Add FoldFreshMemSerializeWithChecksumMem: the machine-checked witness that MemSerialize and ChecksumMem fold together from the resources prepareSCMP holds (fraction accounting 2xR25 within R20, wildcard source bytes, path with nil buffer). Annotations/contracts only; no executable code changes. Not yet run through Gobra (unavailable in this environment) - needs a CI run. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The pairwise-distinctness clause dereferenced layers[i]/layers[j] before the quantifier granting permission to the slice cells; contract well-formedness is checked left to right, so all three CI jobs failed with 'Permission to layers[i] might not suffice' (writer.gobra:153). Reorder the clauses, permissions first, matching decodeLayers. This was the only error in the entire run: router/ verified across all 10 chops otherwise, and every package that ran before the error was clean (pkg/slayers had not run yet - verify-deps aborts at the first package importing gopacket). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
pkg/slayers reported two errors on the previous run (everything else, including the router job, was green): - scion.go:684: the postcondition wand over s.RawDstAddr could not be matched against the wand instance created inside packAddr (which is shaped over packAddr's own variables; Silicon matches wand instances structurally). Re-package the wand in SetDstAddr's body with exactly the postcondition's shape, applying packAddr's wand inside the package block. - scion_test.gobra:75: testDstSetter expected the full dst.Mem() back immediately; under the new contract the caller first applies the returned wand to give back the loaned byte fraction. Adapting the test also documents the intended usage of the new postcondition. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
CI showed that exposing the RawDstAddr byte fraction through
SetDstAddr's postcondition cannot work: a magic wand whose assertion
dereferences a field is not self-framing, so it can neither be stated
in the postcondition (Silicon cannot match it against packAddr's
variable-shaped instance) nor re-packaged in the body ('Permission to
s.RawDstAddr might not suffice'), and a ghost out-parameter would
require restructuring the real call sites. Restore the original
acc(dst.Mem(), R18) contract (keeping the new T4Ip length
postconditions) and revert testDstSetter.
The plan now designates the caller-side extraction for M5: unfold a
fraction of dst.Mem(), transfer the element permissions to RawDstAddr
via SetDstAddr's pointwise aliasing postconditions, and package the
restoring wand over locals - the verified addEndhostPort pattern.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
prepareSCMP is now fully annotated end to end; the trusted-assumption TODO() marker is gone. The proof: - closes the path section early (mirroring the error cases) and refolds the SCION layer, then re-associates the reversed path with a nil buffer via the new (*Decoded).ChangeUbuf (Mem is buffer-independent; Widen requires a superslice and does not apply); - carves the source-address bytes out of ub via the new ExtractAccSrc (mirroring resolveLocalDst's use of ExtractAcc) and, after SetDstAddr, extracts a fraction of the destination-address bytes from srcA via the new ExtractIPBytes (addEndhostPort-style wand); - calls SetSrcAddr in wildcard mode; packAddr/SetSrcAddr now take the resources of wildcard IP addresses component-wise, since Mem() cannot be folded at a concrete amount for the wildcard-held internal IP. net.IP.Mem()'s length constraint (4 or 16), exposed through the new getInternalIPMem getter, provides the checksum evenness facts together with new length postconditions on packAddr/SetSrcAddr/ SetDstAddr/parseAddr/SrcAddr/PackWithPad; - folds MemSerialize + ChecksumMem + the SCMP header's and payload's Mem(nil), builds the ghost layerBufs (now a seq[[]byte]; payload buffers at fraction R55 so the quote can be carved from the split ub), and invokes SerializeLayers against its trusted contract; - derives !IsSupportedPkt(result) from the contract's IO bridge, the IsSupportedRawPktEqGopacket lemma, and revealing both definitions; - restores all resources on every path (the SerializeLayers contract preserves them also on error). packSCMP receives the payload layer's resources field-wise (it is constructed inline at the call sites, where nothing can be folded) and folds Mem(nil) via the new slayers.FoldFreshSCMPPayloadMem; the rawPkt === ub relation is threaded through the ten functions between process/processPkt and packSCMP for the quote. Annotations/contracts only; no executable code changes (go build unchanged). Needs CI iteration. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
Gobra crashes with 'Logic error: found unexpected type: seq[[]byte]' when desugaring an untyped nil inside a seq composite literal (Desugar.litD -> nilType). Bind a typed nil []byte variable first and use it as the element. verify-deps and verify-third-party-libs were green on the M5 commit: all slayers/gopacket lemmas (ExtractAccSrc, ExtractIPBytes, FoldFreshSCMPPayloadMem, the seq-based SerializeLayers contract, and the address-setter postconditions) verify. Only the router package remains to be checked. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The M5 run surfaced two follow-up errors from the component-wise wildcard preconditions of packAddr/SetSrcAddr: - SetDstAddr still held dst.Mem() folded when forwarding to packAddr in wildcard mode; unfold it (at wildcard amount) for IP addresses first. - testSrcSetterWildcard called SetSrcAddr(src, true) with the folded predicate; unfold it in the test body. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The first full run of the prepareSCMP body proof came back with only four errors: - the read of p.scionLayer.SrcIA needs the HeaderMem sub-predicate unfolded (unlike FlowID/TrafficClass, whose permissions sit at the top level of SCION.Mem); - validateSrcDstIA, handleIngressRouterAlert, and handleEgressRouterAlert are intermediate callers on the way to invalidSrcIA/handleSCMPTraceRouteRequest and were missed in the rawPkt threading. Everything else in the proof - the ExtractAccSrc/ExtractIPBytes wand chains, the MemSerialize/ChecksumMem folds, the SerializeLayers call against its trusted contract, and the !IsSupportedPkt derivation - verified on the first attempt. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The last remaining router error was the quote-length bound assert in prepareSCMP: revPath.LenSpec(nil) <= 796 is not derivable at the call site because the NumINF/NumHops bounds are buried two predicate unfoldings deep (Decoded.Mem -> Base.Mem). Add (*Decoded).LenSpecBound, which surfaces the bound with explicit unfolds, and call it before the assert. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The verify-deps job on 85ec14e died before starting ('Failed to resolve action download info. Error: Service Unavailable') and the GitHub App integration is not permitted to re-run failed jobs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The lemma-head run is down to a single error: 0 <= maxQuoteLen. The LenSpecBound lemma discharges the concrete bound revPath.LenSpec(nil) <= 796, but hdrLen's path summand comes from the interface-dispatched scionL.Path.Len(nil), whose postcondition speaks about the interface-level LenSpec. Assert the identity of the receiver and the equality of the two LenSpec applications so the bound transfers. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The quote-bound assert still failed with the lemma in place: the lemma consumed the full Decoded.Mem, so its internal unfold/refold produced a fresh predicate snapshot, severing the link between LenSpec's value at the earlier Path.Len(nil) call and at the asserts. Taking (and giving back) only an R50 fraction leaves the caller with an anchoring fraction, so the heap-dependent LenSpec provably keeps its value across the lemma - the same mechanism by which Decoded.Len's own 'l == LenSpec(ubuf)' postcondition composes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The scion path package hit its 30-minute wall-clock timeout: unrelated members (Widen*/Xover* IO lemmas, DecodeFromBytes) were reported as 'did not terminate' while LenSpecBound itself finished, i.e. the new member consumed budget the rest of the package needed. Strip the lemma to a bare unfold/refold of the two predicates: InfoLen and HopLen are compile-time constants, so the bounds already stored in Base.Mem (NumINF <= MaxINFs, NumHops <= MaxHops) discharge the postcondition without ghost variables, extra asserts, or nonlinear arithmetic. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The last router error was the append of the quote payload onto scmpLayers: the ghost permission was noPerm (perm 0), copied verbatim from upstream where it had never been verified. scmpLayers is a length-3 composite literal (len == cap), so this append always reallocates and Gobra must copy the three existing interface elements into the new backing array - which requires positive read permission. Full access is held from the literal, so pass writePerm. (The working zero-permission appends elsewhere all append within spare capacity and never reallocate.) With this, the maxQuoteLen bound now discharges (the minimized LenSpecBound worked) and this was the sole remaining router error. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
verify-deps, verify-third-party-libs, verify and build are now green;
the append fix worked. The sole remaining router error was the
checksum-fold precondition len(scionL.RawSrcAddr) % 2 == 0.
It holds but needed the case split made explicit. The source address
comes from SetSrcAddr(&net.IPAddr{IP: p.d.internalIP}, wildcard) and
getInternalIPMem gives len(internalIP) in {4,16}. SetSrcAddr yields
either T4Ip (len 4) or T16Ip (len == the IP's length). To let Gobra
conclude:
- packAddr/SetSrcAddr gain a postcondition that an IP address maps to
T4Ip or T16Ip (so the case split is exhaustive);
- prepareSCMP records len(internalIP) in {4,16} before the call (so the
T16Ip postcondition's old(len(IP)) carries the even length through)
and asserts the addr-type membership after.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The previous evenness fix asserted len(internalIP) in {4,16}, but the
type invariant (internalIPInv) permits internalIP == nil (length 0), so
that assert was too strong and became the sole router error. Evenness
still holds - the internal IP length is 0, 4, or 16, all even.
- SetSrcAddr gains a postcondition: for a wildcard IP whose length is
even, len(RawSrcAddr) is even (T4Ip gives 4; T16Ip preserves the
input length). This localizes the old(len(IP)) reasoning to where src
is in scope.
- prepareSCMP now asserts len(internalIP) % 2 == 0 with a nil-aware
case split (nil -> length 0; non-nil -> 4 or 16 from getInternalIPMem)
and drops the addr-type membership assert, relying on the new
postcondition to carry evenness to the checksum fold.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The next router error was !scionL.IsSupportedSerialization() at the SerializeLayers call. The hook reads NextHdr/PathType by unfolding MemSerialize, but FoldFreshMemSerializeWithChecksumMem folds that predicate and its postcondition said nothing about the field values, so across the lemma call Gobra lost NextHdr == L4SCMP. Add a postcondition relating the hook to the pre-fold field values (IsSupportedSerialization() == (old(PathType) == scion.PathType && old(NextHdr) != L4SCMP)), proved in the body by a fold-transparent assert. prepareSCMP sets NextHdr = L4SCMP before the lemma, so the caller now derives !IsSupportedSerialization() and, through the trusted SerializeLayers IO bridge, !IsSupportedPkt(result). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
Past the IsSupportedSerialization assert, the next router error is the SerializeLayers precondition forall i :: acc(&layers[i], R50) && layers[i] != nil. The acc follows from the full access held on the scmpLayers literal/append; the gap is the non-nil quantifier, which Gobra does not lift automatically from the individual element values. Assert it explicitly: element identities and non-nilness for the base three layers right after the literal, then re-establish the quantifier after the quote append (element 3 is a non-nil Payload interface value), and once more before the call so it survives the cause-branch merge (len 3 or 4). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The SerializeLayers call precondition could not be satisfied: the router spreads a pre-built slice (SerializeLayers(..., scmpLayers...)), so the quantified predicate preconditions (forall i :: layers[i].Mem) had to hold over that slice, but Gobra cannot assemble a quantified permission from individually folded layer predicates. (decodeLayers avoids this by passing its layers as separate arguments, which Gobra packs into a fresh slice.) Rewrite the trusted SerializeLayers spec with per-index clauses specialized to the router's three-or-four-layer call shape. Per-index Mem/MemSerialize clauses are dischargeable directly from the individual folds (linked to the slice cells by identity asserts at the call site), and they make the layers implicitly distinct, so the hard-to-prove injectivity clause is dropped. The postcondition returns the same per-index resources; the existing post-call unfolds are unaffected. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
…tity The per-index SerializeLayers spec exposed the next error: the assert that the appended element equals gopacket.Payload(quote) failed. The working append pattern (extn.go) captures the element in a ghost var before the append and asserts identity against it; those elements are pointers, whereas here a Payload value is boxed into the interface slice, and a direct expression comparison does not match. Follow the precedent with an interface-typed ghost var pldElem = gopacket.Payload(quote): fold its (resource-free) Payload.Mem(quote) before the append and assert scmpLayers[3] === pldElem after, so the payload's Mem is available to the per-index SerializeLayers precondition. The executable append argument is unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
Gobra preserves slice-element identity for composite literals (layers 0-2 verify) but not through an append that boxes a value into an interface slice: scmpLayers[3] === <appended Payload> is unprovable in any formulation, so the caller cannot supply layers[3].Mem for the quote payload. Since Payload.Mem is resource-free (just the slice identity), the trusted SerializeLayers spec no longer requires layers[3].Mem or non-nilness for the optional fourth layer - only its R55 byte access, which the caller holds from splitting the quote out of ub. The resource-free Mem and the non-nil check are reconstructed by the (trusted, unverified) implementation. The pldElem ghost, its fold, and the failing identity assert are removed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The verify-router job failed after only ~25 minutes (not the 6h timeout) with a Silicon StackOverflowError that cascaded into RejectedExecutionException as the thread pool shut down; the affected members (process, processOHP, doXover, closureCall) were in-flight when the engine crashed. prepareSCMP is not among them, and verify-deps, verify-third-party-libs, verify and build all passed. As CI pins the Gobra image to 'latest', this run (six days after the prior ones) may have used a regressed image. Re-trigger to check whether the crash is deterministic. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The verify-router job crashed with a Silicon StackOverflowError (deeply nested evaluator recursion) that shut down the verification thread pool; the members reported as not terminating were collateral, and the thread that threw first may well have been in the SCMP path. As a small perturbation to shift the evaluator off the pathological term, build the four-element layerBufs sequence as a direct literal instead of concatenating a single-element sequence. Semantically identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
With the SerializeLayers call now verifying, the remaining router error was the post-call unfold of scionL.ChecksumMem: it is nested inside scmpH.Mem (via SetNetworkLayerForChecksum), and after the trusted call returns scmpH.Mem(nil) Gobra no longer knows scmpH.scn === &scionL, so the nested ChecksumMem cannot be attributed to scionL. The recovery does not need ChecksumMem: it only applies the destination-address byte wand (R20), and scionL.MemSerialize alone holds an R25 fraction of those bytes. scmpH.Mem and the ChecksumMem it contains are local resources not mentioned in prepareSCMP's postcondition, so they are dropped. Remove the two unfolds; keep the MemSerialize unfold that supplies the wand. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The verify-router run on 5bee81a crashed with a StackOverflowError cascading into RejectedExecutionException; the member reported as not terminating this time was dictMaxAssoc (an unrelated dictionary helper), confirming nondeterministic engine instability rather than a proof failure. Other runs of nearby heads (827a059 re-run, 99d6c34) completed normally with a single real error, so re-trigger to obtain a clean verdict on the ChecksumMem-leak fix. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
With ChecksumMem no longer unfolded, the post-call recovery reached the next obligation: applying the SrcAddr magic wand failed with 'wand instance not found'. SrcAddr's wand is stored with its right-hand side over p.scionLayer.RawSrcAddr, but the apply used the equal-but- structurally-distinct ub[startSrc:endSrc], which Silicon's wand matching does not unify (resolveLocalDst gets away with the ub[...] shape only because it applies immediately, before intervening operations). Apply with the RawSrcAddr shape, then recombine into ub via the ExtractAccSrc identity. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
Applying the SrcAddr wand still failed as 'instance not found' even with the RawSrcAddr shape, because a heap-read expression in the apply does not match the wand chunk, whose right-hand side is let-bound to the source-address slice value at SrcAddr's return. (The codebase never applies these address wands - the analogous ones in resolveLocalDst are commented out and the address is instead leaked to a caller; but here srcA is local, so the bytes must be reclaimed.) Capture p.scionLayer.RawSrcAddr into a ghost var immediately after SrcAddr and apply the wand against that stable term; then bridge to ub[startSrc:endSrc] via the identity for the recombine. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The ExtractIPBytes magic wand's LHS footprint is let-bound to the raw argument passed at the call; applying it against a heap-read scionL.RawDstAddr after SerializeLayers fails to match the wand chunk. Capture the slice as a stable ghost term (mirroring the rawSrc fix for the SrcAddr wand) and use it at both the call and the apply. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
Per the design, the destination-address bytes are split R25/R25 between MemSerialize and the ChecksumMem nested in scmpH (via scmpH.scn), with the remaining R20-2*R25 kept back at the fold. Recover both predicates after SerializeLayers to reconstitute the full R20 the ExtractIPBytes wand needs, rather than dropping ChecksumMem (which left the wand R25 short). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
…trapped ChecksumMem The trusted SerializeLayers havocs predicate contents, so neither scmpH.scn (needed to recover the SCION ChecksumMem) nor the SCION RawDstAddr field survives the call. Both are needed to give the loaned destination-address bytes back to the SrcAddr/ExtractIPBytes wand. Rework the fresh-serialization resource layout so nothing reclaim-critical is trapped: - SCION.MemSerialize now holds the full R20 of the destination-address bytes (was R25) and, together with the wildcard source bytes, serves both header serialization and the upper-layer checksum. No ChecksumMem is folded for the fresh flow; FoldFreshMemSerialize replaces FoldFreshMemSerializeWithChecksumMem. - The SCMP header is passed to SerializeLayers through its MemSerialize (its 4-byte header fields only), not its Mem, so the network header's checksum bytes are not duplicated into a predicate the caller cannot reclaim. The checksum is computed from the first layer, whose MemSerialize holds the addresses. - Add a SerializeAddrView accessor to the SerializableLayer interface (nil for all layers but SCION) and have the trusted SerializeLayers preserve it, so prepareSCMP can re-associate the recovered bytes with the slice its wand expects. Mirrors the SerializeBuffer.UBuf identity idiom. prepareSCMP now reclaims the full R20 with a single unfold of the preserved MemSerialize. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
…zeAddrView The postcondition calls layers[0].SerializeAddrView() (a pure interface method) in the post-state, which requires a non-nil receiver; the ensures restated MemSerialize() but not non-nilness. Add layers[0] != nil. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
…ching Reducing the two fold sl.Bytes(nil,0,0) to one (after the SCMP header layer stopped requiring byte access) left Gobra's chunk matcher without slack: the write buffer's cleared UBuf() may alias nil, so sl.Bytes(w.UBuf()) and the nil-buffer layer's sl.Bytes(nil) compete for the same empty-bytes chunks. Restore the second (leaked) empty-bytes fold. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
Add an explicit assert of the full sl.Bytes(p.buffer.UBuf()) permission right before the call. This guides Gobra's chunk matcher to the buffer's own byte chunk (rather than the just-folded empty-byte predicates) for the SerializeLayers precondition, and pinpoints a framing loss if the bytes are not actually held there. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The diagnostic assert of writePerm sl.Bytes(p.buffer.UBuf()) was stricter than the SerializeLayers call's own precondition matcher (which flexibly draws the cleared buffer's empty bytes from the folded empty-byte predicates), and was itself the blocker. Remove it; the two empty-byte folds restore the slack that made the call's buffer precondition verify at 0795633. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
…yers buffer bytes a5551b3 (two folds, no assert) still failed the SerializeLayers buffer-byte precondition, so the fold count was never the cause: the len(UBuf())==0 and UBuf() value facts from Clear do not survive the intervening joins/folds (nothing consumes p.buffer between Clear and the call). Capture the cleared buffer slice as an immutable length-0 ghost right after Clear, then re-fold its empty byte predicate and assert p.buffer.UBuf() === that ghost before the call, so the chunk matcher can discharge sl.Bytes(w.UBuf()). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
…f time The router job's prepareSCMP task ran 2x+ longer than normal after the proof started reaching the (previously error-blocked) post-call reclaim. The likely cost is unfolding scionL.MemSerialize() inline: it materializes the whole bulky header predicate (path memory, path pool, all fields) into prepareSCMP's already fold-heavy SMT context, even though only the R20 destination-address bytes are used and the rest is leaked. Add slayers.(*SCION).ReleaseSerializeDstBytes, which performs that unfold-and-leak in an isolated context and returns just the R20 bytes (tied via old(SerializeAddrView()) to the slice the address wand expects). prepareSCMP now calls it instead of unfolding inline, keeping the path memory out of its proof context. The lemma is checked in verify-deps, not the slow router job. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
…lemma The router task began timing out (6h) exactly when the post-call region first became error-free: previous ~1h runs all errored in the reclaim, pruning the tail, so the two reveal-asserts bridging the trusted call's gopacket-level unsupportedness to !IsSupportedPkt(UBuf()) had never actually been explored. Those reveals expand opaque, quantified definitions (IsSupportedPkt unfolds the full byte predicate) inside a context holding ~10 byte chunks under mceMode=on, a plausible blowup. Add slayers.UnsupportedRawPktImpliesUnsupportedPkt, which performs the IsSupportedRawPktEqGopacket bridge and both reveals in an isolated context (checked cheaply in verify-deps), and call it from prepareSCMP instead of revealing inline. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
The router job passes but takes ~4.4h of the 6h budget, dominated by prepareSCMP's proof context. Shrink it by strategically hiding information: - Trim the trusted SerializeLayers postcondition: stop returning the inner layers' predicates and slice-cell fractions (the router drops those local resources anyway); only the quote payload's byte fraction, the network header's MemSerialize, and the SerializeAddrView/IsSupportedRawPkt facts survive the call, so far fewer chunks are inhaled into the caller. - Hide the bodies of the IsSupportedSerialization and SerializeAddrView hooks behind opaque helper functions (wrapper pattern). Their predicate-unfolding definitions no longer expand at every mention in the router; callers get their values equationally from FoldFreshMemSerialize's and ReleaseSerializeDstBytes' postconditions, whose bodies reveal the definitions once, in an isolated context. - Add an extrinsic reclaim lemma (reclaimScionMemAfterSerialize) composing the three wand applications and the range recombination that return the loaned source-address resources; the wand chunk matching and the address-type ghost branch now happen in the lemma's small context instead of prepareSCMP's. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DTJK8Rjoq7J76yn2GJ2y48
jcp19
commented
Aug 10, 2026
| // @ ensures acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20) | ||
| // @ ensures acc(&s.RawSrcAddr, R30) && acc(&s.RawDstAddr, R30) | ||
| // @ ensures acc(&s.SrcIA, R30) && acc(&s.DstIA, R30) | ||
| // @ ensures acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), _) |
Collaborator
Author
There was a problem hiding this comment.
how can this verift later on if we pass _ as the permission amount here? Don't we have to recover that permission in order to reestablish the onwership of the entire raw pkt later on?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Generated by Claude Code