Complete native accumulation over a distinct parent list #
Main results #
PrunedQuery.exec_accumulateLoop: the native loop adds a returned child exactly once at each contributing listed parent query, within31 N + 3instructions.
The loop invariant uses Mathlib's existing Finset.piecewise for the updated memory cells.
The source list and child values are preserved by the concrete block separations.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_accumulateLoop {w N capacity : ℕ} (x : WordRAM.Data registers) (input : ℕ → ℕ) (V B : ℕ → ℤ) (hN : x.regs count = N) (hinput : ∀ i < N, x.mem (x.regs listBase + i) = input i) (hcode : ∀ i < N, input i < capacity) (hinj : Set.InjOn input {i : ℕ | i < N}) (hparent : ∀ i < N, x.mem (x.regs valueBase + input i) = WordRAM.Signed.encode (V (input i))) (hchild :
∀ i < N,
selected true (x.regs term) (input i) →
x.mem (x.regs childValues + input i / 10) = WordRAM.Signed.encode (B (input i / 10))) (hV : ∀ i < N, GenericRAM.Signed.Fits w (V (input i))) (hB : ∀ i < N, GenericRAM.Signed.Fits w (B (input i / 10))) (hsepSource : x.regs listBase + N ≤ x.regs valueBase ∨ x.regs valueBase + capacity ≤ x.regs listBase) (hsepChild : x.regs valueBase + capacity ≤ x.regs childValues ∨ x.regs childValues + capacity ≤ x.regs valueBase) (h1 : x.regs one = 1) (h9 : x.regs nine = 9) (h10 : x.regs ten = 10) (hw : WordRAM.Fits (w + 2) (x.regs listBase + N + x.regs valueBase + capacity + x.regs childValues + capacity + N + 16)) :
∃ (y : WordRAM.Data registers),
WordRAM.ExecWithin (w + 2) accumulateLoop x y (31 * N + 3) ∧ y.regs index = N ∧ y.mem = (Finset.image (fun (i : ℕ) => x.regs valueBase + input i)
({i ∈ Finset.range N | selected true (x.regs term) (input i)})).piecewise
(fun (a : ℕ) => WordRAM.Signed.encode (V (a - x.regs valueBase) + B ((a - x.regs valueBase) / 10))) x.mem ∧ WordRAM.Modifies { base := x.regs valueBase, length := capacity }.footprint x.mem y.mem ∧ (∀ i < N, y.mem (x.regs listBase + i) = input i) ∧ ∀ (i : Fin registers), ¬AccumulateStepLocal i → y.regs i = x.regs i
This is the real indexed signed-add loop. The list's distinctness is its ordinary memory property, established by the preceding native timestamp scan, not a query-decision oracle.