-
Notifications
You must be signed in to change notification settings - Fork 256
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(avm): merkle tree gadget (#9205)
Resolves #9458
- Loading branch information
1 parent
34e6dd0
commit d52b616
Showing
19 changed files
with
1,140 additions
and
515 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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; | ||
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; | ||
|
||
// 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; | ||
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; | ||
|
||
// 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 }; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.