Inductive Merkle Trees

This file implements Merkle Trees. In contrast to the other Merkle tree implementation in VCVio.CryptoFoundations.MerkleTree, this one is defined inductively.

Implementation Notes

This works with trees that are indexed inductive binary trees, (i.e. indexed in that their definitions and methods carry parameters regarding their structure) as defined in ToMathlib.Data.IndexedBinaryTree.

• We found that the inductive definition seems likely to be convenient for a few reasons:
  • It allows us to handle non-perfect trees.
  • It can allow us to use trees of arbitrary structure in the extractor.
• I considered the indexed type useful because the completeness theorem and extractibility theorems take indices or sets of indices as parameters, and because we are working with trees of arbitrary structure, this lets us avoid having to check that these indices are valid.

Plan/TODOs

• Basic Merkle tree API
  • buildMerkleTree
  • generateProof
  • getPutativeRoot
  • verifyProof
• Completeness theorem
• Collision Lemma (See SNARGs book 18.3)
  • (this is really not a lemma about oracles, so it could go with the binary tree API)
• Extractibility (See SNARGs book 18.5)
• Multi-leaf proofs
• Arbirary arity trees
• Multi-instance

@[reducible]

def InductiveMerkleTree.spec (α : Type u_1) : OracleSpec (α × α)

Define the domain & range of the (single) oracle needed for constructing a Merkle tree with elements from some type α.

We may instantiate α with BitVec n or Fin (2 ^ n) to construct a Merkle tree for boolean vectors of length n.

@[simp]

theorem InductiveMerkleTree.domain_def (α : Type u_1) : (spec α).Domain = (α × α)

@[simp]

theorem InductiveMerkleTree.range_def (α : Type u_1) (z : α × α) : (spec α).Range z = α

def InductiveMerkleTree.singleHash {α : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [HasQuery (spec α) m] (left right : α) : m α

Example: a single hash computation

def InductiveMerkleTree.buildMerkleTree {α : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [HasQuery (spec α) m] {s : BinaryTree.Skeleton} (leaf_tree : BinaryTree.LeafData α s) : m (BinaryTree.FullData α s)

Build the full Merkle tree, returning the tree populated with data on all its nodes

def InductiveMerkleTree.buildMerkleTreeWithHash {α : Type u_1} {s : BinaryTree.Skeleton} (leaf_tree : BinaryTree.LeafData α s) (hashFn : α → α → α) : BinaryTree.FullData α s

A functional form of merkle tree construction, that doesn't depend on the monad. This receives an explicit hash function

@[simp]

theorem InductiveMerkleTree.simulateQ_buildMerkleTree {α : Type u_1} {s : BinaryTree.Skeleton} (leaf_data_tree : BinaryTree.LeafData α s) (f : QueryImpl (spec α) Id) : simulateQ f (buildMerkleTree leaf_data_tree) = buildMerkleTreeWithHash leaf_data_tree fun (left right : α) => f (left, right)

Running the monadic version of buildMerkleTree with an oracle function f is equivalent to running the functional version of buildMerkleTreeWithHash with the same oracle function.

def InductiveMerkleTree.generateProof {α : Type u_1} {s : BinaryTree.Skeleton} (cache_tree : BinaryTree.FullData α s) (idx : BinaryTree.SkeletonLeafIndex s) : List.Vector α idx.depth

Generate a Merkle proof for a leaf at a given idx The proof consists of the sibling hashes needed to recompute the root. Its length is indexed by the leaf depth, so malformed extra hashes are unrepresentable.

TODO rename this to copath and move to BinaryTree?

def InductiveMerkleTree.getPutativeRoot {α : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [HasQuery (spec α) m] {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (leafValue : α) : List.Vector α idx.depth → m α

Given a leaf index, a leaf value at that index, and a proof of the corresponding depth, returns the hash that would be the root of the tree if the proof was valid. i.e. the hash obtained by combining the leaf in sequence with each member of the proof, according to its index.

def InductiveMerkleTree.getPutativeRootWithHash {α : Type u_1} {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (leafValue : α) : List.Vector α idx.depth → (hashFn : α → α → α) → α

A functional version of getPutativeRoot that does not depend on the monad. It receives an explicit hash function hashFn that combines two hashes into one. And recursively calls itself down the tree.

@[simp]

theorem InductiveMerkleTree.simulateQ_getPutativeRoot {α : Type u_1} {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (leafValue : α) (proof : List.Vector α idx.depth) (f : QueryImpl (spec α) Id) : simulateQ f (getPutativeRoot idx leafValue proof) = getPutativeRootWithHash idx leafValue proof fun (left right : α) => f (left, right)

Running the monadic version of getPutativeRoot with an oracle function f, it is equivalent to running the functional version of getPutativeRootWithHash

def InductiveMerkleTree.verifyProof {α : Type} {m : Type → Type u_1} [Monad m] [HasQuery (spec α) m] [DecidableEq α] {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (leafValue rootValue : α) (proof : List.Vector α idx.depth) : OptionT m Unit

Verify a Merkle proof proof that a given leaf at index i is in the Merkle tree with given root. Works by computing the putative root based on the branch, and comparing that to the actual root. Outputs failure if the proof is invalid.

@[simp]

theorem InductiveMerkleTree.functional_completeness {α : Type u_1} {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (leaf_data_tree : BinaryTree.LeafData α s) (hash : α → α → α) : getPutativeRootWithHash idx (leaf_data_tree.get idx) (generateProof (buildMerkleTreeWithHash leaf_data_tree hash) idx) hash = (buildMerkleTreeWithHash leaf_data_tree hash).getRootValue

A functional form of the completeness theorem for Merkle trees. This references the functional versions of getPutativeRoot and buildMerkleTreeWithHash

@[simp]

theorem InductiveMerkleTree.completeness {α : Type} [DecidableEq α] [SampleableType α] {s : BinaryTree.Skeleton} (leaf_data_tree : BinaryTree.LeafData α s) (idx : BinaryTree.SkeletonLeafIndex s) (preexisting_cache : (spec α).QueryCache) : NeverFail ((simulateQ randomOracle do let cache ← buildMerkleTree leaf_data_tree have proof : List.Vector α idx.depth := generateProof cache idx let __discr ← verifyProof idx (leaf_data_tree.get idx) cache.getRootValue proof have x : Option Unit := __discr pure PUnit.unit).run preexisting_cache)

Completeness theorem for Merkle trees.

The proof proceeds by reducing to the functional completeness theorem by a theorem about the OracleComp monad, and then applying the functional version of the completeness theorem.