One cell of the three Convolution-3SUM matrices

This directly adapts fillCells of Anthropic's pinned graph builder at 16a5ce41304fcdaea4e0be7c132e1c361dc26da5, using native unsigned word-RAM instructions. The row and column, all three input indices, and the three destination addresses are computed by the program. A negative BC index is replaced with the negative sentinel -1: both select the filler. Registers 22 through 25 are additional scratch; registers 14 through 21 belong to the caller. The AB and BC destinations follow the input, preserving it for subsequent reads. The final AC write may alias the input; the complete matrix loop uses disjoint blocks.

Main definitions

• Cell.step: compute and write one cell of each matrix.

Main results

• Cell.exec_step: exact memory effect and a constant charged native instruction bound.

References

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

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.cell : Fin 28

Current row-major cell.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.side : Fin 28

Number of vertices per part.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.inst : Fin 28

Instance number.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.matAB : Fin 28

Base address of matrix AB.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.matBC : Fin 28

Base address of matrix BC.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.matAC : Fin 28

Base address of matrix AC.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.len : Fin 28

Input length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.base : Fin 28

Input base address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.filler : Fin 28

Signed encoded filler.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.index : Fin 28

Encoded source index.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.dest : Fin 28

Current destination address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.saved : Fin 28

Saved encoded filler.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.negFill : Fin 28

Encoded negation of the filler.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.row : Fin 28

Computed row of the current cell.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Cell.col : Fin 28

Computed column of the current cell.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.embedding (i : Fin 14) : Fin 28

Place the fourteen weight registers at the start of the cell register file.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.writeWeight (negate : Bool) : WordRAM.Code WordRAM.Basis.standard 28

The existing weight kernel embedded in the larger register file.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.prepareSetup : WordRAM.Code WordRAM.Basis.standard 28

Save the filler, compute the coordinates and prepare its negation operands.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.prepare : WordRAM.Code WordRAM.Basis.standard 28

Compute the row and column, save the filler, and form its signed negation.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.setupAB : WordRAM.Code WordRAM.Basis.standard 28

Write the AB cell, including encoding its index and calculating its address.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.putAB : WordRAM.Code WordRAM.Basis.standard 28

Write the AB cell after computing its index and destination.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.setupBC : WordRAM.Code WordRAM.Basis.standard 28

Write BC, testing for a negative index before unsigned subtraction.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.putBC : WordRAM.Code WordRAM.Basis.standard 28

Write BC after computing its guarded signed index and destination.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.setupAC : WordRAM.Code WordRAM.Basis.standard 28

Write AC with negated filler before negating the selected value, then restore the filler.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.putAC : WordRAM.Code WordRAM.Basis.standard 28

Write AC and restore the caller's positive filler.

def Cslib.Algorithms.WordRAM.ThreeSum.Cell.step : WordRAM.Code WordRAM.Basis.standard 28

Compute and write all three entries at the current row-major cell.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Cell.exec_step {w N b ab bc ac q t s : ℕ} {μ : ℕ → ℤ} {F : ℤ} (x : WordRAM.Data 28) (hcell : x.regs cell = q) (ht : x.regs side = t) (hs : x.regs inst = s) (hab : x.regs matAB = ab) (hbc : x.regs matBC = bc) (hac : x.regs matAC = ac) (hlen : x.regs len = N) (hbase : x.regs base = b) (hf : x.regs filler = WordRAM.Signed.encode F) (hmem : ∀ i < N, x.mem (b + i) = WordRAM.Signed.encode (μ i)) (hq : q < t * t) (hidx : GenericRAM.Signed.Fits w ↑(2 * (t * t) + s + 1)) (hF : GenericRAM.Signed.Fits w F) (hnF : GenericRAM.Signed.Fits w (-F)) (hμ : ∀ i < N, GenericRAM.Signed.Fits w (μ i)) (haddr : WordRAM.Fits (w + 2) (b + N)) (habfit : WordRAM.Fits (w + 2) (ab + q)) (hbcfit : WordRAM.Fits (w + 2) (bc + q)) (hacfit : WordRAM.Fits (w + 2) (ac + q)) (hbelowAB : b + N ≤ ab) (hbelowBC : b + N ≤ bc) : ∃ (y : WordRAM.Data 28), WordRAM.ExecWithin (w + 2) step x y 128 ∧ y.mem = Function.update (Function.update (Function.update x.mem (ab + q) (WordRAM.Signed.encode (ThreeSum.pick N μ F ↑q))) (bc + q) (WordRAM.Signed.encode (ThreeSum.pick N μ F (↑(q % t * t + s) - ↑(q / t))))) (ac + q) (WordRAM.Signed.encode (-ThreeSum.pick N μ (-F) ↑((q / t + q % t) * t + s))) ∧ y.regs filler = x.regs filler ∧ ∀ (i : Fin 28), ↑i = 10 ∨ ↑i = 11 ∨ 14 ≤ ↑i ∧ ↑i ≤ 21 ∨ 26 ≤ ↑i → y.regs i = x.regs i

All index computations, three guarded loads, optional signed negation, stores and argument preparation take at most 128 native instructions. The final halt is excluded. Input cells precede all destinations; the three writes occur in AB, BC, AC order.