Checked pointer-chasing fusion-tree descent

Each iteration reads a tag, compares a leaf or runs an actual node query, and either stops or loads a child pointer. The proof descends through the represented tree; every followed child has smaller height. No execution or correctness assumption is hidden in the invariant.

Main definitions

• QueryProgram.Done: postcondition for a stopped fusion-tree traversal.

Main results

• QueryProgram.exec_loop: inclusive predecessor in at most 201022 * (height + 1) + 2 instructions, with all RAM memory and query preserved.

References

• M. L. Fredman and D. E. Willard, Surpassing the information theoretic bound with fusion trees

structure Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.Done (q : ℕ) (ans : Option ℕ) (mem : ℕ → ℕ) (y : WordRAM.Data registers) : Prop

A stopped traversal returns a conventional option and preserves the original RAM/query.

• active_eq : y.regs active = 0
• zero_eq : y.regs zero = 0
• mem_eq : y.mem = mem
• query_eq : y.regs query = q
• found_le : y.regs found ≤ 1
• answer_eq : answer y = ans

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.exec_loop {w q p : ℕ} {t : Lean.FusionTree.Tree} {x : WordRAM.Data registers} (hx : Entry q p x) (ht : Lean.FusionTree.Tree.Valid (Lean.FusionTree.branching w) t) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) t.keys) (hk : ∀ k ∈ t.keys, WordRAM.Fits w k) (hr : Rep (parameterWords w) t p x.mem) (ha : ArenaFits w p t) (hq : WordRAM.Fits w q) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (loop w) x y (201022 * (t.height + 1) + 2) ∧ Done q (Lean.FusionTree.Tree.predecessor q t) x.mem y

The traversal bound uses the actual tree height, including the final leaf visit.