KZG recursive verifier - #563
Draft
gabriel-barrett wants to merge 26 commits into
Draft
Conversation
gabriel-barrett
force-pushed
the
kzg
branch
3 times, most recently
from
August 18, 2026 18:59
4175c60 to
41a730a
Compare
Track multi-stark branch pcs-traits at d3627b0c. Upstream generalizes the prover/verifier core over crate-owned Pcs/Transcript/ EvaluationDomain/field traits (FRI path pinned byte-identical under a serialized-proof hash) and adds an arkworks BLS12-381 KZG backend behind the "kzg" feature as the terminal, natively-verified stage. No ix-side changes: the consumed surface (config aliases, re-exports) is unchanged and proofs are byte-identical, so vk codec, codegen, and all FFT/shard pins hold as-is.
Aiur is moduleless: names inside the DSL quotations resolve at toplevel merge, not at Lean elaboration, so a DSL file never needs to import another DSL file. Only the assembly points (IxVM/Toplevel.lean, MultiStark.lean) reference the module values at the Lean level and keep their imports. Every DSL file now imports Ix.Aiur.Meta alone.
The recursive verifier computes on the inner proof's field (Goldilocks); today Aiur's outer field IS Goldilocks, so the arithmetic is native. To make that an implementation choice rather than an assumption, the whole inner-field surface moves into GoldilocksNative.lean — types, values, and operations, base and extension, every function always-inlined: - types: Goldilocks (native: G itself), ExtGoldilocks = [Goldilocks; 2]; - pure values: g_zero/g_one/g_two, the binomial modulus g_w, the coset generator g_generator, the maximal two-adic root g_two_adic_root; - base ops: g_add/g_sub/g_neg/g_mul, g_is_zero, the hinted gl_inverse; - extension algebra: eg_add/eg_sub/eg_neg/eg_mul/eg_inverse/eg_div/ eg_eq, written entirely over @g_* calls (representation-agnostic); - byte boundaries: gl_val/gl_lt_p/gl_to_bytes. Goldilocks.lean is folded in and removed. A future GoldilocksForeign provides the same interface over a non-Goldilocks outer field (byte-limb representation; the KZG terminal stage) — swapping fields becomes a toplevel-merge choice, no verifier-side changes. Codegen: the wrappers referenced from compiled circuits survive pruning as empty circuits (deactivated by sparse activation, zero column cost), shifting function indices; kernel codegen is untouched. multi-stark and recursive-verifier suites pass.
…face FRI-side base-field sites converted: exp_by_bits (square-and-multiply), fri_fold2 (the 1/2 and 1/(2s) folds), ro_x (the GENERATOR coset shift, now @g_generator()), the bucket initializers, the final-poly zero check, and every base-to-extension embedding ([x, 0] → [x, @g_zero()]). Native counter/byte arithmetic (block flags, list lengths, index bits) stays native — under a foreign field those remain outer-field values. Codegen regenerated (g_one/g_two/g_generator now referenced from compiled circuits, surviving prune as empty deactivated circuits); multi-stark and recursive-verifier suites pass.
…interface The remaining base-field sites: two_adic_gen (the maximal root is now @g_two_adic_root(), the squaring chain @g_mul), pow2 (2^L as a field value), the selector/vanishing embeddings, from_ext_basis's [0, 1] basis element, pair_mul's binomial modulus (@g_w()), the logUp fold and fingerprint initializers, the boundary-injection normalization 1/(n·g), the public-input embeddings, and every base-to-extension [x, 0] literal. ext_is_zero goes through @g_is_zero. Native counters, selector flattening, and bitmap booleanity asserts stay native. With this, Pcs.lean and Verifier.lean contain no raw inner-field arithmetic: the g_*/eg_* interface (GoldilocksNative.lean) is the single representation point. Codegen regenerated; multi-stark and recursive-verifier suites pass.
…interface The same interface as GoldilocksNative.lean (types, values, base ops, extension algebra, byte boundaries), implemented WITHOUT assuming the outer field is Goldilocks: an element is its canonical value < p as 8 LE bytes, ops are carry/borrow/product chains over the u8 gadgets (64×64→128 schoolbook multiply + Plonky3's reduce128), so the module only assumes byte sums cannot wrap — any large outer field works (the KZG terminal stage's BLS12-381 scalar field). Recovered from Goldilocks.lean's pre-nativization history (2b0924d) and adapted to the interface names. Divergences from native, same semantics: gl_inverse is Fermat (the unconstrained_g_inverse hint speaks the outer field, useless here), gl_val is one conditional subtraction of p, gl_to_bytes is the identity, g_is_zero is a byte-sum test. Exactly one of goldilocksNative/goldilocksForeign merges into a toplevel (same names by design); the verifier keeps native — the wire layers (Deserialize's Ext, challenger plumbing) still assume the native representation, and swapping them is the actual field-migration step. Until then the module compiles as its own toplevel in the multi-stark suite, passing the pre-nativization gl_ops_ref byte vectors (the same vectors the native form pins) plus boundary and two-adic-root checks.
Wrapping the recursive verifier over BLS12-381: architecture, the survey of what is actually tied to Goldilocks (one alias per side), the field-independence observation that lets the foreign verifier be developed entirely on the Goldilocks stack, and the phased plan — A: genericize crates/aiur over the field (pin-gated no-op); B: the foreign verifier toplevel, validated by execution over Goldilocks; C: cost checkpoint + declaration-level inlining; D: KZG instantiation end-to-end at toy scale; E: scale, ceremony SRS, tuning.
crates/aiur no longer assumes Goldilocks: every struct and function is parametrized by an AiurField — multi-stark's crate Field + TwoAdicField + Ord plus canonical-u64 extraction, the one thing the executor needs beyond the traits (only ever called on bytes/pointers/counters and the 8-byte hint, so >64-bit fields may truncate, with the documented caveat that their toplevels must not use the hint). Goldilocks stays the only instantiation (`G`), wired as a DEFAULT type parameter on every public type (Toplevel<F = G>, QueryRecord<F = G>, AiurSystem<SC = AiurConfig>, ...), so ffi and the codegen'd runners compile completely unchanged. Field-specific content that moved behind the abstraction: the gadget carry constants (256^-1, (2^32)^-1) are computed generically instead of pinned Goldilocks literals; p3 trait imports (PrimeCharacteristicRing, PrimeField64) are gone from every module except the Goldilocks AiurField impl; the unconstrained-inverse hint keeps its total 0 -> 0 semantics explicitly (the crate trait leaves inverse(0) free and the p3-backed impls panic). AiurSystem::build stays concrete (it constructs the FRI config); circuit-input synthesis is the generic build_circuit_inputs, ready for a KzgConfig instantiation (Phase D). vk_codec remains Goldilocks-only by instantiation (it defines the stage-2 vk wire format). Gate (behavioral no-op): ix codegen --check byte-identical for both generated files; all 79 kernel FFT pins + the shard pin (6_713_306_166) unchanged; aiur/multi-stark/recursive-verifier suites and the Rust workspace tests pass; clippy clean.
Lean-side constants no longer pass through Goldilocks: Term.field, Pattern.field, Op.const, and match keys carry exact Nats from the elaborator (G.ofNat's silent mod-p wrap is gone from the source path) through every compiler stage. Specialization to a concrete field happens at each consumer, and overflow is a hard ERROR — a constant >= p means the field cannot represent the circuit — never a wrap. With that in force, injectivity is free: distinct match keys stay distinct in every accepted field, so no collision check is needed. - Lean interpreters (BytecodeEval/SourceEval/Interpret): on-the-fly checked embedding (G.ofNat?); overflow raises constantOverflow, and an unrepresentable pattern key matches no value. - FFI (lean_nat_as_field): decodes scalar and GMP-boxed Nats — values in [2^63, p) are boxed, so the old scalar-only read would have broken on them — and panics with the overflow message. - Codegen: Bytecode.Toplevel.checkConstants (off Block.maxConstant) guards emission in the codegen command. Gate: codegen --check byte-identical for both generated files; kernel FFT + shard pins exact; aiur/multi-stark/recursive-verifier suites and the Rust workspace green; clippy clean.
The first Phase-D slice: the Phase-A-generic Aiur pipeline instantiated over the KZG terminal stage. AiurField for multi-stark's Scalar (canonical-low-u64 extraction; exact for the bytes/pointers/counters Aiur reads), and AiurSystem::build_kzg wiring build_circuit_inputs into KzgConfig — D = 1 stage-2 layout, Blake3 transcript, caller-supplied SRS. The FRI parameter fields are vestigial in this instantiation (FRI-vk-codec-only) and stored zeroed. kzg_tests prove and verify a function circuit and the byte-gadget path (Bytes2's 65536-row preprocessed table committed per column via MSM) over Fr, with tamper rejection — the same pipeline the Goldilocks tests run, KZG commitments instead of FRI. Multi-stark bumped to 4aec5a4 (Scalar: Display + canonical_low_u64; additive, FRI pin re-verified). Feature-gated: the default build and all pins are untouched.
multi-stark's FriPcs now retains and exposes its construction parameters (bump to 3cd5316), so the duplicated commitment_parameters/fri_parameters fields on AiurSystem are gone — the vk codec reads them from the system's config. The KZG instantiation loses its zeroed vestigial fields entirely: parameters live on the PCS that owns them, in both backends. vk bytes unchanged; verifier suites and both Goldilocks/KZG Aiur tests pass.
Verification never needs the prover bundle: the encoder becomes system_to_bytes(&System) (parameters read off the System's own PCS), the decoder returns a bare System (parameters live in its config, not a side tuple), and AiurSystem exposes .system() as the verification-sufficient view — toplevel, prover key, and slot widths are prover-side only. The FFI vk export goes through the System-level entry point. vk bytes unchanged; verifier suites pass.
…itter Main's #570 taught the emitter to promote zero-multiplicity hint entries at call and return sites instead of blind-inserting; the recursive-verifier toplevel is generated on this branch, so its runner re-emits under the new pattern. The kernel runner (aiur_ixvm.rs) stays byte-identical to main's — this branch's changes don't alter its emission.
…ase B) The wire layer moves onto the inner-field interface, so the verifier program compiles against either Goldilocks module: - Deserialize: Ext = [Goldilocks; 2]; count_to_bytes (the canonical byte decomposition of an outer-field count, with the < p uniqueness pin) for the vk shape observations, where the foreign gl_to_bytes — an identity on byte-repr values — cannot serve. - SystemDeserialize: Const carries the inner-field representation; ConstSmall ingests through the new gl_from_u16 interface constructor (two raw bytes, no outer-field detour). - Pcs: ro_fold ingests raw lanes via gl_val instead of limb_to_field (identical under native; lands in the byte representation under foreign). limb_to_field stays for outer-field wiring (counts, digest limb compares). - Verifier: pow2 and inorm (the last-row normalization 1/(n·g)) are Goldilocks-typed — they always were semantically. multiStarkForeign = the same merge chain over goldilocksForeign (237 fns vs native's 218). Gate: the new foreign-verifier suite executes it under the Goldilocks interpreter against the factorial stage-2 vectors — honest proof accepted, tampered proof and tampered claim rejected — validating the exact program stage 3 proves over BLS12-381, before any Fr machinery exists. The native verifier runner re-emits with the new wiring (count_to_bytes joins the closure); all native suites unchanged and green.
The KZG instantiation reaches Lean: AiurKzgSystem (external class over AiurSystem<KzgConfig>) with build (dev-grade SRS — bring-your-own parameters come later), proveMultiStark over the raw proof/vk/claims advice blobs, and the native two-pairing verify, the proof travelling as bytes. The FFI toplevel decoder is generic over the outer field (LeanField: checked exact-Nat embedding per field; constants > 2^64 reject loudly rather than guess a multi-limb encoding), and the advice buffer builder generalizes (verifier_io_buffer_in). The kzg feature is always on in the lake build: stage 3 is part of the pipeline. Gate (kzg-verifier suite): prove the foreign verifier's acceptance of a factorial stage-2-style proof over the BLS12-381 scalar field, verify natively, reject a tampered wrap. Measured at toy scale: 43 MB wrap proof, ~21 min prove (dev SRS 2^17, single-threaded, interpreter execution) — the wrap works, and the width cost lands where the plan predicted (Phase C is what shrinks it).
With call-site splicing, every @-call of a foreign interface op inlined its whole byte-gadget body into the CALLER: one g_mul ≈ 930 u8 lookups (reduce128 contains a second mul128), one @eg_mul site ≈ 14k caller columns — the foreign toplevel measured ~386k effective columns, and since the KZG proof carries a commitment point plus two openings PER COLUMN, a 43 MB wrap proof. The heavy interface fns (g_add/g_sub/g_mul/gl_inverse/gl_val, the eg_* family) become thin @-inlined wrappers over plain, memoized *_impl calls: a call site costs one lookup, the byte-gadget width lives once in the impl circuits, and repetition becomes rows there (deduplicated by by-argument memoization). Call sites in Pcs/Verifier stay textually identical; the native module is untouched (its ops splice to trivial arithmetic — the reason the inline convention exists). Pure values and byte logic (g_zero…, g_is_zero, gl_lt_p, gl_from_u16, gl_to_bytes) stay genuinely inline. Measured at factorial scale: foreign width 386k → ~12k effective columns (native: 7.7k); KZG wrap proof 43 MB → 1.38 MB; prove 21 → 7.5 min. All gates re-run green: foreign self-tests, the foreign-verifier interpreter suite, and the kzg-verifier wrap (accept + tamper-reject). Codegen byte-identical (native toplevel unchanged).
The impl circuits still spliced their byte-vector helpers: g_mul_impl carried mul128 twice (reduce128 re-multiplied by EPSILON) at ~930 u8 lookups per copy. Three changes: - add8/sub8/mul1/add16/mul128 are plain memoized circuits now — no circuit carries another's carry chain; only per-byte steps (adc, sbb), the lookup-free select8, and value constructors stay spliced. - reduce128's EPSILON term drops its multiplication entirely: x_hi_lo·(2^32 − 1) = (x_hi_lo << 32) − x_hi_lo, one sub8 (exact in 64 bits; cannot borrow). - stale module docstring (pre-merge status) refreshed. g_mul_impl: 2020 → 144 columns. Foreign−native width delta 6450 → 4931 (D=2 accounting); the KZG wrap proof 1.38 MB → 1.26 MB, prove ~7.5 → ~6.8 min. The remaining delta is dominated by the by-value byte representation at call boundaries (an Ext is 16 caller columns vs the native 2), not by gadget splicing. All gates green: fg_* self tests, foreign-verifier interpreter suite, kzg-verifier wrap.
The remaining foreign-vs-native width gap was the by-value byte representation at every boundary: an Ext cost its holder 16 columns (vs the native 2) in call arguments and outputs, list nodes, and enum fields — ood_loop and logup_steps_fold alone carried +600 columns each with zero byte arithmetic in them. Goldilocks becomes &GBytes (the digest-pointer pattern): values thread by content-addressed pointer — one holder column, an Ext two, exactly the native widths — and only the impls load the bytes (the byte primitives keep working on raw GBytes; load/store happens once per impl). Equal values share a pointer, so memoization survives. The interface and every call site in Pcs/Verifier stay textually unchanged; self-tests store their literals and load for asserts. Measured: foreign width 8,489 columns (D=2 accounting) vs native 7,176 — within 18%, from 386k at the start of the width hunt; the KZG wrap proof 1.26 MB → 854 KB (43 MB originally), prove ~6.5 min. All gates green: fg_* self-tests, foreign-verifier interpreter suite, kzg-verifier wrap (accept + tamper-reject).
After each constant's stage-2 (outer) prove, --kzg wraps that proof: the FOREIGN verifier's acceptance of it is proven over the BLS12-381 scalar field under the KZG backend (AiurKzgSystem, dev-grade SRS of size 2^--kzg-log-srs), then verified natively. The stage-2 proof plays the role the stage-1 proof played for stage 2 — advice bytes, with the stage-2 vk and claim digest-bound as the public input. Rows gain kzg-prove-time / kzg-peak-rss / kzg-proof-size / kzg-verify-time; the pipeline ledger (total-time, pipeline-peak-rss) includes the wrap and requires it before closing the row. Requires --recursive. First measurement, Nat.add_comm at 40 queries: stage 1 prove 1.8 s / 4.5 GiB; stage 2 prove 44 s / 59 GiB (3.4 MB outer proof); stage 3 execution 2.8 min / 59 GiB, witness 25 s / 469 GiB peak — the full Fr trace materialized at once — and the commit phase hit a 2^23-row circuit beyond a 2^20 SRS. Streamed witness + parallel MSM are the prerequisites for running this at benchmark scale.
… bump Two unconstrained hint ops for emulating Goldilocks inside a large outer field: unconstrained_gl_divmod(v) = (q, r) with v = q·p_goldilocks + r over the canonical integer of v, and unconstrained_gl_inverse(v) = v⁻¹ mod p_goldilocks. Threaded through every layer (DSL syntax, stages, checker, lowering/layout as 2 / 1 fresh auxiliaries, the three Lean interpreters, the Rust interpreter/trace/constraints, codegen emission, FFI tags 34/35). Per-field semantics live on AiurField: Goldilocks returns (0, v) and its own inverse; the BLS12-381 scalar does the 256-bit long division and an inverse via Goldilocks arithmetic. multi-stark 3283ff4: Scalar::canonical_limbs_le / from_limbs_le, and ark-ff/asm (kzg) + arkworks parallel MSM/FFT (parallel) — the KZG commit phase ran serial MSMs regardless of the crate's parallel flag. Native codegen byte-identical (the ops are unused by the native toplevels); all existing suites green.
…y check For an outer field wider than p² (BLS12-381 Fr), a Goldilocks value is one outer element < p and every op computes exactly in the outer field, reducing by CHECK instead of by limb arithmetic: x·y = q·p + r with q, r < p (unconstrained_gl_divmod, one degree-2 identity, two 8-byte range checks), x + y and (x + p) − y with a boolean q, the inverse hinted (unconstrained_gl_inverse) and pinned by one multiplication. p is spelled 4294967295·4294967296 + 1 so no literal exceeds p; the module still runs under Goldilocks (hint (0, v), degenerate but correct identities) for the self-tests and the interpreter gate. Evaluation order matters in the outer field: x − y + p wraps at x − y for x < y; x + p − y does not (labelled asserts now name the failing check). Measured on Nat.add_comm's 40-query stage-1 proof, same blobs through both verifiers: width 7,594 vs native 7,176 (was 8,489 after the pointer pass, 386k originally); FFT cost 1.44e11 vs native 1.09e11 — 1.32× (was 6.5×); interpreter execution 12 s vs 7 s (was 65 s). Toy KZG wrap: 33 s, 763 KB proof (was 6.5 min / 854 KB; originally 21 min / 43 MB). Gates green: fg_* self-tests (oracle vectors), foreign- verifier interpreter suite, kzg-verifier wrap (accept + tamper-reject).
Srs::unsafe_dev_setup generated τ-powers serially — 12+ minutes at 2^23, paid on every stage-3 run. Chunked, parallel under the parallel feature. Toy KZG wrap 33 → 22 s.
The aiur prove run now passes --kzg: after each constant's stage-2 prove, the foreign verifier's acceptance of that proof is proven over BLS12-381 under KZG and verified natively. The registry gains the "Stage 3 — FRI recursion on KZG (BLS12-381)" group (kzg-prove-time, kzg-peak-rss, kzg-proof-size, kzg-verify-time; thresholds 10% / 10% / 5% / 10%), the ledger's total-time and pipeline-peak-rss include the wrap, and the dashboard gains the stage-3 plots. bench-typecheck's dev SRS defaults to 2^23 (headroom over the ~2^22 tallest stage-3 trace at kernel scale). The benchmark jobs' timeout widens to 120 minutes. Measured through the CI path (ix bench run, watchdog, 50 queries) on Nat.add_comm: stage 3 prove 924 s, peak 84 GiB, 765 KB proof, native verify 0.17 s; pipeline total 973 s, RAM ceiling 84 GiB — inside the ~108 GiB CI ceiling. Heavy-tier constants, whose stage-2 prove already meets that ceiling, are expected to land stage 3 as oom rows (the registry's stated policy: soundness first, the OOM row documents the gap).
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.
No description provided.