Native weight selection for the Convolution-3SUM reduction

Directly adapts pickStmt and putStmt of Anthropic's pinned graph builder. This code uses the existing unsigned word RAM, its sign-and-magnitude encoding, and its proved subtraction block. No source machine is copied.

One input register holds a signed index, which may be negative or out of range. The code reads only when the index is nonnegative and below N; otherwise it uses the filler. It optionally negates the selected value and stores it at a supplied destination. Addresses and lengths are unsigned; index, filler and input values are encoded signed integers. The nine arithmetic registers are scratch, and the five argument registers are preserved. Destination/input overlap is allowed for this single read-then-write operation; graph-building loops need their own frame.

The theorem charges selection, optional negation and the store, excluding a final halt. Exec.executes adds one instruction for that halt. Computing the index, arranging arguments, traversing matrices and invoking Exact Triangle are not included. This is a graph construction kernel, not a complete reduction or a subquadratic 3SUM solver.

Main definitions

• Weight.select: guarded read, falling back to the encoded filler.
• Weight.store: select, optionally negate, and store one graph weight.

Main results

• Weight.exec_store: at most twenty-eight native instructions at width w + 2.

References

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

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Weight.index : Fin 14

Encoded signed index to read.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Weight.len : Fin 14

Unsigned input length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Weight.base : Fin 14

Unsigned input base address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Weight.filler : Fin 14

Encoded fallback value.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Weight.dest : Fin 14

Unsigned destination address.

def Cslib.Algorithms.WordRAM.ThreeSum.Weight.select : WordRAM.Code WordRAM.Basis.standard 14

Select a signed input word into right, rejecting negative indices before any load.

def Cslib.Algorithms.WordRAM.ThreeSum.Weight.store (negate : Bool) : WordRAM.Code WordRAM.Basis.standard 14

Store a selected weight, optionally negated; all five argument registers are preserved.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Weight.exec_store {w N b d : ℕ} {μ : ℕ → ℤ} {fill z : ℤ} (negate : Bool) (x : WordRAM.Data 14) (hindex : x.regs index = WordRAM.Signed.encode z) (hlen : x.regs len = N) (hbase : x.regs base = b) (hfiller : x.regs filler = WordRAM.Signed.encode fill) (hdest : x.regs dest = d) (hmem : ∀ i < N, x.mem (b + i) = WordRAM.Signed.encode (μ i)) (hz : GenericRAM.Signed.Fits w z) (hfill : GenericRAM.Signed.Fits w fill) (hμ : ∀ i < N, GenericRAM.Signed.Fits w (μ i)) (haddr : WordRAM.Fits (w + 2) (b + N)) : ∃ (y : WordRAM.Data 14), WordRAM.ExecWithin (w + 2) (store negate) x y 28 ∧ y.mem = Function.update x.mem d (WordRAM.Signed.encode (if negate = true then -ThreeSum.pick N μ fill z else ThreeSum.pick N μ fill z)) ∧ ∀ (i : Fin 14), 9 ≤ ↑i → y.regs i = x.regs i

A selected signed weight is stored within twenty-eight unsigned instructions. All address arithmetic is charged, but computing the signed index and preparing arguments are caller costs. The signed bounds are satisfiable even for negative, zero and out-of-range indices.