Complete native catalogue traversal #
The invariant records exactly the processed entries of the existing emitted-node list. Every pointer and signed cell is read from its actual represented block; all future entries survive because the matrix/callee workspace is above twice the preprocessing word envelope.
Main results #
exec_calls: complete charged loop, exact disjunction of all emitted Convolution instances, and preservation of the entire preprocessing prefix.
These native catalogue composition proofs are original.
theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_calls {r κ n w tab U G : ℕ} (c : Host.Callee r) (out : List (ℕ × ThreeSum.ChanHe.Node)) (x : WordRAM.Data (registerCount r)) (hw : width κ c.widthCoefficient n ≤ w) (hN : 4 * G < (n + 2) ^ envelopeExponent κ) (htab : tab < (n + 2) ^ envelopeExponent κ) (hnum : out.length < (n + 2) ^ envelopeExponent κ) (hwords : ∀ (p : ℕ), x.mem p < (n + 2) ^ envelopeExponent κ) (hstored : ChanHe.Traversal.StoredNodes U G tab out x.mem) (hc : Controls tab out.length (4 * G) ((n + 2) ^ envelopeExponent κ) x) (hk : x.regs (controllerRegisters r current) = 0) (hb : x.regs (controllerRegisters r answer) = 0) :
∃ (y : WordRAM.Data (registerCount r)),
WordRAM.ExecWithin w (calls c) x y
(out.length * (Host.callerTime (4 * G) (c.time (Host.sideLength (4 * G)) (2 * (n + 2) ^ envelopeExponent κ + 1)) + 12) + 2) ∧ y.regs (controllerRegisters r answer) ≤ 1 ∧ (y.regs (controllerRegisters r answer) = 1 ↔ ∃ (i : Fin out.length), ThreeSum.Convolution (4 * G) (out[↑i].2.oneArray U)) ∧ ∀ p < 2 * (n + 2) ^ envelopeExponent κ, y.mem p = x.mem p
Execute all actual pointers, retaining every packed input and catalogue cell.