Fix : Unchecked Witness-Derived Indices Cause Deterministic Prover Panics in RAM and Multiplicity Builders [LA-H]

provekit/prover/src/lib.rs

@@ -134,7 +134,8 @@ impl Prove for NoirProver {
                 self.split_witness_builders.w1_layers,
                 &acir_witness_idx_to_value_map,
                 &mut merlin,
-            );
+            )
+            .context("While solving w1 witnesses")?;
         }
 
         // Compress w2 layers to free memory during w1 commit (only when
@@ -181,7 +182,8 @@ impl Prove for NoirProver {
                     w2_layers,
                     &acir_witness_idx_to_value_map,
                     &mut merlin,
-                );
+                )
+                .context("While solving w2 witnesses")?;
             }
             drop(acir_witness_idx_to_value_map);
 

provekit/prover/src/r1cs.rs

@@ -104,13 +104,13 @@ pub fn solve_witness_vec(
     plan: LayeredWitnessBuilders,
     acir_map: &WitnessMap<NoirElement>,
     transcript: &mut ProverState<TranscriptSponge>,
-) {
+) -> Result<()> {
     for layer in &plan.layers {
         match layer.typ {
             LayerType::Other => {
                 // Execute regular operations
                 for builder in &layer.witness_builders {
-                    builder.solve(acir_map, witness, transcript);
+                    builder.solve(acir_map, witness, transcript)?;
                 }
             }
             LayerType::Inverse => {
@@ -205,6 +205,7 @@ pub fn solve_witness_vec(
             }
         }
     }
+    Ok(())
 }
 
 #[cfg(test)]

provekit/prover/src/witness/ram.rs

@@ -1,4 +1,5 @@
 use {
+    anyhow::{ensure, Result},
     ark_ff::PrimeField,
     provekit_common::{
         witness::{SpiceMemoryOperation, SpiceWitnesses},
@@ -7,11 +8,11 @@ use {
 };
 
 pub(crate) trait SpiceWitnessesSolver {
-    fn solve(&self, witness: &mut [Option<FieldElement>]);
+    fn solve(&self, witness: &mut [Option<FieldElement>]) -> Result<()>;
 }
 
 impl SpiceWitnessesSolver for SpiceWitnesses {
-    fn solve(&self, witness: &mut [Option<FieldElement>]) {
+    fn solve(&self, witness: &mut [Option<FieldElement>]) -> Result<()> {
         debug_assert_eq!(
             self.initial_value_witnesses.len(),
             self.memory_length,
@@ -30,6 +31,11 @@ impl SpiceWitnessesSolver for SpiceWitnesses {
                 SpiceMemoryOperation::Load(addr, value, read_timestamp) => {
                     let addr = witness[*addr].unwrap();
                     let addr_as_usize = addr.into_bigint().0[0] as usize;
+                    ensure!(
+                        addr_as_usize < self.memory_length,
+                        "RAM Load: address {addr_as_usize} out of bounds for memory of size {}",
+                        self.memory_length
+                    );
                     witness[*read_timestamp] =
                         Some(FieldElement::from(rt_final[addr_as_usize] as u64));
                     rv_final[addr_as_usize] = witness[*value];
@@ -38,6 +44,11 @@ impl SpiceWitnessesSolver for SpiceWitnesses {
                 SpiceMemoryOperation::Store(addr, old_value, new_value, read_timestamp) => {
                     let addr = witness[*addr].unwrap();
                     let addr_as_usize = addr.into_bigint().0[0] as usize;
+                    ensure!(
+                        addr_as_usize < self.memory_length,
+                        "RAM Store: address {addr_as_usize} out of bounds for memory of size {}",
+                        self.memory_length
+                    );
                     witness[*old_value] = rv_final[addr_as_usize];
                     witness[*read_timestamp] =
                         Some(FieldElement::from(rt_final[addr_as_usize] as u64));
@@ -52,5 +63,6 @@ impl SpiceWitnessesSolver for SpiceWitnesses {
             witness[self.rv_final_start + i] = rv_final[i];
             witness[self.rt_final_start + i] = Some(FieldElement::from(rt_final[i] as u64));
         }
+        Ok(())
     }
 }

provekit/prover/src/witness/witness_builder.rs

@@ -12,6 +12,7 @@ use {
         witness::{digits::DigitalDecompositionWitnessesSolver, ram::SpiceWitnessesSolver},
     },
     acir::native_types::WitnessMap,
+    anyhow::{ensure, Result},
     ark_ff::{BigInteger, Field, PrimeField},
     ark_std::Zero,
     provekit_common::{
@@ -31,7 +32,7 @@ pub trait WitnessBuilderSolver {
         acir_witness_idx_to_value_map: &WitnessMap<NoirElement>,
         witness: &mut [Option<FieldElement>],
         transcript: &mut ProverState<TranscriptSponge>,
-    );
+    ) -> Result<()>;
 }
 
 use super::limb_io::{
@@ -58,7 +59,7 @@ impl WitnessBuilderSolver for WitnessBuilder {
         acir_witness_idx_to_value_map: &WitnessMap<NoirElement>,
         witness: &mut [Option<FieldElement>],
         transcript: &mut ProverState<TranscriptSponge>,
-    ) {
+    ) -> Result<()> {
         match self {
             WitnessBuilder::Constant(ConstantTerm(witness_idx, c)) => {
                 witness[*witness_idx] = Some(*c);
@@ -152,6 +153,11 @@ impl WitnessBuilderSolver for WitnessBuilder {
                     // If the value is representable as just a u64, then it should be the least
                     // significant value in the BigInt representation.
                     let value = get_witness(witness, *value_witness_idx).into_bigint().0[0];
+                    ensure!(
+                        (value as usize) < *range_size,
+                        "MultiplicitiesForRange: value {value} out of bounds for range size \
+                         {range_size}"
+                    );
                     multiplicities[value as usize] += 1;
                 }
                 for (i, count) in multiplicities.iter().enumerate() {
@@ -203,7 +209,7 @@ impl WitnessBuilderSolver for WitnessBuilder {
                 );
             }
             WitnessBuilder::SpiceWitnesses(spice_witnesses) => {
-                spice_witnesses.solve(witness);
+                spice_witnesses.solve(witness)?;
             }
             WitnessBuilder::BinOpLookupDenominator(
                 witness_idx,
@@ -249,11 +255,19 @@ impl WitnessBuilderSolver for WitnessBuilder {
                 );
             }
             WitnessBuilder::MultiplicitiesForBinOp(witness_idx, atomic_bits, operands) => {
-                let mut multiplicities = vec![0u32; 2usize.pow(2 * *atomic_bits)];
+                let table_size = 2usize.pow(2 * *atomic_bits);
+                let mut multiplicities = vec![0u32; table_size];
                 for (lhs, rhs) in operands {
                     let lhs = resolve(witness, lhs);
                     let rhs = resolve(witness, rhs);
-                    let index = (lhs.into_bigint().0[0] << *atomic_bits) + rhs.into_bigint().0[0];
+                    let lhs_limb = lhs.into_bigint().0[0];
+                    let rhs_limb = rhs.into_bigint().0[0];
+                    let index = (lhs_limb << *atomic_bits) + rhs_limb;
+                    ensure!(
+                        (index as usize) < table_size,
+                        "MultiplicitiesForBinOp: index {index} (lhs={lhs_limb}, rhs={rhs_limb}, \
+                         atomic_bits={atomic_bits}) out of bounds for table size {table_size}"
+                    );
                     multiplicities[index as usize] += 1;
                 }
                 for (i, count) in multiplicities.iter().enumerate() {
@@ -917,6 +931,11 @@ impl WitnessBuilderSolver for WitnessBuilder {
                 let mut multiplicities = vec![0u32; table_size];
                 for query in queries {
                     let val = resolve(witness, query).into_bigint().0[0];
+                    ensure!(
+                        (val as usize) < table_size,
+                        "MultiplicitiesForSpread: value {val} out of bounds for table size \
+                         {table_size} (num_bits={num_bits})"
+                    );
                     multiplicities[val as usize] += 1;
                 }
                 for (i, count) in multiplicities.iter().enumerate() {
@@ -937,5 +956,6 @@ impl WitnessBuilderSolver for WitnessBuilder {
                 )
             }
         }
+        Ok(())
     }
 }

tooling/provekit-bench/tests/msm_witness_solving.rs

@@ -98,7 +98,8 @@ fn solve_witnesses(
 
     let acir_map = WitnessMap::<NoirElement>::new();
     let mut transcript = dummy_transcript();
-    solve_witness_vec(&mut witness, layers, &acir_map, &mut transcript);
+    solve_witness_vec(&mut witness, layers, &acir_map, &mut transcript)
+        .expect("witness solving failed");
 
     witness
         .into_iter()