Sparse initialization of requested accumulators

Main definitions

• PrunedQuery.zeroQueryPrefix: the memory after zeroing a listed prefix of query addresses.

Main results

• PrunedQuery.exec_clearRequested: actual indexed clearing within 7 N + 3 instructions.

Repeated requests are permitted. Unlisted cells are preserved, and no dense value directory is initialized by this routine.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.zeroQueryPrefix (mem : ℕ → ℕ) (base : ℕ) (input : ℕ → ℕ) (k : ℕ) : ℕ → ℕ

Clear precisely the addresses named in the processed prefix of an explicit query list.

@[simp]

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.zeroQueryPrefix_zero (mem : ℕ → ℕ) (base : ℕ) (input : ℕ → ℕ) : zeroQueryPrefix mem base input 0 = mem

Clearing no requests leaves memory unchanged.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.zeroQueryPrefix_succ (mem : ℕ → ℕ) (base : ℕ) (input : ℕ → ℕ) (k : ℕ) : zeroQueryPrefix mem base input (k + 1) = Function.update (zeroQueryPrefix mem base input k) (base + input k) 0

One additional listed request is exactly one memory store, including repeated requests.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.zeroQueryPrefix_outside {mem : ℕ → ℕ} {base capacity k : ℕ} {input : ℕ → ℕ} (hcode : ∀ i < k, input i < capacity) {a : ℕ} (ha : ¬{ base := base, length := capacity }.Owns a) : zeroQueryPrefix mem base input k a = mem a

Every cell outside the concrete value directory is preserved by a bounded prefix.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.zeroQueryPrefix_at {mem : ℕ → ℕ} {base k i : ℕ} {input : ℕ → ℕ} (hi : i < k) : zeroQueryPrefix mem base input k (base + input i) = 0

Every requested value in the processed prefix is actually zero in the resulting memory.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ClearLocal (i : Fin registers) : Prop

Registers modified by sparse clearing.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableClearLocal (i : Fin registers) : Decidable (ClearLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_clearValueStep {w : ℕ} (x : WordRAM.Data registers) (q : ℕ) (hq : x.mem (x.regs listBase + x.regs index) = q) (h0 : x.regs nil = 0) (h1 : x.regs one = 1) (hr : WordRAM.Fits w (x.regs listBase + x.regs index)) (hv : WordRAM.Fits w (x.regs valueBase + q)) (hi : WordRAM.Fits w (x.regs index + 1)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w clearValueStep x y 5 ∧ y.regs index = x.regs index + 1 ∧ y.mem = Function.update x.mem (x.regs valueBase + q) 0 ∧ ∀ (i : Fin registers), ¬ClearLocal i → y.regs i = x.regs i

Each requested word costs an indexed source load, indexed zero store and increment.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_clearRequested {w N capacity : ℕ} (x : WordRAM.Data registers) (input : ℕ → ℕ) (hN : x.regs count = N) (hinput : ∀ i < N, x.mem (x.regs listBase + i) = input i) (hcode : ∀ i < N, input i < capacity) (hsep : x.regs listBase + N ≤ x.regs valueBase ∨ x.regs valueBase + capacity ≤ x.regs listBase) (h0 : x.regs nil = 0) (h1 : x.regs one = 1) (hw : WordRAM.Fits w (x.regs listBase + N + x.regs valueBase + capacity + N + 2)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w clearRequested x y (7 * N + 3) ∧ y.regs index = N ∧ y.mem = zeroQueryPrefix x.mem (x.regs valueBase) input N ∧ (∀ i < N, y.mem (x.regs listBase + i) = input i) ∧ ∀ (i : Fin registers), ¬ClearLocal i → y.regs i = x.regs i

The fixed native clearing loop visits only explicit requests. Width follows from concrete source/destination endpoints and lengths, and source preservation follows from their separation.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ClearValuesLocal (i : Fin registers) : Prop

Registers changed by a complete internal-node initialization.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableClearValuesLocal (i : Fin registers) : Decidable (ClearValuesLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_clearValues {w N capacity : ℕ} (x : WordRAM.Data registers) (input : ℕ → ℕ) (hN : x.regs count = N) (hinput : ∀ i < N, x.mem (x.regs listBase + i) = input i) (hcode : ∀ i < N, input i < capacity) (hsep : x.regs listBase + N ≤ x.regs valueBase ∨ x.regs valueBase + capacity ≤ x.regs listBase) (hframeSep : x.regs frame + 4 ≤ x.regs listBase ∨ x.regs listBase + N ≤ x.regs frame) (h0 : x.regs nil = 0) (h1 : x.regs one = 1) (h4 : x.regs frameWidth = 4) (hw : WordRAM.Fits w (x.regs listBase + N + x.regs valueBase + capacity + N + 2)) (hf : WordRAM.Fits w (x.regs frame + 4)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w clearValues x y (7 * N + 8) ∧ y.regs index = N ∧ y.regs term = 0 ∧ y.regs mode = 1 ∧ y.mem = Function.update (zeroQueryPrefix x.mem (x.regs valueBase) input N) (x.regs frame + 3) 0 ∧ (∀ i < N, y.mem (x.regs listBase + i) = input i) ∧ ∀ (i : Fin registers), ¬ClearValuesLocal i → y.regs i = x.regs i

Sparse clearing and actual stored-frame initialization together cost 7 N + 8 instructions. The source list is preserved; the only additional memory write is its frame's fourth word.