A logarithmic word width for the Convolution-3SUM host

The existing parameter program's polynomial budget also bounds the host's matrix addresses, signed indices and filler. Four extra source bits suffice. These bounds cover the host; the concrete solver must separately prove its own execution at the target width.

Main definitions

• Host.width: a positive logarithmic source-width threshold.

Main results

• Host.layout_fits: all matrix addresses and the encoded filler fit.
• Host.index_fits, Host.filler_fits: the signed matrix-builder premises.
• Host.value_fits: polynomially bounded input values fit the signed source width.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.width (κ N : ℕ) : ℕ

Source width; the signed arithmetic kernels use unsigned target words of width w+2.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.width_pos (κ N : ℕ) : 0 < width κ N

The threshold includes the empty input and magnitude exponent zero.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.parameters_width_le (κ N : ℕ) : ChanHe.Parameters.width κ N + 4 ≤ width κ N

The host has at least four more source bits than the parameter routine requires.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.area_le (N : ℕ) : sideLength N * sideLength N ≤ 3 * N + 1

A linear bound for the number of entries per generated matrix.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.layout_fits {κ N w : ℕ} (hw : width κ N ≤ w) : WordRAM.Fits w (N + 1 + 3 * (sideLength N * sideLength N)) ∧ WordRAM.Fits w (4 * (N + 2) ^ κ + 2)

All three matrix blocks and their one-past-end addresses fit at the source width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.filler_fits {κ N w : ℕ} (hw : width κ N ≤ w) : GenericRAM.Signed.Fits w (2 * ↑((N + 2) ^ κ) + 1) ∧ GenericRAM.Signed.Fits w (-(2 * ↑((N + 2) ^ κ) + 1))

The builder's positive and negative filler fit the signed source range.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.index_fits {κ N w s : ℕ} (hw : width κ N ≤ w) (hs : s < 2 * sideLength N) : GenericRAM.Signed.Fits w ↑(2 * (sideLength N * sideLength N) + s + 1)

Every signed input index computed in a generated instance fits.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Host.value_fits {κ N w : ℕ} (hw : width κ N ≤ w) {z : ℤ} (hz : |z| ≤ ↑((N + 2) ^ κ)) : GenericRAM.Signed.Fits w z

A polynomial magnitude bound implies the signed source fit premise.