Issue #697 - cpu::mem_addr constraints (#773)

0xmozak · Oct 24, 2023 · 60d403f · 60d403f
1 parent ed9315a
commit 60d403f
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 1 deletion.
diff --git a/circuits/src/cpu/columns.rs b/circuits/src/cpu/columns.rs
@@ -359,6 +359,8 @@ impl<T: core::ops::Add<Output = T>> OpSelectors<T> {
     pub fn halfword_mem_ops(self) -> T { self.sh + self.lh }
 
     pub fn fullword_mem_ops(self) -> T { self.sw + self.lw }
+
+    pub fn is_mem_ops(self) -> T { self.sb + self.lb + self.sh + self.lh + self.sw + self.lw }
 }
 
 /// Columns containing the data to be matched against `Bitshift` stark.

diff --git a/circuits/src/cpu/memory.rs b/circuits/src/cpu/memory.rs
@@ -39,6 +39,15 @@ pub(crate) fn signed_constraints<P: PackedField>(
     );
 }
 
+pub(crate) fn constraints<P: PackedField>(
+    lv: &CpuState<P>,
+    yield_constr: &mut ConstraintConsumer<P>,
+) {
+    // memory address is equal to rs2-value + imm (wrapping)
+    yield_constr.constraint(lv.inst.ops.is_mem_ops() * (lv.mem_addr - lv.op2_value));
+    // signed memory constraints
+    signed_constraints(lv, yield_constr);
+}
 #[cfg(test)]
 #[allow(clippy::cast_possible_wrap)]
 mod tests {

diff --git a/circuits/src/cpu/stark.rs b/circuits/src/cpu/stark.rs
@@ -238,7 +238,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
         bitwise::constraints(lv, yield_constr);
         branches::comparison_constraints(lv, yield_constr);
         branches::constraints(lv, nv, yield_constr);
-        memory::signed_constraints(lv, yield_constr);
+        memory::constraints(lv, yield_constr);
         signed_comparison::signed_constraints(lv, yield_constr);
         signed_comparison::slt_constraints(lv, yield_constr);
         shift::constraints(lv, yield_constr);