Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Program

Callable queried-product code #

The source product is unchanged. Its translated memory accesses use a runtime base in register 160 and a source-word modulus computed from the original row and query counts. The 160 source registers occupy the low bank; registers 161 and 162 are the modulus and address temporary.

Raw zero/one entries are still doubled by the original charged matrix-input loop. Setup and final normalization touch only the original input and answer spans, never the whole reserved window or caller catalogue. The code definitions here are internal implementation APIs.

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.result :
Fin 163

Absolute result pointer returned to the caller. Also a setup argument register.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.second :
    Fin 163

    Setup argument register.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.third :
      Fin 163

      Setup constant or normalization modulus.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.fourth :
        Fin 163

        Power exponent during setup.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.base :
          Fin 163

          Runtime source-memory base supplied by the caller.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.modulus :
            Fin 163

            Computed source-word modulus, preserved across the translated product.

            Instances For
              source
              @[reducible, inline]
              abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.address :
              Fin 163

              Temporary absolute address.

              Instances For
                source
                @[reducible, inline]
                abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.inputSize :
                Fin 163

                Source register retaining the original input span length.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.output :
                  Fin 163

                  Source register retaining the relative answer pointer.

                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.Reg.queryCount :
                    Fin 163

                    Source register retaining the query occurrence count.

                    Instances For
                      source
                      def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.clogBank (i : Fin 4) :
                      Fin 163

                      The logarithm routine uses four low scratch registers.

                      Instances For
                        source
                        def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.powerBank (i : Fin 5) :
                        Fin 163

                        The power routine uses five low scratch registers.

                        Instances For
                          source
                          def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.normalizeBank (i : Fin 7) :
                          Fin 163

                          Array normalization uses seven low scratch registers.

                          Instances For
                            source
                            def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.readSize :
                            WordRAM.Code WordRAM.Basis.standard 163

                            Read the actual row and occurrence-count headers, and form N+Q+3.

                            Instances For
                              source
                              def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.setup :
                              WordRAM.Code WordRAM.Basis.standard 163

                              Compute 2^(128*clog₂(N+Q+3)) with the existing logarithm and power programs.

                              Instances For
                                source
                                def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.restoreInput :
                                WordRAM.Code WordRAM.Basis.standard 163

                                Normalize the restored local input, so its actual physical words equal their source words.

                                Instances For
                                  source
                                  def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.returnOutput :
                                  WordRAM.Code WordRAM.Basis.standard 163

                                  Normalize the exact output span and return its absolute address.

                                  Instances For
                                    source
                                    def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.program :
                                    WordRAM.Code WordRAM.Basis.standard 163

                                    One fixed native raw-input product callable above an arbitrary caller-supplied base. Every memory translation, source instruction and normalization is part of this code.

                                    Instances For
                                      source
                                      def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.core :
                                      WordRAM.Code WordRAM.Basis.standard 163

                                      Internal execution prefix through setup and the actual translated product.

                                      Instances For
                                        source
                                        def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.sourceWidth (N Q : ℕ) :
                                        ℕ

                                        The derived source width is independent of the physical machine width.

                                        Instances For
                                          source
                                          def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.windowSize (N Q : ℕ) :
                                          ℕ

                                          Polynomially bounded virtual address-space reservation; no bulk initialization is implied.

                                          Instances For