One actual tile call on produced arrays and computed routing words #
Main results #
QueriedProduct.exec_tileStep: load the actual span, construct the kernel ABI, execute the native pruned kernel and propagate its returned epoch while advancing the real tile index.
The proof decodes typed queries from actual saved words; they are not program input. The finite request set, encoding arrays, frames, arithmetic fits and call charge are obtained from the actual producer contracts.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_tileStep {w L m N A t E : ℕ} (hw : 0 < w) (hm : m ≤ L) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (old : ℕ → ℕ) (x : WordRAM.Data 160) (hp : Parameters L m N qs.length x) (hx : x.regs index = t) (ht : t < MatrixMultiplication.Schonhage.numBands L m N ^ 2) (hE : x.regs epoch = E) (hEbound : E ≤ epochBound L m N) (hg : SavedGroups L m N qs.length old x.mem) (he : EncodedBands hm X Y x.mem) (hvalues :
∀ (i : Fin qs.length),
old
(Wanted.codeAddress L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length ↑i) = ↑(PrunedQuery.queryIndex
(MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm) ↑(qs.get i).1
↑(qs.get i).2))) (hoffsets :
∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2,
old (Wanted.offsetAddress L m N qs.length + t) = Nat.count (fun (k : ℕ) => (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) k < t) qs.length) (hmarks : ∀ j < 10 ^ L, x.mem (stampBase L m N qs.length + j) ≤ E) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), |X i k| ≤ ↑A) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), |Y k j| ≤ ↑A) (hmag : magnitudeBound L A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N qs.length)) :
have a := x.mem (offsetBase L m N qs.length + t);
have b := x.mem (offsetBase L m N qs.length + t + 1);
have β := t / MatrixMultiplication.Schonhage.numBands L m N;
have γ := t % MatrixMultiplication.Schonhage.numBands L m N;
∃ (y : WordRAM.Data 160),
WordRAM.ExecWithin (w + 2) tileStep x y
(4 * L + 29 * (b - a) + PrunedQuery.traceWeight
(MatrixMultiplication.Schonhage.wantedStrings (MatrixMultiplication.Schonhage.MaskTable.layout hm)
qs.toFinset β γ) + 64) ∧ Parameters L m N qs.length y ∧ y.regs index = t + 1 ∧ E + 1 ≤ y.regs epoch ∧ y.regs epoch ≤ E + 1 + PrunedQuery.epochAllowance L ∧ SavedGroups L m N qs.length old y.mem ∧ EncodedBands hm X Y y.mem ∧ (∀ j < 10 ^ L, y.mem (stampBase L m N qs.length + j) ≤ y.regs epoch) ∧ (∀ (i : Fin qs.length),
(Wanted.tileKey L m N ∘ Wanted.inputPairs qs) ↑i = t →
y.mem
(groupedBase L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length ↑i) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ ∀ (p : ℕ),
¬(groupedBase L m N qs.length + a ≤ p ∧ p < groupedBase L m N qs.length + b) →
¬(scratchBase L m N qs.length ≤ p ∧ p < memoryEnd L m N qs.length) → y.mem p = x.mem p
One charged native tile, with the actual query set and a reusable timestamp directory. The final memory witness contains every reported pruned value and is the same state whose epoch is passed to the next tile. Its answers are the original signed matrix product.