Complete native adjacent deduplication and multiplicity arrays

The input is a sorted array. The program counts one maximal adjacent run, emits its key and full count, and repeats. The output consists of two adjacent arrays, each with capacity equal to the input length. All run tests, loads, stores, address calculations and control instructions are charged. The total time is linear, including repeated keys and empty inputs.

Main definitions

• flush: store one key/count pair and advance the output cursor.
• body: count and emit one complete run.
• code: the full adjacent deduplication program.

Main results

• exec: full unique-key and multiplicity output with a linear native instruction bound.

def Cslib.Algorithms.WordRAM.Deduplicate.flush : WordRAM.Code WordRAM.Basis.standard 16

Store one key/count pair and advance the output cursor.

def Cslib.Algorithms.WordRAM.Deduplicate.body : WordRAM.Code WordRAM.Basis.standard 16

Count and emit the next maximal run.

def Cslib.Algorithms.WordRAM.Deduplicate.code : WordRAM.Code WordRAM.Basis.standard 16

Initialize the two cursors and count all adjacent runs.

theorem Cslib.Algorithms.WordRAM.Deduplicate.exec {w s base : ℕ} (xs : List ℕ) (x : WordRAM.Data 16) (hn : x.regs len = xs.length) (hs : x.regs src = s) (hk : x.regs keys = base) (hc : x.regs counts = base + xs.length) (hmem : WordRAM.Block.HoldsList s xs x.mem) (hsorted : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) xs) (hbelow : s + xs.length ≤ base) (hfit : WordRAM.Fits w (base + 2 * xs.length)) (h1 : WordRAM.Fits w 1) : ∃ (y : WordRAM.Data 16) (rs : List (ℕ × ℕ)), WordRAM.ExecWithin w code x y (29 * xs.length + 5) ∧ RunEncoding xs rs ∧ y.regs out = rs.length ∧ WordRAM.Block.HoldsList base (List.map Prod.fst rs) y.mem ∧ WordRAM.Block.HoldsList (base + xs.length) (List.map Prod.snd rs) y.mem ∧ WordRAM.Block.HoldsList s xs y.mem ∧ WordRAM.Modifies { base := base, length := 2 * xs.length }.footprint x.mem y.mem

Emit each distinct key once and its full multiplicity in at most 29n+5 instructions. The input precedes the two output blocks; no input cells or cells outside the output blocks change. Counts are ordinary unsigned words bounded by n. No restriction on key signs or canonical encodings is needed: in particular canonical Signed.encode inputs are admitted.