feat(WordRAM): native backends for memory refinements, one realized body per constructor by SamuelSchlesinger · Pull Request #2277 · cslib-community/complexitylib

SamuelSchlesinger · 2026-11-02T03:54:45Z

Current integration source 3627325d is based on actual #2260 main. Its product API carries the exact already-reviewed joint invariant J, with both frame premises preserving J; this is a genuine change from the original raw product type. Original outside review, outside J/product-test coverage, and independent exact-source preservation/coverage audit cover the current source. Local focused and all six default gates passed; fresh canonical hosted validation and normal MQ checks remain required before integration. Only the C7 layer is carried, with no BackendFrame feature copy; original Claude credit and the body-only/uncharged-argument limits remain. Selected abstracts are unaffected.

worker-claude-015dlg8k-adapter (Claude Code, Opus). C7 on #2205: the generic per-constructor adapter that the stack migration (#2272) wrote by hand. It sits beside C2's kernel and changes none of its definitions.

Change

Realization.Backend generalizes MemoryBackend to any Refinement D (Memory.spec w). A Certificate bundles one Realizes with its program, encodings, domain and work. A family C : ι → Certificate B over a finite tag type fixes one register file, one body per tag and one exchange factor, all before every width, refinement, layout and argument. A Backend D C gives each operation a tag, the arg of the tag's program (it may include the runtime layout) and an answer map from the program's result to D.Result o. Backend.Implements S R asks that each method be the selected program with its result mapped by answer, and that admissible states satisfy the program's domain with word-sized arguments. From that:
- Backend.implementation: a StateTransitionImpl D with a functional rep (invariant, abstraction, word bounds);
- Backend.amortized: from R.Amortized Memory.charge upper Φ plus work ≤ c, an Amortized certificate with charge factor * (upper + c + 1) and potential factor * Φ;
- Backend.bound: with zero potential, a Bound; a constant upper gives one constant for every width and layout;
- Backend.sum / Implements.prod: products dispatch on the Sum constructor through ι ⊕ ι' tags, with no native dispatcher;
- exec_memoryState, data/rep_data (a calling-convention state holding a memory) and fits_appendWords.
Label encoding (reviewer-4's point on feat(WordRAM): derive global and framed implementation certificates #2245): the result encoding belongs to the tag, not to the label. The stack's push answers () with zero result words, so its value is never echoed. answer reads the specified result. This matches the reviewer's suggested shape and feat(WordRAM): observe uniform native method answers #2267's uniform carrier.
Realizes.uniformComputableInPolyTime (Realization/Function.lean): one certificate plus an input layout, an entry width and a polynomial bound on memory charge plus work give UniformComputableInPolyTime. Installation and the halt are charged. Stack.Controller.positive_polytime goes from 35 lines to 9.
Width: totalCost_width, clientHistory_width and memoryCost_eq_totalCost: memory charges do not depend on the word width.

Demonstration

ComplexityTests/WordRAMRealizationBackend.lean instantiates the backend on the array stack: three tags, push/pop/size certificates from #2246, correctness from Stack.Memory.refinement, the constant bound from Stack.Memory.amortized, a product of two stacks, and a doubling function via the polytime corollary.

The drop-in rewrite of #2272's Stack/Native.lean is in the coordinator's scratch, not in this PR (tmp/worker-adapter/stack-2272/, with a README listing its statement changes against #2272). It goes from 392 to 181 lines. The register plumbing (slots, scratch layout, argument delivery, decoding and the per-operation proof) is gone. What remains is the instance (tags, certificates, backend, and implements, whose content is the stack's entry fits; about 55 lines) and the public API #2272 re-derives (run_client, modifies, frame, the initial state). It builds with all of #2272 (--wfail, library and tests) on a local merge.

Base and limitations

Based on actual feat(WordRAM): realize tactic for memory-client realizations #2260 main (feat/ram-realize-tactic). feat(WordRAM): realize tactic for memory-client realizations #2260 hasn't merged feat(WordRAM): realize runtime-layout memory-stack methods #2246's latest head 383a52021 yet, so this branch merges it. That merge needed a two-line fix in feat(WordRAM): realize tactic for memory-client realizations #2260's Realizes.iterate₀ (Absorb.lean), because iterateRuntime now destructures its argument. Most of the diff outside the three new files comes from that merge.
As in MemoryBackend, argument installation and answer decoding are uncharged, and bounds count the body only. Bodies are chosen by classical choice from the certificates. Tags must form a Fintype.
For codex-ram-realization-c2-20261101, proposals only, nothing in C2 is changed: the width lemmas and fits_appendWords could move beside runClient_width/appendWords in Basic.lean; MemoryBackend is the instance D = Memory.spec w, R = Refinement.id and could be re-derived from Backend; Result.lean's private runClient_result would help clients state Implements.run with a non-identity answer.

Existing notions considered: MemoryBackend (the special case, left unchanged), Realizes.toStateTransitionImpl and the framed SubroutineBase adapters with one native emitter (#2245, #2267), #2273's native Sum dispatcher, Module.realize (host-side glue is free there), Refinement.Amortized.realize, StateTransitionImpl.ofFn, Bound.exists_executes_const, Realizes.exists_init_program, inputPrefix_exec, UniformComputableInPolyTime.of_code, and runClient_width/clientResult_width/clientState_width. No new execution semantics or judgment: exec is Exec of the selected body from the prepared data. parallel_defs.py finds no parallel definitions.

Validation

At fb0bf0941: lake build --wfail Complexity ComplexityTests ComplexityAbstracts, lake lint, lake exe mk_all --check, lake exe lint-style, lake exe checkInitImports, check_hygiene.py --check-simp, check_tidy_surface.py, check_changed_files.py --base #2260.

AI assistance

Written by Claude Code (Opus) as worker-claude-015dlg8k-adapter. Needs outside-fleet review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

…eld arrays Memory.spec w is the memory oracle of #2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

…ions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

…inements Amortized.mono and Amortized.mul_left (exchange at a constant rate, #2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

…t, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

…structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

….elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

The M1 slice of #2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone #2210; the memory realization kernel and vertical-slice gate remain in #2205. Validation: final staged tree a1b88e3 passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending.

…m-realization-c2-20261101

Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of #2213 under #2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved.

Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under #2213 and #2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged.

Project the four fixed memory-query bodies into the existing semantic StateTransitionImpl interface with explicit delivered-argument preparation and body-only cost bounds. Derive existing framed WordRAM implementations from a semantic module, one global emitter and local initialization/ABI/footprint conditions. Runtime argument maps do not choose a new emitter per object. Combined cost keeps explicit local-work grading, bind/loop equations and a scaled-potential inequality. A native local one-cell ADT and a query-free-loop counterexample check the intended boundary. Faithful full queue initialization and its complete framed/native-client transfer remain open under #2213/#2205. No curated abstract changes or native clock from memory-only costs are claimed. AI-assisted authoring: memory backend by learning-memory-backend-2213-20261101; grading by crypto-realization-grade-2213-20261101; local client by c2-mem-primitives-1730-20261101; adapters/integration by codex-ram-realization-c2-20261101. All new public API needs outside-fleet review.

Stage multiword results from fixed scalar-glue witnesses, charging every coordinate and output copy. Faithful Option words use a tag and unshifted payload, retaining maximum-word values and zero-width none. Consume the unchanged published Stack.Memory methods over full runtime layout words. Native size/push/pop certificates keep explicit validity/invariant/fit conditions and local work 0/10/19. One selected pop emitter handles empty and maximum-word inputs while preserving memory and live registers. This is a bounded #2213/#2205 milestone. The framed queue and faithful allocated queue-client path remain open. No abstract selection or headline changes. AI-assisted authoring: GlueVector by Kernel work/c2-runtime-loop-2213-1651; stack consumer by learning-memory-stack-2213-20261101; integration by codex-ram-realization-c2-20261101. Source M1a 412ad/2218 is unchanged and credited through ordinary prerequisite history. Outside-fleet review remains required.

Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact.

…m-memory-stack-c2-20261101

Address outside review5731265464. Move the exact stack-independent arithmetic and Option rules to public Realizes helpers in GlueVector, remove client copies and reuse appendWords. Infer the actual five-step push composition without typed intermediate certificates; final layouts/indices/domain remain visible. Statement meanings, clocks, source methods and tests are preserved. Codex authoring by roadmap_learning; integration/self-review by roadmap_algorithms. Ordinary parent merge carries2230a929 fix. Both guarded worker packets retained; strict integrated3564 and hygiene pass. Fullsix and fresh outside delta review follow at the frozen updated revision. No selected abstract impact or broader M1 completion claim.

Add `realize`, which proves `Realizes B p input output safe work` for a loop-free memory client by walking its syntax: bind, pure, the four memory queries, `if` on a word comparison and `match` on an optional answer. It keeps the argument layout itself, certifies each `pure` by a syntax-directed `GlueComputable` proof, states intermediate domains in the client's terms and leaves the genuine fit and domain conditions as goals. `Realization/Absorb.lean` adds the derived rules it targets: constant local work is absorbed by the exchange factor (`Realizes.mono_mul`), giving `bind₀`, `branch₀` and `pure₀`, plus `Realizes.congr` and the `WordEncoding` class for intermediate answers. Refs #2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Generalize `Realizes.mono_mul` to local work dominated by the memory charge, and add `Realizes.iterate₀`: a runtime-bounded loop whose body begins with a query has local work `0`, since that query pays each iteration's control unit. `iterate_comap` moves the loop's argument into its step, and `iterationSafe_true` closes trivial loop domains. `realize` now certifies `iterate`, pairs of words, and reports query-free loop bodies. Refs #2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Add `blockWords` and its `WordEncoding` instance, so binds may return blocks and layouts. `realize` certifies a client that allocates a stack, pushes and pops; `exists_init_program` turns it into a flat exact-basis program that outputs the encoding of `some v` from `State.init [c, v]` within a constant number of steps, with no hand-stepped instruction. Deduplicate repeated conditions only within an identical local context. Refs #2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

… proof Merge actual main 8fbc928, preserving every unrelated main entry. Reuse the exact iterate₀ proof-only adaptation already reviewed at fb0bf09 (#2277, review5731981270); public types and all other #2260 feature payloads are unchanged. Original Claude source authorship is retained. Private checkpoint for root/LogsQ audit; validation pending.

SamuelSchlesinger · 2026-11-02T08:02:05Z

Published handoff complete — worker codex-bpl-restack2277-20261102 has no remaining source writer or local producer. LogsQ normally published 3627325d2 on the original branch, using PCP’s independent preservation and dual-review-coverage approval; #2277 subsequently landed as e5930ab7. My focused checks, hygiene and default all-six passed on the frozen source. Claude’s original credit and both outside review scopes are retained. LogsQ owns the remaining integration/publication evidence; I will not retrieve hosted logs or change the canonical branch.

Ordinary parents are approved fb0bf09 and actual #2260 ffd94d9. Preserve every unrelated main entry, pin, credit and canonical import. Retain the already-fulfilled fb0 Absorb proof on main and main's authorized WordRAMRealize wrapper expansion. Backend and its product test use only the exact cached joint-J variant explicitly covered by outside review5732383062; Function remains raw fb0, covered by review5731981270. The public J API delta from raw fb0 is explicit; no BackendFrame feature is imported. Source-origin, complete feature forward/inverse and canonical inventory checks pass. No Lean/kernel, focused or full-six validation is claimed here. Claude's original mathematical/source credit is retained; Codex only prepares the independently reviewed source carry and ordinary actual-main composition.

SamuelSchlesinger · 2026-11-02T08:55:56Z

Qualified preservation/coverage PASS — coordinator codex-pcp-coordinator-preservation-2277-20261102, separate non-author context; I did not author or brief this repair/restack. Audited exact 3627325d2bb98db93e2c58e7acefbdee5e035a55 / tree b6398a9c, ordinary parents [raw fb0bf094, actual ffd94d9e].

The product API genuinely changes from raw fb0: it takes joint invariant J, both frame premises preserve J, and the right entry projects the nested component invariant. I verified the exact cached product doc/type/proof span inside outside-reviewed ed43a2c2, plus the entire adapted test’s exact mode/blob. Review 5732383062 explicitly covers that base J/product-test adaptation; original review 5731981270 covers the remaining raw C7 layer. This reuses those substantive verdicts; it is no new math approval/count and does not claim the raw API is unchanged.

Independent forward/inverse recovery gives exactly three added payloads and the original two imports. Function is exact raw; Backend is exactly the covered cached variant; no BackendFrame feature is copied. All 5,374 unrelated main entries, pins/credit/docs/abstracts and 3,925 canonical imports are preserved. Main Absorb already equals fb0 and stays untouched; the unowned main enqueue-wrapper fix also stays exact.

The delegated-review exception applies to the mechanical restack/composition of these already-covered sources. BPL’s exact-head final validation records all six PASS, focused/hygiene PASS and a clean source. LogsQ verified normal FF publication on the original branch and retarget to main at 08:57:05 UTC on November 2; official source/tree remain exact. Fresh native CI 41416791776 and Guide are active; canonical validation and actual tested-context readiness remain LogsQ’s gates. Original Claude credit and body-only/uncharged-argument scope remain. I ran no build and retrieved no CI/cache logs or artifacts.

SamuelSchlesinger · 2026-11-02T09:06:58Z

Coordinator codex-logsq-1671: #2277 landed as e5930ab7 from 3627325d. Fresh source CI, Guide and the exact actual MQ checkout pass. Both strict physical compositions, reviewed payloads, unrelated prefix entries/pins and complete feature reversal pass.

The product API adds joint invariant J, as explicitly covered by outside review of the exact J/product-test variant, together with original C7 approval and independent dual-coverage preservation. This reuses those verdicts without a new math approval count. Original credit and body-only/uncharged-argument limits remain; BackendFrame and new live-register facts have separate PRs.

The pinned first started main consumer passes all six and published a usable cache: 5,253 unique mappings and all four new references available. Optional handoff reuse was unavailable; it rebuilt two library and three test modules. One saved log/map audit is retained for reuse, with zero artifact-body downloads. Broader #2205 stays open.

Ordinary parents are documentation child19fe13ca and fixed actual #2277 e5930ab. Replay the exact outside-reviewed cac0-to-ed43 six-file feature and only the independently checked two-comment clarification child. Main Backend matches the full reviewed cac0 preimage before the exact ed43 override; all unowned Absorb/tactic/wrapper fixes remain actual-main bytes. Literal complete feature/doc forward and inverse, all entry origins, pins, source credit and canonical inventory checks pass. No new proof or API repair, #2298/#2294 helper copy, Lean build or full-six claim. Retain the fixed finite family / separately charged raw argument-installation limits. Original Claude mathematical/source credit and Codex reused-source credit remain in their existing file headers and documentation.

* feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of cslib-community#2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (cslib-community#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): weaken and rescale amortized refinements Amortized.mono and Amortized.mul_left (exchange at a constant rate, cslib-community#2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): make Refinement.Amortized a structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: array stack over memory and queue method lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Foundations): affine cost bounds are O(size) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: queue over memory Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): product answer types via Sum.elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): queue over two array stacks over the memory oracle The M1 slice of cslib-community#2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): certify compositional register-word glue Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone cslib-community#2210; the memory realization kernel and vertical-slice gate remain in cslib-community#2205. Validation: final staged tree a1b88e3 passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending. * feat(WordRAM): realize memory queries with uniform bind and glue Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of cslib-community#2213 under cslib-community#2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved. * fix(WordRAM): normalize the memory return simp rule * feat(WordRAM): realize bounded loops and initialized client programs Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under cslib-community#2213 and cslib-community#2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged. * feat(WordRAM): derive global and framed implementation certificates Project the four fixed memory-query bodies into the existing semantic StateTransitionImpl interface with explicit delivered-argument preparation and body-only cost bounds. Derive existing framed WordRAM implementations from a semantic module, one global emitter and local initialization/ABI/footprint conditions. Runtime argument maps do not choose a new emitter per object. Combined cost keeps explicit local-work grading, bind/loop equations and a scaled-potential inequality. A native local one-cell ADT and a query-free-loop counterexample check the intended boundary. Faithful full queue initialization and its complete framed/native-client transfer remain open under cslib-community#2213/cslib-community#2205. No curated abstract changes or native clock from memory-only costs are claimed. AI-assisted authoring: memory backend by learning-memory-backend-2213-20261101; grading by crypto-realization-grade-2213-20261101; local client by c2-mem-primitives-1730-20261101; adapters/integration by codex-ram-realization-c2-20261101. All new public API needs outside-fleet review. * feat(WordRAM): realize runtime-layout memory-stack methods Stage multiword results from fixed scalar-glue witnesses, charging every coordinate and output copy. Faithful Option words use a tag and unshifted payload, retaining maximum-word values and zero-width none. Consume the unchanged published Stack.Memory methods over full runtime layout words. Native size/push/pop certificates keep explicit validity/invariant/fit conditions and local work 0/10/19. One selected pop emitter handles empty and maximum-word inputs while preserving memory and live registers. This is a bounded cslib-community#2213/cslib-community#2205 milestone. The framed queue and faithful allocated queue-client path remain open. No abstract selection or headline changes. AI-assisted authoring: GlueVector by Kernel work/c2-runtime-loop-2213-1651; stack consumer by learning-memory-stack-2213-20261101; integration by codex-ram-realization-c2-20261101. Source M1a 412ad/2218 is unchanged and credited through ordinary prerequisite history. Outside-fleet review remains required. * refactor(WordRAM): centralize realization history and word encodings Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact. * feat(WordRAM): realize tactic for memory-client realizations Add `realize`, which proves `Realizes B p input output safe work` for a loop-free memory client by walking its syntax: bind, pure, the four memory queries, `if` on a word comparison and `match` on an optional answer. It keeps the argument layout itself, certifies each `pure` by a syntax-directed `GlueComputable` proof, states intermediate domains in the client's terms and leaves the genuine fit and domain conditions as goals. `Realization/Absorb.lean` adds the derived rules it targets: constant local work is absorbed by the exchange factor (`Realizes.mono_mul`), giving `bind₀`, `branch₀` and `pure₀`, plus `Realizes.congr` and the `WordEncoding` class for intermediate answers. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): loops whose body issues a query in realize Generalize `Realizes.mono_mul` to local work dominated by the memory charge, and add `Realizes.iterate₀`: a runtime-bounded loop whose body begins with a query has local work `0`, since that query pays each iteration's control unit. `iterate_comap` moves the loop's argument into its step, and `iterationSafe_true` closes trivial loop domains. `realize` now certifies `iterate`, pairs of words, and reports query-free loop bodies. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a whole stack client to a flat program via realize Add `blockWords` and its `WordEncoding` instance, so binds may return blocks and layouts. `realize` certifies a client that allocates a stack, pushes and pops; `exists_init_program` turns it into a flat exact-basis program that outputs the encoding of `some v` from `State.init [c, v]` within a constant number of steps, with no hand-stepped instruction. Deduplicate repeated conditions only within an identical local context. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): realize measure-bounded early-exit while loops Add a finite Memory.Prog while representation and one uniform native Code.loop certificate. A source cutoff depends only on explicit initial input; reached-state rank and safety prove truncation is unreachable. Charge actual continuing bodies/control and initial/final guard overhead, including query-free loops; retain potential in the semantic cost telescope. Reuse existing Realizes, Cond, native loop rules and copyBank without a new language or judgment. Default scripts/check.sh all six gates and focused strict library/test checks pass on exact staged tree 2e3c80c, two threads. No selected abstract impact. Refs cslib-community#2259 and cslib-community#2205; the broader gate and heap migration remain open. AI assistance: Codex worker codex-c5-while-1651-20261102 under coordinator delegation; independent outside review is required. * perf(WordRAM): state realize certificates per form in the client's terms `realize` compared its synthesized domain with the composed rules' domain once, at the end, by definitional unfolding. The rules' domain holds the interpreter's runs `clientResult`/`clientState` of every earlier client, nested, and unreduced pair projections, so that check grew steeply with the client: 212k heartbeats for the stack controller, and 2.5M when a bind's first client ends in a `match`. Each form's certificate is now stated for the client as written, with its domain in the client's terms (`certify`), so certificates compose syntactically and the kernel checks each form's agreement locally. A bind's continuation domain is stated at the first client's reply and next memory in closed form (`Realizes.bind₀_of_run`). Result encodings are proved by `Fin.cases` with one `rfl` per coordinate instead of `fin_cases <;> rfl`, and operands are first looked up syntactically among the live words. Adds two performance guards to the tests: a client whose binds begin with a `match`-ending client, and the stack controller in one call. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate the aggregate import after merging cslib-community#2270 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): state iterate₀ in iterateRuntime's named-component form cslib-community#2230 restates iterateRuntime with pattern lambdas over ((d, a), fuel) and appendWords; iterate₀ follows, which also removes its positional projections (cslib-community#1764). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): guarded loops in realize realize now certifies boundedWhile G step D n a whose step begins with a query. The guard is a word comparison (a = b, a < b, a > b, or a ≠ 0 tested as 0 < a) over the live and state words, with any decidability instance; an operand independent of the state is computed before the loop, and the cutoff stays a ghost bound. The certificate is transported back to the client's guard, step and environment, so the loop's domain is whileSafe in the client's terms, under the loop's valid history, ready for whileSafe_of_measure. New leaf Realization/WhileAbsorb: boundedWhile_congr, whileSafe_imp/congr, whileWork_congr (guard, body and environment congruence), the envelope whileWork_le, whileWork_zero_le and the absorbed rule Realizes.while₀. Absorb gains Realizes.consequence_valid. Tests: a memory-reading countdown (also with r ≠ 0 under a classical instance), the queue's transfer over two array stacks counted down by the items left, and a sift-shaped descent with logarithmic rank, plus controls. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(WordRAM): wrap a long line in the realize loop tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(WordRAM): use appendWords for the stack client's environments cslib-community#2230 makes appendWords public in Realization.Basic; the stack client's private append was a copy of it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): keep iterate₀'s statement, as in cslib-community#2277's proof-only repair The proof body alone needs the change for cslib-community#2230's iterateRuntime. Keeping the statement byte-identical to cslib-community#2277 lets the two branches merge without conflict. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a heartbeat budget for the realize transfer loop Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): place the transfer loop's heartbeat budget before its docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a realize loop whose guard and step capture the environment Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…lib-community#2272) * feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of cslib-community#2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (cslib-community#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): weaken and rescale amortized refinements Amortized.mono and Amortized.mul_left (exchange at a constant rate, cslib-community#2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): make Refinement.Amortized a structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: array stack over memory and queue method lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Foundations): affine cost bounds are O(size) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: queue over memory Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): product answer types via Sum.elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): queue over two array stacks over the memory oracle The M1 slice of cslib-community#2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): certify compositional register-word glue Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone cslib-community#2210; the memory realization kernel and vertical-slice gate remain in cslib-community#2205. Validation: final staged tree a1b88e3 passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending. * feat(WordRAM): realize memory queries with uniform bind and glue Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of cslib-community#2213 under cslib-community#2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved. * fix(WordRAM): normalize the memory return simp rule * feat(WordRAM): realize bounded loops and initialized client programs Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under cslib-community#2213 and cslib-community#2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged. * feat(WordRAM): derive global and framed implementation certificates Project the four fixed memory-query bodies into the existing semantic StateTransitionImpl interface with explicit delivered-argument preparation and body-only cost bounds. Derive existing framed WordRAM implementations from a semantic module, one global emitter and local initialization/ABI/footprint conditions. Runtime argument maps do not choose a new emitter per object. Combined cost keeps explicit local-work grading, bind/loop equations and a scaled-potential inequality. A native local one-cell ADT and a query-free-loop counterexample check the intended boundary. Faithful full queue initialization and its complete framed/native-client transfer remain open under cslib-community#2213/cslib-community#2205. No curated abstract changes or native clock from memory-only costs are claimed. AI-assisted authoring: memory backend by learning-memory-backend-2213-20261101; grading by crypto-realization-grade-2213-20261101; local client by c2-mem-primitives-1730-20261101; adapters/integration by codex-ram-realization-c2-20261101. All new public API needs outside-fleet review. * feat(WordRAM): realize runtime-layout memory-stack methods Stage multiword results from fixed scalar-glue witnesses, charging every coordinate and output copy. Faithful Option words use a tag and unshifted payload, retaining maximum-word values and zero-width none. Consume the unchanged published Stack.Memory methods over full runtime layout words. Native size/push/pop certificates keep explicit validity/invariant/fit conditions and local work 0/10/19. One selected pop emitter handles empty and maximum-word inputs while preserving memory and live registers. This is a bounded cslib-community#2213/cslib-community#2205 milestone. The framed queue and faithful allocated queue-client path remain open. No abstract selection or headline changes. AI-assisted authoring: GlueVector by Kernel work/c2-runtime-loop-2213-1651; stack consumer by learning-memory-stack-2213-20261101; integration by codex-ram-realization-c2-20261101. Source M1a 412ad/2218 is unchanged and credited through ordinary prerequisite history. Outside-fleet review remains required. * refactor(WordRAM): centralize realization history and word encodings Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact. * refactor(WordRAM): expose shared glue rules and infer stack push Address outside review5731265464. Move the exact stack-independent arithmetic and Option rules to public Realizes helpers in GlueVector, remove client copies and reuse appendWords. Infer the actual five-step push composition without typed intermediate certificates; final layouts/indices/domain remain visible. Statement meanings, clocks, source methods and tests are preserved. Codex authoring by roadmap_learning; integration/self-review by roadmap_algorithms. Ordinary parent merge carries2230a929 fix. Both guarded worker packets retained; strict integrated3564 and hygiene pass. Fullsix and fresh outside delta review follow at the frozen updated revision. No selected abstract impact or broader M1 completion claim. * feat(WordRAM): realize tactic for memory-client realizations Add `realize`, which proves `Realizes B p input output safe work` for a loop-free memory client by walking its syntax: bind, pure, the four memory queries, `if` on a word comparison and `match` on an optional answer. It keeps the argument layout itself, certifies each `pure` by a syntax-directed `GlueComputable` proof, states intermediate domains in the client's terms and leaves the genuine fit and domain conditions as goals. `Realization/Absorb.lean` adds the derived rules it targets: constant local work is absorbed by the exchange factor (`Realizes.mono_mul`), giving `bind₀`, `branch₀` and `pure₀`, plus `Realizes.congr` and the `WordEncoding` class for intermediate answers. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): loops whose body issues a query in realize Generalize `Realizes.mono_mul` to local work dominated by the memory charge, and add `Realizes.iterate₀`: a runtime-bounded loop whose body begins with a query has local work `0`, since that query pays each iteration's control unit. `iterate_comap` moves the loop's argument into its step, and `iterationSafe_true` closes trivial loop domains. `realize` now certifies `iterate`, pairs of words, and reports query-free loop bodies. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a whole stack client to a flat program via realize Add `blockWords` and its `WordEncoding` instance, so binds may return blocks and layouts. `realize` certifies a client that allocates a stack, pushes and pops; `exists_init_program` turns it into a flat exact-basis program that outputs the encoding of `some v` from `State.init [c, v]` within a constant number of steps, with no hand-stepped instruction. Deduplicate repeated conditions only within an identical local context. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(Stack): migrate the stack to its realized implementation Delete the hand-stepped `Stack/WordRAM/{Basic,Controller}` and re-derive their statements from `Stack.Memory`, C2's `MemoryStack.realizes_*` and `realize`: - `Stack.Spec`: the bounded stack, moved from `Stack.WordRAM.spec`. - `Stack.Native`: the native stack from the realized methods, with `instruction_bound`, `run_client`, `modifies`, `frame` and `initial_rep` restated with one existential per-operation constant. - `Stack.Controller`: the adaptive client as a memory program, linked to the abstract client, certified by `realize`; `positive_polytime` is unchanged. - Chan–He traversal keeps the stepped dispatcher it uses as `Traversal.WordStack` (push and nonempty pop, exact counts unchanged). - The controller and dynamic-program tests move to the exchange cell. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): destructure the loop argument in Realizes.iterate₀ cslib-community#2246's iterateRuntime now binds its argument by a destructuring lambda, so iterate₀ matches the components before omega. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): native backends for memory refinements, one realized body per constructor Realization.Backend generalizes MemoryBackend: from a Refinement D (Memory.spec w) and one Realizes certificate per operation tag it builds a StateTransitionImpl D with a functional representation, amortized and constant instruction bounds, and side-by-side products over Sum tags. Results are encoded per tag; an answer map reads the specified answer, so arguments are never echoed. Realizes.uniformComputableInPolyTime projects a realization to a flat program, charging argument installation and the halt. totalCost_width and memoryCost_eq_totalCost state that memory charges do not depend on the width. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(tests): wrap long lines in the backend test Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): Backend.data, rep_data and fits_appendWords Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): backend test uses fits_appendWords and Backend.data Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(Stack): run the native stack on Realization.Backend Adopts worker-claude-015dlg8k-adapter's drop-in for cslib-community#2277: Stack.Native instantiates Realization.Backend with one certificate per operation constructor, and Controller.positive_polytime comes from Realizes.uniformComputableInPolyTime. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * perf(WordRAM): state realize certificates per form in the client's terms `realize` compared its synthesized domain with the composed rules' domain once, at the end, by definitional unfolding. The rules' domain holds the interpreter's runs `clientResult`/`clientState` of every earlier client, nested, and unreduced pair projections, so that check grew steeply with the client: 212k heartbeats for the stack controller, and 2.5M when a bind's first client ends in a `match`. Each form's certificate is now stated for the client as written, with its domain in the client's terms (`certify`), so certificates compose syntactically and the kernel checks each form's agreement locally. A bind's continuation domain is stated at the first client's reply and next memory in closed form (`Realizes.bind₀_of_run`). Result encodings are proved by `Fin.cases` with one `rfl` per coordinate instead of `fin_cases <;> rfl`, and operands are first looked up syntactically among the live words. Adds two performance guards to the tests: a client whose binds begin with a `match`-ending client, and the stack controller in one call. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(Stack): keep only consumed native API; fold the traversal word stack into TraversalStack Stack.Native keeps the backend, implementation and instruction_bound. run_client, modifies, frame and the initial state had no consumer; the backend test derives each from Bound.exists_executes_const, Backend.exec_memoryState with Stack.Memory.modifies_methods, and Backend.rep_data. The backend test now uses Stack.Native instead of its own copy, and absorbs DataStructureStack. Traversal.WordStack moves into TraversalStack.lean, its only importer, unchanged. Stack.Controller uses memoryCost_eq_totalCost and drops unused imports. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(Stack): realize the controller in one call With cslib-community#2280, realize certifies the whole controller program directly, so the split through realizes_alloc, realizes_run and Realizes.bind goes. positive_polytime reads the conjuncts of program_spec by projection and normalizes the result encoding by simp instead of by unfolding. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * perf(Stack): simplify only the controller's side goals The side goals after realize need no hypothesis rewriting; simp on the goal alone saves about 0.15 s and three simp arguments. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * Fix Stack migration name resolution and framed proof view Append only to frozen cslib-community#2272 head97bd. Explicitly qualify Doubling's eighty Memory.spec references shadowed by the relocated bounded Stack.spec, keeping the original7bf memory oracle and all programs, hypotheses and resources. Wrap four newly long lines. Controller gives the existing amortized certificate its definitionally equal refinement view before .client. No public lemma, definition, capacity premise, program or bound is added. Strict focused Doubling/Controller and all selected Dynamic/Backend/Framed/ Chan-He regressions pass (6506 jobs); global and changed hygiene pass. Complete repair-patch forward/inverse and all unrelated entries/pins/docs are exact. Full-six and independent delta review remain before publication. Original Claude migration authorship and source credits are retained. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…slib-community#2303) * feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of cslib-community#2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (cslib-community#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): weaken and rescale amortized refinements Amortized.mono and Amortized.mul_left (exchange at a constant rate, cslib-community#2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): make Refinement.Amortized a structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: array stack over memory and queue method lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Foundations): affine cost bounds are O(size) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: queue over memory Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): product answer types via Sum.elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): queue over two array stacks over the memory oracle The M1 slice of cslib-community#2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): certify compositional register-word glue Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone cslib-community#2210; the memory realization kernel and vertical-slice gate remain in cslib-community#2205. Validation: final staged tree a1b88e3 passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending. * feat(WordRAM): realize memory queries with uniform bind and glue Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of cslib-community#2213 under cslib-community#2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved. * fix(WordRAM): normalize the memory return simp rule * feat(WordRAM): realize bounded loops and initialized client programs Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under cslib-community#2213 and cslib-community#2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged. * feat(WordRAM): derive global and framed implementation certificates Project the four fixed memory-query bodies into the existing semantic StateTransitionImpl interface with explicit delivered-argument preparation and body-only cost bounds. Derive existing framed WordRAM implementations from a semantic module, one global emitter and local initialization/ABI/footprint conditions. Runtime argument maps do not choose a new emitter per object. Combined cost keeps explicit local-work grading, bind/loop equations and a scaled-potential inequality. A native local one-cell ADT and a query-free-loop counterexample check the intended boundary. Faithful full queue initialization and its complete framed/native-client transfer remain open under cslib-community#2213/cslib-community#2205. No curated abstract changes or native clock from memory-only costs are claimed. AI-assisted authoring: memory backend by learning-memory-backend-2213-20261101; grading by crypto-realization-grade-2213-20261101; local client by c2-mem-primitives-1730-20261101; adapters/integration by codex-ram-realization-c2-20261101. All new public API needs outside-fleet review. * feat(WordRAM): realize runtime-layout memory-stack methods Stage multiword results from fixed scalar-glue witnesses, charging every coordinate and output copy. Faithful Option words use a tag and unshifted payload, retaining maximum-word values and zero-width none. Consume the unchanged published Stack.Memory methods over full runtime layout words. Native size/push/pop certificates keep explicit validity/invariant/fit conditions and local work 0/10/19. One selected pop emitter handles empty and maximum-word inputs while preserving memory and live registers. This is a bounded cslib-community#2213/cslib-community#2205 milestone. The framed queue and faithful allocated queue-client path remain open. No abstract selection or headline changes. AI-assisted authoring: GlueVector by Kernel work/c2-runtime-loop-2213-1651; stack consumer by learning-memory-stack-2213-20261101; integration by codex-ram-realization-c2-20261101. Source M1a 412ad/2218 is unchanged and credited through ordinary prerequisite history. Outside-fleet review remains required. * refactor(WordRAM): centralize realization history and word encodings Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact. * refactor(WordRAM): expose shared glue rules and infer stack push Address outside review5731265464. Move the exact stack-independent arithmetic and Option rules to public Realizes helpers in GlueVector, remove client copies and reuse appendWords. Infer the actual five-step push composition without typed intermediate certificates; final layouts/indices/domain remain visible. Statement meanings, clocks, source methods and tests are preserved. Codex authoring by roadmap_learning; integration/self-review by roadmap_algorithms. Ordinary parent merge carries2230a929 fix. Both guarded worker packets retained; strict integrated3564 and hygiene pass. Fullsix and fresh outside delta review follow at the frozen updated revision. No selected abstract impact or broader M1 completion claim. * feat(WordRAM): realize tactic for memory-client realizations Add `realize`, which proves `Realizes B p input output safe work` for a loop-free memory client by walking its syntax: bind, pure, the four memory queries, `if` on a word comparison and `match` on an optional answer. It keeps the argument layout itself, certifies each `pure` by a syntax-directed `GlueComputable` proof, states intermediate domains in the client's terms and leaves the genuine fit and domain conditions as goals. `Realization/Absorb.lean` adds the derived rules it targets: constant local work is absorbed by the exchange factor (`Realizes.mono_mul`), giving `bind₀`, `branch₀` and `pure₀`, plus `Realizes.congr` and the `WordEncoding` class for intermediate answers. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): loops whose body issues a query in realize Generalize `Realizes.mono_mul` to local work dominated by the memory charge, and add `Realizes.iterate₀`: a runtime-bounded loop whose body begins with a query has local work `0`, since that query pays each iteration's control unit. `iterate_comap` moves the loop's argument into its step, and `iterationSafe_true` closes trivial loop domains. `realize` now certifies `iterate`, pairs of words, and reports query-free loop bodies. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a whole stack client to a flat program via realize Add `blockWords` and its `WordEncoding` instance, so binds may return blocks and layouts. `realize` certifies a client that allocates a stack, pushes and pops; `exists_init_program` turns it into a flat exact-basis program that outputs the encoding of `some v` from `State.init [c, v]` within a constant number of steps, with no hand-stepped instruction. Deduplicate repeated conditions only within an identical local context. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(Stack): migrate the stack to its realized implementation Delete the hand-stepped `Stack/WordRAM/{Basic,Controller}` and re-derive their statements from `Stack.Memory`, C2's `MemoryStack.realizes_*` and `realize`: - `Stack.Spec`: the bounded stack, moved from `Stack.WordRAM.spec`. - `Stack.Native`: the native stack from the realized methods, with `instruction_bound`, `run_client`, `modifies`, `frame` and `initial_rep` restated with one existential per-operation constant. - `Stack.Controller`: the adaptive client as a memory program, linked to the abstract client, certified by `realize`; `positive_polytime` is unchanged. - Chan–He traversal keeps the stepped dispatcher it uses as `Traversal.WordStack` (push and nonempty pop, exact counts unchanged). - The controller and dynamic-program tests move to the exchange cell. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): destructure the loop argument in Realizes.iterate₀ cslib-community#2246's iterateRuntime now binds its argument by a destructuring lambda, so iterate₀ matches the components before omega. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): native backends for memory refinements, one realized body per constructor Realization.Backend generalizes MemoryBackend: from a Refinement D (Memory.spec w) and one Realizes certificate per operation tag it builds a StateTransitionImpl D with a functional representation, amortized and constant instruction bounds, and side-by-side products over Sum tags. Results are encoded per tag; an answer map reads the specified answer, so arguments are never echoed. Realizes.uniformComputableInPolyTime projects a realization to a flat program, charging argument installation and the halt. totalCost_width and memoryCost_eq_totalCost state that memory charges do not depend on the width. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(tests): wrap long lines in the backend test Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): Backend.data, rep_data and fits_appendWords Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): backend test uses fits_appendWords and Backend.data Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(Stack): run the native stack on Realization.Backend Adopts worker-claude-015dlg8k-adapter's drop-in for cslib-community#2277: Stack.Native instantiates Realization.Backend with one certificate per operation constructor, and Controller.positive_polytime comes from Realizes.uniformComputableInPolyTime. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * perf(WordRAM): state realize certificates per form in the client's terms `realize` compared its synthesized domain with the composed rules' domain once, at the end, by definitional unfolding. The rules' domain holds the interpreter's runs `clientResult`/`clientState` of every earlier client, nested, and unreduced pair projections, so that check grew steeply with the client: 212k heartbeats for the stack controller, and 2.5M when a bind's first client ends in a `match`. Each form's certificate is now stated for the client as written, with its domain in the client's terms (`certify`), so certificates compose syntactically and the kernel checks each form's agreement locally. A bind's continuation domain is stated at the first client's reply and next memory in closed form (`Realizes.bind₀_of_run`). Result encodings are proved by `Fin.cases` with one `rfl` per coordinate instead of `fin_cases <;> rfl`, and operands are first looked up syntactically among the live words. Adds two performance guards to the tests: a client whose binds begin with a `match`-ending client, and the stack controller in one call. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(Stack): keep only consumed native API; fold the traversal word stack into TraversalStack Stack.Native keeps the backend, implementation and instruction_bound. run_client, modifies, frame and the initial state had no consumer; the backend test derives each from Bound.exists_executes_const, Backend.exec_memoryState with Stack.Memory.modifies_methods, and Backend.rep_data. The backend test now uses Stack.Native instead of its own copy, and absorbs DataStructureStack. Traversal.WordStack moves into TraversalStack.lean, its only importer, unchanged. Stack.Controller uses memoryCost_eq_totalCost and drops unused imports. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(Stack): realize the controller in one call With cslib-community#2280, realize certifies the whole controller program directly, so the split through realizes_alloc, realizes_run and Realizes.bind goes. positive_polytime reads the conjuncts of program_spec by projection and normalizes the result encoding by simp instead of by unfolding. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * perf(Stack): simplify only the controller's side goals The side goals after realize need no hypothesis rewriting; simp on the goal alone saves about 0.15 s and three simp arguments. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: drop imports the merge duplicated in Complexity.lean Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): framed backends - frames, products over one memory, allocation A backend of a framed refinement carries its frame over: a native operation writes only the footprint and the reserved room (Backend.modifies), and keeps disjoint assertions and structures kept apart (frame_heap, frame). Backends of framed refinements run their product over one memory (Implements.prod_framed), each side within its own region (modifies_inl, modifies_inr). Backend.Allocation names the tag that runs a Memory.Allocator's program; Allocation.exec allocates from arbitrary bounded data within the allocator's cost, writing only the room it takes. Backend.extend adds such tags; install and exists_exec run any tag's body. The memory side is a new leaf, Memory/Region. The stack test restores modifies/frame, constant-time allocation and allocate-then-run, and two stacks over one memory. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): allocate a pair of stacks in one body realizes_allocTwo certifies the allocation of two stacks, one after the other, as Memory.Allocator.prod does; with Backend.extend it becomes the allocation tag of the pair's backend, and allocate_pair sets up both empty stacks from arbitrary bounded data in constant time. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): retain Backend register frames for live-input execution Expose existing shared packing facts and install identity under actual live words; derive a full-frame execution result and raw-live corollary from the same Realizes code_spec. Existing definitions and all previous theorem types are unchanged; exists_exec projects the stronger proof. Tests exercise different result widths, paid zero staging, zero/max-word inputs and a genuine memory-read provider. Under cslib-community#2298 for queue cslib-community#2284 and heap cslib-community#2282; inherited Claude source credit retained. Strict focused3628 and hygiene pass; full-six/outside review pending. * fix(WordRAM): expose Backend extension and preparation metadata Expose only the existing pure extend record and prepare alias so real heap bounds and conditional already-live entry elaborate without local record copies or dependent observation wrappers. All definition bodies/types, code/arg/rep/resource meanings are unchanged. Generic bound_extend and actual-live operation-entry regressions pass with the old clients; full new-head validation/review pending under cslib-community#2298. * Fix Stack migration name resolution and framed proof view Append only to frozen cslib-community#2272 head97bd. Explicitly qualify Doubling's eighty Memory.spec references shadowed by the relocated bounded Stack.spec, keeping the original7bf memory oracle and all programs, hypotheses and resources. Wrap four newly long lines. Controller gives the existing amortized certificate its definitionally equal refinement view before .client. No public lemma, definition, capacity premise, program or bound is added. Strict focused Doubling/Controller and all selected Dynamic/Backend/Framed/ Chan-He regressions pass (6506 jobs); global and changed hygiene pass. Complete repair-patch forward/inverse and all unrelated entries/pins/docs are exact. Full-six and independent delta review remain before publication. Original Claude migration authorship and source credits are retained. * refactor(WordRAM): realize the queue with resident register metadata Use Memory.Prog, boundedWhile, Realizes and one fixed Backend family with actual native tag dispatch and paid count writeback. Preserve the original 2*C reservation, Fits1/end-fit domain, arbitrary dirty bounded initialization in six register instructions, typed FIFO observations, adaptive execution and heap frame. Remove old Basic/Dynamic and superseded prototypes; migrate every client and retain the source transfer equation/invariant/allocator decomposition. Static shared R/F replace the hand program's literal register and instruction constants: call charge4F+6 and terminal potential2F*rear include control, commit and halt. The external client controller/delivery boundary remains; generic framed allocation/composition and the full2205 objective are not completed. Default scripts/check.sh all six PASS at exact staged tree37b5dee43327761897a6c152ef3246de13d12ca0, plus eight strict focused queue targets, imports and hygiene. Parent is the private ordinary joint0abe of public2299/73 and2272/fc; supplier review/actual/current-context gates remain separate. This own layer changes exactly21 paths. Source credit Samuel Schlesinger retained. OpenAI Codex assisted implementation, proofs, tests and source-preserving integration; Kernel's exact metadata-source prefix is reused with its contribution credited and old feasibility refs preserved. Shared providers retain their original authors through parent history. Refs cslib-community#2284; broader cslib-community#2205/cslib-community#2213 remain open. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

* feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of cslib-community#2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (cslib-community#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): weaken and rescale amortized refinements Amortized.mono and Amortized.mul_left (exchange at a constant rate, cslib-community#2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): make Refinement.Amortized a structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: array stack over memory and queue method lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Foundations): affine cost bounds are O(size) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: queue over memory Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): product answer types via Sum.elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): queue over two array stacks over the memory oracle The M1 slice of cslib-community#2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): certify compositional register-word glue Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone cslib-community#2210; the memory realization kernel and vertical-slice gate remain in cslib-community#2205. Validation: final staged tree a1b88e3 passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending. * feat(WordRAM): realize memory queries with uniform bind and glue Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of cslib-community#2213 under cslib-community#2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved. * fix(WordRAM): normalize the memory return simp rule * feat(WordRAM): realize bounded loops and initialized client programs Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under cslib-community#2213 and cslib-community#2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged. * feat(WordRAM): derive global and framed implementation certificates Project the four fixed memory-query bodies into the existing semantic StateTransitionImpl interface with explicit delivered-argument preparation and body-only cost bounds. Derive existing framed WordRAM implementations from a semantic module, one global emitter and local initialization/ABI/footprint conditions. Runtime argument maps do not choose a new emitter per object. Combined cost keeps explicit local-work grading, bind/loop equations and a scaled-potential inequality. A native local one-cell ADT and a query-free-loop counterexample check the intended boundary. Faithful full queue initialization and its complete framed/native-client transfer remain open under cslib-community#2213/cslib-community#2205. No curated abstract changes or native clock from memory-only costs are claimed. AI-assisted authoring: memory backend by learning-memory-backend-2213-20261101; grading by crypto-realization-grade-2213-20261101; local client by c2-mem-primitives-1730-20261101; adapters/integration by codex-ram-realization-c2-20261101. All new public API needs outside-fleet review. * feat(WordRAM): realize runtime-layout memory-stack methods Stage multiword results from fixed scalar-glue witnesses, charging every coordinate and output copy. Faithful Option words use a tag and unshifted payload, retaining maximum-word values and zero-width none. Consume the unchanged published Stack.Memory methods over full runtime layout words. Native size/push/pop certificates keep explicit validity/invariant/fit conditions and local work 0/10/19. One selected pop emitter handles empty and maximum-word inputs while preserving memory and live registers. This is a bounded cslib-community#2213/cslib-community#2205 milestone. The framed queue and faithful allocated queue-client path remain open. No abstract selection or headline changes. AI-assisted authoring: GlueVector by Kernel work/c2-runtime-loop-2213-1651; stack consumer by learning-memory-stack-2213-20261101; integration by codex-ram-realization-c2-20261101. Source M1a 412ad/2218 is unchanged and credited through ordinary prerequisite history. Outside-fleet review remains required. * refactor(WordRAM): centralize realization history and word encodings Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact. * feat(WordRAM): realize tactic for memory-client realizations Add `realize`, which proves `Realizes B p input output safe work` for a loop-free memory client by walking its syntax: bind, pure, the four memory queries, `if` on a word comparison and `match` on an optional answer. It keeps the argument layout itself, certifies each `pure` by a syntax-directed `GlueComputable` proof, states intermediate domains in the client's terms and leaves the genuine fit and domain conditions as goals. `Realization/Absorb.lean` adds the derived rules it targets: constant local work is absorbed by the exchange factor (`Realizes.mono_mul`), giving `bind₀`, `branch₀` and `pure₀`, plus `Realizes.congr` and the `WordEncoding` class for intermediate answers. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): loops whose body issues a query in realize Generalize `Realizes.mono_mul` to local work dominated by the memory charge, and add `Realizes.iterate₀`: a runtime-bounded loop whose body begins with a query has local work `0`, since that query pays each iteration's control unit. `iterate_comap` moves the loop's argument into its step, and `iterationSafe_true` closes trivial loop domains. `realize` now certifies `iterate`, pairs of words, and reports query-free loop bodies. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a whole stack client to a flat program via realize Add `blockWords` and its `WordEncoding` instance, so binds may return blocks and layouts. `realize` certifies a client that allocates a stack, pushes and pops; `exists_init_program` turns it into a flat exact-basis program that outputs the encoding of `some v` from `State.init [c, v]` within a constant number of steps, with no hand-stepped instruction. Deduplicate repeated conditions only within an identical local context. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): realize measure-bounded early-exit while loops Add a finite Memory.Prog while representation and one uniform native Code.loop certificate. A source cutoff depends only on explicit initial input; reached-state rank and safety prove truncation is unreachable. Charge actual continuing bodies/control and initial/final guard overhead, including query-free loops; retain potential in the semantic cost telescope. Reuse existing Realizes, Cond, native loop rules and copyBank without a new language or judgment. Default scripts/check.sh all six gates and focused strict library/test checks pass on exact staged tree 2e3c80c, two threads. No selected abstract impact. Refs cslib-community#2259 and cslib-community#2205; the broader gate and heap migration remain open. AI assistance: Codex worker codex-c5-while-1651-20261102 under coordinator delegation; independent outside review is required. * perf(WordRAM): state realize certificates per form in the client's terms `realize` compared its synthesized domain with the composed rules' domain once, at the end, by definitional unfolding. The rules' domain holds the interpreter's runs `clientResult`/`clientState` of every earlier client, nested, and unreduced pair projections, so that check grew steeply with the client: 212k heartbeats for the stack controller, and 2.5M when a bind's first client ends in a `match`. Each form's certificate is now stated for the client as written, with its domain in the client's terms (`certify`), so certificates compose syntactically and the kernel checks each form's agreement locally. A bind's continuation domain is stated at the first client's reply and next memory in closed form (`Realizes.bind₀_of_run`). Result encodings are proved by `Fin.cases` with one `rfl` per coordinate instead of `fin_cases <;> rfl`, and operands are first looked up syntactically among the live words. Adds two performance guards to the tests: a client whose binds begin with a `match`-ending client, and the stack controller in one call. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: regenerate the aggregate import after merging cslib-community#2270 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): state iterate₀ in iterateRuntime's named-component form cslib-community#2230 restates iterateRuntime with pattern lambdas over ((d, a), fuel) and appendWords; iterate₀ follows, which also removes its positional projections (cslib-community#1764). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): guarded loops in realize realize now certifies boundedWhile G step D n a whose step begins with a query. The guard is a word comparison (a = b, a < b, a > b, or a ≠ 0 tested as 0 < a) over the live and state words, with any decidability instance; an operand independent of the state is computed before the loop, and the cutoff stays a ghost bound. The certificate is transported back to the client's guard, step and environment, so the loop's domain is whileSafe in the client's terms, under the loop's valid history, ready for whileSafe_of_measure. New leaf Realization/WhileAbsorb: boundedWhile_congr, whileSafe_imp/congr, whileWork_congr (guard, body and environment congruence), the envelope whileWork_le, whileWork_zero_le and the absorbed rule Realizes.while₀. Absorb gains Realizes.consequence_valid. Tests: a memory-reading countdown (also with r ≠ 0 under a classical instance), the queue's transfer over two array stacks counted down by the items left, and a sift-shaped descent with logarithmic rank, plus controls. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(WordRAM): wrap a long line in the realize loop tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(WordRAM): use appendWords for the stack client's environments cslib-community#2230 makes appendWords public in Realization.Basic; the stack client's private append was a copy of it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): keep iterate₀'s statement, as in cslib-community#2277's proof-only repair The proof body alone needs the change for cslib-community#2230's iterateRuntime. Keeping the statement byte-identical to cslib-community#2277 lets the two branches merge without conflict. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a heartbeat budget for the realize transfer loop Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): place the transfer loop's heartbeat budget before its docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a realize loop whose guard and step capture the environment Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip(WordRAM): freeze option-pair implementation during gated repair Private checkpoint for cslib-community#2291. Initial focused option clients pass; extended legacy-normalization and native-budget tests currently fail and remain to be repaired. Not a submission or validation claim. * fix(WordRAM): preserve scalar encoding normal form in generic option support Keep the legacy OptionNat embedding and instance, connect it to the shared payload embedding, and check same-body none/max-payload executions. Focused pair/legacy clients passed3586 before the added definitional-instance guard; no full validation or public submission yet. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…slib-community#2300) * feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of cslib-community#2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (cslib-community#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): weaken and rescale amortized refinements Amortized.mono and Amortized.mul_left (exchange at a constant rate, cslib-community#2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): make Refinement.Amortized a structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: array stack over memory and queue method lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Foundations): affine cost bounds are O(size) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: queue over memory Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): product answer types via Sum.elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): queue over two array stacks over the memory oracle The M1 slice of cslib-community#2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): certify compositional register-word glue Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone cslib-community#2210; the memory realization kernel and vertical-slice gate remain in cslib-community#2205. Validation: final staged tree a1b88e3 passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending. * feat(WordRAM): realize memory queries with uniform bind and glue Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of cslib-community#2213 under cslib-community#2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved. * fix(WordRAM): normalize the memory return simp rule * feat(WordRAM): realize bounded loops and initialized client programs Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under cslib-community#2213 and cslib-community#2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged. * feat(WordRAM): derive global and framed implementation certificates Project the four fixed memory-query bodies into the existing semantic StateTransitionImpl interface with explicit delivered-argument preparation and body-only cost bounds. Derive existing framed WordRAM implementations from a semantic module, one global emitter and local initialization/ABI/footprint conditions. Runtime argument maps do not choose a new emitter per object. Combined cost keeps explicit local-work grading, bind/loop equations and a scaled-potential inequality. A native local one-cell ADT and a query-free-loop counterexample check the intended boundary. Faithful full queue initialization and its complete framed/native-client transfer remain open under cslib-community#2213/cslib-community#2205. No curated abstract changes or native clock from memory-only costs are claimed. AI-assisted authoring: memory backend by learning-memory-backend-2213-20261101; grading by crypto-realization-grade-2213-20261101; local client by c2-mem-primitives-1730-20261101; adapters/integration by codex-ram-realization-c2-20261101. All new public API needs outside-fleet review. * feat(WordRAM): realize runtime-layout memory-stack methods Stage multiword results from fixed scalar-glue witnesses, charging every coordinate and output copy. Faithful Option words use a tag and unshifted payload, retaining maximum-word values and zero-width none. Consume the unchanged published Stack.Memory methods over full runtime layout words. Native size/push/pop certificates keep explicit validity/invariant/fit conditions and local work 0/10/19. One selected pop emitter handles empty and maximum-word inputs while preserving memory and live registers. This is a bounded cslib-community#2213/cslib-community#2205 milestone. The framed queue and faithful allocated queue-client path remain open. No abstract selection or headline changes. AI-assisted authoring: GlueVector by Kernel work/c2-runtime-loop-2213-1651; stack consumer by learning-memory-stack-2213-20261101; integration by codex-ram-realization-c2-20261101. Source M1a 412ad/2218 is unchanged and credited through ordinary prerequisite history. Outside-fleet review remains required. * refactor(WordRAM): centralize realization history and word encodings Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact. * refactor(WordRAM): expose shared glue rules and infer stack push Address outside review5731265464. Move the exact stack-independent arithmetic and Option rules to public Realizes helpers in GlueVector, remove client copies and reuse appendWords. Infer the actual five-step push composition without typed intermediate certificates; final layouts/indices/domain remain visible. Statement meanings, clocks, source methods and tests are preserved. Codex authoring by roadmap_learning; integration/self-review by roadmap_algorithms. Ordinary parent merge carries2230a929 fix. Both guarded worker packets retained; strict integrated3564 and hygiene pass. Fullsix and fresh outside delta review follow at the frozen updated revision. No selected abstract impact or broader M1 completion claim. * feat(WordRAM): realize tactic for memory-client realizations Add `realize`, which proves `Realizes B p input output safe work` for a loop-free memory client by walking its syntax: bind, pure, the four memory queries, `if` on a word comparison and `match` on an optional answer. It keeps the argument layout itself, certifies each `pure` by a syntax-directed `GlueComputable` proof, states intermediate domains in the client's terms and leaves the genuine fit and domain conditions as goals. `Realization/Absorb.lean` adds the derived rules it targets: constant local work is absorbed by the exchange factor (`Realizes.mono_mul`), giving `bind₀`, `branch₀` and `pure₀`, plus `Realizes.congr` and the `WordEncoding` class for intermediate answers. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): loops whose body issues a query in realize Generalize `Realizes.mono_mul` to local work dominated by the memory charge, and add `Realizes.iterate₀`: a runtime-bounded loop whose body begins with a query has local work `0`, since that query pays each iteration's control unit. `iterate_comap` moves the loop's argument into its step, and `iterationSafe_true` closes trivial loop domains. `realize` now certifies `iterate`, pairs of words, and reports query-free loop bodies. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a whole stack client to a flat program via realize Add `blockWords` and its `WordEncoding` instance, so binds may return blocks and layouts. `realize` certifies a client that allocates a stack, pushes and pops; `exists_init_program` turns it into a flat exact-basis program that outputs the encoding of `some v` from `State.init [c, v]` within a constant number of steps, with no hand-stepped instruction. Deduplicate repeated conditions only within an identical local context. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): extract the static input reindex leaf Copy the exact existing Realization/Reindex.lean from PR2249 at66650221 onto fixed PR2246/383a52021, avoiding old queue-client dependencies for C5/C6. Original Gitblob18aea578f32743c7f03563931e54f08e111d1728, SHA25646541639a7334403b7dd5b325ca129e4162a433bf02981b2ca258a609496f165. Keep the original Samuel/Codex header, public API, proof and credit unchanged. Add its canonical aggregate import and an actual native read/frame test: select the second environment word, return maxword15, preserve unused7, the entire memory and frontier, with unchanged query charge. Worker codex-reindex-leaf-learning-20261102 under root/Algorithms cslib-community#2266, cslib-community#2213/cslib-community#2205. This removes a concrete C5/C6 dependency blockage; it is not a broader realization/migration endpoint or an approval of the existing API. No selected abstract/catalogue/rendering impact; pins and docs unchanged. Validation: all six default scripts/check.sh gates PASS,2threads, exact frozen content; focused strict leaf/native test3536 and hygiene PASS. Fresh outside-authoring-fleet API/correctness review is required and will be shared by2249/C5/C6. No original parent refs are modified by this layer. AI assistance: OpenAI Codex for extraction, regression and validation. * feat(WordRAM): realize measure-bounded early-exit while loops Add a finite Memory.Prog while representation and one uniform native Code.loop certificate. A source cutoff depends only on explicit initial input; reached-state rank and safety prove truncation is unreachable. Charge actual continuing bodies/control and initial/final guard overhead, including query-free loops; retain potential in the semantic cost telescope. Reuse existing Realizes, Cond, native loop rules and copyBank without a new language or judgment. Default scripts/check.sh all six gates and focused strict library/test checks pass on exact staged tree 2e3c80c, two threads. No selected abstract impact. Refs cslib-community#2259 and cslib-community#2205; the broader gate and heap migration remain open. AI assistance: Codex worker codex-c5-while-1651-20261102 under coordinator delegation; independent outside review is required. * fix(WordRAM): destructure the loop argument in Realizes.iterate₀ cslib-community#2246's iterateRuntime now binds its argument by a destructuring lambda, so iterate₀ matches the components before omega. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): native backends for memory refinements, one realized body per constructor Realization.Backend generalizes MemoryBackend: from a Refinement D (Memory.spec w) and one Realizes certificate per operation tag it builds a StateTransitionImpl D with a functional representation, amortized and constant instruction bounds, and side-by-side products over Sum tags. Results are encoded per tag; an answer map reads the specified answer, so arguments are never echoed. Realizes.uniformComputableInPolyTime projects a realization to a flat program, charging argument installation and the halt. totalCost_width and memoryCost_eq_totalCost state that memory charges do not depend on the width. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(tests): wrap long lines in the backend test Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): Backend.data, rep_data and fits_appendWords Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): backend test uses fits_appendWords and Backend.data Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * perf(WordRAM): state realize certificates per form in the client's terms `realize` compared its synthesized domain with the composed rules' domain once, at the end, by definitional unfolding. The rules' domain holds the interpreter's runs `clientResult`/`clientState` of every earlier client, nested, and unreduced pair projections, so that check grew steeply with the client: 212k heartbeats for the stack controller, and 2.5M when a bind's first client ends in a `match`. Each form's certificate is now stated for the client as written, with its domain in the client's terms (`certify`), so certificates compose syntactically and the kernel checks each form's agreement locally. A bind's continuation domain is stated at the first client's reply and next memory in closed form (`Realizes.bind₀_of_run`). Result encodings are proved by `Fin.cases` with one `rfl` per coordinate instead of `fin_cases <;> rfl`, and operands are first looked up syntactically among the live words. Adds two performance guards to the tests: a client whose binds begin with a `match`-ending client, and the stack controller in one call. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): export initialized flat programs with a standard layout Choose private canonical frontier/input/scratch banks once and project an existing Realizes certificate through the actual charged Data.init prefix, Code.program and halt. The stateful export retains the actual flat Runs, full source memory/frontier and every encoded result word; the scalar Executes corollary removes caller register-layout proofs. Its fixed code, output placement, halt PC and factor precede every runtime width/input. Keep the same raw-layout, length, fit, safe-domain and admissibility premises and C*(memoryCost+work+1)+1 bound. Empty input still requires frontier one to fit; no initialized width-zero case is claimed. The checked initialized-copy client block drops48 to20 lines with its statement unchanged. An actual write/read client checks full post-memory and maximum payload15; the empty-input case retains positive frontier fit. The original Program.lean and all its public interfaces remain exact SHAeeb7346b2d483bede91259eb6f03f50b7b494a735c264a2293e993bf0d800db2. Existing Program/native-prefix source credit remains unchanged. Worker codex-c5-canonical-program-learning-20261102 under root/Algorithms cslib-community#2279, cslib-community#2205/cslib-community#2213, fixed published2230/a929a76f. This is a bounded C5 usability milestone, not a new compiler/language/model or broad completion. Static Fin l observation retains the existing scalar-output scope; zero-output Unit exports remain separate. No selected abstract impact. All six default scripts/check.sh gates PASS,2threads, exact frozen source; strict focused3546, hygiene/check-simp/whitespace and source/pin guards PASS. Fresh outside-author-fleet correctness/API review is required. No own approval or parent source/ref changes. AI assistance: OpenAI Codex. * chore: regenerate the aggregate import after merging cslib-community#2270 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: drop imports the merge duplicated in Complexity.lean Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): state iterate₀ in iterateRuntime's named-component form cslib-community#2230 restates iterateRuntime with pattern lambdas over ((d, a), fuel) and appendWords; iterate₀ follows, which also removes its positional projections (cslib-community#1764). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): framed backends - frames, products over one memory, allocation A backend of a framed refinement carries its frame over: a native operation writes only the footprint and the reserved room (Backend.modifies), and keeps disjoint assertions and structures kept apart (frame_heap, frame). Backends of framed refinements run their product over one memory (Implements.prod_framed), each side within its own region (modifies_inl, modifies_inr). Backend.Allocation names the tag that runs a Memory.Allocator's program; Allocation.exec allocates from arbitrary bounded data within the allocator's cost, writing only the room it takes. Backend.extend adds such tags; install and exists_exec run any tag's body. The memory side is a new leaf, Memory/Region. The stack test restores modifies/frame, constant-time allocation and allocate-then-run, and two stacks over one memory. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): allocate a pair of stacks in one body realizes_allocTwo certifies the allocation of two stacks, one after the other, as Memory.Allocator.prod does; with Backend.extend it becomes the allocation tag of the pair's backend, and allocate_pair sets up both empty stacks from arbitrary bounded data in constant time. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): guarded loops in realize realize now certifies boundedWhile G step D n a whose step begins with a query. The guard is a word comparison (a = b, a < b, a > b, or a ≠ 0 tested as 0 < a) over the live and state words, with any decidability instance; an operand independent of the state is computed before the loop, and the cutoff stays a ghost bound. The certificate is transported back to the client's guard, step and environment, so the loop's domain is whileSafe in the client's terms, under the loop's valid history, ready for whileSafe_of_measure. New leaf Realization/WhileAbsorb: boundedWhile_congr, whileSafe_imp/congr, whileWork_congr (guard, body and environment congruence), the envelope whileWork_le, whileWork_zero_le and the absorbed rule Realizes.while₀. Absorb gains Realizes.consequence_valid. Tests: a memory-reading countdown (also with r ≠ 0 under a classical instance), the queue's transfer over two array stacks counted down by the items left, and a sift-shaped descent with logarithmic rank, plus controls. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(WordRAM): wrap a long line in the realize loop tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(WordRAM): use appendWords for the stack client's environments cslib-community#2230 makes appendWords public in Realization.Basic; the stack client's private append was a copy of it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): keep iterate₀'s statement, as in cslib-community#2277's proof-only repair The proof body alone needs the change for cslib-community#2230's iterateRuntime. Keeping the statement byte-identical to cslib-community#2277 lets the two branches merge without conflict. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a heartbeat budget for the realize transfer loop Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): place the transfer loop's heartbeat budget before its docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a realize loop whose guard and step capture the environment Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): export fixed programs over independent raw memory Generalize the existing canonical initialized whole-state export so raw input words vary after the program, register layout and exchange factor are chosen. The pointwise input-prefix equation relates them to the faithfully encoded argument. Preserve both existing theorem statements as wrappers. The Dijkstra consumer checks one program over every adjacency-list encode with Unit register arguments, plus two different graph memories and a maximum fitting edge weight. Original Program.lean, dependency pins and abstract catalogue are unchanged. All six default scripts/check.sh gates pass at exact tree36ae8037ff716ea9e1c58187285caf3848e0127e (2 threads); focused3572 and hygiene pass. AI assistance: OpenAI Codex, session codex-dijkstra-native-learning-20261102. Refs cslib-community#2281, cslib-community#2288. * wip(WordRAM): freeze option-pair implementation during gated repair Private checkpoint for cslib-community#2291. Initial focused option clients pass; extended legacy-normalization and native-budget tests currently fail and remain to be repaired. Not a submission or validation claim. * fix(WordRAM): preserve scalar encoding normal form in generic option support Keep the legacy OptionNat embedding and instance, connect it to the shared payload embedding, and check same-body none/max-payload executions. Focused pair/legacy clients passed3586 before the added definitional-instance guard; no full validation or public submission yet. * feat(WordRAM): reuse static method certificates and linked runs Add call-site dispatch through existing Realizes.reindex and a small full-run linking congruence leaf. Tests cover opaque uncurried calls, reached-state domains, charged arithmetic staging and complete adaptive memory histories. Original realize/while suites pass unchanged. All six default checks pass at exact tree0b27a9790e6718825abdaf686f3849fff918c002, session7009/2threads; focused3590/2036 and hygiene pass. Known consumer gap: curried functions wrapped in a tuple lambda still need constructor-skeleton matching before publication. This is not the native Dijkstra endpoint. No abstract, pin, original Program or Reindex changes. AI assistance: OpenAI Codex, codex-dijkstra-native-learning-20261102. Refs cslib-community#2288. * fix(WordRAM): match packaged curried method calls Build only pair and dependent-pair argument skeletons before matching a local uniform Realizes certificate. Keep other argument values undetermined until the source call fixes them, and retain the static live-word wiring and zero-work policy. The actual original Memory.siftDown call with a runtime Sigma layout now passes a direct kernel check without unfolding recursion. Production regressions cover curried scalar calls and an opaque curried optional-pair extraction. Original realize/while and optional-word clients pass unchanged. All six default checks pass at exact tree441c917c2daaf4f6dcdf0b4aca2fc326ad7220bc (session35315,2threads), in the ordinary merged public2294 context; strict focused3596/hygiene also pass. Earlier7675 validation covers only its own older tree. No abstract/pin/model changes. AI assistance: OpenAI Codex, codex-dijkstra-native-learning-20261102. Refs cslib-community#2288. * chore(WordRAM): canonicalize supplier import order Source-only composition of original2288 supplier head73704c97, published2268/b32e8357,2281/1e77082f and2294/2eb7dc04. No owned2297 call/link payload is included. Canonical import order matches the all-six-validated current composition with LinkCongr absent; pending supplier correctness/API/integration gates remain separate. AI assistance: OpenAI Codex, codex-dijkstra-call-link-learning-20261102. * fix(realize): match dependent method arguments after charged staging Solve same-head call arguments in binder order, retaining static live-word wiring and reached-state domains. Add the dependent scalar/pair staging regression from the original heap extraction consumer. Validation: default scripts/check.sh, LEAN_NUM_THREADS=2, all six gates pass at tree 3ee50d4 (session46520). Original curried/OptionPair/realize tests and actual heap extraction scalar/pair staging pass. Abstract assessment: no selected statements or scope changed. AI-assisted by OpenAI Codex. Part of cslib-community#2297; the broader native Dijkstra endpoint remains cslib-community#2288. * fix(realize): scope tactic syntax to WordRAM Delegate codex-realize-scope-crypto-20261102 under cslib-community#2297/cslib-community#2300. Preserve the complete inherited elaborator body and all other source entries. A private import no longer activates realize outside Cslib.WordRAM; both namespace and scoped opens activate it. Validation: strict six-target focused build, session 82324, passed 3646 jobs; targeted hygiene and whitespace checks passed. New parser rejection and positive read-certificate regressions pass; unchanged R1/While/Framed/Call/OptionPair suites pass. Exact original-source no-output probe confirms the old global availability. No default full-six or public update is claimed. Original Samuel Schlesinger source credit is retained. AI assistance: OpenAI Codex. * doc(realize): explain scoped method calls and full-run transport Add the authorized reader path to automation.md: exact import and scope activation, local zero-work certificates, live-word reindexing, charged computed-argument staging and domains at the actual reached memory. Link the existing complete scope/call clients rather than copying Lean. Add the short LinkCongr reference in memory-specifications.md, retaining its complete answer/state/history premise and separate native-cost task. The landed Standard section remains verbatim; no other manual changes. Manual impact: update the Algorithm/Operator's Manual API/proof guidance. No Agent Operator's Manual edit: roles, human direction, delegation, review and handoff procedures are unchanged. No selected abstract or catalogue statement/scope/rendering impact. Original code/API/source credit is retained with all five reviewed payloads exact. Both documented Python checks and all37 controls pass; whitespace passes. Documented private PDF build/freshness and affected-page review follow on this clean frozen child, recorded in the final handoff. No Lean build or new-context native validation is claimed. Outside source approval6579489405 is reused; independent source/doc carry review remains required. AI assistance: OpenAI Codex, codex-2300-actual-std-bpl-20261102, authored this bounded documentation child under LogsQ; no canonical publication, source/API repair or queue action is included. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…#2323) * feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of cslib-community#2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (cslib-community#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): weaken and rescale amortized refinements Amortized.mono and Amortized.mul_left (exchange at a constant rate, cslib-community#2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): make Refinement.Amortized a structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: array stack over memory and queue method lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Foundations): affine cost bounds are O(size) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: queue over memory Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): product answer types via Sum.elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): queue over two array stacks over the memory oracle The M1 slice of cslib-community#2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): certify compositional register-word glue Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone cslib-community#2210; the memory realization kernel and vertical-slice gate remain in cslib-community#2205. Validation: final staged tree a1b88e3 passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending. * feat(WordRAM): realize memory queries with uniform bind and glue Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of cslib-community#2213 under cslib-community#2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved. * fix(WordRAM): normalize the memory return simp rule * feat(WordRAM): realize bounded loops and initialized client programs Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under cslib-community#2213 and cslib-community#2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged. * feat(WordRAM): derive global and framed implementation certificates Project the four fixed memory-query bodies into the existing semantic StateTransitionImpl interface with explicit delivered-argument preparation and body-only cost bounds. Derive existing framed WordRAM implementations from a semantic module, one global emitter and local initialization/ABI/footprint conditions. Runtime argument maps do not choose a new emitter per object. Combined cost keeps explicit local-work grading, bind/loop equations and a scaled-potential inequality. A native local one-cell ADT and a query-free-loop counterexample check the intended boundary. Faithful full queue initialization and its complete framed/native-client transfer remain open under cslib-community#2213/cslib-community#2205. No curated abstract changes or native clock from memory-only costs are claimed. AI-assisted authoring: memory backend by learning-memory-backend-2213-20261101; grading by crypto-realization-grade-2213-20261101; local client by c2-mem-primitives-1730-20261101; adapters/integration by codex-ram-realization-c2-20261101. All new public API needs outside-fleet review. * feat(WordRAM): realize runtime-layout memory-stack methods Stage multiword results from fixed scalar-glue witnesses, charging every coordinate and output copy. Faithful Option words use a tag and unshifted payload, retaining maximum-word values and zero-width none. Consume the unchanged published Stack.Memory methods over full runtime layout words. Native size/push/pop certificates keep explicit validity/invariant/fit conditions and local work 0/10/19. One selected pop emitter handles empty and maximum-word inputs while preserving memory and live registers. This is a bounded cslib-community#2213/cslib-community#2205 milestone. The framed queue and faithful allocated queue-client path remain open. No abstract selection or headline changes. AI-assisted authoring: GlueVector by Kernel work/c2-runtime-loop-2213-1651; stack consumer by learning-memory-stack-2213-20261101; integration by codex-ram-realization-c2-20261101. Source M1a 412ad/2218 is unchanged and credited through ordinary prerequisite history. Outside-fleet review remains required. * refactor(WordRAM): centralize realization history and word encodings Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact. * refactor(WordRAM): expose shared glue rules and infer stack push Address outside review5731265464. Move the exact stack-independent arithmetic and Option rules to public Realizes helpers in GlueVector, remove client copies and reuse appendWords. Infer the actual five-step push composition without typed intermediate certificates; final layouts/indices/domain remain visible. Statement meanings, clocks, source methods and tests are preserved. Codex authoring by roadmap_learning; integration/self-review by roadmap_algorithms. Ordinary parent merge carries2230a929 fix. Both guarded worker packets retained; strict integrated3564 and hygiene pass. Fullsix and fresh outside delta review follow at the frozen updated revision. No selected abstract impact or broader M1 completion claim. * feat(WordRAM): realize tactic for memory-client realizations Add `realize`, which proves `Realizes B p input output safe work` for a loop-free memory client by walking its syntax: bind, pure, the four memory queries, `if` on a word comparison and `match` on an optional answer. It keeps the argument layout itself, certifies each `pure` by a syntax-directed `GlueComputable` proof, states intermediate domains in the client's terms and leaves the genuine fit and domain conditions as goals. `Realization/Absorb.lean` adds the derived rules it targets: constant local work is absorbed by the exchange factor (`Realizes.mono_mul`), giving `bind₀`, `branch₀` and `pure₀`, plus `Realizes.congr` and the `WordEncoding` class for intermediate answers. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): loops whose body issues a query in realize Generalize `Realizes.mono_mul` to local work dominated by the memory charge, and add `Realizes.iterate₀`: a runtime-bounded loop whose body begins with a query has local work `0`, since that query pays each iteration's control unit. `iterate_comap` moves the loop's argument into its step, and `iterationSafe_true` closes trivial loop domains. `realize` now certifies `iterate`, pairs of words, and reports query-free loop bodies. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a whole stack client to a flat program via realize Add `blockWords` and its `WordEncoding` instance, so binds may return blocks and layouts. `realize` certifies a client that allocates a stack, pushes and pops; `exists_init_program` turns it into a flat exact-basis program that outputs the encoding of `some v` from `State.init [c, v]` within a constant number of steps, with no hand-stepped instruction. Deduplicate repeated conditions only within an identical local context. Refs cslib-community#2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): extract the static input reindex leaf Copy the exact existing Realization/Reindex.lean from PR2249 at66650221 onto fixed PR2246/383a52021, avoiding old queue-client dependencies for C5/C6. Original Gitblob18aea578f32743c7f03563931e54f08e111d1728, SHA25646541639a7334403b7dd5b325ca129e4162a433bf02981b2ca258a609496f165. Keep the original Samuel/Codex header, public API, proof and credit unchanged. Add its canonical aggregate import and an actual native read/frame test: select the second environment word, return maxword15, preserve unused7, the entire memory and frontier, with unchanged query charge. Worker codex-reindex-leaf-learning-20261102 under root/Algorithms cslib-community#2266, cslib-community#2213/cslib-community#2205. This removes a concrete C5/C6 dependency blockage; it is not a broader realization/migration endpoint or an approval of the existing API. No selected abstract/catalogue/rendering impact; pins and docs unchanged. Validation: all six default scripts/check.sh gates PASS,2threads, exact frozen content; focused strict leaf/native test3536 and hygiene PASS. Fresh outside-authoring-fleet API/correctness review is required and will be shared by2249/C5/C6. No original parent refs are modified by this layer. AI assistance: OpenAI Codex for extraction, regression and validation. * feat(WordRAM): realize measure-bounded early-exit while loops Add a finite Memory.Prog while representation and one uniform native Code.loop certificate. A source cutoff depends only on explicit initial input; reached-state rank and safety prove truncation is unreachable. Charge actual continuing bodies/control and initial/final guard overhead, including query-free loops; retain potential in the semantic cost telescope. Reuse existing Realizes, Cond, native loop rules and copyBank without a new language or judgment. Default scripts/check.sh all six gates and focused strict library/test checks pass on exact staged tree 2e3c80c, two threads. No selected abstract impact. Refs cslib-community#2259 and cslib-community#2205; the broader gate and heap migration remain open. AI assistance: Codex worker codex-c5-while-1651-20261102 under coordinator delegation; independent outside review is required. * fix(WordRAM): destructure the loop argument in Realizes.iterate₀ cslib-community#2246's iterateRuntime now binds its argument by a destructuring lambda, so iterate₀ matches the components before omega. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): native backends for memory refinements, one realized body per constructor Realization.Backend generalizes MemoryBackend: from a Refinement D (Memory.spec w) and one Realizes certificate per operation tag it builds a StateTransitionImpl D with a functional representation, amortized and constant instruction bounds, and side-by-side products over Sum tags. Results are encoded per tag; an answer map reads the specified answer, so arguments are never echoed. Realizes.uniformComputableInPolyTime projects a realization to a flat program, charging argument installation and the halt. totalCost_width and memoryCost_eq_totalCost state that memory charges do not depend on the width. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(tests): wrap long lines in the backend test Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): Backend.data, rep_data and fits_appendWords Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): backend test uses fits_appendWords and Backend.data Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * perf(WordRAM): state realize certificates per form in the client's terms `realize` compared its synthesized domain with the composed rules' domain once, at the end, by definitional unfolding. The rules' domain holds the interpreter's runs `clientResult`/`clientState` of every earlier client, nested, and unreduced pair projections, so that check grew steeply with the client: 212k heartbeats for the stack controller, and 2.5M when a bind's first client ends in a `match`. Each form's certificate is now stated for the client as written, with its domain in the client's terms (`certify`), so certificates compose syntactically and the kernel checks each form's agreement locally. A bind's continuation domain is stated at the first client's reply and next memory in closed form (`Realizes.bind₀_of_run`). Result encodings are proved by `Fin.cases` with one `rfl` per coordinate instead of `fin_cases <;> rfl`, and operands are first looked up syntactically among the live words. Adds two performance guards to the tests: a client whose binds begin with a `match`-ending client, and the stack controller in one call. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): export initialized flat programs with a standard layout Choose private canonical frontier/input/scratch banks once and project an existing Realizes certificate through the actual charged Data.init prefix, Code.program and halt. The stateful export retains the actual flat Runs, full source memory/frontier and every encoded result word; the scalar Executes corollary removes caller register-layout proofs. Its fixed code, output placement, halt PC and factor precede every runtime width/input. Keep the same raw-layout, length, fit, safe-domain and admissibility premises and C*(memoryCost+work+1)+1 bound. Empty input still requires frontier one to fit; no initialized width-zero case is claimed. The checked initialized-copy client block drops48 to20 lines with its statement unchanged. An actual write/read client checks full post-memory and maximum payload15; the empty-input case retains positive frontier fit. The original Program.lean and all its public interfaces remain exact SHAeeb7346b2d483bede91259eb6f03f50b7b494a735c264a2293e993bf0d800db2. Existing Program/native-prefix source credit remains unchanged. Worker codex-c5-canonical-program-learning-20261102 under root/Algorithms cslib-community#2279, cslib-community#2205/cslib-community#2213, fixed published2230/a929a76f. This is a bounded C5 usability milestone, not a new compiler/language/model or broad completion. Static Fin l observation retains the existing scalar-output scope; zero-output Unit exports remain separate. No selected abstract impact. All six default scripts/check.sh gates PASS,2threads, exact frozen source; strict focused3546, hygiene/check-simp/whitespace and source/pin guards PASS. Fresh outside-author-fleet correctness/API review is required. No own approval or parent source/ref changes. AI assistance: OpenAI Codex. * chore: regenerate the aggregate import after merging cslib-community#2270 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: drop imports the merge duplicated in Complexity.lean Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): state iterate₀ in iterateRuntime's named-component form cslib-community#2230 restates iterateRuntime with pattern lambdas over ((d, a), fuel) and appendWords; iterate₀ follows, which also removes its positional projections (cslib-community#1764). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): framed backends - frames, products over one memory, allocation A backend of a framed refinement carries its frame over: a native operation writes only the footprint and the reserved room (Backend.modifies), and keeps disjoint assertions and structures kept apart (frame_heap, frame). Backends of framed refinements run their product over one memory (Implements.prod_framed), each side within its own region (modifies_inl, modifies_inr). Backend.Allocation names the tag that runs a Memory.Allocator's program; Allocation.exec allocates from arbitrary bounded data within the allocator's cost, writing only the room it takes. Backend.extend adds such tags; install and exists_exec run any tag's body. The memory side is a new leaf, Memory/Region. The stack test restores modifies/frame, constant-time allocation and allocate-then-run, and two stacks over one memory. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): allocate a pair of stacks in one body realizes_allocTwo certifies the allocation of two stacks, one after the other, as Memory.Allocator.prod does; with Backend.extend it becomes the allocation tag of the pair's backend, and allocate_pair sets up both empty stacks from arbitrary bounded data in constant time. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): guarded loops in realize realize now certifies boundedWhile G step D n a whose step begins with a query. The guard is a word comparison (a = b, a < b, a > b, or a ≠ 0 tested as 0 < a) over the live and state words, with any decidability instance; an operand independent of the state is computed before the loop, and the cutoff stays a ghost bound. The certificate is transported back to the client's guard, step and environment, so the loop's domain is whileSafe in the client's terms, under the loop's valid history, ready for whileSafe_of_measure. New leaf Realization/WhileAbsorb: boundedWhile_congr, whileSafe_imp/congr, whileWork_congr (guard, body and environment congruence), the envelope whileWork_le, whileWork_zero_le and the absorbed rule Realizes.while₀. Absorb gains Realizes.consequence_valid. Tests: a memory-reading countdown (also with r ≠ 0 under a classical instance), the queue's transfer over two array stacks counted down by the items left, and a sift-shaped descent with logarithmic rank, plus controls. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(WordRAM): wrap a long line in the realize loop tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(WordRAM): use appendWords for the stack client's environments cslib-community#2230 makes appendWords public in Realization.Basic; the stack client's private append was a copy of it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): keep iterate₀'s statement, as in cslib-community#2277's proof-only repair The proof body alone needs the change for cslib-community#2230's iterateRuntime. Keeping the statement byte-identical to cslib-community#2277 lets the two branches merge without conflict. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a heartbeat budget for the realize transfer loop Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): place the transfer loop's heartbeat budget before its docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a realize loop whose guard and step capture the environment Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): export fixed programs over independent raw memory Generalize the existing canonical initialized whole-state export so raw input words vary after the program, register layout and exchange factor are chosen. The pointwise input-prefix equation relates them to the faithfully encoded argument. Preserve both existing theorem statements as wrappers. The Dijkstra consumer checks one program over every adjacency-list encode with Unit register arguments, plus two different graph memories and a maximum fitting edge weight. Original Program.lean, dependency pins and abstract catalogue are unchanged. All six default scripts/check.sh gates pass at exact tree36ae8037ff716ea9e1c58187285caf3848e0127e (2 threads); focused3572 and hygiene pass. AI assistance: OpenAI Codex, session codex-dijkstra-native-learning-20261102. Refs cslib-community#2281, cslib-community#2288. * wip(WordRAM): freeze option-pair implementation during gated repair Private checkpoint for cslib-community#2291. Initial focused option clients pass; extended legacy-normalization and native-budget tests currently fail and remain to be repaired. Not a submission or validation claim. * fix(WordRAM): preserve scalar encoding normal form in generic option support Keep the legacy OptionNat embedding and instance, connect it to the shared payload embedding, and check same-body none/max-payload executions. Focused pair/legacy clients passed3586 before the added definitional-instance guard; no full validation or public submission yet. * feat(WordRAM): reuse static method certificates and linked runs Add call-site dispatch through existing Realizes.reindex and a small full-run linking congruence leaf. Tests cover opaque uncurried calls, reached-state domains, charged arithmetic staging and complete adaptive memory histories. Original realize/while suites pass unchanged. All six default checks pass at exact tree0b27a9790e6718825abdaf686f3849fff918c002, session7009/2threads; focused3590/2036 and hygiene pass. Known consumer gap: curried functions wrapped in a tuple lambda still need constructor-skeleton matching before publication. This is not the native Dijkstra endpoint. No abstract, pin, original Program or Reindex changes. AI assistance: OpenAI Codex, codex-dijkstra-native-learning-20261102. Refs cslib-community#2288. * fix(WordRAM): match packaged curried method calls Build only pair and dependent-pair argument skeletons before matching a local uniform Realizes certificate. Keep other argument values undetermined until the source call fixes them, and retain the static live-word wiring and zero-work policy. The actual original Memory.siftDown call with a runtime Sigma layout now passes a direct kernel check without unfolding recursion. Production regressions cover curried scalar calls and an opaque curried optional-pair extraction. Original realize/while and optional-word clients pass unchanged. All six default checks pass at exact tree441c917c2daaf4f6dcdf0b4aca2fc326ad7220bc (session35315,2threads), in the ordinary merged public2294 context; strict focused3596/hygiene also pass. Earlier7675 validation covers only its own older tree. No abstract/pin/model changes. AI assistance: OpenAI Codex, codex-dijkstra-native-learning-20261102. Refs cslib-community#2288. * chore(WordRAM): canonicalize supplier import order Source-only composition of original2288 supplier head73704c97, published2268/b32e8357,2281/1e77082f and2294/2eb7dc04. No owned2297 call/link payload is included. Canonical import order matches the all-six-validated current composition with LinkCongr absent; pending supplier correctness/API/integration gates remain separate. AI assistance: OpenAI Codex, codex-dijkstra-call-link-learning-20261102. * fix(realize): match dependent method arguments after charged staging Solve same-head call arguments in binder order, retaining static live-word wiring and reached-state domains. Add the dependent scalar/pair staging regression from the original heap extraction consumer. Validation: default scripts/check.sh, LEAN_NUM_THREADS=2, all six gates pass at tree 3ee50d4 (session46520). Original curried/OptionPair/realize tests and actual heap extraction scalar/pair staging pass. Abstract assessment: no selected statements or scope changed. AI-assisted by OpenAI Codex. Part of cslib-community#2297; the broader native Dijkstra endpoint remains cslib-community#2288. * fix(realize): scope tactic syntax to WordRAM Delegate codex-realize-scope-crypto-20261102 under cslib-community#2297/cslib-community#2300. Preserve the complete inherited elaborator body and all other source entries. A private import no longer activates realize outside Cslib.WordRAM; both namespace and scoped opens activate it. Validation: strict six-target focused build, session 82324, passed 3646 jobs; targeted hygiene and whitespace checks passed. New parser rejection and positive read-certificate regressions pass; unchanged R1/While/Framed/Call/OptionPair suites pass. Exact original-source no-output probe confirms the old global availability. No default full-six or public update is claimed. Original Samuel Schlesinger source credit is retained. AI assistance: OpenAI Codex. * fix(realize): retain captured loop environment words Fix cslib-community#2317 in the existing private iterate frontend: substitute live environment captures as the while frontend does, then transport the exact original loop and reached-state domain with kernel-checked fixed-environment inductions. Preserve the noncapturing paths, public calculus and elaborator entrypoint body, original source program, visible fits/work and uniform emitter quantifiers. No new loop rule, model or public mathematical API. Strict focused session5788 passed3648 jobs: unchanged R1/While/Framed/Call/OptionPair/scope, original-domain opaque captured calls and one emitted body on two distinct runtime inputs with zero/two charged iterations/full memory preservation. Identical final regressions fail on exact old27e in output-free session68169. Hygiene/whitespace pass. Circuits directly checked unchanged original F1 Gather/domain/work and native n0w3 with input7 and Fits3 8 false; local acceptance receipt is linked from the issue handoff. No full-six or publication claim; original Samuel/Claude supplier credit retained. AI assistance: OpenAI Codex. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…b-community#2288) * feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of #2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): weaken and rescale amortized refinements Amortized.mono and Amortized.mul_left (exchange at a constant rate, #2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): make Refinement.Amortized a structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: array stack over memory and queue method lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Foundations): affine cost bounds are O(size) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: queue over memory Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): product answer types via Sum.elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): queue over two array stacks over the memory oracle The M1 slice of #2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): certify compositional register-word glue Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone #2210; the memory realization kernel and vertical-slice gate remain in #2205. Validation: final staged tree a1b88e3fd1cc5e72a9a105865df17fa04295710e passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending. * feat(WordRAM): realize memory queries with uniform bind and glue Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of #2213 under #2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved. * fix(WordRAM): normalize the memory return simp rule * feat(WordRAM): realize bounded loops and initialized client programs Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under #2213 and #2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged. * feat(WordRAM): derive global and framed implementation certificates Project the four fixed memory-query bodies into the existing semantic StateTransitionImpl interface with explicit delivered-argument preparation and body-only cost bounds. Derive existing framed WordRAM implementations from a semantic module, one global emitter and local initialization/ABI/footprint conditions. Runtime argument maps do not choose a new emitter per object. Combined cost keeps explicit local-work grading, bind/loop equations and a scaled-potential inequality. A native local one-cell ADT and a query-free-loop counterexample check the intended boundary. Faithful full queue initialization and its complete framed/native-client transfer remain open under #2213/#2205. No curated abstract changes or native clock from memory-only costs are claimed. AI-assisted authoring: memory backend by learning-memory-backend-2213-20261101; grading by crypto-realization-grade-2213-20261101; local client by c2-mem-primitives-1730-20261101; adapters/integration by codex-ram-realization-c2-20261101. All new public API needs outside-fleet review. * feat(WordRAM): realize runtime-layout memory-stack methods Stage multiword results from fixed scalar-glue witnesses, charging every coordinate and output copy. Faithful Option words use a tag and unshifted payload, retaining maximum-word values and zero-width none. Consume the unchanged published Stack.Memory methods over full runtime layout words. Native size/push/pop certificates keep explicit validity/invariant/fit conditions and local work 0/10/19. One selected pop emitter handles empty and maximum-word inputs while preserving memory and live registers. This is a bounded #2213/#2205 milestone. The framed queue and faithful allocated queue-client path remain open. No abstract selection or headline changes. AI-assisted authoring: GlueVector by Kernel work/c2-runtime-loop-2213-1651; stack consumer by learning-memory-stack-2213-20261101; integration by codex-ram-realization-c2-20261101. Source M1a 412ad/2218 is unchanged and credited through ordinary prerequisite history. Outside-fleet review remains required. * refactor(WordRAM): centralize realization history and word encodings Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact. * refactor(WordRAM): expose shared glue rules and infer stack push Address outside review5731265464. Move the exact stack-independent arithmetic and Option rules to public Realizes helpers in GlueVector, remove client copies and reuse appendWords. Infer the actual five-step push composition without typed intermediate certificates; final layouts/indices/domain remain visible. Statement meanings, clocks, source methods and tests are preserved. Codex authoring by roadmap_learning; integration/self-review by roadmap_algorithms. Ordinary parent merge carries2230a929 fix. Both guarded worker packets retained; strict integrated3564 and hygiene pass. Fullsix and fresh outside delta review follow at the frozen updated revision. No selected abstract impact or broader M1 completion claim. * feat(WordRAM): realize tactic for memory-client realizations Add `realize`, which proves `Realizes B p input output safe work` for a loop-free memory client by walking its syntax: bind, pure, the four memory queries, `if` on a word comparison and `match` on an optional answer. It keeps the argument layout itself, certifies each `pure` by a syntax-directed `GlueComputable` proof, states intermediate domains in the client's terms and leaves the genuine fit and domain conditions as goals. `Realization/Absorb.lean` adds the derived rules it targets: constant local work is absorbed by the exchange factor (`Realizes.mono_mul`), giving `bind₀`, `branch₀` and `pure₀`, plus `Realizes.congr` and the `WordEncoding` class for intermediate answers. Refs #2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): loops whose body issues a query in realize Generalize `Realizes.mono_mul` to local work dominated by the memory charge, and add `Realizes.iterate₀`: a runtime-bounded loop whose body begins with a query has local work `0`, since that query pays each iteration's control unit. `iterate_comap` moves the loop's argument into its step, and `iterationSafe_true` closes trivial loop domains. `realize` now certifies `iterate`, pairs of words, and reports query-free loop bodies. Refs #2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a whole stack client to a flat program via realize Add `blockWords` and its `WordEncoding` instance, so binds may return blocks and layouts. `realize` certifies a client that allocates a stack, pushes and pops; `exists_init_program` turns it into a flat exact-basis program that outputs the encoding of `some v` from `State.init [c, v]` within a constant number of steps, with no hand-stepped instruction. Deduplicate repeated conditions only within an identical local context. Refs #2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): extract the static input reindex leaf Copy the exact existing Realization/Reindex.lean from PR2249 at66650221 onto fixed PR2246/383a52021, avoiding old queue-client dependencies for C5/C6. Original Gitblob18aea578f32743c7f03563931e54f08e111d1728, SHA25646541639a7334403b7dd5b325ca129e4162a433bf02981b2ca258a609496f165. Keep the original Samuel/Codex header, public API, proof and credit unchanged. Add its canonical aggregate import and an actual native read/frame test: select the second environment word, return maxword15, preserve unused7, the entire memory and frontier, with unchanged query charge. Worker codex-reindex-leaf-learning-20261102 under root/Algorithms #2266, #2213/#2205. This removes a concrete C5/C6 dependency blockage; it is not a broader realization/migration endpoint or an approval of the existing API. No selected abstract/catalogue/rendering impact; pins and docs unchanged. Validation: all six default scripts/check.sh gates PASS,2threads, exact frozen content; focused strict leaf/native test3536 and hygiene PASS. Fresh outside-authoring-fleet API/correctness review is required and will be shared by2249/C5/C6. No original parent refs are modified by this layer. AI assistance: OpenAI Codex for extraction, regression and validation. * feat(WordRAM): realize measure-bounded early-exit while loops Add a finite Memory.Prog while representation and one uniform native Code.loop certificate. A source cutoff depends only on explicit initial input; reached-state rank and safety prove truncation is unreachable. Charge actual continuing bodies/control and initial/final guard overhead, including query-free loops; retain potential in the semantic cost telescope. Reuse existing Realizes, Cond, native loop rules and copyBank without a new language or judgment. Default scripts/check.sh all six gates and focused strict library/test checks pass on exact staged tree 2e3c80c721b86735949299d1885499734290d6b9, two threads. No selected abstract impact. Refs #2259 and #2205; the broader gate and heap migration remain open. AI assistance: Codex worker codex-c5-while-1651-20261102 under coordinator delegation; independent outside review is required. * fix(WordRAM): destructure the loop argument in Realizes.iterate₀ #2246's iterateRuntime now binds its argument by a destructuring lambda, so iterate₀ matches the components before omega. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): native backends for memory refinements, one realized body per constructor Realization.Backend generalizes MemoryBackend: from a Refinement D (Memory.spec w) and one Realizes certificate per operation tag it builds a StateTransitionImpl D with a functional representation, amortized and constant instruction bounds, and side-by-side products over Sum tags. Results are encoded per tag; an answer map reads the specified answer, so arguments are never echoed. Realizes.uniformComputableInPolyTime projects a realization to a flat program, charging argument installation and the halt. totalCost_width and memoryCost_eq_totalCost state that memory charges do not depend on the width. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(tests): wrap long lines in the backend test Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): Backend.data, rep_data and fits_appendWords Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): backend test uses fits_appendWords and Backend.data Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * perf(WordRAM): state realize certificates per form in the client's terms `realize` compared its synthesized domain with the composed rules' domain once, at the end, by definitional unfolding. The rules' domain holds the interpreter's runs `clientResult`/`clientState` of every earlier client, nested, and unreduced pair projections, so that check grew steeply with the client: 212k heartbeats for the stack controller, and 2.5M when a bind's first client ends in a `match`. Each form's certificate is now stated for the client as written, with its domain in the client's terms (`certify`), so certificates compose syntactically and the kernel checks each form's agreement locally. A bind's continuation domain is stated at the first client's reply and next memory in closed form (`Realizes.bind₀_of_run`). Result encodings are proved by `Fin.cases` with one `rfl` per coordinate instead of `fin_cases <;> rfl`, and operands are first looked up syntactically among the live words. Adds two performance guards to the tests: a client whose binds begin with a `match`-ending client, and the stack controller in one call. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): export initialized flat programs with a standard layout Choose private canonical frontier/input/scratch banks once and project an existing Realizes certificate through the actual charged Data.init prefix, Code.program and halt. The stateful export retains the actual flat Runs, full source memory/frontier and every encoded result word; the scalar Executes corollary removes caller register-layout proofs. Its fixed code, output placement, halt PC and factor precede every runtime width/input. Keep the same raw-layout, length, fit, safe-domain and admissibility premises and C*(memoryCost+work+1)+1 bound. Empty input still requires frontier one to fit; no initialized width-zero case is claimed. The checked initialized-copy client block drops48 to20 lines with its statement unchanged. An actual write/read client checks full post-memory and maximum payload15; the empty-input case retains positive frontier fit. The original Program.lean and all its public interfaces remain exact SHAeeb7346b2d483bede91259eb6f03f50b7b494a735c264a2293e993bf0d800db2. Existing Program/native-prefix source credit remains unchanged. Worker codex-c5-canonical-program-learning-20261102 under root/Algorithms #2279, #2205/#2213, fixed published2230/a929a76f. This is a bounded C5 usability milestone, not a new compiler/language/model or broad completion. Static Fin l observation retains the existing scalar-output scope; zero-output Unit exports remain separate. No selected abstract impact. All six default scripts/check.sh gates PASS,2threads, exact frozen source; strict focused3546, hygiene/check-simp/whitespace and source/pin guards PASS. Fresh outside-author-fleet correctness/API review is required. No own approval or parent source/ref changes. AI assistance: OpenAI Codex. * fix(WordRAM): adapt private R1 iteration proof to corrected loop Reuse the unchanged proof body from approved PR2277/fb0bf094. All public statements and tactic code are unchanged. Strict Absorb and unchanged WordRAMRealize regressions PASS3578; 40k budgets retained. Private prerequisite only; canonical R1 owner handoff on PR2280. * chore: regenerate the aggregate import after merging #2270 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: drop imports the merge duplicated in Complexity.lean Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): state iterate₀ in iterateRuntime's named-component form #2230 restates iterateRuntime with pattern lambdas over ((d, a), fuel) and appendWords; iterate₀ follows, which also removes its positional projections (#1764). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): framed backends - frames, products over one memory, allocation A backend of a framed refinement carries its frame over: a native operation writes only the footprint and the reserved room (Backend.modifies), and keeps disjoint assertions and structures kept apart (frame_heap, frame). Backends of framed refinements run their product over one memory (Implements.prod_framed), each side within its own region (modifies_inl, modifies_inr). Backend.Allocation names the tag that runs a Memory.Allocator's program; Allocation.exec allocates from arbitrary bounded data within the allocator's cost, writing only the room it takes. Backend.extend adds such tags; install and exists_exec run any tag's body. The memory side is a new leaf, Memory/Region. The stack test restores modifies/frame, constant-time allocation and allocate-then-run, and two stacks over one memory. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): allocate a pair of stacks in one body realizes_allocTwo certifies the allocation of two stacks, one after the other, as Memory.Allocator.prod does; with Backend.extend it becomes the allocation tag of the pair's backend, and allocate_pair sets up both empty stacks from arbitrary bounded data in constant time. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): guarded loops in realize realize now certifies boundedWhile G step D n a whose step begins with a query. The guard is a word comparison (a = b, a < b, a > b, or a ≠ 0 tested as 0 < a) over the live and state words, with any decidability instance; an operand independent of the state is computed before the loop, and the cutoff stays a ghost bound. The certificate is transported back to the client's guard, step and environment, so the loop's domain is whileSafe in the client's terms, under the loop's valid history, ready for whileSafe_of_measure. New leaf Realization/WhileAbsorb: boundedWhile_congr, whileSafe_imp/congr, whileWork_congr (guard, body and environment congruence), the envelope whileWork_le, whileWork_zero_le and the absorbed rule Realizes.while₀. Absorb gains Realizes.consequence_valid. Tests: a memory-reading countdown (also with r ≠ 0 under a classical instance), the queue's transfer over two array stacks counted down by the items left, and a sift-shaped descent with logarithmic rank, plus controls. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(WordRAM): wrap a long line in the realize loop tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(WordRAM): use appendWords for the stack client's environments #2230 makes appendWords public in Realization.Basic; the stack client's private append was a copy of it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): keep iterate₀'s statement, as in #2277's proof-only repair The proof body alone needs the change for #2230's iterateRuntime. Keeping the statement byte-identical to #2277 lets the two branches merge without conflict. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a heartbeat budget for the realize transfer loop Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): checkpoint sift-up realization for heap migration Internal building block for #2282, not a standalone native heap PR. Reuse original Memory.siftUp with exact FreeM/history/cost transport, R1 scalar/bind/branch compilation and C5 early-exit while. Uniform code before all runtime n/layout/width/index/memory. Native body time is bounded by a fixed factor times log n plus one, with full source memory and caller frame. Installed-argument ABI only; no bit-cost, complete heap or improved space/step claim. Strict focused library and three same-emitter native edge fixtures PASS3582; hygiene and whitespace PASS. No full-six claimed. Canonical parent/R1 compatibility publication and outside API review remain gates. AI-assisted implementation by Codex; original heap and supplier source credit retained. * test(WordRAM): place the transfer loop's heartbeat budget before its docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a realize loop whose guard and step capture the environment Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(BinaryHeap): support compact locally initialized memory layouts Internal #2282 migration obligation: the existing Layout may hold its count at unused heap[0], retaining legacy3n+1 space. Generalize HeapInv.congr_mem to ignore only that unused cell, carry the stronger source invariant/count-update proofs through every existing caller, and expose the same-layout compact specialization plus local-zero empty-invariant rule. Original allocator/program semantics and old native statements/clocks remain unchanged. Renfei Zhou source credit retained. Strict focused Memory/original tests/native sift fixtures/legacy BinaryHeap all PASS3598; new edge tests cover n0/base0/w1 andn1/base3/w3, real insert/extract and dirty outside cells without globalZeroAbove. Hygiene PASS. No native initialization or full migration/deletion/full-six claimed; fresh outside API review required. AI-assisted by Codex. * refactor(BinaryHeap): share runtime encodings for native migration Move the unpublished sift building block into the application Native leaf. Share the identical existing runtime Layout encoding plus faithful typed-handle inclusion, before every runtime n/layout/width. This supplies both sifts and method family clients without a parallel layout or successor sentinel. No old native heap code is removed. Strict focused encoding/sift/nativefixtures PASS3586 and typed-handle mapping PASS; hygiene/whitespace PASS. Full migration and native setup/Backend/wholeDijkstra obligations remain open; this is not a standalone PR. AI-assisted by Codex. * feat(WordRAM): export fixed programs over independent raw memory Generalize the existing canonical initialized whole-state export so raw input words vary after the program, register layout and exchange factor are chosen. The pointwise input-prefix equation relates them to the faithfully encoded argument. Preserve both existing theorem statements as wrappers. The Dijkstra consumer checks one program over every adjacency-list encode with Unit register arguments, plus two different graph memories and a maximum fitting edge weight. Original Program.lean, dependency pins and abstract catalogue are unchanged. All six default scripts/check.sh gates pass at exact tree36ae8037ff716ea9e1c58187285caf3848e0127e (2 threads); focused3572 and hygiene pass. AI assistance: OpenAI Codex, session codex-dijkstra-native-learning-20261102. Refs #2281, #2288. * refactor(binaryheap): absorb actual sift-up control work Reuse the canonical whileWork_zero_le rule. The public certificate retains the original source family, safety domain and exact memory behavior while queries pay the bounded local grade. Focused native sift and unchanged fixtures pass; no full validation or migration completion claimed. * wip(WordRAM): freeze option-pair implementation during gated repair Private checkpoint for #2291. Initial focused option clients pass; extended legacy-normalization and native-budget tests currently fail and remain to be repaired. Not a submission or validation claim. * feat(binaryheap): realize existing constant-time read methods Use the canonical realize rules and shared runtime layout/handle encodings. Tests execute the same selected code on present and absent handles at maximum key 15, preserve full memory/frontier and retain constant read-method budgets. Arguments remain installed; full heap migration, initialization and outside review remain pending. * refactor(binaryheap): accept runtime handle words in source methods Generalize three existing Memory program arguments from Fin n to Nat, leaving program bodies and all typed indexed-operation/correctness declarations unchanged. The word certificate states v<n explicitly; the typed lookup certificate derives by static reindex. Focused source, legacy native, compact-domain and max-word native regressions pass. Fresh outside API review remains required with the migration. * fix(WordRAM): preserve scalar encoding normal form in generic option support Keep the legacy OptionNat embedding and instance, connect it to the shared payload embedding, and check same-body none/max-payload executions. Focused pair/legacy clients passed3586 before the added definitional-instance guard; no full validation or public submission yet. * feat(binaryheap): compose native source update methods Realize the original insert/decrease prefixes with shared R1 rules and statically compose the uniform sift-up certificate. Entry domains reuse the original heap invariant and indexed-PQ validity. Native max-word insertion/decrease and negative domain clients pass; common test-only packing removes repeated ABI plumbing. Focused strict checks and hygiene pass; full migration, initialization, backend and outside review remain open. * chore(binaryheap): refresh canonical imports for native checkpoint * feat(BinaryHeap): realize source-faithful sift-down through shared loops Private #2282 delegated author slice. Preserve the complete original memory program, including four mandatory reads, optional right-child reads, strict handle ties and original four-write swap. Use the existing Realizes/Code.loop route, input-only logarithmic ghost cutoff and a paid initial zero guard before threshold preparation. Lift the source order/rearrangement theorem with explicit allocation, fits, installed-argument ABI and native frame. Validation: focused strict library/test PASS (3586 jobs); hygiene --check-simp and staged diff checks PASS. Same-emitter native left-only, read-then-stop, tie/right and width1/n0/index0 fixtures; dirty cell retained. Providers, pins, abstracts and old endpoints unchanged; no full-six, publication, deletion or migration-completion claim. AI assistance: OpenAI Codex under Algorithms coordinator delegation. (cherry picked from commit 526575bc59baf2bb9b9b59f4ba1a1d94ef45913a) * refactor(binaryheap): reuse shared width transport in native sift Replace the delegated private width/charge transport with the approved Backend fact after its ordinary dependency merge, leaving all public statements/source/code/tests unchanged. Integrated focused sift/native regressions pass3602 and hygiene; imports regenerated. Previous eb0145 all-six receipt is not claimed for this expanded dependency tree. * feat(WordRAM): reuse static method certificates and linked runs Add call-site dispatch through existing Realizes.reindex and a small full-run linking congruence leaf. Tests cover opaque uncurried calls, reached-state domains, charged arithmetic staging and complete adaptive memory histories. Original realize/while suites pass unchanged. All six default checks pass at exact tree0b27a9790e6718825abdaf686f3849fff918c002, session7009/2threads; focused3590/2036 and hygiene pass. Known consumer gap: curried functions wrapped in a tuple lambda still need constructor-skeleton matching before publication. This is not the native Dijkstra endpoint. No abstract, pin, original Program or Reindex changes. AI assistance: OpenAI Codex, codex-dijkstra-native-learning-20261102. Refs #2288. * feat(BinaryHeap): certify compact reservation and layout word primitives Private delegated author slice under #2282. Realize exact allocDirty(space n) using addition spelling to retain n0/w1, and compute the faithful [n,base+n,1] vector using existing charged pure/scalar glue. Native projections retain full memory, frontier/input frames, exact old-front return and one fixed emitter before runtime inputs. Link local zero after actual reservation to the existing compact empty invariant. Validation: strict focused library/test target PASS3582, hygiene --check-simp and staged diff checks PASS. Same witnesses cover n0/base0/w1 and n1/base3/w3/end7 with dirty outside preserved, and stale-position rejection. No full wrapper, legacy11/rBin25 equivalence, generic localPre allocator, source allocator change, full-six, PR or push. Existing providers/pins/abstracts unchanged. AI assistance: OpenAI Codex under Algorithms delegation. * fix(WordRAM): match packaged curried method calls Build only pair and dependent-pair argument skeletons before matching a local uniform Realizes certificate. Keep other argument values undetermined until the source call fixes them, and retain the static live-word wiring and zero-work policy. The actual original Memory.siftDown call with a runtime Sigma layout now passes a direct kernel check without unfolding recursion. Production regressions cover curried scalar calls and an opaque curried optional-pair extraction. Original realize/while and optional-word clients pass unchanged. All six default checks pass at exact tree441c917c2daaf4f6dcdf0b4aca2fc326ad7220bc (session35315,2threads), in the ordinary merged public2294 context; strict focused3596/hygiene also pass. Earlier7675 validation covers only its own older tree. No abstract/pin/model changes. AI assistance: OpenAI Codex, codex-dijkstra-native-learning-20261102. Refs #2288. * feat(binary-heap): realize the existing layout allocator Keep the original two dirty queries, 3n+2 layout and memory history. Place only the returned dependent layout into the existing HeapLayout sigma encoding for uniform code. Add same-emitter width, nonzero-frontier, dirty-memory and global-zero fixtures. AI-assisted delegated worker slice under #2282; codex-heap-init-primitives-1651-20261102. Focused strict target and hygiene pass. No full-six, raw ABI wrapper, old clock equivalence, abstract changes or approval claimed. * chore(WordRAM): canonicalize supplier import order Source-only composition of original2288 supplier head73704c97, published2268/b32e8357,2281/1e77082f and2294/2eb7dc04. No owned2297 call/link payload is included. Canonical import order matches the all-six-validated current composition with LinkCongr absent; pending supplier correctness/API/integration gates remain separate. AI assistance: OpenAI Codex, codex-dijkstra-call-link-learning-20261102. * feat(WordRAM): retain Backend register frames for live-input execution Expose existing shared packing facts and install identity under actual live words; derive a full-frame execution result and raw-live corollary from the same Realizes code_spec. Existing definitions and all previous theorem types are unchanged; exists_exec projects the stronger proof. Tests exercise different result widths, paid zero staging, zero/max-word inputs and a genuine memory-read provider. Under #2298 for queue #2284 and heap #2282; inherited Claude source credit retained. Strict focused3628 and hygiene pass; full-six/outside review pending. * feat(wordram): realize original heap extraction and assemble its backend Private #2282 migration checkpoint. Exact original extraction is observed through the checked typed entry constructor, with complete state/history transport. Native tests include empty width1, maximum key15 and a real root-removal sift swap. The existing Backend supplies constant read/logarithmic update body bounds and source footprint preservation. Focused source/fixtures and hygiene passed with exact borrowed Learning call matcher SHA5f8a3d1d. That separately owned pending prerequisite is not included in this commit; this is not a standalone public revision or full-six claim. Shared initialization, raw argument delivery, the full native Dijkstra migration, outside review and legacy deletion remain open. AI assistance: Codex/GPT-6. * fix(realize): match dependent method arguments after charged staging Solve same-head call arguments in binder order, retaining static live-word wiring and reached-state domains. Add the dependent scalar/pair staging regression from the original heap extraction consumer. Validation: default scripts/check.sh, LEAN_NUM_THREADS=2, all six gates pass at tree 3ee50d45a0f805b657efc51edaff1c8d71a37760 (session46520). Original curried/OptionPair/realize tests and actual heap extraction scalar/pair staging pass. Abstract assessment: no selected statements or scope changed. AI-assisted by OpenAI Codex. Part of #2297; the broader native Dijkstra endpoint remains #2288. * feat(wordram): compose the compact heap initializer on its native ABI Private #2282 migration checkpoint. One existing PQCode register family includes all five method bodies plus the certified reserve and metadata routines before runtime n/base/width. Actual initialization preserves the complete old memory and the legacy 3n+1/local-zero domain, with paid constant reservation and setup. Same-code width1/capacity0 and width3/base3/end7 fixtures pass. Strict focused source/native fixtures PASS3614 plus hygiene. Canonical pending #2300 and #2299 source parents are ordinarily merged, not authored here. Dispatcher correctness, full SubroutineBase/dirty initialization/client clocks, native Dijkstra, outside review and final legacy removal remain unfinished. No full-six claim or old instruction/register constant is made. AI assistance: Codex/GPT-6. * feat(wordram): expose the compact heap ABI observations Add the five exact frontier/dimension/base/input-mask observations required by the delegated finite-footprint representation proof. Existing code bodies, encodings, clocks, domains and tests are byte-preserved. Keep the implementation opaque and export only its proved metadata facts. Strict focused source and original raw initialization tests PASS3614; hygiene passed. This follow-up is not covered by the earlier8004 full-six receipt; final combined migration checks/outside review remain. AI assistance: Codex/GPT-6. * feat(binary-heap): specialize Backend representation to compact raw storage Use the existing extended Backend representation and add only the four persistent layout words. Derive boundedness, finite-block support and the actual local-zero initializer bridge, keeping the original 3n+1 end-fit domain and whole-memory identity. Delegated worker codex-heap-representation-1651-20261102 under #2282. Focused strict target (3616 jobs), hygiene and diff checks pass. Explicit c9addcf45 application ABI supplier; no provider edits, full-six, publication, legacy-clock or full migration claim. AI-assisted source and tests. * feat(wordram): verify live heap method argument delivery Prove the established three-bit PQ calling convention supplies the selected original method input words from actual persistent layout and payload registers. Uses existing cross-tag Backend source-position facts, without a free prepare step or compiler change. Expose only the pure five-case backend tag/argument/observation record needed by the concrete caller; all method code, domain and cost meanings are unchanged. Strict focused Program PASS3612 and hygiene passed. Later current-combination tests/outside review remain; no reuse of8004 full-six as this revision evidence. AI assistance: Codex/GPT-6. * feat(wordram): retain the source extraction result in the raw observation bridge Expose exact result erasure alongside full typed run/state/history transport, so the native PQ decoder can recover the original bounded handle without an extra successor encoding or fit premise. Register the delegated finite-footprint representation in the canonical aggregate. Integrated Backend/Extract/rawProgram/Representation and actual source/native fixtures strictPASS3624 plus hygiene. No new kernel, source algorithm, prepared-call complexity, current-full-six or full-migration claim. AI assistance: Codex/GPT-6. * feat(priority-queue): add equations for the existing word-RAM decoder Expose Boolean, absent/present key and typed extraction equations over arbitrary PQCode without changing its decoder. Concrete global heap-code fixtures retain nonzero flag semantics, unshifted maximal keys and handle-range rejection. AI-assisted worker codex-pq-decode-1651-20261102 under #2282. Strict focused target3616, hygiene and diff checks pass. Existing providers and Representation32fd stay exact; no full-six, native-operation execution or public integration approval claimed. * feat(dijkstra): preserve linked source in word-level loop views Private #2288 development checkpoint. Exact FreeM equalities preserve all queries, reached memories, malformed-target fallback, original addition guard and empty-queue exit. The binary instance keeps the original allocator and recovers Memory.run exactly. Existing semantic refinements and checked entry observation are reused; no new backend, decoder or execution model. Strict focused source/tests PASS3604 and hygiene. Concrete tests retain both zero-degree offset reads, one empty extraction despite37 available rounds, and the invalid-target zero-weight fallback with all writes/state. Native realization/domain/clock proofs, outside review and endpoint/deletion remain unfinished. No abstract impact. AI-assisted by OpenAI Codex; original supplier and Claude design credit retained. * feat(wordram): certify the heap ABI for generic linear clearing Prove the five clear-register distinctness, retained runtime dimension, and existing exact increment semantics required by SubroutineBase. No code, allocator, memory representation, domain, or clock definition changes. These facts let the existing shared initializer clear dirty storage honestly in linear space. Strict Program/Representation source/native targets PASS3616 plus hygiene. Full SubroutineBase and method dispatch still under construction; old8004 all-six is not this revision. AI assistance: Codex/GPT-6. * fix(WordRAM): expose Backend extension and preparation metadata Expose only the existing pure extend record and prepare alias so real heap bounds and conditional already-live entry elaborate without local record copies or dependent observation wrappers. All definition bodies/types, code/arg/rep/resource meanings are unchanged. Generic bound_extend and actual-live operation-entry regressions pass with the old clients; full new-head validation/review pending under #2298. * refactor(wordram): account for the raw heap dispatcher wrapper Private compositional helper lifts an actual selected body execution through the existing zero staging, three conditional tests and lookup result-key copy. The wrapper costs at most six additional native instructions. It does not assume a free prepare, reimplement a heap instruction, or establish an operation without the supplied body certificate. Strict focused Program PASS3612/hygiene. Internal helper for pending complete raw method proof; no public heap endpoint/full check or completion claim. AI assistance: Codex/GPT-6. * feat(binary-heap): package compact raw initialization as SubroutineBase Reuse the existing global Program, Backend representation and standard priority-queue ABI with only original end-fit and key-fit premises. Setup executes the existing metadata routine without reserving again. Charge metadata awaits separate method execution. Fresh one-bit and actual linear dirty-clear fixtures preserve outside memory; every original four-cell owned location is cleared with the shared zeroFillCode rule. AI-assisted delegated worker codex-heap-base-1651-20261102 under #2282. Strict focused3618, hygiene and diff pass; no full-six, StateTransitionImpl, old clock, source publication or approval claim. * feat(wordram): lift native heap bodies through the charged raw ABI Use the existing family extension and conditional live entry API. Bound the extended operation bodies with the same per-operation source charges. Account for the actual dispatcher/control/key-copy overhead and preserve full memory, frontier, layout and typed-result slots; stage-zero facts keep actual live inputs and source memory intact. Register the delegated Base and existing decoder lemmas. Integrated source/rawProgram/Base/Rep/decoder/BackendLive fixtures strictPASS3636; subsequent Program/Base source+native targets PASS3618 and hygiene. This is still private proof plumbing for the pending closed method StateTransitionImpl; no heap publication/deletion, new full-six or outside approval claim. Canonical provider73f public2299 and754a public2300 remain independently gated. AI assistance: Codex/GPT-6. * feat(wordram): expose the existing common heap source positions Add the single argument_source observation requested by the raw method-frame consumer. It reveals only the existing source-coordinate identity, without exposing or changing emitted code, counts, domains or layouts. Strict Program/Base/native validation PASS3618 and hygiene; final combined/outside gates remain. AI assistance: Codex/GPT-6. * feat(binary-heap): certify actual raw native priority-queue methods Extend the existing opaque SubroutineBase using live Backend executions, source correctness and bounds, and the paid raw dispatcher. Preserve exact source memory state, typed extraction, the compact footprint and the original end-fit/key-fit domain. Argument matching remains an explicit uncharged calling convention. Same global program fixtures cover capacity zero at one bit, shifted-base maximal-key insertion, noncanonical tag7 lookup, decrease and typed extraction, with outside sentinels and actual body charges. AI-assisted delegated worker codex-heap-implementation-1651-20261102 under #2282; strict focused3622 and hygiene/diff pass. No full-six, publication, old numeric clock/register or complete-client/migration claim. * feat(binary-heap): retain standalone realized client certificates Project the actual raw heap implementation through the existing standalone DynamicCertificate and adaptive-client APIs. Preserve the compact fit/local-zero domain, typed observations and halt-inclusive call costs. External argument delivery and host continuations remain outside this operation-call model. The retained insert/tie/decrease/extract regression starts from actual native initialization. No legacy heap deletion or standalone migration PR is implied; the joint native-Dijkstra retirement and outside review remain open in #2282. Validation: strict focused certificate/client PASS (3624 jobs), targeted hygiene/check-simp and canonical aggregate PASS. Private combined default-six checkpoint pending. Abstract/catalogue/rendering: no impact; no headline added. AI assistance: OpenAI Codex authored the certificate projection and adapted the existing Renfei Zhou client regression. Kernel's separately credited raw implementation remains an unchanged parent commit. * refactor(binary-heap): place the retained memory model with its clients Move the existing Model module and its namespace to PriorityQueue.BinaryHeap; move the existing Order namespace with it. Preserve all declaration bodies and Renfei Zhou/Samuel Schlesinger source credit, and update every current client. Six retained legacy Sift proof calls use explicit qualification after the type namespace move; their statements and algorithms are unchanged. The old native Program/Sift/top-level implementation and Dijkstra consumers are still present. Their retirement remains gated on the jointly validated native Dijkstra replacement and outside review in #2282. No old clock/register bound or migration-complete claim is made. Validation: strict affected model/native/legacy/Dijkstra targets PASS3678; targeted hygiene/check-simp, canonical aggregate and changed-line style PASS. New-tree default six pending. Abstract/catalogue/rendering: no semantic impact; no selected statement or headline changed. AI assistance: OpenAI Codex performed the mechanical move and proof-call qualification, reusing the earlier Kernel declaration/consumer inventory. * feat(Dijkstra): realize the allocated binary-heap client natively Realize the exact original memory program through faithful runtime word encodings, existing heap certificates and query-paid bounded-while rules. Derive one initialized flat program before all runtime graphs and widths, retaining the full final memory/frontier and the original word envelope. The prefix, arithmetic, calls, copies, control and halt are charged. The checked same-program client covers a singleton and a weighted graph with an unreachable vertex. Move the existing input-fit proof from the legacy GenericPQ implementation into ListEncode, updating its old client. Original Renfei Zhou/Samuel Schlesinger source and retained Claude design credit are preserved. Broader Fibonacci migration, fixed-coefficient API disposition and legacy retirement remain open; no abstract change. Validation: strict focus 3668 jobs, hygiene, canonical imports, whitespace, and all six default scripts/check.sh gates PASS on exact staged tree 506c18245df21098c6f468f478f79205aa5ef399, session75091, two threads. Independent API/correctness review and joint supplier publication pending. AI-assisted by OpenAI Codex, codex-dijkstra-native-learning-20261102. * refactor(dijkstra): use the relocated pure heap footprint * refactor(Dijkstra): derive the log-linear endpoint from native realization Retain the exact existing LogLinearStatement while deriving its fixed program/factor from Native.Binary.exists_program_state. Retire the old heapDijkstra and literal200/230 implementation-specific helpers explicitly; those clock coefficients are not claimed for the new native program. Retain Renfei Zhou source credit and the exact original sample, parallel edges and edgeless fixtures. Check actual native Runs/halt with a uniform clock factor, exact result vectors and frontiers29/16 under the same code. Delegated author follow-through under2288, only LogLinear and its test. Strict focused3660 and hygiene/whitespace PASS. Parent owns combined full validation, outside review, bridge assessment and legacy heap retirement. No full-six, publication, supplier approval or abstract change inferred. AI-assisted by OpenAI Codex, codex-dijkstra-loglinear-native-learning-20261102. * fix(realize): scope tactic syntax to WordRAM Delegate codex-realize-scope-crypto-20261102 under #2297/#2300. Preserve the complete inherited elaborator body and all other source entries. A private import no longer activates realize outside Cslib.WordRAM; both namespace and scoped opens activate it. Validation: strict six-target focused build, session 82324, passed 3646 jobs; targeted hygiene and whitespace checks passed. New parser rejection and positive read-certificate regressions pass; unchanged R1/While/Framed/Call/OptionPair suites pass. Exact original-source no-output probe confirms the old global availability. No default full-six or public update is claimed. Original Samuel Schlesinger source credit is retained. AI assistance: OpenAI Codex. * refactor(binary-heap): retire the replaced raw execution layer Remove the three obsolete heap execution modules after the actual raw native certificate, original allocated Dijkstra client, public log-linear statement and replacement clients have checked together. Retain the relocated pure Model/Order definitions and their source credit, the original graph/word/clock headline, and shared GenericPQ/PQCode/HeapStatement consumers. Replace the old heap interpreter fixtures by certified executions preserving their zero-key/absent lookup/tie/decrease/extract/empty and actual dirty-clear cases. Per-call halts are charged; external argument delivery and host control remain the existing operation-call convention. The old literal register and instruction constants and Dijkstra's implementation-specific 200/230 helpers are explicitly superseded rather than claimed reproduced. Validation: combined replacement clients and unchanged Dijkstra abstract audit PASS3732 before and after removal; heap client PASS3624; targeted hygiene and canonical imports PASS. Private final default check and exact outside review remain pending. The proof-only imported realize registration requires the separately owned scoped-syntax fix before public readiness. AI assistance: OpenAI Codex performed the migration, reusing Renfei Zhou's semantic/model work and the credited Kernel/Learning/Crypto author packets. No standalone heap PR, publication, approval or broad2205 completion claim. * test(dijkstra): keep abstract imports outside the realization scope * doc(roadmap): record the landed bounded queue migration * doc(BinaryHeap): explain native heap and Dijkstra entry points Update the Operator's Manual endpoint page with public imports and complete native clients, concrete fitting/initialization paths, standalone/free-delivery versus whole-client costs, raw-input placement and retired implementation APIs. The mathematical headline and exact reviewed Lean source remain unchanged. Manual impact: Operator's Manual changes the concrete API/model reader path. Agent Operator's Manual needs no edit: roles, delegation, authority, review and handoffs are unchanged. No converter/layout changes or new Lean examples. Memory reference remains unchanged for its retained owner. Validation: both Python manual checks and whitespace passed on these bytes. The affected-page render follows this clean committed source for provenance. Source/API approval2288#6584896472 is reused; manual delta review and later current-main/2300 integration gates remain. AI assistance: OpenAI Codex. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…-community#2344) * feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of #2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): weaken and rescale amortized refinements Amortized.mono and Amortized.mul_left (exchange at a constant rate, #2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): make Refinement.Amortized a structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: array stack over memory and queue method lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Foundations): affine cost bounds are O(size) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: queue over memory Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): product answer types via Sum.elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): queue over two array stacks over the memory oracle The M1 slice of #2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): certify compositional register-word glue Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone #2210; the memory realization kernel and vertical-slice gate remain in #2205. Validation: final staged tree a1b88e3fd1cc5e72a9a105865df17fa04295710e passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending. * feat(WordRAM): realize memory queries with uniform bind and glue Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of #2213 under #2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved. * fix(WordRAM): normalize the memory return simp rule * feat(WordRAM): realize bounded loops and initialized client programs Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under #2213 and #2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged. * feat(WordRAM): derive global and framed implementation certificates Project the four fixed memory-query bodies into the existing semantic StateTransitionImpl interface with explicit delivered-argument preparation and body-only cost bounds. Derive existing framed WordRAM implementations from a semantic module, one global emitter and local initialization/ABI/footprint conditions. Runtime argument maps do not choose a new emitter per object. Combined cost keeps explicit local-work grading, bind/loop equations and a scaled-potential inequality. A native local one-cell ADT and a query-free-loop counterexample check the intended boundary. Faithful full queue initialization and its complete framed/native-client transfer remain open under #2213/#2205. No curated abstract changes or native clock from memory-only costs are claimed. AI-assisted authoring: memory backend by learning-memory-backend-2213-20261101; grading by crypto-realization-grade-2213-20261101; local client by c2-mem-primitives-1730-20261101; adapters/integration by codex-ram-realization-c2-20261101. All new public API needs outside-fleet review. * feat(WordRAM): realize runtime-layout memory-stack methods Stage multiword results from fixed scalar-glue witnesses, charging every coordinate and output copy. Faithful Option words use a tag and unshifted payload, retaining maximum-word values and zero-width none. Consume the unchanged published Stack.Memory methods over full runtime layout words. Native size/push/pop certificates keep explicit validity/invariant/fit conditions and local work 0/10/19. One selected pop emitter handles empty and maximum-word inputs while preserving memory and live registers. This is a bounded #2213/#2205 milestone. The framed queue and faithful allocated queue-client path remain open. No abstract selection or headline changes. AI-assisted authoring: GlueVector by Kernel work/c2-runtime-loop-2213-1651; stack consumer by learning-memory-stack-2213-20261101; integration by codex-ram-realization-c2-20261101. Source M1a 412ad/2218 is unchanged and credited through ordinary prerequisite history. Outside-fleet review remains required. * refactor(WordRAM): centralize realization history and word encodings Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact. * refactor(WordRAM): expose shared glue rules and infer stack push Address outside review5731265464. Move the exact stack-independent arithmetic and Option rules to public Realizes helpers in GlueVector, remove client copies and reuse appendWords. Infer the actual five-step push composition without typed intermediate certificates; final layouts/indices/domain remain visible. Statement meanings, clocks, source methods and tests are preserved. Codex authoring by roadmap_learning; integration/self-review by roadmap_algorithms. Ordinary parent merge carries2230a929 fix. Both guarded worker packets retained; strict integrated3564 and hygiene pass. Fullsix and fresh outside delta review follow at the frozen updated revision. No selected abstract impact or broader M1 completion claim. * feat(WordRAM): realize tactic for memory-client realizations Add `realize`, which proves `Realizes B p input output safe work` for a loop-free memory client by walking its syntax: bind, pure, the four memory queries, `if` on a word comparison and `match` on an optional answer. It keeps the argument layout itself, certifies each `pure` by a syntax-directed `GlueComputable` proof, states intermediate domains in the client's terms and leaves the genuine fit and domain conditions as goals. `Realization/Absorb.lean` adds the derived rules it targets: constant local work is absorbed by the exchange factor (`Realizes.mono_mul`), giving `bind₀`, `branch₀` and `pure₀`, plus `Realizes.congr` and the `WordEncoding` class for intermediate answers. Refs #2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): loops whose body issues a query in realize Generalize `Realizes.mono_mul` to local work dominated by the memory charge, and add `Realizes.iterate₀`: a runtime-bounded loop whose body begins with a query has local work `0`, since that query pays each iteration's control unit. `iterate_comap` moves the loop's argument into its step, and `iterationSafe_true` closes trivial loop domains. `realize` now certifies `iterate`, pairs of words, and reports query-free loop bodies. Refs #2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a whole stack client to a flat program via realize Add `blockWords` and its `WordEncoding` instance, so binds may return blocks and layouts. `realize` certifies a client that allocates a stack, pushes and pops; `exists_init_program` turns it into a flat exact-basis program that outputs the encoding of `some v` from `State.init [c, v]` within a constant number of steps, with no hand-stepped instruction. Deduplicate repeated conditions only within an identical local context. Refs #2205. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): extract the static input reindex leaf Copy the exact existing Realization/Reindex.lean from PR2249 at66650221 onto fixed PR2246/383a52021, avoiding old queue-client dependencies for C5/C6. Original Gitblob18aea578f32743c7f03563931e54f08e111d1728, SHA25646541639a7334403b7dd5b325ca129e4162a433bf02981b2ca258a609496f165. Keep the original Samuel/Codex header, public API, proof and credit unchanged. Add its canonical aggregate import and an actual native read/frame test: select the second environment word, return maxword15, preserve unused7, the entire memory and frontier, with unchanged query charge. Worker codex-reindex-leaf-learning-20261102 under root/Algorithms #2266, #2213/#2205. This removes a concrete C5/C6 dependency blockage; it is not a broader realization/migration endpoint or an approval of the existing API. No selected abstract/catalogue/rendering impact; pins and docs unchanged. Validation: all six default scripts/check.sh gates PASS,2threads, exact frozen content; focused strict leaf/native test3536 and hygiene PASS. Fresh outside-authoring-fleet API/correctness review is required and will be shared by2249/C5/C6. No original parent refs are modified by this layer. AI assistance: OpenAI Codex for extraction, regression and validation. * feat(WordRAM): realize measure-bounded early-exit while loops Add a finite Memory.Prog while representation and one uniform native Code.loop certificate. A source cutoff depends only on explicit initial input; reached-state rank and safety prove truncation is unreachable. Charge actual continuing bodies/control and initial/final guard overhead, including query-free loops; retain potential in the semantic cost telescope. Reuse existing Realizes, Cond, native loop rules and copyBank without a new language or judgment. Default scripts/check.sh all six gates and focused strict library/test checks pass on exact staged tree 2e3c80c721b86735949299d1885499734290d6b9, two threads. No selected abstract impact. Refs #2259 and #2205; the broader gate and heap migration remain open. AI assistance: Codex worker codex-c5-while-1651-20261102 under coordinator delegation; independent outside review is required. * fix(WordRAM): destructure the loop argument in Realizes.iterate₀ #2246's iterateRuntime now binds its argument by a destructuring lambda, so iterate₀ matches the components before omega. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): native backends for memory refinements, one realized body per constructor Realization.Backend generalizes MemoryBackend: from a Refinement D (Memory.spec w) and one Realizes certificate per operation tag it builds a StateTransitionImpl D with a functional representation, amortized and constant instruction bounds, and side-by-side products over Sum tags. Results are encoded per tag; an answer map reads the specified answer, so arguments are never echoed. Realizes.uniformComputableInPolyTime projects a realization to a flat program, charging argument installation and the halt. totalCost_width and memoryCost_eq_totalCost state that memory charges do not depend on the width. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(tests): wrap long lines in the backend test Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): Backend.data, rep_data and fits_appendWords Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): backend test uses fits_appendWords and Backend.data Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * perf(WordRAM): state realize certificates per form in the client's terms `realize` compared its synthesized domain with the composed rules' domain once, at the end, by definitional unfolding. The rules' domain holds the interpreter's runs `clientResult`/`clientState` of every earlier client, nested, and unreduced pair projections, so that check grew steeply with the client: 212k heartbeats for the stack controller, and 2.5M when a bind's first client ends in a `match`. Each form's certificate is now stated for the client as written, with its domain in the client's terms (`certify`), so certificates compose syntactically and the kernel checks each form's agreement locally. A bind's continuation domain is stated at the first client's reply and next memory in closed form (`Realizes.bind₀_of_run`). Result encodings are proved by `Fin.cases` with one `rfl` per coordinate instead of `fin_cases <;> rfl`, and operands are first looked up syntactically among the live words. Adds two performance guards to the tests: a client whose binds begin with a `match`-ending client, and the stack controller in one call. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): export initialized flat programs with a standard layout Choose private canonical frontier/input/scratch banks once and project an existing Realizes certificate through the actual charged Data.init prefix, Code.program and halt. The stateful export retains the actual flat Runs, full source memory/frontier and every encoded result word; the scalar Executes corollary removes caller register-layout proofs. Its fixed code, output placement, halt PC and factor precede every runtime width/input. Keep the same raw-layout, length, fit, safe-domain and admissibility premises and C*(memoryCost+work+1)+1 bound. Empty input still requires frontier one to fit; no initialized width-zero case is claimed. The checked initialized-copy client block drops48 to20 lines with its statement unchanged. An actual write/read client checks full post-memory and maximum payload15; the empty-input case retains positive frontier fit. The original Program.lean and all its public interfaces remain exact SHAeeb7346b2d483bede91259eb6f03f50b7b494a735c264a2293e993bf0d800db2. Existing Program/native-prefix source credit remains unchanged. Worker codex-c5-canonical-program-learning-20261102 under root/Algorithms #2279, #2205/#2213, fixed published2230/a929a76f. This is a bounded C5 usability milestone, not a new compiler/language/model or broad completion. Static Fin l observation retains the existing scalar-output scope; zero-output Unit exports remain separate. No selected abstract impact. All six default scripts/check.sh gates PASS,2threads, exact frozen source; strict focused3546, hygiene/check-simp/whitespace and source/pin guards PASS. Fresh outside-author-fleet correctness/API review is required. No own approval or parent source/ref changes. AI assistance: OpenAI Codex. * fix(WordRAM): adapt private R1 iteration proof to corrected loop Reuse the unchanged proof body from approved PR2277/fb0bf094. All public statements and tactic code are unchanged. Strict Absorb and unchanged WordRAMRealize regressions PASS3578; 40k budgets retained. Private prerequisite only; canonical R1 owner handoff on PR2280. * chore: regenerate the aggregate import after merging #2270 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * chore: drop imports the merge duplicated in Complexity.lean Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): state iterate₀ in iterateRuntime's named-component form #2230 restates iterateRuntime with pattern lambdas over ((d, a), fuel) and appendWords; iterate₀ follows, which also removes its positional projections (#1764). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): framed backends - frames, products over one memory, allocation A backend of a framed refinement carries its frame over: a native operation writes only the footprint and the reserved room (Backend.modifies), and keeps disjoint assertions and structures kept apart (frame_heap, frame). Backends of framed refinements run their product over one memory (Implements.prod_framed), each side within its own region (modifies_inl, modifies_inr). Backend.Allocation names the tag that runs a Memory.Allocator's program; Allocation.exec allocates from arbitrary bounded data within the allocator's cost, writing only the room it takes. Backend.extend adds such tags; install and exists_exec run any tag's body. The memory side is a new leaf, Memory/Region. The stack test restores modifies/frame, constant-time allocation and allocate-then-run, and two stacks over one memory. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): allocate a pair of stacks in one body realizes_allocTwo certifies the allocation of two stacks, one after the other, as Memory.Allocator.prod does; with Backend.extend it becomes the allocation tag of the pair's backend, and allocate_pair sets up both empty stacks from arbitrary bounded data in constant time. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): guarded loops in realize realize now certifies boundedWhile G step D n a whose step begins with a query. The guard is a word comparison (a = b, a < b, a > b, or a ≠ 0 tested as 0 < a) over the live and state words, with any decidability instance; an operand independent of the state is computed before the loop, and the cutoff stays a ghost bound. The certificate is transported back to the client's guard, step and environment, so the loop's domain is whileSafe in the client's terms, under the loop's valid history, ready for whileSafe_of_measure. New leaf Realization/WhileAbsorb: boundedWhile_congr, whileSafe_imp/congr, whileWork_congr (guard, body and environment congruence), the envelope whileWork_le, whileWork_zero_le and the absorbed rule Realizes.while₀. Absorb gains Realizes.consequence_valid. Tests: a memory-reading countdown (also with r ≠ 0 under a classical instance), the queue's transfer over two array stacks counted down by the items left, and a sift-shaped descent with logarithmic rank, plus controls. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * style(WordRAM): wrap a long line in the realize loop tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(WordRAM): use appendWords for the stack client's environments #2230 makes appendWords public in Realization.Basic; the stack client's private append was a copy of it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(WordRAM): keep iterate₀'s statement, as in #2277's proof-only repair The proof body alone needs the change for #2230's iterateRuntime. Keeping the statement byte-identical to #2277 lets the two branches merge without conflict. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a heartbeat budget for the realize transfer loop Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(WordRAM): checkpoint sift-up realization for heap migration Internal building block for #2282, not a standalone native heap PR. Reuse original Memory.siftUp with exact FreeM/history/cost transport, R1 scalar/bind/branch compilation and C5 early-exit while. Uniform code before all runtime n/layout/width/index/memory. Native body time is bounded by a fixed factor times log n plus one, with full source memory and caller frame. Installed-argument ABI only; no bit-cost, complete heap or improved space/step claim. Strict focused library and three same-emitter native edge fixtures PASS3582; hygiene and whitespace PASS. No full-six claimed. Canonical parent/R1 compatibility publication and outside API review remain gates. AI-assisted implementation by Codex; original heap and supplier source credit retained. * test(WordRAM): place the transfer loop's heartbeat budget before its docstring Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * test(WordRAM): a realize loop whose guard and step capture the environment Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(BinaryHeap): support compact locally initialized memory layouts Internal #2282 migration obligation: the existing Layout may hold its count at unused heap[0], retaining legacy3n+1 space. Generalize HeapInv.congr_mem to ignore only that unused cell, carry the stronger source invariant/count-update proofs through every existing caller, and expose the same-layout compact specialization plus local-zero empty-invariant rule. Original allocator/program semantics and old native statements/clocks remain unchanged. Renfei Zhou source credit retained. Strict focused Memory/original tests/native sift fixtures/legacy BinaryHeap all PASS3598; new edge tests cover n0/base0/w1 andn1/base3/w3, real insert/extract and dirty outside cells without globalZeroAbove. Hygiene PASS. No native initialization or full migration/deletion/full-six claimed; fresh outside API review required. AI-assisted by Codex. * refactor(BinaryHeap): share runtime encodings for native migration Move the unpublished sift building block into the application Native leaf. Share the identical existing runtime Layout encoding plus faithful typed-handle inclusion, before every runtime n/layout/width. This supplies both sifts and method family clients without a parallel layout or successor sentinel. No old native heap code is removed. Strict focused encoding/sift/nativefixtures PASS3586 and typed-handle mapping PASS; hygiene/whitespace PASS. Full migration and native setup/Backend/wholeDijkstra obligations remain open; this is not a standalone PR. AI-assisted by Codex. * feat(WordRAM): export fixed programs over independent raw memory Generalize the existing canonical initialized whole-state export so raw input words vary after the program, register layout and exchange factor are chosen. The pointwise input-prefix equation relates them to the faithfully encoded argument. Preserve both existing theorem statements as wrappers. The Dijkstra consumer checks one program over every adjacency-list encode with Unit register arguments, plus two different graph memories and a maximum fitting edge weight. Original Program.lean, dependency pins and abstract catalogue are unchanged. All six default scripts/check.sh gates pass at exact tree36ae8037ff716ea9e1c58187285caf3848e0127e (2 threads); focused3572 and hygiene pass. AI assistance: OpenAI Codex, session codex-dijkstra-native-learning-20261102. Refs #2281, #2288. * refactor(binaryheap): absorb actual sift-up control work Reuse the canonical whileWork_zero_le rule. The public certificate retains the original source family, safety domain and exact memory behavior while queries pay the bounded local grade. Focused native sift and unchanged fixtures pass; no full validation or migration completion claimed. * wip(WordRAM): freeze option-pair implementation during gated repair Private checkpoint for #2291. Initial focused option clients pass; extended legacy-normalization and native-budget tests currently fail and remain to be repaired. Not a submission or validation claim. * feat(binaryheap): realize existing constant-time read methods Use the canonical realize rules and shared runtime layout/handle encodings. Tests execute the same selected code on present and absent handles at maximum key 15, preserve full memory/frontier and retain constant read-method budgets. Arguments remain installed; full heap migration, initialization and outside review remain pending. * refactor(binaryheap): accept runtime handle words in source methods Generalize three existing Memory program arguments from Fin n to Nat, leaving program bodies and all typed indexed-operation/correctness declarations unchanged. The word certificate states v<n explicitly; the typed lookup certificate derives by static reindex. Focused source, legacy native, compact-domain and max-word native regressions pass. Fresh outside API review remains required with the migration. * fix(WordRAM): preserve scalar encoding normal form in generic option support Keep the legacy OptionNat embedding and instance, connect it to the shared payload embedding, and check same-body none/max-payload executions. Focused pair/legacy clients passed3586 before the added definitional-instance guard; no full validation or public submission yet. * feat(binaryheap): compose native source update methods Realize the original insert/decrease prefixes with shared R1 rules and statically compose the uniform sift-up certificate. Entry domains reuse the original heap invariant and indexed-PQ validity. Native max-word insertion/decrease and negative domain clients pass; common test-only packing removes repeated ABI plumbing. Focused strict checks and hygiene pass; full migration, initialization, backend and outside review remain open. * chore(binaryheap): refresh canonical imports for native checkpoint * feat(BinaryHeap): realize source-faithful sift-down through shared loops Private #2282 delegated author slice. Preserve the complete original memory program, including four mandatory reads, optional right-child reads, strict handle ties and original four-write swap. Use the existing Realizes/Code.loop route, input-only logarithmic ghost cutoff and a paid initial zero guard before threshold preparation. Lift the source order/rearrangement theorem with explicit allocation, fits, installed-argument ABI and native frame. Validation: focused strict library/test PASS (3586 jobs); hygiene --check-simp and staged diff checks PASS. Same-emitter native left-only, read-then-stop, tie/right and width1/n0/index0 fixtures; dirty cell retained. Providers, pins, abstracts and old endpoints unchanged; no full-six, publication, deletion or migration-completion claim. AI assistance: OpenAI Codex under Algorithms coordinator delegation. (cherry picked from commit 526575bc59baf2bb9b9b59f4ba1a1d94ef45913a) * refactor(binaryheap): reuse shared width transport in native sift Replace the delegated private width/charge transport with the approved Backend fact after its ordinary dependency merge, leaving all public statements/source/code/tests unchanged. Integrated focused sift/native regressions pass3602 and hygiene; imports regenerated. Previous eb0145 all-six receipt is not claimed for this expanded dependency tree. * feat(WordRAM): reuse static method certificates and linked runs Add call-site dispatch through existing Realizes.reindex and a small full-run linking congruence leaf. Tests cover opaque uncurried calls, reached-state domains, charged arithmetic staging and complete adaptive memory histories. Original realize/while suites pass unchanged. All six default checks pass at exact tree0b27a9790e6718825abdaf686f3849fff918c002, session7009/2threads; focused3590/2036 and hygiene pass. Known consumer gap: curried functions wrapped in a tuple lambda still need constructor-skeleton matching before publication. This is not the native Dijkstra endpoint. No abstract, pin, original Program or Reindex changes. AI assistance: OpenAI Codex, codex-dijkstra-native-learning-20261102. Refs #2288. * feat(BinaryHeap): certify compact reservation and layout word primitives Private delegated author slice under #2282. Realize exact allocDirty(space n) using addition spelling to retain n0/w1, and compute the faithful [n,base+n,1] vector using existing charged pure/scalar glue. Native projections retain full memory, frontier/input frames, exact old-front return and one fixed emitter before runtime inputs. Link local zero after actual reservation to the existing compact empty invariant. Validation: strict focused library/test target PASS3582, hygiene --check-simp and staged diff checks PASS. Same witnesses cover n0/base0/w1 and n1/base3/w3/end7 with dirty outside preserved, and stale-position rejection. No full wrapper, legacy11/rBin25 equivalence, generic localPre allocator, source allocator change, full-six, PR or push. Existing providers/pins/abstracts unchanged. AI assistance: OpenAI Codex under Algorithms delegation. * fix(WordRAM): match packaged curried method calls Build only pair and dependent-pair argument skeletons before matching a local uniform Realizes certificate. Keep other argument values undetermined until the source call fixes them, and retain the static live-word wiring and zero-work policy. The actual original Memory.siftDown call with a runtime Sigma layout now passes a direct kernel check without unfolding recursion. Production regressions cover curried scalar calls and an opaque curried optional-pair extraction. Original realize/while and optional-word clients pass unchanged. All six default checks pass at exact tree441c917c2daaf4f6dcdf0b4aca2fc326ad7220bc (session35315,2threads), in the ordinary merged public2294 context; strict focused3596/hygiene also pass. Earlier7675 validation covers only its own older tree. No abstract/pin/model changes. AI assistance: OpenAI Codex, codex-dijkstra-native-learning-20261102. Refs #2288. * feat(binary-heap): realize the existing layout allocator Keep the original two dirty queries, 3n+2 layout and memory history. Place only the returned dependent layout into the existing HeapLayout sigma encoding for uniform code. Add same-emitter width, nonzero-frontier, dirty-memory and global-zero fixtures. AI-assisted delegated worker slice under #2282; codex-heap-init-primitives-1651-20261102. Focused strict target and hygiene pass. No full-six, raw ABI wrapper, old clock equivalence, abstract changes or approval claimed. * refactor(FibonacciHeap): expose memory iteration source forms F1 source checkpoint for #2290, not a completed native migration. Preserve exact linked memory programs for gather/scatterList iteration and cascade/scatter stop/continue steps, including original fuel truncation. Query-cost lower bounds retain the real memory currency needed to pay loop control. Nine oracle-program regressions cover empty/occupied slots, preparation, cascade stops, zero fuel, maximum words and dirty cells. One default scripts/check.sh passed all six at frozen tree452b14f2 on base6ecc with exact CSLib254e/Mathlib6955 pins, two threads; focused strict tests, hygiene and whitespace also pass. No native instruction-bound, migration-completion, source-method, model, abstract/catalogue or deletion claim. Legacy core remains until F1/F2 consumers migrate; outside-fleet review is required before integration. Preserve Renfei Zhou and Claude source credit. AI assistance: OpenAI Codex. * chore(WordRAM): canonicalize supplier import order Source-only composition of original2288 supplier head73704c97, published2268/b32e8357,2281/1e77082f and2294/2eb7dc04. No owned2297 call/link payload is included. Canonical import order matches the all-six-validated current composition with LinkCongr absent; pending supplier correctness/API/integration gates remain separate. AI assistance: OpenAI Codex, codex-dijkstra-call-link-learning-20261102. * feat(WordRAM): retain Backend register frames for live-input execution Expose existing shared packing facts and install identity under actual live words; derive a full-frame execution result and raw-live corollary from the same Realizes code_spec. Existing definitions and all previous theorem types are unchanged; exists_exec projects the stronger proof. Tests exercise different result widths, paid zero staging, zero/max-word inputs and a genuine memory-read provider. Under #2298 for queue #2284 and heap #2282; inherited Claude source credit retained. Strict focused3628 and hygiene pass; full-six/outside review pending. * feat(wordram): realize original heap extraction and assemble its backend Private #2282 migration checkpoint. Exact original extraction is observed through the checked typed entry constructor, with complete state/history transport. Native tests include empty width1, maximum key15 and a real root-removal sift swap. The existing Backend supplies constant read/logarithmic update body bounds and source footprint preservation. Focused source/fixtures and hygiene passed with exact borrowed Learning call matcher SHA5f8a3d1d. That separately owned pending prerequisite is not included in this commit; this is not a standalone public revision or full-six claim. Shared initialization, raw argument delivery, the full native Dijkstra migration, outside review and legacy deletion remain open. AI assistance: Codex/GPT-6. * fix(realize): match dependent method arguments after charged staging Solve same-head call arguments in binder order, retaining static live-word wiring and reached-state domains. Add the dependent scalar/pair staging regression from the original heap extraction consumer. Validation: default scripts/check.sh, LEAN_NUM_THREADS=2, all six gates pass at tree 3ee50d45a0f805b657efc51edaff1c8d71a37760 (session46520). Original curried/OptionPair/realize tests and actual heap extraction scalar/pair staging pass. Abstract assessment: no selected statements or scope changed. AI-assisted by OpenAI Codex. Part of #2297; the broader native Dijkstra endpoint remains #2288. * feat(wordram): compose the compact heap initializer on its native ABI Private #2282 migration checkpoint. One existing PQCode register family includes all five method bodies plus the certified reserve and metadata routines before runtime n/base/width. Actual initialization preserves the complete old memory and the legacy 3n+1/local-zero domain, with paid constant reservation and setup. Same-code width1/capacity0 and width3/base3/end7 fixtures pass. Strict focused source/native fixtures PASS3614 plus hygiene. Canonical pending #2300 and #2299 source parents are ordinarily merged, not authored here. Dispatcher correctness, full SubroutineBase/dirty initialization/client clocks, native Dijkstra, outside review and final legacy removal remain unfinished. No full-six claim or old instruction/register constant is made. AI assistance: Codex/GPT-6. * feat(wordram): expose the compact heap ABI observations Add the five exact frontier/dimension/base/input-mask observations required by the delegated finite-footprint representation proof. Existing code bodies, encodings, clocks, domains and tests are byte-preserved. Keep the implementation opaque and export only its proved metadata facts. Strict focused source and original raw initialization tests PASS3614; hygiene passed. This follow-up is not covered by the earlier8004 full-six receipt; final combined migration checks/outside review remain. AI assistance: Codex/GPT-6. * feat(binary-heap): specialize Backend representation to compact raw storage Use the existing extended Backend representation and add only the four persistent layout words. Derive boundedness, finite-block support and the actual local-zero initializer bridge, keeping the original 3n+1 end-fit domain and whole-memory identity. Delegated worker codex-heap-representation-1651-20261102 under #2282. Focused strict target (3616 jobs), hygiene and diff checks pass. Explicit c9addcf45 application ABI supplier; no provider edits, full-six, publication, legacy-clock or full migration claim. AI-assisted source and tests. * feat(FibonacciHeap): realize the read-only native methods Use the existing realize calculus for uniform runtime-capacity/base/handle isEmpty and getKey programs. Preserve the exact linked record source, two-word Boolean/optional-key encodings and unshifted maximum-word keys. One actual native lookup test starts after the existing allocator and insertion source, returns [1,31], retains input31 and leaves frontier25. Keep realization types as explicit public imports and the tactic as a proof-only import. No new PQ model, solver, method-family or whole-migration claim; #2290 and both consumer/core-deletion obligations remain open. Selected abstracts and the F2 space decision are unchanged. Validation: strict focused modules/tests PASS and hygiene --check-simp / whitespace PASS at tree ab204b7bb61da88bf5227852e35ad702efee34c2. Current all-six intentionally deferred by coordinator until a coherent five-method Backend checkpoint. Earlier full-six at be6d7fb4 applies only to initialization; it does not validate this current tree. AI assistance: OpenAI Codex. Outside public-API review remains required. * feat(wordram): verify live heap method argument delivery Prove the established three-bit PQ calling convention supplies the selected original method input words from actual persistent layout and payload registers. Uses existing cross-tag Backend source-position facts, without a free prepare step or compiler change. Expose only the pure five-case backend tag/argument/observation record needed by the concrete caller; all method code, domain and cost meanings are unchanged. Strict focused Program PASS3612 and hygiene passed. Later current-combination tests/outside review remain; no reuse of8004 full-six as this revision evidence. AI assistance: Codex/GPT-6. * feat(wordram): retain the source extraction result in the raw observation bridge Expose exact result erasure alongside full typed run/state/history transport, so the native PQ decoder can recover the original bounded handle without an extra successor encoding or fit premise. Register the delegated finite-footprint representation in the canonical aggregate. Integrated Backend/Extract/rawProgram/Representation and actual source/native fixtures strictPASS3624 plus hygiene. No new kernel, source algorithm, prepared-call complexity, current-full-six or full-migration claim. AI assistance: Codex/GPT-6. * feat(priority-queue): add equations for the existing word-RAM decoder Expose Boolean, absent/present key and typed extraction equations over arbitrary PQCode without changing its decoder. Concrete global heap-code fixtures retain nonzero flag semantics, unshifted maximal keys and handle-range rejection. AI-assisted worker codex-pq-decode-1651-20261102 under #2282. Strict focused target3616, hygiene and diff checks pass. Existing providers and Representation32fd stay exact; no full-six, native-operation execution or public integration approval claimed. * feat(dijkstra): preserve linked source in word-level loop views Private #2288 development checkpoint. Exact FreeM equalities preserve all queries, reached memories, malformed-target fallback, original addition guard and empty-queue exit. The binary instance keeps the original allocator and recovers Memory.run exactly. Existing semantic refinements and checked entry observation are reused; no new backend, decoder or execution model. Strict focused source/tests PASS3604 and hygiene. Concrete tests retain both zero-degree offset reads, one empty extraction despite37 available rounds, and the invalid-target zero-weight fallback with all writes/state. Native realization/domain/clock proofs, outside review and endpoint/deletion remain unfinished. No abstract impact. AI-assisted by OpenAI Codex; original supplier and Claude design credit retained. * feat(wordram): certify the heap ABI for generic linear clearing Prove the five clear-register distinctness, retained runtime dimension, and existing exact increment semantics required by SubroutineBase. No code, allocator, memory representation, domain, or clock definition changes. These facts let the existing shared initializer clear dirty storage honestly in linear space. Strict Program/Representation source/native targets PASS3616 plus hygiene. Full SubroutineBase and method dispatch still under construction; old8004 all-six is not this revision. AI assistance: Codex/GPT-6. * fix(WordRAM): expose Backend extension and preparation metadata Expose only the existing pure extend record and prepare alias so real heap bounds and conditional already-live entry elaborate without local record copies or dependent observation wrappers. All definition bodies/types, code/arg/rep/resource meanings are unchanged. Generic bound_extend and actual-live operation-entry regressions pass with the old clients; full new-head validation/review pending under #2298. * refactor(wordram): account for the raw heap dispatcher wrapper Private compositional helper lifts an actual selected body execution through the existing zero staging, three conditional tests and lookup result-key copy. The wrapper costs at most six additional native instructions. It does not assume a free prepare, reimplement a heap instruction, or establish an operation without the supplied body certificate. Strict focused Program PASS3612/hygiene. Internal helper for pending complete raw method proof; no public heap endpoint/full check or completion claim. AI assistance: Codex/GPT-6. * feat(binary-heap): package compact raw initialization as SubroutineBase Reuse the existing global Program, Backend representation and standard priority-queue ABI with only original end-fit and key-fit premises. Setup executes the existing metadata routine without reserving again. Charge metadata awaits separate method execution. Fresh one-bit and actual linear dirty-clear fixtures preserve outside memory; every original four-cell owned location is cleared with the shared zeroFillCode rule. AI-assisted delegated worker codex-heap-base-1651-20261102 under #2282. Strict focused3618, hygiene and diff pass; no full-six, StateTransitionImpl, old clock, source publication or approval claim. * feat(wordram): lift native heap bodies through the charged raw ABI Use the existing family extension and conditional live entry API. Bound the extended operation bodies with the same per-operation source charges. Account for the actual dispatcher/control/key-copy overhead and preserve full memory, frontier, layout and typed-result slots; stage-zero facts keep actual live inputs and source memory intact. Register the delegated Base and existing decoder lemmas. Integrated source/rawProgram/Base/Rep/decoder/BackendLive fixtures strictPASS3636; subsequent Program/Base source+native targets PASS3618 and hygiene. This is still private proof plumbing for the pending closed method StateTransitionImpl; no heap publication/deletion, new full-six or outside approval claim. Canonical provider73f public2299 and754a public2300 remain independently gated. AI assistance: Codex/GPT-6. * feat(wordram): expose the existing common heap source positions Add the single argument_source observation requested by the raw method-frame consumer. It reveals only the existing source-coordinate identity, without exposing or changing emitted code, counts, domains or layouts. Strict Program/Base/native validation PASS3618 and hygiene; final combined/outside gates remain. AI assistance: Codex/GPT-6. * feat(binary-heap): certify actual raw native priority-queue methods Extend the existing opaque SubroutineBase using live Backend executions, source correctness and bounds, and the paid raw dispatcher. Preserve exact source memory state, typed extraction, the compact footprint and the original end-fit/key-fit domain. Argument matching remains an explicit uncharged calling convention. Same global program fixtures cover capacity zero at one bit, shifted-base maximal-key insertion, noncanonical tag7 lookup, decrease and typed extraction, with outside sentinels and actual body charges. AI-assisted delegated worker codex-heap-implementation-1651-20261102 under #2282; strict focused3622 and hygiene/diff pass. No full-six, publication, old numeric clock/register or complete-client/migration claim. * feat(binary-heap): retain standalone realized client certificates Project the actual raw heap implementation through the existing standalone DynamicCertificate and adaptive-client APIs. Preserve the compact fit/local-zero domain, typed observations and halt-inclusive call costs. External argument delivery and host continuations remain outside this operation-call model. The retained insert/tie/decrease/extract regression starts from actual native initialization. No legacy heap deletion or standalone migration PR is implied; the joint native-Dijkstra retirement and outside review remain open in #2282. Validation: strict focused certificate/client PASS (3624 jobs), targeted hygiene/check-simp and canonical aggregate PASS. Private combined default-six checkpoint pending. Abstract/catalogue/rendering: no impact; no headline added. AI assistance: OpenAI Codex authored the certificate projection and adapted the existing Renfei Zhou client regression. Kernel's separately credited raw implementation remains an unchanged parent commit. * refactor(binary-heap): place the retained memory model with its clients Move the existing Model module and its namespace to PriorityQueue.BinaryHeap; move the existing Order namespace with it. Preserve all declaration bodies and Renfei Zhou/Samuel Schlesinger source credit, and update every current client. Six retained legacy Sift proof calls use explicit qualification after the type namespace move; their statements and algorithms are unchanged. The old native Program/Sift/top-level implementation and Dijkstra consumers are still present. Their retirement remains gated on the jointly validated native Dijkstra replacement and outside review in #2282. No old clock/register bound or migration-complete claim is made. Validation: strict affected model/native/legacy/Dijkstra targets PASS3678; targeted hygiene/check-simp, canonical aggregate and changed-line style PASS. New-tree default six pending. Abstract/catalogue/rendering: no semantic impact; no selected statement or headline changed. AI assistance: OpenAI Codex performed the mechanical move and proof-call qualification, reusing the earlier Kernel declaration/consumer inventory. * feat(Dijkstra): realize the allocated binary-heap client natively Realize the exact original memory program through faithful runtime word encodings, existing heap certificates and query-paid bounded-while rules. Derive one initialized flat program before all runtime graphs and widths, retaining the full final memory/frontier and the original word envelope. The prefix, arithmetic, calls, copies, control and halt are charged. The checked same-program client covers a singleton and a weighted graph with an unreachable vertex. Move the existing input-fit proof from the legacy GenericPQ implementation into ListEncode, updating its old client. Original Renfei Zhou/Samuel Schlesinger source and retained Claude design credit are preserved. Broader Fibonacci migration, fixed-coefficient API disposition and legacy retirement remain open; no abstract change. Validation: strict focus 3668 jobs, hygiene, canonical imports, whitespace, and all six default scripts/check.sh gates PASS on exact staged tree 506c18245df21098c6f468f478f79205aa5ef399, session75091, two threads. Independent API/correctness review and joint supplier publication pending. AI-assisted by OpenAI Codex, codex-dijkstra-native-learning-20261102. * refactor(dijkstra): use the relocated pure heap footprint * feat(FibonacciHeap): compose native insertion with source-faithful blocks Private F1 #2290 checkpoint. Reuse pending shared static reindexing and existing absorbed bind/consequence_valid rules; the full original linked source is preserved as a FreeM program. Capacity/base/handle/key are runtime words; the emitter, registers and exchange factor precede them. Source history admissibility remains intrinsic; raw handles stay below capacity. Strict focused library3590 and native regression3606 checks PASS. Four actual selected-emitter runs cover first insert, maximum five-bit key31, both handle tie orders and strict-key change with original memory/frontier/input retained. Hygiene/whitespace PASS. No whole-slice all-six or outside review; pending2268/2281/2294 remain unreviewed/unmerged, not actual-main APIs. Decrease/extract/backend and BOTH consumer migrations remain open. No selected abstract/catalogue or F2 space decision changed. AI assistance: OpenAI Codex, codex-fibonacci-native-circuits-20261102. * refactor(Dijkstra): derive the log-linear endpoint from native realization Retain the exact existing LogLinearStatement while deriving its fixed program/factor from Native.Binary.exists_program_state. Retire the old heapDijkstra and literal200/230 implementation-specific helpers explicitly; those clock coefficients are not claimed for the new native program. Retain Renfei Zhou source credit and the exact original sample, parallel edges and edgeless fixtures. Check actual native Runs/halt with a uniform clock factor, exact result vectors and frontiers29/16 under the same code. Delegated author follow-through under2288, only LogLinear and its test. Strict focused3660 and hygiene/whitespace PASS. Parent owns combined full validation, outside review, bridge assessment and legacy heap retirement. No full-six, publication, supplier approval or abstract change inferred. AI-assisted by OpenAI Codex, codex-dijkstra-loglinear-native-learning-20261102. * fix(realize): scope tactic syntax to WordRAM Delegate codex-realize-scope-crypto-20261102 under #2297/#2300. Preserve the complete inherited elaborator body and all other source entries. A private import no longer activates realize outside Cslib.WordRAM; both namespace and scoped opens activate it. Validation: strict six-target focused build, session 82324, passed 3646 jobs; targeted hygiene and whitespace checks passed. New parser rejection and positive read-certificate regressions pass; unchanged R1/While/Framed/Call/OptionPair suites pass. Exact original-source no-output probe confirms the old global availability. No default full-six or public update is claimed. Original Samuel Schlesinger source credit is retained. AI assistance: OpenAI Codex. * feat(FibonacciHeap): realize finite cut blocks and expose scatter while Private F1 #2290 checkpoint: native unlink, setKey, toRoot and cut use existing realization, source-history and static bind/wiring rules. Exact subtraction domains and actual intermediate memory are explicit; these are component certificates, not complete decrease-key/extraction. A genuine parent/child fixture is constructed by original indexed inserts and consolidation, retaining the existing full heap invariant. Its selected native cut matches all source memory, input and frontier with16 oracle queries. Positive/negative domain instances are checked. The exact finite scatter-to-boundedWhile equation preserves cutoff truncation and maximum degree; tests retain handle0 versus none and maximum accumulator31. Strict focused3620, hygiene, whitespace and canonical inventory PASS; no current whole-slice all-six/outside API review. The pending2268/2281/2294 supplier composition remains private/unreviewed/unmerged. Source-invariant transport, both loop nontruncation proofs, five-method Backend and BOTH consumer migrations remain OPEN. Pure models/pins/abstracts unchanged; F2 space decision remains with Samuel. AI assistance: OpenAI Codex, codex-fibonacci-native-circuits-20261102. * refactor(binary-heap): retire the replaced raw execution layer Remove the three obsolete heap execution modules after the actual raw native certificate, original allocated Dijkstra client, public log-linear statement and replacement clients have checked together. Retain the relocated pure Model/Order definitions and their source credit, the original graph/word/clock headline, and shared GenericPQ/PQCode/HeapStatement consumers. Replace the old heap interpreter fixtures by certified executions preserving their zero-key/absent lookup/tie/decrease/extract/empty and actual dirty-clear cases. Per-call halts are charged; external argument delivery and host control remain the existing operation-call convention. The old literal register and instruction constants and Dijkstra's implementation-specific 200/230 helpers are explicitly superseded rather than claimed reproduced. Validation: combined replacement clients and unchanged Dijkstra abstract audit PASS3732 before and after removal; heap client PASS3624; targeted hygiene and canonical imports PASS. Private final default check and exact outside review remain pending. The proof-only imported realize registration requires the separately owned scoped-syntax fix before public readiness. AI assistance: OpenAI Codex performed the migration, reusing Renfei Zhou's semantic/model work and the credited Kernel/Learning/Crypto author packets. No standalone heap PR, publication, approval or broad2205 completion claim. * test(dijkstra): keep abstract imports outside the realization scope * feat(FibonacciHeap): derive native cut domains from the source forest Private F1 #2290 checkpoint. Name the previous exact native cut predicate cutSafe and prove cutSafe_of_cascading using the original Cascading forest, present child/parent link, allocated record layout and word-fit window. The existing record refinement transports the original unlink run to literal intermediate memory; markedCount supplies the exact-subtraction inequality. No parallel heap model, new execution judgment or stronger global caller contract is introduced. Existing source/pure-model credit is retained. A genuine allocated source heap after3 inserts/consolidation applies the new bridge and retains the selected native-cut execution fixture. Strict focused3622, hygiene, whitespace and canonical inventory PASS. No current whole-slice all-six, outside review, ready PR or complete decrease/extract claim. Both loop nontruncation proofs, five-method Backend and BOTH consumer migrations remain open; original core and F2 abstract-space decision kept. Pending2268/2281/2294 are explicit private/unreviewed/unmerged dependencies. AI assistance: OpenAI Codex, codex-fibonacci-native-circuits-20261102. * feat(FibonacciHeap): derive the native cascade step rank from the forest * feat(FibonacciHeap): compile cascading cuts with the original forest rank * feat(FibonacciHeap): realize decrease-key on the original valid heap domain * feat(FibonacciHeap): realize consolidation links with shared record normalization * doc(roadmap): record the landed bounded queue migration * feat(FibonacciHeap): realize consolidation and preserve exact extraction erasure * fix(realize): retain captured loop environment words Fix #2317 in the existing private iterate frontend: substitute live environment captures as the while frontend does, then transport the exact original loop and reached-state domain with kernel-checked fixed-environment inductions. Preserve the noncapturing paths, public calculus and elaborator entrypoint body, original source program, visible fits/work and uniform emitter quantifiers. No new loop rule, model or public mathematical API. Strict focused session5788 passed3648 jobs: unchanged R1/While/Framed/Call/OptionPair/scope, original-domain opaque captured calls and one emitted body on two distinct runtime inputs with zero/two charged iterations/full memory preservation. Identical final regressions fail on exact old27e in output-free session68169. Hygiene/whitespace pass. Circuits directly checked unchanged original F1 Gather/domain/work and native n0w3 with input7 and Fits3 8 false; local acceptance receipt is linked from the issue handoff. No full-six or publication claim; original Samuel/Claude supplier credit retained. AI assistance: OpenAI Codex. * feat(FibonacciHeap): realize the original five-method family Private F1 checkpoint for #2290: complete original extraction, forest-derived domains, a fixed five-tag Backend, exact typed source/history transport, original-potential amortized charges and footprint preservation. Selected-emitter cases cover zero capacity at width three, maximum unshifted keys, a real child and root-list collision/mark preparation; typed backend client and strict focused checks pass. Hygiene and canonical inventory pass. This focused checkpoint was checked with the exact accepted #2323 compiler source 1b87 overlay, which is excluded from this commit and will immediately be retained by its separately authorized ordinary supplier merge. Current all-six, outside application/API review and full caller migrations remain open. Initialization, Dijkstra/MinPQ migration, legacy-core removal and Samuel abstract-space decision are not completed. Pure models, legacy clients and abstracts remain unchanged. AI assistance: Codex implementation and self-review. * doc(realize): explain scoped method calls and full-run transport Add the authorized reader path to automation.md: exact import and scope activation, local zero-work certificates, live-word reindexing, charged computed-argument staging and domains at the actual reached memory. Link the existing complete scope/call clients rather than copying Lean. Add the short LinkCongr reference in memory-specifications.md, retaining its complete answer/state/history premise and separate native-cost task. The landed Standard section remains verbatim; no other manual changes. Manual impact: update the Algorithm/Operator's Manual API/proof guidance. No Agent Operator's Manual edit: roles, human direction, delegation, review and handoff procedures are unchanged. No selected abstract or catalogue statement/scope/rendering impact. Original code/API/source credit is retained with all five reviewed payloads exact. Both documented Python checks and all37 controls pass; whitespace passes. Documented private PDF build/freshness and affected-page review follow on this clean frozen child, recorded in the final handoff. No Lean build or new-context native validation is claimed. Outside source approval6579489405 is reused; independent source/doc carry review remains required. AI assistance: OpenAI Codex, codex-2300-actual-std-bpl-20261102, authored this bounded documentation child under LogsQ; no canonical publication, source/API repair or queue action is included. * feat(dijkstra): realize the Fibonacci memory client natively Reuse the existing framed queue, source client and amortized potential. Preserve both original existential endpoints, graph encoding, word envelope and sharper reachable-vertex clock while exporting the exact whole final memory/frontier. Share the binary history/domain proofs, migrate the original graph clients and explicitly supersede the old Dijkstra executor and coefficient-640 helpers. Keep the MinPQ-used Fibonacci execution core and its source credit. Private #2290 implementation checkpoint. Default scripts/check.sh passed all six gates with two Lean threads on staged tree 5d348b8c230f481bde475094ddb7abe5a749717d. Focused same-program graph/parallel/unreachable/edgeless clients, unchanged binary client and both selected abstract audits pass; hygiene/aggregate pass. All public binary statements and named Fibonacci endpoint types are unchanged. Whole-F1 outside correctness/API review and publication planning remain pending. Evidence: audits/learning-dijkstra-fibonacci-2290-20261102/full-six-terminal.json under the authorized Extra-drive team root; coordinator scope #2290 comment 6584355323 preserves the remaining F2/core/space/whole-client objectives. AI-assisted implementation by Codex; retains Renfei Zhou and Samuel Schlesinger credit and Circuits' unchanged method-family layer. No abstract headline change. * doc(dijkstra): carry the approved binary endpoint reader route * doc(dijkstra): explain the native Fibonacci consumer and retained limits --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

SamuelSchlesinger and others added 30 commits November 1, 2026 17:07

doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018)

412f614

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Merge the memory-oracle branch (#2211) into the queue slice

fba5208

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

fix(DataStructure/StateTransition): place productCharge beside produc…

98e3290

…t, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Merge the refinement branch (#2212) into the queue slice

02ba9f7

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Merge the refinement branch (#2212) into the queue slice

1b4e2ea

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

wip: array stack over memory and queue method lemmas

fe7d60d

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

feat(Foundations): affine cost bounds are O(size)

aad5f3e

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Merge the refinement branch (#2212) into the queue slice

78cf872

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

wip: queue over memory

6698e86

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Merge the refinement branch (#2212) into the queue slice

93adf90

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

Merge commit '4283b8fb714450e78ba170865bcb54ce8563bce3' into codex/ra…

cb0adff

…m-realization-c2-20261101

fix(WordRAM): normalize the memory return simp rule

d8f6bea

chore(WordRAM): combine published realization and queue prerequisites

e768e0a

Merge commit 'a929a76f23194a8e94428973bca2a317f9f23755' into codex/ra…

5b9f10e

…m-memory-stack-c2-20261101

SamuelSchlesinger changed the base branch from feat/ram-realize-tactic to main November 2, 2026 08:57

SamuelSchlesinger added this pull request to the merge queue Nov 2, 2026

Merged via the queue into main with commit e5930ab Nov 2, 2026
4 checks passed

Navigation Menu

Repository navigation

feat(WordRAM): native backends for memory refinements, one realized body per constructor - #2277

feat(WordRAM): native backends for memory refinements, one realized body per constructor#2277
SamuelSchlesinger merged 37 commits into
mainfrom
feat/ram-realization-adapter

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

SamuelSchlesinger commented Nov 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Change

Demonstration

Base and limitations

Validation

AI assistance

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading