From b711e5279a866ec070c77056a0fc8d2129fd086e Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Fri, 18 Aug 2023 15:36:46 -0400 Subject: [PATCH 1/3] Combine a few constraints --- evm/src/arithmetic/byte.rs | 3 +-- evm/src/cross_table_lookup.rs | 5 ++--- evm/src/memory/memory_stark.rs | 5 +++-- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/evm/src/arithmetic/byte.rs b/evm/src/arithmetic/byte.rs index 743aa1bc..bb8cd121 100644 --- a/evm/src/arithmetic/byte.rs +++ b/evm/src/arithmetic/byte.rs @@ -318,8 +318,7 @@ pub fn eval_ext_circuit, const D: usize>( } let t = F::Extension::from(F::from_canonical_u64(32)); let t = builder.constant_extension(t); - let idx0_hi = builder.mul_extension(idx_decomp[5], t); - let t = builder.add_extension(idx0_lo5, idx0_hi); + let t = builder.mul_add_extension(idx_decomp[5], t, idx0_lo5); let t = builder.sub_extension(idx[0], t); let t = builder.mul_extension(is_byte, t); yield_constr.constraint(builder, t); diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index 61480d05..8f481325 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -399,7 +399,7 @@ pub(crate) fn eval_cross_table_lookup_checks>(); let combined_next = challenges.combine_circuit(builder, &next_columns_eval); let selected_next = select(builder, next_filter, combined_next); - let mut transition = builder.mul_extension(*local_z, selected_next); - transition = builder.sub_extension(*next_z, transition); + let transition = builder.mul_sub_extension(*local_z, selected_next, *next_z); consumer.constraint_transition(builder, transition); } } diff --git a/evm/src/memory/memory_stark.rs b/evm/src/memory/memory_stark.rs index a0481029..36f75665 100644 --- a/evm/src/memory/memory_stark.rs +++ b/evm/src/memory/memory_stark.rs @@ -408,7 +408,6 @@ impl, const D: usize> Stark for MemoryStark, const D: usize> Stark for MemoryStark Date: Fri, 18 Aug 2023 15:46:23 -0400 Subject: [PATCH 2/3] Reduce overconstraining in decode module --- evm/src/cpu/decode.rs | 31 +++++++------------------------ 1 file changed, 7 insertions(+), 24 deletions(-) diff --git a/evm/src/cpu/decode.rs b/evm/src/cpu/decode.rs index a2918d4c..000274e1 100644 --- a/evm/src/cpu/decode.rs +++ b/evm/src/cpu/decode.rs @@ -118,39 +118,33 @@ pub fn eval_packed_generic( lv: &CpuColumnsView

, yield_constr: &mut ConstraintConsumer

, ) { - let cycle_filter: P = COL_MAP.op.iter().map(|&col_i| lv[col_i]).sum(); - // Ensure that the kernel flag is valid (either 0 or 1). let kernel_mode = lv.is_kernel_mode; - yield_constr.constraint(cycle_filter * kernel_mode * (kernel_mode - P::ONES)); + yield_constr.constraint(kernel_mode * (kernel_mode - P::ONES)); // Ensure that the opcode bits are valid: each has to be either 0 or 1. for bit in lv.opcode_bits { - yield_constr.constraint(cycle_filter * bit * (bit - P::ONES)); + yield_constr.constraint(bit * (bit - P::ONES)); } // Check that the instruction flags are valid. // First, check that they are all either 0 or 1. for (_, _, _, flag_col) in OPCODES { let flag = lv[flag_col]; - yield_constr.constraint(cycle_filter * flag * (flag - P::ONES)); + yield_constr.constraint(flag * (flag - P::ONES)); } // 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)); + yield_constr.constraint(flag * (flag - P::ONES)); // Now check that they sum to 0 or 1. // 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 .into_iter() .map(|(_, _, _, flag_col)| lv[flag_col]) .sum::

() + lv.op.logic_op; - yield_constr.constraint(cycle_filter * flag_sum * (flag_sum - P::ONES)); + yield_constr.constraint(flag_sum * (flag_sum - P::ONES)); // Finally, classify all opcodes, together with the kernel flag, into blocks for (oc, block_length, kernel_only, col) in OPCODES { @@ -176,8 +170,7 @@ pub fn eval_packed_generic( // If unavailable + opcode_mismatch is 0, then the opcode bits all match and we are in the // correct mode. - let constr = lv[col] * (unavailable + opcode_mismatch); - yield_constr.constraint(cycle_filter * constr); + yield_constr.constraint(lv[col] * (unavailable + opcode_mismatch)); } } @@ -188,20 +181,18 @@ pub fn eval_ext_circuit, const D: usize>( ) { let one = builder.one_extension(); - let cycle_filter = builder.add_many_extension(COL_MAP.op.iter().map(|&col_i| lv[col_i])); + // Note: The constraints below do not need to be restricted to CPU cycles. // Ensure that the kernel flag is valid (either 0 or 1). let kernel_mode = lv.is_kernel_mode; { let constr = builder.mul_sub_extension(kernel_mode, kernel_mode, kernel_mode); - let constr = builder.mul_extension(cycle_filter, constr); yield_constr.constraint(builder, constr); } // Ensure that the opcode bits are valid: each has to be either 0 or 1. for bit in lv.opcode_bits { let constr = builder.mul_sub_extension(bit, bit, bit); - let constr = builder.mul_extension(cycle_filter, constr); yield_constr.constraint(builder, constr); } @@ -210,21 +201,15 @@ pub fn eval_ext_circuit, const D: usize>( for (_, _, _, flag_col) in OPCODES { let flag = lv[flag_col]; let constr = builder.mul_sub_extension(flag, flag, flag); - let constr = builder.mul_extension(cycle_filter, constr); yield_constr.constraint(builder, constr); } // 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; 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. // 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 mut flag_sum = lv.op.logic_op; for (_, _, _, flag_col) in OPCODES { @@ -232,7 +217,6 @@ pub fn eval_ext_circuit, const D: usize>( flag_sum = builder.add_extension(flag_sum, flag); } let constr = builder.mul_sub_extension(flag_sum, flag_sum, flag_sum); - let constr = builder.mul_extension(cycle_filter, constr); yield_constr.constraint(builder, constr); } @@ -263,7 +247,6 @@ pub fn eval_ext_circuit, const D: usize>( // correct mode. let constr = builder.add_extension(unavailable, opcode_mismatch); let constr = builder.mul_extension(lv[col], constr); - let constr = builder.mul_extension(cycle_filter, constr); yield_constr.constraint(builder, constr); } } From 0b78c43fa3b4d1bb4537385b7b61379ea1187dfb Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Fri, 18 Aug 2023 15:53:13 -0400 Subject: [PATCH 3/3] Remove filtering in membus --- evm/src/cpu/membus.rs | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/evm/src/cpu/membus.rs b/evm/src/cpu/membus.rs index 8a703f0d..3ee75a65 100644 --- a/evm/src/cpu/membus.rs +++ b/evm/src/cpu/membus.rs @@ -49,11 +49,11 @@ pub fn eval_packed( lv: &CpuColumnsView

, yield_constr: &mut ConstraintConsumer

, ) { - let is_cpu_cycle: P = COL_MAP.op.iter().map(|&col_i| lv[col_i]).sum(); - // Validate `lv.code_context`. It should be 0 if in kernel mode and `lv.context` if in user - // mode. - yield_constr - .constraint(is_cpu_cycle * (lv.code_context - (P::ONES - lv.is_kernel_mode) * lv.context)); + // Validate `lv.code_context`. + // It should be 0 if in kernel mode and `lv.context` if in user mode. + // Note: This doesn't need to be filtered to CPU cycles, as this should also be satisfied + // during Kernel bootstrapping. + yield_constr.constraint(lv.code_context - (P::ONES - lv.is_kernel_mode) * lv.context); // Validate `channel.used`. It should be binary. for channel in lv.mem_channels { @@ -66,13 +66,13 @@ pub fn eval_ext_circuit, const D: usize>( lv: &CpuColumnsView>, yield_constr: &mut RecursiveConstraintConsumer, ) { - // Validate `lv.code_context`. It should be 0 if in kernel mode and `lv.context` if in user - // mode. + // Validate `lv.code_context`. + // It should be 0 if in kernel mode and `lv.context` if in user mode. + // Note: This doesn't need to be filtered to CPU cycles, as this should also be satisfied + // during Kernel bootstrapping. let diff = builder.sub_extension(lv.context, lv.code_context); let constr = builder.mul_sub_extension(lv.is_kernel_mode, lv.context, diff); - let is_cpu_cycle = builder.add_many_extension(COL_MAP.op.iter().map(|&col_i| lv[col_i])); - let filtered_constr = builder.mul_extension(is_cpu_cycle, constr); - yield_constr.constraint(builder, filtered_constr); + yield_constr.constraint(builder, constr); // Validate `channel.used`. It should be binary. for channel in lv.mem_channels {