Native matrix-building loop for Convolution-3SUM

This is a fixed native word-RAM program for one tripartite instance. Its parameters are supplied in registers. Every row/column calculation, index calculation, guarded input read, store and loop instruction is charged. The three matrices follow the input in disjoint blocks.

The construction directly adapts Anthropic's convFillBody and its prefix invariant at formal-math@16a5ce4. The graph builder does not invoke an Exact Triangle solver.

Main definitions

• Fill.body: one matrix cell and the loop-counter increment.
• Fill.program: initialize counters and fill all three matrices.

Main results

• Fill.exec: the complete matrix builder with charged time and memory correctness.

References

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

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Fill.area : Fin 28

Register holding the number of cells in each matrix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Fill.one : Fin 28

Loop increment.

def Cslib.Algorithms.WordRAM.ThreeSum.Fill.body : WordRAM.Code WordRAM.Basis.standard 28

Write all three weights at the current cell and advance the counter.

def Cslib.Algorithms.WordRAM.ThreeSum.Fill.program : WordRAM.Code WordRAM.Basis.standard 28

Initialize the counter and matrix area, then write each row-major cell.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Fill.exec {w : ℕ} (A : Args) (x : WordRAM.Data 28) (ht : x.regs Cell.side = A.t) (hs : x.regs Cell.inst = A.s) (hab : x.regs Cell.matAB = A.ab) (hbc : x.regs Cell.matBC = A.bc) (hac : x.regs Cell.matAC = A.ac) (hlen : x.regs Cell.len = A.N) (hbase : x.regs Cell.base = A.base) (hf : x.regs Cell.filler = WordRAM.Signed.encode A.filler) (hmem : ∀ i < A.N, x.mem (A.base + i) = WordRAM.Signed.encode (A.values i)) (hidx : GenericRAM.Signed.Fits w ↑(2 * (A.t * A.t) + A.s + 1)) (hF : GenericRAM.Signed.Fits w A.filler) (hnF : GenericRAM.Signed.Fits w (-A.filler)) (hμ : ∀ i < A.N, GenericRAM.Signed.Fits w (A.values i)) (haddr : WordRAM.Fits (w + 2) (A.base + A.N)) (habfit : WordRAM.Fits (w + 2) (A.ab + A.t * A.t)) (hbcfit : WordRAM.Fits (w + 2) (A.bc + A.t * A.t)) (hacfit : WordRAM.Fits (w + 2) (A.ac + A.t * A.t)) (hbelow : A.base + A.N ≤ A.ab) (hABBC : A.ab + A.t * A.t ≤ A.bc) (hBCAC : A.bc + A.t * A.t ≤ A.ac) : ∃ (y : WordRAM.Data 28), WordRAM.ExecWithin (w + 2) program x y (131 * (A.t * A.t) + 5) ∧ y.mem = A.filled x.mem (A.t * A.t) ∧ y.regs Cell.side = A.t ∧ y.regs Cell.inst = A.s ∧ y.regs Cell.matAB = A.ab ∧ y.regs Cell.matBC = A.bc ∧ y.regs Cell.matAC = A.ac ∧ y.regs Cell.len = A.N ∧ y.regs Cell.base = A.base ∧ y.regs Cell.filler = WordRAM.Signed.encode A.filler

Fill three disjoint matrices within 131t² + 5 native instructions, excluding the halt. All matrix addresses and the one-past-end addresses fit target words. The signed index bound and both signs of the filler fit the source width. The program keeps its input and parameters.