Actual preprocessed-node calls from traversal #
The large-width routine receives the parameters actually stored by parameterWords.
The small-width routine receives exactly two children, as forced by the branching rule.
Neither branch assumes a node oracle. Both frame the caller's persistent registers.
Main results #
QueryProgram.exec_node: inclusive full-key rank, in at most 201000 instructions.
References #
theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.Entry.frame {q p : ℕ} {x y : WordRAM.Data registers} (hx : Entry q p x) (hq : y.regs query = q) (hp : y.regs pointer = p) (hf : ∀ (i : Fin registers), 31 ≤ ↑i → ↑i < 39 → y.regs i = x.regs i) :
Entry q p y
A node call may alter scratch registers but frames all persistent traversal data.
theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.node_rep {w m p : ℕ} {cs : List Lean.FusionTree.Tree} {mem : ℕ → ℕ} (he : ParameterEligible w cs) (hr : Rep (parameterWords w) (Lean.FusionTree.Tree.node m cs) p mem) :
NodeProgram.Rep (NodeParameters.choose ⋯ ⋯ ⋯ ⋯ ⋯) p mem
Whole-tree representation projects to the exact chosen fusion-node witness.
theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.exec_node {w q p m : ℕ} {cs : List Lean.FusionTree.Tree} {x : WordRAM.Data registers} (hx : Entry q p x) (ht : Lean.FusionTree.Tree.Valid (Lean.FusionTree.branching w) (Lean.FusionTree.Tree.node m cs)) (hs : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (Lean.FusionTree.Tree.node m cs).keys) (hk : ∀ k ∈ (Lean.FusionTree.Tree.node m cs).keys, WordRAM.Fits w k) (hr : Rep (parameterWords w) (Lean.FusionTree.Tree.node m cs) p x.mem) (ha : ArenaFits w p (Lean.FusionTree.Tree.node m cs)) (hq : WordRAM.Fits w q) :
∃ (y : WordRAM.Data registers),
WordRAM.ExecWithin w (node w) x y 201000 ∧ y.regs rank = Lean.FusionTree.upperRank (childMinima cs) q ∧ y.mem = x.mem ∧ Entry q p y
Both actual node implementations return full-key inclusive rank. All preprocessing is derived from the real tree, with constant words and the entire arena fitting explicitly. The instruction bound includes the whole selected node call, with no assumed oracle.