The full SyscallInstrsChip, with full semantics - #122
Open
dtumad wants to merge 121 commits into
Open
Conversation
S1 of the syscall-chip plan: definitions only, no ensemble membership, so nothing ripples yet. syscallChannel is SP1's own bus and reuses the existing SyscallMsg, the carrier the exact v6.4.0 lists already project -- so both models now name this bus with one type. Its payload shape came from the extracted send, which corrected my reading of it: values[0] is clk_high, not a shard index. publicValuesChannel is the second native-only bus. SP1 reads public_values at three differently-shaped places; one addressed cell covers all of them without a variant type, and every message is built from columns a row already has, so a chip carrying them keeps its upstream column count. Both are declared without a provider on purpose: balance then forces the syscall id's table byte and the commit selectors to zero, which is how the profile carve-outs become theorems instead of assumptions. Also records the hazard that blocks S4: both names currently fall into kindOf's else .State bucket, which is inert only while they stay out of the ensemble, and would otherwise corrupt the State clock telescope silently. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
S2a: the Inputs struct and the Spec's skeleton plus HALT arm. The 65 fields are laid out in upstream column order, so the faithfulness codec will be a re-grouping rather than a permutation, and inputs_size pins the count by rfl -- which is what checks the column map I read off the oracle's expression graph against the actual ProvableStruct sizes of CPUState, RegisterAccessCols, Word, and the three gadget blocks. ExitCodeValid is the constraint HaltChip omits: SP1 pins a0's upper two limbs and bounds limb 1 against 0x7F00, the second limb of KoalaBear's modulus. It is stated structurally so the contract stays field-generic; that the reduction is therefore below the modulus, and so decodes injectively, needs the field's actual size and belongs where it is used. The four non-HALT arms constrain columns this commit leaves unconstrained. That makes the row weaker than upstream, not unsound, and the anchor is what will show when it is complete. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Reading the row's interaction list rather than only its constraints shows values[13] sits in the Program message's op_a_0 slot -- the x0 flag, which is what E27/E29/E31/E33 use to force a written zero -- not a gate for op_a keeping its value. Also records that t0 is genuinely written: its read-prior carries the syscall id and its read-back carries op_a_value, where a0 and a1 carry the same word on both sides. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
main now covers every one of the 74 scalar asserts and 18 interactions of Extracted/SystemOracle/SyscallInstrs.lean, plus its eight gadget sub-lists, composed through gadgets that already existed natively: the identifier byte split, five IsZeroOperation arm selectors, and two U16CompareOperation valid-field-element bounds. Three things the interaction list settles that the constraints alone did not. t0's memory pair is a write -- read-prior carries the identifier, read-back carries op_a_value -- where a0 and a1 carry the same word both ways. The Program message takes its operands from columns rather than literals, with op_a_0 in the flag slot. And E55 asserts is_real * op_a_0, so a syscall row never targets x0, which makes the x0 zeroing vacuous on real rows though still asserted. The five public-value conjuncts become one message each, built only from columns the row already has, so the width stays 65: the exit binding on exitChannel, the two digests and two commit flags on publicValuesChannel. No padding push on the exit bus. HaltChip has one because its table is exactly one row, which is what balanced the verifier's ungated pull; a syscall table has many, so that accounting is redesigned at ensemble wiring and this row emits only the faithful is_halt-gated push. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
The 65-column row does elaborate, and the cost lands where the plan predicted. localLength_eq's default tactic times out at whnf on a do-block with sixty assertions and eight subcircuits, so the field is supplied explicitly -- the one place a hand-written ElaboratedCircuit field is warranted rather than a missing circuit_norm lemma. Everything else closes from circuit_norm alone, including all sixteen channel-membership goals. Seven buses are declared: Byte arrives through the readers and the three gadget families, State through CPUState, and Program, Memory, Exit, Syscall and PublicValues directly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Re-reading the oracle's interaction list to its end rather than its first eighteen entries turned up six more. Four are SP1's slice_range_check_u16 on op_a_value, and they matter: t0 is written, and on the HINT_LEN arm no constraint determines the written word, so without them the read-back push could not discharge the Memory bus's isU64 requirement. With them it can, and no profile restriction is needed. The other two are the u8-pair checks on the cached digest word, gated on is_commit. Found while working the soundness tail, which is what forced the question of where op_a_value's range comes from. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Assumptions is True: every fact the Spec reports is either asserted by the row or received as a pulled guarantee. Axioms are the standard three. The halt conjunct is the substantive part. ExitCodeValid is a disjunction because SP1's bound is one -- the compare gadget decides whether a0's limb 1 is below 0x7F00, and where it is not, the two conditionals force limb 1 to equal the bound and limb 0 to vanish. Both branches keep the word's reduction under the modulus, which is what makes the committed exit code decodable. Two things the requirements tail forced. op_a_value's isU64 comes from the four byte range pulls, read out through byteRowSpec_range -- the reason those interactions had to be found first. And next_pc's Spec conjunct is now three component equations rather than a Vector equality, which avoids an extensionality detour and is what consumers want anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
RowContract is the completeness precondition and the row's arm-by-arm contract: gates, reader blocks, arm selection, and one predicate per arm family, plus the facts the Program and Memory pulls carry. Spec stays the narrower soundness conclusion, and rowContract_toSpec records that the one follows from the other -- Clean keeps those two fields apart precisely because completeness must reconstruct constraints no consumer reads. Every arm SP1 dispatches inline has a conjunct here, so a missing arm is a missing conjunct rather than a silent gap. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
SP1 has two syscall types and I picked the wrong name. SyscallChip (syscall/chip.rs) is named SyscallCore or SyscallPrecompile and is the handler table on the far side of the syscall bus -- the one the supported profile excludes, and whose absence is what makes the unprovisioned channel force the carve-out. SyscallInstrsChip (syscall/instructions/) is the ECALL instruction row we actually model, named SyscallInstrs. So SP1Clean.SyscallChip named our row after the table it deliberately does not model. Renamed throughout, and the module docstring now records the distinction so it does not come back. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
All 106 completeness obligations discharged, axiom-clean. RowContract gains the facts a prover must actually supply -- the selector sums, the one-hot sums, and the Program and Memory pulls' well-formedness. Two things cost me time and are worth recording. Ordered bullets, not first-chains: a chain costs goals times alternatives elaborations and blew the heartbeat budget, while positional bullets cost one each. And linear_combination is syntactic on atoms, so a Fin-indexed value and its Nat-indexed twin are different atoms even when defeq -- sub_eq_zero_of_eq or a norm_num pass bridges them where ring cannot. The five booleanity gates are reordered so is_commit and is_commit_deferred sit at positions 2 and 3; the anchor compares lists up to permutation, so ordering is free here and shallower projections are worth having. The bundled circuit is not assembled: requirementsChannelsLawful needs a constraint past the first, and reaching one means normalising the whole sixty-assertion do-block. The file records the structural fix. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
The first of the row's arms to become its own FormalAssertion, establishing the pattern: Inputs and Spec beside the chip's contract, main and elaborated in Native/.../Arms.lean, soundness and completeness in Proofs/.../Arms.lean. The point is that each proof sees only its own arm's constraints. PcArm's soundness and completeness are a dozen lines each and elaborate without strain, where the same six constraints inside the flat row could only be reached by normalising sixty. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Twenty-three of the row's sixty-one inline constraints -- the one-hot digest bitmap, its index rule, the two sum rules, and a1's packing -- now sit behind one FormalAssertion with a six-conjunct Spec. Both directions went through without strain, which is the evidence the decomposition is doing its job: the same twenty-three constraints inside the flat row could not be reached at all without normalising the whole block. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Thirteen more constraints behind one FormalAssertion: the x0 rule, the ENTER_UNCONSTRAINED zeroing, and the rule that every other arm leaves t0 alone. HINT_LEN is the gap the Spec names explicitly -- no arm determines the written word there, which is why SP1 range-checks it separately. Three of six arms extracted; 42 of the row's 61 inline constraints now sit behind bundles. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
The last two of the five. FieldBoundArm is the one worth having twice: the same valid-field-element check bounds a0 for HALT and a1 for COMMIT_DEFERRED_PROOFS, so it is parameterised by word, bit and gate rather than written out at both sites. All five bundles are axiom-clean, and 61 of the row's inline constraints are now behind six proof boundaries instead of one flat block. Two shapes that cost me time and are worth knowing. A FormalAssertion's soundness goal is Spec paired with the composed sub-assertion's requirement disjunct, not Spec alone -- the pair is refine ⟨⟨...⟩, Or.inl rfl⟩, and guessing at it produces type errors that look like projection failures. And a hypothesis stated over a reconstructed record needs its projections reduced before rw will match, though exact still accepts it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
main now composes WriteArm, PcArm, DispatchArm, FieldBoundArm twice, and CommitArm instead of carrying their sixty-odd assertions inline, and the chip's Spec is assembled from the arm Specs rather than restating them -- so the row and its decomposition cannot drift. Chip soundness is closed and axiom-clean, and it is now mostly forwarding: supply each arm its Assumptions, get its Spec back. What it still does for itself is the part that genuinely belongs to the row -- deriving that two selectors cannot both fire, since one identifier cannot equal two codes, which is what gives CommitArm and WriteArm their mutual-exclusion premises. One honest consequence is recorded in the Spec: op_a_0's booleanity reaches the row over the Program bus, which is gated, while SP1 asserts the x0 rule ungated. So the write arm's meaning is reported under exactly that hypothesis rather than pretended unconditional. Completeness and the bundled circuit are next; the arms make both tractable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Chip completeness is closed and axiom-clean. Before the arms were extracted it could not be finished at all -- the closers blew the heartbeat budget -- so the decomposition did the work it was meant to. Most of it is now forwarding: RowContract carries each arm's Assumptions and Spec, and the chip hands them straight over. What it still does itself is the row's own business -- the pull guarantees, the byte range checks, and the IsZero selector semantics. Two contract corrections the proof forced. The written t0 word's isU64 is a chip-level prover fact, not a WriteArm one: the byte pulls that establish it stayed on the row when the arm was split out, and on the HINT_LEN arm nothing else determines that word. And the two U16Compare Specs left SelectorsValid, since FieldBoundArm now owns them. The bundled circuit is still blocked, on requirementsChannelsLawful alone. The file records what was tried and what to try next. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
The blocker was never the size of main. RequirementsChannelsLawful asks a structural question -- which channels do these operations touch -- and I was answering it with circuit_norm, which normalises constraint content and so unfolds every composed circuit's semantics. Measured: the structural simp set does the same first component in 2 seconds against a heartbeat timeout. DivRemChip is the worked precedent and the reason the largest chip in the repo bundles where this one did not: it rewrites with Clean's monadic-append and per-leaf rfl-lemmas and never mentions circuit_norm. The lever is shallowInteractions_subcircuit -- a composed subcircuit contributes nothing shallow -- so the arms, readers and gadgets drop out for free. subcircuitRequirements_eq lands the first component. The second goes through the same way. The third has two open cases of twenty-two, where off_gate_vacuous does not match after the targeted eval rewrite; the file records that as the remaining gap. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
The row's three obligations were already proved; what stood between them and the bundle was `RequirementsChannelsLawful`, whose three components are questions about the block's *metadata*, not its meaning. Answering them through `circuit_norm` normalises all seventy-four constraints to decide which channels a list mentions, and exceeds the elaboration budget doing so. Answering them through the monadic-append and per-leaf `rfl`-lemmas takes two seconds. `DivRemChip` uses the same shape. The twenty-two shallow interactions then split two ways: those on a channel the row guarantees, and the gated pulls whose off-gate `Requirements` is vacuous. The latter arrive in a form `off_gate_vacuous` does not take — Clean states *both* hypotheses about the interaction's own multiplicity, so a pull hands over `-x ≠ -1` and `-x ≠ 0`, not the mixed pair. `off_gate_vacuous_neg` is that form, and saves a rewrite at each of the two dozen call sites on a row this wide. `circuit` is axiom-clean: [propext, Classical.choice, Quot.sound]. This completes S2. The chip is not yet in the ensemble and has no faithfulness anchor — S3 and S4 — so the HaltChip disclosures in the audit and report stand unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
One added line: the chip's `circuit` at [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
921 main / 998 released. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
S3's foundation. The sixty-five-cell codec between the native `Inputs` row and the extracted flat vector, both round-trips, the oracle, the physical row, and the structural split of the row's complete `assertZero` list into thirteen shallow gates plus sixteen composed blocks. Two things are worth recording, because both cost time: The cell correspondence is handled once, not sixty-five times. `syscallInstrsReconfigure_eval` says reconfiguring an evaluated row is evaluating it cell by cell, so every later statement is phrased over `syscallInstrsRustColumns` and the Rust oracle's `cols.values[k]` accesses reduce definitionally to native expressions. The alternative — a sixty-five conjunct field-equation lemma, as `MemoryBumpChip` uses for fifteen — does not scale to this width. `circuit_norm` cannot prove the decomposition: it normalises the content of seventy-odd constraints to answer a question about their arrangement, and exceeds the elaboration budget doing so. The structural `Operations.constraints_*` lemmas answer it in five seconds. The subtlety is that the generic `Circuit.bind_def` walk descends into the sub-`main`s too, so the blocks are stated through `X.circuit.main` — folded — rather than `X.main`. That in turn needs each subcircuit's `localLength` to reduce, which is why `U16toU8OperationSafe` gains the `circuit_localLength` rfl-lemma every other operation already had. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
One lemma per composed circuit, each over an opaque input of that circuit's own row type. That is the whole trick: `circuit_norm` applied to the sixty-five column row at once times out, applied to one arm at a time it is instant. The five arms, the byte split, and the two reader families are now each pinned to an explicit evaluated list. Three of the blocks assert only their own `is_real` gate — the byte split, `CPUState`, and `RegisterAccessCols`. With the chip's own gate and the two remaining reader instances that is six copies, which is exactly how many times SP1's dump repeats `values[64] * (values[64] - 1)`. The correspondence is exact, not absorbed. `FieldBoundArm` is the one block with a subcircuit of its own; its `U16Compare` fragment folds to the extracted Rust list through the shared `u16compare_assertions_exact`. The bridge has to be stated at `circuit.main` rather than `main` — they are defeq, but simp matches syntactically. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
SP1's whole-table assertion list holds exactly when the native row's complete `assertZero` list does, together with the eight public-value conjuncts. The two sides are the same eighty-one propositions and the correspondence is a bijection, checked as one: seven composed sub-operation blocks matching block for block, sixty-six scalars matching one for one, and the eight of `PublicValueBinding`. Nothing is absorbed and nothing is dropped — in particular the six copies of the `is_real` boolean gate SP1's dump emits are matched by six distinct native sources (the chip's own gate, the byte split, `CPUState`, and the three register readers), not collapsed by `and_self`. Only two conjuncts are not a direct match, and they are the interesting ones. SP1 compares the *selected public-value digest* against `a1`; the native row compares its *cached* `digest_word`. The two are interderivable from the digest-byte bindings without dividing by the commit selector, so each direction is one `linear_combination` — no case split on whether the row is a commit. The KoalaBear literals stay confined to `PublicValueBinding`: the native half of the anchor is field-generic and literal-free, which is the shape external report Finding 7 asks for. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
…call key The interaction counterpart of the assertion decomposition, proved the same structural way: the row's complete emitted interaction list split into its sixteen composed blocks and its own three groups. The syscall channel is renamed to SP1's own projection key. `Interaction.toAccess` sends the generated `.raw .syscall` send to `"SP1Raw/syscall"`; with the native channel named anything else the two project to different `LookupAccess` keys, and those keys are exactly what a whole-chip anchor compares. Both sides now also share the `kindOf` fallback classification, which is the same landmine on both sides rather than a divergence — and is fixed for both at once when `InteractionKind` gains a `Syscall` constructor. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Every composed block's emitted interactions, each over an opaque input of its own row type. Four of the sixteen emit nothing — `IsZeroOperation` and three of the five arms are pure `assertZero` blocks — and `FieldBoundArm`'s traffic is entirely its `U16Compare` fragment's. One thing worth recording: `Gadgets.Equality.circuit` is a `FormalAssertion`, not a `FormalCircuit`. Reaching for `FormalCircuit.toSubcircuit_interactions` leaves the subcircuit unfolded with no error message that says why, and the shape it leaves behind looks like a missing `rfl` rather than a wrong lemma. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Stage 1 sub-stage 7. `memoryBalance_of_alignsWith` carries the
`SyscallInstrs` table's produced and consumed Memory messages as a side term
on both sides, exactly as it carries the Halt table's. That is the right
shape for a table whose rows are extracted *after* the walk. It is the wrong
shape for a table whose rows are *walked*: the walk already accounts for a
row's touches through `pushesAt`/`pullsAt`, so carrying them beside it would
double-count.
`syscall_{pushesAt,pullsAt}_eq` are the absorption — the side term *is* the
walked term, so the summand can be dropped from the balance's conclusion
rather than tracked. `memoryFrontierBalance` keeps its syscall summand; it is
the raw ledger form and correct there.
Two supporting pieces. `pushesAt_map_eq_filter_flatMap` and its pulled twin
bridge the walk's per-row view to the ledger's flat view — that identity is
what makes absorption expressible at all. And `syscallRows_{pushesAt,pullsAt}`
state it over *abstract* rows: done directly at the witness's concrete
65-column decode, the same rewrite exceeds the depth budget, which is the
crossing rule biting for the third time this campaign.
`lake build SP1Clean`: 0 errors, 0 warnings.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Sub-stage 7's payoff. `memoryBalance_of_alignsWith` carries four summands beside the instruction rows' touches; `walkedMemoryBalance` restates it over the combined instruction+syscall carrier with the syscall one **gone**, because those rows are now walked rather than extracted beside the walk. `splitPerm` is the only new obligation, and it is the honest statement of what "the trail is an arbitrary interleaving" means: the walked carrier's facts are, up to order, the instruction rows' aligned facts together with the syscall rows' facts. `pushesAt`/`pullsAt` are multiset sums, so the interleaving itself never has to be reconstructed — `pushesAt_perm` plus the new `pushesAt_append` do the whole job. One correction landed with it: `WalkedRow.facts` now takes the instruction carrier as a parameter instead of fixing `ordinaryRowFacts`. The engine does not walk the ordinary carrier — it walks the *aligned* one, related to the ordinary form by `AlignsWith` — so the fixed version produced a carrier the engine could not actually be fed. Also noted: `pushesAt_perm`/`pullsAt_perm` already existed in `ChipContracts`. I wrote copies in `TimedGrounding` before finding them and removed the duplicates; only the genuinely new `_append` pair stays. `lake build SP1Clean`: 0 errors, 0 warnings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
The last structural blocker on the engine's conclusion. The plan's Stage 4 treats the shift off `SailChain done.length` as a headline-relation change; in the engine it is narrower than that, and the reason is worth recording: `DynamicGroundedRow` never mentioned a chain. Only the quantifier in front of it did. `dynamicGrounded_of_weakCurrency` takes a `SailChain steps initial state` and spends it in exactly three places — `valueOperandsBound_of_pullCurrency`, `sourceAValueBound_of_pullCurrency`, `memoryPullsBound_of_pullCurrency` — all of which go through `localValueAt_stepStart_iff` and nothing else. That is the same single appeal `RowWiring.advance_at` made. Swapping it for `localValueAtG_stepStart_iff` gives `dynamicGroundedG_of_weakCurrency`, whose two Sail-shaped hypotheses become `traj n = some state` and `tl.start n` — precisely the two places a 264-tick row made the old form unusable. Both libraries build clean: 0 errors, 0 warnings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
The call-site edit's first half. `listAllInl` is today's projection and it is exactly what `SyscallTableInactive.noActiveRows` exists to make available: with no syscall rows every trail entry is a `Sum.inl`, so the trail *is* a list of decoded instruction rows and the engine can walk it. `listAllWalked` is its successor. It asks only that no **halt** row is present — which the halt-free branch already establishes from `realHaltRows witness = []` — and produces a `WalkedRow` list in the same order, carrying a syscall row through the projection rather than excluding it. Its result is a `List.Forall₂`, not a `List.map`, and that is forced: the two row types are related by a *relation* — the syscall arm decodes a raw array — so there is no function into `WalkedRow` to map with. `Walk.isWalk_forall₂` is the matching transport, and it is why `isWalk_map` could not be reused. `walkedRow_pullAt` also takes its walk edge as a parameter now. The trail is extracted over the *canonicalized* State messages while a row's facts carry the raw ones, so the two differ by `canonState`; `timeAgree` is the bridge, and at the call site it is `timeNat_canonState` — a rewriting, not a new obligation. `lake build SP1Clean`: 0 errors, 0 warnings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`SyscallRowContext` names the five things a syscall row's meaning needs that the row does not carry. `operands` came off the Program bus earlier; the three semantic fields now come off the walk, leaving `pcCarry` as the only premise — and that one is `StateBumpChip`'s carry fact, genuinely external, exactly as the pc's `+ 4` is on the AIR side. The content worth recording is why the three register reads may speak about the *same* state. Their read times are `+0`, `+3` and `+2`, all below `regEffectOffset = 4`, so every one is still in the pre-write half of the row's window and `localValueAtG_regRead_of_traj` sends all three to `traj n`. That lemma is the generalization of `localValueAtG_stepStart_iff` off the exact window start, and it is what the `+3`/`+2` operand reads need. `ecall` then follows from `pcValue` plus the committed `ECALL` fetch — the second use of `witness_syscallRow_ecallTruth`, after the operand indices. Two hoists, both the same rule as before: `SyscallRowContext.of_pieces` assembles over an abstract row, and the `pcBits`-to-event-`pc` coercion moved inside it. Done at the concrete 65-column row, that coercion alone exceeds the depth budget — the documented "`have h : <row spelling> := <slice spelling>` is a defeq coercion that blows up" landmine, hit head-on. `lake build SP1Clean`: 0 errors, 0 warnings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`CoreProfile.CanonicalSyscallCodes` is the disclosed premise the plan's D9 calls for, carried the way `WithinOrdinaryRowLimit` is: one predicate, with both directions projecting into it rather than owning separate spellings. It has to be a premise, and the reason is worth stating where a reader will find it. SP1's AIR reads bytes 0 and 1 of `x5`; its executor dispatches on the full `x5 as u32` through `SyscallCode::from_u32`, which *panics* on a non-enumerated value. So an AIR-valid `HALT` row may carry `x5 = 0x00010000` — a witness the constraint system admits and no execution produces. Canonicity is a fact about the executor, not a consequence of the AIR, so the honest home for it is the profile rather than an invented row constraint that would make the native chip stricter than the one it models. Three pieces: the predicate itself; `EventSegmentWitness.syscallEvents` with `canonicalSyscallCodes_iff`, which proves the segment-level condition *is* the profile's read at the transcript's syscall events; and `syscallEventsOf` with `isInlineCanonical_of_profile` on the native side, which is the form `syscallStepFact_of_advance` consumes. This is what makes `SyscallTableInactive.noActiveRows` removable rather than merely unwanted: with no active syscall rows the condition is vacuous, and with them it is a genuine obligation that had nowhere to live. `lake build SP1Clean`: 0 errors, 0 warnings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
A0 of the syscall closing plan. Four `FormalModel/SupportedShard.lean`
definitions rejected a mixed shard *before* any grounding ran, so emitting
per-row syscall events bought nothing until this landed:
- `executionValid` demanded `execution.AllOrdinary`;
- `SupportedSP1Transition` begins with `event = .ordinary`, and
`AllTransitionsSupported` demanded it of every transition;
- `SupportedHaltingTrace` demanded a dropLast-all-ordinary prefix, so a
*mid-shard* syscall falsified the halting arm too;
- `WithinOrdinaryRowLimit execution.steps` charged syscall steps against the
ordinary instruction-row budget.
The per-transition obligations are now arm-split: `SupportedSP1Transition` is
demanded of `.ordinary` transitions only. A syscall transition's meaning does
not come from the instruction-routing profile at all -- it travels in
`Machine.EventStep.syscall`'s own `SyscallTransition`, already authenticated by
`CoreShardCase`'s trace validity. The model layer needed no change: `Clocked`
already dispatches on `ExecutionEvent.StartsAt` and `finalClock` is already a
duration prefix sum.
Two findings worth recording.
`AllOrdinary` was doing two jobs, and only one of them was a profile
restriction. It was also the **branch discriminator**: `halted_facts` reached
the `.halted` case by refuting the execution branch with `exec.1`. Dropping it
naively would not merely lose a proof -- it would make that theorem's claim
false, since a mixed non-halting shard is `¬ AllOrdinary` and yet squarely in
the execution branch. New `EventExecutionTrace.HaltFree` says what the
execution branch actually means (no transition is a canonical HALT); it is
implied by `AllOrdinary` and refutes `HaltsWith` through `List.mem_of_getLast?`,
so the branches stay disjoint. `halted_facts` now takes `¬ HaltFree`.
The row budget charges ordinary transitions only, via new
`Machine.ordinaryTransitionCount` / `EventExecutionTrace.ordinarySteps`. That
is what the native side already supplied -- `realDecodedInstructionRows` is an
instruction-row count that never included syscall rows -- so the two sides' row
counts stay matched instead of the semantic side over-charging.
`mem_transitions_of_mem_locatedTransitions` and
`AllTransitionsSupported.all_of_allOrdinary` keep every syscall-free consumer
unchanged; `haltedExecution_of_haltGrounding` keeps publishing the stronger
un-split prefix obligation its callers want.
`lake build SP1Clean` 3801 jobs and `lake test` 3816 jobs, both at 0 errors /
0 warnings / no stray `info:`; layering and root-index gates pass.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
A1 of the syscall closing plan. `RowsGrounded.dynamic` indexed its position by `SailChain done.length initial state`; it now indexes by `traj done.length = some state`. `DynamicGroundedRow` never mentioned a chain -- only the quantifier in front of it did -- which is the same shape that made the walk's own parameterization a rename, and `sailTrajectory_eq_some_iff` is already proved in both directions, so today's meaning is recovered verbatim at `Semantics.sailTrajectory initial`. The generalization buys a position index a 264-tick syscall row can also occupy. Note that a row's *duration* never enters here: the index counts steps, and `eventTrajectory` is step-indexed too, so a syscall row sits at index `k` exactly like an instruction row. Duration is a clock-axis concern and stays out of this structure entirely. Four adapter lines outside the definition: two `.mpr` at `grounded.at` in `LocalExecution`, two `.mp` at the `SupportedCoreGrounding` / `SupportedCoreHaltGrounding` construction sites. The engine itself still states its position as a `SailChain`; it moves to the trajectory index later. Also `pcEdgeOf` and `pcWalk_iff_isWalk`, purely additive. `PcWalk` is a redundant copy of `Walk.IsWalk` -- identical nil (`a = b`) and cons (`(edge x).1 = a`) shapes -- so the bridge holds by `Iff.rfl` at every position. Stating it as a lemma rather than redefining `PcWalk` inherits `isWalk_append` (the halt branch is literally a `prefix ++ [one row]` walk), `isWalk_map` and `isWalk_forall₂` while leaving all six call sites untouched, and it is the generalization a syscall row needs: a row with no `ChipRow` still has a pc edge. Acceptance: no pre-existing consumer changed. `AIR`, `HaltExecution`, `BootHalt` and the completeness stack all compile as they stood. `lake build SP1Clean` 3801 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
A2 of the syscall closing plan. Reading the sites changed this step's shape: an ordinary chip row genuinely advances eight ticks, so `eventExecution_of_groundedRows` and `sailRetireChain_of_groundedRows` are the *ordinary* engine and keep their `8 *` correctly. What was owed is the duration-summed form of each building block, with the `8 *` form re-derived from it -- the same generalize-and-recover discipline as A1. Most `8 *` occurrences were never targets: `FormalModel/EventExecution.lean`'s are docstring prose, and `Model/Semantics/Truth.lean`'s are the Sail-specific `microValue`/`LocalValueAt` that `GenericTruth` already supersedes. `statePullAlign8_of_durations` was a `True`-valued stub. It asserted nothing while its docstring called it the easiest and most necessary of the engine's three duration generalizations -- a statement that looks load-bearing and is not. It is now real, in `GenericWalk.lean` beside the two lemmas its proof consumes (`statePullTime_of_stateWalk_durations` and `List.dvd_sum`), and `statePullAlign8_of_stateWalk` is re-derived from it at `duration := fun _ => 8`. That makes all three generalizations real, where `clockCount_of_stateWalk` and `statePullTime_of_stateWalk` were already thin delegating wrappers. Its `8 ∣ duration` premise is what a 264-tick row discharges through `eight_dvd_durationAt`, so alignment survives a mixed timeline. New `transitions_finalClock`: the event clock is the prefix sum of the transition list's own durations, with no ordinary hypothesis -- plain `clockAfterEvents` telescoping. `ordinaryTransitions_finalClock` is now that composed with `ordinaryTransitions_durationSum`. `ordinaryTransitions_clocked` is deliberately *not* generalized: `EventTransitionsClocked` is already the per-position statement, and a syscall event's `StartsAt` is derivable only from the row's `Spec` limb bounds plus `2 ^ 24 < p`, which a row-generic engine does not have. The mixed engine will supply it per row. `lake build SP1Clean` 3801 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
A3a of the syscall closing plan. The eight-tick engine *constructed* its own position index with `chain.snoc`. A mixed walk cannot: a syscall step is not a `SailStep`, so nothing lets the engine extend the trajectory itself. The new `executeWalkEventsAux` **consumes** its index instead -- each row's own advance obligation hands back `traj (k + 1)` -- and stays generic in the row type, because `Soundness/LocalExecution.lean` sits below the entire syscall campaign in the import order and so cannot mention a mixed row type. `WalkAdvancesAt` is that per-position obligation: the row's own semantic step, the trajectory's next value, the outgoing pc / ROM / configuration facts, and -- on the ordinary arm only -- the instruction-routing obligation. The arm split lives in the caller rather than the engine, because `RowsGrounded` still cannot hold a syscall row: `DynamicGroundedRow` is `chipSpec + advanceReady + ValueOperandsBound`, all `ChipRow`-shaped. The routing obligation is guarded by `eventOf row = .ordinary` because `SupportedSP1Transition` begins with exactly that conjunct; a syscall transition's meaning travels in `EventStep.syscall`. The engine reports its trace's events as `suffix.map eventOf` rather than as a step count. That one equation carries the length, the per-row durations -- so the clock is a prefix sum -- and `AllOrdinary` when every row is ordinary, where the eight-tick engine stated all three separately. It is what lets `eventExecution_of_groundedRows` be recovered at `eventOf := fun _ => .ordinary` with its signature byte-identical, so `AIR` and `HaltExecution` are untouched. The eight-tick `executePcWalkEventsAux` is deleted; it is now that recovery. `executePcWalkAux` and `sailRetireChain_of_groundedRows` stay as they were -- they build a `SailRetireChain`, which is ordinary-only by construction. `lake build SP1Clean` 3801 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Groundwork for the mixed-row instantiation of the row-generic engine. `LocalStepFactG` deliberately forgets *which* transition produced the trajectory's successor: `LocalStateTruthG` says only that the trajectory reaches the next state, which is all the truth layer needs. An execution engine that consumes a trajectory needs the `EventStep` itself. The first instinct -- refactor `ordinaryStepFactG_of_advance` and `syscallStepFact_of_advance` to also return the step -- is unnecessary. The trajectory already remembers: `eventTrajectory_succ` evaluates `executeEvent?` at the transcript's own event. So `sailStep_of_eventTrajectory_ordinary` recovers the step at an ordinary position from the trajectory alone, and neither of those two large proofs is touched. Only the ordinary arm needs a lemma. On the syscall arm the `EventStep` is its constructor applied to the row's own payload: `SyscallTransition`'s third component is `handler.run … = some target`, which is definitionally `ExecutableSyscallHandler.relation`, and the trajectory's successor is that same `run`. Underneath it, `sailStep_of_stepOnce` -- the converse of the long-standing `stepOnce_of_sailStep`. `stepOnce` succeeds only by `try_step` running to an `ok`, which is exactly what `SailStep` asserts, so the totalized and relational presentations are interchangeable. The forward direction alone sufficed while the engine *built* its trajectory. `lake build SP1Clean` 3801 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
New `Soundness/SyscallExecution.lean`: the instantiation of the row-generic engine at `WalkedRow`. It lives in its own module because `Soundness/LocalExecution.lean` -- which holds the engine -- sits below this whole campaign in the import order and cannot mention `WalkedRow`. `walkedPcEdge` reads a row's pc edge off its `RowFacts` rather than off a `ChipRow`, which is what lets a syscall row take part at all: it has no `ChipRow`, but it supplies the same two State messages through `syscallRowFacts`. `walkAdvancesAt_of_walk` joins three things, each already proved elsewhere. `GroundedG` supplies the memory-currency antecedent `LocalStepFactG` demands; `LocalStepFactG` then supplies the pushed state truth, which *is* the trajectory's successor together with its pc, ROM and configuration; and `walkedRow_timeStep` with `start_injective` identify **which** index that successor sits at. That last step is the whole content of the campaign's top-ranked risk. The engine counts list positions and the transcript counts timeline positions, and this is the single boundary where they are made the same number -- so a mismatch fails here, at its cause, rather than deep inside a later clock obligation. `start_injective` loses its `private`: it was scoped that way only to avoid a rebuild below `MicroTime.lean` during the sketch phase, and now has a real consumer outside its file. The row's own `EventStep` is deliberately a hypothesis, not a derivation. `LocalStepFactG` forgets it, and recovering it is arm-split: an ordinary row needs `¬ AboutToExecuteEcall`, a syscall row the opposite plus its own `SyscallTransition`. The caller discharges it per arm. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`; check_layering PASS (591 modules), check_root_index PASS (588 modules). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`walkedExecution_of_advances` runs the row-generic engine at `WalkedRow`. The engine reports its events as `rows.map WalkedRow.event`, which is definitionally `transcriptOf data rows` -- `transcriptOf_eq_map` is `rfl` -- so this produces the very transcript the syscall layer is already stated over rather than a parallel one that would then have to be proved equal to it. Same discipline as `walkAdvancesAt_of_walk`, one level up: make the two spellings one term by construction instead of reconciling them afterwards. `walkedExecution_finalClock` is where the 264-tick row is actually paid for. `transitions_finalClock` sums the trace's own event durations with no ordinary hypothesis, and the new pointwise `WalkedRow.duration_event` turns each event duration back into the row width the walk was stated with. Nothing here knows that 8 is a special number. `walkExecution_of_advances` exposes the engine publicly, specialized from the suffix-indexed auxiliary to the whole row list; `eventExecution_of_groundedRows` now goes through it too, so the ordinary and mixed paths share one entry point. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`eventTransitionsClocked_of_starts` states the schedule obligation index-wise: every event must start at the prefix sum of the durations before it. Stating it that way is what lets a mixed trace establish `Clocked` with no all-ordinary hypothesis, where `ordinaryTransitions_clocked` needed one. `walkedExecution_clocked` applies it to the walked carrier. The obligation is arm-split by construction and cannot be otherwise: an instruction row owes nothing, because an ordinary event's `StartsAt` is `True`; a syscall row owes `event.clock =` its own prefix sum, which `syscallEvent_startsAt` derives from the row's `Spec` limb bounds and `2 ^ 24 < p`. That is exactly the fact a row-generic engine cannot produce, which is why it enters as a hypothesis rather than a conclusion -- the same reason `ordinaryTransitions_clocked` was left alone rather than generalized. `walkedExecution_durations` is factored out of the final-clock proof so the clock and the schedule share one statement of "the trace's per-transition widths are the walk's own row widths". `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
The last mechanical piece of the mixed-row instantiation. `stepOf_of_arms` turns each walked row into the `EventStep` the engine asks for, and the two arms genuinely need different things -- which is why no generic argument could have covered both. An ordinary row needs `¬ AboutToExecuteEcall`, which comes from its own routing evidence rather than from the trajectory, plus a determinism step: its `advance` picks some target, the trajectory picks some target, and `stepOnce` being a function identifies them. A syscall row needs the *opposite* ecall fact, from `SyscallRowContext`, plus its payload's `SyscallTransition`; there determinism is free, because `ExecutableSyscallHandler.relation` is definitionally `run = some` and the trajectory's successor is that same `run`. New `handlerRun_of_eventTrajectory_syscall` reads it out, and needs no analogue of `sailStep_of_stepOnce` for exactly that reason. The instruction arm's premise is stated as "this row advances and routes" rather than as a `GroundedRow`, so this lemma stays clear of the wiring and carrier layers; the caller supplies it from `GroundedRow.advance` and `GroundedRow.supportedSP1Transition`. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`walkedRow_widthAt` is the first of `walkE`'s five per-row inputs proved from the ensemble over the mixed carrier, and the first place the two arms' genuinely different clock contracts appear as one statement: `+8` for an instruction row against `+264` for a syscall row. Both were already proved (`witness_realDecodedInstructionRows_timeStep`, `witness_realSyscallInstrsRows_timeStep`); what is new is presenting them under one index. The aligned carrier costs nothing here: `AlignsWith` fixes both State messages on the nose and reorders only the memory lists. One landmine paid for and recorded inline: the syscall arm must *rewrite* with `syscallRowFacts_statePush`/`_statePull` rather than let `exact` reach the messages by defeq. `syscallInstrsRow` unfolds into the table's element construction, and crossing that at a witness row exceeds the depth budget -- `whnf` timeout, no heartbeat setting would have helped, and the fix is the campaign's standing crossing rule rather than a bigger budget. With the rewrite the file elaborates in 2.9s. The witness-level obligations live in their own section: they need `2 ^ 24 < p` for the syscall row's clock recombination, while the engine plumbing above is content with `2 ^ 17`, and a file-wide bump would have handed the plumbing a hypothesis it does not use. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`syscallRowOKCore_of_witness` gathers nine of `syscallRowOKCore`'s ten premises from facts already proved elsewhere: `is_real` from table membership, `Spec` through the currency break, the two clock-byte bounds from the composed `CPUState` reader, the three operand indices from the committed `ECALL` Program row, and the `+264` step. The tenth stays a hypothesis, and the reason is worth naming rather than working around: `align8` relates the row's pull to the **shard's** initial clock, which no single row can see. Only the walk establishes it, inductively, so no quantity of witness facts would discharge it here. `syscallInstrsRow_cpuState_bounds` loses its `private` -- the same "private only until a real consumer lands outside the file" situation as `start_injective`. Its halt-row twin stays private, since its only consumer is still in-file. The proof needed the depth-blow-up remedy, and this instance is worth recording because it bisects to nothing: the statement alone elaborates in 2s, every premise derivation alone is fine, and applying `syscallRowOKCore` at an abstract row is fine -- yet the combination times out, and clearing the context does not help because the cost is not in the context. `set_option diagnostics true` names it directly: 372k `Vector.mapRange` unfoldings driven by `[def_eq] sp1Ensemble`, i.e. `whnf` normalizing the table's element construction because a derived premise and the lemma's expectation of it differ just enough. Interposing an opaque variable -- `generalize <row> = r at <premises> ⊢` -- brings it back to ~2s. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`syscallStepFact_of_witness` and `syscallFrameFact_of_witness` gather the witness-derivable premises of their `_of_advance` counterparts: `is_real`, `Spec` through the currency break, `SelectorsValid`, `PulledFacts`, D9's canonicity, the clock-byte bounds, `op_a`'s `isU64`, the `x5` index, and the `+264` step. The frame twin needs neither the clock bounds nor the `isU64`, because a frame claim never touches the written value. Three premises remain on each, and they are the same three every time: the handler's own semantics (`payload`), the fact that this row's window is the transcript slot carrying *this* row's event (`positioned` -- about the walk order, not the row), and `rowContext`, which needs the trajectory's state at the row's index plus `StateBumpChip`'s pc-carry. That mirrors `align8` in the row contract: the irreducible premises are consistently the ones reaching outside a single row, which is a good sign the decomposition is cutting where the semantics actually joins. Both proofs interpose the opaque row variable prophylactically, now that the failure mode is known. Also `SyscallInstrsChip.Spec.selectorsValid`, a named projection for `Spec`'s twelfth conjunct. Consumers were reaching it through an eleven-deep chain of `.2`s that silently re-points to a different conjunct the moment anyone inserts one -- and `SelectorsValid` is exactly the conjunct every per-arm semantic theorem turns on, so a silent re-point would fail quietly. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`RowWiring.readTime` pins every pull to the row's window start, so it holds at the **ordinary** carrier and not at the aligned one. That is why an instruction row's step and frame facts are proved at the ordinary carrier and then transported -- and why the mixed walk cannot consume them without the trajectory-indexed form of that transport. Four lemmas, each the `G` twin of an existing Sail one: `localStateTruthG_congr`, `ordinaryPullCurrencyG_of_valueAligned`, `localStepFactG_valueAligned_of_ordinary` and `frameFactG_valueAligned_of_ordinary`. They are near-verbatim ports, which is the same result D10 reported for the walk itself: the reasoning was already trajectory-agnostic and only the types said otherwise. The one real difference is that the Sail shift-window lemma derives its window from the state truth, while `localValueAtG_shift_window` is indexed by an explicit step -- so the port has to name the index the pulled state truth already carries. With these in place an instruction row and a syscall row can reach the mixed walk at the same carrier, which is what `walkE` requires. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`engineFactsG_of_kind` and `ChipGroundingContracts.engineFactsG` are the trajectory-indexed twins of `engineFacts_of_kind` and `ChipGroundingContracts.engineFacts`. With them the instruction arm reaches `LocalStepFactG`/`FrameFactG` from the 25 chips' existing contract bundle, which is what the mixed walk needs from an ordinary row. The bundle's three currency-conditional producers -- `wiring`, `chipSpec`, `readiness` -- are reused verbatim. None of them inspects the index, so the D0 circularity break carries over untouched: the row's open Memory inputs still come from the *assumed* pull currency, never from the walk's own output. That is D10's observation about the walk arriving one layer down. The one genuinely new premise is `positioned`. On the Sail side a transcript slot could not be anything but ordinary, so the fact was free; on a mixed transcript it is the statement that this row is not sitting where a syscall event sits, which no row-local datum can decide. That completes the per-row obligations for both arms: `widthAt` and `rowOKAt` were already in place, `stepAt`/`frameAt` land here for instruction rows and in the previous commit for syscall rows, and `pullAt` follows from the State walk. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`walkedTrail_of_haltFree` is the structural replacement for `listAllInl`. That projection needs *both* the halt and the syscall table empty, which is exactly what `SyscallTableInactive.noActiveRows` was buying; this one needs only the halt table empty, and hands back a `WalkedRow` list in the same order -- so a syscall row is carried **through** the projection rather than excluded by it. The correspondence is a `List.Forall₂` and not a `List.map`, because the syscall arm decodes a raw array: the two row types are related by a relation, not a function. `Walk.isWalk_forall₂` is the transport that shape needs, and the edge agreement it asks for is `rfl` arm by arm against the new `walkedCanonEdge` -- `trailCanonEdge` with the halt arm gone. So on any halt-free shard there is now a mixed walk over the canonicalized State edges, with no premise about the syscall table at all. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`walkedTrail_pullAt` is the last of `walkE`'s five per-row inputs, and the one that ties the walk order to the transcript: a walked row at trail index `k` pulls at the transcript's own `tl.start k`. It holds for a mixed shard for the same reason it holds for an ordinary one -- `walkedRow_pullAt` telescopes the State walk against each row's *own* width, and `durationAt_transcriptOf` says the transcript reports that same width at that same index. Nothing here knows that 8 is special. Underneath it, `walkedCanonEdge_steps` and `walkedCanonEdge_timeAgree`. Canonicalization preserves `timeNat` once the endpoint's `clk_high` is genuinely 24-bit, which the goodness filter already supplies for both arms; the widths are the two `timeStep` lemmas; and the instruction arm's carrier agreement is `AlignsWith`, which fixes the State messages on the nose and reorders only the memory lists. With this, all five per-row obligations -- `stepAt`, `frameAt`, `rowOKAt`, `widthAt`, `pullAt` -- are provable from the witness over the mixed carrier, for both arms. What the walked grounding certificate still needs is the two balances, which is bookkeeping over `walkedMemoryBalance` and the State walk's endpoints rather than new semantics. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Assembling the mixed walk turned up a design fact worth naming: the syscall arm's State messages must be re-spelled to canonical, exactly as the instruction arm's are. The walk runs on *canonicalized* edges -- that is what makes the StateBump rows cancel as self-loops -- and a syscall row's pushed message is genuinely non-canonical: `clk_low + 264` may pass `2 ^ 24`, and `next_pc[0] = pc[0] + 4` carries nowhere. Both are upstream's own deliberate non-canonicalities, left for `StateBumpChip`, and recorded in this campaign's ground-truth notes from the start. `ValueAligned` cannot carry that transport. It demands `ordTime` -- every pull sitting at the row's window start -- and a syscall row's three reads deliberately sit at `+0`, `+3` and `+2`, forced by `TouchOK`'s two disjuncts. A bare re-spelling asks for none of that, which is all a canonicalized State edge needs. Hence `localStepFactG_stateRespell`, `frameFactG_stateRespell` and `rowOKCore_stateRespell` beside the `ValueAligned` family rather than as instances of it -- and `rowOKCore_` rather than `rowOK_` for the parallel reason that `RowOK.time8` is an exact eight ticks, which a 264-tick row never meets. The frame transport needs one hypothesis fewer than the step transport: a frame claim reads the pushed message's time and never its pc. One mechanical note: passing `localStateTruthG_congr` its congruence in the wrong direction *while* relying on defeq through `stateRespell`'s projection blows the recursion depth rather than reporting a type error. Making the projections syntactic with `rw` first is what surfaces the real mistake. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`trailWalk_grounded` now takes the canonicalized State edge plus four `timeNat`/`pcBits` agreements, re-spells the carrier internally, walks, and transports the `GroundedG` output back to the rows' own facts. The reason it must is narrow, which is what makes the fix cheap: only `stateBalance` reads the State messages as *messages*. Every other obligation reads them through `timeNat`, and `walkedRow_pullAt` was already written with its edge as a parameter for exactly this reason -- its docstring says the trail is extracted over the canonicalized messages while the row's facts carry the raw ones. So the mismatch is confined to one hypothesis, and internalizing the re-spelling leaves all 49 `WalkedRow.facts` call sites untouched. The alternative -- re-spelling the carrier itself -- would have rippled through four files, and would have put a canonicalization into the definition of what a walked row's facts *are*, which is the wrong place for it: the canonicalization belongs to the trail's extraction, not to the row. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`walkedCanonEdge_agrees` supplies `trailWalk_grounded`'s four re-spelling agreements in one statement: both endpoints' `timeNat` and `pcBits` match the rows' own facts. `timeNat_canonState` and `pcBits_canonState` do the work, the goodness filter already supplies their `clk_high`/`pc1`/`pc2` bounds for both arms, and the instruction arm additionally leans on `AlignsWith`, which fixes the aligned carrier's State messages to the ordinary ones on the nose. `walkedTrail_stateBalance` is the obligation that forced the re-spelling in the first place -- the only one that reads the State messages as *messages* -- and at the canonicalized edge it is `endpointBalance_of_stateWalk` applied to the walk, nothing more. `walkedCanonEdge_timeAgree` is deleted: it is now literally the first projection of `walkedCanonEdge_agrees`, and keeping both would be the kind of quiet duplication this campaign has already paid for twice. The remaining `trailWalk_grounded` hypothesis is the Memory balance. That one is not wiring: `walkedMemoryBalance`'s conclusion still carries the MemoryBump and Halt side terms, so it needs the bump-refresh elimination the ordinary engine performs -- named work, not a gap. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`RefreshWiring`'s `touchPairsAt` bridges are already row-generic --
`pushesAt_of_touchLists` and `pullsAt_of_touchLists` take `{α : Type*}
(rows : List α)` -- so the Memory balance over walked rows is an instantiation
rather than a port. What they need is a per-row touch list and the two facts
that a row's push and pull lists are its projections.
`walkedTouches` supplies the list: the caller's aligned touches for an
instruction row (the same `touchesOf` the ordinary engine chooses), and the
syscall row's own three register touches, which are already paired by
construction.
`walkedTouches_projections` supplies the three obligations, and the syscall arm
gets all three from `RowOKCore` itself -- nothing extra is assumed about the
row. `RowOKCore.touches` is a `List.Forall₂` over the pull and push lists, so
it pins their lengths, which is exactly what makes the `zip` lossless; and it
carries `TouchOK.loc_eq` per touch, which is the per-touch location agreement
`pullsAt_of_touchLists` asks for. That the shape obligation and the balance
obligation are served by the same field is a small piece of evidence the row
contract is cut in the right place.
`lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`walkedTouchBalance` converts the balance's *shape*, not its provenance: `walkedMemoryBalance` supplies the `pushesAt`/`pullsAt` form, and `RefreshWiring`'s two bridges -- already row-generic -- turn it into the per-location touch pairs `exists_refreshFreeTouchLists` consumes. Two terms disappear on the way. On a halt-free shard the Halt table's Memory messages are literally nil (`halt_producedMessages_nil_of_haltFree` and its twin), so both Halt side terms vanish outright. What is left is the MemoryBump refresh pair, which is the elimination's own input rather than a side term -- and nothing about a syscall row survives as a side term at all, because its touches are absorbed into the batch. That absorption is the move the ordinary engine already performs for the halt row, now doing the same job for syscall rows, which is exactly what the plan predicted would replace `noActiveRows`'s memory obligation. `RefreshWiring` is imported directly rather than reached transitively; there is no cycle, since it sits below the whole syscall campaign. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`; check_layering PASS (591 modules), check_root_index PASS (588 modules). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`walkedRewrittenMemoryBalance` is the other end of the touch-pair conversion. `exists_refreshFreeTouchLists` hands back a rewritten touch batch and a weakened finalize frontier whose per-location balance carries no refresh edge; rebuilding each row's carrier from its own rewritten touch list turns that straight back into `pushesAt`/`pullsAt`, which is `walkE`'s `memoryBalance` shape. It is cheap for a structural reason worth recording: `alignedOf`'s two memory projections *are* the touch list's two projections, by definition. So both bridge obligations are `rfl`, and the same two row-generic lemmas that carried the balance into touch-pair form carry it back out. The only genuine premise is the per-touch location agreement, which the rewrite preserves -- a `PullRewrite` moves a pull to a same-location, same-value, no-later ancestor. With this the Memory balance has both ends: `walkedTouchBalance` takes the witness's balance into the elimination's input shape, and this takes the elimination's output back to the walk's. What remains is instantiating the chain at the witness's concrete MemoryBump refresh pairs and frontiers, which is cutover material rather than new machinery. `lake build SP1Clean` 3802 jobs, 0 errors / 0 warnings / no stray `info:`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
Two honesty defects the campaign introduced, both found by running the release
gates rather than by the build.
**The relation grew a third conjunct and four documents still said it had two.**
`SupportedCoreNativeRelation` carries `SyscallTableInactive`, and `AGENTS.md`,
`docs/verification-report.md` ("There is no third conjunct."),
`docs/audit-surface.md` and `docs/release-audit.md` all asserted otherwise. The
Lean docstring disclosed the reversal in place; the documents did not, and a doc
that contradicts the code is worse than one that is merely stale. All four now
name the premise, say it is a placeholder rather than a derived fact, and say
what each field is waiting on -- `noActiveRows` on the engine's mixed-row
carrier, `haltTablePresent` on D8's successor Exit table. None of the gates
caught this: they check currency and declaration resolution, not whether a claim
is true.
**Two axiom-census probes had gone silent.** The census names its targets in
alternation regexes ending `\b`, and `\b` does not match a `_core` suffix -- so
when the syscall wave renamed `sp1ProviderTables_channels_subset` to
`…_core` (the syscall chip speaks on seven buses, so the statement gained a
disjunct), the probe stopped matching and simply generated one line fewer. That
is exactly the failure mode `gen_axiom_probe.py`'s own comment warns about for
release headlines. Both `_core` spellings are now named, which also adds
`sp1AllTables_channels_subset_core` -- never probed at all.
While there, `routeOf_reaches_sail` is dropped from the coverage alternation: it
has matched nothing since the `reaches_sail` path was retired, so it was dead
weight making the alternation look like it covered something it did not.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
`run_audit.sh --main-only --update` from a clean tree, plus the ledger's two counts (923 main, 1000 total). The delta is the two channel-discipline probes the alternation rename had silenced, and the ledger now records *why* they went silent -- the probe's self-check is one-sided. A wrong fully qualified name fails to elaborate and stops a stale census passing; a name that no longer matches an alternation is simply not emitted, and the census shrinks quietly. Prefer exact names over shared prefixes when adding to one. `scripts/run_audit.sh --main-only` now reports AUDIT PASS across all thirteen gates. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d
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
1 participant
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.
Stacked on #121.
The native ensemble stood in for SP1's
SyscallInstrsChipwithHaltChip: a one-row tablecovering one arm of thirteen, and covering it with two restrictions SP1 does not make. This PR
builds the whole chip with the whole semantics — every arm SP1 dispatches inline, constrained as
upstream constrains it and given a real meaning in the execution model.
121 commits, 105 files, +13,549 / −772, 18 new modules.
What lands
The chip.
SyscallInstrsChipwith all thirteen inline arms, itsRowContract/Spec, and thewhole-chip faithfulness anchor
syscallInstrsChip_faithfulcomparing the complete assertion systemand interaction multiset against the extracted Rust row. The table is registered at ensemble
position 54; the ensemble grows to seven channels.
The semantics, in six layers:
eventTrajectory,eventTimeline) whose clock is the transcript'sown prefix-summed durations rather than
8 * steps;engine recovered as an instantiation — no consumer moved, which was the acceptance test;
The mixed-row walk. The row-generic, trajectory-consuming execution engine, the walked-row
carrier, and all five of
walkE's per-row obligations —stepAt,frameAt,rowOKAt,widthAt,pullAt— proved from the witness for both arms. The trail now projects onto walked rows withno premise about the syscall table at all.
What this PR does not claim
Two things stated plainly rather than left to be discovered:
SupportedCoreNativeRelationgains
SyscallTableInactive:noActiveRowsrestricts the certified set to shards whose syscalltable is inactive, and
haltTablePresentkeepsHaltChipthe sole Exit contributor. The chip isproved and registered, but the grounding engine does not yet walk a syscall row's three register
touches. Shards with an active syscall row are outside the certified set today, and the relation
says so.
AGENTS.md,docs/verification-report.md,docs/audit-surface.mdanddocs/release-audit.mdare updated to disclose it — they previously asserted the relation hadexactly two conjuncts, and
verification-report.mdsaid flatly "There is no third conjunct."walkedTouchBalancetakes the witness's balance into the refresh elimination's input shape andwalkedRewrittenMemoryBalancereads its output back out; chaining them at the witness's concreteMemoryBump refresh pairs is the remaining step.
SupportedCoreEventRelationexists and is not yet produced by any soundness theorem; the capstone'sconclusion switch is future work.
One census defect fixed on the way
Two axiom-census probes had gone silent. The census names targets in alternation regexes ending
\b, and\bdoes not match a_coresuffix — so renamingsp1ProviderTables_channels_subsetto…_coredropped its probe with no gate objecting. That is the failure modegen_axiom_probe.py's own comment warns about. Both_corespellings are named explicitly now(which also picks up
sp1AllTables_channels_subset_core, never probed), the deadrouteOf_reaches_sailis dropped, and the ledger records why the probe's self-check is one-sided:a wrong name fails to elaborate, but a name that stops matching is simply not emitted.
Verification
lake build SP1Clean— 3802 jobs, 0 errors / 0 warnings / no strayinfo:lake test— 3817 jobs, cleanscripts/run_audit.sh --main-only— AUDIT PASS, all thirteen gates: nosorryAx, nocompiler-trusted proof constant, no
native_decidein the main library, noskipKernelTC, noaxiom declarations, every elaboration-budget site allowlisted, census matches its snapshot
check_current_docs,check_release_surface,check_audit_surface,check_report_citations,check_root_index,check_layeringall PASSsorryunderSP1Clean/; noset_option maxHeartbeats/maxRecDepthadded🤖 Generated with Claude Code
https://claude.ai/code/session_01J6qohiaMMLVxznWLifuJ2d