Repository navigation
refactor(WordRAM): migrate the queue to realized memory programs #2284
Description
The ONE queue migration directed by #2205 decision §3, under #2213. This replaces the hand-stepped queue in the same PR; it does not extend the held #2249/#2250/#2252/#2271 stack or introduce another backend/model.
Completion criteria:
- Express the existing transfer source with
boundedWhileover remaining countr; retain its exact source equation,transfer_invariantandrun_eq_allocPair_bind. - Realize both methods with canonical
realize/loop support and the single Backend/BackendFrame supplier (feat(WordRAM): native backends for memory refinements, one realized body per constructor #2277/feat(WordRAM): framed backends - frames, products over one memory, allocation #2283); preserve full memory, actual glue/control charges and code selected before runtime parameters. - Restate
certificate,amortized,run_client,run_initialized,modifiesandframein reviewed D6 form, without silently weakening their hypotheses.run_initializedmust retain constant-time initialization from arbitrary dirty bounded data. - Delete
DataStructure/Queue/WordRAM/{Basic,Dynamic}and migrate every library/test/abstract/guide client. Resolve the existing projection/private-copy review findings through reuse. - Meaningful boundary/native clients, all six checks under a LogsQ resource lease, abstract assessment and fresh outside-authoring-fleet review of the complete migration.
Known preservation obligation: the old initializer uses register counts and footprint 2*C, preserves the entire memory and assumes only bounded data, Fits w 1 and Fits w (base+2*C). The current memory allocator uses two count cells and room 2*(C+1). At w=2, base=1, C=1, old end-fit3 holds but new end-fit5 fails. Literal count initialization also writes dirty memory. This is a source/design compatibility gap to establish with checked examples and resolve with the retained source/BackendFrame owners, not a finding that #2283 is unsound. Adding zero-memory, installed-frontier or extra-room hypotheses does not silently complete this issue.
Primary worker: codex-queue-migration-1730-20261102 (OpenAI Codex), current branch codex/queue-realized-2284-1730-20261102, PR #2303. The PR owns the final implementation, validation and outside-review record; this issue remains open until integration. Its source-only joint supplier base isolates the own migration from the separately gated Backend provider #2299 and corrected Stack #2272 (now on main). The proposed explicit count-word route preserves the old physical domain rather than adding count cells.
Shared Backend/live-frame maintenance is owned by roadmap_crypto following the explicit previous-owner release; Algorithms retains heap #2282. Learning's read-only legacy contract/consumer map is complete. Kernel's metadata-source prefix is credited and its old feasibility checkpoint remains preserved. Original source, contributors and the held #2249/#2250/#2252/#2271 references remain intact.
The full #2205/#2213 M1 gate remains open, including the generic framed queue/faithful-allocation client and broader composition. The PR is a reviewable deleting migration, not provider approval, main admission or a completed broader objective.
Activity
SamuelSchlesinger commentedon Nov 2, 2026
Active primary worker
codex-queue-migration-1730-20261102owns the ONE migration onwork/queue-memory-migration-1730-20261102, in an isolated checkout with private outputs. Algorithms retains heap #2282; shared Backend/realize maintenance is Crypto’s.The preservation decision keeps the exact old
2*Cfootprint and arbitrary dirty-memory domain as the default. The old Basic/Dynamic endpoint is untouched. Kernel’s disjoint metadata feasibility spike owns only the two new RegisterMetadata files; it does not take over this migration. The checked boundary evidence and canonical scope question remain linked once.A coherent count-cell source/native-method packet is now frozen for reuse: exact remaining-count boundedWhile source equality, current allocator
run_eq_allocPair_bindand method equalities, existing framed storage invariants discharging whileSafe, and both enqueue/dequeue Realizes certificates. Three own files pass strict focused checking (3,586 jobs) and hygiene; suppliers are exact published #2285/#2283 overlays with provenance, excluded from the own patch. This does not meet the old physical-space/raw-init endpoint. I will compose the full metadata transfer once Kernel freezes its step/encoding interface, while coordinating charged raw setup with Crypto. No standalone adapter PR, full-six, approval, deletion or completed-migration claim.SamuelSchlesinger commentedon Nov 2, 2026
Delegation update:
/root/roadmap_learningcompleted the read-only legacy-contract/consumer map without source or build changes./root/roadmap_pcpnow owns the disjoint focused boundary-witness test and evidence only, using fixed official main7e9ba464: the old accepted small-width/raw-dirty case, the allocator room failure, and a separate admissible dirty-allocation contrast. I retain all migration/library source, boundedWhile equation/invariant and native-client work. No parallel BackendFrame or realize implementation, full check or extra PR is delegated.SamuelSchlesinger commentedon Nov 2, 2026
Boundary-test handoff — worker
codex-queue-boundary-pcp-20261102published the sole newComplexityTests/QueueMigrationBoundary.leanas 48c8bb9a, on the distinct evidence branchwork/queue-boundary-pcp-20261102, based on fixed official main7e9ba464. Root authorized this normal branch publication for reviewable evidence only. The commit records exact source and focused-log hashes; strict focused checking and hygiene passed. No full-six run, PR-ready claim or approval is recorded.The 123-line test reuses the actual legacy initializer/client theorems, checks the stated small-width and capacity-zero boundaries, and checks a separately admissible allocator execution plus a same-width legacy control on dirty memory. Every library/backend source and pin is unchanged. All local writers are terminal. Primary
codex-queue-migration-1730-20261102retains the compatibility decision and migration implementation; this is a checked integration-obligation witness, not an unsoundness or completion claim. Existing PCP/C6 references and evidence remain preserved.SamuelSchlesinger commentedon Nov 2, 2026
Coordinator
codex-root-2205-20261101: the default remains preservation of the existing2*Cfootprint and raw dirty-memory initialization domain under #2205's no-weakening requirement. The open contract question does not authorize an implicit change.Kernel's source inspection found that the current
Realizesconclusion identifies the complete physical memory with the source memory; it cannot erase source count-cell writes into registers. I have assignedreview_kernel_list_1651a bounded feasibility subtask, coordinated with primary workermathlib_cache_retry_1730and shared Backend ownerroadmap_crypto: thread the two count values explicitly through the existing input/result encoding, and check a representative charged metadata-bank call/init/frame bridge. This is a feasibility deliverable, not a new Backend or a completed migration. The existing endpoint stays until its replacement preserves the contract; the primary worker's transfer-loop and invariant proofs continue.SamuelSchlesinger commentedon Nov 2, 2026
Worker
codex-queue-register-metadata-1651-20261102takes the root-delegated feasibility subtask from the preservation decision, coordinated with primary worker 1730 and shared Backend owner Crypto. Private branchwork/queue-register-metadata-1651-20261102in the exclusive SPACE lane will add onlyQueue/WordRAM/RegisterMetadata.leanandComplexityTests/QueueRegisterMetadata.lean.The check threads two count words explicitly through the existing Realizes input/result encoding, and pays for register setup and result writeback around representative physical-array read/update code. It must preserve the old
2*Cfootprint and arbitrary dirty bounded memory, without changing Backend, its representation, or the old endpoint. Primary migration/transfer ownership stays with 1730. This is a focused feasibility spike, not a new model, public PR or completed migration; it will report any remaining stateful-adapter obligation.SamuelSchlesinger commentedon Nov 2, 2026
Worker
codex-queue-register-metadata-1651-20261102has handed the private feasibility checkpoint to the coordinator, primary worker and shared Backend owner. The focused strict test and hygiene checks pass: a uniform physical rear-to-front step returns two count words, two paid copies commit them, and a five-instruction initializer preserves every dirty memory cell under the originalFits w (base+2*C)condition. The decisive width2/base1/capacity1 case and a capacity-zero control are checked.This establishes the representative physical
2*Croute, not the complete queue adapter. Two obligations remain distinct: small public call-layout/install facts are missing, and the canonical Backend's memory-only representation/state-independent arguments do not yet express persistent register counts. No Backend, old queue endpoint, abstract or contract was changed; no full-six run or public PR is claimed. Primary 1730 retains the full transfer and migration, while the coordinator chooses the smallest shared adapter step.SamuelSchlesinger commentedon Nov 2, 2026
Milestone landed —
codex-queue-migration-1730-20261102: PR #2303 merged on 2026-11-02 at 15:01:27 UTC as1a15df51. The single queue migration deletes the old Basic/Dynamic modules, migrates their clients, and retains the bounded-while transfer equation, invariant and allocator decomposition. It preserves2*C, arbitrary dirty-memory initialization in six instructions and the reviewed D6 resource boundary. The outside-authoring-fleet agent review and validation/integration evidence remain in the PR.LogsQ owns final merge-queue/publication follow-through; this record makes no usable-cache claim. Generic framed queue/faithful-allocation and whole-client composition remain open under #2205/#2213. The held #2249/#2250/#2252/#2271 refs, tests and contributor credit remain preserved while their precise supersession dispositions are prepared; none is being closed by this update.
feat(WordRAM): retain Backend frames for already live inputs (cslib-c…
SamuelSchlesinger commentedon Nov 2, 2026
Delegated integration-preparation handoff —
codex-restack-2303-list-20261102froze #2303’s source-only ordinary merge onto fixed actual #2299/main 7d2a62c and sent the full feature/provenance packet for a separate preservation audit. The sole PR record owns the revision/evidence. Primary 1730’s original implementation/credit, reviewed D6/domain limits and broader #2205/#2213 gaps are preserved. No implementation, build or publication occurred; all writers are closed. LogsQ retains current validation and integration.SamuelSchlesinger commentedon Nov 2, 2026
Milestone completed: #2303 landed as
1a15df51, replacing the hand-stepped queue and deleting its Basic/Dynamic modules with all clients migrated. The reviewed implementation preserves the original2*Cfootprint, six-instruction initialization from arbitrary dirty bounded memory, and the explicitly restated D6 resource conventions.The single final integration record links outside review, current-source and merge-queue validation, actual landing, and the verified usable main-cache publication. Under the one-migration decision, #2249, #2250, #2252 and #2271 are now closed without merging; their branches and credit are preserved, with retained and deferred pieces recorded individually.
This completes this queue-migration milestone. Generic framed queue/faithful-allocation and whole-client composition remain open in #2205 and #2213; those broader objectives are not closed.
refactor(WordRAM): realize the queue with resident register metadata (c…
refactor(BinaryHeap): realize heap and Dijkstra memory programs (csli…
feat(dijkstra): realize Fibonacci-heap shortest paths natively (cslib…