Documentation

Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Entry

Initialized producer-to-adapter composition #

One fixed native program runs the complete producer from its original four headers and three signed weight arrays, selects actual ordinal zero and invokes the actual record consumer. The general caller interface handles any occupied ordinal; the initialized client here chooses the first one with real code. Its existence follows from the original positive geometry.

The producer's pre-halt native witness and polynomial word bound derive every source pointer, coordinate, caller base and dirty-word bound used by the record consumer. No producer layout, run, solver or time certificate is an input hypothesis.

source
def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.produce :
WordRAM.Code WordRAM.Basis.standard 320

The complete real producer, using its original low bank.

Instances For
    source
    def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.entryProgram :
    WordRAM.Code WordRAM.Basis.standard 320

    One fixed initialized composition; selecting the first record costs one actual instruction.

    Instances For
      source
      def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.preparationTime (n D g p : ℕ) (values : List ℤ) :
      ℕ

      The unchanged producer's original-header budget, including its standalone halt.

      Instances For
        source
        theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec_input {W m n g p A : ℕ} (values : List ℤ) (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ MatrixMultiplication.Schonhage.D m) (hg : 1 ≤ g) (hp : 0 < p) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) (hv : ∀ z ∈ values, z.natAbs ≤ A) (hW : admissionWidth n (MatrixMultiplication.Schonhage.D m) g p A ≤ W) :
        WordRAM.InputFits W (PreparationInput.input n (MatrixMultiplication.Schonhage.D m) g p values) ∧ have hn := ⋯; ∃ (a : WordRAM.Data 64) (idx : ExactTriangle.InstanceIndex p), WordRAM.ExecWithin W Instances.program (WordRAM.Data.init (PreparationInput.input n (MatrixMultiplication.Schonhage.D m) g p values)) a (preparationTime n (MatrixMultiplication.Schonhage.D m) g p values - 1) ∧ idx ∈ ExactTriangle.instanceIndices (fun (a b : Fin n) => values.getD (Matrix.pairIndex (a, b)) 0) (MatrixMultiplication.Schonhage.D m) g p ∧ recordOrdinal n (MatrixMultiplication.Schonhage.D m) g p (fun (q : ℕ) => values.getD q 0) idx = 0 ∧ have qs := decodedQueries hn a.mem (recordQueries n (MatrixMultiplication.Schonhage.D m) p idx) (recordQueryCount n (MatrixMultiplication.Schonhage.D m) p (fun (q : ℕ) => values.getD q 0) idx); ∃ (y : WordRAM.Data 320), WordRAM.ExecWithin W entryProgram (WordRAM.Data.init (PreparationInput.input n (MatrixMultiplication.Schonhage.D m) g p values)) y (preparationTime n (MatrixMultiplication.Schonhage.D m) g p values + timeBound qs) ∧ y.regs Reg.result = a.regs Instances.heap + MatrixMultiplication.Schonhage.QueriedProduct.outputBase (19 * m) m n qs.length ∧ (∀ (j : Fin qs.length), y.mem (a.regs Instances.heap + (MatrixMultiplication.Schonhage.QueriedProduct.outputBase (19 * m) m n qs.length + ↑j)) = WordRAM.Signed.encode ((leftMatrix m n g p (fun (q : ℕ) => values.getD q 0) idx * rightMatrix m n g p (fun (q : ℕ) => values.getD q 0) idx) (qs.get j).1 (qs.get j).2)) ∧ (∀ (u : ℕ), u < a.regs Instances.heap ∨ a.regs Instances.heap + MatrixMultiplication.Schonhage.CallableProduct.windowSize n qs.length ≤ u → y.mem u = a.mem u) ∧ (∀ (j : Fin 64), y.regs (producerBank j) = a.regs j) ∧ qs.length * 2 ^ m ≤ n ^ 2

        Complete initialized structured execution. The actual producer execution is a conclusion, and its same native memory supplies the coordinate list consumed by the composed adapter.