From 48e2b24b4940273bc68161b02b24ec1855a4ccd1 Mon Sep 17 00:00:00 2001
From: Linda Guiga <101227802+LindaGuiga@users.noreply.github.com>
Date: Wed, 22 Nov 2023 15:59:41 -0500
Subject: [PATCH] Add range check constraints for the looked table (#1380)

* Add constraints to check that looked tables are well constructed for range checks

* Fix comments
---
 evm/src/byte_packing/byte_packing_stark.rs   | 25 ++++++++++++++++++++
 evm/src/keccak_sponge/keccak_sponge_stark.rs | 25 ++++++++++++++++++++
 evm/src/memory/memory_stark.rs               | 17 +++++++++++++
 3 files changed, 67 insertions(+)

diff --git a/evm/src/byte_packing/byte_packing_stark.rs b/evm/src/byte_packing/byte_packing_stark.rs
index 3b42fd06..53273361 100644
--- a/evm/src/byte_packing/byte_packing_stark.rs
+++ b/evm/src/byte_packing/byte_packing_stark.rs
@@ -311,6 +311,17 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for BytePackingSt
         let local_values: &[P; NUM_COLUMNS] = vars.get_local_values().try_into().unwrap();
         let next_values: &[P; NUM_COLUMNS] = vars.get_next_values().try_into().unwrap();
 
+        // Check the range column: First value must be 0, last row
+        // must be 255, and intermediate rows must increment by 0
+        // or 1.
+        let rc1 = local_values[RANGE_COUNTER];
+        let rc2 = next_values[RANGE_COUNTER];
+        yield_constr.constraint_first_row(rc1);
+        let incr = rc2 - rc1;
+        yield_constr.constraint_transition(incr * incr - incr);
+        let range_max = P::Scalar::from_canonical_u64((BYTE_RANGE_MAX - 1) as u64);
+        yield_constr.constraint_last_row(rc1 - range_max);
+
         let one = P::ONES;
 
         // We filter active columns by summing all the byte indices.
@@ -421,6 +432,20 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for BytePackingSt
         let next_values: &[ExtensionTarget<D>; NUM_COLUMNS] =
             vars.get_next_values().try_into().unwrap();
 
+        // Check the range column: First value must be 0, last row
+        // must be 255, and intermediate rows must increment by 0
+        // or 1.
+        let rc1 = local_values[RANGE_COUNTER];
+        let rc2 = next_values[RANGE_COUNTER];
+        yield_constr.constraint_first_row(builder, rc1);
+        let incr = builder.sub_extension(rc2, rc1);
+        let t = builder.mul_sub_extension(incr, incr, incr);
+        yield_constr.constraint_transition(builder, t);
+        let range_max =
+            builder.constant_extension(F::Extension::from_canonical_usize(BYTE_RANGE_MAX - 1));
+        let t = builder.sub_extension(rc1, range_max);
+        yield_constr.constraint_last_row(builder, t);
+
         // We filter active columns by summing all the byte indices.
         // Constraining each of them to be boolean is done later on below.
         let current_filter = builder.add_many_extension(&local_values[BYTE_INDICES_COLS]);
diff --git a/evm/src/keccak_sponge/keccak_sponge_stark.rs b/evm/src/keccak_sponge/keccak_sponge_stark.rs
index a89be91c..f972a32a 100644
--- a/evm/src/keccak_sponge/keccak_sponge_stark.rs
+++ b/evm/src/keccak_sponge/keccak_sponge_stark.rs
@@ -537,6 +537,17 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for KeccakSpongeS
             vars.get_next_values().try_into().unwrap();
         let next_values: &KeccakSpongeColumnsView<P> = next_values.borrow();
 
+        // Check the range column: First value must be 0, last row
+        // must be 255, and intermediate rows must increment by 0
+        // or 1.
+        let rc1 = local_values.range_counter;
+        let rc2 = next_values.range_counter;
+        yield_constr.constraint_first_row(rc1);
+        let incr = rc2 - rc1;
+        yield_constr.constraint_transition(incr * incr - incr);
+        let range_max = P::Scalar::from_canonical_u64((BYTE_RANGE_MAX - 1) as u64);
+        yield_constr.constraint_last_row(rc1 - range_max);
+
         // Each flag (full-input block, final block or implied dummy flag) must be boolean.
         let is_full_input_block = local_values.is_full_input_block;
         yield_constr.constraint(is_full_input_block * (is_full_input_block - P::ONES));
@@ -643,6 +654,20 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for KeccakSpongeS
 
         let one = builder.one_extension();
 
+        // Check the range column: First value must be 0, last row
+        // must be 255, and intermediate rows must increment by 0
+        // or 1.
+        let rc1 = local_values.range_counter;
+        let rc2 = next_values.range_counter;
+        yield_constr.constraint_first_row(builder, rc1);
+        let incr = builder.sub_extension(rc2, rc1);
+        let t = builder.mul_sub_extension(incr, incr, incr);
+        yield_constr.constraint_transition(builder, t);
+        let range_max =
+            builder.constant_extension(F::Extension::from_canonical_usize(BYTE_RANGE_MAX - 1));
+        let t = builder.sub_extension(rc1, range_max);
+        yield_constr.constraint_last_row(builder, t);
+
         // Each flag (full-input block, final block or implied dummy flag) must be boolean.
         let is_full_input_block = local_values.is_full_input_block;
         let constraint = builder.mul_sub_extension(
diff --git a/evm/src/memory/memory_stark.rs b/evm/src/memory/memory_stark.rs
index 689351e5..aa0ec79a 100644
--- a/evm/src/memory/memory_stark.rs
+++ b/evm/src/memory/memory_stark.rs
@@ -335,6 +335,14 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
             yield_constr
                 .constraint_transition(next_is_read * not_address_unchanged * next_values_limbs[i]);
         }
+
+        // Check the range column: First value must be 0,
+        // and intermediate rows must increment by 1.
+        let rc1 = local_values[COUNTER];
+        let rc2 = next_values[COUNTER];
+        yield_constr.constraint_first_row(rc1);
+        let incr = rc2 - rc1;
+        yield_constr.constraint_transition(incr - P::Scalar::ONES);
     }
 
     fn eval_ext_circuit(
@@ -463,6 +471,15 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for MemoryStark<F
             let first_read_constraint = builder.mul_extension(first_read_value, next_is_read);
             yield_constr.constraint_transition(builder, first_read_constraint);
         }
+
+        // Check the range column: First value must be 0,
+        // and intermediate rows must increment by 1.
+        let rc1 = local_values[COUNTER];
+        let rc2 = next_values[COUNTER];
+        yield_constr.constraint_first_row(builder, rc1);
+        let incr = builder.sub_extension(rc2, rc1);
+        let t = builder.sub_extension(incr, one);
+        yield_constr.constraint_transition(builder, t);
     }
 
     fn constraint_degree(&self) -> usize {