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
Browse files Browse the repository at this point in the history 
Introduce the `debug_expression` method to the `EVMConstraintBuilder` which allows specifying an expression inside an ExecutionGadget to be evaluated and printed during assignment.
  • Loading branch information
@ed255
ed255 committed Jun 29, 2023
1 parent 3575aab commit ae37c38
Show file tree
Hide file tree
Showing 3 changed files with 135 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 @@ -224,6 +224,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<(Expression<F>, String)>>,
instrument: Instrument,
// internal state gadgets
begin_tx_gadget: Box<BeginTxGadget<F>>,
Expand Down Expand Up @@ -454,6 +455,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 @@ -475,6 +477,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 @@ -582,6 +585,7 @@ impl<F: Field> ExecutionConfig<F> {
step: step_curr,
height_map,
stored_expressions_map,
debug_expressions_map,
instrument,
};

Expand Down Expand Up @@ -619,6 +623,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<(Expression<F>, String)>>,
instrument: &mut Instrument,
) -> G {
// Configure the gadget with the max height first so we can find out the actual
Expand Down Expand Up @@ -659,6 +664,7 @@ impl<F: Field> ExecutionConfig<F> {
step_next,
height_map,
stored_expressions_map,
debug_expressions_map,
instrument,
G::NAME,
G::EXECUTION_STATE,
Expand All @@ -680,6 +686,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<(Expression<F>, String)>>,
instrument: &mut Instrument,
name: &'static str,
execution_state: ExecutionState,
Expand All @@ -697,6 +704,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 @@ -709,6 +717,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 @@ -895,6 +904,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 @@ -948,6 +959,7 @@ impl<F: Field> ExecutionConfig<F> {
height,
next.copied(),
challenges,
assign_pass,
)?;

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

for row_idx in offset..last_row {
Expand All @@ -1006,6 +1019,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 @@ -1027,6 +1041,7 @@ impl<F: Field> ExecutionConfig<F> {
|| Value::known(F::ZERO),
)?;

assign_pass += 1;
Ok(())
},
)
Expand Down Expand Up @@ -1077,6 +1092,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 @@ -1093,7 +1109,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 @@ -1116,6 +1141,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 @@ -1149,12 +1175,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 @@ -1163,6 +1201,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 @@ -1308,19 +1352,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 @@ -1347,6 +1404,30 @@ impl<F: Field> ExecutionConfig<F> {
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,
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 @@ -183,36 +183,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 @@ -284,6 +284,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<(Expression<F>, String)>,

meta: &'a mut ConstraintSystem<F>,
}
Expand Down Expand Up @@ -330,6 +331,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 @@ -1545,4 +1547,8 @@ impl<'a, F: Field> EVMConstraintBuilder<'a, F> {
None => 1.expr(),
}
}

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

0 comments on commit ae37c38

Please sign in to comment.