MIP-8 page commitments

This file formalizes Merkle Commitments via Induced Subtrees by defining a Gallina (Coq) model of the scheme and proving the main security property about the model.
In subsequent files, the C++ implementation is specified against this model. Once that implementation proof is complete, the security properties proved here transfer to the actual C++ code.
The commitment is for a 128-slot storage page. Each slot is a 32-byte value or empty. The algorithm groups adjacent slots into 64-byte pair leaves, builds the induced subtree over the nonempty pairs, hashes that compact tree, and finally seals the result with the full 128-bit slot bitmap. Empty pages have no merge root; their root is just a hash of the bitmap seal.
The file is organized in the same order a reader should understand the construction.
  • Section Algorithm defines the compact commitment algorithm. This is the simplest presentation: normalize the slot list, form optional pair leaves, recursively build the induced value tree, hash it, and seal it.
  • Section CorrectnessStatement adds the extra vocabulary needed for the security theorem: semantic hash-call locations, located traces, and the aligned-collision assumption. This machinery can be avoided if we only care about a weaker security property which assumes a too strong property about lack of collision on inputs.
  • Section CorrectnessProof proves the statement. You do not need to read it unless you want to: Coq has checked that there are no holes in the proof. It also contains the lower-level reducer facts needed to connect the compact Section 1 presentation with the C++ scratch-array intuition.
The concrete byte types use skylabs.prelude.fin: fin.t n is the type of natural numbers less than n. Internally it is represented as a dependent pair of a number and a proof that the number is below n, but that detail can be ignored here.
The BLAKE3 compression behavior is abstracted by three parameters. H64 hashes one 64-byte block and carries a mode bit so the model can distinguish the C++ leaf-mode calls from merge-mode calls. seal_empty models the 16-byte empty-page seal. seal_nonempty models the 48-byte seal containing the bitmap and a 32-byte induced-subtree root.


Section 1: Algorithm model

This section contains only the objects needed to understand what the MIP-8 page commitment computes.
Section Algorithm.

Definition page_slot_count : nat := 128.
Definition page_pair_count : nat := 64.
Definition page_pair_tree_depth : nat := 6.

The public input is a list of optional slot values. Position n is slot n; None means the slot is absent. Inputs shorter than 128 slots are padded with None, and longer inputs are truncated. This canonical 128-slot view is what the commitment binds.

Definition slot_values : Type := list (option slot_word).

Definition normalize_slots (slots : slot_values) : slot_values :=
  firstn page_slot_count (slots ++ repeat None page_slot_count).

Bitmaps are little-endian bit lists here. bitmap_to_bytes16 packs the 128-slot seal bitmap into the 16 bytes used by the page commitment.
Definition bitmap := list bool.

Definition slot_present (slot : option slot_word) : bool :=
  match slot with
  | Some _ ⇒ true
  | None ⇒ false
  end.

Definition slot_payload (slot : option slot_word) : slot_word :=
  match slot with
  | Some value ⇒ value
  | None ⇒ bytes32_of_N 0
  end.

Local Open Scope N_scope.

Fixpoint bitmap_to_N (bm : bitmap) : N :=
  match bm with
  | [] ⇒ 0
  | bit :: rest ⇒ (if bit then 1 else 0) + 2 × bitmap_to_N rest
  end.

Local Close Scope N_scope.

if bm ≥ 2^128, this returns 0
Definition bitmap_to_bytes16 (bm : bitmap) : bytes16 :=
  @fin.of_N' (pow2N 128) ltac:(solve_pow2N_pos) (bitmap_to_N bm).

Definition slot_bitmap (slots : slot_values) : bitmap :=
  map slot_present (normalize_slots slots).

pair adjacent slots
Fixpoint pair_options_raw
    (slots : slot_values) : list (option pair_leaf) :=
  match slots with
  | first :: second :: rest ⇒
      if slot_present first || slot_present second
      then Some (slot_payload first, slot_payload second) ::
           pair_options_raw rest
      else None :: pair_options_raw rest
  | _ ⇒ []
  end.

Definition pair_options (slots : slot_values)
    : list (option pair_leaf) :=
  pair_options_raw (normalize_slots slots).

subtree_width depth is the number of pair positions below a complete subtree at depth. A leaf-level subtree has width 1, and each parent level doubles the width. The full storage page uses page_pair_tree_depth = 6, so its complete tree has 64 pair positions.
Fixpoint subtree_width (n : nat) : nat :=
  match n with
  | O ⇒ 1
  | S n' ⇒ 2 × subtree_width n'
  end.

The Coq algorithm is designed for ease of understanding, not efficiency, so it is organized differently from the C++ loop. We first pair adjacent slots, then construct the minimal binary tree with the occupied slot pairs as leaves. value_tree represents that compact tree. After that, the pre-seal root hash is just a simple tree recursion.
Inductive value_tree : Type :=
| TreeLeaf (leaf : pair_leaf)
| TreeNode (lchild rchild : value_tree).

just a helper used below to build a tree from slot pairs
Definition combine_value_trees
    (lhs rhs : option value_tree) : option value_tree :=
  match lhs, rhs with
  | None, None ⇒ None
  | Some tree, None ⇒ Some tree
  | None, Some tree ⇒ Some tree
  | Some lhs_tree, Some rhs_tree ⇒
      Some (TreeNode lhs_tree rhs_tree)
  end.

this can be considered the heart of the Coq model:
Fixpoint build_value_tree
    (depth : nat) (pairs : list (option pair_leaf))
    : option value_tree :=
  match depth with
  | O ⇒
      match pairs with
      | [Some value] ⇒ Some (TreeLeaf value)
      | _ ⇒ None
      end
  | S depth' ⇒
      let width := subtree_width depth' in
      combine_value_trees
        (build_value_tree depth' (firstn width pairs))
        (build_value_tree depth' (skipn width pairs))
  end.

Definition value_tree_from_slots
    (slots : slot_values) : option value_tree :=
  build_value_tree page_pair_tree_depth (pair_options slots).

Section value_tree_demo.
  Variables (v0 v1 v8 v32 v32' : slot_word).

  Let zero : slot_word := bytes32_of_N 0.
  Let singleton_pair_slot (value : slot_word) : slot_values :=
    [Some value; None].
  Let demo_slots : slot_values :=
    singleton_pair_slot v0 ++
    singleton_pair_slot v1 ++
    repeat None 12 ++
    singleton_pair_slot v8 ++
    repeat None 46 ++
    [Some v32; Some v32'].
  Let pair0 : pair_leaf := (v0, zero).
  Let pair1 : pair_leaf := (v1, zero).
  Let pair8 : pair_leaf := (v8, zero).
  Let pair32 : pair_leaf := (v32, v32').
  Let demo_tree : value_tree :=
    TreeNode
      (TreeNode
        (TreeNode
          (TreeLeaf pair0)
          (TreeLeaf pair1))
        (TreeLeaf pair8))
      (TreeLeaf pair32).

This example helps build intuition for build_value_tree. The input demo_slots has occupied pair leaves 0, 1, 8, and 32. The many None slots are deliberate: they show that the compact value_tree skips every complete-tree node whose other side is empty. 
slot sketch:
  pair 0  = (v0, 0)
  pair 1  = (v1, 0)
  pairs 2..7 are empty
  pair 8  = (v8, 0)
  pairs 9..31 are empty
  pair 32 = (v32, v32')

value tree:

                 TreeNode
                /        \
           TreeNode     TreeLeaf (v32, v32')
          /        \
     TreeNode     TreeLeaf (v8, 0)
     /      \
TreeLeaf   TreeLeaf
 (v0, 0)   (v1, 0)
In the ambient complete tree, there are unary stretches from pair 8 up to the 0..15 region and from pair 32 up to the 32..63 half. They do not become TreeNode constructors because they do not correspond to hash merges. The example lemma value_tree_from_slots_demo proves that the algorithm returns exactly this compact tree.
  Example value_tree_from_slots_demo :
    value_tree_from_slots demo_slots = Some demo_tree.
  Proof.
    reflexivity.
  Qed.
End value_tree_demo.

Later, the file induced_subtree_bridge.v proves that the complete-tree denotation of a tree built by build_value_tree satisfies the notion page's minimal_connected_subtree predicate: the lemma build_value_tree_paper_minimal_connected_subtree and the uniqueness corollary build_value_tree_unique_paper_minimal_connected_subtree: but these lemmas are not necessary to understand the content of this file.
Once we have the value tree, a simple tree recursion suffices to produce the pre-seal root hash:
  Fixpoint eval_tree (tree : value_tree) : digest :=
    match tree with
    | TreeLeaf value ⇒ H64 leaf_mode value
    | TreeNode lhs rhs ⇒
        H64 merge_mode (eval_tree lhs, eval_tree rhs)
    end.

Final seal step. This is the main algorithm whose security properties we prove below.
  Definition root (slots : slot_values) : digest :=
    match value_tree_from_slots slots with
    | None ⇒ seal_empty (bitmap_to_bytes16 (slot_bitmap slots))
    | Some tree ⇒
        seal_nonempty
          (bitmap_to_bytes16 (slot_bitmap slots))
          (eval_tree tree)
    end.

End Algorithm.

Section 2: Correctness statement

At this point, we can already state a somewhat weak correctness property like:
  Theorem Root_binding_break_extracts_aligned_collision slots slots' :
    Root slots = Root slots' →
    normalize_slots slots ≠ normalize_slots slots' →
    exists_hash_collision (closure slots) (closure slots').
where exists_hash_collision sl sr says that there is a hash_input (e.g. pair of values) in the set sl and there is a hash_input in the set sr, such that their hash outputs are the same. closure s produces a set closed under the hash operations: e.g. calling hash with merge mode on any 2 values in s.
But such a property is unnecessarily weak because it treats every hash collision in the closure as equally relevant. Hash collisions are only problematic if they happen at the same spot in the tree. Next, we build some machinery to be able to define "same spot". The main step here is to define root_with_trace, which is like the Section 1 root function above, but also traces the calls to the hash function and the tree address where each hash happened. To make that easy, we first define a slightly augmented version of value_tree, where each node stores its tree address (merge level and horizontal index in the corresponding complete binary tree).
Intuitively, the proof goes as follows: if two roots are equal, compare the two seal hashes first. If the seal inputs differ, the binding break is already a seal collision. If the seal inputs agree, then the slot bitmap agrees, so both computations have the same induced pair-tree shape. The proof can then walk corresponding leaves and internal merge nodes. At each corresponding position, equality of child digests either gives equal inputs or exposes a hash collision at that same semantic position.
Section CorrectnessStatement.

Located hash calls

Locations are geometric MIP-8 tree positions, not positions in the C++ loop trace. We use merge_level, not root-depth: merge_level = 0 merges adjacent pair leaves, merge_level = 1 merges groups of two pairs, and so on upward through the complete 64-pair tree. parent_index is the horizontal index of that merge at the given level.
Inductive call_loc : Type :=
| LocSeal
| LocPairLeaf (pair_index : nat)
| LocNode (merge_level parent_index : nat).

Inductive call_input : Type :=
| InputLeaf (leaf : pair_leaf)
| InputMerge (left_digest right_digest : digest)
| InputSealEmpty (bitmap_bytes : bytes16)
| InputSealNonempty (bitmap_bytes : bytes16) (tree_root : digest).

Record located_call : Type := mk_located_call {
  located_call_loc : call_loc;
  located_call_input : call_input;
}.

Annotating the compact tree

Section 1's value_tree deliberately omits locations. This proof-only tree is the same tree after annotation: it remembers where each retained pair leaf and merge came from in the complete 64-pair tree.
Inductive located_value_tree : Type :=
| LocatedTreeLeaf (pair_index : nat) (leaf : pair_leaf)
| LocatedTreeNode
    (merge_level parent_index : nat)
    (left_child right_child : located_value_tree).

A compact induced tree cannot recover locations by itself. If one side of a split is empty, combine_value_trees erased that side, so the compact tree no longer says whether a surviving leaf came from the left or right half of the complete tree.
annotate_value_tree therefore walks the compact tree together with the original pair-position list. The list supplies only the missing left/right occupancy information; the values and hash shape still come from the already-built tree.
Fixpoint annotate_value_tree
    (depth start : nat)
    (pairs : list (option pair_leaf)) (tree : value_tree)
    : option located_value_tree :=
  match depth with
  | O ⇒
      match pairs, tree with
      | [Some _], TreeLeaf value ⇒ Some (LocatedTreeLeaf start value)
      | _, _ ⇒ None
      end
  | 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 with
      | None, None ⇒ None
      | Some _, None ⇒
          annotate_value_tree depth' start lhs_pairs tree
      | None, Some _ ⇒
          annotate_value_tree depth' (start + width) rhs_pairs tree
      | Some _, Some _ ⇒
          match tree with
          | TreeNode lhs rhs ⇒
              match annotate_value_tree depth' start lhs_pairs lhs,
                    annotate_value_tree
                      depth' (start + width) rhs_pairs rhs with
              | Some lhs_loc, Some rhs_loc ⇒
                  Some
                    (LocatedTreeNode
                       depth'
                       (start / subtree_width (S depth'))
                       lhs_loc
                       rhs_loc)
              | _, _ ⇒ None
              end
          | TreeLeaf _ ⇒ None
          end
      end
  end.

Definition annotate_tree_from_slots
    (slots : slot_values) (tree : value_tree)
    : option located_value_tree :=
  annotate_value_tree page_pair_tree_depth 0 (pair_options slots) tree.

Annotation recovers the semantic positions erased by the compact tree. These positions are the nodes of the ambient complete 64-pair tree. A location LocNode level parent covers this pair interval: 
parent * 2^(level+1)  through  (parent + 1) * 2^(level+1) - 1
The level says how wide the complete-tree region is, and the parent index says where that region sits horizontally. A compact TreeNode receives a LocNode exactly when both children of that complete-tree region are occupied; unary complete-tree steps are skipped because no hash merge happens there.
These are the locations later used by the aligned-collision statement.
Section annotate_tree_demo.
  Variables (v0 v1 v4 v5 : slot_word).

  Let zero : slot_word := bytes32_of_N 0.
  Let singleton_pair_slot (value : slot_word) : slot_values :=
    [Some value; None].
  Let demo_slots : slot_values :=
    singleton_pair_slot v0 ++
    singleton_pair_slot v1 ++
    repeat None 4 ++
    singleton_pair_slot v4 ++
    singleton_pair_slot v5.
  Let pair0 : pair_leaf := (v0, zero).
  Let pair1 : pair_leaf := (v1, zero).
  Let pair4 : pair_leaf := (v4, zero).
  Let pair5 : pair_leaf := (v5, zero).

  Let demo_tree : value_tree :=
    match value_tree_from_slots demo_slots with
    | Some tree ⇒ tree
    | None ⇒ TreeLeaf pair0
    end.
  Let demo_located_tree : located_value_tree :=
    LocatedTreeNode 2 0
      (LocatedTreeNode 0 0
        (LocatedTreeLeaf 0 pair0)
        (LocatedTreeLeaf 1 pair1))
      (LocatedTreeNode 0 2
        (LocatedTreeLeaf 4 pair4)
        (LocatedTreeLeaf 5 pair5)).

This example shows how annotate_tree_from_slots adds ambient complete-tree locations to the output of build_value_tree. 
occupied pair leaves:
  0, 1, 4, 5

located merge skeleton:

             LocNode 2 0
            /           \
     LocNode 0 0     LocNode 0 2
      /       \       /       \
 0:(v0,0) 1:(v1,0) 4:(v4,0) 5:(v5,0)
LocNode 0 1 does not exist because there were no leaves for positions 2 and 3. No LocNode exists at level 1 either: those complete-tree nodes are unary stretches, so build_value_tree optimized them away. The lemma annotate_tree_from_slots_demo proves the displayed located tree. The helper lemma annotate_demo_tree_from_slots first records that the compact tree for demo_slots is demo_tree.
  Example annotate_demo_tree_from_slots :
    value_tree_from_slots demo_slots = Some demo_tree.
  Proof.
    reflexivity.
  Qed.

  Example annotate_tree_from_slots_demo :
    annotate_tree_from_slots demo_slots demo_tree =
    Some demo_located_tree.
  Proof.
    reflexivity.
  Qed.
End annotate_tree_demo.

  Definition call_digest (input : call_input) : digest :=
    match input with
    | InputLeaf value ⇒ H64 leaf_mode value
    | InputMerge lhs rhs ⇒ H64 merge_mode (lhs, rhs)
    | InputSealEmpty bm ⇒ seal_empty bm
    | InputSealNonempty bm root ⇒ seal_nonempty bm root
    end.

  Record root_trace : Type := {
    traced_root : digest;
    traced_calls : list located_call;
  }.

eval_tree_with_trace is similar to eval_tree above, except it also records the semantic locations and inputs for the hash calls.
  Fixpoint eval_tree_with_trace (tree : located_value_tree) : root_trace :=
    match tree with
    | LocatedTreeLeaf index value ⇒
        let input := InputLeaf value in
        {|
          traced_root := call_digest input;
          traced_calls :=
            [mk_located_call (LocPairLeaf index) input];
        |}
    | LocatedTreeNode level parent lhs rhs ⇒
        let lhs_trace := eval_tree_with_trace lhs in
        let rhs_trace := eval_tree_with_trace rhs in
        let input :=
          InputMerge
            lhs_trace.(traced_root)
            rhs_trace.(traced_root) in
        {|
          traced_root := call_digest input;
          traced_calls :=
            lhs_trace.(traced_calls) ++
            rhs_trace.(traced_calls) ++
            [mk_located_call
               (LocNode level parent)
               input];
        |}
    end.

root with trace

The traced computation is the proof-facing counterpart of Section 1's root function. It computes the digest and the semantic hash-call trace together, so the seal call in the trace visibly uses the same digest returned as the root.
The fallback branch under Some tree is unreachable for public slot_values: Section 3 proves annotate_tree_from_slots_some. It is present only so this proof-facing function is total without making the reader carry an impossible option case.
  Definition root_with_trace (slots : slot_values)
      : root_trace :=
    match value_tree_from_slots slots with
    | None ⇒
        let bitmap_bytes := bitmap_to_bytes16 (slot_bitmap slots) in
        {|
          traced_root := seal_empty bitmap_bytes;
          traced_calls :=
            [mk_located_call
               LocSeal
               (InputSealEmpty bitmap_bytes)];
        |}
    | Some tree ⇒
        let bitmap_bytes := bitmap_to_bytes16 (slot_bitmap slots) in
        match annotate_tree_from_slots slots tree with
        | Some located_tree ⇒
            let tree_trace := eval_tree_with_trace located_tree in
            let tree_root := tree_trace.(traced_root) in
            {|
              traced_root := seal_nonempty bitmap_bytes tree_root;
              traced_calls :=
                tree_trace.(traced_calls) ++
                [mk_located_call
                   LocSeal
                   (InputSealNonempty bitmap_bytes tree_root)];
            |}
        | None ⇒
            {|
              traced_root := seal_nonempty bitmap_bytes (eval_tree tree);
              traced_calls :=
                [mk_located_call
                   LocSeal
                   (InputSealNonempty bitmap_bytes (eval_tree tree))];
            |}
        end
    end.

  Section root_with_trace_demo.
    Variables (v1 v2 v3 : slot_word).

    Let zero : slot_word := bytes32_of_N 0.
    Let leaf0 : pair_leaf := (v1, zero).
    Let leaf1 : pair_leaf := (v2, v1).
    Let leaf2 : pair_leaf := (v3, zero).
    Let demo_slots : slot_values :=
      [Some v1; None; Some v2; Some v1; Some v3].
    Let demo_located_tree : located_value_tree :=
      LocatedTreeNode 1 0
        (LocatedTreeNode 0 0
          (LocatedTreeLeaf 0 leaf0)
          (LocatedTreeLeaf 1 leaf1))
        (LocatedTreeLeaf 2 leaf2).
    Let demo_bitmap : bytes16 :=
      bitmap_to_bytes16 (slot_bitmap demo_slots).
    Let leaf0_digest : digest := call_digest (InputLeaf leaf0).
    Let leaf1_digest : digest := call_digest (InputLeaf leaf1).
    Let leaf2_digest : digest := call_digest (InputLeaf leaf2).
    Let merge01_input : call_input :=
      InputMerge leaf0_digest leaf1_digest.
    Let merge01_digest : digest := call_digest merge01_input.
    Let merge012_input : call_input :=
      InputMerge merge01_digest leaf2_digest.
    Let merge012_digest : digest := call_digest merge012_input.

The example lemma proves the result of root_with_trace on demo_slots
    Example root_with_trace_demo :
      root_with_trace demo_slots =
      {|
        traced_root := seal_nonempty demo_bitmap merge012_digest;
        traced_calls :=
          [mk_located_call (LocPairLeaf 0) (InputLeaf leaf0);
           mk_located_call (LocPairLeaf 1) (InputLeaf leaf1);
           mk_located_call (LocNode 0 0) merge01_input;
           mk_located_call (LocPairLeaf 2) (InputLeaf leaf2);
           mk_located_call (LocNode 1 0) merge012_input;
           mk_located_call
             LocSeal
             (InputSealNonempty demo_bitmap merge012_digest)];
      |}.
    Proof.
      reflexivity.
    Qed.
  End root_with_trace_demo.

An exists_aligned_collision is the precise bad event for binding. It does not say that some two hash calls anywhere collided. It says that the two compared traces contain calls at the same semantic location, with different inputs and equal hash outputs.
  Definition exists_aligned_collision
      (trace trace' : root_trace) : Prop :=
    ∃ loc input input',
      In (mk_located_call loc input)
        trace.(traced_calls) ∧
      In (mk_located_call loc input')
        trace'.(traced_calls) ∧
      input ≠ input' ∧
      call_digest input = call_digest input'.

Main theorem statements

The first theorem says that root_with_trace is only proof instrumentation. Adding semantic call locations and a trace does not change the root computed by the compact Section 1 algorithm. We have aborted this theorem proof here and will prove it later in the file.
  Theorem root_with_trace_root_statement slots :
    (root_with_trace slots).(traced_root) = root slots.

Root_binding_break_extracts_aligned_collision is the binding theorem in its most informative form. It does not assume collision freedom. It says that if two normalized page views are different but their traced computations return the same digest, then the two traces contain an aligned collision.
The statement is phrased directly with root_with_trace because the trace is part of the evidence: exists_aligned_collision refers directly to the two traced computations produced by root_with_trace. The above theorem anyway proves that root_with_trace and the Section 1 root function produce the same root hash.
  Theorem Root_binding_break_extracts_aligned_collision_statement
      slots slots' :
    (root_with_trace slots).(traced_root) = (root_with_trace slots').(traced_root) →
    normalize_slots slots ≠ normalize_slots slots' →
    exists_aligned_collision (root_with_trace slots) (root_with_trace slots').

Forward reference: the C++ proof layer uses this file's Section 1 root function as the pure model for monad::page_commit. The exact C++ postcondition is in page_commit_spec.

End CorrectnessStatement.

Section 3: Correctness proof

The rest of the file is proof machinery. The first group of lemmas shows that the compact recursive algorithm has the expected bitmap and value properties. Later lemmas show that annotation preserves the compact tree root, that located traces line up with root computation, and that equality of roots can be pushed down through aligned locations.
Some definitions in this section look closer to the C++ implementation than Section 1 does. They are proof instrumentation, not the primary specification. Their job is to justify the same induced-tree intuition that the C++ scratch-array reducer implements.
Section CorrectnessProof.

  #[local] Instance call_loc_eq_decision : EqDecision call_loc.

  Definition call_loc_eq_dec
      (loc loc' : call_loc) : {loc = loc'} + {loc ≠ loc'} :=
    decide (loc = loc').

  #[local] Instance call_input_eq_decision : EqDecision call_input.

  Definition call_input_eq_dec
      (input input' : call_input) : {input = input'} + {input ≠ input'} :=
    decide (input = input').

These are proof-only views of the traced located tree. Section 2 keeps only eval_tree_with_trace, where root computation and trace construction happen together; the projections below make later inductions shorter.
  Fixpoint erase_located_tree (tree : located_value_tree) : value_tree :=
    match tree with
    | LocatedTreeLeaf _ value ⇒ TreeLeaf value
    | LocatedTreeNode _ _ lhs rhs ⇒
        TreeNode (erase_located_tree lhs) (erase_located_tree rhs)
    end.

  Definition eval_located_tree (tree : located_value_tree) : digest :=
    (eval_tree_with_trace tree).(traced_root).

  Fixpoint located_tree_values
      (tree : located_value_tree) : list pair_leaf :=
    match tree with
    | LocatedTreeLeaf _ value ⇒ [value]
    | LocatedTreeNode _ _ lhs rhs ⇒
        located_tree_values lhs ++ located_tree_values rhs
    end.

  Definition tree_located_calls (tree : located_value_tree)
      : list located_call :=
    (eval_tree_with_trace tree).(traced_calls).

  Definition slot_from_bit (present : bool) (value : slot_word)
      : option slot_word :=
    if present then Some value else None.

  Fixpoint pair_bitmap_from_slot_bitmap
      (bm : bitmap) : bitmap :=
    match bm with
    | first :: second :: rest ⇒
        (first || second) :: pair_bitmap_from_slot_bitmap rest
    | [last] ⇒ [last]
    | [] ⇒ []
    end.

  Fixpoint pair_leaves_raw (slots : slot_values) : list pair_leaf :=
    match slots with
    | first :: second :: rest ⇒
        (slot_payload first, slot_payload second) :: pair_leaves_raw rest
    | _ ⇒ []
    end.

  Fixpoint select_by_bitmap {A : Type}
      (bm : bitmap) (values : list A) : list A :=
    match bm, values with
    | occupied :: bm_rest, value :: values_rest ⇒
        if occupied
        then value :: select_by_bitmap bm_rest values_rest
        else select_by_bitmap bm_rest values_rest
    | _, _ ⇒ []
    end.

  Definition pair_bitmap (slots : slot_values) : bitmap :=
    pair_bitmap_from_slot_bitmap (slot_bitmap slots).

  Definition pair_leaves (slots : slot_values) : list pair_leaf :=
    pair_leaves_raw (normalize_slots slots).

  Definition active_pair_values (slots : slot_values) : list pair_leaf :=
    select_by_bitmap (pair_bitmap slots) (pair_leaves slots).

  Definition pair_option_present (pair_value : option pair_leaf) : bool :=
    match pair_value with
    | Some _ ⇒ true
    | None ⇒ false
    end.

  Definition pair_option_bitmap (pairs : list (option pair_leaf))
      : bitmap :=
    map pair_option_present pairs.

  Fixpoint pair_option_values
      (pairs : list (option pair_leaf)) : list pair_leaf :=
    match pairs with
    | [] ⇒ []
    | Some pair_value :: rest ⇒ pair_value :: pair_option_values rest
    | None :: rest ⇒ pair_option_values rest
    end.

  Definition index_bit_is_zero (bit index : nat) : bool :=
    Nat.even (index / subtree_width bit).

  Definition same_parent_at_level (bit lhs rhs : nat) : bool :=
    Nat.eqb (lhs / subtree_width (S bit)) (rhs / subtree_width (S bit)).

  Definition sibling_candidate (bit lhs rhs : nat) : bool :=
    same_parent_at_level bit lhs rhs &&
    index_bit_is_zero bit lhs.

The following reducer mirrors the C++ scratch/live-bitmap loop. It is proof instrumentation: Section 1 already gave the readable recursive value-tree algorithm.
  Record live_node : Type := {
    live_index : nat;
    live_tree : value_tree;
  }.

  Fixpoint active_leaf_nodes_from
      (next_index : nat) (bm : bitmap) (values : list pair_leaf)
      : option (list live_node × list pair_leaf) :=
    match bm with
    | [] ⇒ Some ([], values)
    | occupied :: rest ⇒
        if occupied
        then
          match values with
          | [] ⇒ None
          | value :: values_rest ⇒
              match active_leaf_nodes_from
                      (S next_index) rest values_rest with
              | Some (nodes, leftover) ⇒
                  Some
                    ({|
                       live_index := next_index;
                       live_tree := TreeLeaf value;
                     |} :: nodes, leftover)
              | None ⇒ None
              end
          end
        else active_leaf_nodes_from (S next_index) rest values
    end.

  Definition active_leaf_nodes
      (bm : bitmap) (values : list pair_leaf) : option (list live_node) :=
    match active_leaf_nodes_from 0 bm values with
    | Some (nodes, []) ⇒ Some nodes
    | _ ⇒ None
    end.

  Fixpoint merge_level (bit : nat) (nodes : list live_node)
      : list live_node :=
    match nodes with
    | [] ⇒ []
    | current :: rest_nodes ⇒
        match rest_nodes with
        | [] ⇒ [current]
        | next :: later ⇒
            if sibling_candidate bit
                 current.(live_index) next.(live_index)
            then
              {|
                live_index := current.(live_index);
                live_tree :=
                  TreeNode current.(live_tree) next.(live_tree);
              |} :: merge_level bit later
            else current :: merge_level bit rest_nodes
        end
    end.

  Fixpoint reduce_levels
      (fuel bit : nat) (nodes : list live_node) : list live_node :=
    match fuel with
    | O ⇒ nodes
    | S fuel' ⇒
        if length nodes <=? 1
        then nodes
        else reduce_levels fuel' (S bit) (merge_level bit nodes)
    end.

  Inductive commit_result : Type :=
  | CommitMalformed
  | CommitEmpty
  | CommitNonempty (tree : value_tree).

  Definition reducer_result
      (depth : nat) (bm : bitmap) (values : list pair_leaf)
      : commit_result :=
    match active_leaf_nodes bm values with
    | None ⇒ CommitMalformed
    | Some [] ⇒ CommitEmpty
    | Some nodes ⇒
        match reduce_levels depth 0 nodes with
        | [root] ⇒ CommitNonempty root.(live_tree)
        | _ ⇒ CommitMalformed
        end
    end.

  Fixpoint tree_values (tree : value_tree) : list pair_leaf :=
    match tree with
    | TreeLeaf value ⇒ [value]
    | TreeNode lhs rhs ⇒ tree_values lhs ++ tree_values rhs
    end.

  Definition live_values (nodes : list live_node) : list pair_leaf :=
    concat (map (fun node ⇒ tree_values node.(live_tree)) nodes).

  Inductive same_tree_shape : value_tree → value_tree → Prop :=
  | SameTreeLeaf (lhs_value rhs_value : pair_leaf) :
        same_tree_shape
          (TreeLeaf lhs_value)
          (TreeLeaf rhs_value)
  | SameTreeNode
      (lhs lhs' rhs rhs' : value_tree) :
        same_tree_shape lhs lhs' →
        same_tree_shape rhs rhs' →
        same_tree_shape
          (TreeNode lhs rhs)
          (TreeNode lhs' rhs').

  Inductive same_located_tree_shape :
      located_value_tree → located_value_tree → Prop :=
  | SameLocatedTreeLeaf
      (index : nat) (lhs_value rhs_value : pair_leaf) :
        same_located_tree_shape
          (LocatedTreeLeaf index lhs_value)
          (LocatedTreeLeaf index rhs_value)
  | SameLocatedTreeNode
      (level parent : nat)
      (lhs lhs' rhs rhs' : located_value_tree) :
        same_located_tree_shape lhs lhs' →
        same_located_tree_shape rhs rhs' →
        same_located_tree_shape
          (LocatedTreeNode level parent lhs rhs)
          (LocatedTreeNode level parent lhs' rhs').

  Definition same_live_shape (lhs rhs : live_node) : Prop :=
    live_index lhs = live_index rhs ∧
    same_tree_shape (live_tree lhs) (live_tree rhs).

  Definition valid_seal_bitmap (bm : bitmap) : Prop :=
    length bm = 128.

  Fixpoint slots_from_bitmap_values
      (bm : bitmap) (values : list pair_leaf) : option slot_values :=
    match bm with
    | [] ⇒
        match values with
        | [] ⇒ Some []
        | _ :: _ ⇒ None
        end
    | first :: second :: bm_rest ⇒
        if first || second
        then
          match values with
          | (first_value, second_value) :: values_rest ⇒
              match slots_from_bitmap_values bm_rest values_rest with
              | Some slots_rest ⇒
                  Some
                    (slot_from_bit first first_value ::
                     slot_from_bit second second_value ::
                     slots_rest)
              | None ⇒ None
              end
          | [] ⇒ None
          end
        else
          match slots_from_bitmap_values bm_rest values with
          | Some slots_rest ⇒ Some (None :: None :: slots_rest)
          | None ⇒ None
          end
    | [_] ⇒ None
    end.

Basic facts about the algorithmic definitions from Section 1.
  Lemma normalize_slots_length slots :
    length (normalize_slots slots) = page_slot_count.

  Lemma normalize_slots_even slots :
    Nat.even (length (normalize_slots slots)) = true.

  Lemma slot_from_present_payload slot :
    slot_from_bit (slot_present slot) (slot_payload slot) = slot.

  Lemma bitmap_to_N_lt_length bm :
    (bitmap_to_N bm < 2 ^ N.of_nat (length bm))%N.

  Lemma bitmap_to_N_lt_128 bm :
    length bm ≤ 128 → (bitmap_to_N bm < pow2N 128)%N.

  Lemma bitmap_to_bytes16_to_N bm :
    length bm ≤ 128 →
    fin.to_N (bitmap_to_bytes16 bm) = bitmap_to_N bm.

  Lemma bitmap_to_N_inj_same_length bm bm' :
    length bm = length bm' →
    bitmap_to_N bm = bitmap_to_N bm' →
    bm = bm'.
  Lemma bitmap_to_bytes16_inj bm bm' :
    valid_seal_bitmap bm →
    valid_seal_bitmap bm' →
    bitmap_to_bytes16 bm = bitmap_to_bytes16 bm' →
    bm = bm'.

  Lemma pair_options_raw_length_exact slots n :
    length slots = 2 × n →
    length (pair_options_raw slots) = n.

  Lemma pair_options_length slots :
    length (pair_options slots) = page_pair_count.

  Lemma pair_options_bitmap_raw_even slots :
    Nat.even (length slots) = true →
    pair_option_bitmap (pair_options_raw slots) =
    pair_bitmap_from_slot_bitmap (map slot_present slots).

  Lemma pair_options_bitmap slots :
    pair_option_bitmap (pair_options slots) = pair_bitmap slots.

  Lemma pair_options_values_raw slots :
    pair_option_values (pair_options_raw slots) =
    select_by_bitmap
      (pair_bitmap_from_slot_bitmap (map slot_present slots))
      (pair_leaves_raw slots).

  Lemma pair_options_values slots :
    pair_option_values (pair_options slots) = active_pair_values slots.

  Lemma slots_from_bitmap_values_roundtrip_even slots :
    Nat.even (length slots) = true →
    slots_from_bitmap_values
      (map slot_present slots)
      (select_by_bitmap
         (pair_bitmap_from_slot_bitmap (map slot_present slots))
         (pair_leaves_raw slots)) =
    Some slots.

  Lemma slots_from_bitmap_values_roundtrip slots :
    slots_from_bitmap_values
      (slot_bitmap slots)
      (active_pair_values slots) =
    Some (normalize_slots slots).

  Lemma slot_bitmap_valid slots :
    valid_seal_bitmap (slot_bitmap slots).

  Lemma tree_values_nonempty tree :
    tree_values tree ≠ [].

  Lemma eval_located_tree_erase tree :
    eval_tree (erase_located_tree tree) = eval_located_tree tree.

  Lemma located_tree_values_erase tree :
    tree_values (erase_located_tree tree) = located_tree_values tree.

  Lemma pair_option_values_app lhs rhs :
    pair_option_values (lhs ++ rhs) =
    pair_option_values lhs ++ pair_option_values rhs.

  Lemma pair_option_values_firstn_skipn width pairs :
    pair_option_values pairs =
    pair_option_values (firstn width pairs) ++
    pair_option_values (skipn width pairs).

  Lemma build_tree_values_or_empty depth pairs :
    length pairs = subtree_width depth →
    match build_value_tree depth pairs with
    | Some tree ⇒ tree_values tree = pair_option_values pairs
    | None ⇒ pair_option_values pairs = []
    end.

  Lemma value_tree_from_slots_values slots tree :
    value_tree_from_slots slots = Some tree →
    tree_values tree = active_pair_values slots.

  Lemma value_tree_from_slots_empty_values slots :
    value_tree_from_slots slots = None →
    active_pair_values slots = [].

  Lemma build_tree_same_bitmap depth pairs pairs' :
    length pairs = subtree_width depth →
    length pairs' = subtree_width depth →
    pair_option_bitmap pairs = pair_option_bitmap pairs' →
    match build_value_tree depth pairs,
          build_value_tree depth pairs' with
    | Some tree, Some tree' ⇒ same_tree_shape tree tree'
    | None, None ⇒ True
    | _, _ ⇒ False
    end.

  Lemma annotate_value_tree_build_some depth start pairs tree :
    length pairs = subtree_width depth →
    build_value_tree depth pairs = Some tree →
    ∃ located_tree,
      annotate_value_tree depth start pairs tree = Some located_tree ∧
      erase_located_tree located_tree = tree.

  Lemma annotate_tree_from_slots_some slots tree :
    value_tree_from_slots slots = Some tree →
    ∃ located_tree,
      annotate_tree_from_slots slots tree = Some located_tree ∧
      erase_located_tree located_tree = tree.

First main theorem: the traced computation agrees with the small algorithmic specification from Section 1. The proof is intentionally simple: it unfolds both computations and checks that the trace records the same seal digest that the Section 1 root function returns.
  Theorem root_with_trace_root slots :
    (root_with_trace slots).(traced_root) = root slots.

  Lemma annotate_value_tree_same_shape
      depth start pairs pairs' tree tree' located located' :
    length pairs = subtree_width depth →
    length pairs' = subtree_width depth →
    pair_option_bitmap pairs = pair_option_bitmap pairs' →
    annotate_value_tree depth start pairs tree = Some located →
    annotate_value_tree depth start pairs' tree' = Some located' →
    same_located_tree_shape located located'.
  Lemma annotate_tree_from_slots_same_shape
      slots slots' tree tree' located located' :
    slot_bitmap slots = slot_bitmap slots' →
    annotate_tree_from_slots slots tree = Some located →
    annotate_tree_from_slots slots' tree' = Some located' →
    same_located_tree_shape located located'.

  Lemma value_tree_from_slots_same_shape slots slots' tree tree' :
    slot_bitmap slots = slot_bitmap slots' →
    value_tree_from_slots slots = Some tree →
    value_tree_from_slots slots' = Some tree' →
    same_tree_shape tree tree'.

  Lemma normalize_slots_from_same_commit_parts slots slots' :
    slot_bitmap slots = slot_bitmap slots' →
    active_pair_values slots = active_pair_values slots' →
    normalize_slots slots = normalize_slots slots'.

  Definition hash64_call : Set := (hash_mode × bytes64)%type.

  Fixpoint tree_hash_inputs (tree : value_tree) : list hash64_call :=
    match tree with
    | TreeLeaf value ⇒ [(leaf_mode, value)]
    | TreeNode lhs rhs ⇒
        tree_hash_inputs lhs ++
        tree_hash_inputs rhs ++
        [(merge_mode, (eval_tree lhs, eval_tree rhs))]
    end.

  Definition hash64_input_set := hash64_call → Prop.

  Definition collision_free_on (allowed : hash64_input_set) : Prop :=
    ∀ lhs rhs,
      allowed lhs →
      allowed rhs →
      H64 (fst lhs) (snd lhs) = H64 (fst rhs) (snd rhs) →
      lhs = rhs.

  Definition Root_from_bitmaps
      (depth : nat)
      (tree_bm seal_bm : bitmap)
      (values : list pair_leaf)
      : option digest :=
    match reducer_result depth tree_bm values with
    | CommitMalformed ⇒ None
    | CommitEmpty ⇒ Some (seal_empty (bitmap_to_bytes16 seal_bm))
    | CommitNonempty tree ⇒
        Some (seal_nonempty (bitmap_to_bytes16 seal_bm) (eval_tree tree))
    end.

  Definition root_hash_inputs_from_bitmaps
      (depth : nat) (tree_bm : bitmap) (values : list pair_leaf)
      : list hash64_call :=
    match reducer_result depth tree_bm values with
    | CommitMalformed ⇒ []
    | CommitEmpty ⇒ []
    | CommitNonempty tree ⇒ tree_hash_inputs tree
    end.

  Definition root_empty_seal_inputs_from_bitmaps
      (depth : nat)
      (tree_bm seal_bm : bitmap)
      (values : list pair_leaf)
      : list bytes16 :=
    match reducer_result depth tree_bm values with
    | CommitEmpty ⇒ [bitmap_to_bytes16 seal_bm]
    | _ ⇒ []
    end.

  Definition root_nonempty_seal_inputs_from_bitmaps
      (depth : nat)
      (tree_bm seal_bm : bitmap)
      (values : list pair_leaf)
      : list (bytes16 × digest) :=
    match reducer_result depth tree_bm values with
    | CommitNonempty tree ⇒ [(bitmap_to_bytes16 seal_bm, eval_tree tree)]
    | _ ⇒ []
    end.

  Definition valid_bitmap_tuple
      (depth : nat) (bm : bitmap) (values : list pair_leaf) : Prop :=
    reducer_result depth bm values ≠ CommitMalformed.

  Lemma active_leaf_nodes_from_values
      next bm values nodes leftover :
    active_leaf_nodes_from next bm values = Some (nodes, leftover) →
    values = live_values nodes ++ leftover.

  Lemma active_leaf_nodes_values bm values nodes :
    active_leaf_nodes bm values = Some nodes →
    live_values nodes = values.

  Lemma active_leaf_nodes_from_same_shape
      next bm values values' nodes leftover nodes' leftover' :
    active_leaf_nodes_from next bm values = Some (nodes, leftover) →
    active_leaf_nodes_from next bm values' = Some (nodes', leftover') →
    Forall2 same_live_shape nodes nodes'.

  Lemma active_leaf_nodes_same_shape bm values values' nodes nodes' :
    active_leaf_nodes bm values = Some nodes →
    active_leaf_nodes bm values' = Some nodes' →
    Forall2 same_live_shape nodes nodes'.

  Lemma Forall2_same_live_shape_length lhs rhs :
    Forall2 same_live_shape lhs rhs →
    length lhs = length rhs.

  Lemma merge_level_values_strong nodes :
    (∀ bit, live_values (merge_level bit nodes) = live_values nodes) ∧
    (∀ bit current,
        live_values (merge_level bit (current :: nodes)) =
        live_values (current :: nodes)).

  Lemma merge_level_values bit nodes :
    live_values (merge_level bit nodes) = live_values nodes.

  Lemma reduce_levels_values fuel bit nodes :
    live_values (reduce_levels fuel bit nodes) = live_values nodes.

  Lemma merge_level_same_shape_strong nodes :
    (∀ bit nodes',
        Forall2 same_live_shape nodes nodes' →
        Forall2 same_live_shape
          (merge_level bit nodes) (merge_level bit nodes')) ∧
    (∀ bit current current' nodes',
        same_live_shape current current' →
        Forall2 same_live_shape nodes nodes' →
        Forall2 same_live_shape
          (merge_level bit (current :: nodes))
          (merge_level bit (current' :: nodes'))).

  Lemma merge_level_same_shape bit nodes nodes' :
    Forall2 same_live_shape nodes nodes' →
    Forall2 same_live_shape
      (merge_level bit nodes) (merge_level bit nodes').

  Lemma reduce_levels_same_shape fuel bit nodes nodes' :
    Forall2 same_live_shape nodes nodes' →
    Forall2 same_live_shape
      (reduce_levels fuel bit nodes)
      (reduce_levels fuel bit nodes').

  Lemma reducer_result_values depth bm values tree :
    reducer_result depth bm values = CommitNonempty tree →
    tree_values tree = values.

  Lemma reducer_result_same_shape
      depth bm values values' tree tree' :
    reducer_result depth bm values = CommitNonempty tree →
    reducer_result depth bm values' = CommitNonempty tree' →
    same_tree_shape tree tree'.

  Lemma tree_hash_inputs_contains_eval tree :
    In
      match tree with
      | TreeLeaf value ⇒ (leaf_mode, value)
      | TreeNode lhs rhs ⇒
          (merge_mode, (eval_tree lhs, eval_tree rhs))
      end
      (tree_hash_inputs tree).

  Lemma eval_tree_same_shape_no_collision
      allowed tree tree' :
    collision_free_on allowed →
    (∀ input, In input (tree_hash_inputs tree) → allowed input) →
    (∀ input, In input (tree_hash_inputs tree') → allowed input) →
    same_tree_shape tree tree' →
    eval_tree tree = eval_tree tree' →
    tree_values tree = tree_values tree'.

  Lemma eval_located_tree_same_shape_no_aligned_collision tree tree' :
    (∀ loc input input',
        In (mk_located_call loc input)
          (tree_located_calls tree) →
        In (mk_located_call loc input')
          (tree_located_calls tree') →
        call_digest input = call_digest input' →
        input = input') →
    same_located_tree_shape tree tree' →
    eval_located_tree tree = eval_located_tree tree' →
    located_tree_values tree = located_tree_values tree'.

  Definition root_inputs_for_bitmap_pair
      depth tree_bm values tree_bm' values' : list hash64_call :=
    root_hash_inputs_from_bitmaps depth tree_bm values ++
    root_hash_inputs_from_bitmaps depth tree_bm' values'.

  Definition empty_seal_inputs_for_bitmap_pair
      depth tree_bm seal_bm values tree_bm' seal_bm' values'
      : list bytes16 :=
    root_empty_seal_inputs_from_bitmaps depth tree_bm seal_bm values ++
    root_empty_seal_inputs_from_bitmaps depth tree_bm' seal_bm' values'.

  Definition nonempty_seal_inputs_for_bitmap_pair
      depth tree_bm seal_bm values tree_bm' seal_bm' values'
      : list (bytes16 × digest) :=
    root_nonempty_seal_inputs_from_bitmaps depth tree_bm seal_bm values ++
    root_nonempty_seal_inputs_from_bitmaps depth tree_bm' seal_bm' values'.

  Definition seal_empty_collision_free_on
      (allowed : bytes16 → Prop) : Prop :=
    ∀ lhs rhs,
      allowed lhs →
      allowed rhs →
      seal_empty lhs = seal_empty rhs →
      lhs = rhs.

  Definition seal_nonempty_collision_free_on
      (allowed : (bytes16 × digest) → Prop) : Prop :=
    ∀ lhs rhs,
      allowed lhs →
      allowed rhs →
      seal_nonempty (fst lhs) (snd lhs) =
      seal_nonempty (fst rhs) (snd rhs) →
      lhs = rhs.

  Definition seal_empty_nonempty_disjoint_on
      (allowed_empty : bytes16 → Prop)
      (allowed_nonempty : (bytes16 × digest) → Prop) : Prop :=
    ∀ empty_input nonempty_input,
      allowed_empty empty_input →
      allowed_nonempty nonempty_input →
      seal_empty empty_input ≠
      seal_nonempty (fst nonempty_input) (snd nonempty_input).

  Theorem Root_from_bitmaps_injective_no_collision
      depth tree_bm seal_bm values tree_bm' seal_bm' values' :
    valid_bitmap_tuple depth tree_bm values →
    valid_bitmap_tuple depth tree_bm' values' →
    valid_seal_bitmap seal_bm →
    valid_seal_bitmap seal_bm' →
    (seal_bm = seal_bm' → tree_bm = tree_bm') →
    collision_free_on
      (fun input ⇒
         In input
           (root_inputs_for_bitmap_pair depth tree_bm values tree_bm' values')) →
    seal_empty_collision_free_on
      (fun input ⇒
         In input
           (empty_seal_inputs_for_bitmap_pair
              depth tree_bm seal_bm values tree_bm' seal_bm' values')) →
    seal_nonempty_collision_free_on
      (fun input ⇒
         In input
           (nonempty_seal_inputs_for_bitmap_pair
              depth tree_bm seal_bm values tree_bm' seal_bm' values')) →
    seal_empty_nonempty_disjoint_on
      (fun input ⇒
         In input
           (empty_seal_inputs_for_bitmap_pair
              depth tree_bm seal_bm values tree_bm' seal_bm' values'))
      (fun input ⇒
         In input
           (nonempty_seal_inputs_for_bitmap_pair
              depth tree_bm seal_bm values tree_bm' seal_bm' values')) →
    Root_from_bitmaps depth tree_bm seal_bm values =
    Root_from_bitmaps depth tree_bm' seal_bm' values' →
    seal_bm = seal_bm' ∧ tree_bm = tree_bm' ∧ values = values'.

  Theorem Root_from_bitmaps_distinct_no_collision
      depth tree_bm seal_bm values tree_bm' seal_bm' values' :
    valid_bitmap_tuple depth tree_bm values →
    valid_bitmap_tuple depth tree_bm' values' →
    valid_seal_bitmap seal_bm →
    valid_seal_bitmap seal_bm' →
    (seal_bm = seal_bm' → tree_bm = tree_bm') →
    collision_free_on
      (fun input ⇒
         In input
           (root_inputs_for_bitmap_pair depth tree_bm values tree_bm' values')) →
    seal_empty_collision_free_on
      (fun input ⇒
         In input
           (empty_seal_inputs_for_bitmap_pair
              depth tree_bm seal_bm values tree_bm' seal_bm' values')) →
    seal_nonempty_collision_free_on
      (fun input ⇒
         In input
           (nonempty_seal_inputs_for_bitmap_pair
              depth tree_bm seal_bm values tree_bm' seal_bm' values')) →
    seal_empty_nonempty_disjoint_on
      (fun input ⇒
         In input
           (empty_seal_inputs_for_bitmap_pair
              depth tree_bm seal_bm values tree_bm' seal_bm' values'))
      (fun input ⇒
         In input
           (nonempty_seal_inputs_for_bitmap_pair
              depth tree_bm seal_bm values tree_bm' seal_bm' values')) →
    (seal_bm, values) ≠ (seal_bm', values') →
    Root_from_bitmaps depth tree_bm seal_bm values ≠
    Root_from_bitmaps depth tree_bm' seal_bm' values'.

  Definition root_hash_inputs (slots : slot_values) : list hash64_call :=
    match value_tree_from_slots slots with
    | None ⇒ []
    | Some tree ⇒ tree_hash_inputs tree
    end.

  Definition root_inputs_for_pair
      (slots slots' : slot_values) : list hash64_call :=
    root_hash_inputs slots ++ root_hash_inputs slots'.

  Definition empty_seal_inputs (slots : slot_values) : list bytes16 :=
    match value_tree_from_slots slots with
    | None ⇒ [bitmap_to_bytes16 (slot_bitmap slots)]
    | Some _ ⇒ []
    end.

  Definition empty_seal_inputs_for_pair
      (slots slots' : slot_values) : list bytes16 :=
    empty_seal_inputs slots ++ empty_seal_inputs slots'.

  Definition nonempty_seal_inputs
      (slots : slot_values) : list (bytes16 × digest) :=
    match value_tree_from_slots slots with
    | None ⇒ []
    | Some tree ⇒
        [(bitmap_to_bytes16 (slot_bitmap slots), eval_tree tree)]
    end.

  Definition nonempty_seal_inputs_for_pair
      (slots slots' : slot_values) : list (bytes16 × digest) :=
    nonempty_seal_inputs slots ++ nonempty_seal_inputs slots'.

  Definition located_aligned_collision
      (call call' : located_call) : Prop :=
    located_call_loc call = located_call_loc call' ∧
    located_call_input call ≠ located_call_input call' ∧
    call_digest (located_call_input call) =
    call_digest (located_call_input call').

  Definition digest_eq_dec
      (lhs rhs : digest) : {lhs = rhs} + {lhs ≠ rhs} :=
    decide (lhs = rhs).

  Definition located_aligned_collision_dec call call' :
    {located_aligned_collision call call'} +
    {¬ located_aligned_collision call call'}.

  Fixpoint list_exists_sig_dec {A : Type}
      (P : A → Prop)
      (P_dec : ∀ value, {P value} + {¬ P value})
      (values : list A)
      : {value : A & In value values ∧ P value} +
        {¬ ∃ value, In value values ∧ P value}.

  Definition aligned_collision_calls
      (calls calls' : list located_call) : Prop :=
    ∃ call call',
      In call calls ∧
      In call' calls' ∧
      located_aligned_collision call call'.

  Definition aligned_collision_calls_witness
      (calls calls' : list located_call) : Type :=
    {call : located_call &
      {call' : located_call &
        In call calls ∧
        In call' calls' ∧
        located_aligned_collision call call'}}.

  Fixpoint aligned_collision_calls_sig_dec calls calls' :
    aligned_collision_calls_witness calls calls' +
    {¬ aligned_collision_calls calls calls'}.

  Definition aligned_collision_calls_dec calls calls' :
    {aligned_collision_calls calls calls'} +
    {¬ aligned_collision_calls calls calls'}.

  Lemma exists_aligned_collision_iff_calls trace trace' :
    exists_aligned_collision trace trace' ↔
    aligned_collision_calls
      trace.(traced_calls)
      trace'.(traced_calls).

  Definition exists_aligned_collision_dec trace trace' :
    {exists_aligned_collision trace trace'} + {¬ exists_aligned_collision trace trace'}.

This corollary-facing predicate is just the negation of the bad event in the main extractor theorem. It lives in the proof section because the Section 2 statement only needs the positive collision event.
  Definition no_aligned_collisions
      (trace trace' : root_trace) : Prop :=
    ¬ exists_aligned_collision trace trace'.

  Lemma no_aligned_collisions_pointwise trace trace' :
    no_aligned_collisions trace trace' →
    ∀ loc input input',
      In (mk_located_call loc input)
        trace.(traced_calls) →
      In (mk_located_call loc input')
        trace'.(traced_calls) →
      call_digest input = call_digest input' →
      input = input'.

  Theorem Root_injective_no_collision slots slots' :
    no_aligned_collisions
      (root_with_trace slots)
      (root_with_trace slots') →
    root slots = root slots' →
    normalize_slots slots = normalize_slots slots'.
This is the main security theorem: every binding break produces an aligned collision in the two traced computations. The proof searches the two finite traces with exists_aligned_collision_dec. If no bad pair exists, no_aligned_collisions_pointwise turns that absence into the local rule needed to push root equality through the seal and tree locations, forcing the normalized page views to agree and contradicting distinctness.
  Theorem Root_binding_break_extracts_aligned_collision slots slots' :
    (root_with_trace slots).(traced_root) =
    (root_with_trace slots').(traced_root) →
    normalize_slots slots ≠ normalize_slots slots' →
    exists_aligned_collision (root_with_trace slots) (root_with_trace slots').

The no-collision theorem is a corollary of the extractor. It is the form a caller usually wants after separately assuming that the compared traces contain no aligned collision.
  Theorem Root_distinct_no_collision slots slots' :
    no_aligned_collisions
      (root_with_trace slots)
      (root_with_trace slots') →
    normalize_slots slots ≠ normalize_slots slots' →
    root slots ≠ root slots'.
End CorrectnessProof.
This page has been generated by coqdoc