KZG recursive verifier - #563
Draft
gabriel-barrett wants to merge 16 commits into
Draft
Conversation
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.
CI tracked the pipeline as disjoint benchmarks: aiur (stage-1 prove over the curated constants, plus a separate execute cell) and aiur-recursive (stage 2, but only over three fixed constants). Now the aiur benchmark IS the pipeline, per constant: every stage plus the total. Stage 1 proves the constant's IxVM typecheck, stage 2 executes and proves the in-circuit multi-stark verifier over that fresh proof; the KZG stages will fold in as they land. Rows close with the stage ledger (stage1-time / stage2-time / total-time, each stage = witness execute + prove), which also serves as the completion marker for teardown kills. The run covers the same Vectors.csv selection as before, under 40 FRI queries at log-blowup 2 for both stages (50 OOMs the CI hosts), so it lands on a fresh testbed (aiur-x64-32x) — not comparable to the old standalone aiur-check-prove series. The fast Phase-1 execute mode stays as an unscheduled local mode; the fixed-config registry machinery (recursiveConstants) and the !benchmark recursive token are gone with the backend they served.
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.