Complete native ordinary-host workspace initialization #
The actual preprocessing outputs are copied before a fixed-exponent native loop computes the polynomial word reservation. Every multiplication, loop test and final doubling is charged.
Main results #
exec_initialize: exact raw metadata, computed matrix base, counter and Boolean frame.
These native initialization proofs are original.
theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_initialize {r κ n w tab num N d : ℕ} (x : WordRAM.Data (registerCount r)) (hw : width κ d n ≤ w) (hn : x.regs (controllerRegisters r inputLength) = n) (ht : x.regs (preprocessingRegisters r ChanHe.Traversal.outputs) = tab) (hc : x.regs (preprocessingRegisters r ChanHe.Traversal.outputCount) = num) (hl : x.regs (preprocessingRegisters r ChanHe.Preprocessing.packedLength) = N) :
∃ (y : WordRAM.Data (registerCount r)),
WordRAM.ExecWithin w
((setup κ).seq
((WordRAM.Code.rename (controllerRegisters r) power).seq (WordRAM.Code.rename (controllerRegisters r) reserve)))
x y (4 * envelopeExponent κ + 14) ∧ Controls tab num N ((n + 2) ^ envelopeExponent κ) y ∧ y.regs (controllerRegisters r current) = 0 ∧ y.regs (controllerRegisters r answer) = x.regs (controllerRegisters r answer) ∧ y.mem = x.mem
Compute all outer controls from actual preprocessing registers at the global width.