diff --git a/Cargo.toml b/Cargo.toml index e07a9b89a..522c28cf5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -94,5 +94,8 @@ flamegraph = ["pprof2/flamegraph", "pprof2/criterion"] experimental = [] evm = [] io = [] +# Use the original inverse-logup memory-check in ppSNARK instead of Logup-GKR. +# Default (feature off) uses the Logup-GKR memory-check. +logup-no-gkr = [] # Enables insecure setup methods that generate random tau. Only for testing! test-utils = [] diff --git a/benches/sumcheckeq.rs b/benches/sumcheckeq.rs index a526ce3af..6ddf04f79 100644 --- a/benches/sumcheckeq.rs +++ b/benches/sumcheckeq.rs @@ -4,7 +4,7 @@ use criterion::*; use nova_snark::{ provider::Bn256EngineKZG, - spartan::{ppsnark::MemorySumcheckInstance, SumcheckEngine}, + spartan::{mem_check_logup::MemorySumcheckInstance, SumcheckEngine}, traits::Engine, }; use rayon::iter::{IntoParallelIterator, ParallelIterator}; diff --git a/src/frontend/gadgets/num.rs b/src/frontend/gadgets/num.rs index f6e598c82..fb899fa91 100644 --- a/src/frontend/gadgets/num.rs +++ b/src/frontend/gadgets/num.rs @@ -228,7 +228,7 @@ impl AllocatedNum { cs.namespace(|| format!("run ending at {i}")), ¤t_run, )?); - current_run.truncate(0); + current_run.clear(); } // If `last_run` is true, `a` must be false, or it would diff --git a/src/frontend/test_shape_cs.rs b/src/frontend/test_shape_cs.rs index dfa2e419e..fef68c810 100644 --- a/src/frontend/test_shape_cs.rs +++ b/src/frontend/test_shape_cs.rs @@ -141,7 +141,7 @@ where let mut s = String::new(); for input in &self.inputs { - writeln!(s, "INPUT {}", &input).unwrap() + writeln!(s, "INPUT {}", input).unwrap() } let negone = -::ONE; @@ -174,10 +174,10 @@ where match var.0.get_unchecked() { Index::Input(i) => { - write!(s, "`I{}`", &self.inputs[i]).unwrap(); + write!(s, "`I{}`", self.inputs[i]).unwrap(); } Index::Aux(i) => { - write!(s, "`A{}`", &self.aux[i]).unwrap(); + write!(s, "`A{}`", self.aux[i]).unwrap(); } } } diff --git a/src/spartan/logup_gkr/fraction.rs b/src/spartan/logup_gkr/fraction.rs new file mode 100644 index 000000000..7bff7eb34 --- /dev/null +++ b/src/spartan/logup_gkr/fraction.rs @@ -0,0 +1,95 @@ +//! Projective fraction arithmetic for the Logup-GKR fractional-sum tree. +//! +//! A fraction `num/den` is kept in projective form so the GKR circuit never +//! performs a field inversion: the fraction-add gate combines two children +//! `(n_l, d_l)` and `(n_r, d_r)` into `(n_l·d_r + n_r·d_l, d_l·d_r)`. This is the +//! root of why Logup-GKR avoids the inverse-polynomial commitments that the +//! current ppSNARK memory-check pays for. + +use crate::traits::evm_serde::{CustomSerdeTrait, EvmCompatSerde}; +use core::iter::Sum; +use core::ops::Add; +use ff::Field; +use serde::{Deserialize, Serialize}; +use serde_with::serde_as; + +/// A projective fraction `numerator / denominator` over the engine scalar field. +/// +/// Equality of the represented rationals is cross-multiplicative +/// (`a/b == c/d` iff `a·d == c·b`); this type does not normalize. +#[serde_as] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] +#[serde(bound = "F: CustomSerdeTrait")] +pub struct Fraction { + /// Numerator. + #[serde_as(as = "EvmCompatSerde")] + pub num: F, + /// Denominator. + #[serde_as(as = "EvmCompatSerde")] + pub den: F, +} + +impl Fraction { + /// Creates a new projective fraction `num/den`. + pub fn new(num: F, den: F) -> Self { + Self { num, den } + } + + /// The additive identity `0/1` for projective fraction addition. + pub fn zero() -> Self { + Self { + num: F::ZERO, + den: F::ONE, + } + } +} + +/// Projective fraction addition (the 2-to-1 gate): `a/b + c/d = (a·d + c·b)/(b·d)`. +/// +/// `Fraction` is `Copy`, so `+` takes values with no cost. +impl Add for Fraction { + type Output = Self; + + fn add(self, rhs: Self) -> Self { + Self { + num: self.num * rhs.den + rhs.num * self.den, + den: self.den * rhs.den, + } + } +} + +/// Sum of a sequence of fractions, folding from the identity `0/1`. Lets a whole +/// tree level be reduced with `.sum()`. +impl Sum for Fraction { + fn sum>(iter: I) -> Self { + iter.fold(Self::zero(), |a, b| a + b) + } +} + +#[cfg(all(test, feature = "evm"))] +mod evm_serde_tests { + use super::Fraction; + use crate::traits::Engine; + + type E = crate::provider::Bn256EngineKZG; + type Fr = ::Scalar; + + #[test] + fn fraction_has_big_endian_scalar_golden_encoding() { + let fraction = Fraction::new(Fr::from(1), Fr::from(2)); + let config = bincode::config::legacy() + .with_big_endian() + .with_fixed_int_encoding(); + let bytes = bincode::serde::encode_to_vec(fraction, config).expect("serialize fraction"); + + let mut expected = [0u8; 64]; + expected[31] = 1; + expected[63] = 2; + assert_eq!(bytes, expected); + + let (decoded, consumed): (Fraction, usize) = + bincode::serde::decode_from_slice(&bytes, config).expect("deserialize fraction"); + assert_eq!(decoded, fraction); + assert_eq!(consumed, expected.len()); + } +} diff --git a/src/spartan/logup_gkr/layer.rs b/src/spartan/logup_gkr/layer.rs new file mode 100644 index 000000000..958052e9d --- /dev/null +++ b/src/spartan/logup_gkr/layer.rs @@ -0,0 +1,215 @@ +//! Layer type for the Logup-GKR fractional-sum tree. +//! +//! One [`Layer`] is a single level of a tree: two multilinear polynomials +//! (numerator, denominator). The same type serves the input layer, every +//! internal layer, and the output layer — they differ only in height (the +//! coefficient length halves each level, `N → N/2 → … → 1`). The same `Layer` +//! type serves all levels, with no separate input/output variants. +//! +//! ppSNARK constructs separate table and access input layers for each of its row +//! and column relations. Their leaves are `(num, den) = (ts, T+r)` on a table +//! side and `(-1, W+r)` on an access side. +//! +//! # Endianness (critical): MSB-first, pairs are `i` and `i+n` +//! Nova's MLEs are **MSB-first** (`bind_poly_var_top` folds the top variable by +//! `split_at(len/2)`). So a level's two children are the halves `x[i]` (top bit +//! 0) and `x[i+n]` (top bit 1), `n = len/2` — NOT `x[2i]` / `x[2i+1]`. Folding +//! this way keeps the tree consistent with Nova's sumcheck round order +//! (`eval_point` challenges bind MSB→LSB), so the GKR point matches the sumcheck +//! point. + +use crate::spartan::logup_gkr::fraction::Fraction; +use crate::spartan::polys::multilinear::MultilinearPolynomial; +use crate::spartan::polys::multilinear::MultilinearPolynomial as MLE; +use crate::traits::Engine; +use rayon::prelude::*; + +/// Parallelize `fold_up` only above this many output cells. A fold cell is a +/// few field multiplications, so rayon's scheduling overhead dominates on +/// smaller layers. This threshold is intentionally higher than the crate's +/// `PARALLEL_THRESHOLD`, which is tuned for more expensive per-element curve +/// operations such as MSMs. +const FOLD_PARALLEL_THRESHOLD: usize = 1 << 16; + +/// One level of a fractional-sum tree: parallel numerator and denominator +/// multilinear polynomials over `{0,1}^{log len}`. +/// +/// Storage is **two** MLEs. The "left/right" children the fraction gate consumes +/// are the two halves of these MLEs (`x[i]` and `x[i+n]`, `n = len/2`; MSB-first, +/// see module docs), read during the fold. So a layer holds 2 polynomials; a +/// per-layer *claim* exposes 4 values (`nL, nR, dL, dR`; see +/// `proof::LayerFinalClaim`). Do not confuse the two. +/// +/// Invariant: `num.len() == den.len()` and both lengths are a power of two. +/// +/// # Numerator/denominator convention (read before constructing) +/// `num` is the **signed weight** side (`ts` on a table side, `-1` on an access +/// side); `den` is the **fingerprint** side (`T+r` / `W+r`, never +/// inverted). To make an accidental swap impossible, this type has **no +/// positional constructor**: build it with field-init syntax so `num`/`den` are +/// named explicitly, e.g. `Layer { num: ts, den: t_plus_r }`. +pub struct Layer { + /// Numerator = signed weight (`ts` on a table side, `-1` on an access side). + pub num: MultilinearPolynomial, + /// Denominator = fingerprint (`T+r` / `W+r`), never inverted. + pub den: MultilinearPolynomial, +} + +impl Layer { + /// Number of hypercube variables of this layer (`log2(len)`). + pub fn num_vars(&self) -> usize { + self.num.get_num_vars() + } + + /// True when the layer has collapsed to a single cell (the output/root). + pub fn is_output(&self) -> bool { + self.num.len() == 1 + } + + /// Folds this layer one level up via the fraction-add gate, MSB-first: the two + /// children of output cell `i` are the halves `i` (top bit 0) and `i+n` (top + /// bit 1), `n = len/2`. Returns the parent layer of half the height. + /// + /// `(num[i]/den[i]) + (num[i+n]/den[i+n]) = + /// ((num[i]·den[i+n] + num[i+n]·den[i]) / (den[i]·den[i+n]))` + pub fn fold_up(&self) -> Self { + let len = self.num.len(); + debug_assert_eq!(len, self.den.len()); + debug_assert!(len >= 2 && len.is_power_of_two()); + let n = len / 2; + + // Each output cell i is the fraction-add of the two MSB-halves (child cells + // i and i+n) — independent across i, so parallelize above the threshold. + let fold = |i: usize| -> (E::Scalar, E::Scalar) { + let child = Fraction::new(self.num.Z[i], self.den.Z[i]) + + Fraction::new(self.num.Z[i + n], self.den.Z[i + n]); + (child.num, child.den) + }; + + let (next_num, next_den): (Vec<_>, Vec<_>) = if n < FOLD_PARALLEL_THRESHOLD { + (0..n).map(fold).unzip() + } else { + (0..n).into_par_iter().map(fold).unzip() + }; + + Self { + num: MLE::new(next_num), + den: MLE::new(next_den), + } + } + + /// Builds the full tree from this input layer, leaf→root. Result has + /// `log2(len) + 1` entries; `[0]` is the input layer, the last is the single + /// output cell. + pub fn build_tree(self) -> Vec { + let depth = self.num.get_num_vars() + 1; + let mut layers = Vec::with_capacity(depth); + let mut cur = self; + loop { + if cur.is_output() { + layers.push(cur); + break; + } + let next = cur.fold_up(); + layers.push(cur); + cur = next; + } + layers + } + + /// The output cell's fraction `(num, den)` as a two-element claim vector, + /// used to seed the verifier's fold-down (`initial_claims`). + pub fn output_fraction(&self) -> (E::Scalar, E::Scalar) { + debug_assert!(self.is_output()); + (self.num.Z[0], self.den.Z[0]) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::provider::Bn256EngineKZG; + use ff::Field; + + type E = Bn256EngineKZG; + type Fr = ::Scalar; + + // Reference: the rational sum Σ num[i]/den[i] as a single reduced fraction, + // computed with real field inversion (only for the test oracle). + fn ref_sum(num: &[Fr], den: &[Fr]) -> (Fr, Fr) { + // accumulate as projective fraction a/b + c/d = (ad+cb, bd) + let mut acc = (Fr::ZERO, Fr::ONE); + for i in 0..num.len() { + acc = (acc.0 * den[i] + num[i] * acc.1, acc.1 * den[i]); + } + acc + } + + // Cross-multiplication equality for projective fractions. + fn frac_eq((n0, d0): (Fr, Fr), (n1, d1): (Fr, Fr)) -> bool { + n0 * d1 == n1 * d0 + } + + fn layer_from(num: Vec, den: Vec) -> Layer { + Layer { + num: MultilinearPolynomial::new(num.into_iter().map(Fr::from).collect()), + den: MultilinearPolynomial::new(den.into_iter().map(Fr::from).collect()), + } + } + + #[test] + fn fold_up_matches_reference_n4() { + let num = vec![1u64, 2, 3, 4]; + let den = vec![5u64, 6, 7, 8]; + let l = layer_from(num.clone(), den.clone()); + let tree = l.build_tree(); + assert_eq!(tree.len(), 3); // 2 vars → depth 3 + let root = tree.last().unwrap().output_fraction(); + let expected = ref_sum( + &num.iter().map(|&x| Fr::from(x)).collect::>(), + &den.iter().map(|&x| Fr::from(x)).collect::>(), + ); + assert!( + frac_eq(root, expected), + "tree root fraction must equal the reference rational sum" + ); + } + + #[test] + fn fold_up_matches_reference_n8() { + let num: Vec = vec![3, 1, 4, 1, 5, 9, 2, 6]; + let den: Vec = vec![2, 7, 1, 8, 2, 8, 1, 8]; + let l = layer_from(num.clone(), den.clone()); + let tree = l.build_tree(); + assert_eq!(tree.len(), 4); + let root = tree.last().unwrap().output_fraction(); + let expected = ref_sum( + &num.iter().map(|&x| Fr::from(x)).collect::>(), + &den.iter().map(|&x| Fr::from(x)).collect::>(), + ); + assert!(frac_eq(root, expected)); + } + + #[test] + fn logup_balance_gives_zero_numerator() { + // A balanced multiset: table {a,b} with multiplicities {1,1}, lookups {a,b}. + // Σ 1/(α-a) + 1/(α-b) - 1/(α-a) - 1/(α-b) = 0. Encode as one instance's + // input layer with num = [+1,+1,-1,-1], den = [α-a, α-b, α-a, α-b]. + let alpha = Fr::from(100); + let a = Fr::from(7); + let b = Fr::from(9); + let num = vec![Fr::ONE, Fr::ONE, -Fr::ONE, -Fr::ONE]; + let den = vec![alpha - a, alpha - b, alpha - a, alpha - b]; + let l = Layer:: { + num: MultilinearPolynomial::new(num), + den: MultilinearPolynomial::new(den), + }; + let root = l.build_tree().last().unwrap().output_fraction(); + assert_eq!( + root.0, + Fr::ZERO, + "balanced logup must have zero root numerator" + ); + assert_ne!(root.1, Fr::ZERO, "root denominator must be non-zero"); + } +} diff --git a/src/spartan/logup_gkr/mod.rs b/src/spartan/logup_gkr/mod.rs new file mode 100644 index 000000000..22af1107f --- /dev/null +++ b/src/spartan/logup_gkr/mod.rs @@ -0,0 +1,37 @@ +//! Logup-GKR fractional-sum memory-check argument. +//! +//! Replaces the inverse-logup memory-check in `ppsnark.rs` (the +//! `MemorySumcheckInstance` 6-route sumcheck + 4 inverse-polynomial +//! commitments) with four equal-height fractional-sum GKR trees: the table and +//! access sides of the row and column relations. Projective fractions keep the +//! circuit inversion-free and eliminate the four inverse-polynomial +//! commitments. +//! +//! ## Module map +//! - [`fraction`]: projective fraction + 2-to-1 gate (pure). +//! - [`layer`]: the `Layer` type (one tree level: num/den MLEs). +//! - [`proof`]: proof/claim interface. +//! - [`prover`]: fold-up + batched sumcheck prover. +//! - [`verifier`]: fold-down + root check, emits the shared opening claim. +//! +//! ## Boundary with ppSNARK (host reconcile contract) +//! The argument owns no commitment scheme. Its verifier returns a +//! [`proof::LogupGkrOpeningClaim`]: a single shared `eval_point` plus the +//! four input-layer fractions `openings`, ordered `[row_table, row_access, +//! col_table, col_access]`. The **host** then: +//! 1. rerandomizes the seven claimed columns `[L_row, L_col, addr_row, addr_col, +//! ts_row, ts_col, mem_col]` from `eval_point` into the inner sumcheck and +//! binds them at `r_inner_batched` through the batched PCS opening; +//! 2. recomputes the four fractions from those claims (`num = ts` on the table +//! sides, `num = -1` on the access sides) and checks them against `openings`; +//! 3. runs the `0/den` zero-sum balance check. +//! +//! Steps 2-3 are the host's job, never the GKR verifier's. + +pub mod fraction; +pub mod layer; +pub mod proof; +pub mod prover; +pub mod verifier; + +pub use proof::{LogupGkrOpeningClaim, LogupGkrProof}; diff --git a/src/spartan/logup_gkr/proof.rs b/src/spartan/logup_gkr/proof.rs new file mode 100644 index 000000000..2ced531ed --- /dev/null +++ b/src/spartan/logup_gkr/proof.rs @@ -0,0 +1,154 @@ +//! Proof objects for the Logup-GKR fractional-sum argument. +//! +//! # One batched proof over equal-height trees +//! Each input [`Layer`](super::layer::Layer) defines a separate fractional-sum +//! tree. All inputs must already have the same number of variables; the prover +//! does not pad them. At each depth, the corresponding tree layers are batched +//! into one sumcheck via a fresh `λ`, producing one shared evaluation point for +//! all trees. Their claims are carried in a single proof rather than separate +//! per-tree proofs. Sumcheck round polynomials use Nova's `CompressedUniPoly`. + +use crate::spartan::logup_gkr::fraction::Fraction; +use crate::spartan::polys::univariate::CompressedUniPoly; +use crate::traits::Engine; +use serde::{Deserialize, Serialize}; + +/// `rlc(a, b, r) = a + r·(b - a)` — the two-to-one fold of split claims. +#[inline(always)] +fn rlc(a: F, b: F, r: F) -> F { + a + r * (b - a) +} + +/// A claim about one instance's column pair after a layer: the fraction +/// `num/den`. +pub type LayerClaim = Fraction<::Scalar>; + +/// The split (even/odd) final claim of one instance at one layer: the `left` +/// and `right` child fractions `(nL,dL)` and `(nR,dR)`. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct LayerFinalClaim { + /// Left child `(nL, dL)`. + pub left: Fraction, + /// Right child `(nR, dR)`. + pub right: Fraction, +} + +impl LayerFinalClaim { + /// Builds from the four folded sumcheck evaluations `nL, nR, dL, dR`. + /// + /// WARNING: the layer sumcheck's `bound_evals` come out **interleaved** as + /// `[nL, dR, nR, dL]` (matching the flattened virtual-polynomial order + /// `numerator_left, denominator_right, numerator_right, denominator_left`). + /// Map them explicitly — `new(evals[0], evals[2], evals[3], evals[1])` — + /// never slice `evals[0..4]` into the parameters positionally. + pub fn new(nL: E::Scalar, nR: E::Scalar, dL: E::Scalar, dR: E::Scalar) -> Self { + Self { + left: Fraction::new(nL, dL), + right: Fraction::new(nR, dR), + } + } + + /// Folds the split claim into the next layer's claim via `rlc` at `r`. + pub fn fold_into_next_claim(&self, r: E::Scalar) -> LayerClaim { + Fraction::new( + rlc(self.left.num, self.right.num, r), + rlc(self.left.den, self.right.den, r), + ) + } + + /// The gate output `left + right` (projective fraction add). + pub fn compute_gate(&self) -> Fraction { + self.left + self.right + } +} + +/// Sumcheck transcript for one batched tree layer: one compressed round +/// polynomial per variable (the instances are batched into this single +/// sumcheck via `λ`). +#[derive(Clone, Debug, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct LayerSumcheck { + /// Compressed round polynomials, one per sumcheck round of this layer. + pub round_polys: Vec>, +} + +/// A single **batched** Logup-GKR proof over all input instances. +/// +/// Instance-indexed vectors preserve the caller's input order; ppSNARK uses +/// `[row_table, row_access, col_table, col_access]`. `initial_claims` are the +/// per-instance output-layer fractions (observed first). `final_claims[layer]` +/// holds one split claim per instance; `sumchecks[layer]` is the one batched +/// sumcheck for that layer. Layers are ordered output→input, and the top +/// transition (0-variable layer) carries no sumcheck, so +/// `sumchecks.len() + 1 == final_claims.len()`. +/// +/// The per-layer batching challenge `λ` is **not** stored here: it is a +/// Fiat-Shamir challenge the verifier re-samples fresh at each layer (reusing +/// one `λ` across layers would let the prover adaptively forge each layer's +/// claims). Likewise `initial_claims` are not bound to committed data by this +/// proof alone; soundness closes at the host's reconcile step, where the +/// returned `openings` must match the fractions reconstructed from the host's +/// claimed column evaluations at `eval_point`. +#[derive(Clone, Debug, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct LogupGkrProof { + /// Per-instance output-layer claims (the root fractions before fold-down). + pub initial_claims: Vec>, + /// Per-layer, per-instance split final claims, output→input. + pub final_claims: Vec>>, + /// Per-layer batched sumcheck (one fewer than `final_claims`). + pub sumchecks: Vec>, +} + +/// The GKR **prefix** proof: every layer reduction except the last. Carried by +/// the ppSNARK fused memory-check, where the last layer is proven jointly with +/// the Inner sumcheck instead of being folded down here. +/// +/// For height `N = 2^n`, `prefix_final_claims` holds the `n-1` prefix layers +/// (output→input) and `prefix_sumchecks` the `n-2` sumchecks (the root reduction +/// carries none). For `n = 1` both are empty (the single layer is the last one). +#[derive(Clone, Debug, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct LogupGkrPrefixProof { + /// Per-instance output-layer (root) claims, absorbed first. + pub initial_claims: Vec>, + /// The `n-1` prefix layers' split final claims, output→input. + pub prefix_final_claims: Vec>>, + /// The `n-2` prefix layer sumchecks. + pub prefix_sumchecks: Vec>, +} + +/// Verifier output — a **continuation token** carrying the shared opening +/// claim, with its point field named Nova's `eval_point`. +/// +/// The host uses [`Self::eval_point`] to seed the opening-point reduction and +/// uses `openings` to reconcile every reduced input-layer fraction against its +/// claimed columns. The ppSNARK host also performs the `0/den` zero-sum check; +/// neither operation belongs to the GKR verifier. +#[derive(Clone, Debug)] +pub struct LogupGkrOpeningClaim { + eval_point: Vec, + openings: Vec>, +} + +impl LogupGkrOpeningClaim { + /// Constructs the token (only the GKR verifier should call this). + pub fn new(eval_point: Vec, openings: Vec>) -> Self { + Self { + eval_point, + openings, + } + } + + /// The shared evaluation point to which all input-layer claims are reduced. + pub fn eval_point(&self) -> &[E::Scalar] { + &self.eval_point + } + + /// The reduced input-layer fractions in caller input order, which the host + /// reconstructs from its claimed column evaluations and compares against. + pub fn openings(&self) -> &[Fraction] { + &self.openings + } +} diff --git a/src/spartan/logup_gkr/prover.rs b/src/spartan/logup_gkr/prover.rs new file mode 100644 index 000000000..1904e4141 --- /dev/null +++ b/src/spartan/logup_gkr/prover.rs @@ -0,0 +1,819 @@ +//! Prover for the Logup-GKR fractional-sum argument. +//! +//! Implements the prover side of the Logup-GKR protocol defined in +//! `verifier.rs`, sharing its transcript labels and fraction-absorption order. +//! +//! It builds one equal-height tree per input, folds them leaf→root, and for each +//! internal depth runs one transparent cubic sumcheck +//! (`prove_layer_sumcheck`) reducing the merged fraction-sum claim to the next +//! layer. +//! +//! ## Per-layer gate (the verifier's contract) +//! A layer proves, for all instances batched by a per-layer `λ`, +//! `Σ_i (v_p_i + λ v_q_i) = Σ_x eq(τ,x) · Σ_i [nL·dR + nR·dL + λ·dL·dR]_i`. +//! The `eq(τ, ·)` factor is carried as an explicit MLE so the sumcheck's final +//! value reconciles as the verifier demands: `eq(τ,r)·G(r)`. Round polynomials +//! are degree 3 (`eq` deg 1 × gate deg 2 = `spec::LAYER_SC_DEGREE`). +//! +//! ## Endianness +//! The tree folds MSB-first (`Layer::fold_up`, halves `i`/`i+n`), and the +//! sumcheck binds the top variable first, so the sumcheck point is directly the +//! fraction evaluation point of the next layer. + +use crate::errors::NovaError; +use crate::spartan::logup_gkr::layer::Layer; +use crate::spartan::logup_gkr::proof::{ + LayerClaim, LayerFinalClaim, LayerSumcheck, LogupGkrOpeningClaim, LogupGkrProof, +}; +use crate::spartan::polys::multilinear::MultilinearPolynomial; +use crate::traits::{Engine, TranscriptEngineTrait}; +use ff::Field; +use rayon::prelude::*; + +// The prover satisfies the protocol defined by the verifier: it uses the +// verifier's transcript labels (`spec`) and fraction-absorb order, and produces +// a sumcheck whose final value reconciles as `eq(τ,r)·G(r)` (the verifier's +// contract). +use crate::spartan::logup_gkr::verifier::{absorb_fraction, spec}; + +/// Transparent cubic sumcheck for one GKR layer, proving +/// `claim = Σ_x eq(τ, x) · Σ_i [ nLᵢ·dRᵢ + nRᵢ·dLᵢ + λ·dLᵢ·dRᵢ ](x)` +/// over `num_rounds = |τ|` variables. +/// +/// The `eq(τ, ·)` factor is handled by the shared `EqSumCheckInstance` +/// (Gruen eq-factoring, eprint 2024/108: half-size eq tables + O(1) per-round +/// bind), and BDDT claim derivation (eprint 2025/1117 §6.2). The four-instance +/// path reuses the preceding layer's left claims for round-0 `t(0)`, so that +/// round scans only for `t(∞)`; later rounds normally scan for both values. +/// +/// The four half-MLEs are passed struct-of-arrays (`nl`/`nr`/`dl`/`dr`, one +/// entry per instance) so the eq instance can index them directly. Returns the +/// compressed round polynomials, the sumcheck point `r`, and each instance's +/// `(nL, nR, dL, dR)` evaluated at `r`. +/// +/// ppSNARK's four-sub-instance path caches each top-variable delta during +/// evaluation and reuses it during binding; other instance counts retain the +/// general non-mutating evaluation path. `previous_finals` must be the preceding +/// parent reduction's claims in the same instance order as the four MLE slices. +#[allow(clippy::type_complexity)] +fn prove_layer_sumcheck( + claim: E::Scalar, + taus: &[E::Scalar], + nl: &mut [MultilinearPolynomial], + nr: &mut [MultilinearPolynomial], + dl: &mut [MultilinearPolynomial], + dr: &mut [MultilinearPolynomial], + lambda: E::Scalar, + previous_finals: &[LayerFinalClaim], + transcript: &mut E::TE, +) -> Result< + ( + Vec>, + Vec, + Vec<[E::Scalar; 4]>, + ), + NovaError, +> { + use crate::spartan::polys::univariate::{CompressedUniPoly, UniPoly}; + use crate::spartan::sumcheck::eq_sumcheck::EqSumCheckInstance; + + let num_rounds = taus.len(); + let m = nl.len(); + + let mut r: Vec = Vec::with_capacity(num_rounds); + let mut polys: Vec> = Vec::with_capacity(num_rounds); + let mut claim_per_round = claim; + + let mut eq = EqSumCheckInstance::::new(taus.to_vec()); + let cache_deltas = m == 4; + + // Per-instance λ-powers: instance i's numerator gets λ^{2i}, denominator + // λ^{2i+1}. λ^{2i} accumulates by a running product (O(m) muls) instead of + // per-instance pow_vartime. + let mut w_num = E::Scalar::ONE; + let weights: Vec<(E::Scalar, E::Scalar)> = (0..m) + .map(|_| { + let w_den = w_num * lambda; + let pair = (w_num, w_den); + w_num = w_den * lambda; + pair + }) + .collect(); + + // The preceding layer's left claims are this layer's round-0 t(0) + // evaluations at `taus[1..]`. + let round0_t_0 = cache_deltas.then(|| { + assert_eq!(previous_finals.len(), m); + previous_finals + .iter() + .zip(&weights) + .map(|(fc, (w_num, w_den))| *w_num * fc.left.num + *w_den * fc.left.den) + .sum() + }); + + for round in 0..num_rounds { + // Round polynomial s(X) = eq(τ,X) · G(X), degree 3. BDDT derivation returns + // (s(0), cubic coeff, s(-1)); the verifier reconstructs s(1) = claim - s(0). + let (s_0, s_cubic, s_m1) = if cache_deltas { + match (round, round0_t_0) { + (0, Some(t_0)) => eq.evaluation_points_logup_gate_and_cache_deltas_with_t_0( + nl, + nr, + dl, + dr, + &weights, + t_0, + claim_per_round, + ), + _ => eq.evaluation_points_logup_gate_and_cache_deltas( + nl, + nr, + dl, + dr, + &weights, + claim_per_round, + ), + } + } else { + eq.evaluation_points_logup_gate(nl, nr, dl, dr, &weights, claim_per_round) + }; + + let poly = UniPoly::from_evals_deg3(&[s_0, claim_per_round - s_0, s_cubic, s_m1]); + + transcript.absorb(spec::ROUND_POLY, &poly); + let r_i = transcript.squeeze(spec::ROUND_CHALLENGE)?; + r.push(r_i); + polys.push(poly.compress()); + claim_per_round = poly.evaluate(&r_i); + + // Bind the top variable of every half-MLE (eq binds in O(1) via the instance). + nl.par_iter_mut() + .chain(nr.par_iter_mut()) + .chain(dl.par_iter_mut()) + .chain(dr.par_iter_mut()) + .for_each(|p| { + if cache_deltas { + p.bind_poly_var_top_with_cached_delta(&r_i); + } else { + p.bind_poly_var_top(&r_i); + } + }); + eq.bound(&r_i); + } + + let _ = claim_per_round; + let finals: Vec<[E::Scalar; 4]> = (0..m) + .map(|i| [nl[i].Z[0], nr[i].Z[0], dl[i].Z[0], dr[i].Z[0]]) + .collect(); + Ok((polys, r, finals)) +} + +/// Reduces one GKR layer: samples `λ`, either reads the two-cell split (root +/// reduction, `num_vars - j == 0`) or runs `prove_layer_sumcheck`, then absorbs +/// the split final claims, samples the fold challenge, and folds the running +/// claims and evaluation point into the child layer. +/// +/// `children` are the popped child layers (`layers[j-1]`) whose halves the gate +/// consumes. This is the single per-layer body shared by the standalone prefix +/// loop and the standalone last-layer finish, so both drive an identical +/// transcript; the fused ppSNARK driver deliberately does NOT call it for the +/// last layer (it batches that layer with the Inner sumcheck instead). +#[allow(clippy::too_many_arguments)] +fn prove_one_reduction( + j: usize, + num_vars: usize, + m: usize, + mut children: Vec>, + running: &mut Vec<(E::Scalar, E::Scalar)>, + eval_point: &mut Vec, + sumchecks: &mut Vec>, + final_claims_by_layer: &mut Vec>>, + transcript: &mut E::TE, +) -> Result<(), NovaError> { + // Fresh λ per layer, after the previous claims were absorbed. + let lambda = transcript.squeeze(spec::LAMBDA)?; + let n = 1usize << (num_vars - j); + + let mut layer_finals: Vec> = Vec::with_capacity(m); + if num_vars - j == 0 { + // Base case (root reduction): the child layer has exactly two cells; read + // the split directly, no sumcheck. + for c in &children { + layer_finals.push(LayerFinalClaim::::new( + c.num.Z[0], // nL + c.num.Z[1], // nR + c.den.Z[0], // dL + c.den.Z[1], // dR + )); + } + let _ = (lambda, n); // λ unused at the base (single term, no batching) + } else { + // Sumcheck over (num_vars - j) variables. The 2m sub-claims are batched by + // distinct powers of λ (Horner over [p_0,q_0,p_1,q_1,...]) — see verifier. + let previous_finals = final_claims_by_layer + .last() + .expect("every sumcheck layer follows a completed parent reduction"); + let claim: E::Scalar = { + let mut acc = E::Scalar::ZERO; + let mut pw = E::Scalar::ONE; + for (p, q) in running.iter() { + acc += pw * *p; + pw *= lambda; + acc += pw * *q; + pw *= lambda; + } + acc + }; + + // Half-MLEs struct-of-arrays: nL/nR = numerator halves, dL/dR = den halves. + // Move the child buffers into the halves (split each Z at n) instead of + // cloning: `children` is dropped at the end of this call anyway. + let mut nl: Vec> = Vec::with_capacity(m); + let mut nr: Vec> = Vec::with_capacity(m); + let mut dl: Vec> = Vec::with_capacity(m); + let mut dr: Vec> = Vec::with_capacity(m); + for c in children.drain(..) { + let mut num_z = c.num.Z; + let mut den_z = c.den.Z; + let num_hi = num_z.split_off(n); + let den_hi = den_z.split_off(n); + nl.push(MultilinearPolynomial::new(num_z)); + nr.push(MultilinearPolynomial::new(num_hi)); + dl.push(MultilinearPolynomial::new(den_z)); + dr.push(MultilinearPolynomial::new(den_hi)); + } + + let (round_polys, r, finals) = prove_layer_sumcheck::( + claim, + eval_point, + &mut nl, + &mut nr, + &mut dl, + &mut dr, + lambda, + previous_finals, + transcript, + )?; + + for f in &finals { + layer_finals.push(LayerFinalClaim::::new(f[0], f[1], f[2], f[3])); + } + sumchecks.push(LayerSumcheck { round_polys }); + *eval_point = r; // sumcheck point (length num_vars - j) + } + + // Absorb final claims, sample fold challenge, update running claims + point. + for fc in &layer_finals { + absorb_fraction::(transcript, fc.left); + absorb_fraction::(transcript, fc.right); + } + let fold_r = transcript.squeeze(spec::FOLD)?; + + *running = layer_finals + .iter() + .map(|fc| { + let c = fc.fold_into_next_claim(fold_r); + (c.num, c.den) + }) + .collect(); + // New point for layers[j-1] is [fold_r, ...sumcheck_point] (fold_r as MSB). + let mut next_point = Vec::with_capacity(eval_point.len() + 1); + next_point.push(fold_r); + next_point.extend_from_slice(eval_point); + *eval_point = next_point; + + final_claims_by_layer.push(layer_finals); + Ok(()) +} + +/// The prover state captured after the GKR prefix (every layer reduction except +/// the last), holding everything needed to finish the argument — either the +/// standalone last layer, or the fused ppSNARK driver that batches the last +/// layer with the Inner sumcheck. No hidden transcript side effects: all data to +/// resume is explicit here. +pub(crate) struct GkrProverPrefix { + /// Number of instances. + pub(crate) m: usize, + /// `log2` height of every input layer. + pub(crate) num_vars: usize, + /// Per-instance output-layer (root) fractions, already absorbed. + pub(crate) initial_claims: Vec>, + /// Prefix layer sumchecks produced so far, output→input. + pub(crate) sumchecks: Vec>, + /// Prefix per-layer split final claims produced so far, output→input. + pub(crate) final_claims_by_layer: Vec>>, + /// Running per-instance `(num, den)` claim about the last layer's parent + /// (`layers[1]`), or the root claim when `num_vars == 1`. + pub(crate) running: Vec<(E::Scalar, E::Scalar)>, + /// Evaluation point `τ` for the last-layer sumcheck (length `num_vars - 1`; + /// empty when `num_vars == 1`). + pub(crate) eval_point: Vec, + /// The remaining input layer per instance, consumed by the last reduction. + pub(crate) input_layers: Vec>, +} + +/// Runs the GKR prefix: builds the trees, absorbs the root claims, and reduces +/// every layer **except the last**, returning the state needed to finish. For +/// `num_vars == 1` the prefix is empty (the single layer is the last one). +/// +/// See [`prove`] for the full-argument contract; splitting the prefix out lets +/// the ppSNARK fused driver take over the last layer. +pub(crate) fn prove_prefix( + inputs: Vec>, + transcript: &mut E::TE, +) -> Result, NovaError> { + let m = inputs.len(); + if m == 0 { + return Err(NovaError::InvalidNumInstances); + } + let num_vars = inputs[0].num_vars(); + if num_vars == 0 { + // A single-cell input has nothing to fold; the argument needs height ≥ 2. + return Err(NovaError::InvalidSumcheckProof); + } + for inp in &inputs { + if inp.num_vars() != num_vars { + return Err(NovaError::InvalidSumcheckProof); + } + } + + // Build every instance's tree, leaf→root. trees[instance][layer], where + // trees[i][j] has (num_vars - j) variables; [0] = input, [num_vars] = root. + // Layers are consumed root→leaf via `pop()` (see the loop), so the just-proven + // layer is dropped the instant it is consumed. + let mut trees: Vec>> = inputs.into_iter().map(|l| l.build_tree()).collect(); + + // initial_claims = each instance's output (root) fraction, absorbed first. The + // root layer (index num_vars, a single cell) is popped and dropped here; only + // its two scalars survive in `initial_claims`. + let initial_claims: Vec> = trees + .iter_mut() + .map(|t| { + let root = t.pop().expect("tree has a root layer"); + let (n, d) = root.output_fraction(); + LayerClaim::::new(n, d) + }) + .collect(); + for c in &initial_claims { + absorb_fraction::(transcript, *c); + } + + // Running per-instance claims about `layers[j]`, starting at the root. + let mut running: Vec<(E::Scalar, E::Scalar)> = + initial_claims.iter().map(|c| (c.num, c.den)).collect(); + let mut eval_point: Vec = Vec::new(); + + let mut sumchecks: Vec> = Vec::with_capacity(num_vars.saturating_sub(1)); + let mut final_claims_by_layer: Vec>> = Vec::with_capacity(num_vars); + + // Reduce every layer except the last (j = num_vars … 2). For num_vars == 1 + // this range is empty and the single layer is finished by the caller. + for j in (2..=num_vars).rev() { + let children: Vec> = trees.iter_mut().map(|t| t.pop().unwrap()).collect(); + prove_one_reduction::( + j, + num_vars, + m, + children, + &mut running, + &mut eval_point, + &mut sumchecks, + &mut final_claims_by_layer, + transcript, + )?; + } + + // The last remaining layer of each tree is the input layer, consumed by the + // last reduction (standalone finish or fused driver). + let input_layers: Vec> = trees + .iter_mut() + .map(|t| t.pop().expect("input layer remains")) + .collect(); + + Ok(GkrProverPrefix { + m, + num_vars, + initial_claims, + sumchecks, + final_claims_by_layer, + running, + eval_point, + input_layers, + }) +} + +/// Finishes the standalone argument from the prefix state by reducing the last +/// layer with the same `prove_one_reduction` body the prefix uses, then +/// assembles the batched proof and shared opening claim. +pub(crate) fn finish_last_layer_standalone( + prefix: GkrProverPrefix, + transcript: &mut E::TE, +) -> Result<(LogupGkrProof, LogupGkrOpeningClaim), NovaError> { + let GkrProverPrefix { + m, + num_vars, + initial_claims, + mut sumchecks, + mut final_claims_by_layer, + mut running, + mut eval_point, + input_layers, + } = prefix; + + // The last reduction (j = 1) consumes the input layers. + prove_one_reduction::( + 1, + num_vars, + m, + input_layers, + &mut running, + &mut eval_point, + &mut sumchecks, + &mut final_claims_by_layer, + transcript, + )?; + + // openings = each instance's input-layer fraction at the final eval_point + // (length num_vars); equals the last running claim by construction. + let openings: Vec> = running + .iter() + .map(|(n, d)| LayerClaim::::new(*n, *d)) + .collect(); + + let proof = LogupGkrProof { + initial_claims, + final_claims: final_claims_by_layer, + sumchecks, + }; + let claim = LogupGkrOpeningClaim::new(eval_point, openings); + Ok((proof, claim)) +} + +/// Proves the fractional-sum identity `Σ p/q = root` for all equal-height input +/// trees in one batched proof, returning the proof and the shared opening claim. +/// +/// `inputs` holds one input [`Layer`] per instance. Every layer must have the +/// same positive `num_vars`, so every coefficient vector has the same +/// power-of-two length of at least two. The soundness invariant is to absorb +/// every root and layer claim before sampling the challenge that depends on it; +/// `initial_claims` and each layer's `final_claims` enforce this order. +/// +/// This is the prefix + last-layer composition; the two stages share the +/// per-layer body `prove_one_reduction`, so the transcript is identical to the +/// former monolithic loop. +pub fn prove( + inputs: Vec>, + transcript: &mut E::TE, +) -> Result<(LogupGkrProof, LogupGkrOpeningClaim), NovaError> { + let prefix = prove_prefix::(inputs, transcript)?; + finish_last_layer_standalone::(prefix, transcript) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::spartan::logup_gkr::verifier; + use crate::spartan::polys::multilinear::MultilinearPolynomial; + use crate::traits::TranscriptEngineTrait; + + type E = crate::provider::Bn256EngineKZG; + type Fr = ::Scalar; + + fn mle(v: Vec) -> MultilinearPolynomial { + MultilinearPolynomial::new(v.into_iter().map(Fr::from).collect()) + } + + // Full prove→verify round trip: the verifier must accept, and its returned + // openings must equal the prover's actual input-layer fractions at the shared + // evaluation point. + fn round_trip(inputs: Vec<(Vec, Vec)>) { + let layers: Vec> = inputs + .iter() + .map(|(n, d)| Layer:: { + num: mle(n.clone()), + den: mle(d.clone()), + }) + .collect(); + // Keep copies to independently evaluate at the eval_point. + let raw: Vec<(MultilinearPolynomial, MultilinearPolynomial)> = inputs + .iter() + .map(|(n, d)| (mle(n.clone()), mle(d.clone()))) + .collect(); + + let mut tr_p = ::TE::new(b"gkr-test"); + let (proof, claim) = prove::(layers, &mut tr_p).expect("prove"); + + let mut tr_v = ::TE::new(b"gkr-test"); + let vclaim = verifier::verify::(&proof, &mut tr_v).expect("verify"); + + // The verifier point must match the prover point; opening components must + // match direct input-MLE evaluations there. + assert_eq!( + vclaim.eval_point(), + claim.eval_point(), + "eval_point mismatch" + ); + let pt = vclaim.eval_point(); + for (i, (n, d)) in raw.iter().enumerate() { + let en = n.evaluate(pt); + let ed = d.evaluate(pt); + let op = vclaim.openings()[i]; + assert_eq!(op.num, en, "opening[{i}] numerator mismatch"); + assert_eq!(op.den, ed, "opening[{i}] denominator mismatch"); + } + } + + // Full prove -> verify round trips over the transparent-eq layer sumcheck. + #[test] + fn round_trip_single_instance_n4() { + round_trip(vec![(vec![1, 2, 3, 4], vec![5, 6, 7, 8])]); + } + + #[test] + fn round_trip_two_instances_n4() { + round_trip(vec![ + (vec![1, 2, 3, 4], vec![5, 6, 7, 8]), + (vec![9, 8, 7, 6], vec![2, 3, 4, 5]), + ]); + } + + #[test] + fn round_trip_two_instances_n8() { + round_trip(vec![ + (vec![3, 1, 4, 1, 5, 9, 2, 6], vec![2, 7, 1, 8, 2, 8, 1, 8]), + (vec![1, 1, 1, 1, 1, 1, 1, 1], vec![3, 1, 4, 1, 5, 9, 2, 6]), + ]); + } + + // Exercises cached sumchecks with 1-4 rounds and both eq-factor branches. + #[test] + fn round_trip_four_instances_n32() { + let gen = |seed: u64| -> (Vec, Vec) { + let mut s = seed.wrapping_mul(0x9e3779b97f4a7c15).wrapping_add(1); + let mut next = || { + s = s + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + (s >> 33) | 1 + }; + let num = (0..32).map(|_| next()).collect(); + let den = (0..32).map(|_| next()).collect(); + (num, den) + }; + round_trip(vec![gen(5), gen(6), gen(7), gen(8)]); + } + + #[test] + fn verify_rejects_tampered_final_claim() { + let layers = vec![Layer:: { + num: mle(vec![1, 2, 3, 4]), + den: mle(vec![5, 6, 7, 8]), + }]; + let mut tr_p = ::TE::new(b"gkr-test"); + let (mut proof, _) = prove::(layers, &mut tr_p).unwrap(); + // Corrupt one final claim. + proof.final_claims[0][0].left.num += Fr::from(1); + let mut tr_v = ::TE::new(b"gkr-test"); + assert!(verifier::verify::(&proof, &mut tr_v).is_err()); + } + + // Tamper-rejection with m >= 2: mutating per-instance final claims makes the + // verifier reject (caught by transcript binding + the gate's bilinearity). + #[test] + fn verify_rejects_complementary_instance_offset() { + let inputs = [ + (vec![1u64, 2, 3, 4], vec![5u64, 6, 7, 8]), + (vec![9u64, 8, 7, 6], vec![2u64, 3, 4, 5]), + ]; + let layers: Vec> = inputs + .iter() + .map(|(n, d)| Layer:: { + num: mle(n.clone()), + den: mle(d.clone()), + }) + .collect(); + let mut tr_p = ::TE::new(b"gkr-test"); + let (proof_ok, _) = prove::(layers, &mut tr_p).unwrap(); + + // Sanity: the honest proof verifies. + let mut tr_v0 = ::TE::new(b"gkr-test"); + assert!(verifier::verify::(&proof_ok, &mut tr_v0).is_ok()); + + // Target a SUMCHECK layer (final_claims index >= 1; index 0 is the base + // case whose per-instance cross-mult check is not batched). For num_vars=2, + // index 1 is the input-layer reduction. Apply a complementary offset to the + // two instances' left numerators. + let mut proof = proof_ok.clone(); + assert!(proof.final_claims.len() >= 2 && proof.final_claims[1].len() == 2); + let delta = Fr::from(7); + proof.final_claims[1][0].left.num += delta; + proof.final_claims[1][1].left.num -= delta; + + let mut tr_v = ::TE::new(b"gkr-test"); + assert!( + verifier::verify::(&proof, &mut tr_v).is_err(), + "tampered per-instance final claims must be rejected" + ); + } + + // ---- Gate A: staged-refactor byte-equality ---- + // + // Pre-refactor monolithic prover, kept verbatim so the staged + // `prove_prefix` + `finish_last_layer_standalone` split can be proven to + // reproduce the exact same transcript, proof bytes and opening. Delete once + // the staged equivalence is trusted (see PLAN section 17.4). + fn prove_reference( + inputs: Vec>, + transcript: &mut E2::TE, + ) -> Result<(LogupGkrProof, LogupGkrOpeningClaim), NovaError> { + let m = inputs.len(); + if m == 0 { + return Err(NovaError::InvalidNumInstances); + } + let num_vars = inputs[0].num_vars(); + if num_vars == 0 { + return Err(NovaError::InvalidSumcheckProof); + } + for inp in &inputs { + if inp.num_vars() != num_vars { + return Err(NovaError::InvalidSumcheckProof); + } + } + let mut trees: Vec>> = inputs.into_iter().map(|l| l.build_tree()).collect(); + let initial_claims: Vec> = trees + .iter_mut() + .map(|t| { + let root = t.pop().expect("tree has a root layer"); + let (n, d) = root.output_fraction(); + LayerClaim::::new(n, d) + }) + .collect(); + for c in &initial_claims { + absorb_fraction::(transcript, *c); + } + let mut running: Vec<(E2::Scalar, E2::Scalar)> = + initial_claims.iter().map(|c| (c.num, c.den)).collect(); + let mut eval_point: Vec = Vec::new(); + let mut sumchecks: Vec> = Vec::with_capacity(num_vars.saturating_sub(1)); + let mut final_claims_by_layer: Vec>> = Vec::with_capacity(num_vars); + for j in (1..=num_vars).rev() { + let lambda = transcript.squeeze(spec::LAMBDA)?; + let mut children: Vec> = trees.iter_mut().map(|t| t.pop().unwrap()).collect(); + let child_len = 1usize << (num_vars - j + 1); + let n = child_len / 2; + let mut layer_finals: Vec> = Vec::with_capacity(m); + if num_vars - j == 0 { + for c in &children { + layer_finals.push(LayerFinalClaim::::new( + c.num.Z[0], c.num.Z[1], c.den.Z[0], c.den.Z[1], + )); + } + let _ = (lambda, n); + } else { + let previous_finals = final_claims_by_layer + .last() + .expect("every sumcheck layer follows a completed parent reduction"); + let claim: E2::Scalar = { + let mut acc = E2::Scalar::ZERO; + let mut pw = E2::Scalar::ONE; + for (p, q) in &running { + acc += pw * *p; + pw *= lambda; + acc += pw * *q; + pw *= lambda; + } + acc + }; + let mut nl: Vec> = Vec::with_capacity(m); + let mut nr: Vec> = Vec::with_capacity(m); + let mut dl: Vec> = Vec::with_capacity(m); + let mut dr: Vec> = Vec::with_capacity(m); + for c in children.drain(..) { + let mut num_z = c.num.Z; + let mut den_z = c.den.Z; + let num_hi = num_z.split_off(n); + let den_hi = den_z.split_off(n); + nl.push(MultilinearPolynomial::new(num_z)); + nr.push(MultilinearPolynomial::new(num_hi)); + dl.push(MultilinearPolynomial::new(den_z)); + dr.push(MultilinearPolynomial::new(den_hi)); + } + let (round_polys, r, finals) = prove_layer_sumcheck::( + claim, + &eval_point, + &mut nl, + &mut nr, + &mut dl, + &mut dr, + lambda, + previous_finals, + transcript, + )?; + for f in &finals { + layer_finals.push(LayerFinalClaim::::new(f[0], f[1], f[2], f[3])); + } + sumchecks.push(LayerSumcheck { round_polys }); + eval_point = r; + } + for fc in &layer_finals { + absorb_fraction::(transcript, fc.left); + absorb_fraction::(transcript, fc.right); + } + let fold_r = transcript.squeeze(spec::FOLD)?; + running = layer_finals + .iter() + .map(|fc| { + let c = fc.fold_into_next_claim(fold_r); + (c.num, c.den) + }) + .collect(); + let mut next_point = Vec::with_capacity(eval_point.len() + 1); + next_point.push(fold_r); + next_point.extend_from_slice(&eval_point); + eval_point = next_point; + final_claims_by_layer.push(layer_finals); + } + let openings: Vec> = running + .iter() + .map(|(n, d)| LayerClaim::::new(*n, *d)) + .collect(); + let proof = LogupGkrProof { + initial_claims, + final_claims: final_claims_by_layer, + sumchecks, + }; + let claim = LogupGkrOpeningClaim::new(eval_point, openings); + Ok((proof, claim)) + } + + // Instance sets spanning num_vars = 1..5 and m = 1, 2, 4 (both eq-factor + // branches and both the num_vars == 1 base case and the sumcheck path). + fn sample_sets() -> Vec, Vec)>> { + let gen = |seed: u64, len: usize| -> (Vec, Vec) { + let mut s = seed.wrapping_mul(0x9e3779b97f4a7c15).wrapping_add(1); + let mut next = || { + s = s + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + (s >> 33) | 1 + }; + let num = (0..len).map(|_| next()).collect(); + let den = (0..len).map(|_| next()).collect(); + (num, den) + }; + vec![ + vec![(vec![3, 5], vec![7, 11])], // num_vars = 1, m = 1 + vec![(vec![1, 2, 3, 4], vec![5, 6, 7, 8])], // num_vars = 2, m = 1 + vec![gen(1, 8)], // num_vars = 3, m = 1 + vec![gen(2, 4), gen(3, 4)], // num_vars = 2, m = 2 + vec![gen(4, 16), gen(5, 16), gen(6, 16), gen(7, 16)], // num_vars = 4, m = 4 + vec![gen(8, 32), gen(9, 32), gen(10, 32), gen(11, 32)], // num_vars = 5, m = 4 + ] + } + + fn to_layers(set: &[(Vec, Vec)]) -> Vec> { + set + .iter() + .map(|(n, d)| Layer:: { + num: mle(n.clone()), + den: mle(d.clone()), + }) + .collect() + } + + // Gate A (prover): the staged `prove` must byte-for-byte reproduce the + // pre-refactor monolithic prover — same proof bytes, same opening, same + // post-proof transcript sentinel — on every sample instance set. + #[test] + fn staged_prove_matches_reference() { + let cfg = bincode::config::standard(); + for set in sample_sets() { + let mut tr_new = ::TE::new(b"gkr-gate-a"); + let (proof_new, claim_new) = prove::(to_layers(&set), &mut tr_new).expect("staged prove"); + let sentinel_new: Fr = tr_new.squeeze(b"sentinel").expect("sentinel"); + + let mut tr_ref = ::TE::new(b"gkr-gate-a"); + let (proof_ref, claim_ref) = + prove_reference::(to_layers(&set), &mut tr_ref).expect("reference prove"); + let sentinel_ref: Fr = tr_ref.squeeze(b"sentinel").expect("sentinel"); + + let bytes_new = bincode::serde::encode_to_vec(&proof_new, cfg).expect("encode new"); + let bytes_ref = bincode::serde::encode_to_vec(&proof_ref, cfg).expect("encode ref"); + assert_eq!(bytes_new, bytes_ref, "proof bytes differ from reference"); + assert_eq!( + claim_new.eval_point(), + claim_ref.eval_point(), + "opening eval_point differs" + ); + assert_eq!( + claim_new.openings(), + claim_ref.openings(), + "opening fractions differ" + ); + assert_eq!( + sentinel_new, sentinel_ref, + "post-proof transcript sentinel differs" + ); + } + } +} diff --git a/src/spartan/logup_gkr/verifier.rs b/src/spartan/logup_gkr/verifier.rs new file mode 100644 index 000000000..1db967f15 --- /dev/null +++ b/src/spartan/logup_gkr/verifier.rs @@ -0,0 +1,545 @@ +//! Verifier for the Logup-GKR fractional-sum argument. +//! +//! **This file defines the protocol.** It is written independently of any +//! prover: every check is derived from the GKR fractional-sum argument, and the +//! Fiat-Shamir transcript order is fixed here by soundness reasoning (see the +//! module docs below). A prover is correct **iff** it produces a transcript and +//! claims that make this verifier accept; the prover must satisfy this file, not +//! the other way around. +//! +//! ## What is proven +//! For each logup instance `i`, an input layer of projective fractions folds +//! through a binary tree to a single root fraction `(v_p_i, v_q_i)`. The +//! verifier reduces the per-instance root claims down to a single evaluation of +//! the input layer at a shared point, checking each tree layer with one batched +//! sumcheck. It returns that point and the reduced per-instance fractions; the +//! `0/den` zero-sum balance check is the host's job (this argument owns no PCS). +//! +//! ## Layer reduction (the sumcheck contract) +//! A non-root layer with `t` variables, reduced at evaluation point `τ` +//! (`|τ| = t`), carries a per-instance running claim `(v_p_i, v_q_i)`. The +//! verifier samples a fresh batching challenge `λ` and **demands** a sumcheck +//! proving +//! ```text +//! Σ_i (λ^{2i}·v_p_i + λ^{2i+1}·v_q_i) = Σ_x eq(τ, x) · Σ_i G_i(x), +//! G_i(x) = λ^{2i}·(nL_i·dR_i + nR_i·dL_i)(x) + λ^{2i+1}·(dL_i·dR_i)(x), +//! ``` +//! where `(nL_i, nR_i, dL_i, dR_i)` are the num/den halves of instance `i`'s +//! child layer. The 2m per-instance sub-claims (each instance's numerator and +//! denominator relation) are batched by **distinct powers of λ** — a Horner +//! combination over the flattened `[p_0,q_0,p_1,q_1,…]`. This is essential for +//! soundness with m ≥ 2 instances: a plain `Σ_i (v_p_i + λ·v_q_i)` would expose +//! only `Σ v_p` and `Σ v_q` (two slots regardless of m), so a prover could shift +//! one instance's numerator up and another's down and stay undetected. Distinct +//! λ-powers bind every instance's num and den separately. +//! +//! The sumcheck's final value must equal `eq(τ, r)·Σ_i G_i(r)`, reconstructed +//! here from the prover's claimed `(nL,nR,dL,dR)` at `r`. This is a demand on +//! the sumcheck backend: whatever the prover uses, its final evaluation must +//! reconcile transparently against this expression (Nova's +//! `prove_cubic_with_three_inputs` has this shape; see ppSNARK's outer check). +//! +//! ## Fiat-Shamir order (soundness) +//! The transcript order is chosen so each challenge is unpredictable given the +//! values it must bind — a prover cannot adaptively forge later messages: +//! 1. absorb all root claims `(v_p_i, v_q_i)` before anything is sampled; +//! 2. per layer (root→input): sample `λ` (bound to all prior claims/challenges, +//! so the layer's claims cannot be chosen after `λ`), run the layer sumcheck +//! (each round absorbs its polynomial then samples), absorb this layer's +//! final claims, then sample the fold challenge `r_fold` (bound to those +//! claims, so the two children cannot be chosen after `r_fold`). +//! +//! Reusing one `λ` across layers, or sampling `r_fold` before the claims it +//! folds, would each break soundness (adaptive-forgery gaps). + +use crate::errors::NovaError; +use crate::spartan::logup_gkr::fraction::Fraction; +use crate::spartan::logup_gkr::proof::{LayerClaim, LogupGkrOpeningClaim, LogupGkrProof}; +use crate::spartan::polys::eq::EqPolynomial; +use crate::spartan::sumcheck::SumcheckProof; +use crate::traits::{Engine, TranscriptEngineTrait}; +use ff::Field; + +/// The protocol's Fiat-Shamir transcript labels and sumcheck degree, defined by +/// the verifier. The prover must use exactly these. +pub mod spec { + /// Round-polynomial label inside a layer sumcheck. + pub const ROUND_POLY: &[u8] = b"p"; + /// Per-round sumcheck challenge label. + pub const ROUND_CHALLENGE: &[u8] = b"c"; + /// Per-layer batching challenge `λ`. + pub const LAMBDA: &[u8] = b"l"; + /// Per-layer fold challenge. + pub const FOLD: &[u8] = b"f"; + /// Fraction numerator label. + pub const NUM: &[u8] = b"n"; + /// Fraction denominator label. + pub const DEN: &[u8] = b"d"; + /// Degree bound of each layer's batched sumcheck round polynomial: + /// `eq` (degree 1) × gate (degree 2) = degree 3. + pub const LAYER_SC_DEGREE: usize = 3; +} + +/// Absorbs a fraction `(num, den)` into the transcript, in the order the +/// protocol fixes. Shared with the prover (which imports this). +pub fn absorb_fraction(transcript: &mut E::TE, frac: Fraction) { + transcript.absorb(spec::NUM, &frac.num); + transcript.absorb(spec::DEN, &frac.den); +} + +/// Evaluates `Σ_k coeffs[k] · lambda^k` by Horner's method over the coefficient +/// stream (lowest power first). Callers flatten their per-instance components +/// into this order — e.g. the layer sumcheck feeds `[num_0, den_0, num_1, +/// den_1, ...]`, so instance `i`'s numerator lands on `λ^{2i}` and its +/// denominator on `λ^{2i+1}` (a distinct power per component; see the layer +/// comment for why a shared power would be unsound). +fn horner_eval(coeffs: impl IntoIterator, lambda: F) -> F { + let mut acc = F::ZERO; + let mut pw = F::ONE; + for c in coeffs { + acc += pw * c; + pw *= lambda; + } + acc +} + +/// Reduces one GKR layer on the verifier side: samples `λ`, either checks the +/// root gate component-wise (root reduction, `t == 0`) or verifies the layer +/// sumcheck and reconciles its final value against `eq(τ,r)·Σ_i G_i(r)`, then +/// absorbs the split final claims, samples the fold challenge, and folds the +/// running claims and point into the child layer. +/// +/// This is the single per-layer body shared by the standalone prefix loop and +/// the standalone last-layer finish, so both replay an identical transcript. +fn verify_one_reduction( + proof: &LogupGkrProof, + t: usize, + m: usize, + running: &mut Vec>, + point: &mut Vec, + transcript: &mut E::TE, +) -> Result<(), NovaError> { + let layer_finals = &proof.final_claims[t]; + let lambda = transcript.squeeze(spec::LAMBDA)?; + + if t == 0 { + // Root reduction: the claimed root must equal the fraction-add gate of its + // two child cells **component-wise** (`num` and `den` separately). + // Cross-multiplication is unsound here: `(0,0)` cross-equals any `(a,b)`, so + // a prover could post roots `(0,1)` with all-zero children and later + // vacuously pass host reconcile against real columns. HyperPlonk uses the + // same exact check; honesty already produces matching MLE components, so + // this rejects only degenerate / scaled forgeries. + for i in 0..m { + let gate = layer_finals[i].compute_gate(); + let r = running[i]; + if r.num != gate.num || r.den != gate.den { + return Err(NovaError::InvalidSumcheckProof); + } + } + } else { + // Layer sumcheck. The 2m per-instance sub-claims are batched by DISTINCT + // powers of λ: instance i's numerator gets λ^{2i}, its denominator λ^{2i+1} + // (Horner over the flattened `[p_0,q_0,p_1,q_1,...]`). A distinct power per + // component binds every instance separately — a plain `Σ_i (p_i + λ q_i)` + // would only expose `Σ p` and `Σ q` (two slots regardless of m), letting a + // prover offset one instance's numerator up and another's down undetected. + let claim: E::Scalar = horner_eval(running.iter().flat_map(|f| [f.num, f.den]), lambda); + let sc = SumcheckProof::::new(proof.sumchecks[t - 1].round_polys.clone()); + // The layer at step `t` has `t` variables, and `point` (its evaluation + // point, i.e. the sumcheck's τ) has length `t`. + let num_rounds = point.len(); + let (sc_eval, r) = sc.verify(claim, num_rounds, spec::LAYER_SC_DEGREE, transcript)?; + + // The sumcheck contract: its final value must equal + // eq(τ, r) · Σ_i [ λ^{2i}·gate_i.num + λ^{2i+1}·gate_i.den ] + // where gate_i is the fraction-add of instance i's two children. + let eq_at_r = EqPolynomial::new(point.clone()).evaluate(&r); + let gate_sum: E::Scalar = horner_eval( + layer_finals.iter().flat_map(|fc| { + let g = fc.compute_gate(); + [g.num, g.den] + }), + lambda, + ); + if sc_eval != eq_at_r * gate_sum { + return Err(NovaError::InvalidSumcheckProof); + } + *point = r; + } + + // Bind this layer's claims, then draw the fold challenge (so the children + // cannot be chosen after it), then fold to the next layer's claims/point. + for fc in layer_finals { + absorb_fraction::(transcript, fc.left); + absorb_fraction::(transcript, fc.right); + } + let r_fold = transcript.squeeze(spec::FOLD)?; + + *running = layer_finals + .iter() + .map(|fc| fc.fold_into_next_claim(r_fold)) + .collect(); + // The next layer's point prepends the fold challenge as the new top (MSB) + // variable: point' = [r_fold, ...point]. + let mut next_point = Vec::with_capacity(point.len() + 1); + next_point.push(r_fold); + next_point.extend_from_slice(point); + *point = next_point; + Ok(()) +} + +/// The verifier state captured after replaying the GKR prefix (every layer +/// reduction except the last). Mirrors [`super::prover::GkrProverPrefix`]: it +/// holds the running per-instance claims about the last layer's parent and the +/// evaluation point `τ` of the last-layer sumcheck. +pub(crate) struct GkrVerifierPrefix { + /// Number of instances. + pub(crate) m: usize, + /// Number of tree layers reduced in total (`log2` height). + pub(crate) num_vars: usize, + /// Running per-instance claims about the last layer's parent (`layers[1]`), or + /// the root claim when `num_vars == 1`. + pub(crate) running: Vec>, + /// Evaluation point `τ` for the last-layer sumcheck (length `num_vars - 1`). + pub(crate) point: Vec, +} + +impl GkrVerifierPrefix { + /// Assembles the prefix state (used by the fused-driver host to reconstruct it + /// from prefix proof pieces). + pub(crate) fn new( + m: usize, + num_vars: usize, + running: Vec>, + point: Vec, + ) -> Self { + Self { + m, + num_vars, + running, + point, + } + } +} + +/// Replays the GKR prefix: validates shape, absorbs the root claims, and reduces +/// every layer **except the last**, returning the state to finish. For +/// `num_vars == 1` the prefix is empty (the single layer is the last one). +pub(crate) fn verify_prefix( + proof: &LogupGkrProof, + transcript: &mut E::TE, +) -> Result, NovaError> { + let m = proof.initial_claims.len(); + if m == 0 { + return Err(NovaError::InvalidNumInstances); + } + // Structural well-formedness: `final_claims` has one entry per reduction step + // (num_vars entries). The root reduction (index 0) carries no sumcheck, so + // `sumchecks.len() + 1 == final_claims.len()`, and every layer carries one + // split claim per instance. + let num_vars = proof.final_claims.len(); + if num_vars == 0 || proof.sumchecks.len() + 1 != num_vars { + return Err(NovaError::InvalidSumcheckProof); + } + if proof.final_claims.iter().any(|layer| layer.len() != m) { + return Err(NovaError::InvalidSumcheckProof); + } + + // (1) Bind the root claims before any challenge is drawn. + for c in &proof.initial_claims { + absorb_fraction::(transcript, *c); + } + + // running[i] = v_p_i / v_q_i: the claim about the current layer at `point`. + let mut running: Vec> = proof.initial_claims.clone(); + let mut point: Vec = Vec::new(); + + // (2) Reduce every layer except the last (t = 0 … num_vars - 2). + for t in 0..num_vars - 1 { + verify_one_reduction::(proof, t, m, &mut running, &mut point, transcript)?; + } + + Ok(GkrVerifierPrefix { + m, + num_vars, + running, + point, + }) +} + +/// Finishes the standalone verification from the prefix state by reducing the +/// last layer with the same `verify_one_reduction` body the prefix uses, then +/// returns the shared opening claim. +pub(crate) fn finish_last_layer_verify( + proof: &LogupGkrProof, + state: GkrVerifierPrefix, + transcript: &mut E::TE, +) -> Result, NovaError> { + let GkrVerifierPrefix { + m, + num_vars, + mut running, + mut point, + } = state; + verify_one_reduction::(proof, num_vars - 1, m, &mut running, &mut point, transcript)?; + Ok(LogupGkrOpeningClaim::new(point, running)) +} + +/// Verifies the batched fractional-sum proof and returns the shared opening +/// claim (evaluation point + per-instance input-layer fractions). Accepts iff +/// the proof satisfies the protocol defined in this module. +/// +/// This is the prefix + last-layer composition; the two stages share the +/// per-layer body `verify_one_reduction`, so the replay is identical to the +/// former monolithic loop. +pub fn verify( + proof: &LogupGkrProof, + transcript: &mut E::TE, +) -> Result, NovaError> { + let state = verify_prefix::(proof, transcript)?; + finish_last_layer_verify::(proof, state, transcript) +} + +#[cfg(test)] +mod tests { + //! Independence tests: these build a valid proof **by hand** (from the tree + //! fold in `layer.rs` plus the transcript spec in this module) with no use of + //! the `prover` module, demonstrating that the verifier stands on its own. + use super::*; + use crate::spartan::logup_gkr::layer::Layer; + use crate::spartan::logup_gkr::proof::{LayerFinalClaim, LogupGkrProof}; + use crate::spartan::polys::multilinear::MultilinearPolynomial; + + type E = crate::provider::Bn256EngineKZG; + type Fr = ::Scalar; + + fn mle(v: Vec) -> MultilinearPolynomial { + MultilinearPolynomial::new(v.into_iter().map(Fr::from).collect()) + } + + // Hand-build the proof for a single-instance, 2-leaf tree (num_vars = 1): + // only the root reduction (base case) runs — no sumcheck — so the whole proof + // is constructible from `layer.rs` alone, following this module's spec. + fn hand_built_2leaf(num: Vec, den: Vec) -> LogupGkrProof { + assert_eq!(num.len(), 2); + let input = Layer:: { + num: mle(num.clone()), + den: mle(den.clone()), + }; + let tree = input.build_tree(); // [input(1 var), root(0 var)] + let (rn, rd) = tree[1].output_fraction(); + // Base layer split claim = the two child cells directly (nL,nR,dL,dR). + let child = &tree[0]; + let final_claim = LayerFinalClaim::::new( + child.num.Z[0], + child.num.Z[1], + child.den.Z[0], + child.den.Z[1], + ); + LogupGkrProof { + initial_claims: vec![LayerClaim::::new(rn, rd)], + final_claims: vec![vec![final_claim]], + sumchecks: vec![], + } + } + + #[test] + fn verifier_accepts_hand_built_valid_proof() { + let proof = hand_built_2leaf(vec![3, 5], vec![7, 11]); + let mut tr = ::TE::new(b"gkr-indep"); + let claim = + verify::(&proof, &mut tr).expect("verifier must accept a valid hand-built proof"); + // One instance, one variable → eval_point has length 1, one opening. + assert_eq!(claim.eval_point().len(), 1); + assert_eq!(claim.openings().len(), 1); + } + + #[test] + fn verifier_rejects_wrong_root() { + let mut proof = hand_built_2leaf(vec![3, 5], vec![7, 11]); + // Corrupt the root claim so it no longer equals the gate of its children. + proof.initial_claims[0].num += Fr::from(1); + let mut tr = ::TE::new(b"gkr-indep"); + assert!(verify::(&proof, &mut tr).is_err()); + } + + #[test] + fn verifier_rejects_malformed_shape() { + let mut proof = hand_built_2leaf(vec![3, 5], vec![7, 11]); + // sumchecks.len() + 1 must equal final_claims.len(); break it. + proof + .sumchecks + .push(crate::spartan::logup_gkr::proof::LayerSumcheck { + round_polys: vec![], + }); + let mut tr = ::TE::new(b"gkr-indep"); + assert!(verify::(&proof, &mut tr).is_err()); + } + + #[test] + fn verifier_rejects_zero_zero_children_of_unit_root() { + // P0 forgery fragment: root `(0,1)` with children `(0,0)`. Under + // cross-multiplication `0·0 == 0·1` this would pass; exact equality + // rejects it. gate = (0,0) ≠ (0,1). + let zero = Fraction::new(Fr::ZERO, Fr::ZERO); + let proof = LogupGkrProof { + initial_claims: vec![Fraction::new(Fr::ZERO, Fr::ONE)], + final_claims: vec![vec![LayerFinalClaim { + left: zero, + right: zero, + }]], + sumchecks: vec![], + }; + let mut tr = ::TE::new(b"gkr-p0"); + assert!( + verify::(&proof, &mut tr).is_err(), + "must reject (0,1) root with (0,0) children" + ); + } + + #[test] + fn verifier_rejects_scaled_root() { + // Exact equality also rejects a nonzero scale of an otherwise valid gate + // (cross-mult would accept). + let mut proof = hand_built_2leaf(vec![3, 5], vec![7, 11]); + proof.initial_claims[0].num *= Fr::from(2); + proof.initial_claims[0].den *= Fr::from(2); + let mut tr = ::TE::new(b"gkr-indep"); + assert!(verify::(&proof, &mut tr).is_err()); + } + + // ---- Gate A: staged-refactor byte-equality ---- + // + // Pre-refactor monolithic verifier, kept verbatim so the staged + // `verify_prefix` + `finish_last_layer_verify` split can be proven to replay + // an identical transcript and return an identical opening claim. Delete once + // the staged equivalence is trusted (see PLAN section 17.4). This one test + // deliberately consumes the `prover` module (unlike the independence tests + // above) because it compares two verifier drivers on real proofs. + fn verify_reference( + proof: &LogupGkrProof, + transcript: &mut E2::TE, + ) -> Result, NovaError> { + let m = proof.initial_claims.len(); + if m == 0 { + return Err(NovaError::InvalidNumInstances); + } + let num_vars = proof.final_claims.len(); + if num_vars == 0 || proof.sumchecks.len() + 1 != num_vars { + return Err(NovaError::InvalidSumcheckProof); + } + if proof.final_claims.iter().any(|layer| layer.len() != m) { + return Err(NovaError::InvalidSumcheckProof); + } + for c in &proof.initial_claims { + absorb_fraction::(transcript, *c); + } + let mut running: Vec> = proof.initial_claims.clone(); + let mut point: Vec = Vec::new(); + for (t, layer_finals) in proof.final_claims.iter().enumerate() { + let lambda = transcript.squeeze(spec::LAMBDA)?; + if t == 0 { + for i in 0..m { + let gate = layer_finals[i].compute_gate(); + let r = running[i]; + if r.num != gate.num || r.den != gate.den { + return Err(NovaError::InvalidSumcheckProof); + } + } + } else { + let claim: E2::Scalar = horner_eval(running.iter().flat_map(|f| [f.num, f.den]), lambda); + let sc = SumcheckProof::::new(proof.sumchecks[t - 1].round_polys.clone()); + let num_rounds = point.len(); + let (sc_eval, r) = sc.verify(claim, num_rounds, spec::LAYER_SC_DEGREE, transcript)?; + let eq_at_r = EqPolynomial::new(point.clone()).evaluate(&r); + let gate_sum: E2::Scalar = horner_eval( + layer_finals.iter().flat_map(|fc| { + let g = fc.compute_gate(); + [g.num, g.den] + }), + lambda, + ); + if sc_eval != eq_at_r * gate_sum { + return Err(NovaError::InvalidSumcheckProof); + } + point = r; + } + for fc in layer_finals { + absorb_fraction::(transcript, fc.left); + absorb_fraction::(transcript, fc.right); + } + let r_fold = transcript.squeeze(spec::FOLD)?; + running = layer_finals + .iter() + .map(|fc| fc.fold_into_next_claim(r_fold)) + .collect(); + let mut next_point = Vec::with_capacity(point.len() + 1); + next_point.push(r_fold); + next_point.extend_from_slice(&point); + point = next_point; + } + Ok(LogupGkrOpeningClaim::new(point, running)) + } + + // Gate A (verifier): the staged `verify` must replay the same transcript and + // return the same opening claim as the pre-refactor monolithic verifier, on + // real proofs covering num_vars = 1..5 (base case + sumcheck path). + #[test] + fn staged_verify_matches_reference() { + use crate::spartan::logup_gkr::prover; + + let gen = |seed: u64, len: usize| -> (Vec, Vec) { + let mut s = seed.wrapping_mul(0x9e3779b97f4a7c15).wrapping_add(1); + let mut next = || { + s = s + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + (s >> 33) | 1 + }; + let num = (0..len).map(|_| next()).collect(); + let den = (0..len).map(|_| next()).collect(); + (num, den) + }; + let sets: Vec, Vec)>> = vec![ + vec![(vec![3, 5], vec![7, 11])], + vec![(vec![1, 2, 3, 4], vec![5, 6, 7, 8])], + vec![gen(1, 8)], + vec![gen(2, 4), gen(3, 4)], + vec![gen(4, 16), gen(5, 16), gen(6, 16), gen(7, 16)], + vec![gen(8, 32), gen(9, 32), gen(10, 32), gen(11, 32)], + ]; + + for set in sets { + let layers: Vec> = set + .iter() + .map(|(n, d)| Layer:: { + num: mle(n.clone()), + den: mle(d.clone()), + }) + .collect(); + let mut tr_p = ::TE::new(b"gkr-verify"); + let (proof, _) = prover::prove::(layers, &mut tr_p).expect("prove"); + + let mut tr1 = ::TE::new(b"gkr-verify"); + let claim1 = verify::(&proof, &mut tr1).expect("staged verify"); + let s1: Fr = tr1.squeeze(b"sentinel").expect("sentinel"); + + let mut tr2 = ::TE::new(b"gkr-verify"); + let claim2 = verify_reference::(&proof, &mut tr2).expect("reference verify"); + let s2: Fr = tr2.squeeze(b"sentinel").expect("sentinel"); + + assert_eq!( + claim1.eval_point(), + claim2.eval_point(), + "verify eval_point differs from reference" + ); + assert_eq!( + claim1.openings(), + claim2.openings(), + "verify openings differ from reference" + ); + assert_eq!(s1, s2, "post-verify transcript sentinel differs"); + } + } +} diff --git a/src/spartan/mem_check_logup.rs b/src/spartan/mem_check_logup.rs new file mode 100644 index 000000000..af2eea889 --- /dev/null +++ b/src/spartan/mem_check_logup.rs @@ -0,0 +1,557 @@ +//! Inverse-logup memory-check for ppSNARK (the original Microsoft Nova +//! implementation). +//! +//! Selected when the `logup-no-gkr` feature is enabled; otherwise ppSNARK uses +//! the Logup-GKR memory-check in [`super::mem_check_logup_gkr`]. This module +//! holds the pieces specific to the inverse-logup approach — the +//! [`MemorySumcheckInstance`] (six-route sumcheck proving +//! `Σ TS[i]/(T[i]+r) − 1/(W[i]+r) = 0` per row/col via committed inverse +//! oracles) and the [`LogupProofData`] bundle of its proof fields — so they can +//! be feature-gated out of the SNARK cleanly. + +use crate::{ + errors::NovaError, + spartan::{ + batch_invert, + math::Math, + polys::{ + eq::EqPolynomial, identity::IdentityPolynomial, multilinear::MultilinearPolynomial, + multilinear::SparsePolynomial, + }, + sumcheck::{eq_sumcheck::EqSumCheckInstance, SumcheckEngine, SumcheckProof}, + }, + traits::{ + commitment::CommitmentEngineTrait, evm_serde::EvmCompatSerde, Engine, TranscriptEngineTrait, + }, + zip_with, Commitment, CommitmentKey, +}; +use ff::Field; +use rayon::prelude::*; +use serde::{Deserialize, Serialize}; +use serde_with::serde_as; + +/// The inverse-logup memory-check proof fields carried in the ppSNARK proof: +/// commitments to the four inverse oracles (`1/(T+r)·TS`, `1/(W+r)` for row/col) +/// and their evaluations at the shared inner point. Bundled so the SNARK can +/// gate the whole inverse-logup path behind one field. +#[serde_as] +#[derive(Clone, Debug, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct LogupProofData { + /// Commitment to `TS_row/(T_row+r)`. + pub comm_t_plus_r_inv_row: Commitment, + /// Commitment to `1/(W_row+r)`. + pub comm_w_plus_r_inv_row: Commitment, + /// Commitment to `TS_col/(T_col+r)`. + pub comm_t_plus_r_inv_col: Commitment, + /// Commitment to `1/(W_col+r)`. + pub comm_w_plus_r_inv_col: Commitment, + /// Evaluation of `TS_row/(T_row+r)` at the inner point. + #[serde_as(as = "EvmCompatSerde")] + pub eval_t_plus_r_inv_row: E::Scalar, + /// Evaluation of `1/(W_row+r)` at the inner point. + #[serde_as(as = "EvmCompatSerde")] + pub eval_w_plus_r_inv_row: E::Scalar, + /// Evaluation of `TS_col/(T_col+r)` at the inner point. + #[serde_as(as = "EvmCompatSerde")] + pub eval_t_plus_r_inv_col: E::Scalar, + /// Evaluation of `1/(W_col+r)` at the inner point. + #[serde_as(as = "EvmCompatSerde")] + pub eval_w_plus_r_inv_col: E::Scalar, +} + +/// Memory sumcheck instance for PPSNARK LogUp +pub struct MemorySumcheckInstance { + // row + w_plus_r_row: MultilinearPolynomial, + t_plus_r_row: MultilinearPolynomial, + t_plus_r_inv_row: MultilinearPolynomial, + w_plus_r_inv_row: MultilinearPolynomial, + ts_row: MultilinearPolynomial, + + // col + w_plus_r_col: MultilinearPolynomial, + t_plus_r_col: MultilinearPolynomial, + t_plus_r_inv_col: MultilinearPolynomial, + w_plus_r_inv_col: MultilinearPolynomial, + ts_col: MultilinearPolynomial, + + eq_sumcheck: EqSumCheckInstance, + + // Per-claim running claims and saved evaluation points (BDDT, eprint 2025/1117 Section 6.2) + running_claims: [E::Scalar; 6], + saved_evals: [[E::Scalar; 3]; 6], +} + +impl MemorySumcheckInstance { + /// Computes witnesses for MemoryInstanceSumcheck + /// + /// # Description + /// We use the logUp protocol to prove that + /// sum TS\[i\]/(T\[i\] + r) - 1/(W\[i\] + r) = 0 + /// where + /// T_row\[i\] = mem_row\[i\] * gamma + i + /// = eq(tau)\[i\] * gamma + i + /// W_row\[i\] = L_row\[i\] * gamma + addr_row\[i\] + /// = eq(tau)\[row\[i\]\] * gamma + addr_row\[i\] + /// T_col\[i\] = mem_col\[i\] * gamma + i + /// = z\[i\] * gamma + i + /// W_col\[i\] = L_col\[i\] * gamma + addr_col\[i\] + /// = z\[col\[i\]\] * gamma + addr_col\[i\] + /// and + /// TS_row, TS_col are integer-valued vectors representing the number of reads + /// to each memory cell of L_row, L_col + /// + /// The function returns oracles for the polynomials TS\[i\]/(T\[i\] + r), 1/(W\[i\] + r), + /// as well as auxiliary polynomials T\[i\] + r, W\[i\] + r + pub fn compute_oracles( + ck: &CommitmentKey, + r: &E::Scalar, + gamma: &E::Scalar, + mem_row: &[E::Scalar], + addr_row: &[E::Scalar], + L_row: &[E::Scalar], + ts_row: &[E::Scalar], + mem_col: &[E::Scalar], + addr_col: &[E::Scalar], + L_col: &[E::Scalar], + ts_col: &[E::Scalar], + ) -> Result<([Commitment; 4], [Vec; 4], [Vec; 4]), NovaError> { + // hash the tuples of (addr,val) memory contents and read responses into a single field element using `hash_func` + let hash_func_vec = |mem: &[E::Scalar], + addr: &[E::Scalar], + lookups: &[E::Scalar]| + -> (Vec, Vec) { + let hash_func = |addr: &E::Scalar, val: &E::Scalar| -> E::Scalar { *val * gamma + *addr }; + assert_eq!(addr.len(), lookups.len()); + rayon::join( + || { + (0..mem.len()) + .map(|i| hash_func(&E::Scalar::from(i as u64), &mem[i])) + .collect::>() + }, + || { + (0..addr.len()) + .map(|i| hash_func(&addr[i], &lookups[i])) + .collect::>() + }, + ) + }; + + let ((T_row, W_row), (T_col, W_col)) = rayon::join( + || hash_func_vec(mem_row, addr_row, L_row), + || hash_func_vec(mem_col, addr_col, L_col), + ); + + // compute vectors TS[i]/(T[i] + r) and 1/(W[i] + r) + let helper = |T: &[E::Scalar], + W: &[E::Scalar], + TS: &[E::Scalar], + r: &E::Scalar| + -> Result< + ( + Vec, + Vec, + Vec, + Vec, + ), + NovaError, + > { + let t_plus_r_and_w_plus_r = T + .par_iter() + .chain(W.par_iter()) + .map(|e| *e + *r) + .collect::>(); + + let inv = batch_invert(&t_plus_r_and_w_plus_r)?; + + let mut t_plus_r = t_plus_r_and_w_plus_r; + let w_plus_r = t_plus_r.split_off(T.len()); + + let mut t_plus_r_inv = inv; + let w_plus_r_inv = t_plus_r_inv.split_off(T.len()); + + // compute inv[i] * TS[i] in parallel + t_plus_r_inv = zip_with!((t_plus_r_inv.into_par_iter(), TS.par_iter()), |e1, e2| e1 + * *e2) + .collect::>(); + + Ok((t_plus_r_inv, w_plus_r_inv, t_plus_r, w_plus_r)) + }; + + let (row, col) = rayon::join( + || helper(&T_row, &W_row, ts_row, r), + || helper(&T_col, &W_col, ts_col, r), + ); + + let (t_plus_r_inv_row, w_plus_r_inv_row, t_plus_r_row, w_plus_r_row) = row?; + let (t_plus_r_inv_col, w_plus_r_inv_col, t_plus_r_col, w_plus_r_col) = col?; + + let ( + (comm_t_plus_r_inv_row, comm_w_plus_r_inv_row), + (comm_t_plus_r_inv_col, comm_w_plus_r_inv_col), + ) = rayon::join( + || { + rayon::join( + || E::CE::commit(ck, &t_plus_r_inv_row, &E::Scalar::ZERO), + || E::CE::commit(ck, &w_plus_r_inv_row, &E::Scalar::ZERO), + ) + }, + || { + rayon::join( + || E::CE::commit(ck, &t_plus_r_inv_col, &E::Scalar::ZERO), + || E::CE::commit(ck, &w_plus_r_inv_col, &E::Scalar::ZERO), + ) + }, + ); + + let comm_vec = [ + comm_t_plus_r_inv_row, + comm_w_plus_r_inv_row, + comm_t_plus_r_inv_col, + comm_w_plus_r_inv_col, + ]; + + let poly_vec = [ + t_plus_r_inv_row, + w_plus_r_inv_row, + t_plus_r_inv_col, + w_plus_r_inv_col, + ]; + + let aux_poly_vec = [t_plus_r_row, w_plus_r_row, t_plus_r_col, w_plus_r_col]; + + Ok((comm_vec, poly_vec, aux_poly_vec)) + } + + /// Create a new memory sumcheck instance + pub fn new( + polys_oracle: [Vec; 4], + polys_aux: [Vec; 4], + rhos: Vec, + ts_row: Vec, + ts_col: Vec, + ) -> Self { + let [t_plus_r_inv_row, w_plus_r_inv_row, t_plus_r_inv_col, w_plus_r_inv_col] = polys_oracle; + let [t_plus_r_row, w_plus_r_row, t_plus_r_col, w_plus_r_col] = polys_aux; + + Self { + w_plus_r_row: MultilinearPolynomial::new(w_plus_r_row), + t_plus_r_row: MultilinearPolynomial::new(t_plus_r_row), + t_plus_r_inv_row: MultilinearPolynomial::new(t_plus_r_inv_row), + w_plus_r_inv_row: MultilinearPolynomial::new(w_plus_r_inv_row), + ts_row: MultilinearPolynomial::new(ts_row), + w_plus_r_col: MultilinearPolynomial::new(w_plus_r_col), + t_plus_r_col: MultilinearPolynomial::new(t_plus_r_col), + t_plus_r_inv_col: MultilinearPolynomial::new(t_plus_r_inv_col), + w_plus_r_inv_col: MultilinearPolynomial::new(w_plus_r_inv_col), + ts_col: MultilinearPolynomial::new(ts_col), + eq_sumcheck: EqSumCheckInstance::new(rhos), + running_claims: [E::Scalar::ZERO; 6], + saved_evals: [[E::Scalar::ZERO; 3]; 6], + } + } +} + +impl SumcheckEngine for MemorySumcheckInstance { + fn initial_claims(&self) -> Vec { + vec![E::Scalar::ZERO; 6] + } + + fn degree(&self) -> usize { + 3 + } + + fn size(&self) -> usize { + // sanity checks + assert_eq!(self.w_plus_r_row.len(), self.t_plus_r_row.len()); + assert_eq!(self.w_plus_r_row.len(), self.ts_row.len()); + assert_eq!(self.w_plus_r_row.len(), self.w_plus_r_col.len()); + assert_eq!(self.w_plus_r_row.len(), self.t_plus_r_col.len()); + assert_eq!(self.w_plus_r_row.len(), self.ts_col.len()); + + self.w_plus_r_row.len() + } + + fn evaluation_points(&mut self) -> Vec> { + // Pre-borrow all fields as shared references for parallel access + let eq = &self.eq_sumcheck; + let running_claims = &self.running_claims; + let t_plus_r_inv_row = &self.t_plus_r_inv_row; + let w_plus_r_inv_row = &self.w_plus_r_inv_row; + let t_plus_r_row = &self.t_plus_r_row; + let w_plus_r_row = &self.w_plus_r_row; + let ts_row = &self.ts_row; + let t_plus_r_inv_col = &self.t_plus_r_inv_col; + let w_plus_r_inv_col = &self.w_plus_r_inv_col; + let t_plus_r_col = &self.t_plus_r_col; + let w_plus_r_col = &self.w_plus_r_col; + let ts_col = &self.ts_col; + + // inv related evaluation points for linear (A - B) pattern (no claim derivation) + // 0 = sum TS[i]/(T[i] + r) - 1/(W[i] + r) + let ( + ((eval_inv_0_row, eval_inv_3_row), (eval_inv_0_col, eval_inv_3_col)), + ( + ((eval_T_0_row, eval_T_2_row, eval_T_3_row), (eval_W_0_row, eval_W_2_row, eval_W_3_row)), + ((eval_T_0_col, eval_T_2_col, eval_T_3_col), (eval_W_0_col, eval_W_2_col, eval_W_3_col)), + ), + ) = rayon::join( + || { + rayon::join( + || SumcheckProof::::compute_eval_points_linear(t_plus_r_inv_row, w_plus_r_inv_row), + || SumcheckProof::::compute_eval_points_linear(t_plus_r_inv_col, w_plus_r_inv_col), + ) + }, + || { + rayon::join( + || { + // Row evaluation points (claim-derived, BDDT Section 6.2) + rayon::join( + || { + // 0 = sum eq[i] * (inv_T[i] * (T[i] + r) - TS[i])) + eq.evaluation_points_cubic_with_three_inputs( + t_plus_r_inv_row, + t_plus_r_row, + ts_row, + running_claims[2], + ) + }, + || { + // 0 = sum eq[i] * (inv_W[i] * (W[i] + r) - 1)) + eq.evaluation_points_cubic_with_two_inputs( + w_plus_r_inv_row, + w_plus_r_row, + running_claims[3], + ) + }, + ) + }, + || { + // Column evaluation points (claim-derived, BDDT Section 6.2) + rayon::join( + || { + eq.evaluation_points_cubic_with_three_inputs( + t_plus_r_inv_col, + t_plus_r_col, + ts_col, + running_claims[4], + ) + }, + || { + eq.evaluation_points_cubic_with_two_inputs( + w_plus_r_inv_col, + w_plus_r_col, + running_claims[5], + ) + }, + ) + }, + ) + }, + ); + + // Save evaluation points for running claim updates in bound() + self.saved_evals = [ + [eval_inv_0_row, E::Scalar::ZERO, eval_inv_3_row], + [eval_inv_0_col, E::Scalar::ZERO, eval_inv_3_col], + [eval_T_0_row, eval_T_2_row, eval_T_3_row], + [eval_W_0_row, eval_W_2_row, eval_W_3_row], + [eval_T_0_col, eval_T_2_col, eval_T_3_col], + [eval_W_0_col, eval_W_2_col, eval_W_3_col], + ]; + + self.saved_evals.iter().map(|e| e.to_vec()).collect() + } + + fn bound(&mut self, r: &E::Scalar) { + for j in 0..6 { + self.running_claims[j] = + SumcheckProof::::update_claim(self.running_claims[j], &self.saved_evals[j], r); + } + + [ + &mut self.t_plus_r_row, + &mut self.t_plus_r_inv_row, + &mut self.w_plus_r_row, + &mut self.w_plus_r_inv_row, + &mut self.ts_row, + &mut self.t_plus_r_col, + &mut self.t_plus_r_inv_col, + &mut self.w_plus_r_col, + &mut self.w_plus_r_inv_col, + &mut self.ts_col, + ] + .par_iter_mut() + .for_each(|poly| poly.bind_poly_var_top(r)); + + self.eq_sumcheck.bound(r); + } + + fn final_claims(&self) -> Vec> { + let poly_row_final = vec![ + self.t_plus_r_inv_row[0], + self.w_plus_r_inv_row[0], + self.ts_row[0], + ]; + + let poly_col_final = vec![ + self.t_plus_r_inv_col[0], + self.w_plus_r_inv_col[0], + self.ts_col[0], + ]; + + vec![poly_row_final, poly_col_final] + } +} + +/// Prover side of the inverse-logup memory-check: builds the inverse oracles, +/// commits to them, absorbs the commitments, squeezes the `rho` challenges, and +/// returns the `MemorySumcheckInstance` (the first `prove_helper` slot) plus the +/// oracle commitments and polynomials (needed later for the batched PCS +/// opening). `addr_row`/`addr_col` are `S_repr.row`/`col`. +#[allow(clippy::too_many_arguments)] +pub fn prove_step( + ck: &CommitmentKey, + r: E::Scalar, + gamma: E::Scalar, + mem_row: &[E::Scalar], + addr_row: &[E::Scalar], + L_row: &[E::Scalar], + ts_row: &[E::Scalar], + mem_col: &[E::Scalar], + addr_col: &[E::Scalar], + L_col: &[E::Scalar], + ts_col: &[E::Scalar], + num_rounds_inner: usize, + transcript: &mut E::TE, +) -> Result< + ( + MemorySumcheckInstance, + [Commitment; 4], + [Vec; 4], + ), + NovaError, +> { + let (comm_mem_oracles, mem_oracles, mem_aux) = MemorySumcheckInstance::::compute_oracles( + ck, &r, &gamma, mem_row, addr_row, L_row, ts_row, mem_col, addr_col, L_col, ts_col, + )?; + transcript.absorb(b"l", &comm_mem_oracles.as_slice()); + let rho = (0..num_rounds_inner) + .map(|_| transcript.squeeze(b"r")) + .collect::, NovaError>>()?; + let inst = MemorySumcheckInstance::new( + mem_oracles.clone(), + mem_aux, + rho, + ts_row.to_vec(), + ts_col.to_vec(), + ); + Ok((inst, comm_mem_oracles, mem_oracles)) +} + +/// Number of batched-inner claims the memory-check slot contributes (the six +/// inverse-logup routes at coeffs `[0, 6)`). `prove_helper` places the +/// memory-check slot first, so the inner/witness claims come after these. +pub const NUM_MEM_CLAIMS: usize = 6; + +/// The inverse-logup contribution to the batched inner sumcheck's **initial** +/// claim. The six memory routes prove `0 = Σ ...`, so their combined initial +/// claim is zero — this exists for symmetry with the Logup-GKR slot's +/// `verify_initial_claim`, so the caller adds one memory-check contribution +/// regardless of which implementation is active. +pub fn verify_initial_claim(_coeffs: &[E::Scalar]) -> E::Scalar { + E::Scalar::ZERO +} + +/// Verifier side, transcript phase: absorbs the four inverse-oracle commitments +/// and squeezes the `rho` challenges (the eq randomness for the memory +/// sumcheck), mirroring [`prove_step`]. Must run before the inner sumcheck's `s` +/// challenge is drawn. +pub fn verify_pre_inner( + data: &LogupProofData, + num_rounds_inner: usize, + transcript: &mut E::TE, +) -> Result, NovaError> { + transcript.absorb( + b"l", + &vec![ + data.comm_t_plus_r_inv_row, + data.comm_w_plus_r_inv_row, + data.comm_t_plus_r_inv_col, + data.comm_w_plus_r_inv_col, + ] + .as_slice(), + ); + (0..num_rounds_inner) + .map(|_| transcript.squeeze(b"r")) + .collect() +} + +/// Verifier side, final-claim phase: reconstructs the memory-check contribution +/// to the batched inner sumcheck's final claim — the six routes at coeff indices +/// `0..6`, proving `Σ TS/(T+r) − 1/(W+r) = 0` and the well-formedness of the +/// four inverse oracles. `rho` is from [`verify_pre_inner`]; the eval arguments +/// are the shared evaluations at `r_inner_batched`. +#[allow(clippy::too_many_arguments)] +pub fn verify_final_claim( + data: &LogupProofData, + coeffs: &[E::Scalar], + rho: Vec, + gamma: E::Scalar, + r: E::Scalar, + r_outer_full: &[E::Scalar], + r_inner_batched: &[E::Scalar], + num_rounds_inner: usize, + num_vars: usize, + n: usize, + eval_W: E::Scalar, + eval_L_row: E::Scalar, + eval_L_col: E::Scalar, + eval_row: E::Scalar, + eval_col: E::Scalar, + eval_ts_row: E::Scalar, + eval_ts_col: E::Scalar, + x: &[E::Scalar], +) -> E::Scalar { + let rand_eq_bound = EqPolynomial::new(rho).evaluate(r_inner_batched); + let eq_r_outer = EqPolynomial::new(r_outer_full.to_vec()); + let eq_r_outer_at_r_inner = eq_r_outer.evaluate(r_inner_batched); + + // mem_col = z at r_inner_batched, reconstructed from eval_W and public IO. + let eval_mem_col_at_r_inner = { + let (fac, unpad) = { + let l = n.log_2() - (2 * num_vars).log_2(); + let mut fac = E::Scalar::ONE; + for r_p in r_inner_batched.iter().take(l) { + fac *= E::Scalar::ONE - r_p + } + (fac, r_inner_batched[l..].to_vec()) + }; + let eval_x = { + let poly_x = SparsePolynomial::new(unpad.len() - 1, x.to_vec()); + poly_x.evaluate(&unpad[1..]) + }; + eval_W + fac * unpad[0] * eval_x + }; + + let eval_t_plus_r_row = { + let eval_addr = IdentityPolynomial::new(num_rounds_inner).evaluate(r_inner_batched); + eval_addr + gamma * eq_r_outer_at_r_inner + r // mem_row = eq(r_outer_full, ·) + }; + let eval_w_plus_r_row = eval_row + gamma * eval_L_row + r; + let eval_t_plus_r_col = { + let eval_addr = IdentityPolynomial::new(num_rounds_inner).evaluate(r_inner_batched); + eval_addr + gamma * eval_mem_col_at_r_inner + r + }; + let eval_w_plus_r_col = eval_col + gamma * eval_L_col + r; + + coeffs[0] * (data.eval_t_plus_r_inv_row - data.eval_w_plus_r_inv_row) + + coeffs[1] * (data.eval_t_plus_r_inv_col - data.eval_w_plus_r_inv_col) + + coeffs[2] * (rand_eq_bound * (data.eval_t_plus_r_inv_row * eval_t_plus_r_row - eval_ts_row)) + + coeffs[3] + * (rand_eq_bound * (data.eval_w_plus_r_inv_row * eval_w_plus_r_row - E::Scalar::ONE)) + + coeffs[4] * (rand_eq_bound * (data.eval_t_plus_r_inv_col * eval_t_plus_r_col - eval_ts_col)) + + coeffs[5] + * (rand_eq_bound * (data.eval_w_plus_r_inv_col * eval_w_plus_r_col - E::Scalar::ONE)) +} diff --git a/src/spartan/mem_check_logup_gkr.rs b/src/spartan/mem_check_logup_gkr.rs new file mode 100644 index 000000000..76adcede0 --- /dev/null +++ b/src/spartan/mem_check_logup_gkr.rs @@ -0,0 +1,672 @@ +//! Bridge layer wiring Logup-GKR to ppSNARK's memory-check. +//! +//! This module is the *host* half of the Logup-GKR memory-check. The +//! `logup_gkr` core owns the fractional-sum reduction but no PCS; `ppsnark` owns +//! the commitments and inner sumcheck. This bridge supplies ppSNARK's four +//! equal-height sub-instances and fuses the final GKR layer with ppSNARK's inner +//! sumcheck so both reductions land on one shared evaluation point. +//! +//! The verifier closes soundness by (1) reconstructing each input-layer +//! fraction from the column evaluations claimed at the shared evaluation point, +//! (2) comparing those fractions with the GKR reduction, and (3) checking the +//! two fractional balances. [`MemCheckOpenings`] fixes the claimed columns and +//! the fused inner sumcheck plus batched PCS opening bind those claims to the +//! committed columns at the same point. +//! +//! ## The four sub-instances (why four, not two) +//! ppSNARK's memory-check is two logup relations (`row`, `col`), each a balance +//! `Σ ts/(T+r) = Σ 1/(W+r)`. We encode each relation as **two** height-N +//! fractional-sum sub-instances — a *table* side and an *access* side — so all +//! four share one GKR depth `log N`, as required by the batched GKR verifier; +//! every side is exactly N because ppSNARK pads every memory-check column to N +//! in setup. A single +//! 2N-leaf signed-multiplicity tree would instead emit a `log(2N)` point, which +//! cannot be rerandomized against the N-variable inner sumcheck; the two N-leaf +//! trees for each relation keep the point at `log N`. Instance order is fixed: +//! +//! | idx | name | num | den | +//! |-----|-------------|-----------|-----------------------------| +//! | 0 | row_table | `ts_row` | `mem_row·γ + id + r` | +//! | 1 | row_access | `-1` | `L_row·γ + addr_row + r` | +//! | 2 | col_table | `ts_col` | `mem_col·γ + id + r` | +//! | 3 | col_access | `-1` | `L_col·γ + addr_col + r` | +//! +//! where `id = IdentityPolynomial` (the cell address `i`), `mem_row = +//! eq(r_outer_full, ·)`, `mem_col = z`, `addr_row = row`, `addr_col = col`, and +//! `(γ, r)` are the ppSNARK memory-check fingerprint challenges. +//! +//! ## Balance (the host's `0/den` check) +//! The GKR verifier reduces each sub-instance to a root fraction but does **not** +//! check the relation balances — that is this module's job. Balance is a +//! property of the whole relation, i.e. the *root* fractions (the proof's +//! `initial_claims`, bound to the reduction by the GKR verifier), not the +//! input-layer evaluations. The access side carries `num = -1`, so `root_table + +//! root_access = Σ ts/(T+r) − Σ 1/(W+r)`, which must vanish. In projective form +//! that means the *sum's numerator* is zero (the denominator, a product of +//! nonzero dens, cannot be), checked for the row pair `(0,1)` and the col pair +//! `(2,3)`. + +use crate::errors::NovaError; +use crate::spartan::logup_gkr::fraction::Fraction; +use crate::spartan::logup_gkr::layer::Layer; +use crate::spartan::logup_gkr::proof::LogupGkrPrefixProof; +use crate::spartan::mem_check_logup_gkr_fused::{ + prove_fused, verify_fused, verify_gkr_prefix, FusedEndpointEvals, FusedGkrInnerProof, + FusedInnerInputs, +}; +use crate::spartan::polys::eq::EqPolynomial; +use crate::spartan::polys::identity::IdentityPolynomial; +use crate::spartan::polys::masked_eq::MaskedEqPolynomial; +use crate::spartan::polys::multilinear::MultilinearPolynomial; +use crate::spartan::polys::multilinear::SparsePolynomial; +use crate::traits::Engine; +use ff::Field; +use rayon::prelude::*; +use serde::{Deserialize, Serialize}; + +/// Fixed sub-instance count (`row_table, row_access, col_table, col_access`). +pub const NUM_SUB_INSTANCES: usize = 4; + +/// The column evaluations a prover claims at the GKR +/// [`eval_point`](crate::spartan::logup_gkr::LogupGkrOpeningClaim::eval_point). +/// +/// Every field is one column evaluated at the shared GKR point. The host uses +/// them to reconstruct the four sub-instance fractions. The fused inner +/// sumcheck carries the same point through to the batched PCS opening. The +/// verifier computes `id` and `mem_row = eq(r_outer_full, ·)` directly, so +/// neither needs a claim here. +#[derive(Clone, Copy, Debug)] +pub struct MemCheckOpenings { + /// `L_row(eval_point)` — the row lookup column. + pub eval_L_row: E::Scalar, + /// `L_col(eval_point)` — the col lookup column. + pub eval_L_col: E::Scalar, + /// `row(eval_point)` — the row access-address column (`addr_row`). + pub eval_row: E::Scalar, + /// `col(eval_point)` — the col access-address column (`addr_col`). + pub eval_col: E::Scalar, + /// `ts_row(eval_point)` — the row multiplicity column. + pub eval_ts_row: E::Scalar, + /// `ts_col(eval_point)` — the col multiplicity column. + pub eval_ts_col: E::Scalar, + /// `mem_col(eval_point) = z(eval_point)` — the col table-value column. + /// + /// `mem_row` is `eq(r_outer_full, ·)`, which the verifier evaluates directly, + /// so only `mem_col` needs a claim. + pub eval_mem_col: E::Scalar, +} + +/// The prover's memory-check witness: the raw length-N columns fed into +/// Logup-GKR. +/// +/// These are exactly ppSNARK's padded memory-check columns (all length +/// `N = 2^{log N}`). [`build_input_layers`] +/// turns them into the four GKR input layers, and [`prove_step_fused`] runs the +/// fused last-layer sumcheck over them while claiming the evaluations named by +/// [`MemCheckOpenings`] at the shared point. Field meanings match the +/// four-sub-instance table in the module docs: +/// - `mem_row = eq(r_outer_full, ·)`, `mem_col = z` (table values); +/// - `L_row`/`L_col` the lookup columns, `addr_row = row`/`addr_col = col` the +/// access addresses, `ts_row`/`ts_col` the multiplicities. +/// +/// The columns are borrowed, not owned: [`build_input_layers`] only reads them +/// (deriving fresh fraction vectors), so the caller keeps ownership and pays no +/// per-column clone to assemble this witness. +pub struct MemCheckWitness<'a, E: Engine> { + /// Row table values `mem_row = eq(r_outer_full, ·)`. + pub mem_row: &'a [E::Scalar], + /// Col table values `mem_col = z`. + pub mem_col: &'a [E::Scalar], + /// Row lookup column `L_row`. + pub L_row: &'a [E::Scalar], + /// Col lookup column `L_col`. + pub L_col: &'a [E::Scalar], + /// Row access addresses `addr_row = row`. + pub addr_row: &'a [E::Scalar], + /// Col access addresses `addr_col = col`. + pub addr_col: &'a [E::Scalar], + /// Row multiplicities `ts_row`. + pub ts_row: &'a [E::Scalar], + /// Col multiplicities `ts_col`. + pub ts_col: &'a [E::Scalar], +} + +/// Builds the four GKR input layers `[row_table, row_access, col_table, +/// col_access]` from the raw columns and the fingerprint `(gamma, r)`. +/// +/// This is the prover-side dual of the verifier's per-instance reconstruction +/// in `reconcile_and_balance`: it must produce, for every leaf `i`, exactly +/// the fractions the verifier recomputes at `eval_point`. The layers, in order (matching the +/// module-doc table and [`NUM_SUB_INSTANCES`]): +/// +/// | idx | name | num | den | +/// |-----|-------------|------------|-----------------------------| +/// | 0 | row_table | `ts_row` | `mem_row·γ + id + r` | +/// | 1 | row_access | `-1` | `L_row·γ + addr_row + r` | +/// | 2 | col_table | `ts_col` | `mem_col·γ + id + r` | +/// | 3 | col_access | `-1` | `L_col·γ + addr_col + r` | +/// +/// `id[i] = i` is the cell address. All columns must share one length `N`, a +/// power of two (`debug_assert`ed); the returned layers each have `log N` +/// variables, the shared GKR depth. +pub fn build_input_layers( + cols: &MemCheckWitness<'_, E>, + gamma: E::Scalar, + r: E::Scalar, +) -> Vec> { + let n = cols.mem_row.len(); + debug_assert!( + n.is_power_of_two() && n >= 2, + "N must be a power of two >= 2" + ); + for col in [ + &cols.mem_col, + &cols.L_row, + &cols.L_col, + &cols.addr_row, + &cols.addr_col, + &cols.ts_row, + &cols.ts_col, + ] { + debug_assert_eq!(col.len(), n, "all memory-check columns must share length N"); + } + + let neg_one = -E::Scalar::ONE; + // Table-side den: mem·γ + id + r, where id[i] = i (the cell address). + // + // `id[i]` is built by per-chunk accumulation instead of `Scalar::from(i)` per + // element: each chunk pays ONE `from` for its base index, then walks its cells + // with a field `+ ONE`, which is far cheaper than a u64→Montgomery conversion. + // The chunks run in parallel (`par_chunks_mut`), so this keeps full width + // while dropping N `from`s to `N / chunk_size`. + let one = E::Scalar::ONE; + let chunk_size = 1 + n / rayon::current_num_threads().max(1); + let den_table = |mem: &[E::Scalar]| -> Vec { + let mut out = vec![E::Scalar::ZERO; n]; + out + .par_chunks_mut(chunk_size) + .enumerate() + .for_each(|(c, chunk)| { + let mut id = E::Scalar::from((c * chunk_size) as u64); // base index of this chunk + for (out_i, mem_i) in chunk.iter_mut().zip(&mem[c * chunk_size..]) { + *out_i = *mem_i * gamma + id + r; + id += one; + } + }); + out + }; + // Access-side den: L·γ + addr + r. + let den_access = |l: &[E::Scalar], addr: &[E::Scalar]| -> Vec { + (0..n) + .into_par_iter() + .map(|i| l[i] * gamma + addr[i] + r) + .collect() + }; + let mle = |v: Vec| MultilinearPolynomial::new(v); + + vec![ + // idx 0: row_table + Layer:: { + num: mle(cols.ts_row.to_vec()), + den: mle(den_table(cols.mem_row)), + }, + // idx 1: row_access + Layer:: { + num: mle(vec![neg_one; n]), + den: mle(den_access(cols.L_row, cols.addr_row)), + }, + // idx 2: col_table + Layer:: { + num: mle(cols.ts_col.to_vec()), + den: mle(den_table(cols.mem_col)), + }, + // idx 3: col_access + Layer:: { + num: mle(vec![neg_one; n]), + den: mle(den_access(cols.L_col, cols.addr_col)), + }, + ] +} + +/// Reconciles the four input-layer fractions reconstructed from the claimed +/// columns at `eval_point` against the GKR-reduced `reduced` fractions +/// (component-wise, exact), then checks the two relation balances on the `roots` +/// with an explicit denominator-nonzero guard. Shared by the standalone +/// ppSNARK fused path (PLAN section 6.2). +pub(crate) fn reconcile_and_balance( + reduced: &[Fraction], + roots: &[Fraction], + eval_point: &[E::Scalar], + gamma: E::Scalar, + r: E::Scalar, + r_outer_full: &[E::Scalar], + openings: &MemCheckOpenings, +) -> Result<(), NovaError> { + if reduced.len() != NUM_SUB_INSTANCES { + return Err(NovaError::InvalidNumInstances); + } + // Bind GKR depth to the trusted `log N`; otherwise `EqPolynomial::evaluate` + // would panic on a forged depth rather than return `NovaError`. + if eval_point.len() != r_outer_full.len() { + return Err(NovaError::InvalidSumcheckProof); + } + + // (2) Recompute the four input-layer fractions from the claimed columns. + let eval_id = IdentityPolynomial::::new(eval_point.len()).evaluate(eval_point); + let eval_mem_row = EqPolynomial::new(r_outer_full.to_vec()).evaluate(eval_point); + let neg_one = -E::Scalar::ONE; + + let row_table = Fraction::new(openings.eval_ts_row, eval_mem_row * gamma + eval_id + r); + let row_access = Fraction::new(neg_one, openings.eval_L_row * gamma + openings.eval_row + r); + let col_table = Fraction::new( + openings.eval_ts_col, + openings.eval_mem_col * gamma + eval_id + r, + ); + let col_access = Fraction::new(neg_one, openings.eval_L_col * gamma + openings.eval_col + r); + let recomputed = [row_table, row_access, col_table, col_access]; + + // Each recomputed fraction must match the GKR-reduced claim component-wise. + for (rc, red) in recomputed.iter().zip(reduced.iter()) { + if rc.num != red.num || rc.den != red.den { + return Err(NovaError::InvalidSumcheckProof); + } + } + + // (3) Balance on the root fractions (the whole-relation sums). + let [row_table_root, row_access_root, col_table_root, col_access_root] = roots[..] else { + return Err(NovaError::InvalidNumInstances); + }; + let all_dens_nonzero = [ + row_table_root, + row_access_root, + col_table_root, + col_access_root, + ] + .iter() + .all(|f| f.den != E::Scalar::ZERO); + if !all_dens_nonzero { + return Err(NovaError::InvalidSumcheckProof); + } + let row_balanced = (row_table_root + row_access_root).num == E::Scalar::ZERO; + let col_balanced = (col_table_root + col_access_root).num == E::Scalar::ZERO; + if !row_balanced || !col_balanced { + return Err(NovaError::InvalidSumcheckProof); + } + Ok(()) +} + +/// The fused memory-check proof carried in the ppSNARK proof on the default +/// path: the GKR prefix plus the fused last-layer + Inner sumcheck proof. GKR +/// and Inner now land on one shared `r_shared`. +#[derive(Clone, Debug, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct FusedMemCheckProof { + /// The GKR prefix (every layer reduction except the last). + pub prefix: LogupGkrPrefixProof, + /// The fused GKR-last-layer + Inner sumcheck proof. + pub fused: FusedGkrInnerProof, +} + +/// Fused-path prover: build the four GKR input layers, run the prefix, then the +/// fused last-layer + Inner sumcheck. Returns the proof, `r_shared`, and the +/// Inner endpoint evaluations for the host's PCS opening. +pub fn prove_step_fused( + witness: MemCheckWitness<'_, E>, + gamma: E::Scalar, + r: E::Scalar, + inner: FusedInnerInputs, + transcript: &mut E::TE, +) -> Result<(FusedMemCheckProof, Vec, FusedEndpointEvals), NovaError> { + let layers = build_input_layers(&witness, gamma, r); + let prefix = crate::spartan::logup_gkr::prover::prove_prefix::(layers, transcript)?; + let prefix_proof = LogupGkrPrefixProof { + initial_claims: prefix.initial_claims.clone(), + prefix_final_claims: prefix.final_claims_by_layer.clone(), + prefix_sumchecks: prefix.sumchecks.clone(), + }; + let (fused, r_shared, endpoints) = prove_fused::(prefix, inner, transcript)?; + Ok(( + FusedMemCheckProof { + prefix: prefix_proof, + fused, + }, + r_shared, + endpoints, + )) +} + +/// Read-only context for the fused verifier: the memory-check fingerprint, the +/// outer evaluation point, the public IO, and the trusted padding/masking +/// dimensions. Every field is derived from the verifier key or already-bound +/// transcript values, never from the proof. +pub struct FusedVerifyContext<'a, E: Engine> { + /// Memory-check fingerprint challenge `gamma`. + pub gamma: E::Scalar, + /// Memory-check fingerprint challenge `r`. + pub r: E::Scalar, + /// The extended outer point `q = r_outer_full` (length `log N`). + pub r_outer_full: &'a [E::Scalar], + /// Public IO `[u, X...]`, used to reconstruct `mem_col`. + pub public_io: &'a [E::Scalar], + /// `log2(num_vars)` for the masked-eq witness factor. + pub num_masked_vars: usize, + /// `log2(N)` — the trusted inner-sumcheck length. + pub snark_n_log: usize, + /// `log2(2·num_vars)` — the unpadded public-IO boundary. + pub two_num_vars_log: usize, +} + +/// The Inner-relation initial claims (PLAN section 5) folded into the fused +/// sumcheck. +pub struct FusedInnerClaims { + /// `C_A = factor·(eval_Az + c·eval_Bz + c²·eval_Cz)`. + pub abc: E::Scalar, + /// `C_E = factor·eval_E_at_r_outer`. + pub e: E::Scalar, + /// `C_W` — the witness-bound relation claim (zero in ppSNARK). + pub w: E::Scalar, +} + +/// The column evaluations claimed at `r_shared`, checked by the fused Inner +/// endpoint (PLAN section 6.1) and the GKR reconcile (section 6.2), and bound to +/// the committed columns by the batched PCS opening. `W` doubles as the value +/// used to reconstruct `mem_col`. +#[allow(non_snake_case)] +pub struct FusedEndpointClaims { + /// `val(r_shared) = val_A + c·val_B + c²·val_C`. + pub val: E::Scalar, + /// `E(r_shared)`. + pub E: E::Scalar, + /// `W(r_shared)` — also reconstructs `mem_col`. + pub W: E::Scalar, + /// `L_row(r_shared)`. + pub L_row: E::Scalar, + /// `L_col(r_shared)`. + pub L_col: E::Scalar, + /// `row(r_shared)` — the row access address. + pub row: E::Scalar, + /// `col(r_shared)` — the col access address. + pub col: E::Scalar, + /// `ts_row(r_shared)`. + pub ts_row: E::Scalar, + /// `ts_col(r_shared)`. + pub ts_col: E::Scalar, +} + +/// Fused-path verifier: replay the prefix, verify the fused sumcheck, check the +/// Inner endpoint `h(f) == inner_expected` independently, then reconcile the four +/// input-layer fractions and check balance (PLAN section 6). Returns `r_shared`. +/// +/// `endpoints` are the column evaluations at `r_shared`; `mem_col` is +/// reconstructed internally from `endpoints.W` and the public IO once the fused +/// verifier has derived `r_shared`. +pub fn verify_step_fused( + proof: &FusedMemCheckProof, + ctx: &FusedVerifyContext<'_, E>, + claims: &FusedInnerClaims, + endpoints: &FusedEndpointClaims, + transcript: &mut E::TE, +) -> Result, NovaError> { + let prefix_state = verify_gkr_prefix::( + proof.prefix.initial_claims.clone(), + proof.prefix.prefix_final_claims.clone(), + proof.prefix.prefix_sumchecks.clone(), + transcript, + )?; + let out = verify_fused::( + &proof.fused, + prefix_state, + claims.abc, + claims.e, + claims.w, + transcript, + )?; + let r_shared = out.r_shared; + + // Bind the GKR depth to the trusted inner-sumcheck length before any + // `EqPolynomial`/`MaskedEqPolynomial::evaluate` below: a forged proof whose + // GKR depth differs from `log N` yields an `r_shared` of the wrong length, + // and those evaluators `assert_eq!` on the point length (would panic instead + // of returning `Err`). `reconcile_and_balance` re-checks this, but only after + // the Inner endpoint evaluations, so the guard must lead here. + if r_shared.len() != ctx.r_outer_full.len() { + return Err(NovaError::InvalidSumcheckProof); + } + + // Inner endpoint (checked independently of the GKR reconcile, PLAN section 6.1): + // h(f) == beta·L_row·L_col·val + beta^2·eq(q,r_shared)·E + beta^3·masked·W + let eq_r_outer = EqPolynomial::new(ctx.r_outer_full.to_vec()); + let eq_q_at_r = eq_r_outer.evaluate(&r_shared); + let masked = MaskedEqPolynomial::new(&eq_r_outer, ctx.num_masked_vars).evaluate(&r_shared); + let beta = out.beta; + let beta2 = beta * beta; + let beta3 = beta2 * beta; + let inner_expected = beta * endpoints.L_row * endpoints.L_col * endpoints.val + + beta2 * eq_q_at_r * endpoints.E + + beta3 * masked * endpoints.W; + if out.e_inner != inner_expected { + return Err(NovaError::InvalidSumcheckProof); + } + + let l = ctx + .snark_n_log + .checked_sub(ctx.two_num_vars_log) + .ok_or(NovaError::InvalidSumcheckProof)?; + if l >= r_shared.len() { + return Err(NovaError::InvalidSumcheckProof); + } + let mut mc_factor = E::Scalar::ONE; + for r_p in r_shared.iter().take(l) { + mc_factor *= E::Scalar::ONE - *r_p; + } + let r_unpad = r_shared[l..].to_vec(); + let eval_X = { + let poly_X = SparsePolynomial::new(r_unpad.len() - 1, ctx.public_io.to_vec()); + poly_X.evaluate(&r_unpad[1..]) + }; + let eval_mem_col = endpoints.W + mc_factor * r_unpad[0] * eval_X; + let openings = MemCheckOpenings:: { + eval_L_row: endpoints.L_row, + eval_L_col: endpoints.L_col, + eval_row: endpoints.row, + eval_col: endpoints.col, + eval_ts_row: endpoints.ts_row, + eval_ts_col: endpoints.ts_col, + eval_mem_col, + }; + + // GKR reconcile + balance at r_shared (checked separately from the endpoint). + reconcile_and_balance::( + &out.gkr_fractions, + &proof.prefix.initial_claims, + &r_shared, + ctx.gamma, + ctx.r, + ctx.r_outer_full, + &openings, + )?; + + Ok(r_shared) +} + +#[cfg(all(test, not(feature = "logup-no-gkr")))] +mod tests { + use super::*; + use crate::spartan::logup_gkr::proof::{LayerFinalClaim, LogupGkrPrefixProof}; + use crate::spartan::mem_check_logup_gkr_fused::FusedGkrInnerProof; + use crate::spartan::polys::univariate::UniPoly; + use crate::traits::{Engine, TranscriptEngineTrait}; + + type E = crate::provider::Bn256EngineKZG; + type Fr = ::Scalar; + + // Regression for the deleted `rejects_wrong_gkr_depth`: a proof whose GKR depth + // (here `n = 1`) differs from the trusted `log N` must be rejected with `Err`, + // NOT panic inside `EqPolynomial::evaluate` (whose `assert_eq!` on the point + // length would otherwise fire before `reconcile_and_balance`'s own guard). + #[test] + fn verify_step_fused_rejects_wrong_gkr_depth() { + let zero = Fr::ZERO; + let root = Fraction::new(zero, Fr::ONE); + // `(0,1)+(0,1)` gates to `(0,1)`, so the `n = 1` root check passes and + // `verify_fused` returns an `r_shared` of length 1. + let split = LayerFinalClaim { + left: root, + right: root, + }; + let proof = FusedMemCheckProof { + prefix: LogupGkrPrefixProof { + initial_claims: vec![root; NUM_SUB_INSTANCES], + prefix_final_claims: vec![], + prefix_sumchecks: vec![], + }, + fused: FusedGkrInnerProof { + suffix_round_polys: vec![], + input_splits: [split; NUM_SUB_INSTANCES], + msb_round_poly: UniPoly::from_evals_deg3(&[zero, zero, zero, zero]).compress(), + }, + }; + // Trusted `log N = 2` (so `r_outer_full` has length 2) while the forged proof + // reduces to depth 1. + let mut transcript = ::TE::new(b"depth-regression"); + let ctx = FusedVerifyContext:: { + gamma: zero, + r: zero, + r_outer_full: &[zero, zero], + public_io: &[zero], + num_masked_vars: 1, + snark_n_log: 2, + two_num_vars_log: 1, + }; + let claims = FusedInnerClaims:: { + abc: zero, + e: zero, + w: zero, + }; + let endpoints = FusedEndpointClaims:: { + val: zero, + E: zero, + W: zero, + L_row: zero, + L_col: zero, + row: zero, + col: zero, + ts_row: zero, + ts_col: zero, + }; + let verdict = verify_step_fused::(&proof, &ctx, &claims, &endpoints, &mut transcript); + assert!( + matches!(verdict, Err(NovaError::InvalidSumcheckProof)), + "forged GKR depth must be rejected with Err, not panic" + ); + } + + // Recomputes the four input-layer fractions from the claimed columns exactly as + // `reconcile_and_balance` does internally, so a test can build a self-consistent + // "honest" `reduced` set and then perturb `roots` to exercise each guard. + fn recompute( + o: &MemCheckOpenings, + eval_point: &[Fr], + r_outer_full: &[Fr], + gamma: Fr, + r: Fr, + ) -> [Fraction; NUM_SUB_INSTANCES] { + let eval_id = IdentityPolynomial::::new(eval_point.len()).evaluate(eval_point); + let eval_mem_row = EqPolynomial::new(r_outer_full.to_vec()).evaluate(eval_point); + let neg_one = -Fr::ONE; + [ + Fraction::new(o.eval_ts_row, eval_mem_row * gamma + eval_id + r), + Fraction::new(neg_one, o.eval_L_row * gamma + o.eval_row + r), + Fraction::new(o.eval_ts_col, o.eval_mem_col * gamma + eval_id + r), + Fraction::new(neg_one, o.eval_L_col * gamma + o.eval_col + r), + ] + } + + fn reconcile_fixture() -> (MemCheckOpenings, Vec, Vec, Fr, Fr) { + let openings = MemCheckOpenings:: { + eval_L_row: Fr::from(3), + eval_L_col: Fr::from(6), + eval_row: Fr::from(1), + eval_col: Fr::from(2), + eval_ts_row: Fr::from(2), + eval_ts_col: Fr::from(5), + eval_mem_col: Fr::from(9), + }; + ( + openings, + vec![Fr::from(3), Fr::from(5)], // eval_point (log N = 2) + vec![Fr::from(7), Fr::from(2)], // r_outer_full (same length) + Fr::from(11), // gamma + Fr::from(4), // r + ) + } + + // Balanced roots: `(1,1)+(-1,1)` has numerator `0` per relation, dens nonzero. + fn balanced_roots() -> [Fraction; NUM_SUB_INSTANCES] { + let one = Fraction::new(Fr::ONE, Fr::ONE); + let neg = Fraction::new(-Fr::ONE, Fr::ONE); + [one, neg, one, neg] + } + + #[test] + fn reconcile_accepts_consistent_and_balanced() { + let (o, eval_point, r_outer_full, gamma, r) = reconcile_fixture(); + let reduced = recompute(&o, &eval_point, &r_outer_full, gamma, r); + assert!(reconcile_and_balance::( + &reduced, + &balanced_roots(), + &eval_point, + gamma, + r, + &r_outer_full, + &o, + ) + .is_ok()); + } + + #[test] + fn reconcile_rejects_mismatched_column() { + let (o, eval_point, r_outer_full, gamma, r) = reconcile_fixture(); + let mut reduced = recompute(&o, &eval_point, &r_outer_full, gamma, r); + reduced[0].num += Fr::ONE; // GKR-reduced fraction disagrees with the column claim + assert!(reconcile_and_balance::( + &reduced, + &balanced_roots(), + &eval_point, + gamma, + r, + &r_outer_full, + &o, + ) + .is_err()); + } + + #[test] + fn reconcile_rejects_unbalanced_roots() { + let (o, eval_point, r_outer_full, gamma, r) = reconcile_fixture(); + let reduced = recompute(&o, &eval_point, &r_outer_full, gamma, r); + // Reconcile passes, but the row pair no longer sums to zero: `(1,1)+(1,1)`. + let one = Fraction::new(Fr::ONE, Fr::ONE); + let neg = Fraction::new(-Fr::ONE, Fr::ONE); + let roots = [one, one, one, neg]; + assert!( + reconcile_and_balance::(&reduced, &roots, &eval_point, gamma, r, &r_outer_full, &o,) + .is_err() + ); + } + + #[test] + fn reconcile_rejects_zero_root_denominator() { + let (o, eval_point, r_outer_full, gamma, r) = reconcile_fixture(); + let reduced = recompute(&o, &eval_point, &r_outer_full, gamma, r); + // A `0/0` root would make the `num == 0` balance vacuously pass, so the + // explicit den != 0 guard must reject it first. + let zero_zero = Fraction::new(Fr::ZERO, Fr::ZERO); + let neg = Fraction::new(-Fr::ONE, Fr::ONE); + let roots = [zero_zero, neg, Fraction::new(Fr::ONE, Fr::ONE), neg]; + assert!( + reconcile_and_balance::(&reduced, &roots, &eval_point, gamma, r, &r_outer_full, &o,) + .is_err() + ); + } +} diff --git a/src/spartan/mem_check_logup_gkr_fused.rs b/src/spartan/mem_check_logup_gkr_fused.rs new file mode 100644 index 000000000..6bddbe177 --- /dev/null +++ b/src/spartan/mem_check_logup_gkr_fused.rs @@ -0,0 +1,1109 @@ +//! Fused Logup-GKR last layer + ppSNARK Inner sumcheck. +//! +//! The default ppSNARK memory-check runs the full Logup-GKR argument to an +//! independent `gkr_eval_point`, then a seven-column rerandomize sumcheck carries +//! the reconcile columns from that point into the inner sumcheck's +//! `r_inner_batched`. Both are `O(N)` opening-point reductions of the same +//! length. This module fuses them: the GKR argument runs only to its input layer +//! (the prefix, see `super::logup_gkr::prover::prove_prefix`), and its **last +//! layer** shares the `n-1` suffix rounds and the final MSB fold `f` with the +//! Inner sumcheck's three relations, landing both on one shared point +//! `r_shared = f || s`. No seven-column rerandomize; a single PCS opening. +//! +//! ## The four fused relations +//! A fresh `beta` (sampled after the four initial claims are bound) batches: +//! - `G`: the GKR last layer over four fraction sub-instances (row/col × +//! table/access), internally batched by `lambda_last` powers (degree 3, carries +//! the `eq(tau, ·)` factor); +//! - `A`: the ABC relation `Σ L_row·L_col·val` (degree 3); +//! - `E`: the error relation `Σ eq(q, y)·E(y)` with `q = r_outer_full` (degree 2); +//! - `W`: the witness relation `Σ masked_eq·W` (degree 2). +//! +//! `C_0 = C_G + beta·C_A + beta^2·C_E + beta^3·C_W`. Each suffix round sends one +//! fused cubic. After `n-1` rounds the running claim is `e_suffix`; the boundary +//! subtracts the GKR fold endpoint `G_end` (computed by the verifier from the +//! absorbed input splits) so the Inner MSB polynomial `h` satisfies +//! `h(0)+h(1) = e_suffix - G_end`. A single fold `f` closes both protocols. +//! +//! ## Soundness boundary (PLAN section 18) +//! `G_end` is recomputed by the verifier from the split claims (never absorbed +//! from the prover); the Inner endpoint (`h(f) == inner_expected`) and the GKR +//! reconcile are checked **separately** by the host; the splits and full `h` are +//! absorbed strictly before `f`; `beta != lambda_last` and is sampled after the +//! initial claims are bound. + +use crate::errors::NovaError; +use crate::spartan::logup_gkr::fraction::Fraction; +use crate::spartan::logup_gkr::proof::LayerFinalClaim; +use crate::spartan::logup_gkr::prover::GkrProverPrefix; +use crate::spartan::logup_gkr::verifier::GkrVerifierPrefix; +use crate::spartan::polys::eq::EqPolynomial; +use crate::spartan::polys::multilinear::MultilinearPolynomial; +use crate::spartan::polys::univariate::{CompressedUniPoly, UniPoly}; +use crate::spartan::sumcheck::eq_sumcheck::EqSumCheckInstance; +use crate::spartan::sumcheck::SumcheckProof; +use crate::traits::{Engine, TranscriptEngineTrait}; +use ff::Field; +use rayon::prelude::*; +use serde::{Deserialize, Serialize}; + +/// The protocol's Fiat-Shamir transcript labels. Narrow, fusion-specific labels +/// (PLAN section 7) so a future refactor cannot silently reorder the phases. +pub mod spec { + /// Last-layer batching challenge `lambda_last` (8-component GKR gate RLC). + pub const LAST_LAYER_LAMBDA: &[u8] = b"fll"; + /// Numerator label when absorbing an initial or split fraction. + pub const NUM: &[u8] = b"fn"; + /// Denominator label when absorbing an initial or split fraction. + pub const DEN: &[u8] = b"fd"; + /// Cross-protocol batching challenge `beta`. + pub const BATCH_BETA: &[u8] = b"fbe"; + /// Fused suffix round polynomial. + pub const ROUND_POLY: &[u8] = b"fp"; + /// Fused suffix round challenge. + pub const ROUND_CHALLENGE: &[u8] = b"fc"; + /// Inner MSB (boundary) polynomial `h`. + pub const MSB_POLY: &[u8] = b"fmp"; + /// Shared MSB fold challenge `f`. + pub const SHARED_FOLD: &[u8] = b"fmf"; + /// Degree bound of every fused round polynomial (`eq`·gate / product = 3). + pub const FUSED_DEGREE: usize = 3; + /// Number of GKR fraction sub-instances (row/col × table/access). + pub const NUM_GKR_INSTANCES: usize = 4; +} + +/// A single fused GKR-last-layer + Inner-sumcheck proof. +/// +/// `suffix_round_polys` holds the `n-1` shared suffix rounds; `input_splits` +/// holds the four GKR input-layer split claims (fixed length 4); `msb_round_poly` +/// is the single Inner MSB polynomial `h`, decompressed by the verifier with the +/// boundary hint `e_suffix - G_end`. For `n = 1` there are no suffix rounds and +/// `input_splits` are the root reduction's two-cell children. +#[derive(Clone, Debug, Serialize, Deserialize)] +#[serde(bound = "")] +pub struct FusedGkrInnerProof { + /// The `n-1` shared suffix round polynomials (compressed cubics). + pub suffix_round_polys: Vec>, + /// The four GKR input-layer split claims, instance order + /// `[row_table, row_access, col_table, col_access]`. + pub input_splits: [LayerFinalClaim; 4], + /// The Inner MSB (boundary) polynomial `h`, compressed. + pub msb_round_poly: CompressedUniPoly, +} + +/// Prover inputs for the three Inner relations, plus their initial claims. +/// +/// All `Vec`s have length `N = 2^n`. `val = val_A + c·val_B + c^2·val_C` and +/// `masked_eq` are pre-combined by the caller; `q = r_outer_full` has length `n`. +pub struct FusedInnerInputs { + /// Lookup polynomial `L_row`. + #[allow(non_snake_case)] + pub L_row: Vec, + /// Lookup polynomial `L_col`. + #[allow(non_snake_case)] + pub L_col: Vec, + /// Combined value polynomial `val_A + c·val_B + c^2·val_C`. + pub val: Vec, + /// Error polynomial `E`. + #[allow(non_snake_case)] + pub E: Vec, + /// Masked-eq polynomial for the witness-bound relation. + pub masked_eq: Vec, + /// Witness polynomial `W`. + #[allow(non_snake_case)] + pub W: Vec, + /// The point `q = r_outer_full` (length `n`) of the `E` relation. + pub q: Vec, + /// Initial claim `C_A = Σ L_row·L_col·val`. + pub claim_abc: E::Scalar, + /// Initial claim `C_E = Σ eq(q, y)·E(y)`. + pub claim_e: E::Scalar, + /// Initial claim `C_W = Σ masked_eq·W`. + pub claim_w: E::Scalar, +} + +/// The Inner MLE evaluations at `r_shared`, produced by the prover for the host's +/// endpoint check and PCS opening. +pub struct FusedEndpointEvals { + /// `L_row(r_shared)`. + #[allow(non_snake_case)] + pub L_row: E::Scalar, + /// `L_col(r_shared)`. + #[allow(non_snake_case)] + pub L_col: E::Scalar, + /// `val(r_shared)`. + pub val: E::Scalar, + /// `E(r_shared)`. + #[allow(non_snake_case)] + pub E: E::Scalar, + /// `masked_eq(r_shared)`. + pub masked_eq: E::Scalar, + /// `W(r_shared)`. + #[allow(non_snake_case)] + pub W: E::Scalar, + /// `ts_row(r_shared)` — the row_table numerator, read for free from the folded + /// GKR split (no separate opening needed). + pub ts_row: E::Scalar, + /// `ts_col(r_shared)` — the col_table numerator, read for free from the folded + /// GKR split. + pub ts_col: E::Scalar, +} + +/// The fused verifier's output: the shared point, the Inner endpoint value, the +/// batching challenge, and the four reduced GKR input-layer fractions. +pub(crate) struct FusedVerifierOutput { + /// The shared evaluation point `r_shared = f || s` (length `n`). + pub r_shared: Vec, + /// The Inner endpoint value `h(f)`, to be checked against `inner_expected`. + pub e_inner: E::Scalar, + /// The cross-protocol batching challenge `beta` (the host needs it to build + /// `inner_expected`). + pub beta: E::Scalar, + /// The four reduced input-layer fractions in instance order, for the host's + /// component-wise reconcile. + pub gkr_fractions: [Fraction; 4], +} + +/// Absorbs a fraction `(num, den)` into the transcript. +fn absorb_fraction(transcript: &mut E::TE, frac: Fraction) { + transcript.absorb(spec::NUM, &frac.num); + transcript.absorb(spec::DEN, &frac.den); +} + +/// The eight `lambda_last` weights `(a_i, b_i) = (lambda^{2i}, lambda^{2i+1})`. +fn gate_weights(lambda: E::Scalar) -> [(E::Scalar, E::Scalar); 4] { + let mut a = E::Scalar::ONE; + core::array::from_fn(|_| { + let b = a * lambda; + let pair = (a, b); + a = b * lambda; + pair + }) +} + +/// The GKR fold endpoint `G_end = eq(tau, s) · Σ_i [a_i·(nL·dR + nR·dL) + b_i·dL·dR]` +/// reconstructed from the four input splits (verifier recomputes; never absorbed). +fn gkr_endpoint( + splits: &[LayerFinalClaim; 4], + weights: &[(E::Scalar, E::Scalar); 4], + eq_tau_s: E::Scalar, +) -> E::Scalar { + let mut acc = E::Scalar::ZERO; + for (split, (a, b)) in splits.iter().zip(weights.iter()) { + let (nl, dl) = (split.left.num, split.left.den); + let (nr, dr) = (split.right.num, split.right.den); + acc += *a * (nl * dr + nr * dl) + *b * (dl * dr); + } + eq_tau_s * acc +} + +/// Splits an owned `N`-length column into its MSB halves `(P_0, P_1)` where +/// `P_0(x) = P(0, x)` (indices `0..N/2`) and `P_1(x) = P(1, x)` (indices +/// `N/2..N`). Consumes the vector: the low half stays in place and only the high +/// half is a fresh allocation (`split_off`), halving the split copy cost. +fn split_msb( + mut v: Vec, +) -> (MultilinearPolynomial, MultilinearPolynomial) { + let n = v.len() / 2; + let hi = v.split_off(n); + ( + MultilinearPolynomial::new(v), + MultilinearPolynomial::new(hi), + ) +} + +/// The six Inner MLE `(low, high)` endpoint pairs at the current suffix point +/// `s` — i.e. `(P(0, s), P(1, s))` per column — that the shared MSB fold `f` +/// closes into one evaluation each. +#[allow(non_snake_case)] +struct InnerMsbPairs { + L_row: (F, F), + L_col: (F, F), + val: (F, F), + E: (F, F), + masked: (F, F), + W: (F, F), +} + +/// Closes the fused protocol's shared MSB round, the single place the boundary +/// algebra and its transcript order live (both the `n ≥ 2` and `n = 1` provers +/// call it). It: +/// 1. absorbs the four GKR input splits; +/// 2. builds the Inner boundary polynomial `h` (whose `h(0)+h(1)` must equal +/// `h_sum = e_suffix − G_end`) and absorbs it; +/// 3. squeezes the shared fold `f`; +/// 4. folds every Inner pair and the two table-side split numerators +/// (instances 0, 2) to their endpoint evaluation at `f`. +/// +/// `eq_qsuf_s` is `eq(q_suffix, s)`, which is `ONE` when there is no suffix +/// (`n = 1`), so the single closure covers both depths. Returns the compressed +/// `h`, the fold `f`, and the endpoint evaluations. +#[allow(non_snake_case)] +#[allow(clippy::too_many_arguments)] +fn close_inner_msb( + pairs: &InnerMsbPairs, + q_0: E::Scalar, + eq_qsuf_s: E::Scalar, + beta: E::Scalar, + beta2: E::Scalar, + beta3: E::Scalar, + h_sum: E::Scalar, + input_splits: &[LayerFinalClaim; spec::NUM_GKR_INSTANCES], + transcript: &mut E::TE, +) -> Result< + ( + CompressedUniPoly, + E::Scalar, + FusedEndpointEvals, + ), + NovaError, +> { + let one = E::Scalar::ONE; + for sp in input_splits { + absorb_fraction::(transcript, sp.left); + absorb_fraction::(transcript, sp.right); + } + + // h(X) = beta·h_A + beta^2·h_E + beta^3·h_W, each factor linearly interpolated + // between the pair's low and high halves at X. + let h_at = |x: E::Scalar| -> E::Scalar { + let bar = |p: (E::Scalar, E::Scalar)| (one - x) * p.0 + x * p.1; + let ha = bar(pairs.L_row) * bar(pairs.L_col) * bar(pairs.val); + let eq_q0_x = (one - q_0) * (one - x) + q_0 * x; + let he = eq_qsuf_s * eq_q0_x * bar(pairs.E); + let hw = bar(pairs.masked) * bar(pairs.W); + beta * ha + beta2 * he + beta3 * hw + }; + let two = one + one; + let three = two + one; + let h_poly = UniPoly::from_evals(&[h_at(E::Scalar::ZERO), h_at(one), h_at(two), h_at(three)]); + debug_assert_eq!( + h_poly.eval_at_zero() + h_poly.eval_at_one(), + h_sum, + "h(0)+h(1) must equal e_suffix - G_end" + ); + + transcript.absorb(spec::MSB_POLY, &h_poly); + let f = transcript.squeeze(spec::SHARED_FOLD)?; + + let barf = |p: (E::Scalar, E::Scalar)| (one - f) * p.0 + f * p.1; + let endpoints = FusedEndpointEvals { + L_row: barf(pairs.L_row), + L_col: barf(pairs.L_col), + val: barf(pairs.val), + E: barf(pairs.E), + masked_eq: barf(pairs.masked), + W: barf(pairs.W), + // ts_row / ts_col are the row_table / col_table numerators (instances 0, 2), + // read for free from the folded splits at f — no separate opening. + ts_row: barf((input_splits[0].left.num, input_splits[0].right.num)), + ts_col: barf((input_splits[2].left.num, input_splits[2].right.num)), + }; + Ok((h_poly.compress(), f, endpoints)) +} + +/// Proves the fused GKR-last-layer + Inner argument, returning the proof, the +/// shared point `r_shared`, and the Inner endpoint evaluations for the host. +/// +/// `gkr_prefix` is the state from [`super::logup_gkr::prover::prove_prefix`] over +/// the four fraction sub-instances; `inner` supplies the three Inner relations. +/// The prover must have already bound `gkr_prefix`'s prefix into the transcript. +#[allow(non_snake_case)] +pub(crate) fn prove_fused( + gkr_prefix: GkrProverPrefix, + inner: FusedInnerInputs, + transcript: &mut E::TE, +) -> Result<(FusedGkrInnerProof, Vec, FusedEndpointEvals), NovaError> { + assert_eq!( + gkr_prefix.m, + spec::NUM_GKR_INSTANCES, + "fused GKR needs 4 instances" + ); + let n = gkr_prefix.num_vars; + + if n == 1 { + return prove_fused_base(gkr_prefix, inner, transcript); + } + + let GkrProverPrefix { + running, + eval_point: tau, + input_layers, + final_claims_by_layer, + .. + } = gkr_prefix; + debug_assert_eq!(tau.len(), n - 1); + + // 1. lambda_last and the batched last-layer initial claim C_G. + let lambda_last = transcript.squeeze(spec::LAST_LAYER_LAMBDA)?; + let weights = gate_weights::(lambda_last); + let c_g: E::Scalar = running + .iter() + .zip(weights.iter()) + .map(|((num, den), (a, b))| *a * *num + *b * *den) + .sum(); + + // 2. Split every column into MSB halves. Each split is a fresh hi-half + // allocation + copy (page-fault bound), so the 8 GKR splits and 6 Inner + // splits run concurrently to overlap those copies across cores. + type Half = MultilinearPolynomial<::Scalar>; + type Quad = (Half, Half, Half, Half); + let (gkr_halves, inner_halves): (Vec>, Vec<(Half, Half)>) = rayon::join( + || { + input_layers + .into_par_iter() + .map(|layer| { + let (num_lo, num_hi) = split_msb(layer.num.Z); + let (den_lo, den_hi) = split_msb(layer.den.Z); + (num_lo, num_hi, den_lo, den_hi) + }) + .collect() + }, + || { + vec![ + inner.L_row, + inner.L_col, + inner.val, + inner.E, + inner.masked_eq, + inner.W, + ] + .into_par_iter() + .map(split_msb) + .collect() + }, + ); + + let mut nl = Vec::with_capacity(4); + let mut nr = Vec::with_capacity(4); + let mut dl = Vec::with_capacity(4); + let mut dr = Vec::with_capacity(4); + for (num_lo, num_hi, den_lo, den_hi) in gkr_halves { + nl.push(num_lo); + nr.push(num_hi); + dl.push(den_lo); + dr.push(den_hi); + } + + // Consume the inner halves in the `vec![]` order above (L_row, L_col, val, E, + // masked, W); each entry is `(low_half, high_half)`. + let mut inner_iter = inner_halves.into_iter(); + let (mut l_row_0, mut l_row_1) = inner_iter.next().unwrap(); + let (mut l_col_0, mut l_col_1) = inner_iter.next().unwrap(); + let (mut val_0, mut val_1) = inner_iter.next().unwrap(); + let (mut e_0, mut e_1) = inner_iter.next().unwrap(); + let (mut masked_0, mut masked_1) = inner_iter.next().unwrap(); + let (mut w_0, mut w_1) = inner_iter.next().unwrap(); + + let q_0 = inner.q[0]; + let q_suffix: Vec = inner.q[1..].to_vec(); + + // 4. Bind the four initial claims, sample fresh beta. + transcript.absorb( + b"fic", + &[c_g, inner.claim_abc, inner.claim_e, inner.claim_w].as_slice(), + ); + let beta = transcript.squeeze(spec::BATCH_BETA)?; + let beta2 = beta * beta; + let beta3 = beta2 * beta; + + // Per-relation running claims. + let mut e_g = c_g; + let mut e_a = inner.claim_abc; + let mut e_e = inner.claim_e; + let mut e_w = inner.claim_w; + + let mut eq_gkr = EqSumCheckInstance::::new(tau.clone()); + let mut eq_e = EqSumCheckInstance::::new(q_suffix.clone()); + + let mut suffix_round_polys: Vec> = Vec::with_capacity(n - 1); + let mut s: Vec = Vec::with_capacity(n - 1); + + // 5. The n-1 shared suffix rounds. GKR / ABC / E / W use the cached-delta fast + // paths (BDDT claim derivation + delta caching for the following bind). Only + // `e_0`/`e_1` bind non-cached: they carry no round evaluation and are kept + // solely for the boundary `h`. + // + // §20.2: the GKR round-0 `t(0)` is the prefix's last parent-reduction left + // claims (weighted), so round 0 scans only for `t(inf)` — the same shortcut + // `prove_layer_sumcheck` applies to every prefix layer (commit 23d83cd). This + // only reshapes the GKR round-0 evaluation; the numeric result is identical. + let gkr_round0_t_0: E::Scalar = final_claims_by_layer + .last() + .expect("fused last layer follows the prefix parent reduction") + .iter() + .zip(weights.iter()) + .map(|(fc, (w_num, w_den))| *w_num * fc.left.num + *w_den * fc.left.den) + .sum(); + for round in 0..(n - 1) { + let (g_g0, g_gc, g_gm1) = if round == 0 { + eq_gkr.evaluation_points_logup_gate_and_cache_deltas_with_t_0( + &mut nl, + &mut nr, + &mut dl, + &mut dr, + &weights, + gkr_round0_t_0, + e_g, + ) + } else { + eq_gkr.evaluation_points_logup_gate_and_cache_deltas( + &mut nl, &mut nr, &mut dl, &mut dr, &weights, e_g, + ) + }; + + let (a0_0, ac_0, am1_0) = SumcheckProof::::compute_eval_points_cubic_with_cached_deltas( + &mut l_row_0, + &mut l_col_0, + &mut val_0, + ); + let (a0_1, ac_1, am1_1) = SumcheckProof::::compute_eval_points_cubic_with_cached_deltas( + &mut l_row_1, + &mut l_col_1, + &mut val_1, + ); + let (g_a0, g_ac, g_am1) = (a0_0 + a0_1, ac_0 + ac_1, am1_0 + am1_1); + + let (g_e0, _e_bound, g_em1) = eq_e + .evaluation_points_quadratic_with_two_inputs_and_cached_delta(&mut e_0, &mut e_1, q_0, e_e); + + let (w0_0, wm1_0) = + SumcheckProof::::compute_eval_points_quadratic_with_cached_deltas(&mut masked_0, &mut w_0); + let (w0_1, wm1_1) = + SumcheckProof::::compute_eval_points_quadratic_with_cached_deltas(&mut masked_1, &mut w_1); + let (g_w0, g_wm1) = (w0_0 + w0_1, wm1_0 + wm1_1); + + // Per-relation polynomials advance each individual running claim. + let g_poly = UniPoly::from_evals_deg3(&[g_g0, e_g - g_g0, g_gc, g_gm1]); + let a_poly = UniPoly::from_evals_deg3(&[g_a0, e_a - g_a0, g_ac, g_am1]); + let e_poly = UniPoly::from_evals_deg3(&[g_e0, e_e - g_e0, E::Scalar::ZERO, g_em1]); + let w_poly = UniPoly::from_evals_deg3(&[g_w0, e_w - g_w0, E::Scalar::ZERO, g_wm1]); + + // Fused round polynomial (E and W contribute 0 to the cubic coefficient). + let f0 = g_g0 + beta * g_a0 + beta2 * g_e0 + beta3 * g_w0; + let fc = g_gc + beta * g_ac; + let fm1 = g_gm1 + beta * g_am1 + beta2 * g_em1 + beta3 * g_wm1; + let e_comb = e_g + beta * e_a + beta2 * e_e + beta3 * e_w; + let fused = UniPoly::from_evals_deg3(&[f0, e_comb - f0, fc, fm1]); + + transcript.absorb(spec::ROUND_POLY, &fused); + let s_j = transcript.squeeze(spec::ROUND_CHALLENGE)?; + + e_g = g_poly.evaluate(&s_j); + e_a = a_poly.evaluate(&s_j); + e_e = e_poly.evaluate(&s_j); + e_w = w_poly.evaluate(&s_j); + + // Cached-delta bind for GKR / ABC / E (their high halves now hold deltas). + for p in nl + .iter_mut() + .chain(nr.iter_mut()) + .chain(dl.iter_mut()) + .chain(dr.iter_mut()) + { + p.bind_poly_var_top_with_cached_delta(&s_j); + } + eq_gkr.bound(&s_j); + for p in [ + &mut l_row_0, + &mut l_row_1, + &mut l_col_0, + &mut l_col_1, + &mut val_0, + &mut val_1, + ] { + p.bind_poly_var_top_with_cached_delta(&s_j); + } + eq_e.bound(&s_j); + // Cached-delta bind for the witness + E halves (their high halves hold the + // deltas cached by this round's W and E evaluations). + for p in [ + &mut masked_0, + &mut masked_1, + &mut w_0, + &mut w_1, + &mut e_0, + &mut e_1, + ] { + p.bind_poly_var_top_with_cached_delta(&s_j); + } + + s.push(s_j); + suffix_round_polys.push(fused.compress()); + } + + // 6. Input splits + boundary. `G_end` is reconstructed from the splits (never + // absorbed); `close_inner_msb` then absorbs the splits, `h`, and folds `f`. + let input_splits: [LayerFinalClaim; 4] = core::array::from_fn(|i| { + LayerFinalClaim::::new(nl[i].Z[0], nr[i].Z[0], dl[i].Z[0], dr[i].Z[0]) + }); + + let eq_tau_s = EqPolynomial::new(tau.clone()).evaluate(&s); + let g_end = gkr_endpoint::(&input_splits, &weights, eq_tau_s); + let e_suffix = e_g + beta * e_a + beta2 * e_e + beta3 * e_w; + let h_sum = e_suffix - g_end; + + let eq_qsuf_s = EqPolynomial::new(q_suffix.clone()).evaluate(&s); + let pairs = InnerMsbPairs { + L_row: (l_row_0.Z[0], l_row_1.Z[0]), + L_col: (l_col_0.Z[0], l_col_1.Z[0]), + val: (val_0.Z[0], val_1.Z[0]), + E: (e_0.Z[0], e_1.Z[0]), + masked: (masked_0.Z[0], masked_1.Z[0]), + W: (w_0.Z[0], w_1.Z[0]), + }; + let (msb_round_poly, f, endpoints) = close_inner_msb::( + &pairs, + q_0, + eq_qsuf_s, + beta, + beta2, + beta3, + h_sum, + &input_splits, + transcript, + )?; + + // r_shared = f || s (fold challenge as MSB, suffix challenges as the tail). + let mut r_shared = Vec::with_capacity(n); + r_shared.push(f); + r_shared.extend_from_slice(&s); + + let proof = FusedGkrInnerProof { + suffix_round_polys, + input_splits, + msb_round_poly, + }; + Ok((proof, r_shared, endpoints)) +} + +/// The `n = 1` prover: no suffix rounds. The GKR root reduction is an exact +/// component check (done by the verifier from the absorbed splits); the Inner +/// relations contribute a single MSB polynomial `h` with +/// `h(0)+h(1) = beta·C_A + beta^2·C_E + beta^3·C_W`. +#[allow(non_snake_case)] +fn prove_fused_base( + gkr_prefix: GkrProverPrefix, + inner: FusedInnerInputs, + transcript: &mut E::TE, +) -> Result<(FusedGkrInnerProof, Vec, FusedEndpointEvals), NovaError> { + let GkrProverPrefix { input_layers, .. } = gkr_prefix; + let input_splits: [LayerFinalClaim; 4] = core::array::from_fn(|i| { + LayerFinalClaim::::new( + input_layers[i].num.Z[0], + input_layers[i].num.Z[1], + input_layers[i].den.Z[0], + input_layers[i].den.Z[1], + ) + }); + + transcript.absorb( + b"fic", + &[inner.claim_abc, inner.claim_e, inner.claim_w].as_slice(), + ); + let beta = transcript.squeeze(spec::BATCH_BETA)?; + let beta2 = beta * beta; + let beta3 = beta2 * beta; + + // No suffix rounds, so the Inner pairs are the raw two-cell columns and + // eq(q_suffix, s) collapses to ONE; the boundary sum is the beta-batched + // initial claims. `close_inner_msb` handles the rest identically to n >= 2. + let pairs = InnerMsbPairs { + L_row: (inner.L_row[0], inner.L_row[1]), + L_col: (inner.L_col[0], inner.L_col[1]), + val: (inner.val[0], inner.val[1]), + E: (inner.E[0], inner.E[1]), + masked: (inner.masked_eq[0], inner.masked_eq[1]), + W: (inner.W[0], inner.W[1]), + }; + let h_sum = beta * inner.claim_abc + beta2 * inner.claim_e + beta3 * inner.claim_w; + let (msb_round_poly, f, endpoints) = close_inner_msb::( + &pairs, + inner.q[0], + E::Scalar::ONE, + beta, + beta2, + beta3, + h_sum, + &input_splits, + transcript, + )?; + + let proof = FusedGkrInnerProof { + suffix_round_polys: vec![], + input_splits, + msb_round_poly, + }; + Ok((proof, vec![f], endpoints)) +} + +/// Verifies the fused argument, returning the shared point, the Inner endpoint +/// value `h(f)`, the batching challenge `beta`, and the four reduced input-layer +/// fractions. The host then checks `e_inner == inner_expected` and reconciles the +/// four fractions against its committed columns at `r_shared`. +pub(crate) fn verify_fused( + proof: &FusedGkrInnerProof, + gkr_prefix: GkrVerifierPrefix, + claim_abc: E::Scalar, + claim_e: E::Scalar, + claim_w: E::Scalar, + transcript: &mut E::TE, +) -> Result, NovaError> { + assert_eq!(gkr_prefix.m, spec::NUM_GKR_INSTANCES); + let n = gkr_prefix.num_vars; + + if n == 1 { + return verify_fused_base(proof, gkr_prefix, claim_abc, claim_e, claim_w, transcript); + } + + if proof.suffix_round_polys.len() != n - 1 { + return Err(NovaError::InvalidSumcheckProof); + } + let GkrVerifierPrefix { + running, + point: tau, + .. + } = gkr_prefix; + + let lambda_last = transcript.squeeze(spec::LAST_LAYER_LAMBDA)?; + let weights = gate_weights::(lambda_last); + let c_g: E::Scalar = running + .iter() + .zip(weights.iter()) + .map(|(fr, (a, b))| *a * fr.num + *b * fr.den) + .sum(); + + transcript.absorb(b"fic", &[c_g, claim_abc, claim_e, claim_w].as_slice()); + let beta = transcript.squeeze(spec::BATCH_BETA)?; + let beta2 = beta * beta; + let beta3 = beta2 * beta; + let mut e = c_g + beta * claim_abc + beta2 * claim_e + beta3 * claim_w; + + let mut s: Vec = Vec::with_capacity(n - 1); + for poly_c in &proof.suffix_round_polys { + let poly = poly_c.decompress(&e); + if poly.degree() > spec::FUSED_DEGREE { + return Err(NovaError::InvalidSumcheckProof); + } + transcript.absorb(spec::ROUND_POLY, &poly); + let s_j = transcript.squeeze(spec::ROUND_CHALLENGE)?; + e = poly.evaluate(&s_j); + s.push(s_j); + } + let e_suffix = e; + + for sp in &proof.input_splits { + absorb_fraction::(transcript, sp.left); + absorb_fraction::(transcript, sp.right); + } + let eq_tau_s = EqPolynomial::new(tau.clone()).evaluate(&s); + let g_end = gkr_endpoint::(&proof.input_splits, &weights, eq_tau_s); + let h_sum = e_suffix - g_end; + + let h_poly = proof.msb_round_poly.decompress(&h_sum); + if h_poly.degree() > spec::FUSED_DEGREE { + return Err(NovaError::InvalidSumcheckProof); + } + transcript.absorb(spec::MSB_POLY, &h_poly); + let f = transcript.squeeze(spec::SHARED_FOLD)?; + + let mut r_shared = Vec::with_capacity(n); + r_shared.push(f); + r_shared.extend_from_slice(&s); + let e_inner = h_poly.evaluate(&f); + let gkr_fractions: [Fraction; 4] = + core::array::from_fn(|i| proof.input_splits[i].fold_into_next_claim(f)); + + Ok(FusedVerifierOutput { + r_shared, + e_inner, + beta, + gkr_fractions, + }) +} + +/// The `n = 1` verifier: exact component-wise root-gate check (never a +/// probabilistic reduction), then the single Inner MSB polynomial. +fn verify_fused_base( + proof: &FusedGkrInnerProof, + gkr_prefix: GkrVerifierPrefix, + claim_abc: E::Scalar, + claim_e: E::Scalar, + claim_w: E::Scalar, + transcript: &mut E::TE, +) -> Result, NovaError> { + if !proof.suffix_round_polys.is_empty() { + return Err(NovaError::InvalidSumcheckProof); + } + let root = gkr_prefix.running; + + transcript.absorb(b"fic", &[claim_abc, claim_e, claim_w].as_slice()); + let beta = transcript.squeeze(spec::BATCH_BETA)?; + let beta2 = beta * beta; + let beta3 = beta2 * beta; + let h_sum = beta * claim_abc + beta2 * claim_e + beta3 * claim_w; + + for sp in &proof.input_splits { + absorb_fraction::(transcript, sp.left); + absorb_fraction::(transcript, sp.right); + } + // R7: the root claim must equal the fraction-add gate of its two children, + // component-wise (never a scaled / probabilistic check). + for (rt, sp) in root.iter().zip(proof.input_splits.iter()) { + let gate = sp.compute_gate(); + if rt.num != gate.num || rt.den != gate.den { + return Err(NovaError::InvalidSumcheckProof); + } + } + + let h_poly = proof.msb_round_poly.decompress(&h_sum); + if h_poly.degree() > spec::FUSED_DEGREE { + return Err(NovaError::InvalidSumcheckProof); + } + transcript.absorb(spec::MSB_POLY, &h_poly); + let f = transcript.squeeze(spec::SHARED_FOLD)?; + + let e_inner = h_poly.evaluate(&f); + let gkr_fractions: [Fraction; 4] = + core::array::from_fn(|i| proof.input_splits[i].fold_into_next_claim(f)); + + Ok(FusedVerifierOutput { + r_shared: vec![f], + e_inner, + beta, + gkr_fractions, + }) +} + +/// Reconstructs the [`GkrVerifierPrefix`] from the GKR prefix proof pieces by +/// replaying the prefix reductions. For `n = 1` (no prefix layers) it only binds +/// the four root claims. Shared by the isolated tests and the ppSNARK host. +pub(crate) fn verify_gkr_prefix( + initial_claims: Vec>, + prefix_final_claims: Vec>>, + prefix_sumchecks: Vec>, + transcript: &mut E::TE, +) -> Result, NovaError> { + use crate::spartan::logup_gkr::proof::LogupGkrProof; + // The four sub-instances are fixed (`row/col × table/access`); reject any other + // count up front rather than relying on the length-4 destructure in + // `reconcile_and_balance` to catch it downstream. + if initial_claims.len() != spec::NUM_GKR_INSTANCES { + return Err(NovaError::InvalidNumInstances); + } + if prefix_final_claims.is_empty() { + // n = 1: no prefix layers; bind the root claims exactly as prove_prefix did. + for c in &initial_claims { + crate::spartan::logup_gkr::verifier::absorb_fraction::(transcript, *c); + } + return Ok(GkrVerifierPrefix::new( + spec::NUM_GKR_INSTANCES, + 1, + initial_claims, + vec![], + )); + } + let temp = LogupGkrProof { + initial_claims, + final_claims: prefix_final_claims, + sumchecks: prefix_sumchecks, + }; + let claim = crate::spartan::logup_gkr::verifier::verify::(&temp, transcript)?; + Ok(GkrVerifierPrefix::new( + spec::NUM_GKR_INSTANCES, + claim.eval_point().len() + 1, + claim.openings().to_vec(), + claim.eval_point().to_vec(), + )) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::spartan::logup_gkr::layer::Layer; + use crate::spartan::logup_gkr::proof::LayerSumcheck; + use crate::spartan::logup_gkr::prover::prove_prefix; + + type E = crate::provider::Bn256EngineKZG; + type Fr = ::Scalar; + + struct Rng(u64); + impl Rng { + fn next_u64(&mut self) -> u64 { + self.0 = self + .0 + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + self.0 >> 1 + } + fn fr(&mut self) -> Fr { + Fr::from(self.next_u64()) + } + fn nonzero_fr(&mut self) -> Fr { + Fr::from(self.next_u64() | 1) + } + } + + #[allow(non_snake_case)] + struct Inputs { + layer_num: Vec>, + layer_den: Vec>, + L_row: Vec, + L_col: Vec, + val: Vec, + E: Vec, + masked: Vec, + W: Vec, + q: Vec, + } + + fn make_inputs(n: usize, seed: u64) -> Inputs { + let big_n = 1usize << n; + let mut rng = Rng(seed); + let layer_num: Vec> = (0..4) + .map(|_| (0..big_n).map(|_| rng.fr()).collect()) + .collect(); + let layer_den: Vec> = (0..4) + .map(|_| (0..big_n).map(|_| rng.nonzero_fr()).collect()) + .collect(); + Inputs { + layer_num, + layer_den, + L_row: (0..big_n).map(|_| rng.fr()).collect(), + L_col: (0..big_n).map(|_| rng.fr()).collect(), + val: (0..big_n).map(|_| rng.fr()).collect(), + E: (0..big_n).map(|_| rng.fr()).collect(), + masked: (0..big_n).map(|_| rng.fr()).collect(), + W: (0..big_n).map(|_| rng.fr()).collect(), + q: (0..n).map(|_| rng.fr()).collect(), + } + } + + fn mle(v: Vec) -> MultilinearPolynomial { + MultilinearPolynomial::new(v) + } + + fn inner_claims(inp: &Inputs) -> (Fr, Fr, Fr) { + let c_a: Fr = (0..inp.L_row.len()) + .map(|i| inp.L_row[i] * inp.L_col[i] * inp.val[i]) + .sum(); + let c_e = mle(inp.E.clone()).evaluate(&inp.q); + let c_w: Fr = (0..inp.masked.len()) + .map(|i| inp.masked[i] * inp.W[i]) + .sum(); + (c_a, c_e, c_w) + } + + fn make_inner(inp: &Inputs) -> FusedInnerInputs { + let (c_a, c_e, c_w) = inner_claims(inp); + FusedInnerInputs { + L_row: inp.L_row.clone(), + L_col: inp.L_col.clone(), + val: inp.val.clone(), + E: inp.E.clone(), + masked_eq: inp.masked.clone(), + W: inp.W.clone(), + q: inp.q.clone(), + claim_abc: c_a, + claim_e: c_e, + claim_w: c_w, + } + } + + type PrefixPieces = ( + Vec>, + Vec>>, + Vec>, + ); + + fn prove( + inp: &Inputs, + transcript: &mut ::TE, + ) -> (FusedGkrInnerProof, Vec, PrefixPieces, (Fr, Fr, Fr)) { + let layers: Vec> = (0..4) + .map(|i| Layer:: { + num: mle(inp.layer_num[i].clone()), + den: mle(inp.layer_den[i].clone()), + }) + .collect(); + let prefix = prove_prefix::(layers, transcript).expect("prove_prefix"); + let pieces = ( + prefix.initial_claims.clone(), + prefix.final_claims_by_layer.clone(), + prefix.sumchecks.clone(), + ); + let claims = inner_claims(inp); + let inner = make_inner(inp); + let (proof, r_shared, _endpoints) = + prove_fused::(prefix, inner, transcript).expect("prove_fused"); + (proof, r_shared, pieces, claims) + } + + // The host reconcile oracle: direct MLE evaluation at r_shared. Returns Ok(()) + // iff the fused verifier output is consistent with the true columns. + fn host_check(out: &FusedVerifierOutput, inp: &Inputs) -> Result<(), ()> { + let r = &out.r_shared; + for i in 0..4 { + let num = mle(inp.layer_num[i].clone()).evaluate(r); + let den = mle(inp.layer_den[i].clone()).evaluate(r); + if out.gkr_fractions[i].num != num || out.gkr_fractions[i].den != den { + return Err(()); + } + } + let lr = mle(inp.L_row.clone()).evaluate(r); + let lc = mle(inp.L_col.clone()).evaluate(r); + let v = mle(inp.val.clone()).evaluate(r); + let ev = mle(inp.E.clone()).evaluate(r); + let me = mle(inp.masked.clone()).evaluate(r); + let w = mle(inp.W.clone()).evaluate(r); + let eq_q_r = EqPolynomial::new(inp.q.clone()).evaluate(r); + let beta = out.beta; + let beta2 = beta * beta; + let beta3 = beta2 * beta; + let inner_expected = beta * lr * lc * v + beta2 * eq_q_r * ev + beta3 * me * w; + if out.e_inner != inner_expected { + return Err(()); + } + Ok(()) + } + + fn verify( + proof: &FusedGkrInnerProof, + pieces: &PrefixPieces, + claims: (Fr, Fr, Fr), + transcript: &mut ::TE, + ) -> Result, NovaError> { + let prefix = verify_gkr_prefix::( + pieces.0.clone(), + pieces.1.clone(), + pieces.2.clone(), + transcript, + )?; + verify_fused::(proof, prefix, claims.0, claims.1, claims.2, transcript) + } + + fn roundtrip(n: usize, seed: u64) { + let inp = make_inputs(n, seed); + let mut tr_p = ::TE::new(b"fused"); + let (proof, r_shared_p, pieces, claims) = prove(&inp, &mut tr_p); + + let mut tr_v = ::TE::new(b"fused"); + let out = verify(&proof, &pieces, claims, &mut tr_v).expect("verify_fused"); + + assert_eq!(out.r_shared, r_shared_p, "n={n}: r_shared mismatch"); + assert_eq!(out.r_shared.len(), n, "n={n}: r_shared length"); + host_check(&out, &inp).unwrap_or_else(|_| panic!("n={n}: host reconcile failed")); + } + + #[test] + fn roundtrip_all_depths() { + for n in 1..=5 { + roundtrip(n, 100 + n as u64); + } + } + + // Gate C/D (endian): r_shared = [f, s_0, ..., s_{n-2}]; the suffix challenges + // are the tail. The reversed order must NOT reconcile. + #[test] + fn endian_r_shared_is_fold_then_suffix() { + let inp = make_inputs(4, 7); + let mut tr_p = ::TE::new(b"fused"); + let (proof, r_shared, _pieces, _claims) = prove(&inp, &mut tr_p); + // Direct fraction eval at r_shared matches the proof's folded splits; + // at the reversed point it must not (with overwhelming probability). + let f = r_shared[0]; + let mut reversed: Vec = r_shared[1..].to_vec(); + reversed.push(f); + for i in 0..4 { + let num_ok = mle(inp.layer_num[i].clone()).evaluate(&r_shared); + let num_rev = mle(inp.layer_num[i].clone()).evaluate(&reversed); + assert_eq!(proof.input_splits[i].fold_into_next_claim(f).num, num_ok); + assert_ne!(num_ok, num_rev, "reversed point must differ"); + } + } + + fn expect_reject(mutate: impl FnOnce(&mut FusedGkrInnerProof)) { + let inp = make_inputs(4, 55); + let mut tr_p = ::TE::new(b"fused"); + let (mut proof, _r, pieces, claims) = prove(&inp, &mut tr_p); + mutate(&mut proof); + let mut tr_v = ::TE::new(b"fused"); + let verdict = verify(&proof, &pieces, claims, &mut tr_v) + .and_then(|out| host_check(&out, &inp).map_err(|_| NovaError::InvalidSumcheckProof)); + assert!(verdict.is_err(), "tampered proof must be rejected"); + } + + #[test] + fn rejects_tampered_suffix_round_poly() { + expect_reject(|p| { + // Replace the first suffix round polynomial: the transcript diverges, so + // r_shared changes and the reconcile fails. + let bad = UniPoly::from_evals(&[Fr::from(2), Fr::from(5), Fr::from(11), Fr::from(4)]); + p.suffix_round_polys[0] = bad.compress(); + }); + } + + #[test] + fn rejects_tampered_input_split() { + expect_reject(|p| p.input_splits[1].right.den += Fr::from(3)); + } + + #[test] + fn rejects_tampered_msb_poly() { + expect_reject(|p| { + let bad = UniPoly::from_evals(&[Fr::from(1), Fr::from(2), Fr::from(9), Fr::from(1)]); + p.msb_round_poly = bad.compress(); + }); + } + + #[test] + fn rejects_tampered_claim() { + // A wrong Inner claim must be rejected (the endpoint no longer matches). + let inp = make_inputs(4, 88); + let mut tr_p = ::TE::new(b"fused"); + let (proof, _r, pieces, claims) = prove(&inp, &mut tr_p); + let bad_claims = (claims.0 + Fr::from(1), claims.1, claims.2); + let mut tr_v = ::TE::new(b"fused"); + let verdict = verify(&proof, &pieces, bad_claims, &mut tr_v) + .and_then(|out| host_check(&out, &inp).map_err(|_| NovaError::InvalidSumcheckProof)); + assert!(verdict.is_err(), "wrong Inner claim must be rejected"); + } + + // Differential lock (PLAN section 19.3, lightweight form): the fused last-layer + // gate algebra (`gate_weights` + `gkr_endpoint`) must equal the standalone GKR + // gate reconstruction — `eq · Σ_k λ^k · [compute_gate.num, compute_gate.den]` + // (the exact expression `verify_one_reduction` reconciles against). The two + // drivers share the per-round eval kernel but reimplement this boundary + // separately, so this catches a future divergence of the λ-power schedule or + // the fraction-add gate without needing to instrument the prover round-by-round. + #[test] + fn fused_gkr_endpoint_matches_standalone_gate_reconstruction() { + use crate::spartan::logup_gkr::proof::LayerFinalClaim; + let mut rng = Rng(2024); + let lambda = rng.fr(); + let eq_tau_s = rng.fr(); + let splits: [LayerFinalClaim; spec::NUM_GKR_INSTANCES] = + core::array::from_fn(|_| LayerFinalClaim::::new(rng.fr(), rng.fr(), rng.fr(), rng.fr())); + + let weights = gate_weights::(lambda); + let fused = gkr_endpoint::(&splits, &weights, eq_tau_s); + + // Standalone: eq · horner over the flattened [gate.num, gate.den] per instance + // (instance i's numerator on λ^{2i}, denominator on λ^{2i+1}). + let mut standalone = Fr::ZERO; + let mut pw = Fr::ONE; + for sp in &splits { + let g = sp.compute_gate(); + standalone += pw * g.num; + pw *= lambda; + standalone += pw * g.den; + pw *= lambda; + } + standalone *= eq_tau_s; + + assert_eq!( + fused, standalone, + "fused last-layer gate algebra diverged from the standalone GKR reconstruction" + ); + } +} diff --git a/src/spartan/mod.rs b/src/spartan/mod.rs index f62a4c81f..1b0521d3e 100644 --- a/src/spartan/mod.rs +++ b/src/spartan/mod.rs @@ -6,6 +6,10 @@ //! //! In polynomial.rs we also provide foundational types and functions for manipulating multilinear polynomials. pub mod direct; +pub mod logup_gkr; +pub mod mem_check_logup; +pub mod mem_check_logup_gkr; +pub mod mem_check_logup_gkr_fused; pub mod ppsnark; pub mod snark; diff --git a/src/spartan/polys/multilinear.rs b/src/spartan/polys/multilinear.rs index 93d072697..ba596481b 100644 --- a/src/spartan/polys/multilinear.rs +++ b/src/spartan/polys/multilinear.rs @@ -83,6 +83,39 @@ impl MultilinearPolynomial { self.num_vars -= 1; } + /// Binds the top variable after the high half has been replaced by + /// `high - low`. + /// + /// This is the second half of an explicit evaluate-then-bind optimization: + /// the round-polynomial evaluation stores each top-variable slope in the + /// corresponding high-half slot, then this method reuses it once the + /// verifier challenge is known. + /// + /// # Preconditions + /// + /// The high half must contain `high - low` from the matching cached-delta + /// evaluation in the current round. Calling this after a non-caching + /// evaluation silently produces the wrong polynomial. + pub(crate) fn bind_poly_var_top_with_cached_delta(&mut self, r: &Scalar) { + assert!(self.num_vars > 0); + + let n = self.len() / 2; + let (left, deltas) = self.Z.split_at_mut(n); + + if n < PARALLEL_THRESHOLD { + left.iter_mut().zip(deltas.iter()).for_each(|(low, delta)| { + *low += *r * delta; + }); + } else { + zip_with_for_each!((left.par_iter_mut(), deltas.par_iter()), |low, delta| { + *low += *r * delta; + }); + } + + self.Z.resize(n, Scalar::ZERO); + self.num_vars -= 1; + } + /// Evaluates the polynomial at the given point. /// Returns Z(r) in O(n) time using O(sqrt(n)) memory for eq tables. /// @@ -411,6 +444,35 @@ mod tests { bind_and_evaluate_with::(); } + fn cached_delta_bind_matches_with() { + for num_vars in [7, 13] { + let mut rng = ChaCha20Rng::from_seed([num_vars as u8; 32]); + let poly = random(num_vars, &mut rng); + let r = F::random(&mut rng); + + let mut expected = poly.clone(); + expected.bind_poly_var_top(&r); + + let mut actual = poly; + let half = actual.len() / 2; + let (low, high) = actual.Z.split_at_mut(half); + high + .iter_mut() + .zip(low.iter()) + .for_each(|(high, low)| *high -= low); + actual.bind_poly_var_top_with_cached_delta(&r); + + assert_eq!(actual, expected); + } + } + + #[test] + fn test_cached_delta_bind_matches() { + cached_delta_bind_matches_with::(); + cached_delta_bind_matches_with::(); + cached_delta_bind_matches_with::(); + } + fn test_multi_evaluate_with_matches_single() { let mut rng = ChaCha20Rng::from_seed([42u8; 32]); let num_vars = 6; diff --git a/src/spartan/ppsnark.rs b/src/spartan/ppsnark.rs index 95f52c15f..000cefd61 100644 --- a/src/spartan/ppsnark.rs +++ b/src/spartan/ppsnark.rs @@ -3,22 +3,26 @@ //! The verifier in this preprocessing SNARK maintains a commitment to R1CS matrices. This is beneficial when using a //! polynomial commitment scheme in which the verifier's costs is succinct. //! The SNARK implemented here is described in the MicroNova paper. +#[cfg(feature = "logup-no-gkr")] +use crate::spartan::mem_check_logup; +#[cfg(not(feature = "logup-no-gkr"))] +use crate::spartan::{ + mem_check_logup_gkr::{self, MemCheckWitness}, + mem_check_logup_gkr_fused, +}; +#[cfg(feature = "logup-no-gkr")] +use crate::spartan::{ + polys::univariate::{CompressedUniPoly, UniPoly}, + powers, +}; use crate::traits::evm_serde::EvmCompatSerde; use crate::{ digest::{DigestComputer, SimpleDigestible}, errors::NovaError, r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness}, spartan::{ - batch_invert, math::Math, - polys::{ - eq::EqPolynomial, - identity::IdentityPolynomial, - masked_eq::MaskedEqPolynomial, - multilinear::{MultilinearPolynomial, SparsePolynomial}, - univariate::{CompressedUniPoly, UniPoly}, - }, - powers, + polys::{eq::EqPolynomial, masked_eq::MaskedEqPolynomial, multilinear::MultilinearPolynomial}, sumcheck::{eq_sumcheck::EqSumCheckInstance, SumcheckEngine, SumcheckProof}, PolyEvalInstance, PolyEvalWitness, }, @@ -32,6 +36,7 @@ use crate::{ }; use core::cmp::max; use ff::Field; +#[cfg(feature = "logup-no-gkr")] use itertools::Itertools as _; use once_cell::sync::OnceCell; use rayon::prelude::*; @@ -324,351 +329,6 @@ impl SumcheckEngine for WitnessBoundSumcheck { } } -/// Memory sumcheck instance for PPSNARK LogUp -pub struct MemorySumcheckInstance { - // row - w_plus_r_row: MultilinearPolynomial, - t_plus_r_row: MultilinearPolynomial, - t_plus_r_inv_row: MultilinearPolynomial, - w_plus_r_inv_row: MultilinearPolynomial, - ts_row: MultilinearPolynomial, - - // col - w_plus_r_col: MultilinearPolynomial, - t_plus_r_col: MultilinearPolynomial, - t_plus_r_inv_col: MultilinearPolynomial, - w_plus_r_inv_col: MultilinearPolynomial, - ts_col: MultilinearPolynomial, - - eq_sumcheck: EqSumCheckInstance, - - // Per-claim running claims and saved evaluation points (BDDT, eprint 2025/1117 Section 6.2) - running_claims: [E::Scalar; 6], - saved_evals: [[E::Scalar; 3]; 6], -} - -impl MemorySumcheckInstance { - /// Computes witnesses for MemoryInstanceSumcheck - /// - /// # Description - /// We use the logUp protocol to prove that - /// sum TS\[i\]/(T\[i\] + r) - 1/(W\[i\] + r) = 0 - /// where - /// T_row\[i\] = mem_row\[i\] * gamma + i - /// = eq(tau)\[i\] * gamma + i - /// W_row\[i\] = L_row\[i\] * gamma + addr_row\[i\] - /// = eq(tau)\[row\[i\]\] * gamma + addr_row\[i\] - /// T_col\[i\] = mem_col\[i\] * gamma + i - /// = z\[i\] * gamma + i - /// W_col\[i\] = L_col\[i\] * gamma + addr_col\[i\] - /// = z\[col\[i\]\] * gamma + addr_col\[i\] - /// and - /// TS_row, TS_col are integer-valued vectors representing the number of reads - /// to each memory cell of L_row, L_col - /// - /// The function returns oracles for the polynomials TS\[i\]/(T\[i\] + r), 1/(W\[i\] + r), - /// as well as auxiliary polynomials T\[i\] + r, W\[i\] + r - pub fn compute_oracles( - ck: &CommitmentKey, - r: &E::Scalar, - gamma: &E::Scalar, - mem_row: &[E::Scalar], - addr_row: &[E::Scalar], - L_row: &[E::Scalar], - ts_row: &[E::Scalar], - mem_col: &[E::Scalar], - addr_col: &[E::Scalar], - L_col: &[E::Scalar], - ts_col: &[E::Scalar], - ) -> Result<([Commitment; 4], [Vec; 4], [Vec; 4]), NovaError> { - // hash the tuples of (addr,val) memory contents and read responses into a single field element using `hash_func` - let hash_func_vec = |mem: &[E::Scalar], - addr: &[E::Scalar], - lookups: &[E::Scalar]| - -> (Vec, Vec) { - let hash_func = |addr: &E::Scalar, val: &E::Scalar| -> E::Scalar { *val * gamma + *addr }; - assert_eq!(addr.len(), lookups.len()); - rayon::join( - || { - (0..mem.len()) - .map(|i| hash_func(&E::Scalar::from(i as u64), &mem[i])) - .collect::>() - }, - || { - (0..addr.len()) - .map(|i| hash_func(&addr[i], &lookups[i])) - .collect::>() - }, - ) - }; - - let ((T_row, W_row), (T_col, W_col)) = rayon::join( - || hash_func_vec(mem_row, addr_row, L_row), - || hash_func_vec(mem_col, addr_col, L_col), - ); - - // compute vectors TS[i]/(T[i] + r) and 1/(W[i] + r) - let helper = |T: &[E::Scalar], - W: &[E::Scalar], - TS: &[E::Scalar], - r: &E::Scalar| - -> Result< - ( - Vec, - Vec, - Vec, - Vec, - ), - NovaError, - > { - let t_plus_r_and_w_plus_r = T - .par_iter() - .chain(W.par_iter()) - .map(|e| *e + *r) - .collect::>(); - - let inv = batch_invert(&t_plus_r_and_w_plus_r)?; - - let mut t_plus_r = t_plus_r_and_w_plus_r; - let w_plus_r = t_plus_r.split_off(T.len()); - - let mut t_plus_r_inv = inv; - let w_plus_r_inv = t_plus_r_inv.split_off(T.len()); - - // compute inv[i] * TS[i] in parallel - t_plus_r_inv = zip_with!((t_plus_r_inv.into_par_iter(), TS.par_iter()), |e1, e2| e1 - * *e2) - .collect::>(); - - Ok((t_plus_r_inv, w_plus_r_inv, t_plus_r, w_plus_r)) - }; - - let (row, col) = rayon::join( - || helper(&T_row, &W_row, ts_row, r), - || helper(&T_col, &W_col, ts_col, r), - ); - - let (t_plus_r_inv_row, w_plus_r_inv_row, t_plus_r_row, w_plus_r_row) = row?; - let (t_plus_r_inv_col, w_plus_r_inv_col, t_plus_r_col, w_plus_r_col) = col?; - - let ( - (comm_t_plus_r_inv_row, comm_w_plus_r_inv_row), - (comm_t_plus_r_inv_col, comm_w_plus_r_inv_col), - ) = rayon::join( - || { - rayon::join( - || E::CE::commit(ck, &t_plus_r_inv_row, &E::Scalar::ZERO), - || E::CE::commit(ck, &w_plus_r_inv_row, &E::Scalar::ZERO), - ) - }, - || { - rayon::join( - || E::CE::commit(ck, &t_plus_r_inv_col, &E::Scalar::ZERO), - || E::CE::commit(ck, &w_plus_r_inv_col, &E::Scalar::ZERO), - ) - }, - ); - - let comm_vec = [ - comm_t_plus_r_inv_row, - comm_w_plus_r_inv_row, - comm_t_plus_r_inv_col, - comm_w_plus_r_inv_col, - ]; - - let poly_vec = [ - t_plus_r_inv_row, - w_plus_r_inv_row, - t_plus_r_inv_col, - w_plus_r_inv_col, - ]; - - let aux_poly_vec = [t_plus_r_row, w_plus_r_row, t_plus_r_col, w_plus_r_col]; - - Ok((comm_vec, poly_vec, aux_poly_vec)) - } - - /// Create a new memory sumcheck instance - pub fn new( - polys_oracle: [Vec; 4], - polys_aux: [Vec; 4], - rhos: Vec, - ts_row: Vec, - ts_col: Vec, - ) -> Self { - let [t_plus_r_inv_row, w_plus_r_inv_row, t_plus_r_inv_col, w_plus_r_inv_col] = polys_oracle; - let [t_plus_r_row, w_plus_r_row, t_plus_r_col, w_plus_r_col] = polys_aux; - - Self { - w_plus_r_row: MultilinearPolynomial::new(w_plus_r_row), - t_plus_r_row: MultilinearPolynomial::new(t_plus_r_row), - t_plus_r_inv_row: MultilinearPolynomial::new(t_plus_r_inv_row), - w_plus_r_inv_row: MultilinearPolynomial::new(w_plus_r_inv_row), - ts_row: MultilinearPolynomial::new(ts_row), - w_plus_r_col: MultilinearPolynomial::new(w_plus_r_col), - t_plus_r_col: MultilinearPolynomial::new(t_plus_r_col), - t_plus_r_inv_col: MultilinearPolynomial::new(t_plus_r_inv_col), - w_plus_r_inv_col: MultilinearPolynomial::new(w_plus_r_inv_col), - ts_col: MultilinearPolynomial::new(ts_col), - eq_sumcheck: EqSumCheckInstance::new(rhos), - running_claims: [E::Scalar::ZERO; 6], - saved_evals: [[E::Scalar::ZERO; 3]; 6], - } - } -} - -impl SumcheckEngine for MemorySumcheckInstance { - fn initial_claims(&self) -> Vec { - vec![E::Scalar::ZERO; 6] - } - - fn degree(&self) -> usize { - 3 - } - - fn size(&self) -> usize { - // sanity checks - assert_eq!(self.w_plus_r_row.len(), self.t_plus_r_row.len()); - assert_eq!(self.w_plus_r_row.len(), self.ts_row.len()); - assert_eq!(self.w_plus_r_row.len(), self.w_plus_r_col.len()); - assert_eq!(self.w_plus_r_row.len(), self.t_plus_r_col.len()); - assert_eq!(self.w_plus_r_row.len(), self.ts_col.len()); - - self.w_plus_r_row.len() - } - - fn evaluation_points(&mut self) -> Vec> { - // Pre-borrow all fields as shared references for parallel access - let eq = &self.eq_sumcheck; - let running_claims = &self.running_claims; - let t_plus_r_inv_row = &self.t_plus_r_inv_row; - let w_plus_r_inv_row = &self.w_plus_r_inv_row; - let t_plus_r_row = &self.t_plus_r_row; - let w_plus_r_row = &self.w_plus_r_row; - let ts_row = &self.ts_row; - let t_plus_r_inv_col = &self.t_plus_r_inv_col; - let w_plus_r_inv_col = &self.w_plus_r_inv_col; - let t_plus_r_col = &self.t_plus_r_col; - let w_plus_r_col = &self.w_plus_r_col; - let ts_col = &self.ts_col; - - // inv related evaluation points for linear (A - B) pattern (no claim derivation) - // 0 = sum TS[i]/(T[i] + r) - 1/(W[i] + r) - let ( - ((eval_inv_0_row, eval_inv_3_row), (eval_inv_0_col, eval_inv_3_col)), - ( - ((eval_T_0_row, eval_T_2_row, eval_T_3_row), (eval_W_0_row, eval_W_2_row, eval_W_3_row)), - ((eval_T_0_col, eval_T_2_col, eval_T_3_col), (eval_W_0_col, eval_W_2_col, eval_W_3_col)), - ), - ) = rayon::join( - || { - rayon::join( - || SumcheckProof::::compute_eval_points_linear(t_plus_r_inv_row, w_plus_r_inv_row), - || SumcheckProof::::compute_eval_points_linear(t_plus_r_inv_col, w_plus_r_inv_col), - ) - }, - || { - rayon::join( - || { - // Row evaluation points (claim-derived, BDDT Section 6.2) - rayon::join( - || { - // 0 = sum eq[i] * (inv_T[i] * (T[i] + r) - TS[i])) - eq.evaluation_points_cubic_with_three_inputs( - t_plus_r_inv_row, - t_plus_r_row, - ts_row, - running_claims[2], - ) - }, - || { - // 0 = sum eq[i] * (inv_W[i] * (W[i] + r) - 1)) - eq.evaluation_points_cubic_with_two_inputs( - w_plus_r_inv_row, - w_plus_r_row, - running_claims[3], - ) - }, - ) - }, - || { - // Column evaluation points (claim-derived, BDDT Section 6.2) - rayon::join( - || { - eq.evaluation_points_cubic_with_three_inputs( - t_plus_r_inv_col, - t_plus_r_col, - ts_col, - running_claims[4], - ) - }, - || { - eq.evaluation_points_cubic_with_two_inputs( - w_plus_r_inv_col, - w_plus_r_col, - running_claims[5], - ) - }, - ) - }, - ) - }, - ); - - // Save evaluation points for running claim updates in bound() - self.saved_evals = [ - [eval_inv_0_row, E::Scalar::ZERO, eval_inv_3_row], - [eval_inv_0_col, E::Scalar::ZERO, eval_inv_3_col], - [eval_T_0_row, eval_T_2_row, eval_T_3_row], - [eval_W_0_row, eval_W_2_row, eval_W_3_row], - [eval_T_0_col, eval_T_2_col, eval_T_3_col], - [eval_W_0_col, eval_W_2_col, eval_W_3_col], - ]; - - self.saved_evals.iter().map(|e| e.to_vec()).collect() - } - - fn bound(&mut self, r: &E::Scalar) { - for j in 0..6 { - self.running_claims[j] = - SumcheckProof::::update_claim(self.running_claims[j], &self.saved_evals[j], r); - } - - [ - &mut self.t_plus_r_row, - &mut self.t_plus_r_inv_row, - &mut self.w_plus_r_row, - &mut self.w_plus_r_inv_row, - &mut self.ts_row, - &mut self.t_plus_r_col, - &mut self.t_plus_r_inv_col, - &mut self.w_plus_r_col, - &mut self.w_plus_r_inv_col, - &mut self.ts_col, - ] - .par_iter_mut() - .for_each(|poly| poly.bind_poly_var_top(r)); - - self.eq_sumcheck.bound(r); - } - - fn final_claims(&self) -> Vec> { - let poly_row_final = vec![ - self.t_plus_r_inv_row[0], - self.w_plus_r_inv_row[0], - self.ts_row[0], - ]; - - let poly_col_final = vec![ - self.t_plus_r_inv_col[0], - self.w_plus_r_inv_col[0], - self.ts_col[0], - ]; - - vec![poly_row_final, poly_col_final] - } -} - /// Inner batched sumcheck instance for PPSNARK /// /// Proves two claims: @@ -739,16 +399,22 @@ impl SumcheckEngine for InnerBatchedSumcheckInstance { } fn evaluation_points(&mut self) -> Vec> { - let (poly_A, poly_B, poly_C) = (&self.poly_L_row, &self.poly_L_col, &self.poly_val); + let running_claim_E = self.running_claim_E; + let eq_sumcheck = &self.eq_sumcheck; + let (poly_A, poly_B, poly_C, poly_E) = ( + &mut self.poly_L_row, + &mut self.poly_L_col, + &mut self.poly_val, + &mut self.poly_E, + ); // E claim: 1 N-scaling sum + claim-derived (BDDT, eprint 2025/1117 Section 6.2) let ((eval_point_0, bound_coeff, eval_point_inf), (eval_E_0, eval_E_bound_coeff, eval_E_inf)) = rayon::join( - || SumcheckProof::::compute_eval_points_cubic(poly_A, poly_B, poly_C), + || SumcheckProof::::compute_eval_points_cubic_with_cached_deltas(poly_A, poly_B, poly_C), || { - self - .eq_sumcheck - .evaluation_points_quadratic_with_one_input(&self.poly_E, self.running_claim_E) + eq_sumcheck + .evaluation_points_quadratic_with_one_input_and_cached_delta(poly_E, running_claim_E) }, ); @@ -772,7 +438,7 @@ impl SumcheckEngine for InnerBatchedSumcheckInstance { &mut self.poly_E, ] .par_iter_mut() - .for_each(|poly| poly.bind_poly_var_top(r)); + .for_each(|poly| poly.bind_poly_var_top_with_cached_delta(r)); self.eq_sumcheck.bound(r); } @@ -820,11 +486,14 @@ pub struct RelaxedR1CSSNARK> { comm_L_row: Commitment, comm_L_col: Commitment, - // commitments to aid the memory checks - comm_t_plus_r_inv_row: Commitment, - comm_w_plus_r_inv_row: Commitment, - comm_t_plus_r_inv_col: Commitment, - comm_w_plus_r_inv_col: Commitment, + // Memory-check proof data, one field per implementation, feature-gated: + // inverse-logup (feature `logup-no-gkr`) carries the four inverse-oracle + // commitments + evals; Logup-GKR (default) carries the fractional-sum proof + + // the rerandomize claims. + #[cfg(feature = "logup-no-gkr")] + mem_check: mem_check_logup::LogupProofData, + #[cfg(not(feature = "logup-no-gkr"))] + mem_check_gkr_fused: mem_check_logup_gkr::FusedMemCheckProof, // outer sum-check proof sc_outer: SumcheckProof, @@ -840,6 +509,7 @@ pub struct RelaxedR1CSSNARK> { eval_E_at_r_outer: E::Scalar, // inner batched sum-check proof + #[cfg(feature = "logup-no-gkr")] sc_inner_batched: SumcheckProof, // claims from the end of sum-check @@ -859,22 +529,15 @@ pub struct RelaxedR1CSSNARK> { #[serde_as(as = "EvmCompatSerde")] eval_W: E::Scalar, - #[serde_as(as = "EvmCompatSerde")] - eval_t_plus_r_inv_row: E::Scalar, + // Shared address/multiplicity evaluations (both memory-check implementations + // open these at the inner point). #[serde_as(as = "EvmCompatSerde")] eval_row: E::Scalar, // address #[serde_as(as = "EvmCompatSerde")] - eval_w_plus_r_inv_row: E::Scalar, - #[serde_as(as = "EvmCompatSerde")] eval_ts_row: E::Scalar, - - #[serde_as(as = "EvmCompatSerde")] - eval_t_plus_r_inv_col: E::Scalar, #[serde_as(as = "EvmCompatSerde")] eval_col: E::Scalar, // address #[serde_as(as = "EvmCompatSerde")] - eval_w_plus_r_inv_col: E::Scalar, - #[serde_as(as = "EvmCompatSerde")] eval_ts_col: E::Scalar, // a PCS evaluation argument @@ -882,7 +545,12 @@ pub struct RelaxedR1CSSNARK> { } impl> RelaxedR1CSSNARK { - /// Batched inner sum-check prover for 3 instances: memory, inner_batched, and witness. + /// Batched inner sum-check prover for three instances: a memory-check slot, + /// the inner batched instance, and the witness-bound instance. The + /// memory-check slot is the inverse-logup `MemorySumcheckInstance` when + /// feature `logup-no-gkr` is enabled, folded with the inner and witness slots + /// into one RLC'd sumcheck landing at the shared point `r_inner_batched`. + #[cfg(feature = "logup-no-gkr")] fn prove_helper( mem: &mut T1, inner: &mut T2, @@ -910,6 +578,7 @@ impl> RelaxedR1CSSNARK { assert_eq!(mem.degree(), witness.degree()); // these claims are already added to the transcript, so we do not need to add + let num_mem_claims = mem.initial_claims().len(); let claims = mem .initial_claims() .into_iter() @@ -920,6 +589,14 @@ impl> RelaxedR1CSSNARK { let s = transcript.squeeze(b"r")?; let coeffs = powers::(&s, claims.len()); + // Let the memory-check slot collapse its equally-shaped claims into a single + // random linear combination now that the batch coefficients are known. This + // is a no-op for instances that don't override the hook. The slot leads the + // batch, so its coefficient slice starts at `coeffs[0] == 1`, keeping the + // fused round polynomial byte-identical to the per-column sum (see the trait + // doc on `fuse_with_coeffs`). + mem.fuse_with_coeffs(&coeffs[..num_mem_claims]); + // compute the joint claim let claim = zip_with!((claims.iter(), coeffs.iter()), |c_1, c_2| *c_1 * c_2).sum(); @@ -1064,8 +741,11 @@ impl> RelaxedR1CSSNARKTrait for Relax let S = S.pad(); // sanity check that R1CSShape has all required size characteristics assert!(S.is_regular_shape()); + // Capture `num_vars` up front so `S` can be released right after the + // evaluation oracles are built (the witness-bound sumcheck only needs this). + let num_vars = S.num_vars; - let W = W.pad(&S); // pad the witness + let W_padded = W.pad(&S); // pad the witness let mut transcript = E::TE::new(b"RelaxedR1CSSNARK"); // append the verifier key (which includes commitment to R1CS matrices) and the RelaxedR1CSInstance to the transcript @@ -1073,7 +753,7 @@ impl> RelaxedR1CSSNARKTrait for Relax transcript.absorb(b"U", U); // compute the full satisfying assignment by concatenating W.W, U.u, and U.X - let z = [W.W.clone(), vec![U.u], U.X.clone()].concat(); + let z = [W_padded.W.clone(), vec![U.u], U.X.clone()].concat(); // compute Az, Bz, Cz let (Az, Bz, Cz) = S.multiply_vec(&z)?; @@ -1089,11 +769,8 @@ impl> RelaxedR1CSSNARKTrait for Relax // Step 1: Outer sum-check (standalone, degree-3) on size-m polynomials // Proves: 0 = Σ_{x∈{0,1}^log(m)} eq(τ,x) * (Az(x) * Bz(x) - (u·Cz(x) + E(x))) - let uCz_E: Vec = Cz - .iter() - .zip(W.E.iter()) - .map(|(cz, e)| U.u * *cz + *e) - .collect(); + let uCz_E: Vec = + zip_with!(par_iter, (Cz, W_padded.E), |cz, e| U.u * *cz + *e).collect(); let mut poly_Az = MultilinearPolynomial::new(Az); let mut poly_Bz = MultilinearPolynomial::new(Bz); let mut poly_uCz_E = MultilinearPolynomial::new(uCz_E); @@ -1113,6 +790,15 @@ impl> RelaxedR1CSSNARKTrait for Relax let eval_Cz_at_r_outer = MultilinearPolynomial::evaluate_with(&Cz, &r_outer); let eval_E_at_r_outer = claims_outer[2] - U.u * eval_Cz_at_r_outer; + // The outer sum-check polynomials are bound to length 1 but still hold + // ~m-capacity buffers, and `Cz` is no longer read after its evaluation above. + // Release them before the memory-check / inner phase allocates its N-sized + // buffers, so ~4m scalars do not stay resident across the peak. + drop(poly_Az); + drop(poly_Bz); + drop(poly_uCz_E); + drop(Cz); + // Absorb outer sum-check claims into transcript transcript.absorb( b"e", @@ -1141,8 +827,12 @@ impl> RelaxedR1CSSNARKTrait for Relax .fold(E::Scalar::ONE, |acc, r| acc * (E::Scalar::ONE - r)); // Pad E and W to size N for inner sum-check and PCS - let E = padded::(&W.E, pk.S_repr.N, &E::Scalar::ZERO); - let W = padded::(&W.W, pk.S_repr.N, &E::Scalar::ZERO); + let E = padded::(&W_padded.E, pk.S_repr.N, &E::Scalar::ZERO); + let W = padded::(&W_padded.W, pk.S_repr.N, &E::Scalar::ZERO); + // The length-m padded relaxed witness is no longer needed once the + // N-sized `E`/`W` are materialized. Drop it explicitly (rather than letting + // the `W` shadow above merely hide it) so ~2m scalars leave the working set. + drop(W_padded); // ----------------------------------------------------------------------- // Step 2: Prepare the batched inner batched sum-check (memory + inner_batched + witness) @@ -1152,9 +842,19 @@ impl> RelaxedR1CSSNARKTrait for Relax // L_row(i) = eq(r_outer_full, row(i)) for all i // L_col(i) = z(col(i)) for all i, where z is the full satisfying assignment let (mem_row, mem_col, L_row, L_col) = pk.S_repr.evaluation_oracles(&S, &r_outer_full, &z); + // After the evaluation oracles are built, the local padded shape `S` + // and the assignment `z` are no longer used (only `S.num_vars` is needed + // later, saved above). Dropping `S` also frees the three sparse matrices and + // their lazily-built SpMV precompute caches, which can exceed the dense + // vectors in size. Overlap the release with the L_row/L_col MSMs. let (comm_L_row, comm_L_col) = rayon::join( || E::CE::commit(ck, &L_row, &E::Scalar::ZERO), - || E::CE::commit(ck, &L_col, &E::Scalar::ZERO), + || { + let comm = E::CE::commit(ck, &L_col, &E::Scalar::ZERO); + drop(z); + drop(S); + comm + }, ); // Absorb commitments to L_row and L_col @@ -1167,13 +867,29 @@ impl> RelaxedR1CSSNARKTrait for Relax let gamma = transcript.squeeze(b"g")?; let r = transcript.squeeze(b"r")?; - let (mut inner_batched_sc_inst, mem_res) = rayon::join( - || { - // Inner batched sum-check instance for: - // (a) ABC claim: factor·(v_A + c·v_B + c²·v_C) = Σ L_row(y) * (val_A + c·val_B + c²·val_C)(y) * L_col(y) - // (b) E claim: factor·eval_E = Σ eq(r_outer_full, y) * E(y) - // The claims are scaled by factor because the inner sum-check uses r_outer_full - // and eq(r_outer_full, j) = factor · eq(r_outer, j) for j < m. + #[cfg(feature = "logup-no-gkr")] + let ( + r_inner_batched, + sc_inner_batched, + eval_L_row, + eval_L_col, + eval_E, + eval_ts_row, + eval_ts_col, + eval_W, + eval_t_plus_r_inv_row, + eval_w_plus_r_inv_row, + eval_t_plus_r_inv_col, + eval_w_plus_r_inv_col, + comm_mem_oracles, + mem_oracles, + ) = { + // Build the inner-batched instance in parallel with the inverse-logup + // memory-check slot. The inner instance is: + // (a) ABC claim: factor·(v_A + c·v_B + c²·v_C) = Σ L_row(y) * (val_A + c·val_B + c²·val_C)(y) * L_col(y) + // (b) E claim: factor·eval_E = Σ eq(r_outer_full, y) * E(y) + // scaled by factor because the inner sum-check uses r_outer_full. + let build_inner = || { let val = zip_with!( par_iter, (pk.S_repr.val_A, pk.S_repr.val_B, pk.S_repr.val_C), @@ -1190,14 +906,15 @@ impl> RelaxedR1CSSNARKTrait for Relax r_outer_full.clone(), // eq challenges for factored eq (Gruen) E.clone(), ) - }, - || { - // Memory sum-check instance to prove L_row and L_col are well-formed - let (comm_mem_oracles, mem_oracles, mem_aux) = - MemorySumcheckInstance::::compute_oracles( + }; + + let (mut inner_batched_sc_inst, (mut mem, comm_mem_oracles, mem_oracles)) = { + let mem_res = rayon::join(build_inner, || { + // Inverse-logup: build the inverse oracles, commit, absorb, squeeze rho. + mem_check_logup::prove_step::( ck, - &r, - &gamma, + r, + gamma, &mem_row, &pk.S_repr.row, &L_row, @@ -1206,58 +923,135 @@ impl> RelaxedR1CSSNARKTrait for Relax &pk.S_repr.col, &L_col, &pk.S_repr.ts_col, - )?; - // absorb the commitments - transcript.absorb(b"l", &comm_mem_oracles.as_slice()); - - let rho = (0..num_rounds_inner) - .map(|_| transcript.squeeze(b"r")) - .collect::, NovaError>>()?; - - Ok::<_, NovaError>(( - MemorySumcheckInstance::new( - mem_oracles.clone(), - mem_aux, - rho, - pk.S_repr.ts_row.clone(), - pk.S_repr.ts_col.clone(), - ), - comm_mem_oracles, - mem_oracles, - )) - }, - ); + num_rounds_inner, + &mut transcript, + ) + }); + (mem_res.0, mem_res.1?) + }; - let (mut mem_sc_inst, comm_mem_oracles, mem_oracles) = mem_res?; + let mut witness_sc_inst = + WitnessBoundSumcheck::new(r_outer_full.clone(), W.clone(), num_vars); + let (sc_inner_batched, r_inner_batched, claims_mem, claims_inner_batched, claims_witness) = + Self::prove_helper( + &mut mem, + &mut inner_batched_sc_inst, + &mut witness_sc_inst, + &mut transcript, + )?; + + let eval_L_row = claims_inner_batched[0][0]; + let eval_L_col = claims_inner_batched[0][1]; + let eval_E = claims_inner_batched[1][0]; + let ( + eval_t_plus_r_inv_row, + eval_w_plus_r_inv_row, + eval_ts_row, + eval_t_plus_r_inv_col, + eval_w_plus_r_inv_col, + eval_ts_col, + ) = ( + claims_mem[0][0], + claims_mem[0][1], + claims_mem[0][2], + claims_mem[1][0], + claims_mem[1][1], + claims_mem[1][2], + ); + let eval_W = claims_witness[0][0]; - // Witness bound sum-check using r_outer_full as the random evaluation point - let mut witness_sc_inst = - WitnessBoundSumcheck::new(r_outer_full.clone(), W.clone(), S.num_vars); + ( + r_inner_batched, + sc_inner_batched, + eval_L_row, + eval_L_col, + eval_E, + eval_ts_row, + eval_ts_col, + eval_W, + eval_t_plus_r_inv_row, + eval_w_plus_r_inv_row, + eval_t_plus_r_inv_col, + eval_w_plus_r_inv_col, + comm_mem_oracles, + mem_oracles, + ) + }; - // ----------------------------------------------------------------------- - // Step 3: Run the batched inner batched sum-check (3 instances) - // ----------------------------------------------------------------------- - let (sc_inner_batched, r_inner_batched, claims_mem, claims_inner_batched, claims_witness) = - Self::prove_helper( - &mut mem_sc_inst, - &mut inner_batched_sc_inst, - &mut witness_sc_inst, + #[cfg(not(feature = "logup-no-gkr"))] + let ( + r_inner_batched, + mem_check_gkr_fused, + eval_L_row, + eval_L_col, + eval_E, + eval_ts_row, + eval_ts_col, + eval_W, + ) = { + let val = zip_with!( + par_iter, + (pk.S_repr.val_A, pk.S_repr.val_B, pk.S_repr.val_C), + |v_a, v_b, v_c| *v_a + c * *v_b + c * c * *v_c + ) + .collect::>(); + let masked_eq = + MaskedEqPolynomial::new(&EqPolynomial::new(r_outer_full.clone()), num_vars.log_2()).evals(); + let inner_inputs = mem_check_logup_gkr_fused::FusedInnerInputs { + L_row: L_row.clone(), + L_col: L_col.clone(), + val, + E: E.clone(), + masked_eq, + W: W.clone(), + q: r_outer_full.clone(), + claim_abc: factor + * (eval_Az_at_r_outer + c * eval_Bz_at_r_outer + c * c * eval_Cz_at_r_outer), + claim_e: factor * eval_E_at_r_outer, + claim_w: E::Scalar::ZERO, + }; + let witness = MemCheckWitness:: { + mem_row: &mem_row, + mem_col: &mem_col, + L_row: &L_row, + L_col: &L_col, + addr_row: &pk.S_repr.row, + addr_col: &pk.S_repr.col, + ts_row: &pk.S_repr.ts_row, + ts_col: &pk.S_repr.ts_col, + }; + let (mem_check_gkr_fused, r_shared, endpoints) = mem_check_logup_gkr::prove_step_fused::( + witness, + gamma, + r, + inner_inputs, &mut transcript, )?; + // Every column the batch opening needs at r_shared already came out of the + // fused sumcheck: L_row/L_col/E/W are the Inner endpoints, ts_row/ts_col are + // the row_table/col_table numerators folded from the GKR splits. No extra + // O(N) opening here. + let (eval_L_row, eval_L_col, eval_E, eval_W, eval_ts_row, eval_ts_col) = ( + endpoints.L_row, + endpoints.L_col, + endpoints.E, + endpoints.W, + endpoints.ts_row, + endpoints.ts_col, + ); + let r_inner_batched = r_shared; - // Claims from the inner batched sum-check - let eval_L_row = claims_inner_batched[0][0]; - let eval_L_col = claims_inner_batched[0][1]; - let eval_E = claims_inner_batched[1][0]; // E(r_inner_batched) — rerandomized to open at same point - - let eval_t_plus_r_inv_row = claims_mem[0][0]; - let eval_w_plus_r_inv_row = claims_mem[0][1]; - let eval_ts_row = claims_mem[0][2]; - - let eval_t_plus_r_inv_col = claims_mem[1][0]; - let eval_w_plus_r_inv_col = claims_mem[1][1]; - let eval_ts_col = claims_mem[1][2]; - let eval_W = claims_witness[0][0]; + ( + r_inner_batched, + mem_check_gkr_fused, + eval_L_row, + eval_L_col, + eval_E, + eval_ts_row, + eval_ts_col, + eval_W, + ) + }; // Compute evaluations at r_inner_batched that did not come for free from the sum-check let (eval_val_A, eval_val_B, eval_val_C, eval_row, eval_col) = { @@ -1274,8 +1068,14 @@ impl> RelaxedR1CSSNARKTrait for Relax (e[0], e[1], e[2], e[3], e[4]) }; - // All evaluations are at r_inner_batched — fold into one claim for batch PCS opening - let eval_vec = vec![ + // All evaluations are at r_inner_batched — fold into one claim for batch PCS + // opening. Shared columns come first (both memory-check implementations open + // them); the four inverse-oracle columns, present only under inverse-logup, + // are appended at the end. The batch is an order-agnostic RLC, so any + // ordering is fine as long as prove and verify agree — see the verifier's + // matching construction. + #[cfg_attr(not(feature = "logup-no-gkr"), allow(unused_mut))] + let mut eval_vec = vec![ eval_W, eval_E, eval_L_row, @@ -1283,17 +1083,13 @@ impl> RelaxedR1CSSNARKTrait for Relax eval_val_A, eval_val_B, eval_val_C, - eval_t_plus_r_inv_row, eval_row, - eval_w_plus_r_inv_row, eval_ts_row, - eval_t_plus_r_inv_col, eval_col, - eval_w_plus_r_inv_col, eval_ts_col, ]; - - let comm_vec = [ + #[cfg_attr(not(feature = "logup-no-gkr"), allow(unused_mut))] + let mut comm_vec = vec![ U.comm_W, U.comm_E, comm_L_row, @@ -1301,16 +1097,13 @@ impl> RelaxedR1CSSNARKTrait for Relax pk.S_comm.comm_val_A, pk.S_comm.comm_val_B, pk.S_comm.comm_val_C, - comm_mem_oracles[0], pk.S_comm.comm_row, - comm_mem_oracles[1], pk.S_comm.comm_ts_row, - comm_mem_oracles[2], pk.S_comm.comm_col, - comm_mem_oracles[3], pk.S_comm.comm_ts_col, ]; - let poly_vec = [ + #[cfg_attr(not(feature = "logup-no-gkr"), allow(unused_mut))] + let mut poly_vec: Vec<&Vec> = vec![ &W, &E, &L_row, @@ -1318,15 +1111,23 @@ impl> RelaxedR1CSSNARKTrait for Relax &pk.S_repr.val_A, &pk.S_repr.val_B, &pk.S_repr.val_C, - mem_oracles[0].as_ref(), &pk.S_repr.row, - mem_oracles[1].as_ref(), &pk.S_repr.ts_row, - mem_oracles[2].as_ref(), &pk.S_repr.col, - mem_oracles[3].as_ref(), &pk.S_repr.ts_col, ]; + #[cfg(feature = "logup-no-gkr")] + { + eval_vec.extend([ + eval_t_plus_r_inv_row, + eval_w_plus_r_inv_row, + eval_t_plus_r_inv_col, + eval_w_plus_r_inv_col, + ]); + comm_vec.extend(comm_mem_oracles); + poly_vec.extend(mem_oracles.iter()); + } + transcript.absorb(b"e", &eval_vec.as_slice()); // comm_vec is already in the transcript let c = transcript.squeeze(b"c")?; let w: PolyEvalWitness = PolyEvalWitness::batch(&poly_vec, &c); @@ -1347,10 +1148,19 @@ impl> RelaxedR1CSSNARKTrait for Relax comm_L_row, comm_L_col, - comm_t_plus_r_inv_row: comm_mem_oracles[0], - comm_w_plus_r_inv_row: comm_mem_oracles[1], - comm_t_plus_r_inv_col: comm_mem_oracles[2], - comm_w_plus_r_inv_col: comm_mem_oracles[3], + #[cfg(feature = "logup-no-gkr")] + mem_check: mem_check_logup::LogupProofData { + comm_t_plus_r_inv_row: comm_mem_oracles[0], + comm_w_plus_r_inv_row: comm_mem_oracles[1], + comm_t_plus_r_inv_col: comm_mem_oracles[2], + comm_w_plus_r_inv_col: comm_mem_oracles[3], + eval_t_plus_r_inv_row, + eval_w_plus_r_inv_row, + eval_t_plus_r_inv_col, + eval_w_plus_r_inv_col, + }, + #[cfg(not(feature = "logup-no-gkr"))] + mem_check_gkr_fused, sc_outer, @@ -1359,6 +1169,7 @@ impl> RelaxedR1CSSNARKTrait for Relax eval_Cz_at_r_outer, eval_E_at_r_outer, + #[cfg(feature = "logup-no-gkr")] sc_inner_batched, eval_E, @@ -1370,14 +1181,9 @@ impl> RelaxedR1CSSNARKTrait for Relax eval_W, - eval_t_plus_r_inv_row, eval_row, - eval_w_plus_r_inv_row, eval_ts_row, - eval_col, - eval_t_plus_r_inv_col, - eval_w_plus_r_inv_col, eval_ts_col, eval_arg, @@ -1456,153 +1262,131 @@ impl> RelaxedR1CSSNARKTrait for Relax let gamma = transcript.squeeze(b"g")?; let r = transcript.squeeze(b"r")?; - transcript.absorb( - b"l", - &vec![ - self.comm_t_plus_r_inv_row, - self.comm_w_plus_r_inv_row, - self.comm_t_plus_r_inv_col, - self.comm_w_plus_r_inv_col, - ] - .as_slice(), - ); + #[cfg(feature = "logup-no-gkr")] + let r_inner_batched = { + // Memory-check transcript phase: absorb the inverse-oracle commitments and + // squeeze the memory sumcheck's eq randomness `rho` before the inner + // sumcheck's `s` challenge. + let rho = + mem_check_logup::verify_pre_inner::(&self.mem_check, num_rounds_inner, &mut transcript)?; + + // Batched-inner claim layout for inverse-logup: + // memory-check [0, 6), ABC at 6, E at 7, witness at 8. + let mem_claims = mem_check_logup::NUM_MEM_CLAIMS; + let abc_idx = mem_claims; + let e_idx = mem_claims + 1; + let wit_idx = mem_claims + 2; + let num_claims = mem_claims + 3; + let s = transcript.squeeze(b"r")?; + let coeffs = powers::(&s, num_claims); + + let claim_inner_batched_ABC = factor + * (self.eval_Az_at_r_outer + c * self.eval_Bz_at_r_outer + c * c * self.eval_Cz_at_r_outer); + let mem_initial = mem_check_logup::verify_initial_claim::(&coeffs); + let claim = coeffs[abc_idx] * claim_inner_batched_ABC + + coeffs[e_idx] * factor * self.eval_E_at_r_outer + + mem_initial; + + let (claim_sc_inner_batched_final, r_inner_batched) = + self + .sc_inner_batched + .verify(claim, num_rounds_inner, 3, &mut transcript)?; + + let claim_sc_inner_batched_expected = { + let eq_r_outer = EqPolynomial::new(r_outer_full.clone()); + let eq_r_outer_at_r_inner_batched = eq_r_outer.evaluate(&r_inner_batched); + let taus_masked_bound_r_inner_batched = + MaskedEqPolynomial::new(&eq_r_outer, vk.num_vars.log_2()).evaluate(&r_inner_batched); + + let public_io: Vec = vec![U.u].into_iter().chain(U.X.iter().cloned()).collect(); + let mem_final = mem_check_logup::verify_final_claim::( + &self.mem_check, + &coeffs, + rho, + gamma, + r, + &r_outer_full, + &r_inner_batched, + num_rounds_inner, + vk.num_vars, + vk.S_comm.N, + self.eval_W, + self.eval_L_row, + self.eval_L_col, + self.eval_row, + self.eval_col, + self.eval_ts_row, + self.eval_ts_col, + &public_io, + ); + + let claim_inner_batched_ABC_final = coeffs[abc_idx] + * self.eval_L_row + * self.eval_L_col + * (self.eval_val_A + c * self.eval_val_B + c * c * self.eval_val_C); + let claim_inner_batched_E_final = + coeffs[e_idx] * eq_r_outer_at_r_inner_batched * self.eval_E; + let claim_witness_final = coeffs[wit_idx] * taus_masked_bound_r_inner_batched * self.eval_W; + + mem_final + + claim_inner_batched_ABC_final + + claim_inner_batched_E_final + + claim_witness_final + }; - let rho = (0..num_rounds_inner) - .map(|_| transcript.squeeze(b"r")) - .collect::, NovaError>>()?; + if claim_sc_inner_batched_expected != claim_sc_inner_batched_final { + return Err(NovaError::InvalidSumcheckProof); + } - // 9 claims: 6 memory + 2 inner (ABC + E) + 1 witness - let num_claims = 9; - let s = transcript.squeeze(b"r")?; - let coeffs = powers::(&s, num_claims); - - // Compute the combined initial claim - // Claims 0-5: memory (all zero) - // Claim 6: inner ABC = factor * (eval_Az + c * eval_Bz + c² * eval_Cz) - // Claim 7: inner E = factor * eval_E - // Claim 8: witness (zero) - // The factor accounts for zero-padding: eval_P(r_outer_full) = factor * eval_P(r_outer) - let claim_inner_batched_ABC = factor - * (self.eval_Az_at_r_outer + c * self.eval_Bz_at_r_outer + c * c * self.eval_Cz_at_r_outer); - let claim = coeffs[6] * claim_inner_batched_ABC + coeffs[7] * factor * self.eval_E_at_r_outer; - - // Verify inner batched sum-check - let (claim_sc_inner_batched_final, r_inner_batched) = - self - .sc_inner_batched - .verify(claim, num_rounds_inner, 3, &mut transcript)?; - - // Verify inner batched sum-check final claim - let claim_sc_inner_batched_expected = { - let rand_eq_bound_r_inner_batched = EqPolynomial::new(rho).evaluate(&r_inner_batched); - - // eq(r_outer_full, r_inner_batched) for the E claim and memory row address check - let eq_r_outer = EqPolynomial::new(r_outer_full.clone()); - let eq_r_outer_at_r_inner_batched = eq_r_outer.evaluate(&r_inner_batched); - - // masked eq for witness bound check (using r_outer_full as random point) - let taus_masked_bound_r_inner_batched = - MaskedEqPolynomial::new(&eq_r_outer, vk.num_vars.log_2()).evaluate(&r_inner_batched); - - let eval_t_plus_r_row = { - let eval_addr_row = IdentityPolynomial::new(num_rounds_inner).evaluate(&r_inner_batched); - let eval_val_row = eq_r_outer_at_r_inner_batched; // mem_row = eq(r_outer_full, ·) - let eval_t = eval_addr_row + gamma * eval_val_row; - eval_t + r - }; + r_inner_batched + }; - let eval_w_plus_r_row = { - let eval_addr_row = self.eval_row; - let eval_val_row = self.eval_L_row; - let eval_w = eval_addr_row + gamma * eval_val_row; - eval_w + r + #[cfg(not(feature = "logup-no-gkr"))] + let r_inner_batched = { + let public_io: Vec = core::iter::once(U.u).chain(U.X.iter().cloned()).collect(); + let claim_abc = factor + * (self.eval_Az_at_r_outer + c * self.eval_Bz_at_r_outer + c * c * self.eval_Cz_at_r_outer); + let claim_e = factor * self.eval_E_at_r_outer; + let eval_val = self.eval_val_A + c * self.eval_val_B + c * c * self.eval_val_C; + let ctx = mem_check_logup_gkr::FusedVerifyContext:: { + gamma, + r, + r_outer_full: &r_outer_full, + public_io: &public_io, + num_masked_vars: vk.num_vars.log_2(), + snark_n_log: vk.S_comm.N.log_2(), + two_num_vars_log: (2 * vk.num_vars).log_2(), }; - - let eval_t_plus_r_col = { - let eval_addr_col = IdentityPolynomial::new(num_rounds_inner).evaluate(&r_inner_batched); - - // memory contents is z, so we compute eval_Z from eval_W and eval_X - let eval_val_col = { - // r_inner_batched was padded, so we now remove the padding - let (factor, r_inner_batched_unpad) = { - let l = vk.S_comm.N.log_2() - (2 * vk.num_vars).log_2(); - - let mut factor = E::Scalar::ONE; - for r_p in r_inner_batched.iter().take(l) { - factor *= E::Scalar::ONE - r_p - } - - let r_inner_batched_unpad = r_inner_batched[l..].to_vec(); - - (factor, r_inner_batched_unpad) - }; - - let eval_X = { - // public IO is (u, X) - let X = vec![U.u] - .into_iter() - .chain(U.X.iter().cloned()) - .collect::>(); - - // evaluate the sparse polynomial at r_inner_batched_unpad[1..] - let poly_X = SparsePolynomial::new(r_inner_batched_unpad.len() - 1, X); - poly_X.evaluate(&r_inner_batched_unpad[1..]) - }; - - self.eval_W + factor * r_inner_batched_unpad[0] * eval_X - }; - let eval_t = eval_addr_col + gamma * eval_val_col; - eval_t + r + let claims = mem_check_logup_gkr::FusedInnerClaims:: { + abc: claim_abc, + e: claim_e, + w: E::Scalar::ZERO, }; - - let eval_w_plus_r_col = { - let eval_addr_col = self.eval_col; - let eval_val_col = self.eval_L_col; - let eval_w = eval_addr_col + gamma * eval_val_col; - eval_w + r + let endpoints = mem_check_logup_gkr::FusedEndpointClaims:: { + val: eval_val, + E: self.eval_E, + W: self.eval_W, + L_row: self.eval_L_row, + L_col: self.eval_L_col, + row: self.eval_row, + col: self.eval_col, + ts_row: self.eval_ts_row, + ts_col: self.eval_ts_col, }; - - // Memory claims (coeffs 0-5) - let claim_mem_final_expected: E::Scalar = coeffs[0] - * (self.eval_t_plus_r_inv_row - self.eval_w_plus_r_inv_row) - + coeffs[1] * (self.eval_t_plus_r_inv_col - self.eval_w_plus_r_inv_col) - + coeffs[2] - * (rand_eq_bound_r_inner_batched - * (self.eval_t_plus_r_inv_row * eval_t_plus_r_row - self.eval_ts_row)) - + coeffs[3] - * (rand_eq_bound_r_inner_batched - * (self.eval_w_plus_r_inv_row * eval_w_plus_r_row - E::Scalar::ONE)) - + coeffs[4] - * (rand_eq_bound_r_inner_batched - * (self.eval_t_plus_r_inv_col * eval_t_plus_r_col - self.eval_ts_col)) - + coeffs[5] - * (rand_eq_bound_r_inner_batched - * (self.eval_w_plus_r_inv_col * eval_w_plus_r_col - E::Scalar::ONE)); - - // Inner batched ABC claim (coeff 6): L_row * L_col * (val_A + c·val_B + c²·val_C) - let claim_inner_batched_ABC_final = coeffs[6] - * self.eval_L_row - * self.eval_L_col - * (self.eval_val_A + c * self.eval_val_B + c * c * self.eval_val_C); - - // Inner batched E claim (coeff 7): eq(r_outer_full, r_inner_batched) * E(r_inner_batched) - let claim_inner_batched_E_final = coeffs[7] * eq_r_outer_at_r_inner_batched * self.eval_E; - - // Witness claim (coeff 8) - let claim_witness_final = coeffs[8] * taus_masked_bound_r_inner_batched * self.eval_W; - - claim_mem_final_expected - + claim_inner_batched_ABC_final - + claim_inner_batched_E_final - + claim_witness_final + mem_check_logup_gkr::verify_step_fused::( + &self.mem_check_gkr_fused, + &ctx, + &claims, + &endpoints, + &mut transcript, + )? }; - if claim_sc_inner_batched_expected != claim_sc_inner_batched_final { - return Err(NovaError::InvalidSumcheckProof); - } - - // Verify polynomial openings — all at r_inner_batched - let eval_vec = vec![ + // Verify polynomial openings — all at r_inner_batched. Shared columns first, + // the inverse-oracle columns (inverse-logup only) appended at the end. Must + // match the prover's column ordering exactly. + #[cfg_attr(not(feature = "logup-no-gkr"), allow(unused_mut))] + let mut eval_vec = vec![ self.eval_W, self.eval_E, self.eval_L_row, @@ -1610,16 +1394,13 @@ impl> RelaxedR1CSSNARKTrait for Relax self.eval_val_A, self.eval_val_B, self.eval_val_C, - self.eval_t_plus_r_inv_row, self.eval_row, - self.eval_w_plus_r_inv_row, self.eval_ts_row, - self.eval_t_plus_r_inv_col, self.eval_col, - self.eval_w_plus_r_inv_col, self.eval_ts_col, ]; - let comm_vec = [ + #[cfg_attr(not(feature = "logup-no-gkr"), allow(unused_mut))] + let mut comm_vec = vec![ U.comm_W, U.comm_E, self.comm_L_row, @@ -1627,15 +1408,27 @@ impl> RelaxedR1CSSNARKTrait for Relax vk.S_comm.comm_val_A, vk.S_comm.comm_val_B, vk.S_comm.comm_val_C, - self.comm_t_plus_r_inv_row, vk.S_comm.comm_row, - self.comm_w_plus_r_inv_row, vk.S_comm.comm_ts_row, - self.comm_t_plus_r_inv_col, vk.S_comm.comm_col, - self.comm_w_plus_r_inv_col, vk.S_comm.comm_ts_col, ]; + #[cfg(feature = "logup-no-gkr")] + { + eval_vec.extend([ + self.mem_check.eval_t_plus_r_inv_row, + self.mem_check.eval_w_plus_r_inv_row, + self.mem_check.eval_t_plus_r_inv_col, + self.mem_check.eval_w_plus_r_inv_col, + ]); + comm_vec.extend([ + self.mem_check.comm_t_plus_r_inv_row, + self.mem_check.comm_w_plus_r_inv_row, + self.mem_check.comm_t_plus_r_inv_col, + self.mem_check.comm_w_plus_r_inv_col, + ]); + } + transcript.absorb(b"e", &eval_vec.as_slice()); // comm_vec is already in the transcript let c = transcript.squeeze(b"c")?; let u: PolyEvalInstance = diff --git a/src/spartan/sumcheck.rs b/src/spartan/sumcheck.rs index 27a38dcf3..9290f4945 100644 --- a/src/spartan/sumcheck.rs +++ b/src/spartan/sumcheck.rs @@ -1,4 +1,5 @@ use crate::{ + constants::PARALLEL_THRESHOLD, errors::NovaError, spartan::{ polys::{ @@ -10,6 +11,7 @@ use crate::{ traits::{Engine, TranscriptEngineTrait}, }; use ff::{Field, PrimeField}; +use itertools::Itertools as _; use rayon::prelude::*; use serde::{Deserialize, Serialize}; @@ -30,6 +32,21 @@ pub trait SumcheckEngine: Send + Sync { /// For degree-2 (quadratic) claims: [p(0), 0, p(-1)] fn evaluation_points(&mut self) -> Vec>; + /// Optional hook: once the batched prover's linear-combination coefficients + /// are known (squeezed inside `prove_helper`), an instance may collapse its + /// several equally-shaped claims into a single random linear combination so it + /// scans/binds one polynomial per round instead of many. `coeffs` are exactly + /// this instance's slice of the batch coefficients (same order as + /// [`Self::initial_claims`]). The default is a no-op. + /// + /// Correctness contract: after fusing, [`Self::evaluation_points`] must still + /// return one triple per original claim so positional `Σ coeffs[i]·evals[i]` + /// in the batched prover is unchanged. Fusing instances therefore return the + /// combined triple in slot 0 (whose coefficient is 1 when it leads the batch) + /// and zeros elsewhere, which is byte-identical to computing each triple + /// separately and summing. + fn fuse_with_coeffs(&mut self, _coeffs: &[E::Scalar]) {} + /// bounds a variable in the constituent polynomials fn bound(&mut self, r: &E::Scalar); @@ -406,6 +423,62 @@ impl SumcheckProof { ) } + /// Quadratic (`poly_A * poly_B`) evaluation points that also cache each + /// top-variable delta into the high halves, mirroring + /// [`Self::compute_eval_points_cubic_with_cached_deltas`]. The caller must bind + /// both polynomials with + /// `MultilinearPolynomial::bind_poly_var_top_with_cached_delta` afterwards. + /// + /// Returns `(eval_0, eval_inf)`. + #[inline] + pub fn compute_eval_points_quadratic_with_cached_deltas( + poly_A: &mut MultilinearPolynomial, + poly_B: &mut MultilinearPolynomial, + ) -> (E::Scalar, E::Scalar) { + let len = poly_A.len() / 2; + assert_eq!(poly_B.len(), poly_A.len()); + + let (a_low, a_delta) = poly_A.Z.split_at_mut(len); + let (b_low, b_delta) = poly_B.Z.split_at_mut(len); + + let eval = + |a_low: &E::Scalar, a_delta: &mut E::Scalar, b_low: &E::Scalar, b_delta: &mut E::Scalar| { + *a_delta -= a_low; + *b_delta -= b_low; + // eval_0 = A_lo·B_lo; eval_inf = A(-1)·B(-1) = (A_lo - dA)·(B_lo - dB). + (*a_low * *b_low, (*a_low - *a_delta) * (*b_low - *b_delta)) + }; + + if len < PARALLEL_THRESHOLD { + zip_with!( + ( + a_low.iter(), + a_delta.iter_mut(), + b_low.iter(), + b_delta.iter_mut() + ), + |a_low, a_delta, b_low, b_delta| eval(a_low, a_delta, b_low, b_delta) + ) + .fold((E::Scalar::ZERO, E::Scalar::ZERO), |acc, item| { + (acc.0 + item.0, acc.1 + item.1) + }) + } else { + zip_with!( + ( + a_low.par_iter(), + a_delta.par_iter_mut(), + b_low.par_iter(), + b_delta.par_iter_mut() + ), + |a_low, a_delta, b_low, b_delta| eval(a_low, a_delta, b_low, b_delta) + ) + .reduce( + || (E::Scalar::ZERO, E::Scalar::ZERO), + |a, b| (a.0 + b.0, a.1 + b.1), + ) + } + } + /// Computes evaluation points for a cubic product sumcheck round (`poly_A * poly_B * poly_C`). /// /// Returns `(eval_0, cubic_coeff, eval_inf)` where: @@ -442,6 +515,85 @@ impl SumcheckProof { ) } + /// Computes cubic evaluation points while replacing every polynomial's high + /// half with its top-variable delta. + /// + /// The caller must bind all three polynomials with + /// `MultilinearPolynomial::bind_poly_var_top_with_cached_delta` before reading + /// their high halves again. + /// + /// Returns `(eval_0, cubic_coeff, eval_inf)`, the same layout as + /// [`Self::compute_eval_points_cubic`]. + #[inline] + pub fn compute_eval_points_cubic_with_cached_deltas( + poly_A: &mut MultilinearPolynomial, + poly_B: &mut MultilinearPolynomial, + poly_C: &mut MultilinearPolynomial, + ) -> (E::Scalar, E::Scalar, E::Scalar) { + let len = poly_A.len() / 2; + assert_eq!(poly_B.len(), poly_A.len()); + assert_eq!(poly_C.len(), poly_A.len()); + + let (a_low, a_delta) = poly_A.Z.split_at_mut(len); + let (b_low, b_delta) = poly_B.Z.split_at_mut(len); + let (c_low, c_delta) = poly_C.Z.split_at_mut(len); + + let eval = |a_low: &E::Scalar, + a_delta: &mut E::Scalar, + b_low: &E::Scalar, + b_delta: &mut E::Scalar, + c_low: &E::Scalar, + c_delta: &mut E::Scalar| { + *a_delta -= a_low; + *b_delta -= b_low; + *c_delta -= c_low; + + ( + *a_low * *b_low * *c_low, + *a_delta * *b_delta * *c_delta, + (*a_low - *a_delta) * (*b_low - *b_delta) * (*c_low - *c_delta), + ) + }; + + if len < PARALLEL_THRESHOLD { + zip_with!( + ( + a_low.iter(), + a_delta.iter_mut(), + b_low.iter(), + b_delta.iter_mut(), + c_low.iter(), + c_delta.iter_mut() + ), + |a_low, a_delta, b_low, b_delta, c_low, c_delta| eval( + a_low, a_delta, b_low, b_delta, c_low, c_delta + ) + ) + .fold( + (E::Scalar::ZERO, E::Scalar::ZERO, E::Scalar::ZERO), + |acc, item| (acc.0 + item.0, acc.1 + item.1, acc.2 + item.2), + ) + } else { + zip_with!( + ( + a_low.par_iter(), + a_delta.par_iter_mut(), + b_low.par_iter(), + b_delta.par_iter_mut(), + c_low.par_iter(), + c_delta.par_iter_mut() + ), + |a_low, a_delta, b_low, b_delta, c_low, c_delta| eval( + a_low, a_delta, b_low, b_delta, c_low, c_delta + ) + ) + .reduce( + || (E::Scalar::ZERO, E::Scalar::ZERO, E::Scalar::ZERO), + |a, b| (a.0 + b.0, a.1 + b.1, a.2 + b.2), + ) + } + } + /// Prove poly_A * poly_B - poly_C pub fn prove_cubic_with_three_inputs( claim: &E::Scalar, @@ -585,8 +737,11 @@ pub mod eq_sumcheck { //! //! The claim-derived evaluation points (computing only 2 N-scaling sums per round //! instead of 3) follow BDDT (eprint 2025/1117, Section 6.2). - use crate::{spartan::polys::multilinear::MultilinearPolynomial, traits::Engine}; - use ff::Field; + use crate::{ + constants::PARALLEL_THRESHOLD, spartan::polys::multilinear::MultilinearPolynomial, + traits::Engine, + }; + use ff::{Field, PrimeField}; use rayon::{iter::ZipEq, prelude::*, slice::Iter}; /// Instance for optimized equality polynomial sumcheck. @@ -603,6 +758,179 @@ pub mod eq_sumcheck { eq_tau_0_a_inf: Vec<(E::Scalar, E::Scalar, E::Scalar)>, } + struct LogupGateCell<'a, Scalar> { + nl_0: Scalar, + nl_delta: &'a mut Scalar, + nr_0: Scalar, + nr_delta: &'a mut Scalar, + dl_0: Scalar, + dl_delta: &'a mut Scalar, + dr_0: Scalar, + dr_delta: &'a mut Scalar, + } + + impl LogupGateCell<'_, Scalar> { + fn cache_and_evaluate( + self, + weights: (Scalar, Scalar), + ) -> (Scalar, Scalar) { + *self.nl_delta -= self.nl_0; + *self.nr_delta -= self.nr_0; + *self.dl_delta -= self.dl_0; + *self.dr_delta -= self.dr_0; + + let (w_num, w_den) = weights; + ( + if EVALUATE_T_0 { + w_num * (self.nl_0 * self.dr_0 + self.nr_0 * self.dl_0) + w_den * (self.dl_0 * self.dr_0) + } else { + Scalar::ZERO + }, + w_num * (*self.nl_delta * *self.dr_delta + *self.nr_delta * *self.dl_delta) + + w_den * (*self.dl_delta * *self.dr_delta), + ) + } + } + + struct LogupGateInstanceSlices<'a, Scalar> { + nl_low: &'a [Scalar], + nl_delta: &'a mut [Scalar], + nr_low: &'a [Scalar], + nr_delta: &'a mut [Scalar], + dl_low: &'a [Scalar], + dl_delta: &'a mut [Scalar], + dr_low: &'a [Scalar], + dr_delta: &'a mut [Scalar], + } + + impl<'a, Scalar: PrimeField> LogupGateInstanceSlices<'a, Scalar> { + fn new( + nl: &'a mut MultilinearPolynomial, + nr: &'a mut MultilinearPolynomial, + dl: &'a mut MultilinearPolynomial, + dr: &'a mut MultilinearPolynomial, + ) -> Self { + let half = nl.Z.len() / 2; + let (nl_low, nl_delta) = nl.Z.split_at_mut(half); + let (nr_low, nr_delta) = nr.Z.split_at_mut(half); + let (dl_low, dl_delta) = dl.Z.split_at_mut(half); + let (dr_low, dr_delta) = dr.Z.split_at_mut(half); + Self { + nl_low, + nl_delta, + nr_low, + nr_delta, + dl_low, + dl_delta, + dr_low, + dr_delta, + } + } + + fn par_iter_mut(&mut self) -> impl IndexedParallelIterator> { + zip_with!( + ( + self.nl_low.par_iter(), + self.nl_delta.par_iter_mut(), + self.nr_low.par_iter(), + self.nr_delta.par_iter_mut(), + self.dl_low.par_iter(), + self.dl_delta.par_iter_mut(), + self.dr_low.par_iter(), + self.dr_delta.par_iter_mut() + ), + |nl_0, nl_delta, nr_0, nr_delta, dl_0, dl_delta, dr_0, dr_delta| LogupGateCell { + nl_0: *nl_0, + nl_delta, + nr_0: *nr_0, + nr_delta, + dl_0: *dl_0, + dl_delta, + dr_0: *dr_0, + dr_delta, + } + ) + } + } + + fn cache_four_logup_gate_deltas( + nl: &mut [MultilinearPolynomial], + nr: &mut [MultilinearPolynomial], + dl: &mut [MultilinearPolynomial], + dr: &mut [MultilinearPolynomial], + weights: &[(Scalar, Scalar)], + factor: &Factor, + ) -> (Scalar, Scalar) + where + Scalar: PrimeField, + Factor: Fn(usize) -> Scalar + Sync, + { + let mut instances: Vec<_> = nl + .iter_mut() + .zip(nr.iter_mut()) + .zip(dl.iter_mut()) + .zip(dr.iter_mut()) + .map(|(((nl, nr), dl), dr)| LogupGateInstanceSlices::new(nl, nr, dl, dr)) + .collect(); + let [i0, i1, i2, i3] = instances.as_mut_slice() else { + unreachable!("the ppSNARK Logup-GKR gate has four sub-instances"); + }; + let [w0, w1, w2, w3] = weights else { + unreachable!("the ppSNARK Logup-GKR gate has four weight pairs"); + }; + + zip_with!( + ( + i0.par_iter_mut(), + i1.par_iter_mut(), + i2.par_iter_mut(), + i3.par_iter_mut() + ), + |c0, c1, c2, c3| { + let g0 = c0.cache_and_evaluate::(*w0); + let g1 = c1.cache_and_evaluate::(*w1); + let g2 = c2.cache_and_evaluate::(*w2); + let g3 = c3.cache_and_evaluate::(*w3); + (g0.0 + g1.0 + g2.0 + g3.0, g0.1 + g1.1 + g2.1 + g3.1) + } + ) + .enumerate() + .map(|(id, gate)| { + let eq_factor = factor(id); + (gate.0 * eq_factor, gate.1 * eq_factor) + }) + .reduce( + || (Scalar::ZERO, Scalar::ZERO), + |a, b| (a.0 + b.0, a.1 + b.1), + ) + } + + /// Caches four Logup-GKR instances' deltas, optionally taking `t(0)` from the + /// caller instead of evaluating it over the low halves. + #[allow(clippy::too_many_arguments)] + fn cache_four_logup_gate_deltas_with_t_0( + nl: &mut [MultilinearPolynomial], + nr: &mut [MultilinearPolynomial], + dl: &mut [MultilinearPolynomial], + dr: &mut [MultilinearPolynomial], + weights: &[(Scalar, Scalar)], + t_0: Option, + factor: &Factor, + ) -> (Scalar, Scalar) + where + Scalar: PrimeField, + Factor: Fn(usize) -> Scalar + Sync, + { + match t_0 { + Some(t_0) => { + let (_, t_inf) = + cache_four_logup_gate_deltas::(nl, nr, dl, dr, weights, factor); + (t_0, t_inf) + } + None => cache_four_logup_gate_deltas::(nl, nr, dl, dr, weights, factor), + } + } + impl EqSumCheckInstance { /// Creates a new EqSumCheckInstance from tau values. pub fn new(taus: Vec) -> Self { @@ -893,6 +1221,301 @@ pub mod eq_sumcheck { (s_0, s_leading, s_m1) } + /// Evaluates `eq(tau, X)` times a weighted sum of fractional-add gates + /// without modifying the input MLEs. + /// + /// Each instance contributes + /// `w_num * (nL * dR + nR * dL) + w_den * dL * dR`. The degree-2 inner + /// polynomial uses BDDT claim derivation from `t(0)` and `t(inf)`, falling + /// back to a third sum when `tau = 0`. + #[inline] + #[allow(clippy::too_many_arguments)] + pub fn evaluation_points_logup_gate( + &self, + nl: &[MultilinearPolynomial], + nr: &[MultilinearPolynomial], + dl: &[MultilinearPolynomial], + dr: &[MultilinearPolynomial], + weights: &[(E::Scalar, E::Scalar)], + claim: E::Scalar, + ) -> (E::Scalar, E::Scalar, E::Scalar) { + let m = nl.len(); + assert!(m > 0); + assert_eq!(m, nr.len()); + assert_eq!(m, dl.len()); + assert_eq!(m, dr.len()); + assert_eq!(m, weights.len()); + assert_eq!(nl[0].Z.len() % 2, 0); + + let half_p = nl[0].Z.len() / 2; + let gate_0_inf = |id: usize| -> (E::Scalar, E::Scalar) { + let mut sum_0 = E::Scalar::ZERO; + let mut sum_inf = E::Scalar::ZERO; + for i in 0..m { + let (w_num, w_den) = weights[i]; + let nl_0 = nl[i].Z[id]; + let nr_0 = nr[i].Z[id]; + let dl_0 = dl[i].Z[id]; + let dr_0 = dr[i].Z[id]; + let nl_s = nl[i].Z[id + half_p] - nl_0; + let nr_s = nr[i].Z[id + half_p] - nr_0; + let dl_s = dl[i].Z[id + half_p] - dl_0; + let dr_s = dr[i].Z[id + half_p] - dr_0; + sum_0 += w_num * (nl_0 * dr_0 + nr_0 * dl_0) + w_den * (dl_0 * dr_0); + sum_inf += w_num * (nl_s * dr_s + nr_s * dl_s) + w_den * (dl_s * dr_s); + } + (sum_0, sum_inf) + }; + + let (t_0, t_inf) = if self.round < self.first_half { + let (poly_eq_left, poly_eq_right, second_half, low_mask) = self.poly_eqs_first_half(); + (0..half_p) + .into_par_iter() + .map(|id| { + let factor = poly_eq_left[id >> second_half] * poly_eq_right[id & low_mask]; + let gate = gate_0_inf(id); + (gate.0 * factor, gate.1 * factor) + }) + .reduce( + || (E::Scalar::ZERO, E::Scalar::ZERO), + |a, b| (a.0 + b.0, a.1 + b.1), + ) + } else { + let poly_eq_right = self.poly_eq_right_last_half(); + (0..half_p) + .into_par_iter() + .map(|id| { + let gate = gate_0_inf(id); + (gate.0 * poly_eq_right[id], gate.1 * poly_eq_right[id]) + }) + .reduce( + || (E::Scalar::ZERO, E::Scalar::ZERO), + |a, b| (a.0 + b.0, a.1 + b.1), + ) + }; + + if let Some(result) = self.derive_from_claim_deg2(t_0, t_inf, claim) { + result + } else { + self.fallback_eval_inf_logup_gate(t_0, t_inf, nl, nr, dl, dr, weights) + } + } + + /// Computes the Logup-GKR evaluation at `-1` when `tau = 0` prevents claim + /// derivation. + #[inline] + #[allow(clippy::too_many_arguments)] + fn fallback_eval_inf_logup_gate( + &self, + t_0: E::Scalar, + t_inf: E::Scalar, + nl: &[MultilinearPolynomial], + nr: &[MultilinearPolynomial], + dl: &[MultilinearPolynomial], + dr: &[MultilinearPolynomial], + weights: &[(E::Scalar, E::Scalar)], + ) -> (E::Scalar, E::Scalar, E::Scalar) { + let p = self.eval_eq_left; + let (eq_0, eq_slope, eq_m1) = self.eq_tau_0_a_inf[self.round - 1]; + let m = nl.len(); + let half_p = nl[0].Z.len() / 2; + let s_0 = eq_0 * p * t_0; + let s_leading = eq_slope * p * t_inf; + + let gate_m1 = |id: usize| -> E::Scalar { + let mut sum = E::Scalar::ZERO; + for i in 0..m { + let (w_num, w_den) = weights[i]; + let nl_m1 = nl[i].Z[id].double() - nl[i].Z[id + half_p]; + let nr_m1 = nr[i].Z[id].double() - nr[i].Z[id + half_p]; + let dl_m1 = dl[i].Z[id].double() - dl[i].Z[id + half_p]; + let dr_m1 = dr[i].Z[id].double() - dr[i].Z[id + half_p]; + sum += w_num * (nl_m1 * dr_m1 + nr_m1 * dl_m1) + w_den * (dl_m1 * dr_m1); + } + sum + }; + + let t_m1 = if self.round < self.first_half { + let (poly_eq_left, poly_eq_right, second_half, low_mask) = self.poly_eqs_first_half(); + (0..half_p) + .into_par_iter() + .map(|id| gate_m1(id) * poly_eq_left[id >> second_half] * poly_eq_right[id & low_mask]) + .reduce(|| E::Scalar::ZERO, |a, b| a + b) + } else { + let poly_eq_right = self.poly_eq_right_last_half(); + (0..half_p) + .into_par_iter() + .map(|id| gate_m1(id) * poly_eq_right[id]) + .reduce(|| E::Scalar::ZERO, |a, b| a + b) + }; + + let s_m1 = eq_m1 * p * t_m1; + (s_0, s_leading, s_m1) + } + + /// Evaluates ppSNARK's four Logup-GKR sub-instances and caches each + /// top-variable delta in its MLE's high half. + /// + /// The scan evaluates `t(0)` and `t(inf)`. BDDT claim derivation obtains + /// `s(-1)`, falling back to a third sum when the equality factor at `X=1` + /// is noninvertible. + /// `claim` must be the current `s(0) + s(1)` claim. Returns + /// `(s(0), X^3 coefficient of s, s(-1))`. + /// Every input must subsequently be bound with + /// `MultilinearPolynomial::bind_poly_var_top_with_cached_delta`. + /// + /// # Panics + /// + /// Panics unless all argument slices contain four equally sized, nonconstant + /// MLEs matching the current equality-sumcheck round. + #[inline] + #[allow(clippy::too_many_arguments)] + pub fn evaluation_points_logup_gate_and_cache_deltas( + &self, + nl: &mut [MultilinearPolynomial], + nr: &mut [MultilinearPolynomial], + dl: &mut [MultilinearPolynomial], + dr: &mut [MultilinearPolynomial], + weights: &[(E::Scalar, E::Scalar)], + claim: E::Scalar, + ) -> (E::Scalar, E::Scalar, E::Scalar) { + self.evaluation_points_logup_gate_and_cache_deltas_inner(nl, nr, dl, dr, weights, None, claim) + } + + /// Round-0 specialization that accepts the already-evaluated inner `t(0)`. + /// + /// `t_0` is the weighted inner gate sum at `X=0`, before multiplication by + /// the current equality factor. This method still caches every `high - low` + /// delta and returns `(s(0), X^3 coefficient of s, s(-1))`; callers must + /// subsequently bind with + /// `MultilinearPolynomial::bind_poly_var_top_with_cached_delta`. + /// + /// # Panics + /// + /// Panics unless called in round 0 with exactly four compatible + /// sub-instances. + #[inline] + #[allow(clippy::too_many_arguments)] + pub(crate) fn evaluation_points_logup_gate_and_cache_deltas_with_t_0( + &self, + nl: &mut [MultilinearPolynomial], + nr: &mut [MultilinearPolynomial], + dl: &mut [MultilinearPolynomial], + dr: &mut [MultilinearPolynomial], + weights: &[(E::Scalar, E::Scalar)], + t_0: E::Scalar, + claim: E::Scalar, + ) -> (E::Scalar, E::Scalar, E::Scalar) { + assert_eq!(self.round, 1, "precomputed t(0) is only valid in round 0"); + self.evaluation_points_logup_gate_and_cache_deltas_inner( + nl, + nr, + dl, + dr, + weights, + Some(t_0), + claim, + ) + } + + #[inline] + #[allow(clippy::too_many_arguments)] + fn evaluation_points_logup_gate_and_cache_deltas_inner( + &self, + nl: &mut [MultilinearPolynomial], + nr: &mut [MultilinearPolynomial], + dl: &mut [MultilinearPolynomial], + dr: &mut [MultilinearPolynomial], + weights: &[(E::Scalar, E::Scalar)], + known_t_0: Option, + claim: E::Scalar, + ) -> (E::Scalar, E::Scalar, E::Scalar) { + let m = nl.len(); + assert!(m > 0); + assert_eq!(m, nr.len()); + assert_eq!(m, dl.len()); + assert_eq!(m, dr.len()); + assert_eq!(m, weights.len()); + assert_eq!(nl[0].Z.len() % 2, 0); + assert_eq!( + m, 4, + "cached Logup-GKR evaluation is specialized for ppSNARK's four sub-instances" + ); + + let (t_0, t_inf) = if self.round < self.first_half { + let (poly_eq_left, poly_eq_right, second_half, low_mask) = self.poly_eqs_first_half(); + let factor = |id| poly_eq_left[id >> second_half] * poly_eq_right[id & low_mask]; + cache_four_logup_gate_deltas_with_t_0(nl, nr, dl, dr, weights, known_t_0, &factor) + } else { + let poly_eq_right = self.poly_eq_right_last_half(); + let factor = |id| poly_eq_right[id]; + cache_four_logup_gate_deltas_with_t_0(nl, nr, dl, dr, weights, known_t_0, &factor) + }; + + if let Some(result) = self.derive_from_claim_deg2(t_0, t_inf, claim) { + result + } else { + self.fallback_eval_inf_logup_gate_with_cached_deltas(t_0, t_inf, nl, nr, dl, dr, weights) + } + } + + /// Computes `s(-1)` from cached deltas when claim derivation cannot invert + /// the current equality factor. + #[inline] + #[allow(clippy::too_many_arguments)] + fn fallback_eval_inf_logup_gate_with_cached_deltas( + &self, + t_0: E::Scalar, + t_inf: E::Scalar, + nl: &[MultilinearPolynomial], + nr: &[MultilinearPolynomial], + dl: &[MultilinearPolynomial], + dr: &[MultilinearPolynomial], + weights: &[(E::Scalar, E::Scalar)], + ) -> (E::Scalar, E::Scalar, E::Scalar) { + let p = self.eval_eq_left; + let (eq_0, eq_slope, eq_m1) = self.eq_tau_0_a_inf[self.round - 1]; + let m = nl.len(); + let half_p = nl[0].Z.len() / 2; + + let s_0 = eq_0 * p * t_0; + let s_leading = eq_slope * p * t_inf; + + // m(-1) = low - (high - low) = low - cached_delta. + let gate_m1 = |id: usize| -> E::Scalar { + let mut sum = E::Scalar::ZERO; + for i in 0..m { + let (w_num, w_den) = weights[i]; + let nl_m1 = nl[i].Z[id] - nl[i].Z[id + half_p]; + let nr_m1 = nr[i].Z[id] - nr[i].Z[id + half_p]; + let dl_m1 = dl[i].Z[id] - dl[i].Z[id + half_p]; + let dr_m1 = dr[i].Z[id] - dr[i].Z[id + half_p]; + sum += w_num * (nl_m1 * dr_m1 + nr_m1 * dl_m1) + w_den * (dl_m1 * dr_m1); + } + sum + }; + + let t_m1 = if self.round < self.first_half { + let (poly_eq_left, poly_eq_right, second_half, low_mask) = self.poly_eqs_first_half(); + (0..half_p) + .into_par_iter() + .map(|id| { + let factor = poly_eq_left[id >> second_half] * poly_eq_right[id & low_mask]; + gate_m1(id) * factor + }) + .reduce(|| E::Scalar::ZERO, |a, b| a + b) + } else { + let poly_eq_right = self.poly_eq_right_last_half(); + (0..half_p) + .into_par_iter() + .map(|id| gate_m1(id) * poly_eq_right[id]) + .reduce(|| E::Scalar::ZERO, |a, b| a + b) + }; + + let s_m1 = eq_m1 * p * t_m1; + (s_0, s_leading, s_m1) + } + /// Evaluate eq(tau,X) * (A*B - C) using 2 N-scaling sums instead of 3 /// (BDDT, eprint 2025/1117 Section 6.2). /// Falls back to computing all 3 sums when tau=0 makes derivation impossible. @@ -1079,6 +1702,175 @@ pub mod eq_sumcheck { } } + /// Evaluates `eq(tau, X) * A(X)` while caching `A(high) - A(low)` in + /// `A`'s high half for the following bind. + /// + /// The caller must use + /// `MultilinearPolynomial::bind_poly_var_top_with_cached_delta` for this round. + #[inline] + pub fn evaluation_points_quadratic_with_one_input_and_cached_delta( + &self, + poly_A: &mut MultilinearPolynomial, + claim: E::Scalar, + ) -> (E::Scalar, E::Scalar, E::Scalar) { + debug_assert_eq!(poly_A.len() % 2, 0); + + let in_first_half = self.round < self.first_half; + let half_p = poly_A.Z.len() / 2; + let (low, delta) = poly_A.Z.split_at_mut(half_p); + + let t_0 = if in_first_half { + let (poly_eq_left, poly_eq_right, second_half, low_mask) = self.poly_eqs_first_half(); + let eval = |id: usize, low: &E::Scalar, delta: &mut E::Scalar| { + *delta -= low; + *low * poly_eq_left[id >> second_half] * poly_eq_right[id & low_mask] + }; + + if half_p < PARALLEL_THRESHOLD { + low + .iter() + .zip(delta.iter_mut()) + .enumerate() + .map(|(id, (low, delta))| eval(id, low, delta)) + .sum() + } else { + low + .par_iter() + .zip(delta.par_iter_mut()) + .enumerate() + .map(|(id, (low, delta))| eval(id, low, delta)) + .sum() + } + } else { + let poly_eq_right = self.poly_eq_right_last_half(); + let eval = |id: usize, low: &E::Scalar, delta: &mut E::Scalar| { + *delta -= low; + *low * poly_eq_right[id] + }; + + if half_p < PARALLEL_THRESHOLD { + low + .iter() + .zip(delta.iter_mut()) + .enumerate() + .map(|(id, (low, delta))| eval(id, low, delta)) + .sum() + } else { + low + .par_iter() + .zip(delta.par_iter_mut()) + .enumerate() + .map(|(id, (low, delta))| eval(id, low, delta)) + .sum() + } + }; + + if let Some(result) = self.derive_from_claim_deg1(t_0, claim) { + result + } else { + self.fallback_eval_inf_one_input_with_cached_delta(t_0, poly_A) + } + } + + /// Evaluates `eq(tau, X) * ((1 - q0) * e0(X) + q0 * e1(X))` while caching + /// `high - low` in both `e0`'s and `e1`'s high halves for the following bind. + /// + /// This fuses the MSB-weighted `E` combination into the round evaluation, so + /// the fused prover never materializes `e_weighted = (1-q0)*e0 + q0*e1`. The + /// combined inner polynomial is still degree 1 in `X`, so BDDT claim + /// derivation (`derive_from_claim_deg1`) applies unchanged. Both `e0` + /// and `e1` must then bind with + /// `MultilinearPolynomial::bind_poly_var_top_with_cached_delta`. + #[inline] + pub fn evaluation_points_quadratic_with_two_inputs_and_cached_delta( + &self, + poly_e0: &mut MultilinearPolynomial, + poly_e1: &mut MultilinearPolynomial, + q0: E::Scalar, + claim: E::Scalar, + ) -> (E::Scalar, E::Scalar, E::Scalar) { + debug_assert_eq!(poly_e0.len() % 2, 0); + debug_assert_eq!(poly_e0.len(), poly_e1.len()); + let one_minus_q0 = E::Scalar::ONE - q0; + + let in_first_half = self.round < self.first_half; + let half_p = poly_e0.Z.len() / 2; + let (e0_low, e0_delta) = poly_e0.Z.split_at_mut(half_p); + let (e1_low, e1_delta) = poly_e1.Z.split_at_mut(half_p); + + let t_0 = if in_first_half { + let (poly_eq_left, poly_eq_right, second_half, low_mask) = self.poly_eqs_first_half(); + let eval = |id: usize, + e0_low: &E::Scalar, + e0_delta: &mut E::Scalar, + e1_low: &E::Scalar, + e1_delta: &mut E::Scalar| { + *e0_delta -= e0_low; + *e1_delta -= e1_low; + let combined = one_minus_q0 * *e0_low + q0 * *e1_low; + combined * poly_eq_left[id >> second_half] * poly_eq_right[id & low_mask] + }; + + if half_p < PARALLEL_THRESHOLD { + e0_low + .iter() + .zip(e0_delta.iter_mut()) + .zip(e1_low.iter()) + .zip(e1_delta.iter_mut()) + .enumerate() + .map(|(id, (((e0l, e0d), e1l), e1d))| eval(id, e0l, e0d, e1l, e1d)) + .sum() + } else { + e0_low + .par_iter() + .zip(e0_delta.par_iter_mut()) + .zip(e1_low.par_iter()) + .zip(e1_delta.par_iter_mut()) + .enumerate() + .map(|(id, (((e0l, e0d), e1l), e1d))| eval(id, e0l, e0d, e1l, e1d)) + .sum() + } + } else { + let poly_eq_right = self.poly_eq_right_last_half(); + let eval = |id: usize, + e0_low: &E::Scalar, + e0_delta: &mut E::Scalar, + e1_low: &E::Scalar, + e1_delta: &mut E::Scalar| { + *e0_delta -= e0_low; + *e1_delta -= e1_low; + let combined = one_minus_q0 * *e0_low + q0 * *e1_low; + combined * poly_eq_right[id] + }; + + if half_p < PARALLEL_THRESHOLD { + e0_low + .iter() + .zip(e0_delta.iter_mut()) + .zip(e1_low.iter()) + .zip(e1_delta.iter_mut()) + .enumerate() + .map(|(id, (((e0l, e0d), e1l), e1d))| eval(id, e0l, e0d, e1l, e1d)) + .sum() + } else { + e0_low + .par_iter() + .zip(e0_delta.par_iter_mut()) + .zip(e1_low.par_iter()) + .zip(e1_delta.par_iter_mut()) + .enumerate() + .map(|(id, (((e0l, e0d), e1l), e1d))| eval(id, e0l, e0d, e1l, e1d)) + .sum() + } + }; + + if let Some(result) = self.derive_from_claim_deg1(t_0, claim) { + result + } else { + self.fallback_eval_inf_two_inputs_with_cached_delta(t_0, poly_e0, poly_e1, q0) + } + } + /// Fallback for three-input case: compute eval_inf via third N-scaling sum /// when claim-based derivation is impossible (tau=0). #[inline] @@ -1221,6 +2013,95 @@ pub mod eq_sumcheck { (s_0, s_leading, s_m1) } + /// Computes the one-input evaluation at `-1` from the cached delta when + /// `tau = 0` prevents claim derivation. + #[inline] + fn fallback_eval_inf_one_input_with_cached_delta( + &self, + t_0: E::Scalar, + poly_A: &MultilinearPolynomial, + ) -> (E::Scalar, E::Scalar, E::Scalar) { + let p = self.eval_eq_left; + let (eq_0, _eq_slope, eq_m1) = self.eq_tau_0_a_inf[self.round - 1]; + + let s_0 = eq_0 * p * t_0; + let s_leading = E::Scalar::ZERO; + + let half_p = poly_A.Z.len() / 2; + let (low, delta) = poly_A.Z.split_at(half_p); + + let t_m1 = if self.round < self.first_half { + let (poly_eq_left, poly_eq_right, second_half, low_mask) = self.poly_eqs_first_half(); + (0..half_p) + .into_par_iter() + .map(|id| { + let factor = poly_eq_left[id >> second_half] * poly_eq_right[id & low_mask]; + (low[id] - delta[id]) * factor + }) + .reduce(|| E::Scalar::ZERO, |a, b| a + b) + } else { + let poly_eq_right = self.poly_eq_right_last_half(); + (0..half_p) + .into_par_iter() + .map(|id| (low[id] - delta[id]) * poly_eq_right[id]) + .reduce(|| E::Scalar::ZERO, |a, b| a + b) + }; + + let s_m1 = eq_m1 * p * t_m1; + (s_0, s_leading, s_m1) + } + + /// `tau = 0` fallback for the two-input (`e0`/`e1`) cached-delta kernel: + /// computes `s(-1)` from the already-cached deltas when claim derivation + /// cannot invert the equality factor. + #[inline] + fn fallback_eval_inf_two_inputs_with_cached_delta( + &self, + t_0: E::Scalar, + poly_e0: &MultilinearPolynomial, + poly_e1: &MultilinearPolynomial, + q0: E::Scalar, + ) -> (E::Scalar, E::Scalar, E::Scalar) { + let one_minus_q0 = E::Scalar::ONE - q0; + let p = self.eval_eq_left; + let (eq_0, _eq_slope, eq_m1) = self.eq_tau_0_a_inf[self.round - 1]; + + let s_0 = eq_0 * p * t_0; + let s_leading = E::Scalar::ZERO; + + let half_p = poly_e0.Z.len() / 2; + let (e0_low, e0_delta) = poly_e0.Z.split_at(half_p); + let (e1_low, e1_delta) = poly_e1.Z.split_at(half_p); + + // combined(-1) = (1-q0)*(e0_low - e0_delta) + q0*(e1_low - e1_delta), + // where e{0,1}_delta already hold high - low from the eval pass. + let t_m1 = if self.round < self.first_half { + let (poly_eq_left, poly_eq_right, second_half, low_mask) = self.poly_eqs_first_half(); + (0..half_p) + .into_par_iter() + .map(|id| { + let factor = poly_eq_left[id >> second_half] * poly_eq_right[id & low_mask]; + let combined_m1 = + one_minus_q0 * (e0_low[id] - e0_delta[id]) + q0 * (e1_low[id] - e1_delta[id]); + combined_m1 * factor + }) + .reduce(|| E::Scalar::ZERO, |a, b| a + b) + } else { + let poly_eq_right = self.poly_eq_right_last_half(); + (0..half_p) + .into_par_iter() + .map(|id| { + let combined_m1 = + one_minus_q0 * (e0_low[id] - e0_delta[id]) + q0 * (e1_low[id] - e1_delta[id]); + combined_m1 * poly_eq_right[id] + }) + .reduce(|| E::Scalar::ZERO, |a, b| a + b) + }; + + let s_m1 = eq_m1 * p * t_m1; + (s_0, s_leading, s_m1) + } + /// Binds a variable in the sumcheck instance. #[inline] pub fn bound(&mut self, r: &E::Scalar) {