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 results

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

References

• [FW93]

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.Entry.running {q p : ℕ} {x : WordRAM.Data registers} (hx : Entry q p x) : (WordRAM.Cond.lt zero active).Holds x

The loop condition holds at entry.

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.Done.stopped {q : ℕ} {ans : Option ℕ} {mem : ℕ → ℕ} {y : WordRAM.Data registers} (hy : Done q ans mem y) : ¬(WordRAM.Cond.lt zero active).Holds y

The loop condition fails after completion.

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.exec_loop_height (h : ℕ) {w q p : ℕ} {t : Lean.FusionTree.Tree} {x : WordRAM.Data registers} (hheight_bound : t.height ≤ h) (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 * (h + 1) + 2) ∧ Done q (Lean.FusionTree.Tree.predecessor q t) x.mem y

Complete loop execution from real preprocessed RAM. Every iteration costs at most 201020 instructions and there are at most height + 1 iterations; loop tests and jumps are charged too. The pointer may change, while all memory and the query are preserved.

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.