Merkle Trees as a vector commitment

Notes & TODOs

We want this treatment to be as comprehensive as possible. In particular, our formalization should (eventually) include all complexities such as the following:

• Multi-instance extraction & simulation
• Dealing with arbitrary trees (may have arity > 2, or is not complete)
• Path pruning optimization

@[reducible]

def MerkleTree.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 MerkleTree.domain_def (α : Type u_1) : (spec α).Domain = (α × α)

@[simp]

theorem MerkleTree.range_def (α : Type u_1) {x : α × α} : (spec α).Range x = α

def MerkleTree.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 MerkleTree.Cache (α : Type u_1) (n : ℕ) : Type u_1

Cache for Merkle tree. Indexed by j : Fin (n + 1), i.e. j = 0, 1, ..., n.

def MerkleTree.Cache.cons (α : Type u_1) (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) (cache : Cache α n) : Cache α (n + 1)

Add a base layer to the cache

def MerkleTree.Cache.upper (α : Type u_1) (n : ℕ) (cache : Cache α (n + 1)) : Cache α n

Removes the leaves layer to the cache, returning only the layers of the tree above this

def MerkleTree.Cache.leaves (α : Type u_1) (n : ℕ) (cache : Cache α (n + 1)) : List.Vector α (2 ^ (n + 1))

Returns the leaves of the cache

@[simp]

theorem MerkleTree.Cache.upper_cons (α : Type u_1) (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) (cache : Cache α n) : upper α n (cons α n leaves cache) = cache

@[simp]

theorem MerkleTree.Cache.leaves_cons (α : Type u_1) (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) (cache : Cache α n) : Cache.leaves α n (cons α n leaves cache) = leaves

def MerkleTree.buildLayer (α : Type u_1) {m : Type u_1 → Type u_2} [Monad m] [HasQuery (spec α) m] (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) : m (List.Vector α (2 ^ n))

Compute the next layer of the Merkle tree

def MerkleTree.buildMerkleTree (α : Type u_1) {m : Type u_1 → Type u_2} [Monad m] [HasQuery (spec α) m] (n : ℕ) (leaves : List.Vector α (2 ^ n)) : m (Cache α n)

Build the full Merkle tree, returning the cache

def MerkleTree.getRoot (α : Type u_1) {n : ℕ} (cache : Cache α n) : α

Get the root of the Merkle tree

def MerkleTree.findNeighbors {n : ℕ} (i : Fin (2 ^ n)) (layer : Fin n) : Fin (2 ^ (↑layer + 1))

Figure out the indices of the Merkle tree nodes that are needed to recompute the root from the given leaf

@[simp]

theorem MerkleTree.getRoot_trivial (α : Type u_1) {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [HasQuery (spec α) m] (a : α) : getRoot α <$> buildMerkleTree α 0 ⟨[a], ⋯⟩ = pure a

@[simp]

theorem MerkleTree.getRoot_single (α : Type u_1) (a b : α) : getRoot α <$> buildMerkleTree α 1 ⟨[a, b], ⋯⟩ = liftM (OracleQuery.query (a, b))

def MerkleTree.siblingIndex {n : ℕ} (i : Fin (2 ^ (n + 1))) : Fin (2 ^ (n + 1))

Sibling index in a perfect binary tree layer indexed by Fin (2 ^ (n + 1)).

def MerkleTree.generateProof (α : Type u_1) {n : ℕ} (i : Fin (2 ^ n)) (cache : Cache α n) : List.Vector α n

Generate a Merkle proof that a given leaf at index i is in the Merkle tree. The proof consists of the Merkle tree nodes that are needed to recompute the root from the given leaf.

def MerkleTree.getPutativeRoot (α : Type u_1) {m : Type u_1 → Type u_2} [Monad m] [HasQuery (spec α) m] {n : ℕ} (i : Fin (2 ^ n)) (leaf : α) (proof : List.Vector α n) : m α

Given a leaf index, a leaf at that index, and putative proof, 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 MerkleTree.verifyProof (α : Type) [DecidableEq α] {m : Type → Type u_1} [Monad m] [HasQuery (spec α) m] {n : ℕ} (i : Fin (2 ^ n)) (leaf root : α) (proof : List.Vector α n) : 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.

theorem MerkleTree.buildLayer_neverFails (α : Type) [DecidableEq α] [SampleableType α] [(spec α).DecidableEq] (preexisting_cache : (spec α).QueryCache) (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) : NeverFail ((simulateQ randomOracle (buildLayer α n leaves)).run preexisting_cache)

theorem MerkleTree.buildMerkleTree_neverFails (α : Type) [DecidableEq α] [SampleableType α] {n : ℕ} [(spec α).DecidableEq] (leaves : List.Vector α (2 ^ n)) (preexisting_cache : (spec α).QueryCache) : NeverFail ((simulateQ randomOracle (buildMerkleTree α n leaves)).run preexisting_cache)

Building a Merkle tree never results in failure (no matter what queries have already been made to the oracle before it runs).

def MerkleTree.buildLayer_with_hash (α : Type u_1) (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) (hashFn : α × α → α) : List.Vector α (2 ^ n)

A purely functional version of buildLayer, given an explicit hash function.

def MerkleTree.buildMerkleTree_with_hash (α : Type u_1) (n : ℕ) (leaves : List.Vector α (2 ^ n)) (hashFn : α × α → α) : Cache α n

A purely functional version of buildMerkleTree, given an explicit hash function.

def MerkleTree.getPutativeRoot_with_hash (α : Type u_1) {n : ℕ} (i : Fin (2 ^ n)) (leaf : α) (proof : List.Vector α n) (hashFn : α × α → α) : α

A purely functional version of getPutativeRoot, given an explicit hash function.

@[simp]

theorem MerkleTree.simulateQ_query_eq (α : Type u_1) (f : QueryImpl (spec α) Id) (x : α × α) : simulateQ f (liftM (OracleQuery.query x)) = f x

@[simp]

theorem MerkleTree.simulateQ_listVector_mmap_query (α : Type u_1) (f : QueryImpl (spec α) Id) {m : ℕ} (xs : List.Vector (α × α) m) : simulateQ f (List.Vector.mmap (fun (x : OracleSpec.Domain fun (a : α × α) => α) => liftM (OracleQuery.query x)) xs) = List.Vector.map f xs

@[simp]

theorem MerkleTree.simulateQ_buildLayer_eq (α : Type u_1) (f : QueryImpl (spec α) Id) (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) : simulateQ f (buildLayer α n leaves) = buildLayer_with_hash α n leaves f

@[simp]

theorem MerkleTree.simulateQ_buildMerkleTree_eq (α : Type u_1) (f : QueryImpl (spec α) Id) (n : ℕ) (leaves : List.Vector α (2 ^ n)) : simulateQ f (buildMerkleTree α n leaves) = buildMerkleTree_with_hash α n leaves f

@[simp]

theorem MerkleTree.simulateQ_getPutativeRoot_eq (α : Type u_1) (f : QueryImpl (spec α) Id) {n : ℕ} (i : Fin (2 ^ n)) (leaf : α) (proof : List.Vector α n) : simulateQ f (getPutativeRoot α i leaf proof) = getPutativeRoot_with_hash α i leaf proof f

theorem MerkleTree.functional_completeness (α : Type u_1) {n : ℕ} (leaves : List.Vector α (2 ^ n)) (i : Fin (2 ^ n)) (hashFn : α × α → α) : getPutativeRoot_with_hash α i leaves[i] (generateProof α i (buildMerkleTree_with_hash α n leaves hashFn)) hashFn = getRoot α (buildMerkleTree_with_hash α n leaves hashFn)

A functional completeness theorem for Merkle proofs built from buildMerkleTree_with_hash.

theorem MerkleTree.completeness (α : Type) [DecidableEq α] [SampleableType α] {n : ℕ} [(spec α).DecidableEq] (leaves : List.Vector α (2 ^ n)) (i : Fin (2 ^ n)) (preexisting_cache : (spec α).QueryCache) : NeverFail ((simulateQ randomOracle do let cache ← buildMerkleTree α n leaves have proof : List.Vector α n := generateProof α i cache let __discr ← verifyProof α i leaves[i] (getRoot α cache) proof have x : Option Unit := __discr pure PUnit.unit).run preexisting_cache)

Completeness theorem for Merkle trees: for any full binary tree with 2 ^ n leaves, and for any index i, the verifier accepts the opening proof at index i generated by the prover.