Actual full-key neighbor loads

The key table begins eighteen words after the record base and has stride two. Its second word in each entry is a child pointer; this subroutine reads the full-key minima only. All constants, address calculations, copies and both loads are charged.

Main results

• NodeProgram.exec_neighbors: select a minimum-exclusive-or sketch neighbor in 25 instructions.

References

• [FW93]

def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.neighborInputs : List (Fin registers × Fin registers)

Registers copied before the two actual full-key loads.

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

Load the table offset and stride, charging address addition as well.

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

Caller setup followed by the checked two-neighbor program.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_neighbors {w n q a : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hn : 0 < n) (hs : StrictMono keys) (hk : ∀ (i : Fin n), keys i < 2 ^ w) (hnB : n ≤ Lean.FusionTree.branching w) (hlarge : 9 ≤ Nat.log 2 w) (x : WordRAM.Data registers) (hx : Prepared p x) (hq : WordRAM.Fits w q) (hxq : x.regs query = q) (hxa : x.regs pointer = a) (hxt : x.regs cut = Lean.FusionTree.sketchRank w keys q) (ha : WordRAM.Fits w (a + 18 + (n - 1) * 2)) (hkeys : ∀ (i : Fin n), x.mem (a + 18 + ↑i * 2) = keys i) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w neighbors x y 25 ∧ Frame x y ∧ ∃ (j : Fin n), y.regs (neighborBank 14) = keys j ∧ y.regs (neighborBank 15) = keys j ^^^ q ∧ Lean.FusionTree.IsSketchNeighbor w keys q j ∧ ∀ (i : Fin n), Lean.FusionTree.IsSketchNeighbor w keys q i → keys j ^^^ q ≤ keys i ^^^ q

The output key and its exclusive or are selected from actual stride-two memory loads. The only representation premise is the literal full-key table, with explicit address bounds.