Skip to content

Commit

Permalink
Fix the error of the expr degree in signed comparator exceeding the m…
Browse files Browse the repository at this point in the history
…ax degree (privacy-scaling-explorations#296)

* reduce signed cmp degree

* improve debug information

* Update zkevm-circuits/src/evm_circuit/util/constraint_builder.rs

Co-authored-by: Han <[email protected]>

Co-authored-by: HAOYUatHZ <[email protected]>
Co-authored-by: Han <[email protected]>
  • Loading branch information
3 people authored Jan 21, 2022
1 parent 5c88289 commit 0ecd0c0
Show file tree
Hide file tree
Showing 6 changed files with 104 additions and 65 deletions.
3 changes: 2 additions & 1 deletion zkevm-circuits/src/evm_circuit/execution.rs
Original file line number Diff line number Diff line change
Expand Up @@ -296,7 +296,8 @@ impl<F: FieldExt> ExecutionConfig<F> {

// Push lookups of this ExecutionState to independent_lookups for
// further configuration in configure_lookup.
independent_lookups.push(lookups);
independent_lookups
.push(lookups.iter().map(|(_, lookup)| lookup.clone()).collect());

gadget
}
Expand Down
19 changes: 11 additions & 8 deletions zkevm-circuits/src/evm_circuit/execution/bitwise.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,14 +47,17 @@ impl<F: FieldExt> ExecutionGadget<F> for BitwiseGadget<F> {
let tag = FixedTableTag::BitwiseAnd.expr()
+ (opcode.expr() - OpcodeId::AND.as_u64().expr());
for idx in 0..32 {
cb.add_lookup(Lookup::Fixed {
tag: tag.clone(),
values: [
a.cells[idx].expr(),
b.cells[idx].expr(),
c.cells[idx].expr(),
],
});
cb.add_lookup(
"Bitwise lookup",
Lookup::Fixed {
tag: tag.clone(),
values: [
a.cells[idx].expr(),
b.cells[idx].expr(),
c.cells[idx].expr(),
],
},
);
}

// State transition
Expand Down
12 changes: 7 additions & 5 deletions zkevm-circuits/src/evm_circuit/execution/signed_comparator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -107,11 +107,13 @@ impl<F: FieldExt> ExecutionGadget<F> for SignedComparatorGadget<F> {
// result = if b < 0 && a >= 0, slt = 0.
let a_neg_b_pos = (1.expr() - a_pos.expr()) * b_pos.expr();
let b_neg_a_pos = (1.expr() - b_pos.expr()) * a_pos.expr();
let result = select::expr(
a_neg_b_pos,
1.expr(),
select::expr(b_neg_a_pos, 0.expr(), a_lt_b),
);

// Only one of the following 3 condition can be true
// a_neg_b_pos => result = 1
// b_neg_a_pos => result = 0
// 1 - a_neg_b_pos - b_neg_a_pos => result = a_lt_b
let result = a_neg_b_pos.clone()
+ (1.expr() - a_neg_b_pos - b_neg_a_pos) * a_lt_b;

// Pop a and b from the stack, push the result on the stack.
cb.stack_pop(select::expr(is_sgt.expr(), b.expr(), a.expr()));
Expand Down
13 changes: 8 additions & 5 deletions zkevm-circuits/src/evm_circuit/execution/signextend.rs
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ impl<F: FieldExt> ExecutionGadget<F> for SignextendGadget<F> {
// selector is the sum of the current and all previous `is_selected`
// values.
cb.require_equal(
"Constrain selector == 1 when is_selected == 1 || previous selector == 1",
"Constrain selector == 1 when is_selected == 1 || previous selector == 1",
is_selected.clone()
+ if idx > 0 {
selectors[idx - 1].expr()
Expand All @@ -102,10 +102,13 @@ impl<F: FieldExt> ExecutionGadget<F> for SignextendGadget<F> {
// This will use the most significant bit of the selected byte to return
// the sign byte, which is a byte with all its bits set to the
// sign of the selected byte.
cb.add_lookup(Lookup::Fixed {
tag: FixedTableTag::SignByte.expr(),
values: [selected_byte, sign_byte.expr(), 0.expr()],
});
cb.add_lookup(
"SignByte lookup",
Lookup::Fixed {
tag: FixedTableTag::SignByte.expr(),
values: [selected_byte, sign_byte.expr(), 0.expr()],
},
);

// Verify the result.
// The LSB always remains the same, all other bytes with their selector
Expand Down
19 changes: 11 additions & 8 deletions zkevm-circuits/src/evm_circuit/util/common_gadget.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,14 +37,17 @@ impl<F: FieldExt> SameContextGadget<F> {
dynamic_gas_cost: Option<Expression<F>>,
) -> Self {
cb.opcode_lookup(opcode.expr(), 1.expr());
cb.add_lookup(Lookup::Fixed {
tag: FixedTableTag::ResponsibleOpcode.expr(),
values: [
cb.execution_state().as_u64().expr(),
opcode.expr(),
0.expr(),
],
});
cb.add_lookup(
"Responsible opcode lookup",
Lookup::Fixed {
tag: FixedTableTag::ResponsibleOpcode.expr(),
values: [
cb.execution_state().as_u64().expr(),
opcode.expr(),
0.expr(),
],
},
);

let mut gas_cost = cb
.execution_state()
Expand Down
103 changes: 65 additions & 38 deletions zkevm-circuits/src/evm_circuit/util/constraint_builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ pub(crate) struct ConstraintBuilder<'a, F> {
execution_state: ExecutionState,
constraints: Vec<(&'static str, Expression<F>)>,
constraints_first_step: Vec<(&'static str, Expression<F>)>,
lookups: Vec<Lookup<F>>,
lookups: Vec<(&'static str, Lookup<F>)>,
row_usages: Vec<StepRowUsage>,
rw_counter_offset: usize,
program_counter_offset: usize,
Expand Down Expand Up @@ -95,7 +95,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
) -> (
Vec<(&'static str, Expression<F>)>,
Vec<(&'static str, Expression<F>)>,
Vec<Lookup<F>>,
Vec<(&'static str, Lookup<F>)>,
Vec<Preset<F>>,
) {
let mut constraints = self.constraints;
Expand Down Expand Up @@ -142,8 +142,8 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
.collect(),
self.lookups
.into_iter()
.map(|lookup| {
lookup.conditional(execution_state_selector.clone())
.map(|(name, lookup)| {
(name, lookup.conditional(execution_state_selector.clone()))
})
.collect(),
presets,
Expand Down Expand Up @@ -358,17 +358,20 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
// Fixed

pub(crate) fn range_lookup(&mut self, value: Expression<F>, range: u64) {
let tag = match range {
16 => FixedTableTag::Range16,
32 => FixedTableTag::Range32,
256 => FixedTableTag::Range256,
512 => FixedTableTag::Range512,
let (name, tag) = match range {
16 => ("Range16", FixedTableTag::Range16),
32 => ("Range32", FixedTableTag::Range32),
256 => ("Range256", FixedTableTag::Range256),
512 => ("Range512", FixedTableTag::Range512),
_ => unimplemented!(),
};
self.add_lookup(Lookup::Fixed {
tag: tag.expr(),
values: [value, 0.expr(), 0.expr()],
});
self.add_lookup(
name,
Lookup::Fixed {
tag: tag.expr(),
values: [value, 0.expr(), 0.expr()],
},
);
}

// Opcode
Expand Down Expand Up @@ -400,6 +403,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
is_root_create.clone(),
);
self.add_lookup(
"Opcode lookup",
Lookup::Bytecode {
hash: self.curr.state.opcode_source.expr(),
index,
Expand Down Expand Up @@ -438,12 +442,15 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
field_tag: Expression<F>,
value: Expression<F>,
) {
self.add_lookup(Lookup::Tx {
id,
field_tag,
index: 0.expr(),
value,
});
self.add_lookup(
"Tx lookup",
Lookup::Tx {
id,
field_tag,
index: 0.expr(),
value,
},
);
}

// block
Expand All @@ -453,11 +460,14 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
number: Option<Expression<F>>,
val: Expression<F>,
) {
self.add_lookup(Lookup::Block {
field_tag: tag,
number: number.unwrap_or_else(|| 0.expr()),
value: val,
});
self.add_lookup(
"Block lookup",
Lookup::Block {
field_tag: tag,
number: number.unwrap_or_else(|| 0.expr()),
value: val,
},
);
}

// Rw
Expand All @@ -466,28 +476,34 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
/// useful for state reversion or dummuy lookup.
fn rw_lookup_with_counter(
&mut self,
name: &'static str,
counter: Expression<F>,
is_write: Expression<F>,
tag: RwTableTag,
values: [Expression<F>; 5],
) {
self.add_lookup(Lookup::Rw {
counter,
is_write,
tag: tag.expr(),
values,
});
self.add_lookup(
name,
Lookup::Rw {
counter,
is_write,
tag: tag.expr(),
values,
},
);
}

/// Add a Lookup::Rw and increase the rw_counter_offset, useful in normal
/// cases.
fn rw_lookup(
&mut self,
name: &'static str,
is_write: Expression<F>,
tag: RwTableTag,
values: [Expression<F>; 5],
) {
self.rw_lookup_with_counter(
name,
self.curr.state.rw_counter.expr() + self.rw_counter_offset.expr(),
is_write,
tag,
Expand All @@ -498,12 +514,13 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {

fn state_write_with_reversion(
&mut self,
name: &'static str,
tag: RwTableTag,
mut values: [Expression<F>; 5],
is_persistent: Expression<F>,
rw_counter_end_of_reversion: Expression<F>,
) {
self.rw_lookup(true.expr(), tag, values.clone());
self.rw_lookup(name, true.expr(), tag, values.clone());

// Revert if is_persistent is 0
self.condition(1.expr() - is_persistent, |cb| {
Expand All @@ -521,6 +538,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
}

cb.rw_lookup_with_counter(
name,
rw_counter_end_of_reversion - state_write_counter,
true.expr(),
tag,
Expand All @@ -541,6 +559,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
value_prev: Expression<F>,
) {
self.rw_lookup(
"AccountAccessList write",
true.expr(),
RwTableTag::TxAccessListAccount,
[tx_id, account_address, value, value_prev, 0.expr()],
Expand All @@ -556,6 +575,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
value: Expression<F>,
) {
self.rw_lookup(
"Account read",
false.expr(),
RwTableTag::Account,
[
Expand All @@ -576,6 +596,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
value_prev: Expression<F>,
) {
self.rw_lookup(
"Account write",
true.expr(),
RwTableTag::Account,
[
Expand All @@ -598,6 +619,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
rw_counter_end_of_reversion: Expression<F>,
) {
self.state_write_with_reversion(
"Account write with reversion",
RwTableTag::Account,
[
account_address,
Expand Down Expand Up @@ -630,6 +652,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
value: Expression<F>,
) {
self.rw_lookup(
"CallContext lookup",
false.expr(),
RwTableTag::CallContext,
[
Expand Down Expand Up @@ -665,6 +688,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
value: Expression<F>,
) {
self.rw_lookup(
"Stack lookup",
is_write,
RwTableTag::Stack,
[
Expand All @@ -686,6 +710,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
byte: Expression<F>,
) {
self.rw_lookup(
"Memory lookup",
is_write,
RwTableTag::Memory,
[
Expand All @@ -706,6 +731,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
byte: Expression<F>,
) {
self.rw_lookup_with_counter(
"Memory lookup",
rw_counter,
is_write,
RwTableTag::Memory,
Expand All @@ -721,10 +747,11 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {

// Validation

pub(crate) fn validate_degree(&self, degree: usize) {
pub(crate) fn validate_degree(&self, degree: usize, name: &'static str) {
assert!(
degree <= MAX_DEGREE,
"Expression degree too high: {} > {}",
"Expression {} degree too high: {} > {}",
name,
degree,
MAX_DEGREE,
);
Expand Down Expand Up @@ -765,7 +792,7 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
Some(condition) => condition.clone() * constraint,
None => constraint,
};
self.validate_degree(constraint.degree());
self.validate_degree(constraint.degree(), name);
self.constraints.push((name, constraint));
}

Expand All @@ -778,16 +805,16 @@ impl<'a, F: FieldExt> ConstraintBuilder<'a, F> {
Some(condition) => condition.clone() * constraint,
None => constraint,
};
self.validate_degree(constraint.degree());
self.validate_degree(constraint.degree(), name);
self.constraints_first_step.push((name, constraint));
}

pub(crate) fn add_lookup(&mut self, lookup: Lookup<F>) {
pub(crate) fn add_lookup(&mut self, name: &'static str, lookup: Lookup<F>) {
let lookup = match &self.condition {
Some(condition) => lookup.conditional(condition.clone()),
None => lookup,
};
self.validate_degree(lookup.degree() + LOOKUP_DEGREE);
self.lookups.push(lookup);
self.validate_degree(lookup.degree() + LOOKUP_DEGREE, name);
self.lookups.push((name, lookup));
}
}

0 comments on commit 0ecd0c0

Please sign in to comment.