feat: enhance clamp lookup and polynomial commitment handling

Author: Forpee

jolt-atlas-core/src/onnx_proof/clamp_lookups/mod.rs

@@ -410,7 +410,7 @@ pub fn verify_clamp_lookup<F: JoltField, T: Transcript>(
 /// (empty for scalar nodes, which prove the clamp directly).
 pub fn clamp_committed_polys(node: &ComputationNode) -> Vec<CommittedPoly> {
     if is_scalar(node) {
-        return vec![];
+        return Vec::new();
     }
     let d = ClampEncoding::new(node).one_hot_params().instruction_d;
     (0..d)
@@ -427,7 +427,9 @@ pub fn verify_scalar_clamp<F: JoltField>(
     op: &str,
 ) -> Result<(), ProofVerifyError> {
     let value = recover_small_int(combined).ok_or_else(|| {
-        ProofVerifyError::InvalidOpeningProof(format!("{op} (scalar): value not in i32 range"))
+        ProofVerifyError::InvalidOpeningProof(format!(
+            "{op} (scalar): accumulation claim is not a small signed-integer encoding"
+        ))
     })?;
     let expected = F::from_i32(value.clamp(i32::MIN as i64, i32::MAX as i64) as i32);
     if output_claim != expected {

jolt-atlas-core/src/onnx_proof/prover.rs

@@ -234,7 +234,7 @@ impl<F: JoltField, T: Transcript, PCS: CommitmentScheme<Field = F>> ONNXProof<F,
     }
 
     #[tracing::instrument(skip_all)]
-    fn commit_to_polynomials(
+    pub(super) fn commit_to_polynomials(
         poly_map: &BTreeMap<CommittedPoly, MultilinearPolynomial<F>>,
         pcs: &PCS::ProverSetup,
     ) -> Vec<PCS::Commitment> {

jolt-atlas-core/src/onnx_proof/zk.rs

@@ -1847,12 +1847,24 @@ pub fn prove_zk(
     // public auxiliary vectors) toggle this flag off and back on.
     prover.accumulator.zk_mode = true;
 
-    let (poly_map, commitments) = ONNXProof::<F, T, PCS>::commit_witness_polynomials(
-        pp.model(),
-        &prover.trace,
-        &pp.generators,
-        &mut prover.transcript,
-    );
+    // The ZK pipeline proves `Add`/`Sub`/`Sum` un-clamped (the saturating clamp
+    // lookup is not yet wired into `prove_zk`; per-node provers are the
+    // un-clamped `AddProver`/`SubProver`/`SumAxisProver`). Those provers never
+    // open the clamp one-hot decomposition (`ClampRaD`), so committing it would
+    // leave it without an opening-reduction sumcheck. Filter it out here so the
+    // committed set matches what the zk sumchecks actually open. (The non-ZK
+    // path commits and opens `ClampRaD` as usual.)
+    let poly_map: std::collections::BTreeMap<
+        common::CommittedPoly,
+        joltworks::poly::multilinear_polynomial::MultilinearPolynomial<F>,
+    > = ONNXProof::<F, T, PCS>::polynomial_map(pp.model(), &prover.trace)
+        .into_iter()
+        .filter(|(poly, _)| !matches!(poly, common::CommittedPoly::ClampRaD(..)))
+        .collect();
+    let commitments = ONNXProof::<F, T, PCS>::commit_to_polynomials(&poly_map, &pp.generators);
+    for commitment in &commitments {
+        prover.transcript.append_serializable(commitment);
+    }
     // The output claim is a public scalar derived from IO; both prover and
     // verifier (`verify_zk` does `transcript.append_scalar(&expected_output_claim)`)
     // append it in the clear. Toggle prover zk_mode off so its append fires.

joltworks/src/lookup_tables/sat_clamp.rs

@@ -80,6 +80,13 @@ impl<const XLEN: usize> PrefixSuffixDecompositionTrait<XLEN> for SatClampTable<X
     }
 
     fn combine<F: JoltField>(&self, prefixes: &[PrefixEval<F>], suffixes: &[SuffixEval<F>]) -> F {
+        // The prefix-suffix decomposition hard-codes the i32 split point and uses
+        // `i32::MAX`, so it is only correct for a 64-bit address. (The MLE /
+        // materialization paths additionally support XLEN = 16.)
+        debug_assert_eq!(
+            XLEN, 64,
+            "SatClampTable prefix-suffix decomposition is only valid for XLEN = 64"
+        );
         let [suffix_one, suffix_not_lower_msb_upper_eqz, suffix_not_lower_msb_upper_eqz_low, suffix_lower_msb_upper_eqo_low] =
             suffixes.try_into().unwrap();
         let [prefix_sat_val, prefix_upper_eqz, prefix_upper_eqo, prefix_lower_msb, prefix_not_lower_msb, prefix_lower_word_no_msb] =

joltworks/src/poly/signed_identity_poly.rs

@@ -86,8 +86,10 @@ impl<F: JoltField> PolynomialEvaluation<F> for SignedIdentityPoly<F> {
                 // Weight of the variable being bound this round.
                 let slope = F::from_u128(1 << self.num_bound_vars);
                 // Two's-complement sign penalty: sign bit contributes -2^(n-1),
-                // encoded here as (slope_at_sign_bit - 2^n).
-                let sign_penalty = F::from_u64(self.num_vars.pow2() as u64);
+                // encoded here as (slope_at_sign_bit - 2^n). Use a u128 shift so
+                // this stays correct for `num_vars >= 64` (64-bit clamp lookups),
+                // matching `evaluate`'s `from_u128(1 << num_vars)`.
+                let sign_penalty = F::from_u128(1u128 << self.num_vars);
 
                 if self.sign_bit_pos() == self.num_bound_vars {
                     // Binding the sign bit: p(0) = bound_value (sign=0, no penalty),

joltworks/src/utils/lookup_bits.rs

@@ -62,7 +62,12 @@ impl LookupBits {
     }
 
     pub fn eqo(&self) -> bool {
-        self.bits == (1 << self.len) - 1
+        // `1u64 << 64` overflows; clamp lookups use 64-bit indices, so handle it.
+        if self.len == 64 {
+            self.bits == u64::MAX
+        } else {
+            self.bits == (1u64 << self.len) - 1
+        }
     }
 }