fix: make range check protocol sound by moving word value evaluation …

…into sumcheck (#440)

# Rationale for this change

Currently, the prover in the range check protocol establishes a column
of values from 0 to the max value that a word can be represented by, in
the case of bytes, 256. This is unsound because the prover could send
commitments to any values and the protocol would successfully verify,
when it is crucial that the word values be the sequentially represented
values that fit inside of the word (in the case of bytes, this is a
column containing all values from 0..256). This PR moves this step of
word value calculation into the actual sumcheck machinery, ensuring that
the correct values are produced during protocol execution.

# What changes are included in this PR?

- [x] Add a new ```rho_256_evaluation``` field to the
```SumcheckMleEvaluations``` struct
- [x] Alter ```SumcheckMleEvaluations``` constructor to produce the
```rho_256_evaluation``` evaluations
- [x] Alter the range check verifier to consume the
```rho_256_evaluation```, assuming that the ```FirstRoundBuilder```
correctly executes the ```produce_one_evaluation_length``` function in a
gadget or test expression.

# Are these changes tested?
Yes, by existing tests

crates/proof-of-sql/src/base/proof/error.rs

@@ -43,4 +43,7 @@ pub enum ProofSizeMismatch {
     /// This error occurs when the proof has too few one lengths.
     #[snafu(display("Proof has too few one lengths"))]
     TooFewOneLengths,
+    /// This error occurs when the proof has too few sumcheck variables.
+    #[snafu(display("Proof has too few sumcheck variables"))]
+    TooFewSumcheckVariables,
 }

crates/proof-of-sql/src/sql/proof/sumcheck_mle_evaluations.rs

@@ -26,6 +26,9 @@ pub struct SumcheckMleEvaluations<'a, S: Scalar> {
     pub random_evaluation: S,
     /// The evaluations (at the random point generated by sumcheck) of the mles that are evaluated by the inner product argument. These are batched together and checked by a single IPA.
     pub pcs_proof_evaluations: &'a [S],
+
+    /// Evaluation (at the random point generated by sumcheck) of the function `rho_256` that is defined by `rho_256(x)` = x when 0 <= x < 256 and 0 otherwise.
+    pub rho_256_evaluation: Option<S>,
 }
 
 #[allow(
@@ -46,6 +49,22 @@ impl<'a, S: Scalar> SumcheckMleEvaluations<'a, S> {
         sumcheck_random_scalars: &SumcheckRandomScalars<S>,
         pcs_proof_evaluations: &'a [S],
     ) -> Self {
+        let rho_256_evaluation = if evaluation_point.len() < 8 {
+            None
+        } else {
+            let rho_256_intermediate = evaluation_point
+                .iter()
+                .take(8)
+                .rev()
+                .fold(S::ZERO, |acc, &x| acc * S::TWO + x);
+            Some(
+                evaluation_point
+                    .iter()
+                    .skip(8)
+                    .fold(rho_256_intermediate, |acc, &x| acc * (S::ONE - x)),
+            )
+        };
+
         assert_eq!(
             evaluation_point.len(),
             sumcheck_random_scalars.entrywise_point.len()
@@ -74,6 +93,7 @@ impl<'a, S: Scalar> SumcheckMleEvaluations<'a, S> {
             singleton_one_evaluation,
             random_evaluation,
             pcs_proof_evaluations,
+            rho_256_evaluation,
         }
     }
 }

crates/proof-of-sql/src/sql/proof_gadgets/range_check.rs

@@ -239,7 +239,6 @@ fn prove_word_values<'a, S: Scalar + 'a>(
     // Allocate from 0 to 255 and pertrub with verifier challenge
     let word_values: &mut [S] =
         alloc.alloc_slice_fill_with(max(256, scalars.len()), |i| S::from(&(i as u8)));
-    builder.produce_intermediate_mle(word_values as &[_]);
 
     // Now produce an intermediate MLE over the inverted word values + verifier challenge alpha
     let word_vals_inv: &mut [S] = alloc.alloc_slice_fill_with(256, |i| {
@@ -274,11 +273,11 @@ fn prove_word_values<'a, S: Scalar + 'a>(
 /// multiplied by the inverted word value, is zero.
 ///
 /// ```text
-/// ∑ (I₀ + I₁ + I₂ + I₃ - (C * IN)) = 0
+/// ∑ (I₀ + I₁ + I₂ ... Iₙ - (C * IN)) = 0
 /// ```
 ///
 /// Where:
-/// - `I₀, I₁, I₂, I₃` are the inverted word columns.
+/// - `I₀ + I₁ + I₂ ... Iₙ` are the inverted word columns.
 /// - `C` is the count of each word.
 /// - `IN` is the inverted word values column.
 #[allow(clippy::missing_panics_doc)]
@@ -378,7 +377,12 @@ where
         "Range check failed, column contains values outside of the selected range"
     );
 
-    let word_vals_eval = builder.try_consume_mle_evaluation()?;
+    let word_vals_eval = builder
+        .mle_evaluations
+        .rho_256_evaluation
+        .ok_or(ProofSizeMismatch::TooFewSumcheckVariables)?;
+    // Ensures that we have enough sumcheck variables
+    let _ = builder.try_consume_one_evaluation()?;
     let word_vals_plus_alpha_inv = builder.try_consume_mle_evaluation()?;
     let word_value_constraint = word_vals_plus_alpha_inv * (word_vals_eval + alpha);
 

crates/proof-of-sql/src/sql/proof_gadgets/range_check_test.rs

@@ -27,6 +27,7 @@ impl ProverEvaluate for RangeCheckTestPlan {
         table_map: &IndexMap<TableRef, Table<'a, S>>,
     ) -> Table<'a, S> {
         builder.request_post_result_challenges(1);
+        builder.produce_one_evaluation_length(256);
         table_map[&self.column.table_ref()].clone()
     }