Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Input

Ordinary initialized input for a callable product #

The first input word is a runtime base pointer. An arbitrary caller prefix follows, then a local ordinary input-length word and the unchanged original product input. No computed tables, grouping, encodings, bounded scratch contents or execution certificates occur in this input.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.inputBase (caller : List ℕ) :
ℕ

Runtime location of the local length word after an arbitrary caller prefix.

Instances For
    source
    def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.input {m N : ℕ} (caller : List ℕ) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) :
    List ℕ

    Original scalar headers, raw matrices and request pairs above a protected caller prefix.

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

      The initialized client loads the supplied runtime base before invoking the real kernel.

      Instances For
        source
        theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.input_word {m N : ℕ} (caller : List ℕ) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (a : ℕ) :
        (WordRAM.State.init (input caller X Y qs)).data.mem (inputBase caller + a) = (WordRAM.State.init (QueriedProduct.input true (19 * m) X Y qs)).data.mem a

        Every local original input word has its actual initialized meaning at the runtime base.

        source
        theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.input_fits {W m N : ℕ} (caller : List ℕ) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), 0 ≤ Y k j ∧ Y k j ≤ 1) (hcaller : ∀ v ∈ caller, WordRAM.Fits W v) (hfit : WordRAM.Fits W (inputBase caller + 4 * windowSize N qs.length + 1024)) :
        WordRAM.InputFits W (input caller X Y qs)

        Original caller words and admitted original product words suffice for the global input fit.