[SamuelSchlesinger]

worker-claude-015dlg8k-cuckoomem (Claude Code, Opus), for #2205 (randomized hops, D10). First of four stacked PRs implementing Pagh and Rodler's cuckoo hashing over the memory oracle (#2262 → #2263 → #2264 → #2265); stacked on #2236.

Change

The seed-level model (Dictionary/CuckooHashing/Model.lean, pure). Scheme.spec is cuckoo hashing as a RandomizedSpec: a state holds the seed, the keys in insertion order, the dictionary and a freshness flag; the tables are not stored, they are pureReplay of the keys. An insertion of a new key keeps the seed if the replay still succeeds and otherwise rehashes (Scheme.rehashLaw): up to attempts uniform seeds, then a fallback seed. Programs over memory are finite FreeM terms, so the Las Vegas loop cannot run until success; the fallback keeps every operation correct and its probability 2^-attempts per rehash is charged.

• Scheme.dictRefinement: the dictionary is refined by the model; answers do not depend on the seeds (run_map_dict).
• Scheme.expectedCost_le: under IsCuckooHashPair (the existing pure analysis, reused unchanged), the expected charge of any admissible client is at most opBound per operation. The proof tracks the law of the model state (DistInv): fresh states are uniform on the surviving seeds, stale states have probability at most |keys| · 2^-attempts. A per-state ExpectedAmortized certificate cannot give O(1) (an adversary knowing the seed could pick a failing key), so this is the oblivious argument the answers permit.

Layout and lookup over Memory (Dictionary/CuckooHashing/Memory/Basic.lean). Named fields: count, freshness flag, keys, values, two tables (2^b slots, slotWord = index + 1), two hash tables (U cells, as in the RandomTable pilot). The abstraction reads a Model; the invariant asks the tables to encode pureReplay. A lookup probes two slots and computes lookupEntry (wp_probe, at most 6 reads; wp_getProg, 7).

Also: Probability.PMF.map_apply_of_support (general, in Probability/PMF/Map.lean), and StateTransition/WP.lean from #2244 (aaf6c3cb3, cherry-picked unchanged; it leaves this diff when #2244 lands).

Existing notions considered: pureReplay, lookupEntry, survivingSeeds, IsCuckooHashPair and cuckooWalkRounds are reused unchanged. Model/Scheme are new because no seed-level randomized specification of cuckoo hashing exists; the WordRAM file keeps the seed in machine memory and does the distributional argument on ExecCodeDist. Memory.Prog specifications use #2244's StateTransitionSpec.wp rather than a local predicate.

Validation

lake build --wfail of the touched modules and their importers, check_hygiene.py --check-simp; CI runs the full gates. No sorry, axioms or heartbeat overrides.

AI assistance

Written by Claude Code (Opus) as an agent; no human review yet.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[SamuelSchlesinger]

coordinator-claude-015dlg8k (Claude Code): on hold as drafts (#2262–#2265), under the #2205 policy that Samuel approved. No parallel ports land without a deletion plan, and migrations must not weaken statements. The chain is sound and reuses pureReplay/IsCuckooHashPair unchanged. But its seeds are #2232's random tables, which rewrite 2U cells per rehash, so the expected insertion bound is O(1 + U/(n·maxEvictions)), weaker than WordRAM/CuckooHashing.lean's O_c(1).

To resume: implement the regime-switched polynomial / double-tabulation family over Memory (it plugs into the same hop), match the existing bound, and then replace and delete Dictionary/WordRAM/CuckooHashing.lean in the same stack. Parts that are reusable on their own, the seed-level Scheme model and RandomizedSpec.expectedCost_bind_le, can be split out if another client needs them first.