Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Layout

Protected buffers for native queried products #

Main definitions #

These numeric specifications describe the addresses computed by the native header. Neither a layout nor an execution/cost certificate is supplied to the program.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.inputEnd (m N Q : ℕ) :
ℕ

One past the original initialized input, including the native length word.

Instances For
    source
    def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.queryInputBase (m N : ℕ) :
    ℕ

    Original coordinate pairs follow both row-major input matrices.

    Instances For
      source
      def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.snapshotBase (L m N Q : ℕ) :
      ℕ

      The sum reserves disjoint space above the input and both low producer allocations. Using a sum permits direct arithmetic without a hidden maximum/layout operation.

      Instances For
        source
        def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.offsetBase (L m N Q : ℕ) :
        ℕ

        Actual prefix offsets are saved here before the band producer reuses low memory.

        Instances For
          source
          def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.codeBase (L m N Q : ℕ) :
          ℕ

          The grouped numerical codes follow all offsets, including their terminal word.

          Instances For
            source
            def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.originalBase (L m N Q : ℕ) :
            ℕ

            The actual original-index permutation follows the grouped codes.

            Instances For
              source
              def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.groupedBase (L m N Q : ℕ) :
              ℕ

              Kernel reporting writes answers in grouped order into this separate array.

              Instances For
                source
                def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.outputBase (L m N Q : ℕ) :
                ℕ

                Reconstructed answers in original list order; repeated requests have separate cells.

                Instances For
                  source
                  def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.scratchBase (L m N Q : ℕ) :
                  ℕ

                  Every source, saved routing array and answer block precedes reusable kernel scratch.

                  Instances For
                    source
                    def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.stampBase (L m N Q : ℕ) :
                    ℕ

                    The shared timestamp directory follows the kernel's actual frames and depth rows.

                    Instances For
                      source
                      def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.memoryEnd (L m N Q : ℕ) :
                      ℕ

                      One past the explicit whole-program allocation.

                      Instances For
                        source
                        def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.epochBound (L m N : ℕ) :
                        ℕ

                        Every tile call increases its actual returned epoch by at most this total envelope.

                        Instances For
                          source
                          def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.wordBudget (L m N Q : ℕ) :
                          ℕ

                          Ordinary scalar bound covering all producer, caller and kernel address arithmetic. Signed arithmetic has its separate original-entry magnitude envelope.

                          Instances For
                            source
                            def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.magnitudeBound (L A : ℕ) :
                            ℕ

                            The source's magnitude bounds on shared encodings derive the kernel's operand bounds.

                            Instances For
                              source
                              theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.producers_le_snapshot (L m N Q : ℕ) :
                              BandPreparation.memoryEnd L m N ≤ snapshotBase L m N Q ∧ Wanted.memoryLimit L m N Q ≤ snapshotBase L m N Q ∧ inputEnd m N Q ≤ snapshotBase L m N Q

                              Both low producer work areas and the complete original input precede its snapshot.

                              source
                              theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.buffer_order (L m N Q : ℕ) :
                              snapshotBase L m N Q + inputEnd m N Q = offsetBase L m N Q ∧ offsetBase L m N Q + MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 1 = codeBase L m N Q ∧ codeBase L m N Q + Q = originalBase L m N Q ∧ originalBase L m N Q + Q = groupedBase L m N Q ∧ groupedBase L m N Q + Q = outputBase L m N Q ∧ outputBase L m N Q + Q = scratchBase L m N Q

                              The high buffers are adjacent and ordered, including zero-length answer arrays.

                              source
                              theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.query_address_lt {m N Q i s : ℕ} (hi : i < Q) (hs : s < 2) :
                              queryInputBase m N + 2 * i + s < inputEnd m N Q

                              Real original query addresses lie strictly inside the original input prefix.