Add Range Check 128 Builtin Files

stwo_cairo_prover/crates/prover/src/components/mod.rs

@@ -21,6 +21,7 @@ pub mod jump_opcode_double_deref;
 pub mod jump_opcode_rel;
 pub mod jump_opcode_rel_imm;
 pub mod memory;
+pub mod range_check_builtin_bits_128;
 pub mod range_check_vector;
 pub mod ret_opcode;
 pub mod utils;

stwo_cairo_prover/crates/prover/src/components/range_check_builtin_bits_128/component.rs

@@ -0,0 +1,159 @@
+#![allow(non_camel_case_types)]
+#![allow(unused_imports)]
+use num_traits::{One, Zero};
+use serde::{Deserialize, Serialize};
+use stwo_cairo_serialize::CairoSerialize;
+use stwo_prover::constraint_framework::logup::{LogupAtRow, LogupSums, LookupElements};
+use stwo_prover::constraint_framework::{
+    EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry,
+};
+use stwo_prover::core::backend::simd::m31::LOG_N_LANES;
+use stwo_prover::core::channel::Channel;
+use stwo_prover::core::fields::m31::M31;
+use stwo_prover::core::fields::qm31::SecureField;
+use stwo_prover::core::fields::secure_column::SECURE_EXTENSION_DEGREE;
+use stwo_prover::core::pcs::TreeVec;
+
+use crate::cairo_air::preprocessed::{PreProcessedColumn, Seq};
+use crate::relations;
+
+pub struct Eval {
+    pub claim: Claim,
+    pub memory_address_to_id_lookup_elements: relations::MemoryAddressToId,
+    pub memory_id_to_big_lookup_elements: relations::MemoryIdToBig,
+}
+
+#[derive(Copy, Clone, Serialize, Deserialize, CairoSerialize)]
+pub struct Claim {
+    pub log_size: u32,
+    pub range_check_builtin_segment_start: u32,
+}
+impl Claim {
+    pub fn new(log_size: u32, range_check_builtin_segment_start: u32) -> Self {
+        assert!(log_size >= LOG_N_LANES);
+        Self {
+            log_size,
+            range_check_builtin_segment_start,
+        }
+    }
+
+    pub fn log_sizes(&self) -> TreeVec<Vec<u32>> {
+        let log_size = self.log_size;
+        let trace_log_sizes = vec![log_size; 17];
+        let interaction_log_sizes = vec![log_size; SECURE_EXTENSION_DEGREE];
+        let preprocessed_log_sizes = vec![log_size];
+        TreeVec::new(vec![
+            preprocessed_log_sizes,
+            trace_log_sizes,
+            interaction_log_sizes,
+        ])
+    }
+
+    pub fn mix_into(&self, channel: &mut impl Channel) {
+        channel.mix_u64(self.log_size as u64);
+        channel.mix_u64(self.range_check_builtin_segment_start as u64);
+    }
+}
+
+#[derive(Copy, Clone, Serialize, Deserialize, CairoSerialize)]
+pub struct InteractionClaim {
+    pub logup_sums: LogupSums,
+}
+impl InteractionClaim {
+    pub fn mix_into(&self, channel: &mut impl Channel) {
+        let (total_sum, claimed_sum) = self.logup_sums;
+        channel.mix_felts(&[total_sum]);
+        if let Some(claimed_sum) = claimed_sum {
+            channel.mix_felts(&[claimed_sum.0]);
+            channel.mix_u64(claimed_sum.1 as u64);
+        }
+    }
+}
+
+pub type Component = FrameworkComponent<Eval>;
+
+impl FrameworkEval for Eval {
+    fn log_size(&self) -> u32 {
+        self.claim.log_size
+    }
+
+    fn max_constraint_log_degree_bound(&self) -> u32 {
+        self.log_size() + 1
+    }
+
+    #[allow(unused_parens)]
+    #[allow(clippy::double_parens)]
+    #[allow(non_snake_case)]
+    fn evaluate<E: EvalAtRow>(&self, mut eval: E) -> E {
+        let M31_1 = E::F::from(M31::from(1));
+        let M31_2 = E::F::from(M31::from(2));
+        let seq =
+            eval.get_preprocessed_column(PreProcessedColumn::Seq(Seq::new(self.log_size())).id());
+        let value_id_col0 = eval.next_trace_mask();
+        let value_limb_0_col1 = eval.next_trace_mask();
+        let value_limb_1_col2 = eval.next_trace_mask();
+        let value_limb_2_col3 = eval.next_trace_mask();
+        let value_limb_3_col4 = eval.next_trace_mask();
+        let value_limb_4_col5 = eval.next_trace_mask();
+        let value_limb_5_col6 = eval.next_trace_mask();
+        let value_limb_6_col7 = eval.next_trace_mask();
+        let value_limb_7_col8 = eval.next_trace_mask();
+        let value_limb_8_col9 = eval.next_trace_mask();
+        let value_limb_9_col10 = eval.next_trace_mask();
+        let value_limb_10_col11 = eval.next_trace_mask();
+        let value_limb_11_col12 = eval.next_trace_mask();
+        let value_limb_12_col13 = eval.next_trace_mask();
+        let value_limb_13_col14 = eval.next_trace_mask();
+        let value_limb_14_col15 = eval.next_trace_mask();
+        let msb_col16 = eval.next_trace_mask();
+
+        // Read Positive Num Bits 128.
+
+        eval.add_to_relation(RelationEntry::new(
+            &self.memory_address_to_id_lookup_elements,
+            E::EF::one(),
+            &[
+                (E::F::from(M31::from(self.claim.range_check_builtin_segment_start)) + seq.clone()),
+                value_id_col0.clone(),
+            ],
+        ));
+
+        // Range Check Last Limb Bits In Ms Limb 2.
+
+        // msb is a bit.
+        eval.add_constraint((msb_col16.clone() * (M31_1.clone() - msb_col16.clone())));
+        let bit_before_msb_tmp_c9e8f_3 = eval
+            .add_intermediate((value_limb_14_col15.clone() - (msb_col16.clone() * M31_2.clone())));
+        // bit before msb is a bit.
+        eval.add_constraint(
+            (bit_before_msb_tmp_c9e8f_3.clone()
+                * (M31_1.clone() - bit_before_msb_tmp_c9e8f_3.clone())),
+        );
+
+        eval.add_to_relation(RelationEntry::new(
+            &self.memory_id_to_big_lookup_elements,
+            E::EF::one(),
+            &[
+                value_id_col0.clone(),
+                value_limb_0_col1.clone(),
+                value_limb_1_col2.clone(),
+                value_limb_2_col3.clone(),
+                value_limb_3_col4.clone(),
+                value_limb_4_col5.clone(),
+                value_limb_5_col6.clone(),
+                value_limb_6_col7.clone(),
+                value_limb_7_col8.clone(),
+                value_limb_8_col9.clone(),
+                value_limb_9_col10.clone(),
+                value_limb_10_col11.clone(),
+                value_limb_11_col12.clone(),
+                value_limb_12_col13.clone(),
+                value_limb_13_col14.clone(),
+                value_limb_14_col15.clone(),
+            ],
+        ));
+
+        eval.finalize_logup_in_pairs();
+        eval
+    }
+}

stwo_cairo_prover/crates/prover/src/components/range_check_builtin_bits_128/mod.rs

@@ -0,0 +1,5 @@
+pub mod component;
+pub mod prover;
+
+pub use component::{Claim, Component, Eval, InteractionClaim};
+pub use prover::{ClaimGenerator, InteractionClaimGenerator};