diff --git a/evm/src/all_stark.rs b/evm/src/all_stark.rs index c6a7b44744..1d78557990 100644 --- a/evm/src/all_stark.rs +++ b/evm/src/all_stark.rs @@ -129,13 +129,22 @@ fn ctl_byte_packing() -> CrossTableLookup { 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, ) } diff --git a/evm/src/byte_packing/byte_packing_stark.rs b/evm/src/byte_packing/byte_packing_stark.rs index 5b3c44911a..3b42fd06e1 100644 --- a/evm/src/byte_packing/byte_packing_stark.rs +++ b/evm/src/byte_packing/byte_packing_stark.rs @@ -68,12 +68,11 @@ pub(crate) fn ctl_looked_data() -> Vec> { // obtain the corresponding limb. let outputs: Vec> = (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(); diff --git a/evm/src/cpu/cpu_stark.rs b/evm/src/cpu/cpu_stark.rs index ef6e74c237..891d1d3827 100644 --- a/evm/src/cpu/cpu_stark.rs +++ b/evm/src/cpu/cpu_stark.rs @@ -157,6 +157,33 @@ pub(crate) fn ctl_filter_byte_unpacking() -> Column { 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() -> Vec> { + 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() -> Column { + 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. diff --git a/evm/src/cpu/stack.rs b/evm/src/cpu/stack.rs index 8710cba361..033c6adcc3 100644 --- a/evm/src/cpu/stack.rs +++ b/evm/src/cpu/stack.rs @@ -102,7 +102,11 @@ pub(crate) const STACK_BEHAVIORS: OpsColumnsView> = OpsCol pushes: true, disable_other_channels: true, }), - push: None, // TODO + push: Some(StackBehavior { + num_pops: 0, + pushes: true, + disable_other_channels: true, + }), dup_swap: None, context_op: None, mload_32bytes: Some(StackBehavior { diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index 6102b47547..f067f797ec 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -178,6 +178,19 @@ impl Column { 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>>( + 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>>(cs: I) -> Self { diff --git a/evm/src/witness/operation.rs b/evm/src/witness/operation.rs index 0c30c6d617..a7228f420c 100644 --- a/evm/src/witness/operation.rs +++ b/evm/src/witness/operation.rs @@ -449,23 +449,26 @@ pub(crate) fn generate_push( } 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(()) diff --git a/evm/tests/empty_txn_list.rs b/evm/tests/empty_txn_list.rs index d2e8ca3301..80b5beb0ec 100644 --- a/evm/tests/empty_txn_list.rs +++ b/evm/tests/empty_txn_list.rs @@ -74,7 +74,7 @@ fn test_empty_txn_list() -> anyhow::Result<()> { let all_circuits = AllRecursiveCircuits::::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, ); diff --git a/evm/tests/log_opcode.rs b/evm/tests/log_opcode.rs index f6fb2a1fd9..309d357bf4 100644 --- a/evm/tests/log_opcode.rs +++ b/evm/tests/log_opcode.rs @@ -459,7 +459,7 @@ fn test_log_with_aggreg() -> anyhow::Result<()> { // Preprocess all circuits. let all_circuits = AllRecursiveCircuits::::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, );