Loading and selecting sketch neighbors

An inclusive sketch cut has at most two neighboring full keys. Clamp the two indices to a nonempty array, load both keys, and compare their exclusive or with the query. Clamping allows the same bounded program to handle cuts at either end of the array.

Main definitions

• NeighborProgram.code: load two full keys and choose the smaller exclusive or.

Main results

• NeighborProgram.exec: checked execution in at most eighteen instructions.

References

• Fredman and Willard, Surpassing the information theoretic bound with fusion trees.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.query : Fin 17

Query word, preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.cut : Fin 17

Inclusive sketch cut, preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.count : Fin 17

Nonzero node occupancy, preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.base : Fin 17

Address of the first full key, preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.stride : Fin 17

Distance between full keys, preserved.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.one : Fin 17

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.leftIndex : Fin 17

Clamped predecessor index.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.rightIndex : Fin 17

Clamped successor index.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.excess : Fin 17

Clamping scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.address : Fin 17

Memory address scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.leftKey : Fin 17

First candidate key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.rightKey : Fin 17

Second candidate key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.leftXor : Fin 17

First candidate's exclusive or with the query.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.rightXor : Fin 17

Second candidate's exclusive or with the query.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.chosen : Fin 17

Selected key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.divergence : Fin 17

Selected key's exclusive or with the query.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.index : Fin 17

Selected array index.

def Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.left (t : ℕ) : ℕ

Clamped predecessor position.

def Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.right (n t : ℕ) : ℕ

Clamped successor position, expressed using two saturating subtractions.

theorem Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.indices_lt {n t : ℕ} (hn : 0 < n) (ht : t ≤ n) : left t < n ∧ right n t < n

theorem Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.indices_neighbors {n t : ℕ} (hn : 0 < n) (ht : t ≤ n) : (left t + 1 = t ∨ left t = t) ∧ (right n t + 1 = t ∨ right n t = t)

Exactly one of the two optional sketch neighbors is repeated at an end cut.

def Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.selectIndex (score : ℕ → ℕ) (n t : ℕ) : ℕ

Index selected by the comparison in code.

theorem Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.selectIndex_spec (score : ℕ → ℕ) {n t : ℕ} (hn : 0 < n) (ht : t ≤ n) : selectIndex score n t < n ∧ (selectIndex score n t + 1 = t ∨ selectIndex score n t = t) ∧ ∀ i < n, i + 1 = t ∨ i = t → score (selectIndex score n t) ≤ score i

The clamped comparison chooses a valid neighbor of minimum score among all neighbors of the cut. At either end the repeated candidate causes no exception.

def Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.code : WordRAM.Code WordRAM.Basis.standard 17

Thirteen instructions load the candidates. Selection adds four or five instructions, including control flow, and prefers the left candidate when exclusive-or values tie.

def Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.loaded (x : WordRAM.Data 17) (q n t a d : ℕ) : WordRAM.Data 17

State after loading, before the one comparison selecting a candidate.

def Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.result (x : WordRAM.Data 17) (q n t a d : ℕ) : WordRAM.Data 17

Final state, choosing the smaller full-word exclusive or.

theorem Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.result_spec (x : WordRAM.Data 17) (q n t a d : ℕ) : have j := selectIndex (fun (i : ℕ) => x.mem (a + i * d) ^^^ q) n t; (result x q n t a d).regs index = j ∧ (result x q n t a d).regs chosen = x.mem (a + j * d) ∧ (result x q n t a d).regs divergence = x.mem (a + j * d) ^^^ q

The returned key, exclusive-or value, and index describe the same selected array entry.

theorem Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.result_sketchNeighbor {w n q a d : ℕ} (x : WordRAM.Data 17) (keys : Fin n → ℕ) (hn : 0 < n) (hkeys : ∀ (i : Fin n), x.mem (a + ↑i * d) = keys i) : ∃ (j : Fin n), (result x q n (Lean.FusionTree.sketchRank w keys q) a d).regs index = ↑j ∧ (result x q n (Lean.FusionTree.sketchRank w keys q) a d).regs chosen = keys j ∧ (result x q n (Lean.FusionTree.sketchRank w keys q) a d).regs divergence = 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

With an actual sketch cut and an encoded full-key array, the output identifies a sketch neighbor with minimum exclusive-or value among the neighbors. No full-key scan supplies the answer. The statement is separate from the checked execution and can be composed with it.

theorem Cslib.Algorithms.WordRAM.FusionTree.NeighborProgram.exec {w q n t a d : ℕ} (x : WordRAM.Data 17) (hn : 0 < n) (ht : t ≤ n) (hq : WordRAM.Fits w q) (hnfit : WordRAM.Fits w n) (ha : WordRAM.Fits w (a + (n - 1) * d)) (hkeys : ∀ i < n, WordRAM.Fits w (x.mem (a + i * d))) (hxq : x.regs query = q) (hxt : x.regs cut = t) (hxn : x.regs count = n) (hxa : x.regs base = a) (hxd : x.regs stride = d) : WordRAM.ExecWithin w code x (result x q n t a d) 18 ∧ (result x q n t a d).mem = x.mem

Loading two clamped neighbors and selecting one takes at most eighteen actual checked instructions. The address premise covers the last array key; every accessed address and intermediate product lies below it. The query, cut, occupancy, base, stride, and memory are preserved. Constant preparation and the sketch cut itself are separate.