diff --git a/Complexity.lean b/Complexity.lean index db61c5ea8..85da76cde 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -6,6 +6,7 @@ public import Complexity.Algorithms.ExactTriangle.Lopsided public import Complexity.Algorithms.ExactTriangle.Splitting public import Complexity.Algorithms.ExactTriangle.Weights public import Complexity.Algorithms.ExactTriangle.Witnesses +public import Complexity.Algorithms.Lean.Dictionary public import Complexity.Algorithms.Lean.FusionTree.Capacity public import Complexity.Algorithms.Lean.FusionTree.Compression public import Complexity.Algorithms.Lean.FusionTree.Correction @@ -147,6 +148,7 @@ public import Complexity.Algorithms.WordRAM.FusionTree.Query.Traversal public import Complexity.Algorithms.WordRAM.FusionTree.Rank public import Complexity.Algorithms.WordRAM.FusionTree.ReadHeader public import Complexity.Algorithms.WordRAM.FusionTree.Static +public import Complexity.Algorithms.WordRAM.Hashing.MultiplyShift public import Complexity.Algorithms.WordRAM.Histogram public import Complexity.Algorithms.WordRAM.Karger.Contract public import Complexity.Algorithms.WordRAM.Karger.FastCut @@ -2454,6 +2456,7 @@ public import Complexity.Foundations.Data.BitString.ParityTestBounds public import Complexity.Foundations.Data.BitString.ParityTests public import Complexity.Foundations.Data.BitString.PartialAssignment public import Complexity.Foundations.Data.BitString.PartialAssignment.Counting +public import Complexity.Foundations.Data.BitString.Prefix public import Complexity.Foundations.Data.BitString.Propagation public import Complexity.Foundations.Data.BitString.ShortWords public import Complexity.Foundations.Data.BitString.Sign @@ -2582,6 +2585,7 @@ public import Complexity.Foundations.FieldTheory.Finite.BinaryField public import Complexity.Foundations.FieldTheory.Finite.LinearizedPolynomial public import Complexity.Foundations.FieldTheory.Finite.ReducedMonomial public import Complexity.Foundations.FieldTheory.Finite.Subfield +public import Complexity.Foundations.FieldTheory.Finite.Trinomial public import Complexity.Foundations.FieldTheory.Finite.UnitSum public import Complexity.Foundations.FieldTheory.TensorBasis public import Complexity.Foundations.Geometry.Euclidean.Angle.Cap @@ -2887,6 +2891,7 @@ public import Complexity.Probability.IID public import Complexity.Probability.Isolation public import Complexity.Probability.KWiseIndependent public import Complexity.Probability.KWiseIndependent.Polynomial +public import Complexity.Probability.KWiseIndependent.Trinomial public import Complexity.Probability.LocalLemma public import Complexity.Probability.LoomisWhitney public import Complexity.Probability.MinEntropy diff --git a/Complexity/Algorithms/Lean/Dictionary.lean b/Complexity/Algorithms/Lean/Dictionary.lean new file mode 100644 index 000000000..23dc36016 --- /dev/null +++ b/Complexity/Algorithms/Lean/Dictionary.lean @@ -0,0 +1,234 @@ +/- +Copyright (c) 2026 Renfei Zhou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Renfei Zhou +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Foundations.Semantics.Stateful.Basic +public import Mathlib.Data.Fintype.Basic + +/-! +# Bounded-capacity dictionary specification + +This file defines a deterministic abstract specification +(`Cslib.Algorithms.Lean.Dictionary.spec`) for a bounded-capacity dictionary mapping keys from a +finite universe `Fin U` to natural-number values bounded by `V`, supporting at most `n_max` +distinct stored keys at any point in time. + +States map each key `u : Fin U` to `Option ℕ` (`none` when absent, `some v` when present with +value `v`). Following `Cslib.Algorithms.Lean.IndexedMinPQ`, values are represented as `ℕ` with the +bound `v < V` enforced by operation admissibility (`valid`), so Word-RAM realizations can encode +`Option ℕ` in a single machine register (`0` for `none` and `v + 1` for `some v`) without carrying +dependent `Fin V` proof obligations inside register decoding. + +An insertion `insert u v` is admissible whenever `v < V` and either the current number of stored +keys `(dom s).card` is strictly below the capacity bound `n_max`, or `u` is already present in `s` +(in which case updating `s u` to `some v` overwrites the existing value in place without increasing +`(dom s).card`). This specification models lookup-and-insert dictionaries without a deletion +operation. + +## Main definitions + +* `Cslib.Algorithms.Lean.Dictionary.Op`: dictionary operations (`get`, `insert`). +* `Cslib.Algorithms.Lean.Dictionary.State`, `empty`, `dom`: abstract map state, empty dictionary, + and finite set of present keys. +* `Cslib.Algorithms.Lean.Dictionary.ValuesBounded`: invariant that all stored values lie below `V`. +* `Cslib.Algorithms.Lean.Dictionary.spec`: the `Cslib.Stateful.Spec` with universe `U`, value bound + `V`, and capacity bound `n_max`. + +## Main results + +* `dom_empty`, `card_dom_empty`, `dom_insert`: domain evolution under initialization and insertion. +* `card_dom_insert_le`, `card_dom_insert_eq_of_isSome`, `card_dom_insert_eq_of_eq_none`: + cardinality laws for `dom` under in-place updates and new-key insertions. +* `card_dom_step_le_of_valid`, `card_dom_run_le_of_validHistory`, `card_dom_run_empty_le`: + any admissible operation history starting from `empty U` maintains `(dom s).card ≤ n_max`. +* `valuesBounded_empty`, `valuesBounded_step_of_valid`, `valuesBounded_run_of_validHistory`: + any admissible operation history maintains `ValuesBounded V s`. + +## References + +* [T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, *Introduction to Algorithms*, + Chapter 11][CLRS2009] +-/ + +public section + +namespace Cslib.Algorithms.Lean.Dictionary + +/-- Lookup and insertion operations on a dictionary over keys `Fin U` and natural-number values. -/ +inductive Op (U : ℕ) where + /-- Look up the value associated with key `u`, if present. -/ + | get (u : Fin U) + /-- Associate key `u` with value `v`, inserting `u` if absent or overwriting its value if + present. -/ + | insert (u : Fin U) (v : ℕ) + deriving DecidableEq, Repr + +/-- Abstract state of a dictionary over universe `Fin U`. -/ +abbrev State (U : ℕ) := Fin U → Option ℕ + +/-- The empty dictionary on `Fin U`. -/ +@[expose] +def empty (U : ℕ) : State U := fun _ => none + +/-- The finite set of keys currently present in state `s`. -/ +@[expose] +def dom {U : ℕ} (s : State U) : Finset (Fin U) := + Finset.univ.filter fun u => (s u).isSome + +/-- Predicate asserting that every value stored in state `s` is strictly less than `V`. -/ +@[expose] +def ValuesBounded {U : ℕ} (V : ℕ) (s : State U) : Prop := + ∀ u v, s u = some v → v < V + +/-- Bounded-capacity dictionary specification over key universe `Fin U`, value bound `V`, and +maximum key count `n_max`. -/ +@[expose] +def spec (U V n_max : ℕ) : Cslib.Stateful.Spec where + State := State U + Op := Op U + Result + | .get _ => Option ℕ + | .insert _ _ => Unit + step s + | .get u => (s, s u) + | .insert u v => (Function.update s u (some v), ()) + valid s + | .get _ => True + | .insert u v => ((dom s).card < n_max ∨ (s u).isSome) ∧ v < V + +/-! ### Domain, capacity, and value-bound lemmas -/ + +/-- A key belongs to `dom s` if and only if `(s u).isSome`. -/ +@[simp] +theorem mem_dom_iff_isSome {U : ℕ} {s : State U} {u : Fin U} : + u ∈ dom s ↔ (s u).isSome := by + simp [dom] + +/-- A key belongs to `dom s` if and only if `s u = some v` for some value `v`. -/ +theorem mem_dom_iff {U : ℕ} {s : State U} {u : Fin U} : + u ∈ dom s ↔ ∃ v, s u = some v := by + simp [dom, Option.isSome_iff_exists] + +/-- A key is outside `dom s` if and only if `s u = none`. -/ +theorem notMem_dom_iff {U : ℕ} {s : State U} {u : Fin U} : + u ∉ dom s ↔ s u = none := by + simp [dom] + +/-- The empty dictionary has empty domain. -/ +@[simp] +theorem dom_empty (U : ℕ) : dom (empty U) = ∅ := by + ext u + simp [dom, empty] + +/-- The empty dictionary stores `0` keys. -/ +theorem card_dom_empty (U : ℕ) : (dom (empty U)).card = 0 := by + simp + +/-- Updating `u` to `some v` inserts `u` into `dom s`. -/ +@[simp] +theorem dom_insert {U : ℕ} (s : State U) (u : Fin U) (v : ℕ) : + dom (Function.update s u (some v)) = insert u (dom s) := by + ext x + by_cases hxu : x = u + · subst hxu; simp [dom] + · simp [dom, hxu] + +/-- Updating a key `u` already in `dom s` preserves `dom s`. -/ +theorem dom_insert_of_mem {U : ℕ} {s : State U} {u : Fin U} (hu : u ∈ dom s) (v : ℕ) : + dom (Function.update s u (some v)) = dom s := by + rw [dom_insert, Finset.insert_eq_of_mem hu] + +/-- Updating a key `u` with `(s u).isSome` preserves `dom s`. -/ +theorem dom_insert_of_isSome {U : ℕ} {s : State U} {u : Fin U} (hu : (s u).isSome) (v : ℕ) : + dom (Function.update s u (some v)) = dom s := + dom_insert_of_mem (mem_dom_iff_isSome.mpr hu) v + +/-- Updating `u` to `some v` increases `(dom s).card` by at most `1`. -/ +theorem card_dom_insert_le {U : ℕ} (s : State U) (u : Fin U) (v : ℕ) : + (dom (Function.update s u (some v))).card ≤ (dom s).card + 1 := by + rw [dom_insert] + exact Finset.card_insert_le u (dom s) + +/-- Updating a present key `u` (`(s u).isSome`) leaves `(dom s).card` unchanged. -/ +theorem card_dom_insert_eq_of_isSome {U : ℕ} {s : State U} {u : Fin U} + (hu : (s u).isSome) (v : ℕ) : + (dom (Function.update s u (some v))).card = (dom s).card := by + rw [dom_insert_of_isSome hu] + +/-- Inserting an absent key `u` (`s u = none`) increases `(dom s).card` by `1`. -/ +theorem card_dom_insert_eq_of_eq_none {U : ℕ} {s : State U} {u : Fin U} + (hu : s u = none) (v : ℕ) : + (dom (Function.update s u (some v))).card = (dom s).card + 1 := by + rw [dom_insert, Finset.card_insert_of_notMem (notMem_dom_iff.mpr hu)] + +/-- Any single admissible dictionary operation preserves the capacity bound +`(dom s).card ≤ n_max`. -/ +theorem card_dom_step_le_of_valid {U V n_max : ℕ} {s : State U} {o : Op U} + (hs : (dom s).card ≤ n_max) (hval : (spec U V n_max).valid s o) : + (dom ((spec U V n_max).step s o).1).card ≤ n_max := by + cases o with + | get u => exact hs + | insert u v => + rcases hval.1 with hlt | hisSome + · have hle := card_dom_insert_le s u v + dsimp only [spec] + omega + · dsimp only [spec] + rw [card_dom_insert_eq_of_isSome hisSome] + exact hs + +/-- Any admissible operation history preserves `(dom s).card ≤ n_max`. -/ +theorem card_dom_run_le_of_validHistory {U V n_max : ℕ} {s : State U} {os : List (Op U)} + (hs : (dom s).card ≤ n_max) (hvh : (spec U V n_max).ValidHistory s os) : + (dom ((spec U V n_max).run s os).1).card ≤ n_max := by + induction os generalizing s with + | nil => exact hs + | cons o os ih => + exact ih (card_dom_step_le_of_valid hs hvh.1) hvh.2 + +/-- Any admissible operation history starting from `empty U` reaches a state with at most `n_max` +keys. -/ +theorem card_dom_run_empty_le {U V n_max : ℕ} {os : List (Op U)} + (hvh : (spec U V n_max).ValidHistory (empty U) os) : + (dom ((spec U V n_max).run (empty U) os).1).card ≤ n_max := + card_dom_run_le_of_validHistory (by simp) hvh + +/-- The empty dictionary satisfies `ValuesBounded V`. -/ +theorem valuesBounded_empty (U V : ℕ) : ValuesBounded V (empty U) := by + intro u v h + simp [empty] at h + +/-- Any single admissible dictionary operation preserves `ValuesBounded V`. -/ +theorem valuesBounded_step_of_valid {U V n_max : ℕ} {s : State U} {o : Op U} + (hs : ValuesBounded V s) (hval : (spec U V n_max).valid s o) : + ValuesBounded V ((spec U V n_max).step s o).1 := by + cases o with + | get u => exact hs + | insert u v => + intro x w hxw + dsimp only [spec] at hxw + by_cases hxu : x = u + · subst hxu + rw [Function.update_self] at hxw + injection hxw with hvw + subst hvw + exact hval.2 + · rw [Function.update_of_ne hxu] at hxw + exact hs x w hxw + +/-- Any admissible operation history preserves `ValuesBounded V`. -/ +theorem valuesBounded_run_of_validHistory {U V n_max : ℕ} {s : State U} {os : List (Op U)} + (hs : ValuesBounded V s) (hvh : (spec U V n_max).ValidHistory s os) : + ValuesBounded V ((spec U V n_max).run s os).1 := by + induction os generalizing s with + | nil => exact hs + | cons o os ih => + exact ih (valuesBounded_step_of_valid hs hvh.1) hvh.2 + +end Cslib.Algorithms.Lean.Dictionary diff --git a/Complexity/Algorithms/WordRAM/Hashing/MultiplyShift.lean b/Complexity/Algorithms/WordRAM/Hashing/MultiplyShift.lean new file mode 100644 index 000000000..1fa41f673 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/Hashing/MultiplyShift.lean @@ -0,0 +1,364 @@ +/- +Copyright (c) 2026 Renfei Zhou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Renfei Zhou +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Randomized.Structured +public import Complexity.Probability.HashFamily.MultiplyShift + +/-! +# Self-contained Word-RAM multiply-shift hashing + +This file implements the multiply-shift universal hash family of Dietzfelbinger, Hagerup, +Katajainen, and Penttonen [DietzfelbingerHagerupKatajainenPenttonen1997] 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*][DietzfelbingerHagerupKatajainenPenttonen1997], Lemma 2.4. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.Hashing.MultiplyShift + +open Cslib.WordRAM Cslib.Probability +open scoped ENNReal + +/-! ## Register layout (`Fin 5`) -/ + +/-- Register `0`: holds the sampled seed `b < 2 ^ (w₀ - 1)`. -/ +abbrev regB : Fin 5 := 0 + +/-- Register `1`: holds the input key `x < 2 ^ w₀`. -/ +abbrev regX : Fin 5 := 1 + +/-- Register `2`: receives the `M`-bit hash value `multiplyShift w₀ M b x`. -/ +abbrev regOut : Fin 5 := 2 + +/-- Register `3`: first scratch register. -/ +abbrev regT1 : Fin 5 := 3 + +/-- Register `4`: second scratch register. -/ +abbrev regT2 : Fin 5 := 4 + +/-! ## Seed initialization (`initCode`) -/ + +/-- 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. -/ +@[expose] +def initCode (w₀ : ℕ) : Code .exact 5 := + .seq (.op (.const regT1 (2 ^ (w₀ - 1) - 1))) + (.rand regB regT1) + +/-- Closed-form machine data after `initCode w₀` samples `k`. -/ +@[expose] +def initData (w₀ : ℕ) (d : Data 5) (k : ℕ) : Data 5 := + (d.set regT1 (2 ^ (w₀ - 1) - 1)).set regB k + +/-- Exact `ProbComp` computation induced by `initCode w₀` from initial data `d`. -/ +@[expose] +def initComp (w₀ : ℕ) (d : Data 5) : ProbComp (Data 5 × ℕ) := do + let k ← ProbComp.unifFin (2 ^ (w₀ - 1) - 1) + pure (initData w₀ d k.val, 2) + +@[simp] +theorem initData_regs_b (w₀ : ℕ) (d : Data 5) (k : ℕ) : + (initData w₀ d k).regs regB = k := by + simp [initData] + +@[simp] +theorem initData_regs_x (w₀ : ℕ) (d : Data 5) (k : ℕ) : + (initData w₀ d k).regs regX = d.regs regX := by + simp [initData, regB, regX, regT1] + +@[simp] +theorem initData_regs_out (w₀ : ℕ) (d : Data 5) (k : ℕ) : + (initData w₀ d k).regs regOut = d.regs regOut := by + simp [initData, regB, regOut, regT1] + +@[simp] +theorem initData_mem (w₀ : ℕ) (d : Data 5) (k : ℕ) : + (initData w₀ d k).mem = d.mem := by rfl + +private theorem fits_two_pow_pred_sub_one {w₀ w : ℕ} (hw : w₀ ≤ w) : + Fits w (2 ^ (w₀ - 1) - 1) := by + rw [fits_iff] + have h1 : 2 ^ (w₀ - 1) - 1 < 2 ^ (w₀ - 1) := Nat.sub_lt (by positivity) one_pos + have h2 : 2 ^ (w₀ - 1) ≤ 2 ^ w := Nat.pow_le_pow_right two_pos (by omega) + exact h1.trans_le h2 + +/-- When `w₀ ≤ w`, `initCode w₀` executes cleanly in `2` instructions and `1` `rand` call with exact +`ProbComp` semantics `initComp w₀ d`. -/ +theorem initCode_execRand {w₀ w : ℕ} (hw : w₀ ≤ w) (d : Data 5) : + ExecRand w (initCode w₀) d (initComp w₀ d) := by + have hfit : Fits w (2 ^ (w₀ - 1) - 1) := fits_two_pow_pred_sub_one hw + set d1 := d.set regT1 (2 ^ (w₀ - 1) - 1) + have hd1 : d1.regs regT1 = 2 ^ (w₀ - 1) - 1 := by simp [d1] + have h1 : Exec w (.op (.const regT1 (2 ^ (w₀ - 1) - 1)) : Code .exact 5) d d1 1 := + Exec.const hfit + have hfit' : Fits w (d1.regs regT1) := by + rw [hd1] + exact hfit + have h2 := ExecRand.rand (B := .exact) (w := w) (dst := regB) (src := regT1) (x := d1) hfit' + rw [hd1] at h2 + have hseq := h1.seqRand h2 + have heq : ((fun z : Data 5 × ℕ => (z.1, 1 + z.2)) <$> (do + let k ← ProbComp.unifFin (2 ^ (w₀ - 1) - 1) + pure (d1.set regB k.val, 1))) = initComp w₀ d := by + simp [initComp, initData, d1, ← bind_pure_comp, bind_assoc] + rwa [heq] at hseq + +/-- 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. -/ +theorem initCode_execRandWithin {w₀ w : ℕ} (hw : w₀ ≤ w) (d : Data 5) : + ExecRandWithin w (initCode w₀) d + (fun d' => d'.regs regB < 2 ^ (w₀ - 1) ∧ + d'.regs regX = d.regs regX ∧ + d'.regs regOut = d.regs regOut ∧ + d'.mem = d.mem) 2 1 := by + refine ⟨initComp w₀ d, initCode_execRand hw d, ?_, ?_⟩ + · dsimp only [initComp] + simpa only [Nat.add_zero] using + (ProbComp.isQueryBounded_unifFin (2 ^ (w₀ - 1) - 1)).bind fun _ => .pure _ 0 + · intro z hz + dsimp only [initComp] at hz + obtain ⟨k, -, hk⟩ := OracleComp.mem_supportWith_bind_iff.mp hz + cases OracleComp.eq_of_mem_supportWith_pure hk + have hlt : k.val < 2 ^ (w₀ - 1) := by + have hpos : 1 ≤ 2 ^ (w₀ - 1) := Nat.one_le_two_pow + have hk_lt := k.isLt + omega + exact ⟨⟨by simpa using hlt, by simp, by simp, rfl⟩, le_rfl⟩ + +/-- Extracting the seed `< 2 ^ (w₀ - 1)` from register `regB` of a machine state `d'`, defaulting to +`0` outside the valid range. -/ +@[expose] +def extractSeed (w₀ : ℕ) (d' : Data 5) : Fin (2 ^ (w₀ - 1)) := + if h : d'.regs regB < 2 ^ (w₀ - 1) then ⟨d'.regs regB, h⟩ + else ⟨0, by positivity⟩ + +@[simp] +theorem extractSeed_initData (w₀ : ℕ) (d : Data 5) (k : Fin (2 ^ (w₀ - 1) - 1 + 1)) : + extractSeed w₀ (initData w₀ d k.val) = + finCongr (Nat.sub_add_cancel Nat.one_le_two_pow) k := by + have hlt : k.val < 2 ^ (w₀ - 1) := by + have hpos : 1 ≤ 2 ^ (w₀ - 1) := Nat.one_le_two_pow + have hk_lt := k.isLt + omega + apply Fin.ext + simp [extractSeed, hlt] + +/-- **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)))`. -/ +theorem map_extractSeed_eval_initComp (w₀ : ℕ) (d : Data 5) : + ((initComp w₀ d).eval).map (fun z => extractSeed w₀ z.1) = + PMF.uniformOfFintype (Fin (2 ^ (w₀ - 1))) := by + have heval : (initComp w₀ d).eval = + (PMF.uniformOfFintype (Fin (2 ^ (w₀ - 1) - 1 + 1))).map + (fun k => (initData w₀ d k.val, 2)) := by + rw [initComp, bind_pure_comp, ProbComp.eval_map, ProbComp.eval_unifFin] + rw [heval, PMF.map_comp] + have hcomp : ((fun z : Data 5 × ℕ => extractSeed w₀ z.1) ∘ + fun k : Fin (2 ^ (w₀ - 1) - 1 + 1) => (initData w₀ d k.val, 2)) = + finCongr (Nat.sub_add_cancel Nat.one_le_two_pow) := by + funext k + exact extractSeed_initData w₀ d k + rw [hcomp] + exact PMF.uniformOfFintype_map_equiv (finCongr (Nat.sub_add_cancel Nat.one_le_two_pow)) + +/-! ## Deterministic hash evaluation (`evalCode`) -/ + +/-- 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`. -/ +@[expose] +def evalCode (w₀ M : ℕ) : Code .exact 5 := + .seq (.op (.const regT1 2)) + (.seq (.op (.exactBin .mul regT1 regT1 regB)) + (.seq (.op (.const regT2 1)) + (.seq (.op (.exactBin .add regT1 regT1 regT2)) + (.seq (.op (.exactBin .mul regT1 regT1 regX)) + (.seq (.op (.const regT2 (2 ^ w₀ - 1))) + (.seq (.op (.exactBin .and regT1 regT1 regT2)) + (.seq (.op (.const regT2 (w₀ - M))) + (.op (.exactBin .shiftRight regOut regT1 regT2))))))))) + +/-- Closed-form final machine data produced by `evalCode w₀ M` from `d`. -/ +@[expose] +def evalData (w₀ M : ℕ) (d : Data 5) : Data 5 := + let b := d.regs regB + let x := d.regs regX + let low := ((2 * b + 1) * x) &&& (2 ^ w₀ - 1) + (((d.set regT1 low).set regT2 (w₀ - M)).set regOut (low >>> (w₀ - M))) + +@[simp] +theorem evalData_regs_out (w₀ M : ℕ) (d : Data 5) : + (evalData w₀ M d).regs regOut = + (((2 * d.regs regB + 1) * d.regs regX) &&& (2 ^ w₀ - 1)) >>> (w₀ - M) := by + simp [evalData] + +/-- The output register `regOut` of `evalData w₀ M d` equals +`Cslib.Probability.multiplyShift w₀ M`. -/ +theorem evalData_regs_out_eq_multiplyShift (w₀ M : ℕ) (d : Data 5) + (b : Fin (2 ^ (w₀ - 1))) (x : Fin (2 ^ w₀)) + (hb : d.regs regB = b.val) (hx : d.regs regX = x.val) : + (evalData w₀ M d).regs regOut = multiplyShift w₀ M b x := by + rw [evalData_regs_out, hb, hx, Nat.and_two_pow_sub_one_eq_mod, Nat.shiftRight_eq_div_pow, + multiplyShift] + +@[simp] +theorem evalData_regs_b (w₀ M : ℕ) (d : Data 5) : + (evalData w₀ M d).regs regB = d.regs regB := by + simp [evalData, regB, regOut, regT1, regT2] + +@[simp] +theorem evalData_regs_x (w₀ M : ℕ) (d : Data 5) : + (evalData w₀ M d).regs regX = d.regs regX := by + simp [evalData, regX, regOut, regT1, regT2] + +@[simp] +theorem evalData_mem (w₀ M : ℕ) (d : Data 5) : + (evalData w₀ M d).mem = d.mem := by rfl + +/-- **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 evalCode_exec {w₀ M w : ℕ} (hw₀ : 0 < w₀) (hw : 2 * w₀ ≤ w) + {d : Data 5} (hb : d.regs regB < 2 ^ (w₀ - 1)) (hx : d.regs regX < 2 ^ w₀) : + Exec w (evalCode w₀ M) d (evalData w₀ M d) 9 := by + set b := d.regs regB + set x := d.regs regX + have hw₀_le : w₀ ≤ w := by omega + have hpow_w₀ : 2 ^ w₀ ≤ 2 ^ w := Nat.pow_le_pow_right two_pos hw₀_le + have h2b1_lt : 2 * b + 1 < 2 ^ w₀ := by + have hpow1 : 2 * 2 ^ (w₀ - 1) = 2 ^ w₀ := by + conv_rhs => rw [← Nat.sub_add_cancel hw₀, pow_succ'] + omega + have hfit_2 : Fits w 2 := by + rw [fits_iff] + have h4 : 4 ≤ 2 ^ w := + calc 4 = 2 ^ 2 := by decide + _ ≤ 2 ^ w := Nat.pow_le_pow_right two_pos (by omega) + omega + have hfit_2b : Fits w (2 * b) := by + rw [fits_iff] + exact (by omega : 2 * b < 2 * b + 1).trans (h2b1_lt.trans_le hpow_w₀) + have hfit_1 : Fits w 1 := fits_one (by omega) + have hfit_2b1 : Fits w (2 * b + 1) := by + rw [fits_iff] + exact h2b1_lt.trans_le hpow_w₀ + have hfit_prod : Fits w ((2 * b + 1) * x) := by + rw [fits_iff] + calc (2 * b + 1) * x < 2 ^ w₀ * 2 ^ w₀ := + Nat.mul_lt_mul_of_lt_of_lt h2b1_lt hx + _ = 2 ^ (2 * w₀) := by rw [two_mul, pow_add] + _ ≤ 2 ^ w := Nat.pow_le_pow_right two_pos hw + have hfit_mask : Fits w (2 ^ w₀ - 1) := by + rw [fits_iff] + exact (Nat.sub_lt (by positivity) one_pos).trans_le hpow_w₀ + have hlow_lt : ((2 * b + 1) * x) &&& (2 ^ w₀ - 1) < 2 ^ w₀ := by + rw [Nat.and_two_pow_sub_one_eq_mod] + exact Nat.mod_lt _ (by positivity) + have hfit_low : Fits w (((2 * b + 1) * x) &&& (2 ^ w₀ - 1)) := by + rw [fits_iff] + exact hlow_lt.trans_le hpow_w₀ + have hfit_shift : Fits w (w₀ - M) := by + rw [fits_iff] + exact (Nat.sub_le w₀ M).trans_lt (Nat.lt_two_pow_self.trans_le hpow_w₀) + have hfit_out : Fits w ((((2 * b + 1) * x) &&& (2 ^ w₀ - 1)) >>> (w₀ - M)) := by + rw [fits_iff, Nat.shiftRight_eq_div_pow] + exact (Nat.div_le_self _ _).trans_lt (hlow_lt.trans_le hpow_w₀) + set d1 := d.set regT1 2 + have s1 : Exec w (.op (.const regT1 2) : Code .exact 5) d d1 1 := Exec.const hfit_2 + set d2 := d1.set regT1 (2 * b) + have s2 : Exec w (.op (.exactBin .mul regT1 regT1 regB)) d1 d2 1 := + Exec.alu (by simp [StandardOp.evalExact, d1, b, regT1, regB]) hfit_2b + set d3 := d2.set regT2 1 + have s3 : Exec w (.op (.const regT2 1) : Code .exact 5) d2 d3 1 := Exec.const hfit_1 + set d4 := d3.set regT1 (2 * b + 1) + have s4 : Exec w (.op (.exactBin .add regT1 regT1 regT2)) d3 d4 1 := + Exec.alu (by simp [StandardOp.evalExact, d3, d2, regT1, regT2]) hfit_2b1 + set d5 := d4.set regT1 ((2 * b + 1) * x) + have s5 : Exec w (.op (.exactBin .mul regT1 regT1 regX)) d4 d5 1 := + Exec.alu (by simp [StandardOp.evalExact, d4, d3, d2, d1, x, regT1, regT2, regX]) hfit_prod + set d6 := d5.set regT2 (2 ^ w₀ - 1) + have s6 : Exec w (.op (.const regT2 (2 ^ w₀ - 1)) : Code .exact 5) d5 d6 1 := + Exec.const hfit_mask + set d7 := d6.set regT1 (((2 * b + 1) * x) &&& (2 ^ w₀ - 1)) + have s7 : Exec w (.op (.exactBin .and regT1 regT1 regT2)) d6 d7 1 := + Exec.alu (by simp [StandardOp.evalExact, d6, d5, regT1, regT2]) hfit_low + set d8 := d7.set regT2 (w₀ - M) + have s8 : Exec w (.op (.const regT2 (w₀ - M)) : Code .exact 5) d7 d8 1 := + Exec.const hfit_shift + set d9 := d8.set regOut ((((2 * b + 1) * x) &&& (2 ^ w₀ - 1)) >>> (w₀ - M)) + have s9 : Exec w (.op (.exactBin .shiftRight regOut regT1 regT2)) d8 d9 1 := + Exec.alu (by simp [StandardOp.evalExact, d8, d7, regT1, regT2]) hfit_out + have hseq := s1.seq (s2.seq (s3.seq (s4.seq (s5.seq (s6.seq (s7.seq (s8.seq s9))))))) + have hd9 : d9 = evalData w₀ M d := by + ext i + · fin_cases i <;> rfl + · rfl + rw [hd9] at hseq + exact hseq + +/-- Bounded-time execution corollary for `evalCode w₀ M` (`9` instructions). -/ +theorem evalCode_execWithin {w₀ M w : ℕ} (hw₀ : 0 < w₀) (hw : 2 * w₀ ≤ w) + {d : Data 5} (hb : d.regs regB < 2 ^ (w₀ - 1)) (hx : d.regs regX < 2 ^ w₀) : + ExecWithin w (evalCode w₀ M) d (evalData w₀ M d) 9 := + (evalCode_exec hw₀ hw hb hx).within + +/-- **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₀`. -/ +theorem isUniversalHash_evalData {w₀ M : ℕ} (hw₀ : 0 < w₀) (hM : M ≤ w₀) (d : Data 5) : + IsUniversalHash + (((initComp w₀ d).eval).map (fun z => extractSeed w₀ z.1)) + (fun b (x : Fin (2 ^ w₀)) => + (evalData w₀ M ((d.set regB b.val).set regX x.val)).regs regOut) + (2 / 2 ^ M) := by + rw [map_extractSeed_eval_initComp] + have hfun : (fun (b : Fin (2 ^ (w₀ - 1))) (x : Fin (2 ^ w₀)) => + (evalData w₀ M ((d.set regB b.val).set regX x.val)).regs regOut) = + multiplyShift w₀ M := by + funext b x + exact evalData_regs_out_eq_multiplyShift w₀ M + ((d.set regB b.val).set regX x.val) b x (by simp [regB, regX]) (by simp [regX]) + rw [hfun] + exact isUniversalHash_multiplyShift hw₀ hM + +end Cslib.Algorithms.WordRAM.Hashing.MultiplyShift diff --git a/Complexity/Foundations/Data/BitString/Prefix.lean b/Complexity/Foundations/Data/BitString/Prefix.lean new file mode 100644 index 000000000..aa5034100 --- /dev/null +++ b/Complexity/Foundations/Data/BitString/Prefix.lean @@ -0,0 +1,115 @@ +/- +Copyright (c) 2026 Renfei Zhou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Renfei Zhou +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Foundations.Data.BitString.Basic + +/-! +# Bit-prefix projection of bit strings as an additive homomorphism + +When `M ≤ q`, taking the first `M` bits of a `q`-bit word `v : BitString q` agrees with +`Cslib.BitString.zeroExtend (d' := M) v`, forms a surjective additive group homomorphism +`Cslib.BitString.restrictBitsAddHom hM : BitString q →+ BitString M`, and reduces the unsigned +integer value `Cslib.BitString.equivFin q v` modulo `2 ^ M` +(`Cslib.BitString.val_equivFin_restrictBitsAddHom`). + +Placing these declarations in a dedicated topic module avoids expanding the public interface of the +widely imported `Complexity/Foundations/Data/BitString/Basic.lean`. + +## Main definitions + +* `Cslib.BitString.restrictBitsAddHom`: projecting `BitString q` to its first `M ≤ q` bits as an + additive group homomorphism `BitString q →+ BitString M`. + +## Main results + +* `Cslib.BitString.restrictBitsAddHom_eq_zeroExtend`: `restrictBitsAddHom hM v` agrees with + `zeroExtend (d' := M) v`. +* `Cslib.BitString.restrictBitsAddHom_zeroExtend`, `Cslib.BitString.restrictBitsAddHom_surjective`: + `zeroExtend` is a right inverse to `restrictBitsAddHom hM`, which is therefore surjective. +* `Cslib.BitString.val_equivFin_restrictBitsAddHom`: the unsigned value of `restrictBitsAddHom hM v` + is `(equivFin q v).val % 2 ^ M`. +-/ + +public section + +namespace Cslib.BitString + +/-- Projecting a `q`-bit string to its first `M ≤ q` bits as an additive group homomorphism. -/ +@[expose] def restrictBitsAddHom {q M : ℕ} (hM : M ≤ q) : BitString q →+ BitString M where + toFun v j := v (Fin.castLE hM j) + map_zero' := rfl + map_add' _ _ := rfl + +/-- When `M ≤ q`, `restrictBitsAddHom hM v` agrees pointwise with `zeroExtend (d' := M) v`. -/ +theorem restrictBitsAddHom_eq_zeroExtend {q M : ℕ} (hM : M ≤ q) (v : BitString q) : + restrictBitsAddHom hM v = zeroExtend (d' := M) v := by + funext j + have hj : j.val < q := lt_of_lt_of_le j.isLt hM + simp [restrictBitsAddHom, zeroExtend, hj, Fin.castLE] + +/-- Zero-extending an `M`-bit string to `q ≥ M` bits is a right inverse to +`restrictBitsAddHom hM`. -/ +@[simp] +theorem restrictBitsAddHom_zeroExtend {q M : ℕ} (hM : M ≤ q) (w : BitString M) : + restrictBitsAddHom hM (zeroExtend w) = w := by + ext j + simp [restrictBitsAddHom, zeroExtend, j.isLt] + +/-- `restrictBitsAddHom hM` is surjective whenever `M ≤ q`. -/ +theorem restrictBitsAddHom_surjective {q M : ℕ} (hM : M ≤ q) : + Function.Surjective (restrictBitsAddHom hM) := + fun w => ⟨zeroExtend w, restrictBitsAddHom_zeroExtend hM w⟩ + +/-- Helper: `(b + 2 * x) % 2 ^ (M + 1) = b + 2 * (x % 2 ^ M)` for `b < 2`. -/ +private theorem add_two_mul_mod_two_pow_succ {b : ℕ} (hb : b < 2) (x M : ℕ) : + (b + 2 * x) % 2 ^ (M + 1) = b + 2 * (x % 2 ^ M) := by + have hdiv : (b + 2 * x) / 2 ^ (M + 1) = x / 2 ^ M := by + rw [pow_succ', ← Nat.div_div_eq_div_mul] + have h1 : (b + 2 * x) / 2 = x := by omega + rw [h1] + have hmul : 2 ^ (M + 1) * (x / 2 ^ M) = 2 * (2 ^ M * (x / 2 ^ M)) := by + rw [pow_succ', mul_assoc] + have hmod1 := Nat.div_add_mod (b + 2 * x) (2 ^ (M + 1)) + have hmod2 := Nat.div_add_mod x (2 ^ M) + rw [hdiv, hmul] at hmod1 + omega + +/-- Taking the first `M ≤ q` bits of `v : BitString q` corresponds to taking its unsigned integer +value modulo `2 ^ M`. -/ +theorem val_equivFin_restrictBitsAddHom {q M : ℕ} (hM : M ≤ q) (v : BitString q) : + (equivFin M (restrictBitsAddHom hM v)).val = (equivFin q v).val % 2 ^ M := by + induction M generalizing q with + | zero => + have hlt := (equivFin 0 (restrictBitsAddHom hM v)).isLt + omega + | succ M ih => + cases q with + | zero => omega + | succ q => + have hM' : M ≤ q := Nat.le_of_succ_le_succ hM + have hcons : restrictBitsAddHom hM v = + Fin.cons (v 0) (restrictBitsAddHom hM' (Fin.tail v)) := by + ext j + refine Fin.cases ?_ ?_ j + · rfl + · intro i + rfl + conv_rhs => rw [← Fin.cons_self_tail v] + rw [hcons, val_equivFin_cons, val_equivFin_cons, ih hM' (Fin.tail v)] + have hb : (v 0).toNat < 2 := by cases v 0 <;> decide + exact (add_two_mul_mod_two_pow_succ hb _ M).symm + +/-- Taking the `M`-bit prefix of `v : BitString q` via `zeroExtend` when `M ≤ q` reduces its +unsigned integer value modulo `2 ^ M`. -/ +theorem val_equivFin_zeroExtend_of_le {q M : ℕ} (hM : M ≤ q) (v : BitString q) : + (equivFin M (zeroExtend v)).val = (equivFin q v).val % 2 ^ M := by + rw [← restrictBitsAddHom_eq_zeroExtend hM v, val_equivFin_restrictBitsAddHom hM v] + +end Cslib.BitString diff --git a/Complexity/Foundations/FieldTheory/Finite/Trinomial.lean b/Complexity/Foundations/FieldTheory/Finite/Trinomial.lean new file mode 100644 index 000000000..1a44604df --- /dev/null +++ b/Complexity/Foundations/FieldTheory/Finite/Trinomial.lean @@ -0,0 +1,583 @@ +/- +Copyright (c) 2026 Renfei Zhou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Renfei Zhou +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Foundations.FieldTheory.Finite.BinaryField +public import Complexity.Foundations.Data.BitString.Basic +public import Complexity.Foundations.Data.BitString.Binary +public import Mathlib.RingTheory.Polynomial.Cyclotomic.Basic +import Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization +import Mathlib.RingTheory.ZMod.UnitsCyclic + +/-! +# Explicit binary fields defined by irreducible trinomials + +For every `t : ℕ`, the cyclotomic polynomial `Φ_{3 ^ (t + 1)}(X)` over `𝔽₂ = ZMod 2` is the +explicit trinomial +`Cslib.trinomial t = X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1`. +Because `2` is a primitive root modulo `3 ^ (t + 1)` for every `t` (`orderOf 2 = 2 * 3 ^ t`), +`Cslib.trinomial t` is irreducible over `ZMod 2` (`Cslib.irreducible_trinomial`) [Lidl and +Niederreiter, Theorem 2.47][LidlNiederreiter1997]. + +Unlike `Cslib.BinaryField w`, whose modulus `Cslib.leastIrreducible w` is defined by an exhaustive +search over binary codes, `Cslib.TrinomialField t = AdjoinRoot (trinomial t)` has a closed-form +sparse modulus of degree `2 * 3 ^ t` for every `t : ℕ` without any runtime polynomial search. +Moreover, because `(X ^ (3 ^ t) + 1) * trinomial t = X ^ (3 ^ (t + 1)) + 1` over `ZMod 2`, any +binary polynomial of degree less than `4 * 3 ^ t` (whose binary code below `2 ^ (4 * 3 ^ t)` splits +into four `3 ^ t`-bit limbs, with the low two limbs kept together as a `2 * 3 ^ t`-bit word) +reduces modulo `trinomial t` in closed form using only bitwise shifts, masks, and exclusive-or +(`Cslib.reduceTrinomialCode`, `Cslib.mk_polyOfCode_reduceTrinomialCode`). Paired with carryless +multiplication `Cslib.clmul` (`Cslib.polyOfCode_clmul`), this gives loop-free arithmetic for +`Cslib.TrinomialField t` on unsigned machine words. + +## Main definitions + +* `Cslib.trinomial`: the binary trinomial `X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1`. +* `Cslib.clmul`: carryless multiplication of natural-number polynomial codes over `𝔽₂`. +* `Cslib.reduceTrinomialCode`: 4-limb bitwise reduction modulo `trinomial t` on natural-number + codes below `2 ^ (4 * 3 ^ t)` (four `3 ^ t`-bit limbs). +* `Cslib.TrinomialField`: the explicit binary field `AdjoinRoot (trinomial t)` of degree + `2 * 3 ^ t`. +* `Cslib.TrinomialField.basis`, `Cslib.TrinomialField.equivBits`, + `Cslib.TrinomialField.equivFin`, `Cslib.TrinomialField.embed`, + `Cslib.TrinomialField.embedFin`: power basis, coordinate equivalences with `BitString (2 * 3 ^ t)` + and `Fin (2 ^ (2 * 3 ^ t))`, and embeddings of bit strings and bounded natural indices. + +## Main results + +* `Cslib.trinomial_eq_cyclotomic`, `Cslib.monic_trinomial`, `Cslib.natDegree_trinomial`, + `Cslib.irreducible_trinomial`: `trinomial t` is the `3 ^ (t + 1)`-th cyclotomic polynomial over + `ZMod 2`, monic of degree `2 * 3 ^ t`, and irreducible. +* `Cslib.coeff_polyOfCode`, `Cslib.polyOfCode_injective`, `Cslib.polyOfCode_xor`, + `Cslib.polyOfCode_shiftLeft`, `Cslib.polyOfCode_eq_and_add_shiftRight`: bit-level correspondence + between `polyOfCode` and bitwise operations on `ℕ`. +* `Cslib.polyOfCode_clmul`, `Cslib.clmul_lt_two_pow`: `clmul` computes polynomial multiplication + over `ZMod 2` and respects bit-width bounds. +* `Cslib.reduceTrinomialCode_lt`, `Cslib.mk_polyOfCode_reduceTrinomialCode`: `reduceTrinomialCode` + produces a `< 2 ^ (2 * 3 ^ t)` code congruent modulo `trinomial t`. +* `Cslib.TrinomialField.card`, `Cslib.TrinomialField.val_equivFin_add`, + `Cslib.TrinomialField.val_equivFin_mul`: cardinality and unsigned-word arithmetic laws of + `TrinomialField t`. + +## References + +* [R. Lidl, H. Niederreiter, *Finite Fields*, Section 2.4 and Chapter 3][LidlNiederreiter1997] +-/ + +public section + +namespace Cslib + +open BitString Module Polynomial + +/-! ## Irreducibility of `X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1` over `ZMod 2` -/ + +/-- The binary trinomial `X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1` of degree `2 * 3 ^ t` over `ZMod 2`. -/ +@[expose] noncomputable def trinomial (t : ℕ) : (ZMod 2)[X] := + X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1 + +/-- `trinomial t` is the `3 ^ (t + 1)`-th cyclotomic polynomial over `ZMod 2`. -/ +theorem trinomial_eq_cyclotomic (t : ℕ) : + trinomial t = cyclotomic (3 ^ (t + 1)) (ZMod 2) := by + rw [cyclotomic_prime_pow_eq_geom_sum (R := ZMod 2) Nat.prime_three, + Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_one] + simp only [trinomial, pow_zero, pow_one, ← pow_mul, mul_comm (3 ^ t) 2] + ring + +/-- `trinomial t` is monic for every `t : ℕ`. -/ +theorem monic_trinomial (t : ℕ) : (trinomial t).Monic := by + rw [trinomial_eq_cyclotomic] + exact cyclotomic.monic (3 ^ (t + 1)) (ZMod 2) + +/-- `trinomial t` has degree `2 * 3 ^ t`. -/ +theorem natDegree_trinomial (t : ℕ) : (trinomial t).natDegree = 2 * 3 ^ t := by + rw [trinomial_eq_cyclotomic, natDegree_cyclotomic, + Nat.totient_prime_pow Nat.prime_three (Nat.succ_pos t), Nat.succ_sub_one, mul_comm] + +/-- In `(ZMod 2)[X]`, any polynomial added to itself vanishes. -/ +private theorem zmod2_poly_add_self (p : (ZMod 2)[X]) : p + p = 0 := by + ext i + rw [coeff_add, coeff_zero] + exact (by decide : ∀ c : ZMod 2, c + c = 0) (p.coeff i) + +/-- Over `ZMod 2`, multiplying `trinomial t` by `X ^ (3 ^ t) + 1` yields `X ^ (3 ^ (t + 1)) + 1`. -/ +theorem mul_trinomial_eq (t : ℕ) : + (X ^ (3 ^ t) + 1) * trinomial t = X ^ (3 ^ (t + 1)) + 1 := by + have h1 : (X ^ (3 ^ t) + 1) * trinomial t = + (X ^ (3 * 3 ^ t) + 1) + + ((X ^ (2 * 3 ^ t) + X ^ (3 ^ t)) + (X ^ (2 * 3 ^ t) + X ^ (3 ^ t))) := by + unfold trinomial + have hpow2 : X ^ (3 ^ t) * X ^ (3 ^ t) = (X : (ZMod 2)[X]) ^ (2 * 3 ^ t) := by + rw [← pow_add, two_mul] + have hpow3 : X ^ (3 ^ t) * X ^ (2 * 3 ^ t) = (X : (ZMod 2)[X]) ^ (3 * 3 ^ t) := by + rw [← pow_add, show 3 ^ t + 2 * 3 ^ t = 3 * 3 ^ t by ring] + calc (X ^ (3 ^ t) + 1) * (X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1) + = X ^ (3 ^ t) * X ^ (2 * 3 ^ t) + X ^ (3 ^ t) * X ^ (3 ^ t) + X ^ (3 ^ t) + + X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1 := by ring + _ = (X ^ (3 * 3 ^ t) + 1) + + ((X ^ (2 * 3 ^ t) + X ^ (3 ^ t)) + (X ^ (2 * 3 ^ t) + X ^ (3 ^ t))) := by + rw [hpow2, hpow3]; ring + rw [h1, zmod2_poly_add_self, add_zero, pow_succ', mul_comm 3 (3 ^ t)] + +/-- In `ZMod 3`, `2 ^ (3 ^ t) = 2` for every `t : ℕ`. -/ +private theorem zmod3_two_pow_three_pow (t : ℕ) : (2 : ZMod 3) ^ (3 ^ t) = 2 := by + induction t with + | zero => decide + | succ t ih => + rw [pow_succ, pow_mul, ih] + decide + +/-- In `ZMod (3 ^ (t + 1))`, `2 ^ (3 ^ t) ≠ 1`. -/ +private theorem zmod_three_pow_two_pow_ne_one (t : ℕ) : + (2 : ZMod (3 ^ (t + 1))) ^ (3 ^ t) ≠ 1 := by + intro h + have hdvd : 3 ∣ 3 ^ (t + 1) := dvd_pow_self 3 (Nat.succ_ne_zero t) + have hcast := congrArg (ZMod.castHom hdvd (ZMod 3)) h + simp only [map_pow, map_ofNat, map_one] at hcast + rw [zmod3_two_pow_three_pow] at hcast + revert hcast + decide + +/-- The multiplicative order of `2` modulo `3 ^ (t + 1)` is `2 * 3 ^ t`. -/ +theorem orderOf_two_zmod_three_pow (t : ℕ) : + orderOf (2 : ZMod (3 ^ (t + 1))) = 2 * 3 ^ t := by + have h4 : orderOf (4 : ZMod (3 ^ (t + 1))) = 3 ^ t := by + simpa [show (1 + 3 : ZMod (3 ^ (t + 1))) = 4 by ring] using + ZMod.orderOf_one_add_prime Nat.prime_three (by decide) t + have hsq : (4 : ZMod (3 ^ (t + 1))) = (2 : ZMod (3 ^ (t + 1))) ^ 2 := by ring + rw [hsq, orderOf_pow' (2 : ZMod (3 ^ (t + 1))) (by decide)] at h4 + set d := orderOf (2 : ZMod (3 ^ (t + 1))) + have hgd_dvd : d.gcd 2 ∣ 2 := Nat.gcd_dvd_right d 2 + have hgd_le : d.gcd 2 ≤ 2 := Nat.le_of_dvd (by decide) hgd_dvd + have hgd_pos : 0 < d.gcd 2 := Nat.gcd_pos_of_pos_right d (by decide) + have h_mul : d = 3 ^ t * d.gcd 2 := + (Nat.div_eq_iff_eq_mul_left hgd_pos (Nat.gcd_dvd_left d 2)).mp h4 + rcases ( by omega : d.gcd 2 = 1 ∨ d.gcd 2 = 2 ) with h1 | h2 + · rw [h1, mul_one] at h_mul + exfalso + apply zmod_three_pow_two_pow_ne_one t + rw [← h_mul] + exact pow_orderOf_eq_one (2 : ZMod (3 ^ (t + 1))) + · rw [h_mul, h2, mul_comm] + +/-- **`trinomial t` is irreducible over `ZMod 2` for every `t : ℕ`** +[Lidl and Niederreiter, Theorem 2.47][LidlNiederreiter1997]. -/ +theorem irreducible_trinomial (t : ℕ) : Irreducible (trinomial t) := by + have : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩ + have hndvd : ¬ 2 ∣ 3 ^ (t + 1) := by + intro hdvd + have h23 : 2 ∣ 3 := Nat.prime_two.dvd_of_dvd_pow hdvd + omega + refine ZMod.irreducible_of_dvd_cyclotomic_of_natDegree hndvd ?_ ?_ + · exact ⟨1, by rw [← trinomial_eq_cyclotomic, mul_one]⟩ + · rw [natDegree_trinomial] + have hunit : orderOf (ZMod.unitOfCoprime 2 (Nat.prime_two.coprime_iff_not_dvd.mpr hndvd)) = + orderOf (2 : ZMod (3 ^ (t + 1))) := by + rw [← orderOf_injective (Units.coeHom (ZMod (3 ^ (t + 1)))) Units.coeHom_injective] + rfl + rw [hunit, orderOf_two_zmod_three_pow] + +/-! ## Bitwise operations, carryless multiplication, and 4-limb reduction on `polyOfCode` -/ + +/-- Unfolding `polyOfCode m` into its constant term `m : ZMod 2` and `X * polyOfCode (m / 2)`. -/ +theorem polyOfCode_eq_C_add_X_mul (m : ℕ) : + polyOfCode m = C (m : ZMod 2) + X * polyOfCode (m / 2) := by + rcases eq_or_ne m 0 with rfl | hm + · simp [polyOfCode_zero] + · rw [polyOfCode, ite_eq_right hm] + +/-- Helper characterizing `(m : ZMod 2)` from `m % 2`. -/ +private theorem natCast_zmod_two_eq (m : ℕ) : + (m : ZMod 2) = if m % 2 = 1 then 1 else 0 := by + rcases Nat.mod_two_eq_zero_or_one m with h0 | h1 + · have hm : (m : ZMod 2) = 0 := (ZMod.natCast_eq_zero_iff m 2).mpr (Nat.dvd_of_mod_eq_zero h0) + simp [h0, hm] + · have hm : (m : ZMod 2) = 1 := by + rw [← Nat.div_add_mod m 2, h1, Nat.cast_add, Nat.cast_mul, ZMod.natCast_self, + zero_mul, zero_add, Nat.cast_one] + simp [h1, hm] + +/-- Coefficient `i` of `polyOfCode m` is bit `i` of `m` read in `ZMod 2`. -/ +theorem coeff_polyOfCode (m i : ℕ) : + (polyOfCode m).coeff i = bitEquiv.symm (m.testBit i) := by + induction i generalizing m with + | zero => + rw [polyOfCode_eq_C_add_X_mul] + simp only [coeff_add, coeff_C_zero, coeff_X_mul_zero, add_zero, Nat.testBit_zero, + natCast_zmod_two_eq] + rcases Nat.mod_two_eq_zero_or_one m with h | h <;> simp [h] + | succ i ih => + rw [polyOfCode_eq_C_add_X_mul, coeff_add, coeff_C_succ, zero_add, coeff_X_mul, + ih (m / 2), Nat.testBit_succ] + +/-- `polyOfCode` is injective: distinct natural numbers have distinct binary polynomials. -/ +theorem polyOfCode_injective : Function.Injective polyOfCode := by + intro a b hab + apply Nat.eq_of_testBit_eq + intro i + have hi := congrArg (fun p : (ZMod 2)[X] => bitEquiv (p.coeff i)) hab + simpa [coeff_polyOfCode] using hi + +/-- If `m < 2 ^ k`, then `polyOfCode m` has degree strictly less than `k`. -/ +theorem degree_polyOfCode_lt {m k : ℕ} (hm : m < 2 ^ k) : + (polyOfCode m).degree < k := by + rcases eq_or_ne m 0 with rfl | hm0 + · simp only [polyOfCode_zero, degree_zero] + exact WithBot.bot_lt_coe k + · have hne : polyOfCode m ≠ 0 := (polyOfCode_ne_zero_and_natDegree hm0).1 + rw [degree_eq_natDegree hne, natDegree_polyOfCode hm0, Nat.cast_lt] + exact Nat.log_lt_of_lt_pow hm0 hm + +/-- Bitwise exclusive-or on codes corresponds to polynomial addition over `ZMod 2`. -/ +@[simp] +theorem polyOfCode_xor (a b : ℕ) : + polyOfCode (a ^^^ b) = polyOfCode a + polyOfCode b := by + ext i + rw [coeff_add, coeff_polyOfCode, coeff_polyOfCode, coeff_polyOfCode, Nat.testBit_xor] + cases a.testBit i <;> cases b.testBit i <;> decide + +/-- Left-shifting a code by `k` bits multiplies its polynomial by `X ^ k`. -/ +@[simp] +theorem polyOfCode_shiftLeft (a k : ℕ) : + polyOfCode (a <<< k) = X ^ k * polyOfCode a := by + ext i + rw [coeff_polyOfCode, coeff_X_pow_mul', Nat.testBit_shiftLeft] + by_cases hik : k ≤ i + · simp [hik, coeff_polyOfCode] + · simp [hik] + +/-- Splitting a code at bit `k` into its low `k` bits (`a &&& (2 ^ k - 1)`) and high bits +(`a >>> k`). -/ +theorem polyOfCode_eq_and_add_shiftRight (a k : ℕ) : + polyOfCode a = polyOfCode (a &&& (2 ^ k - 1)) + X ^ k * polyOfCode (a >>> k) := by + ext i + rw [coeff_add, coeff_X_pow_mul', coeff_polyOfCode, coeff_polyOfCode, + Nat.testBit_and, Nat.testBit_two_pow_sub_one] + by_cases hik : k ≤ i + · have hlt : ¬ i < k := not_lt.mpr hik + simp [hik, hlt, coeff_polyOfCode, Nat.testBit_shiftRight, Nat.add_sub_of_le hik] + · have hlt : i < k := lt_of_not_ge hik + simp [hik, hlt] + +/-- Carryless multiplication of natural-number polynomial codes over `ZMod 2`. -/ +@[expose] def clmul (a b : ℕ) : ℕ := + if b = 0 then 0 + else (if b % 2 = 1 then a else 0) ^^^ (clmul a (b / 2) <<< 1) +decreasing_by omega + +/-- Carryless multiplication by `0` on the right is `0`. -/ +@[simp] +theorem clmul_zero_right (a : ℕ) : clmul a 0 = 0 := by + rw [clmul, ite_eq_left rfl] + +/-- Step equation for `clmul` in terms of bitwise shift and mask. -/ +theorem clmul_step (a b : ℕ) : + clmul a b = (if b &&& 1 = 1 then a else 0) ^^^ (clmul a (b >>> 1) <<< 1) := by + have hand : b &&& 1 = b % 2 := Nat.and_two_pow_sub_one_eq_mod b 1 + have hshr : b >>> 1 = b / 2 := Nat.shiftRight_eq_div_pow b 1 + rw [hand, hshr] + rcases eq_or_ne b 0 with rfl | hb + · simp + · rw [clmul, ite_eq_right hb] + +/-- **`clmul` computes polynomial multiplication over `ZMod 2`**. -/ +@[simp] +theorem polyOfCode_clmul (a b : ℕ) : + polyOfCode (clmul a b) = polyOfCode a * polyOfCode b := by + induction b using Nat.strong_induction_on with + | _ b ih => + rcases eq_or_ne b 0 with rfl | hb + · simp + · rw [clmul, ite_eq_right hb, polyOfCode_xor, polyOfCode_shiftLeft, pow_one, + ih (b / 2) (Nat.div_lt_self (Nat.pos_of_ne_zero hb) one_lt_two)] + conv_rhs => rw [polyOfCode_eq_C_add_X_mul b] + have hbit : polyOfCode (if b % 2 = 1 then a else 0) = polyOfCode a * C (b : ZMod 2) := by + rw [natCast_zmod_two_eq] + split_ifs <;> simp + rw [hbit] + ring + +/-- Carryless multiplication by `0` on the left is `0`. -/ +@[simp] +theorem clmul_zero_left (b : ℕ) : clmul 0 b = 0 := + polyOfCode_injective (by simp) + +/-- Carryless multiplication is commutative. -/ +theorem clmul_comm (a b : ℕ) : clmul a b = clmul b a := + polyOfCode_injective (by simp [mul_comm]) + +/-- Carryless multiplication distributes over `^^^` on the left. -/ +theorem clmul_xor_left (a b c : ℕ) : clmul (a ^^^ b) c = clmul a c ^^^ clmul b c := + polyOfCode_injective (by simp [add_mul]) + +/-- Carryless multiplication distributes over `^^^` on the right. -/ +theorem clmul_xor_right (a b c : ℕ) : clmul a (b ^^^ c) = clmul a b ^^^ clmul a c := + polyOfCode_injective (by simp [mul_add]) + +/-- Carryless multiplication commutes with left shifts on the left. -/ +theorem clmul_shiftLeft_left (a b k : ℕ) : clmul (a <<< k) b = clmul a b <<< k := + polyOfCode_injective (by simp [mul_assoc]) + +/-- Carryless multiplication commutes with left shifts on the right. -/ +theorem clmul_shiftLeft_right (a b k : ℕ) : clmul a (b <<< k) = clmul a b <<< k := + polyOfCode_injective (by simp [mul_left_comm]) + +/-- If `a < 2 ^ m` and `b < 2 ^ n`, then `clmul a b < 2 ^ (m + n)`. -/ +theorem clmul_lt_two_pow {a b m n : ℕ} (ha : a < 2 ^ m) (hb : b < 2 ^ n) : + clmul a b < 2 ^ (m + n) := by + induction n generalizing b with + | zero => + have hb0 : b = 0 := by omega + subst hb0 + simp only [clmul_zero_right, add_zero] + positivity + | succ n ih => + rcases eq_or_ne b 0 with rfl | hb0 + · simp only [clmul_zero_right] + positivity + · rw [clmul, ite_eq_right hb0] + have hdiv : b / 2 < 2 ^ n := by + rw [pow_succ] at hb + omega + have hrec := ih hdiv + have hsh : clmul a (b / 2) <<< 1 < 2 ^ (m + (n + 1)) := by + rw [Nat.shiftLeft_eq, pow_one, ← add_assoc, pow_succ] + omega + have hlow : (if b % 2 = 1 then a else 0) < 2 ^ (m + (n + 1)) := by + have hle : 2 ^ m ≤ 2 ^ (m + (n + 1)) := + Nat.pow_le_pow_right two_pos (Nat.le_add_right m (n + 1)) + split_ifs <;> omega + exact Nat.xor_lt_two_pow hlow hsh + +/-- If `a < 2 ^ q` and `b < 2 ^ q`, then `clmul a b < 2 ^ (2 * q)`. -/ +theorem clmul_lt_two_pow_two_mul {a b q : ℕ} (ha : a < 2 ^ q) (hb : b < 2 ^ q) : + clmul a b < 2 ^ (2 * q) := by + rw [two_mul] + exact clmul_lt_two_pow ha hb + +/-- **8-operation loop-free 4-limb reduction modulo `trinomial t`**: +viewing a code `c < 2 ^ (4 * 3 ^ t)` as four `3 ^ t`-bit limbs (with the low two limbs kept +together as `cLow`), reduces `c` to a code `< 2 ^ (2 * 3 ^ t)` representing the same element of +`AdjoinRoot (trinomial t)`. -/ +@[expose] def reduceTrinomialCode (t c : ℕ) : ℕ := + let r := 3 ^ t + let c3 := c >>> (3 * r) + let c2 := (c >>> (2 * r)) &&& (2 ^ r - 1) + let cLow := c &&& (2 ^ (2 * r) - 1) + ((cLow ^^^ c3) ^^^ c2) ^^^ (c2 <<< r) + +/-- For `c < 2 ^ (4 * 3 ^ t)`, `reduceTrinomialCode t c < 2 ^ (2 * 3 ^ t)`. -/ +theorem reduceTrinomialCode_lt (t : ℕ) {c : ℕ} (hc : c < 2 ^ (4 * 3 ^ t)) : + reduceTrinomialCode t c < 2 ^ (2 * 3 ^ t) := by + dsimp only [reduceTrinomialCode] + set r := 3 ^ t + have hr_le : 2 ^ r ≤ 2 ^ (2 * r) := Nat.pow_le_pow_right two_pos (by omega) + have hcLow : c &&& (2 ^ (2 * r) - 1) < 2 ^ (2 * r) := by + rw [Nat.and_two_pow_sub_one_eq_mod] + exact Nat.mod_lt c (by positivity) + have hc3 : c >>> (3 * r) < 2 ^ (2 * r) := by + rw [Nat.shiftRight_eq_div_pow] + have hlt : c / 2 ^ (3 * r) < 2 ^ r := by + apply Nat.div_lt_of_lt_mul + rwa [← pow_add, show 3 * r + r = 4 * r by omega] + exact hlt.trans_le hr_le + have hc2_r : (c >>> (2 * r)) &&& (2 ^ r - 1) < 2 ^ r := by + rw [Nat.and_two_pow_sub_one_eq_mod] + exact Nat.mod_lt _ (by positivity) + have hc2 : (c >>> (2 * r)) &&& (2 ^ r - 1) < 2 ^ (2 * r) := hc2_r.trans_le hr_le + have hc2_sh : ((c >>> (2 * r)) &&& (2 ^ r - 1)) <<< r < 2 ^ (2 * r) := by + have hpow : 2 ^ (2 * r) = 2 ^ r * 2 ^ r := by rw [two_mul, pow_add] + rw [Nat.shiftLeft_eq, hpow] + exact Nat.mul_lt_mul_of_pos_right hc2_r (by positivity) + exact Nat.xor_lt_two_pow (Nat.xor_lt_two_pow (Nat.xor_lt_two_pow hcLow hc3) hc2) hc2_sh + +/-- **`reduceTrinomialCode t c` is congruent to `c` modulo `trinomial t` for every `c : ℕ`**. -/ +theorem mk_polyOfCode_reduceTrinomialCode (t c : ℕ) : + AdjoinRoot.mk (trinomial t) (polyOfCode (reduceTrinomialCode t c)) = + AdjoinRoot.mk (trinomial t) (polyOfCode c) := by + set r := 3 ^ t + set c3 := c >>> (3 * r) + set c2 := (c >>> (2 * r)) &&& (2 ^ r - 1) + set cLow := c &&& (2 ^ (2 * r) - 1) + have hsplit1 : polyOfCode c = polyOfCode cLow + X ^ (2 * r) * polyOfCode (c >>> (2 * r)) := + polyOfCode_eq_and_add_shiftRight c (2 * r) + have hsplit2 : polyOfCode (c >>> (2 * r)) = polyOfCode c2 + X ^ r * polyOfCode c3 := by + have h := polyOfCode_eq_and_add_shiftRight (c >>> (2 * r)) r + rwa [← Nat.shiftRight_add, show 2 * r + r = 3 * r by omega] at h + have hred : polyOfCode (reduceTrinomialCode t c) = + polyOfCode cLow + polyOfCode c3 + polyOfCode c2 + X ^ r * polyOfCode c2 := by + change polyOfCode (((cLow ^^^ c3) ^^^ c2) ^^^ (c2 <<< r)) = _ + simp only [polyOfCode_xor, polyOfCode_shiftLeft] + have hdiff : polyOfCode c = + polyOfCode (reduceTrinomialCode t c) + + (polyOfCode c2 + (X ^ r + 1) * polyOfCode c3) * trinomial t := by + rw [hsplit1, hsplit2, hred] + have htri : trinomial t = X ^ (2 * r) + X ^ r + 1 := rfl + have hrr : (X : (ZMod 2)[X]) ^ r * X ^ r = X ^ (2 * r) := by + rw [← pow_add, two_mul] + set P0 := polyOfCode cLow + set P2 := polyOfCode c2 + set P3 := polyOfCode c3 + set Xr : (ZMod 2)[X] := X ^ r + have halg : + P0 + P3 + P2 + Xr * P2 + (P2 + (Xr + 1) * P3) * (Xr * Xr + Xr + 1) = + P0 + (Xr * Xr) * (P2 + Xr * P3) + + ((P2 + Xr * P2 + P3 + Xr * P3 + Xr * Xr * P3) + + (P2 + Xr * P2 + P3 + Xr * P3 + Xr * Xr * P3)) := by + ring + rw [htri, ← hrr, halg, zmod2_poly_add_self, add_zero] + rw [hdiff, map_add, map_mul, AdjoinRoot.mk_self, mul_zero, add_zero] + +/-! ## The explicit trinomial field `TrinomialField t` -/ + +/-- **The explicit binary field of degree `2 * 3 ^ t`**: binary polynomials modulo `trinomial t`. -/ +abbrev TrinomialField (t : ℕ) : Type := AdjoinRoot (trinomial t) + +namespace TrinomialField + +/-- Degree `2 * 3 ^ t` is always positive. -/ +theorem deg_ne_zero (t : ℕ) : 2 * 3 ^ t ≠ 0 := by positivity + +/-- The modulus `trinomial t` is irreducible, so the quotient is a field. -/ +instance (t : ℕ) : Fact (Irreducible (trinomial t)) := + ⟨irreducible_trinomial t⟩ + +/-- `TrinomialField t` is a field. -/ +noncomputable instance (t : ℕ) : Field (TrinomialField t) := AdjoinRoot.instField + +/-- `TrinomialField t` is finite, through its coordinates in the power basis. -/ +noncomputable instance (t : ℕ) : Fintype (TrinomialField t) := + Fintype.ofEquiv _ + (AdjoinRoot.powerBasisAux' (monic_trinomial t)).equivFun.toEquiv.symm + +/-- Equality in `TrinomialField t`, decided classically. -/ +noncomputable instance (t : ℕ) : DecidableEq (TrinomialField t) := Classical.decEq _ + +/-- `TrinomialField t` has characteristic two. -/ +instance (t : ℕ) : CharP (TrinomialField t) 2 := + charP_of_injective_algebraMap (algebraMap (ZMod 2) (TrinomialField t)).injective 2 + +/-- **The power basis** `1, α, …, α ^ (2 * 3 ^ t - 1)` at the root `α` of `trinomial t`. -/ +noncomputable def basis (t : ℕ) : Module.Basis (Fin (2 * 3 ^ t)) (ZMod 2) (TrinomialField t) := + (AdjoinRoot.powerBasisAux' (monic_trinomial t)).reindex + (finCongr (natDegree_trinomial t)) + +/-- Basis vector `i` is the power `α ^ i` of the root. -/ +theorem basis_apply (t : ℕ) (i : Fin (2 * 3 ^ t)) : + basis t i = AdjoinRoot.root (trinomial t) ^ (i : ℕ) := by + rw [basis, Module.Basis.reindex_apply] + exact (AdjoinRoot.powerBasis' (monic_trinomial t)).basis_eq_pow + ((finCongr (natDegree_trinomial t)).symm i) + +/-- **The encoding by bits**: the `2 * 3 ^ t` coordinates in the power basis as an additive +equivalence `TrinomialField t ≃+ BitString (2 * 3 ^ t)`. -/ +noncomputable def equivBits (t : ℕ) : TrinomialField t ≃+ BitString (2 * 3 ^ t) := + (basis t).equivFun.toAddEquiv.trans (AddEquiv.piCongrRight fun _ => bitEquiv.toAddEquiv) + +/-- Bit `j` of an element is its coordinate `j` in the power basis. -/ +theorem equivBits_apply (t : ℕ) (x : TrinomialField t) (j : Fin (2 * 3 ^ t)) : + equivBits t x j = bitEquiv ((basis t).repr x j) := by + rfl + +/-- The element with given bits is the combination of the basis vectors selected by the bits. -/ +theorem equivBits_symm_apply (t : ℕ) (v : BitString (2 * 3 ^ t)) : + (equivBits t).symm v = ∑ j, bitEquiv.symm (v j) • basis t j := by + simp [equivBits, Module.Basis.equivFun_symm_apply] + +/-- **`TrinomialField t` has `2 ^ (2 * 3 ^ t)` elements.** -/ +theorem card (t : ℕ) : Fintype.card (TrinomialField t) = 2 ^ (2 * 3 ^ t) := by + rw [Fintype.card_congr (equivBits t).toEquiv, BitString.card] + +/-- The encoding of the class of a binary polynomial of degree less than `2 * 3 ^ t` is its list +of coefficients. -/ +theorem equivBits_mk (t : ℕ) {p : (ZMod 2)[X]} (hp : p.degree < (2 * 3 ^ t : ℕ)) + (j : Fin (2 * 3 ^ t)) : + equivBits t (AdjoinRoot.mk (trinomial t) p) j = bitEquiv (p.coeff j) := by + have hdeg : p.degree < (trinomial t).degree := by + rw [degree_eq_natDegree (irreducible_trinomial t).ne_zero, natDegree_trinomial] + exact hp + rw [equivBits_apply, basis, Module.Basis.repr_reindex_apply, + AdjoinRoot.powerBasisAux'_repr_apply_to_fun, AdjoinRoot.modByMonicHom_mk, + (modByMonic_eq_self_iff (monic_trinomial t)).2 hdeg] + rfl + +/-- **Numbering of `TrinomialField t` by `Fin (2 ^ (2 * 3 ^ t))`** via its power-basis bits. -/ +@[expose] noncomputable def equivFin (t : ℕ) : TrinomialField t ≃ Fin (2 ^ (2 * 3 ^ t)) := + (equivBits t).toEquiv.trans (BitString.equivFin (2 * 3 ^ t)) + +/-- For `c < 2 ^ (2 * 3 ^ t)`, the `equivFin t` coordinate of +`AdjoinRoot.mk (trinomial t) (polyOfCode c)` is `c`. -/ +theorem val_equivFin_mk_polyOfCode (t : ℕ) {c : ℕ} (hc : c < 2 ^ (2 * 3 ^ t)) : + (equivFin t (AdjoinRoot.mk (trinomial t) (polyOfCode c))).val = c := by + have hbits : equivBits t (AdjoinRoot.mk (trinomial t) (polyOfCode c)) = + (BitString.equivFin (2 * 3 ^ t)).symm ⟨c, hc⟩ := by + ext j + rw [equivBits_mk t (degree_polyOfCode_lt hc) j, coeff_polyOfCode, RingEquiv.apply_symm_apply, + BitString.equivFin_symm_apply] + change (BitString.equivFin (2 * 3 ^ t) + (equivBits t (AdjoinRoot.mk (trinomial t) (polyOfCode c)))).val = c + rw [hbits, Equiv.apply_symm_apply] + +/-- The inverse of `equivFin t` sends `m : Fin (2 ^ (2 * 3 ^ t))` to +`AdjoinRoot.mk (trinomial t) (polyOfCode m.val)`. -/ +theorem equivFin_symm_eq_mk_polyOfCode (t : ℕ) (m : Fin (2 ^ (2 * 3 ^ t))) : + (equivFin t).symm m = AdjoinRoot.mk (trinomial t) (polyOfCode m.val) := by + apply (equivFin t).injective + rw [Equiv.apply_symm_apply] + exact Fin.ext (val_equivFin_mk_polyOfCode t m.isLt).symm + +/-- Every `x : TrinomialField t` is the class of `polyOfCode (equivFin t x).val`. -/ +theorem mk_polyOfCode_val_equivFin (t : ℕ) (x : TrinomialField t) : + AdjoinRoot.mk (trinomial t) (polyOfCode (equivFin t x).val) = x := by + rw [← equivFin_symm_eq_mk_polyOfCode, Equiv.symm_apply_apply] + +/-- Addition in `TrinomialField t` corresponds to bitwise exclusive-or (`^^^`) on `equivFin t` +coordinates. -/ +theorem val_equivFin_add (t : ℕ) (x y : TrinomialField t) : + (equivFin t (x + y)).val = (equivFin t x).val ^^^ (equivFin t y).val := by + have hxy : (equivFin t x).val ^^^ (equivFin t y).val < 2 ^ (2 * 3 ^ t) := + Nat.xor_lt_two_pow (equivFin t x).isLt (equivFin t y).isLt + conv_lhs => rw [← mk_polyOfCode_val_equivFin t x, ← mk_polyOfCode_val_equivFin t y] + rw [← map_add, ← polyOfCode_xor, val_equivFin_mk_polyOfCode t hxy] + +/-- Multiplication in `TrinomialField t` corresponds to carryless multiplication `clmul` followed +by 4-limb reduction `reduceTrinomialCode` on `equivFin t` coordinates. -/ +theorem val_equivFin_mul (t : ℕ) (x y : TrinomialField t) : + (equivFin t (x * y)).val = + reduceTrinomialCode t (clmul (equivFin t x).val (equivFin t y).val) := by + have hcl : clmul (equivFin t x).val (equivFin t y).val < 2 ^ (4 * 3 ^ t) := by + rw [show 4 * 3 ^ t = 2 * (2 * 3 ^ t) by ring] + exact clmul_lt_two_pow_two_mul (equivFin t x).isLt (equivFin t y).isLt + have hred : reduceTrinomialCode t (clmul (equivFin t x).val (equivFin t y).val) < + 2 ^ (2 * 3 ^ t) := + reduceTrinomialCode_lt t hcl + conv_lhs => rw [← mk_polyOfCode_val_equivFin t x, ← mk_polyOfCode_val_equivFin t y] + rw [← map_mul, ← polyOfCode_clmul, ← mk_polyOfCode_reduceTrinomialCode, + val_equivFin_mk_polyOfCode t hred] + +/-- **The embedding of bit strings of length `b ≤ 2 * 3 ^ t`** into `TrinomialField t`. -/ +@[expose] noncomputable def embed {t b : ℕ} (hb : b ≤ 2 * 3 ^ t) : + BitString b ↪ TrinomialField t where + toFun a := (equivBits t).symm (BitString.zeroExtend a) + inj' _ _ h := BitString.zeroExtend_injective hb ((equivBits t).symm.injective h) + +/-- **The embedding of keys `Fin U` (`U ≤ 2 ^ (2 * 3 ^ t)`)** into `TrinomialField t`. -/ +@[expose] noncomputable def embedFin {t U : ℕ} (hU : U ≤ 2 ^ (2 * 3 ^ t)) : + Fin U ↪ TrinomialField t where + toFun u := (equivFin t).symm (Fin.castLE hU u) + inj' := (equivFin t).symm.injective.comp (Fin.castLE_injective hU) + +/-- Applying `embedFin hU` to `u : Fin U` gives `AdjoinRoot.mk (trinomial t) (polyOfCode u.val)`. -/ +theorem embedFin_apply {t U : ℕ} (hU : U ≤ 2 ^ (2 * 3 ^ t)) (u : Fin U) : + embedFin hU u = AdjoinRoot.mk (trinomial t) (polyOfCode u.val) := + equivFin_symm_eq_mk_polyOfCode t (Fin.castLE hU u) + +end TrinomialField + +end Cslib diff --git a/Complexity/Probability/KWiseIndependent.lean b/Complexity/Probability/KWiseIndependent.lean index 3982e40df..3fbbf08b1 100644 --- a/Complexity/Probability/KWiseIndependent.lean +++ b/Complexity/Probability/KWiseIndependent.lean @@ -53,6 +53,12 @@ tuples gives a better constant. * `Cslib.Probability.IsKWiseIndependentHash.isPairwiseIndependentHash`, `Cslib.Probability.isKWiseIndependentHash_two_iff`: for `k ≥ 2` the family is pairwise independent, and `2`-wise independence is pairwise independence with a seed. +* `Cslib.Probability.IsKWiseIndependentHash.comp_seedEquiv`, + `Cslib.Probability.IsKWiseIndependentHash.comp`, + `Cslib.Probability.IsKWiseIndependentHash.map_equiv`, + `Cslib.Probability.IsKWiseIndependentHash.comp_surjective_addMonoidHom`: preservation of + `k`-wise independence under seed equivalences, injective domain maps, output equivalences, and + surjective additive group homomorphisms. * `Cslib.Probability.isKWiseIndependentHash_of_surjective`: an additive family whose restrictions to sets of at most `k` points are onto is `k`-wise independent. * `Cslib.Probability.IsKWiseIndependentHash.expect_sum_pow_le`: the `2 m`-th moment bound. @@ -108,6 +114,59 @@ theorem mono (hh : IsKWiseIndependentHash k h) {k' : ℕ} (hk : k' ≤ k) : IsKWiseIndependentHash k' h where dens_filter_restrict_eq hT y := hh.dens_filter_restrict_eq (hT.trans hk) y +/-- Relabelling the seed space by an equivalence `e : ι' ≃ ι` preserves `k`-wise independence. -/ +theorem comp_seedEquiv {ι' : Type*} [Fintype ι'] (hh : IsKWiseIndependentHash k h) + (e : ι' ≃ ι) : IsKWiseIndependentHash k (fun i' x => h (e i') x) where + dens_filter_restrict_eq {T} hT y := by + rw [dens_eq_card_div_card, ← hh.dens_filter_restrict_eq hT y, dens_eq_card_div_card, + Fintype.card_congr e] + congr 2 + exact card_equiv e fun i' => by simp + +/-- Precomposing the input domain with an injective map `e : X' → X` preserves `k`-wise +independence. -/ +theorem comp {X' : Type*} (hh : IsKWiseIndependentHash k h) {e : X' → X} + (he : Function.Injective e) : IsKWiseIndependentHash k (fun i x' => h i (e x')) where + dens_filter_restrict_eq {T} hT y := by + let emb : X' ↪ X := ⟨e, he⟩ + have hmem (z : T.map emb) : ∃ x' ∈ T, emb x' = z.1 := mem_map.1 z.2 + let eT : T ≃ T.map emb := + { toFun := fun x => ⟨e x.1, mem_map_of_mem emb x.2⟩ + invFun := fun z => ⟨(hmem z).choose, (hmem z).choose_spec.1⟩ + left_inv := fun x => + Subtype.ext (he (hmem ⟨e x.1, mem_map_of_mem emb x.2⟩).choose_spec.2) + right_inv := fun z => Subtype.ext (hmem z).choose_spec.2 } + have hcard : #(T.map emb) = #T := card_map emb + have hmap : #(T.map emb) ≤ k := hcard.le.trans hT + have hdens := hh.dens_filter_restrict_eq hmap (fun z => y (eT.symm z)) + rw [hcard] at hdens + rw [← hdens] + congr 1 + ext i + simp only [mem_filter, mem_univ, true_and] + constructor + · intro hi + funext z + have hz : (T.map emb).restrict (h i) z = T.restrict (fun x' => h i (e x')) (eT.symm z) := by + simp only [restrict] + exact congrArg (h i) (congrArg Subtype.val (eT.apply_symm_apply z)).symm + rw [hz, hi] + · intro hi + funext x + have hx := congrFun hi (eT x) + rw [Equiv.symm_apply_apply] at hx + exact hx + +/-- Postcomposing the output values with an equivalence `e : Y ≃ Z` preserves `k`-wise +independence. -/ +theorem map_equiv {Z : Type*} [Fintype Z] [DecidableEq Z] (hh : IsKWiseIndependentHash k h) + (e : Y ≃ Z) : IsKWiseIndependentHash k (fun i x => e (h i x)) where + dens_filter_restrict_eq {T} hT z := by + rw [← Fintype.card_congr e, ← hh.dens_filter_restrict_eq hT (fun x => e.symm (z x))] + congr 1 + ext i + simp only [mem_filter, mem_univ, true_and, funext_iff, restrict, Equiv.eq_symm_apply] + section Expect variable {𝕜 : Type*} [Semifield 𝕜] [CharZero 𝕜] @@ -145,6 +204,26 @@ theorem expect_prod (hh : IsKWiseIndependentHash k h) {T : Finset X} (hT : #T end Expect +/-- Postcomposing the output values with a surjective additive group homomorphism `π : Y →+ Z` +between finite additive groups preserves `k`-wise independence. -/ +theorem comp_surjective_addMonoidHom {Z : Type*} [AddGroup Y] [AddGroup Z] [Fintype Z] + [DecidableEq Z] (hh : IsKWiseIndependentHash k h) (π : Y →+ Z) + (hπ : Function.Surjective π) : IsKWiseIndependentHash k (fun i x => π (h i x)) where + dens_filter_restrict_eq {T} hT z := by + classical + let πT (y : T → Y) : T → Z := fun x => π (y x) + have hexp := hh.expect_restrict hT (fun y : T → Y => if πT y = z then (1 : ℚ≥0) else 0) + simp only [Fintype.expect_boole, NNRat.cast_id] at hexp + have hfun (i : ι) : (πT (T.restrict (h i)) = z) ↔ (T.restrict (fun x => π (h i x)) = z) := + Iff.rfl + simp only [hfun] at hexp + rw [hexp] + have hshift := dens_filter_eq_of_shift (f := πT) (fun c => by + refine ⟨Equiv.addRight (fun x => (hπ (c x)).choose), fun y => funext fun x => ?_⟩ + simp [πT, Pi.add_apply, map_add, (hπ (c x)).choose_spec]) z + rw [Fintype.card_fun, Fintype.card_coe, Nat.cast_pow] at hshift + exact hshift + /-- A `k`-wise independent family with `k ≥ 2` is pairwise independent. -/ theorem isPairwiseIndependentHash (hh : IsKWiseIndependentHash k h) (hk : 2 ≤ k) : IsPairwiseIndependentHash h where diff --git a/Complexity/Probability/KWiseIndependent/Trinomial.lean b/Complexity/Probability/KWiseIndependent/Trinomial.lean new file mode 100644 index 000000000..0f564bcf6 --- /dev/null +++ b/Complexity/Probability/KWiseIndependent/Trinomial.lean @@ -0,0 +1,218 @@ +/- +Copyright (c) 2026 Renfei Zhou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Renfei Zhou +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Data.BitString.Prefix +public import Complexity.Foundations.FieldTheory.Finite.Trinomial +public import Complexity.Probability.KWiseIndependent.Polynomial + +/-! +# Exact `k`-wise independent hashing over explicit trinomial binary fields + +By evaluating degree-`< k` polynomials over the explicit binary field +`Cslib.TrinomialField t = AdjoinRoot (X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1)` and projecting the result +to its low `M ≤ 2 * 3 ^ t` coordinates in the power basis, we obtain an explicit, zero-bias +`k`-wise independent hash family (`Cslib.Probability.trinomialPolyHash`) from `Fin U` onto +`Fin (2 ^ M)` whenever `U ≤ 2 ^ (2 * 3 ^ t)` and `M ≤ 2 * 3 ^ t` +(`Cslib.Probability.isKWiseIndependentHash_trinomialPolyHash`) +[Vadhan, Section 3.5.5][Vadhan2012]; [Wegman and Carter][WegmanCarter1981]. + +Because the coordinate map +`Cslib.TrinomialField.equivBits t : TrinomialField t ≃+ BitString (2 * 3 ^ t)` +and the bit-prefix projection `BitString (2 * 3 ^ t) →+ BitString M` are surjective additive group +homomorphisms over `𝔽₂`, every output bucket in `Fin (2 ^ M)` has the exact same preimage size in +`TrinomialField t`. Consequently, projecting to the low `M` bits preserves exact `k`-wise +independence without modulo bias. + +We also provide `Cslib.Probability.trinomialStep U M`, which selects a trinomial parameter `t` +satisfying `U ≤ 2 ^ (2 * 3 ^ t)`, `M ≤ 2 * 3 ^ t`, and +`2 * 3 ^ t ≤ 3 * max (Nat.clog 2 (max U 2)) (max M 1)`. + +## Main definitions + +* `Cslib.Probability.trinomialStep`: selects `t : ℕ` so that `2 * 3 ^ t` covers both `log₂ U` and + `M` within a factor of `3`. +* `Cslib.Probability.trinomialDeg`: the field degree `2 * 3 ^ trinomialStep U M`. +* `Cslib.Probability.trinomialPolyEval`: degree-`< k` polynomial evaluation over + `Cslib.TrinomialField t` on natural-number word coordinates. +* `Cslib.Probability.trinomialPolyHash`: the `k`-wise independent trinomial polynomial hash family + from `Fin U` to `Fin (2 ^ M)`. + +## Main results + +* `Cslib.Probability.isKWiseIndependentHash_trinomialPolyHash`: `trinomialPolyHash t k U M` is + `k`-wise independent whenever `U ≤ 2 ^ (2 * 3 ^ t)` and `M ≤ 2 * 3 ^ t`. +* `Cslib.Probability.le_two_pow_trinomialDeg`, `Cslib.Probability.le_trinomialDeg`, + `Cslib.Probability.trinomialDeg_le_three_mul`: degree bounds for `trinomialStep U M`. + +## References + +* [S. P. Vadhan, *Pseudorandomness*, Section 3.5.5][Vadhan2012] +* [M. N. Wegman, J. L. Carter, *New hash functions and their use in authentication and set + equality*][WegmanCarter1981] +-/ + +public section + +namespace Cslib.Probability + +open BitString Finset + +/-! ## Trinomial degree selection -/ + +/-- Smallest exponent `t : ℕ` such that `B ≤ 2 * 3 ^ t`. -/ +@[expose] def trinomialStepAux (B : ℕ) : ℕ := + if B ≤ 2 then 0 + else trinomialStepAux ((B + 2) / 3) + 1 +decreasing_by omega + +/-- `2 * 3 ^ trinomialStepAux B` is at least `B`. -/ +theorem le_two_mul_three_pow_trinomialStepAux (B : ℕ) : + B ≤ 2 * 3 ^ trinomialStepAux B := by + induction B using Nat.strong_induction_on with + | _ B ih => + rw [trinomialStepAux] + split_ifs with hB + · simp [hB] + · have hrec := ih ((B + 2) / 3) (by omega) + rw [pow_succ, ← mul_assoc] + omega + +/-- When `2 < B`, `trinomialStepAux B` is positive and `2 * 3 ^ (trinomialStepAux B - 1) < B`. -/ +private theorem two_mul_three_pow_pred_lt_of_two_lt {B : ℕ} (hB : 2 < B) : + 0 < trinomialStepAux B ∧ 2 * 3 ^ (trinomialStepAux B - 1) < B := by + induction B using Nat.strong_induction_on with + | _ B ih => + have hle : ¬ B ≤ 2 := not_le.mpr hB + rw [trinomialStepAux, ite_eq_right hle] + refine ⟨Nat.succ_pos _, ?_⟩ + rw [Nat.add_sub_cancel] + by_cases hB' : (B + 2) / 3 ≤ 2 + · have h0 : trinomialStepAux ((B + 2) / 3) = 0 := by + rw [trinomialStepAux, ite_eq_left hB'] + rw [h0] + omega + · obtain ⟨ht', hlt'⟩ := ih ((B + 2) / 3) (by omega) (not_le.mp hB') + have hpow : 3 ^ trinomialStepAux ((B + 2) / 3) = + 3 ^ (trinomialStepAux ((B + 2) / 3) - 1) * 3 := by + conv_lhs => rw [← Nat.sub_add_cancel ht', pow_succ] + omega + +/-- `2 * 3 ^ trinomialStepAux B` is at most `3 * max B 1`. -/ +theorem two_mul_three_pow_trinomialStepAux_le (B : ℕ) : + 2 * 3 ^ trinomialStepAux B ≤ 3 * max B 1 := by + by_cases hB : B ≤ 2 + · rw [trinomialStepAux, ite_eq_left hB] + omega + · obtain ⟨ht, hlt⟩ := two_mul_three_pow_pred_lt_of_two_lt (not_le.mp hB) + have hpow : 3 ^ trinomialStepAux B = 3 ^ (trinomialStepAux B - 1) * 3 := by + conv_lhs => rw [← Nat.sub_add_cancel ht, pow_succ] + omega + +/-- Target bit-width needed to embed `Fin U` and project to `M` bits. -/ +@[expose] def trinomialTargetBits (U M : ℕ) : ℕ := + max (Nat.clog 2 (max U 2)) (max M 1) + +/-- Selected trinomial parameter `t` for universe size `U` and output bit-length `M`. -/ +@[expose] def trinomialStep (U M : ℕ) : ℕ := + trinomialStepAux (trinomialTargetBits U M) + +/-- Selected trinomial field degree `2 * 3 ^ trinomialStep U M`. -/ +@[expose] def trinomialDeg (U M : ℕ) : ℕ := + 2 * 3 ^ trinomialStep U M + +/-- The selected trinomial degree is at least `trinomialTargetBits U M`. -/ +theorem trinomialTargetBits_le_trinomialDeg (U M : ℕ) : + trinomialTargetBits U M ≤ trinomialDeg U M := + le_two_mul_three_pow_trinomialStepAux (trinomialTargetBits U M) + +/-- The universe size `U` fits inside `2 ^ trinomialDeg U M`. -/ +theorem le_two_pow_trinomialDeg (U M : ℕ) : + U ≤ 2 ^ trinomialDeg U M := by + have hclog : Nat.clog 2 (max U 2) ≤ trinomialDeg U M := + (le_max_left _ _).trans (trinomialTargetBits_le_trinomialDeg U M) + calc U ≤ max U 2 := le_max_left U 2 + _ ≤ 2 ^ Nat.clog 2 (max U 2) := Nat.le_pow_clog one_lt_two (max U 2) + _ ≤ 2 ^ trinomialDeg U M := Nat.pow_le_pow_right two_pos hclog + +/-- The output bit-length `M` is at most `trinomialDeg U M`. -/ +theorem le_trinomialDeg (U M : ℕ) : + M ≤ trinomialDeg U M := + ((le_max_left M 1).trans (le_max_right _ _)).trans (trinomialTargetBits_le_trinomialDeg U M) + +/-- The selected trinomial degree is within a factor of `3` of `trinomialTargetBits U M`. -/ +theorem trinomialDeg_le_three_mul (U M : ℕ) : + trinomialDeg U M ≤ 3 * max (Nat.clog 2 (max U 2)) (max M 1) := by + have h1 : 1 ≤ trinomialTargetBits U M := + (le_max_right M 1).trans (le_max_right _ _) + have hle := two_mul_three_pow_trinomialStepAux_le (trinomialTargetBits U M) + rwa [max_eq_left h1] at hle + +/-! ## Trinomial polynomial hashing -/ + +/-- Evaluate the degree-`< k` polynomial with seed coefficients `c : Fin k → Fin (2 ^ (2 * 3 ^ t))` +over `TrinomialField t` at the key `u : Fin U`, returning the `2 * 3 ^ t`-bit result as an element +of `Fin (2 ^ (2 * 3 ^ t))`. -/ +@[expose] noncomputable def trinomialPolyEval (t k U : ℕ) + (c : Fin k → Fin (2 ^ (2 * 3 ^ t))) (u : Fin U) : Fin (2 ^ (2 * 3 ^ t)) := + TrinomialField.equivFin t + (polynomialHash (fun j => (TrinomialField.equivFin t).symm (c j)) + (AdjoinRoot.mk (trinomial t) (polyOfCode u.val))) + +/-- **The `k`-wise independent trinomial polynomial hash family** from `Fin U` to `Fin (2 ^ M)`: +evaluates a degree-`< k` polynomial over `TrinomialField t` and projects to the low `M` bits. -/ +@[expose] noncomputable def trinomialPolyHash (t k U M : ℕ) + (c : Fin k → Fin (2 ^ (2 * 3 ^ t))) (u : Fin U) : Fin (2 ^ M) := + ⟨(trinomialPolyEval t k U c u).val % 2 ^ M, Nat.mod_lt _ (by positivity)⟩ + +/-- The numeric output of `trinomialPolyHash` is the bitwise mask `&&& (2 ^ M - 1)` of +`trinomialPolyEval`. -/ +theorem val_trinomialPolyHash (t k U M : ℕ) + (c : Fin k → Fin (2 ^ (2 * 3 ^ t))) (u : Fin U) : + (trinomialPolyHash t k U M c u).val = + (trinomialPolyEval t k U c u).val &&& (2 ^ M - 1) := by + simp [trinomialPolyHash, Nat.and_two_pow_sub_one_eq_mod] + +/-- When `M ≤ 2 * 3 ^ t`, `trinomialPolyHash` agrees with projecting the power-basis bits of the +field polynomial evaluation to the first `M` bits. -/ +theorem trinomialPolyHash_eq_equivFin_restrictBits {t k U M : ℕ} (hM : M ≤ 2 * 3 ^ t) + (c : Fin k → Fin (2 ^ (2 * 3 ^ t))) (u : Fin U) : + trinomialPolyHash t k U M c u = + BitString.equivFin M (restrictBitsAddHom hM (TrinomialField.equivBits t + (polynomialHash (fun j => (TrinomialField.equivFin t).symm (c j)) + (AdjoinRoot.mk (trinomial t) (polyOfCode u.val))))) := by + apply Fin.ext + rw [val_equivFin_restrictBitsAddHom hM] + rfl + +/-- **`trinomialPolyHash t k U M` is an exact `k`-wise independent hash family** onto `Fin (2 ^ M)` +whenever `U ≤ 2 ^ (2 * 3 ^ t)` and `M ≤ 2 * 3 ^ t`. -/ +theorem isKWiseIndependentHash_trinomialPolyHash {t k U M : ℕ} + (hU : U ≤ 2 ^ (2 * 3 ^ t)) (hM : M ≤ 2 * 3 ^ t) : + IsKWiseIndependentHash k (trinomialPolyHash t k U M) := by + have hpoly : IsKWiseIndependentHash k + (polynomialHash : (Fin k → TrinomialField t) → TrinomialField t → TrinomialField t) := + isKWiseIndependentHash_polynomialHash k + have hseed := hpoly.comp_seedEquiv + (Equiv.piCongrRight fun _ : Fin k => (TrinomialField.equivFin t).symm) + have hkey := hseed.comp (TrinomialField.embedFin hU).injective + let proj : TrinomialField t →+ BitString M := + (restrictBitsAddHom hM).comp (TrinomialField.equivBits t).toAddMonoidHom + have hproj_surj : Function.Surjective proj := + (restrictBitsAddHom_surjective hM).comp (TrinomialField.equivBits t).surjective + have hbits := (hkey.comp_surjective_addMonoidHom proj hproj_surj).map_equiv (BitString.equivFin M) + have heq : trinomialPolyHash t k U M = fun c u => + BitString.equivFin M (proj + (polynomialHash (fun j => (TrinomialField.equivFin t).symm (c j)) + (TrinomialField.embedFin hU u))) := by + funext c u + rw [trinomialPolyHash_eq_equivFin_restrictBits hM, TrinomialField.embedFin_apply hU] + rfl + rwa [heq] + +end Cslib.Probability diff --git a/ComplexityTests/TrinomialKWiseHash.lean b/ComplexityTests/TrinomialKWiseHash.lean new file mode 100644 index 000000000..2ccc8c7ab --- /dev/null +++ b/ComplexityTests/TrinomialKWiseHash.lean @@ -0,0 +1,181 @@ +/- +Copyright (c) 2026 Renfei Zhou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Renfei Zhou +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Foundations.FieldTheory.Finite.Trinomial +public import Complexity.Probability.KWiseIndependent.Trinomial +public import Complexity.Algorithms.Lean.Dictionary +public import Complexity.Algorithms.WordRAM.Hashing.MultiplyShift + +/-! +# Unit tests for trinomial binary fields, `k`-wise independent trinomial hashing, `Dictionary.spec`, +and Word-RAM `MultiplyShift` + +Verifies non-vacuity and concrete behavior of: +1. `Cslib.trinomial`, `Cslib.irreducible_trinomial`, `Cslib.clmul`, `Cslib.reduceTrinomialCode`, + and `Cslib.TrinomialField`; +2. `Cslib.Probability.trinomialPolyHash` and + `Cslib.Probability.isKWiseIndependentHash_trinomialPolyHash` at `k = 5`, together with + `Cslib.Probability.trinomialStep` degree bounds; +3. `Cslib.Algorithms.Lean.Dictionary.spec` including in-place overwrites at full capacity `n_max`; +4. `Cslib.Algorithms.WordRAM.Hashing.MultiplyShift.initCode`, `evalCode`, and + `isUniversalHash_evalData`. +-/ + +public section + +namespace ComplexityTests.TrinomialKWiseHash + +open Cslib Cslib.Probability Cslib.WordRAM +open Cslib.Algorithms.Lean +open Cslib.Algorithms.WordRAM.Hashing +open scoped ENNReal + +/-! ## 1. Explicit trinomial binary fields and 4-limb reduction -/ + +/-- `trinomial 0 = X ^ 2 + X + 1` and `trinomial 1 = X ^ 6 + X ^ 3 + 1` are irreducible over +`ZMod 2`. -/ +theorem trinomial_zero_and_one_irreducible : + Irreducible (trinomial 0) ∧ Irreducible (trinomial 1) ∧ + Fintype.card (TrinomialField 0) = 4 ∧ Fintype.card (TrinomialField 1) = 64 := + ⟨irreducible_trinomial 0, irreducible_trinomial 1, + TrinomialField.card 0, TrinomialField.card 1⟩ + +/-- Concrete check of `clmul` and `reduceTrinomialCode` at `t = 0` (`X ^ 2 + X + 1`, code `7`): +multiplying `X + 1` (code `3`) by `X + 1` (code `3`) gives `X ^ 2 + 1` (code `5`), which reduces +modulo `X ^ 2 + X + 1` to `X` (code `2`). -/ +theorem clmul_and_reduce_t0 : + clmul 3 3 = 5 ∧ + reduceTrinomialCode 0 (clmul 3 3) = 2 ∧ + AdjoinRoot.mk (trinomial 0) (polyOfCode 2) = + AdjoinRoot.mk (trinomial 0) (polyOfCode 3 * polyOfCode 3) := by + have hcl : clmul 3 3 = 5 := by + rw [clmul, clmul, clmul] + decide + have hred : reduceTrinomialCode 0 (clmul 3 3) = 2 := by + rw [hcl] + decide + refine ⟨hcl, hred, ?_⟩ + have h2 : polyOfCode 2 = polyOfCode (reduceTrinomialCode 0 (clmul 3 3)) := + congrArg polyOfCode hred.symm + rw [h2, mk_polyOfCode_reduceTrinomialCode, polyOfCode_clmul] + +/-- Concrete check of 4-limb reduction at `t = 1` (`r = 3`, degree `6`, modulus +`X ^ 6 + X ^ 3 + 1`): for `c = 2 ^ 11 + 2 ^ 7 + 5 = 2181 < 2 ^ 12`, `reduceTrinomialCode 1 c = 19` +(`X ^ 4 + X + 1`) and represents the same element of `TrinomialField 1`. -/ +theorem reduce_t1_sound : + let c := 2 ^ 11 + 2 ^ 7 + 5 + reduceTrinomialCode 1 c = 19 ∧ + reduceTrinomialCode 1 c < 64 ∧ + AdjoinRoot.mk (trinomial 1) (polyOfCode 19) = + AdjoinRoot.mk (trinomial 1) (polyOfCode c) := by + have hred : reduceTrinomialCode 1 (2 ^ 11 + 2 ^ 7 + 5) = 19 := by decide + refine ⟨hred, reduceTrinomialCode_lt 1 (by decide), ?_⟩ + have h19 : polyOfCode 19 = polyOfCode (reduceTrinomialCode 1 (2 ^ 11 + 2 ^ 7 + 5)) := + congrArg polyOfCode hred.symm + rw [h19, mk_polyOfCode_reduceTrinomialCode] + +/-! ## 2. Exact `5`-wise independent trinomial polynomial hashing -/ + +/-- Non-vacuous `5`-wise independent hash family from `Fin 1000` onto `Fin 1024` (`M = 10`) over +`TrinomialField 2` (degree `2 * 3 ^ 2 = 18`, field size `2 ^ 18 = 262144`). -/ +theorem five_wise_independent_trinomialPolyHash : + IsKWiseIndependentHash 5 (trinomialPolyHash 2 5 1000 10) := + isKWiseIndependentHash_trinomialPolyHash (by decide) (by decide) + +/-- Using `trinomialStep U M` automatically selects a valid trinomial field degree for any `(U, M)` +and yields an exact `5`-wise independent family onto `Fin (2 ^ M)`. -/ +theorem five_wise_independent_auto_step (U M : ℕ) : + let t := trinomialStep U M + U ≤ 2 ^ (2 * 3 ^ t) ∧ + M ≤ 2 * 3 ^ t ∧ + 2 * 3 ^ t ≤ 3 * max (Nat.clog 2 (max U 2)) (max M 1) ∧ + IsKWiseIndependentHash 5 (trinomialPolyHash t 5 U M) := + ⟨le_two_pow_trinomialDeg U M, + le_trinomialDeg U M, + trinomialDeg_le_three_mul U M, + isKWiseIndependentHash_trinomialPolyHash (le_two_pow_trinomialDeg U M) (le_trinomialDeg U M)⟩ + +/-- Concrete check of `trinomialStep`: for `U = 1000, M = 10`, `trinomialStep 1000 10 = 2` and +`trinomialDeg 1000 10 = 18`. -/ +theorem trinomialStep_concrete : + trinomialStep 1000 10 = 2 ∧ trinomialDeg 1000 10 = 18 := by + have hclog : Nat.clog 2 (max 1000 2) ≤ 10 := + (Nat.clog_le_iff_le_pow one_lt_two).mpr (by decide) + have ht : trinomialTargetBits 1000 10 = 10 := by + rw [trinomialTargetBits] + omega + have hs : trinomialStep 1000 10 = 2 := by + rw [trinomialStep, ht, trinomialStepAux, trinomialStepAux, trinomialStepAux] + decide + exact ⟨hs, by rw [trinomialDeg, hs]; decide⟩ + +/-! ## 3. Bounded-capacity `Dictionary.spec` -/ + +/-- Concrete operation history on `Dictionary.spec 8 100 2` (universe `8`, values `< 100`, capacity +`n_max = 2`): +inserts two distinct keys `(1, 42)` and `(5, 17)` reaching capacity `2`, then overwrites key `1` +in-place with `99` (which is valid even at full capacity `(dom s).card = 2` because key `1` is +already present!), and queries keys `1`, `5`, and `3`. -/ +def sampleDictOps : List (Dictionary.Op 8) := + [.insert 1 42, .insert 5 17, .insert 1 99, .get 1, .get 5, .get 3] + +theorem sampleDictOps_valid_and_run : + (Dictionary.spec 8 100 2).ValidHistory (Dictionary.empty 8) sampleDictOps ∧ + let finalState := ((Dictionary.spec 8 100 2).run (Dictionary.empty 8) sampleDictOps).1 + (Dictionary.dom finalState).card = 2 ∧ + Dictionary.ValuesBounded 100 finalState ∧ + finalState 1 = some 99 ∧ + finalState 5 = some 17 ∧ + finalState 3 = none := by + have hvh : (Dictionary.spec 8 100 2).ValidHistory (Dictionary.empty 8) sampleDictOps := by + dsimp [sampleDictOps, Stateful.Spec.ValidHistory, Dictionary.spec] + decide + refine ⟨hvh, ?_, + Dictionary.valuesBounded_run_of_validHistory (Dictionary.valuesBounded_empty 8 100) hvh, + by decide, by decide, by decide⟩ + decide + +/-! ## 4. Self-contained Word-RAM `MultiplyShift` -/ + +/-- Non-vacuous execution of `MultiplyShift.initCode` and `MultiplyShift.evalCode` at sub-word width +`w₀ = 8`, output bits `M = 4`, and machine word width `w = 16` (`2 * w₀ ≤ w`): +* `initCode 8` executes in `2` instructions and `1` `rand` call, producing a uniform seed in + `Fin 128`; +* `evalCode 8 4` executes in `9` deterministic instructions, computing `multiplyShift 8 4 b x` in + register `regOut`; +* the resulting hash family is `(2 / 16)`-universal. -/ +theorem multiplyShift_wordram_concrete (d : Data 5) : + ExecRand 16 (MultiplyShift.initCode 8) d (MultiplyShift.initComp 8 d) ∧ + ((MultiplyShift.initComp 8 d).eval).map (fun z => MultiplyShift.extractSeed 8 z.1) = + PMF.uniformOfFintype (Fin 128) ∧ + (∀ b : Fin 128, ∀ x : Fin 256, + let dIn := (d.set MultiplyShift.regB b.val).set MultiplyShift.regX x.val + Exec 16 (MultiplyShift.evalCode 8 4) dIn (MultiplyShift.evalData 8 4 dIn) 9 ∧ + (MultiplyShift.evalData 8 4 dIn).regs MultiplyShift.regOut = multiplyShift 8 4 b x) ∧ + IsUniversalHash + (((MultiplyShift.initComp 8 d).eval).map (fun z => MultiplyShift.extractSeed 8 z.1)) + (fun b (x : Fin 256) => + (MultiplyShift.evalData 8 4 + ((d.set MultiplyShift.regB b.val).set MultiplyShift.regX x.val)).regs + MultiplyShift.regOut) + (2 / 2 ^ 4) := by + refine ⟨MultiplyShift.initCode_execRand (by decide) d, + MultiplyShift.map_extractSeed_eval_initComp 8 d, + fun b x => ⟨MultiplyShift.evalCode_exec (by decide) (by decide) + (by simp [MultiplyShift.regB, MultiplyShift.regX]) + (by simp [MultiplyShift.regX]), + MultiplyShift.evalData_regs_out_eq_multiplyShift 8 4 _ b x + (by simp [MultiplyShift.regB, MultiplyShift.regX]) + (by simp [MultiplyShift.regX])⟩, + MultiplyShift.isUniversalHash_evalData (by decide) (by decide) d⟩ + +end ComplexityTests.TrinomialKWiseHash + +end