feat: merge-train/avm (#17862)

BEGIN_COMMIT_OVERRIDE
fix(avm)!: Append-only tree reads (#17757)
chore: avm TS tests should only ever create a single world state
instance (#17703)
feat!: merkle check pre-audit (#17771)
feat: AVM simulate via NAPI with hinted DBs (#17704)
feat(avm): simulate with ws (#17635)
chore: static batch inverses (#17899)
END_COMMIT_OVERRIDE

Author: jeanmon

barretenberg/cpp/pil/vm2/poseidon2_hash.pil

@@ -18,6 +18,13 @@ namespace poseidon2_hash;
     #[skippable_if]
     sel = 0;
 
+    // If the current row is not active, then there are no more active rows after that.
+    // Note that sel cannot be activated in the first row as sel' is defined.
+    // As a consequence, if a row is activated (sel == 1) somewhere in this sub-trace, then
+    // the activated rows start from the second row and are contiguous.
+    #[TRACE_CONTINUITY]
+    (1 - precomputed.first_row) * (1 - sel) * sel' = 0;
+
     // === Input Values ===
     // Unpadded Length of the inputs to be hashed
     pol commit input_len;
@@ -46,8 +53,11 @@ namespace poseidon2_hash;
     // The last row of hashing for the given input
     pol commit end;
     end * (1 - end) = 0;
-    // End and first row are NAND - they cannot both be one.
-    end * precomputed.first_row = 0;
+
+    // Selector must be 1 in end row
+    #[SELECTOR_ON_END]
+    end * (1 - sel) = 0;
+
     // Our latch condition can either be the designated end of the computation or the first row
     // The previous relation ensures they cannot both be 1
     pol LATCH_CONDITION = end + precomputed.first_row;

barretenberg/cpp/pil/vm2/trees/merkle_check.pil

@@ -3,20 +3,43 @@ include "../precomputed.pil";
 
 /**
  * A gadget that checks a merkle read or a write.
- * One sibling node is processed per row, performing 1 hash if it's a merkle read
- * or 2 hashes if it's a merkle write.
+ * A merkle read consists in proving membership of a leaf (`read_leaf`) in a Merkle tree (against a given root).
+ * For a merkle write, we additionally compute the new root of the tree with the new leaf (`updated_leaf`)
+ * value. The sibling path is the same for both reads and writes and therefore the membership check and
+ * the new root computation can be processed in "parallel".
+ * One sibling node is processed per row, performing 1 hash (Poseidon2) if it is a merkle read
+ * or 2 hashes if it is a merkle write.
  *
  * WARNING: This gadget will break if used with `tree_height >= 254`
  *
+ * Precondition: tree_height/path_len < 254
+ *
+ * Errors: None
+ *
+ * Number of rows per computation: tree_height/path_len
+ *
  * Read usage:
- *     caller_sel { read_leaf, leaf_index, tree_height, expected_root }
- *     in merkle_check.start { merkle_check.read_node, merkle_check.index, merkle_check.path_len, merkle_check.read_root }
+ *     caller_sel {
+ *         read_leaf, leaf_index, tree_height, expected_root
+ *     } in merkle_check.start {
+ *         merkle_check.read_node, merkle_check.index, merkle_check.path_len, merkle_check.read_root
+ *     };
  *
  * Write usage:
- *     caller_sel { one, prev_leaf_value, next_leaf_value,
- *         leaf_index, tree_height, prev_root, next_root }
- *     in merkle_check.start { merkle_check.write, merkle_check.read_node, merkle_check.write_node,
- *         merkle_check.index, merkle_check.path_len, merkle_check.read_root, merkle_check.write_root }
+ *     caller_sel {
+ *         one, current_leaf, updated_leaf,
+ *         leaf_index, tree_height, prev_root, next_root
+ * } in merkle_check.start {
+ *         merkle_check.write, merkle_check.read_node, merkle_check.write_node,
+ *         merkle_check.index, merkle_check.path_len, merkle_check.read_root, merkle_check.write_root
+ *     };
+ *
+ * Read/Write flexible usage: One can call the write usage variant with a boolean in the first column
+ * to toggle between read and write. However, the caller needs to ensure that trace generation will
+ * set `updated_leaf` and `next_root` to 0 when `write` is 0.
+ *
+ * USAGE WARNING: Never invoke this gadget using `merkle_check.write` as destination selector. This would be
+ *                completely under-constrained as we do not enforce `sel == 1` when `write == 1`.
  *
  * Common inputs
  * @column read_node The value of the node being read. When `start == 1`, this is the leaf.
@@ -27,7 +50,10 @@ include "../precomputed.pil";
  * Write specific inputs
  * @column write Whether this is a write operation.
  * @column write_node The value of the node being written. When `start == 1`, this is the new leaf.
- * @column write_root The merkle root that results of replacing the leaf with the new leaf at the index provided in the read_root. This will be propagated down to be matched internally on `end`.
+ *
+ * Write specific output
+ * @column write_root The merkle root that results of replacing the leaf with the new leaf at the index provided
+ *                    in the read_root. This will be propagated down to be matched internally on `end`.
  *
  * Internals/hints
  * @column sibling The value of the sibling node to be hashed with `read_node`.
@@ -49,110 +75,121 @@ include "../precomputed.pil";
  * +-----------+-------+----------+---------+---------------+----------------+-----------------+------------------+-----------+-------+------------+-----------------+------------------+-------------------+------------+-------+-----+-----+
  */
 namespace merkle_check;
-    pol commit sel;
-    sel * (1 - sel) = 0;
-    // No relations will be checked if this identity is satisfied.
-    #[skippable_if]
+   #[skippable_if]
     sel = 0;
 
-    // If the current row is not active, then there are no more active rows after that.
-    // Note that sel cannot be activated in the first row as sel' is defined.
-    // As a consequence, if a row is activated (sel == 1) somewhere in this sub-trace, then
-    // the activated rows start from the second row and are contiguous.
-    #[TRACE_CONTINUITY]
-    (1 - precomputed.first_row) * (1 - sel) * sel' = 0;
+    pol commit sel; // @boolean
+    sel * (1 - sel) = 0;
 
     // Common inputs - These must be looked up both on read and write
     pol commit read_node;
     pol commit index;
     pol commit path_len;
     pol commit read_root;
 
-    // Write specific inputs - These are only looked up when we want to update the root
-    pol commit write;
-    write * (1 - write) = 0; // bool
+    // Write specific inputs/outputs - These are only looked up when we want to update the root
+    pol commit write; // This should be a boolean passed by the caller. For a read usage, it is under-constrained but read
+                      // relevant values are constrained. For write, the caller must pass 1.
     pol commit write_node;
     pol commit write_root;
 
     // Hints
     pol commit sibling;
 
     // Boundaries
-    pol commit start;
-    pol commit end;
-    pol NOT_END = sel * (1 - end);
-    start * (1 - start) = 0; // bool
-    end * (1 - end) = 0; // bool
-
-    // only one of end or first_row can be 1
-    // end can't be 1 for first row
-    end * precomputed.first_row = 0;
-    // LATCH_CONDITION is true if either end is 1 or first_row is 1
-    pol LATCH_CONDITION = end + precomputed.first_row;
-
-    #[START_AFTER_LATCH]
-    sel' * (start' - LATCH_CONDITION) = 0;
+    pol commit start; // @boolean
+    pol commit end; // @boolean
+    start * (1 - start) = 0;
+    end * (1 - end) = 0;
 
-    // Selector must be 1 in end row
-    #[SELECTOR_ON_END]
-    end * (1 - sel) = 0;
+    // End when remaining path reaches 1. In other words, (path_len == 1) <==> (end == 1)
+    pol PATH_LEN_MIN_ONE = path_len - 1;
+    pol commit path_len_min_one_inv;
+    #[END_IFF_REM_PATH_EMPTY]
+    sel * (PATH_LEN_MIN_ONE * (end * (1 - path_len_min_one_inv) + path_len_min_one_inv) - 1 + end) = 0;
+
+    // This prevents a computation to be stopped prematurely, i.e., truncating last rows before
+    // we reach a row where end == 1. Note that #[END_IFF_REM_PATH_EMPTY] is conditioned on `sel == 1`
+    // and a malicious prover could prematurely stop by setting `sel == 0` and `end == 0`.
+    #[COMPUTATION_FINISH_AT_END]
+    sel * (1 - sel') * (1 - end) = 0;
+
+    // This gadget is looked up based on `start` destination selector and therefore we
+    // need to ensure that this computation is performed on the active (`sel == 1`) rows. Otherwise,
+    // a malicious prover could circumvent most of the constraints. Note that #[START_AFTER_LATCH]
+    // does not prevent this from happening.
+    // In addition, we want `end == 1` to be on an active row as well.
+    #[SELECTOR_ON_START_OR_END]
+    (start + end) * (1 - sel) = 0;
+
+    // LATCH_CONDITION is true if either `end` is 1 or `first_row` is 1
+    // LATCH_CONDITION is a boolean because `end` cannot be 1 on the first row (as `sel == 1` when `end == 1`
+    // and `sel == 0` on first row)
+    pol LATCH_CONDITION = end + precomputed.first_row;
 
     #[PROPAGATE_READ_ROOT]
-    NOT_END * (read_root' - read_root) = 0;
+    (1 - LATCH_CONDITION) * (read_root' - read_root) = 0;
     #[PROPAGATE_WRITE]
-    NOT_END * (write' - write) = 0;
+    (1 - LATCH_CONDITION) * (write' - write) = 0;
     #[PROPAGATE_WRITE_ROOT]
-    NOT_END * (write_root' - write_root) = 0;
+    (1 - LATCH_CONDITION) * (write_root' - write_root) = 0;
 
     // If we are not done, the path_len decrements by 1
     #[PATH_LEN_DECREMENTS]
-    NOT_END * (path_len' - path_len + 1) = 0;
+    sel * (1 - end) * (path_len' - path_len + 1) = 0;
 
-    // End when remaining path reaches 1. In other words, (path_len == 1) <==> (end == 1)
-    pol REMAINING_PATH_LEN = path_len - 1;
-
-    pol commit remaining_path_len_inv;
-    #[END_WHEN_PATH_EMPTY]
-    sel * (REMAINING_PATH_LEN * (end * (1 - remaining_path_len_inv) + remaining_path_len_inv) - 1 + end) = 0;
-
-    // index_is_even is constrained to be correct by the NEXT_INDEX_IS_HALVED and FINAL_INDEX_IS_0_OR_1 constraints
-    pol commit index_is_even;
+    // index_is_even is constrained to be correct by the NEXT_INDEX_IS_HALVED and FINAL_INDEX_IS_ODD_BOOLEAN constraints
+    pol commit index_is_even; // @boolean
     index_is_even * (1 - index_is_even) = 0;
     pol INDEX_IS_ODD = (1 - index_is_even);
     // The index into the next layer is half the current index.
     // We don't need to worry about underflowing the field since (index - INDEX_IS_ODD)
     // will be even (over the integers) and as the field is not of characteristic 2, index' == index / 2 over the integers
     #[NEXT_INDEX_IS_HALVED]
-    NOT_END * (index' * 2 + INDEX_IS_ODD - index) = 0;
+    sel * (1 - end) * (2 * index' + INDEX_IS_ODD - index) = 0;
 
-    // Ensure that the final index is 0 or 1.
+    // Ensure that the final index is 0 or 1 by setting it to INDEX_IS_ODD.
     // This ensures that the previous layer cannot overflow the field in the halving constraint
-    // when doing `index' * 2`. This propagates backwards ensuring that no
+    // when doing `2 * index'`. This propagates backwards ensuring that no
     // layer can overflow on the halving constraint's multiplication by 2 as long as
     // tree_height < 254.
-    #[FINAL_INDEX_IS_0_OR_1]
-    end * (index * (1 - index)) = 0;
-    // NOTE: index_is_even is essentially a vertical bit-decomposition of leaf_index.
+    // In addition, this relation constrains the value of `index_is_even` for the last row. without
+    // it `index_is_even` would be under-constrained and a malicious prover could swap the sibling
+    // and the node at the top Merkle tree layer in some relations further below.
+    #[FINAL_INDEX_EQUAL_TO_FIRST_BIT]
+    end * (index - INDEX_IS_ODD) = 0;
+
+    // The bit decomposition of leaf_index corresponds to the INDEX_IS_ODD bits. Namely,
+    // for an initial path_len == LEN, we have:
+    // leaf_index = sum_{i=0}^{LEN-1} INDEX_IS_ODD[i] * 2^i
+    // where INDEX_IS_ODD[i] denotes the value of INDEX_IS_ODD at row i (incrementing
+    // top-down and starting from 0). Therefore, any leaf_index < 2^LEN will be decomposed
+    // and constrained correctly.
 
     // left_node and right_node are sent to poseidon2
     // The constraints below arrange node and sibling for read and write into proper left/right order
     pol commit read_left_node;
     pol commit read_right_node;
     pol commit write_left_node;
     pol commit write_right_node;
-    // This is accomplished by using index_is_even to toggle the (left_node - right_node) term.
-    // If index is even, left_node (to send to poseidon2) is node and right_node is sibling.
-    // And vice-versa.
-    #[ASSIGN_NODE_LEFT_OR_RIGHT_READ]
-    sel * (index_is_even * (read_left_node - read_right_node) + read_right_node - read_node) = 0;
-    #[ASSIGN_SIBLING_LEFT_OR_RIGHT_READ]
-    sel * (index_is_even * (read_right_node - read_left_node) + read_left_node - sibling) = 0;
-
-    #[ASSIGN_NODE_LEFT_OR_RIGHT_WRITE]
-    write * (index_is_even * (write_left_node - write_right_node) + write_right_node - write_node) = 0;
-    #[ASSIGN_SIBLING_LEFT_OR_RIGHT_WRITE]
-    write * (index_is_even * (write_right_node - write_left_node) + write_left_node - sibling) = 0;
-    // NOTE: don't think these can be safely combined
+
+    // This is accomplished by using the value of `index_is_even`. If `index_is_even == 1`, it means that
+    // the current node position at the current layer is even. As a layer index starts at 0, this means that
+    // the current node is the left child of its parent and the sibling is the right child.
+    // Conversly, if `index_is_even == 0`, the curren node is the right child of its parent and the sibling
+    // is the left child.
+    // For `index_is_even == 1`, we assign `read_left_node := read_node` and `read_right_node := sibling`.
+    // For `index_is_even == 0`, we assign `read_left_node := sibling` and `read_right_node := read_node`.
+    #[READ_LEFT_NODE]
+    read_left_node = index_is_even * (read_node - sibling) + sibling;
+    #[READ_RIGHT_NODE]
+    read_right_node = index_is_even * (sibling - read_node) + read_node;
+
+    // Same as above for write (but conditioned on `write == 1`).
+    #[WRITE_LEFT_NODE]
+    write_left_node = write * (index_is_even * (write_node - sibling) + sibling);
+    #[WRITE_RIGHT_NODE]
+    write_right_node = write * (index_is_even * (sibling - write_node) + write_node);
 
     // output_hash = hash(left_node, right_node)
     //     if index_is_even: output_hash = hash(node, sibling)
@@ -163,18 +200,24 @@ namespace merkle_check;
 
     // Lookup to the full poseidon2 gadget
     #[MERKLE_POSEIDON2_READ]
-    sel { read_left_node, read_right_node, /*input_2=*/ precomputed.zero, /*start=1=*/ sel, read_output_hash }
-    in poseidon2_hash.end { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.start, poseidon2_hash.output };
+    sel {
+        read_left_node, read_right_node, /*input_2=*/ precomputed.zero, /*start=1=*/ sel, read_output_hash
+    } in poseidon2_hash.end {
+        poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.start, poseidon2_hash.output
+    };
 
     #[MERKLE_POSEIDON2_WRITE]
-    write { write_left_node, write_right_node, /*input_2=*/ precomputed.zero, /*start=1=*/ sel, write_output_hash }
-    in poseidon2_hash.end { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.start, poseidon2_hash.output };
+    write {
+        write_left_node, write_right_node, /*input_2=*/ precomputed.zero, /*start=1=*/ write, write_output_hash
+    } in poseidon2_hash.end {
+        poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.start, poseidon2_hash.output
+    };
 
     // If we are not done, this row's output_hash is the next row's node
     #[OUTPUT_HASH_IS_NEXT_ROWS_READ_NODE]
-    NOT_END * (read_node' - read_output_hash) = 0;
+    (1 - LATCH_CONDITION) * (read_node' - read_output_hash) = 0;
     #[OUTPUT_HASH_IS_NEXT_ROWS_WRITE_NODE]
-    NOT_END * (write_node' - write_output_hash) = 0;
+    (1 - LATCH_CONDITION) * (write_node' - write_output_hash) = 0;
 
     // If we are done, the output hash is the root
     #[READ_OUTPUT_HASH_IS_READ_ROOT]

barretenberg/cpp/src/CMakeLists.txt

@@ -193,6 +193,7 @@ set(BARRETENBERG_TARGET_OBJECTS
 if(NOT DISABLE_AZTEC_VM AND NOT FUZZING)
     # enable AVM
     list(APPEND BARRETENBERG_TARGET_OBJECTS $<TARGET_OBJECTS:vm2_objects>)
+    list(APPEND BARRETENBERG_TARGET_OBJECTS $<TARGET_OBJECTS:world_state_objects>)
 endif()
 
 if(NOT WASM AND NOT FUZZING)

barretenberg/cpp/src/barretenberg/api/api_avm.cpp

@@ -81,7 +81,7 @@ void avm_simulate(const std::filesystem::path& inputs_path)
     AVM_TRACK_TIME("command/avm_simulate", {
         avm2::AvmAPI avm;
         auto inputs = avm2::AvmAPI::ProvingInputs::from(read_file(inputs_path));
-        avm.simulate(inputs.hints);
+        avm.simulate_with_hinted_dbs(inputs);
     });
 
     print_avm_stats();