Merkle Trees as a vector commitment

This file defines the vector-style Merkle tree API: the oracle spec, the layered cache, monadic and purely functional builders (buildMerkleTree, buildMerkleTree_with_hash), proof generation and verification, and the bridging simulateQ lemmas that translate the monadic operations into their hash-function counterparts. Completeness of this construction is proven in VCVio.CryptoFoundations.MerkleTree.Vector.Completeness.

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] [hq : 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 (OracleSpec.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) : m Bool

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. Returns true if the proof is valid, and false otherwise.

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_singleHash (α : Type u_1) (f : QueryImpl (spec α) Id) (left right : α) : simulateQ f (singleHash α left right) = f (left, right)

@[simp]

theorem MerkleTree.simulateQ_listVector_mmap_singleHash (α : Type u_1) (f : QueryImpl (spec α) Id) {m : ℕ} (xs : List.Vector (α × α) m) : simulateQ f (List.Vector.mmap (fun (x : α × α) => singleHash α x.1 x.2) 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