The native Convolution-3SUM instance loop

The supplied solver is an actual finite structured program. Its six input registers hold the side, weight bound, three matrix pointers and workspace pointer; its seventh register returns an unsigned Boolean. Solver registers are disjoint from the host bank. The host writes each instance using Fill.program, copies its arguments, executes the solver and accumulates the verdict. The execution theorem requires the concrete solver's execution/correctness/frame proof; it does not establish a fast solver by assuming one.

The construction directly adapts Anthropic's pinned c3Round and c3Body.

Main definitions

• Host.instanceArgsAt, Host.instanceArgs: caller-owned and standalone matrix layouts.
• Host.hit: the mathematical verdict for one instance.
• Host.round: fill, invoke the solver and advance one instance.
• Host.loop: the complete instance loop.

References

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

def Cslib.Algorithms.WordRAM.ThreeSum.Host.instanceArgsAt (N U src workspace s : ℕ) (μ : ℕ → ℤ) : Fill.Args

The matrices occupy a caller-supplied workspace; the input has its own source pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.instanceArgs (N U s : ℕ) (μ : ℕ → ℤ) : Fill.Args

The standalone input and matrix placement is one caller-layout specialization.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.hit (N U s : ℕ) (μ : ℕ → ℤ) : Prop

The exact-triangle answer for one instance of the explicit reduction.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.fillRegisters (i : Fin 28) : Fin 64

Embed the fixed matrix-builder register bank.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.fillSetup : WordRAM.Code WordRAM.Basis.standard 64

Copy every matrix-builder argument; the builder bank occupies the first 28 registers.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.fill : WordRAM.Code WordRAM.Basis.standard 64

Matrix construction, including its argument copies.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.hostRegisters {r : ℕ} (i : Fin 64) : Fin (64 + r)

Host registers precede the solver bank.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.solverRegisters {r : ℕ} (i : Fin r) : Fin (64 + r)

The solver bank is disjoint from every host register.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.solverArg {r : ℕ} (i : Fin 7) : Fin (r + 7)

One of the seven fixed protocol registers in the solver bank.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.callRegisters {r : ℕ} (i : Fin 7) : Fin (64 + (r + 7))

Protocol registers after placing the solver after the host.

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

Prepare the solver's side, unsigned bound, AB/BC/AC pointers and free pointer.

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

Accumulate the unsigned Boolean result and advance the instance counter.

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

One complete instance, invoking the supplied finite solver in its own register bank.

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

Every one of the 2t instances is examined, without an uncharged early-exit operation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_fill_at {w N U src workspace s : ℕ} (μ : ℕ → ℤ) (x : WordRAM.Data 64) (hp : ParametersAt N U src workspace x) (hs : x.regs inst = s) (hmem : ∀ i < N, x.mem (src + i) = WordRAM.Signed.encode (μ i)) (hidx : 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))) (hbelow : src + N ≤ workspace) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin (w + 2) fill x y (131 * (sideLength N * sideLength N) + 13) ∧ ParametersAt N U src workspace y ∧ y.regs inst = s ∧ y.regs found = x.regs found ∧ y.mem = (instanceArgsAt N U src workspace s μ).filled x.mem (sideLength N * sideLength N) ∧ ∀ a < workspace, y.mem a = x.mem a

All eight argument copies and the complete matrix builder are charged. Memory before the matrix blocks is preserved; the result contains the three actual serialized matrices.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.hostRegisters_injective {r : ℕ} : Function.Injective hostRegisters

The host register bank is embedded injectively.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_round_at {w r N U src workspace s T : ℕ} (μ : ℕ → ℤ) (solver : WordRAM.Code WordRAM.Basis.standard (r + 7)) (x : WordRAM.Data (64 + (r + 7))) (hp : ParametersAt N U src workspace (WordRAM.Data.comap hostRegisters x)) (hs : x.regs (hostRegisters inst) = s) (hslt : s < 2 * sideLength N) (hf : x.regs (hostRegisters found) ≤ 1) (hmem : ∀ i < N, x.mem (src + i) = WordRAM.Signed.encode (μ i)) (hidx : 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))) (hbelow : src + N ≤ workspace) (hsolver : ∀ (a : WordRAM.Data (r + 7)) (mem : ℕ → ℕ), a.regs (solverArg 0) = sideLength N → a.regs (solverArg 1) = 2 * U + 1 → a.regs (solverArg 2) = workspace → a.regs (solverArg 3) = workspace + sideLength N * sideLength N → a.regs (solverArg 4) = workspace + 2 * (sideLength N * sideLength N) → a.regs (solverArg 5) = workspace + 3 * (sideLength N * sideLength N) → a.mem = (instanceArgsAt N U src workspace 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 < workspace, b.mem a = mem a) : ∃ (y : WordRAM.Data (64 + (r + 7))), WordRAM.ExecWithin (w + 2) (round solver) x y (131 * (sideLength N * sideLength N) + T + 23) ∧ ParametersAt N U src workspace (WordRAM.Data.comap hostRegisters y) ∧ y.regs (hostRegisters inst) = s + 1 ∧ y.regs (hostRegisters found) ≤ 1 ∧ (y.regs (hostRegisters found) = 1 ↔ x.regs (hostRegisters found) = 1 ∨ hit N U s μ) ∧ ∀ a < workspace, y.mem a = x.mem a

One generated instance, with the concrete solver's native execution proof supplied by the caller. The solver may overwrite matrices and scratch, but preserves the memory prefix below the workspace, including the supplied input. The matrices in its premise are produced by the native builder, with no supplied layout oracle.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_loop_at {w r N U src workspace T : ℕ} (μ : ℕ → ℤ) (solver : WordRAM.Code WordRAM.Basis.standard (r + 7)) (x : WordRAM.Data (64 + (r + 7))) (hp : ParametersAt N U src workspace (WordRAM.Data.comap hostRegisters x)) (hi : x.regs (hostRegisters inst) = 0) (hf : x.regs (hostRegisters found) = 0) (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))) (hbelow : src + N ≤ workspace) (hsolver : ∀ 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) = workspace → a.regs (solverArg 3) = workspace + sideLength N * sideLength N → a.regs (solverArg 4) = workspace + 2 * (sideLength N * sideLength N) → a.regs (solverArg 5) = workspace + 3 * (sideLength N * sideLength N) → a.mem = (instanceArgsAt N U src workspace 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 < workspace, b.mem a = mem a) : ∃ (y : WordRAM.Data (64 + (r + 7))), WordRAM.ExecWithin (w + 2) (loop solver) x y (2 * sideLength N * (131 * (sideLength N * sideLength N) + T + 25) + 2) ∧ ParametersAt N U src workspace (WordRAM.Data.comap hostRegisters y) ∧ y.regs (hostRegisters inst) = 2 * sideLength N ∧ y.regs (hostRegisters found) ≤ 1 ∧ (y.regs (hostRegisters found) = 1 ↔ ∃ s < 2 * sideLength N, hit N U s μ) ∧ ∀ a < workspace, y.mem a = x.mem a

The complete native instance loop. Its invariant records exactly the instances already examined, retains the original input, and charges every solver call and loop instruction.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_fill {w N U s : ℕ} (μ : ℕ → ℤ) (x : WordRAM.Data 64) (hp : Parameters N U x) (hs : x.regs inst = s) (hmem : ∀ i < N, x.mem (1 + i) = WordRAM.Signed.encode (μ i)) (hidx : 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) (N + 1 + 3 * (sideLength N * sideLength N))) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin (w + 2) fill x y (131 * (sideLength N * sideLength N) + 13) ∧ Parameters N U y ∧ y.regs inst = s ∧ y.regs found = x.regs found ∧ y.mem = (instanceArgs N U s μ).filled x.mem (sideLength N * sideLength N) ∧ ∀ a < N + 1, y.mem a = x.mem a

Standalone specialization of the caller-layout execution theorem.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_round {w r N U s T : ℕ} (μ : ℕ → ℤ) (solver : WordRAM.Code WordRAM.Basis.standard (r + 7)) (x : WordRAM.Data (64 + (r + 7))) (hp : Parameters N U (WordRAM.Data.comap hostRegisters x)) (hs : x.regs (hostRegisters inst) = s) (hslt : s < 2 * sideLength N) (hf : x.regs (hostRegisters found) ≤ 1) (hmem : ∀ i < N, x.mem (1 + i) = WordRAM.Signed.encode (μ i)) (hidx : 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) (N + 1 + 3 * (sideLength N * sideLength N))) (hsolver : ∀ (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))), WordRAM.ExecWithin (w + 2) (round solver) x y (131 * (sideLength N * sideLength N) + T + 23) ∧ Parameters N U (WordRAM.Data.comap hostRegisters y) ∧ y.regs (hostRegisters inst) = s + 1 ∧ y.regs (hostRegisters found) ≤ 1 ∧ (y.regs (hostRegisters found) = 1 ↔ x.regs (hostRegisters found) = 1 ∨ hit N U s μ) ∧ ∀ a < N + 1, y.mem a = x.mem a

Standalone specialization of the caller-layout execution theorem.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_loop {w r N U T : ℕ} (μ : ℕ → ℤ) (solver : WordRAM.Code WordRAM.Basis.standard (r + 7)) (x : WordRAM.Data (64 + (r + 7))) (hp : Parameters N U (WordRAM.Data.comap hostRegisters x)) (hi : x.regs (hostRegisters inst) = 0) (hf : x.regs (hostRegisters found) = 0) (hmem : ∀ i < N, x.mem (1 + 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) (N + 1 + 3 * (sideLength N * sideLength N))) (hsolver : ∀ 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))), WordRAM.ExecWithin (w + 2) (loop solver) x y (2 * sideLength N * (131 * (sideLength N * sideLength N) + T + 25) + 2) ∧ Parameters N U (WordRAM.Data.comap hostRegisters y) ∧ y.regs (hostRegisters inst) = 2 * sideLength N ∧ y.regs (hostRegisters found) ≤ 1 ∧ (y.regs (hostRegisters found) = 1 ↔ ∃ s < 2 * sideLength N, hit N U s μ) ∧ ∀ a < N + 1, y.mem a = x.mem a

Standalone specialization of the caller-layout execution theorem.