Merkleproof verify circuit (#143)

* merkletree: add keypath circuit

* merkletree-circuit: implement proof of existence verification in-circuit

* parametrize max_depth at the tree circuit

* Constrain selectors in-circuit

* implement merketree nonexistence proof circuit, and add edgecase tests

* add non-existence proofs documentation in the mdbook, mv EMPTY->EMPTY_VALUE & NULL->EMPTY_HASH, dependency clean and public exposure methods

* review comments, some extra polishing and add a test that expects wrong proofs to fail

* Add circuit to check only merkleproofs-of-existence

With this, the merkletree_circuit module offers two different circuits:
- `MerkleProofCircuit`: allows to verify both proofs of existence and proofs
non-existence with the same circuit.
- `MerkleProofExistenceCircuit`: allows to verify proofs of existence only.

In this way, if only proofs of existence are needed,
`MerkleProofExistenceCircuit` should be used, which requires less amount
of constraints than `MerkleProofCircuit`.

* Code review

---------

Co-authored-by: Ahmad <root@ahmadafuni.com>
This commit is contained in:
arnaucube 2025-03-18 19:34:01 +01:00 committed by GitHub
parent abce0af675
commit b1689c5b37
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 683 additions and 26 deletions

View file

@ -137,6 +137,10 @@ Since leaf positions are deterministic based on the key, the same approach is us
For the current use cases, we don't need to prove that the key exists but the value is different on that leaf, so we only use the option 1.
There are 2 cases to have into account when dealing with non-inclusion proofs:
- case i) the expected leaf does not exist.
- case ii) the expected leaf does exist in the tree, but it has a different `key`.
## Encoding
> TODO: how key-values, nodes, merkle-proofs, ... are encoded.