The complete native Convolution-3SUM host

The host computes its parameters from the ordinary input header, constructs every instance, executes the supplied finite solver program in a disjoint register bank, accumulates its answer, and halts. The source word width is logarithmic for polynomially bounded integer inputs.

This is a conditional native reduction: the caller must prove execution, correctness and input preservation of the actual solver code at the stated width and charged budget. The host does not supply a fast Exact Triangle solver or finish the subquadratic 3SUM endpoint.

The construction directly adapts Anthropic's pinned c3Body.

Main definitions

• Host.body: initialization and the complete native instance loop.
• Host.time: charged time, including the final halt.

Main results

• Host.runs_input: actual initialized native execution, output and input preservation.

References

• V. Vassilevska Williams and R. Williams, Finding, minimizing, and counting weighted subgraphs

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

The code depends only on the fixed magnitude exponent and the supplied finite solver.

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

Complete charged instruction budget, including the halt and every solver invocation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.time_bound (κ N T : ℕ) : time κ N T ≤ 2 * sideLength N * T + 1000 * (N + 1) * sideLength N + (400 * κ + 3000) * Nat.clog 2 (N + 2)

Solver time is multiplied by 2t; all host work is Oκ((N+1)t + log(N+2)).

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.runs_input {κ w r T : ℕ} (input : List ℤ) (solver : WordRAM.Code WordRAM.Basis.standard (r + 7)) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) (hsolver : have N := input.length; have U := (N + 2) ^ κ; have μ := fun (i : ℕ) => input.getD i 0; ∀ s < 2 * sideLength N, ∀ (a : WordRAM.Data (r + 7)) (mem : ℕ → ℕ), a.regs (solverArg 0) = sideLength N → a.regs (solverArg 1) = 2 * U + 1 → a.regs (solverArg 2) = N + 1 → a.regs (solverArg 3) = N + 1 + sideLength N * sideLength N → a.regs (solverArg 4) = N + 1 + 2 * (sideLength N * sideLength N) → a.regs (solverArg 5) = N + 1 + 3 * (sideLength N * sideLength N) → a.mem = (instanceArgs N U s μ).filled mem (sideLength N * sideLength N) → ∃ (b : WordRAM.Data (r + 7)), WordRAM.ExecWithin (w + 2) solver a b T ∧ b.regs (solverArg 6) ≤ 1 ∧ (b.regs (solverArg 6) = 1 ↔ hit N U s μ) ∧ ∀ a < N + 1, b.mem a = mem a) : ∃ (y : WordRAM.Data (64 + (r + 7))), ∃ t ≤ time κ input.length T, WordRAM.Runs (w + 2) ((body κ solver).program (hostRegisters found)) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) { pc := (body κ solver).size, data := y } (t - 1) ∧ WordRAM.Executes (w + 2) ((body κ solver).program (hostRegisters found)) (WordRAM.State.init (List.map WordRAM.Signed.encode input)) (y.regs (hostRegisters found)) t ∧ y.regs (hostRegisters found) ≤ 1 ∧ (y.regs (hostRegisters found) = 1 ↔ ThreeSum.Convolution input.length fun (i : ℕ) => input.getD i 0) ∧ (∀ a < input.length + 1, y.mem a = (WordRAM.Data.init (List.map WordRAM.Signed.encode input)).mem a) ∧ WordRAM.Data.Bounded (w + 2) y

Native initialized execution at target width w+2. The execution witness identifies the actual pre-halt state containing the output. The sole solver premise is an execution theorem for the concrete solver argument, on the matrices the host actually constructs.