Actual catalogue-pointer calls

Pointer loads, argument copies, the complete native Convolution call and Boolean accumulation are charged separately. The callee bank cannot overwrite outer controls; its memory frame keeps every remaining pointer and packed input below the reserved workspace.

Main results

• exec_loadSetup: actual pointer-table load and all four callee argument copies.
• exec_finish: exact native Boolean accumulation and loop increment.

These native composition proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_loadSetup {r w tab num N V k : ℕ} (x : WordRAM.Data (registerCount r)) (hc : Controls tab num N V x) (hk : x.regs (controllerRegisters r current) = k) (ha : WordRAM.Fits w (tab + k)) : ∃ (y : WordRAM.Data (registerCount r)), WordRAM.ExecWithin w ((WordRAM.Code.rename (controllerRegisters r) loadSource).seq callSetup) x y 6 ∧ (WordRAM.Data.comap (hostRegisters r) y).regs (Host.hostRegisters Host.len) = N ∧ (WordRAM.Data.comap (hostRegisters r) y).regs (Host.hostRegisters Host.upper) = V ∧ (WordRAM.Data.comap (hostRegisters r) y).regs (Host.hostRegisters Host.base) = x.mem (tab + k) ∧ (WordRAM.Data.comap (hostRegisters r) y).regs (Host.hostRegisters Host.matAB) = 2 * V ∧ Controls tab num N V y ∧ y.regs (controllerRegisters r current) = k ∧ y.regs (controllerRegisters r answer) = x.regs (controllerRegisters r answer) ∧ y.mem = x.mem

Load a pointer from actual memory and pass its raw runtime arguments to the host.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_finish {r w k b v : ℕ} (x : WordRAM.Data (registerCount r)) (ho : x.regs (controllerRegisters r one) = 1) (hk : x.regs (controllerRegisters r current) = k) (hb : x.regs (controllerRegisters r answer) = b) (hv : x.regs (hostRegisters r (Host.hostRegisters Host.found)) = v) (hfit : WordRAM.Fits w (k + 1)) : ∃ (y : WordRAM.Data (registerCount r)), WordRAM.ExecWithin w finish x y 4 ∧ y.regs (controllerRegisters r current) = k + 1 ∧ (y.regs (controllerRegisters r answer) = if v = 1 then 1 else b) ∧ (∀ (i : Fin 16), i ≠ current → i ≠ answer → y.regs (controllerRegisters r i) = x.regs (controllerRegisters r i)) ∧ y.mem = x.mem

Boolean accumulation and the next index are actual native instructions.