Repository navigation
feat(Dictionary/CuckooHashing): rehashing over memory with coins - #2264
Draft
SamuelSchlesinger wants to merge 1 commit into
Draft
SamuelSchlesinger wants to merge 1 commit into
SamuelSchlesinger wants to merge 1 commit into
Conversation
A rehash draws fresh hash tables with the RandomTable fill, rebuilds, and falls back to the position seed after its attempts. Its law is Scheme.rehashLaw, every outcome satisfies the invariant, and its expected cost is bounded when attempts fail with probability at most a half. Adds RandomizedSpec.expectedCost_bind_le and PMF.tsum_pure_mul. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG
This was referenced Nov 2, 2026
SamuelSchlesinger
marked this pull request as draft
November 2, 2026 02:38
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. Third of four stacked PRs on cuckoo hashing over the memory oracle; stacked on #2263.Change
Dictionary/CuckooHashing/Memory/Rehash.lean: rehashing overMemorywith coins.HashFamily.RandomTablepilot'sfill, clears the tables and replays the keys; two fills are a uniform seed (run_fills_bind, viarun_fillanduniformOfFintype_prod). Afternfailed attempts the fallback hashes each key to its position in the first table, under which every insertion settles (isSome_pureReplay_posMap).rehash_spec: the stored model after a rehash followsScheme.rehashLawexactly, and every outcome satisfies the invariant.expectedCost_rehash_le: when a uniform seed fails the keys with probability at most a half, a rehash costs at mostrehashCostin expectation (geometric attempts plus the fallback). This is the spec-level counterpart ofExecCodeDist.loop_geometric.demonicValid_rehash: every memory call is admissible.API addition in
StateTransition/Randomized.lean(randhop2's lane is idle; posted on #2205):RandomizedSpec.expectedCost_bind_le, boundingp >>= kby a bound onpplus one on the continuation from every outcome. AlsoProbability.PMF.tsum_pure_mulbesidetsum_map_mul/tsum_bind_mul.Validation
lake build --wfailof the touched modules and their importers; 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