Flat initialized executions of native pruned queries

Main results

• PrunedQuery.runs: prefix Runs and charged halting Executes from actual State.init, connected to the same final memory, existing finite pruned values and outside frame.
• PrunedQuery.bounded_reachable: every reachable prefix has target-sized data words.

The single fixed program returns the unsigned pointer to its encoded answer list. Queries may repeat and their order is preserved. Its 96 registers and code-size bound are independent of depth, query count, input values and physical word width. These initialized-run theorems, runs_wide in Pruned.Width and exec_kernel in Pruned.Kernel are the client interfaces. Stage exec_* lemmas in their dependencies are internal implementation APIs exported for proof composition.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.runs {w L A B : ℕ} (hw : 0 < w) (a b : Fin (10 ^ L) → ℤ) (qs : List (Fin (10 ^ L))) (ha : ∀ (v : Fin (10 ^ L)), |a v| ≤ ↑A) (hb : ∀ (v : Fin (10 ^ L)), |b v| ≤ ↑B) (hmag : magnitudeBound L A B < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L qs.length)) : WordRAM.InputFits (w + 2) (input L a b qs) ∧ ∃ (y : WordRAM.Data registers), ∃ n ≤ timeBound qs, WordRAM.Runs (w + 2) (program.program output) (WordRAM.State.init (input L a b qs)) { pc := program.size, data := y } n ∧ WordRAM.Executes (w + 2) (program.program output) (WordRAM.State.init (input L a b qs)) (outputBase L qs.length) (n + 1) ∧ WordRAM.Data.Bounded (w + 2) y ∧ (∀ (i : Fin qs.length), y.mem (outputBase L qs.length + ↑i) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.Pruned.result L (fun (v : MatrixMultiplication.Schonhage.Leaf L) => a (Encoding.leafIndex v)) (fun (v : MatrixMultiplication.Schonhage.Leaf L) => b (Encoding.leafIndex v)) (requested qs) (queryAt (qs.get i)))) ∧ ∀ (c : ℕ), ¬(outputBase L qs.length ≤ c ∧ c < memoryEnd L qs.length) → y.mem c = (WordRAM.State.init (input L a b qs)).data.mem c

Actual initialized flat executions. The prefix witness holding all answers is precisely the state at the final halt, and the halt is charged as one further target instruction.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.bounded_reachable {w L A B n : ℕ} (hw : 0 < w) (a b : Fin (10 ^ L) → ℤ) (qs : List (Fin (10 ^ L))) (ha : ∀ (v : Fin (10 ^ L)), |a v| ≤ ↑A) (hb : ∀ (v : Fin (10 ^ L)), |b v| ≤ ↑B) (hmag : magnitudeBound L A B < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L qs.length)) {y : WordRAM.State registers} (hy : WordRAM.Runs (w + 2) (program.program output) (WordRAM.State.init (input L a b qs)) y n) : WordRAM.Data.Bounded (w + 2) y.data

Ordinary native safety applies to every initialized reachable prefix, not merely the returned witness. The admission hypotheses are the same numerical original-input bounds.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.runs_bilinear {w L A B : ℕ} (hw : 0 < w) (left right : Fin (10 ^ L) → ℤ) (qs : List (Fin (10 ^ L))) (a : MatrixMultiplication.Schonhage.LeftStr L → ℤ) (b : MatrixMultiplication.Schonhage.RightStr L → ℤ) (hleft : ∀ (v : MatrixMultiplication.Schonhage.Leaf L), left (Encoding.leafIndex v) = MatrixMultiplication.Schonhage.encodingL a v) (hright : ∀ (v : MatrixMultiplication.Schonhage.Leaf L), right (Encoding.leafIndex v) = MatrixMultiplication.Schonhage.encodingR b v) (ha : ∀ (v : Fin (10 ^ L)), |left v| ≤ ↑A) (hb : ∀ (v : Fin (10 ^ L)), |right v| ≤ ↑B) (hmag : magnitudeBound L A B < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L qs.length)) : WordRAM.InputFits (w + 2) (input L left right qs) ∧ ∃ (y : WordRAM.Data registers), ∃ n ≤ timeBound qs, WordRAM.Runs (w + 2) (program.program output) (WordRAM.State.init (input L left right qs)) { pc := program.size, data := y } n ∧ WordRAM.Executes (w + 2) (program.program output) (WordRAM.State.init (input L left right qs)) (outputBase L qs.length) (n + 1) ∧ WordRAM.Data.Bounded (w + 2) y ∧ (∀ (i : Fin qs.length), y.mem (outputBase L qs.length + ↑i) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.bilinearProduct a b (queryAt (qs.get i)))) ∧ ∀ (c : ℕ), ¬(outputBase L qs.length ≤ c ∧ c < memoryEnd L qs.length) → y.mem c = (WordRAM.State.init (input L left right qs)).data.mem c

An encoder producer's existing leaf-value contract gives the original bilinear product at every supplied query. This is the same actual initialized program and charged run as runs; the mathematical specialization adds no machine operation or assumed producer execution.