Loading concrete fusion-node parameters

The representation below consists entirely of literal memory equalities. It supplies no query result or execution assumption. The complete eighteen-word header load is charged.

Main definitions

• NodeProgram.Rep: actual parameter words and interleaved full keys in RAM.
• NodeProgram.Ready: loaded header, original query and address, and unchanged key table.

Main results

• NodeProgram.exec_readHeader: all header words are loaded in 55 instructions.

References

• [FW93]

structure Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.Rep {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (a : ℕ) (mem : ℕ → ℕ) : Prop

Literal representation of an internal node's occupancy, fifteen parameters and full-key minima. The unused tag, cached minimum and child pointers are read or skipped as appropriate; they carry no query oracle. This is a projection of the contiguous tree representation.

• count_eq : mem (a + 1) = n

  Actual occupancy at header offset one.

• words_eq (j : Fin 15) : mem (a + 3 + ↑j) = p.words j

  Actual fifteen preprocessing words at offsets three through seventeen.

• keys_eq (i : Fin n) : mem (a + 18 + ↑i * 2) = keys i

  Full-key minima in the interleaved child table.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.rep_of_tree {w a m : ℕ} {cs : List Lean.FusionTree.Tree} {parameters : Parameters} {mem : ℕ → ℕ} (p : NodeParameters w fun (i : Fin cs.length) => cs[i].minimum) (hr : FusionTree.Rep parameters (Lean.FusionTree.Tree.node m cs) a mem) (hp : parameters (Lean.FusionTree.Tree.node m cs) = p.words) : Rep p a mem

The node contract is a literal projection of the contiguous tree representation. Only equality with the actual stored parameter words is required.

structure Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.Ready {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (q a : ℕ) (x : WordRAM.Data registers) : Prop

Loaded parameters and original inputs, with the actual full-key table.

• prepared : Prepared p x

  Actual loaded header.

• query_eq : x.regs query = q

  Original query.

• pointer_eq : x.regs pointer = a

  Original record base.

• keys_eq (i : Fin n) : x.mem (a + 18 + ↑i * 2) = keys i

  Actual stride-two full-key table.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.Ready.frame {w n q a : ℕ} {keys : Fin n → ℕ} {p : NodeParameters w keys} {x y : WordRAM.Data registers} (hx : Ready p q a x) (hf : Frame x y) : Ready p q a y

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.Ready.set_scratch {w n q a : ℕ} {keys : Fin n → ℕ} {p : NodeParameters w keys} {x : WordRAM.Data registers} (hx : Ready p q a x) (i : Fin registers) (v : ℕ) (hlo : 2 ≤ ↑i) (hhi : ↑i < 10) : Ready p q a (x.set i v)

Scratch register updates preserve the original inputs and loaded node data.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.Ready.except_scratch {w n q a : ℕ} {keys : Fin n → ℕ} {p : NodeParameters w keys} {x y : WordRAM.Data registers} (hx : Ready p q a x) (i : Fin registers) (hlo : 2 ≤ ↑i) (hhi : ↑i < 10) (hm : y.mem = x.mem) (hp : ∀ (j : Fin registers), ↑j < 40 → j ≠ i → y.regs j = x.regs j) : Ready p q a y

A subroutine may return through one caller scratch register while framing the rest.

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.readHeader : WordRAM.Code WordRAM.Basis.standard registers

Copy the base pointer, then perform the actual eighteen-word header load.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_readHeader {w n q a : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (x : WordRAM.Data registers) (hr : Rep p a x.mem) (ha : WordRAM.Fits w (a + 17)) (hxq : x.regs query = q) (hxa : x.regs pointer = a) : ∃ (y : WordRAM.Data registers), WordRAM.Exec w readHeader x y 55 ∧ Ready p q a y ∧ y.mem = x.mem

Header loading takes 55 actual instructions and preserves memory and both inputs.