Move multiply product check into Spartan outer sumcheck#1301
Open
Move multiply product check into Spartan outer sumcheck#1301
Conversation
…d extended-integer arithmetic Remove the `Product` virtual polynomial and `RightLookupEqProductIfMul` R1CS constraint from the product-virtualization stage. Instead, prove the multiply instruction identity `is_mul * (rl - li*ri) = 0` directly in the Spartan outer sumcheck as an additive degree-3 (inside eq) term. Key changes: - Outer sumcheck now proves: eq(τ,x) * [Az·Bz + is_mul*(rl - li*ri)] = 0 - First product round uses fused materialization + eval: computes t(2) and t(∞) from trace using S64/S128/S160/S192 extended-integer arithmetic and FMAdd<F, S192>/FMAdd<F, S160> deferred-reduction accumulation, eliminating all field conversions (F::from_i128, F::from_u128) from the inner loop - Subsequent rounds use compact MultilinearPolynomial storage (bool/u64/u128/ i128) that binds to field elements on challenge ingestion - Rebalance R1CS groups: move RamAddrEqZeroIfNotLoadStore to second group - Merge old Stage 3 into Stage 2; reorder instances (RAM first, Spartan second) - Add gruen_poly_deg_4 for degree-4 round polynomials - Add FMAdd<F, u64> for Acc7S and FMAdd<i32, u64> for S192Sum Made-with: Cursor
…uct-virtual-poly branch Resolve merge conflicts preserving HEAD's 6-stage structure (product constraint hoisted into Spartan outer sumcheck) while porting main's BlindFold ZK protocol, accumulator type renames (WideAccumS, MedAccumS, SmallAccumU, etc.), and C generic parameter on proof types. Key conflict resolutions: - accumulation.rs: HEAD's new FMAdd impls with main's type names - instruction_lookups.rs: HEAD's 3-term claim reduction with main's reduce_mul_u128 - proof_serialization.rs: 6-stage proof fields + blindfold_proof (cfg-gated) - outer.rs: OuterRemainingSumcheckParams + prev_claim_product field - prover.rs: 6-stage prove + prove_batched_sumcheck + prove_blindfold - r1cs/evaluation.rs: HEAD's R1CS layout with main's accumulator types - verifier.rs: 6-stage verify + verify_blindfold with 6-stage arrays BlindFold constraint fixes for auto-merged ZK code: - outer.rs: add product term (is_mul*(rl-li*ri)) to output_claim_constraint - product.rs: update output_claim_constraint for 4 constraints (3+4 factors) - instruction_lookups.rs: remove LeftInstructionInput/RightInstructionInput - instruction_input.rs: SumcheckId::SpartanOuter for input_claim_constraint - bytecode/read_raf_checking.rs: Stage 2 = 11 terms, Stage 3 = 4 terms - increments.rs: fix s_cycle_stage field references Made-with: Cursor
Hoist mid-file and in-function `use` statements to top-level import blocks, replace fully qualified paths (3+ segments) with short names, and add proper cfg gates for conditionally-used imports. Made-with: Cursor
…al match Product was removed from R1CS inputs (hoisted to outer sumcheck) and VirtualPolynomial::Product variant was deleted. Update z3-verifier to match: drop &self.product from r1cs_inputs() array and remove the Product match arm from virtpoly_to_int(). Made-with: Cursor
…ator refactor) Made-with: Cursor
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
Productvirtual polynomial from the product-virtualization stage and theRightLookupEqProductIfMulR1CS constraint. Instead, prove the multiply-instruction identityis_mul * (rl - li*ri) = 0directly in the Spartan outer sumcheck as an additive degree-3 (inside eq) term.t(2)andt(∞)from trace usingS64/S128/S160/S192deferred-reduction accumulation (FMAdd<F, S192>,FMAdd<F, S160>viamul_trunc), eliminating all field conversions (F::from_i128,F::from_u128) from the inner loop. Subsequent rounds use compactMultilinearPolynomialstorage (bool/u64/u128/i128) that binds to field elements on challenge ingestion.RamAddrEqZeroIfNotLoadStorefrom the first group to the second group (itsBzisu64andAzis dense, making it a poor fit for the first group's boolean-optimized path).Test plan
cargo nextest run -p jolt-core muldivpassescargo clippy -p jolt-core --all-targets --features allocative,host -- -D warningscleancargo nextest run -p jolt-core)Made with Cursor