Repository navigation
[0.5.0] Completion plan: optimal compilation for every production root #106
Description
Completion plan for LexLean: every production root is certified optimal, nothing outside LexLean is trusted without a LexLean implementation and its oracles, and the 0.5.0 release satisfies the amended completion criterion (SPEC.md §30.4). MNIST is a consumer and evidence only: UOR-Foundation/MNIST#3.
Constraints every item satisfies
| ID | Constraint |
|---|---|
| C1 | LexLean is general: no rule, constant, register row or acceptance criterion names or depends on one consumer. A consumer may be cited as evidence, never as the definition of done. |
| C2 | Anything compiled with LexLean performs optimally: every production root is certified optimal over a universe, machine contract and objective fixed before any optimizer runs. |
| C3 | No claim of optimality over an unrestricted program universe (by Blum's speedup theorem some computable functions have no fastest program); optimality is always relative to a declared universe. |
| C4 | The universe is never what an optimizer can generate, and representation minimality is never execution optimality without a proved bridge (#15; SPEC.md §17.18). |
| C5 | Proof and measurement stay separate: wall time on hardware is always an open measurement. |
| C6 | One authoritative source per claim; register row, scenario and failing test before implementation; nothing deferred or stubbed (R1, R3, R4). |
| C7 | The universal theorems that carry optimality (universal data handles) are generated from LexLean's foundation, the UOR Atlas, not enumerated. |
| C8 | No time or effort estimates. |
| C9 | Nothing outside LexLean is assumed correct or complete. A capability the plan relies on is implemented in LexLean and checked against validation oracles; a non-LexLean implementation can falsify but never establishes a claim. The pinned Lean toolchain and kernel are the trusted base SPEC.md §5.1 names; rustc and the hardware are checked by differentials (§17.17, SP-11). |
Decisions
| ID | Status | Record |
|---|---|---|
| D1 | Resolved: LexLean source is normative; SPEC.md and TOML registers become projections | #111 |
| D2 | Narrowed: realization grammar and claim class | #107 |
| D3 | Narrowed: universal data handles generated from the Atlas | #108 |
| D4 | Narrowed: exported roots carry #[target_feature]; which targets first |
#109 |
| D5 | Resolved: #52–#63 are outside §31 and #15, so outside completion | this issue |
| D6 | Resolved: the ONNX decoder lives in UOR-Foundation/ONNX (to be created) | UOR-Foundation/MNIST#15 |
| D7 | Open: where κ-addressing in LexLean lives | #110 |
Items
| ID | Item | Record |
|---|---|---|
| L0.1 | Collection, fold and iteration primitives realized as loops (after PR #104) | #105 |
| L0.2 | Certificates for calls of any operand count | #97, PR #101 |
| L0.3 | Certificate budgets lifted | PR #99 |
| L0.4 | Open pull requests reviewed against R3–R6 and merged or closed | PRs #68, #82, #100, #102, #104 |
| L1.3 | Normative text as LexLean source | #111 |
| L1.1 | Production and optimality in purpose and scope | #112 |
| L1.2 | Release identity for 0.5.0 and languages 1.0–1.2 | #113 |
| L1.4 | #84 superseded (fold-as-loop → L0.1; borrows and regions → L4.2; constant capacity dropped) | #84 |
| L2.1 | Compiler authored in LexLean | #27 (stages #89–#93) |
| L2.2 | Language-model components | #30 |
| L2.3 | Model/reasoning stdlib and PrismPM fixture | #32 |
| L2.4 | vv extended to every L3, L4 and L5 item |
#33 |
| L2.5 | Release closure | #34 |
| L3.1 | Byte-to-fixed-width conversion | #114 |
| L3.2 | Artifacts as compile-time constants | #115 |
| L3.3 | Overflow discharged by proved bounds | #116 |
| L3.4 | Lemmas for equalities over folds | #117 |
| L3.5 | IEEE-754 bit patterns as exact rationals | #118 |
| L4.1 | Target machine contracts | #119 |
| L4.2 | Realization universe by grammar | #120 |
| L4.3 | Mandatory global_optimal certificate at export |
#121 |
| L4.4 | Lower-bound library from the Atlas | #122 |
| L4.5 | Bridge from certified cost to wall time | #123 |
| L4.6 | General performance corpus | #124 |
| L4.7 | Self-application | #125 |
| L5.1 | SHA-256 in LexLean | #126 |
| L5.2 | κ-addressing in LexLean | #127 |
| L6.1 | Release 0.5.0 | #128 |
Upstream items outside LexLean: PrismPM UOR-Foundation/PrismPM#184, UOR-Foundation/PrismPM#186, UOR-Foundation/PrismPM#194; UOR-Foundation/ONNX UOR-Foundation/MNIST#15.
Order
Defects first (L0); then the v0.4 issues and language gaps (L2, L3), with L1.3 after #93 and L1.1–L1.2 after L1.3; L5.1 and L5.2 can start now (L5.2 after D7); optimality (L4) after D2, D3 and D4; the release (L6.1) last. Every item enters as a §31 row, a scenario and a failing test (R3), and every acceptance criterion quantifies over the corpus of L4.6 (C1).
Generated by Claude Code
Activity