One actual ordinary-host catalogue iteration #
The loaded pointer is read from actual memory, and every local fit follows from the global logarithmic width and the preprocessing polynomial word bound. Both catalogue and signed payloads are preserved below the shared matrix workspace.
Main results #
exec_body: one full Convolution call, exact Boolean update, index advance and prefix frame.
These native composition proofs are original.
theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_body {r κ n w tab num N k b : ℕ} (c : Host.Callee r) (x : WordRAM.Data (registerCount r)) (μ : ℕ → ℤ) (hw : width κ c.widthCoefficient n ≤ w) (hN : N < (n + 2) ^ envelopeExponent κ) (htab : tab < (n + 2) ^ envelopeExponent κ) (hnum : num < (n + 2) ^ envelopeExponent κ) (hknum : k < num) (hc : Controls tab num N ((n + 2) ^ envelopeExponent κ) x) (hk : x.regs (controllerRegisters r current) = k) (hb : x.regs (controllerRegisters r answer) = b) (hb1 : b ≤ 1) (hptr : x.mem (tab + k) < (n + 2) ^ envelopeExponent κ) (hvalues : ∀ i < N, |μ i| ≤ ↑((n + 2) ^ envelopeExponent κ)) (hmem : ∀ i < N, x.mem (x.mem (tab + k) + i) = WordRAM.Signed.encode (μ i)) :
∃ (y : WordRAM.Data (registerCount r)),
WordRAM.ExecWithin w (body c) x y
(Host.callerTime N (c.time (Host.sideLength N) (2 * (n + 2) ^ envelopeExponent κ + 1)) + 10) ∧ Controls tab num N ((n + 2) ^ envelopeExponent κ) y ∧ y.regs (controllerRegisters r current) = k + 1 ∧ y.regs (controllerRegisters r answer) ≤ 1 ∧ (y.regs (controllerRegisters r answer) = 1 ↔ b = 1 ∨ ThreeSum.Convolution N μ) ∧ ∀ p < 2 * (n + 2) ^ envelopeExponent κ, y.mem p = x.mem p
One pointed-to call, including all index/address/argument/Boolean work.