Clarify satisfying small-value sumcheck contract

Author: wu-s-john

src/lagrange_accumulator/accumulator_builder.rs

@@ -7,7 +7,8 @@
 //! Builder functions for constructing Lagrange accumulators (Procedure 9).
 //!
 //! This module provides:
-//! - [`build_accumulators_spartan`]: Optimized builder for Spartan's cubic relation
+//! - [`build_accumulators_spartan_satisfying`]: Optimized builder for Spartan's
+//!   satisfying-witness cubic relation
 
 use super::{
   accumulator::LagrangeAccumulators, csr::Csr, domain::LagrangeIndex,
@@ -93,10 +94,16 @@ pub(crate) fn build_beta_cache<const D: usize>(l0: usize) -> BetaPrefixCache {
   BetaPrefixCache { cache, num_betas }
 }
 
-/// Procedure 9: Build accumulators A_i(v, u) for Spartan's first sum-check (Algorithm 6).
+/// Procedure 9: Build accumulators A_i(v, u) for Spartan's satisfying-witness
+/// first sum-check (Algorithm 6).
 ///
 /// Computes accumulators for: g(X) = eq(τ, X) · (Az(X) · Bz(X) - Cz(X))
 ///
+/// This specialized builder assumes `Az * Bz = Cz` on `{0,1}^n`. Under that
+/// satisfying-witness invariant, all binary-β contributions vanish, so the
+/// optimized prefix rounds can omit explicit `C` handling and only accumulate
+/// the non-binary β values containing `∞`.
+///
 /// D is the degree bound of t_i(X) (not s_i); for Spartan, D = 2.
 ///
 /// # Type Parameters
@@ -124,7 +131,7 @@ pub(crate) fn build_beta_cache<const D: usize>(l0: usize) -> BetaPrefixCache {
 ///
 /// - Skip binary betas: for satisfying witnesses, Az·Bz = Cz on {0,1}^n, so Az·Bz - Cz = 0
 /// - Only process betas containing ∞ (non-binary evaluations where contributions are non-zero)
-pub fn build_accumulators_spartan<F, SV>(
+pub fn build_accumulators_spartan_satisfying<F, SV>(
   az: &MultilinearPolynomial<SV>,
   bz: &MultilinearPolynomial<SV>,
   taus: &[F],
@@ -161,7 +168,8 @@ where
   } = build_beta_cache::<2>(l0);
 
   // Only betas containing at least one ∞ coordinate contribute non-zero values.
-  // On binary inputs {0,1}^n, Az·Bz = Cz (R1CS identity), so Az·Bz - Cz = 0.
+  // This builder intentionally omits explicit C terms: on satisfying witnesses,
+  // Az·Bz = Cz on {0,1}^n, so all binary-β contributions are zero already.
   let betas_with_infty: Vec<usize> = (0..num_betas)
     .filter(|&i| (0..l0).any(|d| (i / base.pow(d as u32)) % base == 0))
     .collect();
@@ -223,7 +231,8 @@ where
           );
           let bz_ext = &state.bz_extended_evals[..bz_size];
 
-          // Only process betas with ∞ - binary betas contribute 0 for satisfying witnesses
+          // Only process betas with ∞. Omitting explicit C terms is intentional here:
+          // the satisfying-witness invariant makes every binary-β contribution vanish.
           // Uses delayed modular reduction: accumulates into unreduced wide-limb form.
           for &beta_idx in &betas_with_infty {
             let prod = SV::wide_mul(az_ext[beta_idx], bz_ext[beta_idx]);
@@ -301,7 +310,7 @@ mod tests {
   /// Binary-β zero shortcut: Az=Bz=Cz=first variable (x0), so Az·Bz−Cz=0 on binary β.
   /// Non-binary β (∞) should yield non-zero in some bucket.
   #[test]
-  fn test_binary_beta_zero_shortcut_behavior() {
+  fn test_binary_beta_zero_shortcut_behavior_for_satisfying_witness() {
     // Use l0=1 so round 0 buckets are fed only by β of length 1 (easy to reason about).
     let l0 = 1;
     let l = 2;
@@ -316,7 +325,7 @@ mod tests {
 
     let taus: Vec<Scalar> = vec![Scalar::from(3u64), Scalar::from(5u64)];
 
-    let (acc, _, _) = build_accumulators_spartan(&az, &bz, &taus, l0);
+    let (acc, _, _) = build_accumulators_spartan_satisfying(&az, &bz, &taus, l0);
 
     // Only round 0 exists (v is empty). β ranges over U_d with binary {0,1} and non-binary {∞}.
     // Buckets for u = 0 should be zero (binary β), bucket for u = ∞ should be non-zero.
@@ -333,11 +342,12 @@ mod tests {
     );
   }
 
-  /// Test build_accumulators_spartan with i32 witnesses produces consistent results.
+  /// Test `build_accumulators_spartan_satisfying` with i32 satisfying witnesses
+  /// produces consistent results.
   ///
   /// Verifies that running the same computation twice produces the same output.
   #[test]
-  fn test_build_accumulators_spartan_small_consistent() {
+  fn test_build_accumulators_spartan_satisfying_small_consistent() {
     let l0 = 2;
 
     // Define deterministic Az, Bz over {0,1}^4 using small values
@@ -364,8 +374,8 @@ mod tests {
     ];
 
     // Build accumulators twice
-    let (acc1, _, _) = build_accumulators_spartan(&az, &bz, &taus, l0);
-    let (acc2, _, _) = build_accumulators_spartan(&az, &bz, &taus, l0);
+    let (acc1, _, _) = build_accumulators_spartan_satisfying(&az, &bz, &taus, l0);
+    let (acc2, _, _) = build_accumulators_spartan_satisfying(&az, &bz, &taus, l0);
 
     // Compare all buckets
     for round in 0..l0 {
@@ -384,9 +394,10 @@ mod tests {
     }
   }
 
-  /// Test build_accumulators_spartan with i32 witnesses using larger inputs to stress test.
+  /// Test `build_accumulators_spartan_satisfying` with i32 satisfying witnesses
+  /// using larger inputs to stress the satisfying-witness shortcut.
   #[test]
-  fn test_build_accumulators_spartan_small_larger() {
+  fn test_build_accumulators_spartan_satisfying_small_larger() {
     let l0 = 3;
     let l = 10;
     let n = 1 << l;
@@ -402,8 +413,8 @@ mod tests {
     let taus: Vec<Scalar> = (0..l).map(|i| Scalar::from((i * 7 + 3) as u64)).collect();
 
     // Build accumulators twice to verify consistency
-    let (acc1, _, _) = build_accumulators_spartan(&az, &bz, &taus, l0);
-    let (acc2, _, _) = build_accumulators_spartan(&az, &bz, &taus, l0);
+    let (acc1, _, _) = build_accumulators_spartan_satisfying(&az, &bz, &taus, l0);
+    let (acc2, _, _) = build_accumulators_spartan_satisfying(&az, &bz, &taus, l0);
 
     for round in 0..l0 {
       let num_v = (D + 1).pow(round as u32);

src/lagrange_accumulator/mod.rs

@@ -47,7 +47,7 @@ pub use basis::{LagrangeBasisFactory, LagrangeCoeff};
 pub use accumulator::{LagrangeAccumulators, RoundAccumulator};
 
 // Builder functions
-pub use accumulator_builder::{SPARTAN_T_DEGREE, build_accumulators_spartan};
+pub use accumulator_builder::{SPARTAN_T_DEGREE, build_accumulators_spartan_satisfying};
 
 // Eq round factor and derivation
 pub use eq_round::{EqRoundFactor, derive_t1};

src/lagrange_accumulator/thread_state.rs

@@ -7,15 +7,15 @@
 //! Thread-local scratch buffers for accumulator building.
 //!
 //! These structs eliminate per-iteration heap allocations in the parallel fold loops
-//! of `build_accumulators_spartan`. By hoisting buffer allocations to the fold identity
+//! of `build_accumulators_spartan_satisfying`. By hoisting buffer allocations to the fold identity
 //! closure (called once per Rayon thread subdivision), we reduce allocations from
 //! O(num_x_out) to O(num_threads).
 
 use super::accumulator::LagrangeAccumulators;
 use crate::big_num::{DelayedReduction, SmallValue, SmallValueEngine};
 use num_traits::Zero;
 
-/// Thread-local scratch buffers for `build_accumulators_spartan`.
+/// Thread-local scratch buffers for `build_accumulators_spartan_satisfying`.
 ///
 /// # Motivation
 ///

src/small_sumcheck.rs

@@ -16,14 +16,15 @@
 //!
 //! # Overview
 //!
-//! The main entry point is [`prove_cubic_small_value`], which implements
+//! The main entry point is [`prove_cubic_small_value_satisfying`], which implements
+//! the satisfying-witness-only version of the small-value optimization.
 
 use crate::{
   big_num::{DelayedReduction, SmallValue, SmallValueEngine},
   errors::SpartanError,
   lagrange_accumulator::{
     EqRoundFactor, LagrangeAccumulators, LagrangeBasisFactory, LagrangeCoeff, LagrangeEvals,
-    LagrangeHatEvals, SPARTAN_T_DEGREE, build_accumulators_spartan, derive_t1,
+    LagrangeHatEvals, SPARTAN_T_DEGREE, build_accumulators_spartan_satisfying, derive_t1,
   },
   polys::{eq::EqPolynomial, multilinear::MultilinearPolynomial, univariate::UniPoly},
   start_span,
@@ -202,6 +203,8 @@ where
 ///
 /// Field-element polynomials are created internally via batched eq-weighted binding
 /// from the small-value inputs, eliminating the need for pre-allocated field polys.
+/// This specialized prover assumes a satisfying witness, so `Az * Bz = Cz` on
+/// `{0,1}^n` and the incoming `claim` is expected to be zero.
 ///
 /// Generic over `SmallValue` to support both i32/i64 and i64/i128 configurations.
 ///
@@ -211,7 +214,7 @@ where
 ///   `min(LB, num_rounds / 2)`. Caller should ensure input values are bounded by
 ///   `SV::MAX / 3^LB` for safe Lagrange extension (see [`ExtensionBound`]).
 ///   Typical values are 3-4 for practical instances (3^4 = 81× growth factor).
-pub fn prove_cubic_small_value<E, SV, const LB: usize>(
+pub fn prove_cubic_small_value_satisfying<E, SV, const LB: usize>(
   claim: &E::Scalar,
   taus: Vec<E::Scalar>,
   poly_A_small: &MultilinearPolynomial<SV>,
@@ -242,13 +245,15 @@ where
   }
 
   // ===== Pre-computation Phase =====
-  // Build accumulators A_i(v, u) for all i ∈ [ℓ₀] using small-value arithmetic.
+  // Build satisfying-witness accumulators A_i(v, u) for all i ∈ [ℓ₀] using
+  // small-value arithmetic. This optimized prefix path intentionally omits
+  // explicit C handling because Az·Bz - Cz vanishes on binary points.
   // Also builds eq pyramids for reuse by EqSumCheckInstance.
   // Internally computes eq tables with balanced split and precomputed eq_cache.
   // Uses: small × small → intermediate (for Az·Bz products),
   // then intermediate × field (for eq weighting via DelayedReduction).
   let (accumulators, mut e_in_pyramid, e_xout_pyramid) =
-    build_accumulators_spartan(poly_A_small, poly_B_small, &taus, l0);
+    build_accumulators_spartan_satisfying(poly_A_small, poly_B_small, &taus, l0);
 
   let mut small_value_sumcheck =
     SmallValueSumCheck::<E::Scalar, SPARTAN_T_DEGREE>::from_accumulators(accumulators);
@@ -300,9 +305,10 @@ where
   }
 
   // ===== Transition Phase =====
-  // Create bound field-element polynomials via batched eq-weighted small-value accumulation.
-  // Binds all completed small-value rounds in a single pass using field×int
-  // unreduced accumulation.
+  // Create bound field-element polynomials via batched eq-weighted small-value
+  // accumulation. The satisfying-witness shortcut only applies to the prefix
+  // accumulators above; we still carry `poly_C_small` explicitly through this
+  // transition and all remaining rounds.
   let (_bind_span, bind_t) = start_span!("bind_poly_vars_transition");
   let (mut poly_A, mut poly_B, mut poly_C) =
     bind_three_polys_batched_small_value(
@@ -323,7 +329,8 @@ where
     // This matches the Nova optimization where τ[l₀] is tracked in eval_eq_left.
     e_in_pyramid.pop();
 
-    // Reuse the precomputed eq pyramids when all planned small-value rounds succeeded.
+    // Reuse the precomputed eq pyramids when all planned small-value rounds
+    // succeeded under the satisfying-witness shortcut.
     eq_sumcheck::EqSumCheckInstance::<E>::from_pyramids(
       e_in_pyramid,
       e_xout_pyramid,
@@ -407,9 +414,9 @@ mod tests {
   type E = PallasHyraxEngine;
   type F = <E as Engine>::Scalar;
 
-  /// Generic helper to test that SmallValueSumCheck produces the same polynomial
-  /// evaluations as EqSumCheckInstance across multiple rounds.
-  fn run_smallvalue_round_test<SV>()
+  /// Generic helper to test that `SmallValueSumCheck` produces the same
+  /// polynomial evaluations as `EqSumCheckInstance` on satisfying inputs.
+  fn run_satisfying_smallvalue_round_test<SV>()
   where
     SV: SmallValue + Mul<Output = SV> + TryFrom<usize>,
     <SV as TryFrom<usize>>::Error: Debug,
@@ -423,7 +430,7 @@ mod tests {
       .map(|i| F::from((i + 2) as u64))
       .collect::<Vec<_>>();
 
-    // Small-value polynomials for build_accumulators_spartan
+    // Small-value polynomials for build_accumulators_spartan_satisfying
     let az_small: Vec<SV> = (0..n).map(|i| SV::try_from(i + 1).unwrap()).collect();
     let bz_small: Vec<SV> = (0..n).map(|i| SV::try_from(i + 3).unwrap()).collect();
     let cz_small: Vec<SV> = az_small
@@ -447,8 +454,9 @@ mod tests {
     // Claim = 0 for satisfying witness (Az·Bz = Cz)
     let mut claim = F::ZERO;
 
-    // Build accumulators using the simplified API
-    let (accs, _, _) = build_accumulators_spartan(&az_poly, &bz_poly, &taus, SMALL_VALUE_ROUNDS);
+    // Build accumulators using the satisfying-witness API.
+    let (accs, _, _) =
+      build_accumulators_spartan_satisfying(&az_poly, &bz_poly, &taus, SMALL_VALUE_ROUNDS);
     let mut small_value = SmallValueSumCheck::from_accumulators(accs);
 
     // Full eq_instance for verification against standard sumcheck
@@ -512,17 +520,17 @@ mod tests {
   }
 
   #[test]
-  fn test_smallvalue_round_matches_eq_instance_evals_i32() {
-    run_smallvalue_round_test::<i32>();
+  fn test_satisfying_smallvalue_round_matches_eq_instance_evals_i32() {
+    run_satisfying_smallvalue_round_test::<i32>();
   }
 
   #[test]
-  fn test_smallvalue_round_matches_eq_instance_evals_i64() {
-    run_smallvalue_round_test::<i64>();
+  fn test_satisfying_smallvalue_round_matches_eq_instance_evals_i64() {
+    run_satisfying_smallvalue_round_test::<i64>();
   }
 
-  /// Test that prove_cubic_small_value produces identical
-  /// output to prove_cubic_with_three_inputs using synthetic small-value polynomials.
+  /// Test that `prove_cubic_small_value_satisfying` produces identical output
+  /// to `prove_cubic_with_three_inputs` on satisfying synthetic inputs.
   ///
   /// Uses synthetic Az, Bz values in a small range and computes Cz = Az * Bz.
   fn run_equivalence_test<SV>(num_vars: usize)
@@ -599,7 +607,7 @@ mod tests {
     .expect("standard prove should succeed");
 
     // Run small-value method
-    let (proof2, r2, evals2) = prove_cubic_small_value::<E, SV, 3>(
+    let (proof2, r2, evals2) = prove_cubic_small_value_satisfying::<E, SV, 3>(
       &claim,
       taus.clone(),
       &az_small_poly,
@@ -633,7 +641,7 @@ mod tests {
     assert_eq!(final_claim, expected, "final claim mismatch");
   }
 
-  /// Test small-value sumcheck equivalence with synthetic polynomials.
+  /// Test satisfying small-value sumcheck equivalence with synthetic polynomials.
   ///
   /// Tests multiple sizes to ensure equivalence holds for various l0 values.
   /// With LB=3, l0 = min(3, num_vars - 1):
@@ -643,21 +651,21 @@ mod tests {
   /// - num_vars=6: l0=3, suffix_vars=3
   /// - num_vars=10: l0=3, suffix_vars=7
   #[test]
-  fn test_sumcheck_equivalence_with_synthetic_i32() {
+  fn test_satisfying_sumcheck_equivalence_with_synthetic_i32() {
     for num_vars in [2, 3, 4, 6, 10] {
       run_equivalence_test::<i32>(num_vars);
     }
   }
 
   #[test]
-  fn test_sumcheck_equivalence_with_synthetic_i64() {
+  fn test_satisfying_sumcheck_equivalence_with_synthetic_i64() {
     for num_vars in [2, 3, 4, 6, 10] {
       run_equivalence_test::<i64>(num_vars);
     }
   }
 
   #[test]
-  fn test_sumcheck_equivalence_when_first_tau_is_zero() {
+  fn test_satisfying_sumcheck_equivalence_when_first_tau_is_zero() {
     const NUM_VARS: usize = 6;
     const SEED: u64 = 0xDEADBEEF;
     let mut rng = StdRng::seed_from_u64(SEED);
@@ -697,7 +705,7 @@ mod perf_tests {
   #[cfg(not(debug_assertions))]
   const TEST_SIZES: &[usize] = &[16, 18, 20, 22, 24];
 
-  fn test_small_value_sumcheck_with<E: Engine>()
+  fn test_satisfying_small_value_sumcheck_with<E: Engine>()
   where
     E::Scalar: SmallValueEngine<i64>,
   {
@@ -733,7 +741,7 @@ mod perf_tests {
         num_vars = num_vars
       );
 
-      let (proof, _r, _evals) = prove_cubic_small_value::<E, _, 3>(
+      let (proof, _r, _evals) = prove_cubic_small_value_satisfying::<E, _, 3>(
         &E::Scalar::ZERO,
         taus.clone(),
         &az_poly,
@@ -754,7 +762,7 @@ mod perf_tests {
   }
 
   #[test]
-  fn test_small_value_sumcheck_perf() {
+  fn test_satisfying_small_value_sumcheck_perf() {
     let _ = tracing_subscriber::fmt()
       .with_target(false)
       .with_ansi(true)
@@ -764,14 +772,14 @@ mod perf_tests {
     use crate::provider::Bn254Engine;
 
     // Always test with BN254
-    test_small_value_sumcheck_with::<Bn254Engine>();
+    test_satisfying_small_value_sumcheck_with::<Bn254Engine>();
 
     // Additional engines only in release builds
     #[cfg(not(debug_assertions))]
     {
       use crate::provider::{PallasHyraxEngine, T256HyraxEngine};
-      test_small_value_sumcheck_with::<PallasHyraxEngine>();
-      test_small_value_sumcheck_with::<T256HyraxEngine>();
+      test_satisfying_small_value_sumcheck_with::<PallasHyraxEngine>();
+      test_satisfying_small_value_sumcheck_with::<T256HyraxEngine>();
     }
   }
 }