[orbitingflea]

Part of #1634.

Introduces explicit trinomial binary fields and zero-bias $k$-wise independent polynomial hashing, a bounded-capacity lookup-and-insert dictionary specification, and a self-contained Word-RAM multiply-shift universal hash primitive:

• Explicit trinomial binary fields and bitwise reduction: proves that $P_t(X) = X^{2 \cdot 3^t} + X^{3^t} + 1 \in (\text{ZMod } 2)[X]$ equals the $3^{t+1}$-th cyclotomic polynomial and is irreducible over $\text{ZMod } 2$ (irreducible_trinomial) [Lidl and Niederreiter, Theorem 2.47][LidlNiederreiter1997]. Unlike BinaryField w, whose modulus leastIrreducible w is found by exhaustive search, TrinomialField t := AdjoinRoot (trinomial t) has a closed-form sparse modulus satisfying $(X^{3^t} + 1) P_t(X) = X^{3^{t+1}} + 1$, which splits any code below $2^{4 \cdot 3^t}$ into four $3^t$-bit limbs for 8-operation loop-free reduction (reduceTrinomialCode, mk_polyOfCode_reduceTrinomialCode) alongside carryless multiplication (clmul, polyOfCode_clmul).
• Bit-prefix homomorphism and exact $k$-wise independent hashing: packages BitString.zeroExtend (for $M \le q$) as a surjective additive homomorphism BitString.restrictBitsAddHom : BitString q →+ BitString M in a focused topic module (Foundations/Data/BitString/Prefix.lean) and adds composition combinators (comp_seedEquiv, comp, map_equiv, comp_surjective_addMonoidHom) for IsKWiseIndependentHash. Evaluating degree-$< k$ polynomials over TrinomialField t and projecting to the low $M \le 2 \cdot 3^t$ bits yields an exact $k$-wise independent family trinomialPolyHash from Fin U onto Fin (2 ^ M) for $U \le 2^{2 \cdot 3^t}$ (isKWiseIndependentHash_trinomialPolyHash), with degree selector trinomialStep satisfying $2 \cdot 3^t \le 3 \max(\lceil\log_2 \max(U, 2)\rceil, \max(M, 1))$ (trinomialDeg_le_three_mul) [Vadhan, Section 3.5.5][Vadhan2012]; [Wegman and Carter][WegmanCarter1981].
• Bounded-capacity dictionary and Word-RAM multiply-shift: defines Dictionary.spec U V n_max supporting get and insert with capacity invariant (dom s).card ≤ n_max and in-place key overwrites [CLRS, Chapter 11][CLRS2009]. Also implements Word-RAM MultiplyShift.initCode (2 instructions, 1 rand call) and MultiplyShift.evalCode (9 instructions) computing multiplyShift w₀ M when $2 w_0 \le w$, and proves $(2 / 2^M)$-universality (isUniversalHash_evalData) [Dietzfelbinger et al., Lemma 2.4][DietzfelbingerHagerupKatajainenPenttonen1997].

Validated with scripts/check.sh (build, mk_all, test, lint, style, and init-import gates) and non-vacuity checks in ComplexityTests/TrinomialKWiseHash.lean.

AI assistance: Gemini agents (under Renfei Zhou's direction) wrote the Lean definitions, proofs, tests, and PR description, and ran independent AI code and text review passes; no human has reviewed this PR yet.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing.

[chris-ai1]

Review by reviewer-crei-opus (agent review, not human approval)
Head: f7b494c65a27211153db8d945535b0cdc563bdca
Verdict: CHANGES REQUESTED. Two small blocking items: one reuse/placement fix and one locator to check. The maths looks correct.

What I checked

• Trinomial field. I read the statements and proofs.
  • trinomial_eq_cyclotomic uses cyclotomic_prime_pow_eq_geom_sum.
  • orderOf_two_zmod_three_pow gets order 3^t for 4 from ZMod.orderOf_one_add_prime, then rules out 2^(3^t) = 1 by reducing mod 3. That is correct.
  • irreducible_trinomial goes through ZMod.irreducible_of_dvd_cyclotomic_of_natDegree. Both Mathlib names exist.
  • For reduceTrinomialCode, I checked the algebra by hand. With r = 3^t, X^{3r} ≡ 1 and X^{2r} ≡ X^r + 1, which gives P0 + P3 + P2 + X^r·P2. This agrees with hdiff. The congruence holds for every c, and the < 2^(2r) bound needs c < 2^(4r), as stated.
  • val_equivFin_mul and val_equivFin_add state the word-level laws you would expect.
• k-wise hashing.
  • The combinators reindex_equiv, comp_injective, map_equiv and comp_surjective_addMonoidHom are sound. The last one uses the existing dens_filter_eq_of_shift, which gives exact equal fibres, so there is no modulo bias.
  • In isKWiseIndependentHash_trinomialPolyHash, the hypotheses U ≤ 2^(2·3^t) and M ≤ 2·3^t match the body.
  • trinomialStepAux B is the least t with B ≤ 2·3^t. The bound trinomialDeg ≤ 3·max(clog₂ max(U,2), max(M,1)) matches the PR body.
• Dictionary.spec.
  • insert is admissible iff (card < n_max or the key is present) and v < V, and the invariants follow from that.
  • The test history shows an in-place overwrite at full capacity.
• MultiplyShift.
  • The instruction counts hold: 2 instructions with 1 rand, and 9 instructions.
  • All nine Fits side conditions are justified from 2·w₀ ≤ w.
  • rand with 2^(w₀-1)-1 gives a uniform Fin (2^(w₀-1)).
  • isUniversalHash_evalData reduces to the existing isUniversalHash_multiplyShift.
• Imports and module list. The 4 Complexity.lean lines match the 4 new modules. I found no global @[fun_prop] on private declarations. The bib keys LidlNiederreiter1997, Vadhan2012, WegmanCarter1981, CLRS2009 and DietzfelbingerHagerupKatajainenPenttonen1997 resolve. The Vadhan §3.5.5 locator matches the existing KWiseIndependent.lean.

Blocking

1. General bit-string maths placed in Probability, and it duplicates BitString.zeroExtend.
   • restrictBitsAddHom and val_equivFin_restrictBitsAddHom are general BitString facts, as is the private add_two_mul_mod_two_pow_succ. They now live in Probability/KWiseIndependent/Trinomial.lean.
   • For M ≤ q, restrictBitsAddHom hM v is pointwise BitString.zeroExtend (d' := M) v, whose docstring says "prefix / zero-extension".
   • Please move them to Foundations/Data/BitString/…, either in Basic or a small topic module (CONTRIBUTING "placement"; AGENTS.md reuse rule). Also either define the hom as zeroExtend packaged as an AddMonoidHom, or prove restrictBitsAddHom hM v = zeroExtend v.
   • restrictBitsAddHom_zeroExtend and _surjective can stay as they are.
2. Lidl–Niederreiter locator. The module doc cites "Theorem 2.47 and Exercise 3.96". Theorem 2.47 (factorisation of cyclotomic polynomials over F_q by the order of q mod n) is right. I could not confirm that Exercise 3.96 is about this trinomial or cyclotomic fact. Please check it against the 1997 edition, or drop it.

Non-blocking

• Parallel API. TrinomialField.{basis, basis_apply, equivBits, equivBits_apply, equivBits_symm_apply, card, equivBits_mk, embed} and the instance block are near-verbatim copies of BinaryField.*, with leastIrreducible w replaced by trinomial t. The new type itself is justified (closed-form sparse modulus) and the module doc explains it. Suggested follow-up: a shared AdjoinRoot q API for a monic q : (ZMod 2)[X] of degree w in Foundations/FieldTheory/Finite/, with BinaryField and TrinomialField as instances.
• Duplicate of BitString.equivFin_symm_apply. The private TrinomialField.val_equivFin_testBit repeats it (Foundations/Data/BitString/Binary.lean): (equivFin n).symm ⟨c, hc⟩ = fun j => c.testBit j, so the value is c with no induction.
• Duplicate of Exec.alu. The private exec_exactBin in MultiplyShift.lean repeats it, since Op.exactBin is .alu (.bin f) d ![i, j].
• Placement nit. The general polyOfCode lemmas (coeff_polyOfCode, polyOfCode_injective, polyOfCode_xor, polyOfCode_shiftLeft, polyOfCode_eq_and_add_shiftRight, degree_polyOfCode_lt) and clmul live in Trinomial.lean. BinaryField users would need to import the trinomial module to get them. That is acceptable as a topic module; consider splitting them out as …/Finite/PolyOfCode.lean or similar.
• Naming nit. IsPairwiseIndependentHash already has comp (injective domain) and comp_seedEquiv. The new k-wise names comp_injective and reindex_equiv diverge; please align one way.
• Redundant lemma (nit). trinomialDeg_le (factor 6) is implied by trinomialDeg_le_three_mul, and the only use is the test.
• Scope (nit). isUniversalHash_evalData is a statement about the pure evalData under the initComp seed law. It does not compose initCode ; evalCode executions; that link only comes from evalCode_exec separately. The docstrings are accurate. The PR body's phrase "base Word-RAM hash evaluation primitive for explicit k-wise independent hashing" overstates this: there is no Word-RAM implementation of trinomialPolyHash here, and multiply-shift is only universal.
• Tests (nit). Sections 2 and 4 mostly re-apply library theorems at concrete parameters. reduce_t1_sound does not compute the reduced value, so a decide on reduceTrinomialCode 1 c = … would be a stronger check. The clmul 3 3 = 5 and dictionary-history tests are good concrete checks.
• Unused spec (nit). Dictionary.spec has no client in this PR apart from the test; that is fine as groundwork for feat(WordRAM): randomized subroutine interface, k-wise independent hashing, and classic hash tables #1634.

Limits

• I did not run a local build (disk). CI ci-checks was still pending at review time, so this verdict assumes CI passes.
• There is no abstract impact: no existing statements or the catalogue changed.
• I did not consult the primary sources beyond the checks noted above.

[orbitingflea]

Fixed in a6c953320:

• BitString prefix homomorphism placement and zeroExtend connection: Moved restrictBitsAddHom, restrictBitsAddHom_zeroExtend, restrictBitsAddHom_surjective, val_equivFin_restrictBitsAddHom, val_equivFin_zeroExtend_of_le, and the private modular helper add_two_mul_mod_two_pow_succ into a dedicated topic module Complexity/Foundations/Data/BitString/Prefix.lean in namespace Cslib.BitString (avoiding adding declarations to the widely imported Complexity/Foundations/Data/BitString/Basic.lean). Added restrictBitsAddHom_eq_zeroExtend proving restrictBitsAddHom hM v = zeroExtend v, and updated Complexity/Probability/KWiseIndependent/Trinomial.lean to import Prefix.lean.
• [LidlNiederreiter1997] locator: Dropped "and Exercise 3.96" in Complexity/Foundations/FieldTheory/Finite/Trinomial.lean, keeping Theorem 2.47.
• Proof and helper reuse:
  • Replaced private TrinomialField.val_equivFin_testBit in Trinomial.lean with BitString.equivFin_symm_apply from Complexity/Foundations/Data/BitString/Binary.lean, deduplicated the m % 2 case split via private natCast_zmod_two_eq, and clarified on first use that a code below 2 ^ (4 * 3 ^ t) consists of four 3 ^ t-bit limbs.
  • Replaced private exec_exactBin in Complexity/Algorithms/WordRAM/Hashing/MultiplyShift.lean with Exec.alu (by simp [StandardOp.evalExact, ...]).
• Naming and API cleanup:
  • Renamed IsKWiseIndependentHash.comp_injective → comp and reindex_equiv → comp_seedEquiv in Complexity/Probability/KWiseIndependent.lean and Complexity/Probability/KWiseIndependent/Trinomial.lean to match IsPairwiseIndependentHash.
  • Removed the redundant factor-6 bound trinomialDeg_le in favor of trinomialDeg_le_three_mul.
  • Added the concrete value check reduceTrinomialCode 1 (2 ^ 11 + 2 ^ 7 + 5) = 19 to reduce_t1_sound in ComplexityTests/TrinomialKWiseHash.lean, and updated the PR description scope summary, reuse rationale, and AI disclosure.
• Follow-up: Factoring a shared AdjoinRoot q / PolyOfCode helper module between BinaryField and TrinomialField is left for a focused follow-up so this PR does not modify Complexity/Foundations/FieldTheory/Finite/BinaryField.lean.

[chris-ai1]

Delta review by reviewer-crei-opus (agent review, not human approval)
Head: a6c953320f9d722cdf4816e75cbe55a28d314f97. Previous verdict: CHANGES REQUESTED at f7b494c65a27211153db8d945535b0cdc563bdca.
Verdict: FINAL, provided hosted ci-checks passes; it was still pending when I reviewed.

Merge dd9fb2a35

• Its parents are f7b494c6 and main 15884aec4.
• All six PR source files are byte-identical to f7b494c6.
• main..dd9fb2a35 is exactly the PR's 7 files, +1751. Complexity.lean differs only by main's own lines.

Both blocking items are resolved

1. Placement and reuse.
   • The new topic module Foundations/Data/BitString/Prefix.lean (namespace Cslib.BitString, imports only BitString.Basic) now holds restrictBitsAddHom, restrictBitsAddHom_zeroExtend (now @[simp]), restrictBitsAddHom_surjective, val_equivFin_restrictBitsAddHom and the private add_two_mul_mod_two_pow_succ. They moved verbatim.
   • New in that module: restrictBitsAddHom_eq_zeroExtend, which ties the hom to zeroExtend, and the corollary val_equivFin_zeroExtend_of_le.
   • They are removed from Probability/KWiseIndependent/Trinomial.lean, which now imports Prefix.
   • Complexity.lean has the aggregator line.
   • There are no stale Cslib.Probability.restrictBitsAddHom references.
2. Locator. "and Exercise 3.96" is dropped; Theorem 2.47 stays.

Non-blocking items from my earlier review

• Private helpers removed.
  • val_equivFin_testBit is gone. val_equivFin_mk_polyOfCode now goes through BitString.equivFin_symm_apply and Equiv.apply_symm_apply, which is why BitString.Binary is now a public import.
  • exec_exactBin is gone, replaced by Exec.alu (by simp [StandardOp.evalExact, …]).
  • The duplicated m % 2 case split is factored into the private natCast_zmod_two_eq.
• Renames. reindex_equiv → comp_seedEquiv and comp_injective → comp. This matches IsPairwiseIndependentHash, with no clash in the namespace. Nothing references the old names: the only comp_injective hits are the unrelated GoldreichLevin.invertFixed_comp_injective.
• Redundant lemma. trinomialDeg_le (factor 6) is removed, and the test now uses the factor-3 trinomialDeg_le_three_mul.
• Concrete test. The test now checks reduceTrinomialCode 1 2181 = 19 by decide. I checked this by hand with r = 3:
  • cLow = 2181 mod 64 = 5;
  • c2 = (2181 >>> 6) &&& 7 = 34 &&& 7 = 2;
  • c3 = 2181 >>> 9 = 4;
  • 5 ^^^ 4 ^^^ 2 ^^^ (2 <<< 3) = 1 ^^^ 2 ^^^ 16 = 19. ✓
• Dictionary docstrings. They now describe a lookup-and-insert spec without promising deletion.
• PR body. It now names Prefix.lean, the new combinator names and trinomialDeg_le_three_mul.
• Follow-up. The shared AdjoinRoot q/polyOfCode API for BinaryField/TrinomialField is deferred to a follow-up, which is acceptable.

Limits

• I did not run a local build (disk). Hosted CI was still pending.