Add missing constraints for DUP/SWAP (#1310)

0xPolygonZero · Oct 26, 2023 · 3aeec83 · 3aeec83
1 parent 44af80f
commit 3aeec83
Showing 1 changed file with 43 additions and 8 deletions.
diff --git a/evm/src/cpu/dup_swap.rs b/evm/src/cpu/dup_swap.rs
@@ -6,6 +6,7 @@ use plonky2::hash::hash_types::RichField;
 use plonky2::iop::ext_target::ExtensionTarget;
 use plonky2::plonk::circuit_builder::CircuitBuilder;
 
+use super::membus::NUM_GP_CHANNELS;
 use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
 use crate::cpu::columns::{CpuColumnsView, MemoryChannelView};
 use crate::memory::segments::Segment;
@@ -129,7 +130,13 @@ fn eval_packed_dup<P: PackedField>(
     // Constrain nv.stack_len.
     yield_constr.constraint_transition(filter * (nv.stack_len - lv.stack_len - P::ONES));
 
-    // TODO: Constrain unused channels?
+    // Disable next top.
+    yield_constr.constraint(filter * nv.mem_channels[0].used);
+
+    // Constrain unused channels.
+    for i in 3..NUM_GP_CHANNELS {
+        yield_constr.constraint(filter * lv.mem_channels[i].used);
+    }
 }
 
 fn eval_ext_circuit_dup<F: RichField + Extendable<D>, const D: usize>(
@@ -175,11 +182,23 @@ fn eval_ext_circuit_dup<F: RichField + Extendable<D>, const D: usize>(
     constrain_channel_ext_circuit(builder, true, filter, n, read_channel, lv, yield_constr);
 
     // Constrain nv.stack_len.
-    let diff = builder.sub_extension(nv.stack_len, lv.stack_len);
-    let constr = builder.mul_sub_extension(filter, diff, filter);
-    yield_constr.constraint_transition(builder, constr);
+    {
+        let diff = builder.sub_extension(nv.stack_len, lv.stack_len);
+        let constr = builder.mul_sub_extension(filter, diff, filter);
+        yield_constr.constraint_transition(builder, constr);
+    }
 
-    // TODO: Constrain unused channels?
+    // Disable next top.
+    {
+        let constr = builder.mul_extension(filter, nv.mem_channels[0].used);
+        yield_constr.constraint(builder, constr);
+    }
+
+    // Constrain unused channels.
+    for i in 3..NUM_GP_CHANNELS {
+        let constr = builder.mul_extension(filter, lv.mem_channels[i].used);
+        yield_constr.constraint(builder, constr);
+    }
 }
 
 fn eval_packed_swap<P: PackedField>(
@@ -203,10 +222,16 @@ fn eval_packed_swap<P: PackedField>(
     channels_equal_packed(filter, in2_channel, &nv.mem_channels[0], yield_constr);
     constrain_channel_packed(true, filter, n_plus_one, in2_channel, lv, yield_constr);
 
-    // Constrain nv.stack_len;
+    // Constrain nv.stack_len.
     yield_constr.constraint(filter * (nv.stack_len - lv.stack_len));
 
-    // TODO: Constrain unused channels?
+    // Disable next top.
+    yield_constr.constraint(filter * nv.mem_channels[0].used);
+
+    // Constrain unused channels.
+    for i in 3..NUM_GP_CHANNELS {
+        yield_constr.constraint(filter * lv.mem_channels[i].used);
+    }
 }
 
 fn eval_ext_circuit_swap<F: RichField + Extendable<D>, const D: usize>(
@@ -259,7 +284,17 @@ fn eval_ext_circuit_swap<F: RichField + Extendable<D>, const D: usize>(
     let constr = builder.mul_extension(filter, diff);
     yield_constr.constraint(builder, constr);
 
-    // TODO: Constrain unused channels?
+    // Disable next top.
+    {
+        let constr = builder.mul_extension(filter, nv.mem_channels[0].used);
+        yield_constr.constraint(builder, constr);
+    }
+
+    // Constrain unused channels.
+    for i in 3..NUM_GP_CHANNELS {
+        let constr = builder.mul_extension(filter, lv.mem_channels[i].used);
+        yield_constr.constraint(builder, constr);
+    }
 }
 
 pub fn eval_packed<P: PackedField>(