Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(avm): merkle tree gadget #9205

Merged
merged 1 commit into from
Oct 28, 2024
Merged

feat(avm): merkle tree gadget #9205

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 57 additions & 0 deletions barretenberg/cpp/pil/avm/gadgets/merkle_tree.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
include "./poseidon2_full.pil";

// Handles membership and insertion into a merkle tree
namespace merkle_tree(256);

pol commit sel_merkle_tree;
sel_merkle_tree * (1 - sel_merkle_tree) = 0;
// Gotta stop using clk for things that are more like foreign keys
pol commit clk;
// Inputs to the gadget
pol commit leaf_value;
pol commit leaf_index;
pol commit path_len;
pol commit expected_tree_root;
// These are all hinted
pol commit sibling_value;

// If we are not done, the path_len decrements by 1
sel_merkle_tree * (1 - latch) * (path_len' - path_len + 1) = 0;

pol commit latch;
latch * (1 - latch) = 0;
IlyasRidhuan marked this conversation as resolved.
Show resolved Hide resolved
pol commit path_len_inv;
// latch == 1 when the path_len == 0
sel_merkle_tree * (path_len * (latch * (1 - path_len_inv) + path_len_inv) - 1 + latch) = 0;
Comment on lines +24 to +25
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My brain is having trouble understaning this

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks very confusing but is our standard check for "set A = 1 when B = 0, and set A = 0 when B !=0".
It works as follows

  1. Note that a * a_inverse == 1, but a_inverse only exists if a != 0 (0 is the only element without an inverse in the field).
  2. If latch == 0, then the formula becomes path_len * path_len_inv - 1 = 0 (which can only be true when path_len != 0, since we need a valid path_len_inv.
  3. If latch == 1 then the formula becomes path_len * ( 1 - path_len_inv + path_len_inv) = 0, simplified this is path_len = 0

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah I see.... Makes sense! I'd through this in comments (either everywhere we use it, or in one place that we can point to) 🤷


// TODO: Constrain that this is indeed even.
// Note this might be covered by the halving of the leaf index if the original index is constrained.
pol commit leaf_index_is_even;
leaf_index_is_even * (1 - leaf_index_is_even) = 0;
IlyasRidhuan marked this conversation as resolved.
Show resolved Hide resolved
pol LEAF_INDEX_IS_ODD = (1 - leaf_index_is_even);
// If we are not done, the next leaf index is half the current leaf index;
// We don't need to worry about underflowing the field since (leaf_index - LEAF_INDEX_IS_ODD)
// wil be even (over the integers) and as the field is not of characteristic 2, leaf_index' == leaf_index / 2 over the integers
sel_merkle_tree * (1 - latch) * (leaf_index' * 2 + LEAF_INDEX_IS_ODD - leaf_index) = 0;
IlyasRidhuan marked this conversation as resolved.
Show resolved Hide resolved
Comment on lines +32 to +35
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: maybe silly, this would be easier to read for me if the + LEAF_INDEX_IS_ODD was at the end.


// These are what are sent to poseidon2
// These arrange the leaf_value and sibling_value in the correct order
pol commit left_hash;
pol commit right_hash;
// I dont think these can be safely combined
// if the leaf index is even, the leaf value is the left hash and the sibling value is the right hash
// vice-versa
sel_merkle_tree * leaf_index_is_even * (left_hash - right_hash) + right_hash - leaf_value = 0;
sel_merkle_tree * leaf_index_is_even * (right_hash - left_hash) + left_hash - sibling_value = 0;
pol commit output_hash;

// If we are not done, the output hash is the next value in
sel_merkle_tree * (1 - latch) * (leaf_value' - output_hash) = 0;

pol LAST_COMPUTE = sel_merkle_tree * latch;
// LAST_COMPUTE will be used in permutations to other traces

// Permutation to the full poseidon2 gadget
#[PERM_MERKLE_POSEIDON2]
sel_merkle_tree { clk, left_hash, right_hash, output_hash } is
poseidon2_full.sel_merkle_tree {poseidon2_full.clk, poseidon2_full.input_0, poseidon2_full.input_1, poseidon2_full.output };
2 changes: 2 additions & 0 deletions barretenberg/cpp/pil/avm/gadgets/poseidon2_full.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,3 +87,5 @@ namespace poseidon2_full(256);
{ poseidon2.clk, poseidon2.a_0, poseidon2.a_1, poseidon2.a_2, poseidon2.a_3,
poseidon2.b_0, poseidon2.b_1, poseidon2.b_2, poseidon2.b_3 };

// ======== Merkle Tree Selector ======================
pol commit sel_merkle_tree;
1 change: 1 addition & 0 deletions barretenberg/cpp/pil/avm/main.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ include "gadgets/poseidon2.pil";
include "gadgets/poseidon2_full.pil";
include "gadgets/keccakf1600.pil";
include "gadgets/mem_slice.pil";
include "gadgets/merkle_tree.pil";

namespace main(256);
//===== CONSTANT POLYNOMIALS ==================================================
Expand Down
14 changes: 14 additions & 0 deletions barretenberg/cpp/src/barretenberg/vm/avm/generated/circuit_builder.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -423,6 +423,19 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.mem_tsp.set_if_valid_index(i, rows[i].mem_tsp);
polys.mem_val.set_if_valid_index(i, rows[i].mem_val);
polys.mem_w_in_tag.set_if_valid_index(i, rows[i].mem_w_in_tag);
polys.merkle_tree_clk.set_if_valid_index(i, rows[i].merkle_tree_clk);
polys.merkle_tree_expected_tree_root.set_if_valid_index(i, rows[i].merkle_tree_expected_tree_root);
polys.merkle_tree_latch.set_if_valid_index(i, rows[i].merkle_tree_latch);
polys.merkle_tree_leaf_index.set_if_valid_index(i, rows[i].merkle_tree_leaf_index);
polys.merkle_tree_leaf_index_is_even.set_if_valid_index(i, rows[i].merkle_tree_leaf_index_is_even);
polys.merkle_tree_leaf_value.set_if_valid_index(i, rows[i].merkle_tree_leaf_value);
polys.merkle_tree_left_hash.set_if_valid_index(i, rows[i].merkle_tree_left_hash);
polys.merkle_tree_output_hash.set_if_valid_index(i, rows[i].merkle_tree_output_hash);
polys.merkle_tree_path_len.set_if_valid_index(i, rows[i].merkle_tree_path_len);
polys.merkle_tree_path_len_inv.set_if_valid_index(i, rows[i].merkle_tree_path_len_inv);
polys.merkle_tree_right_hash.set_if_valid_index(i, rows[i].merkle_tree_right_hash);
polys.merkle_tree_sel_merkle_tree.set_if_valid_index(i, rows[i].merkle_tree_sel_merkle_tree);
polys.merkle_tree_sibling_value.set_if_valid_index(i, rows[i].merkle_tree_sibling_value);
polys.poseidon2_B_10_0.set_if_valid_index(i, rows[i].poseidon2_B_10_0);
polys.poseidon2_B_10_1.set_if_valid_index(i, rows[i].poseidon2_B_10_1);
polys.poseidon2_B_10_2.set_if_valid_index(i, rows[i].poseidon2_B_10_2);
Expand Down Expand Up @@ -714,6 +727,7 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
i, rows[i].poseidon2_full_num_perm_rounds_rem_inv);
polys.poseidon2_full_output.set_if_valid_index(i, rows[i].poseidon2_full_output);
polys.poseidon2_full_padding.set_if_valid_index(i, rows[i].poseidon2_full_padding);
polys.poseidon2_full_sel_merkle_tree.set_if_valid_index(i, rows[i].poseidon2_full_sel_merkle_tree);
polys.poseidon2_full_sel_poseidon.set_if_valid_index(i, rows[i].poseidon2_full_sel_poseidon);
polys.poseidon2_full_start_poseidon.set_if_valid_index(i, rows[i].poseidon2_full_start_poseidon);
polys.poseidon2_input_addr.set_if_valid_index(i, rows[i].poseidon2_input_addr);
Expand Down
Loading
Loading