Refactor packet parsing to use seq[byte] views instead of slice permissions#423
Draft
jcp19 wants to merge 36 commits into
Draft
Refactor packet parsing to use seq[byte] views instead of slice permissions#423jcp19 wants to merge 36 commits into
jcp19 wants to merge 36 commits into
Conversation
Describes how to replace slice+permission-based ghost parsing functions (Timestamp, BytesToIO_HF, CurrSeg, absPkt, ...) with permission-free pure functions over seq[byte], obtained from a new opaque View function in the slices package. Includes the strengthened slice-lemma specs, the list of offset-equality/widening lemmas that become redundant, the new lemmas required (view extensionality, write-effect), and a bottom-up migration order. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Add an opaque ghost pure function View(s, start, end) that abstracts the contents of a Bytes predicate instance into a seq[byte], characterized elementwise via GetByte in its postcondition. Strengthen the specs of SplitByIndex/CombineAtIndex/Reslice/Unslice/SplitRange/CombineRange to relate the views of the predicate instances they exchange, add the extensionality lemma ViewEqFromElements and the subslice lemma ViewOfSubslice, and define seqs.ToSeqByte as an alias of View. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
ConsDir, Peer, Timestamp, AbsUinfo, BytesToAbsInfoField and BytesToIO_HF now take exactly the bytes of the field they parse as a seq[byte], computed from a buffer with sl.View, and no longer require offsets or sl.Bytes permissions. They read multi-byte fields with the byte-level binary.BigEndian.*Spec functions, which removes the unfolding and AssertSliceOverlap boilerplate. BytesToAbsInfoFieldHelper, the slice-based MAC helpers and the OffsetEq/Widen lemmas are removed; a seq-based FromSeqToMacArray/EqualSeqImplyEqualMac replaces the latter. The DecodeFromBytes/SerializeTo proofs relate the buffers to the parsers through views. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
CurrSeg/LeftSeg/RightSeg/MidSeg/hopFields/segment, RawBytesToMetaHdr, RawBytesToBase, validPktMetaHdr, absPkt, the *WithInfo family and all lemmas relating them (Widen*, *SegEquality, Xover*, IncCurrSeg, HopsFrom*, Align*) now operate on mathematical sequences obtained with sl.View instead of byte slices guarded by sl.Bytes. This removes all permission threading from those lemmas, including the recursive fraction-halving tricks; boundary lemmas and CorrectlyDecoded* keep their buffer arguments and take views internally. The SetInfoField and SetHopField proofs are restructured around a single SplitRange/ CombineRange pair over the written field, replacing the previous decomposition of the buffer into per-infofield and per-segment predicate instances. Base/MetaHdr specs (EqAbsHeader, DecodeFromBytesSpec, SerializeToSpec) are expressed over views as well. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
GetAddressOffset, GetLength, GetPathType, GetNextHdr, ValidPktMetaHdr, IsSupportedPkt and EqPathTypeWithBuffer now take the view of the packet instead of a slice with a sl.Bytes predicate, which merges the *WithinLength variants into the plain getters and the slice-based IsSupportedPkt into the former IsSupportedRawPkt. ValidHeaderOffset takes the view explicitly and its To/FromSubSlice lemmas become pure sequence lemmas; IsSupportedPktSubslice likewise. EqAbsHeader keeps its buffer signature but is defined through the view and scion.RawBytesToBase. The SCION SerializeTo/DecodeFromBytes proofs are restructured around views, dropping the reslicing choreography that only served the old heap-dependent lemmas. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
absPkt and absIO_val now abstract packets from the view of the buffer rather than from a slice guarded by sl.Bytes; MsgToAbsVal and absReturnErr take the view at the boundary. The widening lemmas (absIO_valWidenLemma and helpers) and the AbsPktToSubSliceAbsPkt/ SubSliceAbsPktToAbsPkt bridging lemmas become permission-free sequence lemmas built on sl.ViewOfSubslice and the seq-based scion.Widen* lemmas. All dataplane.go contracts and proof annotations are rewritten to pass views to the converted functions. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Gobra applies Go's automatic semicolon insertion rules, so a spec line ending in ++ is parsed as a postfix increment and the clause fails to parse. Keep the concatenation operator mid-line. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
- Restore the MetaLen bound of MetaHdr.DecodeFromBytesSpec and SerializeToSpec as a body conjunct instead of a precondition: as a precondition it is not yet established at the point where Base.DecodeFromBytes's guarded postcondition mentions the spec. - Add CombineRangeNoView_Bytes, a variant of CombineRange_Bytes without view postconditions, for contexts where heap-dependent functions cannot be evaluated in the old state, and use it in the magic-wand package block in the epic package. - State CombineRange_Bytes's view postcondition under a single old() instead of one old() per concatenated view. - In the dataplane, evaluate the truncated ValidHeaderOffset facts over the view of the left subrange instance sl.View(ub, 0, startP), which stays available while the whole-range instance is split, and bridge between the two forms with asserts around the To/FromSubSlice lemmas. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Bytes exists to hide the quantified permissions to a slice's elements; exposing a quantified elementwise equality as a postcondition of View reintroduced a quantifier at every application, polluting the proof context of every client (and dragging GetByte's precondition into every state where a View application is evaluated, including old states at call sites). View now only exposes the length of its result; the elementwise characterization is established explicitly, where needed, with the new ViewElems lemma. The slices-internal proofs and the DecodeFromBytes/SerializeTo proofs invoke it at the points where they bridge between heap contents and views, and seqs.ToSeqByte no longer restates the quantified equality. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
…quantifiers The explicit elementwise reasoning made SplitByIndex_Bytes time out: the combination of the ViewElems quantifier, the GetByte bridging quantifiers and sequence take/drop axioms blows up instantiation. Prove the view relations of the split/combine/reslice lemmas structurally instead, with two recursive lemmas over ViewAux (ViewAuxSplit and ViewAuxReslice) that never introduce quantified content facts. ViewElems and ViewEqFromElements remain available for proofs that genuinely need the elementwise characterization, but the slices-internal proofs no longer use them. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
ViewAuxSplit and ViewAuxReslice required the elementwise wildcard permissions without ensuring them back. Within the package this is harmless, but importing packages model the post-state from the contract alone, where the ViewAux applications in the postcondition then lack any permission to the slice elements. Declare the quantified permissions as preserved. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The application of ViewAux to the subslice in the postcondition is only well-defined given the pointer equalities between the elements of the subslice and of the original slice. Inside the package these facts come from the lemma body, but importing packages only see the contract, so bind them in the postcondition itself with the usual AssertSliceOverlap let-binding. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
CombineAtIndex_Bytes and ViewOfSubslice timed out because every ViewAux application in their contexts instantiated both its recursive definitional axiom and its quantified elementwise postcondition. Treat ViewAux like View itself: opaque, exposing only the length of its result. The recursion lemmas unroll the definition one step at a time with reveal, and the elementwise characterization moves into the recursive ViewAuxElems lemma, used only by ViewElems. Also give the verification-directory CI job more headroom, as the slices package now carries the contents reasoning. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The ViewAux helper lemmas preserved the elementwise permissions at wildcard amount, so callers could no longer restore their predicate instances at a concrete fraction afterwards: consuming a wildcard from p and receiving a wildcard back does not yield p. Give the helper lemmas an explicit permission parameter instead. In Unslice_Bytes, the permission-transfer loop additionally havocs the byte values from the verifier's perspective unless the invariants track them, so tie the contents to the entry view throughout the loop again. Also trigger the bridging assertion of ViewEqFromElements on the caller-supplied sequence, matching its precondition. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Equating applications of an opaque heap-dependent function across an unfold or fold does not hold up in Silicon, which made every snapshot hop in the slices proofs fail; the definitional axiom of a transparent recursive function is fuel-limited and harmless (hopFields relies on this throughout), so drop the opaque modifier from ViewAux while keeping its contents out of the postconditions. Furthermore, a call to ViewElems havocs the predicate snapshot from the caller's perspective, detaching facts anchored to earlier View and GetByte applications; ViewElems now additionally ensures that the view and the bytes are unchanged, so callers' facts carry across the call regardless of whether they were established before or after it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The six in-package failures of the last run all had the same shape: a view captured before a call to one of the recursion lemmas could not be related to ViewAux applications after the call, because the lemma consumes the full fraction of the quantified permissions and Silicon does not preserve the snapshot identity across the call. Instead of relying on that identity, the recursion lemmas now promise explicitly that they change neither the bytes of the slice nor the values of the relevant ViewAux applications, so the callers' equalities survive the calls as contract-carried facts. ViewOfSubslice previously unfolded both predicate instances and ran the recursion lemmas over two overlapping quantified permission sets, which made the prover diverge. It is now proved by composing SplitRange_Bytes and CombineRange_Bytes on half of the permissions to the whole slice: the retained fractions pin the views, and the split postcondition provides the subsequence relation directly. CombineRange_Bytes's view postcondition now applies old() to each View application separately instead of to the whole concatenation; this is the shape CombineAtIndex_Bytes already uses, and the only shape that is known to re-check robustly when contracts are imported by the router verification job. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
…yers The previous round left four ill-formedness errors: the asserts that relate a freshly folded predicate instance to ViewAux evaluated ViewAux after all element permissions had been folded away. The folds now happen in two halves, so that the bridging assert runs while half of the element permissions are still held. ViewAuxSplit stopped terminating under its enlarged contract; its byte-preservation quantifier is not used by any caller (framing covers the one byte the proof needs), so it is dropped, together with two redundant guiding asserts. In slayers, the common-header outline of SCION.DecodeFromBytes unfolded the full fraction of Bytes(data), losing the connection between the captured view and the refolded instance, which made the GetPathType postcondition fail. It now unfolds only R42 out of R41, so the retained instance pins the view. SCION.SerializeTo's assert vSer0[4] == b4 failed because no GetByte term from the state before the ViewElems call existed, leaving the lemma's preservation postcondition uninstantiated; explicit GetByte asserts on both sides of the call provide the triggers. DecodeFromBytes also gets exhaleMode(1), matching the setter lemmas in path/scion, as an attempt to stop its divergence under the default exhale mode. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Both the single-old and the per-application-old formulations of CombineRange_Bytes's view relation fail to re-check under the router job's verification flags, each time reporting the first View application under old(). Stating the relation as three separate clauses, one per predicate instance and each equating a subsequence of the combined view with the old view of one instance, gives the importing check smaller assertions to handle, isolates which application the failure belongs to, and keeps the other clauses usable at call sites even if one clause keeps failing. The information content is unchanged, and callers consume the relation in this sliced form anyway. ViewAuxSplit still did not terminate after its contract was slimmed, so it now runs with exhaleMode(1), like the setter lemmas in path/scion that faced similar divergence. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Carrying the preservation of all three ViewAux ranges in a single recursive lemma made the prover diverge, and forcing exhaleMode(1) on it crashed the prover instead. Each caller only needs part of the contract, so the lemma is split accordingly: ViewAuxSplit keeps the concatenation equation and the preservation of the whole range, which is what SplitByIndex_Bytes consumes, and the new ViewAuxSplitParts provides the equation and the preservation of the two subranges, which is what CombineAtIndex_Bytes consumes. Each proof now contains a single old-state definitional step, the same size at which ViewAuxElems already verifies. The byte-preservation postcondition of ViewElems now also triggers on the current-state GetByte term, so that consumers reach the old value from terms the elementwise characterization creates. InfoField.SerializeTo and HopField.SerializeTo failed with the same missing-trigger shape as SCION.SerializeTo did before: the views taken after ViewElems could not be related to the bytes captured before the fold, because no GetByte term from the pre-call state existed. The same explicit GetByte asserts on both sides of the call provide the anchors, covering the MAC bytes as well in HopField's case. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The last slices error was the step in ViewEqFromElements from the precondition's characterization of `other` (in terms of the old GetByte values) to the current state: the instantiation chain across the lemma call did not go through. The DecodeFromBytes proofs of InfoField and HopField already demonstrate the robust alternative: calling ViewElems with only part of the held fraction keeps a positive fraction of the predicate instance untouched, so its snapshot, and with it every GetByte and View application, is the same term before and after the call, and no old-state reasoning is needed at all. ViewEqFromElements now calls ViewElems with p/2, and the SerializeTo proofs of InfoField and HopField call it with half the write permission. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The GetByte anchors alone made both InfoField.SerializeTo and HopField.SerializeTo verify; switching the ViewElems calls to half of the write permission on top of that made HopField.SerializeTo diverge. Go back to the exact form that verified. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The postcondition relates DecodeFromBytesSpec to the view of raw in the final state, but the body unfolded the full held fraction of Bytes(raw), so the refolded instance's view could not be connected to the captured one. Unfolding only R51 out of the held R50 keeps a positive fraction of the instance untouched, which pins the view, as in SCION.DecodeFromBytes's common-header outline. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The view postcondition of CombineRange_Bytes failed to re-check when imported by the router verification job in every formulation tried: a single old() around the concatenation, old() per View application, and one clause per instance all report that the permission to the first instance under old() might not suffice, while the structurally identical clauses of CombineAtIndex_Bytes and Unslice_Bytes pass in the same job. CombineRange_Bytes therefore no longer relates views at all, and the new CombineRangeWithViews_Bytes carries the relation through ghost parameters instead: the preconditions bind the three piece views in the state before the call, so the postconditions need no old() expressions. Call sites satisfy the bindings trivially by passing the View applications themselves. Call sites whose subsequent proof consumes the view relation are migrated to the new lemma; the remaining sites, including all deferred cleanup calls, only recombine permissions and stay on the view-free lemma. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Raw.ToDecoded captured the serialized meta bytes by unfolding the predicate instances and threaded them through the combines and splits with raw-value asserts, which no longer connect now that MetaHdr.SerializeTo's postcondition speaks about the view of the buffer. The bytes are now captured from that view, and the sliced-view postconditions of the split, reslice and combine lemmas carry them to the instance that Decoded.DecodeFromBytes consumes. Decoded.DecodeFromBytes's postcondition characterizes the meta header through GetByte in the final state, while Base.DecodeFromBytes provides the fact about the view at the beginning; the retained fraction of Bytes(data) pins the view across the decode loops, and a final ViewElems call bridges the view elements to the GetByte terms. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
With the contract-level import failure of the combine lemma gone, the IsSupportedPkt preservation postconditions of the five packet processing functions still failed: IsSupportedPktSubslice reduces IsSupportedPkt to the first CmnHdrLen bytes of the view on each side of the path modification, but nothing related the two prefixes. The view of the buffer up to the path offset is pinned across the modification, since a fraction of that instance is retained throughout; the added asserts capture it and equate the common-header prefixes of the packet view before and after, which closes the chain by congruence. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
HopField.SerializeTo oscillates around the verification timeout: it diverged, passed after the trigger anchors were added, and diverged again after unrelated contract changes shifted the instantiation behavior. The quantified asserts about the MAC bytes multiply the matched triggers over sequence slicing and concatenation terms, so they are replaced by their six ground instances, and the premise of EqualSeqImplyEqualMac is stated per index instead of with a quantifier; its proof already only uses the ground instances, and its other caller has the ground facts available by instantiation. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The unsupported-packet assert after copying the serialized SCMP packet into rawPkt failed because nothing related the view of rawPkt after the full unfold, copy and refold to the view of the serialization buffer. IsSupportedPkt only depends on bytes 4 and 8, so ground GetByte bridges on both sides of the copy connect the two views. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Decoded.DecodeFromBytes characterizes the decoded meta header through GetByte in its final state, while the asserts before the call relate the view elements to the serialized bytes. The retained fraction of the instance pins the view across the call; the added ViewElems call and ground asserts connect the GetByte terms to it, which lets the serialize-deserialize roundtrip lemma conclude that the decoded meta header equals the original one. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The lemma calls in the body establish all ingredients of BytesStoreCurrSeg, but the postcondition check does not find the multi-step chains between them, in particular the composition of the sequence-slicing steps for the future hopfields and the congruence between the two spellings of the suffix of the hopfield bytes. The added asserts state each step explicitly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The previous spelled-out chain re-derived the future hopfields in three equivalent forms and invoked an unneeded widening for the current hopfield, which made the member exceed the verification timeout instead of failing. The definition of segment shows the minimal chain: the future hopfields are the suffix of the base-zero hopFields application, so one drop-of-drop step and the existing prefix, alignment and widening lemmas suffice, with the head equality following from the definitional unrolling alone. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
Both the bare lemma calls and the spelled-out chains made the member exceed the verification timeout: with all the recursive hopFields facts in one context, the proof search grinds. The three independent parts of the chain, the head and the tail of the future hopfields and the past hopfields, are now established by dedicated helper lemmas whose contracts state exactly the subsequence forms BytesStoreCurrSeg mentions, so each proof search stays small and the main lemma only composes their postconditions. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
path/scion completed within 30m while it still had the failing BytesStoreCurrSeg postcondition, but now that the postcondition is discharged the package hits the wall with no per-member error. Raising the timeout tells us whether the proofs are sound but slow or whether a member genuinely diverges. The intent is to bring the budget back to 30m once the sequence/slice annotations are streamlined. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
The previous commit changed only the workflow file and did not create a workflow run, so the 45m path/scion budget was never exercised. This empty commit forces a run to establish whether path/scion is sound-but-slow within 45m. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e
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.
Summary
This PR refactors the packet parsing verification to separate heap access from parsing logic. Instead of requiring
sl.Bytespermissions throughout the parsing chain, parsing functions now operate on mathematicalseq[byte]views obtained from a singleViewfunction. This eliminates the need for numerous permission-plumbing lemmas and makes the code more maintainable.Key Changes
Added
Viewfunction inverification/utils/slices: A new opaque function that abstracts asl.Bytesrange into a mathematicalseq[byte], with elementwise characterization exposed as postconditions. IncludesViewAuxhelper andViewEqFromElementsextensionality lemma.Converted parsing functions to operate on
seq[byte]: Updated functions across multiple files to take sequence views instead of byte slices with permissions:pkg/slayers/path/infofield_spec.gobra:ConsDir,Peer,Timestamp,AbsUinfonow takeseq[byte]of exactly one info fieldpkg/slayers/path/hopfield_spec.gobra:BytesToIO_HFnow takesseq[byte]of exactly one hop fieldpkg/slayers/path/scion/raw_spec.gobra:CurrSeg,LeftSeg,RightSeg,MidSeg,absPkt,RawBytesToMetaHdr,RawBytesToBasenow operate onseq[byte]router/io-spec.gobra:absPktnow takesseq[byte]Eliminated permission-plumbing lemmas: Removed or significantly reduced scaffolding like
OffsetEq,Widen*, andSubslicelemmas that were purely for permission manipulation. Replaced with pure sequence-level lemmas inwiden-lemma.gobrafiles.Updated call sites: Modified all callers to use
sl.View(buffer, 0, len(buffer))when passing buffers to parsing functions, enabling subrange access through pure sequence slicing.Added view-level helper functions: Introduced
InfofieldByteSeqandHopfieldsByteSeqinpkg/slayers/path/scion/info_hop_setter_lemmas.gobraas sequence-based analogues of their slice counterparts.Updated lemmas and specifications: Modified postconditions and preconditions throughout to work with views instead of permissions, including
ValidHeaderOffset,SliceBytesIntoSegments, and various IO specification lemmas.Added documentation: Included comprehensive plan document (
doc/verification/byte-slice-parsing-refactor.md) explaining the rationale and implementation strategy.Notable Implementation Details
Viewfunction uses wildcard permission amounts (_) to work under any fraction, matching the pattern ofseqs.ToSeqByteBytes(s, start, end)is preserved,View(s, start, end)is known to be unchangedv[a:b]), which is definitional, instead of requiring ghost permission operationsEqAbsHeaderandValidPktMetaHdrkeep buffer arguments forMemwhile their contents-reasoning goes through views*WithInfofamily of functions and allowingCurrSegto keep its packet-relative signaturehttps://claude.ai/code/session_01WU4M35n52cXp2gs9RozB8e