Conversation
akoidefi
force-pushed
the
feat/verifier-transpilation-gnark
branch
from
3a28852 to
920db4a
Compare
0xParti
force-pushed
the
feat/verifier-transpilation-gnark
branch
from
eb13040 to
c31c8c4
Compare
0xParti
requested review from
0xAndoroid,
markosg04,
moodlezoup and
sagar-a16z
as code owners
moodlezoup
left a comment
moodlezoup
left a comment
There was a problem hiding this comment.
Amazing work, just a few questions and nits
| fn challenge_scalar<JF: JoltField>(&mut self) -> JF { | ||
| self.challenge_scalar_128_bits() | ||
| } | ||
|
|
||
| fn challenge_scalar_128_bits<JF: JoltField>(&mut self) -> JF { | ||
| // Full 32-byte hash output = full Fr challenge (no truncation). | ||
| // challenge_bytes(32) → challenge_bytes32 → one hash invocation. | ||
| // from_le_bytes_mod_order(serialize_le(Fr)) = Fr (identity). | ||
| let mut buf = vec![0u8; 32]; | ||
| self.challenge_bytes(&mut buf); | ||
| JF::from_bytes(&buf) | ||
| } |
There was a problem hiding this comment.
| fn challenge_scalar<JF: JoltField>(&mut self) -> JF { | |
| self.challenge_scalar_128_bits() | |
| } | |
| fn challenge_scalar_128_bits<JF: JoltField>(&mut self) -> JF { | |
| // Full 32-byte hash output = full Fr challenge (no truncation). | |
| // challenge_bytes(32) → challenge_bytes32 → one hash invocation. | |
| // from_le_bytes_mod_order(serialize_le(Fr)) = Fr (identity). | |
| let mut buf = vec![0u8; 32]; | |
| self.challenge_bytes(&mut buf); | |
| JF::from_bytes(&buf) | |
| } | |
| fn challenge_scalar<JF: JoltField>(&mut self) -> JF { | |
| // Full 32-byte hash output = full Fr challenge (no truncation). | |
| // challenge_bytes(32) → challenge_bytes32 → one hash invocation. | |
| // from_le_bytes_mod_order(serialize_le(Fr)) = Fr (identity). | |
| let mut buf = vec![0u8; 32]; | |
| self.challenge_bytes(&mut buf); | |
| JF::from_bytes(&buf) | |
| } | |
| fn challenge_scalar_128_bits<JF: JoltField>(&mut self) -> JF { | |
| unimplemented!("128-bit challenges are unsupported for PoseidonTranscript"); | |
| } |
| // Full Fr challenge via challenge_scalar_128_bits, then wrap in Challenge type. | ||
| // Mont254BitChallenge<F> is a newtype of F → same memory layout → transmute is safe. | ||
| let scalar: JF = self.challenge_scalar_128_bits(); |
There was a problem hiding this comment.
| // Full Fr challenge via challenge_scalar_128_bits, then wrap in Challenge type. | |
| // Mont254BitChallenge<F> is a newtype of F → same memory layout → transmute is safe. | |
| let scalar: JF = self.challenge_scalar_128_bits(); | |
| // Full Fr challenge via challenge_scalar, then wrap in Challenge type. | |
| // Mont254BitChallenge<F> is a newtype of F → same memory layout → transmute is safe. | |
| let scalar: JF = self.challenge_scalar(); |
| sumcheck: SumcheckId, | ||
| ) -> Option<(OpeningPoint<BIG_ENDIAN, F>, F)>; | ||
|
|
||
| // === Methods for generic verifier (transpilation support) === |
There was a problem hiding this comment.
maybe add these methods to a new AbstractVerifierOpeningAccumulator<F: JoltField>: OpeningAccumulator<F> trait
There was a problem hiding this comment.
Yes, we addressed this in eff5f8c
We had to changed multiple files that imported this
| // ============================================================================= | ||
| // Serialization Implementations (required by trait bounds) | ||
| // ============================================================================= |
There was a problem hiding this comment.
nit: I think for empty structs, we should be able to #[derive(CanonicalSerialize, CanonicalDeserialize)]
| //! Currently supported: | ||
| //! - **gnark**: Go/Groth16 circuit generation (~250 constraints per Poseidon hash) | ||
| //! | ||
| //! esto es un delirio absoluto de claudio |
| // Fallback: create constant from bytes (for non-transpilation use) | ||
| MleAst::from_i128(0) |
There was a problem hiding this comment.
is this right? Should we just panic here?
| // pow2 contains precomputed powers of 2 for bit recomposition. | ||
| var pow2 [256]*big.Int |
There was a problem hiding this comment.
i think this is unused
| // Fallback for non-MleAst types (shouldn't happen in transpilation) | ||
| self.hash_and_update(MleAst::from_u64(0)); |
There was a problem hiding this comment.
can we panic here instead?
| // Panic is NOT pushed here — fiat_shamir_preamble sends it through | ||
| // append_u64, which calls raw_append_u64 (bypasses raw_append_bytes/FIFO). |
There was a problem hiding this comment.
I'm confused by this –– doesn't this mean that panic is not fully symbolic in the circuit?
There was a problem hiding this comment.
Panic is fully symbolic. It enters the circuit through two paths:
- Transcript: raw_append_u64 hashes it as a concrete constant into the Poseidon state (correct for Fiat-Shamir since the value is already committed).
- RAM MLE: allocated as witness variable io_panic_val, used by eval_io_mle for the panic contribution and termination checks.
Our comment was confusing because "NOT pushed here" referred to the byte-chunk FIFO, not to the circuit. Updated the comment to clarify da017a7
| "emulated.Element[emulated.BN254Fp]" | ||
| } | ||
| }; | ||
| output.push_str(&format!("\t{field_name} {go_type} `gnark:\",public\"`\n")); |
There was a problem hiding this comment.
I may be missing something, but aren't we making all of the circuit inputs public by doing this?
There was a problem hiding this comment.
Discussed on the call. All inputs are intentionally public right now because without PCS verification in the circuit (deferred pending PCS choice), commitments and proof data need to be externally verifiable. Once the PCS is integrated, we'll split public/private using the existing WitnessType infrastructure in AstBundle. The exact public surface still needs investigation since some inputs may benefit from staying public to save in-circuit range checks. Added a comment in codegen documenting this 9af2a73
|
This looks good to me; will merge once conflicts are resolved |
akoidefi
force-pushed
the
feat/verifier-transpilation-gnark
branch
from
9af2a73 to
31017f3
Compare
|
Review the following changes in direct dependencies. Learn more about Socket for GitHub.
|
|
Warning Review the following alerts detected in dependencies. According to your organization's Security Policy, it is recommended to resolve "Warn" alerts. Learn more about Socket for GitHub.
|
Adds PoseidonTranscript using light_poseidon over BN254. Uses width-3 Poseidon to include n_rounds in every hash call for domain separation, same as Blake2b/Keccak. Chunks large inputs into 32-byte pieces since Poseidon has fixed-width inputs. Gated behind transcript-poseidon feature flag.
Co-authored-by: Markos <53157953+markosg04@users.noreply.github.com>
- Add PoseidonParams<F> trait for type-level parameter configuration - Implement FrParams (uses new_circom) and FqParams (generated params) - Add poseidon_fq_params.rs with BN254 Fq parameters (128-bit security) - Create type aliases PoseidonTranscriptFr and PoseidonTranscriptFq - Fq params generated with poseidon-paramgen v0.4.0 (audited by NCC Group) This enables SNARK composition where sumchecks operate over Fq.
Stage 1 now works end-to-end with Groth16 prove/verify. The main issue was using the wrong transcript - proof was generated with Blake2b (default) but Go circuit uses Poseidon. Fixed by documenting that --features transcript-poseidon is required for gnark transpilation. Changes: - Add debug-expected-output feature flag for transcript debugging - Add detailed debug output for challenge derivation (behind feature flag) - Clean up old stage1_* files (replaced by stages16) - Remove obsolete debug tools and witness loader - Improve codegen and mle_ast for per-assertion CSE
…register claim reduction) Stage 3 adds 3 batched sumchecks to the transpiled verifier: - Spartan shift: verifies next-cycle values match trace - Instruction input: verifies operand constraints - Register claim reduction: batches register access claims Results (Stages 1-3): - Assertions: 5 (up from 4) - Constraints: 763,394 (+231,208 from Stage 2) - Groth16 prove: ~1.85s - Groth16 verify: ~1.44ms
Stage 4 adds 4 batched sumchecks: - Register read/write checking - RAM ra booleanity - RAM val evaluation - RAM val final Results (Stages 1-4): - Assertions: 10 (up from 5) - Constraints: 1,048,560 (+285,166 from Stage 3) - Groth16 prove: ~2.5s - Groth16 verify: ~1.5ms Bug fix: Added memoization to count_mul_by_zero() in transpile_stages.rs. Without memoization, the function hung for 6+ minutes due to exponential traversal of shared AST nodes (common subexpressions).
Stage 5 (Register val evaluation, RAM Hamming booleanity, RAM ra reduction, Lookups read-raf) now passes with 13 assertions and 1,531,516 constraints. Fixed stack overflow during code generation by converting recursive and functions to iterative implementations using explicit stacks. Stage 5's deeper AST exceeded stack limits even with 128MB stack size. Results: - Assertions: 13 (up from 10 in Stage 4) - Constraints: 1,531,516 (+482,956 from Stage 4) - Proof size: 164 bytes - Prove time: 3.78s - Verify time: 1.59ms
Add comprehensive tests to verify the generated circuit is performing real cryptographic verification and not passing blindly: - TestCorruptedWitnessRejected: Targeted corruption of commitment, PC claims, register values, RAM booleanity - all correctly rejected - TestRandomFuzzing: 20 random field corruptions, 100% rejection rate - TestAssertionCountMatchesTheory: Verifies 13 assertions match expected - TestCircuitNotTrivial: Validates 1.5M constraints, 5924 Poseidon hashes, 11839 multiplications - confirms real cryptographic work These tests provide confidence that the transpiled circuit is sound.
…hashing Add tools for benchmarking different Poseidon widths: - extract_poseidon_constants.rs: Generate Go constants for any width - poseidon_vectors.rs: Generate test vectors for verification - constants4.go, constants5.go: Pre-generated width-4/5 constants Benchmark results: width-4 (3 inputs) is optimal (+12.8% constraints for width-5). Also applies semantic fix to PoseidonAstTranscript: append_message, append_u64, append_scalar now use direct poseidon calls matching jolt-core's immediate hashing semantics.
Remove functions and binaries that depended on the old stage1_only_verifier: - Remove generate_stage1_circuit* functions from codegen.rs - Remove export_stage1_ast/export_stage1_poseidon_ast from ast_json.rs - Delete verify_final_claim.rs binary - Delete run_full_stage1.rs binary (was broken) - Update lib.rs exports The gnark-transpiler now uses transpilable_verifier exclusively for stages 1-5 verification.
Remove unused functions and imports that were left behind after the stage1_only_verifier cleanup: codegen.rs: - Remove unused imports (Bindings, common_subexpression_elimination_incremental, insert_node) - Remove unused method edge_to_gnark on MemoizedCodeGen - Remove dead CSE helper functions (~260 lines): - atom_to_gnark_with_offset - edge_to_gnark_with_offset - generate_gnark_expr_with_vars_and_offset - generate_gnark_expr_for_node_with_offset - generate_gnark_expr_with_cse - Fix unused variable warning with matches!() macro ast_json.rs: - Remove unused import get_node - Remove dead tree traversal functions (~80 lines): - collect_nodes_from_root - collect_vars_from_node - collect_vars_from_edge transpile_stages.rs: - Remove unused imports (ark_ff::PrimeField, serde::Serialize) - Fix unused mut warning on accumulator - Fix unused variables (indent, Poseidon match arms)
Co-Authored-By: akoi <197815935+akoidefi@users.noreply.github.com>
Enable transpilation of Jolt programs that use TrustedAdvice (e.g., merkle-tree example). The key fix is in GenericRamValCheckVerifier::new which now computes init_eval using eval_initial_ram_mle + advice contributions instead of a direct polynomial evaluation that missed advice regions. Changes: - merkle-tree example: add --save flag and transcript feature flags - transpiler main.rs: add --trusted-advice CLI arg to load and symbolize advice commitments - transpilable_verifier.rs: fix init_eval to include advice selector * advice_eval terms via compute_advice_init_contributions - gnark_codegen.rs: split large constraints into sub-functions and cap inline expression size to prevent Go compiler OOM
…umulator After rebasing onto upstream/main, VerifierOpeningAccumulator gained deduplication logic (populate_or_alias_opening) that aliases openings when the same polynomial is opened at the same evaluation point by different sumcheck stages. AstOpeningAccumulator didn't handle this, pushing extra zero claims to pending_claims and corrupting the Fiat-Shamir transcript. Replicate the aliasing logic 1:1: Case A (key in proof) aliases if same poly already opened at same point, otherwise stores normally. Case B (key not in proof) aliases to matching opening or creates with zero claim. Point comparison uses AST NodeId equality.
- Remove unused deps ark-ec and serde from transpiler (machete) - Add zk feature to transpiler so cfg guards propagate correctly - Gate symbolize_proof body and helpers with #[cfg(not(feature = "zk"))] to handle JoltProof conditional fields (opening_claims vs blindfold_proof) - Add zk_generator fields to JoltVerifierPreprocessing in main.rs - Inline format string variables in transpiler/main.rs (clippy) - Refactor zklean-extractor main.rs to use library imports instead of mod re-declarations (fixes dead_code warnings and module resolution) - Export lookup_table_flags and sumchecks from zklean-extractor lib.rs - Add #[allow(clippy::op_ref)] on test that intentionally tests &refs - Add scripts/ci-local.sh for local CI verification
Make IO values (inputs, outputs, panic) symbolic witness variables instead of hardcoded constants in the generated Groth16 circuit. This is the first step toward universality classes (same circuit for same-shaped programs). jolt-core changes (non-breaking, additive only): - Add SparseEvalCoeff trait with u64 (Barrett) and F: JoltField (direct mul) impls - Rename sparse_eval_u64_block → sparse_eval_block<F, V: SparseEvalCoeff<F>> - Add thread-local overrides (PENDING_IO_MLE, PENDING_INITIAL_RAM) - Add early returns in eval_io_mle/eval_initial_ram_mle for symbolic path transpiler changes: - New io_replay.rs: FIFO queue for transcript byte overrides - poseidon.rs: raw_append_bytes consumes FIFO, raw_append_label_with_len bypasses it - New symbolize.rs: symbolize_io_device() creates symbolic IO variables - main.rs: integrate symbolic IO + PENDING_INITIAL_RAM before verify() E2E verified: 2,777,232 constraints, 164-byte Groth16 proof, 2ms verify.
…e_scalar_128_bits unsupported
… raw_append_scalar
- Remove unused OpeningAccumulator import in univariate_skip.rs - Fix long line formatting in verifier.rs, main.rs, ast_commitment_scheme.rs
cargo fmt for AbstractVerifierOpeningAccumulator long lines, remove duplicate Blake2bTranscript import, update fiat_shamir_preamble call in transpilable_verifier to match upstream 8-arg signature.
akoidefi
force-pushed
the
feat/verifier-transpilation-gnark
branch
from
74c625e to
5f274c4
Compare
@moodlezoup this is ready to merge now |
The imports for JoltCurve, SumcheckInstanceProof, UniSkipFirstRoundProofVariant, and CompressedUniPoly were gated with #[cfg(not(feature = "zk"))], but the two functions using them (symbolize_uni_skip_variant, symbolize_sumcheck_variant) were not. CI runs clippy with --features zk which removes the imports but leaves the functions, causing "cannot find type" errors.
…pilation-gnark # Conflicts: # Cargo.lock # jolt-core/src/zkvm/ram/read_write_checking.rs
4 participants
Jolt Verifier Transpilation Pipeline
Summary
Symbolic transpilation pipeline that converts Jolt's Rust verifier (stages 1-7) into a target-agnostic intermediate representation. First code generation target is gnark/Groth16.
Related: Builds on top of
zklean-extractor/from PR #684Motivation
Recursive proof verification requires running the Jolt verifier inside a circuit. Manually rewriting the verifier in Go would be:
Instead, we run the original Rust verifier with a symbolic type (
MleAst) that records operations instead of computing them. The recorded AST can then be mechanically translated to any circuit framework.Architecture
The pipeline builds on zklean's
MleAstsymbolic type (PR #684), which implementsJoltFieldbut records operations as an AST instead of computing them. We extended this foundation with:PartialEqimpl records assertions instead of comparingKey components we built:
TranspilableVerifierJoltVerifierhandles ZK variants, stage 8, and recursion. A separate module avoids polluting the main verifier with transpilation conditionals.OpeningAccumulatortraitaccumulator.append_*()to collect opening claims. Making this a trait lets us swap the real accumulator with a symbolic one. Required addingA: OpeningAccumulator<F>to ~25 stage verifiers.PoseidonAstTranscriptMleAstvalues throughfrom_bytes()calls.Per-constraint expression trees: zklean uses a single global AST, which works well for their Lean4 extraction use case. For Jolt transpilation with transcript-derived challenges, we found it easier to build N independent expression trees (one per equality assertion). Each tree has its own CSE context (
cse_0_*,cse_1_*, etc.), making debugging simpler: when a constraint fails, all its CSE variables are self-contained. Converting to a single tree is straightforward if needed.The IR is target-agnostic: adding a new backend (e.g., Circom, Plonky2) only requires implementing AST traversal and code emission for that target.
Poseidon Implementation
Both Rust and Go use circom-compatible BN254 Poseidon parameters (x^5 S-box, 8 full rounds, 56 partial rounds). Constants and test vectors are extracted from the same source to guarantee parity.
light-poseidonv0.4.0Poseidon::<Fr>::new_circom(width). Also used to extract round constants and MDS matrices for Go.succinctlabs/gnark-plonky2-verifier/poseidonlight-poseidonviaextract_poseidon_constantsbinary.Test vectors are generated from Rust (
cargo run -p transpiler --bin poseidon_vectors) and verified in Go tests, ensuring both implementations produce identical outputs.Scope
Included:
Excluded (intentionally):
Changes
New crate:
transpiler/src/main.rssrc/gnark_codegen.rssrc/symbolic_proof.rssrc/symbolize.rssrc/symbolic_traits/Modified:
zklean-extractor/src/mle_ast.rssrc/ast_bundle.rssrc/scalar_ops.rsModified:
jolt-core/src/transcripts/poseidon.rssrc/zkvm/transpilable_verifier.rssrc/poly/opening_proof.rsOpeningAccumulatora traitNew:
transpiler/go/poseidon/e2e_test.gostages_circuit_test.gostages_circuit.gostages_witness.jsonReview Guide
Critical paths:
symbolic_traits/poseidon.rs: Fiat-Shamir transcript must produce identical challenges in Rust and Gomle_ast.rsconstraint mode: ThePartialEqimpl records equality assertions instead of comparing valuesgnark_codegen.rs: CSE correctness and iterative AST traversal (avoids stack overflow on deep trees)Architectural decisions:
OpeningAccumulatortrait: Enables swapping concrete accumulator with symbolic one across ~25 stage verifiersmle_ast.rs: PassesMleAstvalues through type boundaries where generics aren't possible (e.g.,from_bytes())Testing
Known Limitations
No advice support in transpiler binary: The
TranspilableVerifiersupports advice, but the main.rs doesn't pass advice commitments (the fibonacci example doesn't use them).No ZK mode: The
TranspilableVerifierpanics on ZK proof variants. ZK mode was added recently and will be incorporated in a future commit.Circuit universality: The generated Groth16 circuit size depends on trace length and bytecode size. Each program configuration requires its own trusted setup. To avoid per-program setups, we plan to define universality classes: groups of programs with similar parameters that share the same circuit and setup, with acceptable padding overhead for smaller programs. IR generation will not get affected by future changes on this direction.
Future Work