Native headers, powers and evaluator pointers #
Main results #
PrunedQuery.exec_initialize: load both actual headers, compute the encoding-array length, derive every evaluator pointer, and establish the ordinary register calling convention.
The prefix uses 4L+27 instructions, including its power loop. Its continuation is the existing
structured sequence rule, so composing it with evaluation gives the original fixed program.
This continuation lemma is an internal implementation API for the complete initialized-run
theorems in Pruned.Flat and Pruned.Width.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_initialize {w L Q : ℕ} (x : WordRAM.Data registers) (hL : x.mem 1 = L) (hQ : x.mem 2 = Q) (hfit : WordRAM.Fits w (addressBound L Q)) :
∃ (y : WordRAM.Data registers),
y.mem = x.mem ∧ KernelRegs L (scratchBase L Q) 3 (3 + 10 ^ L) y ∧ y.regs queryCount = Q ∧ y.regs queries = 3 + 2 * 10 ^ L ∧ y.regs output = outputBase L Q ∧ y.regs epoch = 0 ∧ ∀ (tail : WordRAM.Code WordRAM.Basis.standard registers) (z : WordRAM.Data registers) (T : ℕ),
WordRAM.ExecWithin w tail y z T →
WordRAM.ExecWithin w (header.seq (powers.seq (parameters.seq (locate.seq tail)))) x z (4 * L + 27 + T)
Initialization derives all pointers from the two ordinary scalar headers. Its output assertion contains no execution or fit fields; the charged native composition is proved here.