Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Pruned.Child

Computed nonempty-child transitions of the native controller #

Main results #

The nonemptiness premise selects a case of the proof. The machine itself tests the count that it has just computed; no query-selection or layout certificate is input to its code.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childWrites (L f d : ℕ) :
Finset ℕ

Only the next query row, timestamps and the next four-word frame may change during a nonempty-child transition. In particular, parent queries, accumulators and frame survive.

Instances For
    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_node_child {w L f a0 b0 d N p k : ℕ} (x : WordRAM.Data registers) (hregs : KernelRegs L f a0 b0 x) (hd : x.regs level = d) (hdL : d < L) (hm : x.regs mode = 1) (hN : x.mem (f + 4 * d) = N) (hcap : N ≤ 10 ^ L) (hpref : x.mem (f + 4 * d + 1) = p) (hp : p < 10 ^ d) (hstride : x.mem (f + 4 * d + 2) = 10 ^ d) (hterm : x.mem (f + 4 * d + 3) = k) (hk : k < 10) (input : ℕ → ℕ) (hinput : ∀ i < N, x.mem (f + 4 * (L + 1) + d * 10 ^ L + i) = input i) (hcodes : ∀ i < N, input i < 10 ^ L) (hmarks : ∀ q < 10 ^ L, x.mem (f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L + q) ≤ x.regs epoch) (hne : (scanSet true k input N).Nonempty) (hw : WordRAM.Fits w (8 * f + 64 * (L + 1) * 10 ^ L + x.regs epoch + 128)) :
    ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w step x y (20 * N + 42) ∧ KernelRegs L f a0 b0 y ∧ y.regs level = d + 1 ∧ y.regs mode = 0 ∧ y.regs active = x.regs active ∧ y.regs epoch = x.regs epoch + 1 ∧ ScanMemory y.mem (f + 4 * (L + 1) + (d + 1) * 10 ^ L) (f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L) (x.regs epoch + 1) (10 ^ L) (scanSet true k input N) ∧ y.mem (f + 4 * (d + 1)) = (scanSet true k input N).card ∧ y.mem (f + 4 * (d + 1) + 1) = p + k * 10 ^ d ∧ y.mem (f + 4 * (d + 1) + 2) = 10 ^ (d + 1) ∧ y.mem (f + 4 * (d + 1) + 3) = 0 ∧ WordRAM.Modifies (childWrites L f d) x.mem y.mem

    This is the actual full controller transition, not a callee execution assumption. All three controller comparisons, the complete native scan, four frame stores and index work fit in 20 N + 42 instructions. The produced directory describes the same final memory.