From 3aeec83a05a6150fec8b08eeb349f5d4e891e1a5 Mon Sep 17 00:00:00 2001
From: Hamy Ratoanina <hamy.ratoanina@toposware.com>
Date: Thu, 26 Oct 2023 09:59:02 -0400
Subject: [PATCH] Add missing constraints for DUP/SWAP (#1310)

---
 evm/src/cpu/dup_swap.rs | 51 ++++++++++++++++++++++++++++++++++-------
 1 file changed, 43 insertions(+), 8 deletions(-)

diff --git a/evm/src/cpu/dup_swap.rs b/evm/src/cpu/dup_swap.rs
index 0cc6c67c8f..94169d173f 100644
--- 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>(