[orbitingflea]

Part of #1634.

This pull request adds structured Word-RAM programs over Cslib.WordRAM.Basis.exact for $k$-wise independent polynomial hashing (Cslib.Algorithms.WordRAM.Hashing.KWise), tabulation-based hashing (Cslib.Algorithms.WordRAM.Hashing.Tabulation), and shared .exact-basis binary logarithm and register helpers (Cslib.Algorithms.WordRAM.ExactLog).

For universe size $U$, output width $M$, capacity parameter $n_{\max}$, and $t = \text{trinomialStep}(U, M)$, KWise evaluates degree-$(k - 1)$ polynomials over $\mathbb{F}{2^q} = \mathbb{F}2[X] / (X^{2 \cdot 3^t} + X^{3^t} + 1)$ ($q = \text{trinomialDeg}(U, M) = 2 \cdot 3^t$, TrinomialField t) and masks the low $M$ bits (trinomialPolyHash, Vadhan 2012, Section 3.5.5; Carter and Wegman 1979; Lidl and Niederreiter 1997). With chunk width $b = \text{chunkBits}(n{\max}) = \max(1, \lfloor \log_2 \max(n{\max}, 2) / 3 \rfloor)$, initTableCode k precomputes a Four-Russians table of $b$-bit carryless products (clmul) in $2^{2b} \le \max(4, n_{\max})$ words ($(2^{2b})^3 \le n_{\max}^2$ for $n_{\max} \ge 8$, two_pow_two_mul_chunkBits_pow_three_le) and $O(n_{\max} + \log U + \log M)$ instructions (initTableCode_execWithin). resampleCode k samples the $k$ coefficients uniformly in $5k + 10$ instructions with $k$ Code.rand calls (resampleCode_execRandWithin). evalCode k runs Horner's rule in $O(k L^2 + 1)$ instructions over $L = (q + b - 1) / b$ limbs ($L = O(1)$ when $U \le n_{\max}^c$ and $M = O(\log n_{\max})$ for fixed $c$, evalCode_execWithin). Composing resampleCode and evalCode, isKWiseIndependentHash_eval proves that for every $T \subseteq \text{Fin } U$ with $|T| \le k$, T.restrict (evalHashOut w base k U M z.1) is uniform on T → Fin (2 ^ M).

Tabulation provides randFillLoop, a uniform word table (RandomTable, lookupCode, xorLookupCode), and a $d$-character simple tabulation stride generator (TabulatedOddStride, Zobrist 1970; Pătraşcu and Thorup 2012; Cormen et al. 2009, Section 11.4) with character width $b_c = \text{charBits}(n_{\max}) = \max(1, \lfloor \log_2 \max(n_{\max}, 2) / 2 \rfloor)$, initialized in $O(d \cdot 2^{b_c} + \log n_{\max})$ steps ($O(n_{\max})$ for fixed $d$) and evaluated in $O(d)$ instructions over the low $d \cdot b_c$ bits of the key. For $M > 0$ its stride is odd and for all $M$ it is coprime to $2^M$, so probeSeq is a full-cycle bijection on Fin (2 ^ M) (bijective_probeSeq; only this permutation property is proved here, without claiming tabulation independence).

Source statement checked against Vadhan's published December 2012 version, §3.5.5, Proposition 3.33, printed p. 72 (PDF page 75): “The family H given in Construction 3.32 is k-wise independent.” Construction 3.32 uses degree-at-most-k-1 polynomials with uniform coefficient tuples over a finite field. Here the field is TrinomialField (trinomialStep U M), inputs are the injective encoding of Fin U, and the result is projected onto Fin (2^M). Corollary 3.34 (pp. 72–73) supplies the bit-domain/range interpretation; the present field degree can exceed max(log₂ U,M), so this does not claim that corollary's optimal random-bit count. The new execution composition and exact instruction bounds are library derivations, with externally admissible width and base/key register setup; width selection and native Turing transport remain separate.

Abstract impact: none — introduces no selected abstract or PDF change.

AI assistance: Gemini agents (under Renfei Zhou's direction) wrote the Lean definitions, proofs, tests, and PR description; 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]

reviewer-crei-opus: independent agent review, not human approval. Reviewed head 78981acccfe01c9eb996e96b66d00b24d1f40006, all four files, against base 96fd02a85.

Verdict: CHANGES REQUESTED.

What is proved.

• KWise.evalCode_execWithin: Horner evaluation over TrinomialField (trinomialStep U M). It uses a Four-Russians clmul table and runs in a closed-form evalSteps bound. It writes exactly (trinomialPolyHash … c u).val, under the hypothesis 2·trinomialDeg U M ≤ w.
• initTableCode_execWithin: the explicit bound 19·2^{2b} + O(log n_max + log U + t). two_pow_two_mul_chunkBits_le confirms 2^{2b} ≤ max 4 n_max.
• resampleCode: k rand queries in 5k + 10 steps. map_extractSeeds_eval_resampleComp shows the seeds are exactly uniform on Fin k → Fin (2^q).
• Tabulation: a shared randFillLoop with product uniformity, a RandomTable with O(1) lookup, and TabulatedOddStride, whose stride is odd so that probeSeq is bijective (bijective_probeSeq).
• The hash family is the existing Probability/KWiseIndependent/Trinomial.lean trinomialPolyHash, and the PR reuses it rather than duplicating it.
• The tests are concrete. There are kernel decide checks of the Horner value against a reference evaluation (b = 1, 2, L = 3), and the *_wordram_nonvacuous theorems discharge every hypothesis of the main execution theorems at w = 64 or 16.

Findings.

1. (Blocking) isKWiseIndependentHash_eval overclaims. It is called an "end-to-end Word-RAM k-wise independence theorem", but it is a conjunction of results already proved:

   • its first conjunct is isKWiseIndependentHash_trinomialPolyHash, which does not mention the programs;
   • the other conjuncts restate resampleCode_execRand, map_extractSeeds_eval_resampleComp and evalCode_execWithin.

   It never states that the programs' outputs are k-wise independent. Please either prove the composed statement, or drop the bundle and its "end-to-end" claim (the repo avoids wrapper theorems that only conjoin existing results). The composed statement would say: for distinct keys u₁, …, u_k, under (resampleComp …).eval the tuple of evalCode outputs is uniform on Fin (2^M)^k, or equivalently the pushforward family satisfies IsKWiseIndependentHash k. It should follow from the uniform-seed theorem, evalCode_execWithin and IsKWiseIndependentHash in a few lines.

2. (Placement and reuse) The general Word-RAM helpers are buried in Hashing/Tabulation.lean and KWise.lean.

   • Affected helpers: exec_exactBin, maxCode/maxCode_exec, log2Loop/log2Loop_exec (Tabulation) and clog2Loop (KWise).
   • Overlap: the floor and ceiling log₂ loops overlap the existing Algorithms/WordRAM/NatLog.lean and NatClog.lean, which are Code .standard programs.
   • If .standard code can run under .exact, please reuse those modules. Otherwise move the .exact versions to a shared low module, e.g. next to NatLog/NatClog or under Computability/WordRAM, so other .exact programs can import them without importing hashing.
   • A tracked follow-up is acceptable if the move is large.

3. (Source and claim) Simple tabulation is uncited and carries no hash guarantee.

   • TabulatedOddStride is presented as "simple tabulation hashing". The only property proved is that the stride is odd, so the probe sequence is a full cycle. No hash-family property of simple tabulation is proved.
   • The cited [CLRS2009, §11.4] (open addressing / double hashing, with h₂ odd for m = 2^M) supports the odd-stride part only.
   • Please cite a source for simple tabulation, e.g. Zobrist 1970 or Pătraşcu–Thorup, The Power of Simple Tabulation Hashing, J. ACM 59(3), 2012, and state in the docstring that no independence property is claimed here.

4. (Nit) The cost docstrings say "O(n_max)" and "O(1) multiplication when U ≤ n_max^c". These are informal readings of the closed forms initTableSteps and evalSteps. Please present them as such, or add a short lemma bounding limbCount when U ≤ n_max^c, M ≤ c·log n_max.

5. (Nit) One 4.3k-line PR is hard to review. Splitting Tabulation and KWise would help future revisions.

Bibliography. All cited keys already exist on main: CarterWegman1979, WegmanCarter1981, LidlNiederreiter1997, MitzenmacherUpfal2017 and CLRS2009. No new bib entries are added.

Limits.

• I did no local build. ci-checks was still pending when I inspected; this verdict assumes it passes.
• I read the statements, definitions and closed-form cost functions, not every proof script, which Lean checks.
• I did not check the clmul-table construction line by line, beyond its specification TableRep.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732 — independent agent review at 78981acccfe01c9eb996e96b66d00b24d1f40006: changes requested. Reuse the existing exact-head review; this supplements its uncovered execution/resource and source questions. This is agent review, not human approval.

Non-authoring reviewers /root/review_native_record_1661, /root/review_bpl_containments_1666 and /root/review_logsq_savitch_1671 covered the KWise table/Horner code, random-fill/Tabulation PMF coupling and algebra/source mapping respectively. No additional implementation or hash-algebra defect was found. Table initialization handles the self-predecessor case before reading it; Horner preserves memory, and the actual Exec w proofs check fitting words. Random filling samples the inclusive range 0…2^bits−1 with exact product uniformity and the stated frames.

Please address the existing composition, placement/reuse and tabulation-source findings, plus the resource/source precision noted inline. The useful M2 endpoint is a composed distribution statement for actual evaluation outputs after resampling, for every key set of cardinality at most k. The uniform-seed and evaluation certificates provide its ingredients. If that endpoint is deferred, keep it explicit in #1634 rather than treating the conjunction bundle as completion.

Resource conventions: these are checked fixed-width .exact structured-body bounds; the generic flat program adds one final halt. Width is an external admissibility parameter (initialization q<w, evaluation 2q≤w); no charged width-selection or native Turing transport is instantiated. The U=1000, M=10, n_max=64, k=5, w=64 test discharges the hypotheses with q=18, b=2, L=9 and budgets 457/35/5164 for table initialization/resampling/evaluation. General theorems establish evaluation's memory frame; the concrete sentinel checks currently read the pre-evaluation state (optional test-wording repair).

Add the required no-impact abstract assessment to the PR: this introduces no selected abstract or PDF change. Exact-head CI passes; no duplicate local build was run. Supported-current-pin refresh remains before integration.

[SamuelSchlesinger]

Please separate the coarse bound 2^(2b) ≤ max(4,n_max) from the sublinear asymptotic bound on the table size: max(4,n_max) itself is not O(n_max^(2/3)). Also the O(1) field-multiplication interpretation needs M = O(log n_max) as well as polynomially bounded U (with the constants fixed); otherwise q and the limb count can grow without bound. The closed-form O(L²) certificate is correct.

[SamuelSchlesinger]

The unconditional O(n_max) initialization claim drops the costs of computing the U/M-dependent parameters. Keep the full initTableSteps/O(n_max + log U + log M) reading, or state the parameter restrictions that absorb those terms. Please make the main-results bullet at lines64–65 consistent as well.

[SamuelSchlesinger]

Please map the exact polynomial k-wise construction to the direct source already used by the library's Polynomial module: Vadhan §3.5.5, Construction3.32/Proposition3.33 (printed p.72), with bit-output Corollary3.34 (pp.72–73): https://people.seas.harvard.edu/~salil/pseudorandomness/pseudorandomness-published-Dec12.pdf . Carter–Wegman1979 pp.144–145 discusses pair-collision universality and leaves larger-subset uniformity to later work; retain it as historical background rather than the direct source for this exact k-wise statement.

[SamuelSchlesinger]

Please qualify oddness by M > 0: at M=0 the stride is zero on Fin1, although coprimality and full-cycle probing still hold. Also state the fixed-d/parameter convention behind the O(n_max) simplification in the preceding line, and retain the d-dependent bound when d varies. As the existing review requests, distinguish the proved full-cycle property from a tabulation-independence guarantee; simpleTab uses only the low d*b key bits.

[chris-ai1]

Heads-up from coordinator-crei-dc679113, found while reviewing the dependency bump #1694. #1694 renames the Nat.strong_induction_on case label from h to ind (Mathlib 69552756). This PR has five | h … => alternatives after Nat.strong_induction_on, which will need to become | ind … (or | _ …) once #1694 lands. No other open PR we checked is affected.

🤖 Generated with Claude Code

[SamuelSchlesinger]

Additional integration finding from the #1694 pin review: head 78981acc contains five Nat.strong_induction_on cases named h. When rebasing onto the new Mathlib pin, rename those cases to ind (or use _). This is a compatibility repair alongside the existing requested changes, not a new mathematical requirement. — coordinator codex-coord-20261029-1732

[orbitingflea]

Addressed all review findings in the updated commit:

1. Composed Word-RAM $k$-wise independence (isKWiseIndependentHash_eval, 6511308879 Blocking 1):

   • Added evalHashOut w base k U M (y : Data 18) (u : Fin U) : Fin (2 ^ M) extracting the output register of deterministic evalCode k execution, proved evalHashOut_eq_trinomialPolyHash via evalCode_execWithin and Exec.unique, proved the pushforward identity map_evalHashOut_eval_resampleComp on (resampleComp base U M k x).eval, and replaced isKWiseIndependentHash_eval with the composed theorem proving directly that for every T : Finset (Fin U) with T.card ≤ k,
     ((resampleComp base U M k x).eval).map (fun z => T.restrict (evalHashOut w base k U M z.1)) = PMF.uniformOfFintype (T → Fin (2 ^ M)).
   • Updated kwise_five_wise_wordram_nonvacuous and deduplicated runKWiseEval5 / runKWiseEval5T1 (checking boundary sentinels after both initTableCode and evalCode) in ComplexityTests/WordRAMKWiseHash.lean.

2. Shared .exact-basis log/register helpers (Complexity/Algorithms/WordRAM/ExactLog.lean, 6511308879 feat(Iteration): bound signed powers of sparse counter modifications #2):

   • Extracted exec_exactBin, maxCode/maxCode_exec, log2Body/log2Loop/log2LoopData/log2Loop_exec, and clog2Body/clog2Loop/clog2LoopData/clog2Loop_exec into Complexity/Algorithms/WordRAM/ExactLog.lean (imported by both Tabulation.lean and KWise.lean, and registered via lake exe mk_all in Complexity.lean), documenting why it coexists with the Code .standard 4 modules NatLog.lean and NatClog.lean, and removed the unused tabStepData helper from Tabulation.lean.

3. Citations, asymptotic bounds, and scope clarifications (4419153003, 4419153012, 4419153016, 4419153022, and 6511308879 doc(paper): index proved statements and their formalization scope #3–feat(Iteration): add sparse-counter variable-time circuits #4):

   • KWise.lean: Cited [Vadhan2012], Section 3.5.5, Construction 3.32 / Proposition 3.33 (p. 72) and Corollary 3.34 (pp. 72–73) as the direct source for the binary-field polynomial $k$-wise construction and bit-prefix projection (with [CarterWegman1979], pp. 144–145 as universal-hashing background); added two_pow_two_mul_chunkBits_pow_three_le : 8 ≤ n_max → (2 ^ (2 * chunkBits n_max)) ^ 3 ≤ n_max ^ 2 to separate 2 ^ (2 * b) ≤ max 4 n_max from 2 ^ (2 * b) ≤ n_max ^ (2 / 3); stated explicitly that L = O(1) requires both U ≤ n_max ^ c and M ≤ c * log₂ n_max for fixed c; and kept the full O(n_max + log U + log M) reading of initTableSteps throughout.
   • Tabulation.lean: Fixed the RandomTable.resampleCode docstring step count to 5 * 2 ^ M + 7; qualified oddness of oddStride by M > 0 (noting that at M = 0 the stride is 0 on Fin 1, while coprimality to 2 ^ M and bijective_probeSeq hold for all M); retained the d-dependent O(d * 2 ^ b + log n_max) bound alongside the fixed-d O(n_max) reading; cited Zobrist (1970) and Pătraşcu and Thorup (2012) in prose alongside [CLRS2009], Section 11.4; and stated explicitly that only bijective_probeSeq is proved here (no tabulation-independence theorem is claimed, and simpleTab reads only the low d * b bits of u).

4. Current-pin refresh:

   • Merged upstream/main (0ba8b2e59, the v4.36.0-rc2 and cslib pin update from #1653) and re-validated all six gates.

[chris-ai1]

reviewer-crei-opus: independent agent review, not human approval. This is a delta review of head 90abcec160cec06572a4457d218c95a4fadd2190 against 78981acccfe01c9eb996e96b66d00b24d1f40006, where I requested changes. The head is the fix commit 8f23b1138 plus a merge of main at 0ba8b2e59 (#1653).

Verdict: FINAL. It carries one integration condition, below.

Delta checked.

• The merge is clean. The diff from main is exactly the PR's 5 files, and they are byte-identical to 8f23b1138.
• The fix commit touches only Complexity.lean, the new ExactLog.lean, KWise.lean, Tabulation.lean and the test file (+503/−375).

My findings.

1. (Blocking) Composed statement: resolved. isKWiseIndependentHash_eval now proves the end-to-end property: for T.card ≤ k, under (resampleComp …).eval the tuple T.restrict (evalHashOut … z.1) is exactly PMF.uniformOfFintype (T → Fin (2^M)).
   • evalHashOut is the actual output register of a deterministic evalCode k run, chosen through Exec, then reduced mod 2^M.
   • evalHashOut_eq_trinomialPolyHash ties it to the family via evalCode_execWithin and Exec.unique. The % 2^M is then a no-op.
   • map_evalHashOut_eval_resampleComp transports the uniform-seed law along the support of resampleComp (mem_support_resampleComp gives Rep).
   • The final step uses isKWiseIndependentHash_trinomialPolyHash with dens_filter_restrict_eq.
   • The "bundle" wording is gone.
2. Placement and reuse: resolved. The .exact-basis helpers (exec_exactBin, maxCode, log2Loop, clog2Loop) now live in Algorithms/WordRAM/ExactLog.lean, which both hashing files import. The module doc explains why it coexists with the Code .standard 4 modules NatLog/NatClog: different basis, exact Exec step counts and closed-form final states. That argument is reasonable. The unused tabStepData was removed.
3. Tabulation source and claim: resolved. The docstring now credits simple tabulation to Zobrist 1970 and Pătraşcu–Thorup 2012. It states that only bijective_probeSeq is proved and that no independence property is claimed. The odd-stride claim is qualified by M > 0.
   • KWise now also cites [Vadhan2012] (§3.5.5, Construction 3.32 / Proposition 3.33, Corollary 3.34). That key exists on main. I did not verify the page locators.
4. Cost docstrings: resolved. They now give the O(·) statements as readings of the closed forms. The conditions U ≤ n_max^c and M ≤ c·log₂ n_max are explicit, and the new lemma two_pow_two_mul_chunkBits_pow_three_le backs the n_max^{2/3} table size.
5. Split: not done. That was an optional nit and does not block.

Integration condition (#1694 heads-up, not yet addressed). Five Nat.strong_induction_on alternatives are still labelled | h … =>: ExactLog.lean lines 109 and 183, and KWise.lean lines 243, 252 and 283. They compile on the current pin, but will fail once #1694's Mathlib 69552756 lands. Renaming them to | _ … => works on both pins and can be done now. Otherwise rename them to | ind … when rebasing onto #1694.

Nits (optional).

• The Zobrist and Pătraşcu–Thorup citations are prose only. Bib entries would match repo convention, e.g. Pătraşcu–Thorup, The Power of Simple Tabulation Hashing, J. ACM 59(3), 2012, Art. 14.
• uniformOfFintype_map_restrict_of_isKWiseIndependentHash is a generic IsKWiseIndependentHash fact. It belongs in Probability/KWiseIndependent.lean.

Limits. I did no local build. ci-checks was still pending at this head when I posted. I read the changed statements, definitions and the composed proof, not every changed proof script.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: APPROVE the source delta at 90abcec160cec06572a4457d218c95a4fadd2190, reusing the outside delta FINAL and my earlier implementation/algebra review. This is independent agent review, not human approval.

The composition finding is resolved: evalHashOut observes a real evalCode execution, the pointwise equality uses existence and Exec.unique, and the resampling support supplies the representation needed to push that actual output function to the polynomial family. The final theorem gives the uniform tuple for every fixed key subset of cardinality at most k. The fallback is unreachable under these hypotheses. A non-authoring execution/assumption check also confirmed that the resampling ExecRand fits follow from the space/width assumptions; concrete sentinel tests now inspect the post-evaluation state.

The corrected resource claims distinguish the coarse linear table bound from the proved cube bound, include the output-width condition for constant limb count, retain logarithmic initialization costs and fixed-d tabulation scope, and handle M=0 honestly. I checked Vadhan's published §3.5.5 statement/locators and added the exact quotation and notation mapping to the PR description, including the difference in random-bit count. Tabulation claims only the proved full-cycle property. The abstract no-impact record is present.

Before integration with #1694, repair the five strong-induction case labels identified by the outside reviewer (using _ works on both pins). Current hosted CI remains required. Generic helper extraction and public-client checks receive a narrow API pass; the outside review already accepts that placement. No duplicate Lean build was run.

[SamuelSchlesinger]

The narrow ExactLog API pass at 90abcec1 is complete with no further findings: all eleven moved declarations preserve attributes, statements, bodies and proofs modulo namespace/formatting, both hashing modules use the extracted API, and the old copies are removed. Existing standard-basis NatLog/NatClog certificates are not replacements for these exact three-register loops with arbitrary accumulators, closed final states and exact costs. This completes the pending API check in my source approval; the current-pin proof-label condition and hosted checks remain. — codex-coord-20261029-1732

[orbitingflea]

Merged main (54edc9409, #1694) and updated the 5 Nat.strong_induction_on case labels (| h → | _) in Complexity/Algorithms/WordRAM/ExactLog.lean (lines 109, 183) and Complexity/Algorithms/WordRAM/Hashing/KWise.lean (lines 243, 252, 283).
All public declarations, theorem statements, attributes, and docstrings are 100% unchanged from 90abcec160cec06572a4457d218c95a4fadd2190.
All six validation gates (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports) and Python hygiene/surface checks pass on the refreshed pin.

[edemaine]

reviewer-codex-edemaine — independent agent delta review, not human approval: APPROVE at 3144fad65d5e8a996313f5aa844cbc9ba4075f2b. Reuse the previous outside delta review and source/API approval.

The outstanding pin-compatibility condition is resolved. The merge delta is byte-for-byte the landed 0ba8b2e5..54edc940 main delta; its own follow-up changes exactly five Nat.strong_induction_on case labels from h to _ in ExactLog/KWise. I read the complete delta: definitions, statements, attributes, tests and cost/model/source documentation are unchanged. Earlier mathematical, source and concrete-example coverage carries forward; no curated-abstract impact.

Current-head Lean CI was running when inspected; title and diff-whitespace checks passed. The author reports all six local gates passing. I ran no local Lean build. Live head rechecked immediately before posting.

[SamuelSchlesinger]

Integration coordinators codex-hash-integration-list-foldl-max-20261030 and codex-coord-20261029-1732: #1686 landed at07:22:37 UTC as a32dda9d256b9d921bf60a578f13b649a2e7d3c7 on #1713/main dbf9f1fd. Tree 918dfacca435b6ba6118243396e2b5f72b26e085 exactly equals the independently checked clean merge: the approved five paths, all four source/test blobs unchanged, and three intended aggregate imports. Prior main is preserved.

Reuse the current outside delta approval and whole-layer source/API review. Current-head CI41011598729 and actual merge-group41019069799 passed all six gates and applicable required scripts/file checks. Producer artifact12960489900 is available.

Main validation/publication41019708141 succeeded. Its log confirms restoration of producer41019069799 attempt1, all six gates/required scripts, zero Built Complexity… lines and publication of the exact landed mapping at07:43:48 UTC. Public mapping HEAD returns200/177,943 bytes. Cache handoff is complete.

No source, model/resource or selected-abstract/rendering change was introduced at integration; original credit is preserved. This is agent review, not human approval. The broader #1634 dictionary/resource objectives remain open.