Repository navigation
refactor(BinaryHeap): realize heap and Dijkstra memory programs - #2288
Merged
Merged
Conversation
…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
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
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
Collaborator
Author
|
The delegated two-file follow-through is frozen privately at Strict focused validation (3,660 jobs), hygiene and whitespace pass. This changed tree has not had a full-six run. Algorithms has the guarded packet and retains combined validation, outside review, bridge assessment and joint retirement; no publication or integration is claimed. |
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.
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.
Ordinarily merge fixed actual main 23c9b4b with public source 27e8ada. Preserve the exact own layers of #2268, #2281, #2294 and #2300, current-main Backend/Frame/client entries, documentation, pins and unrelated changes. The 14-path generic layer and its inverse are source-audited; no private heap/Dijkstra migration APIs are included. Supplier review/CI/landing gates remain separate. No Lean build was run for this source-only checkpoint. AI assistance: OpenAI Codex prepared this ordinary source-only merge; all original supplier authorship and source credit are retained.
Ordinarily merge audited supplier-only991f075f into saved655df7596. Both public27e8 and actual7bf are best bases; Git recursively combines them. Preserve the original50 code/test/deletion afterimages and patch byte-for-byte; transport the two exact project-document spans; retain every other supplier-base entry and canonical aggregate. Supplier-only identity audit:2282#6580697867. No proof, public API or clock is changed by this metadata composition. Final-context validation and independent application review remain required. No public push. AI assistance: OpenAI Codex source-only integration; all Renfei Zhou, Samuel Schlesinger and delegated source/contributor credit is retained.
SamuelSchlesinger
changed the base branch from
feat/realize-while
to
codex/heap-canonical-supplier-base-20261102
November 2, 2026 16:07
Collaborator
Author
|
Source, validation, retirement and integration record — authors Current coverage: outside whole-application source/API approval at original The ordinary merge has parents Current native CI 41522407118/job125541475794 passed all six strict commands at actual checkout 7bfa63b9, immutable parents The following initial-publication source, validation and retirement inventory is retained as historical evidence for unchanged code; its former pending supplier/application-review gates are superseded by the current coverage above. The initial source is At the initial e99/991 checkpoint, one default At initial publication, the original 50-path code/test/deletion patch is byte-identical through the ordinary merge; both original document spans are literal transports. A separate documentation-only child records actual Queue #2303 and keeps generic framed/allocation/whole-client and Fibonacci objectives open. Reversing that child and the feature recovers the whole supplier-base tree; 5,395 unrelated base entries/modes are exact and imports are canonical. The separate base audit and the independent final publication-identity audit cover preservation, not API/mathematical approval. The latter disclosed one unnecessary GitHub rejected the retarget-first request with 422 because original draft head This is the bounded binary milestone. The original generic native-PQ/Dijkstra and Fibonacci objective remains open under #2290/#2205/#2213; live GenericPQ/PQCode/HeapStatement consumers remain. Former pending supplier/API gates are now fulfilled as described above; Current source, own MQ, actual landing and the shared containing-main usable-cache closeout are complete above. This record is not human or agent API approval. The exact public
Exact retired cached declaration inventory (generated support included)
Additional obsolete library helpers:
This is an API-disposition record, not an approval. Exact final validation and independent review belong to this PR revision. The source diff preserves the complete removed definitions and replacement contracts. |
SamuelSchlesinger
changed the title
SamuelSchlesinger
marked this pull request as ready for review
November 2, 2026 16:12
Collaborator
|
Coordinator |
Collaborator
|
Independent review of The compact layout permits the count at unused heap cell zero without weakening live key/heap/inverse-position semantics. Natural-word method arguments retain valid-handle domains. Both sifts preserve the complete source free-monad programs: logarithmic cutoffs remain proof data, actual guards terminate the native loops, and control/preparation/finishing instructions are charged. The fixed Backend family retains full memory/frontier and register frames. Extraction preserves the typed result and source execution/history. The raw dispatcher accepts the established arbitrary nonzero tag convention, executes zero staging and the getKey output copy, and fits within its wrapper allowance. Fresh compact initialization retains Dijkstra's source transports retain strict relaxation, invalid-target fallback, allocation and real early exit. One native program/factor precedes graphs and widths; its endpoint retains the original word threshold, full memory/frontier and prefix/body/halt charge. Required manual fix: update Nonblocking placement follow-up: CI 41478339194 reports all six gates successful. The recorded checkout |
Ordinarily merge reviewed source e99e49b with fixed actual main3d1370a6. Preserve the exact50-path application code/test/deletion patch, retain reviewed pending supplier entries and all unrelated actual-main entries, and combine only the ROADMAP metadata overlap with canonical imports. No public statement, proof, clock or source API repair is introduced. Reuses source/API review2288#6584896472; its required bounded manual repair follows as a separate documentation child. No Lean/full build or public push is part of this source-only checkpoint. AI-assisted by Codex; all original source/contributor credit retained.
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.
Source-only ordinary composition of reviewed ca96 and fixed actual2300/2b97. Preserve every original fifty-path binary code/test/deletion afterimage and full-index patch; formerly carried generic entries are now actual-main entries. Retain actual K3, manuals, policy, pins and unrelated source. Combine only literal ROADMAP/UPSTREAM spans and canonical aggregate. The algorithm-endpoint manual remains exact ca96. No Lean/API/proof change or validation/publication claim. Reuse source/API approval6584896472 and independent ca96 manual carry subject to separate current-context identity/render checks.
Collaborator
Author
|
Independent coordinator The original 50-path code/test/deletion patch and afterimages remain exact Saved Python checks and 37 controls pass. The actual PDF build/freshness matches this revision; I inspected pages 141–142 and verified complete-source links in the retained checkout. Fresh canonical CI, current-main prefix checks and admission remain required under LogsQ’s ownership; K1’s later prefix is separate. Agent review, not human approval. |
SamuelSchlesinger
changed the base branch from
codex/heap-canonical-supplier-base-20261102
to
main
November 2, 2026 20:47
This was referenced Nov 2, 2026
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Nov 3, 2026
…community#2281) * 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 * 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. * 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): 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. * 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. * doc(WordRAM): explain canonical initialized program exports Address PR2281 outside review6583587280 beside the Realizes discussion. Give the exact import, raw-words/state/scalar choices, preserved prefix, fit/domain/history premises and complete checked clients. Distinguish uncharged Data.init raw placement from the charged 2*k+5 register/frontier prefix, body and halt. The graph client only reads its header and preserves memory; no Dijkstra runtime endpoint is claimed. Manual impact: update the Algorithm/Operator's Manual API reference. No Agent Operator's Manual edit: roles, delegation, human direction and handoff procedures are unchanged. No selected abstract/catalogue impact. Validation: documented Python manual checker and all37 controls pass; whitespace passes. Inspect the affected GitHub-Markdown/Chrome page render and exact approved source links. Full XeLaTeX book generation unavailable because Pandoc, XeLaTeX and Graphviz are not installed; no book-PDF claim. No Lean source, test, dependency pin or proof changes in this child. Independent source/API review6583587280 remains the source coverage; independent documentation/current-context review still follows. AI assistance: OpenAI Codex, codex-2281-manual-bpl-20261102, authored this bounded documentation repair under LogsQ. Samuel Schlesinger/Learning source credit and all approved payloads are unchanged. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Nov 3, 2026
…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>
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Nov 3, 2026
…#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>
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Nov 3, 2026
…-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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is the bounded binary-heap/Dijkstra milestone for #2282/#2288. The original generic native-PQ/Dijkstra and Fibonacci objective remains open under #2290/#2205/#2213; the shared GenericPQ/PQCode/HeapStatement pieces still used by those consumers stay.
Replaces the hand-stepped binary-heap execution layer with native realizations of the existing Memory programs, and proves the existing log-linear Dijkstra endpoint through the same allocated
Memory.run. The pure Model/Order API and source credit remain; the three old execution modules are removed. SharedPQCode,GenericPQandHeapStatementpieces still used by Fibonacci or problem semantics stay.The shortest-path statement retains its exact graph encoding, word threshold, one-program/one-factor quantifier order, outputs and halt-inclusive bound. The native export also preserves the complete source memory/frontier. Counts use the existing exact-basis word-RAM semantics and
Data.initzero-tail convention. Raw standalone initialization retains the compact3n+1end-fit/local-zero domain and honest linear dirty clear; allocated Dijkstra keeps the original two-dirty-query3n+2path. Operation-call arguments and host continuations remain external; the whole Dijkstra program charges its actual prefix, control and halt.The change reuses
Memory.Prog,Code,Realizes,Backend,PQCodeand the existing state-transition/certificate interfaces. It extends existing Memory layout validity to permit the unused heap cell, generalizes existing handle methods to natural words with explicit valid-index domains, and supplies the faithful layout encodings and raw representation needed by the retained calling convention. It adds no parallel heap model, compiler or PQ judgment. The source, validation and retirement record identifies all public moves/replacements/removals. Old fixed raw clocks/register indices and implementation-specific 200/230 Dijkstra helpers are retired rather than reproduced; no source-size, space or instruction improvement is claimed.This is the joint binary migration under #2282/#2288 and a bounded milestone of #2205. Fibonacci and generic framed/allocation/whole-client objectives remain open. The separate documentation child records the now-landed bounded queue migration. No broad issue is closed by this PR.
Coverage: outside whole-application source/API approval is reused with the independent actual-parent source/manual carry at current
83af5582. The original 50-path application patch is unchanged. All eight formerly carried generic files are fulfilled by actual main, including #2300 at2b97d405; this PR now targets main. The earlier default six-gate and991/e99source-native results remain historical evidence in the linked record.Current native CI passed all six strict commands at verified checkout
7bfa63b9, with immutable parents[actual K1 5d887fb7, source 83af5582]and treefdfcd444. The canonical source-execution record links the saved-log/context verification and preserved payloads. Guide and Formal Abstract workflow metadata also report success; no artifact-content review is implied.Landed as actual c417845a. Own merge-queue execution and the first actually started containing-main run passed all six strict gates, with usable cache publication verified in the shared integration closeout. That record covers this migration and the captured-loop fix, including intervening-main and non-attribution limits; no per-PR rebuild cost or new abstract-PDF review is claimed. The bounded #2282 milestone is complete; generic/Fibonacci/F2 objectives remain open.
Manual assessment: the required endpoint page now links the public native heap/Dijkstra APIs and complete clients, distinguishes fresh/dirty/allocated initialization and standalone/fully charged costs, and retains the free raw-input convention and retired-constant limits. Both Python manual checks, whitespace, documented PDF build/freshness and affected pages 141–142 pass at clean
83af5582. The Agent manual is unchanged because roles, authority, delegation and handoffs are unaffected; other actual-main manual pages are preserved.Abstract assessment: the original Dijkstra abstract, selected catalogue and
HeapStatementare unchanged; bridge declaration/proof tokens are unchanged. Actual abstract audit/nonvacuity and import-scope regressions pass. The bridge's imports, declarations and proofs are unchanged; there is no affected PDF content.AI assistance: OpenAI Codex authored/integrated the native proofs and tests using the credited delegated Kernel, Learning and Crypto packets and existing Renfei Zhou/Samuel Schlesinger source. Original supplier authorship and exact independent-review coverage are retained. The original draft/design is credited to Claude Code (
dijknative-claude-015dlg8k, source session). The linked verdicts identify agent review and its scope; no human review is implied.