Exportable witness generation for all 25 chips, gated against SP1's real prover - #114
Closed
dtumad wants to merge 55 commits into
Closed
Exportable witness generation for all 25 chips, gated against SP1's real prover#114dtumad wants to merge 55 commits into
dtumad wants to merge 55 commits into
Conversation
…etes) New scripts/check_no_witness_native.sh counts witnessNative/witnessVectorNative/ Unconstrained*Native/.native-payload sites in SP1Clean/ (baseline: 172 textual hits). Report-only by default; --enforce (exit 1 on any hit) flips on at wave W7. Wired non-blocking into run_audit.sh and the CI guards job. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
AddOperation gains populateProgram (Witgen.M, letU-shared carries) and the opaque populateIR wrapper + populateIR_eval, tying the IR evaluation to the unchanged pure populate under isU64 bounds (u64Wrap discharges the 2^64 wraps). AddChip main swaps witnessVectorNative for witnessIR (fields 4) (populateIR ...); completeness crosses the folded boundary with one populateIR_eval rewrite and closes with spec_populate verbatim. Full build, lake test (byte-identical goldens), and the axiom census are all unchanged-green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Addi reuses AddOperation.populateIR directly. SubOperation gains its own populateProgram/populateIR: the u64 sort has no subtraction, so the per-limb two's complement 65535 - b_i is taken at field-expression level and bridged by val_complement (below 2^16 the field difference's value is the N difference, since 2^17 < p). Both completeness proofs cross the folded boundary with one populateIR_eval rewrite. Full build (0 warnings/info), lake test with byte-identical goldens, and the main-scope axiom census are unchanged-green; AddChip.completeness verifies as [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Proofs/WitgenBridge.lean holds the shared machinery for Clean's Circuit.ComputableWitnesses obligation: a zero-witness operation list satisfies any witness-congruence condition vacuously (its witness ops produce Vector F 0), so a chip's composed readers and gadgets are dispatched by their cell count rather than unfolded -- which is what keeps these proofs off the elaboration cliff. AddOperation gains populateIR_congr (environment-locality of the witness IR, the counterpart of the semantic populateIR_eval), and AddChip.computableWitnesses proves the chip's generators read only its own input row. This is phase 0 of the completeness programme: it is the step that turns each chip's completeness field from 'any environment consistent with my generators' into 'the row my generator built'. It is provable precisely because the row is on the exportable IR -- a witness closure reading ProverHint cannot satisfy ComputableWitnesses at all, since AgreesBelow does not constrain hint. Full build (0 warnings/info), lake test, and the audit all pass; the new theorem is [propext, Classical.choice, Quot.sound]-clean and the census is unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Introduces witnessVectorIR (Native/WitnessCombinator.lean), the combinator the cutover actually needs: a full WitgenIR payload in Clean's literal-cell-count shape. Clean's witnessIR (fields m) emits '.witness (size (fields m))', which is definitionally but not syntactically m, so it leaks into the offset arithmetic of every later operation and stalls the structural proofs (chip faithfulness anchors, TypedMemorySelectors, exposedChannels_eq) on 'offset + size (fields 2) + size (fields 1)' instead of 'offset + 3'. With the literal shape those proofs need only a token rename, which is what makes the remaining waves mechanical. Add/Addi/Sub move onto it too. Addw/Subw gain valueIR/msbIR programs (the msb re-derives the high limb from the same carry chain, and needs the field bound since it reads .val of a cast limb). UType's addend is pure input arithmetic, so it goes straight to witnessVector with no populate companion; UType/Jal/Jalr all reuse AddOperation.populateIR. Jalr's lsb becomes witnessField over an earlier witnessed cell; its u64 sort truncates, so hlsb_val strips the % 2^64 from the value uses via the add result's own isU64, while binarity survives it untouched. Full build (0 warnings/info), lake test with byte-identical goldens, and the audit all pass; census unchanged. Escape-hatch census: 167 -> 128 sites. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Six chip docstrings still described the row as witnessed 'via populate'; the witness is now the exportable IR, with populate remaining its value-level anchor (and, for Jal/Jalr/Branch/DivRem/UType, the shared vocabulary their contracts are written in). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The four add/sub-family operations each carried two defs (a Witgen.M builder plus a toIR wrapper) where one suffices. Running sums are now ordinary Lean lets that inline into each output expression, so each witness IR is a plain ofFExprs with no locals array. What this buys: six defs removed; every eval/congr proof drops from a full "simp" to "simp only" (the locals-array normalization was what forced the non-only form, and it is the Array.size landmine that cost the most time in W1); and Clean's Witgen.M / letU / toIR surface disappears from the repo entirely, taking with it the documented "no sharing behind an opaque prefix" restriction. The congr proofs additionally disable the u64Wrap simproc, which would otherwise run omega with no bounds in scope. Cost, recorded in the docstring: the exported term repeats carry subterms, O(n^2) nodes -- ten for four limbs. letU sharing remains the alternative if that ever matters for a wider operand. The statements of populateIR_eval / _congr are unchanged, so this is a drop-in: no chip proof, faithfulness anchor, or trace test was touched. Full build (0 warnings), lake test with byte-identical goldens, and the audit all pass; census unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two top-level libraries modelled on VCVio's ToMathlib/, with its load-bearing
rule: ToMathlib imports only Mathlib, ToClean imports Clean (and may import
ToMathlib), and NEITHER may import SP1Clean. That is what keeps the material
genuinely contributable, and it makes the terminal step of an accepted upstream
PR a plain deletion plus a repoint of importers -- exactly how VCVio retired
~40 ToMathlib files when PolyFun landed.
Declarations live in the namespace they would occupy upstream, so acceptance
changes no call site: witnessVectorIR moves into namespace Circuit with a
matching export, beside Clean's own witnessVector; the two zero-witness
composition lemmas move into namespace FlatOperation, where they belong next to
compose_computableWitnesses. Each file's docstring now states the gap against
upstream -- what exists there, what is missing, why -- since that text becomes
the PR description.
First three residents, all previously carrying explicit "candidate for upstream"
notes and all with zero SP1 content:
ToClean/Circuit/WitnessCombinator.lean (witnessVectorIR + ExplicitCircuits)
ToClean/Circuit/WitgenBridge.lean (forAll_witnessCongr_of_{localLength_zero,subcircuit})
ToMathlib/General.lean (was Math/Misc.lean: 100% generic, zero Clean imports)
Plumbing: both get their own lean_lib with the same eight linter flags as the
core pillars (upstream-bound material gets no relaxation) and join
defaultTargets, so every module compiles even before an SP1Clean file imports
it. Six scripts hard-coded SP1Clean as a path or namespace prefix and would have
left the new trees unpoliced; all are widened -- check_root_index (now
parameterised over the three trees, and it fails if a tree exists without its
index), the four source guards, check_report_citations, and sp1Lint's keep
predicate plus its import set (the upstream libs are imported only when their
oleans exist, so the driver runs before and after they are created).
Verified the guards actually fire rather than passing vacuously: planted a
native_decide, a skipKernelTC, a maxHeartbeats override and an unindexed module
in the new trees, confirmed each guard failed, then removed them.
Full build (0 warnings), lake test, lake lint, and the audit all pass; census
unchanged.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two more residents, both previously unlabelled but entirely Clean-generic:
ToClean/Circuit/InteractionRecovery.lean (was Model/, 215 lines, 12 lemmas)
Every statement is over Subcircuit / RawChannel / FormalCircuit /
GeneralFormalCircuit / FormalAssertion / ChannelsLawful; it imports only
Clean.Circuit.Basic and Clean.Circuit.Subcircuit, and one of its own
docstrings already called it "the channel-generic home of...". SP1 appeared
only in motivating prose.
ToClean/Tactic/GetElemFastPath.lean (was Math/, one macro_rules)
Registers `decide` as a get_elem_tactic_extensible rule, so a literal index
bound closes in ~26 heartbeats instead of the ~0.34s that core Std's
range-support rule costs in a 40-hypothesis circuit context. Its real
upstream is Std, not Clean; Clean is the pragmatic intermediate because the
rule must register after Std's, and the docstring says so.
InteractionRecovery drops its SP1Clean namespace prefix and keeps the bare
`InteractionRecovery` namespace, which is both the name Clean would adopt and
the reason all 31 call sites resolve unchanged -- only the `open` lines in 34
Faithful/Soundness files needed the prefix removed.
Full build (0 warnings), lake test, lake lint, and the audit all pass; census
unchanged.
Still queued for the harvest: CircuitProofStart (whole file is Clean-generic,
but its witnessNative quartet retires at cutover W7, so it moves after that),
ChipOracle's 11 constraint-normalisation lemmas, DivRem's assertZeros
combinator, Model/Channels' four generic helpers, Walk.lean and the ZMod
numeral block into ToMathlib. EvalVec stays put: vec4_eval's useful form is the
extractor's literal shape at SP1's word length, so it is not as generic as it
looks.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ToClean/Circuit/WitgenCongr.lean gives the witness IR a syntactic read set and proves the congruence it justifies: two prover environments carrying the same committed data and prover hints, and agreeing on every circuit expression the program embeds and every raw cell it reads, produce identical witnesses. FExpr.exprs / U64Expr.exprs / BExpr.exprs the embedded circuit expressions Step.exprs / VExpr.exprs / WitgenIR.exprs lifted through steps and formers VExpr.envIndices / WitgenIR.envIndices the raw cells envRange reads CtxAgree locals, loop index, data, hint FExpr/U64Expr/BExpr.eval_congr one mutual block, all 32 cases evalSteps_congr the let-fold; establishes locals VExpr.eval_congr, WitgenIR.eval_congr the capstone Why this rather than a per-gadget simp: Circuit.ComputableWitnesses is exactly a witness-congruence obligation, and discharging it by unfolding the IR body under circuit_norm walks into the u64Wrap simproc, which runs omega on every % 2^64 subterm. In a congruence goal there are no bounds in scope for those omega calls to use, so each one fails at full cost -- measured downstream at >=32x, still failing at eight times the default heartbeat budget. Applying a lemma sidesteps the trap structurally, and replaces every hand-written per-operation *_congr. .native is excluded rather than assumed away: an arbitrary Lean closure has no inspectable read set, which is precisely why a chip must reach the .ir form before it can be shown to generate witnesses honestly. The data/hint premises are the other half of a known upstream gap: ProverEnvironment.AgreesBelow constrains only `get`, so a witness reading dataGet/hintGet cannot satisfy ComputableWitnesses as Clean states it today. Adding those two conjuncts upstream weakens every obligation (so existing instances stay true) and is rfl at both use sites, since fromList and fromArray carry constant data/hint. That patch is queued; this lemma is already stated against the fixed form. Axiom-clean: [propext, Classical.choice, Quot.sound]. Builds with zero warnings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The per-chip eval_* lemmas push evaluation DOWN into components; circuit_norm's normal form goes the other way, pulling projections UP out of eval (ProvableStruct.eval_eq_eval is tagged down-high, and StructEvalSimprocs' lift simprocs rewrite eval env (s.f) to (eval env s).f). Two opposite orientations of one equation cannot both live in a confluent simp set, which is why those lemmas are inert under circuit_norm and why any proof needing them first has to undo the normalisation by hand. AddChip now also states its two operand words the other way round -- (ProvableStruct.eval env input).op_b_val = Vector.map (Expression.eval env) input.op_b_val -- with the projection already outside and an inert right-hand side (Expression.eval env appears unapplied, so no lift simproc fires). Those are safe to tag, and they are directly usable by any proof holding struct-level input agreement, which is exactly the form ComputableWitnesses hands over. Payoff: AddChip.computableWitnesses drops from about thirty lines to eight -- the two bespoke `key` lemmas and their rewrite gymnastics are gone, replaced by congrArg through the tagged lemma. Only vector-valued operands get this treatment. A scalar field is already in normal form as (ProvableStruct.eval env cols).f, and restating one would loop against the lift simproc -- so RTypeReader.eval_opA0 and its five siblings are deliberately left alone. Also records, in ToClean/Circuit/WitgenCongr.lean, an applicability limit found by testing F1a's capstone against the real obligation: WitgenIR.eval_congr takes env.data/env.hint agreement, and FormalCircuitBase.ComputableWitnesses supplies neither -- it relates env and env' by AgreesBelow, which constrains get alone. So the generic congruence is not yet applicable at a chip, and gadgets keep their own small congruence lemmas meanwhile. The docstring names the two ways to close it: the upstream AgreesBelow patch (preferred, and already queued), or a local metaKeys refinement that drops both premises for programs free of dataGet/hintGet. Full build (0 warnings) -- which is the real test, since two new circuit_norm lemmas change a global simp set -- plus lake test, lake lint, and the audit all pass; census unchanged. AddChip.computableWitnesses stays [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ProverEnvironment.AgreesBelow constrained only env.get, but a witness generator can read three channels of a ProverEnvironment: cells, committed data (via FExpr.dataGet) and prover hints (via FExpr.hintGet). Since ComputableWitnesses is exactly "AgreesBelow n env env' implies the generators agree", that obligation was false -- not merely hard -- for any program touching the witness IR's documented nondeterministic escape hatch. The fix strengthens AgreesBelow with the two missing conjuncts. It cannot be shimmed in ToClean: a local copy with the stronger hypothesis yields a WEAKER obligation, and Clean's own witgen_usesLocalWitnesses needs the stronger one, so the shim would not feed the theorem it exists to feed. Hence the fork. Clean therefore moves from Verified-zkEVM/clean 0e53b9f2 to dtumad/clean branch sp1-integration at 8301b77a -- the same base plus one change (f5ae8e17) and a worked example (8301b77a). AgreesBelow sits in hypothesis position everywhere but one discharge site, where both environments are ProverEnvironment.fromList _ hint with constant data, so the new components are rfl; no Clean conclusion weakens and the two theorems concluding with it get strictly stronger. The example file's not_computable_from_cells_alone exhibits two environments agreeing on every cell but committing different memory, which is what makes this a bug fix rather than an ergonomics request. The fork is disclosed rather than assumed benign: docs/release-audit.md gains a paragraph naming the base, the delta and the exit condition, the verification report gains trust item T5, and docs/agents/clean-upstream.md records the fork state, the branch-to-PR map, and the standing rule -- a change that MODIFIES an existing Clean declaration goes in the fork, a pure addition stays in ToClean. Re-pin to upstream when the PR merges. sp1-integration must keep the pinned rev reachable, since Lake clones refs/heads and tags only. Also here, from sizing the rest of the upstream queue: JalrChip's proof-start macro drops its scoped struct-eval pass. That step transcribed Clean's 27 structEvalSimpLemmas by hand -- the set is meta-level data, unreachable from surface simp only -- under a comment asking the reader to keep the copy in sync. Replacing it with a tactic that reads Clean's array directly showed the step was dead: with the enclosing try stripped, simp reports "made no progress" in soundness, and completeness has no h_holds at all. try had been swallowing both. Both proofs elaborate identically without it (5.3s vs 5.4s), and the transcription was byte-identical to Clean's current list, so the drift hazard was real but had never fired. Deleted rather than replaced; the replacement tactic has no other call site, so it lives in clean-upstream.md as a snippet instead of in the build. What survives is the hoist, which is measured and is the whole of what the macro buys. GetElemFastPath's docstring now names its real upstream, Lean core/Std rather than Clean, and two docs stop citing its pre-move path. Full build (0 warnings), lake test, lake lint and run_audit --main-only all pass; the axiom census is unchanged across the re-pin. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…and hint Two files asserted, as fact, that the generic witness congruence could not be applied at a chip's ComputableWitnesses obligation. That was true at the previous Clean pin and is false at the current one, and both statements are load-bearing -- one is the recorded rationale for a campaign decision. Checked rather than assumed. Against AddOperation.populateIR: eval_congr unifies (ofFExprs unfolds to .ir [] (.lit ...)), AgreesBelow.data_eq/.hint_eq supply the two premises the obligation previously withheld, the hcells premise is vacuous because the program has no envRange node, and the syntactic read set reduces to a literal list of operand expressions -- so membership becomes a disjunction that input agreement discharges. Two things block a naive simp only and are worth recording, since neither is visible from the goal text: a gadget's running sums are ordinary Lean lets, so the WitgenIR.exprs match cannot reduce until they are zeta-reduced (simp only on the gadget name does this, unfold does not), and VExpr.exprs on a literal leaves FExpr.exprsList over a Vector.toList that needs Vector.toList_mk. The resulting simp set is gadget-independent apart from the populateIR name, which is the sense in which this is one congruence for every gadget rather than one per gadget. It also stays clear of circuit_norm, so the u64Wrap trap never arises -- the truncations live inside U64Expr, not as Nat HMod. AddChip's note keeps its conclusion but on the correct grounds: a .native closure has no read set at all, which is why hint-driven chips move to typed inputs. The old stronger reason -- that AgreesBelow did not constrain hint, making even the IR's hintGet node unprovable -- no longer holds, so the W4 pilot now chooses between the two hint encodings on their merits. Retiring the five bespoke per-gadget congruence lemmas onto eval_congr, which also removes the tree's last five -Witgen.u64Wrap disable sites, is the follow-up. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rejected The queue entry claimed the simproc's cost was wasted work on its failure path -- "in a congruence goal there are no bounds, so every % subterm pays a complete failing omega" -- and specified a pre-filter accordingly. Implementing it falsified the claim, in three stages. First screen, filtering omega's input down to the hypotheses it can actually consume: Clean's suite stayed green, our proof still timed out at 200k heartbeats. Second screen, skipping the call outright when neither the operand's shape nor any readable hypothesis could bound it: also green upstream, also no effect locally. An earlier form of the second skipped on hypotheses alone, and Clean's own tests rejected it immediately -- Ch32, Maj32 and Add32 all broke, because omega derives bounds from term structure with an empty context, so a bound need not come from a hypothesis at all. Then the measurement that should have come first. On AddOperation.populateIR_congr, the simp takes 118s with the simproc enabled and needs a 4M-heartbeat budget to finish at all, against 1.9s for the whole module with it disabled -- about 60x -- and the profile is diffuse, with no entry above threshold. The calls are not failing. They are succeeding: the operands are structurally bounded, `(… % 65536) % 2^64`, so omega discharges each one, and the cost is the volume of successful calls. No screen can help with work that is being done on purpose. The branch is pushed as dtumad/clean u64wrap-prefilter and deliberately NOT merged into sp1-integration, which stays at the AgreesBelow commit; the pin is unchanged. A branch reaching sp1-integration has to clear two bars -- Clean's suite green, and a measured effect on local chip work -- and this one cleared only the first. What survives is a better-specified entry: the useful change is a syntactic bound computer for the common shapes that never reaches omega, not a screen; it is real meta-programming rather than a small patch; and it is low priority, because it blocks no chip work. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ongruence
Second chip on the witgen bridge. SubOperation gains populateIR_congr, SubChip
gains the two operand lemmas in circuit_norm's orientation, and the CW proof is
AddChip's shape unchanged -- the chips compose the same six operations in the same
order, so the only difference is that Sub's witnessed value is a two's-complement
sum whose complement limbs are Expression arithmetic over the operands and carry no
extra environment dependence. Built first try; axiom-clean.
It also settles whether WitgenIR.eval_congr should replace those per-gadget
lemmas. Measured head to head on Add, now that the AgreesBelow fix makes the
generic route available at all:
bespoke (Vector.ext + interval_cases + simp only [circuit_norm, -u64Wrap])
~6 lines, 1.9s for the module
via eval_congr
~9 lines, 2.1s
so the generic route is slightly longer, no faster, and its rcases arity -- 20
disjuncts for a 4-limb carry chain -- is gadget-specific, which is the per-gadget
coupling it was supposed to remove. The bespoke lemmas stay, and the plan to retire
them onto eval_congr is dropped.
The recipe is recorded rather than discarded, because two of its three obstacles
are invisible from the goal text: a gadget's running sums are ordinary Lean lets,
so the exprs match cannot reduce until they are zeta-reduced (simp only on the
gadget name does this, unfold does not), and operator-sugared arithmetic is HDiv at
U64Expr x Nat rather than the U64Expr.div constructor, so exprs cannot match it
until Clean's _def rfl-lemmas fire.
Two things would still flip the verdict, and both are recorded next to it.
Robustness: the generic route never touches circuit_norm, so it cannot walk into
the u64Wrap cost, whereas the bespoke proofs depend on remembering -Witgen.u64Wrap
-- forgetting it costs 118s and a 4M-heartbeat budget on Add alone. Reach: a
witness reading dataGet/hintGet has no bespoke route at all, since simping its body
cannot relate two environments with unrelated committed data. That is the case the
lemma exists for and the one the hint-driven chips will meet.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e hatch
Witness generation that runs through a Lean closure keeps a circuit runnable but
rejects #assert_exportable, so the generator can never be serialized for a proving
backend -- which is the whole point of the IR. AddressOperation is the best ratio
in the tree for fixing that: two sites, and it is the ONLY escape hatch the nine
memory chips have. Each of Load{Byte,Half,Word,Double,X0} and
Store{Byte,Half,Word,Double} composes AddressOperation.circuit and witnesses
nothing itself.
It is also the cheapest conversion available. AddrAddOperation.populate is
AddOperation.populate with three limbs instead of four -- the same base-2^16 carry
chain -- so populateIR, populateIR_eval and populateIR_congr are the frozen recipe
one limb shorter. The second site is a single field inverse, and FExpr.inv's 0 goes
to 0 convention is exactly what the gate wants, so the padding row (is_real = 0)
needs no special case.
The inverse witness reads `value`, the output of the witness before it. That is not
a problem but the point: those are variables at strictly lower offsets, which is
what an .expr leaf is for and what keeps the row's witnesses computable.
Only the completeness seam moved. The witness obligation is now stated against the
IR, so it crosses to `populate` once through populateIR_eval and reads the
witnessed cells off h_value directly, replacing three per-limb rewrites of the
closure's evaluated operands.
Ripple: none. The full build passes untouched -- the memory chips name
AddressOperation.circuit in their elaborated simp sets rather than the witness
form, and using witnessVectorIR (literal width) rather than witnessIR (fields m)
avoids the size (fields m) offset leak that bit the W2 wave.
Verified with the tool rather than by inspection. #assert_exportable had never been
used in this repo; it now reports "exportable ✓ (4 witness cells)" for LoadByte,
StoreWord and LoadX0, and still fails on Bitwise with the flat indices of its two
surviving closures -- so the check is known to have teeth, not assumed to.
Real construction sites 63 -> 61; chips still on the escape hatch 17 -> 8. The
guard's headline count only moves 128 -> 126 and understates this: most of its hits
are proof-side simp references and infra lemmas deleted at the enforcement wave.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ty battery
Finishes the honest-witness side of the ported set: Addi, Addw, Subw, UType, Jal
and Jalr join Add and Sub, so every chip on the witness IR now proves that its
generators read only the input row and cells below their own offset -- the
precondition that lets Clean's array-backed interpreter reproduce them. All eight
are [propext, Classical.choice, Quot.sound].
The recipe from Add/Sub carried, but the six chips fan out along one axis the
earlier two did not exercise: what the witness operands actually ARE.
Addi register read + immediate, through the I-type reader
Addw / Subw two payloads each -- W-result limbs and its sign bit
Jal addends CONSTRUCTED, not projected: pc ++ 0, plus an immediate,
plus the literal 4 whose limbs need no agreement at all
UType addend `is_auipc · pc`, witnessed as a bare literal vector
Jalr both styles, plus an alignment bit that reads add_value[0] --
a cell this same row witnessed eight positions earlier
That last one is the case ComputableWitnesses exists to permit, and it is the
first proof here to use the environment-agreement hypothesis rather than input
agreement: AgreesBelow.get_eq closes it, which is the accessor the pinned Clean
change added.
Two things learned that are worth the next chip's time. UType's literal-vector
witness cannot be closed with circuit_norm -- the payload is inline in `main`
rather than behind a named populateIR, so there is no opacity boundary and the
simp reaches the whole chip and blows the budget; unfolding the IR evaluator alone
(WitgenIR.eval, evalSteps, VExpr.eval) is both correct and cheap. And constant
operand limbs need Expression.eval named explicitly, since simp will not reduce
`eval env 0` on its own.
JTypeReader gained the eval_cols lemma every other reader already had.
SP1CleanTest/Exportable.lean is the new artifact, and the reason any of this
means something. #assert_exportable walks a circuit's flattened operations and
fails, naming flat indices, if a witness is still a native closure -- so it
checks by evaluation what check_no_witness_native.sh checks by grep. Eighteen
chips pass; the cell counts are pinned with #guard_msgs, so witness-count drift
is caught too. Both directions verified rather than assumed: Bitwise fails with
the flat indices of its two closures, and mis-stating a count fails the golden.
Coverage is exactly the converted set and grows a wave at a time -- the chips
absent from that file are the remaining waves, named there with the reason each
would fail today.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
SP1 pads DivRem with "0 divided by 1" DIVU rows -- `is_divu = 1`, not all-zero (crates/core/machine/src/alu/divrem/mod.rs, unchanged from our pinned a630089d9 through v6.4.0: that tag's 15 commits touch only sp1-gpu and zkevm, and the diff over crates/core/machine/src/alu/ and cpu/ is empty). The old encoding expressed that as a non-zero `getD` default on an eight-slot hint, and a non-zero default is the one thing Clean's witness IR cannot reproduce: `FExpr.hintGet` reads a missing row as zeros. So the eight-slot encoding is what kept this chip on the `.native` escape hatch, and the workaround on offer was to infer row-presence from the flag sum -- a spec refinement to "an all-zero row means padding", weakening a definition that ~2,800 lines of completeness proof cite. Re-encode instead. The hint carries the other seven flags and `is_divu` is derived as `1 - Σ(seven)`. The flags are one-hot with sum 1 unconditionally, so nothing is lost -- there is no all-zero state to represent -- and an absent key now gives seven zeros, hence `is_divu = 1`: exactly SP1's template, for free and with no `.ite`. The ambiguity does not get papered over, it stops existing, because in this encoding an all-zero row genuinely IS the DIVU row. `hintFlags` still returns a `Vector 8` in the same slot order, so all ~30 downstream uses of `f[i]` are untouched; only the reading changed. The hint schema is ours to choose -- SP1's prover has no hint concept for these flags, and the vectors are built by our own harness from the dumped executor opcode. Two facts that were prover assumptions are now theorems. `hintFlags_sum_eq_one` is an identity for every hint, honest or not, so ProverAssumptions drops its `Σ f = 1` conjunct and the completeness proof derives it -- a weaker contract for the same result. `hintFlags_absent` states the template correspondence directly. Value-preserving, and checked rather than argued: `divremchip_trace_conforms` is a native_decide comparison of the trace derived from this chip's own witness closures against vectors dumped from SP1's real Rust generate_trace, and it still passes byte for byte -- padding rows included, since the pad row is built with the empty hint and so exercises the derived slot directly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…vRem The queue entry claimed the missing U64Expr.sdiv/srem meant "DivRem's populate cannot be expressed and that chip stays on the .native escape hatch", and sized a PR to add them. The premise is false, and leaving it would send someone to build an upstream feature we do not need. Signed division IS the sign/magnitude construction over the unsigned ops the sort already has -- Lean core defines BitVec.sdiv as a four-case match on the operand msbs, each arm udiv applied to .neg-normalized operands. This repo had already proved half the reduction before the entry was written (srem_eq_bvAbs), negation is one node since every u64 op wraps, and the chip already commits magnitudes and signs as columns, so it is the arithmetization SP1 itself uses rather than a reformulation invented to dodge the gap. Three of the entry's own caveats invert under that encoding. i64::MIN / -1 needs no special case and leaves no signed primitive to diverge on. The divide-by-zero .ite was already an outer branch before any sdiv. And "there is no Int normalization set" is the strongest argument FOR the magnitude form, which stays in Nat where u64Wrap and omega already work. Kept as a record rather than deleted, since the transferable lesson is that a missing-primitive ticket should first check whether the primitive is definitionally the ops already present. Its citation is by lemma name rather than line number -- the line I first wrote was already three off, which is the argument against line-number citations into a moving file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… code out Opening wave of the end-state campaign (extractable witgen + per-shard completeness + one anchoring layer + the Rust seam): - check_no_witness_native.sh: the scope comment and all three user-facing messages now say SP1Clean/ + ToClean/, which is what the grep has always covered. ToClean is upstream-destined library code, so it must stay exportable too - the comment was wrong, not the grep. - WitnessCombinator.lean: reworded the one prose mention that matched the guard pattern, so --enforce can flip at cutover completion without an allowlist. - Exportable.lean: DivRem's "needs signed division in the u64 sort" claim was withdrawn with U6 (srem_eq_bvAbs proved half the sign/magnitude reduction); the docstring now records the true remaining cost (30 sites, 217 cells). - Add/Sub trace-anchor docstrings: rows have come from the witness-IR programs (populateIR), not Lean closures, since the W1 cutover. - TraceGenerator.keepCols: deleted; zero users, all anchors compare unmasked. Escape-hatch census: 126 -> 125 (the ToClean prose hit). Gates: full build 3663 jobs clean, lake test clean, audit PASS with unchanged census, lint, root index 444 modules. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The three shared pieces the remaining seven conversions draw on, landed first so no wave reinvents them: - U16MSBOperation.populate_msbF: the FExpr twin of populate_msb (high bit of a 16-bit operand as u64-sort division by 2^15), with its eval lemma (16-bit bound keeps val from wrapping) and bounds-free congruence. Consumers: Lt's sign compare, Mul's sign extension, the shifts' msbs. - Native/Witgen/HintFlags.lean: hintFlagsIR, the common witness-IR form of every chip's hintFlags accessor (row 0 of a string-keyed ProverHint, zeros when absent - hintGet's default IS the accessors' .getD fallback). First hintGet material in the repo; the congruence closes from the fork's AgreesBelow hint component alone. - ToMathlib Nat.two_pow_shiftRight: 2 ^ n >>> k = 2 ^ (n - k), the only subtraction-free spelling of the shifts' 2^(16-s) scale factors available in the subtraction-less u64 expression sort. All three deliberately NOT @[circuit_norm] (opacity doctrine); only the eval/congr lemmas cross the boundary. Gates: full build 3664 jobs clean, lake test clean, audit PASS with unchanged census, lint, root index 445 modules. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
New top-level rust/ directory for Rust-side consumers of the witness-gen export. Deliberately in this repo, not the extraction overlay: the overlay is provenance-frozen, and the interpreter consumes only the wire format (docs/witgen-wire-format.md, wave D3) - zero SP1 types - so the directory ships to the SP1 team as-is. Scaffold only: package metadata, a stub main, and the README stating the contract (conformance oracle, completeness-side, never a trusted component). Parser, KoalaBear arithmetic, evaluator, and the differential test against SP1-dumped fixtures land in wave D4. cargo stays out of the Lean CI; scripts/run_interp_diff.sh (D4) wraps the manual run. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ecipe The W4 pilot clears the first hint-driven chip from the escape hatch, and with it every idiom the remaining conversions repeat: - BitwiseU16Operation gains the struct-shaped IR twin: populateFE (the sixteen columns as a Columns-of-FExprs, result operands computed in the u64 sort - even bytes val % 256, odd bytes val / 256, agreeing with populate's field-side (w - low)*256^-1 on bounded limbs), byteOpF (the field-opcode ite matching byteOp's val branches by val injectivity), populateFE_eval (+ its per-cell corollary, the exact completeness-seam shape) and populateFE_congr (+ its raw ofFExprs payload form). The measured lesson is folded in as structure: u64Wrap's omega takes the whole context as facts, so the sixteen cells assemble by term-mode chains through opaque-struct toElements navigators and six per-shape helpers with minimal contexts - the file needs no budget escape and builds in ~4s. - BitwiseChip.main: the flag cells read "bitwise_flags" through witnessVectorIR + hintFlagsIR (the repo's first FExpr.hintGet), and the column struct through witness (populateFE ...). Cell counts stay literal; the explicit elaborated instance, Faithful anchor, and all six Soundness consumers are untouched. - Completeness rewires through ONE value-level pins have (hcolsPop, via populateFE_eval_cell): the old definitional .native ascription - and the 32M-heartbeat trap its comment documented - is gone; populate never unfolds. - computableWitnesses (Proofs/Chips/BitwiseChip/Witgen.lean): the flag payload closes from AgreesBelow's hint component alone (the fork's fix cashing out), the gadget payload from operand projections plus h_agree.get_eq on the three earlier flag cells of the same row. [propext, Classical.choice, Quot.sound]. - docs/agents/porting-recipe.md gains the witness-IR port recipe (the guard script's remediation pointer now resolves), distilled from the Add and Bitwise pilots including the fold rule and the CW slot count (=== gates yes, plain assertZeros no). Gates: full build 3665 jobs clean; lake test clean with the Bitwise trace anchor passing UNMODIFIED - the native_decide byte-for-byte re-derivation of every dumped SP1 row (padding included) through the new IR path; audit PASS, census unchanged; lint; root index 446. Escape-hatch census 126 -> 122 (59 construction sites remain across 6 chips). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Second hint chip off the escape hatch, a mechanical replay of the A2 recipe with one deliberate investment: the LtOperationUnsigned scan twins (comparisonLimbsF / flagsF / notEqInvF / compareBitF, with scanF_eval and scanF_congr over ABSTRACT limb expressions) live at the unsigned gadget, because DivRem instantiates the same functions at its remainder/divisor words in wave A7. The scans are pure field-sort - =? (feq) conditions mirroring the value scans' dis-equality with branches swapped, FExpr.inv leaves, <? (flt) for the compare bit - so their eval lemmas are bounds- free if-congruences. LtOperationSigned gains populateFE (populate_msbF's first consumers in the is_signed-gated sign bits; sign-adjusted limb expressions; every unsigned cell wrapped in the is_real gate mirroring the value side's zeroCols branch), six toElements navigators, populateFE_eval (one is_real case split resolves every gate on both sides at once), populateFE_eval_cell, and populateFE_congr_flat. Chip side: flags through witnessVectorIR + hintFlagsIR "lt_flags", the column struct through witness (populateFE ...); completeness rewired through one value-level pins have (the definitional .native ascriptions and their documented 32M-heartbeat trap deleted); computableWitnesses proved with the is_slt cell below the payload via AgreesBelow.get_eq and the is_real input via the h_input projection. [propext, Classical.choice, Quot.sound]. Gates: full build 3666 jobs clean; lake test clean with the Lt trace anchor passing UNMODIFIED (byte-for-byte against SP1's dumped rows through the new IR path); audit PASS, census unchanged; lint; root index 447. Escape-hatch census 122 -> 119 (57 construction sites, 5 chips). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…iscipline The widest single conversion: six-flag hintFlagsIR, the repo's first single-cell witnessField (.hintGet "branch_branching"), the named nextPcIR (the is_branching-selected blend of two inline AddOperation carry chains, with an elementwise eval lemma concluding exactly the per-cell blend form the completeness pins consume), and the LtOperationSigned struct through A3's populateFE with is_signed the SUM of two flag cells below it. Completeness (Core.lean, the largest seam yet): the flags/branching pins bridge through the ofFExprs-form eval lemmas (this chip normalizes to the raw payload form, unlike Bitwise/Lt - both bridge statements exist now); the three next_pc pins rebuild through nextPcIR_eval; the lt pin turned out STRUCT-level, so it closes by one rw chain (he_lt, populateFE_eval at explicit literal operands, h_input.1) with zero navigator machinery. The old .native ascriptions and the eval_native_apply normalizer line are gone. Structural fallout absorbed: Formal.lean's and Faithful/BranchChip's shallow op-list simp lists swap the retired combinator names for witnessVectorIR/witnessField/Witnessable.witness/witnessIR (hFieldSize died with witnessNative's size-shaped lengths - the IR emits literal widths). computableWitnesses closes with per-index term chains (getElem_map + congrArg through h_input) after the struct-eval simp routes all measured out as whnf hazards; is_branching and the two comparison flags read same-row cells via AgreesBelow.get_eq. [propext, Classical.choice, Quot.sound]. Branch has NO trace anchor - flagged per plan: CW + the rewired completeness + the untouched soundness are this wave's checks; the idioms are the ones the anchored Bitwise/Lt waves validated byte-for-byte. Gates: full build 3667 jobs clean, lake test clean, audit PASS with unchanged census, lint, root index 448. Escape-hatch census 119 -> 99 (53 construction sites across 4 chips: Mul, ShiftLeft, ShiftRight, DivRem). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e gadget Converts MulChip's three escape-hatch witness sites to the exportable IR (guard census 99 → 86; the hatch now lives only in the shifts and DivRem): * `MulOperation.populateFE` — the 45-cell IR twin of `populate`: the sign/zero-extended byte streams (`streamF`), the u64-sorted convolution fold (`cpF`), and the authoring-time chain recursion (`chainF`) mirroring `MulCarryChain.chainM` shape-for-shape, so `chainF_eval` is one induction (with the chain bound as a *scoped* hypothesis — the global form is false past limb 15). Sign selectors (`bsgnF`/`csgnF`) and the `is_mulw`-gated `product_msb` are the only field-sort cells. * `populateFE_eval` — 45 cells against nine `toElements` navigators over an opaque struct; carry/product cells rewire tactically through `Vector.getElem_ofFn` (letting `exact` unify through `ofFn` at a literal index is a whnf-through-recursion timeout). `populateFE_eval_cell` is the completeness-seam corollary; the bounds-free congr ladder (`populateFE_congr_flat`) mirrors the eval ladder twin-for-twin. * Chip swaps: flags via `hintFlagsIR "mul_flags" 5`, the struct via `witness (populateFE …)`, and the result word as the repo's first `.ofExprs` site (pure same-row reads of flags/product/msb cells). * Completeness rewires through `populateFE_eval_cell` + the new `hsum13` one-hot val-bound (the sign-selector premise); `eval_opBVal`/`eval_opCVal` land in Defs; structural/Faithful simp lists drop the retired native combinator names. * `MulChip.computableWitnesses` (7 slots): flags close from `AgreesBelow.hint_eq`, the struct from `populateFE_congr_flat` + three same-row `get_eq`s, the `.ofExprs` word cell-by-cell via `getElem_eval_ofExprs` + `get_eq` chains. Axioms: the pure three plus Mul's own already-disclosed `bv_decide` constants (inherited through the `circuit` bundle, identical to `MulChip.circuit`). Gates: full build 0/0, Mul trace anchor + MulOperationWitness battery pass UNMODIFIED (the byte-for-byte semantic gate on the swap), audit census clean, lint clean, root index 449, Exportable pins 54 witness cells. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…nts land Converts ShiftLeftChip's nine escape-hatch witness payloads in-place (guard census 86 → 77; the hatch now lives only in ShiftRight and DivRem): * Nine IR twins in `Populate.lean` § Witness IR: the subtraction-free split modulus `2^(16−bitShift)` is `65536 >>> s` (`Nat.two_pow_shiftRight` from ToMathlib closes the ℕ side), the power encodings are `1 <<< (c & m)`, and `populateA`'s variant dispatch is one `.listGet` per cell over the u64 byte-shift index (in range by `byteShiftNat_lt`) with the SLLW branch's `.ite`-placed low pair + `populate_msbF · 65535` sign fill. * Nine eval lemmas: `aF_eval` resolves the flag/byte-shift dispatch cell by cell (`set … clear_value` so the match scrutinee generalizes; the SLL match closes by `norm_num [← hkeq]`, the two-condition SLLW splits kill contradictory branches by omega). UInt64 shift semantics normalize manually — the `% 64` mask and variable-exponent `% 2^64` wraps are outside the wrap simproc's omega reach. * Ten congr twins (bounds-free, `-Witgen.u64Wrap`), incl. a local `evalList` pointwise congruence for the `.listGet` cells. * `witnessPrefix` swaps all nine `.witness n (.native …)` payloads in place; the WitgenIR-quantified structural lemmas survive unchanged. A/B gate: Defs 5.98s vs 6.01s baseline, Formal 6.26s vs 5.2s (the family eval haves), within noise of the 135-site `circuit_norm` risk the plan flagged. * Completeness rewires by nine family-eval rewrites at the pinned obligations — the value-level pin block below is untouched. * `computableWitnesses` (16 slots: CPUState + 9 payloads + U16MSB + ALUTypeReader + RegisterWrite + two flattened Equality gates + Core tail), axioms pure `[propext, Classical.choice, Quot.sound]`; operand projections `eval_opBPrev`/`eval_opCPrev`/`eval_immC` land in Defs. Gates: full build 0/0, ShiftLeft trace anchor passes UNMODIFIED (the hint-driven byte-for-byte semantic gate), audit census clean, lint clean, root index 450, Exportable pins 33 witness cells. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…traction
Converts ShiftRightChip's eleven escape-hatch witness payloads in-place
(guard census 77 → 66; the hatch now lives only in DivRem):
* Eleven IR twins in `Populate.lean` § Witness IR: the split modulus is
`2^bitShift = 1 <<< s`, the inverted powers `{65536,256,16} >>> (c&mask)`,
the *effective* top limbs carry the `(is_srl+is_sra)` field factor through
`FExpr.val` (their wrap-drops need the one-hot bound), and the arithmetic
sign fill `m·65536 − m·2^(16−s)` takes the subtraction-free u64 form
`m·((65535/v)·v)` for the power-of-two `v` (the `hfill` identity closes by
`clear_value` + 16-case `interval_cases`/`norm_num`). `c_bits` reuses
`ShiftLeftChip.cBitsIR`.
* The eval ladder handles the two-modulus recombination (`higher[i] +
lower[i+1]·2^(16−s)`) with explicit per-cell wrap-drops — variable-power
products are outside the wrap simproc's omega reach, and `% 2^(c&15)` is a
variable modulus omega rejects outright (`congr 2` strips it). `aF_eval`
resolves the 64-bit diagonal placement (`.listGet` + `norm_num [← hkeq]`)
and the word branch's placed-limb MSB via `populateA_val_lt`-transported
bounds.
* Full congr ladder incl. an `evalList` pointwise congruence; the word
branch's fill terms close pointwise (`circuit_norm` distributes the sums
before compound facts can match).
* `witnessPrefix` swaps all eleven payloads in place. A/B gate: Defs 7.41s
vs 7.51s baseline (the 27.6s Formal "baseline" was a polluted measurement
— it included the Defs rebuild; the rewired file elaborates in ~6s).
* Completeness rewires by eleven family-eval rewrites; the flag facts the
sign selectors need (`he14`/`hone`/`hsum01`) derive up front from the
chip's one-hot assumption via `one_hot_resolve`. The three `set` aliases
come FIRST — abstracting the enlarged context afterwards was the whnf
blow-up (the fold rule: keep the context the sets traverse small).
* `computableWitnesses` (22 slots: CPUState + 11 payloads + 3 U16MSB +
ALUTypeReader + RegisterWrite + 4 flattened Equality gates + Core tail),
axioms pure `[propext, Classical.choice, Quot.sound]`.
Gates: full build 0/0, ShiftRight trace anchor passes UNMODIFIED, audit
census clean, lint clean, root index 451, Exportable pins 37 witness cells.
This closes A6 — every chip except DivRem now generates witnesses on the
exportable IR.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The `srem_eq_bvAbs` twin the DivRem witness-IR conversion is built on (campaign plan A7's front-loaded first item): `BitVec.sdiv` repackaged on `bvAbs` magnitudes with the msb-XOR sign, width-generic, one `cases`-pair over `BitVec.sdiv_eq`'s four-case form. Public (the IR eval ladder will cite it from the twin layer). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…s, ctq product block, sub-op FExpr twins The exportable-IR substrate for the DivRem conversion (the terminal A-track wave), all proof-complete with the value layer: - Populate/IR.lean: the u64 dispatch calculus (negU/absU/sdivU/sremU, the width-32 embedded family, low32U/sext32U, wordU, the derived flagF hint flags) with per-builder toNat lemmas, and the quotBitsU/remBitsU dispatch evals (one flat simp + split_ifs; the umod leaves close by manual rfl+rw chains — a circuit_norm toNat_mod push cascades into a kernel deep recursion, the `/` twin does not). - Populate/IRWord.lean: wordFOfU64 (the wordOfBits unpack), the bComp/cComp toBitVec64 characterisations, compU/compF operand dispatches, quotCompBitsU/remCompBitsU. - Populate/IRCtq.lean: the 128-bit c_times_quotient block in the u64 sort — umulhU (textbook four-half decomposition), ctqHiU (signed corrections via negU, the mulh-from-umulh identity), ctqLimbU/ctqLimbF with evals against populateCtq. The operand values enter as opaque fvars (obtain, not `set` — kernel-size discipline: set-lets over the product words recurse the kernel). - Populate/FE.lean (in progress): 17 of the ~30 site payloads with eval lemmas (flags, the six result/comp words, the four msb cells, the three sign scalars, abs_c/abs_remainder/ max_abs_c_or_1). - Sub-operation FExpr-word twins beside their operations: MulOperation.populateFEW (+eval, +congr_flat; the stream/chain ladder is shared), AddOperation.populateFW, IsZeroOperation/IsZeroWordOperation/IsEqualWordOperation.populateFE (+evals, +congrs). Full build 0/0, lake test green (trace anchors unmodified), audit census clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…payload combinators, and the one-time zero-struct navigators The small generic layer that cracks the nested-ProvableStruct flatten wall for the DivRem struct sites (empirically validated at default heartbeats before landing): - ToClean/Circuit/WitgenEval.lean (new, Clean-only imports — an upstream PR unit): Witgen.toElements_eval + Witgen.getElem_eval_toElements (the ProvableType-generic counterparts of Clean's Expression.eval versions; both definitional one-liners) collapse every per-cell fact about a flattened struct payload to one rewrite plus the payload's struct-level eval lemma — no per-struct navigator family needed for evaluation. And Witgen.gateFE / Witgen.iteFE lift the prover idiom `if is_real = 1 then populate … else zeroCols` to the struct level, with eval lemmas producing the value-level `if` directly (defined independently of each other: defining one via the other would cross the toElements tower of a compound literal definitionally — the whnf cliff). - IsZeroWordOperation: eleven toElements cell navigators (the MulOperation technique), consumed only by zc_cell (every flattened zero-struct cell is zero) and fromElements_zero; IsEqualWordOperation: toElements_mk (the single-field wrapper flattens to a cast of its field's flattening — kills the nested tower in one rewrite) + zc_cell + fromElements_zero; MulOperation: zc_cell + fromElements_zero via its existing navigators. These are the gated-composition else-branch facts eval_gateFE's replicate-zero form lands on. Full build 0/0, root index green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…gation words, misc, and the remainder-check block
Twelve more site payloads with eval lemmas in Populate/FE.lean (the b/c sites need no new
definitions — IRWord's compF serves them directly at the swap):
- the overflow result cells ovbResFE/ovcResFE as toElements-cell-10 reads of the gated
IsEqualWordOperation payloads (via A7c's Witgen.getElem_eval_toElements + the op-level
result_eq_toElements bridges; the ite shells are handled fully manually — rfl-unfold,
BExpr.eval_feq_iff-derived feq_true/feq_false condition helpers, if_pos/if_neg — because
the mixed circuit_norm route loops in the fields-projection machinery on nested projections);
- isOverflowFE and the seven-cell scalFE;
- ctqFE (assembly over IRCtq's ctqLimbF at the computational quotient and operand packs);
- isC0FE (ungated flat IsZeroWordOperation payload over compF) and ltGateFE
(is_real · (1 − is_c_0.result));
- wCnegFE/wRnegFE (cell-gated AddOperation.populateFW words) and the three-cell miscFE;
- the remainder-check comparison block clFE/ltfFE/neiFE/bitFE, all four families off ONE
shared LtOperationUnsigned.scanF_eval application over (absRemFE, maxAbsFE) under the
shared gate.
Also: IsZeroWordOperation.result_eq_toElements / IsEqualWordOperation.{toElements_mk (now
F-generic), result_eq_toElements} — the public faces of the navigator family for result-cell
reads. Full build 0/0.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…product/overflow structs The last of the 30 site payloads, all with eval lemmas: - mulLowerFE/mulUpperFE: Witgen.gateFE over MulOperation.populateFEW at the computational quotient/operand packs (upper gates on `is_real ∧ 64-bit-class` via BExpr.and, running the signed stream at `flagF 0 + flagF 2` — its binarity enters as the contract-provided hypothesis); the else branches land on MulOperation.fromElements_zero. - ovbFE/ovcFE: gateFE ∘ iteFE with the W-truncated and full IsEqualWordOperation.populateFE branches; eval_gateFE's RHS exposes the iteFE evaluation verbatim for eval_iteFE. - The carry chain: remAddendU (dif on the word boundary: committed remainder_comp limb below, sign fill `.val remNegFE · 65535` above — the sign value's ≤ 4 bound under flag binarity keeps the u64 `.val` truncation honest) + carryChainU (authoring-time recursion) + carryChainU_toNat, ONE conjunction-motive induction carrying the ≤ 5 bound so wrap-freeness at each step needs no external re-derivation. Full build 0/0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The ComputableWitnesses counterparts of the Populate eval lemmas: every payload's environment-locality over the operand reads, is_real, and the div_rem_flags hint. Most sites are one flat same-tree simp (leaf facts in the same pass that forms the dispatch conditions — a later pass cannot reach leaves under the baked Decidable instances). The struct-read and scan sites are compositional per srwMsbIR_congr's discipline: IsEqualWordOperation.populateFE_congr / LtOperationUnsigned.scanF_congr / carry addend+limb helpers instantiated as haves over folded sub-payloads, with the is_overflow cells routed through an explicitly instantiated Witgen.getElem_eval_toElements and closed by if_congr + exact (the struct-eval terms match only up to instance paths). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Completes the DivRem congr layer for the four struct-shaped sites the CW file consumes at the flattened level: mulLower/mulUpper (gate condition + the flat MulOperation battery transported through the new bridges) and ovb/ovc (gateFE/iteFE + IsEqualWordOperation.populateFE_congr, closed per-cell through an explicitly instantiated getElem_eval_toElements). ToClean/Circuit/WitgenEval.lean gains the three M-generic transport lemmas (cell-from-site, struct-from-flat, flat-from-struct) — the same upstream-gap family as the A7c collapse pair. Baked-Decidable condition residues close instance-agnostically via decide_eq_decide. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e IR The terminal A-track port (30 sites / 217 cells). populateRow's closures become witnessVectorIR payloads (the two product structs via witness (var := Var Extracted.MulOperation) on the gateFE twins; ovb/ovc flat through the toElements cast; msb cells as one-cell vectors), with populateRow_output_eq reduced to the plain circuit_norm simp — 5.5s against the 39s native baseline. The eight structural simps take Witnessable.witness_provable (the projection rfl-lemma; the bare class projection is inert in simp). The completeness Driver rewires all 30 pins through one block of named-argument site-eval instantiations, with the struct pins on dsimp + trans/exact chains that never simp the big hypothesis. New Witgen.lean proves ComputableWitnesses from the A7f congruence layer ([propext, Classical.choice, Quot.sound]); Exportable gains the pinned 217-cell entry and loses the deferral rationale. The DivRem trace anchor passes unmodified — the native_decide byte-for-byte re-derivation through the IR path is the semantic gate on the swap. Escape-hatch census 66 → 23 (all remaining sites are A8 plumbing). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
With the DivRem port landed, the last witnessNative plumbing goes: the four CircuitNormalization shim lemmas (CircuitProofStart.lean — their call sites all died with the per-chip token swaps), the four TypedProgram localLength/interactions lemmas, and the two stale prose mentions. check_no_witness_native.sh now runs --enforce in run_audit.sh and the CI guards job: any future .native witness site fails the build. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
scripts/witgenExport.lean serializes all 25 chip circuits at SP1Prime in Clean's version-1 witgen wire format (witness programs + the complete assert/lookup/ interact list) plus a per-chip manifest carrying what the wire omits (field modulus, input width, chip name, hint schema — derived by walking the payload) and an index.json, all in supportedChips registry order with a startup cross-check. Driver is an interpreted script (WITGEN_ARGS=... lake env lean scripts/witgenExport.lean): lean --run is unavailable because the generated Sail model owns the root main, and a lean_exe would native-compile the whole import closure for nothing. The Clean pin advances to the fork's witgen-share merge (2dad7788): WitgenIR.share interns every distinct non-trivial subterm as a let-step, with the eval-preservation theorem WitgenIR.eval_share proved axiom-clean — without it the wire format expands shared subterms into trees and DivRem's witness programs serialize to 1.22 GB (two ops at 552 MB); with it the committed payload is 1.04 MB and the whole 25-chip export totals ~2.3 MB, byte-stable across regenerations. scripts/check_witgen_export.sh gates the committed tree: structural mode (enforcing, no toolchain needed) joins the CI guards job and run_audit A2; --regen byte-diffs a fresh export in the CI test job where the SP1CleanTest oleans are warm, so golden drift on a pin bump is caught automatically. Fork-delta disclosures updated in docs/release-audit.md and docs/agents/clean-upstream.md (branch witgen-share, queue entry U11). Gates: full build 0/0, lake test (trace anchors unmodified), run_audit PASS both scopes, lake lint, exporter run twice byte-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Written from the committed export/witgen artifacts. Documents: the envelope and four operation forms; the four expression sorts with the sort-directed parsing rule (type tags collide across sorts) and the three wire-tag/ctor-name disagreements (u64Eq is equality, u64Lt vs lt, field lt); the totality semantics an implementation must copy (0⁻¹ = 0, u64 x/0 = 0 and x%0 = x, shifts masked mod 64, localVar sort-mismatch/OOB → 0, listGet OOB → 0, missing hint → zeros); the evaluation loop as a transcription of Circuit.witgen; steps sharing and the proven-eval-preserving share pass behind the committed payload sizes; manifest/index schemas; byte-stability and the pin-bump runbook; the SP1-specific facts (hint-only, eight tables at row 0, zero-default = padding). The doc joins check_report_citations.sh's gated list and the docs index; rust/README.md's reference to it now resolves. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
scripts/witgenExport.lean gains --testdata: per-chip trace.json fixtures with honest per-row provenance. The ten trace-anchored chips get one row per SP1-dumped executor event — inputs via the EventPopulate flatteners, hints via the per-chip builders from the dumped opcode, expectedRow copied verbatim from SP1's real generate_trace output (whose equality with the circuit derivation the native_decide anchors pin, named in the provenance block) — plus an honest padding row: anchored for the chips whose padding SP1 derives by populate (ShiftLeft/ShiftRight/DivRem, the latter's is_divu template reproduced from the absent hint key), unanchored zero-input rows for the zero-fill chips. All 25 chips additionally carry deterministic seeded synthetic rows (an LCG; committed fixtures must be byte-stable) with 0/1-valued schema-derived hint tables. expectedWitness is always the Lean reference evaluation (FlatOperation.witgen) over the SHARED operation list — the same programs the wire carries, justified by WitgenIR.eval_share. 684 KB across 25 fixtures (10×50 + 15×5 rows); generation 24 s (DivRem's share pass dominates); regeneration byte-identical. check_witgen_export.sh now validates testdata structurally (row widths against the manifests) in the default gate and regenerates + byte-diffs both trees in --regen; the wire format doc gains the fixtures section. The Add fixture's expectedWitness was independently cross-checked against a hand-computed u16-limb carry chain. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
rust/witgen-interp becomes real: a self-contained interpreter for the version-1 wire format (docs/witgen-wire-format.md), one dependency (serde_json, Value level only). Five modules: field.rs (a minimal Field trait — the wire needs +, ·, inv with 0⁻¹=0, canonical value, and reduction; no subtraction node exists — with KoalaBear as naive u64-mod arithmetic and Fermat inverse), wire.rs (sort-directed manual parser; case names follow the WIRE TAGS so the u64Eq-is-equality / u64Lt / lt naming traps cannot bite; errors carry JSON paths), eval.rs (a transcription of Circuit.witgen with the totality conventions: x/0=0, x%0=x, shifts masked mod 64, localVar sort-mismatch/OOB → 0, listGet OOB → 0, missing hint/data → zeros, mapRange binds idx, envRange absolute, bitsOf field-level; per-op spans recorded for mismatch attribution), fixtures.rs (the differential runner; failures name chip / row / cell / the originating witness op), main.rs (check --export-dir [--chip] [--verbose], exit 0/1/2) + lib.rs and tests/conformance.rs (the battery as a cargo test). Results: all 14 trap unit tests pass, and the full differential reproduces all 575 fixture rows across the 25 chips exactly — including DivRem's 217-cell rows — on the committed export. Failure injection verified loud: a corrupted cell reports 'DivRem row 3 (event): cell 17 expected 2 got 1 (witness op #3, local cell 1)'. cargo fmt and clippy clean. scripts/run_interp_diff.sh wraps the run (--regen re-verifies the export first; cargo stays out of the Lean CI); rust/README.md gains the runbook. No SP1-specific types or names in src/ — the crate is deliberately upstreamable toward Verified-zkEVM/clean#404. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ecks, throughput What a final full product requires, prototyped end to end: 1. Row maps. The ChipFaithful reconfigure functions are fully polymorphic struct re-wirings, so applying them at the Expression level yields each chip's complete symbolic Rust row — exported as <Chip>.rowmap.json (one Expression per Rust column over absolute cell indices; 25 files, byte-stable, gated by check_witgen_export.sh). The interpreter evaluates them after witgen and now RECONSTRUCTS FULL SP1 TRACE ROWS: all 444 anchored fixture rows (10 chips × 44 events + the 3 derived padding templates) match SP1's dumped generate_trace bytes column-for-column, 33-246 columns each. 2. Self-checking. The payload's assert operations now parse with their bodies and every constraint (17-321 per chip) is checked = 0 on every anchored row — a per-row AIR check in Rust from the same artifact. Interaction bodies parse too; per-row bus sends are counted (Add: 12 SP1Byte sends/row, DivRem: 4327 total), demonstrating the byte-multiplicity dependency accounting is derivable from the export with no extra artifact. 3. Throughput (single-threaded, witgen + full row, bench subcommand): Add 2.08M rows/s, Bitwise 902K, Mul 413K, ShiftRight 339K, DivRem 34.8K — the sharing pass puts an interpreter in a usable class for conformance and checking-prover use; IR-to-Rust codegen remains the lever for prover-grade trace generation. Full differential still green (575 rows, 14 unit tests, fmt+clippy clean); export regeneration byte-identical; wire doc gains the row-map section. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…patch mechanism The extraction provenance moves from overlay-plus-dirty-patches to a fully committed branch: SP1_SEMANTIC_COMMIT -> f66b4bff5 (the v6.4.0 release tag; semantic delta from v6.3.1+8 is three core/executor plumbing files, zero chip/ compiler/hypercube changes) and SP1_PINNED_COMMIT -> de017f475 (succinctlabs/sp1 branch dtumad/lean-extraction, five clean commits on the tag: IntoShape derives, field-generic IR, whole-chip extraction, style, and the new chip_traces dump binary). - update_extracted.py: verify_extractor_patch, the patch digests, and scripts/extractor-patches/ are deleted; verify_extractor_clean requires a clean checkout instead (every extraction change is an ordinary commit). verify_extractor_overlay is unchanged and passes against the branch (merge base + changed-file allowlist + derive-line-only machine diff, re-verified independently). - Extracted/: full EXTRACT_AIR_ONLY regeneration at the new pin is byte-identical across all 60 generated modules except Provenance.lean, which drops the patch-digest field and records the new revisions. - CoreProfile: sp1SemanticRevision/sp1SemanticDescription -> v6.4.0 (the rfl tie to the extracted provenance still closes). - Docs: pin tables and quotes updated (release-audit row renamed to "SP1 extraction branch", patch-digest row dropped); extraction.md rewritten off the overlay/patch mechanism; v6.3.1 doc-comment labels relabeled to v6.4.0 in 25 hand-written files (honest: the extracted AIR is byte-identical at both revisions). Gates: lake build SP1Clean (3672 jobs), lake test, run_audit.sh (both census scopes stable), lake lint, check_pins, check_witgen_export all green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
export/sp1dump/ (25 <Chip>.dump.json + index.json, 1.3 MB) is the SP1-side
conformance anchor for the dump-based fixture pipeline: deterministic per-chip
event batteries plus the full padded generate_trace row matrix, produced by the
chip_traces binary committed at the extraction pin.
- scripts/update_sp1_dumps.sh: the sole writer. Fail-closed fences before any
cargo run: $SP1_DIR must be exactly SP1_PINNED_COMMIT (read from
update_extracted.py, the single source of truth) with a clean worktree.
--check regenerates into a temp dir and requires byte-identity (verified:
PASS at the pin, so the committed dumps are reproducible).
- index.json records {schemaVersion, sp1Commit, chips}; check_pins.sh gains
the sp1Commit == SP1_PINNED_COMMIT cross-check so dumps and extracted AIR
can never describe different Rust trees.
- check_witgen_export.sh gains validate_sp1dump (always-on structural: 25
dumps parse, rows match the declared width x height, index consistent) —
runs in the CI guards job and run_audit like the other export trees.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…tion-time gate
`--testdata` is rewritten off the committed SP1 trace dumps: all 25 chips now
carry SP1-anchored event rows, each one recomputed at generation time and
matched cell-for-cell against SP1's real generate_trace output before anything
is written.
- Inputs are recovered from the dumped rows through the symbolic row maps
(every native input cell is a bare var column of the Rust row, except
is_real on the six flag-hinted chips, 1 on event rows — fail-closed against
row-map drift). Hint tables derive from the event's opcode discriminant;
Branch additionally derives its is_branching bit from the operand values,
mirroring branch/trace.rs exactly. The 10-chip TraceWitness import battery
and anchoredData are gone from the exporter.
- THE GATE: every event row and every derived padding row (ShiftLeft/
ShiftRight/DivRem) is recomputed via FlatOperation.witgen over the shared
operations + row-map evaluation, and must equal the dumped row cell-for-cell
(throws with chip/row/column detail); zero-fill chips' dumped padding is
asserted all-zero; a value-level circuitTraceRowMapped spot check pins the
Expression-level path on event row 0 of every chip.
- The gate immediately caught four real populate divergences on previously
unanchored chips: SP1 populates the op_a link/result word only when rd != x0
(jal/jalr trace.rs, utype mod.rs) while our circuits witnessed it
unconditionally. Fixed by AddOperation.populateIRGated (an op_a_0-gated
witness payload mirroring SP1's `if !op_a_0 { populate }`; asserts unchanged,
so ChipFaithful and all soundness proofs are untouched) with eval_off/
eval_on/congr lemmas, wired into the three chips' mains, completeness
drivers (which already assume op_a_0 = 0), and CW proofs.
- Differential coverage grows from 575 rows / 444 anchored (10 chips) to
857 rows / 706 anchored (25 chips): the Rust interpreter reproduces every
row, reconstructs every anchored full SP1 row through the row maps, and
checks all constraints = 0 on it. Regeneration is byte-stable.
- docs/witgen-wire-format.md fixtures section rewritten for the new anchored/
provenance semantics.
Gates: lake build SP1Clean (0/0), lake test, run_audit.sh (censuses stable),
lake lint, check_witgen_export.sh --regen, run_interp_diff.sh all green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…eir pipeline
The 21 native_decide conformance anchors (11 operation witness anchors + 10
whole-chip trace anchors) and their machinery retire in favor of the
dump-anchored pipeline landed in E1b/E2: committed chip_traces dumps at the
extraction pin, the fail-closed generation-time gate over all 25 chips, and
the Rust interpreter differential. The successor is strictly stronger —
25 chips instead of 10, reproducible dump provenance instead of frozen
unreproducible vectors (audit finding F-R-01 dissolves), and CI-resident
regeneration instead of a native_decide battery.
- Deleted: SP1CleanTest/WitnessTests/ (23 files) and the 20
TraceGenTests/<Chip>ChipTrace{Vectors,Witness}.lean batteries. Kept:
Exportable, NonVacuity (SP1Prime repointed to Exportable), NonVacuityReal,
Audit, and the TraceGenTests substrate (TraceGenerator/EventPopulate/
Conformance — consumed by the real-row anchors and the exporter's spot
check); docstrings updated for the new role.
- update_extracted.py: the witness/trace registries, renderers, passes, and
the now-vacuous EXTRACT_AIR_ONLY flag are gone (−296 lines); the script
emits AIR artifacts only. Full regeneration at the pin re-verified
byte-identical across all 60 modules.
- Gates moved in lockstep: option_escapes_allowlist drops its 3 retired
entries (exact-set gate), gen_axiom_probe drops the retired glob (test
census 58 -> 37 probes, total 524 -> 503; snapshot regenerated),
check_witgen_export's olean probe repoints to Exportable, README/
axiom-ledger/overview/release-audit counts updated.
- Docs: AGENTS.md test-layer description, extraction.md pipeline diagram and
future work, verification-report §4.1/§4.3 (F-R-01 closure) and §9
(conformance = the dump-anchored gate + differential), release-audit
native_decide disclosure, roadmap regeneration checklist.
Gates: lake build SP1Clean (0/0), lake test, run_audit.sh (main census
unchanged, test census updated deliberately), lake lint,
check_witgen_export.sh all green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- rust/README.md: the interpreter description now covers the row-map full-row reconstruction and per-row constraint checks; differential count 575 -> ~857 (706 SP1-anchored, all 25 chips). - run_interp_diff.sh header: all 25 chips carry SP1-anchored event rows (the "ten trace-anchored chips" wording predated E2). - docs/roadmap.md P3: records that the generate_trace connection now exists at conformance strength (wire-format export + dumps + the fail-closed gate + the Rust differential); the proved-construction completeness target stays open; drops the stale "batteries remain regression tests" clause (they were retired in E3). - AGENTS.md: fix the dangling "roadmap W12" pointer (an older roadmap scheme). - docs/agents/clean-upstream.md: add the missing U11 section body (the witgen-share branch was the only queue entry with no writeup): the sharing pass + eval_share sizes and shape, the two riders the PR should carry (field Hashable instance, the wire-format doc), and the note that U11 is the single Clean-side prerequisite for stock-upstream artifact production. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
New rust/witgen-interp/src/check.rs, the pure module an SP1-side conformance
test will share verbatim with the fixture differential:
- check_row(program, row_map, inputs, hints) -> RowCheck { cells, spans,
rust_row, constraint_failures, sends }: witness generation, full-row
reconstruction through the symbolic row map, every assert evaluated, and
nonzero-multiplicity interaction channels collected.
- derive_inputs(row_map, input_width, row, is_real_hinted, is_real): the
row-map inversion (bare-var gather with the six-chip is_real rule),
fail-closed on any other unmapped input cell — the Rust twin of the Lean
gate's inversionOf/invertInputs.
- first_mismatch + 5 unit tests (recovery, is_real rule, fail-closed gap,
width guard, earliest-mismatch).
fixtures::run_chip now delegates to check_row — behavior-identical (the
differential reproduces all 857 rows with the same per-chip reports). The
hint-context convention is now documented and structural: witness generation
reads the real hints; the row map and assert/interact expressions are
Expression-sort (no hint/data nodes) and evaluate against empty tables,
matching the Lean gate's hint-free rowValsOf. Also a FixtureRow type alias
for the clippy type-complexity warning that surfaced with the current
toolchain.
Verify: cargo test (19 unit + conformance), clippy 0 warnings, fmt clean,
scripts/run_interp_diff.sh 857/857 rows byte-identical reports.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Writes the memo rust/README.md has pointed at since D4b (previously a dangling reference): the two-implementations/one-comparison-chain framing, the exported artifact set, today's Rust-to-Lean conformance pipeline and what its gate has caught, why witness generation is the safe (completeness-side) thing to share, the proposed inversion (a conformance test inside SP1's workspace running check_row/derive_inputs against live generate_trace rows), the versioning contract, and the eventual generated-populate end state. Indexed in docs/README.md. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The U11 witgen-share branch on dtumad/clean now carries its two PR riders as ordinary commits (branch = 4 commits off upstream 0e53b9f2, fork-only): - 86f35a74: scoped Witgen.instHashableOfVal (canonical-value Hashable for any FiniteField), so Operations.witgenJsonShared? is callable stock — scoped to never shadow a type-specific downstream instance. Verified: the fork's WitnessShare/WitnessExport build green. - d8a2dc36: doc/witgen-wire-format.md for Clean's doc/ — the serialized contract had no upstream spec (witgen-authoring.md covers the authoring surface only); adapted from this repo's spec with the SP1-specific sections removed, and witgen-authoring.md's dangling witgen-ir-plan.md pointer fixed. sp1-lean side: docs/agents/upstream-drafts.md is the repo-resident, refreshed issue + PR text (857-row differential state, the riders, the #404 interpreter offer, filing commands, and the post-merge checklist: re-pin, open scoped Witgen in the exporter, repoint the wire doc's normative paragraph). POSTING REMAINS OWNER-GATED. clean-upstream.md's U11 entry and the agents index updated to match. The sp1-lean Clean pin is unchanged (sp1-integration @ 2dad7788 — the riders live on the branch only). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…tree
Sole writer of sp1/crates/core/compiler/testdata/lean-witgen/: copies the
committed export/witgen/ (byte-identical, enforced by --check) and stamps a
provenance.json sidecar {sp1LeanCommit, cleanRev, wireVersion} at vendoring
time — attribution lives in the sidecar precisely so the artifacts
themselves stay revision-free and byte-stable. Refuses to stamp from a
dirty export/witgen tree.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
SP1_PINNED_COMMIT -> 2b7ce1442 (dtumad/lean-extraction, v6.4.0-9): the four new commits expose the chip_traces battery layer as a library, vendor the witgen-interp reference interpreter + the exported artifacts (testdata/lean-witgen with a provenance sidecar), add the in-repo witgen_conformance test (all 25 chips: live generate_trace rows reconstructed from the verified generators, cell-for-cell + constraints=0, in SP1's default cargo test --workspace scope), and clear two clippy warnings in the IR emitter. The root Cargo.toml joins the extraction-tooling allowlist (the vendored workspace member). Verified at the new pin: extraction regen byte-identical (Provenance strings only), dumper output byte-identical (only index.json's sp1Commit moves), fixtures re-gated (provenance strings only), lake build/test, run_audit both scopes, check_pins, vendor --check, and the 857-row differential all green. docs: release-audit pin row, extraction.md branch range + future-work (the upstream PR now ships the conformance test; seam-A retirement stays gated on that test running in authoritative SP1 CI). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…print Per the hardening-first decision: the inverted check must not touch SP1's CI in any way until the artifact-sync protocol is agreed. On the extraction branch (pin advanced to b5616f908c, v6.4.0-10) the check moved from a cargo integration test — which cargo test --workspace would have run — into crates/core/compiler/conformance-check/, a standalone package with its own cargo workspace, excluded from SP1's. The vendored witgen-interp moved out of the workspace member set with it (cargo makes a path dependency of a member a member even against exclude, so the dependency edge had to leave the workspace too). Verified: no witgen/conformance package appears in SP1's workspace_members; cargo build / cargo test --workspace there builds and runs none of it; the only conformance-related code in the workspace build is the inert battery library. sp1-lean gains the sole driver, scripts/run_sp1_conformance.sh: pin fence + clean-worktree fence + vendored-artifact byte-identity check (vendor_witgen_artifacts.sh --check), then the standalone check via --manifest-path with a shared target dir — all 25 chips reproduce generate_trace, exit 1 on any mismatch. Deliberately in NO CI on either side; promotion into SP1 CI is the later hardening step and remains the S5 retirement trigger. Pin dance re-run at the corrected hash (the first attempt used a misremembered tail and the fail-closed fence caught it): extraction regen byte-identical (Provenance strings only), dumps identical except index.json sp1Commit, fixtures re-gated (provenance strings only). Docs: rust-integration-memo §4 (the check exists today, opt-in, promotion criteria), extraction.md future-work + branch range, release-audit pin row. Gates: run_sp1_conformance.sh 25/25, lake build/test, run_audit both scopes, check_pins, run_interp_diff 857/857 all green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…the queue Before filing anything upstream we read the Clean maintainer's in-flight work end-to-end. Three corrections and one deletion follow from it. What we found (recorded in clean-upstream.md's new "Clean's direction (2026-08)" section, with evidence): - Clean is not abandoning the witness IR — it is abandoning the JSON *runtime interpreter*. #446 deletes the Rust JSON backend (-10,301) and the Lean-spawning harness, but WitnessExport.lean survives and is maintained in lockstep; the stated policy keeps JSON as a diagnostic, not an evaluator. - Their codegen makes subterm sharing MORE valuable: Clean/Air/Extraction reuses the witness IR directly, renders each Step one-for-one as a Rust `let`, and does no CSE anywhere in the pipeline. So U11 is re-scoped from "shrinks the JSON" to "shrinks and speeds up the generated Rust", its wire-format-doc rider is withdrawn (it stays ours), and the rebase debt is itemized: three new FExpr constructors, evalSteps' new idx/proverInput parameters, and the idx question that #446's RowProgram opens (its steps evaluate at idx := row, which falsifies our `.idx -> const 0` premise there while leaving it sound for WitgenIR). - U1 is not "not yet filed": it is PR #450, approved 2026-08-14, pending merge. Recorded with the conjunct-order divergence from #426 and the fact that DataWitness.lean's falsity proof exists only in #450. - U10 shrinks: #426's branch already has `size_fields`, but tagged `@[grind norm]` only, so it never fires under simp only [circuit_norm]. The ask is one attribute, and if it lands WitnessCombinator is deleted rather than upstreamed. - #451 is upstream's (better) answer to our recorded struct-eval orientation problem, so our 303-occurrence census becomes input for it, not a new issue. Deleted ToClean/Circuit/WitgenCongr.lean (406 lines, zero importers). It violated our own rule that ToClean residents must have live call sites, and it competes architecturally with the maintainer's computable_witnesses tactic, so it will not be filed. Recoverable from git history; the follow-up at the next re-pin is to check whether that tactic discharges what our five bespoke per-gadget congruence lemmas do. Also: the coming #426/#448/#451 migration is now scheduled work rather than a surprise (ofFExprs -> ofCompositeFExpr, the FormalCircuitBase computableWitnesses field, deletion of compose_computableWitnesses, and the new struct-eval normal form); InteractionRecovery gains the mandated ## Upstream section; the interpreter's copy-of-record is stated in rust/README.md; upstream-drafts.md is rewritten for the new reality. Gates: lake build SP1Clean+ToClean (3674 jobs), check_root_index (457 modules), run_audit --main-only. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e drift Local prep only — nothing pushed to succinctlabs/sp1 or sp1-private. The extraction series is rebuilt (in the sibling sp1 checkout, branch dtumad/lean-extraction-clean) from 10 working commits into 5 born-final Conventional-Commits commits based on v6.4.0, verified byte-identical to the original series (git diff between the two tips is empty). It builds, clippy and fmt are clean, the standalone conformance check passes 25/25, and cargo metadata still reports no witgen/conformance workspace members. docs/agents/sp1-upstream-draft.md holds the branch description, the PR body written to SP1's template, and the exact filing commands. The load-bearing finding is architectural. Rebasing that series onto sp1-private/main applies textually clean but does not build, and the reason is not mechanical: SP1's internal line has replaced the global-accumulation memory-consistency architecture with a Merkle-tree one. Measured against our v6.4.0 pin, RiscvAir loses Global, MemoryGlobalInit, MemoryGlobalFinal, PageProtGlobalInit, PageProtGlobalFinal and all four Syscall* tables and gains MerkleTreeTraversal, LeafHash, LeafHashControl, HintRead and HintReadControl; six InteractionKind variants go with them. What carries over: all 25 instruction chips (no file under alu/, control_flow/, memory/instructions/, utype/ differs) and their four buses — the whole native-chip, ChipFaithful, advance/Sail, and grounding layer. What does not: the 6-table memory-boundary cluster and the syscall system tables, hence Extracted/SystemOracle/*, CoreAIRManifest, and the CoreProfile enum. Consequences recorded where they change decisions: extraction.md gains an "Upstream architecture drift" section with the measurements and the decision to stay pinned at v6.4.0 (public, released, externally reproducible, and in sp1-private's own history, so still a legitimate PR base there); roadmap P0 section 2 gains a sequencing warning, since several of its grounding bullets (Global's boundary facts, the syscall tables, page-prot) target tables upstream is retiring, while the Program/Byte/Range/MemoryLocal/MemoryBump/ StateBump bullets survive the redesign. Nothing proved becomes untrue — every claim is pinned to v6.4.0 — but the next increment should aim at the parts that carry forward. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
Stacks under #110 — base is
dtumad/v1.0-release, so this PR shows only the witgen campaign's 54 commits. Deliberately a draft: leaving it unmerged keeps #110's review scope frozen at what was already opened for review.What this is
Witness generation for all 25 instruction chips is now exportable data rather than opaque Lean closures, and that export is checked — cell for cell — against SP1's real prover.
Every chip's
mainbuilds its witness cells from Clean's witness IR (witnessVectorIR … populateIR …). The same term is what the chip's kernel-checked completeness proof witnesses, so the thing we export is provably the thing we proved about (populateIR_evalties the IR to the value-levelpopulate;spec_populateties that to the chip's semantic contract;Circuit.witgenprovably builds the environment the proofs quantify over). A CI guard (check_no_witness_native.sh --enforce) keeps it that way.The conformance chain
scripts/witgenExport.leanwrites, per chip: the wire-format witness program, the symbolic Rust row (the auditedChipFaithfulreconfigure map applied atExpressionlevel), and a manifest. Byte-stable;check_witgen_export.sh --regendiffs a fresh export in CI. Serialization goes through a proven-evaluation-preserving sharing pass (WitgenIR.eval_share), without which DivRem alone is 1.22 GB (1.04 MB with it).export/sp1dump/holds SP1's realgenerate_traceoutput (events + full padded matrices) for all 25 chips, dumped by a binary committed at the pinned extraction branch and reproducible byte-for-byte at that pin.--testdatarecovers each event row's inputs from the dumped row itself through the symbolic row map, re-runs the witness programs, evaluates the row map, and fails closed unless the reconstructed row equals SP1's row cell-for-cell. It re-runs in CI. It has teeth: on its first full run it caught that SP1 populates theop_alink word only whenrd ≠ x0(jal/jalr/utype) while our circuits witnessed it unconditionally — the Lean side was corrected to match.rust/witgen-interp(one dependency, no SP1 types, no Lean) re-runs the programs from the wire bytes alone over 857 fixture rows, 710 of them SP1-anchored across all 25 chips, reconstructs every anchored full row, and checks that every extracted AIR constraint evaluates to zero on it.generate_traceand checks it against the vendored verified generators (25/25). Deliberately outside SP1's workspace, so nothing in theircargo build/cargo test --workspacebuilds or runs it; driven from here byscripts/run_sp1_conformance.sh.Retirement
The 21 legacy
native_decideconformance anchors and their generated vector batteries are deleted (43 files), along with ~291 lines ofupdate_extracted.pymachinery and the uncommitted-patch extraction mechanism. The successor is strictly stronger: 25 chips instead of 10, reproducible dump provenance instead of frozen unreproducible vectors, and a fail-closed gate in CI instead of a battery. This also dissolves audit finding F-R-01 (the old batteries' dumper existed at no pinned revision; the new one is an ordinary commit at the pin).Census: 503 probed declarations (466 main + 37 test), down from 524.
Also here
docs/witgen-wire-format.md(the format spec) anddocs/rust-integration-memo.md(the SP1-facing integration story).docs/agents/clean-upstream.mdnow records what upstream Clean is actually building and what we will and will not send them.Reviewing this
The diff is 370 files / +284k, but ~268k of that is committed generated artifacts under
export/(witgen payloads, row maps, manifests, SP1 dumps, differential fixtures). The hand-written surface is roughly:SP1Clean/Proofs+6.7k (the per-chipWitgen.leancomputable-witness proofs),SP1Clean/Native+4.2k (IR payloads),rust/+1.9k,scripts/+1.4k,docs/+1.2k.CI adds three steps: two guards (
check_no_witness_native.sh --enforce,check_witgen_export.sh) and the--regenbyte-identity check afterlake test. No cargo in CI.🤖 Generated with Claude Code