Actual fusion-tree traversal instructions

The traversal uses eight caller registers, disjoint from both node routines. A width-indexed choice of node code is made at compilation. The stored tree, its keys and its query remain runtime inputs. Leaves return an option as a presence flag and a full-key value.

Main definitions

• QueryProgram.code: initialization followed by pointer-chasing descent.
• QueryProgram.answer: the conventional two-register option encoding.

Main results

• QueryProgram.exec_leaf: literal leaf loads and inclusive full-key comparison.
• QueryProgram.exec_follow: the actual stride-two child-pointer load.

References

• [FW93]

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.registers : ℕ

Both node subroutines use the same fixed register file.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.query : Fin registers

Query key, preserved throughout traversal.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.pointer : Fin registers

Current record pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.rank : Fin registers

Inclusive rank returned by either node routine.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.active : Fin registers

Loop flag.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.found : Fin registers

Answer presence flag.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.value : Fin registers

Answer full key, zero on absence.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.one : Fin registers

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.zero : Fin registers

Constant zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.address : Fin registers

Address scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.tag : Fin registers

Record tag, then leaf key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.offset : Fin registers

Leaf presence or child-table offset.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.answer (x : WordRAM.Data registers) : Option ℕ

Conventional presence/value representation, including key zero.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.setup : WordRAM.Code WordRAM.Basis.standard registers

Constant-register installation is part of the charged query.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.leaf : WordRAM.Code WordRAM.Basis.standard registers

Inspect a literal leaf record; comparison is inclusive at equality.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.follow : WordRAM.Code WordRAM.Basis.standard registers

Positive rank r selects pointer entry p + 19 + 2(r-1).

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.node (w : ℕ) : WordRAM.Code WordRAM.Basis.standard registers

Code selection depends only on the physical word width.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.internal (w : ℕ) : WordRAM.Code WordRAM.Basis.standard registers

Zero rank terminates with absence; positive rank follows an actual stored pointer.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.body (w : ℕ) : WordRAM.Code WordRAM.Basis.standard registers

One traversal iteration first loads the current record tag.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.loop (w : ℕ) : WordRAM.Code WordRAM.Basis.standard registers

Descent terminates at a leaf or a zero child rank.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.code (w : ℕ) : WordRAM.Code WordRAM.Basis.standard registers

Actual width-indexed query code, with initialization included.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.program (w : ℕ) : WordRAM.Program WordRAM.Basis.standard registers

Flat query program; it halts with the value register, with presence retained in found.

structure Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.Entry (q p : ℕ) (x : WordRAM.Data registers) : Prop

Persistent registers before visiting a record. No scratch-register assumptions occur.

• query_eq : x.regs query = q
• pointer_eq : x.regs pointer = p
• active_eq : x.regs active = 1
• found_eq : x.regs found = 0
• value_eq : x.regs value = 0
• one_eq : x.regs one = 1
• zero_eq : x.regs zero = 0

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.initialized (x : WordRAM.Data registers) : WordRAM.Data registers

Initialization data, with arbitrary preexisting workspace and memory.

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.exec_initialize {w : ℕ} (x : WordRAM.Data registers) (hw : WordRAM.Fits w 1) : WordRAM.Exec w setup x (initialized x) 5 ∧ Entry (x.regs query) (x.regs pointer) (initialized x)

Five charged constant instructions establish all traversal constants.

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.Entry.set_scratch {q p : ℕ} {x : WordRAM.Data registers} (hx : Entry q p x) (i : Fin registers) (hi : 36 ≤ ↑i) (hi' : ↑i ≤ 38) (v : ℕ) : Entry q p (x.set i v)

Updating traversal scratch preserves the entry invariant.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.leafResult (x : WordRAM.Data registers) (p q : ℕ) : WordRAM.Data registers

Exact literal leaf execution data.

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.exec_leaf {w q p : ℕ} {x : WordRAM.Data registers} (hx : Entry q p x) (ha : WordRAM.Fits w (p + 2)) : WordRAM.ExecWithin w leaf x (leafResult x p q) 12

Charged presence/key loads and comparisons need at most twelve instructions.

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.leafResult_spec {q p : ℕ} {x : WordRAM.Data registers} (hx : Entry q p x) : (leafResult x p q).regs active = 0 ∧ (leafResult x p q).regs zero = 0 ∧ (leafResult x p q).mem = x.mem ∧ (leafResult x p q).regs query = q ∧ (leafResult x p q).regs found ≤ 1 ∧ answer (leafResult x p q) = if x.mem (p + 1) = 0 ∨ q < x.mem (p + 2) then none else some (x.mem (p + 2))

Leaf execution stops, preserves memory and query, and returns a canonical option.

def Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.followResult (x : WordRAM.Data registers) (p r : ℕ) : WordRAM.Data registers

Literal register updates and load for the selected child pointer.

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.exec_follow {w q p r : ℕ} {x : WordRAM.Data registers} (hx : Entry q p x) (hr : x.regs rank = r) (ha : WordRAM.Fits w (p + 19 + 2 * (r - 1))) : WordRAM.Exec w follow x (followResult x p r) 6

Six real instructions compute and load the interleaved pointer.

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.followResult_entry {q p r : ℕ} {x : WordRAM.Data registers} (hx : Entry q p x) : Entry q (x.mem (p + 19 + 2 * (r - 1))) (followResult x p r)

Following a child preserves the invariant, changing only the current record address.

theorem Cslib.Algorithms.WordRAM.FusionTree.QueryProgram.followResult_mem (x : WordRAM.Data registers) (p r : ℕ) : (followResult x p r).mem = x.mem

Child-pointer traversal has no memory writes.