Self-contained Word-RAM multiply-shift hashing

This file implements the multiply-shift universal hash family of Dietzfelbinger, Hagerup, Katajainen, and Penttonen [DHKP97] as a self-contained pair of structured Word-RAM programs over Cslib.WordRAM.Basis.exact:

• Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initCode w₀: samples a uniform seed b ∈ [0, 2 ^ (w₀ - 1) - 1] into register regB in 2 instructions and 1 Instr.rand call.
• Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalCode w₀ M: deterministically computes ((2 * b + 1) * x % 2 ^ w₀) / 2 ^ (w₀ - M) in register regOut from seed b in regB and key x in regX in 9 instructions (0 rand calls) without intermediate word overflow whenever 0 < w₀, M ≤ w₀, and 2 * w₀ ≤ w.

We prove that initCode w₀ induces the exact uniform distribution PMF.uniformOfFintype (Fin (2 ^ (w₀ - 1))) on the seed register regB, that evalCode w₀ M computes Cslib.Probability.multiplyShift w₀ M b x, and hence that the Word-RAM evaluation map is (2 / 2 ^ M)-universal (isUniversalHash_evalData).

Main definitions

• regB, regX, regOut, regT1, regT2: register layout in Fin 5.
• initCode, initComp: seed-sampling code and its exact ProbComp semantics.
• evalCode, evalData: deterministic evaluation code and its closed-form final Data 5.

Main results

• initCode_execRand, initCode_execRandWithin: exact and Hoare-style execution of initCode.
• map_extractSeed_eval_initComp: the seed sampled by initCode has distribution PMF.uniformOfFintype (Fin (2 ^ (w₀ - 1))).
• evalCode_exec, evalCode_execWithin: exact 9-instruction execution of evalCode computing Cslib.Probability.multiplyShift w₀ M.
• isUniversalHash_evalData: the hash family computed in register regOut by evalCode under the seed distribution of initCode is (2 / 2 ^ M)-universal.

References

• M. Dietzfelbinger, T. Hagerup, J. Katajainen, M. Penttonen, A Reliable Randomized Algorithm for the Closest-Pair Problem, Lemma 2.4.

Register layout (Fin 5)

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.regB : Fin 5

Register 0: holds the sampled seed b < 2 ^ (w₀ - 1).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.regX : Fin 5

Register 1: holds the input key x < 2 ^ w₀.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.regOut : Fin 5

Register 2: receives the M-bit hash value multiplyShift w₀ M b x.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.regT1 : Fin 5

Register 3: first scratch register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.regT2 : Fin 5

Register 4: second scratch register.

Seed initialization (initCode)

def Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initCode (w₀ : ℕ) : WordRAM.Code WordRAM.Basis.exact 5

Structured Word-RAM program that initializes the multiply-shift seed b ∈ [0, 2 ^ (w₀ - 1) - 1] in regB using 2 instructions and 1 rand call.

def Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initData (w₀ : ℕ) (d : WordRAM.Data 5) (k : ℕ) : WordRAM.Data 5

Closed-form machine data after initCode w₀ samples k.

def Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initComp (w₀ : ℕ) (d : WordRAM.Data 5) : ProbComp (WordRAM.Data 5 × ℕ)

Exact ProbComp computation induced by initCode w₀ from initial data d.

@[simp]

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initData_regs_b (w₀ : ℕ) (d : WordRAM.Data 5) (k : ℕ) : (initData w₀ d k).regs regB = k

@[simp]

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initData_regs_x (w₀ : ℕ) (d : WordRAM.Data 5) (k : ℕ) : (initData w₀ d k).regs regX = d.regs regX

@[simp]

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initData_regs_out (w₀ : ℕ) (d : WordRAM.Data 5) (k : ℕ) : (initData w₀ d k).regs regOut = d.regs regOut

@[simp]

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initData_mem (w₀ : ℕ) (d : WordRAM.Data 5) (k : ℕ) : (initData w₀ d k).mem = d.mem

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initCode_execRand {w₀ w : ℕ} (hw : w₀ ≤ w) (d : WordRAM.Data 5) : WordRAM.ExecRand w (initCode w₀) d (initComp w₀ d)

When w₀ ≤ w, initCode w₀ executes cleanly in 2 instructions and 1 rand call with exact ProbComp semantics initComp w₀ d.

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initCode_execRandWithin {w₀ w : ℕ} (hw : w₀ ≤ w) (d : WordRAM.Data 5) : WordRAM.ExecRandWithin w (initCode w₀) d (fun (d' : WordRAM.Data 5) => d'.regs regB < 2 ^ (w₀ - 1) ∧ d'.regs regX = d.regs regX ∧ d'.regs regOut = d.regs regOut ∧ d'.mem = d.mem) 2 1

Hoare-style specification for initCode w₀: runs in 2 steps and 1 rand call, placing a seed < 2 ^ (w₀ - 1) in regB while preserving regX, regOut, and memory.

def Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.extractSeed (w₀ : ℕ) (d' : WordRAM.Data 5) : Fin (2 ^ (w₀ - 1))

Extracting the seed < 2 ^ (w₀ - 1) from register regB of a machine state d', defaulting to 0 outside the valid range.

@[simp]

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.extractSeed_initData (w₀ : ℕ) (d : WordRAM.Data 5) (k : Fin (2 ^ (w₀ - 1) - 1 + 1)) : extractSeed w₀ (initData w₀ d ↑k) = (finCongr ⋯) k

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.map_extractSeed_eval_initComp (w₀ : ℕ) (d : WordRAM.Data 5) : PMF.map (fun (z : WordRAM.Data 5 × ℕ) => extractSeed w₀ z.1) (initComp w₀ d).eval = Probability.PMF.uniformOfFintype (Fin (2 ^ (w₀ - 1)))

Uniformity of the sampled seed: the distribution of extractSeed w₀ z.1 under (initComp w₀ d).eval is the exact uniform distribution PMF.uniformOfFintype (Fin (2 ^ (w₀ - 1))).

Deterministic hash evaluation (evalCode)

def Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalCode (w₀ M : ℕ) : WordRAM.Code WordRAM.Basis.exact 5

Structured Word-RAM program that evaluates multiplyShift w₀ M in 9 deterministic instructions (0 rand calls), reading b from regB and x from regX and writing the hash value into regOut.

def Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalData (w₀ M : ℕ) (d : WordRAM.Data 5) : WordRAM.Data 5

Closed-form final machine data produced by evalCode w₀ M from d.

@[simp]

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalData_regs_out (w₀ M : ℕ) (d : WordRAM.Data 5) : (evalData w₀ M d).regs regOut = ((2 * d.regs regB + 1) * d.regs regX &&& 2 ^ w₀ - 1) >>> (w₀ - M)

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalData_regs_out_eq_multiplyShift (w₀ M : ℕ) (d : WordRAM.Data 5) (b : Fin (2 ^ (w₀ - 1))) (x : Fin (2 ^ w₀)) (hb : d.regs regB = ↑b) (hx : d.regs regX = ↑x) : (evalData w₀ M d).regs regOut = Probability.multiplyShift w₀ M b x

The output register regOut of evalData w₀ M d equals Cslib.Probability.multiplyShift w₀ M.

@[simp]

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalData_regs_b (w₀ M : ℕ) (d : WordRAM.Data 5) : (evalData w₀ M d).regs regB = d.regs regB

@[simp]

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalData_regs_x (w₀ M : ℕ) (d : WordRAM.Data 5) : (evalData w₀ M d).regs regX = d.regs regX

@[simp]

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalData_mem (w₀ M : ℕ) (d : WordRAM.Data 5) : (evalData w₀ M d).mem = d.mem

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalCode_exec {w₀ M w : ℕ} (hw₀ : 0 < w₀) (hw : 2 * w₀ ≤ w) {d : WordRAM.Data 5} (hb : d.regs regB < 2 ^ (w₀ - 1)) (hx : d.regs regX < 2 ^ w₀) : WordRAM.Exec w (evalCode w₀ M) d (evalData w₀ M d) 9

Exact 9-instruction execution of evalCode w₀ M without intermediate word overflow when 0 < w₀, 2 * w₀ ≤ w, d.regs regB < 2 ^ (w₀ - 1), and d.regs regX < 2 ^ w₀.

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.evalCode_execWithin {w₀ M w : ℕ} (hw₀ : 0 < w₀) (hw : 2 * w₀ ≤ w) {d : WordRAM.Data 5} (hb : d.regs regB < 2 ^ (w₀ - 1)) (hx : d.regs regX < 2 ^ w₀) : WordRAM.ExecWithin w (evalCode w₀ M) d (evalData w₀ M d) 9

Bounded-time execution corollary for evalCode w₀ M (9 instructions).

theorem Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.isUniversalHash_evalData {w₀ M : ℕ} (hw₀ : 0 < w₀) (hM : M ≤ w₀) (d : WordRAM.Data 5) : Probability.IsUniversalHash (PMF.map (fun (z : WordRAM.Data 5 × ℕ) => extractSeed w₀ z.1) (initComp w₀ d).eval) (fun (b : Fin (2 ^ (w₀ - 1))) (x : Fin (2 ^ w₀)) => (evalData w₀ M ((d.set regB ↑b).set regX ↑x)).regs regOut) (2 / 2 ^ M)

Universal hashing guarantee for the Word-RAM multiply-shift implementation: under the seed distribution of initCode w₀, the hash function mapping x : Fin (2 ^ w₀) to the output register regOut of evalData w₀ M is (2 / 2 ^ M)-universal whenever 0 < w₀ and M ≤ w₀.