Executing Convolution-3SUM in caller-owned memory

The unchanged builder and instance loop read the actual source pointer and write only in the caller-owned matrix workspace. The certified finite callee preserves the entire prefix below that workspace, so every catalogue pointer and every remaining packed input survives each call.

Main definitions

• bodyAt: complete register-argument host using the existing setup, builder and loop.
• callerTime: all setup, matrix, loop and finite-callee instructions, excluding halt.

Main results

• Callee.exec_instance: discharge the actual generated matrix call.
• exec_at: exact Convolution verdict and protected-prefix frame.

These caller-layout composition proofs are original and reuse the existing finite reduction.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.bodyAt {r : ℕ} (solver : WordRAM.Code WordRAM.Basis.standard (r + 7)) : WordRAM.Code WordRAM.Basis.standard (64 + (r + 7))

The same finite loop, initialized from caller-provided raw register arguments.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.callerTime (N T : ℕ) : ℕ

Complete caller-entry instruction budget; the caller charges its final halt separately.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.Callee.not_readsWidth_bodyAt {r : ℕ} (c : Callee r) : ¬(bodyAt c.code).ReadsWidth

Caller initialization and the reused native kernels do not observe physical width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.Callee.exec_instance {r w N U src workspace s : ℕ} (c : Callee r) (μ : ℕ → ℤ) (hvalues : ∀ i < N, |μ i| ≤ ↑U) (hw : c.widthCoefficient * Nat.clog 2 (workspace + 3 * (sideLength N * sideLength N) + (2 * U + 1) + sideLength N + 2) ≤ w) (a : WordRAM.Data (r + 7)) (mem : ℕ → ℕ) (ht : a.regs (solverArg 0) = sideLength N) (hF : a.regs (solverArg 1) = 2 * U + 1) (hab : a.regs (solverArg 2) = workspace) (hbc : a.regs (solverArg 3) = workspace + sideLength N * sideLength N) (hac : a.regs (solverArg 4) = workspace + 2 * (sideLength N * sideLength N)) (hfree : a.regs (solverArg 5) = workspace + 3 * (sideLength N * sideLength N)) (hm : a.mem = (instanceArgsAt N U src workspace s μ).filled mem (sideLength N * sideLength N)) : ∃ (b : WordRAM.Data (r + 7)), WordRAM.ExecWithin w c.code a b (c.time (sideLength N) (2 * U + 1)) ∧ b.regs (solverArg 6) ≤ 1 ∧ (b.regs (solverArg 6) = 1 ↔ hit N U s μ) ∧ ∀ p < workspace, b.mem p = mem p

The finite callee's matrix contract applies to the exact memory written by the builder.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_at {r w N U src workspace : ℕ} (c : Callee r) (μ : ℕ → ℤ) (x : WordRAM.Data (64 + (r + 7))) (hN : x.regs (hostRegisters len) = N) (hU : x.regs (hostRegisters upper) = U) (hb : x.regs (hostRegisters base) = src) (hab : x.regs (hostRegisters matAB) = workspace) (hbelow : src + N ≤ workspace) (hvalues : ∀ i < N, |μ i| ≤ ↑U) (hmem : ∀ i < N, x.mem (src + i) = WordRAM.Signed.encode (μ i)) (hidx : ∀ s < 2 * sideLength N, GenericRAM.Signed.Fits w ↑(2 * (sideLength N * sideLength N) + s + 1)) (hF : GenericRAM.Signed.Fits w (2 * ↑U + 1)) (hnF : GenericRAM.Signed.Fits w (-(2 * ↑U + 1))) (hμ : ∀ i < N, GenericRAM.Signed.Fits w (μ i)) (hsize : WordRAM.Fits (w + 2) (workspace + 3 * (sideLength N * sideLength N))) (hfill : WordRAM.Fits (w + 2) (4 * U + 2)) (hsqrt : WordRAM.Fits (w + 2) (4 * N + 4)) (hcw : c.widthCoefficient * Nat.clog 2 (workspace + 3 * (sideLength N * sideLength N) + (2 * U + 1) + sideLength N + 2) ≤ w + 2) : ∃ (y : WordRAM.Data (64 + (r + 7))), WordRAM.ExecWithin (w + 2) (bodyAt c.code) x y (callerTime N (c.time (sideLength N) (2 * U + 1))) ∧ y.regs (hostRegisters found) ≤ 1 ∧ (y.regs (hostRegisters found) = 1 ↔ ThreeSum.Convolution N μ) ∧ ∀ p < workspace, y.mem p = x.mem p

Actual caller-argument execution with a Boolean Convolution verdict and a full prefix frame.