copy-fix-terminate: secure termination (#649)

* copy-fix-terminate: stronger termination requirements

* copy-fix-terminate: add witness generation, doc, and fix tests

---------

Co-authored-by: Aurélien Nicolas <[email protected]>

Author: naure

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| F::from(*bit) + 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

@@ -57,6 +57,11 @@ const NEXT_ROW: Rotation = Rotation(1);
 /// The next step, processing the next byte. This connects reader-to-reader or writer-to-writer.
 const NEXT_STEP: Rotation = Rotation(2);
 
+// 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> {
@@ -208,7 +213,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
         constrain_tag(
             meta,
             q_enable,
-            tag,
+            &tag,
             is_precompiled,
             is_tx_calldata,
             is_bytecode,
@@ -238,7 +243,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
 
             constrain_first_last(cb, is_reader.expr(), is_first.expr(), is_last.expr());
 
-            constrain_must_terminate(cb, meta, q_enable, is_last.expr());
+            constrain_must_terminate(cb, meta, q_enable, &tag);
 
             constrain_forward_parameters(cb, meta, is_continue.expr(), id, tag, src_addr_end);
 
@@ -627,15 +632,13 @@ impl<F: Field> CopyCircuitConfig<F> {
     ) -> Result<(), Error> {
         let copy_rows_needed = copy_events
             .iter()
-            .map(|c| c.copy_bytes.bytes.len() * 2)
+            .map(|c| c.full_length() as usize * 2)
             .sum::<usize>();
-
-        // The `+ 2` is used to take into account the two extra empty copy rows needed
-        // to satisfy the queries at `NEXT_STEP`.
         assert!(
-            copy_rows_needed + 2 <= max_copy_rows,
+            copy_rows_needed + DISABLED_ROWS + UNUSED_ROWS <= max_copy_rows,
             "copy rows not enough {copy_rows_needed} 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 is_src_end_chip = IsEqualChip::construct(self.is_src_end.clone());
@@ -662,7 +665,7 @@ impl<F: Field> CopyCircuitConfig<F> {
                         "offset is {} before {}th copy event(bytes len: {}): {:?}",
                         offset,
                         ev_idx,
-                        copy_event.copy_bytes.bytes.len(),
+                        copy_event.full_length(),
                         {
                             let mut copy_event = copy_event.clone();
                             copy_event.copy_bytes.bytes.clear();
@@ -681,33 +684,28 @@ impl<F: Field> CopyCircuitConfig<F> {
                     log::trace!("offset after {}th copy event: {}", ev_idx, offset);
                 }
 
-                for _ in 0..max_copy_rows - copy_rows_needed - 2 {
+                for _ in 0..filler_rows {
                     self.assign_padding_row(
                         &mut region,
                         &mut offset,
-                        false,
+                        true,
                         &tag_chip,
                         &is_src_end_chip,
                         &lt_word_end_chip,
                     )?;
                 }
+                assert_eq!(offset % 2, 0, "enabled rows must come in pairs");
 
-                self.assign_padding_row(
-                    &mut region,
-                    &mut offset,
-                    true,
-                    &tag_chip,
-                    &is_src_end_chip,
-                    &lt_word_end_chip,
-                )?;
-                self.assign_padding_row(
-                    &mut region,
-                    &mut offset,
-                    true,
-                    &tag_chip,
-                    &is_src_end_chip,
-                    &lt_word_end_chip,
-                )?;
+                for _ in 0..DISABLED_ROWS {
+                    self.assign_padding_row(
+                        &mut region,
+                        &mut offset,
+                        false,
+                        &tag_chip,
+                        &is_src_end_chip,
+                        &lt_word_end_chip,
+                    )?;
+                }
 
                 Ok(())
             },
@@ -719,7 +717,7 @@ impl<F: Field> CopyCircuitConfig<F> {
         &self,
         region: &mut Region<F>,
         offset: &mut usize,
-        is_last_two: bool,
+        enabled: bool,
         tag_chip: &BinaryNumberChip<F, CopyDataType, 4>,
         is_src_end_chip: &IsEqualChip<F>,
         lt_word_end_chip: &IsEqualChip<F>,
@@ -729,13 +727,11 @@ impl<F: Field> CopyCircuitConfig<F> {
             || "q_enable",
             self.q_enable,
             *offset,
-            || Value::known(F::from(!is_last_two)),
+            || Value::known(F::from(enabled)),
         )?;
-        if !is_last_two {
-            // q_step
-            if *offset % 2 == 0 {
-                self.q_step.enable(region, *offset)?;
-            }
+        // q_step
+        if enabled && *offset % 2 == 0 {
+            self.q_step.enable(region, *offset)?;
         }
 
         // is_first
@@ -1012,9 +1008,10 @@ impl<F: Field> SubCircuit<F> for CopyCircuit<F> {
             block
                 .copy_events
                 .iter()
-                .map(|c| c.copy_bytes.bytes.len() * 2)
+                .map(|c| c.full_length() as usize * 2)
                 .sum::<usize>()
-                + 2,
+                + UNUSED_ROWS
+                + DISABLED_ROWS,
             block.circuits_params.max_copy_rows,
         )
     }

zkevm-circuits/src/copy_circuit/copy_gadgets.rs

@@ -14,7 +14,7 @@ use crate::evm_circuit::util::constraint_builder::{BaseConstraintBuilder, Constr
 pub fn constrain_tag<F: Field>(
     meta: &mut ConstraintSystem<F>,
     q_enable: Column<Fixed>,
-    tag: BinaryNumberConfig<CopyDataType, 4>,
+    tag: &BinaryNumberConfig<CopyDataType, 4>,
     is_precompiled: Column<Advice>,
     is_tx_calldata: Column<Advice>,
     is_bytecode: Column<Advice>,
@@ -85,17 +85,22 @@ pub fn constrain_must_terminate<F: Field>(
     cb: &mut BaseConstraintBuilder<F>,
     meta: &mut VirtualCells<'_, F>,
     q_enable: Column<Fixed>,
-    is_last: Expression<F>,
+    tag: &BinaryNumberConfig<CopyDataType, 4>,
 ) {
-    // Prevent an event from spilling into the rows where constraints are disabled.
-    // This also ensures that eventually is_last=1, because eventually q_enable=0.
-    cb.require_zero(
-        "the next row is enabled",
-        and::expr([
-            not::expr(is_last),
-            not::expr(meta.query_fixed(q_enable, NEXT_ROW)),
-        ]),
-    );
+    // 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 constrain_forward_parameters. 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(CURRENT)(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, NEXT_STEP),
+            1.expr(),
+        );
+    });
 }
 
 /// Copy the parameters of the event through all rows of the event.

zkevm-circuits/src/copy_circuit/test.rs

@@ -62,7 +62,7 @@ pub fn test_copy_circuit_from_block<F: Field>(
 }
 
 fn gen_calldatacopy_data() -> CircuitInputBuilder {
-    let length = 0x0fffusize;
+    let length = 512 / 2 - 32;
     let code = bytecode! {
         PUSH32(Word::from(length))
         PUSH32(Word::from(0x00))
@@ -87,9 +87,9 @@ fn gen_calldatacopy_data() -> CircuitInputBuilder {
     let mut builder = BlockData::new_from_geth_data_with_params(
         block.clone(),
         CircuitsParams {
-            max_rws: 8192,
-            max_copy_rows: 8192 + 2,
-            max_calldata: 5000,
+            max_rws: 512,
+            max_copy_rows: 512,
+            max_calldata: 512,
             ..Default::default()
         },
     )
@@ -173,9 +173,9 @@ fn gen_returndatacopy_data() -> CircuitInputBuilder {
     let mut builder = BlockData::new_from_geth_data_with_params(
         block.clone(),
         CircuitsParams {
-            max_rws: 8192,
-            max_copy_rows: 8192 + 2,
-            max_calldata: 5000,
+            max_rws: 512,
+            max_copy_rows: 512,
+            max_calldata: 512,
             ..Default::default()
         },
     )
@@ -224,14 +224,14 @@ fn gen_extcodecopy_data() -> CircuitInputBuilder {
 }
 
 fn gen_sha3_data() -> CircuitInputBuilder {
-    let (code, _) = gen_sha3_code(0x20, 0x200, MemoryKind::EqualToSize);
+    let (code, _) = gen_sha3_code(0x20, 512 - 32, MemoryKind::EqualToSize);
     let test_ctx = TestContext::<2, 1>::simple_ctx_with_bytecode(code).unwrap();
     let block: GethData = test_ctx.into();
     let mut builder = BlockData::new_from_geth_data_with_params(
         block.clone(),
         CircuitsParams {
-            max_rws: 2000,
-            max_copy_rows: 0x250 * 2 + 2,
+            max_rws: 1024,
+            max_copy_rows: 1024,
             ..Default::default()
         },
     )
@@ -308,7 +308,7 @@ fn gen_return_data() -> CircuitInputBuilder {
 fn copy_circuit_valid_calldatacopy() {
     let builder = gen_calldatacopy_data();
     let block = block_convert::<Fr>(&builder.block, &builder.code_db).unwrap();
-    assert_eq!(test_copy_circuit_from_block(14, block), Ok(()));
+    assert_eq!(test_copy_circuit_from_block(10, block), Ok(()));
 }
 
 #[test]
@@ -322,7 +322,7 @@ fn copy_circuit_valid_codecopy() {
 fn copy_circuit_valid_returndatacopy() {
     let builder = gen_returndatacopy_data();
     let block = block_convert::<Fr>(&builder.block, &builder.code_db).unwrap();
-    assert_eq!(test_copy_circuit_from_block(14, block), Ok(()));
+    assert_eq!(test_copy_circuit_from_block(10, block), Ok(()));
 }
 
 #[test]
@@ -373,7 +373,7 @@ fn copy_circuit_invalid_calldatacopy() {
     let block = block_convert::<Fr>(&builder.block, &builder.code_db).unwrap();
 
     assert_error_matches(
-        test_copy_circuit_from_block(14, block),
+        test_copy_circuit_from_block(10, block),
         vec!["Memory word lookup", "Tx calldata lookup"],
     );
 }

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

@@ -324,7 +324,7 @@ mod test {
         CircuitTestBuilder::new_from_test_ctx(ctx)
             .params(CircuitsParams {
                 max_rws: 2048,
-                max_copy_rows: 1795,
+                max_copy_rows: 1796,
                 ..Default::default()
             })
             .run();