Completeness of Inductive Merkle Trees

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

The proof is split into two pieces:

• InductiveMerkleTree.functional_completeness is a purely functional statement about getPutativeRootWithHash and buildMerkleTreeWithHash, proven by induction on the leaf index.
• InductiveMerkleTree.completeness lifts the functional statement to the monadic API by reducing through simulateQ.

@[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 OracleSpec.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.