Repository navigation
feat(Dictionary/CuckooHashing): distributional hop and expected cost from allocation - #2265
Draft
SamuelSchlesinger wants to merge 1 commit into
Draft
SamuelSchlesinger wants to merge 1 commit into
SamuelSchlesinger wants to merge 1 commit into
Conversation
…from allocation Layout.refinement refines the seed-level model by the memory methods with coins, exactly in law and within the model charges in expectation. The run from allocation answers as the dictionary does, and its expected memory cost is the start plus Scheme.opBound per operation; run_tableBits instantiates Pagh and Rodler's parameters. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
worker-claude-015dlg8k-cuckoomem(Claude Code, Opus), for #2205. Last of four stacked PRs on cuckoo hashing over the memory oracle; stacked on #2264.Change
Dictionary/CuckooHashing/Memory.lean: the distributional hop and the expected-cost transfer.Layout.refinement : RandomizedRefinement (Scheme.spec V n_max) (Memory.spec w).toRandomized.withCoins. Each method realizes the model's law exactly (methods_spec), andexpectedAmortizedshows its expected memory cost is at most the model's charge (7 per lookup or update,10 + 8 · roundsper new key, plusrehashCostwhen the seed fails), with zero potential.runallocates the table, marks the seed fresh, draws the hash tables and serves a dictionary client.run_correct: from any memory with room, its answer is a point mass at the dictionary's answer (throughrun_linkandScheme.run_map_dict).expectedCost_run_le: its expected memory cost is at mostspan + 2 + 4UplusScheme.opBoundper operation of the client's history (throughExpectedAmortized.clientandScheme.expectedCost_le).run_tableBitsinstantiates Pagh and Rodler's parameters (tableBits,maxEvictions,isCuckooHashPair_uniform): 7 units per lookup and44 + 6 · rehashCost / (n_max · maxEvictions n_max)per insertion, in expectation. A test runs it on a concrete client.Scope and limitation. The seed is a pair of random hash tables (the #2232 pilot), so a rehash writes
2Ucells and the insertion bound isO(1 + U / (n_max log n_max)), not theO_c(1)ofWordRAM/CuckooHashing.lean, whose regime-switched polynomial/double-tabulation family hasO(n)seeds. A memory implementation of that family plugs into the same hop (onlyIsCuckooHashPair, the fallback and the resample cost change).compCoinsis not needed: the rehash coins are the hash family's resamples, inlined in one memory hop. Execution on the word RAM is hop 4 (C2), not built here.Probability.PMF.pure_injectiveis added besidemap_injective.Size against the hand-stepped version. Memory layer 2,773 lines (Basic 524, Insert 682, Rehash 963, Memory 604) plus the pure model 976, against
WordRAM/CuckooHashing.lean6,461 and the WordRAM half ofHashFamily.lean1,236. Longest proofs: 150 (wp_fallbackProg), 147 (wp_insertProg_new), 131 (DistInv.tsum_charge_le, pure), 109 (wp_evict) against 286 (insertCode_execCodeDist), 253, 243 (evictRoundBodyCode_execWithin), 232 (cuckoo_steps_expected_amortized), 220 (getCode_execWithin). Both reuse the pure analysis (Dictionary/CuckooHashing.lean, the pure half ofHashFamily.lean) unchanged.Validation
lake build --wfail Complexity ComplexityTests ComplexityAbstractslocally; CI runs the full gates.AI assistance
Written by Claude Code (Opus) as an agent; no human review yet.
🤖 Generated with Claude Code
https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG