Skip to content
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.

Commit

Permalink
Add debug expr in EVMConstraintBuilder (#1500)
Browse files Browse the repository at this point in the history 
### Description

Introduce the `debug_expression` method to the `EVMConstraintBuilder`
which allows specifying an expression inside an ExecutionGadget to be
evaluated and printed during assignment.

This can be very useful for debugging. With this we can print the value
of cells, but also of arbitrary expressions. For example, it allows
printing the evaluation of all the expressions used in a lookup
(previous to the RLC).

### Type of change

- [ ] Bug fix (non-breaking change which fixes an issue)
- [x] New feature (non-breaking change which adds functionality)
- [ ] Breaking change (fix or feature that would cause existing
functionality to not work as expected)
- [ ] This change requires a documentation update

### Contents

When calling `cb.debug_expression`, the expression is stored in the
`EVMConstraintBuilder` along with a string. Later on, at assignment,
whenever a step is assigned to an `ExecutionState` that had some debug
expressions specified, those expressions will be evaluated and printed.

#### Example usage

In the `PushGadget::configure` method I include the following line:
```rust
cb.debug_expression("push.code_hash", code_hash.expr());
```
Then I run the a test that assigns this state (with `--nocapture` to see
the stdout):
```
cargo test push_gadget_simple --release --all-features -- --nocapture
```
And I will get the following:
```
Debug expression "push.code_hash"=0x178027364c9ed08d00e38dbf197bbf65e45779c1d1b9dca1a229f7b7360892ce [offset=19, step=Op(PUSH1), expr=Advice { query_index: 591, column_index: 76, rotation: Rotation(0), phase: Phase(1) }]
```

---------

Co-authored-by: Chih Cheng Liang <[email protected]>
  • Loading branch information
@ed255 @ChihChengLiang
ed255 and ChihChengLiang authored Jul 7, 2023
1 parent 3c8ce57 commit 6bcb1d0
Show file tree
Hide file tree
Showing 4 changed files with 138 additions and 39 deletions.
111 changes: 96 additions & 15 deletions zkevm-circuits/src/evm_circuit/execution.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ use crate::{
constraint_builder::{
BaseConstraintBuilder, ConstrainBuilderCommon, EVMConstraintBuilder,
},
rlc,
evaluate_expression, rlc,
},
witness::{Block, Call, ExecStep, Transaction},
},
Expand Down Expand Up @@ -225,6 +225,7 @@ pub struct ExecutionConfig<F> {
step: Step<F>,
pub(crate) height_map: HashMap<ExecutionState, usize>,
stored_expressions_map: HashMap<ExecutionState, Vec<StoredExpression<F>>>,
debug_expressions_map: HashMap<ExecutionState, Vec<(String, Expression<F>)>>,
instrument: Instrument,
// internal state gadgets
begin_tx_gadget: Box<BeginTxGadget<F>>,
Expand Down Expand Up @@ -453,6 +454,7 @@ impl<F: Field> ExecutionConfig<F> {
});

let mut stored_expressions_map = HashMap::new();
let mut debug_expressions_map = HashMap::new();

macro_rules! configure_gadget {
() => {
Expand All @@ -474,6 +476,7 @@ impl<F: Field> ExecutionConfig<F> {
&step_curr,
&mut height_map,
&mut stored_expressions_map,
&mut debug_expressions_map,
&mut instrument,
))
})()
Expand Down Expand Up @@ -579,6 +582,7 @@ impl<F: Field> ExecutionConfig<F> {
step: step_curr,
height_map,
stored_expressions_map,
debug_expressions_map,
instrument,
};

Expand Down Expand Up @@ -617,6 +621,7 @@ impl<F: Field> ExecutionConfig<F> {
step_curr: &Step<F>,
height_map: &mut HashMap<ExecutionState, usize>,
stored_expressions_map: &mut HashMap<ExecutionState, Vec<StoredExpression<F>>>,
debug_expressions_map: &mut HashMap<ExecutionState, Vec<(String, Expression<F>)>>,
instrument: &mut Instrument,
) -> G {
// Configure the gadget with the max height first so we can find out the actual
Expand Down Expand Up @@ -657,6 +662,7 @@ impl<F: Field> ExecutionConfig<F> {
step_next,
height_map,
stored_expressions_map,
debug_expressions_map,
instrument,
G::NAME,
G::EXECUTION_STATE,
Expand All @@ -678,6 +684,7 @@ impl<F: Field> ExecutionConfig<F> {
step_next: &Step<F>,
height_map: &mut HashMap<ExecutionState, usize>,
stored_expressions_map: &mut HashMap<ExecutionState, Vec<StoredExpression<F>>>,
debug_expressions_map: &mut HashMap<ExecutionState, Vec<(String, Expression<F>)>>,
instrument: &mut Instrument,
name: &'static str,
execution_state: ExecutionState,
Expand All @@ -695,6 +702,7 @@ impl<F: Field> ExecutionConfig<F> {

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),
Expand All @@ -707,6 +715,7 @@ impl<F: Field> ExecutionConfig<F> {
"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<F>) -> Expression<F> =
Expand Down Expand Up @@ -887,6 +896,8 @@ impl<F: Field> ExecutionConfig<F> {
block: &Block<F>,
challenges: &Challenges<Value<F>>,
) -> 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| {
Expand Down Expand Up @@ -940,6 +951,7 @@ impl<F: Field> ExecutionConfig<F> {
height,
next.copied(),
challenges,
assign_pass,
)?;

// q_step logic
Expand Down Expand Up @@ -976,6 +988,7 @@ impl<F: Field> ExecutionConfig<F> {
end_block_not_last,
height,
challenges,
assign_pass,
)?;

for row_idx in offset..last_row {
Expand All @@ -998,6 +1011,7 @@ impl<F: Field> ExecutionConfig<F> {
height,
None,
challenges,
assign_pass,
)?;
self.assign_q_step(&mut region, offset, height)?;
// enable q_step_last
Expand All @@ -1019,6 +1033,7 @@ impl<F: Field> ExecutionConfig<F> {
|| Value::known(F::ZERO),
)?;

assign_pass += 1;
Ok(())
},
)
Expand Down Expand Up @@ -1070,6 +1085,7 @@ impl<F: Field> ExecutionConfig<F> {
step: &ExecStep,
height: usize,
challenges: &Challenges<Value<F>>,
assign_pass: usize,
) -> Result<(), Error> {
if offset_end <= offset_begin {
return Ok(());
Expand All @@ -1086,7 +1102,16 @@ impl<F: Field> ExecutionConfig<F> {
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()),
Expand All @@ -1109,6 +1134,7 @@ impl<F: Field> ExecutionConfig<F> {
height: usize,
next: Option<(&Transaction, &Call, &ExecStep)>,
challenges: &Challenges<Value<F>>,
assign_pass: usize,
) -> Result<(), Error> {
if !matches!(step.execution_state(), ExecutionState::EndBlock) {
log::trace!(
Expand Down Expand Up @@ -1142,12 +1168,24 @@ impl<F: Field> ExecutionConfig<F> {
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>,
Expand All @@ -1156,6 +1194,12 @@ impl<F: Field> ExecutionConfig<F> {
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)?;
Expand Down Expand Up @@ -1299,19 +1343,32 @@ impl<F: Field> ExecutionConfig<F> {

// 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(())
Expand All @@ -1338,6 +1395,30 @@ impl<F: Field> ExecutionConfig<F> {
Ok(assigned_stored_expressions)
}

fn print_debug_expressions(
&self,
region: &mut CachedRegion<'_, '_, F>,
offset: usize,
step: &ExecStep,
) {
for (name, expression) 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,
Expand Down
3 changes: 3 additions & 0 deletions zkevm-circuits/src/evm_circuit/execution/begin_tx.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,8 @@ impl<F: Field> ExecutionGadget<F> for BeginTxGadget<F> {
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,
Expand All @@ -89,6 +91,7 @@ impl<F: Field> ExecutionGadget<F> for BeginTxGadget<F> {
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,
Expand Down
57 changes: 33 additions & 24 deletions zkevm-circuits/src/evm_circuit/util.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -180,36 +180,45 @@ impl<F> Hash for StoredExpression<F> {
}
}

/// Evaluate an expression using a `CachedRegion` at `offset`.
pub(crate) fn evaluate_expression<F: Field>(
expr: &Expression<F>,
region: &CachedRegion<'_, '_, F>,
offset: usize,
) -> Value<F> {
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<F: Field> StoredExpression<F> {
pub fn assign(
&self,
region: &mut CachedRegion<'_, '_, F>,
offset: usize,
) -> Result<Value<F>, 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)
}
Expand Down
6 changes: 6 additions & 0 deletions zkevm-circuits/src/evm_circuit/util/constraint_builder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -307,6 +307,7 @@ pub(crate) struct EVMConstraintBuilder<'a, F: Field> {
conditions: Vec<Expression<F>>,
constraints_location: ConstraintLocation,
stored_expressions: Vec<StoredExpression<F>>,
pub(crate) debug_expressions: Vec<(String, Expression<F>)>,

meta: &'a mut ConstraintSystem<F>,
}
Expand Down Expand Up @@ -353,6 +354,7 @@ impl<'a, F: Field> EVMConstraintBuilder<'a, F> {
constraints_location: ConstraintLocation::Step,
stored_expressions: Vec::new(),
meta,
debug_expressions: Vec::new(),
}
}

Expand Down Expand Up @@ -1671,4 +1673,8 @@ impl<'a, F: Field> EVMConstraintBuilder<'a, F> {
None => 1.expr(),
}
}

pub fn debug_expression<S: Into<String>>(&mut self, name: S, expr: Expression<F>) {
self.debug_expressions.push((name.into(), expr));
}
}

0 comments on commit 6bcb1d0

Please sign in to comment.