Definition & Security Proofs for Merkle Trees

[quangvdao]

This issue tracks all development of Merkle trees. This is the basic vector commitment scheme that is required for all proof systems we care about (later development may bring in other schemes such as KZG, Bulletproofs, etc.)

We would like to prove completeness, extractability, and hiding for Merkle trees. These proofs (extractability and hiding) are non-trivial, and will require serious effort (from the core team or a serious outside contributor). The reference for this is in Chiesa & Yogev's recent zkSNARK textbook.

Relevant files in ZKLib:

• Merkle Trees
• Basic Definitions of Commitment Schemes

Depends on progress in #2 to be able to state security properties for Merkle commitments.

Tasks:

• Flesh out the definitions of Merkle trees, especially the opening phase.
  • Single index opening
• Prove completeness of Merkle commitments.
  • Single-index
  • Batch-index
• Initial development of the extractability proof.
  • Extractor definition
  • Single-instance extractability
    • Single-index
    • Batch-index
  • Multi-instance extractability
• Initial development of the hiding proof.

References:

• Chapter 18 (Merkle commitment scheme) of Building Cryptographic Proofs from Hash Functions.
• Section 3 of the original IOP paper.

The textbook has more details but the paper might be an easier first read.

[quangvdao]

@BoltonBailey just assigning you for tracking reason. Feel free to add updated TODOs here especially related to the inductively defined definition.

[BoltonBailey]

For an update, this code now lives in VCVio, but we now have proof for single-index completeness and single-instance extractability. I have updated the above checklist to flesh out more points.

[Abraxas1010]

I've opened Verified-zkEVM/VCVio#473 addressing the batch-index completeness checkbox above (plus a batch analogue of the opening-uniqueness result).

Design in one paragraph: a batch is a selector sel : LeafData Bool s; the authentication data BatchProof α sel mirrors the tree but is pruned at unselected subtrees (one root hash per maximal unselected subtree, no duplication of shared copath nodes, no hashes at all when every leaf is opened), with malformed proofs unrepresentable by typing. functional_batch_completeness is proved by structural induction and lifted to Pr[verify] = 1 under the random oracle through simulateQ, mirroring the single-index pair. Axiom footprints are in the PR description.

Batch-index extractability looks reachable by generalizing the Extractability.lean game to selectors — I'd be glad to take that on as a follow-up if the design in #473 lands in a shape you're happy with.

---

Contributed by The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.