Charged protected-buffer calculation #
Main results #
QueriedProduct.exec_layout: calculate every persistent scalar from the actual producer header and original request count, with all intermediate fits derived from original inputs.
This is an internal execution API. It receives ordinary header equalities and a numerical input bound, not a supplied layout or intermediate-state certificate.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_layout {w L m N Q : ℕ} (x : WordRAM.Data 160) (hp : BandPreparation.BandParameters L m N (WordRAM.Data.comap bank x)) (hQ : x.mem 4 = Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 160), WordRAM.ExecWithin w layout x y 50 ∧ Parameters L m N Q y ∧ y.mem = x.mem
Actual native layout calculation, preserving all original memory.