Audit Fixes EIP2930/1559 RLP Decoding Table Correspondence

zkevm-circuits/src/rlp_circuit_fsm.rs

@@ -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
@@ -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(),
@@ -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);
@@ -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(
@@ -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,
@@ -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,
@@ -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,