Register banks for fusion-node queries

The query uses a fixed register file. Header, compression, rank, neighbor, boundary, and multiword highest-bit workspaces occupy disjoint intervals. Explicit copies connect them.

Main definitions

• NodeProgram.Frame: memory and registers below forty are unchanged by a subroutine.
• NodeProgram.moves: charged register copies, with a terminal self-copy.
• NodeProgram.Prepared: the actual eighteen loaded header words supply node parameters.

References

• [FW93]

@[reducible, inline]

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

Fixed physical register count, independent of width and node occupancy.

@[reducible, inline]

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

Original bounded query.

@[reducible, inline]

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

Original record address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.out : Fin registers

Final full-key inclusive rank.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.argument : Fin registers

Full word to compress, and later the compressed result.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.cut : Fin registers

Initial inclusive sketch rank.

@[reducible, inline]

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

Constant zero for control flow.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.chosen : Fin registers

Selected full key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.divergence : Fin registers

Exclusive or of the selected full key and original query.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.position : Fin registers

Highest differing position on a miss.

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.bank {k : ℕ} (offset : ℕ) (hk : offset + k ≤ registers) (i : Fin k) : Fin registers

A contiguous register embedding.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.bank_injective {k offset : ℕ} (hk : offset + k ≤ registers) : Function.Injective (bank offset hk)

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.preserves_rename {k : ℕ} {f : Fin k → Fin registers} (c : WordRAM.Code WordRAM.Basis.standard k) (i : Fin registers) (hi : ∀ (j : Fin k), f j ≠ i) : WordRAM.Code.Preserves i (WordRAM.Code.rename f c)

A renamed subroutine cannot write a register outside its embedding. This proof treats the subroutine structurally and does not expand its instruction graph.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.preserves_bank {k offset : ℕ} (hk : offset + k ≤ registers) (c : WordRAM.Code WordRAM.Basis.standard k) (i : Fin registers) (hi : ↑i < offset ∨ offset + k ≤ ↑i) : WordRAM.Code.Preserves i (WordRAM.Code.rename (bank offset hk) c)

In particular, a contiguous bank frames every physical register outside its interval.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.headerBank : Fin 21 → Fin registers

Eighteen-word header reader, including its pointer and address scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.compressBank : Fin 21 → Fin registers

Compression workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.rankBank : Fin 10 → Fin registers

Inclusive or strict rank workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.neighborBank : Fin 17 → Fin registers

Two-neighbor loader and selector.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.boundaryBank : Fin 10 → Fin registers

Correction boundaries.

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.parameter (j : Fin 15) : Fin registers

Header register holding one of the fifteen stored preprocessing words.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.count : Fin registers

Header register holding occupancy.

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.Frame (x y : WordRAM.Data registers) : Prop

Memory and caller registers below forty agree. The direction follows execution.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.Frame.refl (x : WordRAM.Data registers) : Frame x x

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.Frame.trans {x y z : WordRAM.Data registers} (hxy : Frame x y) (hyz : Frame y z) : Frame x z

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.frame_set (x : WordRAM.Data registers) (i : Fin registers) (v : ℕ) (hi : 40 ≤ ↑i) : Frame x (x.set i v)

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.frame_extend {k offset : ℕ} (hk : offset + k ≤ registers) (ho : 40 ≤ offset) (x : WordRAM.Data registers) (y : WordRAM.Data k) (hm : y.mem = x.mem) : Frame x (WordRAM.Data.extend (bank offset hk) y x)

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.moves : List (Fin registers × Fin registers) → WordRAM.Code WordRAM.Basis.standard registers

Copy a finite sequence of registers, charging also a final self-copy of register 39. The final self-copy supplies an executable empty sequence without a special RAM primitive.

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.moved (xs : List (Fin registers × Fin registers)) (x : WordRAM.Data registers) : WordRAM.Data registers

Exact result of the charged copies.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.size_moves (xs : List (Fin registers × Fin registers)) : (moves xs).size = xs.length + 1

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_moves (w : ℕ) (xs : List (Fin registers × Fin registers)) (x : WordRAM.Data registers) : WordRAM.Exec w (moves xs) x (moved xs x) (xs.length + 1)

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.frame_moved (xs : List (Fin registers × Fin registers)) (x : WordRAM.Data registers) (hs : ∀ p ∈ xs, 40 ≤ ↑p.1) : Frame x (moved xs x)

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

Literal values loaded from the actual header. This is a register contract, with no correctness, execution, or rank oracle among its fields.

• count_eq : x.regs count = n

  Actual occupancy word.

• words_eq (j : Fin 15) : x.regs (parameter j) = p.words j

  Actual fifteen parameter words.

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

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.Prepared.set_low {w n : ℕ} {keys : Fin n → ℕ} {p : NodeParameters w keys} {x : WordRAM.Data registers} (hx : Prepared p x) (i : Fin registers) (v : ℕ) (hi : ↑i < 10) : Prepared p (x.set i v)

Caller scratch registers zero through nine are disjoint from the loaded header.