search

crytic / properties

Pre-built security properties for common Ethereum operations
GNU Affero General Public License v3.0
275 stars 42 forks source link

[Feature-request]: Merkle trie properties #24

Open bsamuels453 opened 1 year ago

bsamuels453 commented 1 year ago

Describe the desired feature or improvement

  1. How challenging would it be to create a generic set of merkle trie properties?
  2. Do merkle trie library interfaces have enough commonalities for this kind of test suite to be possible?
bsamuels453 commented 1 year ago

Constructs that could be tested:

  1. Merkle Mountain Ranges
  2. Merkle Multi-proofs
  3. Normal Merkle proofs
bsamuels453 commented 1 year ago

property ideas:

  1. Given a trie T and items to be added X and Y, a. assert root(T.add(x)) != root(T.add(y)) b. assert root(T.add(x).add(y)) == root(T.add(y).add(x)) c. assert root(T.add(x).add(x)) == root(T.add(x)) (or reverts)
  2. something to check that the value being proved is a leaf and not an intermediate node (I don't think this applies to merkle-patricia tries)
  3. everything from the guidance