feat(avm)!: memory multi permutations (#16586)

# Multi permutation builder (tracegen)

This component solves the following problem. Suppose you have `n`
permutations (P1, ..., Pn) such that
* The destination tuple columns (and therefore table) are the same for
all of them (e.g., mem.address, mem.value).
* There is a "global" destination table selector (mem.sel)
* The source selectors are (potentially) different, and **already set**
(e.g., execution.sel_addressing_base,
execution.sel_addressing_indirect_0..., sha256.mem_op_1...)
* The destination selectors are different, but UNSET. E.g.,
mem.sel_addressing_base, mem.sel_addressing_indirect_0...)

You want to find, for each source row of each permutation, a row in the
destination table and set the right destination selector. For the next
source row or permutation, you should not be able to consider the
"already used" destination rows, because this is a permutation.

## Solution

The multipermutation builder is templated over a list of permutation
settings. It builds an index of the destination table, and basically
applies the algorithm mentioned above.

## Example in this PR

For this PR, I made the required changes for Addressing, Keccak(mem) and
Sha256. Note, especially for sha, that we didn't need separate SOURCE
selectors because these are separate permutation instances.

## Downside

All of this gets currently done in one thread, and is also centralized
in the memory trace builder (as opposed to the sources). This might be
possible to change later.

Author: fcarreiro

barretenberg/cpp/pil/vm2/execution/addressing.pil

@@ -128,11 +128,9 @@ pol NUM_RELATIVE_E = 1 - sel_do_base_check;
 #[NUM_RELATIVE_INV_CHECK]
 NUM_RELATIVE_X * (NUM_RELATIVE_E * (1 - NUM_RELATIVE_Y) + NUM_RELATIVE_Y) - 1 + NUM_RELATIVE_E = 0;
 
-// FIXME: this should eventually be a permutation.
 #[BASE_ADDRESS_FROM_MEMORY]
 sel_do_base_check { precomputed.clk, context_id, /*address=*/precomputed.zero, /*value=*/base_address_val, /*tag=*/base_address_tag, /*rw=*/precomputed.zero/*(read)*/ }
-in
-memory.sel { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
+is memory.sel_addressing_base { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
 
 // This error will be true iff the base address is not valid AND we did actually check it.
 pol commit sel_base_address_failure;
@@ -259,30 +257,28 @@ sel_should_apply_indirection[6] = SEL_OP_IS_INDIRECT_EFFECTIVE_6_ * (1 - sel_rel
 pol commit rop_tag[7];
 
 // If indirection is applied, we need to lookup the value from memory.
-// If sel_should_apply_indirection is 1, then we know the address is valid therefore we can make the lookups.
-// TODO: complete these lookups once we get memory done. In particular, clk and space id.
-// FIXME: these should eventually be permutations.
+// If sel_should_apply_indirection is 1, then we know the address is valid therefore we can make the permutations.
 #[INDIRECT_FROM_MEMORY_0]
 sel_should_apply_indirection[0] { precomputed.clk, context_id, /*address=*/op_after_relative[0], /*value=*/rop[0], /*tag=*/rop_tag[0], /*rw=*/precomputed.zero/*(read)*/ }
-in memory.sel { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
+is memory.sel_addressing_indirect[0] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
 #[INDIRECT_FROM_MEMORY_1]
 sel_should_apply_indirection[1] { precomputed.clk, context_id, /*address=*/op_after_relative[1], /*value=*/rop[1], /*tag=*/rop_tag[1], /*rw=*/precomputed.zero/*(read)*/ }
-in memory.sel { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
+is memory.sel_addressing_indirect[1] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
 #[INDIRECT_FROM_MEMORY_2]
 sel_should_apply_indirection[2] { precomputed.clk, context_id, /*address=*/op_after_relative[2], /*value=*/rop[2], /*tag=*/rop_tag[2], /*rw=*/precomputed.zero/*(read)*/ }
-in memory.sel { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
+is memory.sel_addressing_indirect[2] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
 #[INDIRECT_FROM_MEMORY_3]
 sel_should_apply_indirection[3] { precomputed.clk, context_id, /*address=*/op_after_relative[3], /*value=*/rop[3], /*tag=*/rop_tag[3], /*rw=*/precomputed.zero/*(read)*/ }
-in memory.sel { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
+is memory.sel_addressing_indirect[3] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
 #[INDIRECT_FROM_MEMORY_4]
 sel_should_apply_indirection[4] { precomputed.clk, context_id, /*address=*/op_after_relative[4], /*value=*/rop[4], /*tag=*/rop_tag[4], /*rw=*/precomputed.zero/*(read)*/ }
-in memory.sel { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
+is memory.sel_addressing_indirect[4] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
 #[INDIRECT_FROM_MEMORY_5]
 sel_should_apply_indirection[5] { precomputed.clk, context_id, /*address=*/op_after_relative[5], /*value=*/rop[5], /*tag=*/rop_tag[5], /*rw=*/precomputed.zero/*(read)*/ }
-in memory.sel { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
+is memory.sel_addressing_indirect[5] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
 #[INDIRECT_FROM_MEMORY_6]
 sel_should_apply_indirection[6] { precomputed.clk, context_id, /*address=*/op_after_relative[6], /*value=*/rop[6], /*tag=*/rop_tag[6], /*rw=*/precomputed.zero/*(read)*/ }
-in memory.sel { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
+is memory.sel_addressing_indirect[6] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
 
 // Otherwise, if indirection is not applied , we propagate the operands from the previous step.
 #[INDIRECT_PROPAGATION_0]

barretenberg/cpp/pil/vm2/keccak_memory.pil

@@ -237,13 +237,9 @@ val43 = (1 - last) * val42';
 #[VAL44]
 val44 = (1 - last) * val43';
 
-// Memory permutation
-// TODO: Proper memory permutation (not a lookup), and introduce a specific
-// selector for keccak in memory sub-trace.
 #[SLICE_TO_MEM]
-sel {clk, addr, val00, tag, rw, space_id}
-in // TODO: replace with `is` (permutation)
-memory.sel { memory.clk, memory.address, memory.value, memory.tag, memory.rw, memory.space_id };
+sel { clk, space_id, addr, val00, tag, rw }
+is memory.sel_keccak { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
 
 // Used to constrain the number of rounds in keccakf1600.pil through the slice_write lookup.
 pol commit num_rounds;

barretenberg/cpp/pil/vm2/memory.pil

@@ -10,6 +10,49 @@ pol commit tag;
 pol commit rw;
 pol commit space_id;
 
+// Permutation selectors (addressing.pil).
+pol commit sel_addressing_base;
+pol commit sel_addressing_indirect[7];
+sel_addressing_base * (1 - sel_addressing_base) = 0;
+sel_addressing_indirect[0] * (1 - sel_addressing_indirect[0]) = 0;
+sel_addressing_indirect[1] * (1 - sel_addressing_indirect[1]) = 0;
+sel_addressing_indirect[2] * (1 - sel_addressing_indirect[2]) = 0;
+sel_addressing_indirect[3] * (1 - sel_addressing_indirect[3]) = 0;
+sel_addressing_indirect[4] * (1 - sel_addressing_indirect[4]) = 0;
+sel_addressing_indirect[5] * (1 - sel_addressing_indirect[5]) = 0;
+sel_addressing_indirect[6] * (1 - sel_addressing_indirect[6]) = 0;
+
+// Permutation selectors (keccak_memory.pil).
+pol commit sel_keccak;
+sel_keccak * (1 - sel_keccak) = 0;
+
+// Permutation selectors (sha256_mem.pil).
+pol commit sel_sha256_read;
+pol commit sel_sha256_op[8];
+sel_sha256_read * (1 - sel_sha256_read) = 0;
+sel_sha256_op[0] * (1 - sel_sha256_op[0]) = 0;
+sel_sha256_op[1] * (1 - sel_sha256_op[1]) = 0;
+sel_sha256_op[2] * (1 - sel_sha256_op[2]) = 0;
+sel_sha256_op[3] * (1 - sel_sha256_op[3]) = 0;
+sel_sha256_op[4] * (1 - sel_sha256_op[4]) = 0;
+sel_sha256_op[5] * (1 - sel_sha256_op[5]) = 0;
+sel_sha256_op[6] * (1 - sel_sha256_op[6]) = 0;
+sel_sha256_op[7] * (1 - sel_sha256_op[7]) = 0;
+
+// Permutation consistency.
+/*
+sel = // Addressing.
+      sel_addressing_base
+    + sel_addressing_indirect[0] + sel_addressing_indirect[1] + sel_addressing_indirect[2] + sel_addressing_indirect[3]
+    + sel_addressing_indirect[4] + sel_addressing_indirect[5] + sel_addressing_indirect[6]
+    // Keccak.
+    + sel_keccak
+    // Sha256.
+    + sel_sha256_read
+    + sel_sha256_op[0] + sel_sha256_op[1] + sel_sha256_op[2] + sel_sha256_op[3]
+    + sel_sha256_op[4] + sel_sha256_op[5] + sel_sha256_op[6] + sel_sha256_op[7];
+*/
+
 #[skippable_if]
 sel = 0;
 

barretenberg/cpp/pil/vm2/sha256_mem.pil

@@ -15,12 +15,12 @@ include "execution.pil";
  * sha256.start { sha256.execution_clk, sha256.space_id, sha256.output_addr, sha256.state_addr, sha256.input_addr, sha256.err };
  *
  * This trace reads and writes the following:
- * (1) Read State: From { state_addr, state_addr + 1, ..., state_addr + 7 } 
+ * (1) Read State: From { state_addr, state_addr + 1, ..., state_addr + 7 }
  * (2) Read Input: From { input_addr, input_addr + 1, ..., input_addr + 15 }
  * (3) Write Output: From { output_addr, output_addr + 1, ..., output_addr + 7 }
  * All values operated on in this subtrace are validated to be U32.
  * This subtrace has a mix of a vertical and horizontal memory accesses.
- * The State and Outputs are written horizontally (i.e. there are 8 columns), this means that 
+ * The State and Outputs are written horizontally (i.e. there are 8 columns), this means that
  * they are loaded in "parallel" and therefore they form their own temporality groups (for the purpose of any errors)
  * The Input is "mixed" into the hash at each round (from round 1 to 16), this means the inputs are loaded in a single column and the i-th input
  * is loaded in the i-th row of computation. Therefore, a single load is a temporality group (for the purpose of errors).
@@ -90,7 +90,7 @@ include "execution.pil";
  */
 
 namespace sha256;
-    
+
     pol commit sel;
     sel * (1 - sel) = 0;
 
@@ -117,7 +117,7 @@ namespace sha256;
     #[LATCH_HAS_SEL_ON] // sel = 1 when latch = 1, sel = 0 at first row because of shift relations
     latch * (1 - sel) = 0;
     // This is now guaranteed to be mututally exclusive because of the above condition and since sel = 0 at row = 0 (since it has shifts)
-    pol LATCH_CONDITION = latch + precomputed.first_row; 
+    pol LATCH_CONDITION = latch + precomputed.first_row;
 
     #[START_AFTER_LAST]
     sel' * (start' - LATCH_CONDITION) = 0;
@@ -177,7 +177,7 @@ namespace sha256;
     // Memory Operations: State and Output
     ////////////////////////////////////////////////////////
     // Since reading the hash state and writing the hash outputs have similar "shapes" (i.e. 8 columns)
-    // and occur at different "times" (the start and end (latch) respectively), we define a set of 
+    // and occur at different "times" (the start and end (latch) respectively), we define a set of
     // shared columns that we can re-use between the two. This saves us ~24 columns and 8 permutations.
 
     pol commit memory_address[8]; // Addresses to read from or write to
@@ -230,101 +230,100 @@ namespace sha256;
     // flag that accounts for this
     pol commit rw;
     rw = OUTPUT_WRITE_CONDITION;
-    // TODO: These need to be changed to permutations once we have the custom permutation selectors impl
     #[MEM_OP_0]
-    sel_mem_state_or_output { 
-        execution_clk,       memory_address[0],
-        memory_register[0],  memory_tag[0],
-        space_id,            /*rw=*/ rw
-    } in
-    memory.sel { 
-        memory.clk,      memory.address,
-        memory.value,    memory.tag,
-        memory.space_id, memory.rw
+    sel_mem_state_or_output {
+        execution_clk,       space_id,
+        memory_address[0],   memory_register[0],
+        memory_tag[0],       /*rw=*/ rw
+    } is
+    memory.sel_sha256_op[0] {
+        memory.clk,      memory.space_id,
+        memory.address,  memory.value,
+        memory.tag,      memory.rw
     };
 
     #[MEM_OP_1]
-    sel_mem_state_or_output { 
-        execution_clk,       memory_address[1],
-        memory_register[1],  memory_tag[1],
-        space_id,            /*rw=*/ rw
-    } in
-    memory.sel { 
-        memory.clk,      memory.address,
-        memory.value,    memory.tag,
-        memory.space_id, memory.rw
+    sel_mem_state_or_output {
+        execution_clk,       space_id,
+        memory_address[1],   memory_register[1],
+        memory_tag[1],       /*rw=*/ rw
+    } is
+    memory.sel_sha256_op[1] {
+        memory.clk,      memory.space_id,
+        memory.address,  memory.value,
+        memory.tag,      memory.rw
     };
 
     #[MEM_OP_2]
-    sel_mem_state_or_output { 
-        execution_clk,       memory_address[2],
-        memory_register[2],  memory_tag[2],
-        space_id,            /*rw=*/ rw
-    } in
-    memory.sel { 
-        memory.clk,      memory.address,
-        memory.value,    memory.tag,
-        memory.space_id, memory.rw
+    sel_mem_state_or_output {
+        execution_clk,       space_id,
+        memory_address[2],   memory_register[2],
+        memory_tag[2],       /*rw=*/ rw
+    } is
+    memory.sel_sha256_op[2] {
+        memory.clk,      memory.space_id,
+        memory.address,  memory.value,
+        memory.tag,      memory.rw
     };
 
     #[MEM_OP_3]
-    sel_mem_state_or_output { 
-        execution_clk,       memory_address[3],
-        memory_register[3],  memory_tag[3],
-        space_id,            /*rw=*/ rw
-    } in
-    memory.sel { 
-        memory.clk,      memory.address,
-        memory.value,    memory.tag,
-        memory.space_id, memory.rw
+    sel_mem_state_or_output {
+        execution_clk,       space_id,
+        memory_address[3],   memory_register[3],
+        memory_tag[3],       /*rw=*/ rw
+    } is
+    memory.sel_sha256_op[3] {
+        memory.clk,      memory.space_id,
+        memory.address,  memory.value,
+        memory.tag,      memory.rw
     };
 
     #[MEM_OP_4]
-    sel_mem_state_or_output { 
-        execution_clk,       memory_address[4],
-        memory_register[4],  memory_tag[4],
-        space_id,            /*rw=*/ rw
-    } in
-    memory.sel { 
-        memory.clk,      memory.address,
-        memory.value,    memory.tag,
-        memory.space_id, memory.rw
+    sel_mem_state_or_output {
+        execution_clk,       space_id,
+        memory_address[4],   memory_register[4],
+        memory_tag[4],       /*rw=*/ rw
+    } is
+    memory.sel_sha256_op[4] {
+        memory.clk,      memory.space_id,
+        memory.address,  memory.value,
+        memory.tag,      memory.rw
     };
 
     #[MEM_OP_5]
-    sel_mem_state_or_output { 
-        execution_clk,       memory_address[5],
-        memory_register[5],  memory_tag[5],
-        space_id,            /*rw=*/ rw
-    } in
-    memory.sel { 
-        memory.clk,      memory.address,
-        memory.value,    memory.tag,
-        memory.space_id, memory.rw
+    sel_mem_state_or_output {
+        execution_clk,       space_id,
+        memory_address[5],   memory_register[5],
+        memory_tag[5],       /*rw=*/ rw
+    } is
+    memory.sel_sha256_op[5] {
+        memory.clk,      memory.space_id,
+        memory.address,  memory.value,
+        memory.tag,      memory.rw
     };
 
     #[MEM_OP_6]
-    sel_mem_state_or_output { 
-        execution_clk,       memory_address[6],
-        memory_register[6],  memory_tag[6],
-        space_id,            /*rw=*/ rw
-    } in
-    memory.sel { 
-        memory.clk,      memory.address,
-        memory.value,    memory.tag,
-        memory.space_id, memory.rw
+    sel_mem_state_or_output {
+        execution_clk,       space_id,
+        memory_address[6],   memory_register[6],
+        memory_tag[6],       /*rw=*/ rw
+    } is
+    memory.sel_sha256_op[6] {
+        memory.clk,      memory.space_id,
+        memory.address,  memory.value,
+        memory.tag,      memory.rw
     };
 
     #[MEM_OP_7]
-    sel_mem_state_or_output { 
-        execution_clk,       memory_address[7],
-        memory_register[7],  memory_tag[7],
-        space_id,            /*rw=*/ rw
-    } in
-    memory.sel { 
-        memory.clk,      memory.address,
-        memory.value,    memory.tag,
-        memory.space_id, memory.rw
+    sel_mem_state_or_output {
+        execution_clk,       space_id,
+        memory_address[7],   memory_register[7],
+        memory_tag[7],       /*rw=*/ rw
+    } is
+    memory.sel_sha256_op[7] {
+        memory.clk,      memory.space_id,
+        memory.address,  memory.value,
+        memory.tag,      memory.rw
     };
 
     ////////////////////////////////////////////////
@@ -345,7 +344,7 @@ namespace sha256;
     pol BATCHED_TAG_CHECK = 2**0 * STATE_TAG_DIFF_0 + 2**3 * STATE_TAG_DIFF_1
                           + 2**6 * STATE_TAG_DIFF_2 + 2**9 * STATE_TAG_DIFF_3
                           + 2**12 * STATE_TAG_DIFF_4 + 2**15 * STATE_TAG_DIFF_5
-                          + 2**18 * STATE_TAG_DIFF_6 + 2**21 * STATE_TAG_DIFF_7; 
+                          + 2**18 * STATE_TAG_DIFF_6 + 2**21 * STATE_TAG_DIFF_7;
 
     pol commit batch_tag_inv;
     #[BATCH_ZERO_CHECK_READ]
@@ -385,7 +384,7 @@ namespace sha256;
     sel * (1 - LATCH_CONDITION) * (input_rounds_rem' - (input_rounds_rem - sel_is_input_round)) = 0;
 
     // Read input if we have not had an error from the previous temporality groups and this is an input round
-    pol commit sel_read_input_from_memory; 
+    pol commit sel_read_input_from_memory;
     sel_read_input_from_memory = sel * (1 - mem_out_of_range_err) * sel_is_input_round * (1 - sel_invalid_state_tag_err);
 
     // Put the result of the input loads in to the corresponding w value
@@ -396,15 +395,15 @@ namespace sha256;
     pol commit input_tag;
 
     #[MEM_INPUT_READ]
-    sel_read_input_from_memory { 
-        execution_clk,       input_addr,
-        input,               input_tag,
-        space_id,            /*rw=*/ precomputed.zero
-    } in
-    memory.sel { 
-        memory.clk,      memory.address,
-        memory.value,    memory.tag,
-        memory.space_id, memory.rw
+    sel_read_input_from_memory {
+        execution_clk,       space_id,
+        input_addr,          input,
+        input_tag,           /*rw=*/ precomputed.zero
+    } is
+    memory.sel_sha256_read {
+        memory.clk,      memory.space_id,
+        memory.address,  memory.value,
+        memory.tag,      memory.rw
     };
 
     ////////////////////////////////////////////////
@@ -418,7 +417,7 @@ namespace sha256;
     pol commit sel_invalid_input_row_tag_err;
     sel_invalid_input_row_tag_err * (1 - sel_invalid_input_row_tag_err) = 0;
 
-    pol INPUT_TAG_DIFF = sel_read_input_from_memory * (input_tag - constants.MEM_TAG_U32); 
+    pol INPUT_TAG_DIFF = sel_read_input_from_memory * (input_tag - constants.MEM_TAG_U32);
     pol commit input_tag_diff_inv;
     // Iff INPUT_TAG_DIFF != 0, sel_invalid_input_row_tag_err = 1
     #[INPUT_TAG_DIFF_CHECK]