Charged execution of the native Chan–He placement scan

Main results

• Place.tagged_encode: the unsigned sign/magnitude calculation is the exact tagged integer.

References

The encoding calculation and native proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.tagged_encode (neg : Bool) (z : ℤ) (t : ℕ) (ht : z.natAbs ≤ t) : WordRAM.Signed.encode (signedValue neg z + ↑t) = if WordRAM.Signed.encode z % 2 = if neg = true then 1 else 0 then 2 * t + (WordRAM.Signed.encode z / 2 + WordRAM.Signed.encode z / 2) else 2 * t - (WordRAM.Signed.encode z / 2 + WordRAM.Signed.encode z / 2)

The encoded tagged value can be computed without a signed primitive. The positive tag dominates the integer magnitude, so unsigned subtraction cannot truncate a negative result.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.budget (x : WordRAM.Data 32) (M N U t : ℕ) : ℕ

A polynomial envelope for every value and address produced by the placement scan. The caller supplies a fit for this sum; no fit of an uncomputed output is assumed.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.exec_body {w M N U t : ℕ} (x : WordRAM.Data 32) (values : ℕ → ℤ) (neg : Bool) (hM : 0 < M) (hN : 2 * M ≤ N) (hc : x.regs column < 4) (hd : x.regs distance ≤ 4 * M) (ht : U ≤ t) (hmod : x.regs modulus = M) (htag : x.regs tag = 2 * t) (hneg : x.regs negative = if neg = true then 1 else 0) (h1 : x.regs one = 1) (h2 : x.regs two = 2) (h4 : x.regs four = 4) (h0 : x.regs zero = 0) (hi : x.regs idx < x.regs len) (hcount : x.regs count = (heavyList values (x.regs len) M (x.regs idx)).length) (hbdd : (values (x.regs idx)).natAbs ≤ U) (hfit : WordRAM.Fits w (budget x M N U t)) (hinput : x.mem (x.regs src + x.regs idx) = WordRAM.Signed.encode (values (x.regs idx))) (hkey : x.mem (x.regs keys + x.regs idx) = residueKey M (values (x.regs idx))) (hhist : x.mem (x.regs hist + residueKey M (values (x.regs idx))) = Histogram.count (fun (j : ℕ) => residueKey M (values j)) (x.regs len) (residueKey M (values (x.regs idx)))) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin w body x y 30 ∧ y.mem = write x.mem values (x.regs len) M (x.regs heavy) (x.regs packed) (x.regs column) (x.regs distance) t neg (x.regs idx) ∧ y.regs count = (heavyList values (x.regs len) M (x.regs idx + 1)).length ∧ y.regs idx = x.regs idx + 1 ∧ ∀ (i : Fin 32), 9 ≤ ↑i ∧ ↑i ≤ 19 ∨ i = one ∨ i = two ∨ i = four ∨ i = zero → y.regs i = x.regs i

One complete scan round, including classification, sign/tag work, both light stores, heavy count maintenance and the input cursor increment.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.exec {w M N U t : ℕ} (x : WordRAM.Data 32) (values : ℕ → ℤ) (neg : Bool) (hM : 0 < M) (hN : 2 * M ≤ N) (hc : x.regs column < 4) (hd : x.regs distance ≤ 4 * M) (ht : U ≤ t) (hmod : x.regs modulus = M) (htag : x.regs tag = 2 * t) (hneg : x.regs negative = if neg = true then 1 else 0) (hbdd : ∀ i < x.regs len, (values i).natAbs ≤ U) (hfit : WordRAM.Fits w (budget x M N U t)) (hsh : x.regs src + x.regs len ≤ x.regs heavy) (hhp : x.regs heavy + x.regs len ≤ x.regs packed) (hpk : x.regs packed + 4 * N ≤ x.regs keys) (hkh : x.regs keys + x.regs len ≤ x.regs hist) (hinput : ∀ i < x.regs len, x.mem (x.regs src + i) = WordRAM.Signed.encode (values i)) (hkey : ∀ i < x.regs len, x.mem (x.regs keys + i) = residueKey M (values i)) (hhist : ∀ r < M, x.mem (x.regs hist + r) = Histogram.count (fun (j : ℕ) => residueKey M (values j)) (x.regs len) r) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin w program x y (32 * x.regs len + 8) ∧ y.mem = memory x.mem values (x.regs len) M (x.regs heavy) (x.regs packed) (x.regs column) (x.regs distance) t neg (x.regs len) ∧ y.regs count = (heavyList values (x.regs len) M (x.regs len)).length ∧ ∀ (i : Fin 32), 9 ≤ ↑i ∧ ↑i ≤ 19 → y.regs i = x.regs i

Complete native placement in at most 32n+8 instructions, excluding halt. All input, residue and histogram reads are proved from the memory frame, rather than assumed anew at iterations. The heavy block precedes the packed block, which precedes the counting workspace.