Documentation

Complexity.Algorithms.WordRAM.FusionTree.Node

Constant-time full-key fusion-node queries #

This width-indexed standard-basis RAM program returns the true inclusive rank of every bounded query in a sorted internal node. Its constants are actual preprocessing witnesses, loaded from the contiguous eighteen-word header. The program charges header loads, all register transfers, both stride-two full-key neighbor loads, multiword highest-bit arithmetic, and the second compression and rank. Memory and the original query and pointer are preserved.

The large-width branch assumes 2 ≤ n ≤ branching w and 9 ≤ Nat.log 2 w. Leaves, small-width binary nodes and tree traversal are separate. No preprocessing-time bound is claimed. No correctness or execution oracle is a parameter of the representation.

Main definitions #

Main results #

References #

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

The zero query bit needs a strict upper-boundary rank; the one bit needs an inclusive lower-boundary rank. Both calls include query compression and all transfers.

Instances For
    source
    def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.correction (w : ℕ) :
    WordRAM.Code WordRAM.Basis.standard registers

    On a miss, compute the highest differing bit and query its sibling boundary.

    Instances For
      source
      def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.finish (w : ℕ) :
      WordRAM.Code WordRAM.Basis.standard registers

      Exact hits return the first cut. Misses execute the actual full-key correction.

      Instances For
        source
        def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.code (w : ℕ) :
        WordRAM.Code WordRAM.Basis.standard registers

        Complete width-indexed internal-node query. Node-dependent constants occur only in RAM.

        Instances For
          source
          theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.size_code (w : ℕ) :
          (code w).size ≤ 201000

          One width-independent code-size bound includes both branches of every conditional.

          source
          theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.preserves_caller (w : ℕ) (i : Fin registers) (hlo : 31 ≤ ↑i) (hhi : ↑i < 39) :
          WordRAM.Code.Preserves i (code w)

          Registers 31 through 38 belong to the outer traversal. They are outside every node workspace; the terminal self-copy used by moves occupies register 39 instead.

          source
          theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.caller_regs_eq {w t : ℕ} {x y : WordRAM.Data registers} (he : WordRAM.Exec w (code w) x y t) (i : Fin registers) (hlo : 31 ≤ ↑i) (hhi : ↑i < 39) :
          y.regs i = x.regs i

          Every actual execution frames the caller's eight traversal registers.

          source
          theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.caller_regs_eq_within {w t : ℕ} {x y : WordRAM.Data registers} (he : WordRAM.ExecWithin w (code w) x y t) (i : Fin registers) (hlo : 31 ≤ ↑i) (hhi : ↑i < 39) :
          y.regs i = x.regs i

          The same caller frame for bounded-time executions, directly usable by traversal.

          source
          theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_correction {w n q a : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hw : 3 ≤ 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) (j : Fin n) (hj : keys j ≠ q) (hd : x.regs divergence = keys j ^^^ q) (hz : x.regs zero = 0) :
          ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (correction w) x y 200138 ∧ y.regs out = Lean.FusionTree.boundaryRank w keys q j ∧ Ready p q a y ∧ y.mem = x.mem

          A miss executes the concrete highest-bit and boundary programs, returning the mathematical sibling-boundary rank. All incoming workspace registers may be arbitrary.

          source
          theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec {w n q a : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hn : 2 ≤ 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) (hr : Rep p a x.mem) (hq : WordRAM.Fits w q) (ha : WordRAM.Fits w (a + 18 + (n - 1) * 2)) (hxq : x.regs query = q) (hxa : x.regs pointer = a) :
          ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (code w) x y 201000 ∧ y.regs out = Lean.FusionTree.upperRank keys q ∧ y.mem = x.mem ∧ y.regs query = q ∧ y.regs pointer = a

          Every bounded query receives its true inclusive full-key rank. The physical program depends only on w, and 201000 bounds the actual instruction count uniformly in w, n, the keys, their preprocessing witnesses and the query. Registers 0 and 1 and all memory are preserved. The address premise covers the last full key in the stride-two table.

          source
          theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exists_preprocessing {w n : ℕ} {keys : Fin n → ℕ} (hn : 2 ≤ n) (hs : StrictMono keys) (hk : ∀ (i : Fin n), keys i < 2 ^ w) (hnB : n ≤ Lean.FusionTree.branching w) (hlarge : 9 ≤ Nat.log 2 w) :
          ∃ (p : NodeParameters w keys), (∀ (j : Fin 15), WordRAM.Fits w (p.words j)) ∧ ∀ (q a : ℕ) (x : WordRAM.Data registers), Rep p a x.mem → WordRAM.Fits w q → WordRAM.Fits w (a + 18 + (n - 1) * 2) → x.regs query = q → x.regs pointer = a → ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (code w) x y 201000 ∧ y.regs out = Lean.FusionTree.upperRank keys q ∧ y.mem = x.mem ∧ y.regs query = q ∧ y.regs pointer = a

          Real preprocessing witnesses exist, all fifteen stored words fit, and the same width-indexed program answers every bounded query on every memory realizing those witnesses. The witness construction has no preprocessing-time assertion.