Add push constraints

evm/src/all_stark.rs

@@ -129,13 +129,22 @@ fn ctl_byte_packing<F: Field>() -> CrossTableLookup<F> {
         cpu_stark::ctl_data_byte_unpacking(),
         Some(cpu_stark::ctl_filter_byte_unpacking()),
     );
+    let cpu_push_packing_looking = TableWithColumns::new(
+        Table::Cpu,
+        cpu_stark::ctl_data_byte_packing_push(),
+        Some(cpu_stark::ctl_filter_byte_packing_push()),
+    );
     let byte_packing_looked = TableWithColumns::new(
         Table::BytePacking,
         byte_packing_stark::ctl_looked_data(),
         Some(byte_packing_stark::ctl_looked_filter()),
     );
     CrossTableLookup::new(
-        vec![cpu_packing_looking, cpu_unpacking_looking],
+        vec![
+            cpu_packing_looking,
+            cpu_unpacking_looking,
+            cpu_push_packing_looking,
+        ],
         byte_packing_looked,
     )
 }

evm/src/byte_packing/byte_packing_stark.rs

@@ -68,12 +68,11 @@ pub(crate) fn ctl_looked_data<F: Field>() -> Vec<Column<F>> {
     // obtain the corresponding limb.
     let outputs: Vec<Column<F>> = (0..8)
         .map(|i| {
-            let range = (value_bytes(i * 4)..value_bytes(i * 4) + 4).collect_vec();
+            let range = (value_bytes(i * 4)..value_bytes(i * 4) + 4);
             Column::linear_combination(
                 range
-                    .iter()
                     .enumerate()
-                    .map(|(j, &c)| (c, F::from_canonical_u64(1 << (8 * j)))),
+                    .map(|(j, c)| (c, F::from_canonical_u64(1 << (8 * j)))),
             )
         })
         .collect();

evm/src/cpu/cpu_stark.rs

@@ -157,6 +157,33 @@ pub(crate) fn ctl_filter_byte_unpacking<F: Field>() -> Column<F> {
     Column::single(COL_MAP.op.mstore_32bytes)
 }
 
+/// Creates the vector of `Columns` corresponding to the contents of the CPU registers when performing a `PUSH`.
+/// `PUSH` internal reads are done by calling `BytePackingStark`.
+pub(crate) fn ctl_data_byte_packing_push<F: Field>() -> Vec<Column<F>> {
+    let context = Column::single(COL_MAP.code_context);
+    let segment = Column::constant(F::from_canonical_usize(Segment::Code as usize));
+    // The initial offset if `pc + 1`.
+    let virt =
+        Column::linear_combination_with_constant([(COL_MAP.program_counter, F::ONE)], F::ONE);
+    let val = Column::singles_next_row(COL_MAP.mem_channels[0].value);
+
+    // We fetch the length from the `PUSH` opcode lower bits, that indicate `len - 1`.
+    let len = Column::le_bits_with_constant(&COL_MAP.opcode_bits[0..5], F::ONE);
+
+    let num_channels = F::from_canonical_usize(NUM_CHANNELS);
+    let timestamp = Column::linear_combination([(COL_MAP.clock, num_channels)]);
+
+    let mut res = vec![context, segment, virt, len, timestamp];
+    res.extend(val);
+
+    res
+}
+
+/// CTL filter for the `PUSH` operation.
+pub(crate) fn ctl_filter_byte_packing_push<F: Field>() -> Column<F> {
+    Column::single(COL_MAP.op.push)
+}
+
 /// Index of the memory channel storing code.
 pub const MEM_CODE_CHANNEL_IDX: usize = 0;
 /// Index of the first general purpose memory channel.

evm/src/cross_table_lookup.rs

@@ -178,6 +178,19 @@ impl<F: Field> Column<F> {
         Self::linear_combination(cs.into_iter().map(|c| *c.borrow()).zip(F::TWO.powers()))
     }
 
+    /// Given an iterator of columns (c_0, ..., c_n) containing bits in little endian order:
+    /// returns the representation of c_0 + 2 * c_1 + ... + 2^n * c_n + k where `k` is an
+    /// additional constant.
+    pub(crate) fn le_bits_with_constant<I: IntoIterator<Item = impl Borrow<usize>>>(
+        cs: I,
+        constant: F,
+    ) -> Self {
+        Self::linear_combination_with_constant(
+            cs.into_iter().map(|c| *c.borrow()).zip(F::TWO.powers()),
+            constant,
+        )
+    }
+
     /// Given an iterator of columns (c_0, ..., c_n) containing bytes in little endian order:
     /// returns the representation of c_0 + 256 * c_1 + ... + 256^n * c_n.
     pub(crate) fn le_bytes<I: IntoIterator<Item = impl Borrow<usize>>>(cs: I) -> Self {

evm/src/witness/operation.rs

@@ -449,23 +449,26 @@ pub(crate) fn generate_push<F: Field>(
     }
     let initial_offset = state.registers.program_counter + 1;
 
+    let base_address = MemoryAddress::new(code_context, Segment::Code, initial_offset);
     // First read val without going through `mem_read_with_log` type methods, so we can pass it
     // to stack_push_log_and_fill.
     let bytes = (0..num_bytes)
         .map(|i| {
             state
                 .memory
-                .get(MemoryAddress::new(
-                    code_context,
-                    Segment::Code,
-                    initial_offset + i,
-                ))
+                .get(MemoryAddress {
+                    virt: base_address.virt + i,
+                    ..base_address
+                })
                 .low_u32() as u8
         })
         .collect_vec();
 
     let val = U256::from_big_endian(&bytes);
     push_with_write(state, &mut row, val)?;
+
+    byte_packing_log(state, base_address, bytes);
+
     state.traces.push_cpu(row);
 
     Ok(())

evm/tests/empty_txn_list.rs

@@ -74,7 +74,7 @@ fn test_empty_txn_list() -> anyhow::Result<()> {
 
     let all_circuits = AllRecursiveCircuits::<F, C, D>::new(
         &all_stark,
-        &[16..17, 10..11, 15..16, 14..15, 10..11, 12..13, 18..19], // Minimal ranges to prove an empty list
+        &[16..17, 11..12, 15..16, 14..15, 9..10, 12..13, 18..19], // Minimal ranges to prove an empty list
         &config,
     );
 

evm/tests/log_opcode.rs

@@ -459,7 +459,7 @@ fn test_log_with_aggreg() -> anyhow::Result<()> {
     // Preprocess all circuits.
     let all_circuits = AllRecursiveCircuits::<F, C, D>::new(
         &all_stark,
-        &[16..17, 12..14, 17..18, 14..15, 9..11, 12..13, 19..20],
+        &[16..17, 17..19, 17..18, 14..15, 10..11, 12..13, 19..20],
         &config,
     );