feat: native Zig verifier foundation#88
Open
MatteoMer wants to merge 12 commits into
Open
Conversation
Add the core infrastructure for a native Zig verifier that eliminates the Rust FFI dependency for proof verification: - Complete proof deserialization (readJoltProof, readDoryProof, readOpeningClaims, readOpeningId, readG1/G2Compressed) - DoryVerifierSetup deserialization with roundtrip test - Lightweight VerifierPreprocessingData parser (extracts digest, memory layout, entry address without full BytecodePreprocessing JSON parsing) - Sumcheck verifier with compressed polynomial recovery, Horner evaluation, and transcript integration - UniSkip round verification - Top-level verify() entry point with Fiat-Shamir transcript reconstruction and all 7 stage sumcheck verification - CLI --native flag for native verification path - Dory opening verification stubbed (TODO for follow-up) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Machine-verified Montgomery field arithmetic (Coq-proven correct for ALL inputs) generated via fiat-crypto v0.1.5 word_by_word_montgomery backend. Native Zig output — no C/libc dependency. Generated for both BN254 Fr (scalar) and Fp (base) fields with 4x64-bit limbs. R constants verified to match existing params.zig values. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
FiatField wraps fiat-crypto generated Zig code with a MontgomeryField- compatible API (add, sub, mul, square, inverse, fromRaw, toBytesBE, etc.). BN254 Fr and Fp types cross-validated against MontgomeryField for all operations: one, add, sub, mul, square, inverse, neg, sumOfProducts, toBytesBE, fromBytesBE. All tests pass. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Validates fiat-crypto Fr and Fp against arkworks-generated test vectors (fr_ops.txt: 24 vectors, fp_ops.txt: 24 vectors) covering add, sub, mul, and inv operations with large field elements. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1000-iteration PRNG tests (fixed seed) validating: - Commutativity, associativity, distributivity - Additive/multiplicative identity and inverse - square(a) == mul(a,a) - Serialization round-trip - Cross-validation: every op matches MontgomeryField on random inputs Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Instantiates generic Fp2/Fp6/Fp12 factories from curves/extensions.zig with fiat-crypto backed FiatFp. Includes mulByXi (ξ = 9+u) for BN254. All differential test vectors pass: - Fp2: 48 vectors (add/sub/mul/square/inv/conjugate) - Fp6: 40 vectors (add/sub/mul/square/inv) - Fp12: 30+ vectors (add/sub/mul/square/inv/conjugate/cyclotomic_square) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Complete pairing implementation (Miller loop + final exponentiation) using fiat-crypto backed Fp/Fp2/Fp6/Fp12. Includes: - G1/G2 point types and scalar multiplication - G2 homogeneous projective with doubling/addition line evaluation - Sparse Fp12 multiplication (fp12MulBy034) - Frobenius endomorphisms with precomputed coefficients - Final exponentiation (easy part + hard part via arkworks algorithm) All generator_cases.txt pairing test vectors pass. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds fiat/mod.zig as module entry point exporting Fr, Fp, Fp2, Fp6, Fp12, G1Point, G2Point, pairingFp, millerLoop, and finalExponentiation. Accessible from downstream as zolt_arith.fiat.*. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…umcheck, opening accumulator, Stage 1 Add core verification infrastructure for the native Zig verifier: - Degree bound enforcement in sumcheck verifier (per-round compressed poly length must match expected degree; UniSkip degree bound check) - VerifierOpeningAccumulator: collects polynomial opening claims across stages for later batch Dory PCS verification - BatchedSumcheckVerifier: front-loaded batched sumcheck with staggered rounds, batching coefficients, and expected output claim verification - Stage 1 verifier: UniSkip sum-of-evals check, proper claim threading from UniSkip → remaining sumcheck, opening claim caching from proof All unit tests pass including new tests for degree bound rejection, accumulator operations, and batched sumcheck single-instance equivalence. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Fix critical transcript compatibility in batched_sumcheck.zig: use
per-claim appendScalar("sumcheck_claim") and per-coeff challengeScalarFull()
to match the prover's exact transcript pattern
- Implement Stage 2 verifier (stage2_verifier.zig):
- 5-instance batching: RamRW, ProductVirtual, InstrLookups, RamRaf, Output
- Proper input claim computation from Stage 1 opening claims
- gamma_rwc, gamma_instr challenge sampling matching upstream
- Staggered rounds with correct scaling factors
- Wire Stage 2 into verifier/mod.zig with UniSkip sum-of-evals check
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
… verify() Implement per-stage verifier structs for stages 3-7: - Stage 3: 3 instances (Shift, InstructionInput, RegistersClaim) with shift_gamma_powers, instr_gamma, reg_gamma challenges - Stage 4: 2 instances (RegistersRW, RamValCheck) with gamma_stage4 and ram_val_check_gamma domain separator - Stage 5: 3 instances (LookupsReadRaf, RamRaClaim, RegistersValEval) with gamma_ram_ra, gamma_lookups_raf staggered rounds - Stage 6: 6 instances (BytecodeRaf, Booleanity, HammingBool, RamRaVirt, LookupsRaVirt, IncClaim) with complex challenge setup - Stage 7: 1 instance (HammingWeightClaim) degree 2 Wire all stages into verifier/mod.zig, replacing the generic loop with per-stage verification. Remove dead getSumcheckInitialClaim placeholder. Each stage properly samples pre-batching gamma challenges matching the prover's transcript sequence, computes input claims from the opening accumulator, and runs batched sumcheck. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Implement Dory opening proof verifier with full transcript replay: - VMV message (c, d2, e1) appended to transcript - Reduce-and-fold rounds: first_message → beta challenge → second_message → alpha challenge - Final message → gamma challenge (keeps transcript in sync) - Make doryAppendGT/G1/G2 public in dory.zig for verifier access Wire Stage 8 into verifier/mod.zig: if proof has joint_opening_proof, run Dory transcript replay for Fiat-Shamir binding. Update TODO.md: mark stages 1-7 and Dory transcript replay as complete. Remaining for full soundness: - Dory algebraic state updates (GT exponentiation per round) - Final pairing check (e(E1, g2_0) vs C * ht^(gamma^2)) - Per-stage expectedOutputClaim checks - Per-stage cacheOpenings with actual polynomial IDs Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Native Zig verifier foundation with formally verified field arithmetic.
Verifier scaffold (commit 1)
verifyCLI command stubPhase 1: Fiat-crypto verified field arithmetic (commits 2-8)
word_by_word_montgomery, Coq-proven correct for ALL inputs). Native Zig output — no C/libc dependency.curves/extensions.zig.New files
fiat/bn254_{fr,fp}_fiat.zigfiat/fiat_field.zigfiat/bn254.zigfiat/extensions.zigfiat/pairing.zigfiat/{diff,ext_diff,property}_tests.zigfiat/mod.zigzolt_arith.fiat.*)Test plan
zig build testinpackages/zolt-arith/— all passparams.zig🤖 Generated with Claude Code