Documentation

Complexity.Algorithms.WordRAM.FusionTree.Node.Correction

Executable correction subroutines #

The highest-bit call accepts an ordinary physical register and initializes its own bank. The boundary and second-rank calls charge all register transfers. No call changes memory.

Main results #

References #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.msbBank :
Fin (WordRAM.Multiword.Bank.capacity 44 + 4) → Fin registers

Disjoint workspace for the complete multiword highest-bit program.

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

    Copy the physical input, run the actual highest-bit program, and copy its scalar result.

    Instances For
      source
      theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_highest {w d : ℕ} (hw : 3 ≤ w) (x : WordRAM.Data registers) (hd : WordRAM.Fits w d) (hxd : x.regs divergence = d) :
      ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w (highest w) x y 200002 ∧ y.regs position = d.log2 ∧ y.mem = x.mem ∧ ∀ (i : Fin registers), ↑i < 40 → i ≠ position → y.regs i = x.regs i

      The 200000-instruction MSB bound plus its two actual caller copies.

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

      The two transfers into the boundary workspace.

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

        Prepare two inputs and compute both correction boundaries.

        Instances For
          source
          theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_boundaries {w q d : ℕ} (x : WordRAM.Data registers) (hq : WordRAM.Fits w q) (hd : d < w) (hxq : x.regs query = q) (hxd : x.regs position = d) :
          ∃ (y : WordRAM.Data registers), WordRAM.Exec w boundaries x y 13 ∧ Frame x y ∧ y.regs (boundaryBank 7) = BitString.lowerBoundary q d ∧ y.regs (boundaryBank 8) = BitString.upperBoundary q d ∧ y.regs (boundaryBank 9) = q >>> d &&& 1

          The boundary call includes three transfer instructions and ten arithmetic instructions.

          source
          def Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.secondQuery (strict : Bool) (src : Fin registers) :
          WordRAM.Code WordRAM.Basis.standard registers

          Transfer a full word to the compressor, make a sketch query and return the rank.

          Instances For
            source
            theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.exec_secondQuery {w n q a z : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (strict : Bool) (src : Fin registers) (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) (hz : WordRAM.Fits w z) (hxz : x.regs src = z) :
            ∃ (y : WordRAM.Data registers), WordRAM.Exec w (secondQuery strict src) x y 121 ∧ y.regs out = sketchCut strict w keys z ∧ Ready p q a y ∧ y.mem = x.mem

            Both caller copies and all 119 sketch-query instructions are charged.

            source
            theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.bit_eq_zero_iff (q d : ℕ) :
            q >>> d &&& 1 = 0 ↔ q.testBit d = false

            The numeric bit tested by RAM is zero precisely when the Boolean query bit is false.

            source
            theorem Cslib.Algorithms.WordRAM.FusionTree.NodeProgram.boundary_fits {w q d : ℕ} (hq : WordRAM.Fits w q) (hd : d < w) :
            WordRAM.Fits w (BitString.lowerBoundary q d) ∧ WordRAM.Fits w (BitString.upperBoundary q d)

            Both boundary words are physical words, including a differing bit at w - 1.