Caller-owned Convolution-3SUM input and workspace

The caller supplies raw length, magnitude, input pointer and matrix-workspace pointer in the existing host registers. Initialization reuses the existing square-root and layout code without reading header zero. The input pointer is restored before the unchanged instance loop runs.

Main definitions

• prepareAt: prepare the actual caller-owned source and matrix blocks.

Main results

• exec_prepare_at: charged setup with exact parameters and a complete memory frame.

These native ABI composition proofs are original.

@[reducible, inline]

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

Saved caller input pointer; the existing layout and square-root banks do not change it.

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

Adapt the existing adjacent-block layout to the caller's chosen matrix start.

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

Restore the actual source pointer after computing the caller's matrix layout.

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

Initialize from actual register arguments, without touching any memory cell.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.exec_prepare_at {w N U src workspace : ℕ} (x : WordRAM.Data 64) (hN : x.regs len = N) (hU : x.regs upper = U) (hb : x.regs base = src) (hab : x.regs matAB = workspace) (hbelow : src + N ≤ workspace) (hsize : WordRAM.Fits w (workspace + 3 * (sideLength N * sideLength N))) (hfill : WordRAM.Fits w (4 * U + 2)) (hsqrt : WordRAM.Fits w (4 * N + 4)) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin w prepareAt x y (5 * N.sqrt + 24) ∧ ParametersAt N U src workspace y ∧ y.regs inst = 0 ∧ y.regs found = 0 ∧ y.mem = x.mem

Every source/layout operation is charged. The source and all other caller memory are kept.