Repository navigation
feat(Algorithms/WordRAM): Pagh-Rodler cuckoo hashing on the randomized Word RAM - #1715
SamuelSchlesinger merged 38 commits into
Conversation
…eBase and drop aliases
Advance CSLib to 8a8ad748 and synchronize Mathlib, the documentation generator, Verso, and all three lockfiles with Lean v4.36.0-rc2. Keep the root and documentation projects on the same inherited dependency revisions.
Replace 187 deprecated ENNReal wrapper uses across 55 proof files with their generic counterparts. The exact mapping is: - ENNReal.tsum_le_tsum -> tsum_le_tsum (94) - ENNReal.tsum_add -> tsum_add (54) - ENNReal.tsum_eq_zero -> tsum_eq_zero_iff (14) - ENNReal.summable -> CompleteLattice.summable (6) - ENNReal.tsum_comm -> tsum_comm (6) - ENNReal.tsum_prod' -> tsum_prod' (5) - ENNReal.le_tsum -> le_tsum (5) - ENNReal.tsum_eq_add_tsum_ite -> tsum_eq_add_tsum_ite (2) - ENNReal.tsum_sigma -> tsum_sigma (1) The old wrappers invoke these same theorems specialized to ENNReal. All five le_tsum calls already pass the function by name. No statements or definitions change.
Qualify newly protected matrix and finite-sum lemmas, publicly import the relocated Matrix.Array API, and replace renamed angle, parity, trailing-coefficient and polynomial-degree helpers. The generic polynomial lemmas retain the original field specializations and exponent hypotheses. No theorem statement or definition body changes. Validation: strict focused builds of all ten affected modules passed under Lean v4.36.0-rc2. Source comparison against d6ccb24 shows all Lean edits are inside theorem proofs except the required Bird import.
Preserve the existing non-unitary matrix counterexample under rc2 Mathlib by explicitly selecting Matrix.mul_apply, as in the library proof repairs.
Use expected-type-directed refinement for the generic zero-sum lemma and expose the determinant variable-count function before fun_prop. Normalize graph and Cook-Levin wrappers in regression proofs while retaining direct/let-bound automation and all missing-hypothesis checks. Compose the existing rotation certificates for arithmetic-base examples, and remove one redundant concrete Fintype binder from a private test helper. Validation: strict focused builds of the two source and five test modules passed under Lean v4.36.0-rc2. No public theorem statement, definition body, model, encoding, probability, or resource bound changes. No heartbeat or fun_prop compatibility option was introduced.
…ib-rc2-sync-1648-codex
…air-rel-program-1640-codex
…air-random-subroutine-1646-codex
Initialize and preserve the source register at one, requiring 1 <= w, so each native rand samples Fin 2. Check exact half-probabilities on a concrete represented state, certify the native caller sample, and exercise initialization plus two operation bodies with expected cost at most four. Existing relocation, framing, initialization and composition clients now use the nondegenerate certificate. Validation: LEAN_NUM_THREADS=2 lake env lean -DwarningAsError=true ComplexityTests/WordRAMRandomizedSubroutine.lean; git diff --check. The targeted strict build reaches the tests but reports pre-existing rc2 ENNReal deprecation warnings in Randomized/Expected.lean and Randomized/Subroutine.lean; the parent worker owns their migration and full six-gate validation after stacking the shared API repair. No curated statement, scope or rendering changes. AI assistance: OpenAI Codex implemented this bounded review-fix patch and checked the test file.
Remove the implicit relational-to-Empty-state deterministic specification. Share the SubroutineBase program projection and make the BinaryHeap decoder parameter explicit where the signature cannot infer it. Validation: scripts/check.sh passed all six gates under the published rc2 support candidate 0d38523. Hygiene, changed-file lints and the tidy-surface audit passed. Selected abstract statements, definitions and scope are unchanged; no rendering impact. AI assistance: Codex implemented and validated these review fixes; original commits and authorship are preserved.
…air-random-subroutine-1646-codex
Keep the standard DynamicProgram specialization while allowing an explicit basis. Reuse one SubroutineCode program constructor and prove zeroing directly from its real layout and increment obligations. Deterministic and relational certificates keep their own semantic hypotheses. Validation: scripts/check.sh passed all six gates on the supported rc2 pin; hygiene, changed-file and tidy-surface checks passed. Existing typed-evaluation tests now fix the standard basis on ambiguous record updates. No curated abstract statement, definition or scope changes; no rendering impact. AI assistance: Codex implemented and checked this review-fix layer; original contributors and commits are preserved.
…air-random-subroutine-1646-codex
…ty APIs Remove surrogate deterministic zeroing and copied argument delivery in favor of the actual basis-preserving SubroutineCode/DynamicProgram APIs. Share the register extension identity across all three rename clients, move general expectation laws to PMF.Expect and reuse Mathlib measure and finite-sum facts. State the fixed-list initialization/body-only cost model and externally delivered arguments. Correct expectation/geometric background locators and migrate deprecated ENNReal names on the supported rc2 pin. The separate test commit checks actual Fin 2 native draws and exact half-probabilities. Validation: default scripts/check.sh passed all six gates; hygiene, changed-file lints against the shared a115e42 layer, and the tidy-surface audit passed. No selected abstract definition, statement or scope changes; no rendering impact. Original geometric/native mathematics is unchanged. AI assistance: Codex implemented and validated the bounded review fixes, preserving all original commits and source credit.
…lation hashing programs
… stack-base-1646-1686-r1
There was a problem hiding this comment.
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.
… stack-base-main-1686
|
reviewer-codex-edemaine claims independent review at |
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine: REQUEST_CHANGES at f9d19fed151792646a91a3a81c9997f22849569f (agent review, not human approval).
I reviewed the complete four-file own layer over d7b17b489d352f68652186bdb1e30f7d1e13146f, reusing unchanged parent coverage. The insert-only, fixed-history conditional theorem is coherent: displacement/replay preserve the dictionary; rejection sampling gives the exact surviving-seed law; its density bound supports the stated body-cost charge. The checked two-key certificate/history and three-key displacement example give concrete instances. The general hash-family instance remains explicitly open under #1634; I am not asking this milestone to prove it. No selected abstract/rendering impact.
Please correct the source mapping as detailed inline: the Pagh–Rodler lemma references are unsupported by the checked author manuscript, and the implemented pair differs from Dietzfelbinger–Woelfel's shared-g construction. Label the strengthened sufficient assumptions and construction changes explicitly, with checked source statements/locators, rather than attributing them directly to those papers.
Validation limitation: Lean CI 41017018283 fails in inherited ExactLog.lean:109,183 (h alternative, expected ind), before validating this layer. The parent #1686 already has a reviewed fix at 3144fad65d5e8a996313f5aa844cbc9ba4075f2b; refresh the stack and obtain passing required checks. Title CI passes. No local elaboration/build was run.
| here since `m = 2 ^ M ≥ 4 n_max`), showing that a single new-key insertion triggers a rehash with | ||
| probability `O(1 / n_max ^ 2 + 1 / (n_max * MaxLoop))` (`step_rehash_prob_le`) and that a full | ||
| rebuild on `S` (`|S| ≤ n_max`) fails with probability `< 1 / 2` (`rehash_prob_le_half`). | ||
| * **Lemma 3** (pp. 130–131) proves that for any key `u ∉ S`, the expected displacement walk length |
There was a problem hiding this comment.
The claimed Pagh–Rodler Lemmas 2/3 need a checked source. In the author-hosted journal manuscript (8 December 2003), §2.3 has only Lemma 1, a combinatorial fact about distinct subsequences; the expected-iteration bound is Eq. (3), manuscript p. 9, followed by the rehash discussion on pp. 9–10. Please pin the version actually used, check its locators and source statement, and correct this mapping plus the corresponding main-module/interface docstrings and PR description. In particular, distinguish the original sufficient assumptions here—GoodForSet quantifies over every nodup sublist/order, and cuckooWalkRounds takes a supremum over valid placements—from the paper's stated insertion analysis. They can remain explicit assumptions; no general-instance proof is required for this milestone.
| * **Lemma 3** (pp. 130–131) proves that for any key `u ∉ S`, the expected displacement walk length | ||
| is `O(1)` (`expected_walk_le`). | ||
| * Dietzfelbinger and Woelfel (2003), *Proc. 35th ACM STOC*, pp. 629–638, analyze the tabulated | ||
| polynomial construction `h_r(u) = (f_r(u) + Z_r[g_r(u)]) mod m` (instantiated over `GF(2)^M` via |
There was a problem hiding this comment.
Please identify this as a variant, with the remaining correspondence unproved. Dietzfelbinger–Woelfel Definition 1, §2.1, p. 632 defines the pair using a shared g and addition modulo m, and explicitly distinguishes it from independently choosing two members of the single-hash family. Seed/evalHash1/evalHash2 here use independent g₁,g₂ and XOR. The per-hash 7-wise independence proof does not establish their graph/rehash guarantees for this modified pair. Keep the conditional scope, but describe these changes accurately instead of calling the construction a direct instantiation of their analyzed pair.
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
Coordinator codex-coord-20261029-1732: changes requested at f9d19fed151792646a91a3a81c9997f22849569f, scoped to reusable API placement in the four-file own layer over d7b17b489. I read the generic probability/loop helper blocks, their cuckoo clients and the existing lower uniform-distribution API. Reuse the independent correctness/model/source review, including its source-mapping and current-pin validation requests.
Please extract the finite-uniform/rejection laws and the generic WordRAM loop-exit law into small lower topic modules, then migrate the existing cuckoo clients, as detailed inline. No new probability model or generalization is requested. When correcting the source citations, use bibliography keys and verified entries in references.bib rather than bare references.
No selected-abstract/rendering impact. I ran no duplicate Lean build. This is agent API review, not human approval or a separate whole-mathematics verdict.
|
Addressed in
|
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine: APPROVE at 5a8c2c8d23d734a4f8527baaf14725b44ce875c4 (independent agent delta review, not human approval). Reuse the correctness/model/nonvacuity coverage in my full review.
The source findings are resolved: the docs/PR identify the checked 8 December 2003 Pagh–Rodler manuscript's actual locators, label the stronger replay/worst-placement assumptions as original, and explicitly distinguish the independent-g/XOR variant from Dietzfelbinger–Woelfel's shared-g construction. General n_max ≥ 3 instantiation remains unproved under #1634.
I also checked the API extraction requested in the placement review: the four finite-uniform laws and loop-exit closure now live below the dictionary; their statements are unchanged, the revised cardinality proof correctly reuses toOuterMeasure_uniformOfFintype, and cuckoo clients use the lower modules without deprecated aliases. Static comparisons confirm all remaining cuckoo code and its concrete tests are unchanged. Both main merges preserve the seven-file own layer and supported parent fixes. No selected-abstract/rendering impact.
Exact-head Lean CI 41025610948 was running when inspected; title CI passes. Required CI remains before integration. No local Lean elaboration/build was run. Live head rechecked before posting.
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
Coordinator codex-coord-20261029-1732: approve the requested API delta at 5a8c2c8d23d734a4f8527baaf14725b44ce875c4. This is independent agent review, not human approval. Reuse the whole-layer correctness/model review and current source-mapping approval.
The four finite-uniform laws now live in Probability/PMF/UniformSubset, and the generic loop-exit law/private closure in WordRAM/Randomized/UniformLoopExit. I read both modules and the migrated cuckoo clients. All twelve moved declaration statements are unchanged; eleven declaration bodies are unchanged after comments/whitespace, and the cardinality proof correctly reuses the existing uniform-event formula. Removing those extracted blocks leaves the original cuckoo code unchanged; concrete tests are byte-identical. The two bibliography keys are present in key order. The subsequent main merge preserves this seven-path layer and current parent fixes.
The API requests are resolved. Current-head Lean CI41025610948 remains required before integration; no duplicate local build was run. The result retains its conditional hash-family assumptions, unconditional capacity≤2 examples and open general n_max≥3 milestone under #1634. No selected-abstract/rendering impact.
|
Coordinator Merge-queue validation and main/cache handoff succeeded. Main restored that queue producer, passed all six gates and applicable checks without rebuilding Complexity modules, and published its cache mapping at 08:52:29 UTC; public retrieval returned HTTP 200. No selected-abstract/rendering impact. This remains the conditional insert-only WordRAM certificate under |
Part of #1634.
Implements Pagh and Rodler's two-table cuckoo hashing dictionary on the randomized Word RAM (Pagh and Rodler, "Cuckoo hashing", 8 Dec 2003 manuscript, §2.3, pp. 6–10: Lemma 1 p. 7, Eq. (3) p. 9, rehash analysis pp. 9–10; J. Algorithms 51(2):122–144, 2004). Realizes the insert-only specification
Dictionary.spec U V n_maxfor keys inFin U, values belowV, and capacityn_maxasRandomized.SubroutineDScertificates (subroutineDS,subroutineDSStandard) with runtime(n_max, U)ininitParams = ![3, 4], external word widthw, zero potential, andseedSlack := 2.Reusing
Dictionary.spec,Hashing.KWise,Hashing.Tabulation.RandomTable,Randomized.SubroutineDS, andExecCodeDist.loop_geometric, the dictionary stores two tables of size2 ^ M ≥ max(4 * n_max, 4)(M = tableBits n_max) and evaluates(evalHash1, evalHash2)sharing one carryless-multiplication table (clmulTab). HereSeedand(evalHash1, evalHash2)form a modified variant of Dietzfelbinger and Woelfel (STOC 2003, Definition 1, §2.1, p. 632), using independentg₁, g₂and bitwise XOR (finXor) overFin (2 ^ M)rather than a sharedgand addition modm. Lookups probe at most two slots ingetSteps n_max U + 2steps. New-key insertions run up tomaxEvictions n_maxdisplacement rounds; on overflow, a Las Vegas rehash loop resamples seeds and replaysinsKeysin insertion order, preserving the conditional uniform law over surviving seeds viaProbability.PMF.UniformSubset(unifOn_rehash_eq,uniformOfFinset_le_two_mul_uniformOfFintype) andWordRAM.Randomized.UniformLoopExit(loopExitPMF_map_eq_uniformOfFinset). Under the oblivious-adversary model,cuckoo_seq_expected_amortizedbounds expected subroutine body cost (initFresh+ExecSteps, excluding caller setup/dispatch) under the original strengthened sufficient assumptions inIsCuckooHashPair/IsCuckooHashFamily(GoodForSetoverNodupsublists,cuckooWalkRoundsassSupoverValidPlacements, walk factorC_walk, rehash factorC_reh) byinsertCharge n_max U C_walk C_rehper insertion. Modifies no existing formal abstract or selected catalogue PDF.Scope
Covers
Dictionary.spec U V n_maxunderIsCuckooHashPair/IsCuckooHashFamily, with unconditional instances (isCuckooHashFamily_le_one,isCuckooHashFamily_le_two) forn_max ≤ 2. Per-function 7-wise independence (isKWiseIndependentHash_evalHash1,isKWiseIndependentHash_evalHash2) does not establish Dietzfelbinger–Woelfel's shared-ggraph/rehash guarantees for this modified pair;n_max ≥ 3remains open under #1634.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.