chore: constraint selectors when is_real zero (#873)

succinctlabs · Jun 3, 2024 · c6c0a5d · c6c0a5d
1 parent c3e9337
commit c6c0a5d
Show file tree

Hide file tree

Showing 2 changed files with 41 additions and 5 deletions.
diff --git a/core/src/cpu/air/mod.rs b/core/src/cpu/air/mod.rs
@@ -26,10 +26,12 @@ use crate::operations::BabyBearWordRangeChecker;
 use crate::runtime::Opcode;
 
 use super::columns::eval_channel_selectors;
+use super::columns::OPCODE_SELECTORS_COL_MAP;
 
 impl<AB> Air<AB> for CpuChip
 where
     AB: SP1AirBuilder + AirBuilderWithPublicValues,
+    AB::Var: Sized,
 {
     #[inline(never)]
     fn eval(&self, builder: &mut AB) {
@@ -123,6 +125,27 @@ where
 
         // Check that the is_real flag is correct.
         self.eval_is_real(builder, local, next);
+
+        // Check that when `is_real=0` that all flags that send interactions are zero.
+        local
+            .selectors
+            .into_iter()
+            .enumerate()
+            .for_each(|(i, selector)| {
+                if i == OPCODE_SELECTORS_COL_MAP.imm_b {
+                    builder
+                        .when(AB::Expr::one() - local.is_real)
+                        .assert_one(local.selectors.imm_b);
+                } else if i == OPCODE_SELECTORS_COL_MAP.imm_c {
+                    builder
+                        .when(AB::Expr::one() - local.is_real)
+                        .assert_one(local.selectors.imm_c);
+                } else {
+                    builder
+                        .when(AB::Expr::one() - local.is_real)
+                        .assert_zero(selector);
+                }
+            });
     }
 }
 

diff --git a/core/src/cpu/columns/opcode.rs b/core/src/cpu/columns/opcode.rs
@@ -1,11 +1,23 @@
 use p3_field::PrimeField;
 use sp1_derive::AlignedBorrow;
-use std::mem::size_of;
+use std::mem::{size_of, transmute};
 use std::vec::IntoIter;
 
-use crate::runtime::{Instruction, Opcode};
+use crate::{
+    runtime::{Instruction, Opcode},
+    utils::indices_arr,
+};
 
 pub const NUM_OPCODE_SELECTOR_COLS: usize = size_of::<OpcodeSelectorCols<u8>>();
+pub const OPCODE_SELECTORS_COL_MAP: OpcodeSelectorCols<usize> = make_selectors_col_map();
+
+/// Creates the column map for the CPU.
+const fn make_selectors_col_map() -> OpcodeSelectorCols<usize> {
+    let indices_arr = indices_arr::<NUM_OPCODE_SELECTOR_COLS>();
+    unsafe {
+        transmute::<[usize; NUM_OPCODE_SELECTOR_COLS], OpcodeSelectorCols<usize>>(indices_arr)
+    }
+}
 
 /// The column layout for opcode selectors.
 #[derive(AlignedBorrow, Clone, Copy, Default, Debug)]
@@ -98,7 +110,7 @@ impl<T> IntoIterator for OpcodeSelectorCols<T> {
     type IntoIter = IntoIter<T>;
 
     fn into_iter(self) -> Self::IntoIter {
-        vec![
+        let columns = vec![
             self.imm_b,
             self.imm_c,
             self.is_alu,
@@ -121,7 +133,8 @@ impl<T> IntoIterator for OpcodeSelectorCols<T> {
             self.is_jal,
             self.is_auipc,
             self.is_unimpl,
-        ]
-        .into_iter()
+        ];
+        assert_eq!(columns.len(), NUM_OPCODE_SELECTOR_COLS);
+        columns.into_iter()
     }
 }