Charged word-RAM histograms

A fixed program clears a histogram and inserts the keys of a disjoint input array. An insertion into a bucket of size c creates 2c ordered collisions. Every address calculation, load, increment, store and loop test is charged.

Main definitions

• Histogram.count: bucket sizes in an input prefix.
• Histogram.pairs: ordered collisions accumulated by prefix insertion.
• Histogram.program: clear the buckets, then insert the input keys.

Main results

• Histogram.exec: histogram construction and collision counting with a linear instruction bound.

References

• T. M. Chan and Q. He, Reducing 3SUM to Convolution-3SUM

def Cslib.Algorithms.WordRAM.Histogram.count (keys : ℕ → ℕ) (k b : ℕ) : ℕ

Number of occurrences of a key among the first k input positions.

@[simp]

theorem Cslib.Algorithms.WordRAM.Histogram.count_zero (keys : ℕ → ℕ) (b : ℕ) : count keys 0 b = 0

theorem Cslib.Algorithms.WordRAM.Histogram.count_succ (keys : ℕ → ℕ) (k b : ℕ) : count keys (k + 1) b = count keys k b + if keys k = b then 1 else 0

Inserting one key changes just its bucket.

theorem Cslib.Algorithms.WordRAM.Histogram.count_le (keys : ℕ → ℕ) (k b : ℕ) : count keys k b ≤ k

A bucket cannot contain more positions than the prefix.

def Cslib.Algorithms.WordRAM.Histogram.pairs (keys : ℕ → ℕ) : ℕ → ℕ

Ordered collisions accumulated while inserting successive keys.

theorem Cslib.Algorithms.WordRAM.Histogram.pairs_le_sq (keys : ℕ → ℕ) (k : ℕ) : pairs keys k ≤ k * k

The prefix collision counter is at most the square of the prefix length.

theorem Cslib.Algorithms.WordRAM.Histogram.pairs_eq_card (keys : ℕ → ℕ) (k : ℕ) : pairs keys k = {p ∈ (Finset.range k).offDiag | keys p.1 = keys p.2}.card

The insertion counter counts exactly the ordered pairs of different positions with the same key, including when equal keys occur at different input positions.

def Cslib.Algorithms.WordRAM.Histogram.memory (mem keys : ℕ → ℕ) (dst bins k : ℕ) : ℕ → ℕ

The original memory, with the histogram block replaced by prefix bucket counts.

theorem Cslib.Algorithms.WordRAM.Histogram.memory_read (mem keys : ℕ → ℕ) (dst bins k b : ℕ) (hb : b < bins) : memory mem keys dst bins k (dst + b) = count keys k b

Reading a histogram bucket.

theorem Cslib.Algorithms.WordRAM.Histogram.memory_outside (mem keys : ℕ → ℕ) (dst bins k a : ℕ) (ha : ¬(dst ≤ a ∧ a < dst + bins)) : memory mem keys dst bins k a = mem a

Histogram writes preserve all other cells.

theorem Cslib.Algorithms.WordRAM.Histogram.memory_succ (mem keys : ℕ → ℕ) (dst bins k : ℕ) (hk : keys k < bins) : memory mem keys dst bins (k + 1) = Function.update (memory mem keys dst bins k) (dst + keys k) (count keys k (keys k) + 1)

One insertion is a single histogram-cell update.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.src : Fin 11

Input base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.dst : Fin 11

Histogram base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.len : Fin 11

Number of input keys.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.bins : Fin 11

Number of buckets.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.idx : Fin 11

Prefix length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.addr : Fin 11

Temporary address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.key : Fin 11

Current key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.bucketSize : Fin 11

Current bucket count.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.total : Fin 11

Number of ordered collisions.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.one : Fin 11

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Histogram.zero : Fin 11

Constant zero.

def Cslib.Algorithms.WordRAM.Histogram.clearBody : WordRAM.Code WordRAM.Basis.standard 11

Clear one histogram cell and advance the cursor.

def Cslib.Algorithms.WordRAM.Histogram.body : WordRAM.Code WordRAM.Basis.standard 11

Insert one key and add twice its old bucket count.

def Cslib.Algorithms.WordRAM.Histogram.clear : WordRAM.Code WordRAM.Basis.standard 11

Clear the histogram, retaining the input and all four parameters.

def Cslib.Algorithms.WordRAM.Histogram.insert : WordRAM.Code WordRAM.Basis.standard 11

Insert all keys into a cleared histogram.

def Cslib.Algorithms.WordRAM.Histogram.program : WordRAM.Code WordRAM.Basis.standard 11

Fixed code, with all bases and lengths supplied in registers.

theorem Cslib.Algorithms.WordRAM.Histogram.exec {w : ℕ} (x : WordRAM.Data 11) (keys : ℕ → ℕ) (h1 : WordRAM.Fits w 1) (hs : WordRAM.Fits w (x.regs src + x.regs len)) (hd : WordRAM.Fits w (x.regs dst + x.regs bins)) (ht : WordRAM.Fits w (x.regs len * x.regs len + x.regs len + 1)) (hdisj : x.regs src + x.regs len ≤ x.regs dst) (hkeys : ∀ i < x.regs len, keys i < x.regs bins) (hinput : ∀ i < x.regs len, x.mem (x.regs src + i) = keys i) : ∃ (y : WordRAM.Data 11), WordRAM.ExecWithin w program x y (5 * x.regs bins + 11 * x.regs len + 9) ∧ y.mem = memory x.mem keys (x.regs dst) (x.regs bins) (x.regs len) ∧ y.regs total = pairs keys (x.regs len) ∧ ∀ (i : Fin 11), ↑i < 4 → y.regs i = x.regs i

Build a histogram and count ordered collisions within 5M + 11n + 9 native instructions. The input keys lie in [0,M). The input precedes the output block. Both one-past-end addresses and the quadratic counter bound must fit. These are explicit local contracts; constructing the keys and deriving a logarithmic width are separate client obligations.