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.registers, NodeProgram.query, NodeProgram.pointer, NodeProgram.out, NodeProgram.argument, NodeProgram.cut, NodeProgram.zero, NodeProgram.chosen, NodeProgram.divergence, NodeProgram.position: physical register count and caller registers.
• NodeProgram.bank, NodeProgram.headerBank, NodeProgram.compressBank, NodeProgram.rankBank, NodeProgram.neighborBank, NodeProgram.boundaryBank, NodeProgram.parameter, NodeProgram.count: contiguous subroutine register banks and header register indices.
• NodeProgram.Frame: memory and registers below forty are unchanged by a subroutine.
• NodeProgram.moves, NodeProgram.moved: charged register copies, with a terminal self-copy, and their resulting state.
• 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)

Contiguous register embeddings are injective.

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

Frame is reflexive.

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

Frame is transitive.

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)

Updating a register at index at least 40 preserves Frame.

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)

Extending a subroutine state into a register bank at offset at least 40 preserves Frame.

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

The instruction count of moves xs is 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)

Executing moves xs reaches moved xs x in xs.length + 1 steps.

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)

Register copies whose destinations are at index at least 40 preserve Frame.

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

The Prepared header invariant is preserved across Frame transitions.

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.