fix(avm): keccak pre-audit

barretenberg/cpp/pil/vm2/keccak_memory.pil

@@ -11,7 +11,7 @@ include "constants_gen.pil";
  * keccak_memory.start_read { keccak_memory.val_0_, keccak_memory.val_1_, ... keccak_memory.val_24_,
  *                            keccak_memory.clk, keccak_memory.addr, keccak_memory.space_id, keccak_memory.tag_error };
  *
- * Inputs: state_in_00, state_in_01, ... state_in_44, clk, src_addr, space_id
+ * Inputs: state_in_00, state_in_10, ... state_in_44, clk, src_addr, space_id
  * Output: tag_error
  *
  * Usage for writing a slice (permutation and not lookup):
@@ -26,10 +26,10 @@ include "constants_gen.pil";
  * Parameter: round is fixed to 24.
  *
  * - state_in_00, state_in_10, ... state_in_44 are the 25 U64 keccak state values of the read slice.
- * - state_out_00, state_out_10 ... state_out_44 are the 25 U64 keccak state values of the write slice.
+ * - state_out_00, state_out_10, ... state_out_44 are the 25 U64 keccak state values of the write slice.
  * - dst_addr and src_addr are the first memory offset of the pertaining slice.
  * - space_id serves to propagate the right memory space up to the memory trace.
- * - clk is required for the unicity in the permutation and to propagate to the memory trace
+ * - clk is required for uniqueness in the permutation and to propagate to the memory trace
  *   to unambiguously order the memory operations.
  * - tag_error is set to 1 if any tag error is detected.
  * - Passing the tuple element `round` serves to constrain it to be equal to 24 (see keccakf1600.pil).
@@ -40,10 +40,10 @@ namespace keccak_memory;
 // This gadget is only dedicated to read and write memory slices corresponding
 // to the input and output of keccakf1600. An input and output state for keccakf1600
 // is composed of 25 U64 contiguous memory values. This gadget will read or write
-// 25 such values based on a passed memory offset. It read/writes the 25 values
+// 25 such values based on a passed memory offset. It reads/writes the 25 values
 // and for the read case checks that each tag is U64. Otherwise, we return a tag error.
 //
-// Precondition: We assume the passed offset being such that offset + 24 < 2^32, so
+// Precondition: We assume the passed offset is such that offset + 24 < 2^32, so
 //               that the slice fits into the memory space.
 
 // We use a multi-row computation to shift the read/written values to the row where the lookup
@@ -90,6 +90,9 @@ sel * (1 - sel) = 0;
 #[skippable_if]
 sel = 0;
 
+// Weaker than the standard recipe: only prevents 0->1 transitions (not 1->0 mid-block).
+// However, this is safe because a truncated block (sel dropping to 0 early) cannot produce a valid
+// write: #[WRITE_TO_SLICE] is a permutation requiring round == 24 on a row with sel == 1.
 #[TRACE_CONTINUITY]
 (1 - precomputed.first_row) * (1 - sel) * sel' = 0;
 
@@ -206,7 +209,7 @@ val[5] = (1 - LATCH_CONDITION) * val[4]';
 val[6] = (1 - LATCH_CONDITION) * val[5]';
 #[VAL07]
 val[7] = (1 - LATCH_CONDITION) * val[6]';
-#[VAL8]
+#[VAL08]
 val[8] = (1 - LATCH_CONDITION) * val[7]';
 #[VAL09]
 val[9] = (1 - LATCH_CONDITION) * val[8]';
@@ -247,23 +250,23 @@ is memory.sel_keccak { memory.clk, memory.space_id, memory.address, memory.value
 
 // Used to constrain the number of rounds in keccakf1600.pil through the slice_write lookup.
 pol commit num_rounds;
-sel * (num_rounds - constants.AVM_KECCAKF1600_NUM_ROUNDS) = 0; // TODO: Remove once we support constants in lookups
+sel * (num_rounds - constants.AVM_KECCAKF1600_NUM_ROUNDS) = 0; // Lookup constant support: Can be removed when we support constants in lookups.
 
 /* Prevention of illegal memory operations:
  *
  * If `sel == 1` (required to trigger a memory operation) we have `ctr != 0` by #[SEL_CTR_NON_ZERO].
  * We consider two cases for the previous row above:
- * 1) LATCH_CONDITION == 1: By #[START_AFTER_LATCH] we have `start_read == 1` or `start_write` == 1 and implies that
+ * 1) LATCH_CONDITION == 1: By #[START_AFTER_LATCH] we have `start_read == 1` or `start_write == 1` which implies that
  *                          `ctr == 1` which is legitimate.
  * 2) LATCH_CONDITION == 0: By #[CTR_INCREMENT] and #[TRACE_CONTINUITY], we have ctr - 1 on the previous row.
  *                          We can continue this propagation bottom-up until we reach a row whose previous row
  *                          has `LATCH_CONDITION == 1`. We know that this exists because at the latest it
  *                          happens at the very first row of the trace (precomputed.first_row == 1). When this happens,
- *                          by #[START_AFTER_LATCH] we have `start_read == 1` or `start_write` == 1 and we must have
+ *                          by #[START_AFTER_LATCH] we have `start_read == 1` or `start_write == 1` and we must have
  *                          `ctr == 1`. This shows that this is a legitimate memory operation.
  *                          Note that if we were to start with a counter larger than AVM_KECCAKF1600_STATE_SIZE, then
  *                          in a bottom-up propagation, we would reach a row with `ctr == AVM_KECCAKF1600_STATE_SIZE`
  *                          and `last` and `LATCH_CONDITION` equal to 1. However, this would contradict that on the
- *                          below row `ctr == AVM_KECCAKF1600_STATE_SIZE + 1` and `start_read == 1` or `start_write == 1`.
+ *                          row below `ctr == AVM_KECCAKF1600_STATE_SIZE + 1` and `start_read == 1` or `start_write == 1`.
  *                          Namely, #[CTR_INIT] enforces `ctr == 1`.
  */