Documentation

Complexity.Algorithms.WordRAM.FusionTree.Boundary

Checked correction boundaries #

After finding the highest differing position, fusion-node correction replaces the query's suffix by a sibling-subtree extreme. Both extremes and the original query bit are computed without constructing the overflowing word 2^w.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.query :
Fin 10

Original query, preserved.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.position :
    Fin 10

    Highest differing bit position, preserved.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.one :
      Fin 10

      Constant one.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.next :
        Fin 10

        Position immediately above the differing bit.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.power :
          Fin 10

          The differing bit's power of two.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.low :
            Fin 10

            Mask below the differing bit.

            Instances For
              source
              @[reducible, inline]
              abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.stem :
              Fin 10

              Common stem followed by zeros.

              Instances For
                source
                @[reducible, inline]
                abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.lower :
                Fin 10

                All-ones extreme in the lower sibling subtree.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.upper :
                  Fin 10

                  All-zeros extreme in the upper sibling subtree.

                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.bit :
                    Fin 10

                    Zero or one according to the query's differing bit.

                    Instances For
                      source
                      def Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.code :
                      WordRAM.Code WordRAM.Basis.standard 10

                      Compute both extremes and the bit selecting the correction convention.

                      Instances For
                        source
                        def Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.result (x : WordRAM.Data 10) (q p : ℕ) :
                        WordRAM.Data 10

                        The precise output state, including all scratch registers.

                        Instances For
                          source
                          theorem Cslib.Algorithms.WordRAM.FusionTree.BoundaryProgram.exec {w q p : ℕ} (x : WordRAM.Data 10) (hq : WordRAM.Fits w q) (hp : p < w) (hxq : x.regs query = q) (hxp : x.regs position = p) :
                          WordRAM.Exec w code x (result x q p) 10 ∧ (result x q p).regs lower = BitString.lowerBoundary q p ∧ (result x q p).regs upper = BitString.upperBoundary q p ∧ (result x q p).regs bit = q >>> p &&& 1 ∧ (result x q p).mem = x.mem

                          Ten checked instructions compute both sibling extremes and the selecting bit. The position may be w-1; the program never materializes 2^w. Query, position, and memory are preserved. Finding the differing position is a separate operation.