Actual empty-child transitions

Main results

• PrunedQuery.exec_node_emptyChild: compute an empty child by real native scanning, advance the parent term, and preserve its request list and partial values.

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

An empty-child transition may change the temporary child list, shared stamps and the parent frame. Its first three frame words are also explicitly preserved below.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_node_emptyChild {w L f a0 b0 d N 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) (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) (hempty : scanSet true k input N = ∅) (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 + 33) ∧ KernelRegs L f a0 b0 y ∧ y.regs level = d ∧ y.regs mode = 1 ∧ 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) ∅ ∧ (∀ j < 3, y.mem (f + 4 * d + j) = x.mem (f + 4 * d + j)) ∧ y.mem (f + 4 * d + 3) = k + 1 ∧ WordRAM.Modifies (emptyChildWrites L f d) x.mem y.mem

The program itself observes its computed zero child count and skips the recursive push. Every scan, comparison, increment and stored counter is charged.