Bridge from MIP-8 value trees to induced subtrees

induced_subtree.v proves the paper theorem over complete binary trees: nodes are root-to-node paths and a subtree is a predicate on those paths.

commitment.v uses a more compact executable tree. A value_tree contains only occupied pair leaves and binary merge nodes that are actually hashed. Unary stretches of the complete tree are collapsed because they do not produce hashes.

This file connects the two views. Given the original pair-position list used by build_value_tree, compact_value_tree_nodes expands the compact tree back into the complete-tree nodes that lie on paths to occupied pair leaves. The main theorems are stated directly with the paper-level minimal_connected_subtree predicate rather than introducing a second, compact-tree-specific minimality notion.

Occupied pair leaves as a paper bitmap

occupied_leaf_path depth pairs path means that path names an occupied pair leaf in the complete tree whose leaves are represented by pairs. The recursion follows the same bisection as build_value_tree: false selects the left half and true selects the right half.

Fixpoint occupied_leaf_path
    (depth : nat) (pairs : list (option pair_leaf)) (path : node) : Prop :=
  match depth with
  | O ⇒
      path = [] ∧ ∃ value , pairs = [Some value ]
  | S depth' ⇒
      let width := subtree_width depth' in
      match path with
      | false :: rest ⇒
          occupied_leaf_path depth' (firstn width pairs) rest
      | true :: rest ⇒
          occupied_leaf_path depth' (skipn width pairs) rest
      | [] ⇒ False
      end
  end.

Definition pair_leaf_bitmap
    (depth : nat) (pairs : list (option pair_leaf)) : node → Prop :=
  occupied_leaf_path depth pairs.

Expanding the compact value tree

compact_value_tree_nodes depth pairs tree is the complete-tree node predicate denoted by a compact value_tree built from pairs. Every recursive subtree includes its local root []. If only one child side is occupied, the compact tree has no unary constructor, so the original pairs list is used to decide whether to continue through the left or right branch.

Fixpoint compact_value_tree_nodes
    (depth : nat) (pairs : list (option pair_leaf)) (tree : value_tree)
    (path : node) : Prop :=
  match depth with
  | O ⇒
      path = [] ∧ ∃ value , pairs = [Some value ]
  | S depth' ⇒
      let width := subtree_width depth' in
      let lhs_pairs := firstn width pairs in
      let rhs_pairs := skipn width pairs in
      match build_value_tree depth' lhs_pairs,
            build_value_tree depth' rhs_pairs,
            tree with
      | Some _, None, _ ⇒
          path = [] ∨
          ∃ rest ,
            path = false :: rest ∧
            compact_value_tree_nodes depth' lhs_pairs tree rest
      | None, Some _, _ ⇒
          path = [] ∨
          ∃ rest ,
            path = true :: rest ∧
            compact_value_tree_nodes depth' rhs_pairs tree rest
      | Some _, Some _, TreeNode lhs rhs ⇒
          path = [] ∨
          (∃ rest ,
            path = false :: rest ∧
            compact_value_tree_nodes depth' lhs_pairs lhs rest ) ∨
          (∃ rest ,
            path = true :: rest ∧
            compact_value_tree_nodes depth' rhs_pairs rhs rest )
      | _, _, _ ⇒ False
      end
  end.

Path lemmas

Lemma prefix_to_nil path :
  prefix path [] → path = [].

Lemma prefix_cons bit path leaf :
  prefix path leaf →
  prefix (bit :: path) (bit :: leaf).

Lemma prefix_of_cons_inv bit path leaf :
  prefix path (bit :: leaf) →
  path = [] ∨
  ∃ rest ,
    path = bit :: rest ∧ prefix rest leaf.

Lemma isleaf_cons bit depth leaf :
  isleaf depth leaf →
  isleaf (S depth) (bit :: leaf).

Lemma occupied_leaf_path_length depth pairs path :
  occupied_leaf_path depth pairs path →
  length path = depth.

Lemma occupied_leaf_path_build_value_tree
    depth pairs path :
  length pairs = subtree_width depth →
  occupied_leaf_path depth pairs path →
  ∃ tree , build_value_tree depth pairs = Some tree.

Lemma no_occupied_leaf_path_of_no_tree depth pairs :
  length pairs = subtree_width depth →
  build_value_tree depth pairs = None →
  ∀ path, ¬ occupied_leaf_path depth pairs path.

Lemma compact_value_tree_nodes_root depth pairs tree :
  length pairs = subtree_width depth →
  build_value_tree depth pairs = Some tree →
  compact_value_tree_nodes depth pairs tree [].

The bridge theorem

Lemma compact_value_tree_nodes_are_induced
    depth pairs tree :
  length pairs = subtree_width depth →
  build_value_tree depth pairs = Some tree →
  ∀ path,
    compact_value_tree_nodes depth pairs tree path ↔
    induced_nodes depth (pair_leaf_bitmap depth pairs) path.

Lemma minimal_connected_subtree_ext
    height bitmap subtree subtree' :
  (∀ path, subtree path ↔ subtree' path ) →
  minimal_connected_subtree height bitmap subtree →
  minimal_connected_subtree height bitmap subtree'.

Theorem build_value_tree_paper_minimal_connected_subtree
    depth pairs tree :
  length pairs = subtree_width depth →
  build_value_tree depth pairs = Some tree →
  minimal_connected_subtree depth (pair_leaf_bitmap depth pairs)
    (compact_value_tree_nodes depth pairs tree).

The compact tree is therefore not just a valid minimal subtree. Its complete-tree denotation is exactly the unique subtree satisfying the paper-level minimality specification.

Corollary build_value_tree_unique_paper_minimal_connected_subtree
    depth pairs tree :
  length pairs = subtree_width depth →
  build_value_tree depth pairs = Some tree →
  ∀ subtree,
    minimal_connected_subtree depth (pair_leaf_bitmap depth pairs) subtree ↔
    subtree = compact_value_tree_nodes depth pairs tree.

This page has been generated by coqdoc