From ee9ce4c59d2b5e8ebda0a3938a2bed491bfac42f Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Mon, 7 Aug 2023 15:04:03 -0400 Subject: [PATCH 1/4] Combine AND and OR flags in CpuStark --- evm/src/cpu/columns/ops.rs | 5 ++--- evm/src/cpu/control_flow.rs | 5 ++--- evm/src/cpu/cpu_stark.rs | 4 ++-- evm/src/cpu/decode.rs | 5 ++--- evm/src/cpu/gas.rs | 3 +-- evm/src/cpu/stack.rs | 3 +-- evm/src/keccak_sponge/keccak_sponge_stark.rs | 3 +-- evm/src/logic.rs | 3 +-- evm/src/witness/transition.rs | 5 +++-- 9 files changed, 15 insertions(+), 21 deletions(-) diff --git a/evm/src/cpu/columns/ops.rs b/evm/src/cpu/columns/ops.rs index 663653ad..8b449f40 100644 --- a/evm/src/cpu/columns/ops.rs +++ b/evm/src/cpu/columns/ops.rs @@ -24,9 +24,8 @@ pub struct OpsColumnsView { pub gt: T, pub eq: T, // Note: This column must be 0 when is_cpu_cycle = 0. pub iszero: T, // Note: This column must be 0 when is_cpu_cycle = 0. - // TODO: combine AND, OR, and XOR into one flag - pub and: T, - pub or: T, + // TODO: combine AND/OR, and XOR into one flag + pub and_or: T, pub xor: T, pub not: T, pub byte: T, diff --git a/evm/src/cpu/control_flow.rs b/evm/src/cpu/control_flow.rs index 35546bb7..abbaa7ce 100644 --- a/evm/src/cpu/control_flow.rs +++ b/evm/src/cpu/control_flow.rs @@ -8,7 +8,7 @@ use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer use crate::cpu::columns::{CpuColumnsView, COL_MAP}; use crate::cpu::kernel::aggregator::KERNEL; -const NATIVE_INSTRUCTIONS: [usize; 32] = [ +const NATIVE_INSTRUCTIONS: [usize; 31] = [ COL_MAP.op.add, COL_MAP.op.mul, COL_MAP.op.sub, @@ -23,8 +23,7 @@ const NATIVE_INSTRUCTIONS: [usize; 32] = [ COL_MAP.op.gt, COL_MAP.op.eq, COL_MAP.op.iszero, - COL_MAP.op.and, - COL_MAP.op.or, + COL_MAP.op.and_or, COL_MAP.op.xor, COL_MAP.op.not, COL_MAP.op.shl, diff --git a/evm/src/cpu/cpu_stark.rs b/evm/src/cpu/cpu_stark.rs index 16b72725..883b6043 100644 --- a/evm/src/cpu/cpu_stark.rs +++ b/evm/src/cpu/cpu_stark.rs @@ -83,11 +83,11 @@ fn ctl_data_ternops(ops: &[usize], is_shift: bool) -> Vec> { } pub fn ctl_data_logic() -> Vec> { - ctl_data_binops(&[COL_MAP.op.and, COL_MAP.op.or, COL_MAP.op.xor]) + ctl_data_binops(&[COL_MAP.op.and_or, COL_MAP.op.xor]) } pub fn ctl_filter_logic() -> Column { - Column::sum([COL_MAP.op.and, COL_MAP.op.or, COL_MAP.op.xor]) + Column::sum([COL_MAP.op.and_or, COL_MAP.op.xor]) } pub fn ctl_arithmetic_base_rows() -> TableWithColumns { diff --git a/evm/src/cpu/decode.rs b/evm/src/cpu/decode.rs index 459fca62..36a5eca4 100644 --- a/evm/src/cpu/decode.rs +++ b/evm/src/cpu/decode.rs @@ -22,7 +22,7 @@ use crate::cpu::columns::{CpuColumnsView, COL_MAP}; /// behavior. /// Note: invalid opcodes are not represented here. _Any_ opcode is permitted to decode to /// `is_invalid`. The kernel then verifies that the opcode was _actually_ invalid. -const OPCODES: [(u8, usize, bool, usize); 37] = [ +const OPCODES: [(u8, usize, bool, usize); 36] = [ // (start index of block, number of top bits to check (log2), kernel-only, flag column) (0x01, 0, false, COL_MAP.op.add), (0x02, 0, false, COL_MAP.op.mul), @@ -38,8 +38,7 @@ const OPCODES: [(u8, usize, bool, usize); 37] = [ (0x11, 0, false, COL_MAP.op.gt), (0x14, 0, false, COL_MAP.op.eq), (0x15, 0, false, COL_MAP.op.iszero), - (0x16, 0, false, COL_MAP.op.and), - (0x17, 0, false, COL_MAP.op.or), + (0x16, 1, false, COL_MAP.op.and_or), (0x18, 0, false, COL_MAP.op.xor), (0x19, 0, false, COL_MAP.op.not), (0x1a, 0, false, COL_MAP.op.byte), diff --git a/evm/src/cpu/gas.rs b/evm/src/cpu/gas.rs index 9fb32298..6da9cc84 100644 --- a/evm/src/cpu/gas.rs +++ b/evm/src/cpu/gas.rs @@ -33,8 +33,7 @@ const SIMPLE_OPCODES: OpsColumnsView> = OpsColumnsView { gt: G_VERYLOW, eq: G_VERYLOW, iszero: G_VERYLOW, - and: G_VERYLOW, - or: G_VERYLOW, + and_or: G_VERYLOW, xor: G_VERYLOW, not: G_VERYLOW, byte: G_VERYLOW, diff --git a/evm/src/cpu/stack.rs b/evm/src/cpu/stack.rs index 5a04b661..f6bd9892 100644 --- a/evm/src/cpu/stack.rs +++ b/evm/src/cpu/stack.rs @@ -55,8 +55,7 @@ const STACK_BEHAVIORS: OpsColumnsView> = OpsColumnsView { gt: BASIC_BINARY_OP, eq: BASIC_BINARY_OP, iszero: BASIC_UNARY_OP, - and: BASIC_BINARY_OP, - or: BASIC_BINARY_OP, + and_or: BASIC_BINARY_OP, xor: BASIC_BINARY_OP, not: BASIC_UNARY_OP, byte: BASIC_BINARY_OP, diff --git a/evm/src/keccak_sponge/keccak_sponge_stark.rs b/evm/src/keccak_sponge/keccak_sponge_stark.rs index b40a2488..c8cbbd48 100644 --- a/evm/src/keccak_sponge/keccak_sponge_stark.rs +++ b/evm/src/keccak_sponge/keccak_sponge_stark.rs @@ -103,8 +103,7 @@ pub(crate) fn ctl_looking_logic(i: usize) -> Vec> { let cols = KECCAK_SPONGE_COL_MAP; let mut res = vec![ - Column::zero(), // is_and - Column::zero(), // is_or + Column::zero(), // is_and_or Column::one(), // is_xor ]; diff --git a/evm/src/logic.rs b/evm/src/logic.rs index b7429610..0c069762 100644 --- a/evm/src/logic.rs +++ b/evm/src/logic.rs @@ -53,8 +53,7 @@ pub(crate) mod columns { pub fn ctl_data() -> Vec> { let mut res = vec![ - Column::single(columns::IS_AND), - Column::single(columns::IS_OR), + Column::sum([columns::IS_AND, columns::IS_OR]), Column::single(columns::IS_XOR), ]; res.extend(columns::limb_bit_cols_for_input(columns::INPUT0).map(Column::le_bits)); diff --git a/evm/src/witness/transition.rs b/evm/src/witness/transition.rs index c5937c7f..dcac4e71 100644 --- a/evm/src/witness/transition.rs +++ b/evm/src/witness/transition.rs @@ -160,8 +160,9 @@ fn fill_op_flag(op: Operation, row: &mut CpuColumnsView) { Operation::Not => &mut flags.not, Operation::Syscall(_, _, _) => &mut flags.syscall, Operation::Eq => &mut flags.eq, - Operation::BinaryLogic(logic::Op::And) => &mut flags.and, - Operation::BinaryLogic(logic::Op::Or) => &mut flags.or, + Operation::BinaryLogic(logic::Op::And) | Operation::BinaryLogic(logic::Op::Or) => { + &mut flags.and_or + } Operation::BinaryLogic(logic::Op::Xor) => &mut flags.xor, Operation::BinaryArithmetic(arithmetic::BinaryOperator::Add) => &mut flags.add, Operation::BinaryArithmetic(arithmetic::BinaryOperator::Mul) => &mut flags.mul, From 437f57a862751f7ae9aa28587379311924989f9a Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Fri, 11 Aug 2023 09:23:58 -0400 Subject: [PATCH 2/4] Fix logic CTL --- evm/src/cpu/cpu_stark.rs | 4 +++- evm/src/keccak_sponge/keccak_sponge_stark.rs | 3 +-- evm/src/logic.rs | 9 +++++---- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/evm/src/cpu/cpu_stark.rs b/evm/src/cpu/cpu_stark.rs index 883b6043..d54cf625 100644 --- a/evm/src/cpu/cpu_stark.rs +++ b/evm/src/cpu/cpu_stark.rs @@ -83,7 +83,9 @@ fn ctl_data_ternops(ops: &[usize], is_shift: bool) -> Vec> { } pub fn ctl_data_logic() -> Vec> { - ctl_data_binops(&[COL_MAP.op.and_or, COL_MAP.op.xor]) + let mut res = vec![Column::le_bits(COL_MAP.opcode_bits)]; + res.extend(ctl_data_binops(&[])); + res } pub fn ctl_filter_logic() -> Column { diff --git a/evm/src/keccak_sponge/keccak_sponge_stark.rs b/evm/src/keccak_sponge/keccak_sponge_stark.rs index c8cbbd48..32d3a555 100644 --- a/evm/src/keccak_sponge/keccak_sponge_stark.rs +++ b/evm/src/keccak_sponge/keccak_sponge_stark.rs @@ -103,8 +103,7 @@ pub(crate) fn ctl_looking_logic(i: usize) -> Vec> { let cols = KECCAK_SPONGE_COL_MAP; let mut res = vec![ - Column::zero(), // is_and_or - Column::one(), // is_xor + Column::constant(F::from_canonical_u8(0x18)), // is_xor ]; // Input 0 contains some of the sponge's original rate chunks. If this is the last CTL, we won't diff --git a/evm/src/logic.rs b/evm/src/logic.rs index 0c069762..3695503b 100644 --- a/evm/src/logic.rs +++ b/evm/src/logic.rs @@ -52,10 +52,11 @@ pub(crate) mod columns { } pub fn ctl_data() -> Vec> { - let mut res = vec![ - Column::sum([columns::IS_AND, columns::IS_OR]), - Column::single(columns::IS_XOR), - ]; + let mut res = vec![Column::linear_combination([ + (columns::IS_AND, F::from_canonical_u8(0x16)), + (columns::IS_OR, F::from_canonical_u8(0x17)), + (columns::IS_XOR, F::from_canonical_u8(0x18)), + ])]; res.extend(columns::limb_bit_cols_for_input(columns::INPUT0).map(Column::le_bits)); res.extend(columns::limb_bit_cols_for_input(columns::INPUT1).map(Column::le_bits)); res.extend(columns::RESULT.map(Column::single)); From e10eaad09b6d3da5ff196523a052ca21ed7f2144 Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Fri, 11 Aug 2023 10:17:45 -0400 Subject: [PATCH 3/4] Combine all logic flags together --- evm/src/cpu/columns/ops.rs | 8 +++----- evm/src/cpu/control_flow.rs | 5 ++--- evm/src/cpu/cpu_stark.rs | 2 +- evm/src/cpu/decode.rs | 30 +++++++++++++++++++++++++----- evm/src/cpu/gas.rs | 3 +-- evm/src/cpu/stack.rs | 3 +-- evm/src/logic.rs | 4 ++++ evm/src/witness/transition.rs | 5 +---- 8 files changed, 38 insertions(+), 22 deletions(-) diff --git a/evm/src/cpu/columns/ops.rs b/evm/src/cpu/columns/ops.rs index 8b449f40..ecc5e83a 100644 --- a/evm/src/cpu/columns/ops.rs +++ b/evm/src/cpu/columns/ops.rs @@ -22,11 +22,9 @@ pub struct OpsColumnsView { pub submod: T, pub lt: T, pub gt: T, - pub eq: T, // Note: This column must be 0 when is_cpu_cycle = 0. - pub iszero: T, // Note: This column must be 0 when is_cpu_cycle = 0. - // TODO: combine AND/OR, and XOR into one flag - pub and_or: T, - pub xor: T, + pub eq: T, // Note: This column must be 0 when is_cpu_cycle = 0. + pub iszero: T, // Note: This column must be 0 when is_cpu_cycle = 0. + pub logic_op: T, // Combines AND, OR and XOR flags. pub not: T, pub byte: T, // TODO: combine SHL and SHR into one flag diff --git a/evm/src/cpu/control_flow.rs b/evm/src/cpu/control_flow.rs index abbaa7ce..eec2378b 100644 --- a/evm/src/cpu/control_flow.rs +++ b/evm/src/cpu/control_flow.rs @@ -8,7 +8,7 @@ use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer use crate::cpu::columns::{CpuColumnsView, COL_MAP}; use crate::cpu::kernel::aggregator::KERNEL; -const NATIVE_INSTRUCTIONS: [usize; 31] = [ +const NATIVE_INSTRUCTIONS: [usize; 30] = [ COL_MAP.op.add, COL_MAP.op.mul, COL_MAP.op.sub, @@ -23,8 +23,7 @@ const NATIVE_INSTRUCTIONS: [usize; 31] = [ COL_MAP.op.gt, COL_MAP.op.eq, COL_MAP.op.iszero, - COL_MAP.op.and_or, - COL_MAP.op.xor, + COL_MAP.op.logic_op, COL_MAP.op.not, COL_MAP.op.shl, COL_MAP.op.shr, diff --git a/evm/src/cpu/cpu_stark.rs b/evm/src/cpu/cpu_stark.rs index d54cf625..19cca992 100644 --- a/evm/src/cpu/cpu_stark.rs +++ b/evm/src/cpu/cpu_stark.rs @@ -89,7 +89,7 @@ pub fn ctl_data_logic() -> Vec> { } pub fn ctl_filter_logic() -> Column { - Column::sum([COL_MAP.op.and_or, COL_MAP.op.xor]) + Column::single(COL_MAP.op.logic_op) } pub fn ctl_arithmetic_base_rows() -> TableWithColumns { diff --git a/evm/src/cpu/decode.rs b/evm/src/cpu/decode.rs index 36a5eca4..e8d595b3 100644 --- a/evm/src/cpu/decode.rs +++ b/evm/src/cpu/decode.rs @@ -22,7 +22,7 @@ use crate::cpu::columns::{CpuColumnsView, COL_MAP}; /// behavior. /// Note: invalid opcodes are not represented here. _Any_ opcode is permitted to decode to /// `is_invalid`. The kernel then verifies that the opcode was _actually_ invalid. -const OPCODES: [(u8, usize, bool, usize); 36] = [ +const OPCODES: [(u8, usize, bool, usize); 34] = [ // (start index of block, number of top bits to check (log2), kernel-only, flag column) (0x01, 0, false, COL_MAP.op.add), (0x02, 0, false, COL_MAP.op.mul), @@ -38,8 +38,7 @@ const OPCODES: [(u8, usize, bool, usize); 36] = [ (0x11, 0, false, COL_MAP.op.gt), (0x14, 0, false, COL_MAP.op.eq), (0x15, 0, false, COL_MAP.op.iszero), - (0x16, 1, false, COL_MAP.op.and_or), - (0x18, 0, false, COL_MAP.op.xor), + // AND, OR and XOR flags are handled directly on the logic table side (0x19, 0, false, COL_MAP.op.not), (0x1a, 0, false, COL_MAP.op.byte), (0x1b, 0, false, COL_MAP.op.shl), @@ -143,11 +142,21 @@ pub fn eval_packed_generic( let flag = lv[flag_col]; yield_constr.constraint(cycle_filter * flag * (flag - P::ONES)); } + // Manually check for the logic_op flag combining AND, OR and XOR. + // TODO: This would go away once cycle_filter is replaced by the sum + // of all CPU opcode flags. + let flag = lv.op.logic_op; + yield_constr.constraint(cycle_filter * flag * (flag - P::ONES)); + // Now check that they sum to 0 or 1. + // Include the logic_op flag encompassing AND, OR and XOR opcodes. + // TODO: This would go away once cycle_filter is replaced by the sum + // of all CPU opcode flags. let flag_sum: P = OPCODES .into_iter() .map(|(_, _, _, flag_col)| lv[flag_col]) - .sum::

(); + .sum::

() + + lv.op.logic_op; yield_constr.constraint(cycle_filter * flag_sum * (flag_sum - P::ONES)); // Finally, classify all opcodes, together with the kernel flag, into blocks @@ -211,9 +220,20 @@ pub fn eval_ext_circuit, const D: usize>( let constr = builder.mul_extension(cycle_filter, constr); yield_constr.constraint(builder, constr); } + // Manually check for the logic_op flag combining AND, OR and XOR. + // TODO: This would go away once cycle_filter is replaced by the sum + // of all CPU opcode flags. + let flag = lv.op.logic_op; + let constr = builder.mul_sub_extension(flag, flag, flag); + let constr = builder.mul_extension(cycle_filter, constr); + yield_constr.constraint(builder, constr); + // Now check that they sum to 0 or 1. + // Include the logic_op flag encompassing AND, OR and XOR opcodes. + // TODO: This would go away once cycle_filter is replaced by the sum + // of all CPU opcode flags. { - let mut flag_sum = builder.zero_extension(); + let mut flag_sum = lv.op.logic_op; for (_, _, _, flag_col) in OPCODES { let flag = lv[flag_col]; flag_sum = builder.add_extension(flag_sum, flag); diff --git a/evm/src/cpu/gas.rs b/evm/src/cpu/gas.rs index 6da9cc84..a7235137 100644 --- a/evm/src/cpu/gas.rs +++ b/evm/src/cpu/gas.rs @@ -33,8 +33,7 @@ const SIMPLE_OPCODES: OpsColumnsView> = OpsColumnsView { gt: G_VERYLOW, eq: G_VERYLOW, iszero: G_VERYLOW, - and_or: G_VERYLOW, - xor: G_VERYLOW, + logic_op: G_VERYLOW, not: G_VERYLOW, byte: G_VERYLOW, shl: G_VERYLOW, diff --git a/evm/src/cpu/stack.rs b/evm/src/cpu/stack.rs index f6bd9892..ef290d0a 100644 --- a/evm/src/cpu/stack.rs +++ b/evm/src/cpu/stack.rs @@ -55,8 +55,7 @@ const STACK_BEHAVIORS: OpsColumnsView> = OpsColumnsView { gt: BASIC_BINARY_OP, eq: BASIC_BINARY_OP, iszero: BASIC_UNARY_OP, - and_or: BASIC_BINARY_OP, - xor: BASIC_BINARY_OP, + logic_op: BASIC_BINARY_OP, not: BASIC_UNARY_OP, byte: BASIC_BINARY_OP, shl: Some(StackBehavior { diff --git a/evm/src/logic.rs b/evm/src/logic.rs index 3695503b..3529ed9a 100644 --- a/evm/src/logic.rs +++ b/evm/src/logic.rs @@ -52,6 +52,10 @@ pub(crate) mod columns { } pub fn ctl_data() -> Vec> { + // We scale each filter flag with the associated opcode value. + // If a logic operation is happening on the CPU side, the CTL + // will enforce that the reconstructed opcode value from the + // opcode bits matches. let mut res = vec![Column::linear_combination([ (columns::IS_AND, F::from_canonical_u8(0x16)), (columns::IS_OR, F::from_canonical_u8(0x17)), diff --git a/evm/src/witness/transition.rs b/evm/src/witness/transition.rs index dcac4e71..b8929114 100644 --- a/evm/src/witness/transition.rs +++ b/evm/src/witness/transition.rs @@ -160,10 +160,7 @@ fn fill_op_flag(op: Operation, row: &mut CpuColumnsView) { Operation::Not => &mut flags.not, Operation::Syscall(_, _, _) => &mut flags.syscall, Operation::Eq => &mut flags.eq, - Operation::BinaryLogic(logic::Op::And) | Operation::BinaryLogic(logic::Op::Or) => { - &mut flags.and_or - } - Operation::BinaryLogic(logic::Op::Xor) => &mut flags.xor, + Operation::BinaryLogic(_) => &mut flags.logic_op, Operation::BinaryArithmetic(arithmetic::BinaryOperator::Add) => &mut flags.add, Operation::BinaryArithmetic(arithmetic::BinaryOperator::Mul) => &mut flags.mul, Operation::BinaryArithmetic(arithmetic::BinaryOperator::Sub) => &mut flags.sub, From 654f7cac42afc7c379d3145e13dbbdcf82e13e7e Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Fri, 11 Aug 2023 10:21:11 -0400 Subject: [PATCH 4/4] Comment --- evm/src/cpu/cpu_stark.rs | 1 + evm/src/cpu/decode.rs | 10 +++++----- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/evm/src/cpu/cpu_stark.rs b/evm/src/cpu/cpu_stark.rs index 19cca992..25a3c5e7 100644 --- a/evm/src/cpu/cpu_stark.rs +++ b/evm/src/cpu/cpu_stark.rs @@ -83,6 +83,7 @@ fn ctl_data_ternops(ops: &[usize], is_shift: bool) -> Vec> { } pub fn ctl_data_logic() -> Vec> { + // Instead of taking single columns, we reconstruct the entire opcode value directly. let mut res = vec![Column::le_bits(COL_MAP.opcode_bits)]; res.extend(ctl_data_binops(&[])); res diff --git a/evm/src/cpu/decode.rs b/evm/src/cpu/decode.rs index e8d595b3..88c44c7c 100644 --- a/evm/src/cpu/decode.rs +++ b/evm/src/cpu/decode.rs @@ -38,7 +38,7 @@ const OPCODES: [(u8, usize, bool, usize); 34] = [ (0x11, 0, false, COL_MAP.op.gt), (0x14, 0, false, COL_MAP.op.eq), (0x15, 0, false, COL_MAP.op.iszero), - // AND, OR and XOR flags are handled directly on the logic table side + // AND, OR and XOR flags are handled partly manually here, and partly through the Logic table CTL. (0x19, 0, false, COL_MAP.op.not), (0x1a, 0, false, COL_MAP.op.byte), (0x1b, 0, false, COL_MAP.op.shl), @@ -142,14 +142,14 @@ pub fn eval_packed_generic( let flag = lv[flag_col]; yield_constr.constraint(cycle_filter * flag * (flag - P::ONES)); } - // Manually check for the logic_op flag combining AND, OR and XOR. + // Manually check the logic_op flag combining AND, OR and XOR. // TODO: This would go away once cycle_filter is replaced by the sum // of all CPU opcode flags. let flag = lv.op.logic_op; yield_constr.constraint(cycle_filter * flag * (flag - P::ONES)); // Now check that they sum to 0 or 1. - // Include the logic_op flag encompassing AND, OR and XOR opcodes. + // Includes the logic_op flag encompassing AND, OR and XOR opcodes. // TODO: This would go away once cycle_filter is replaced by the sum // of all CPU opcode flags. let flag_sum: P = OPCODES @@ -220,7 +220,7 @@ pub fn eval_ext_circuit, const D: usize>( let constr = builder.mul_extension(cycle_filter, constr); yield_constr.constraint(builder, constr); } - // Manually check for the logic_op flag combining AND, OR and XOR. + // Manually check the logic_op flag combining AND, OR and XOR. // TODO: This would go away once cycle_filter is replaced by the sum // of all CPU opcode flags. let flag = lv.op.logic_op; @@ -229,7 +229,7 @@ pub fn eval_ext_circuit, const D: usize>( yield_constr.constraint(builder, constr); // Now check that they sum to 0 or 1. - // Include the logic_op flag encompassing AND, OR and XOR opcodes. + // Includes the logic_op flag encompassing AND, OR and XOR opcodes. // TODO: This would go away once cycle_filter is replaced by the sum // of all CPU opcode flags. {