copy-fix-terminate: enforce secure termination of the copy circuit (#…

…1568)

### Description

This PR fixes two soundness issues in the Copy circuit. 

1. There are a number of checks at the end of an event when is_last=1.
However, there are no guarantees that this last row exists. The last
event may not be checked fully.

2. The constraints may query cells of the "last two rows", whose content
is not constrained. For example, booleans are not necessarily booleans
there.

### Type of change

- [x] Bug fix (non-breaking change which fixes an issue)

### Content

This is a backport from Scroll, see more details here:
scroll-tech#649. Quoting:

The new constraint constrain_must_terminate guarantees that:
- a "last row" is eventually reached so that final checks happen,
- and every row of an event can safely query rotations 1 and 2.

Now to witness generation. There must be two additional rows that are
enabled so their content is verified, but not used because they touch
disabled rows. See UNUSED_ROWS.

Note that there was already a sanity check that no constraints query
reserved rows with the error `active on an unusable row - missing
selector?`. Rows can be reserved for blinding, or beyond max_rows, or
simply to avoid wrap around back to the first row. This check was
satisfied by adding two disabled rows (see assign_padding_row(…)).
However, this alone was not sound.

### How Has This Been Tested?

    cargo test --release -p zkevm-circuits -p zkevm-circuits  -- copy

Co-authored-by: Aurélien Nicolas <info@nau.re>

bus-mapping/src/circuit_input_builder.rs

@@ -388,7 +388,7 @@ impl CircuitInputBuilder<DynamicCParams> {
                 .iter()
                 .fold(0, |acc, c| acc + c.bytes.len())
                 * 2
-                + 2;
+                + 4; // disabled and unused rows.
 
             let total_rws_before_padding: usize =
                 <RWCounter as Into<usize>>::into(self.block_ctx.rwc) - 1; // -1 since rwc start from index `1`

gadgets/src/binary_number.rs

@@ -59,6 +59,15 @@ where
         }
     }
 
+    /// Return the constant that represents a given value. To be compared with the value expression.
+    pub fn constant_expr<F: Field>(&self, value: T) -> Expression<F> {
+        let f = value.as_bits().iter().fold(
+            F::ZERO,
+            |result, bit| if *bit { F::ONE } else { F::ZERO } + result * F::from(2),
+        );
+        Expression::Constant(f)
+    }
+
     /// Returns a function that can evaluate to a binary expression, that
     /// evaluates to 1 if value is equal to value as bits. The returned
     /// expression is of degree N.

zkevm-circuits/src/copy_circuit.rs

@@ -27,18 +27,26 @@ use bus_mapping::{
 };
 use eth_types::Field;
 use gadgets::{
-    binary_number::BinaryNumberChip,
+    binary_number::{BinaryNumberChip, BinaryNumberConfig},
     less_than::{LtChip, LtConfig, LtInstruction},
     util::{and, not, or, Expr},
 };
 use halo2_proofs::{
     circuit::{Layouter, Region, Value},
-    plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, SecondPhase, Selector},
+    plonk::{
+        Advice, Column, ConstraintSystem, Error, Expression, Fixed, SecondPhase, Selector,
+        VirtualCells,
+    },
     poly::Rotation,
 };
 use itertools::Itertools;
 use std::marker::PhantomData;
 
+// Rows to enable but not use, that can be queried safely by the last event.
+const UNUSED_ROWS: usize = 2;
+// Rows to disable, so they do not query into Halo2 reserved rows.
+const DISABLED_ROWS: usize = 2;
+
 /// The rw table shared between evm circuit and state circuit
 #[derive(Clone, Debug)]
 pub struct CopyCircuitConfig<F> {
@@ -161,6 +169,8 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
                 ]),
             );
 
+            constrain_must_terminate(&mut cb, meta, q_enable, &tag);
+
             let not_last_two_rows = 1.expr()
                 - meta.query_advice(is_last, Rotation::cur())
                 - meta.query_advice(is_last, Rotation::next());
@@ -468,6 +478,29 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
     }
 }
 
+/// Verify that is_last goes to 1 at some point.
+pub fn constrain_must_terminate<F: Field>(
+    cb: &mut BaseConstraintBuilder<F>,
+    meta: &mut VirtualCells<'_, F>,
+    q_enable: Column<Fixed>,
+    tag: &BinaryNumberConfig<CopyDataType, 3>,
+) {
+    // If an event has started (tag != Padding on reader and writer rows), require q_enable=1 at the
+    // next step. This prevents querying rows where constraints are disabled.
+    //
+    // The tag is then copied to the next step by "rows[0].tag == rows[2].tag". Eventually,
+    // q_enable=0. By that point the tag must have switched to Padding, which is only possible with
+    // is_last=1. This guarantees that all the final conditions are checked.
+    let is_event = tag.value(Rotation::cur())(meta) - tag.constant_expr::<F>(CopyDataType::Padding);
+    cb.condition(is_event, |cb| {
+        cb.require_equal(
+            "the next step is enabled",
+            meta.query_fixed(q_enable, Rotation(2)),
+            1.expr(),
+        );
+    });
+}
+
 impl<F: Field> CopyCircuitConfig<F> {
     /// Assign an individual copy event to the Copy Circuit.
     pub fn assign_copy_event(
@@ -566,11 +599,11 @@ impl<F: Field> CopyCircuitConfig<F> {
     ) -> Result<(), Error> {
         let copy_rows_needed = copy_events.iter().map(|c| c.bytes.len() * 2).sum::<usize>();
 
-        // The `+ 2` is used to take into account the two extra empty copy rows needed
-        // to satisfy the query at `Rotation(2)` performed inside of the
-        // `rows[2].value == rows[0].value * r + rows[1].value` requirement in the RLC
-        // Accumulation gate.
-        assert!(copy_rows_needed + 2 <= max_copy_rows);
+        assert!(
+            copy_rows_needed + DISABLED_ROWS + UNUSED_ROWS <= max_copy_rows,
+            "copy rows not enough {copy_rows_needed} + 4 vs {max_copy_rows}"
+        );
+        let filler_rows = max_copy_rows - copy_rows_needed - DISABLED_ROWS;
 
         let tag_chip = BinaryNumberChip::construct(self.copy_table.tag);
         let lt_chip = LtChip::construct(self.addr_lt_addr_end);
@@ -597,12 +630,14 @@ impl<F: Field> CopyCircuitConfig<F> {
                     )?;
                 }
 
-                for _ in 0..max_copy_rows - copy_rows_needed - 2 {
-                    self.assign_padding_row(&mut region, &mut offset, false, &tag_chip, &lt_chip)?;
+                for _ in 0..filler_rows {
+                    self.assign_padding_row(&mut region, &mut offset, true, &tag_chip, &lt_chip)?;
                 }
+                assert_eq!(offset % 2, 0, "enabled rows must come in pairs");
 
-                self.assign_padding_row(&mut region, &mut offset, true, &tag_chip, &lt_chip)?;
-                self.assign_padding_row(&mut region, &mut offset, true, &tag_chip, &lt_chip)?;
+                for _ in 0..DISABLED_ROWS {
+                    self.assign_padding_row(&mut region, &mut offset, false, &tag_chip, &lt_chip)?;
+                }
 
                 Ok(())
             },
@@ -613,22 +648,20 @@ impl<F: Field> CopyCircuitConfig<F> {
         &self,
         region: &mut Region<F>,
         offset: &mut usize,
-        is_last_two: bool,
+        enabled: bool,
         tag_chip: &BinaryNumberChip<F, CopyDataType, 3>,
         lt_chip: &LtChip<F, 8>,
     ) -> Result<(), Error> {
-        if !is_last_two {
-            // q_enable
-            region.assign_fixed(
-                || "q_enable",
-                self.q_enable,
-                *offset,
-                || Value::known(F::ONE),
-            )?;
-            // q_step
-            if *offset % 2 == 0 {
-                self.q_step.enable(region, *offset)?;
-            }
+        // q_enable
+        region.assign_fixed(
+            || "q_enable",
+            self.q_enable,
+            *offset,
+            || Value::known(if enabled { F::ONE } else { F::ZERO }),
+        )?;
+        // q_step
+        if enabled && *offset % 2 == 0 {
+            self.q_step.enable(region, *offset)?;
         }
 
         // is_first