Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Pruned.Memory

Concrete input and scratch layout for native pruned queries #

Main definitions #

The standard State.init length cell precedes this list. Query codes and the two source arrays are read-only. The timestamp region is initially zero because it lies beyond the supplied input.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.input (L : ℕ) (a b : Fin (10 ^ L) → ℤ) (qs : List (Fin (10 ^ L))) :
List ℕ

Flat initialized input: depth, query count, both signed arrays, then explicit query codes.

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

    Start of the returned values, in the original query-list order.

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

      First stack-frame cell, immediately after the returned values.

      Instances For
        source
        def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.listsBase (L Q : ℕ) :
        ℕ

        Query lists occupy one 10^L block per possible stack depth.

        Instances For
          source
          def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.valuesBase (L Q : ℕ) :
          ℕ

          Values occupy a separate 10^L block per depth.

          Instances For
            source
            def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.stampsBase (L Q : ℕ) :
            ℕ

            One shared timestamp directory suffices for all child-set constructions.

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

              One-past-end address of the complete output and scratch footprint.

              Instances For
                source
                def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.addressBound (L Q : ℕ) :
                ℕ

                A scalar budget for the concrete addresses, counters, powers and timestamp generations.

                Instances For
                  source
                  theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.length_input (L : ℕ) (a b : Fin (10 ^ L) → ℤ) (qs : List (Fin (10 ^ L))) :
                  (input L a b qs).length = 2 + 2 * 10 ^ L + qs.length

                  The initialized payload includes no precomputed child requests or recursion certificate.