Memory frames and output readback for complete counting/placement calls #

Main results #

CountPlace.memory_outside: only the specified data, descriptor and workspace cells change.
CountPlace.memory_heavy: exact compact heavy data.
CountPlace.memory_arrXY, CountPlace.memory_arrZ: exact packed light columns.

These composition proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.memory_outside (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t scratch hist descriptor N : ℕ) (neg : Bool) (hM : 0 < M) (hN : 2 * M ≤ N) (hc : col < 4) (hd : dist ≤ 4 * M) (a : ℕ) (ho : ¬(out ≤ a ∧ a < out + n)) (hp : ¬(dst ≤ a ∧ a < dst + 4 * N)) (hk : ¬(scratch ≤ a ∧ a < scratch + n)) (hh : ¬(hist ≤ a ∧ a < hist + M)) (he : a ≠ descriptor) :

memory mem values n M out dst col dist t scratch hist descriptor neg a = mem a

No write escapes the four explicit blocks and descriptor cell.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.memory_descriptor (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t scratch hist descriptor : ℕ) (neg : Bool) :

memory mem values n M out dst col dist t scratch hist descriptor neg descriptor = (Place.heavyList values n M n).length

The count store always writes the compact output length.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.memory_heavy (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t scratch hist descriptor : ℕ) (neg : Bool) (hdisj : out + n ≤ dst) (he : descriptor < out) {j : ℕ} (hj : j < (Place.heavyList values n M n).length) :

memory mem values n M out dst col dist t scratch hist descriptor neg (out + j) = WordRAM.Signed.encode (Place.heavyList values n M n)[j]

The compact output contains the original signed encodings in input order.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.memory_other_column (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t scratch hist descriptor N : ℕ) (neg : Bool) (hdisj : out + n ≤ dst) (hc : col < 4) (hd : dist = 0 ∨ dist = 4 * M) (hk : dst + 4 * N ≤ scratch) (hh : scratch + n ≤ hist) (he : descriptor < dst) {u : ℕ} (hu : u < 4 * N) (hcol : u % 4 ≠ col) :

memory mem values n M out dst col dist t scratch hist descriptor neg (dst + u) = mem (dst + u)

The counting workspace and descriptor do not affect other packed columns.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.memory_arrXY (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col t U scratch hist descriptor N : ℕ) (hM : 0 < M) (hdisj : out + n ≤ dst) (hk : dst + 4 * N ≤ scratch) (hh : scratch + n ≤ hist) (he : descriptor < dst) (hinj : Set.InjOn values ↑(Finset.range n)) {i : ℕ} (hi : 4 * i + col < 4 * N) (hpad : mem (dst + 4 * i + col) = WordRAM.Signed.encode (ThreeSum.ChanHe.pad U + ↑t)) :

memory mem values n M out dst col 0 t scratch hist descriptor false (dst + 4 * i + col) = WordRAM.Signed.encode (ThreeSum.ChanHe.arrXY (Finset.image values (Finset.range n)) M U i + ↑t)

A complete counting/placement call writes the exact first or second light column.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.memory_arrZ (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col t U scratch hist descriptor N : ℕ) (hM : 0 < M) (hdisj : out + n ≤ dst) (hk : dst + 4 * N ≤ scratch) (hh : scratch + n ≤ hist) (he : descriptor < dst) (hinj : Set.InjOn values ↑(Finset.range n)) {i : ℕ} (hi : 4 * i + col < 4 * N) (hpad : mem (dst + 4 * i + col) = WordRAM.Signed.encode (-ThreeSum.ChanHe.pad U + ↑t)) :

memory mem values n M out dst col (4 * M) t scratch hist descriptor true (dst + 4 * i + col) = WordRAM.Signed.encode (ThreeSum.ChanHe.arrZ (Finset.image values (Finset.range n)) M U i + ↑t)

A complete counting/placement call writes the exact duplicated and negated third column.