From ae37c3831123f39016778596ac1a1a8a440575c7 Mon Sep 17 00:00:00 2001 From: Eduard S Date: Thu, 22 Jun 2023 14:30:18 +0200 Subject: [PATCH 1/2] Add debug expr in EVMConstraintBuilder Introduce the `debug_expression` method to the `EVMConstraintBuilder` which allows specifying an expression inside an ExecutionGadget to be evaluated and printed during assignment. --- zkevm-circuits/src/evm_circuit/execution.rs | 111 +++++++++++++++--- zkevm-circuits/src/evm_circuit/util.rs | 57 +++++---- .../evm_circuit/util/constraint_builder.rs | 6 + 3 files changed, 135 insertions(+), 39 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution.rs b/zkevm-circuits/src/evm_circuit/execution.rs index 8def043c10..507439115a 100644 --- a/zkevm-circuits/src/evm_circuit/execution.rs +++ b/zkevm-circuits/src/evm_circuit/execution.rs @@ -16,7 +16,7 @@ use crate::{ constraint_builder::{ BaseConstraintBuilder, ConstrainBuilderCommon, EVMConstraintBuilder, }, - rlc, + evaluate_expression, rlc, }, witness::{Block, Call, ExecStep, Transaction}, }, @@ -224,6 +224,7 @@ pub struct ExecutionConfig { step: Step, pub(crate) height_map: HashMap, stored_expressions_map: HashMap>>, + debug_expressions_map: HashMap, String)>>, instrument: Instrument, // internal state gadgets begin_tx_gadget: Box>, @@ -454,6 +455,7 @@ impl ExecutionConfig { }); let mut stored_expressions_map = HashMap::new(); + let mut debug_expressions_map = HashMap::new(); macro_rules! configure_gadget { () => { @@ -475,6 +477,7 @@ impl ExecutionConfig { &step_curr, &mut height_map, &mut stored_expressions_map, + &mut debug_expressions_map, &mut instrument, )) })() @@ -582,6 +585,7 @@ impl ExecutionConfig { step: step_curr, height_map, stored_expressions_map, + debug_expressions_map, instrument, }; @@ -619,6 +623,7 @@ impl ExecutionConfig { step_curr: &Step, height_map: &mut HashMap, stored_expressions_map: &mut HashMap>>, + debug_expressions_map: &mut HashMap, String)>>, instrument: &mut Instrument, ) -> G { // Configure the gadget with the max height first so we can find out the actual @@ -659,6 +664,7 @@ impl ExecutionConfig { step_next, height_map, stored_expressions_map, + debug_expressions_map, instrument, G::NAME, G::EXECUTION_STATE, @@ -680,6 +686,7 @@ impl ExecutionConfig { step_next: &Step, height_map: &mut HashMap, stored_expressions_map: &mut HashMap>>, + debug_expressions_map: &mut HashMap, String)>>, instrument: &mut Instrument, name: &'static str, execution_state: ExecutionState, @@ -697,6 +704,7 @@ impl ExecutionConfig { instrument.on_gadget_built(execution_state, &cb); + let debug_expressions = cb.debug_expressions.clone(); let (constraints, stored_expressions, _, meta) = cb.build(); debug_assert!( !height_map.contains_key(&execution_state), @@ -709,6 +717,7 @@ impl ExecutionConfig { "execution state already configured" ); stored_expressions_map.insert(execution_state, stored_expressions); + debug_expressions_map.insert(execution_state, debug_expressions); // Enforce the logic for this opcode let sel_step: &dyn Fn(&mut VirtualCells) -> Expression = @@ -895,6 +904,8 @@ impl ExecutionConfig { block: &Block, challenges: &Challenges>, ) -> Result<(), Error> { + // Track number of calls to `layouter.assign_region` as layouter assignment passes. + let mut assign_pass = 0; layouter.assign_region( || "Execution step", |mut region| { @@ -948,6 +959,7 @@ impl ExecutionConfig { height, next.copied(), challenges, + assign_pass, )?; // q_step logic @@ -984,6 +996,7 @@ impl ExecutionConfig { end_block_not_last, height, challenges, + assign_pass, )?; for row_idx in offset..last_row { @@ -1006,6 +1019,7 @@ impl ExecutionConfig { height, None, challenges, + assign_pass, )?; self.assign_q_step(&mut region, offset, height)?; // enable q_step_last @@ -1027,6 +1041,7 @@ impl ExecutionConfig { || Value::known(F::ZERO), )?; + assign_pass += 1; Ok(()) }, ) @@ -1077,6 +1092,7 @@ impl ExecutionConfig { step: &ExecStep, height: usize, challenges: &Challenges>, + assign_pass: usize, ) -> Result<(), Error> { if offset_end <= offset_begin { return Ok(()); @@ -1093,7 +1109,16 @@ impl ExecutionConfig { 1, offset_begin, ); - self.assign_exec_step_int(region, offset_begin, block, transaction, call, step)?; + self.assign_exec_step_int( + region, + offset_begin, + block, + transaction, + call, + step, + false, + assign_pass, + )?; region.replicate_assignment_for_range( || format!("repeat {:?} rows", step.execution_state()), @@ -1116,6 +1141,7 @@ impl ExecutionConfig { height: usize, next: Option<(&Transaction, &Call, &ExecStep)>, challenges: &Challenges>, + assign_pass: usize, ) -> Result<(), Error> { if !matches!(step.execution_state(), ExecutionState::EndBlock) { log::trace!( @@ -1149,12 +1175,24 @@ impl ExecutionConfig { transaction_next, call_next, step_next, + true, + assign_pass, )?; } - self.assign_exec_step_int(region, offset, block, transaction, call, step) + self.assign_exec_step_int( + region, + offset, + block, + transaction, + call, + step, + false, + assign_pass, + ) } + #[allow(clippy::too_many_arguments)] fn assign_exec_step_int( &self, region: &mut CachedRegion<'_, '_, F>, @@ -1163,6 +1201,12 @@ impl ExecutionConfig { transaction: &Transaction, call: &Call, step: &ExecStep, + // Set to true when we're assigning the next step before the current step to have + // next step assignments for evaluation of the stored expressions in current step that + // depend on the next step. + is_next: bool, + // Layouter assignment pass + assign_pass: usize, ) -> Result<(), Error> { self.step .assign_exec_step(region, offset, block, call, step)?; @@ -1308,19 +1352,32 @@ impl ExecutionConfig { // Fill in the witness values for stored expressions let assigned_stored_expressions = self.assign_stored_expressions(region, offset, step)?; + // Both `SimpleFloorPlanner` and `V1` do two passes; we only enter here once (on the second + // pass). + if !is_next && assign_pass == 1 { + // We only want to print at the latest possible Phase. Currently halo2 implements 3 + // phases. The `lookup_input` randomness is calculated after SecondPhase, so we print + // the debug expressions only once when we're at third phase, when `lookup_input` has + // a `Value::known`. This gets called for every `synthesize` call that the Layouter + // does. + region.challenges().lookup_input().assert_if_known(|_| { + self.print_debug_expressions(region, offset, step); + true + }); - // enable with `RUST_LOG=debug` - if log::log_enabled!(log::Level::Debug) { - let is_padding_step = matches!(step.execution_state(), ExecutionState::EndBlock) - && step.rw_indices_len() == 0; - if !is_padding_step { - // expensive function call - Self::check_rw_lookup( - &assigned_stored_expressions, - step, - block, - region.challenges(), - ); + // enable with `RUST_LOG=debug` + if log::log_enabled!(log::Level::Debug) { + let is_padding_step = matches!(step.execution_state(), ExecutionState::EndBlock) + && step.rw_indices_len() == 0; + if !is_padding_step { + // expensive function call + Self::check_rw_lookup( + &assigned_stored_expressions, + step, + block, + region.challenges(), + ); + } } } Ok(()) @@ -1347,6 +1404,30 @@ impl ExecutionConfig { Ok(assigned_stored_expressions) } + fn print_debug_expressions( + &self, + region: &mut CachedRegion<'_, '_, F>, + offset: usize, + step: &ExecStep, + ) { + for (expression, name) in self + .debug_expressions_map + .get(&step.execution_state()) + .unwrap_or_else(|| panic!("Execution state unknown: {:?}", step.execution_state())) + { + let value = evaluate_expression(expression, region, offset); + let mut value_string = "unknown".to_string(); + value.assert_if_known(|f| { + value_string = format!("{:?}", f); + true + }); + println!( + "Debug expression \"{}\"={} [offset={}, step={:?}, expr={:?}]", + name, value_string, offset, step.exec_state, expression + ); + } + } + fn check_rw_lookup( assigned_stored_expressions: &[(String, F)], step: &ExecStep, diff --git a/zkevm-circuits/src/evm_circuit/util.rs b/zkevm-circuits/src/evm_circuit/util.rs index d9eaef44ce..aae1006a42 100644 --- a/zkevm-circuits/src/evm_circuit/util.rs +++ b/zkevm-circuits/src/evm_circuit/util.rs @@ -183,36 +183,45 @@ impl Hash for StoredExpression { } } +/// Evaluate an expression using a `CachedRegion` at `offset`. +pub(crate) fn evaluate_expression( + expr: &Expression, + region: &CachedRegion<'_, '_, F>, + offset: usize, +) -> Value { + expr.evaluate( + &|scalar| Value::known(scalar), + &|_| unimplemented!("selector column"), + &|fixed_query| { + Value::known(region.get_fixed( + offset, + fixed_query.column_index(), + fixed_query.rotation(), + )) + }, + &|advice_query| { + Value::known(region.get_advice( + offset, + advice_query.column_index(), + advice_query.rotation(), + )) + }, + &|_| unimplemented!("instance column"), + &|challenge| *region.challenges().indexed()[challenge.index()], + &|a| -a, + &|a, b| a + b, + &|a, b| a * b, + &|a, scalar| a * Value::known(scalar), + ) +} + impl StoredExpression { pub fn assign( &self, region: &mut CachedRegion<'_, '_, F>, offset: usize, ) -> Result, Error> { - let value = self.expr.evaluate( - &|scalar| Value::known(scalar), - &|_| unimplemented!("selector column"), - &|fixed_query| { - Value::known(region.get_fixed( - offset, - fixed_query.column_index(), - fixed_query.rotation(), - )) - }, - &|advice_query| { - Value::known(region.get_advice( - offset, - advice_query.column_index(), - advice_query.rotation(), - )) - }, - &|_| unimplemented!("instance column"), - &|challenge| *region.challenges().indexed()[challenge.index()], - &|a| -a, - &|a, b| a + b, - &|a, b| a * b, - &|a, scalar| a * Value::known(scalar), - ); + let value = evaluate_expression(&self.expr, region, offset); self.cell.assign(region, offset, value)?; Ok(value) } diff --git a/zkevm-circuits/src/evm_circuit/util/constraint_builder.rs b/zkevm-circuits/src/evm_circuit/util/constraint_builder.rs index c90a02c0ed..3f95c5014b 100644 --- a/zkevm-circuits/src/evm_circuit/util/constraint_builder.rs +++ b/zkevm-circuits/src/evm_circuit/util/constraint_builder.rs @@ -284,6 +284,7 @@ pub(crate) struct EVMConstraintBuilder<'a, F: Field> { conditions: Vec>, constraints_location: ConstraintLocation, stored_expressions: Vec>, + pub(crate) debug_expressions: Vec<(Expression, String)>, meta: &'a mut ConstraintSystem, } @@ -330,6 +331,7 @@ impl<'a, F: Field> EVMConstraintBuilder<'a, F> { constraints_location: ConstraintLocation::Step, stored_expressions: Vec::new(), meta, + debug_expressions: Vec::new(), } } @@ -1545,4 +1547,8 @@ impl<'a, F: Field> EVMConstraintBuilder<'a, F> { None => 1.expr(), } } + + pub fn debug_expression(&mut self, expr: Expression, name: String) { + self.debug_expressions.push((expr, name)); + } } From 0c62d2c83239a7e7fa7ec3ce5c4f0b480606259e Mon Sep 17 00:00:00 2001 From: Eduard S Date: Fri, 7 Jul 2023 10:31:08 +0200 Subject: [PATCH 2/2] Update from @hero78119 feedback --- zkevm-circuits/src/evm_circuit/execution.rs | 8 ++++---- zkevm-circuits/src/evm_circuit/execution/begin_tx.rs | 3 +++ zkevm-circuits/src/evm_circuit/util/constraint_builder.rs | 6 +++--- 3 files changed, 10 insertions(+), 7 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution.rs b/zkevm-circuits/src/evm_circuit/execution.rs index 8fb66473f2..bf6892cfdf 100644 --- a/zkevm-circuits/src/evm_circuit/execution.rs +++ b/zkevm-circuits/src/evm_circuit/execution.rs @@ -225,7 +225,7 @@ pub struct ExecutionConfig { step: Step, pub(crate) height_map: HashMap, stored_expressions_map: HashMap>>, - debug_expressions_map: HashMap, String)>>, + debug_expressions_map: HashMap)>>, instrument: Instrument, // internal state gadgets begin_tx_gadget: Box>, @@ -621,7 +621,7 @@ impl ExecutionConfig { step_curr: &Step, height_map: &mut HashMap, stored_expressions_map: &mut HashMap>>, - debug_expressions_map: &mut HashMap, String)>>, + debug_expressions_map: &mut HashMap)>>, instrument: &mut Instrument, ) -> G { // Configure the gadget with the max height first so we can find out the actual @@ -684,7 +684,7 @@ impl ExecutionConfig { step_next: &Step, height_map: &mut HashMap, stored_expressions_map: &mut HashMap>>, - debug_expressions_map: &mut HashMap, String)>>, + debug_expressions_map: &mut HashMap)>>, instrument: &mut Instrument, name: &'static str, execution_state: ExecutionState, @@ -1401,7 +1401,7 @@ impl ExecutionConfig { offset: usize, step: &ExecStep, ) { - for (expression, name) in self + for (name, expression) in self .debug_expressions_map .get(&step.execution_state()) .unwrap_or_else(|| panic!("Execution state unknown: {:?}", step.execution_state())) diff --git a/zkevm-circuits/src/evm_circuit/execution/begin_tx.rs b/zkevm-circuits/src/evm_circuit/execution/begin_tx.rs index 9e337cf164..66172a4789 100644 --- a/zkevm-circuits/src/evm_circuit/execution/begin_tx.rs +++ b/zkevm-circuits/src/evm_circuit/execution/begin_tx.rs @@ -78,6 +78,8 @@ impl ExecutionGadget for BeginTxGadget { let call_id = cb.curr.state.rw_counter.clone(); let tx_id = cb.query_cell(); // already constrain `if step_first && tx_id = 1` and `tx_id += 1` at EndTx + + cb.debug_expression("tx_id", tx_id.expr()); cb.call_context_lookup_write( Some(call_id.expr()), CallContextFieldTag::TxId, @@ -89,6 +91,7 @@ impl ExecutionGadget for BeginTxGadget { CallContextFieldTag::IsSuccess, Word::from_lo_unchecked(reversion_info.is_persistent()), ); // rwc_delta += 1 + cb.debug_expression(format!("call_id {}", 3), call_id.expr()); let [tx_nonce, tx_gas, tx_is_create, tx_call_data_length, tx_call_data_gas_cost] = [ TxContextFieldTag::Nonce, diff --git a/zkevm-circuits/src/evm_circuit/util/constraint_builder.rs b/zkevm-circuits/src/evm_circuit/util/constraint_builder.rs index 5b2cd2d7c4..c5d1457cbf 100644 --- a/zkevm-circuits/src/evm_circuit/util/constraint_builder.rs +++ b/zkevm-circuits/src/evm_circuit/util/constraint_builder.rs @@ -307,7 +307,7 @@ pub(crate) struct EVMConstraintBuilder<'a, F: Field> { conditions: Vec>, constraints_location: ConstraintLocation, stored_expressions: Vec>, - pub(crate) debug_expressions: Vec<(Expression, String)>, + pub(crate) debug_expressions: Vec<(String, Expression)>, meta: &'a mut ConstraintSystem, } @@ -1678,7 +1678,7 @@ impl<'a, F: Field> EVMConstraintBuilder<'a, F> { } } - pub fn debug_expression(&mut self, expr: Expression, name: String) { - self.debug_expressions.push((expr, name)); + pub fn debug_expression>(&mut self, name: S, expr: Expression) { + self.debug_expressions.push((name.into(), expr)); } }