Inductive Merkle Tree Extractability

This file develops extractability for the inductive Merkle tree commitment scheme. The extractor reconstructs a partial tree from the committing adversary's query log and the opened root, and the main theorem bounds the probability that an adversary opens a leaf that disagrees with the extracted tree.

Main definitions

We make several definitions to set up and analyze the extractability game under namespace InductiveMerkleTree:

• Adversary: a two-phase Merkle tree adversary, bundling an auxiliary state type, a committing phase producing a claimed root and state, and an opening phase producing a (leaf index, leaf value, authentication path) triple from that state.
• extractor: builds a FullData (Option α) s from a query log, root, and skeleton by walking down from the root and pulling each node's children from the unique log entry whose response matches.
• extractabilityGame: the bundled game running a Adversary against the extractor and verifier, recording the verifier's outcome along with the extracted tree and proof.
• ChainInLog: structural predicate witnessing that a query log contains the hash chain from root down to leaf along the path determined by idx.

Main results

• extractability: an adversary wins the extractability game with probability at most (qb + s.depth)^2 / (2|α|) + 1 / |α|, by union-bounding collision probability against the no-collision lucky-guess bound.

Note that our bound is looser than the SNARGs book's bound in Lemma 18.5.1 of ((qb - 1) * qb) / 2 / |α| + (depth + 1) * 2 * size / |α|. This is because we have simplified the proof at the expense of tightness (tighter, that is, in the qb >> size case) by analyzing collisions for the full game at once. A future improvement might be to re-structure the proof to recover the tighter bound.

TODO

• The lemmas here all specialize to (m := OracleComp (spec α)) because the proofs rely on OracleComp-specific machinery — withQueryLog, support, probEvent, and the ChainInLog log predicate over a concrete QueryLog. Generalizing them to an arbitrary monad m (so they apply to e.g. SimulateQ without re-proving) would first require a generic "computation-with-query-log" interface at the framework level, but might be good at some point.

References

• Building Cryptographic Proofs from Hash Functions by Chiesa and Yogev, Lemma 18.5.1.

@[implicit_reducible]

noncomputable def InductiveMerkleTree.instIsUniformSpec {α : Type} [Fintype α] [Inhabited α] : (spec α).IsUniformSpec

Local IsUniformSpec opt-in for spec α: the single Merkle hash oracle samples uniformly from α whenever α is finite and inhabited. Kept local so that downstream files outside this module do not silently pick up uniform semantics for spec α.

Adversary

structure InductiveMerkleTree.Adversary (α : Type) (s : BinaryTree.Skeleton) : Type 1

An adversary in the Merkle tree extractability game, packaged as a single two-phase object: a committing phase that produces a claimed root together with auxiliary state, and an opening phase that consumes the auxiliary state to produce a (leaf index, leaf value, authentication path) triple.

• AuxState : Type

  Auxiliary state carried from the committing phase to the opening phase.

• commit : OracleComp (spec α) (α × self.AuxState)

  Committing phase: produce a claimed root and auxiliary state.

• opening : self.AuxState → OracleComp (spec α) ((idx : BinaryTree.SkeletonLeafIndex s) × α × List.Vector α idx.depth)

  Opening phase: given the auxiliary state, produce a leaf index, claimed leaf value, and authentication path.

def InductiveMerkleTree.Adversary.IsTwoPhaseTotalQueryBound {α : Type} {s : BinaryTree.Skeleton} (𝒜 : Adversary α s) (qb : ℕ) : Prop

The combined two-phase execution of 𝒜 has total query bound qb.

Extractability game

def InductiveMerkleTree.extractorChildren {α : Type} [DecidableEq α] (cache : (spec α).QueryLog) (a : α) : Option (α × α)

The child-decomposition function used by the Merkle-tree extractor. Given a cache and a node value a, look up the first query in cache whose response is a and return its input pair; if no such entry exists, return none.

def InductiveMerkleTree.extractor {α : Type} [DecidableEq α] (s : BinaryTree.Skeleton) (cache : (spec α).QueryLog) (root : α) : BinaryTree.FullData (Option α) s

The extraction algorithm for Merkle trees: from a query log cache, a root, and a skeleton s, build a partial tree of type FullData (Option α) s by walking down from root. A node with value some a looks up the unique log entry whose response is a and uses its input pair as the children's values; in every other case (no matching entry, or the parent is already none) both children are none. Implemented as optionPopulateDown driven by extractorChildren.

def InductiveMerkleTree.extractabilityGame {α : Type} [DecidableEq α] {s : BinaryTree.Skeleton} (𝒜 : Adversary α s) : OracleComp (spec α) (α × 𝒜.AuxState × (idx : BinaryTree.SkeletonLeafIndex s) × α × List.Vector α idx.depth × BinaryTree.FullData (Option α) s × List.Vector (Option α) idx.depth × Bool)

The game for extractability.

This is represented as a single OracleComp that runs the committing adversary, extractor, opening adversary, and verifier in sequence and returns the transcript of the execution.

def InductiveMerkleTree.AdversaryWinsExtractabilityGame {α : Type} [DecidableEq α] {s : BinaryTree.Skeleton} {AuxState : Type} : α × AuxState × (idx : BinaryTree.SkeletonLeafIndex s) × α × List.Vector α idx.depth × BinaryTree.FullData (Option α) s × List.Vector (Option α) idx.depth × Bool → Prop

The event that the adversary wins the extractability game: verification passes but the extracted leaf or proof does not match.

theorem InductiveMerkleTree.extractabilityGame_isTotalQueryBound {α : Type} [DecidableEq α] {s : BinaryTree.Skeleton} (𝒜 : Adversary α s) (qb : ℕ) (h : 𝒜.IsTwoPhaseTotalQueryBound qb) : (extractabilityGame 𝒜).IsTotalQueryBound (qb + s.depth)

If the adversary 𝒜 has two-phase total query bound qb, then the full extractability game has total query bound qb + s.depth.

The extra s.depth accounts for the verifyProof step, which traverses the path from the queried leaf to the root, making at most s.depth oracle queries.

def InductiveMerkleTree.ChainInLog {α : Type} {s : BinaryTree.Skeleton} (log : (spec α).QueryLog) (leaf root : α) (idx : BinaryTree.SkeletonLeafIndex s) : List.Vector α idx.depth → Prop

Predicate stating that log contains a hash chain from leaf (combined with the sibling values in proof) up to root along the path determined by idx.

theorem InductiveMerkleTree.logHasCollision_of_chainInLog_of_ne {α : Type} {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (log : (spec α).QueryLog) (root x y : α) (proof₁ proof₂ : List.Vector α idx.depth) (hne : (x, proof₁) ≠ (y, proof₂)) (hc₁ : ChainInLog log x root idx proof₁) (hc₂ : ChainInLog log y root idx proof₂) : OracleComp.LogHasCollision log

Log-level binding (Collision Lemma at the log level). Log-formalized analog of getPutativeRootWithHash_binding_collision: two distinct openings (x, proof₁) ≠ (y, proof₂) of the same root at the same index, both witnessed by hash chains ChainInLog in the same log, force log to contain a hash collision (two log entries with equal responses but distinct inputs).

theorem InductiveMerkleTree.chainInLog_of_extractor_get_ne_none {α : Type} [DecidableEq α] {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (log : (spec α).QueryLog) (root : α) (h_ne_none : (extractor s log root).get idx.toNodeIndex ≠ none) : ∃ (extLeaf : α) (extProof : List.Vector α idx.depth), (extractor s log root).get idx.toNodeIndex = some extLeaf ∧ (generateProof (extractor s log root) idx).toList = List.map some extProof.toList ∧ ChainInLog log extLeaf root idx extProof

Extractor recovery to a log chain. When the extractor's path at idx is intact (the value there is ≠ none), the extracted leaf value and proof form a hash chain ChainInLog in the log. The conclusion bundles three facts: the extracted leaf (extLeaf), the recovered authentication path (extProof), and a chain witness in log connecting them to root.

theorem InductiveMerkleTree.extractability {α : Type} [DecidableEq α] [Fintype α] [Inhabited α] {s : BinaryTree.Skeleton} (𝒜 : Adversary α s) (qb : ℕ) (h_IsQueryBound_qb : 𝒜.IsTwoPhaseTotalQueryBound qb) : probEvent (extractabilityGame 𝒜) AdversaryWinsExtractabilityGame ≤ (↑qb + ↑s.depth) ^ 2 / (2 * ↑(Fintype.card α)) + 1 / ↑(Fintype.card α)

The extractability theorem for Merkle trees.

Adapting from the SNARGs book Lemma 18.5.1:

For any adversary 𝒜 whose committing and opening phases together obey the two-phase total query bound qb, if the game runs 𝒜.commit and 𝒜.opening, and the extractor algorithm is run on the resulting cache and root, then with probability at most κ does 𝒜 "win the extractability game", i.e. simultaneously

• the merkle tree verification passes on the proof from 𝒜.opening
• but the extracted (leaf value, proof) pair does not match the adversary's (leaf value, proof) pair

Where κ is 1/|α| * ((qb + s.depth)^2 / 2 + 1).