Repository navigation
feat(Dictionary/CuckooHashing): eviction walk and insertion over memory - #2263
Draft
SamuelSchlesinger wants to merge 1 commit into
Draft
SamuelSchlesinger wants to merge 1 commit into
SamuelSchlesinger wants to merge 1 commit into
Conversation
The walk computes pureEvict on the encoded tables in eight memory units per round, a replay computes pureReplay, and an insertion appends a new key and walks it, answering whether a rehash is needed. 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. Second of four stacked PRs on cuckoo hashing over the memory oracle; stacked on #2262.Change
Dictionary/CuckooHashing/Memory/Insert.lean: the eviction walk and insertion overMemory.Layout.evictcomputesWordRAM.CuckooHashing.pureEvicton the encoded tables (wp_evict): each round reads the hashes and displaced keys and writes two slots, at most 8 units per round, so8 * evictRoundsper walk. It writes only the tables.Layout.Walkis the memory relation it needs: hash cells hold the seed, key cells the keys, the tables encode a pure table whose entries point at their keys (Consistent).Layout.replayreplays keys by successive walks and computespureReplay(wp_replay).Layout.insertProg: a stored key is overwritten in place (wp_insertProg_present, 7 units); a new key is appended and walked (wp_insertProg_new,10 + 8 * evictRoundsunits). It answers whether a rehash is needed, which is exactly when the keys with the new one do not replay; otherwise the invariant is restored.The pure displacement model (
pureEvict,evictRounds,pureReplay_append_singleton) is reused unchanged; the memory proofs mention no registers,Fitschains or instruction counts.Validation
lake build --wfailof the touched modules; 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