Completeness of vector Merkle trees

This file proves the completeness theorem for the vector-style Merkle tree construction defined in VCVio.CryptoFoundations.MerkleTree.Vector.Defs: honestly generated proofs verify against honestly built roots.

The proof is split into two pieces:

• MerkleTree.functional_completeness is a purely functional statement about getPutativeRoot_with_hash and buildMerkleTree_with_hash, proven by induction on the tree depth.
• MerkleTree.completeness lifts the functional statement to the monadic API by reducing through simulateQ of the random oracle.

The auxiliary buildLayer_neverFails and buildMerkleTree_neverFails lemmas record that honest tree construction never fails under the random-oracle simulation, which the completeness reduction relies on.

theorem MerkleTree.buildLayer_neverFails (α : Type) [DecidableEq α] [SampleableType α] [(spec α).DecidableEq] (preexisting_cache : (spec α).QueryCache) (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) : NeverFail ((simulateQ OracleSpec.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 OracleSpec.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).

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 α] [Inhabited α] [SampleableType α] {n : ℕ} [(spec α).DecidableEq] (leaves : List.Vector α (2 ^ n)) (i : Fin (2 ^ n)) (preexisting_cache : (spec α).QueryCache) : (probEvent ((simulateQ OracleSpec.randomOracle do let cache ← buildMerkleTree α n leaves have proof : List.Vector α n := generateProof α i cache let verified ← verifyProof α i leaves[i] (getRoot α cache) proof pure verified).run preexisting_cache) fun (v : Bool × (spec α).QueryCache) => v.1 = true) = 1

Completeness theorem for Merkle trees: for any full binary tree with 2 ^ n leaves, and for any index i, the honestly-generated opening proof verifies against the honestly-built root with probability one.