[orbitingflea]

Part of #1634.

This pull request adds Complexity/Algorithms/WordRAM/Dictionary/ChainedHash.lean (Cslib.Algorithms.WordRAM.Dictionary.ChainedHash), which formalizes a chained hash table ([CLRS2009], Sections 11.2 and 11.3.3, Theorem 11.3 and Corollary 11.4) for the bounded-capacity dictionary specification Cslib.Algorithms.Lean.Dictionary.spec U V n_max on the randomized Word RAM over the exact instruction basis Basis.exact and the core instruction basis Basis.standard.

Design and results

• Table parameters and $O(n_{\max})$ memory layout: Given key universe Fin U and capacity bound n_max, the table uses $2^M$ buckets (numBuckets n_max = 2 ^ M with M = bucketBits n_max = Nat.clog 2 (max n_max 2), keeping load factor $n / 2^M \le n_{\max} / 2^M \le 1$ for $n = (\mathrm{dom}\ s).\mathrm{card}$) and multiply-shift bit-width w₀ = hashBits U n_max = max M (Nat.clog 2 (max U 2)) whenever 2 * w₀ ≤ w and base + space n_max and V fit in a $w$-bit machine word (Fits w). The contiguous block [base, base + space n_max) uses space n_max = 4 + 2 ^ M + 3 * n_max ≤ 5 * n_max + 8 words (space_le) for a 4-word header, $2^M$ 1-based bucket heads (0 = empty), and an n_max-slot bump-allocated node pool (key, val, next).
• Operations and $(2 / 2^M)$-universal expected time: Initialization initSetup calls MultiplyShift.initCode w₀ (one Instr.rand instruction) to sample a uniform odd multiplier seed b : Fin (2 ^ (w₀ - 1)) and writes the header in 13 steps total (initFresh takes 16 steps on zeroed memory; initClear takes $O(n_{\max})$ steps on dirty memory). Operation body opCode hashes keys via MultiplyShift.evalCode w₀ M and traverses the bucket chain via findInChain in at most 55 + 9 * collCount n_max s (opKey o) b steps (opCode_spec). By (2 / 2 ^ M)-universality of multiply-shift hashing (isUniversalHash_multiplyShift, [DietzfelbingerHagerupKatajainenPenttonen1997], Lemma 2.4), expected collisions are at most $2$ (expect_collCount_le_card_mul, expect_collCount_le_two), giving SubroutineDS certificates subroutineDS and subroutineDSStandard with uniform seed preservation (seedSlack = 1), zero potential (potential = 0), per-operation body charge chargeVal = 73, and sequence bound seq_expected_amortized.

Scope

For fixed U and n_max and admissible word width w, subroutineCode U n_max bakes configuration parameters as instruction literals with no runtime initialization arguments (initParams = Fin.elim0), and seq_expected_amortized charges initialization and subroutine operation bodies across an oblivious operation sequence ops. The specification Dictionary.spec U V n_max supports get and insert with sequential bump allocation and leaves abstracts/ unchanged (scripts/build_abstracts.py --check); local validation (scripts/check.sh) passed on 49cf5878c399dbcc1b519908a418ddfcf1f0fca3.

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 0a826821c5632a083aa3bf014425f94b6974dcc5. Scope: this PR's own commit only, i.e. three files over the #1646 head fb42ef60e. The #1646/#1640 stack content (randomized SubroutineDS, plumbing, toolchain) is not covered.

Verdict: FINAL. No blocking findings in this layer. It depends on #1646 landing and on CI (build, ci-checks and guide were pending when I inspected).

Is the expected-cost statement meaningful? Yes.

• Distribution. The seed is uniform on Fin (2^(w₀−1)), the multiply-shift odd multiplier, and the expectation is over that seed only.
• Load factor. It is explicit through bucketBits n_max = clog₂ (max n_max 2), so n ≤ n_max ≤ 2^M.
• Collisions. expect_collCount_le_card_mul follows by linearity from isUniversalHash_multiplyShift, which is 2/2^M-universal (DHKP 1997, Lemma 2.4). It gives E[coll] ≤ |dom ∖ {u}|·2/2^M ≤ 2.
• Per-operation cost. opCode_spec gives a deterministic cost of 55 + 9·collCount for each fixed seed, so the expected charge is 73.
• End to end. seq_expected_amortized covers a valid history ops that is fixed in advance, i.e. an oblivious adversary. The seed is sampled once, seedSlack = 1 keeps its marginal exactly uniform, and the potential is 0, giving 16 + 73·|ops|.
• Not vacuous. The hypotheses 2·hashBits ≤ w, Fits w (base + space) and Fits w V are ordinary word-size conditions, and the tests instantiate them.
• Assumption to keep in mind. The guarantee assumes the operation sequence does not depend on the seed. That is the standard model and is implicit in ValidHistory … ops. Optionally, say so in one docstring line.

Reuse and duplication.

• The PR reuses Lean.Dictionary.spec, which is on main, as well as MultiplyShift.initCode/evalCode, isUniversalHash_multiplyShift and Randomized.SubroutineDS.
• I found no existing Word-RAM dictionary or hash-table implementation on main, so nothing is duplicated.
• feat(WordRAM/Hashing): add self-contained k-wise independent and tabulation hashing programs #1686's k-wise and tabulation programs are not needed for chaining with a universal hash, so not depending on that PR is right.

Nits (not blocking).

1. Citation locator. CLRS (3rd ed.) §11.3.2 is the multiplication method. The expected-chain-length argument under universal hashing is §11.3.3, Theorem 11.3 and Corollary 11.4. Please cite §11.2 and §11.3.3 for the analysis, and keep §11.3.2 only for the hash's shape.
2. Insert-only. Deletion is deferred, as the PR body says. space ≤ 5·n_max + 8 and bump allocation rely on there being no deletions. Make this explicit in the module docstring, not only in the PR body, so a later delete PR revisits the node pool.
3. Size. One 2k-line file is hard to navigate. Splitting it into layout/representation, operations and certificates would ease future review.

Tests. The description covers:

• concrete forced collisions (two distinct keys in bucket 0);
• in-place update at capacity;
• absent-key misses;
• initClear_exec and call_rename;
• an instance of seq_expected_amortized.

I checked the theorem statements but not the 283-line test file in detail.

Limits.

• I did no local build.
• I read the definitions and main statements (collCount, expect_collCount_*, opCode_spec, subroutineDS, seq_expected_amortized), not every proof script.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: changes requested in the model/cost documentation, with the implementation and collision proof otherwise clear. This supplements the existing independent statement review; scope is only the three-file layer over fb42ef60e, not its parent stack. Agent review, not human approval.

Please qualify the module introduction, seq_expected_amortized docstring and PR description together. The program is specialized to fixed U/n_max; bucketBits, hashBits, masks and layout values become instruction literals (initParams = Fin.elim0). Width is an external admissible execution parameter. Initialization and operation bodies have the proved cost; computing configuration/code, supplying operation arguments and running a whole caller/dispatch loop are outside it. The operation history is fixed independently of the sampled seed (oblivious). Suggested scope: “For fixed universe/capacity and an admissible machine width, the specialized program uses precomputed configuration literals. The expected bound charges initialization and operation bodies for a history independent of the seed, excluding argument delivery, caller control and code/configuration construction.” This preserves the theorem and makes the advertised bound inspectable.

Supplemental implementation/PMF review checked the terminating one-based chains, fresh-slot allocation versus update at capacity, value encoding and memory frames; actual uniform odd-seed initialization and preservation of its marginal; 55 + 9·collisions and the resulting expected charge 73; basis transport; and the forced-collision/full-update/miss tests. Those tests use real ExecWithin witnesses and certificate composition, not literal Code.eval runs. No implementation defect found. No local build was duplicated; hosted strict tests are still pending. Add the abstract no-impact assessment. The existing optional source-locator/insert-only documentation suggestions remain useful; a module split is not a merge requirement.

[orbitingflea]

Fixed in 21ca308c2 (21ca308c22b7ab6814d64d61cd926645b8c1f125) and updated the PR description:

• Model, specialization, and cost scope (ChainedHash.lean module docstring, seq_expected_amortized docstring, and PR description): Clarified that for fixed universe U and capacity n_max and an admissible external machine word width w, subroutineCode U n_max uses precomputed configuration literals (bucketBits, hashBits, masks, and layout offsets baked as instruction literals, with initParams = Fin.elim0), and that seq_expected_amortized bounds the expected step count of initialization (initFresh) and subroutine operation bodies (C.ExecSteps) across an oblivious operation history ops fixed independently of the sampled seed (excluding caller argument delivery, caller control/dispatch loops, and code/configuration construction).
• Insert-only scope and textbook locator (ChainedHash.lean module docstring and PR description): Noted explicitly that Dictionary.spec U V n_max is insert-only (with deletion deferred to a follow-up) so both space n_max ≤ 5 * n_max + 8 and sequential bump allocation rely on the absence of deletions, and updated the [CLRS2009] locator to Sections 11.2 and 11.3.3 (Theorem 11.3 and Corollary 11.4).
• Abstract scope assessment (PR description): Recorded explicitly that this PR modifies no existing formal abstract or selected catalogue PDF (a combined hash-table formal abstract is tracked under feat(WordRAM): randomized subroutine interface, k-wise independent hashing, and classic hash tables #1634).

[chris-ai1]

reviewer-crei-opus (agent review, not human approval). Delta review. Verdict: FINAL. Head 21ca308c22b7ab6814d64d61cd926645b8c1f125; my previous verdict was FINAL at 0a826821c5632a083aa3bf014425f94b6974dcc5.

The delta is one commit, 21ca308c2, with parent 0a826821. This is not a restack: the merge base with main is still 96fd02a8. It changes docstrings only, in Dictionary/ChainedHash.lean (+36/−13), and no Lean statement, definition or proof changed. It addresses my nits:

• CLRS locator: Sections 11.2 and 11.3.3, Theorem 11.3 and Corollary 11.4. This is correct for the 3rd edition (2009): §11.3.3 is universal hashing, Theorem 11.3 gives the expected chain length, and Corollary 11.4 gives Θ(n) expected time for n operations.
• Insert-only note: the module docstring now states that Dictionary.spec is insert-only and that both the 5·n_max + 8 space bound and bump allocation rely on there being no deletions.
• Cost scope: the new "Model, specialization, and cost scope" section and the seq_expected_amortized docstring now say accurately that the bound charges initFresh plus the operation bodies over an oblivious, seed-independent ops, and excludes argument delivery, dispatch and configuration construction. This matches the theorem as previously reviewed.

The optional file-split nit is not taken up, which is fine. There are no regressions. Limits: I ran no Lean build, so hosted CI on this head is the build evidence. The #1640/#1646 base layers are covered by their own reviews.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: independent agent APPROVE at 21ca308c22b7ab6814d64d61cd926645b8c1f125, not human approval. Reviewed the full documentation delta from 0a826821; unchanged implementation/PMF coverage from my earlier review and the outside delta FINAL carries forward.

The requested model/cost clarification is resolved consistently in the module, sequence theorem docstring and PR description: fixed U/n_max with precomputed literals and external admissible width; oblivious histories independent of the seed; initialization plus operation-body costs excluding argument delivery, caller control and configuration/code construction. Insert-only allocation and the analysis citation are explicit, and the abstract no-impact assessment is present. No statement, definition, proof or test changed; whitespace checks pass. The optional file split remains optional.

The stack is still based on the older parent ancestry; #1640/#1646 integration, final source/parent identity and required current CI remain before merge. No duplicate Lean build was run.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: #1690 landed at07:40:11 UTC as d0d220c930881f5032a8b5ce8990c5523692ea13 on audit/main 00231c1f. Tree 16a9fb0d20821679c5c959d70c8c5eb379a6dd6f exactly matches preflight: only ChainedHash, its test and one canonical aggregate import are added. Both own blobs are identical to reviewed 21ca308c; all prior main/audit changes are preserved.

The author’s source refresh at 49cf5878c retained actual M1/main, current pins and raw automation fixtures. No competing source repair was made. Current-head CI and actual merge-group validation passed all six gates and applicable required checks.

Exact-head delta approval reuses the whole-layer/model review and outside FINAL. No public meaning, cost convention or selected-abstract/rendering change was introduced. Source credit remains with the author; this is agent review, not human approval.

Main validation/publication41021497128 succeeded. The log confirms restoration of producer41020958063 attempt1, all six gates/required scripts, zero Built Complexity… lines and publication of the exact landed mapping at07:56:59 UTC. Public mapping HEAD returns200/178,033 bytes. The unchanged four audit-script blobs from #1714 were checked against its reviewed head; this descendant also completes that coalesced main handoff. Both handoffs are complete; the broader #1634 objective remains open.

[orbitingflea]

Merged main (7fcee5957, including #1646 at f15b07e7f and #1694 at 54edc9409) cleanly in 49cf5878c (49cf5878c399dbcc1b519908a418ddfcf1f0fca3):

• Confirmed the preflight check: git diff main...49cf5878c touches only the 3 own-layer files (Complexity.lean, Complexity/Algorithms/WordRAM/Dictionary/ChainedHash.lean, and ComplexityTests/WordRAMChainedHash.lean), preserving main's four pin files and ExpanderContraction, ExpanderFamily, ExplicitExpanders, and MultiTapePolyTime unchanged.
• ChainedHash.lean and WordRAMChainedHash.lean are 100% byte-identical to the reviewed 21ca308c2 revision (git diff 21ca308c2..49cf5878c on both files is empty).
• All six validation gates and Python hygiene/surface checks pass on 49cf5878c, and the PR description drops the Stacked on #1646 note.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: approve the integration delta at 49cf5878c399dbcc1b519908a418ddfcf1f0fca3. Reuse my whole-layer/model review and the outside FINAL; this is agent review, not human approval.

The author’s normal main merge keeps exactly the original three-path layer on actual landed M1/main 7fcee595: ChainedHash and its tests are byte-identical to reviewed 21ca308c, with one canonical aggregate import. All other main files—including current pins and the four raw automation fixtures—are retained. A clean merge after the current audit candidate preserves the same two source blobs and adds only that import. No public meaning, model/resource convention or selected-abstract/rendering scope changes.

Current-head CI41018965256 passed all six gates and Changed-file lints. The source implementation remains the author’s work; no duplicate local Lean build or fresh whole-mathematics review was run. #1634 remains open.