Adds sparse merkle tree in noname `stdlib` #249

0xnullifier · 2025-01-01T17:11:12Z

This pr adds the sparse merkle tree to stdlib and closes #223

The testing was done against the output of circomlibjs you can find the script here.

The approach taken is almost identical to the circom's implementation mentioned in the issue.

0xnullifier · 2025-01-03T06:03:54Z

Hey @katat can you take a look?

katat · 2025-01-03T08:06:44Z

Thanks! Will take a look soon.

0xnullifier · 2025-01-03T08:34:32Z

hey it seems the checks failed due to enforce formating
So I will go ahead and fix them

katat

Nice work!
I just had a round of review, and will need another rounds. I left some comments.

I think some of the arithmetic logic can be simplified using ifelse block.
More documentation on the arithmetic logic in the compute_roots and next_state, if they can't be simplified ifelse, would be useful.

src/tests/stdlib/smt/smt_verify.no

src/stdlib/native/smt/lib.no

katat · 2025-01-06T08:24:11Z

src/stdlib/native/smt/lib.no

+/// Field: mimc7 hash for key = 1 and values = [key,value]
+fn compute_leaf_hash(key: Field, value: Field) -> Field {
+    let hash_values = [key, value];
+    return mimc::mimc7_hash(hash_values, 1);


is it correct to provide 1 as the secret key?

Yeah this was in the iden3 specification I think this is mainly for domain seperation of the internal and leaf hash functions other than that I cannot find a reason why

src/stdlib/native/smt/lib.no

katat · 2025-01-06T11:20:53Z

src/stdlib/native/smt/lib.no

+///     `is_update`:  whether the operation is an update operation
+/// # Returns
+///     `[Bool;6]`: the next state
+fn next_state(


it'd better to have more documentation on the logic for each transition.

Got it. It was written at the top but I will repeat it below

src/stdlib/native/smt/lib.no

katat · 2025-01-06T11:38:40Z

src/stdlib/native/smt/lib.no

+    let new_key_bits = bits::to_bits(LEN , new_key);
+
+    let mut level_inserted = old_level_inserted(enabled,siblings);
+    let mut states = [[false;6]; LEN];


would it be easier if it is a field value to represent the different states intead of using an array of booleans?

yeah but that makes the states computation a bit more difficult as in this case I can directly do boolean operations as my state transitions are dictated by booleans.
Also the assertion that there is only one state at a time

I tried the single state variable earlier but it got too difficult but when we do #248 it will be way easier maybe we can refactor then?

One more point is that circomlib also uses 6 variables for some reason maybe it has less constraints this way?

src/stdlib/native/smt/lib.no

katat

Sorry for the delay. Finally got a chance to go through the code logic :D
Lgtm, @mimoo might want to have another round.

I am wondering if we can encapsulate the code a bit more using structs. The idea is like:

struct SMT {
    root: Field,
    ...
}

// init smt with a root
fn SMT.new(root, ...) -> SMT {
...
}

// differentiate the operations via different methods
// once updated, it should update the SMT.root internally
fn SMT.insert(...)
fn SMT.update(...)
fn SMT.delete(...)

// for verifying the membership
fn SMT.verify_membership(...)
fn SMT.verify_non_membership(...)

For the non membership verification logic, I am wondering what are the assumptions.

There seems no comparisons in terms of branch navigations among the following two keys in order to indicate the key doesn't exist because of the proof of exists of the not_found_key.

Is this something agreed externally in practice, or actually something missing in the circuit? In other word, how can it prove the key doesn't exist by proving its relationship with not_found_key, which has been proven exist already.

katat · 2025-01-07T08:58:52Z

src/stdlib/native/smt/lib.no

+
+
+
+// State Constants for computing new roots


Suggested change

// State Constants for computing new roots

// States for computing new roots

katat · 2025-01-07T09:10:55Z

src/stdlib/native/smt/lib.no

+    done[LEN - 2] = level_inserted[LEN - 1];
+
+    for idx in 1..(LEN-1) {
+        let is_sibling_zero = siblings[(LEN - 2) - idx] == 0;


it'd better to have a var to represent the reversed index:

let reversed_idx = (LEN - 1) - idx;

katat · 2025-01-07T09:12:45Z

src/stdlib/native/smt/lib.no

+    let mut done = [false; LEN];
+
+
+    level_inserted[(LEN - 1)] = !(siblings[LEN- 2] == 0);


Suggested change

level_inserted[(LEN - 1)] = !(siblings[LEN- 2] == 0);

level_inserted[LEN - 1] = !(siblings[LEN - 2] == 0);

katat · 2025-01-07T09:32:59Z

src/stdlib/native/smt/lib.no

+/// This function get the level where the key will be inserted. level 0 is the root , 1 is next and so on..
+/// To find this level all the child level must have a sibling of 0 and
+/// the parent level has a sibling != 0. The root is assumed to have a parent level with a sibling != 0
+fn level_inserted(siblings: [Field;LEN]) ->  [Bool;LEN] {


shouldn't sibling need to be [Field; LEN - 1]

yup there is no need for the full array but then I would have to slice the array which would be expensive so I think it is better to do this correct me if I'm wrong

katat · 2025-01-07T09:50:08Z

src/stdlib/native/smt/lib.no

+
+
+    level_inserted[(LEN - 1)] = !(siblings[LEN- 2] == 0);
+    done[LEN - 2] = level_inserted[LEN - 1];


Might be better to use a mutable bool variable for done instead of array.
Then in the for loop

for idx in 1..(LEN - 1) { ... done = done || level_inserted[(LEN - 1) - idx]; ... }

katat · 2025-01-21T07:15:38Z

src/stdlib/native/smt/lib.no

+    let not_found_leaf = compute_leaf_hash(not_found_key,not_found_val);
+    let leaf = compute_leaf_hash(key,value);
+
+    let nfk_bits = bits::to_bits(LEN , not_found_key);


is nfk_bits going to be used somewhere?

maybe add a comment here to note this is just for range checking.

0xnullifier · 2025-01-21T11:15:53Z

Hey @katat the run fails as the test do not pass due to If-Else Monomarphisation but it seems that there is a bug in the way we are type checking in the mast for ExprKind::IfElse.

noname/src/mast/mod.rs

Line 1066 in a9a83b8

if then_mono.typ != else_mono.typ {

As my code fails due to unmatching types if Field {const : true} and Field { const: false} if I change it to something like this :

            let is_match = match (&then_mono.typ, &else_mono.typ) {
                (Some(then_ty), Some(else_ty)) => then_ty.match_expected(else_ty, false),
                // handle all the case
            };

Then it works

0xnullifier · 2025-01-21T11:17:38Z

I am wondering if we can encapsulate the code a bit more using structs. The idea is like:

This looks better I will refactor the code to something like this

Is this something agreed externally in practice, or actually something missing in the circuit? In other word, how can it prove the key doesn't exist by proving its relationship with not_found_key, which has been proven exist already

When proving non membership proofs we want to give a merkle proof (root + siblings) to the position where the key should have been which can be a zero or a occupied leaf the not_found_key represents this position maybe I can change the name to something else if it is confusing like auxiliary_key . This is the case for the iden3 implementations of sparse merkle tree. For example in their golang implementation they also give a auxiliary NodeAux or zero. some other smt implementations like celestia also do the same of adding the Auxiliary node data in non membership proofs

There seems no comparisons in terms of branch navigations among the following two keys in order to indicate the key doesn't exist because of the proof of exists of the not_found_key.

The not found key is used to compute the the not_found_leaf which is used to compute the root to match the current root

katat · 2025-01-21T13:19:09Z

The not found key is used to compute the the not_found_leaf which is used to compute the root to match the current root

but how does this relate to proving not_found_leaf occupies where the membership key is supposed to be in the path?

katat · 2025-01-21T13:20:15Z

As my code fails due to unmatching types if Field {const : true} and Field { const: false} if I change it to something like this :

Oh yeah, nice spot!
Do you want to create a separate PR to fix this?

0xnullifier · 2025-01-21T13:34:19Z

Oh yeah, nice spot!
Do you want to create a separate PR to fix this?

Do I just raise the pr directly or open a issue and then raise a pr?

but how does this relate to proving not_found_leaf occupies where the membership key is supposed to be in the path?

I think i don't get the question. The compute_root function place this root in place of where key is supposed to be like. So here is what I am saying

To compute the green node we need the not_found_key right ? If we did not have that we would not have any way of computing the root and checking if the given root is equal to the computed root. lmk if there is anything wrong with the way I am thinking

katat · 2025-01-22T03:21:14Z

Do I just raise the pr directly or open a issue and then raise a pr?

It is fine to just create a pr and point it to the comment above for reference.

I think i don't get the question. The compute_root function place this root in place of where key is supposed to be like. So here is what I am saying

Nice diagram, thanks!
I think I got it now. The compute_root always takes the key bits to determine the branches. So if the not_found_leaf is proven exist via the key_bits, it implies the key doesn't exist.

let new_root = compute_root(
    states[(LEN - 1) - idx],
    computed_root,
    siblings[(LEN - 1) - idx],
    key_bits[(LEN - 1) - idx], // the branching bit is always based on the key
    not_found_leaf,
    leaf
);

adds sparse merkle tree to the stdlib

f35fde5

0xnullifier force-pushed the smt branch from 479c9c5 to f35fde5 Compare January 1, 2025 18:31

fmt changes

e543726

katat reviewed Jan 6, 2025

View reviewed changes

0xnullifier added 2 commits January 6, 2025 19:39

adds more documentation and simple code using if-else

6b64b4e

changes the switcher and adds more documentation

cc0a656

katat reviewed Jan 21, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Adds sparse merkle tree in noname `stdlib` #249

Adds sparse merkle tree in noname `stdlib` #249

0xnullifier commented Jan 1, 2025

0xnullifier commented Jan 3, 2025

katat commented Jan 3, 2025

0xnullifier commented Jan 3, 2025

katat left a comment

katat Jan 6, 2025

0xnullifier Jan 6, 2025 •

edited

Loading

katat Jan 6, 2025

0xnullifier Jan 6, 2025 •

edited

Loading

katat Jan 6, 2025

0xnullifier Jan 6, 2025 •

edited

Loading

katat left a comment •

edited

Loading

katat Jan 7, 2025

katat Jan 7, 2025

katat Jan 7, 2025

katat Jan 7, 2025

0xnullifier Jan 21, 2025

katat Jan 7, 2025

katat Jan 21, 2025

katat Jan 21, 2025

0xnullifier commented Jan 21, 2025 •

edited

Loading

0xnullifier commented Jan 21, 2025 •

edited

Loading

katat commented Jan 21, 2025

katat commented Jan 21, 2025

0xnullifier commented Jan 21, 2025 •

edited

Loading

katat commented Jan 22, 2025

	// State Constants for computing new roots
	// States for computing new roots

		let mut done = [false; LEN];


		level_inserted[(LEN - 1)] = !(siblings[LEN- 2] == 0);

	level_inserted[(LEN - 1)] = !(siblings[LEN- 2] == 0);
	level_inserted[LEN - 1] = !(siblings[LEN - 2] == 0);



		level_inserted[(LEN - 1)] = !(siblings[LEN- 2] == 0);
		done[LEN - 2] = level_inserted[LEN - 1];

Adds sparse merkle tree in noname stdlib #249

Are you sure you want to change the base?

Adds sparse merkle tree in noname stdlib #249

Conversation

0xnullifier commented Jan 1, 2025

0xnullifier commented Jan 3, 2025

katat commented Jan 3, 2025

0xnullifier commented Jan 3, 2025

katat left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

0xnullifier Jan 6, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

0xnullifier Jan 6, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

0xnullifier Jan 6, 2025 • edited Loading

Choose a reason for hiding this comment

katat left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

0xnullifier commented Jan 21, 2025 • edited Loading

0xnullifier commented Jan 21, 2025 • edited Loading

katat commented Jan 21, 2025

katat commented Jan 21, 2025

0xnullifier commented Jan 21, 2025 • edited Loading

katat commented Jan 22, 2025

Adds sparse merkle tree in noname `stdlib` #249

Adds sparse merkle tree in noname `stdlib` #249

0xnullifier Jan 6, 2025 •

edited

Loading

0xnullifier Jan 6, 2025 •

edited

Loading

0xnullifier Jan 6, 2025 •

edited

Loading

katat left a comment •

edited

Loading

0xnullifier commented Jan 21, 2025 •

edited

Loading

0xnullifier commented Jan 21, 2025 •

edited

Loading

0xnullifier commented Jan 21, 2025 •

edited

Loading