Caller scalars from actual native parameters #
Main results #
QueriedProduct.producer_fits: original numerical admission covers both producer kernels.QueriedProduct.exec_parameters: actual powers, mask counting, root and band count, with a charge and complete high-register/memory frame.
The parameter phase reads original headers only. No computed roots, subset tables or intermediate-state fit assertions are supplied by the caller.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.producer_fits {w L m N Q : ℕ} (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
Numerical admission is on original scalar parameters, not machine states.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.caller_fits {w L m N Q : ℕ} (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
A common numerical margin covers caller counters, all allocation endpoints and constants.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_parameters {w L m N Q : ℕ} (hm : m ≤ L) (x : WordRAM.Data 160) (hL : x.mem 1 = L) (hmemory : x.mem 2 = m) (hN : x.mem 3 = N) (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 160),
WordRAM.ExecWithin w parameters x y (16 * L + 49 + ((6 * L + 16) * 2 ^ L + 14)) ∧ BandPreparation.BandParameters L m N (WordRAM.Data.comap bank y) ∧ y.mem = x.mem ∧ ∀ (i : Fin 160), 96 ≤ ↑i → y.regs i = x.regs i
All actual parameter computation is charged, and the original matrix/query memory is untouched. Reusing the low bank preserves every high caller register.