Total query bounds for inductive Merkle tree primitives

This file establishes IsTotalQueryBound lemmas for the oracle computations defined in Defs.lean:

• singleHash_isTotalQueryBound — singleHash makes one oracle query.
• getPutativeRoot_isTotalQueryBound — getPutativeRoot makes idx.depth queries, one per level walked from the leaf to the root.
• verifyProof_isTotalQueryBound — verifyProof inherits the same bound.
• verifyProof_isTotalQueryBound_skeleton_depth — coarsening to the uniform s.depth bound, useful when the bound must not depend on idx.

These bounds are consumed downstream by the extractability argument, which needs to know the total number of queries any honest Merkle operation issues.

Total query bounds for Merkle-tree primitives

theorem InductiveMerkleTree.singleHash_isTotalQueryBound {α : Type} (left right : α) : (singleHash left right).IsTotalQueryBound 1

singleHash makes exactly one oracle query, hence has total query bound 1.

theorem InductiveMerkleTree.getPutativeRoot_isTotalQueryBound {α : Type} {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (leafValue : α) (proof : List.Vector α idx.depth) : (getPutativeRoot idx leafValue proof).IsTotalQueryBound idx.depth

getPutativeRoot makes one oracle query per level of idx, so it has total query bound idx.depth.

theorem InductiveMerkleTree.verifyProof_isTotalQueryBound {α : Type} [DecidableEq α] {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (leafValue rootValue : α) (proof : List.Vector α idx.depth) : (verifyProof idx leafValue rootValue proof).IsTotalQueryBound idx.depth

verifyProof makes the same idx.depth queries as getPutativeRoot; the trailing equality test is pure.

theorem InductiveMerkleTree.verifyProof_isTotalQueryBound_skeleton_depth {α : Type} [DecidableEq α] {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (leafValue rootValue : α) (proof : List.Vector α idx.depth) : (verifyProof idx leafValue rootValue proof).IsTotalQueryBound s.depth

Coarser form of verifyProof_isTotalQueryBound bounded by the full skeleton depth s.depth rather than the per-leaf idx.depth. Useful when the bound must be uniform across all leaf indices of s.