feat: merge-train/avm

barretenberg/cpp/pil/vm2/keccak_memory.pil

@@ -90,6 +90,9 @@ sel * (1 - sel) = 0;
 #[skippable_if]
 sel = 0;
 
+#[TRACE_CONTINUITY]
+(1 - precomputed.first_row) * (1 - sel) * sel' = 0;
+
 pol commit start_read; // @boolean
 start_read * (1 - start_read) = 0;
 
@@ -109,11 +112,13 @@ pol commit val[25];
 // We enforce the initial ctr to be set to 1.
 #[CTR_INIT]
 (start_read + start_write) * (ctr - 1) = 0;
+// It follows that: `start_read == 1 ==> sel == 1` and `start_write == 1 ==> sel == 1`.
 
 #[RW_READ_INIT]
 start_read * rw = 0;
 #[RW_WRITE_INIT]
 start_write * (1 - rw) = 0;
+// It follows that `start_read` and `start_write` are mutually exclusive.
 
 // sel == 1 <==> ctr != 0
 pol commit ctr_inv;
@@ -137,9 +142,18 @@ pol commit last; // @boolean (by definition)
 #[LAST]
 last = 1 - (1 - ctr_end) * (1 - single_tag_error);
 
+#[LAST_HAS_SEL_ON]
+last * (1 - sel) = 0;
+
+// Latch condition is boolean because `last` cannot be activated at first row due to #[LAST_HAS_SEL_ON].
+pol LATCH_CONDITION = last + precomputed.first_row;
+
+#[START_AFTER_LATCH]
+sel' * (start_read' + start_write' - LATCH_CONDITION) = 0;
+
 #[CTR_INCREMENT]
 // Note: sel factor is required for an empty row to satisfy this relation
-sel * (1 - last) * (ctr' - ctr - 1) = 0;
+sel * (1 - LATCH_CONDITION) * (ctr' - ctr - 1) = 0;
 
 // Copied from memory.pil through lookup and constrained to be boolean in memory.pil.
 pol commit rw; // @boolean (constrained by memory.pil)
@@ -155,21 +169,21 @@ rw * single_tag_error = 0;
 last * (tag_error - single_tag_error) = 0;
 
 #[TAG_ERROR_PROPAGATION]
-(1 - last) * (tag_error - tag_error') = 0;
+(1 - LATCH_CONDITION) * (tag_error - tag_error') = 0;
 
 // No need to enforce a boolean constraint for tag_error as it follows from the above constraints.
 
 #[MEM_ADDR_INCREMENT]
-sel * (1 - last) * (addr + 1 - addr') = 0;
+sel * (1 - LATCH_CONDITION) * (addr + 1 - addr') = 0;
 
 #[SPACEID_PROPAGATION]
-(1 - last) * (space_id - space_id') = 0;
+(1 - LATCH_CONDITION) * (space_id - space_id') = 0;
 
 #[CLK_PROPAGATION]
-(1 - last) * (clk' - clk) = 0;
+(1 - LATCH_CONDITION) * (clk' - clk) = 0;
 
 #[RW_PROPAGATION]
-(1 - last) * (rw' - rw) = 0;
+(1 - LATCH_CONDITION) * (rw' - rw) = 0;
 
 // Check if the tag is U64
 // We constrain single_tag_error == 1 <==> tag is not U64.
@@ -179,53 +193,53 @@ pol TAG_MIN_U64 = tag - constants.MEM_TAG_U64;
 sel * (TAG_MIN_U64 * ((1 - single_tag_error) * (1 - tag_min_u64_inv) + tag_min_u64_inv) - single_tag_error) = 0;
 
 #[VAL01]
-val[1] = (1 - last) * val[0]';
+val[1] = (1 - LATCH_CONDITION) * val[0]';
 #[VAL02]
-val[2] = (1 - last) * val[1]';
+val[2] = (1 - LATCH_CONDITION) * val[1]';
 #[VAL03]
-val[3] = (1 - last) * val[2]';
+val[3] = (1 - LATCH_CONDITION) * val[2]';
 #[VAL04]
-val[4] = (1 - last) * val[3]';
+val[4] = (1 - LATCH_CONDITION) * val[3]';
 #[VAL05]
-val[5] = (1 - last) * val[4]';
+val[5] = (1 - LATCH_CONDITION) * val[4]';
 #[VAL06]
-val[6] = (1 - last) * val[5]';
+val[6] = (1 - LATCH_CONDITION) * val[5]';
 #[VAL07]
-val[7] = (1 - last) * val[6]';
+val[7] = (1 - LATCH_CONDITION) * val[6]';
 #[VAL8]
-val[8] = (1 - last) * val[7]';
+val[8] = (1 - LATCH_CONDITION) * val[7]';
 #[VAL09]
-val[9] = (1 - last) * val[8]';
+val[9] = (1 - LATCH_CONDITION) * val[8]';
 #[VAL10]
-val[10] = (1 - last) * val[9]';
+val[10] = (1 - LATCH_CONDITION) * val[9]';
 #[VAL11]
-val[11] = (1 - last) * val[10]';
+val[11] = (1 - LATCH_CONDITION) * val[10]';
 #[VAL12]
-val[12] = (1 - last) * val[11]';
+val[12] = (1 - LATCH_CONDITION) * val[11]';
 #[VAL13]
-val[13] = (1 - last) * val[12]';
+val[13] = (1 - LATCH_CONDITION) * val[12]';
 #[VAL14]
-val[14] = (1 - last) * val[13]';
+val[14] = (1 - LATCH_CONDITION) * val[13]';
 #[VAL15]
-val[15] = (1 - last) * val[14]';
+val[15] = (1 - LATCH_CONDITION) * val[14]';
 #[VAL16]
-val[16] = (1 - last) * val[15]';
+val[16] = (1 - LATCH_CONDITION) * val[15]';
 #[VAL17]
-val[17] = (1 - last) * val[16]';
+val[17] = (1 - LATCH_CONDITION) * val[16]';
 #[VAL18]
-val[18] = (1 - last) * val[17]';
+val[18] = (1 - LATCH_CONDITION) * val[17]';
 #[VAL19]
-val[19] = (1 - last) * val[18]';
+val[19] = (1 - LATCH_CONDITION) * val[18]';
 #[VAL20]
-val[20] = (1 - last) * val[19]';
+val[20] = (1 - LATCH_CONDITION) * val[19]';
 #[VAL21]
-val[21] = (1 - last) * val[20]';
+val[21] = (1 - LATCH_CONDITION) * val[20]';
 #[VAL22]
-val[22] = (1 - last) * val[21]';
+val[22] = (1 - LATCH_CONDITION) * val[21]';
 #[VAL23]
-val[23] = (1 - last) * val[22]';
+val[23] = (1 - LATCH_CONDITION) * val[22]';
 #[VAL24]
-val[24] = (1 - last) * val[23]';
+val[24] = (1 - LATCH_CONDITION) * val[23]';
 
 #[SLICE_TO_MEM]
 sel { clk, space_id, addr, val[0], tag, rw }
@@ -234,3 +248,22 @@ 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
+
+/* 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
+ *                          `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
+ *                          `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`.
+ *                          Namely, #[CTR_INIT] enforces `ctr == 1`.
+ */

barretenberg/cpp/pil/vm2/keccakf1600.pil

@@ -76,10 +76,13 @@ sel * (1 - sel) = 0;
 #[skippable_if]
 sel = 0;
 
+#[TRACE_CONTINUITY]
+(1 - precomputed.first_row) * (1 - sel) * sel' = 0;
+
 // error is defined below after round function
 pol commit sel_no_error; // @boolean (by definition)
 #[SEL_NO_ERROR]
-start * (sel_no_error - 1 + error) = 0;
+sel * (sel_no_error - 1 + error) = 0;
 
 // Round number which starts at 1 and ends at AVM_KECCAKF1600_NUM_ROUNDS (24).
 pol commit round;
@@ -96,21 +99,36 @@ start * (round - 1) = 0;
 pol commit round_inv;
 #[KECCAK_SEL_ROUND_NON_ZERO]
 round * ((1 - sel) * (1 - round_inv) + round_inv) - sel = 0;
-
-#[KECCAK_ROUND_INCREMENT]
-// Note: sel factor is required for an empty row to satisfy this relation
-sel * (1 - last) * (round' - round - 1) = 0;
+// This implies that `start == 1 ==> sel == 1`.
 
 // Selector for the last round of a keccak permutation
 // If no error is detected in row where `start == 1`, we have last == 1 <==> round == AVM_KECCAKF1600_NUM_ROUNDS (24)
-// Otherwise, `last` is unconstrained but witness generator will toggle it on the initial row.
 // This is achieved through #[SEL_SLICE_WRITE] and #[WRITE_TO_SLICE]. If there is no error,
 // the former guarantees that the write slice is active whenever `last == 1`. The latter guarantees
 // that `round` is equal to 24 (by fixing a constant 24 in the destination permutation tuple).
 pol commit last; // @boolean
 last * (1 - last) = 0;
 
-// TODO: We need this temporarily while we do not allow for constants in the lookup tuple
+// We enforce that `last == 1` whenever `error == 1`.
+// Note that error is constrained only on the start row.
+#[LAST_ON_ERROR]
+error * (last - 1) = 0;
+
+#[START_AFTER_LATCH]
+sel' * (start' - LATCH_CONDITION) = 0;
+
+#[LAST_HAS_SEL_ON]
+last * (1 - sel) = 0;
+
+// `sel == 0` on the first row because of shift relations and thus `last` is mutually
+// exclusive with `precomputed.first_row`.
+pol LATCH_CONDITION = last + precomputed.first_row;
+
+#[KECCAK_ROUND_INCREMENT]
+// Note: sel factor is required for an empty row to satisfy this relation
+sel * (1 - LATCH_CONDITION) * (round' - round - 1) = 0;
+
+// Lookup tuple constants: We need this temporarily while we do not allow for constants in the lookup tuple
 pol commit bitwise_xor_op_id;
 sel * (bitwise_xor_op_id - constants.AVM_BITWISE_XOR_OP_ID) = 0;
 pol commit bitwise_and_op_id;
@@ -1280,59 +1298,59 @@ bitwise.start_keccak { bitwise.op_id, bitwise.acc_ia, bitwise.acc_ib, bitwise.ac
 // the output state, otherwise we initialize the next state_in values for the next round.
 
 #[NEXT_STATE_IN_00]
-(1 - last) * (state_in_00' - state_iota_00) = 0;
+(1 - LATCH_CONDITION) * (state_in_00' - state_iota_00) = 0;
 #[NEXT_STATE_IN_01]
-(1 - last) * (state_in_01' - state_chi_01) = 0;
+(1 - LATCH_CONDITION) * (state_in_01' - state_chi_01) = 0;
 #[NEXT_STATE_IN_02]
-(1 - last) * (state_in_02' - state_chi_02) = 0;
+(1 - LATCH_CONDITION) * (state_in_02' - state_chi_02) = 0;
 #[NEXT_STATE_IN_03]
-(1 - last) * (state_in_03' - state_chi_03) = 0;
+(1 - LATCH_CONDITION) * (state_in_03' - state_chi_03) = 0;
 #[NEXT_STATE_IN_04]
-(1 - last) * (state_in_04' - state_chi_04) = 0;
+(1 - LATCH_CONDITION) * (state_in_04' - state_chi_04) = 0;
 
 #[NEXT_STATE_IN_10]
-(1 - last) * (state_in_10' - state_chi_10) = 0;
+(1 - LATCH_CONDITION) * (state_in_10' - state_chi_10) = 0;
 #[NEXT_STATE_IN_11]
-(1 - last) * (state_in_11' - state_chi_11) = 0;
+(1 - LATCH_CONDITION) * (state_in_11' - state_chi_11) = 0;
 #[NEXT_STATE_IN_12]
-(1 - last) * (state_in_12' - state_chi_12) = 0;
+(1 - LATCH_CONDITION) * (state_in_12' - state_chi_12) = 0;
 #[NEXT_STATE_IN_13]
-(1 - last) * (state_in_13' - state_chi_13) = 0;
+(1 - LATCH_CONDITION) * (state_in_13' - state_chi_13) = 0;
 #[NEXT_STATE_IN_14]
-(1 - last) * (state_in_14' - state_chi_14) = 0;
+(1 - LATCH_CONDITION) * (state_in_14' - state_chi_14) = 0;
 
 #[NEXT_STATE_IN_20]
-(1 - last) * (state_in_20' - state_chi_20) = 0;
+(1 - LATCH_CONDITION) * (state_in_20' - state_chi_20) = 0;
 #[NEXT_STATE_IN_21]
-(1 - last) * (state_in_21' - state_chi_21) = 0;
+(1 - LATCH_CONDITION) * (state_in_21' - state_chi_21) = 0;
 #[NEXT_STATE_IN_22]
-(1 - last) * (state_in_22' - state_chi_22) = 0;
+(1 - LATCH_CONDITION) * (state_in_22' - state_chi_22) = 0;
 #[NEXT_STATE_IN_23]
-(1 - last) * (state_in_23' - state_chi_23) = 0;
+(1 - LATCH_CONDITION) * (state_in_23' - state_chi_23) = 0;
 #[NEXT_STATE_IN_24]
-(1 - last) * (state_in_24' - state_chi_24) = 0;
+(1 - LATCH_CONDITION) * (state_in_24' - state_chi_24) = 0;
 
 #[NEXT_STATE_IN_30]
-(1 - last) * (state_in_30' - state_chi_30) = 0;
+(1 - LATCH_CONDITION) * (state_in_30' - state_chi_30) = 0;
 #[NEXT_STATE_IN_31]
-(1 - last) * (state_in_31' - state_chi_31) = 0;
+(1 - LATCH_CONDITION) * (state_in_31' - state_chi_31) = 0;
 #[NEXT_STATE_IN_32]
-(1 - last) * (state_in_32' - state_chi_32) = 0;
+(1 - LATCH_CONDITION) * (state_in_32' - state_chi_32) = 0;
 #[NEXT_STATE_IN_33]
-(1 - last) * (state_in_33' - state_chi_33) = 0;
+(1 - LATCH_CONDITION) * (state_in_33' - state_chi_33) = 0;
 #[NEXT_STATE_IN_34]
-(1 - last) * (state_in_34' - state_chi_34) = 0;
+(1 - LATCH_CONDITION) * (state_in_34' - state_chi_34) = 0;
 
 #[NEXT_STATE_IN_40]
-(1 - last) * (state_in_40' - state_chi_40) = 0;
+(1 - LATCH_CONDITION) * (state_in_40' - state_chi_40) = 0;
 #[NEXT_STATE_IN_41]
-(1 - last) * (state_in_41' - state_chi_41) = 0;
+(1 - LATCH_CONDITION) * (state_in_41' - state_chi_41) = 0;
 #[NEXT_STATE_IN_42]
-(1 - last) * (state_in_42' - state_chi_42) = 0;
+(1 - LATCH_CONDITION) * (state_in_42' - state_chi_42) = 0;
 #[NEXT_STATE_IN_43]
-(1 - last) * (state_in_43' - state_chi_43) = 0;
+(1 - LATCH_CONDITION) * (state_in_43' - state_chi_43) = 0;
 #[NEXT_STATE_IN_44]
-(1 - last) * (state_in_44' - state_chi_44) = 0;
+(1 - LATCH_CONDITION) * (state_in_44' - state_chi_44) = 0;
 
 //#############################################################################
 //                  Read-Write to memory slice and error handling
@@ -1373,16 +1391,16 @@ start { dst_addr, highest_slice_address, dst_out_of_range_error } in gt.sel_othe
 error = 1 - (1 - src_out_of_range_error) * (1 - dst_out_of_range_error) * (1 - tag_error);
 
 #[DST_ADDR_PROPAGATION]
-(1 - last) * (dst_addr' - dst_addr) = 0;
+(1 - LATCH_CONDITION) * (dst_addr' - dst_addr) = 0;
 #[CLK_PROPAGATION]
-(1 - last) * (clk' - clk) = 0;
+(1 - LATCH_CONDITION) * (clk' - clk) = 0;
 #[SPACE_ID_PROPAGATION]
-(1 - last) * (space_id' - space_id) = 0;
+(1 - LATCH_CONDITION) * (space_id' - space_id) = 0;
 
 // It is crucial to propagate sel_no_error to the bottom (last == 1) as to properly
 // activate the slice write lookup (see below).
 #[SEL_NO_ERROR_PROPAGATION]
-(1 - last) * (sel_no_error' - sel_no_error) = 0;
+(1 - LATCH_CONDITION) * (sel_no_error' - sel_no_error) = 0;
 
 // Note that we do not propagate src_out_of_range_error, dst_out_of_range_error, tag_error, error
 // as they are not affecting constraints in the other rows. Error propagation to the caller
@@ -1399,6 +1417,23 @@ sel_slice_read = start * (1 - src_out_of_range_error) * (1 - dst_out_of_range_er
 #[SEL_SLICE_WRITE]
 sel_slice_write = sel_no_error * last;
 
+// Prevention of illegitimate writes to memory:
+// sel_slice_write == 1 ==> round == 24 (by #[WRITE_TO_SLICE])
+// From #[KECCAK_SEL_ROUND_NON_ZERO], we have `sel == 1`.
+// Since `last` is a boolean and `sel_no_error` is boolean on an active row,
+// `last == 1` and `sel_no_error == 1`.
+// This row must have `start == 0` because otherwise `round` would be equal to 1 instead of 24.
+// As a consequence, the previous row must have `LATCH_CONDITION == 0` by #[START_AFTER_LATCH]
+// which enforces a bottom-up propagation of `sel_no_error` and a decreasing counter for `round`
+// by #[SEL_NO_ERROR_PROPAGATION] and #[KECCAK_ROUND_INCREMENT]. When the propagation reaches
+// `round == 1`, we have `sel == 1` (#[KECCAK_SEL_ROUND_NON_ZERO]) two possible cases:
+// 1) The row above is `precomputed.first_row == 1` which implies that `start == 1`.
+// 2) Otherwise, by #[TRACE_CONTINUITY], the above row must be active (sel == 1)
+//    and we cannot decrement `round` anymore (would be zero which contradicts #[KECCAK_SEL_ROUND_NON_ZERO]).
+//    As a consequence, the above row must have `last == LATCH_CONDITION == 1` which implies that `start == 1`.
+// This shows that any "slice write to memory" operation was triggered by a legitimate keccak permutation
+// because `start` is the destination selector for the keccak permutation.
+
 #[READ_TO_SLICE]
 // Standard Keccak layout: memory[(y * 5) + x] = A[x][y]
 // State columns ordered in column-major order (by x coordinate first, then y)
@@ -1429,7 +1464,7 @@ sel_slice_write { state_iota_00, state_chi_10, state_chi_20, state_chi_30, state
                   state_chi_03,  state_chi_13, state_chi_23, state_chi_33, state_chi_43,
                   state_chi_04,  state_chi_14, state_chi_24, state_chi_34, state_chi_44,
                   clk, dst_addr, space_id, round }
-is
+is // Crucial to be a permutation to prevent any illegal write to memory in keccak_memory.pil.
 keccak_memory.start_write { keccak_memory.val[0], keccak_memory.val[1], keccak_memory.val[2], keccak_memory.val[3], keccak_memory.val[4],
                             keccak_memory.val[5], keccak_memory.val[6], keccak_memory.val[7], keccak_memory.val[8], keccak_memory.val[9],
                             keccak_memory.val[10], keccak_memory.val[11], keccak_memory.val[12], keccak_memory.val[13], keccak_memory.val[14],

barretenberg/cpp/pil/vm2/memory.pil

@@ -174,7 +174,7 @@ sel = // Addressing.
 // Other boolean constraints.
 sel * (1 - sel) = 0; // Ensure mutual exclusivity of the permutation selectors.
 last_access * (1 - last_access) = 0;
-rw * (1 - rw) = 0; // TODO: should already be constrained by each source of interaction lookups.
+rw * (1 - rw) = 0; // Some source sub-trace relies on this constraint (e.g., keccak_memory.pil)
 sel_tag_is_ff * (1 - sel_tag_is_ff) = 0;
 
 // Trace must be contiguous.

barretenberg/cpp/pil/vm2/poseidon2_mem.pil

@@ -168,7 +168,6 @@ namespace poseidon2_perm_mem;
     ////////////////////////////////////////////////
     // Write output to memory
     ////////////////////////////////////////////////
-    // TODO: These need to be changed to permutations once we have the custom permutation selectors
     #[POS_WRITE_MEM_0]
     sel_should_exec {
         execution_clk,                   space_id,