Conversation
…y kernel replay (Verified-zkEVM#306) The KoalaBear degree-5 and degree-6 extension irreducibility proofs (`quinticPoly_irreducible`, `sexticPoly_irreducible`) type-check fine at compile time but are effectively unbounded to *re-check* from an empty environment (Lean's `Environment.replay`, as used by `lean4checker` and by external proof-auditing tools): the check grows past 58 GiB without finishing. Cause: the Rabin lemmas are stated in terms of `Fintype.card F`, and the callers bridge the concrete field size in with `rw [hcard]`. On a cold re-check the kernel is forced to reduce `Fintype.card (ZMod p)` -- an enumeration of ~p (~2.1e9 for KoalaBear) elements -- to reconcile it with the numeral. Compilation avoids this because the elaborator handles the equation propositionally; replay re-faces the raw defeq. (The huge `X^(card^k)` power is *not* the cause -- it stays syntactically matched and is never reduced; the `X^4-C` degree-4 extension, which has no such enumeration, re-checks fine at the same closure size.) Fix: add explicit-cardinality wrappers `irreducible_of_rabin_prime_degree_of_card` and `irreducible_of_rabin_degree_six_of_card` that take the field size as a numeral `q` with `Fintype.card F = q`, proved by `subst hq` from the existing lemmas -- so they are definitionally the same statement, no axiom, nothing weakened. The two callers pass `q := fieldSize` and drop the `rw [hcard]` casts, so the certificates are stated with `q` concrete and the kernel never enumerates `Fintype.card`. Measured on the degree-6 case: re-checking the full 19,908-constant closure goes from unbounded (>58 GiB, killed) to ~9 s. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…erified-zkEVM#307) The `_of_card` wrappers added in Verified-zkEVM#306 are correct, but their docstrings justified the numeral form by claiming the `Fintype.card F` form makes a from-empty kernel replay reduce `Fintype.card F` (for a `ZMod p` field, an enumeration of ~`p` elements). It does not: `rw [hcard]` elaborates to `Eq.mpr (id (congrArg motive hcard)) cert`, whose kernel check only beta-reduces the motive, so `Fintype.card F` never reaches whnf position. Measured kernel type-checking of both proofs is single-digit milliseconds either way, with run-to-run variance exceeding the difference between the forms; and since Lean kernel-checks each theorem at `addDecl` during an ordinary build, a from-empty replay runs that same check. Replace the rationale with the one that does hold, and that `irreducible_X_pow_four_sub_C_of_card` already documents on the binomial side: the generated certificates are already stated in terms of `fieldSize`, so each Rabin condition applies directly instead of needing a `rw [hcard]` cast. Also drop the claim that the two forms are "definitionally equal" — the plain form is the `q := Fintype.card F` instance of the numeral one. Make `q` implicit and rename `hq` to `hcard`, matching the binomial `_of_card` form: `q` is uniquely determined by `hcard`, which precedes `h_trace`/`h_cop`, so inference never needs higher-order matching. Update `docs/wiki/field-extensions.md`, whose "Adding a new non-binomial extension" recipe still routed new extensions to the non-`_of_card` wrappers that the two canonical callers had moved away from, per the maintenance contract in `docs/wiki/README.md`. Pin the round trip in `CompPolyTests.RabinCertificate`: instantiating each `_of_card` form at `q := Fintype.card F` with `rfl` must recover the plain statement verbatim, so "nothing is weakened" is checked rather than asserted. The opposite direction is the wrapper's own proof body. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…erified-zkEVM#305) `Multivariate/Wheels.lean` held two lemmas in the root `List` and `Option` namespaces with no multivariate content, which forced a cross-subtree import just to reach them. Move them to the repo's homes for generic lemmas and give them Mathlib-conforming names and proofs. - `List.distinct_of_inj_nodup` -> `List.Nodup.pairwise_ne_map` in `Data/List/Lemmas.lean`. The statement is `List.Nodup.map` transported along `List.pairwise_map`, so the induction, `aesop`, and `grind` collapse to a one-line term proof. - `Option.filter_irrel` -> `Option.filter_eq_self` in the new `Data/Option/Lemmas.lean`, generalized to `Type*` and restated as an iff to match `List.filter_eq_self` and `Array.filter_eq_self`. Proof is `cases o <;> simp`. `Multivariate/MvPolyEquiv/Core.lean` now imports `Data/List/Lemmas.lean` directly instead of picking the lemma up transitively through `Unlawful`. Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Alexander Hicks <25369263+alexanderlhicks@users.noreply.github.com>
…EVM#308) Co-authored-by: Derek Sorensen <derek.sorensen@ethereum.org>
* feat(fields): add Mersenne31 field scaffold * feat(fields): implement fast Mersenne31 arithmetic * chore(fields): add comments * refactor(fields): modularize Mersenne31 basic and fast implementations * doc(fields): add Mersenne31 to readme * test(fields): add Mersenne31 tests * fix(fields): export Mersenne compatibility module --------- Co-authored-by: Derek Sorensen <derek.sorensen@ethereum.org> Co-authored-by: Derek Sorensen <d@dhsorens.com>
…eline (Verified-zkEVM#300) * feat(scripts): kernel-level axiom sweep with committed regression baseline Add `lake exe axiomsweep`: walks the compiled environment and computes, for every CompPoly.* declaration, its transitive axiom dependencies — the #print axioms information, library-wide, in one pass. Reads elaborated .olean data, so private and macro-generated declarations are included and no source heuristics are involved. Baseline at this commit: 7589 declarations across 275 modules, 0 sorryAx-tainted, 0 non-standard-axiom-tainted — the library is fully kernel-clean, and --check now keeps it that way (fails iff a declaration is tainted that scripts/axiom_baseline.json does not list; the 6 'sorry' tokens greps report on main are all inside comments). Wire-up: report-only CI step in lean_action_ci.yml after the warm rebuild; docs/wiki/quickstart.md documents the workflow. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix(axiomsweep): adversarial-review fixes — fixpoint collector, floor, docs Collector: two-phase DFS + fixpoint repair. The one-pass DFS finalized self-referencing constants (every inductive/ctor pair) prematurely and memoized the wrong result for all later roots — confirmed by review to produce rows diverging from #print axioms on sibling repos. The repair pass re-derives every set in finalization order until stable: the least fixpoint = true kernel closure, strictly more accurate than #print axioms inside mutual families. Also: axiom *types* are traversed (CollectAxioms parity), duplicate constNames rows deduped (7589→7573), native trust-axiom names normalized to their owner (ax_N_M counters are Elab.async/toolchain-volatile), --check/--update-baseline mutually exclusive, unknown --root fails gracefully, nonstandard shrinkage detected, and bare Lean.ofReduceBool/Lean.trustCompiler are never baselinable (floor). Docs: known blind spots documented (structure-field defaults and examples never enter any environment walk; unimported files — paired with check_imports); scope stated (tests/ and bench/ outside the sweep); corrected sorry-token count (5, all comments); inventory rows added to scripts/README.md, docs/wiki/generated-files.md, AGENTS.md fast-start, quickstart CI mapping + lower-level commands. CI: infrastructure failures (exit != 1) now fail the step; only taint findings are report-only during the soak. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore(axiomsweep): rewrap overlong docstring line; annotate UInt32 literal for 4.30/4.31 portability Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * bug: test the CI sweep * fix: remove bug * fix(axiomsweep): enforce taint policy --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Derek Sorensen <derek.sorensen@ethereum.org> Co-authored-by: Derek Sorensen <d@dhsorens.com>
…VM#286) * feat(fields): initial fast binary towers (k <= 6) * test(fields): fast binary tower regression guards * docs(fields): fast binary tower rows in README and wiki * feat(fields): fast binary towers multiplication + proofs * feat(fields): fast binary towers mult, sqr and inv * feat(fields): field instance for fast binary towers * feat(fields): small optimizations for towers * feat(fields): port fast binary tower onto main (Lean 4.32, module system) Module headers on Fast.lean and its tests, de-private helpers the module system requires in exposed bodies, regenerated import lists. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * feat(fields): removed external C from fast BT; using tables for GF(2^8) * bench(fields): added benchmarks for fast BT implementation * feat(fields): minro proof changes in fast BT * chore(fields): added minor test case in fast BT * docs(fields): adding/modifying comments * refactor(fields): split defs in fast BT for zero-import * bench(fields): fixed result naming in fast BT benchmarks * bench(fields): fast BT smaller units in benchmarks --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Derek Sorensen <derek.sorensen@ethereum.org> Co-authored-by: Derek Sorensen <d@dhsorens.com>
Co-authored-by: Derek Sorensen <derek.sorensen@ethereum.org>
* feat(fields): add fast Goldilocks arithmetic
* tests(fields): add tests for goldilocks
* refactor(fields): reland fast Goldilocks without the C extern tier
Bring the relanded work up to current repo conventions.
Namespace: `Basic.lean` used a nested `namespace Goldilocks.Basic`, which
renamed the public API to `Goldilocks.Basic.fieldSize` / `.Field` and broke
`bench/CompPolyBench/Common.lean`. Use plain `namespace Goldilocks`, matching
`Mersenne31/Basic.lean`, so the existing names survive.
Layout: collapse `Fast/{Internal,Reduction,Arithmetic,Theorems,Field}.lean`
into `Fast.lean` plus a zero-import `FastDefs.lean`, matching the two-file
idiom of `Binary/Tower/{Fast,FastDefs}.lean`. No field in `Fields/` has a
`Fast/` subdirectory, and a single module is what makes `private` usable
across these declarations. `FastDefs.lean` holds only raw word kernels so
`precompileModules` lanes can compile it without pulling in mathlib.
Module system: add `module` headers, `public import`, and
`@[expose] public section`; the test file uses `public meta` since `#guard`
evaluates compiled code during elaboration.
Also rename `neg_modulus` to `negModulus` (`def`s are lowerCamelCase) and
replace `letI` with `let` in a proof, per the style linter.
* feat(fields): complete the Goldilocks fast bridge and split word-level proofs
Add the `raw_*` / `toNat_*` bridge lemmas that `Mersenne31/Fast.lean` carries and
this implementation omitted: `raw_mk`, `raw_eq_val`, `raw_zero`, `raw_one`,
`toNat_mk`, `toNat_eq_val_toNat`, `toNat_zero`, `toNat_one`, `toNat_ofNat`,
`toNat_ofUInt64`, and `toNat_ofField`. Only the `toField_*` half of the bridge was
proved before, which left the natural-representative side unavailable to `simp`.
`toNat_ofUInt64` reduces to the raw word before case-splitting: unfolding the
subtype first leaves the membership proof depending on the term being rewritten.
Split the word level into `FastReduction.lean` (low-level `UInt64` lemmas and raw
kernel correctness) so no file exceeds the 1500-line lint limit. The three modules
now divide by role: `FastDefs` runtime kernels, `FastReduction` their correctness,
`Fast` the carrier, operations, canonical bridge, and instances.
Also mark `invExponent` private and drop the `@[noinline]` on `inv`, which
diverged from Mersenne31 without justification.
* feat(bench): add Goldilocks arithmetic benchmark group
Add `fields-goldilocks-mul` and `fields-goldilocks-inv`, each running the
canonical `ZMod` implementation against the verified native-word one on shared
inputs so the group checksum cross-checks the two. Registered last in `allTasks`
because adding a group shifts the shared `StdGen` and would otherwise change the
checksums of every group after it, and wired into `BENCH_CI_GROUPS` so CI covers
them.
Measured at the medium preset: multiplication 810ns to 643ns, inversion 10.59us
to 1.04us. The modest multiplication ratio is because array indexing dominates
that loop for both arms; inversion is the real win.
`checksumGoldilocksFast` calls `Goldilocks.Fast.toNat` directly, since the carrier
is an `abbrev` for a `Subtype` and dot notation would resolve to `Subtype.toNat`.
Drop the local `Fact (Nat.Prime Goldilocks.fieldSize)` instance from the benchmark
helpers, now redundant with the one in `Goldilocks/Basic.lean`. Document the field
in `Fields/README.md`, `README.md`, `ROADMAP.md`, and the benchmark README.
---------
Co-authored-by: Varun Thakore <vrnthakore@gmail.com>
…zkEVM#290) * feat(univariate): Shoup and Las Vegas root-search backends Re-land olympichek's Shoup trace splitter and bounded Las Vegas Cantor–Zassenhaus stack from Verified-zkEVM#253/Verified-zkEVM#254 onto current main (module system, Lean 4.32). Both implement LinearFactorProductSplitter for fields without a smooth multiplicative-subgroup schedule. - Roots/Shoup: small-char trace coordinates [vzGS92] with correctness - Roots/LasVegas: odd CZ + char-2 trace branches, ProbeFamily, probability - Tests on ZMod 2/5/11 and binary-tower level 0 (Tower integration path) - Docs/ROADMAP: close the non-smooth splitter gap; note high-width Tower SmallPrimeTraceContext instances as follow-up Port fixes for open-friendly CPolynomial APIs and module-system proof adjustments. No parallel Binary/Extension field stack in this PR. Co-authored-by: Derek Sorensen <d@dhsorens.com> * fix(roots): adapt Shoup and Las Vegas proofs to Lean 4.33.1 The rebase onto current main left the build failing on module-system exposure and mathlib drift, not on any mathematical content. All 21 library modules and 3 test modules already carried `module`, `public import` and `@[expose] public section`; the failures were downstream of main tightening definition exposure. - `import all` for the same-package implementation dependencies these proofs step through (`Univariate.Basic`, `Modular`, `Raw.Division`, `Raw.Modular`, `ToPoly.Core`). `natDegree`, `coeff`, `eval`, `monicNormalize`, `modByMonic` and the `Raw` modular kernels live in bare `public section`s, so their bodies are opaque downstream and `simp [natDegree]`, `unfold monicNormalize`, `change` into the `Raw` layer and `natDegree 0 = 0 := rfl` all stopped working. This is the pattern `docs/wiki/module-system.md` prescribes for exactly this case. - Bridge `toPoly 0 = 0` with `toPoly_eq_zero_iff` rather than relying on definitional reduction. - `letI`/`haveI` to `let`/`have` (26 sites) per the `haveILetI` style linter, and `Set.mem_setOf_eq` to `Set.mem_ofPred_eq` (32 sites) for the mathlib 4.32 to 4.33 deprecation. - Prove the two `ContainsAllFieldElements` obligations with plain `decide` over the whole quantifier, matching `tests/.../Roots/Enumeration.lean`. List membership decidability now wants `BEq`/`LawfulBEq`, which the previous `fin_cases`-then-`decide` shape could not synthesize. A `natDegree_zero` characterization lemma in `Univariate/Basic.lean` would be the tidier long-term fix for the last of those; left out to keep this change inside the PR's own files. Build, tests, lint, imports, docs integrity and `axiomsweep --check` all pass; the sweep stays at 0 sorry and 0 non-standard axioms. --------- Co-authored-by: Valerii Huhnin <olympichek1@gmail.com>
…erified-zkEVM#312) * feat(linalg): order-basis approximant layer over polynomial matrices The linear-algebra half of the Guruswami-Sudan approximant interpolation work from Verified-zkEVM#255, split out so it can be reviewed on its own. It stands under ROADMAP item 10 independently of the decoder backends that consume it. Adds `LinearAlgebra/PolynomialMatrix/Approximant/`: - `ModularEquation/` — modular key equations with soundness and completeness - `PMBasis/` — the divide-and-conquer order-basis recursion, with X-adic soundness, kernel-leaf soundness/completeness, and the scalar and span kernel-leaf layers - `PartialLinearization.lean` — degree balancing for the recursion plus the supporting matrix pieces it needs: `Operations.lean`, `RowSelection.lean`, `StrassenCorrectness.lean` (fast multiplication used by the PM-Basis recursion), and `MuldersStorjohannCorrectness/WeakPopovMinimal.lean`. * fix(linalg): port the approximant layer to Lean 4.33.1 Module-system and toolchain adaptation for the relanded order-basis layer. - `import all` for the same-package implementation dependencies these proofs step through (`Univariate.Basic`, `Univariate.Raw.Core`). `coeff`, `ofArray` and the `Raw` wrappers sit in bare `public section`s, so their bodies are opaque downstream and `rw [CPolynomial.ofArray]`, `simp [Raw.coeff]` and `p.coeff i = (↑p).coeff i := rfl` all stopped working. This is the pattern `docs/wiki/module-system.md` prescribes for the case. - `letI` to `let` per the `haveILetI` style linter. - Record the layer under ROADMAP item 10. --------- Co-authored-by: Valerii Huhnin <olympichek1@gmail.com>
…ied-zkEVM#313) * feat(bivariate): approximant-basis and hybrid GS interpolation Two further Guruswami-Sudan interpolation backends from Verified-zkEVM#255, built on the order-basis layer. - `Interpolation/ApproximantBasis/` — solves the interpolation problem as a modular key equation through PM-Basis, quasi-linear in code length and independent of the corruption level - `Interpolation/Hybrid/` — budgeted Lee-O'Sullivan reduction with approximant fallback; correctness follows from equality to whichever verified backend it dispatched to - `Interpolation/WitnessDivisibility*` — the fast multiplicity check, proved equivalent to the Hasse pointwise check Wired into the existing `GSInterpContext` / `Implementations` pattern, so the `gsCore_sound` and `gsCore_complete_*` contracts carry over unchanged. * fix(bivariate): port GS approximant interpolation to 4.33.1 and benchmark it Port and measurement for the relanded interpolation backends. Module-system adaptation, same class as the rest of the reland: - `import all` for the same-package implementation dependencies these proofs step through (`Univariate.Basic`, `Univariate.Raw.Core`, `ToPoly.Core`). `linearFactor`, `coeff`, `ofArray` and `toPoly` sit in bare `public section`s, so their bodies are opaque downstream. - `eval_map_taylorAlgHom`: keep `taylorAlgHom` folded so the `@[simp, norm_cast]` `coe_taylorAlgHom` can fire, and discharge `taylorAlgHom x (C y) = C y` explicitly rather than by definitional reduction. - Drop two simp arguments the elaborator now reports as unused. - Prove the test's `ContainsAllFieldElements` obligation with explicit `List.Mem` witnesses; `Decidable (_ ∈ _.toList)` no longer synthesizes for this carrier, so neither `decide` nor `fin_cases <;> decide` applies. Benchmark: four rows added to the existing `guruswami-sudan-interp-small-koalabear` group, covering approximant-basis and hybrid over canonical and native-word KoalaBear. Adding rows rather than a new group keeps the shared `StdGen` untouched, so no other group's checksums move, and the group is already in `BENCH_CI_GROUPS`. What the numbers say at the small shape (n=64, k=16, m=2, small preset): Lee-O'Sullivan direct 13.6ms, approximant-basis 180.1ms, hybrid 16.5ms canonical; 2.3ms / 63.7ms / 3.9ms on the fast field. The approximant backend is an order of magnitude slower here, which is expected — its advantage is asymptotic in code length and the crossover is well above n=128, the largest shape the suite currently defines. The hybrid backend matching Lee-O'Sullivan almost exactly is the meaningful result: its budget correctly declines to fall back at this size. Substantiating the quasi-linear claim needs a large-n shape, which is a separate scope decision because of CI wall-clock. --------- Co-authored-by: Valerii Huhnin <olympichek1@gmail.com>
…ified-zkEVM#315) * feat(multivariate): add partial evaluation of the first variable - Multivariate/PartialEval.lean: partialEvalFirst (fix variable 0) with its evaluation and per-variable degree-bound lemmas. - Operations.lean: add the fromCMvPolynomial_bind₁ bridge lemma. * port(multivariate): migrate partial evaluation to the module system Land the salvageable half of the original change and drop the rest. - Module-system migration: `module` header, `public import`, and `@[expose] public section`, matching the rest of `Multivariate/`. Imports reduce to `Operations` plus `Mathlib.Algebra.MvPolynomial.Degrees`. - Drop the degree-bound wrappers. `CDegreeLE` and `CMvDegreeLE` were subtypes with no instances, operations or lemmas, and `IndividualDegreeLE` was unused even by the degree theorem that motivated it; all three existed only to give an external consumer names to refer to. - Replace every `simp`/`simpa` in the new code with `simp only`/`simpa only` per the repo tactic guidance. - Generalize the ring variable from `Type` to `Type*`. - Add regression coverage: the action on generators, agreement with direct evaluation on a concrete polynomial, and the degree bound. The checks are symbolic because the carrier is a quotient of `Std.ExtTreeMap`, so kernel reduction gets stuck on `Quot.lift`. * port(multivariate): harden partial-evaluation proofs against import drift - Use core `Fin.succ_inj` instead of Mathlib's `Fin.succ_injective`. The latter lives in `Mathlib/Data/Fin/SuccPred.lean` and was reachable here only through an incidental import closure rather than anything this file asks for. - Finish the `simp only` conversion in the test file. --------- Co-authored-by: Cody Gunton <codygunton@gmail.com>
…rified-zkEVM#274) * feat(fields): Pasta base fields on the eight-limb Montgomery implementation Add `Fields/Pasta`, the per-field facade for the Pallas and Vesta base fields, following the KoalaBear layering: * `Pasta/Basic.lean` — the two 255-bit primes with Pratt primality certificates (ported from the certificates by Daira-Emma Hopwood, using CompPoly's own `PrattCertificate` infrastructure), their `Fact` and `Field` instances, and the 2-cycle abbreviations relating each curve's scalar field to the other's base field; * `Pasta/Fast.lean` — the `Mont64x8Field` constants for both fields and the namespaced `Pallas.Fast` / `Vesta.Fast` API over the shared eight-limb implementation, with the canonical-field bridge; * `Pasta.lean` — the facade re-exporting both. `Mont64x8Field` moves from the raw layer to `Montgomery/Native64x8Field` alongside the carrier it parameterizes, mirroring `Mont32Field` in `Montgomery/Native32Field`, and now carries `prime` like its single-word counterpart, so the bridge no longer takes a separate `Fact` argument. Tests cross-check both fast fields against canonical `ZMod` arithmetic for powers and inverses. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * feat(fields): scalar radix-2 FFT over eight-limb Montgomery elements Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
…ule (Verified-zkEVM#316) `CompPoly/Fields/Mersenne.lean` was a compatibility re-export left behind when Verified-zkEVM#257 renamed the real module to `CompPoly.Fields.Mersenne31` and split it into `Basic`/`Fast`. It declared nothing of its own. Nothing in the repository imported it except the generated `CompPoly.lean`, which picks up every tracked module and so inherited its deprecation warning: every `lake build` reported one, and `lake build --wfail` failed. Downstream consumers on the old path should import `CompPoly.Fields.Mersenne31`.
Add product and append characterizations for the executable multilinear equality kernel, with a scalar-evaluation support lemma and regression tests. Adapted from Verified-zkEVM/leanth#10. Co-authored-by: Elias Judin <ejudin@gmail.com>
…ied-zkEVM#320) * refactor(fields): make carry-less multiplication width-generic `BinaryField.clMul` was fixed at 128x128 -> 256 bits, so no other width could reuse it or its correctness proof. Add width-generic `carryLessMul {v w}` alongside `zeroExtendTo` and the `toPoly` splitting lemmas `toPoly_eq_range` and `toPoly_split`, and redefine `clMul` as its 128-bit instance. `clMul`, `clSq`, and `to256` keep their names and signatures, and `clMul_unfold`, `toPoly_clMul`, and `toPoly_128_extend_256` become corollaries of the generic versions, so the GHASH development is unchanged apart from its proofs collapsing. `clMulNat`, the Nat-based kernel checker, is untouched. Also fix `scripts/gen_rabin_certificate.py`, whose line wrapping broke at degree 64 over GF(2): it only ever wrapped a step across two lines and never wrapped `poly_to_lean` output, so a small prime with many terms emitted 152 lines over the 100-column limit. Wrap coefficient lists across as many lines as needed, emit the regeneration command as a fenced shell block, and replace the hardcoded `Authors:` line with an `--authors` flag. The generator still reproduces both committed KoalaBear certificates byte-for-byte and passes its self-tests. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * fix(gen_rabin_certificate): Escape shell backslash outside of single quote to ensure 100 line limit is enforced Add --f= rather --f '...' so that argparse can accept negative coefficients for generating certificate data. Regenerate certificate data for Quintix and Sextic KoalaBear extensions, only headers have been changed and means that the certificates are now not byte for byte identical * fix(gen_rabin_certificate): update stale --f references and add wrapping/format test --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…erified-zkEVM#321) * refactor(fields): make carry-less multiplication width-generic `BinaryField.clMul` was fixed at 128x128 -> 256 bits, so no other width could reuse it or its correctness proof. Add width-generic `carryLessMul {v w}` alongside `zeroExtendTo` and the `toPoly` splitting lemmas `toPoly_eq_range` and `toPoly_split`, and redefine `clMul` as its 128-bit instance. `clMul`, `clSq`, and `to256` keep their names and signatures, and `clMul_unfold`, `toPoly_clMul`, and `toPoly_128_extend_256` become corollaries of the generic versions, so the GHASH development is unchanged apart from its proofs collapsing. `clMulNat`, the Nat-based kernel checker, is untouched. Also fix `scripts/gen_rabin_certificate.py`, whose line wrapping broke at degree 64 over GF(2): it only ever wrapped a step across two lines and never wrapped `poly_to_lean` output, so a small prime with many terms emitted 152 lines over the 100-column limit. Wrap coefficient lists across as many lines as needed, emit the regeneration command as a fenced shell block, and replace the hardcoded `Authors:` line with an `--authors` flag. The generator still reproduces both committed KoalaBear certificates byte-for-byte and passes its self-tests. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * fix(gen_rabin_certificate): Escape shell backslash outside of single quote to ensure 100 line limit is enforced Add --f= rather --f '...' so that argparse can accept negative coefficients for generating certificate data. Regenerate certificate data for Quintix and Sextic KoalaBear extensions, only headers have been changed and means that the certificates are now not byte for byte identical * fix(gen_rabin_certificate): update stale --f references and add wrapping/format test * feat(fields): add polynomial-basis GF(2^64) and its cubic extension Add `GF(2)[x]/(x^64 + x^4 + x^3 + x + 1)` as a flat quotient by a single irreducible degree-64 pentanomial, together with its degree-3 extension `GF(2^64)[y]/(y^3 + y + 1)`, giving GF(2^192). CompPoly already reaches GF(2^64) as level 6 of `Fields/Binary/Tower/`, but that builds it by iterated quadratic extension. The two fields are abstractly isomorphic and use different bases, so their bit-level encodings disagree: on the same bit patterns `2 * 3` is `6` here and `1` in the tower's rung. Neither substitutes for the other wherever the encoding is observable, and no polynomial-basis GF(2^64) existed before this. An element is a `BitVec 64` whose bit `i` is the coefficient of `x^i`. Addition is `xor`, multiplication is a width-generic carry-less product folded back into 64 bits through the reduction constant `0x1B`, and inversion is an Itoh-Tsujii addition chain. The extension reuses the computable framework in `Fields/Extension/`, so its carrier is definitionally `Vector BF64 3`. Degree 64 is composite, so `irreducible_of_rabin_prime_degree` is unsound here -- a product of equal-degree factors passes its collapsed condition. The general `Polynomial.irreducible_of_rabin` is used instead, against certificate data regenerated by `scripts/gen_rabin_certificate.py` and replayed in the kernel. The cubic needs no certificate: a root would satisfy `a^7 = 1`, so its order divides both `7` and `2^64 - 1`, which are coprime. The algebraic instances are written out field-by-field rather than transported through `Function.Injective.commRing`, which takes the bridge map as data and would make the arithmetic noncomputable -- taking the extension down with it, since `Ext.mul` reaches through the base field's `Field` instance. `Pow` is `npowBinRec` rather than the linear `npowRec`; a full-order exponent needs about 64 multiplications instead of 2^64, which is the difference between usable and unusable in the kernel. Regression coverage checks base-field vectors with `decide +kernel` and extension vectors with `#guard`. The latter runs the compiled arithmetic, so a `Field` instance that regressed to noncomputable would fail the build rather than pass silently. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * feat(fields): add `CharP Ext3 2` and the `ext3Gen` lemmas `Ext3` had no `CharP` instance. `BF64` and `BF64Quot` both carry one, but it is not found by instance search from `Algebra BF64 Ext3` alone, so the `CharTwo` API — `add_self_eq_zero`, `add_sq`, and the rest — was unavailable on the extension. That is the first thing a consumer of a binary field reaches for. Add the instance the same way `Impl.lean` derives it for `BF64Quot`, via `charP_of_injective_algebraMap'`, and place it ahead of the generator lemmas since the defining relation needs it. Also add the named-generator layer that `KoalaBear.Ext4` and `Ext5` provide but `Ext3` lacked: `ext3Gen`, `ext3Gen_eq_gen`, `toQuot_ext3Gen`, `aeval_ext3Gen`, and `ext3Gen_pow_three`, the defining relation `y^3 = y + 1` in usable form. Without these a consumer had to write `Ext.gen (P := ext3Params)` by hand and rewrite through `Ext.aeval_gen_poly` and `ext3Params_poly` themselves; the regression tests felt this and defined their own local `y`. Following `ext5Gen_eq_gen`, `ext3Gen_eq_gen` is deliberately not `@[simp]`, since as a rewrite it fires before `ext3Gen_pow_three` can match. `card_ext3` becomes `@[simp]` to match `card_ext4` and `card_ext5`. The relation is stated as `ext3Gen ^ 3 = ext3Gen + 1` rather than with `Ext.ofBase`, because `aeval_one` already normalises the constant to `1`; `KoalaBear` needs `Ext.ofBase` only because its constant is `-1`. `linear_combination` cannot discharge it — it reasons over the integers, so it will not turn `y^3 + y + 1 = 0` into `y^3 = y + 1` in characteristic two — hence `CharTwo.sub_eq_add` and `add_assoc`. Also correct the file headers: the copyright holder returns to `CompPoly Contributors`, matching every other file in the repository, with the individual credited on the `Authors:` line, and the facade picks up the author it was missing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * refactor(fields): tighten BF64 resource budgets and docstrings Review follow-ups on the BF64 modules, all confined to this PR's own files. Resource options were over-provisioned. `Basic.lean` declared `maxHeartbeats 4000000` and `Reduce.lean` `2000000` — the two largest values in the repository, against a previous maximum of 1600000 — but bisection shows `Basic.lean` compiles at 400000 and `Reduce.lean` at the 200000 default. The `maxRecDepth` escalations in `Reduce.lean` and `Ext3.lean` are likewise unnecessary; only `Basic.lean` needs a raised depth, and 4000 suffices for it. An inflated budget hides a future regression rather than preventing one. Also replaces a bare `simp` in `lowHalf_testBit` with `simp only`, per the tactic guidance in `CLAUDE.md`, and adds docstrings to the degree, monicity, and operation-unfolding lemmas that lacked them. `ROADMAP.md`: the new BF64 entry was inserted between "Basic field definitions" and the sub-bullets nested beneath it, orphaning that block. Moved it after, so it reads as the sibling it is. Verified: `lake build`, `lake test`, `lake exe axiomsweep --check` (0 sorry, 0 non-standard axioms), `lint-style.sh`, `check-imports.sh`, and `check-docs-integrity.py` all pass. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * refactor(fields): carry toPoly_one_shiftLeft lemma into Common.lean to prevent BF64 from importing its sibling field * chore(fields): update documentation to include BF64 certificate and Char-2 dreferences --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…#324) * fix(algebra): require identity maps in algebra towers * refactor(algebra): polish tower identity contract
…-group seeding (Verified-zkEVM#319) * perf(bench): measure the benchmark, not the harness The timed loop folded a `Nat` checksum modulo the largest prime below 2^64 into every iteration, so each fold was a heap-allocating bignum multiply-and-mod inside the measured region. Fold results through a `UInt64` sink instead and keep the strong `Nat` digest in the untimed validation pass, where correctness is actually established. `runTimed` gains an optional `sink : α → UInt64` defaulting to a truncation of the existing `Nat` digest, so all 226 call sites keep working while the bignum leaves the timed region everywhere. Carriers whose canonical value exceeds 2^63 declare a native sink; `Goldilocks.Fast` and `ZMod` do so here. Add `harness-floor` and `harness-canary`. The floor times an empty body and is the per-iteration cost every other benchmark sits on top of; the canary times a known non-eliminable body and fails the run if it does not clear the floor by `canaryFloorRatio`. A benchmark that has been optimised away otherwise looks exactly like a benchmark that got very fast. Both additive-NTT sinks now fold over every output position. The reference row returns `Fin (2 ^ n) → α`, so realising the whole result is part of its work and not part of the `Array`-returning fast row's; a sink may only skip work the benchmark has already done. Measured on darwin/arm64 at `--small`: harness floor 1.89 ns/iter, `goldilocks-mul-fast` 619 ns -> 3 ns, `goldilocks-mul-zmod` 788 ns -> 365 ns, reported ratio 1.27x -> ~108x. Two full 68-group runs agree on every one of 250 validation digests. Also escape `jsonString` via `Lean.Json.renderString`, hoist `arrayToFinFunction` out of its fold in `checksumConcreteBtfOutputArray`, and emit `sink_digest` so the timed accumulator stays observably live. * feat(bench): collect samples instead of one total, and report dispersion Every benchmark reported one sample of one total, so a scheduler hiccup and a real regression were indistinguishable. Worse, 67 of 253 rows timed exactly one iteration and 107 timed three or fewer, which is where the large-NTT and batch-eval numbers live. Treat each benchmark's iteration count as a total-work budget and split it into up to `targetSampleCount` timed samples. Report the median as the headline number alongside min, mean, p95, standard deviation and median absolute deviation, and emit the whole per-sample vector so the distribution can be examined offline. Label Tukey outliers at the conventional 1.5x and 3x interquartile fences without dropping them, since a sample that took ten times the median is data about the machine. Suppress labelling when the interquartile range is zero, where both fences collapse onto the quartiles and mark every sample that differs at all. Where one iteration already exhausts the budget the row is reported as `n=1` rather than as a number with an implied precision it does not have. Cap the validation pass at `validationIterationCap`, and let it count towards warmup: it has already executed the body, so an expensive workload validated once now runs twice per benchmark rather than three times. Across a full 68-group `--small` run: 172 of 286 rows now carry five or more samples, median dispersion is 1.4% of the median with a 5.1% maximum, and the timed-region total is unchanged at 152 s. * feat(bench): seed each group from its key One StdGen was threaded through the selected groups in order, so a group's inputs depended on which groups ran before it. `--group X` and `--groups X,Y` measured different inputs for X, adding a group anywhere changed the inputs of every group after it, and the CI subset measured neither what a full local run measured nor what any earlier run measured. Confirmed empirically: 199 of 235 rows shared with a six-week-old result file differ for no reason other than groups having been added between the two commits. Derive each group's generator from its key inside `BenchTask.fromGroupRunner`. Every registered task goes through that function, so no group runner changes. Registration becomes authoritative while we are here: `fromGroupRunner` stamps the key and title from the `BenchGroupInfo` that `--list` and the CI allowlist validate against, so a runner can no longer drift from its registration. Remove 25 declarations with no references anywhere: ten per-area `runX` wrappers and fifteen `*GroupInfos` aggregate lists. Verified: a group measures identical inputs alone, alongside another group, and with the order reversed; and the exact `BENCH_CI_GROUPS` subset reproduces the full run's digest on all 184 comparable rows. * feat(bench): report the host, tidy output, and document the harness Hardware probing was `lscpu`, `nproc`, `/proc/meminfo` and `df --output`, all Linux-only, so every local report read `unavailable outside GitHub Actions` on the primary development platform. Fall back to `sysctl` when the Linux probes are absent, parsing the BSD `df -h` table where the size is the second field rather than the first. Write reports and results to `bench/out/` instead of dropping them beside the sources. Two ignore rules across two files become one, and CI's artifact glob can no longer pick up anything but the run it just made -- on a fresh checkout it never did, but locally it swept every stale file into the artifact. `tests/CompPolyTests/Fields/Binary/CommonBench.lean` was an unimported `#eval` benchmark, but it also carried four `#guard` correctness checks and the removed `Finset.fold` baseline that pins `clMul` to the behaviour it replaced, so CI has never run them. Move those into `Fields/Binary/Common.lean`, which the test driver imports, and delete the benchmark. `NTT/Benchmark.lean` stays: it holds the only NTT-vs-schoolbook crossover logic in the repo. Add `docs/wiki/benchmarking.md`, registered in both hand-maintained lists in the wiki README, covering the validation/timed split, the rule that a sink may only skip work the benchmark has already done, how to read dispersion, the harness self-check, determinism, and the remaining gaps. * ci(bench): gate on benchmark correctness, run timings on demand The benchmark step was doing two unrelated jobs in the blocking CI job: 41 groups cross-checking each canonical `ZMod` model against its native-word implementation on random inputs plus the harness canary, and a timing report. Only the first is worth gating on. `ubuntu-latest` is a shared 2-vCPU VM, and the median sample dispersion measured on a quiet local machine is 1.4%, so gating on those timings would gate on noise. Add `--validate-only`, which runs the untimed digest pass and the group agreement check and collects no samples. It is deterministic and machine independent, which is what a gate should be, and it is the fast local answer to whether an implementation is still correct. The mode is threaded through an `IO.Ref` set from the command line rather than a parameter, because every alternative means editing all 226 `runTimed` call sites. The canary needs an escape hatch: it compares timed totals, so with no samples collected `0 < 3 * 0` is false and it would pass vacuously in exactly the mode CI runs, disabling the one guard against benchmark bodies being optimised away. `runTimed` therefore takes `forceTiming`, which the self-check sets. Main CI now runs `--validate-only`. Over the 41 curated groups at `--medium` on darwin/arm64 that is 32s against 124s for the timed run it replaces, and it still fails the build on a digest mismatch or a collapsed canary. Timings move to a new `benchmarks.yml`, produced on demand three ways: Actions -> Benchmarks -> Run workflow with a preset and optional group list, a `/bench` comment from a repo member following the existing `/review` convention, or automatically on a PR touching `bench/**` -- the one place a path filter genuinely fits, since a change to the harness itself should be measured. It restores the build caches and never saves them, because the Actions cache is already documented as over quota. Path filtering the benchmarks themselves was considered and rejected: a group's performance depends on whatever it transitively calls, and `CompPoly/Fields/Montgomery/**` underpins nearly every group, so a filter honest enough to be safe would fire on almost every substantive PR. `BENCH_CI_GROUPS` moves out of the workflow `env:` into `bench/ci-groups.txt`, since a second workflow cannot read a workflow-scoped variable and duplicating 41 keys invites drift. The list now sits next to the benchmarks it names. * docs(bench): correct the claim about shared-runner noise I asserted, here and in the wiki and both workflow comments, that sample dispersion on a shared CI runner would be worse than the 1.4% median MAD measured locally. The first real run of the timing workflow says the opposite: median MAD 0.2%, p90 0.5%, max 1.0% across 172 replicated rows. A development laptop with frequency scaling and heterogeneous cores is a noisier place to measure than an idle VM slice. What is worse on CI is the tail -- 56 of 172 rows carried severe Tukey outliers against 27 of 286 locally, which is what a quiet baseline punctuated by preemption looks like. The decision to keep timings out of the gate is unchanged, but the reason was wrong. A gate compares runs against each other, on a runner whose CPU model varies between runs, and a single run cannot measure that variance. Timings are advisory because cross-run comparability is unvalidated, not because within-run noise is high. Also record the measured runner costs: the correctness gate is 46s where the timed run it replaced was about 167s. * test(fields): pin both widths of the carry-less multiply The baseline rescued from `CommonBench.lean` was written against `clMul`, but Verified-zkEVM#320 has since made the multiplication width-generic and Verified-zkEVM#321 added `BF64`, whose `mul` is the 64-bit instance. As merged, the rescued guards pinned only the 128-bit width; the new one was covered only indirectly, by Verified-zkEVM#321's reference vectors, which pin the field rather than the multiplication against its predecessor. Generalize `clMulBaseline` in the operand width and add four guards at width 64. Verified by breaking one and confirming the build fails. Also record the `GF(2^64)` bench coverage gap in the wiki's known-gaps list: the tower groups are still the only binary-field timings.
…unts (Verified-zkEVM#337) * feat(bench): add wall-clock measurement budgets A geometric calibration ramp and the sizing arithmetic that will replace the 229 hand-tuned `selectNat` iteration counts. Nothing calls it yet, so this commit cannot change a reported number. The ramp doubles as warmup and threads the sink accumulator, so it is no more eliminable than the timed samples are. Its cost estimate comes from the last step alone: the early steps run cold, and an estimate biased high sizes samples short, which inflates the dispersion the suite exists to report. `planFromCalibration` carries two ceilings rather than one. A sample is sized to `sampleNanos`, which is deliberately preset-independent -- a sample is a mean over its iterations, so varying it by preset would make `--small` and `--large` report structurally different spread for identical code. A separate `measureNanos` total is what lets the workloads costing seconds per iteration be replicated at all; without it they would sit at one sample forever. Nine `#guard`s pin the sizing at 1.5 ns, at 1 ms, at 13 s under both a 60 s and a 2 s total, and at a zero cost estimate, which must neither divide by zero nor collapse the sample count. * refactor(bench): give runTimed a spec record, keeping the positional form `runTimed` took five consecutive `String` arguments across 228 call sites, where a transposed pair is a silent mislabelling rather than a type error. `runTimedSpec` takes them as a `BenchSpec` record instead. The three `α`-dependent arguments stay outside the record. Giving `BenchSpec` a type parameter so it could carry `sink` would put one on every literal in the suite in order to serve the forty rows that override it, and a group with a `ZMod` row beside a `Fast` row has a different result type per row anyway. The positional `runTimed` survives as a wrapper so the migration of the call sites is a separate commit that provably changes nothing. It goes away once they have all moved. Verified: `--validate-only` output is byte-identical to the previous commit at all three presets, over all 286 rows. * refactor(bench): move all 228 call sites onto the spec record Mechanical. Each site's five label strings move into a `BenchSpec` literal and every expression is carried over byte-identical; `digestIterations` takes whatever the site passed as `checksumIterations`, or the old default `min validationIterationCap measured` where it relied on it. No behaviour changes here, which is the point of keeping it separate: the whole edit is proved by diffing the non-timing columns of a full run. Two shapes needed care. `Univariate/Roots/FiniteField.lean` passed the digest count as a tenth positional argument rather than by name. `Harness/SelfCheck.lean` is the only user of `forceTiming`, which is now a spec field. Verified: `--validate-only` at `--small` is byte-identical to the previous commit over all 286 rows, and the build is warning-clean with no line over the 100-column limit. * refactor(bench): make digests the body's period, not the preset's count `checksumIterations` was `min 256 measured`, so a group's digest varied with the preset: 195 of the 282 rows shared across presets carried three different values. Under budget-driven sizing the same expression would make it vary with the *machine*, which turns committed digest fixtures from awkward into impossible. The rule is now that `digestIterations` is the **period of the body in its iteration index**, capped at 256. That is not a weaker check: iterations past one full cycle recompute a bit-identical result, so a `fun _ ↦ …` body folding its digest once sees exactly what folding it 256 times saw. `validationIterationCap` and `groupChecksumIterations` are replaced by `digestIterationCap` and `digestPeriod`, which takes a period rather than a list of iteration counts. Each group now names its own: fun _ ↦ … bodies digestPeriod 1 21 groups 32-point pools (univariate, multivariate, digestPeriod <n> 13 groups multilinear, bivariate evaluation) 64-element pools (tower, extension, deflate) digestPeriod <n> 5 groups 256-element pools (Goldilocks, Mont64x8) digestPeriod <n> 4 groups The periods are single-sourced from what the runner already computes — `points.size`, `perturb.size`, `values.size` — or from a named constant where the literal was previously repeated at the call sites: `bivariatePointCount`, `multilinearPointCount`, `extPoolSize`. `multilinear`'s point helpers now take the raw iteration index and reduce internally, so the period has one home rather than twelve. Two sites are not periods. `harness-floor` and `harness-canary` are unbounded in `i` and are cross-checked against nothing, so they take a pinned `harnessDigestIterations`. And `guruswami-sudan-packed-filter` had `candidateCount := preset.selectNat 128 64 32` — an *input shape* wearing a budget's clothes, which no digest-length rule could have fixed. Pinned at 128; that group's `input_shape` column stops moving between presets too. Verified with `--validate-only` at all three presets over all groups: digests differing across presets 195 of 282 -> 0 of 284 columns that moved vs. b5fe1ad checksum, checksum_iterations, and input_shape on the two packed-filter rows columns that did not move warmup_iterations, measured_iterations, iters_per_sample, sample_count 203 of 284 rows changed digest at `--large`; the other 81 were already at their period (68 at 1, 13 at 256). The curated `--validate-only --medium` pass goes from 36.1 s to 33.0 s locally — a small saving, as §11.4.3 predicted, because the cost sits in rows that were already validated exactly once. * fix(bench): compare canary and floor per iteration, not by total The dead-code canary asserted `canary.totalNanos > 3 * floor.totalNanos`. That separates the two rows only while they run the same number of iterations, which is true today and stops being true one commit from now: sizing each row from a wall-clock budget equalises totals *by construction*. The assertion would then throw on every run, and the natural-looking repair — lowering `canaryFloorRatio` until it passes — would leave it passing vacuously forever, with the harness silently unable to detect that benchmark bodies are being optimised away. Compares `stats.medianPicos` instead, which is already per iteration and is what the ratio was always meant to express. Landing it before the sizing flip rather than after keeps the flip from having to be verified through a check that is throwing. A zero median on either row now throws separately: it means the clock could not resolve the loop, in which case the ratio cannot say anything either way. Observed ratios, so a future collapse shows up as a changed number rather than a threshold that happens still to pass: timed small 244x medium 160x large 353x --validate-only small 210x medium 390x large 776x Failure path re-checked as `docs/wiki/benchmarking.md` asks: with `canaryRounds := 0` the canary measures 1683 ps against a 2391 ps floor and `--validate-only --small` fails with the collapse message. * fix(bench): draw the root-search workload from the group's random stream The finite-field root group has been reporting its cost divided by `itersPerSample` since it was written. Its body was a closed term — `p` was a `let` bound to the nullary constant `nonlinearRootPolynomial`, and the root context is a constant too — so the whole computation was evaluated once and every later iteration in a sample got the cached array back. That is invisible while `itersPerSample` is 1, which is what the hand-tuned counts gave it at `--medium`, and it shows up as a clean division everywhere else. Measured at the counts in `HEAD~1`: row itersPerSample --medium --large ntt 1 -> 2 764 ms 376 ms (/2) nttfast 1 -> 6 232 ms 38.8 ms (/6) fast-naive 1 -> 3 484 ms 162 ms (/3) fast-ntt 1 -> 6 286 ms 47.6 ms (/6) fast-nttfast 3 -> 20 24.4 ms 3.66 ms (/6.7) The seeds are now offset by a `base` drawn from the group's own random stream, so the polynomial is a local built at run time rather than a constant the compiler can float out of the loop — the same shape every other group in the suite already has. Nothing about the workload moves: still degree 66, still `rootWorkloadDistinctRoots` distinct roots with one of them repeated. The digest period stays 1, so the `--validate-only` pass costs exactly what it did, which matters because this is the most expensive group on the blocking CI gate. Afterwards the medians hold still as `itersPerSample` goes from 1 to 20: ntt 721 ms -> 727 ms fast-ntt 276 ms -> 272 ms nttfast 229 ms -> 235 ms fast-nttfast 76.3 ms -> 73.9 ms fast-naive 450 ms -> 462 ms naive 2365 ms -> 2408 ms `fast-nttfast`'s real cost is 74 ms, not the 24 ms the suite has been reporting. All six rows still agree on one digest, and it is identical at all three presets. Found by the per-iteration median comparison that the sizing flip's verification calls for; landing it first so that comparison starts from honest numbers. * refactor(bench): size every benchmark from a wall-clock budget A preset now selects a `BenchBudget` — warmup nanoseconds, sample length, sample count, and a total ceiling per row — instead of an iteration count per benchmark. `runTimedSpec` calibrates each row against that budget with the geometric ramp added in `ae22c05`: the ramp doubles as warmup, its last step estimates the per-iteration cost, that estimate fixes `itersPerSample`, and `measureNanos` caps how many samples the row can afford. An iteration count was the wrong unit. It is not comparable between two rows of one table, it goes stale as the code it measures gets faster, and picking one for a new benchmark is guesswork that has to be redone on every machine — which is why 228 of them were written down by hand and then left alone. Deleted with the counts: `BenchPreset.selectNat`, the eleven `*WarmupIterations` / `*MeasuredIterations` helpers, `gsWarmupIterations`, `harnessMeasuredIterations`, `planSamples`, `targetSampleCount`, `warmThenTime`, `warmIterations`, the `MulBudgets` record, the `BenchPreset → Nat` parameters of the five generic runners, and the positional `runTimed` shim that existed only to make `b5fe1ad` mechanical. 236 budget `let`s go with them. `collectSamples` takes the ramp's accumulator instead of a warmup count, which is what keeps the ramp non-eliminable. Under `--validate-only` calibration does not run at all. A ramp on a thirteen-second body costs thirteen seconds, and `--validate-only` is the only benchmark step on the blocking CI path. Warmup and sample count become table columns rather than shared metadata lines. They were rendered with `matchingNat?`, which stops matching once two rows of a group are calibrated separately — the lines would have vanished from every report with no error. Only the digest length is still shared by construction. Verification, `--medium`, curated set, against `HEAD~1`: --validate-only at all three presets only the two forceTiming harness rows move; their digests are unchanged and the other 284 rows are byte-identical per-iteration medians 0 of 130 rows with >=5 samples fall outside 2x; the whole distribution is 0.878-1.086, median 1.006 calibration stability, 3 runs iters_per_sample within 1.004x (fast) and 1.009x (ZMod) on goldilocks-mul sample_count = 0 none sample_count = 1 2 rows, both flagged unreplicated rows with < 5 samples 22 -> 9 curated timed run 120.1 s -> 110.7 s The replication gain is the point: rows were under-sampled because a count was mis-tuned, and the harness can now tell the difference between "expensive" and "mis-tuned". What it does not fix is input shape — the rows still reading `n=1` have single iterations that genuinely exhaust the budget, and no harness change reaches that. One thing is lost deliberately: `measured_iterations` is no longer comparable across runs, since it depends on how fast the machine was during calibration. `Median` and `Spread` are the columns to compare. * feat(bench): put group identity in the JSONL and provenance in a manifest Two things the results file could not say. **Which group a row belongs to.** The key and the title lived only in the Markdown report, so a JSONL consumer had to reconstruct the grouping from row names. `group_key` and `group_title` are stamped in `flattenGroups` from `BenchGroup`, because `runTimedSpec` genuinely does not know — a row is built before it is placed in a group. The key comes from the same registry entry that `--list` and `bench/ci-groups.txt` validate against, via `BenchTask.fromGroupRunner`, so it cannot drift from the group it names. **What produced the numbers.** `bench/out/manifest-<runId>.json` records the commit, a dirty flag, the toolchain, the preset and the budget it resolved to, the seed, the selection, and the host. This matters more than it used to: `measured_iterations` was a written-down constant and is now a function of how fast the machine was during calibration, so the JSONL lost its one stable provenance signal in the previous commit. A timing from a dirty tree is not attributable to anything, which is why the flag is not optional. Deliberately a separate file rather than a header line in the JSONL — every consumer of that file assumes uniform records, and a header would break all of them at once. Written for every run, `--validate-only` and `--markdown-only` included. Both workflows' artifact steps glob it, or it would never leave the runner. `renderMarkdown` now takes the hardware the manifest already collected instead of probing the host a second time. Verified with `--validate-only` at all three presets: `group_key` is populated on all 286 rows, and every pre-existing column is identical on 284 of them. The two that move are `harness-floor` and `harness-canary`, the only rows measured under `--validate-only`, and only in their calibrated iteration counts — 3.6%, which is what run-to-run calibration noise looks like. * docs(bench): record budget-driven sizing and the Radar deferral `BENCHMARKING.md` gains a §12.6 change-log entry in the voice of the existing ones: what the flip does, the two load-bearing design points (`sampleNanos` fixed across presets, `measureNanos` as a second ceiling), the three preparatory steps, and the three findings — the canary that would have inverted silently, the root group that had been dividing its cost by `itersPerSample` since it was written, and the two report lines that would have disappeared without an error. §11.6 now records Radar as deferred **by decision** rather than pending, so it is not rediscovered later as an oversight, and says why the regression gate stays blocked behind it. `docs/wiki/benchmarking.md` says how a row's size is now chosen and that `Iterations` stopped being comparable between runs, and "Adding a benchmark" gains the two rules a new row has to get right: `digestIterations` is the body's period in `i` and must never be preset- or machine-shaped, and the body must depend on `i` through a value built at run time, because a closed body is evaluated once and cached.
… chained bodies (Verified-zkEVM#338) * feat(bench): report work units, and name the median statistic correctly Two things a row could not say, both needed before any operation-chain or transform benchmark can be read. **`workUnits`.** A row that performs one operation per iteration reports a per-iteration median and that is the number. A row that chains a thousand multiplications, or transforms 2^16 points, does not: its per-iteration median has to be divided by the work it did. `BenchSpec` and `BenchRecord` gain `workUnits`, the JSONL gains `work_units`, and the group table gains a `Per unit (ps)` column. `workUnits` describes the **problem**, not the implementation, and the rows of a group must agree on it. A radix-4 plan and a radix-2 reference perform different butterfly counts for the same transform; letting each row divide by its own count would divide away precisely the algorithmic difference the group exists to show. So the column is gated on `matchingNat?` rather than on "some row set it", and disagreement inside a group now fails the run the way a digest mismatch does — it means the group was specified wrong, not that the table needs a special case. The column is picoseconds rather than a chosen unit because a per-unit figure is normally sub-nanosecond, which is exactly where `chooseTimeUnit` renders `0.000`. It is deliberately *not* mirrored into the JSONL: that file carries `work_units` and the full statistics, and a consumer dividing for itself does not inherit the integer truncation this column accepts to stay readable. **`average_nanos` was a median.** `averageNanos := stats.medianPicos / 1000` — the field has described the wrong statistic since it was introduced. Renamed to `medianNanos` / `median_nanos`. Checked first that nothing consumes the JSONL: both workflows glob the results files as artifacts and neither parses a field, and `scripts/build_timing_report.sh` is about build timing, a different file. `keepSome` is generalised from `Option String` to any type so the optional column can use it. Verified digest-neutral: `--validate-only` at all three presets, only the two `forceTiming` harness rows move and only in their calibrated iteration counts (3.8% and 5.9%, which is run-to-run calibration noise); digests unchanged and the other 284 rows byte-identical. * feat(bench): let one group carry several digest comparisons `checksumMismatchGroups` required *every* row of a group to share a digest. That is right when a group is two implementations of one operation, and wrong as soon as a group wants to hold more than one comparison: a field's `mul` and its `add` belong in the same table and can obviously not agree on a digest. The consequence was structural, not cosmetic. Base-field coverage is a matrix of (field x operation x chain shape), and one-comparison-per-group turns it into roughly 83 two-row groups — 83 more keys to maintain by hand in `bench/ci-groups.txt`, and about 1200 lines of report in which every table has two rows and one ratio. Rows now carry a `digestClass` and agreement is required *within* a class rather than across the group. `classesAgree` replaces the group-wide check; `renderChecksumStatus` and the validation table print one digest per class. Empty is a class like any other, so every existing group keeps exactly the behaviour it had. This takes the coverage work from ~83 new groups of 2 rows to ~10 of 12-20, and it has a benefit beyond the count: rows in one group share a single `genFor` operand draw, so per-operation ratios within a field become directly comparable instead of each being measured against a different random input. Verified digest-neutral at all three presets: every pre-existing group has one class, so every digest and every agreement verdict is unchanged. * feat(bench): measure an operation in a chain, not one operation per loop The suite cannot currently measure a field operation. `harness-floor` is 1.80 ns/iteration and `goldilocks-mul-fast` is 3.16 ns; the generated C shows why. The operand-pool idiom every group uses, `xs.getD (i % xs.size) unit`, compiles to two boxed-`Nat` modulos, two bounds checks and two boxed array reads around a single unboxed multiply. The operation is a rounding error in its own measurement. `Harness/Chain.lean` runs the operation `n` times per timed iteration and the row divides by `n` through `workUnits`, in the two shapes Plonky3 separates: `chainLatency` (dependent, one operation at a time) and `chainThroughput` (ten independent accumulators). Three properties are load-bearing, and each is there because the obvious alternative is measurably wrong: - **No array.** `Subtype` erases to its payload, but `Array` does not inherit that: every element is a `lean_object*` and `lean_box_uint64` allocates. A one-cycle dependent chain cannot be fed from a pointer array. This is also why the chain lengths are not Plonky3's element counts — matching the count would mismatch the working set. - **No `for` with `let mut`.** `ForIn` threads one state value, so ten mutable locals become a nested `Prod`, which has two relevant fields and does not erase: nine allocations per round around ten multiplies. Both combinators are tail-recursive with scalar parameters instead. - **The inner block is unrolled.** The `Nat` counter costs a `lean_nat_sub`, a `lean_dec` and a `lean_nat_dec_eq` per round, several times a Montgomery multiply. The counter now runs blocks of 64. Verified in the emitted IR rather than assumed. In `.lake/build/ir/CompPolyBench/Harness/SelfCheck.c` the specialised loops take `(lean_object* n, uint64_t acc)` and ten `uint64_t` accumulators respectively, contain zero `lean_alloc_*`, and spend one counter triple per 64 operations (latency) and per 40 (throughput). Two self-check groups, the chain analogues of `harness-floor` and `harness-canary`. `harness-chain-floor` carries the cheapest honest operation in both shapes: 530 ps per operation dependent and 109 ps ten-wide on an M3 Max, against a two-cycle pair at about 247 ps per cycle. The chain machinery therefore costs nothing measurable on top of the operation itself. `harness-chain-linearity` fails the run unless eight times the rounds costs at least four times as much; it measures 8.6x. The floor operation must mix two algebras, which is not obvious and cost a measurement to learn. The natural choice, `x ^^^ (x >>> 7)`, is the `GF(2)`-linear map `I + S`, and in characteristic two `(I + S) ^ 64` is `I + S ^ 64` — a shift right by 448, so a 64-deep block of it is the identity. LLVM finds this. The row reported 15 ps per operation, a sixteenth of a cycle, and the linearity check passed anyway, because what collapses is each block and not the loop over blocks. A wrapping add carries between bits and does not commute with the shift that way. Digest-neutral: `--medium --validate-only` over all groups gives 290 records against 286, the four new rows are the four added here, and no existing checksum moves. * feat(bench): share the per-field input, checksum and sink helpers `Univariate/Basic.lean` carried six `private` helpers — a fast-array conversion and a checksum for each of BN254, BLS12-381 and BLS12-377 — that the Montgomery arithmetic groups need too. Moved to a new `CompPolyBench/Fields/Inputs.lean`, together with Mersenne31's generator, conversion and checksum, and a sink for the eight-limb Montgomery carrier that reads two limbs instead of reassembling a 256-bit bignum. Not in `CompPolyBench.Common`, which every benchmark imports, because the field modules behind these are needed by a handful. The split is by import cost. Digest-neutral: the three curve groups validate to the checksums they had before. Deliberately excluded, and this is the surprise: `GF(2^64)` in the polynomial basis. `BF64.instFintype` (`CompPoly/Fields/Binary/BF64/Impl.lean:391`) is `Fintype.ofEquiv _ equivFin.symm`, a closed constant of a type whose value is a `Finset` of all `2 ^ 64` elements. Lean evaluates closed constants at module initialisation, so **any executable importing that module hangs before `main` runs** — `--list` never prints, memory climbs past 2.5 GB, and a sample shows the whole stack inside `_init_lp_CompPoly_BF64_instFintype___closed__3 → List.finRange`. Elaboration never notices, because the interpreter forces constants on demand, which is why the tests build. The BF64 and `Ext3` groups wait on a fix to that instance. * feat(bench): measure mul, add, inv and pow over the four small prime fields `BENCHMARKING.md` §13 names Plonky3 as the peer for BabyBear, KoalaBear, Goldilocks and Mersenne31 arithmetic. The suite measured Goldilocks `mul` and `inv` and nothing else on that list, and measured those with the operand-pool body shape, which reports the harness rather than the field. Sixteen groups: `mul`, `add`, `inv` and `pow` over the four fields, canonical `ZMod` beside the verified native-word representation, cross-checked by the group digest. `mul` and `add` carry a latency row and a throughput row, split the way Plonky3 splits `benchmark_mul_latency` from `benchmark_mul_throughput`, in one group under two digest classes. `inv` and `pow` carry latency only, as the peer does, over a chain twenty times shorter because one operation is tens of multiplications. The chain is seeded from an operand pool indexed by the iteration counter. One boxed array read per 1280 operations is under a tenth of a percent, and it buys a body that genuinely depends on `i` — so it is neither cached as a closed term nor hoisted out of the sample loop — and a digest over 64 inputs rather than one. The operation reaches `chainLatency` as a direct argument of an `@[specialize]` runner, never through a structure field or a `[Field F]` dictionary. This is why the group runners are written out one per field and operation instead of generated: a generated one would capture the operation in a closure, and an indirect call per operation is more than the operation. Verified in the IR — every fast row's loop specialises to `uint32_t` or `uint64_t` with zero `lean_alloc_*`, and KoalaBear's Montgomery multiply appears as unboxed 32- and 64-bit arithmetic with no boxing at all. `fields-goldilocks-mul` and `fields-goldilocks-inv` keep their keys but are now chained, so their digests change; `Fields/Goldilocks.lean` folds into the shared runner and `add` and `pow` join it. On an M3 Max at `--small`, per operation: | | latency | throughput | |---|---:|---:| | KoalaBear `mul` (fast) | 3.24 ns | 0.54 ns | | BabyBear `mul` (fast) | 3.34 ns | 0.53 ns | | Mersenne31 `mul` (fast) | 2.22 ns | 0.42 ns | | Goldilocks `mul` (fast) | 3.31 ns | 0.68 ns | | KoalaBear `add` (fast) | 1.12 ns | 0.60 ns | Roughly 13 cycles of dependent latency against 2.2 cycles of throughput for a Montgomery multiply, which is the shape of the algorithm rather than of the harness: the chain floor is 0.53 ns for a two-cycle pair. Inversion is 139 ns on fast KoalaBear against 1.14 us canonical, and 410 ns on fast Goldilocks against 8.66 us. One asymmetry the coverage turned up and does not explain: canonical BabyBear `mul` is 32.0 ns per operation against 5.9 ns for canonical KoalaBear and Mersenne31, all three being `ZMod p` for a 31-bit prime. * perf(fields): give BabyBear the explicit Field instance KoalaBear already has `KoalaBear/Basic.lean:63` declares `instance : Field Field := ZMod.instField fieldSize`. `BabyBear/Basic.lean` did not, and left synthesis to find the path itself. The two fields are otherwise the same shape — `abbrev Field := ZMod fieldSize` for a 31-bit prime — so the new `fields-babybear-mul` group put them side by side and the gap was visible immediately: | canonical `mul`, per operation | before | after | |---|---:|---:| | BabyBear | 32.0 ns | 5.92 ns | | KoalaBear | 5.94 ns | 5.94 ns | | Mersenne31 | 6.02 ns | 6.02 ns | 5.4x, and it lands exactly on the two fields that already had the instance. This is the case `CLAUDE.md` describes under Performance Guidelines: prefer an explicit instance construction where the synthesis path is long. `lake build` is warning-clean, `lake test` passes, and `lake exe axiomsweep --check` reports no new taint. * feat(bench): measure the eight-limb Montgomery multiply `mul` over the BN254, BLS12-381 and BLS12-377 scalar fields, canonical `ZMod` beside the eight-limb Montgomery carrier, latency and throughput. Inversion over these carriers already has `fields-mont64x8-*-inv`, which compares three algorithms rather than two representations, so this adds multiplication only. A quarter-depth chain: a 256-bit Montgomery multiply is an order of magnitude more than a 32-bit one and the canonical row three further orders, so the full depth would put one iteration past the sample budget. Choosing a shorter depth exposed a footgun, now closed. `chainLatency` runs whole `unrollBlock`s and `chainThroughput` whole `throughputUnroll`s, so a depth that is not a multiple of one is silently rounded down — and a row that took `workUnits` from the depth it *asked* for would then divide by operations the machine never performed. `latencyUnits` and `throughputUnitsOf` compute what the chain actually does, and every row now takes `workUnits` from those. A mismatched pair fails the group's workUnits check instead of reporting a number. On an M3 Max at `--small`, per operation: the eight-limb multiply is 37.8 ns (BN254), 39.7 ns (BLS12-381) and 37.3 ns (BLS12-377) against 196-212 ns canonical, a little over 5x. Throughput barely beats latency — 35.7 ns against 37.8 ns for BN254 — because each operation allocates its eight-limb result, so the chain is bound by allocation rather than by the dependency it was built to expose. * feat(bench): sweep the multiplicative NTT on its own, over size `BENCHMARKING.md` §13 names the multiplicative NTT as one of the operations to measure against Plonky3, and the only way to see it here was as one term of `univariate-mul-*`. Ten groups sweep the forward and inverse transforms over `n = 2^8` to `2^16` on KoalaBear and BabyBear, reference radix-2 against the planned radix-4, in one group per size under two digest classes. `workUnits` is the radix-2 butterfly count, `n / 2 * log n`. It is a property of the problem: giving the radix-4 row its own smaller count would divide away the algorithmic advantage the group exists to show. Bit reversal stays out of the timed region. `Plan.forwardImpl` returns bit-reversed output and `Plan.inverseImpl` expects bit-reversed input, so the forward group puts the permutation in the planned row's checksum — used only in the untimed pass — with an explicit sink so the default cannot drag it back in, and the inverse group permutes that row's input once, before timing. The permutation is defined locally rather than imported from `NTT.Transform.bitRevPermute`, which the reference transform is itself built from: importing it would let one wrong `bitRevNat` produce two compensating errors and a group that agrees on a wrong digest. Every body reads its input from a two-entry pool indexed by the iteration counter, and that is load-bearing. The first version precomputed the spectrum with the very expression the forward reference row then timed; the compiler recognised the two as one and the row reported 6 ns for a `2^12` transform, 1.6 million iterations per sample, identically at every size. The plan construction group had the matching failure from the other documented cause — `Plan.ofDomain d` for a literal `d` is a closed term, evaluated once and cached — and reported 32 ns for both of its sizes. On an M3 Max at `--small`, per butterfly: the planned transform is 3.4-5.6 ns and the reference 82-124 ns, a factor of about 25. The reference is why the sweep splits at `2^12`: one reference inverse is 2.5 ms there and 53 ms at `2^16`, past the sample budget, so above the cap the groups carry the planned rows alone and the cross-check lives at the sizes below. Plan construction is 58.7 us at `2^12` and 837 us at `2^16` — linear, and about half a transform at the larger size, which is the number a caller tempted to rebuild a plan per transform needs to see. * feat(bench): measure Reed-Solomon encoding and the schoolbook/NTT crossover Two groups the roadmap has wanted and the suite has never had. **Reed-Solomon encoding.** `ReedSolomon.encode` evaluates the message polynomial at every domain node by Horner, `Θ(n · k)`; `nttCodeword` is the forward NTT, `Θ(n log n)`. They are *equal*, not merely equivalent — `forwardImpl_eq_encode` — so the group digest checks the identity rather than only cross-checking two implementations of a shared spec. Rate one half, the FRI setting. At `n = 2^8` the definitional encoder is 887 us against 125 us; at `2^10`, 17.0 ms against 0.60 ms. The quadratic row is why the paired groups stop at `2^10`, with a third group carrying the NTT encoder alone at `2^14`. Worth noting from those numbers: `nttCodeword` is built on `Forward.forwardImpl`, the reference radix-2 transform, so it inherits the 25x the new `ntt-*` groups measure against the planned one. Routing the certified encoder through a `Plan` is a change to `CompPoly/`, not to `bench/`, so it is left alone here. **Crossover.** Six sizes from degree<4 to degree<1024, schoolbook against the planned NTT pipeline. The crossover falls between 8 and 16: schoolbook wins at degree<4 (3.05 us against 3.97 us) and degree<8 (7.89 against 8.10), and loses from degree<16 (18.1 against 16.6) upward, reaching 41.7 against 32.7 at degree<32. Read that with a caveat the per-unit column makes visible: both rows sit within a third of 1 us per coefficient at *every* size across a 256-fold range. An NTT is `k log k`, so a cost exactly linear in `k` over that range says the shared `CPolynomial` path — canonicalisation and allocation — sets the scale for both rows, and the crossover measured here is a property of the API rather than of the transforms underneath it. Both groups index a two-entry input pool by the iteration counter, for the reason recorded in `NTT/Transform.lean`. * chore(tests): delete the two orphaned `#eval` benchmarks Neither was imported by `tests/CompPolyTests.lean`, so neither ran under `lake test` or in CI, and neither carried a `#guard` or a theorem. They printed timings through `#eval` at elaboration time and were invoked by hand. `BENCHMARKING.md` §12.6 recorded a deliberate decision to keep `Univariate/NTT/Benchmark.lean`: it held the only NTT-vs-schoolbook crossover logic in the repo and was "the specification for a future crossover metric". That metric is now the `univariate-mul-crossover-*` groups, so the commitment is discharged and the file goes with it. `Bivariate/KroneckerBenchmark.lean` measured the Kronecker-backed multiply that `bivariate-full-*` already covers. The audit sections of `BENCHMARKING.md` describe the state they audited and are left saying so; only the backticked paths are adjusted, in the shape §1.3 already uses for `CommonBench.lean`, so `python3 ./scripts/check-docs-integrity.py` stays green. * feat(bench): measure the tower's table-driven kernels against its recursive ones `Tower/FastDefs.lean` carries `GF(2^8)` multiplication, `GF(2^64)` multiplication and `GF(2^64)` inversion twice — once as the recursive tower construction, once driven by a precomputed table — proves the two equal, and never measured which is faster, which is the only reason the table exists. All six are bare `UInt64` kernels, so they chain with nothing to unbox and nothing to allocate. Per operation on an M3 Max at `--small`: | | recursive | table | | |---|---:|---:|---:| | `GF(2^8)` mul, latency | 18.4 ns | 2.49 ns | 7.4x | | `GF(2^8)` mul, throughput | 5.76 ns | 0.31 ns | 18x | | `GF(2^64)` mul, latency | 169 ns | 15.7 ns | 10.8x | | `GF(2^64)` inv, latency | 304 ns | 44.2 ns | 6.9x | The `GF(2^8)` group needs its operands below `2 ^ 8` and the bound is not cosmetic: `mul8T_eq_mul8` (`Tower/Fast.lean:441`) holds only there, because `mul8T` indexes a 65536-entry table with `(a <<< 8) + b`. Fed full machine words the first version read out of range, `get!` returned zero, and the group reported both a digest mismatch and a table that looked 4x *slower* than the recursion at latency while 10x faster at throughput. The agreement check caught it; the timings alone would not have. `ChainRep` and the four chained-group runners lose their `private` so this file can use them. They stay in `Fields/Arith.lean` rather than moving beside `Harness/Chain.lean`, which deliberately does not import `runTimedSpec`. * docs(bench): record the coverage work, and the two ways a body goes missing `bench/README.md` gains the group inventory for the new families, the per-unit column and the two chain shapes, a warning that a per-unit number is not comparable with `harness-floor`, and the chain half of the self-check. `docs/wiki/benchmarking.md` gains a "Chained bodies" section — the three load-bearing properties of the combinators and the two call-site rules that are easy to get wrong — and splits the "make the body depend on `i`" step into its two distinct failure modes, closed-term caching and loop-invariance, each with the group here that hit it. Its known-gaps list loses what this closes and gains the `BF64.instFintype` blocker in full, so nobody spends an afternoon rediscovering that importing that module hangs the executable before `main`. `BENCHMARKING.md` gains §12.7. `ROADMAP.md` item 6 marks operation-level coverage done and narrows what remains to baselines and the external comparison. `bench/ci-groups.txt` grows from 44 keys to 59: every new family is represented, and where a family is a sweep, the middle of it stands in for the rest — a body that is wrong at one size is wrong at all of them. The gate got cheaper anyway, ~34s to ~29s of CPU, because the BabyBear `Field` instance that the coverage turned up speeds up every canonical BabyBear row in the set. Two labels the new report made wrong are fixed while here: the canonical inverse rows said "inv (Fermat chain)" when `ZMod.inv` is extended Euclid, and the two binary-tower rows rendered identically because they shared a field label as well as a method.
…d-zkEVM#325) Keep Mathlib’s default tensor actions and expose the right-action basis through the generic API. Preserve the binary-tower compatibility import. Reviewed and validated PR head: 118a533.
Restore module-level references for the tensor basis construction. Reviewed and validated PR head: 38a771e.
…fied-zkEVM#326) Reviewed and validated PR head: 7080201.
Reviewed and validated PR head: 9ba604f.
…tes (Verified-zkEVM#330) Reviewed and validated PR head: 1672483.
…-zkEVM#331) Reviewed and validated PR head: 6b2b9f2.
Reviewed and validated PR head: 8bafbba.
…zkEVM#328) Reviewed and validated PR head: 3ad9a16.
Reviewed and validated PR head: de73ab5.
…ied-zkEVM#334) Reviewed and validated PR head: e055696.
…-zkEVM#335) Reviewed and validated PR head: 5850f8c.
…r basis (Verified-zkEVM#341) Reviewed and validated PR head: 5cedfc8.
…he abstract tower (Verified-zkEVM#343) Reviewed and validated PR head: 3293141.
…ed-zkEVM#345) Reviewed and validated PR head: ac3f637.
…ower (Verified-zkEVM#344) Reviewed and validated PR head: d613a0e.
…r instances (Verified-zkEVM#342) Reviewed and validated PR head: cfc67e7.
Reviewed and validated PR head: c04946e.
Fresh-kernel leanchecker replay of the sextic and quintic irreducibility proofs fails with "(kernel) deep recursion detected". Pass the concrete ZMod fieldSize Field and Fintype instances explicitly to the Rabin wrappers and add the sextic addDeclCore replay regression. The theorem statements, polynomials, certificates, and Fact instances are unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CGr4BwA4aq2b4seaRKoLzs
This was referenced Sep 21, 2026
Author
|
Closing: the challenge pins this commit directly from my fork (proximity-prize/proximity-prize#569), as it pinned |
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
11 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
TL;DR
1e470b46still lacks for the Proximity Prize verifier: the KoalaBear sextic and quintic irreducibility proofs fail a fresh kernel replay with(kernel) deep recursion detected.ZModinstances explicitly insexticPoly_irreducibleandquinticPoly_irreducible; statements, polynomials, certificates and axioms are unchanged. A regression test replays the imported sextic proof body in a fresh kernel.mainis upstream as of 11 August with no commits of its own, and the fix has to sit on upstream1e470b46(Lean v4.33.1, Mathlib0df444a3), the CompPoly revision pinned by ArkLib65dea00c, the ArkLib the Proximity Prize migration uses. Supersedes fix: support Lean 4.33.1 and sextic proof replay #1.rabin-explicit-qon 4.32.2. Merging intomainis not required for that; hosting it as a branch works the same way.To review just our change: the "Fix KoalaBear irreducibility proof replay" commit in the Commits tab, or
git log -1 -p yudduy/fix/sextic-replay-lean-4.33.1.Why
The proof elaborates fine; only re-checking the stored proof term in a fresh kernel blows the default recursion limit, because instance resolution takes a different, deeper path than the certificates were built on. Upstream Verified-zkEVM#306 added the
_of_cardwrappers; the remaining fix (Verified-zkEVM#323 upstream, closed in favour of this fork) is to hand the wrapper the sameFieldandFintypeinstances the certificates use.Upstream has since removed the unsafe form altogether (Verified-zkEVM#369, on Lean v4.34.0). The challenge stays on v4.33.1 because that is the Prove2me environment, and ArkLib
65dea00cpins1e470b46, which predates Verified-zkEVM#369, so this fix lives here until the challenge moves to v4.34.Where to review
CompPoly/Fields/KoalaBear/Ext6/SexticIrreducible.leanandExt5/QuinticIrreducible.lean: the explicit instances must leave the theorems being proved unchanged.tests/CompPolyTests/Fields/KoalaBear/SexticReplay.lean: imports the module and re-adds the proof under its own statement withaddDeclCoreat trust level 0, so a regression shows up inlake testrather than on the verifier.Tested
lake build: clean, no warnings.lake test: all 75 test modules pass, including the new replay test, which fails on the unfixed sextic proof withSextic kernel replay failed: (kernel) deep recursion detected.lake env leancheckeron both modules now exits 0 (both failed before; the quintic failure was found while checking this change).#print axiomson both theorems:propext,Classical.choice,Quot.sound. The repository's axiom sweep reports no sorry or non-standard axioms across all 355 modules.Please review
main, or host the commit as a branch the challenge pins directly, as withrabin-explicit-q? Either works for #569. For the branch:git fetch https://github.com/yudduy/CompPoly.git fix/sextic-replay-lean-4.33.1, push it under whatever name you use, and close this.🤖 Generated with Claude Code
https://claude.ai/code/session_01CGr4BwA4aq2b4seaRKoLzs