[SamuelSchlesinger]

Part of #2205 (M1a, decision D7). worker-claude-015dlg8k-m1a (Claude Code, Opus) wrote this PR.

This adds the memory oracle that #2205's implementation hops are written against. The signature was posted on the issue first (comment) so that the realization kernel (C2/M1b) can build against it.

• Complexity/DataStructure/Memory/Spec.lean. Memory.spec w is a deterministic StateTransitionSpec with these operations:

  • read, write;
  • alloc: zeroed, charged k + 1;
  • allocDirty: one unit.

  Its state is the whole memory mem : ℕ → ℕ plus an allocation frontier. valid carries the preconditions: accessed addresses lie below the frontier, written values satisfy Fits w, and the frontier after an allocation fits. WellFormed (frontier and cells fit) is preserved by admissible histories, so allocated addresses fit a word. Memory.Prog is the client monad (PFunctor.FreeM, hence OracleComp). State.init is the word RAM's input convention.

• Complexity/DataStructure/Memory/Field.lean. Named field arrays are WordRAM.Blocks accessed by b.get i and b.set i v. The file also adds Block.Allocated, the list view Block.entries (which realizes Block.HoldsList), allocBlock/allocBlockDirty, and one-step runClient lemmas.

• ComplexityTests/DataStructureMemory.lean. A struct-of-arrays linked list is allocated, built and summed by pointer chasing, and a scratch block is reused across two rounds. The tests check answers, histories, charges and admissibility at w = 8, and that a read above the frontier, an oversized write and an overflowing allocation are rejected.

This is infrastructure, not new mathematics.

Existing notions considered.

• Reused: WordRAM.Block, Block.Owns, Block.Realizes/HoldsList, WordRAM.clear (allocation semantics), Fits, Data.init, StateTransitionSpec.ofFn.
• WordRAM.alloc/readAt/writeAt are the machine code that a realization of these operations would use. They are not duplicated here.
• No existing StateTransitionSpec models word-addressed memory (R2 gap 1 in the WordRAM: algorithms as oracle programs, refined to RAM by game-hop proofs (stem hand-stepped proofs) #2205 research).
• Block.entries is the function form of Block.HoldsList, which is a relation. An abstraction function needs the function form; holdsList_entries relates the two. outputList is the length-prefixed special case.

Validation. At head 5909d1bae, lake build Complexity ComplexityTests ComplexityAbstracts --wfail --iofail passes locally. The CI-only checks also pass: check_hygiene.py --check-simp, check_tidy_surface.py and check_changed_files.py. Hosted CI runs the full gates.

Limits. Allocation is bump-only, with no free. The realization on the word RAM is #2205 C2 (Codex). The open interface questions are listed in the linked comment.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[edemaine]

Agent review by reviewer-codex-edemaine (independent worker): APPROVE at 5909d1bae7648600e86ab49730835ce9d336ca95.

Reviewed the complete four-file change and the underlying StateTransitionSpec, WordRAM.Block, allocation and input definitions. Admissible histories preserve fitting cell contents and frontier; allocated addresses consequently fit. Zeroed allocation clears precisely its new interval, dirty allocation preserves existing contents, and field framing/list-view lemmas match those semantics. Field accesses still require their index bounds when proving admissibility.

The concrete 8-bit linked-list client checks result 12, its exact history and charge 15; scratch reuse and rejected read/write/allocation cases provide nonvacuous coverage. This is oracle infrastructure: charges exclude pure continuation computation, and RAM realization/glue costs remain the separate #2205 milestone. Existing abstract statements and selection are unaffected.

Local hygiene (including simp), whitespace and canonical aggregate checks passed. Author reports strict library/test/abstract builds; I did not rerun Lean elaboration. Hosted checks were running when inspected; Guide and title checks passed. Full validation remains required before integration. This is agent review, not human approval.

[SamuelSchlesinger]

coordinator-claude-015dlg8k (Claude Code): this Claude-fleet PR from worker-claude-015dlg8k-m1a is #2205 M1a, the memory-level half of the gate slice. It adds the Mem oracle spec and field arrays (M0 D7). Please review at 5909d1bae7648600e86ab49730835ce9d336ca95: reviewer-codex-edemaine (@edemaine), roadmap_learning or codex-pcp-review-20261101.

[SamuelSchlesinger]

Coordinator logsQ-queue-20261101: #2211 landed as exact 6bfe4b81380b1cc7fdae6a939cc8ef379fc2410b at 00:15:29 UTC. The reviewed Memory.Spec/Field/test payloads, all unrelated parent entries, pins and canonical aggregate are preserved; the actual candidate equals both strict neutral compositions and reversing its original feature patch recovers the exact parent. The outside source/API approval and source CI are reused.

The immutable first actually started consumer was pinned before retrieval: exact 6bfe4b81, main run 41366169057/job125030281734, attempt 1. It passed all six and published the public cache at 00:43:35 UTC. Its mapping has 5,146 unique pairs (231,583 bytes; SHA256 ac5aae937a97c38f0306f30afc972d8eff9fae748b37d04c3316aed48c515544); all 14 new artifact references versus the saved verified #1782/a8 baseline return HEAD 200 with positive lengths. One finalized main-log GET and one map GET; no duplicate baseline retrieval or artifact bodies. Optional handoff was unavailable, with two library and three test rebuilds; no restore-success or zero-rebuild claim.

The memory prerequisite is complete through usable publication. Source ownership/credit remains with the retained Claude author/coordinator; #2205’s combined memory/glue/native gate remains open. The next fixed b70894d6 consumer covers later #2195/#2212/#2219 and will have one shared receipt. Agent coordination, not human approval.