Preparing the native Convolution-3SUM host

The host reads the standard length header and computes a polynomial magnitude bound using the existing native parameter program. It then computes the matrix side and consecutive matrix addresses. The parameter program's additional computations are included in the instruction count.

This directly adapts the setup of Anthropic's pinned c3Body. The complete reduction must also fill every instance and invoke a concrete certified solver.

Main definitions

• Host.ParametersAt, Host.Parameters: caller-owned and standalone register interfaces.
• Host.prepare: native header, magnitude, square-root and layout computation.

Main results

• Host.exec_prepare: exact prepared parameters and a charged setup bound.

References

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

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.len : Fin 64

Input length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.upper : Fin 64

Polynomial magnitude bound.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.base : Fin 64

Input base address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.matAB : Fin 64

AB matrix base address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.matBC : Fin 64

BC matrix base address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.matAC : Fin 64

AC matrix base address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.free : Fin 64

Solver workspace starts after the three matrices.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.side : Fin 64

Number of vertices per part.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.inst : Fin 64

Current instance number.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.stop : Fin 64

Number of instances.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.found : Fin 64

Accumulated Boolean verdict.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.one : Fin 64

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.filler : Fin 64

Unsigned filler magnitude.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.encodedFiller : Fin 64

Signed-encoded positive filler.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.area : Fin 64

Number of entries per matrix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.sqrtArg : Fin 64

Square-root argument.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.sqrtRoot : Fin 64

Square-root output.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.parameterRegisters (i : Fin 24) : Fin 64

Register embedding for the existing parameter routine.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.sqrtRegisters (i : Fin 6) : Fin 64

Register embedding for successive squares.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.sideLength (N : ℕ) : ℕ

The mathematical side length used by the reduction.

structure Cslib.Algorithms.WordRAM.ThreeSum.Host.ParametersAt (N U src workspace : ℕ) (x : WordRAM.Data 64) : Prop

Runtime source and caller-owned matrix workspace retained throughout the instance loop.

• len : x.regs Host.len = N

  Input length.

• upper : x.regs Host.upper = U

  Magnitude bound.

• base : x.regs Host.base = src

  Caller-supplied input pointer.

• ab : x.regs matAB = workspace

  AB starts in the caller-owned matrix workspace.

• bc : x.regs matBC = workspace + sideLength N * sideLength N

  BC follows AB.

• ac : x.regs matAC = workspace + 2 * (sideLength N * sideLength N)

  AC follows BC.

• free : x.regs Host.free = workspace + 3 * (sideLength N * sideLength N)

  Solver scratch follows AC.

• side : x.regs Host.side = sideLength N

  Side length.

• stop : x.regs Host.stop = 2 * sideLength N

  Two instances per possible low-index sum.

• filler : x.regs Host.filler = 2 * U + 1

  Positive invalid-index filler.

• encodedFiller : x.regs Host.encodedFiller = 4 * U + 2

  Sign-and-magnitude representation of that filler.

• one : x.regs Host.one = 1

  Loop increment.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Parameters (N U : ℕ) (x : WordRAM.Data 64) : Prop

Standalone layout: input starts after header zero and matrices immediately follow it.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.parameterLen : Fin 64

Input-length output of the parameter bank.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.parameterUpper : Fin 64

Magnitude output of the parameter bank.

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

Copy the two needed parameter outputs and initialize constants.

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

Consecutive output blocks and the two loop counters.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.prepare (κ : ℕ) : WordRAM.Code WordRAM.Basis.standard 64

All initialization consists of actual native subprograms and charged register operations.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_layout_at {w N U src : ℕ} (x : WordRAM.Data 64) (hN : x.regs len = N) (hU : x.regs upper = U) (hb : x.regs base = src) (ho : x.regs one = 1) (hr : x.regs sqrtRoot = N.sqrt) (hsize : WordRAM.Fits w (N + src + 3 * (sideLength N * sideLength N))) (hfill : WordRAM.Fits w (4 * U + 2)) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin w layout x y 12 ∧ ParametersAt N U src (N + src) y ∧ y.regs inst = 0 ∧ y.regs found = 0 ∧ y.mem = x.mem

Existing layout code also supports arbitrary source placement.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_prepare {w : ℕ} (κ : ℕ) (x : WordRAM.Data 64) (hbudget : WordRAM.Fits w (ChanHe.Parameters.Math.budget (x.mem 0) ((x.mem 0 + 2) ^ κ))) (hsize : WordRAM.Fits w (x.mem 0 + 1 + 3 * (sideLength (x.mem 0) * sideLength (x.mem 0)))) (hfill : WordRAM.Fits w (4 * (x.mem 0 + 2) ^ κ + 2)) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin w (prepare κ) x y (ChanHe.Parameters.time κ (x.mem 0) ((x.mem 0 + 2) ^ κ) + 5 * (x.mem 0).sqrt + 24) ∧ Parameters (x.mem 0) ((x.mem 0 + 2) ^ κ) y ∧ y.regs inst = 0 ∧ y.regs found = 0 ∧ y.mem = x.mem

Exact initialization from the ordinary length header. The existing parameter program computes U = (N+2)^κ; its entire execution is charged, including the unused extra parameters. The additional fit premises cover matrix addresses and the encoded filler, and are independent of any solver execution contract.