Skip to content

Commit

Permalink
Audit Fixes EIP2930/1559 RLP Decoding Table Correspondence (#1181)
Browse files Browse the repository at this point in the history 
* Remove debug flags

* Add decoding table PUSH lookup correspondence

* Complete Stack Op Correspondence

* fmt

* Correct lookup constraint

* Remove unused macro

* fmt

* Correct lookup constraint for pre 2930 txs

* fmt

* Adjust comments

* fmt

* Add lookup indicator column for state machine

* Add correct condition for stack op lookups

* Complete PUSH op lookup

* Correct POP op lookup

* Correct PUSH lookup

* fmt

* Add backward compatibility for eip155 and pre155

* Add al_idx to input expression

* Add access list idx to PUSH correspondence

---------

Co-authored-by: DreamWuGit <[email protected]>
  • Loading branch information
@darth-cy @DreamWuGit
darth-cy and DreamWuGit authored Apr 24, 2024
1 parent ff2fbd4 commit e65f258
Showing 1 changed file with 274 additions and 42 deletions.
316 changes: 274 additions & 42 deletions zkevm-circuits/src/rlp_circuit_fsm.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -338,6 +338,12 @@ pub struct RlpCircuitConfig<F> {
is_stack_al_idx_diff: Column<Advice>,
/// Decoding table key change indicator. storage key idx change.
is_stack_sk_idx_diff: Column<Advice>,
/// Indicator column (PUSH) for lookup op into the decoding table from state machine
is_push_op_lookup: Column<Advice>,
/// Indicator column (POP) for lookup op into the decoding table from state machine
is_pop_op_lookup: Column<Advice>,
/// Indicator column (UPDATE) for lookup op into the decoding table from state machine
is_update_op_lookup: Column<Advice>,
/// Check for byte_value <= 0x80
byte_value_lte_0x80: ComparatorConfig<F, 1>,
/// Check for byte_value >= 0x80
Expand Down Expand Up @@ -417,6 +423,9 @@ impl<F: Field> RlpCircuitConfig<F> {
is_new_access_list_storage_key,
is_access_list_end,
is_storage_key_list_end,
is_push_op_lookup,
is_pop_op_lookup,
is_update_op_lookup,
) = (
meta.fixed_column(),
meta.fixed_column(),
Expand All @@ -440,6 +449,9 @@ impl<F: Field> RlpCircuitConfig<F> {
meta.advice_column(),
meta.advice_column(),
meta.advice_column(),
meta.advice_column(),
meta.advice_column(),
meta.advice_column(),
);

let tag_value_acc = meta.advice_column_in(SecondPhase);
Expand Down Expand Up @@ -2140,48 +2152,6 @@ impl<F: Field> RlpCircuitConfig<F> {
]))
});

meta.create_gate("Decoding table stack op INIT", |meta| {
let mut cb = BaseConstraintBuilder::default();

cb.require_equal(
"stack init pushes all remaining_bytes onto depth 0",
meta.query_advice(rlp_decoding_table.value, Rotation::cur()),
meta.query_advice(byte_rev_idx, Rotation::cur()),
);
cb.require_equal(
"stack can only init once with the first byte",
meta.query_advice(byte_idx, Rotation::cur()),
1.expr(),
);
cb.require_zero(
"stack inits at depth 0",
meta.query_advice(rlp_decoding_table.depth, Rotation::cur()),
);
cb.require_zero(
"stack inits with al_idx at 0",
meta.query_advice(rlp_decoding_table.al_idx, Rotation::cur()),
);
cb.require_zero(
"stack inits with sk_idx at 0",
meta.query_advice(rlp_decoding_table.sk_idx, Rotation::cur()),
);
cb.condition(
not::expr(meta.query_fixed(q_first, Rotation::cur())),
|cb| {
cb.require_boolean(
"tx_id can only stay the same or increment by 1",
meta.query_advice(rlp_decoding_table.tx_id, Rotation::cur())
- meta.query_advice(rlp_decoding_table.tx_id, Rotation::prev()),
);
},
);

cb.gate(and::expr([
meta.query_fixed(q_enabled, Rotation::cur()),
meta.query_advice(rlp_decoding_table.is_stack_init, Rotation::cur()),
]))
});

// Cross-depth stack constraints in the RlpDecodingTable
// These two sets of lookups ensure exact correspondence of PUSH and POP records
meta.lookup_any(
Expand Down Expand Up @@ -2256,6 +2226,235 @@ impl<F: Field> RlpCircuitConfig<F> {

debug_assert!(meta.degree() <= 9);

/////////////////////////////////////////////////////////////////////
///////// Rlp Decoding Table and RLP Circuit Correspondence /////////
/////////////////////////////////////////////////////////////////////
// RLP Decoding Table is sorted using an id = (tx_id, format, depth, access_list_idx,
// storage_key_idx) but bytes in the RLP circuit (rlp_table) is processed in order.
// Therefore, to prevent malicious injection of stack ops that don't correspond to
// actual bytes in the RLP circuit, lookups are added to ensure correct correspondence.

// The Init Op is not affected by sorting and stays at first position in decoding table.
// For this reason, its correctness and correspondence is constrained using a gate
// instead of lookup.
meta.create_gate("State machine lookup indicators into the decoding table", |meta| {
let mut cb = BaseConstraintBuilder::default();

// stack operation indicators
cb.require_equal(
"each state machine row (not padding) must correspond to a stack op in the decoding table",
sum::expr([
meta.query_advice(rlp_decoding_table.is_stack_init, Rotation::cur()), // INIT is not affected by sorting
meta.query_advice(is_push_op_lookup, Rotation::cur()),
meta.query_advice(is_pop_op_lookup, Rotation::cur()),
meta.query_advice(is_update_op_lookup, Rotation::cur()),
]),
1.expr(),
);

cb.require_boolean(
"is_push_op_lookup is binary",
meta.query_advice(is_push_op_lookup, Rotation::cur()),
);
cb.require_boolean(
"is_pop_op_lookup is binary",
meta.query_advice(is_pop_op_lookup, Rotation::cur()),
);
cb.require_boolean(
"is_update_op_lookup is binary",
meta.query_advice(is_update_op_lookup, Rotation::cur()),
);

// Correct state machine condition for PUSH op
cb.require_equal(
"is_push_op_lookup is the last row of a begin tag",
meta.query_advice(is_push_op_lookup, Rotation::cur()),
and::expr([
meta.query_advice(is_tag_begin, Rotation::cur()),
state_bits.value_equals(State::DecodeTagStart, Rotation::next())(meta),
// Backward compatibility for EIP155 and pre-155 txs. The first begin tag corresponds to INIT
not::expr(meta.query_advice(rlp_decoding_table.is_stack_init, Rotation::cur())),
])
);
cb.condition(
meta.query_advice(is_push_op_lookup, Rotation::cur()), |cb| {
cb.require_equal(
"PUSH op within state machine should increase depth",
meta.query_advice(depth, Rotation::cur()) + 1.expr(),
meta.query_advice(depth, Rotation::next()),
);
});

// Correct state machine condition for POP op
cb.require_equal(
"is_pop_op_lookup is the last row of an end tag",
meta.query_advice(is_pop_op_lookup, Rotation::cur()),
meta.query_advice(is_tag_end, Rotation::cur()),
);
cb.condition(
meta.query_advice(is_pop_op_lookup, Rotation::cur()),
|cb| {
cb.require_zero(
"POP op within state machine should decrease depth, except the last byte of an instance.",
(
meta.query_advice(depth, Rotation::next()) + 1.expr()
- meta.query_advice(depth, Rotation::cur())
) * (
meta.query_advice(byte_rev_idx, Rotation::cur()) - 1.expr()
),
);
});

cb.gate(and::expr([
meta.query_fixed(q_enabled, Rotation::cur()),
not::expr(is_end(meta)),
]))
});

meta.create_gate("Decoding table stack op INIT correspondence", |meta| {
let mut cb = BaseConstraintBuilder::default();

cb.require_equal(
"stack init pushes all remaining_bytes onto depth 0",
meta.query_advice(rlp_decoding_table.value, Rotation::cur()),
meta.query_advice(byte_rev_idx, Rotation::cur()),
);
cb.require_equal(
"stack can only init once with the first byte",
meta.query_advice(byte_idx, Rotation::cur()),
1.expr(),
);
cb.require_zero(
"stack inits at depth 0",
meta.query_advice(rlp_decoding_table.depth, Rotation::cur()),
);
cb.require_zero(
"stack inits with al_idx at 0",
meta.query_advice(rlp_decoding_table.al_idx, Rotation::cur()),
);
cb.require_zero(
"stack inits with sk_idx at 0",
meta.query_advice(rlp_decoding_table.sk_idx, Rotation::cur()),
);
cb.condition(
not::expr(meta.query_fixed(q_first, Rotation::cur())),
|cb| {
cb.require_boolean(
"tx_id can only stay the same or increment by 1",
meta.query_advice(rlp_decoding_table.tx_id, Rotation::cur())
- meta.query_advice(rlp_decoding_table.tx_id, Rotation::prev()),
);
},
);
cb.require_equal(
"Init Op has DecodeTagStart in the state machine",
is_decode_tag_start(meta),
1.expr(),
);

cb.gate(and::expr([
meta.query_fixed(q_enabled, Rotation::cur()),
meta.query_advice(rlp_decoding_table.is_stack_init, Rotation::cur()),
]))
});

meta.lookup_any("Decoding table stack op PUSH correspondence", |meta| {
let enable = meta.query_advice(is_push_op_lookup, Rotation::cur());

let input_exprs = vec![
meta.query_advice(tx_id, Rotation::cur()),
meta.query_advice(format, Rotation::cur()),
meta.query_advice(byte_idx, Rotation::cur()),
meta.query_advice(depth, Rotation::cur()) + 1.expr(),
1.expr(),
select::expr(
is_decode_tag_start(meta),
meta.query_advice(byte_value, Rotation::cur()) - 192.expr(),
meta.query_advice(tag_value_acc, Rotation::cur()),
),
0.expr(),
meta.query_advice(rlp_table.access_list_idx, Rotation::cur()),
];
let table_exprs = vec![
meta.query_advice(rlp_decoding_table.tx_id, Rotation::cur()),
meta.query_advice(rlp_decoding_table.format, Rotation::cur()),
meta.query_advice(rlp_decoding_table.byte_idx, Rotation::cur()),
meta.query_advice(rlp_decoding_table.depth, Rotation::cur()),
meta.query_advice(rlp_decoding_table.is_stack_push, Rotation::cur()),
meta.query_advice(rlp_decoding_table.value, Rotation::cur()),
meta.query_advice(rlp_decoding_table.value_prev, Rotation::cur()),
select::expr(
meta.query_advice(is_stack_depth_three, Rotation::cur()),
meta.query_advice(rlp_decoding_table.al_idx, Rotation::cur()) - 1.expr(),
meta.query_advice(rlp_decoding_table.al_idx, Rotation::cur()),
),
];
input_exprs
.into_iter()
.zip(table_exprs)
.map(|(input, table)| (input * enable.expr(), table))
.collect()
});

meta.lookup_any("Decoding table stack op POP correspondence", |meta| {
let enable = select::expr(
sum::expr([
meta.query_advice(rlp_decoding_table.is_stack_init, Rotation::next()),
is_padding_in_dt.expr(Rotation::next())(meta),
]),
0.expr(),
meta.query_advice(is_pop_op_lookup, Rotation::cur()),
);

let input_exprs = vec![
meta.query_advice(tx_id, Rotation::cur()),
meta.query_advice(format, Rotation::cur()),
meta.query_advice(byte_idx, Rotation::cur()),
meta.query_advice(depth, Rotation::cur()) - 1.expr(),
1.expr(),
];
let table_exprs = vec![
meta.query_advice(rlp_decoding_table.tx_id, Rotation::cur()),
meta.query_advice(rlp_decoding_table.format, Rotation::cur()),
meta.query_advice(rlp_decoding_table.byte_idx, Rotation::cur()),
meta.query_advice(rlp_decoding_table.depth, Rotation::cur()),
meta.query_advice(rlp_decoding_table.is_stack_pop, Rotation::cur()),
];
input_exprs
.into_iter()
.zip(table_exprs)
.map(|(input, table)| (input * enable.expr(), table))
.collect()
});

meta.lookup_any("Decoding table stack op UPDATE correspondence", |meta| {
let enable = meta.query_advice(is_update_op_lookup, Rotation::cur());

let input_exprs = vec![
meta.query_advice(tx_id, Rotation::cur()),
meta.query_advice(format, Rotation::cur()),
meta.query_advice(byte_idx, Rotation::cur()),
meta.query_advice(depth, Rotation::cur()),
1.expr(),
meta.query_advice(rlp_table.access_list_idx, Rotation::cur()),
];
let table_exprs = vec![
meta.query_advice(rlp_decoding_table.tx_id, Rotation::cur()),
meta.query_advice(rlp_decoding_table.format, Rotation::cur()),
meta.query_advice(rlp_decoding_table.byte_idx, Rotation::cur()),
meta.query_advice(rlp_decoding_table.depth, Rotation::cur()),
meta.query_advice(rlp_decoding_table.is_stack_update, Rotation::cur()),
meta.query_advice(rlp_decoding_table.al_idx, Rotation::cur()),
];
input_exprs
.into_iter()
.zip(table_exprs)
.map(|(input, table)| (input * enable.expr(), table))
.collect()
});

debug_assert!(meta.degree() <= 9);

Self {
q_first,
q_last,
Expand Down Expand Up @@ -2299,6 +2498,9 @@ impl<F: Field> RlpCircuitConfig<F> {
is_stack_depth_diff,
is_stack_al_idx_diff,
is_stack_sk_idx_diff,
is_push_op_lookup,
is_pop_op_lookup,
is_update_op_lookup,
byte_value_lte_0x80,
byte_value_gte_0x80,
byte_value_lte_0xb8,
Expand Down Expand Up @@ -2359,6 +2561,36 @@ impl<F: Field> RlpCircuitConfig<F> {
))
},
)?;

// Assign lookup indicators from state machine into decoding table
let is_init = matches!(witness.rlp_decoding_table.stack_op, StackOp::Init);
let is_begin = !is_init
&& (witness_next.is_none()
|| witness_next.unwrap().state_machine.state == State::DecodeTagStart)
&& (witness.state_machine.tag == Tag::BeginObject
|| witness.state_machine.tag == Tag::BeginVector);
region.assign_advice(
|| "is_push_op_lookup",
self.is_push_op_lookup,
row,
|| Value::known(F::from(is_begin as u64)),
)?;
let is_end = witness.state_machine.tag == Tag::EndVector
|| witness.state_machine.tag == Tag::EndObject;
region.assign_advice(
|| "is_pop_op_lookup",
self.is_pop_op_lookup,
row,
|| Value::known(F::from(is_end as u64)),
)?;
let is_update = !(is_init || is_begin || is_end);
region.assign_advice(
|| "is_update_op_lookup",
self.is_update_op_lookup,
row,
|| Value::known(F::from(is_update as u64)),
)?;

region.assign_advice(
|| "rlp_table.tag_value",
self.rlp_table.tag_value,
Expand Down

0 comments on commit e65f258

Please sign in to comment.