feat: define theorem for extractability for Merkle trees

ArkLib.lean

@@ -1,9 +1,11 @@
 import ArkLib.AGM.Basic
 import ArkLib.CommitmentScheme.Basic
 import ArkLib.CommitmentScheme.Fold
-import ArkLib.CommitmentScheme.InductiveMerkleTree
 import ArkLib.CommitmentScheme.KZG
 import ArkLib.CommitmentScheme.MerkleTree
+import ArkLib.CommitmentScheme.MerkleTree.Completeness
+import ArkLib.CommitmentScheme.MerkleTree.Defs
+import ArkLib.CommitmentScheme.MerkleTree.Extractability
 import ArkLib.CommitmentScheme.SimpleRO
 import ArkLib.CommitmentScheme.Tensor
 import ArkLib.CommitmentScheme.Trivial

ArkLib/CommitmentScheme/MerkleTree/Completeness.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2024 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+
+import ArkLib.CommitmentScheme.MerkleTree.Defs
+
+/-!
+# Inductive Merkle Tree Completeness
+
+-/
+
+
+namespace InductiveMerkleTree
+
+open List OracleSpec OracleComp BinaryTree
+
+variable {α : Type}
+
+/--
+A functional form of the completeness theorem for Merkle trees.
+This references the functional versions of `getPutativeRoot` and `buildMerkleTree_with_hash`
+-/
+theorem functional_completeness (α : Type) {s : Skeleton}
+  (idx : SkeletonLeafIndex s)
+  (leaf_data_tree : LeafData α s)
+  (hash : α → α → α) :
+  (getPutativeRoot_with_hash
+    idx
+    (leaf_data_tree.get idx)
+    (generateProof
+      (buildMerkleTree_with_hash leaf_data_tree hash) idx)
+    (hash)) =
+  (buildMerkleTree_with_hash leaf_data_tree hash).getRootValue := by
+  induction s with
+  | leaf =>
+    match leaf_data_tree with
+    | LeafData.leaf a =>
+      cases idx with
+      | ofLeaf =>
+        simp [buildMerkleTree_with_hash, getPutativeRoot_with_hash]
+  | internal s_left s_right left_ih right_ih =>
+    match leaf_data_tree with
+    | LeafData.internal left right =>
+      cases idx with
+      | ofLeft idxLeft =>
+        simp_rw [LeafData.get_ofLeft, LeafData.leftSubtree_internal, buildMerkleTree_with_hash,
+          generateProof_ofLeft, FullData.rightSubtree, FullData.leftSubtree,
+          getPutativeRoot_with_hash, left_ih, FullData.internal_getRootValue]
+      | ofRight idxRight =>
+        simp_rw [LeafData.get_ofRight, LeafData.rightSubtree_internal, buildMerkleTree_with_hash,
+          generateProof_ofRight, FullData.leftSubtree, FullData.rightSubtree,
+          getPutativeRoot_with_hash, right_ih, FullData.internal_getRootValue]
+
+
+/--
+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.
+-/
+theorem completeness [DecidableEq α] [SelectableType α] {s}
+    (leaf_data_tree : LeafData α s) (idx : BinaryTree.SkeletonLeafIndex s)
+    (preexisting_cache : (spec α).QueryCache) :
+    (((do
+      let cache ← buildMerkleTree leaf_data_tree
+      let proof := generateProof cache idx
+      let verified ← verifyProof idx (leaf_data_tree.get idx) (cache.getRootValue) proof
+      guard verified
+      ).simulateQ (randomOracle)).run preexisting_cache).neverFails := by
+  -- An OracleComp is never failing on any preexisting cache
+  -- if it never fails when run with any oracle function.
+  revert preexisting_cache
+  rw [randomOracle_neverFails_iff_runWithOracle_neverFails]
+  -- Call this hash function `f`
+  intro f
+  -- Simplify
+  simp only [verifyProof, bind_pure_comp, guard_eq, bind_map_left, beq_iff_eq, runWithOracle_bind,
+    runWithOracle_buildMerkleTree, runWithOracle_getPutativeRoot, apply_ite, runWithOracle_pure,
+    runWithOracle_failure, Option.bind_eq_bind, Option.bind_some, Option.isSome_some,
+    Option.isSome_none, Bool.if_false_right, Bool.and_true, decide_eq_true_eq]
+  exact functional_completeness α idx leaf_data_tree fun left right ↦ f () (left, right)
+
+end InductiveMerkleTree

ArkLib/CommitmentScheme/InductiveMerkleTree.lean → ArkLib/CommitmentScheme/MerkleTree/Defs.lean

@@ -6,8 +6,6 @@ Authors: Quang Dao
 
 import VCVio
 import ArkLib.ToMathlib.Data.IndexedBinaryTree.Basic
-import ArkLib.CommitmentScheme.Basic
-import Mathlib.Data.Vector.Snoc
 import ArkLib.ToVCVio.Oracle
 
 /-!
@@ -25,7 +23,7 @@ as defined in `ArkLib.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
+* I considered the indexed type useful because the completeness theorem and Extractability 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.
@@ -38,11 +36,15 @@ as defined in `ArkLib.Data.IndexedBinaryTree`.
   - [x] `getPutativeRoot`
   - [x] `verifyProof`
 - [x] Completeness theorem
+  - Note that we handle only single-branch proofs, without multi-leaf proofs.
+  - See SNARGs book 29.2 for the "path-pruning" optimization.
+  - See [here](https://eprint.iacr.org/2021/281.pdf#page=7.03) or [here](https://dev.risczero.com/proof-system-in-detail.pdf) for a slightly different approach ("Merkle caps"/"chopped Merkle trees") used in practice.
 - [ ] 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)
+- [ ] Extractability (See SNARGs book 18.5)
+- [ ] Leaf type distinct from hash type
 - [ ] Multi-leaf proofs
-- [ ] Arbirary arity trees
+- [ ] Arbitrary arity trees
 - [ ] Multi-instance
 
 -/
@@ -248,77 +250,12 @@ lemma runWithOracle_getPutativeRoot {s} (idx : BinaryTree.SkeletonLeafIndex s)
 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.
+Returns a boolean true/false depending on whether the proof is valid or not
 -/
 def verifyProof {α} [DecidableEq α] {s}
     (idx : BinaryTree.SkeletonLeafIndex s) (leafValue : α) (rootValue : α)
-    (proof : List α) : OracleComp (spec α) Unit := do
+    (proof : List α) : OracleComp (spec α) Bool := do
   let putative_root ← getPutativeRoot idx leafValue proof
-  guard (putative_root = rootValue)
-
-/--
-A functional form of the completeness theorem for Merkle trees.
-This references the functional versions of `getPutativeRoot` and `buildMerkleTree_with_hash`
--/
-theorem functional_completeness (α : Type) {s : Skeleton}
-  (idx : SkeletonLeafIndex s)
-  (leaf_data_tree : LeafData α s)
-  (hash : α → α → α) :
-  (getPutativeRoot_with_hash
-    idx
-    (leaf_data_tree.get idx)
-    (generateProof
-      (buildMerkleTree_with_hash leaf_data_tree hash) idx)
-    (hash)) =
-  (buildMerkleTree_with_hash leaf_data_tree hash).getRootValue := by
-  induction s with
-  | leaf =>
-    match leaf_data_tree with
-    | LeafData.leaf a =>
-      cases idx with
-      | ofLeaf =>
-        simp [buildMerkleTree_with_hash, getPutativeRoot_with_hash]
-  | internal s_left s_right left_ih right_ih =>
-    match leaf_data_tree with
-    | LeafData.internal left right =>
-      cases idx with
-      | ofLeft idxLeft =>
-        simp_rw [LeafData.get_ofLeft, LeafData.leftSubtree_internal, buildMerkleTree_with_hash,
-          generateProof_ofLeft, FullData.rightSubtree, FullData.leftSubtree,
-          getPutativeRoot_with_hash, left_ih, FullData.internal_getRootValue]
-      | ofRight idxRight =>
-        simp_rw [LeafData.get_ofRight, LeafData.rightSubtree_internal, buildMerkleTree_with_hash,
-          generateProof_ofRight, FullData.leftSubtree, FullData.rightSubtree,
-          getPutativeRoot_with_hash, right_ih, FullData.internal_getRootValue]
-
-
-/--
-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.
--/
-theorem completeness [DecidableEq α] [SelectableType α] {s}
-    (leaf_data_tree : LeafData α s) (idx : BinaryTree.SkeletonLeafIndex s)
-    (preexisting_cache : (spec α).QueryCache) :
-    (((do
-      let cache ← buildMerkleTree leaf_data_tree
-      let proof := generateProof cache idx
-      let _ ← verifyProof idx (leaf_data_tree.get idx) (cache.getRootValue) proof
-      ).simulateQ (randomOracle)).run preexisting_cache).neverFails := by
-  -- An OracleComp is never failing on any preexisting cache
-  -- if it never fails when run with any oracle function.
-  revert preexisting_cache
-  rw [randomOracle_neverFails_iff_runWithOracle_neverFails]
-  -- Call this hash function `f`
-  intro f
-  -- Simplify
-  simp_rw [verifyProof, guard_eq, bind_pure_comp, id_map', runWithOracle_bind,
-    runWithOracle_buildMerkleTree, runWithOracle_getPutativeRoot]
-  simp only [apply_ite, runWithOracle_pure, runWithOracle_failure, Option.bind_eq_bind,
-    Option.bind_some, Option.isSome_some, Option.isSome_none, Bool.if_false_right, Bool.and_true,
-    decide_eq_true_eq]
-  exact functional_completeness α idx leaf_data_tree fun left right ↦ f () (left, right)
+  return (putative_root == rootValue)
 
 end InductiveMerkleTree