Compact native frontend scans

Each pass reads both canonical keys and their full multiplicities. It appends only selected keys to a disjoint destination. The singleton-zero arrays are written separately, so empty input needs no exceptional semantics.

Main definitions

• Scan.program: charged compact selection from the radix output.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.keys : Fin 48

Key pointer, count pointer and number of distinct keys.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.counts : Fin 48

Key pointer, count pointer and number of distinct keys.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.len : Fin 48

Key pointer, count pointer and number of distinct keys.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.dst : Fin 48

Output pointer, input cursor and output length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.idx : Fin 48

Output pointer, input cursor and output length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.out : Fin 48

Output pointer, input cursor and output length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.addr : Fin 48

Address scratch.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.body : WordRAM.Code WordRAM.Basis.standard 48

Load one full key/count pair, compute its selection, optionally append, and advance.

def Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.program : WordRAM.Code WordRAM.Basis.standard 48

Reset both cursors and scan all distinct keys.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.step {w : ℕ} (x : WordRAM.Data 48) (hz : x.regs Select.zero = 0) (h1 : x.regs Select.one = 1) (h2 : x.regs Select.two = 2) (h3 : x.regs Select.three = 3) (h4 : x.regs Select.four = 4) (h5 : x.regs Select.five = 5) (hsmall : WordRAM.Fits w 5) (hkaddr : WordRAM.Fits w (x.regs keys + x.regs idx)) (hcaddr : WordRAM.Fits w (x.regs counts + x.regs idx)) (hdaddr : WordRAM.Fits w (x.regs dst + x.regs out)) (hi : WordRAM.Fits w (x.regs idx + 1)) (ho : WordRAM.Fits w (x.regs out + 1)) (hkey : WordRAM.Fits w (x.mem (x.regs keys + x.regs idx))) (habs : x.mem (x.regs keys + x.regs idx) / 2 ≤ 2 * x.regs Select.magnitude) (hfit : WordRAM.Fits w (4 * x.regs Select.magnitude + 2)) (hdouble : WordRAM.Fits w (2 * x.mem (x.regs keys + x.regs idx))) : have p := (x.mem (x.regs keys + x.regs idx), x.mem (x.regs counts + x.regs idx)); have k := Math.keep (x.regs Select.magnitude) (x.regs Select.beta) (x.regs Select.beta') (x.regs Select.digit) (x.regs Select.mode) p; ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w body x y 41 ∧ y.regs idx = x.regs idx + 1 ∧ y.regs out = x.regs out + k.toNat ∧ y.mem = if k = true then Function.update x.mem (x.regs dst + x.regs out) (Math.value (x.regs Select.mode) p.1) else x.mem

One charged compacting iteration.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Scan.exec {w : ℕ} (rs : List (ℕ × ℕ)) (x : WordRAM.Data 48) (hn : x.regs len = rs.length) (hz : x.regs Select.zero = 0) (h1 : x.regs Select.one = 1) (h2 : x.regs Select.two = 2) (h3 : x.regs Select.three = 3) (h4 : x.regs Select.four = 4) (h5 : x.regs Select.five = 5) (hk : WordRAM.Block.HoldsList (x.regs keys) (List.map Prod.fst rs) x.mem) (hc : WordRAM.Block.HoldsList (x.regs counts) (List.map Prod.snd rs) x.mem) (hkey : ∀ p ∈ rs, WordRAM.Fits w p.1) (habs : ∀ p ∈ rs, p.1 / 2 ≤ 2 * x.regs Select.magnitude) (hdouble : ∀ p ∈ rs, WordRAM.Fits w (2 * p.1)) (hfit : WordRAM.Fits w (4 * x.regs Select.magnitude + 2)) (hsmall : WordRAM.Fits w 5) (hka : WordRAM.Fits w (x.regs keys + rs.length)) (hca : WordRAM.Fits w (x.regs counts + rs.length)) (hda : WordRAM.Fits w (x.regs dst + rs.length + 1)) (hkd : x.regs keys + rs.length ≤ x.regs dst) (hcd : x.regs counts + rs.length ≤ x.regs dst) : ∃ (y : WordRAM.Data 48), WordRAM.ExecWithin w program x y (43 * rs.length + 4) ∧ WordRAM.Block.HoldsList (x.regs dst) (Math.select (x.regs Select.magnitude) (x.regs Select.beta) (x.regs Select.beta') (x.regs Select.digit) (x.regs Select.mode) rs) y.mem ∧ y.regs out = (Math.select (x.regs Select.magnitude) (x.regs Select.beta) (x.regs Select.beta') (x.regs Select.digit) (x.regs Select.mode) rs).length ∧ WordRAM.Modifies { base := x.regs dst, length := rs.length }.footprint x.mem y.mem ∧ ∀ (j : Fin 48), WordRAM.Code.Preserves j body → y.regs j = x.regs j

Complete compact scan, with arbitrary old output/scratch memory and an exact memory frame. The source key/count blocks precede the output; their contents and all caller registers that the body does not write are retained.