Memory layout of the Convolution-3SUM graph builder

The three matrices occupy disjoint row-major blocks following the input. This directly adapts the memory invariant of Anthropic's ConvFill.Args.filled at formal-math@16a5ce4. Values use the native signed encoding; addresses are natural numbers.

Main definitions

• Fill.Args: layout and values of one tripartite instance.
• Fill.Args.filled: the memory after writing a prefix of each matrix.

Main results

• Fill.Args.filled_succ: one round consists of exactly three writes.
• Fill.Args.input_filled: matrix writes preserve the input.
• Fill.Args.matrices_filled: the completed memory contains the mathematical reduction.

References

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

structure Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args : Type

Input length, matrix side and instance number, input base and three matrix bases, input values, and the filler. The bounds and disjointness assumptions belong to the execution theorem.

• N : ℕ

  Input length.

• t : ℕ

  Side length of each matrix.

• s : ℕ

  Instance number.

• base : ℕ

  Input base address.

• ab : ℕ

  AB matrix base address.

• bc : ℕ

  BC matrix base address.

• ac : ℕ

  AC matrix base address.

• values : ℕ → ℤ

  Mathematical input values.

• filler : ℤ

  Invalid-index filler.

def Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args.valueAB (A : Args) (q : ℕ) : ℕ

The encoded AB weight in row-major cell q.

def Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args.valueBC (A : Args) (q : ℕ) : ℕ

The encoded BC weight; a negative index is rejected before reading the input.

def Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args.valueAC (A : Args) (q : ℕ) : ℕ

The encoded AC weight; invalid entries retain the positive filler.

def Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args.filled (A : Args) (mem : ℕ → ℕ) (q : ℕ) : ℕ → ℕ

The memory after writing the first q cells of all three matrices.

@[simp]

theorem Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args.filled_zero (A : Args) (mem : ℕ → ℕ) : A.filled mem 0 = mem

A zero-length prefix leaves all memory unchanged.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args.filled_succ (A : Args) (mem : ℕ → ℕ) {q : ℕ} (hbc : A.ab + A.t * A.t ≤ A.bc) (hac : A.bc + A.t * A.t ≤ A.ac) (hq : q < A.t * A.t) : A.filled mem (q + 1) = Function.update (Function.update (Function.update (A.filled mem q) (A.ab + q) (A.valueAB q)) (A.bc + q) (A.valueBC q)) (A.ac + q) (A.valueAC q)

One round writes one cell of each matrix, in AB, BC, AC order.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args.outside_filled (A : Args) (mem : ℕ → ℕ) (q a : ℕ) (hab : ¬(A.ab ≤ a ∧ a < A.ab + q)) (hbc : ¬(A.bc ≤ a ∧ a < A.bc + q)) (hac : ¬(A.ac ≤ a ∧ a < A.ac + q)) : A.filled mem q a = mem a

Cells outside the three written prefixes retain their old contents.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args.input_filled (A : Args) (mem : ℕ → ℕ) (q : ℕ) (hinput : A.base + A.N ≤ A.ab) (hbc : A.ab ≤ A.bc) (hac : A.bc ≤ A.ac) {i : ℕ} (hi : i < A.N) : A.filled mem q (A.base + i) = mem (A.base + i)

Disjoint matrix prefixes preserve all input cells.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Fill.Args.matrices_filled (A : Args) (mem : ℕ → ℕ) (hbc : A.ab + A.t * A.t ≤ A.bc) (hac : A.bc + A.t * A.t ≤ A.ac) (a b c : Fin A.t) : A.filled mem (A.t * A.t) (A.ab + ↑a * A.t + ↑b) = WordRAM.Signed.encode (ThreeSum.weightAB A.N A.values A.filler a b) ∧ A.filled mem (A.t * A.t) (A.bc + ↑b * A.t + ↑c) = WordRAM.Signed.encode (ThreeSum.weightBC A.N A.s A.values A.filler b c) ∧ A.filled mem (A.t * A.t) (A.ac + ↑a * A.t + ↑c) = WordRAM.Signed.encode (ThreeSum.weightAC A.N A.s A.values A.filler a c)

The fully written blocks contain the three matrices of the mathematical reduction.