Ordinary initialized wanted-position inputs

Main definitions

• Wanted.input: four raw headers followed by the ordinary interleaved coordinate words.
• Wanted.inputPairs: a zero extension of that original finite list for natural-index invariants.

Main results

• Wanted.input_fits: the original header, length and coordinate words fit the admitted width.
• Wanted.input_word: initialized memory contains each original coordinate at its actual address.
• Wanted.exec_input: the fixed program computes the grouped arrays from actual State.init.

No powers, valid masks, tile keys, offsets, query codes or permutation words occur in the input.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.input {N : ℕ} (L m : ℕ) (qs : List (Fin N × Fin N)) : List ℕ

Four unsigned scalar headers followed by each row/column pair in original list order. The standard State.init length word precedes this payload at address zero.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.inputPairs {N : ℕ} (qs : List (Fin N × Fin N)) (i : ℕ) : ℕ × ℕ

Ordinary input positions extended by zero outside the supplied list. This is a mathematical view of original words, not a query-code or layout certificate.

@[simp]

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.inputPairs_get {N : ℕ} (qs : List (Fin N × Fin N)) (i : Fin qs.length) : inputPairs qs ↑i = (↑(qs.get i).1, ↑(qs.get i).2)

Every in-range position is exactly its original pair.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.input_length {N : ℕ} (L m : ℕ) (qs : List (Fin N × Fin N)) : (input L m qs).length + 1 = inputLimit qs.length

The native length header and coordinate input end at the concrete allocation boundary.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.inputPairs_lt {N : ℕ} (qs : List (Fin N × Fin N)) (i : ℕ) (hi : i < qs.length) : (inputPairs qs i).1 < N ∧ (inputPairs qs i).2 < N

Both original coordinates are below the original matrix dimension.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.input_word {N : ℕ} (L m : ℕ) (qs : List (Fin N × Fin N)) (i : Fin qs.length) (s : Fin 2) : (WordRAM.State.init (input L m qs)).data.mem (5 + 2 * ↑i + ↑s) = if s = 0 then ↑(qs.get i).1 else ↑(qs.get i).2

The exact initialized row/column word, with address calculations in original list order.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.input_fits {w L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (hfit : WordRAM.Fits w (wordBudget L m N qs.length)) : WordRAM.InputFits w (input L m qs)

Header, length and every coordinate word fit from the same original numerical budget.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_input {w L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (hfit : WordRAM.Fits w (wordBudget L m N qs.length)) : WordRAM.InputFits w (input L m qs) ∧ ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w program (WordRAM.State.init (input L m qs)).data y (timeBound L m N qs.length) ∧ Parameters L m N qs.length y ∧ WordRAM.Data.Bounded w y ∧ (∀ (i : Fin qs.length), y.mem (codeAddress L m N qs.length + CountingSort.position (tileKey L m N ∘ inputPairs qs) qs.length ↑i) = ↑(PrunedQuery.queryIndex (MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm) ↑(qs.get i).1 ↑(qs.get i).2)) ∧ y.mem (originalAddress L m N qs.length + CountingSort.position (tileKey L m N ∘ inputPairs qs) qs.length ↑i) = ↑i) ∧ (∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2, y.mem (offsetAddress L m N qs.length + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ inputPairs qs) k < t) qs.length) ∧ y.mem (offsetAddress L m N qs.length + MatrixMultiplication.Schonhage.numBands L m N ^ 2) = qs.length ∧ ∀ (a : ℕ), a < inputLimit qs.length ∨ memoryLimit L m N qs.length ≤ a → y.mem a = (WordRAM.State.init (input L m qs)).data.mem a

Complete execution from the actual initialized list, with guaranteed input fit and a bounded returned state. All auxiliary tables, counts, offsets and codes are computed natively.