refactor prepareSCMP#425
Draft
jcp19 wants to merge 18 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
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