Documentation

Complexity.Algorithms.WordRAM.FusionTree.Node.Initial

First fusion-node query and full-key selection #

The first sketch query obtains a cut. Two full-key loads then select a neighboring key by exclusive or. The original query and record address remain available for correction.

Main results #

References #

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

Copy the selected full key and exclusive or, and initialize the branch's zero register.

Instances For
    source
    def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.initial :
    WordRAM.Code WordRAM.Basis.standard registers

    Initial compression, inclusive sketch cut, and the two full-key neighbor loads.

    Instances For
      source
      theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_initial {w n q a : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hw : 2 ≤ w) (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 : Ready p q a x) (hq : WordRAM.Fits w q) (ha : WordRAM.Fits w (a + 18 + (n - 1) * 2)) :
      ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w initial x y 149 ∧ Ready p q a y ∧ y.mem = x.mem ∧ y.regs cut = Lean.FusionTree.sketchRank w keys q ∧ y.regs zero = 0 ∧ ∃ (j : Fin n), y.regs chosen = keys j ∧ y.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

      A concrete first query produces a genuine minimum-exclusive-or sketch neighbor. All setup and copies are charged; memory and original inputs are preserved.