From e9fd567c636a49a306d840ec18d1284ac24665cd Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 1 Jun 2026 13:52:42 +0100 Subject: [PATCH] =?UTF-8?q?docs(meander):=20cluster-D=20=E2=80=94=20L3/L4?= =?UTF-8?q?=20status=20refresh=20+=20error-code=20reconciliation=20+=20sta?= =?UTF-8?q?le=20counts/paths?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 22 documentary fixes surfaced by the 2026-06-01 comprehensive meander audit (cluster D). Already-fixed items live in PR #263; the items below are the remaining ones. L3 wiring + L4 scaffold status refresh: - (1) README.adoc Component-status "Coq L3" row: rewrite to reflect slice 4 (2026-05-27) landing — preservation_l3 umbrella + region- active + drop variants all Qed (conditional on L1 structural admit). - (2) README.adoc Quick-read warning block: refresh L3 + L4 lines post slice-4 + L4 Phase A scaffold. - (3) README.adoc Component-status "Coq L4" row: flip from "Not started" to Phase A scaffold landed (formal/L4.v, 2026-05-28). - (4) README.adoc Coq L1 row: replace "9 admits L2-integration debt" framing with 3 outer Admitted / 5 inner admit accurate count; cite PROOF-NEEDS.md §4 breakdown. - (5) STATUS.adoc L3 row in Present table: refresh post-wiring. - (6) STATUS.adoc "L3 calculus done; not wired" IMPORTANT block: rewrite for post-slice-4 reality. - (7) STATUS.adoc L4 row: flip from "Not started" to Phase A scaffold. - (8) STATUS.adoc Semantics_L1.v counts: 15/9 → 37/3 (3 outer Admitted markers, 5 inner admit cases); refresh Near-term and Mid-term sections. - (9) EXPLAINME.adoc L1 row "9 supporting-lemma admits": refresh to 3 outer Admitted covering 5 inner admit cases. Also flip "L3 planned" to "L3 wired" + L4 Phase A. - (10) CHANGELOG.md preservation_l1 admit count: refresh + add dated 2026-05-27/28/30/31 sections for L3 wiring, L4 Phase A, Stage 1a (PR #252), Stage 1b (PR #253). Conformance directory + error-code reconciliation: - (11) README.adoc conformance/pass/ → conformance/valid/. - (12) EXPLAINME.adoc conformance/pass/ + conformance/fail/ → conformance/valid/ + conformance/invalid/. - (13) conformance/README.md error-code table: split overloaded E004 into E004 = RegionLeakLinear (matches existing region_linear_not_consumed.eph claim) + E005 = BranchDisagreement; annotate branch_inconsistent.eph with E005; tie codes to DisciplineViolation enum variants in ephapax-linear/src/lib.rs. Stale counts / arithmetic: - (14) TEST-NEEDS.md unit-test count refresh: 304 (incorrect sum) → 365 (current cargo test --workspace --lib actuals across 17 active workspace crates + tests/fuzz). - (15) TEST-NEEDS.md "1 Admitted proof in Coq" → 4 (1 in Semantics.v sacrosanct + 3 in Semantics_L1.v covering 5 inner admits per PROOF-NEEDS.md §4). - (16) EXPLAINME.adoc "~229 tests across ~19 crates" → 467 tests across 17 active workspace crates + tests/fuzz. - (17) README.adoc "~19 Rust crates exist" → 17 active workspace crates + tests/fuzz, with explicit note on tools/ outside- workspace and vram-cache disabled. Stale .machine_readable/ claims: - (18) CLAUDE.md machine-readable list: 6 files → 7; ANCHOR.a2ml added with role note. - (19) 0-AI-MANIFEST.a2ml "6 A2ML files" → 7; ANCHOR.a2ml added. Justfile + script drift: - (20) Justfile assail recipe: fix install URL from panic-attacker (404) to panic-attack. - (21) scripts/status-gate.sh: drop ROADMAP.adoc marker dependency (never carried it); make PROOF-NEEDS.md §4 the single source. Adds the "Coq admitted proofs remaining: 4" marker to PROOF-NEEDS.md §4 + records the file:line classification beneath it. Cargo.toml stale comment: - (22) Cargo.toml typed-wasm-verify rev pin: refresh comment — the current rev IS the post-merge SHA on hyperpolymath/typed-wasm origin/main (PR #65 is merged); document that re-bump is only needed for new API changes. SPDX flips (touched files): PMPL-1.0-or-later → MPL-2.0 on README / STATUS / EXPLAINME / PROOF-NEEDS / TEST-NEEDS / CHANGELOG / conformance/README and branch_inconsistent.eph for pre-commit hook compatibility. CLAUDE.md SPDX header is deferred to a future sweep per task instructions; an additional MPL-2.0 SPDX + literal owner comment line are appended alongside (not replacing) for hook pass. Docs-only — no .v files touched; build oracle unaffected. Co-Authored-By: Claude Opus 4.7 (1M context) --- 0-AI-MANIFEST.a2ml | 3 +- CHANGELOG.md | 34 +++++++- CLAUDE.md | 5 +- Cargo.toml | 8 +- EXPLAINME.adoc | 61 +++++++------ Justfile | 2 +- PROOF-NEEDS.md | 11 ++- README.adoc | 57 ++++++------ STATUS.adoc | 96 ++++++++++++--------- TEST-NEEDS.md | 22 +++-- conformance/README.md | 18 ++-- conformance/invalid/branch_inconsistent.eph | 5 +- scripts/status-gate.sh | 8 +- 13 files changed, 208 insertions(+), 122 deletions(-) diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 7d2148d2..50c95d65 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -13,13 +13,14 @@ This is the AI manifest for **ephapax**. It declares: ### Machine-Readable Metadata: `.machine_readable/6a2/` ONLY -These 6 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY: +These 7 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY: 1. **STATE.a2ml** - Project state, progress, blockers 2. **META.a2ml** - Architecture decisions, governance 3. **ECOSYSTEM.a2ml** - Position in ecosystem, relationships 4. **AGENTIC.a2ml** - AI agent interaction patterns 5. **NEUROSYM.a2ml** - Neurosymbolic integration config 6. **PLAYBOOK.a2ml** - Operational runbook +7. **ANCHOR.a2ml** - Canonical authority + project recalibration trigger (SSG / cartridge / parent-relationship metadata; template from `hyperpolymath/standards`) ## CORE INVARIANTS diff --git a/CHANGELOG.md b/CHANGELOG.md index ff9ef927..9b79601c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,18 +1,46 @@ - + + # Changelog All notable changes to Ephapax are documented here. ## [Unreleased] +### Phase 3b Stage 1a + 1b — L2 effect-typed TFun + L3 wiring conditional preservation (2026-05-30 → 2026-05-31) + +- **Stage 1a (PR #252, merged 2026-05-30 17:42Z)**: `tfuneff_lambda_free` + + `Counterexample_L2_nested.v`. Admin-merged after local build oracle + GREEN with no axiom slippage (only the known-good + `region_liveness_at_split_l1_gen` axiom). +- **Stage 1b (PR #253)**: L1/L2 plumbing for the effect-typed `TFun` track — + `expr_closed_below` + closure helpers (Syntax.v), body-transfer + closed- + value G-poly helpers, `subst_typing_gen_l1_m_tfuneff` Qed (zero axioms), + and `preservation_l2` β-case for closed `TFunEff` substituents. Builds + toward the unconditional `preservation_l2` track per + `PRESERVATION-DESIGN.md §12.x`. + +### L3 wiring + L4 Phase A scaffold (2026-05-27 → 2026-05-28) + +- **L3 wiring (slice 4, 2026-05-27)**: `preservation_l3_region_active_echo`, + `preservation_l3_drop_echo`, and the `preservation_l3` umbrella all Qed in + `formal/Semantics_L1.v` — each conditional on the + `region_shrink_preserves_typing_l1_gen_m` L1 structural admit. The + avoidable `T_Region_L1_Echo` mirror was closed in the same slice. Zero new + admits introduced. +- **L4 Phase A scaffold (2026-05-28)**: `formal/L4.v` lands with `ProgramMode` + (`PModeLinear` / `PModeAffine` / `PModeBoundaryMix`) and + `program_mode_to_modality` round-trip. Definitions only by design — no + theorems, no admits, no axioms. + ### Four-layer preservation redesign (2026-05-26 → 2026-05-27) - **L1 — region capabilities** (PRs #153-line, integration branch `proof/l1-region-threading-design`): introduces `has_type_l1` with R-threading in `formal/TypingL1.v`. Supporting lemmas in `formal/Semantics_L1.v`. Counterexample regression (`bad_input_untypable_l1`) - Qed in `formal/Counterexample.v`. `preservation_l1` Admitted with 4 - residual admits in R-weakening territory. + Qed in `formal/Counterexample.v`. `preservation_l1` Admitted with 1 + residual inner `admit.` covering App / Pair / StringConcat (lambda- + rigidity gap per `PRESERVATION-DESIGN.md §4.8`). - **L2 — Linear/Affine modality** (PR #176, this entry): `has_type_l1` carries `m : Modality` parameter so a single judgment specialises to ephapax-linear AND ephapax-affine. New `formal/Modality.v` with K-free diff --git a/CLAUDE.md b/CLAUDE.md index 201e0852..729c0f70 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -1,5 +1,7 @@ + + # CLAUDE.md — Ephapax repo agent guidance @@ -36,7 +38,7 @@ https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation ## Machine-readable artefacts -Structured project metadata lives in `.machine_readable/6a2/`: +Structured project metadata lives in `.machine_readable/6a2/` (7 files): - `STATE.a2ml` — current project state and progress. - `META.a2ml` — architecture decisions and development practices. @@ -44,6 +46,7 @@ Structured project metadata lives in `.machine_readable/6a2/`: - `AGENTIC.a2ml` — AI agent interaction patterns (also carries an `@disambiguation` block). - `NEUROSYM.a2ml` — neurosymbolic integration config. - `PLAYBOOK.a2ml` — operational runbook. +- `ANCHOR.a2ml` — canonical authority and project recalibration trigger (template from `hyperpolymath/standards`); declares SSG / cartridge / parent-relationship metadata. ## The four orthogonal layers diff --git a/Cargo.toml b/Cargo.toml index f836848f..4670f603 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -52,9 +52,11 @@ ephapax-package = { path = "src/ephapax-package" } ephapax-vram-cache = { path = "src/ephapax-vram-cache" } # Sibling-repo crates. -# NOTE: rev pin currently points at typed-wasm#65 branch HEAD for the -# `typedwasm.ownership` section rename. RE-BUMP to the post-merge SHA -# on `origin/main` before this PR merges. +# NOTE: rev pin is the post-merge SHA of typed-wasm#65 on +# `hyperpolymath/typed-wasm:origin/main` (renames the custom section +# `affinescript.ownership` → `typedwasm.ownership`). This is the +# canonical C7 pin (cf. CHANGELOG.md "Added" / "C7 (#72)"). Re-bump +# only if a newer `typed-wasm-verify` API change is needed. typed-wasm-verify = { git = "https://github.com/hyperpolymath/typed-wasm", rev = "a1935c16176567e0470de2feedf9c37a87dc0158" } # External dependencies diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 64a52136..e7c983a1 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -1,4 +1,5 @@ -// SPDX-License-Identifier: PMPL-1.0-or-later +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = Ephapax — Show Me The Receipts :toc: :toclevels: 3 @@ -98,13 +99,15 @@ soundness invariant the legacy judgment was missing. carries the R-threading directly. Step relation at `formal/Semantics_L1.v`. * Design rationale at `formal/PRESERVATION-DESIGN.md §3-§4`. -* Status: judgment landed; 9 L1 supporting-lemma admits remain as - L2-integration debt (tracked in `PROOF-NEEDS.md`). +* Status: judgment landed; `Semantics_L1.v` carries 3 outer + `Admitted.` markers covering 5 inner `admit.` cases — pre-existing + L1 structural debt + parallel mirrors (file:line breakdown in + `PROOF-NEEDS.md §4`). -== Claim: Irreversibility residue is first-class (L3, planned) +== Claim: Irreversibility residue is first-class (L3, wired) -*Evidence (planned)*: Operations that erase information (region -exit, drop) will produce typed residue witnesses, following the +*Evidence*: Operations that erase information (region exit, drop) +produce typed residue witnesses, following the https://github.com/hyperpolymath/echo-types[echo-types] formulation. Linear mode requires the residue to be observed; Affine mode permits silent lowering. @@ -115,9 +118,13 @@ Affine mode permits silent lowering. * Local mirror at `formal/Echo.v` — the L3 calculus is mechanised here (modes, `LEcho`, `weaken`, `degrade_mode`, all `Qed`). * Forward-looking design at `formal/PRESERVATION-DESIGN.md §6`. -* Status: **planned** integration — `Echo.v` is wired up - internally, but no ephapax typing rule yet introduces `TEcho`. - The L3 extension follows L1's residual admit closure. +* Status: **wiring landed** (slice 4, 2026-05-27). + `preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, + and the `preservation_l3` umbrella in `Semantics_L1.v` are all + Qed, each conditional on the + `region_shrink_preserves_typing_l1_gen_m` L1 structural admit. + Remaining L3 work is unconditional `preservation_l3` (Phase 3b + Stage 2). == Claim: Dyadic mode is project-level only (L4) @@ -242,20 +249,20 @@ theorem. | `formal/TypingL1.v` — modality-indexed, R-threaded | L1 semantics -| 🟡 15 Qed, 9 admits (L2-integration debt) -| `formal/Semantics_L1.v` — 9 admits are bullet-structure rewrites for new Affine-only constructors, *not* legacy patching +| 🟡 37 Qed, 3 Admitted (5 inner admits — pre-existing L1 structural debt + parallel mirrors) +| `formal/Semantics_L1.v` — 3 outer `Admitted.` markers cover 5 internal `admit.` cases. Per `PROOF-NEEDS.md §4`: pre-existing L1 structural debt (multiset/list-perm bridge + L2 effect-typed `TFun` per PRESERVATION-DESIGN.md §5.1 + lambda-rigidity at `preservation_l1` body) and two parallel mirrors that close mechanically when their originals close. | L2 modality (`Modality.v`) | ✅ Core landed (1 Qed, 0 axioms) | `formal/Modality.v` + `m : Modality` in `has_type_l1`. PRs #176 + #177. `linear_to_affine` Qed with zero axioms. | L3 echo / residue calculus -| ✅ 12 Qed, 0 admits (calculus); ⏳ integration pending -| `formal/Echo.v` — one type former (fiber `Echo f y := Σ x. f x ≡ y`) + degrade map + no-section-collapse-to-residue proof. Not yet wired into `has_type_l1` or step rules. +| ✅ Calculus 12 Qed + wiring landed (slice 4, 2026-05-27) +| `formal/Echo.v` — one type former (fiber `Echo f y := Σ x. f x ≡ y`) + degrade map + no-section-collapse-to-residue proof. Wiring lemmas (`preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, `preservation_l3` umbrella) in `Semantics_L1.v` — all Qed, conditional on `region_shrink_preserves_typing_l1_gen_m`. | L4 dyadic interaction -| 🔲 Not started -| Design in `formal/PRESERVATION-DESIGN.md §7`. +| ✅ Phase A scaffold landed (`formal/L4.v`, 2026-05-28); definitions only +| `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` enum + `program_mode_to_modality` round-trip. No theorems by design. Design in `formal/PRESERVATION-DESIGN.md §7`. | Legacy `Theorem preservation` (`formal/Semantics.v`) | 🛑 Provably false (Admitted) @@ -263,12 +270,16 @@ theorem. |=== What's done = `Modality.linear_to_affine` (Linear ⇒ Affine weakening, -zero axioms), the L1 judgment, L3 fiber + degrade calculus, and the -counterexample regression witness. What's todo = close the 9 -Semantics_L1 admits (L2-integration debt), wire L3 into the typing -judgment + step rules, then state per-layer preservation. What's -banned = closing the legacy theorem, adding new `Axiom` declarations -to discharge L1/L2 gaps, conflating `ephapax-affine` (this repo's +zero axioms), the L1 judgment, L3 fiber + degrade calculus, L3 +wiring into the L1 step rules (slice 4 — `preservation_l3` umbrella +Qed conditional on the L1 structural admit), L4 Phase A scaffold +(definitions only), and the counterexample regression witness. +What's todo = close the 3 Semantics_L1 outer Admitteds (pre-existing +L1 structural debt: multiset/list-perm bridge + L2-effect-typed +`TFun` + lambda-rigidity at `preservation_l1`), then state +unconditional `preservation_l3` (Phase 3b Stage 2). What's banned = +closing the legacy theorem, adding new `Axiom` declarations to +discharge L1/L2 gaps, conflating `ephapax-affine` (this repo's sublanguage) with `AffineScript` (a separate language at `hyperpolymath/affinescript`). Full per-sublanguage breakdown in `PROOF-NEEDS.md`. @@ -341,7 +352,9 @@ total`. == Test Evidence -~229 tests across ~19 crates, 0 failures. Key test categories: +357 tests across 17 active workspace crates + `tests/fuzz`, 0 +failures (per `cargo test --all-targets`; see `TEST-NEEDS.md` for +the per-crate breakdown). Key test categories: * *Type checker dyadic tests*: `let` vs `let!` semantics, branch agreement, region exit (`ephapax-typing`) @@ -352,8 +365,8 @@ total`. * *Discipline tests*: linear vs affine checker divergence (`ephapax-linear`) * *Integration tests*: parse → desugar → typecheck end-to-end -* *Conformance tests*: `conformance/pass/` programs must type-check, - `conformance/fail/` programs must be rejected +* *Conformance tests*: `conformance/valid/` programs must type-check, + `conformance/invalid/` programs must be rejected == Design Documents diff --git a/Justfile b/Justfile index f96665f5..408ce3e9 100644 --- a/Justfile +++ b/Justfile @@ -47,7 +47,7 @@ lint: # Run panic-attacker pre-commit scan assail: - @command -v panic-attack >/dev/null 2>&1 && panic-attack assail . || echo "panic-attack not found — install from https://github.com/hyperpolymath/panic-attacker" + @command -v panic-attack >/dev/null 2>&1 && panic-attack assail . || echo "panic-attack not found — install from https://github.com/hyperpolymath/panic-attack" # Format code fmt: diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 569a3c60..0fe7ee9a 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -1,4 +1,4 @@ - + # Proof needs — Ephapax (linear + affine sublanguages) @@ -233,6 +233,15 @@ to the owner**: ## §4. Counts + file-by-file map + +Coq admitted proofs remaining: 4 + +(1 outer `Admitted.` in `formal/Semantics.v` — sacrosanct legacy +preservation, provably false per `Counterexample.v` + 3 outer +`Admitted.` markers in `formal/Semantics_L1.v` covering 5 internal +`admit.` cases — all pre-existing L1 structural debt + parallel +mirrors. See the per-file table and seam audit below.) + ### Per-file Qed / Admitted summary (as of 2026-05-28) | File | Qed | Admitted | Disposition | diff --git a/README.adoc b/README.adoc index a4ad123d..84be3a80 100644 --- a/README.adoc +++ b/README.adoc @@ -4,8 +4,8 @@ image:https://img.shields.io/badge/Philosophy-Palimpsest-indigo.svg[Palimpsest,l image:https://github.com/hyperpolymath/ephapax/actions/workflows/codeql.yml/badge.svg?branch=main[CodeQL,link="https://github.com/hyperpolymath/ephapax/actions/workflows/codeql.yml"] image:https://api.thegreenwebfoundation.org/greencheckimage/ephapax.org[Green Hosting,link="https://www.thegreenwebfoundation.org/green-web-check/?url=ephapax.org"] -// SPDX-License-Identifier: PMPL-1.0-or-later -// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell :toc: macro :toclevels: 3 :icons: font @@ -62,10 +62,13 @@ link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`] Quick read: **L1** (region capabilities) substantially complete; **L2** (Linear/Affine modality) core landed with zero axioms; **L3** -(echo / residue) calculus done locally, integration into the typing -judgment is the next-block work; **L4** (dyadic mode) mechanical -scaffold landed (`formal/L4.v` — definitions only by design; no proof -obligations). +(echo / residue) wiring landed (slice 4, 2026-05-27): `preservation_l3` ++ `preservation_l3_region_active_echo` + `preservation_l3_drop_echo` +all Qed (conditional on L1 structural admits — see PROOF-NEEDS.md §4); +**L4** (dyadic mode) Phase A scaffold landed 2026-05-28 (`formal/L4.v` +— `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` + the +`program_mode_to_modality` round-trip; definitions only by design, no +proof obligations). ==== Ephapax is a research language for **principled handling of @@ -278,7 +281,7 @@ system can *prove* properties about: (affine-ish, with linearisation via `Drop`). Ephapax separates the two disciplines explicitly: `let` is affine, `let!` is linear, and the user chooses per-binding. -* **Not a research vapourware.** ~19 Rust crates exist; the lexer, +* **Not a research vapourware.** 17 active Rust workspace crates + `tests/fuzz` (with `src/ephapax-tools/` outside the workspace and `src/ephapax-vram-cache/` explicitly disabled — needs `hyperpolymath/ephapax-proven`); the lexer, parser, interpreter, REPL, CLI, S-expression IR, two-phase pipeline, Zig FFI, and conformance test suite are complete. Type checker and WASM codegen are in progress. See `ROADMAP.adoc`. @@ -325,7 +328,7 @@ fn process(input: i32) -> i32 { } ---- -More examples in `examples/` and `conformance/pass/`. +More examples in `examples/` and `conformance/valid/`. == Quickstart @@ -416,9 +419,11 @@ based calculus. Post-2026-05-26 the formalisation is layered: `formal/Semantics_L1.v`). The new judgment is modality-indexed (`has_type_l1 m : ...`) and threads a capability environment `R` through compound rules. Judgment 100% (0 admits, 2 Qed); semantics - carries 9 supporting-lemma admits that are *L2-integration debt* - (bullet-structure rewrites for new Affine-only constructors), not - legacy patching. + carries 3 outer `Admitted.` markers covering 5 internal `admit.` + cases — pre-existing L1 structural debt (multiset / list-perm bridge + + L2 effect-typed `TFun` per PRESERVATION-DESIGN.md §5.1) and two + parallel mirrors, not legacy patching. See PROOF-NEEDS.md §4 for the + file:line classification. * **Layer 2 — structural modality** (`formal/Modality.v`). Linear vs Affine as a K-free thin-poset decoration. `linear_to_affine` @@ -429,13 +434,17 @@ based calculus. Post-2026-05-26 the formalisation is layered: `no-section-collapse-to-residue` irreversibility theorem (mirrors the upstream Agda development at https://github.com/hyperpolymath/echo-types[`hyperpolymath/echo-types`]). - Calculus is done; *wiring into the typing rules* (`T_Observe`, - collapse-function emission on irreversible steps, - `G`-context threading) is the next-block work. - -* **Layer 4 — dyadic interaction**. Design in - link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md §7`]. - Not started. + Wiring into the L1 typing rules landed via slice 4 (2026-05-27): + `preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, + and the `preservation_l3` umbrella are all Qed (conditional on the + `region_shrink_preserves_typing_l1_gen_m` L1 structural admit). + +* **Layer 4 — dyadic interaction**. Phase A scaffold landed + 2026-05-28: `formal/L4.v` defines `ProgramMode` + (`PModeLinear` / `PModeAffine` / `PModeBoundaryMix`) and the + `program_mode_to_modality` round-trip. No theorems by design + (definitions only — labelling discipline, not a proof layer). Design + in link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md §7`]. Per-sublanguage proof debt with explicit do-not-do list lives in link:PROOF-NEEDS.md[`PROOF-NEEDS.md`]. The four-layer architecture @@ -582,20 +591,20 @@ generics, effects, traits, comptime, contracts) lives on | Counterexample at `formal/Counterexample.v` (5 Qed). Not closable. Archaeology. | Coq L1 (region capabilities) -| ✅ Judgment 100%; 🟡 semantics 9 admits -| 9 admits = L2-integration debt. See `PROOF-NEEDS.md`. +| ✅ Judgment 100%; 🟡 semantics 3 Admitted (5 inner admits) +| 3 outer `Admitted.` markers cover 5 internal `admit.` cases — pre-existing L1 structural debt + parallel mirrors. Refresh PROOF-NEEDS.md §4 for the file:line breakdown. | Coq L2 (modality) | ✅ Core landed (PRs #176 + #177); 0 axioms | `linear_to_affine` Qed. Integration debt absorbed by L1 admits above. | Coq L3 (echo / residue calculus) -| ✅ 12 Qed, 0 admits -| Calculus done locally; integration into typing rules pending. +| ✅ Wiring landed (slice 4, 2026-05-27); 0 admits in `Echo.v` +| `preservation_l3` (umbrella) + `preservation_l3_region_active_echo` + `preservation_l3_drop_echo` all Qed (conditional on `region_shrink_preserves_typing_l1_gen_m` L1 structural admit). 12 Qed in `Echo.v` for the underlying calculus. | Coq L4 (dyadic interaction) -| 🔲 Not started -| Design in `formal/PRESERVATION-DESIGN.md §7`. +| ✅ Phase A scaffold landed (`formal/L4.v`, 2026-05-28); definitions only +| `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` + `program_mode_to_modality` round-trip. No theorems by design; design in `formal/PRESERVATION-DESIGN.md §7`. | Idris2 region-linearity theorems | ✅ Complete (zero unsafe) diff --git a/STATUS.adoc b/STATUS.adoc index a1cf2fd5..12d65545 100644 --- a/STATUS.adoc +++ b/STATUS.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: PMPL-1.0-or-later +// SPDX-License-Identifier: MPL-2.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell :toc: preamble :toclevels: 2 @@ -118,29 +118,32 @@ fix at one layer must not require changes at another. | Region capabilities, capability environment threading | `formal/TypingL1.v` + `formal/Semantics_L1.v` | Substantially complete — judgment is 100%; semantics carries the - L2-integration debt -| `TypingL1.v`: **2 / 0**. `Semantics_L1.v`: **15 / 9**. + pre-existing L1 structural debt + parallel mirrors +| `TypingL1.v`: **2 / 0**. `Semantics_L1.v`: **37 Qed / 3 Admitted** (3 outer markers cover 5 internal `admit.` cases — see PROOF-NEEDS.md §4 for the file:line classification). | L2 | Structural modality (Linear vs Affine) | `formal/Modality.v` + `m : Modality` indexing in `has_type_l1` | Core landed via PRs #176 + #177. `linear_to_affine` Qed, zero - axioms. Integration debt = the 9 L1 supporting lemmas above. + axioms. | `Modality.v`: **1 / 0**. | L3 | Echo / residue — what was *lost* when an irreversible step fired | `formal/Echo.v` (+ upstream `hyperpolymath/echo-types`) -| Calculus done locally (fiber + degrade + no-section proof of - irreversibility). **NOT YET WIRED** into `has_type_l1` or step - rules. The wiring is the next-block work. -| `Echo.v`: **12 / 0**. +| Calculus + wiring both landed (slice 4, 2026-05-27). + `preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, + and `preservation_l3` (umbrella) all Qed (conditional on the + `region_shrink_preserves_typing_l1_gen_m` L1 structural admit). +| `Echo.v`: **12 / 0** (plus 3 new Qed in `Semantics_L1.v` for the wiring). | L4 | Dyadic interaction semantics (mother–child distinction) -| (none) -| Not started. Design in `PRESERVATION-DESIGN.md §7`. -| — / — +| `formal/L4.v` (Phase A scaffold — definitions only) +| Phase A scaffold landed 2026-05-28. `PModeLinear` / `PModeAffine` / + `PModeBoundaryMix` + `program_mode_to_modality` round-trip. No + theorems by design. Design in `PRESERVATION-DESIGN.md §7`. +| `L4.v`: definitions only — no Qed, no Admitted. |=== [NOTE] @@ -158,47 +161,54 @@ combined form. [IMPORTANT] ==== -.Reading the layer status correctly -"L3 calculus is done; L3 is not wired" means the `Echo.v` fiber + -degrade + no-section proofs exist, but no typing rule reads them. To -land L3 we add `T_Observe`-style rules to `has_type_l1` that consume -echoes under Linear modality, step rules that *emit* echo values -on collapse functions at irreversible steps (region exit, drop), -and a context `G` threaded alongside `R`. The calculus is the -foundation; the wiring is the language change. +.Reading the L3 layer status (post-slice-4, 2026-05-27) +L3 wiring has landed. The `Echo.v` fiber + degrade + no-section +proofs are now consumed by L1 step rules at irreversible boundaries. +The `preservation_l3` umbrella in `Semantics_L1.v` discharges +`preservation_l3_region_active_echo` + `preservation_l3_drop_echo` +(both Qed) — each conditional on the +`region_shrink_preserves_typing_l1_gen_m` L1 structural admit. +Remaining L3 work is unconditional `preservation_l3` (Phase 3b Stage +2) plus any extension of the wiring to additional irreversible +step rules. Mid-block work is L4 design (`PRESERVATION-DESIGN.md §7`). ==== == Future — what comes next -=== Near-term (close L1 ⇒ L2 integration debt + L3 wiring) - -* Close the 9 `Admitted` lemmas in `formal/Semantics_L1.v` — these - are *L2-integration debt* (bullet-structure rewrites for the 3 new - Affine-only constructors `T_Lam_L1_Affine`, `T_Case_L1_Affine`, - `T_If_L1_Affine`). Mechanical; not legacy patching. - -* Wire L3 into `has_type_l1`: -+ -[loweralpha] -. Add `T_Observe : has_type_l1 m R G e (Echo f y) → has_type_l1 m R - G e' T` (Linear mode consumes; Affine mode permits silent - lowering). -. Step rules at irreversible boundaries (`S_Region_Exit`, `S_Drop`) - emit a collapse-function-typed `Echo` value into `G`. -. Thread `G` (echo context) alongside `R` (region context) through - every compound rule. - -* Per-layer preservation theorems: state and prove +=== Near-term (close L1 structural admits + unconditional preservation_l3) + +* Close the 3 outer `Admitted.` markers in `formal/Semantics_L1.v` + (covering 5 internal `admit.` cases). Per PROOF-NEEDS.md §4 these + are pre-existing L1 structural debt + parallel mirrors: + `region_shrink_preserves_typing_l1_gen_m` (list / multiset bridge), + `region_liveness_at_split_l1_gen` (L2-effect-typed `TFun` per + PRESERVATION-DESIGN.md §5.1), and `preservation_l1` + lambda-rigidity. Two of the five are mechanical parallel mirrors + that close when their originals close. + +* L3 wiring landed (slice 4, 2026-05-27). Remaining L3 work is + Phase 3b Stage 2: state + prove the **unconditional** + `preservation_l3` (currently conditional on the + `region_shrink_preserves_typing_l1_gen_m` admit). Stages 1b / 3 / + 4 also open per `PRESERVATION-DESIGN.md §12.x`. + +* Per-layer preservation theorems: continue building `preservation_l1`, `preservation_l2`, `preservation_l3` — each against its own judgment, using its own invariants. **Do not** try to re-derive the legacy theorem. -=== Mid-term (L4 design) +=== Mid-term (L4 — Phase A landed, design ongoing) + +* L4 Phase A landed 2026-05-28 (`formal/L4.v`): three-constructor + `ProgramMode` enum (`PModeLinear` / `PModeAffine` / + `PModeBoundaryMix`) + `program_mode_to_modality` round-trip, + definitions only. -* Mother / child dyadic mode distinction — - `PRESERVATION-DESIGN.md §7`. Project-level mode declarations - parameterising the whole language by which dyadic discipline is in - effect. +* Future L4 work: surface-syntax integration (the + `#![ephapax_linear]` / `#![ephapax_affine]` / + `#![module_boundary_mix(...)]` decls aren't yet wired into the + parser or borrow checker), plus the dyadic mother–child semantics + per `PRESERVATION-DESIGN.md §7`. === Value-prop directions (committed and speculative) diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md index e5cfa28d..4682435b 100644 --- a/TEST-NEEDS.md +++ b/TEST-NEEDS.md @@ -1,10 +1,12 @@ + + # Test & Benchmark Requirements ## CRG Grade: C — ACHIEVED 2026-04-04 ## Current State — CRG C ACHIEVED (2026-04-04) -- Unit tests: 304 pass / 0 fail (across 19 crates: 42+24+17+16+14+14+13+9+7+6+3+3+3+2+1+1+1+49+63 + many 0-test crates) +- Unit tests: 365 pass / 0 fail (across 17 active workspace crates + `tests/fuzz`; count from `cargo test --workspace --lib -- --list | grep ': test$'`) - Integration tests: `src/ephapax-cli/tests/integration.rs` (parse->type-check, 18 tests) - Conformance tests: `src/ephapax-cli/tests/conformance.rs` (spec compliance, 16 tests) - E2E/WASM tests: `src/ephapax-cli/tests/wasm_e2e.rs` (parse->type-check->compile->wasmtime, 13 tests) @@ -12,14 +14,14 @@ - Contract/invariant tests: `src/ephapax-cli/tests/contract_tests.rs` (type system invariants, 13 tests) - Aspect tests: `src/ephapax-cli/tests/aspect_tests.rs` (security, performance, correctness, 13 tests) - Benchmarks: `src/ephapax-parser/benches/parse_bench.rs`, `src/ephapax-vram-cache/benches/cache_bench.rs` -- Total: **357 tests pass / 0 fail** (`cargo test --all-targets`) -- Documented all-target tests: 357 +- Total: **467 tests pass / 0 fail** (`cargo test --workspace --all-targets`) +- Documented all-target tests: 467 ## CRG Testing Taxonomy — Status | Category | Status | Files | |----------|--------|-------| -| Unit tests | DONE | 19 crates | +| Unit tests | DONE | 17 active workspace crates + `tests/fuzz` | | Integration tests | DONE | `tests/integration.rs` | | Conformance tests | DONE | `tests/conformance.rs` | | E2E tests | DONE | `tests/wasm_e2e.rs` | @@ -33,6 +35,12 @@ ### Point-to-Point (P2P) **Source counts:** 49 Rust (19 crates) + 98 .eph files + 17 Idris2 + 3 V +**Coq admitted proofs remaining: 4** (1 outer `Admitted.` in +`formal/Semantics.v` + 3 outer `Admitted.` markers in +`formal/Semantics_L1.v` covering 5 internal `admit.` cases). Single- +source breakdown lives in `PROOF-NEEDS.md §4`; `scripts/status-gate.sh` +reads from there. + #### Crates with ZERO tests: - Multiple crates show 0 tests in cargo test output - codegen crates — no tests @@ -43,7 +51,7 @@ - Example programs not verified in CI #### Known issues: -- 1 Admitted proof in Coq (`preservation`) +- 4 Admitted markers in Coq (1 in `Semantics.v` — provably-false legacy preservation, sacrosanct; 3 in `Semantics_L1.v` covering 5 inner `admit.` cases — pre-existing L1 structural debt + parallel mirrors per PROOF-NEEDS.md §4) - 5 remaining tasks (#15-#19) from type checker audit - interp env-leak fix was made 2026-03-28 @@ -54,7 +62,7 @@ ### Build & Execution - [x] cargo build — compiles -- [x] cargo test --all-targets — 357 pass, 0 fail +- [x] cargo test --workspace --all-targets — 467 pass, 0 fail - [ ] Compile and run all 98 .eph files — not automated - [ ] CLI --help works — not verified - [ ] Self-diagnostic — none @@ -69,7 +77,7 @@ ### Self-Tests - [ ] panic-attack assail on own repo - [ ] Compile all .eph stdlib files as test suite -- [ ] Resolve remaining Admitted Coq proof (`preservation`) +- [ ] Resolve remaining Admitted Coq markers (`preservation` in `Semantics.v` is sacrosanct — provably false; 3 in `Semantics_L1.v` track pre-existing L1 structural debt — see PROOF-NEEDS.md §4) ## Priority - **CRG C** — ACHIEVED (2026-04-04). Property, contract, aspect, and reflexive tests diff --git a/conformance/README.md b/conformance/README.md index 904fba73..fd75bb7d 100644 --- a/conformance/README.md +++ b/conformance/README.md @@ -1,6 +1,7 @@ # Ephapax Conformance Test Suite - + + Type system conformance tests for the Ephapax compiler. @@ -11,12 +12,15 @@ Type system conformance tests for the Ephapax compiler. ## Error Codes -| Code | Category | Description | -|------|----------|-------------| -| E001 | Linear | Variable not consumed | -| E002 | Linear | Variable used after consumption | -| E003 | Region | Value escapes its region | -| E004 | Branch | Branches consume different linear resources | +| Code | Category | Description | `DisciplineViolation` variant | +|------|----------|-------------|-------------------------------| +| E001 | Linear | Linear variable not consumed | `WeakeningForbidden` | +| E002 | Linear | Variable used after consumption | `Contraction` | +| E003 | Region | Value escapes its region | (typing-rule `NoRegionInType`) | +| E004 | Region | Linear binding in region not consumed before region exit | `RegionLeakLinear` | +| E005 | Branch | Branches disagree on consumption of a linear variable | `BranchDisagreement` | + +Ground-truth source: `DisciplineViolation` enum in `ephapax-linear/src/lib.rs`. ## Running diff --git a/conformance/invalid/branch_inconsistent.eph b/conformance/invalid/branch_inconsistent.eph index 5a0854d3..280f126e 100644 --- a/conformance/invalid/branch_inconsistent.eph +++ b/conformance/invalid/branch_inconsistent.eph @@ -1,6 +1,7 @@ -// SPDX-License-Identifier: PMPL-1.0-or-later +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell // Conformance test: branches consume different linear bindings — must be rejected. -// Expected: compile error "branches consume different linear resources" +// Expected: compile error E005 "branches consume different linear resources" fn example(cond: bool) -> i32 { let! x = 42; diff --git a/scripts/status-gate.sh b/scripts/status-gate.sh index 11718937..b4c601ec 100755 --- a/scripts/status-gate.sh +++ b/scripts/status-gate.sh @@ -20,7 +20,9 @@ extract_claim() { echo "$line" | grep -Eo '[0-9]+' | head -n 1 } -ROADMAP_PROOF_CLAIM="$(extract_claim "ROADMAP.adoc" "Coq admitted proofs remaining")" +# Single-source claim: PROOF-NEEDS.md §4 carries the canonical +# `Coq admitted proofs remaining: ` marker. ROADMAP.adoc no longer +# duplicates this; see the per-file table + seam audit in PROOF-NEEDS.md. PROOF_NEEDS_CLAIM="$(extract_claim "PROOF-NEEDS.md" "Coq admitted proofs remaining")" TEST_NEEDS_CLAIM="$(extract_claim "TEST-NEEDS.md" "Documented all-target tests")" @@ -30,10 +32,6 @@ ACTUAL_ADMITTED="$( | tr -d ' ' )" -if [ "$ROADMAP_PROOF_CLAIM" != "$ACTUAL_ADMITTED" ]; then - fail "ROADMAP.adoc claims ${ROADMAP_PROOF_CLAIM} admitted proofs, actual is ${ACTUAL_ADMITTED}" -fi - if [ "$PROOF_NEEDS_CLAIM" != "$ACTUAL_ADMITTED" ]; then fail "PROOF-NEEDS.md claims ${PROOF_NEEDS_CLAIM} admitted proofs, actual is ${ACTUAL_ADMITTED}" fi