Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Product.Routing

Native routing preparation from original coordinates #

Main results #

The earlier router memory in the conclusion is an existential witness produced by its actual execution. It is not a catalogue, layout or run certificate supplied by the caller.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.routingTimeBound (L m N Q : ℕ) :
ℕ

The sum of the actual preparation phases, before matrix adaptation and encoding.

Instances For
    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_prepareRouting {w L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (x : WordRAM.Data 160) (hL : x.mem 1 = L) (hmemory : x.mem 2 = m) (hN : x.mem 3 = N) (hQ : x.mem 4 = qs.length) (hqueries : ∀ i < qs.length, x.mem (queryInputBase m N + 2 * i) = (Wanted.inputPairs qs i).1 ∧ x.mem (queryInputBase m N + 2 * i + 1) = (Wanted.inputPairs qs i).2) (hfit : WordRAM.Fits w (wordBudget L m N qs.length)) :
    ∃ (y : WordRAM.Data 160) (old : ℕ → ℕ), WordRAM.ExecWithin w prepareRouting x y (routingTimeBound L m N qs.length) ∧ Parameters L m N qs.length y ∧ SavedGroups L m N qs.length old y.mem ∧ (∀ (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)) ∧ old (Wanted.originalAddress L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length ↑i) = ↑i) ∧ (∀ 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) ∧ (∀ j < inputEnd m N qs.length, y.mem (snapshotBase L m N qs.length + j) = x.mem j) ∧ ∀ (a : ℕ), a < 5 ∨ groupedBase L m N qs.length ≤ a → y.mem a = x.mem a

    Real original coordinates suffice to establish all routing invariants and a protected copy of the entire original input. Header zero and outside memory may be arbitrary.