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

Add debug expr in EVMConstraintBuilder #1500

Merged
merged 5 commits into from
Jul 7, 2023
Merged

Add debug expr in EVMConstraintBuilder #1500

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
ae37c38
Add debug expr in EVMConstraintBuilder
ed255 Jun 22, 2023
b6be489
Merge branch 'main' into feature/debug-expr-evm1
ChihChengLiang Jul 4, 2023
082346c
Merge branch 'main' into feature/debug-expr-evm1
ed255 Jul 7, 2023
0c62d2c
Update from @hero78119 feedback
ed255 Jul 7, 2023
b28c00a
Merge branch 'main' into feature/debug-expr-evm1
ed255 Jul 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
111 changes: 96 additions & 15 deletions zkevm-circuits/src/evm_circuit/execution.rs
View file
Open in desktop
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 @@ -223,6 +223,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 @@ -452,6 +453,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 @@ -473,6 +475,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 @@ -578,6 +581,7 @@ impl<F: Field> ExecutionConfig<F> {
step: step_curr,
height_map,
stored_expressions_map,
debug_expressions_map,
instrument,
};

Expand Down Expand Up @@ -616,6 +620,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 @@ -656,6 +661,7 @@ impl<F: Field> ExecutionConfig<F> {
step_next,
height_map,
stored_expressions_map,
debug_expressions_map,
instrument,
G::NAME,
G::EXECUTION_STATE,
Expand All @@ -677,6 +683,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 @@ -694,6 +701,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 @@ -706,6 +714,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 @@ -908,6 +917,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 @@ -961,6 +972,7 @@ impl<F: Field> ExecutionConfig<F> {
height,
next.copied(),
challenges,
assign_pass,
)?;

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

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

assign_pass += 1;
Ok(())
},
)
Expand Down Expand Up @@ -1091,6 +1106,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 @@ -1107,7 +1123,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 @@ -1130,6 +1155,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 @@ -1163,12 +1189,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 @@ -1177,6 +1215,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,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Will is_final or is_final_step be better? Or has_next if final_step is not accurate. I understand to use is as prefix while it's a bool type but in this case is_next is not clear to know what it really means.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think is_final or has_next doesn't hold the real meaning here. Let me explain why I call this is_next. Each step is assigned two times. The list of steps is iterated in a window of size 2 where we have (current_step, next_step), and we assign the next first and the current afterwards in each iteration. See

zkevm-circuits/zkevm-circuits/src/evm_circuit/execution.rs

Lines 1180 to 1206 in b6be489

// Also set the witness of the next step.
// These may be used in stored expressions and
// so their witness values need to be known to be able
// to correctly calculate the intermediate value.
if let Some((transaction_next, call_next, step_next)) = next {
self.assign_exec_step_int(
region,
offset + height,
block,
transaction_next,
call_next,
step_next,
true,
assign_pass,
)?;
}
self.assign_exec_step_int(
region,
offset,
block,
transaction,
call,
step,
false,
assign_pass,
)

So if we have the steps [a, b, c] we pair them like (cur=a, next=b), (cur=b, next=c), (cur=c, next=None). And we do the following assignments:

  • b (next)
  • a (cur)
  • b (cur)
  • c (next)
  • c (cur)

So here the is_next means that we're assigning the next step before we assign the current steps for it's "side effects", but we'll go over and assign that step again later.

Do you have another suggestion instead of is_next that conveys this meaning?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for your explanation, is_next makes sense to me now. :)

// Layouter assignment pass
assign_pass: usize,
) -> Result<(), Error> {
self.step
.assign_exec_step(region, offset, block, call, step)?;
Expand Down Expand Up @@ -1320,19 +1364,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 @@ -1359,6 +1416,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
Open in desktop
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
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -303,6 +303,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 @@ -349,6 +350,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(&mut self, expr: Expression<F>, name: String) {
self.debug_expressions.push((expr, name));
}
}
Loading