From 1e44ee3681f546c59e698ee1e244ea9631d96560 Mon Sep 17 00:00:00 2001 From: Jacqueline Nabaglo Date: Tue, 14 Jun 2022 17:38:42 -0700 Subject: [PATCH] EQ and ISZERO (#566) --- evm/src/cpu/columns.rs | 15 ++- evm/src/cpu/decode.rs | 13 +++ evm/src/cpu/simple_logic/eq_iszero.rs | 156 ++++++++++++++++++++++++++ evm/src/cpu/simple_logic/mod.rs | 4 + 4 files changed, 183 insertions(+), 5 deletions(-) create mode 100644 evm/src/cpu/simple_logic/eq_iszero.rs diff --git a/evm/src/cpu/columns.rs b/evm/src/cpu/columns.rs index ab97cd4a..6fa15492 100644 --- a/evm/src/cpu/columns.rs +++ b/evm/src/cpu/columns.rs @@ -26,8 +26,8 @@ pub const IS_LT: usize = IS_SIGNEXTEND + 1; pub const IS_GT: usize = IS_LT + 1; pub const IS_SLT: usize = IS_GT + 1; pub const IS_SGT: usize = IS_SLT + 1; -pub const IS_EQ: usize = IS_SGT + 1; -pub const IS_ISZERO: usize = IS_EQ + 1; +pub const IS_EQ: usize = IS_SGT + 1; // Note: This column must be 0 when is_cpu_cycle = 0. +pub const IS_ISZERO: usize = IS_EQ + 1; // Note: This column must be 0 when is_cpu_cycle = 0. pub const IS_AND: usize = IS_ISZERO + 1; pub const IS_OR: usize = IS_AND + 1; pub const IS_XOR: usize = IS_OR + 1; @@ -144,8 +144,13 @@ pub const KECCAK_INPUT_LIMBS: Range = START_KECCAK_INPUT..START_KECCAK_IN pub const START_KECCAK_OUTPUT: usize = KECCAK_INPUT_LIMBS.end; pub const KECCAK_OUTPUT_LIMBS: Range = START_KECCAK_OUTPUT..START_KECCAK_OUTPUT + 50; -// Assuming a limb size of 16 bits. +// Assuming a limb size of 16 bits. This can be changed, but it must be <= 28 bits. +// TODO: These input/output columns can be shared between the simple logic operations and others. pub const SIMPLE_LOGIC_INPUT0: Range = KECCAK_OUTPUT_LIMBS.end..KECCAK_OUTPUT_LIMBS.end + 16; -pub const SIMPLE_LOGIC_OUTPUT: Range = SIMPLE_LOGIC_INPUT0.end..SIMPLE_LOGIC_INPUT0.end + 16; +pub const SIMPLE_LOGIC_INPUT1: Range = SIMPLE_LOGIC_INPUT0.end..SIMPLE_LOGIC_INPUT0.end + 16; +pub const SIMPLE_LOGIC_OUTPUT: Range = SIMPLE_LOGIC_INPUT1.end..SIMPLE_LOGIC_INPUT1.end + 16; -pub const NUM_CPU_COLUMNS: usize = SIMPLE_LOGIC_OUTPUT.end; +pub const SIMPLE_LOGIC_DIFF: usize = SIMPLE_LOGIC_OUTPUT.end; +pub const SIMPLE_LOGIC_DIFF_INV: usize = SIMPLE_LOGIC_DIFF + 1; + +pub const NUM_CPU_COLUMNS: usize = SIMPLE_LOGIC_DIFF_INV + 1; diff --git a/evm/src/cpu/decode.rs b/evm/src/cpu/decode.rs index 523a8350..d9f4c60a 100644 --- a/evm/src/cpu/decode.rs +++ b/evm/src/cpu/decode.rs @@ -124,6 +124,9 @@ const OPCODES: [(u64, usize, usize); 102] = [ pub fn generate(lv: &mut [F; columns::NUM_CPU_COLUMNS]) { let cycle_filter = lv[columns::IS_CPU_CYCLE]; if cycle_filter == F::ZERO { + // These columns cannot be shared. + lv[columns::IS_EQ] = F::ZERO; + lv[columns::IS_ISZERO] = F::ZERO; return; } // This assert is not _strictly_ necessary, but I include it as a sanity check. @@ -160,6 +163,10 @@ pub fn eval_packed_generic( ) { let cycle_filter = lv[columns::IS_CPU_CYCLE]; + // If cycle_filter = 0, then we require is_eq = 0 and is_iszero = 0. + yield_constr.constraint((cycle_filter - P::ONES) * lv[columns::IS_EQ]); + yield_constr.constraint((cycle_filter - P::ONES) * lv[columns::IS_ISZERO]); + // Ensure that the opcode bits are valid: each has to be either 0 or 1, and they must match // the opcode. Note that this also validates that this implicitly range-checks the opcode. let bits = columns::OPCODE_BITS.map(|i| lv[i]); @@ -207,6 +214,12 @@ pub fn eval_ext_circuit, const D: usize>( ) { let cycle_filter = lv[columns::IS_CPU_CYCLE]; + // If cycle_filter = 0, then we require is_eq = 0 and is_iszero = 0. + for flag in [lv[columns::IS_EQ], lv[columns::IS_ISZERO]] { + let constr = builder.mul_sub_extension(cycle_filter, flag, flag); + yield_constr.constraint(builder, constr); + } + // Ensure that the opcode bits are valid: each has to be either 0 or 1, and they must match // the opcode. Note that this also validates that this implicitly range-checks the opcode. let bits = columns::OPCODE_BITS.map(|i| lv[i]); diff --git a/evm/src/cpu/simple_logic/eq_iszero.rs b/evm/src/cpu/simple_logic/eq_iszero.rs new file mode 100644 index 00000000..cd806eae --- /dev/null +++ b/evm/src/cpu/simple_logic/eq_iszero.rs @@ -0,0 +1,156 @@ +use plonky2::field::extension_field::Extendable; +use plonky2::field::packed_field::PackedField; +use plonky2::hash::hash_types::RichField; +use plonky2::iop::ext_target::ExtensionTarget; + +use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; +use crate::cpu::columns; + +const LIMB_SIZE: usize = 16; + +pub fn generate(lv: &mut [F; columns::NUM_CPU_COLUMNS]) { + let eq_filter = lv[columns::IS_EQ].to_canonical_u64(); + let iszero_filter = lv[columns::IS_ISZERO].to_canonical_u64(); + assert!(eq_filter <= 1); + assert!(iszero_filter <= 1); + assert!(eq_filter + iszero_filter <= 1); + + if eq_filter != 1 && iszero_filter != 1 { + return; + } + + let diffs = if eq_filter == 1 { + columns::SIMPLE_LOGIC_INPUT0 + .zip(columns::SIMPLE_LOGIC_INPUT1) + .map(|(in0_col, in1_col)| { + let in0 = lv[in0_col]; + let in1 = lv[in1_col]; + assert_eq!(in0.to_canonical_u64() >> LIMB_SIZE, 0); + assert_eq!(in1.to_canonical_u64() >> LIMB_SIZE, 0); + let diff = in0 - in1; + diff.square() + }) + .sum() + } else if iszero_filter == 1 { + columns::SIMPLE_LOGIC_INPUT0.map(|i| lv[i]).sum() + } else { + panic!() + }; + + lv[columns::SIMPLE_LOGIC_DIFF] = diffs; + lv[columns::SIMPLE_LOGIC_DIFF_INV] = diffs.try_inverse().unwrap_or(F::ZERO); + + lv[columns::SIMPLE_LOGIC_OUTPUT.start] = F::from_bool(diffs == F::ZERO); + for i in columns::SIMPLE_LOGIC_OUTPUT.start + 1..columns::SIMPLE_LOGIC_OUTPUT.end { + lv[i] = F::ZERO; + } +} + +pub fn eval_packed( + lv: &[P; columns::NUM_CPU_COLUMNS], + yield_constr: &mut ConstraintConsumer

, +) { + let eq_filter = lv[columns::IS_EQ]; + let iszero_filter = lv[columns::IS_ISZERO]; + let eq_or_iszero_filter = eq_filter + iszero_filter; + + let ls_bit = lv[columns::SIMPLE_LOGIC_OUTPUT.start]; + + // Handle EQ and ISZERO. Most limbs of the output are 0, but the least-significant one is + // either 0 or 1. + yield_constr.constraint(eq_or_iszero_filter * ls_bit * (ls_bit - P::ONES)); + + for bit_col in columns::SIMPLE_LOGIC_OUTPUT.start + 1..columns::SIMPLE_LOGIC_OUTPUT.end { + let bit = lv[bit_col]; + yield_constr.constraint(eq_or_iszero_filter * bit); + } + + // Check SIMPLE_LOGIC_DIFF + let diffs = lv[columns::SIMPLE_LOGIC_DIFF]; + let diffs_inv = lv[columns::SIMPLE_LOGIC_DIFF_INV]; + { + let input0_sum: P = columns::SIMPLE_LOGIC_INPUT0.map(|i| lv[i]).sum(); + yield_constr.constraint(iszero_filter * (diffs - input0_sum)); + + let sum_squared_diffs: P = columns::SIMPLE_LOGIC_INPUT0 + .zip(columns::SIMPLE_LOGIC_INPUT1) + .map(|(in0_col, in1_col)| { + let in0 = lv[in0_col]; + let in1 = lv[in1_col]; + let diff = in0 - in1; + diff.square() + }) + .sum(); + yield_constr.constraint(eq_filter * (diffs - sum_squared_diffs)); + } + + // diffs != 0 => ls_bit == 0 + yield_constr.constraint(eq_or_iszero_filter * diffs * ls_bit); + // ls_bit == 0 => diffs != 0 (we provide a diffs_inv) + yield_constr.constraint(eq_or_iszero_filter * (diffs * diffs_inv + ls_bit - P::ONES)); +} + +pub fn eval_ext_circuit, const D: usize>( + builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder, + lv: &[ExtensionTarget; columns::NUM_CPU_COLUMNS], + yield_constr: &mut RecursiveConstraintConsumer, +) { + let eq_filter = lv[columns::IS_EQ]; + let iszero_filter = lv[columns::IS_ISZERO]; + let eq_or_iszero_filter = builder.add_extension(eq_filter, iszero_filter); + + let ls_bit = lv[columns::SIMPLE_LOGIC_OUTPUT.start]; + + // Handle EQ and ISZERO. Most limbs of the output are 0, but the least-significant one is + // either 0 or 1. + { + let constr = builder.mul_sub_extension(ls_bit, ls_bit, ls_bit); + let constr = builder.mul_extension(eq_or_iszero_filter, constr); + yield_constr.constraint(builder, constr); + } + + for bit_col in columns::SIMPLE_LOGIC_OUTPUT.start + 1..columns::SIMPLE_LOGIC_OUTPUT.end { + let bit = lv[bit_col]; + let constr = builder.mul_extension(eq_or_iszero_filter, bit); + yield_constr.constraint(builder, constr); + } + + // Check SIMPLE_LOGIC_DIFF + let diffs = lv[columns::SIMPLE_LOGIC_DIFF]; + let diffs_inv = lv[columns::SIMPLE_LOGIC_DIFF_INV]; + { + let input0_sum = builder.add_many_extension(columns::SIMPLE_LOGIC_INPUT0.map(|i| lv[i])); + { + let constr = builder.sub_extension(diffs, input0_sum); + let constr = builder.mul_extension(iszero_filter, constr); + yield_constr.constraint(builder, constr); + } + + let sum_squared_diffs = columns::SIMPLE_LOGIC_INPUT0 + .zip(columns::SIMPLE_LOGIC_INPUT1) + .fold(builder.zero_extension(), |acc, (in0_col, in1_col)| { + let in0 = lv[in0_col]; + let in1 = lv[in1_col]; + let diff = builder.sub_extension(in0, in1); + builder.mul_add_extension(diff, diff, acc) + }); + { + let constr = builder.sub_extension(diffs, sum_squared_diffs); + let constr = builder.mul_extension(eq_filter, constr); + yield_constr.constraint(builder, constr); + } + } + + { + // diffs != 0 => ls_bit == 0 + let constr = builder.mul_extension(diffs, ls_bit); + let constr = builder.mul_extension(eq_or_iszero_filter, constr); + yield_constr.constraint(builder, constr); + } + { + // ls_bit == 0 => diffs != 0 (we provide a diffs_inv) + let constr = builder.mul_add_extension(diffs, diffs_inv, ls_bit); + let constr = builder.mul_sub_extension(eq_or_iszero_filter, constr, eq_or_iszero_filter); + yield_constr.constraint(builder, constr); + } +} diff --git a/evm/src/cpu/simple_logic/mod.rs b/evm/src/cpu/simple_logic/mod.rs index bc4283f1..ee9491dc 100644 --- a/evm/src/cpu/simple_logic/mod.rs +++ b/evm/src/cpu/simple_logic/mod.rs @@ -1,3 +1,4 @@ +mod eq_iszero; mod not; use plonky2::field::extension_field::Extendable; @@ -16,6 +17,7 @@ pub fn generate(lv: &mut [F; columns::NUM_CPU_COLUMNS]) { assert_eq!(cycle_filter, 1); not::generate(lv); + eq_iszero::generate(lv); } pub fn eval_packed( @@ -23,6 +25,7 @@ pub fn eval_packed( yield_constr: &mut ConstraintConsumer

, ) { not::eval_packed(lv, yield_constr); + eq_iszero::eval_packed(lv, yield_constr); } pub fn eval_ext_circuit, const D: usize>( @@ -31,4 +34,5 @@ pub fn eval_ext_circuit, const D: usize>( yield_constr: &mut RecursiveConstraintConsumer, ) { not::eval_ext_circuit(builder, lv, yield_constr); + eq_iszero::eval_ext_circuit(builder, lv, yield_constr); }