From 82081a091ed8cd247f718a84d564fae951fa5372 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 17:37:19 +0000 Subject: [PATCH 1/4] docs: clarify preservation proof boundaries Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .machine_readable/6a2/STATE.a2ml | 13 +- CITATION.cff | 2 +- CLAUDE.md | 142 +++--- EXPLAINME.adoc | 356 ++++++++++---- PROOF-NEEDS.adoc | 288 ++++++----- README.adoc | 322 ++++++------- ROADMAP.adoc | 118 +++-- STATUS.adoc | 173 +++---- TEST-NEEDS.adoc | 12 +- V1-TO-V2.adoc | 97 ++-- brand/marr-levels.svg | 2 +- docs/proof-debt.adoc | 71 +-- docs/vision/EPHAPAX-VISION.adoc | 60 +-- docs/wikis/Home.md | 8 +- ephapax-linear/README.adoc | 7 +- formal/Counterexample.v | 30 +- formal/Counterexample_L2.v | 21 +- formal/Counterexample_L2_nested.v | 14 +- formal/Counterexample_PreservationL1.v | 11 +- formal/Counterexample_StepPop.v | 7 +- ...ALATION-4.8-leaf-rule-region-liveness.adoc | 12 +- formal/L1ChoreoExperiment2.v | 22 +- formal/PRESERVATION-DESIGN.adoc | 450 ++++++++++-------- formal/PRESERVATION-HANDOFF.adoc | 30 +- formal/PROOF-STATUS.a2ml | 95 ++-- formal/Semantics_L1.v | 176 ++++--- formal/TypingL1.v | 19 +- 27 files changed, 1455 insertions(+), 1103 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 42348534..1d22535d 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -5,10 +5,17 @@ # See: standards/a2ml-templates/STATE.a2ml.v2.spec.adoc @state(version="2.0"): +# current_* fields below supersede the 2026-06 journal text and the dated +# owner-directive snapshot; see CLAUDE.md and PROOF-NEEDS.adoc for policy. phase: "implementation" -next_action: "Phase D slice 4 Phase 3b Stages 2-4 (#240/#241/#242): Stage 1 (both 1a + 1b) complete. Stages 2-4 sequenced per the owner-approved 4-stage plan: Stage 2 (#240) ELam annotation extension — independent of Stage 1, ships when prioritised; Stage 3 (#241) CPS + relaxed Phase 3b — blocked on Stage 2; Stage 4 (#242) compound non-linear + unconditional preservation_l2 — blocked on Stage 3. Stage 4's destination collapses Stage 1b's three preconditions (P1 = tfuneff_lambda_free, P2 = regions_introduced_by ⊆ R_in_v, P3 = expr_closed_below 0 v) once typing-derived closure invariants land. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted`; no touching `Semantics.v` / `Typing.v` / `Counterexample.v`; no closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority." +next_action: "Owner-approved L1/L2 soundness redesign: preserve the legacy five-Qed counterexample and durable Admitted; do not prove the refuted step_pop_disjoint_from_type_l1 or preservation_l1 statements; do not claim unconditional L2 preservation. First classify each exact obligation under hyperpolymath/mathesis/estate-mathematical-architecture and standards/3-practice/PROOF-POLICY.adoc. Grade 3 is Agda-only; current Coq witnesses are not Grade 3, and Ephapax-specific engineering claims map to Idris2 unless an implementation-independent Agda theory statement is explicitly defined. Update the proof ledger after policy resolution; no proof build was run in this environment." last_action: "Proof + stdlib wave 2026-06-01 → 02 landed (13 PRs): canonical-forms L1 modality-polymorphic (#274, P43, 7 lemmas axiom-free, prerequisite for progress_l1/P42); Print Assumptions audit framework across L1 + L3 keystones (#270, closes P10/P32); step_pop_disjoint_from_type_l1 stated + EASY cases Qed-closed (#280, P06, HARD cases blocked on #240/#241/#242); Rust↔Coq is_linear_ty truth-table mechanical assertion (#273, P28); OwnershipKind from_byte/to_byte round-trip (#277, P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions as linear scopes (#275, D04), Allen's interval algebra (#272, D11), MessageHandle as linear typestate (#279, D17), monoidal aggregates (#281, D18); doc truth-restore + banned-preservation framing buried (#263); cluster-D L3/L4 status meander (#278); Track C panic-attack triage (#271); coq-build noble apt CI fix (#282, unblocks ~5 PRs); R5b standards SHA bump (#276). Plus CHANGELOG sync (#283). Build oracle clean across all 12 .v files. Print Assumptions: canonical_*_l1_m + most new lemmas zero-axiom; expected residuals (preservation_l1, region_liveness_at_split_l1_gen, region_shrink_preserves_typing_l1_gen_m) tracked. Stages 2-4 (#240/#241/#242) still un-touched. Wiki Proof-status.md refreshed 2026-06-02. | INFRA (2026-06-24, non-proof track): governance docs landed (#314 — CODEOWNERS/GOVERNANCE.adoc/MAINTAINERS.adoc); standards reusable-workflow pins remediated (#315) and current at d135b05 (#316); Hypatia neurosymbolic gate now active and reporting 37 pre-existing findings (5 crit / 7 high / 25 med) — triage handed off (docs/governance/HYPATIA-HANDOFF.md), standards visibility patch drafted-not-applied. No .v files touched; no proof-state change." -updated: 2026-06-24T18:13:15Z +current_last_action: "2026-11-01 proof-honesty audit: updated local status surfaces, retained all proof terms, and recorded Mathesis Grade 3/standards mapping without promoting Coq evidence to Grade 3. No Coq build run; coqc unavailable." +current_proof_boundary: "Legacy preservation is refuted and its Admitted is durable; step_pop_disjoint_from_type_l1 and modality-polymorphic preservation_l1 are refuted as stated; no unconditional preservation_l2 theorem is declared; preserve all Coq regressions." +current_grade_target: "Mathesis Grade 3 requested but not claimed. Grade 3 requires local Agda checking; current regressions are Coq. Standards proof policy maps repo-specific engineering claims to Idris2 unless an implementation-independent Agda theory statement is explicitly identified." +proof_policy_sources: ["https://github.com/hyperpolymath/mathesis/blob/main/estate-mathematical-architecture", "https://github.com/hyperpolymath/standards/blob/main/3-practice/PROOF-POLICY.adoc"] +proof_status_source: "PROOF-NEEDS.adoc + EXPLAINME.adoc proof ledger" +updated: 2026-11-01 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"): # Captured durable directive — preservation work is the four-layer redesign, @@ -107,7 +114,7 @@ updated: 2026-06-24T18:13:15Z # Doc lockdown: # CLAUDE.md — owner directive § # formal/PRESERVATION-DESIGN.md — CANONICAL banner -# formal/PRESERVATION-HANDOFF.md — ARCHAEOLOGY ONLY banner +# formal/PRESERVATION-HANDOFF.adoc — ARCHAEOLOGY ONLY banner # ROADMAP.adoc — closure-plan section removed @end @end diff --git a/CITATION.cff b/CITATION.cff index aa8edb2a..ba7d1842 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -2,7 +2,7 @@ cff-version: 1.2.0 message: "If you use this software, please cite it as below." type: software title: "Ephapax" -abstract: "Dyadic linear+affine type system for compile-time WASM memory safety — no use-after-free, no leaks, region-based allocation. Mechanically proved in Coq and Idris2." +abstract: "Research language exploring dyadic linear/affine typing, region-based allocation, and WebAssembly. Includes Coq and Idris2 proof artifacts; current counterexamples refute unrestricted legacy and L1 preservation, no unconditional L2 preservation theorem is established, and implementation refinement remains unproved." authors: - family-names: "Jewell" given-names: "Jonathan D.A." diff --git a/CLAUDE.md b/CLAUDE.md index cf6a7a4d..a99657ee 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -19,7 +19,7 @@ | Proofs | `formal/Semantics.v` (Coq), `src/abi/Ephapax/…` (Idris2) | None mechanized; `lib/borrow.ml` only | **Internal naming trap.** Ephapax itself is dyadic. Inside this repo: -- **ephapax-linear** = strict, formally-verified core. +- **ephapax-linear** = strict core with formal artifacts; no full language-soundness or implementation-refinement proof is claimed. - **ephapax-affine** = versatile prototyping companion to ephapax-linear. Both are *internal sublanguages*. They share one AST, one Rust crate (`ephapax-linear/`), one grammar directory. **The `ephapax-affine` sublanguage is NOT AffineScript.** The word `affine` is shared because both happen to be substructural-logic-family type systems — that's a logic-family fact, not a project relationship. @@ -59,50 +59,54 @@ When working in this repo, the typing system has four layers. Knowing which laye | **L3 — Echo residue** | "Is this about *what was lost* when an irreversible step fired?" | | **L4 — Dyadic mode** | "Is this a project-level mode declaration question?" | -Most questions touch exactly one layer. The design rationale is in `formal/PRESERVATION-DESIGN.md`. The verified counterexample that forced the redesign is in `formal/Counterexample.v` (3 lemmas under the legacy judgment + `bad_input_untypable_l1` under the new `has_type_l1`). +Proof and design history is in `formal/PRESERVATION-DESIGN.adoc`; current status is in `PROOF-NEEDS.adoc`. The legacy counterexample and the separate L1 regressions are in `formal/Counterexample.v`, `Counterexample_StepPop.v`, and `Counterexample_PreservationL1.v`. These prove exact counterexamples, not a sound replacement. -**Standing rule**: if a proposed change appears to require a side condition on a compound typing rule (e.g. "the sibling doesn't reference this region"), pause — the four-layer threading should make that side condition *derivable*, not stated. +**Standing rule**: if a proposed change appears to require a side condition on a compound typing rule (e.g. "the sibling doesn't reference this region"), do not assume it is derivable. The pinned L1 witnesses show that the current judgment does not encode the temporal dependency. Pause and propose an explicit judgment/step redesign; do not patch the false preservation theorem by strengthening a helper lemma. **Disambiguation reminder**: the names L1/L2/L3/L4 (layer names), `ephapax-linear`/`ephapax-affine` (L2 modes / the Rust crate), and `Linear`/`Affine` as used in echo-types (L3 modes) deliberately overlap because the underlying thin-poset construction is shared. Agents must disambiguate by context. ## Standing reminders -- Formal-proof work touches `formal/Semantics.v` + `formal/TypingL1.v` (Coq) and `src/abi/Ephapax/…/*.idr` (Idris2). Both build oracles are authoritative; `coqc` and `idris2 --check` are the only "is this proved?" answers. -- The legacy preservation closure plan is superseded by `formal/PRESERVATION-DESIGN.md` (four-layer redesign). `formal/PRESERVATION-HANDOFF.md` carries the historical diagnostic record only. -- Ephapax-affine type proofs are **NOT** done — `formal/` mechanises a single legacy judgment + L1's `has_type_l1`; there is no separate mechanised ephapax-affine until L2 + the Linear ⇒ Affine weakening lemma land. See `PRESERVATION-DESIGN.md §12.15`. +- Formal-proof work spans Coq, Idris2, and the applicable estate policy. Checker output is evidence only for the exact proposition and assumptions run; a green build does not establish general language soundness. +- The legacy preservation closure plan is obsolete. `formal/PRESERVATION-DESIGN.adoc` is design/history, not a proof result; `formal/PRESERVATION-HANDOFF.adoc` is historical diagnosis only. +- Modality and `linear_to_affine` artifacts are mechanised, but no unconditional L1/L2 preservation theorem is established. The modality-polymorphic L1 statement is refuted as stated; see `PROOF-NEEDS.adoc` and the EXPLAINME ledger. - All commits GPG-signed (key `4A03639C1EB1F86C7F0C97A91835A14A2867091E`), email `6759885+hyperpolymath@users.noreply.github.com`. Auto-merge ON for every PR. --- ## Orientation: this language is gestating — engage with v2 -**Read `V1-TO-V2.adoc` first.** Ephapax is *not* dead, broken, or -abandoned — it is part-way through a deliberate second draft on two -tracks (grammar and soundness proof), both landing. Do not read the -prohibitions below as "there is nothing to do here." They fence off -exactly **two** v1 artefacts; everything in v2 is open and wants work. +**Read `V1-TO-V2.adoc` first.** Ephapax is part-way through a deliberate +second draft on grammar and proof design. The legacy preservation theorem +is false, and later counterexamples also refute the current unrestricted +L1 preservation claim; L2 has no unconditional preservation theorem. +Do not read this as "there is nothing to do here": the active work is to +redesign and state sound replacement theorems, not to prove refuted ones. **Where the tractable work is (engage with this):** -- **Proof, L1** — close the residual L1 structural admits in - `formal/Semantics_L1.v` (list/multiset bridge; - `region_shrink_preserves_typing_l1_gen_m`; `TFun` effect typing). - These are *v2 design follow-ups*, not legacy patching. See - `PROOF-NEEDS.md §4`. -- **Proof, L3** — state + prove the **unconditional** `preservation_l3` - (currently conditional on an L1 admit). +- **Proof, L1** — do not attempt to close the unrestricted + `step_pop_disjoint_from_type_l1` or `preservation_l1` statements: + both are refuted by pinned Coq counterexamples. The open work is an + owner-approved judgment/step redesign with an explicit temporal + invariant, followed by a new theorem with a stated boundary. +- **Proof, L2** — no unconditional `preservation_l2` theorem exists. + Keep the fresh-region and nested-`TFunEff` counterexamples visible; + the existing β-case lemmas are conditional. +- **Proof, L3** — the Qed preservation result is scoped to matching + echo-emitting typing/step rules; it is not general L1/L2 preservation. - **Grammar, v2** — continue the phase work in `spec/ephapax-v2-grammar.ebnf` + the `v2_grammar_phase_*` CLI tests. - **Proof, L4** — Phase A scaffold landed; mother–child dyadic - semantics (`PRESERVATION-DESIGN.md §7`) is the next design step. + semantics (`PRESERVATION-DESIGN.adoc §7`) is the next design step. -## 🛑 Owner directive 2026-05-27 — the two fences (narrow, load-bearing) +## 🛑 Owner directive snapshot (2026-05-27) — legacy fence plus later L1 regressions -> The guardrails below are narrow by design. They stop one specific -> wasted path (several sessions burned hours trying to close a theorem -> that is *proven* unclosable). They do **not** mean "skip this repo." -> Engage with the v2 work listed above; just keep off the two fenced -> v1 artefacts. +> The guardrails below protect pinned counterexamples and the false +> statements they refute. They do **not** mean "skip this repo." The +> active work is redesigning sound judgments and theorem boundaries; +> do not try to prove legacy or L1 statements that have already been +> refuted. ### TL;DR @@ -110,14 +114,16 @@ Ephapax preservation as originally stated in `formal/Semantics.v` is **provably false** — and that is a *result*, not a defeat: `formal/Counterexample.v` exhibits a concrete configuration that types, steps, and lands at an untypable post-state (5 lemmas `Qed`), which -named the exact invariant the redesign needed. So the work is **not** to -close `Theorem preservation` in `Semantics.v` (no closure exists; the -`Admitted` is deliberate). The work is the **four-layer principled -redesign** (L1 region capabilities / L2 modality, now `m`-indexed into -`has_type_l1` / L3 echo / L4 dyadic mode) in -`formal/PRESERVATION-DESIGN.md`, where preservation is **re-derived -per layer** from explicit invariants. Three of the four layers already -carry `Qed` theorems — this is a healthy build, not a stalled one. +named an invariant missing from the legacy judgment. So the work is **not** +to close `Theorem preservation` in `Semantics.v` (no closure exists; the +`Admitted` is deliberate). Nor should the current unrestricted L1 +preservation be treated as routine debt: `Counterexample_StepPop.v` and +`Counterexample_PreservationL1.v` refute its supporting claim and capstone. +There is no unconditional L2 preservation theorem; the L2 β-case helpers +are conditional and later counterexamples document distinct gaps. The +four-layer architecture in `formal/PRESERVATION-DESIGN.adoc` is a design +program, not proof that the language is sound. Preserve each local +counterexample and state any replacement theorem with its exact boundary. ### DO NOT @@ -138,15 +144,13 @@ them if asked; if asked anyway, push back and link this section. invariant the counterexample demands; no lemma collection bolted onto it will help. -3. **DO NOT close any residual axiom in `formal/Semantics_L1.v` - (e.g. `region_liveness_at_split_l1` if it returns) by adding - proof tricks, side-conditions discharged ad-hoc, or strengthened - lemma signatures within the current judgment shape.** This is - *the same kind of patching that produced the legacy admits*, one - layer up. The post-L2-hybrid main carries the `Modality` - parameter directly in `has_type_l1`; closures that previously - looked like "an L1 fix" are now cross-layer and must be - reasoned-about at the layered level. +3. **DO NOT try to complete the current unrestricted + `step_pop_disjoint_from_type_l1` or `preservation_l1` statements in + `formal/Semantics_L1.v`.** Both are refuted by pinned witnesses; their + `Admitted.` markers are transparent boundaries, not ordinary debt. + Do not route around the counterexamples with ad-hoc side conditions or + helper-signature changes. A separately stated sound theorem after an + owner-approved judgment/step redesign is allowed and expected. 4. **DO NOT follow the "Preservation closure plan" steps in historical PRs / branches / comments.** Anything dated before @@ -162,28 +166,36 @@ them if asked; if asked anyway, push back and link this section. ### DO -1. **DO read `formal/PRESERVATION-DESIGN.md` first.** It is the - canonical design source. The four-layer architecture, the - missing-invariant statement, and the per-layer plan are all - there. - -2. **DO continue the layered build:** - - L1 (`TypingL1.v` + `Semantics_L1.v`): R-threading + modality - parameter (post-L2-hybrid). Residual admits are L1 design - follow-ups, not legacy patching. - - L2: modality landed in-place via PRs #176 + #177 - (`has_type_l1` now carries `m : Modality`; - `linear_to_affine` Qed with zero axioms). 6 L1 supporting - lemmas in `Semantics_L1.v` regressed to Admitted post-L2 — - bullet-structure rewrite needed for the 3 new Affine-only - constructors. - - L3 (`Echo.v`): K-free, forward-looking. Not wired into L1/L2 - judgments yet — that's L1 ⇒ L3 follow-up. - - L4: not started; design in §7 of the design doc. - -3. **DO derive preservation per-layer.** `preservation_l1` is - proved in the L1 vocabulary, against the L1 judgment, using L1 - invariants. The same shape for L2 / L3 / L4 as each lands. +1. **DO read `PROOF-NEEDS.adoc` and `EXPLAINME.adoc` for current status.** + `formal/PRESERVATION-DESIGN.adoc` records the architecture and history; + it is not evidence that a layer's preservation theorem is established. + +2. **DO continue the layered build without overclaiming:** + - L1 (`TypingL1.v` + `Semantics_L1.v`): the judgment and helper + lemmas exist, but the unrestricted preservation claim is refuted. + Replacement design is open; its theorem boundary must be explicit. + - L2: modality is mechanised and `linear_to_affine` is Qed, but + no unconditional `preservation_l2` theorem exists. Treat the + β-case lemmas as conditional and retain both L2 counterexamples. + - L3 (`Echo.v`): calculus and selected matching-rule preservation + results are Qed; do not generalise them to L1/L2. + - L4: scaffold/design only; no preservation theorem. + +3. **DO state and prove only sound replacement theorems.** A theorem + name or layer label does not make a statement true. First write the + exact judgment, transition relation, hypotheses, and boundary; then + prove it locally and report its assumptions and regressions. + +4. **DO follow estate proofing and grading policy.** Consult + `hyperpolymath/mathesis/estate-mathematical-architecture` for grades + and `hyperpolymath/standards/3-practice/PROOF-POLICY.adoc` for prover + mapping. Mathesis Grade 3 specifically requires a local Agda proof; + Coq `Qed` is Coq evidence, not Grade 3. Standards maps + Ephapax-specific engineering claims to Idris2 unless an + implementation-independent theory statement is explicitly defined. + Do not assign a Grade 3 label until that classification and exact + statement correspondence are recorded in `EXPLAINME.adoc` and + `PROOF-NEEDS.adoc`. 4. **DO escalate before patching.** If a proof attempt requires adding a side-condition to fix a sibling-region-disjointness @@ -214,7 +226,7 @@ Two questions to ask before touching `formal/`: in a new layer, not to admit it. 2. **Am I about to close an L1/L2/L3 admit by reasoning that - crosses layers?** If yes — check `PRESERVATION-DESIGN.md` for + crosses layers?** If yes — check `PRESERVATION-DESIGN.adoc` for the cross-layer dependency annotations. The layered design intentionally splits some closures across layers; trying to close them within one layer alone is the trap. diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 1e60f88d..ed901d2c 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -11,11 +11,11 @@ README.adoc is tied to a specific file, test, or proof obligation. [quote, README] ____ -A dyadic linear+affine type system for compile-time WebAssembly -memory safety. Resources are tracked through the type system so the -compiler can guarantee — without a garbage collector — that no value -is used after being freed, no resource is leaked, and region-scoped -allocations are deallocated in bulk at scope exit. +A research language for principled handling of irreversible boundaries +in WebAssembly. Ephapax aims to track resource use and typed evidence at +region exits and drops. Its local preservation obligations remain under +proof: the legacy theorem and current unrestricted L1 theorem are refuted, +and no unconditional L2 preservation theorem is established. ____ == Claim: Dyadic Type System (L2) @@ -33,8 +33,10 @@ L1 / L3 / L4 evidence follows below. * `BindingForm::Param` -- follows type linearity Tests `test_let_allows_unconsumed_linear` and `test_let_bang_rejects_unconsumed` -verify the distinction. `test_let_bang_rejects_unconsumed_unrestricted` proves -that `let!` enforces exactly-once even for unrestricted types like `I32`. +exercise the distinction. `test_let_bang_rejects_unconsumed_unrestricted` checks +that this implementation rejects `let!` without consumption for unrestricted +types like `I32`. These are behavioral tests, not a proof of language soundness +or compiler refinement. The Coq-side L2 evidence is `linear_to_affine : Linear ≤ Affine` (Qed, zero axioms) in `formal/Modality.v`. @@ -47,11 +49,14 @@ zero axioms) in `formal/Modality.v`. * `src/ephapax-syntax/` -- Core AST with binary sums, `case`/`inl`/`inr` * `src/ephapax-desugar/` -- Transforms surface to core -The Coq formal proofs (`formal/`) reason about the core AST only. New surface -features (pattern matching, named constructors) never invalidate the proofs. +The Coq formal artifacts (`formal/`) reason about the core AST only. Surface +features such as pattern matching and named constructors are not part of those +proofs. The desugar/type-check test below exercises the implementation, but no +formal preservation theorem currently connects the surface pipeline to the +Coq calculus. -Test `integration_desugar_typecheck_no_parser` in `ephapax-desugar` verifies the -full pipeline: surface AST -> desugar -> core AST -> type check. +Test `integration_desugar_typecheck_no_parser` in `ephapax-desugar` exercises the +pipeline: surface AST -> desugar -> core AST -> type check. == Claim: Pattern Matching Desugars to Binary Sums @@ -78,54 +83,50 @@ demonstrate where they diverge on identical programs (e.g. == Claim: Region-Based Memory -*Evidence*: `check_region` in `src/ephapax-typing/src/lib.rs` enforces: - -1. *NoRegionInType* -- return type must not reference the region (no escape) -2. *Consumption at region exit* -- only bindings that `demands_consumption()` must - be consumed; affine bindings are implicitly dropped - -Test `test_region_non_escaping` verifies escape detection. -Test `test_region_string_allocation` verifies in-region allocation. - -== Claim: Sibling-safe region capabilities (L1) - -*Evidence*: Region capabilities are threaded as input/output -environments through every compound typing rule. A sibling cannot -reference a region a previous sibling has exited — this is the -soundness invariant the legacy judgment was missing. - -* Counterexample at `formal/Counterexample.v` (all five lemmas - `Qed`) demonstrates the soundness gap the threading fixes. -* The new `has_type_l1` judgment lives in `formal/TypingL1.v` and - carries the R-threading directly. Step relation at - `formal/Semantics_L1.v`. -* Design rationale at `formal/PRESERVATION-DESIGN.md §3-§4`. -* 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`). +*Implementation evidence*: `check_region` in `src/ephapax-typing/src/lib.rs` +checks that the return type does not reference the region and that bindings +marked `demands_consumption()` are consumed at region exit. The tests +`test_region_non_escaping` and `test_region_string_allocation` exercise this +checker behavior. These tests do not establish a theorem connecting the Rust +checker or runtime to the Coq calculus. + +== Claim: Region capability threading (L1; soundness boundary open) + +*Evidence*: `has_type_l1` threads region environments through compound +rules in `formal/TypingL1.v`. This is the redesign's intended capability +accounting, but the current judgment does **not** establish that a region +used by a surviving sibling remains live across another sibling's step. + +* `formal/Counterexample.v` contains five Qed lemmas. Three prove the + legacy witness types, steps, and becomes untypable; the L1 regression + proves only that this particular input is rejected in both modes. +* `formal/Counterexample_StepPop.v` refutes the unrestricted + `step_pop_disjoint_from_type_l1` statement. +* `formal/Counterexample_PreservationL1.v` refutes the + modality-polymorphic `preservation_l1` statement through its Linear + instance. It does not establish that a separate Affine-only statement + is false. +* The local proof artifacts are Coq evidence only. The exact open + replacement boundary and Grade 3 policy are in `PROOF-NEEDS.adoc`. == Claim: Irreversibility residue is first-class (L3, wired) -*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. +*Design*: The L3 calculus models typed residues for selected irreversible +operations, drawing on the `echo-types` formulation. This does not establish +that all runtime region exits/drops emit or discharge residue; the local Qed +preservation results are scoped to the matching rules listed below. * Upstream theory at `~/developer/repos/echo-types/proofs/agda/EchoLinear.agda` (lines 30–101), already mechanised. * 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`. +* Forward-looking design at `formal/PRESERVATION-DESIGN.adoc §6`. * 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). + and the `preservation_l3` umbrella in `Semantics_L1.v` are Qed for + their matching echo-emitting rule pairs. These scoped results do not + establish general L1/L2 preservation. == Claim: Dyadic mode is project-level only (L4) @@ -134,8 +135,8 @@ Affine mode permits silent lowering. `program_mode_to_modality` (total mapping to L2's modality). No theorems, no admits, no axioms — by design. -* Companion design note: `formal/L4-DYADIC.md`. -* Canonical design source: `formal/PRESERVATION-DESIGN.md §7`. +* Companion design note: `formal/L4-DYADIC.adoc`. +* Canonical design source: `formal/PRESERVATION-DESIGN.adoc §7`. * Surface syntax for the L4 declaration (`#![ephapax_linear]` / `#![ephapax_affine]` / `#![module_boundary_mix(...)]`) is not yet wired into the parser @@ -152,7 +153,7 @@ theorems, no admits, no axioms — by design. | *Rust* | Compiler implementation language | *Pest (PEG)* | Parser generator -- surface + core grammars | *WASM* | Compilation target -- portable, sandboxed, near-native -| *Coq* | Formal proofs of core calculus soundness +| *Coq* | Core-calculus proof artifacts and counterexample regressions; general preservation remains unproved/refuted as documented | *Idris 2* | ABI definitions with dependent type proofs | *Zig* | FFI implementation (C-compatible, cross-compilation) |=== @@ -167,9 +168,9 @@ theorems, no admits, no axioms — by design. | Core language design — affine (`let`) and linear (`let!`) bindings enforced by the type checker in `src/ephapax-typing/src/lib.rs` | gossamer (`src/core/Bridge.eph` uses `let!` for window handles and IPC channels); all Ephapax-backed applications in the account -| *Coq formal proofs* -| `formal/` — progress and preservation theorems for the core calculus; two-layer AST keeps proofs stable as surface language grows -| ephapax-pipewire proving ground (PipeWire filter-node linearity); proven repo (`formal/coq/` — 48 Qed / 1 Admitted estate-wide) +| *Coq formal artifacts* +| `formal/` — local typing/semantics lemmas and pinned counterexamples. The legacy and unrestricted L1 preservation claims are refuted; no unconditional L2 preservation theorem is established. +| ephapax-pipewire proving ground (PipeWire filter-node linearity); local evidence remains Coq-specific and does not establish Ephapax implementation refinement | *Idris2 ABI + Zig FFI standard* | `idris2/` ABI definitions; Zig FFI layer per the hyperpolymath ABI/FFI universal standard @@ -211,9 +212,11 @@ theorems, no admits, no axioms — by design. | `conformance/` | Conformance test suite (valid/invalid programs) |=== -== Claim: Mechanically Proved Soundness +== Claim: Formal Proof Artifacts and Soundness Boundary -*Evidence*: Two complementary formalisations, both run on every push. +*Evidence*: Coq and Idris2 formal artifacts are present. CI build success +checks compilation, not the truth of every intended language-level theorem; +the exact preservation boundary is recorded below. === Coq (`formal/`) @@ -226,16 +229,19 @@ configuration that types under the legacy judgment, steps via the operational semantics, and lands at an untypable post-state. The `Admitted.` on `Theorem preservation` is correct — no proof closes it. -The post-discovery work is the **four-layer principled redesign** -documented in `formal/PRESERVATION-DESIGN.md`, where preservation is -*re-derived per layer* from explicit invariants. Any earlier-in-this- -README counts of "910 → 22 → 12 open goals" are archaeology, not -instructions. See `STATUS.adoc` for the past/present/future map. +The post-discovery architecture is a design program, not yet a sound +replacement. The unrestricted L1 preservation statement is refuted by +`Counterexample_PreservationL1.v`; L2 has no unconditional preservation +theorem, and its counterexamples constrain the β-case helpers. L3's Qed +results are scoped to matching echo rules. Any earlier-in-this-README +counts of "910 → 22 → 12 open goals" are archaeology, not instructions. +See `STATUS.adoc` and `PROOF-NEEDS.adoc` for current boundaries. ==== -The Coq formalisation is now layered. Each layer has its own -judgment, its own invariants, and its own per-layer preservation -theorem. +The Coq formalisation has layered judgments and infrastructure, but +not a soundness theorem for every layer. L1's unrestricted preservation +claim is refuted, L2 has no unconditional preservation theorem, and L3's +Qed results are scoped to matching echo rule pairs. [cols="3,1,3"] |=== @@ -250,8 +256,8 @@ theorem. | `formal/TypingL1.v` — modality-indexed, R-threaded | L1 semantics -| 🟡 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. +| 🛑 Current unrestricted preservation statements refuted +| `formal/Semantics_L1.v` has two outer `Admitted.` markers: `step_pop_disjoint_from_type_l1` and `preservation_l1`. Both unrestricted statements have pinned Coq counterexamples; they are not routine open proof debt. See `PROOF-NEEDS.adoc`. | L2 modality (`Modality.v`) | ✅ Core landed (1 Qed, 0 axioms) @@ -259,11 +265,11 @@ theorem. | L3 echo / residue calculus | ✅ 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`. +| `formal/Echo.v` — one type former (fiber `Echo f y := Σ x. f x ≡ y`) + degrade map + no-section-collapse-to-residue proof. The Qed wiring lemmas cover matching echo-emitting rule pairs only; they do not prove general L1/L2 preservation. | L4 dyadic interaction | ✅ 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`. +| `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` enum + `program_mode_to_modality` round-trip. No theorems by design. Design in `formal/PRESERVATION-DESIGN.adoc §7`. | Legacy `Theorem preservation` (`formal/Semantics.v`) | 🛑 Provably false (Admitted) @@ -271,19 +277,134 @@ theorem. |=== What's done = `Modality.linear_to_affine` (Linear ⇒ Affine weakening, -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`. +zero axioms), the L1 judgment and helper lemmas, the L3 calculus and +scoped matching-rule preservation results, the L4 Phase A scaffold +(definitions only), and pinned counterexample regressions. What's open = +redesign the L1 judgment/step interface and state sound replacement +theorems; L2 has no unconditional preservation theorem and its β-case +helpers remain conditional. What's banned = trying to prove the false +legacy or current unrestricted L1 statements, masking counterexamples, +adding new `Axiom` declarations, or conflating `ephapax-affine` (this +repo's sublanguage) with `AffineScript` (a separate language at +`hyperpolymath/affinescript`). Full boundary in `PROOF-NEEDS.adoc`. + +== Proof Ledger + +This ledger follows the estate proof-ledger vocabulary. “Proven” rows record +existing local Coq propositions with Qed proof terms; they do not imply that +the language implementation refines the calculus. The source baseline for +this audit is `800030f3c92536cce57acb5e82da6cf27b942826`; proof-status files +name the relevant scripts. The Coq 8.18.0 build recipe is +`cd formal && coq_makefile -f _CoqProject -o build.mk && make -f build.mk`. +`coqc` is unavailable in this editing environment. The 2026-10-27 CI run +`40435929887` succeeded overall but its Coq build job was skipped, so it is +not a proof-build receipt. No fresh build is claimed here; the source proof +scripts and theorem statements were not changed in this audit, only their +documentation comments were clarified. + +[cols="2,1,2,2,3",options="header"] +|=== +|Obligation / result |Status |Checker (version, flags) |Where |Trust boundary + +|The legacy `+preservation+` statement is false as stated |proven +|Coq 8.18.0; project build recipe above +|`+formal/Counterexample.v+`: `+bad_typable+`, `+bad_step+`, `+bad_post_untypable+` +|Concrete witness refutes the legacy universal statement only. It proves +no redesign or implementation refinement; retain the separate legacy +`+Admitted.+` unchanged. + +|`+step_pop_disjoint_from_type_l1+` is false as stated |proven +|Coq 8.18.0; project build recipe above +|`+formal/Counterexample_StepPop.v+`: `+step_pop_disjoint_from_type_l1_FALSE+` +|One typed step removes a region free in the result type. This refutes the +unrestricted helper; it does not prove a replacement with added premises. + +|The modality-polymorphic `+preservation_l1+` statement is false |proven +|Coq 8.18.0; project build recipe above +|`+formal/Counterexample_PreservationL1.v+`: `+preservation_l1_FALSE+` +|The refuting instance is Linear; the pre-state also types in Affine. This +witness alone does not refute a separate Affine-only theorem. + +|Unrestricted L1 region shrinking is false |proven +|Coq 8.18.0; project build recipe above +|`+formal/Counterexample_RegionShrink.v+`: `+region_shrink_is_FALSE+` (six Qed witnesses/lemmas) +|Two nested active regions consume duplicate ambient entries; removing one +entry breaks typing despite strict syntactic freeness. The old universal +helper is not proof debt. + +|Restricted L1 region-shrink replacement |proven +|Coq 8.18.0; project build recipe above +|`+formal/Semantics_L1.v+`: `+region_shrink_msperm+`, `+region_shrink_neutral+`, `+region_shrink_value+` +|Requires output multiset-permutation; value/neutral corollaries cover the +actual call sites. This restricted result does not restore unrestricted +region shrinking or general preservation. + +|L1 no-exit liveness and strengthened substitution helpers |proven (conditional) +|Coq 8.18.0; project build recipe above +|`+formal/Semantics_L1.v+`: `+region_liveness_no_exit_l1_gen+`, `+subst_preserves_typing_l1+` +|No-exit premise is explicit; these lemmas support restricted substitution +and do not prove preservation for arbitrary operational steps. + +|Linear-to-Affine weakening `+linear_to_affine+` |proven +|Coq 8.18.0; project build recipe above; zero axioms as recorded +|`+formal/TypingL1.v+` (`+Modality+` definitions in `+formal/Modality.v+`) +|Shows the local modality weakening relation only. It does not prove +L1/L2 preservation for either mode. + +|L2 β-case helper family |proven (conditional) +|Coq 8.18.0; project build recipe above +|`+formal/TypingL2.v+`: `+preservation_l2_app_eff_beta_linear_l1+`, `+_linear+`, `+_ground_nonlinear_l1+`, `+_ground_nonlinear+`, `+_tfuneff_l1+`, `+_tfuneff+` +|Requires the exact value/type/effect premises in each lemma. The +`+TFunEff+` case also requires `+tfuneff_lambda_free+`, the region-introduction +subset condition, and closure below zero. These are restricted β-case +lemmas, not unconditional L2 preservation. + +|L3 matching echo-rule preservation results |proven (scoped) +|Coq 8.18.0; project build recipe above +|`+formal/Semantics_L1.v+`: `+preservation_l3_region_active_echo+`, `+preservation_l3_drop_echo+`, `+preservation_l3+` +|Only matching echo-emitting typing/step-rule pairs; does not establish +general L1/L2 preservation or implementation refinement. + +|Fresh-region L2 β witness (input types, steps, result is untypable at L1) |proven +|Coq 8.18.0; project build recipe above +|`+formal/Counterexample_L2.v+`: `+e_before_typed+`, `+e_step+`, `+e_after_untypable+` +|Exact `+TFunEff+`/fresh-region witness only. It motivates restricted β +lemmas; it is not a full L2 preservation theorem. + +|Nested-`+TFunEff+` L2 β witness (input types, steps, result is untypable at L1) |proven +|Coq 8.18.0; project build recipe above +|`+formal/Counterexample_L2_nested.v+`: corresponding three witness lemmas +|Exact nested-lambda witness only. Its conditions distinguish this gap +from the fresh-region case; it is not full L2 preservation. + +|Sound replacement for unrestricted L1 preservation |open +|— +|`+PROOF-NEEDS.adoc+`; no replacement theorem is yet stated +|Requires a sound judgment/step boundary and explicit temporal invariant; +all L1 regressions remain mandatory controls. + +|Unconditional `+preservation_l2+` |open +|— +|No such theorem is declared in the current tree; see `+formal/TypingL2.v+` +|Current β-case helpers are conditional; `+preservation_l2_via_l1+` +transparently depends on the refuted L1 statement. + +|Mathesis Grade 3 receipt for Ephapax language soundness |open (target) +|Agda receipt required by the Mathesis architecture +|No Agda Grade 3 proof currently recorded +|The existing witnesses are Coq, not Grade 3. Standards classifies local +Ephapax-specific typing/step claims as engineering (Idris2) unless a genuine +implementation-independent theory statement is defined. Resolve this +mapping before assigning a Grade 3 label; see `+PROOF-NEEDS.adoc+`. +|=== + +Grade labels are not interchangeable with this ledger's statuses. Per +`+hyperpolymath/mathesis/estate-mathematical-architecture+`, Grade 3 means +locally checked in Agda without independent translation. Per +`+hyperpolymath/standards/3-practice/PROOF-POLICY.adoc+`, engineering and +theory obligations follow different verifier routes. Therefore no Coq +`+Qed+` row above is labelled Grade 3, and no upstream or cross-repo +conceptual result discharges an Ephapax-specific obligation. === Idris2 (`idris2/src/Ephapax/` + `src/formal/`) @@ -349,12 +470,72 @@ properties of the region-linear calculus: |=== All five with zero `believe_me`, zero postulates, under `%default -total`. +total`. Scope caveat: `regionSafetyExtract` and `noGCExtract` return +proof witnesses supplied as inputs; their proof terms are valid but their +stated results are vacuous wrappers, not standalone region-safety or +GC-freedom theorems. + +=== Idris2 Proof Ledger + +These rows record existing Idris2 source proofs and their exact scope; they +do not establish that the Rust implementation refines the formal model. +The source baseline is `800030f3c92536cce57acb5e82da6cf27b942826`. +`idris2` is unavailable in this editing environment, so there is no fresh +build receipt. The repository documents Idris2 0.8.0 and builds the formal +package with `cd src/formal && idris2 --build ephapax-formal.ipkg`; the CI +workflow currently uses a mutable `snazzybucket/idris2:latest` image tag, +so this is not a reproducibly pinned toolchain receipt. + +[cols="2,1,2,2,3",options="header"] +|=== +|Obligation / result |Status |Checker (version, flags) |Where |Trust boundary + +|Static no-escape proposition `+noEscapeTheorem+` |proven +|Idris2 0.8.0; `%default total`; package build above (historically reported, not rerun here) +|`+src/formal/Ephapax/Formal/RegionLinear.idr:129+` +|Proves the indexed type-level contradiction `+NoRegionInType r (Scoped r a) -> Void+`. It does not establish runtime escape-freedom or connect to Coq/Rust semantics. + +|Qualifier orthogonality `+orthogonalityLemma+` |proven +|Idris2 0.8.0; `%default total`; package build above (historically reported, not rerun here) +|`+src/formal/Ephapax/Formal/RegionLinear.idr:164+` +|Transports a `+CannotEscape+` witness across a qualifier change in the local datatype. It is not a language preservation theorem. + +|Region safety extraction `+regionSafetyExtract+` and GC extraction `+noGCExtract+` |proven (vacuous wrappers) +|Idris2 0.8.0; `%default total`; package build above (historically reported, not rerun here) +|`+src/formal/Ephapax/Formal/RegionLinear.idr:139,151+` +|Return supplied input witnesses unchanged. They prove no standalone runtime region-safety or GC-freedom property. + +|Linear split coverage `+splitLinearCoverage+` |proven +|Idris2 0.8.0; `%default total`; package build above (historically reported, not rerun here) +|`+src/formal/Ephapax/Formal/Qualifier.idr+` +|For an indexed `+Split+`, each linear binding at any context position occurs in at least one branch. It does not prove exclusivity or consumption consistency across arbitrary language control flow. + +|Region outlives transitivity `+outlivesTransitive+` |proven +|Idris2 0.8.0; `%default total`; package build above (historically reported, not rerun here) +|`+src/formal/Ephapax/Formal/Region.idr:72+` +|Pure transitivity of the abstract outlives relation; no operational safety or compiler-refinement result. + +|FFI result-code round trip `+compileResultRoundTrip+` |proven +|Idris2 0.8.0; `%default total`; `+idris2 --build ephapax-abi.ipkg+` (historically reported, not rerun here) +|`+src/abi/Ephapax/ABI/Foreign.idr:108+` +|Case analysis for the local enum/int mapping only; not evidence that Rust/WASM compilation succeeds or preserves source typing. + +|ABI seam E1/E2-control-flow/E3-runtime/E4/E5/E6 obligations |open / erased postulates +|Idris2 package build checks declarations, not discharged proofs +|`+src/abi/Ephapax/ABI/Invariants.idr+`; register in `+PROOF-NEEDS.adoc+` §5.3 +|Declarations state owed obligations (type preservation, control-flow consumption, runtime no-escape, no-GC, WASM typing, IR semantics). They are not proof receipts; E2 position-form and E3 static form are separately discharged as above. +|=== + +Idris2 evidence follows the Standards route for repository-specific +engineering claims, but it is not thereby Mathesis Grade 3: Grade 3 +requires a locally checked Agda proof. The current Coq and Idris2 rows +must retain their checker labels and cannot be upgraded by cross-repo +vocabulary or by the proof-policy mapping alone. == Test Evidence 357 tests across 17 active workspace crates + `tests/fuzz`, 0 -failures (per `cargo test --all-targets`; see `TEST-NEEDS.md` for +failures (per `cargo test --all-targets`; see `TEST-NEEDS.adoc` for the per-crate breakdown). Key test categories: * *Type checker dyadic tests*: `let` vs `let!` semantics, branch @@ -378,12 +559,13 @@ the per-crate breakdown). Key test categories: * `docs/specs/LANGUAGE-COMPARISON.adoc` — comparison against 10 languages * `docs/vision/EPHAPAX-VISION.adoc` — design rationale, why dyadic + regions + WASM -* `formal/PRESERVATION-HANDOFF.md` — *archaeology only*: per-case +* `formal/PRESERVATION-HANDOFF.adoc` — *archaeology only*: per-case checklist from the pre-2026-05-26 legacy-judgment closure plan, retained for historical context. The legacy `preservation` is - provably false; the path forward is the per-layer theorems documented - in `formal/PRESERVATION-DESIGN.md`. -* `PROOF-NEEDS.md` — outstanding proof obligations + leverage + provably false; the design document records an architecture, not an + established soundness result. Current proof boundaries and replacement + obligations are in `PROOF-NEEDS.adoc`. +* `PROOF-NEEDS.adoc` — outstanding proof obligations + leverage == Questions? diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index b8782aa6..b4ac9902 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -4,8 +4,10 @@ ____ === 🛑 First-read disambiguation (human + machine readers) *This document is for `+hyperpolymath/ephapax+`.* Ephapax is a research -language for compile-time WebAssembly memory safety, formally verified -in Coq + Idris2. +language for compile-time WebAssembly memory safety with formal artifacts +in Coq and Idris2. Current Coq counterexamples refute legacy and +unrestricted L1 preservation; no unconditional L2 theorem or +implementation-refinement proof is established. *Ephapax is NOT `+hyperpolymath/affinescript+`.* AffineScript is a separate, unrelated language (JS/TS/AffineScript successor, OCaml + @@ -27,10 +29,79 @@ ____ === Reading guide -This file is the _proof-debt audit_ for Ephapax post-counterexample -(2026-05-26). It supersedes earlier versions of `+PROOF-NEEDS.md+` that -still referenced the legacy preservation closure plan as if it were -viable. +This file is the proof-status audit for Ephapax. It supersedes earlier +versions that treated the legacy preservation closure plan as viable. +Keep these categories distinct: + +* *Legacy archaeology*: the original `+preservation+` statement is false; + its durable `+Admitted.+` and pinned five-`+Qed+` regression in + `+formal/Counterexample.v+` are intentional and must remain together. +* *Redesigned judgments*: L1/L2 change typing interfaces; conceptual + vocabulary or results from another repo do not discharge Ephapax's + language-soundness obligations. +* *Proved regressions*: counterexamples and positive controls are + machine-checked evidence about exact statements, not general preservation + theorems. +* *Genuinely open obligations*: only unrefuted statements belong here. A + refuted theorem requires an explicit redesign or restricted replacement, + not an attempt to prove the old claim. + +The current preservation boundary is: + +[cols="18%,26%,56%",options="header"] +|=== +|Layer |Status |Evidence / boundary +|Legacy |*False as stated; pinned archaeology* |`+Counterexample.v+` has +5 `+Qed+` lemmas. Keep the one durable `+Admitted.+` in +`+Semantics.v+`; do not relabel it ordinary debt or replace it with a fake +proof. +|L1 |*Current universal statement false as stated* |`+Counterexample_StepPop.v+` +refutes `+step_pop_disjoint_from_type_l1+`; `+Counterexample_PreservationL1.v+` +refutes the modality-polymorphic `+preservation_l1+` via its Linear +instance (the pre-state witness types in both modes). It does not by itself +refute a separate Affine-only theorem. The existing +`+bad_input_untypable_l1+` only rejects the original legacy witness; it does +not establish L1 preservation. +|L2 |*No unconditional theorem established* |`+preservation_l2+` is not +declared as a theorem in the current tree. `+Counterexample_L2.v+` and +`+Counterexample_L2_nested.v+` witness distinct β-preservation gaps. The +Qed β-case lemmas in `+TypingL2.v+` are conditional and do not assert the +refuted unrestricted claim. +|Replacement work |*Open design obligation* |Specify sound judgments / +side conditions and state exact replacement preservation theorems. These +are new obligations; the refuted legacy and L1 statements remain pinned. +|=== + +==== Estate proofing policy and Grade 3 target + +Follow the estate's canonical references for proof method and grade: + +* link:https://github.com/hyperpolymath/mathesis/blob/main/estate-mathematical-architecture[`hyperpolymath/mathesis/estate-mathematical-architecture`] + defines Grade 3 as an Agda proof that type-checks locally and has not been + independently translated. Grade 2/1 claims require their separate + translation/API evidence. +* link:https://github.com/hyperpolymath/standards/blob/main/3-practice/PROOF-POLICY.adoc[`hyperpolymath/standards/3-practice/PROOF-POLICY.adoc`] + assigns implementation-specific engineering obligations to Idris2 and + implementation-independent theory to Agda, rechecked in Rocq and Lean. + Its deciding test is whether a claim names a repository-specific type, + function, or wire format. The + link:https://github.com/hyperpolymath/standards/blob/main/docs/README-EXPLAINME-STANDARD.adoc[proof-ledger standard] + also requires every claimed proof (including open/refuted claims) to + appear in `+EXPLAINME.adoc+` with status, checker, location, and trust + boundary. + +*Grade 3 is the requested target, not a status to apply retroactively.* The +current regression witnesses are Coq scripts (`+Qed+`), so they are not +Mathesis Grade 3 receipts. The Ephapax-specific `+has_type_l1+`/`+step+` +claims also appear engineering-specific under the current standards mapping; +that mapping does not automatically make them Agda theory. Until an +owner-approved formulation resolves this boundary, record current Coq +results as Coq evidence, retain `+COUNTEREXAMPLE+` for refuted statements, +and do not label them Grade 3. A future Agda Grade 3 receipt must include +the exact proposition, assumptions, source commit, pinned Agda/toolchain, +canonical invocation, and evidence that it is the same Ephapax statement; +it must not be inferred from shared vocabulary or another repository's +proof. No Grade 2/1 claim is made here. The audit is split by sublanguage: @@ -41,7 +112,7 @@ The audit is split by sublanguage: For the architectural background see link:STATUS.adoc[`+STATUS.adoc+`] and -link:formal/PRESERVATION-DESIGN.md[`+formal/PRESERVATION-DESIGN.md+`]. +link:formal/PRESERVATION-DESIGN.adoc[`+formal/PRESERVATION-DESIGN.adoc+`]. ''''' @@ -81,8 +152,10 @@ TFunEff). Slice 4 L3 wiring delivered `+weaken_modality+` family (5), `+preservation_l2_via_l1+` (conditional on `+preservation_l1+`), `+linear_value_retype_l1_m+`, and 3 `+preservation_l2_app_eff_beta_*+` variants (Linear / ground_nonlinear / -tfuneff conditional on Stage 1b side conditions P1+P2+P3). Stage 2/3/4 -(#240/#241/#242) drop the conditions. +TFunEff conditional on their listed side conditions). The separate L2 +counterexamples below show why these restrictions matter; planned Stages +2/3/4 are not evidence that the unrestricted theorem has been proved, and +no unconditional `+preservation_l2+` is present in this tree. |L4 labelling scaffold (Phase A, 2026-05-28) |`+formal/L4.v+` |`+ProgramMode+` enum (`+PModeLinear+` / `+PModeAffine+` / @@ -94,8 +167,11 @@ Definitions only — no theorems, zero axioms. |5 + 5 Qed pinning the Phase 4c (fresh-region scope crossing) and Phase 3b (nested TFunEff) soundness-gap classes -|Counterexample regression witness |`+formal/Counterexample.v+` |5 Qed -(`+bad_input_untypable_l1+` proved under both modes) +|Pinned legacy counterexample + L1 positive regression +|`+formal/Counterexample.v+` |5 Qed in total: three lemmas establish the +legacy counterexample; `+t_loc_l1_R_preserving+` supports the L1 argument; +`+bad_input_untypable_l1+` rejects this one input in both modes. This is +not a proof of L1 preservation. |Operational checker (Rust, ephapax-linear sublanguage) |`+ephapax-linear/src/linear.rs+` |working — discharges resource-exact @@ -121,14 +197,13 @@ graceful abandonment |Affine-mode echo discipline (LEcho Affine = lowered triple) |`+formal/Echo.v+` (calculus) |calculus done; rule wiring pending -|Affine forward progress lemmas |`+formal/Semantics_L1.v+` -|bullet-structure rewrites + `+subst_typing_gen_l1_m+` + -`+region_shrink_preserves_typing_l1_gen_m+` m-polymorphic -generalisations landed 2026-05-27; Phase 3b Stage 1a + 1b landed -2026-05-30/31 via #252 + #253. Remaining admits are pre-existing L1 -structural debt + one provably-false-as-stated sub-case -(`+Semantics_L1.v:1994+` / mirror `+:2014+` — closure requires Phase D -reformulation, not direct proof). See §4 seam audit. +|L1/L2 conditional helper infrastructure |`+formal/Semantics_L1.v+` and `+formal/TypingL2.v+` +|Stage 3b and β-case helpers landed with explicit premises; they are not +unconditional preservation theorems. The unrestricted region-shrink helper +and former region-liveness lemma were refuted and removed; the restricted +`+region_shrink_msperm+`/value/neutral results are Qed. Two outer L1 +`+Admitted+` markers remain, and both unrestricted statements are now +refuted by pinned counterexamples (see §1 boundary and §4 seam audit). |=== ==== Counterexample regression @@ -144,13 +219,15 @@ in both Linear and Affine modes configuration |=== -→ The counterexample establishes the gap. The new L1 judgment closes it. +→ The L1 judgment rejects the *specific legacy input*. The later +`+Counterexample_PreservationL1.v+` shows that this local regression does +not make the current L1 preservation theorem sound. ''''' === §2. What’s todo -==== Near-term (L1 ⇒ L2 integration debt — mechanical) +==== L1/L2 preservation boundary (historical lemmas vs. open redesign) [width="100%",cols="34%,33%,33%",options="header",] |=== @@ -172,25 +249,25 @@ m-polymorphic helper (residual list-vs-multiset structural admit isolated to T_Region_Active_L1 shadowed case inside _gen_m) |`+formal/Semantics_L1.v+` |done 2026-05-27 (L2-β follow-up #3) -|Close T_Region_Active_L1 [rr = r] shadowed sub-case of -region_shrink_preserves_typing_l1_gen_m (list-vs-multiset bridge — -option (a) L1 perm lemma, (b) multiset reformulation, or (c) -T_Region_*_L1 redesign per the case’s own note) -|`+formal/Semantics_L1.v+` |structural; non-trivial — investigation -owed; lambda-body’s shadowing internal ERegion is the obstacle +|✅ Replace the unrestricted region-shrink helper |`+formal/Semantics_L1.v+`, +`+Counterexample_RegionShrink.v+` |the unrestricted statement is refuted; +`+region_shrink_msperm+` and the value/neutral corollaries are Qed. Do not +attempt to prove the old unrestricted helper. -|State and prove `+preservation_l1+` for both modes -|`+formal/Semantics_L1.v+` |depends on region_shrink + region_liveness -narrow admit +|Redesign the L1 judgment / step interface and state a sound replacement +for `+preservation_l1+` |`+formal/Semantics_L1.v+`, +`+Counterexample_PreservationL1.v+` |open design obligation; the current +unrestricted statement is refuted and must not be treated as closable debt |=== -==== Near-term (L3 wiring — design + mechanisation) +==== L3 wiring (scoped result; not general preservation) -L3 calculus is done in `+formal/Echo.v+` (12 Qed, no admits). What’s -missing is the _integration_ into the typing judgment and the step -rules. The shape is laid out in `+formal/PRESERVATION-DESIGN.md §6.3+` -"`Where echo enters the typing rules`" and (for the diagram) in §6 (to -be added). +The L3 calculus and its specific typing/step-rule integration are present. +`+preservation_l3_region_active_echo+`, `+preservation_l3_drop_echo+`, and +`+preservation_l3+` are Qed for their matching echo-emitting cases. These +results are scoped to those rule pairs; they do not repair or imply general +L1/L2 preservation. See `+formal/Semantics_L1.v+` and +`+formal/PRESERVATION-DESIGN.adoc+` for the exact theorem statements. [width="100%",cols="34%,33%,33%",options="header",] |=== @@ -247,9 +324,9 @@ plus an umbrella `+preservation_l3+` (their conjunction, Qed). Zero new admits or axioms. Per-case alignment forced by `+T_Echo_L1+`’s witness-type premise; non-deterministic crossover cases are non-preserving by design (typing derivation pins the path). -Conditionally Qed under the pre-existing -`+region_shrink_preserves_typing_l1_gen_m+` L1 structural admit per -PRESERVATION-DESIGN.md §5.1. +Qed for the stated matching echo paths; this is not a general L1/L2 +preservation theorem and has no dependency on the refuted unrestricted +region-shrink statement. |⏸ Register `+TEcho+` as linear via `+is_linear_ty+` (Phase B Slice 1) — DEFERRED 2026-05-28 |Realises the design intent annotated at @@ -292,14 +369,14 @@ effect-typed TFun) introduces the natural setting: lambda bodies’ R-flow becomes effect-typed, which gives the structural invariant that lets body-input-shrinkage discharge. The 2 admits at lines 553/621 remain as documented L1 debt, and the outer `+Admitted.+` at line 653 + the -`+preservation_l3+` dependency annotation in PRESERVATION-DESIGN.md §5.1 +`+preservation_l3+` dependency annotation in PRESERVATION-DESIGN.adoc §5.1 continue to attribute them correctly. |=== ==== Mid-term (L4 — scaffold landed 2026-05-28) L4 covers dyadic interaction semantics (mother–child distinction). Per -`+formal/PRESERVATION-DESIGN.md §7+`, L4 is "`not a separate proof +`+formal/PRESERVATION-DESIGN.adoc §7+`, L4 is "`not a separate proof layer. It is a labelling discipline at the program / module level… No proofs change.`" @@ -434,34 +511,27 @@ the owner*: === §4. Counts + file-by-file map -Coq admitted proofs remaining: 3 - -(1 outer `+Admitted.+` in `+formal/Semantics.v+` — sacrosanct legacy -preservation, provably false per `+Counterexample.v+` + *2* outer -`+Admitted.+` markers in `+formal/Semantics_L1.v+` — the two open L1 -lemmas `+step_pop+` / `+preservation_l1+`. *Updated 2026-06-26 (this -branch) against rebuilt `+coqc 8.18.0+` + -`+scripts/status-gate.sh --proofs+` ground truth. Two closures dropped -the count 5 → 3:* *(a) `+region_shrink_preserves_typing_l1_gen_m+` was -_dissolved_ (the 2026-06-16 multiset-perm closure) — its general form is -proven false and pinned in `+formal/Counterexample_RegionShrink.v+`, the -surviving value corollary `+region_shrink_value+` is `+Qed+`/axiom-free, -and `+preservation_l3+` is consequently UNCONDITIONALLY axiom-free.* -*(b) `+region_liveness_at_split_l1_gen+` — the provably-false -`+In rv R -> In rv R'+` lemma — was _removed_. Its 13 consumers in -`+subst_typing_gen_l1_m+` now route through the TRUE, `+Qed+` -`+region_liveness_no_exit_l1_gen+`, supplied with the honest -`+val_region_no_exit+` premise threaded through -`+subst_typing_gen_l1_m+` / `+subst_typing_gen_l1+` / -`+subst_preserves_typing_l1+` and the L2 β-case lemmas -(`+preservation_l2_app_eff_beta_linear+` / `+_l1+`) — all of which -`+Print Assumptions+` now reports as "`Closed under the global context`" -(axiom-free) instead of depending on a false axiom.* The two remaining -outer markers are `+step_pop_disjoint_from_type_l1+` and -`+preservation_l1+` (capstone, gated on `+step_pop+`); §5’s line numbers -are earlier-branch snapshots, superseded here.) - -==== Per-file Qed / Admitted summary (as of 2026-06-01) +Coq `+Admitted.+` marker count: *3* (current source inventory): one +legacy marker plus two in `+Semantics_L1.v+`. This is a marker count, not +a count of sound obligations still awaiting routine proof: + +* `+formal/Semantics.v+` `+preservation+`: false as stated; durable + legacy archaeology, pinned by `+Counterexample.v+`. +* `+formal/Semantics_L1.v+` `+step_pop_disjoint_from_type_l1+` and + `+preservation_l1+`: both unrestricted statements are refuted by + `+Counterexample_StepPop.v+` and + `+Counterexample_PreservationL1.v+`; neither is ordinary proof debt. +* The false unrestricted region-shrink helper was replaced by + `+region_shrink_msperm+` and proved value/neutral corollaries. The + false unconditional region-liveness helper was removed and replaced at + call sites by the no-exit formulation. These are separate refuted + helper statements and do not create additional live `+Admitted.+` + markers. + +Open work is redesigning L1/L2 judgments and stating sound replacement +theorems with exact hypotheses. See the current boundary at the start of +this document; the dated detail below is historical. +==== Archived per-file Qed / Admitted summary (2026-06-01; superseded) [width="100%",cols="23%,>28%,>28%,21%",options="header",] |=== @@ -489,9 +559,10 @@ soundness-gap witness — nested TFunEff (analogue structure to modality-indexed |`+formal/Semantics_L1.v+` |*54* |*2* |✅ active — Phase 3b Stage 1a + -1b landed via PRs #252 + #253. *2* outer `+Admitted.+` markers — the two -open L1 lemmas (`+step_pop_disjoint_from_type_l1+` / -`+preservation_l1+`). *Updated 2026-06-26: `+region_shrink…gen_m+` +1b landed via PRs #252 + #253. *2* outer `+Admitted.+` markers — +`+step_pop_disjoint_from_type_l1+` and `+preservation_l1+`; both +unrestricted statements are refuted by later pinned regressions, not +ordinary open obligations. *Updated 2026-06-26: `+region_shrink…gen_m+` dissolved (2026-06-16) and `+region_liveness_at_split_l1_gen+` removed (this branch) via the honest `+val_region_no_exit+` reformulation — see the §4 marker note. `+preservation_l3+` and the L2 β-case lemmas are now @@ -524,7 +595,7 @@ linearity, narrow no-escape proof; no `+believe_me+` / `+sorry+` / `+assert_total+` |=== -==== Seam audit (current 2026-06-01): every admit/axiom classified +==== Archived seam audit (2026-06-01; superseded by current classifications) The current `+admit.+` / `+Admitted.+` set in `+formal/*.v+`. The remaining admits are exactly the *pre-existing L1 structural debt* (with @@ -552,7 +623,7 @@ internal `+:576+` + `+:646+` |When both internal admits close sub-case; *GENUINELY FALSE as stated* (single-case counterexample documented at site lines 1923-1926); current `+Admitted.+` is a transparency mark, not "`almost done`" |L2 effect-typed `+TFun+` per -`+PRESERVATION-DESIGN.md §5.1+`; closure requires reformulation, not +`+PRESERVATION-DESIGN.adoc §5.1+`; closure requires reformulation, not direct proof |`+Semantics_L1.v:2014+` (`+admit.+`) |*Parallel mirror* of `+:1994+` — @@ -566,7 +637,7 @@ never directly — only via reformulation) |`+Semantics_L1.v:3132+` (`+admit.+`) |*Pre-existing* — `+preservation_l1+` body, covering S_StringConcat_Step2 + S_App_Step2 + S_Pair_Step2 cases; lambda-rigidity gap per -`+PRESERVATION-DESIGN.md §4.8+` |Phase 3b Stages 2/3/4 (#240/#241/#242) +`+PRESERVATION-DESIGN.adoc §4.8+` |Phase 3b Stages 2/3/4 (#240/#241/#242) — L2 effect-typed lambdas with `+R_in/R_out+` syntactic annotations |`+Semantics_L1.v:3133+` (`+Admitted.+`) |*Outer marker* — depends on @@ -625,15 +696,16 @@ build`" jobs. ''''' -=== §5. Closure plan + current-branch state + foundation audit (2026-06-16) +=== §5. Archived closure-plan snapshots + foundation audit (2026-06-16 onward) ____ -This section is a dated *status + plan* snapshot. It does *not* -supersede §1–§4 (which track `+main+`); it records (a) the authoritative -ground-truthed admit set on the current proof branch, (b) the committed -closure route, and (c) the independent trust audit of the foundation -repos the route builds on. Sourced from a ground-truth sweep -(`+coqc+`/`+grep+`-verified, not doc-trusted), not from prose. +This section preserves dated historical snapshots for traceability; it is +not current status and is superseded by §1–§4 and the current preservation +boundary at the start of this document. In particular, later Coq +counterexamples refuted `+step_pop_disjoint_from_type_l1+` and +`+preservation_l1+`; old “open closure route” language below must not be +read as a plan to prove those unrestricted statements. The foundation-repo +audit is separate and cannot discharge Ephapax's local soundness obligations. *Companion design docs* `+L1-REGION-REFOUNDATION-PLAN.md+` and `+L1-ELIMINATOR-FORK.md+` (referenced below) live in *PR #299* (branch @@ -642,7 +714,7 @@ tropical applicability case study is `+tropical-resource-typing+` PR #21 (`+docs/applications/ephapax-l1-regions.adoc+`). ____ -==== 5.1 Current proof branch +==== 5.1 Archived proof-branch snapshot (superseded) Branch `+proofs/l1-effect-typing-Aprime+` (A′ effect-typed-only lambdas). *A′ closes 0 of 4 L1 admits* — the open obligations are @@ -665,7 +737,7 @@ companion `+fix/proof-gates+` PR repairs the script (`+//+`→`+#+`) and wires it into CI so future drift is flagged. (A′ shifts the line numbers but not the count.) -==== 5.2 The four L1 admits — authoritative classification (this branch) +==== 5.2 Archived L1-admit table (not authoritative; later counterexamples supersede) [width="99%",cols="20%,16%,16%,16%,16%,16%",options="header",] |=== @@ -696,37 +768,35 @@ lambda) but region-count coherence at a region exit. *⚠️ 2026-07-07 under `+S_Pair_Step1+`), and lands at `+R'=[]+` with `+rv ∈ free_regions(T)+`. Same class as admit #2’s history: the `+Admitted.+` hides a falsehood, not a gap. |*the eliminator fork* — now -with a Qed forcing argument that typing ⇏ trace coherence -|*Reformulation, owner-gated* — restate with a liveness/coherence -premise or restrict to value-anchored consumers (the sole caller retypes -an `+ELoc+` value whose `+T_Loc_L1+` typing carried `+In r R+`; the -refuting sibling is a variable, which no `+S_*_Step2+` case retypes at -`+R'+`). The choreographic route’s task is now provably "`make coherence -a judgment-level input`", not "`derive it`". +with a Qed forcing argument that typing ⇏ trace coherence. The initial +value-anchored restriction proposal is superseded: the later witness in +`+Counterexample_PreservationL1.v+` refutes the `+S_StringConcat_Step2+` +case with an `+ELoc+` anchor. The current unrestricted lemma must not be +proved; a replacement requires an explicitly different judgment or +premise, owner-approved and independently proved. `+Counterexample_StepPop.v+` header + `+L1-ELIMINATOR-FORK.md+` §3–§8 |4 |`+preservation_l1+` (capstone) |`+Semantics_L1.v:3367+` |`+:3379+` |*⚠️ provably FALSE AS STATED (2026-07-07, experiment 3b)* — `+formal/Counterexample_PreservationL1.v+` (Qed, zero axioms): `+EStringConcat (ELoc 0 rv) (ESnd (EPair (ERegion rv (EI32 0)) (EVar 0)))+` -at `+R=[rv]+` types in both modalities, steps (the sibling’s region-exit -pops the only `+rv+`), and the post-state is untypable — the `+ELoc+` -anchor’s `+T_Loc_L1+` demands `+In rv []+`. The value-anchored escape +at `+R=[rv]+` types in both modalities and steps (the sibling’s region-exit +pops the only `+rv+`). In the Linear instance the post-state is untypable — +the `+ELoc+` anchor’s `+T_Loc_L1+` demands `+In rv []+`. The value-anchored escape hatch suggested by `+Counterexample_StepPop.v+` is closed: the dangling dependence here IS a value. |*NOT closable by lemmas* — the judgment -must carry the temporal invariant (region-liveness-through-reduction): -either coherence as a judgment input (choreographic-foundational route, -now Qed-mandatory) or leaf-rule strengthening that rejects the witness -at typing (A′/path-3 family, to be re-examined against this witness). -Owner decision; record in `+PRESERVATION-DESIGN.md+`. +needs a temporal invariant such as region-liveness-through-reduction, +encoded in the judgment or enforced by strengthened leaf rules that reject +the witness. These are redesign directions, not established proofs; owner +decision required and to be recorded in `+PRESERVATION-DESIGN.adoc+`. |=== -`+preservation_l3+` (`+Semantics_L1.v+`, *Qed*) is real and depends on -*only* admit #1 (`+region_shrink+`); it flips *unconditional* the moment -#1 closes. `+L4.v+` is *scaffold-unbuilt* (`+ProgramMode+` + round-trip -mapping; definitions only, no theorems — not debt, just not yet built). -No hidden 5th admit, no `+Axiom+`/`+Parameter+`/`+Hypothesis+` smuggled -assumption, no fake-`+Qed+` was found anywhere in `+formal/*.v+`. +`+preservation_l3+` (`+Semantics_L1.v+`, *Qed*) is scoped to the +matching echo-emitting rule pairs; it does not depend on the removed +unrestricted region-shrink helper and does not establish general L1/L2 +preservation. `+L4.v+` is a scaffold (`+ProgramMode+` + round-trip +mapping; definitions only, no theorems). The marker inventory above is +not evidence that a refuted theorem should be closed. ==== 5.3 Idris2 ABI proof needs (a separate axis from the Coq L1 admits) @@ -737,9 +807,9 @@ forward to a discharging proof: [width="100%",cols="34%,33%,33%",options="header",] |=== |ID |Invariant |Status -|E1 |Type preservation (operational) |*owed* — forwards to Coq -`+preservation+` (legacy is false; real obligation is -`+preservation_l1+`) +|E1 |Type preservation (operational) |*owed* — legacy `+preservation+` +is false and current unrestricted `+preservation_l1+` is refuted. This +requires a separately stated, sound replacement theorem in Coq. |E2 |Linear consumption across control flow |E2a position-form *DISCHARGED* (`+splitLinearCoverage+`, Qed, `+Formal/Qualifier.idr+`); @@ -872,7 +942,7 @@ foundation it builds on is independently verified. * link:STATUS.adoc[`+STATUS.adoc+`] — past / present / future temporal map. -* link:formal/PRESERVATION-DESIGN.md[`+formal/PRESERVATION-DESIGN.md+`] +* link:formal/PRESERVATION-DESIGN.adoc[`+formal/PRESERVATION-DESIGN.adoc+`] — canonical four-layer design doctrine. * link:CLAUDE.md[`+CLAUDE.md+`] — agent guidance; owner directive 2026-05-27. diff --git a/README.adoc b/README.adoc index c81b1be0..dd46a713 100644 --- a/README.adoc +++ b/README.adoc @@ -43,14 +43,12 @@ link:https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambigu ==== [NOTE] -.🌱 Ephapax is gestating — second-draft in progress, and going well (start with `V1-TO-V2.adoc`) +.🌱 Ephapax is gestating — second-draft in progress; proof redesign required (start with `V1-TO-V2.adoc`) ==== -This language is **not dead, abandoned, or frozen** — it is mid-way -through a deliberate *second draft*, on two independent tracks, and both -are landing. The full story (and why the older "provably false / -archaeology" wording misled readers into writing the project off) is in -link:V1-TO-V2.adoc[`V1-TO-V2.adoc`]. Read that first; this box is the -short version. +This language is in a deliberate second-draft process. Grammar work is +active; the proof track has preserved a false legacy theorem and discovered +further L1/L2 gaps that require redesign. The full status is in +link:V1-TO-V2.adoc[`V1-TO-V2.adoc`] and `PROOF-NEEDS.adoc`. **The grammar (v1 → v2).** The flat v1 surface worked for the core but could not grow into modules / generics / effects / comptime. v2 adds the @@ -63,28 +61,23 @@ counterexample (link:formal/Counterexample.v[`formal/Counterexample.v`], 5 Qed lemmas) *proved* that preservation as stated in the legacy single-judgment design is unsound — a region exit could invalidate a sibling's assumptions untracked. Discovering that **with a proof, before -anyone depended on it**, is the rare correct thing, not a failure. The -redesign re-derives preservation across *four orthogonal layers* (regions -/ modality / echo / dyadic mode), each from its own explicit invariants. -The legacy theorem stays `Admitted` on purpose — it is proven unclosable, -so it is fenced off, not abandoned. - -Quick proof-status read: **L1** (region capabilities) substantially -complete; **L2** (Linear/Affine modality) core landed with zero axioms; -**L3** (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`, definitions by design). - -**For anyone (human or bot) doing the work:** the only fenced-off -artefacts are the *one* falsified legacy theorem and the *one* superseded -flat grammar. Everything in the v2 columns — the grammar phases and the -per-layer proofs — is open and tractable. Authoritative maps: +anyone depended on it**, is the rare correct thing, not a failure. The four-layer architecture is a design program, not an established +preservation result. The legacy theorem stays `Admitted` on purpose; later +pinned counterexamples also refute the unrestricted L1 preservation claim. +There is no unconditional L2 preservation theorem, while the L2 β-case +helpers are conditional. L3's `preservation_l3` and case lemmas are Qed +for matching echo-emitting rule pairs only; L4 is a Phase A scaffold. + +**For anyone (human or bot) doing the work:** preserve every pinned +counterexample and do not attempt to prove a refuted statement. Active proof +work means specifying and proving sound replacements locally for Ephapax's +own syntax, judgments, and steps—not relying on shared vocabulary or an +upstream repository. +Authoritative maps: link:V1-TO-V2.adoc[`V1-TO-V2.adoc`] (the frame), link:STATUS.adoc[`STATUS.adoc`] (operational past/present/future), -link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`] -(four-layer architecture), link:PROOF-NEEDS.md[`PROOF-NEEDS.md`] (proof +link:formal/PRESERVATION-DESIGN.adoc[`formal/PRESERVATION-DESIGN.adoc`] +(four-layer architecture), link:PROOF-NEEDS.adoc[`PROOF-NEEDS.adoc`] (proof debt + do-not-do list). Anything dated before 2026-05-26 describing a "preservation closure plan" or "910 → 12 goals" is the record of how the first draft hit its wall — read it as history, not instructions. @@ -95,26 +88,27 @@ irreversible boundaries** (region exits, drops, key erasure, audit trails) in compile-time-memory-safe WebAssembly. Real systems are irreversible — operating systems deallocate, databases drop tables, security systems erase keys, compilers collapse high-level -distinctions. Ephapax gives a disciplined, machine-checkable -framework to handle those boundaries responsibly: the type system -tracks not just *what is owned* but *what was lost when it was given -up*, so reclamation can carry mandatory evidence where it matters -(audit, compliance, cryptographic erasure) and degrade to free where -it doesn't (inference loops, hot paths). - -The core calculus is mechanically formalised. Soundness theorems on -the dynamic side (Coq) and structural-safety theorems on the type -side (Idris2) are checked by their respective proof assistants on -every push. +distinctions. Ephapax is designed to track not just *what is owned* but *what was +lost when it was given up*, so reclamation can carry evidence where it +matters and degrade where it does not. This is a research design goal, +not a claim that all language-level soundness obligations are proved. + +The core has Coq and Idris2 formal artifacts, but the current Coq +preservation story is incomplete and has pinned counterexamples: legacy +preservation and the unrestricted L1 statement are false as stated, and +no unconditional L2 theorem is established. See the proof ledger and +`PROOF-NEEDS.adoc` before interpreting any local lemma as a language-wide +guarantee. toc::[] == Why "Ephapax"? -The Greek _ἐφάπαξ_ ("ephapax") means **once for all**. It is the -guarantee linear types make: every resource is used **exactly once**. -You consume it, or you transfer ownership of it, or you drop it — -but you cannot reach for it twice, and you cannot forget about it. +The Greek _ἐφάπαξ_ ("ephapax") means **once for all**. It evokes the +linear-typing design goal: track each linear resource so it is consumed +exactly once. The intended guarantee must still be established for +Ephapax's judgments, implementation, and operational semantics; current +preservation counterexamples show that this is not automatic. == What this is @@ -131,21 +125,22 @@ Ephapax is a programming language with: below for how this composes with L1/L3/L4. | **Region-based memory (L1)** -| Allocations live in named regions (`region r: ...`). The type - system threads a region-capability environment through every - expression so a sibling cannot read from a region another sibling - has just exited. When a region's scope ends, the runtime bulk-frees - every resource in it. No allocator overhead per object; no - per-object frees. +| Allocations are designed around named regions (`region r: ...`). The + L1 judgment threads a region-capability environment, but current + unrestricted L1 preservation is refuted by pinned Coq counterexamples; + sibling safety is a design goal, not an established guarantee. When a + region's scope ends, the runtime bulk-frees resources in it; this + implementation behavior is not proved to refine the calculus. | **Second-class borrows** | `&x` gives temporary access without consuming `x`. Borrows cannot be stored, escape their introduction scope, or be used after the borrowed resource is freed. -| **Compile-time memory safety** -| No use-after-free, no double-free, no leaks of linear resources - — caught at type-check time, before a binary is produced. +| **Compile-time memory safety (design target)** +| The intended goal is to reject use-after-free, double-free, and leaks + of linear resources before code generation. General preservation and + implementation refinement are not established; see `PROOF-NEEDS.adoc`. | **WebAssembly target** | `wasm32-unknown-unknown` primary; native via Cranelift secondary. @@ -157,20 +152,20 @@ Ephapax is a programming language with: == The four layers -Ephapax composes four orthogonal disciplines. Each is a thin-poset -refinement, so they compose without coherence obligations -(https://github.com/hyperpolymath/echo-types[echo-types] supplies the -recipe). +Ephapax's design separates four disciplines. Their composition and +soundness are proof obligations, not an automatic consequence of +orthogonality or of a related repository's theory. `echo-types` is a +conceptual reference; Ephapax-local claims require Ephapax-local proofs. [cols="1,3"] |=== | Layer | What it enforces | **L1 — Region capabilities** -| Every live region is tracked in an input/output environment threaded - through every expression. A region cannot be referenced after a - sibling has exited it. Soundness proof in `formal/TypingL1.v` + - `formal/Semantics_L1.v`. +| Region environments are threaded through compound typing rules. This + is intended to prevent stale sibling references, but the current + preservation statement is refuted as stated by pinned L1 counterexamples; + it is not a proved language guarantee. See `PROOF-NEEDS.adoc`. | **L2 — Structural discipline (linear ↔ affine)** | The *modality* of the surrounding program decides whether linear @@ -196,14 +191,13 @@ recipe). .Soundness story **** -The four-layer separation is *not* decorative — it exists because the -original "linear+affine + regions" framing admitted a verified -counterexample to preservation (see `formal/Counterexample.v` and -`formal/PRESERVATION-DESIGN.md`). The four-layer redesign restores -soundness by making each discipline's invariants explicit and -orthogonal: preservation is *re-derived per layer* from explicit -invariants rather than forced through a single judgment that hides -them. +The four-layer separation is a design response to the verified legacy +counterexample (`formal/Counterexample.v`), not itself a soundness proof. +Later pinned regressions refute the current unrestricted L1 preservation +statement, and no unconditional L2 preservation theorem is established. +Making invariants explicit is necessary design work, but every Ephapax +typing/step combination still requires a local theorem with proven +assumptions. See `PROOF-NEEDS.adoc` for the current boundary. **** == Three superpowers @@ -217,31 +211,26 @@ with: | Superpower | What it gives you | **A. Accountability of irreversible reclamation** -| You can free memory (`S_Region_Exit`, `S_Drop`) and the type system - *knows* you lost the data — and tracks what depended on it. Under - the Linear modality the reclamation event carries a mandatory - evidence-bearing `Echo` value; under Affine you opt out for - performance. Pairs cleanly with region-based memory management - (deterministic bulk free) to deliver high-assurance reclamation - that tracing GC cannot — by design, tracing GC *hides* the - reclamation evidence. +| The design aims to make irreversible events (`S_Region_Exit`, + `S_Drop`) carry typed evidence under Linear discipline, with a more + permissive Affine path. This is a design intent; the local L1/L2 + preservation gaps mean it is not yet an end-to-end proved guarantee. | **B. Selective reversibility (thin-poset)** | Linear ≤ Affine is a two-point thin poset at the L2 modality. You pick per-region (or per-project) which discipline applies. Same code shape, different evidence obligations. Concrete examples: *Linear* during backpropagation (must keep the gradient residue); - *Affine* during inference (drop the residue, save memory). You get - the safety of reversibility where you need it, and the performance - of irreversibility where you don't. + *Affine* during inference (drop the residue, save memory). These are + design examples; their safety properties require local proofs and are + not established by the modality poset alone. | **C. Debugging + provenance** -| Attach Linear Echoes to critical state changes. The type system - guarantees the receipt (preimage) of that state change was retained - — so when a bug fires, the inputs that produced the error are - recoverable by construction. In Affine mode you opt out of this - debugging info, with the same code shape. The evidence is a - *theorem-level guarantee*, not a runtime convention. +| The design uses Linear Echoes to require receipts (preimages) for + selected state changes and permits opting out in Affine mode. The + intended guarantee is that evidence is retained, but current preservation + gaps mean this must not be described as a proved end-to-end language + guarantee yet. |=== [CAUTION] @@ -262,37 +251,36 @@ discipline on deterministic Rust-style drop for critical resources not committed. ==== -== What this enables +== Design targets and use cases -The three superpowers translate to concrete use cases the type -system can *prove* properties about: +These are intended applications of the design, not currently established +end-to-end language guarantees. Any particular safety claim needs a proved +Ephapax theorem with its exact assumptions and implementation boundary. -* **Mandatory evidence for critical actions.** By making certain - echoes Linear (mandatory observation), the type system guarantees - that a region exit *always* emits an audit trail, or that a drop - *always* triggers a required cleanup. +* **Mandatory evidence for critical actions (design target).** A future + Linear-echo discipline is intended to require observation of selected + region exits or drops. The current L3 Qed lemmas cover matching rule + pairs only; they do not establish this end-to-end guarantee. -* **GDPR "right to be forgotten" with certified evidence of - erasure.** Linear-echo discipline on the `S_Drop` of a personal-data - resource is a type-level proof that erasure happened *and* that the - required notification / log was produced. Auditors get a - machine-checkable artefact instead of a process attestation. +* **GDPR "right to be forgotten" with certified evidence of erasure + (potential application).** The design explores making deletion evidence + explicit. No current Ephapax theorem proves erasure, notification, or + logging for personal-data programs. -* **Verified resource management for keys, secrets, and sensitive - buffers.** Linear-echo on the deallocation of a key buffer - guarantees provable erasure; the typing rule cannot be silenced. +* **Resource management for keys, secrets, and sensitive buffers + (potential application).** The design aims to make selected deallocation + events auditable; it does not currently prove physical erasure or + implementation refinement. -* **Selective reversibility without redesigning your language.** - The thin-poset means you don't redesign the runtime to be - bijective. You add *one* type former (the fiber) and layer - existing L2 modalities over it. Orthogonal and compositional. +* **Selective reversibility.** The Linear/Affine modality is mechanised, + and the Echo calculus has a local non-invertibility result. These + isolated facts do not prove the proposed system composes soundly or + provides end-to-end guarantees. -* **Machine-checkable foundation for policy enforcement.** The - thin-poset Linear ≤ Affine + the proven non-invertibility - (`EchoResidue.no-section-collapse-to-residue`) gives sharp, - proof-relevant reasoning: *weakening obligations is allowed*, - *strengthening them back is impossible*. Clean logical foundation - for compliance work. +* **Potential foundation for policy enforcement.** Any compliance claim + requires a precisely scoped Ephapax theorem and an implementation + boundary; cross-repository Echo results and conceptual vocabulary do + not discharge those obligations. == What this isn't @@ -381,11 +369,11 @@ Prerequisites: [source] ---- ephapax/ -├── formal/ # Coq operational semantics + soundness +├── formal/ # Coq syntax, judgments, semantics, lemmas, and counterexamples │ ├── Syntax.v # AST and types │ ├── Typing.v # Region-linear typing rules │ ├── Semantics.v # Small-step substitution semantics -│ └── PRESERVATION-HANDOFF.md # Per-case checklist for preservation +│ └── PRESERVATION-HANDOFF.adoc # Per-case checklist for preservation ├── idris2/ # Idris2 frontend (parser + typechecker) │ ├── src/Ephapax/IR/ # AST, decode/encode, S-expression IR │ ├── src/Ephapax/Parse/ # Lexer, parser, stream, ZigBuffer FFI @@ -435,14 +423,15 @@ based calculus. Post-2026-05-26 the formalisation is layered: pre-discovery PR list and the explicit do-not-do reasoning. * **Layer 1 — region capabilities** (`formal/TypingL1.v`, - `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 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. + `formal/Semantics_L1.v`). The modality-indexed judgment threads a + capability environment `R`. The judgment and helper lemmas are + mechanised, but the unrestricted `preservation_l1` statement is + refuted by `Counterexample_PreservationL1.v`; its supporting + `step_pop_disjoint_from_type_l1` statement is separately refuted by + `Counterexample_StepPop.v`. Their `Admitted.` markers must not be + treated as routine proof debt. A sound replacement requires a + judgment/step redesign and an explicit theorem boundary. See + `PROOF-NEEDS.adoc`. * **Layer 2 — structural modality** (`formal/Modality.v`). Linear vs Affine as a K-free thin-poset decoration. `linear_to_affine` @@ -455,20 +444,20 @@ based calculus. Post-2026-05-26 the formalisation is layered: https://github.com/hyperpolymath/echo-types[`hyperpolymath/echo-types`]). 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). + and the `preservation_l3` umbrella are Qed for their matching echo + rule pairs; they do not establish general L1/L2 preservation. * **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`]. + in link:formal/PRESERVATION-DESIGN.adoc[`formal/PRESERVATION-DESIGN.adoc §7`]. Per-sublanguage proof debt with explicit do-not-do list lives in -link:PROOF-NEEDS.md[`PROOF-NEEDS.md`]. The four-layer architecture +link:PROOF-NEEDS.adoc[`PROOF-NEEDS.adoc`]. The four-layer architecture rationale is in -link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`]. +link:formal/PRESERVATION-DESIGN.adoc[`formal/PRESERVATION-DESIGN.adoc`]. The counterexample itself is link:formal/Counterexample.v[`formal/Counterexample.v`] (5 Qed). @@ -492,11 +481,12 @@ Two Idris2 developments: zero `believe_me`, zero `assert_smaller` introduced; 14 `covering` markers retained for documented Idris2 0.8.0 SCT limits. -* **`src/formal/`** — region-linearity theorems on the type side: - `noEscapeTheorem`, `regionSafetyExtract`, `noGCExtract`, - `orthogonalityLemma`, plus `splitLinearCoverage` generalising - the non-diminishment property (PR #85). All four headline theorems - complete with **zero unsafe patterns**. +* **`src/formal/`** — local Idris2 structural results include + `noEscapeTheorem`, `orthogonalityLemma`, and `splitLinearCoverage`. + `regionSafetyExtract` and `noGCExtract` are total but vacuous wrappers + returning supplied witnesses. These do not establish operational + region safety, general preservation, or Rust/compiler refinement; the + ABI obligation register records what remains owed. [source,bash] ---- @@ -610,24 +600,24 @@ generics, effects, traits, comptime, contracts) lives on | Counterexample at `formal/Counterexample.v` (5 Qed). Not closable. Archaeology. | Coq L1 (region capabilities) -| ✅ 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. +| Judgment and helpers mechanised; unrestricted preservation refuted +| `Counterexample_StepPop.v` refutes `step_pop_disjoint_from_type_l1`; `Counterexample_PreservationL1.v` refutes `preservation_l1`. These are pinned regressions, not ordinary open proof debt. | Coq L2 (modality) -| ✅ Core landed (PRs #176 + #177); 0 axioms -| `linear_to_affine` Qed. Integration debt absorbed by L1 admits above. +| ✅ Modality core landed (PRs #176 + #177); 0 axioms +| `linear_to_affine` Qed. No unconditional `preservation_l2` theorem is established. The L2 β-case lemmas are conditional; `Counterexample_L2.v` and `Counterexample_L2_nested.v` document distinct gaps. | Coq L3 (echo / residue calculus) -| ✅ 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. +| ✅ Scoped matching-rule preservation results Qed; 0 admits in `Echo.v` +| `preservation_l3` and its two case lemmas cover matching echo-emitting rule pairs only; they do not establish general L1/L2 preservation. 12 Qed in `Echo.v` for the underlying calculus. | Coq L4 (dyadic interaction) | ✅ 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`. +| `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` + `program_mode_to_modality` round-trip. No theorems by design; design in `formal/PRESERVATION-DESIGN.adoc §7`. -| Idris2 region-linearity theorems -| ✅ Complete (zero unsafe) -| +| Idris2 structural results +| ✅ Local total proofs; two extraction wrappers are vacuous +| `noEscapeTheorem`, `orthogonalityLemma`, `splitLinearCoverage`, and `outlivesTransitive` have exact local scopes. No runtime no-escape, general language soundness, or implementation-refinement proof is established; see the EXPLAINME ledger and `PROOF-NEEDS.adoc` §5.3. | LSP server | 🟡 Partial @@ -652,14 +642,14 @@ generics, effects, traits, comptime, contracts) lives on are we?" Read this before any `.v` file or any PR comment dated before 2026-05-26. -| link:PROOF-NEEDS.md[PROOF-NEEDS.md] +| link:PROOF-NEEDS.adoc[PROOF-NEEDS.adoc] | Per-sublanguage proof debt audit. What's done (Qed), what's todo, what's banned (anti-pattern detector). Separated for ephapax-linear and ephapax-affine sublanguages. -| link:formal/PRESERVATION-DESIGN.md[formal/PRESERVATION-DESIGN.md] -| **Canonical four-layer design doctrine.** Why the counterexample - forced the redesign, the four orthogonal concerns, per-layer plans. +| link:formal/PRESERVATION-DESIGN.adoc[formal/PRESERVATION-DESIGN.adoc] +| **Design history and architecture.** Why the legacy counterexample + motivated the four-layer proposal; not proof that preservation holds per layer. | link:formal/Counterexample.v[formal/Counterexample.v] | The 5 Qed lemmas that pin the soundness gap of the legacy judgment. @@ -676,9 +666,9 @@ generics, effects, traits, comptime, contracts) lives on | link:ROADMAP.adoc[ROADMAP.adoc] | Milestones (v0.1.0 → v1.0.0), per-version checklists, current open work. Note: any pre-2026-05-26 closure-plan content is superseded - by STATUS.adoc + PRESERVATION-DESIGN.md. + by STATUS.adoc + PRESERVATION-DESIGN.adoc. -| link:formal/PRESERVATION-HANDOFF.md[formal/PRESERVATION-HANDOFF.md] +| link:formal/PRESERVATION-HANDOFF.adoc[formal/PRESERVATION-HANDOFF.adoc] | **Archaeology only** — historical diagnostic record of the pre-counterexample closure attempts. Reads as a closure plan; isn't one. Useful only for understanding *why* the redesign happened. @@ -686,13 +676,13 @@ generics, effects, traits, comptime, contracts) lives on | link:RUST-SPARK-STANCE.adoc[RUST-SPARK-STANCE.adoc] | Stance on Rust + SPARK interop and where Ephapax fits. -| link:TOPOLOGY.md[TOPOLOGY.md] +| link:TOPOLOGY.adoc[TOPOLOGY.adoc] | Module dependency graph + crate layering. -| link:TEST-NEEDS.md[TEST-NEEDS.md] +| link:TEST-NEEDS.adoc[TEST-NEEDS.adoc] | Outstanding test coverage gaps. -| link:CHANGELOG.md[CHANGELOG.md] +| link:CHANGELOG.adoc[CHANGELOG.adoc] | Per-release change log. | link:docs/vision/EPHAPAX-VISION.adoc[docs/vision/EPHAPAX-VISION.adoc] @@ -710,10 +700,10 @@ generics, effects, traits, comptime, contracts) lives on | link:.github/CONTRIBUTING.md[.github/CONTRIBUTING.md] | Contribution guide. -| link:CODE_OF_CONDUCT.md[CODE_OF_CONDUCT.md] +| link:CODE_OF_CONDUCT.adoc[CODE_OF_CONDUCT.adoc] | Code of conduct. -| link:SECURITY.md[SECURITY.md] +| link:SECURITY.adoc[SECURITY.adoc] | Security policy. |=== @@ -765,18 +755,19 @@ comparison against ten of these. Contributions welcome. Please see: * link:.github/CONTRIBUTING.md[.github/CONTRIBUTING.md] — getting started -* link:CODE_OF_CONDUCT.md[CODE_OF_CONDUCT.md] — community standards +* link:CODE_OF_CONDUCT.adoc[CODE_OF_CONDUCT.adoc] — community standards The highest-leverage open work, in priority order: -1. **Phase 3b Stages 2 → 4** (issues #240/#241/#242) — `ELam` annotation - extension, CPS-form substitution, then compound non-linear values + - unconditional `preservation_l2`. The path forward; see - `formal/PRESERVATION-DESIGN.md §12.15` and `formal/PHASE-D-REDESIGN.md`. -2. **Progress for L1** — state and prove `progress_l1` plus the L1 - `canonical_*` lemmas (currently legacy-only at `Semantics.v:603-630`). - Combined with the conditional `preservation_l1`, this gives - conventional type-soundness in conditional form. +1. **L1/L2 soundness redesign** — specify judgment and operational + invariants that reject the pinned counterexamples, then state and prove + replacement preservation theorems with explicit hypotheses. Existing + Phase 3b work is conditional infrastructure, not an unconditional + L2 theorem. +2. **Progress for redesigned judgments** — state and prove progress and + canonical forms only against the final redesigned judgments. Do not + combine these with the refuted unrestricted `preservation_l1` claim to + assert conventional type soundness. 3. **Fuel-refactor `Parse/Parser.idr`** from `%default covering` to `%default total`. Substantial — ~30 mutually-recursive combinators threaded through a `Stream` record. @@ -789,11 +780,14 @@ The highest-leverage open work, in priority order: *Closing the legacy `Theorem preservation` in `formal/Semantics.v` is NOT a valid contribution.* That theorem is provably false (sealed by `formal/Counterexample.v`); its `Admitted.` is correct and durable per -owner directive 2026-05-27. `formal/PRESERVATION-HANDOFF.md` is -archaeology kept for context. The path forward is the per-layer -preservation theorems (`preservation_l1`, `preservation_l2`, -`preservation_l3`) on the redesigned judgment in `formal/Semantics_L1.v`. -See `formal/PRESERVATION-DESIGN.md §12` and `PROOF-NEEDS.md §3`. +owner directive 2026-05-27. `formal/PRESERVATION-HANDOFF.adoc` is +archaeology kept for context. The redesigned judgments are a separate development, not yet a sound +replacement: `preservation_l1` is refuted as stated, and no unconditional +`preservation_l2` theorem exists. L2 β-case lemmas have explicit +preconditions; L3 results cover only matching echo rule pairs. The active +work is to specify and prove sound replacement theorems without weakening +the pinned regressions. See `formal/PRESERVATION-DESIGN.adoc` and +`PROOF-NEEDS.adoc`. ==== == Licence diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 9dbf9844..31aac0da 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -29,16 +29,18 @@ table (P28); OwnershipKind from_byte/to_byte round-trip (P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions (D04), Allen's interval algebra (D11), MessageHandle (D17), monoidal aggregates (D18). Stages 2-4 of the Phase 3b plan (#240/#241/#242) remain -un-touched. See `CHANGELOG.md` for full enumeration and per-PR detail. +un-touched. See `CHANGELOG.adoc` for full enumeration and per-PR detail. == Four-layer redesign (2026-05-26 → ) The verified preservation counterexample (`formal/Counterexample.v`, five `Qed` lemmas) closed the original preservation closure plan as unreachable in the legacy single-layer -typing judgment. The new plan separates four orthogonal layers; each -is implemented in sequence and preservation is *re-derived per -layer* from explicit invariants. +typing judgment. The architecture separates four concerns, but its existence does not +establish language soundness. The current unrestricted L1 preservation +statement is refuted, L2 has no unconditional preservation theorem, and +L3 results are scoped to matching echo rule pairs. Replacement theorem +statements and proofs remain the live soundness milestone. . *L1 — Region capability threading* + @@ -46,8 +48,10 @@ layer* from explicit invariants. region-capability environment) through every compound rule. - Land in `formal/TypingL1.v` + `formal/Semantics_L1.v` against `Counterexample.v` as a regression oracle. -- Status: judgment landed, `m`-indexed post-L2-hybrid; 9 L1 - supporting-lemma admits remain as L2-integration debt. +- Status: judgment landed and `m`-indexed. Two outer L1 `Admitted.` + markers remain, but both unrestricted statements are refuted by pinned + counterexamples; they are not routine integration debt. Several helpers + are conditional and do not establish general preservation. . *L2 — Modality parameter* + @@ -60,30 +64,29 @@ layer* from explicit invariants. . *L3 — Echo residue* + -- `formal/Echo.v` mirrors `echo-types/proofs/agda/Echo.agda`. The - L3 calculus (modes, `LEcho`, `weaken`, `degrade_mode`) is - mechanised locally. -- Next: introduce `TEcho ⟨op⟩` + the `T_Observe` rule into the - typing judgment; modify `S_Region_Exit` and `S_Drop` to produce - residue values. -- Status: K-free scaffold landed via #166/#167/#173; typing-rule - integration is the next-block work. +- `formal/Echo.v` contains the L3 calculus; typing and step-rule + integration has also landed. +- `preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, + and `preservation_l3` are Qed only for matching echo-emitting rule + pairs. This does not establish general L1/L2 preservation. +- Status: keep the scoped rule-pair boundary; additional coverage is + separate work. . *L4 — Mode declaration* + - Project-level metadata (`Cargo.toml` or `ephapax.toml`). Type checker reads the declaration and selects the L2 modality. -- No proof obligations of its own — see `formal/L4-DYADIC.md`. +- No proof obligations of its own — see `formal/L4-DYADIC.adoc`. - Status: mechanical scaffold landed in `formal/L4.v` (`ProgramMode` + `program_mode_to_modality`); surface syntax not yet wired into the parser. The previous *Preservation closure plan* section is **archived** — -see `formal/PRESERVATION-HANDOFF.md` for the historical record. PRs +see `formal/PRESERVATION-HANDOFF.adoc` for the historical record. PRs #92 / #102 / #104 / #106 / #114 / #116 / #117 / #121 / #146 are pre-discovery; treat them as archaeology, not instructions. -Canonical design source: `formal/PRESERVATION-DESIGN.md`. +Canonical design source: `formal/PRESERVATION-DESIGN.adoc`. == Formal-proof status @@ -122,7 +125,7 @@ substitution semantics: | **`preservation`** (legacy) | 🔴 Admitted — **provably false**, do not attempt to close -| `formal/Counterexample.v` exhibits five `Qed.` lemmas showing the theorem is genuinely false (`bad_typable`, `bad_step`, `bad_post_untypable`, `t_loc_l1_R_preserving`, `bad_input_untypable_l1`). The 11-goals story (PRs #92/#102/#104/#106/#114/#116/#117/#121/#146) is pre-discovery archaeology. The work is the **four-layer redesign** in `formal/PRESERVATION-DESIGN.md`, with preservation re-derived per-layer (`preservation_l1` in `Semantics_L1.v`, etc.). See `CLAUDE.md` at repo root for the owner directive (2026-05-27). +| `formal/Counterexample.v` pins five `Qed` lemmas, including the three core legacy witness lemmas (`bad_typable`, `bad_step`, `bad_post_untypable`) and the separate L1 regression. The 11-goals story (PRs #92/#102/#104/#106/#114/#116/#117/#121/#146) is pre-discovery archaeology. The four-layer architecture in `formal/PRESERVATION-DESIGN.adoc` is a design program, not a proof result: later pinned regressions refute unrestricted L1 preservation, and no unconditional L2 theorem is established. Do not describe preservation as re-derived per layer. See `CLAUDE.md` and `PROOF-NEEDS.adoc` for current boundaries. |=== **Historical note**: an earlier in-file comment claimed `preservation` @@ -217,31 +220,20 @@ All four headline theorems complete with **zero `believe_me` / * [ ] Type checker completion (`ephapax-typing`) * [ ] WASM code generation: lambda/app compilation (closure conversion) * [x] Coq: `subst_preserves_typing` (Qed) -* [ ] **Coq: re-derive preservation in the four-layer architecture** - — `Theorem preservation` in `formal/Semantics.v` is **provably - false** (verified by `formal/Counterexample.v`, five `Qed` - lemmas). The work is **not** to close that theorem; it is to - derive `preservation_l1` / `preservation_l2` / `preservation_l3` - per-layer in the redesigned architecture documented in - `formal/PRESERVATION-DESIGN.md`. Status (2026-06-01): - - L1 (`Semantics_L1.v` `preservation_l1`): Admitted with 1 inner - `admit.` covering S_StringConcat/S_App/S_Pair Step2 cases - (lambda-rigidity gap closing via Phase 3b Stage 2+3+4); - - L2 (in-place modality, PRs #176 + #177): `linear_to_affine` - Qed zero axioms; `preservation_l2_via_l1` Qed (conditional on - `preservation_l1`); 3 β-case lemmas Qed for ground non-linear, - Stage 1b TFunEff (conditional on side conditions), and Linear; - unconditional `preservation_l2` blocked on Phase 3b Stages 2/3/4 - (#240/#241/#242); - - L3 (`Echo.v` + slice 4 wiring): `preservation_l3_region_active_echo`, - `preservation_l3_drop_echo`, and umbrella `preservation_l3` all - Qed (conditional on the `region_shrink_preserves_typing_l1_gen_m` - structural admit that itself closes at Phase D); - - L4 (`L4.v`): Phase A scaffold landed 2026-05-28 (Definitions - only — `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` + - `program_mode_to_modality` round-trip). - See also `CLAUDE.md` at repo root and `PROOF-NEEDS.md` for the - complete picture. +* [ ] **Coq: specify and prove sound replacement preservation theorems.** + The legacy `Theorem preservation` is refuted by `Counterexample.v` + and must remain `Admitted.` The current unrestricted L1 + `preservation_l1` is refuted by `Counterexample_PreservationL1.v`, + with its supporting `step_pop_disjoint_from_type_l1` separately + refuted by `Counterexample_StepPop.v`; do not treat either as + unfinished routine proof debt. L2 has no unconditional + `preservation_l2` theorem: `Counterexample_L2.v` and + `Counterexample_L2_nested.v` record distinct β-preservation gaps, + while current β-case lemmas are conditional. L3 Qed results cover + matching echo rule pairs only. The open milestone is an explicit + L1/L2 judgment/step redesign and exact replacement theorem + boundaries, with all counterexample regressions retained. See + `PROOF-NEEDS.adoc` and `CLAUDE.md`. [#preservation-closure-plan] == Preservation: superseded by four-layer redesign @@ -254,15 +246,15 @@ No sequence of lemmas closes it because no proof exists. Canonical path now: -- **Design source**: `formal/PRESERVATION-DESIGN.md` (four orthogonal - layers: L1 region capabilities / L2 modality / L3 echo / L4 dyadic - mode). -- **Layered Coq files**: `TypingL1.v` (now `m`-indexed post-#176), - `Semantics_L1.v`, `Modality.v`, `Echo.v` — preservation re-derived - per layer from explicit invariants. +- **Design history**: `formal/PRESERVATION-DESIGN.adoc` records the four-layer + architecture; it is not a proof result. +- **Current Coq boundary**: `TypingL1.v`, `Semantics_L1.v`, `Modality.v`, + and `Echo.v` contain local judgments and lemmas. Unrestricted L1 + preservation is refuted; L2 has no unconditional theorem; L3 results + cover matching echo rule pairs only. - **Agent guidance**: `CLAUDE.md` at the repo root. - **Historical record**: the per-case reduction story (910 → 11 - goals) lives in `formal/PRESERVATION-HANDOFF.md` as archaeology. + goals) lives in `formal/PRESERVATION-HANDOFF.adoc` as archaeology. PRs #92 / #102 / #104 / #106 / #114 / #116 / #117 / #121 / #146 are pre-discovery; treat them as history, not instructions. @@ -301,16 +293,18 @@ audio buffer management: == v1.0.0 — Production ready -* [ ] **Per-layer preservation theorems closed**: `preservation_l1`, - `preservation_l2` (unconditional, post-Phase-3b Stage 4), and - `preservation_l3` (umbrella) all `Qed.` in `formal/Semantics_L1.v` - with clean `Print Assumptions`. See `formal/PRESERVATION-DESIGN.md - §12` and Phase 3b Stages 2/3/4 (#240/#241/#242). -+ +* [ ] **Sound language-level preservation boundary established**: + redesign/refine L1 and L2 judgments and prove replacement theorems + only after they state their exact hypotheses and cover the retained + counterexamples. The current `preservation_l1` and + `step_pop_disjoint_from_type_l1` statements are refuted; no + unconditional `preservation_l2` theorem exists. Existing L3 Qed + results are scoped to matching echo rule pairs. + NOTE: The legacy `Theorem preservation` in `formal/Semantics.v` is -provably false (`formal/Counterexample.v`) and stays `Admitted.` by -owner directive 2026-05-27. Closing it is NOT a v1.0 blocker — the -four-layer redesign supersedes it. +provably false (`formal/Counterexample.v`) and its `Admitted.` is durable. +It is archaeological, not ordinary proof debt, and any replacement must +be a separately stated theorem. * [ ] Idris2 `Parse/Parser.idr` upgraded from `%default covering` to `%default total` (LL(k) fuel-refactor; deferred separate campaign) * [ ] Stable surface syntax (already locked, but confirm no changes needed) @@ -330,12 +324,12 @@ four-layer redesign supersedes it. * link:README.adoc[README] — project overview + quickstart * link:EXPLAINME.adoc[EXPLAINME] — "show me the receipts" for the README's claims -* link:PROOF-NEEDS.md[PROOF-NEEDS] — outstanding proof obligations + leverage +* link:PROOF-NEEDS.adoc[PROOF-NEEDS] — outstanding proof obligations + leverage * link:RUST-SPARK-STANCE.adoc[RUST-SPARK-STANCE] — comparison + interop notes -* link:formal/PRESERVATION-HANDOFF.md[PRESERVATION-HANDOFF] — *archaeology only*: +* link:formal/PRESERVATION-HANDOFF.adoc[PRESERVATION-HANDOFF] — *archaeology only*: per-case Coq preservation checklist from the pre-discovery legacy-judgment closure plan. Retained for historical context. Not actionable; see - `formal/PRESERVATION-DESIGN.md` for the four-layer redesign. + `formal/PRESERVATION-DESIGN.adoc` for the four-layer redesign. * link:docs/vision/EPHAPAX-VISION.adoc[Vision document] — design rationale * link:docs/specs/DESIGN-DECISIONS.adoc[Design decisions] — 17 ADRs * link:docs/specs/LANGUAGE-COMPARISON.adoc[Language comparison] — vs 10 other languages diff --git a/STATUS.adoc b/STATUS.adoc index a3f2ef0c..c40aad3c 100644 --- a/STATUS.adoc +++ b/STATUS.adoc @@ -10,7 +10,7 @@ [IMPORTANT] .🛑 First-read disambiguation (human + machine readers) ==== -**This is `hyperpolymath/ephapax`.** Ephapax is a *research language for compile-time WebAssembly memory safety*, formally verified in Coq + Idris2, written in Rust + Coq + Idris2. +**This is `hyperpolymath/ephapax`.** Ephapax is a *research language for compile-time WebAssembly memory safety*, with formal artifacts in Coq + Idris2 and an implementation in Rust. The existing proofs do not establish general language soundness or implementation refinement; see `PROOF-NEEDS.adoc`. **Ephapax is *not* `hyperpolymath/affinescript`.** AffineScript is a *separate, unrelated language* that succeeds JavaScript / TypeScript / AffineScript — application-developer-facing, OCaml + AffineScript runtime, no mechanised proofs, no first-class regions. AffineScript is in a different universe with its own purpose, its own audience, its own codebase, its own roadmap. @@ -18,7 +18,7 @@ **Internal naming trap**: Ephapax itself is dyadic — it has two *internal sublanguages*: -* `ephapax-linear` — strict, formally-verified core +* `ephapax-linear` — strict core with formal artifacts; no full language-soundness or implementation-refinement proof is claimed * `ephapax-affine` — versatile prototyping companion to `ephapax-linear` Both live inside this repo (`ephapax-linear/` crate, shared AST, shared grammar). **`ephapax-affine` is NOT AffineScript.** The word `affine` overlapping in both names is a coincidence of substructural-logic terminology, not a project relationship. @@ -32,10 +32,11 @@ https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation [discrete] ==== One-paragraph orientation -Ephapax is **gestating** — part-way through a deliberate second draft, -on two independent tracks (grammar and soundness proof), both landing. -For the why-this-is-healthy framing, read link:V1-TO-V2.adoc[`V1-TO-V2.adoc`] -first; this document is the *operational* map underneath it. +Ephapax is **gestating** — part-way through a deliberate second draft. +Grammar work is active; the proof track has preserved the legacy +counterexample and discovered further L1/L2 gaps requiring redesign. +For the project framing, read link:V1-TO-V2.adoc[`V1-TO-V2.adoc`]; this +document is the *operational* map underneath it. On 2026-05-26 a verified Coq counterexample (`formal/Counterexample.v`, 5 Qed lemmas) *proved* that preservation as stated in the legacy @@ -43,17 +44,20 @@ single-judgment design (`formal/Semantics.v`) is unsound. Proving your own first draft's limit, before anyone depends on it, is the rare correct move — and it named exactly the invariant the redesign needed. The work since is **not** to close that theorem (no closure exists; the -`Admitted` is deliberate) but to build the *four-layer principled -redesign* (`formal/PRESERVATION-DESIGN.md`) where preservation is -**re-derived per layer** from explicit invariants. Three of the four -layers already carry `Qed` theorems. - -This document maps what that means for the repo: which work is **past** -(the v1 lesson — read it, don't build on it), which is **present** -(the v2 layers — active, extend), and which is **future** (next moves). -The two fenced-off v1 artefacts are narrow; everything in the v2 columns -is open and tractable. Read this before opening any `.v` file or any PR -comment dated before 2026-05-26. +`Admitted` is deliberate). The redesign is a separate line of work, not +an already sound replacement: the unrestricted L1 preservation statement +is also refuted by `formal/Counterexample_StepPop.v` and +`formal/Counterexample_PreservationL1.v`, while no unconditional L2 +preservation theorem is established. The L1/L2 counterexamples and the +conditional L2 lemmas are tracked separately in `PROOF-NEEDS.adoc`. +L3 calculus/wiring results do not discharge these language-soundness +obligations. + +This document distinguishes **legacy archaeology**, **redesigned +judgments**, **proved regressions**, and **open replacement obligations**. +Not every v2 claim is sound or tractable in its current statement: read +the pinned L1/L2 counterexamples before proposing closure work. See +`PROOF-NEEDS.adoc` for the canonical theorem boundary. toc::[] @@ -88,7 +92,7 @@ v2 layers below are where forward work goes). | The 910 → 12 admit-reduction trail under the legacy judgment. | All pre-2026-05-26. Closed retrospectively as archaeology. -| `formal/PRESERVATION-HANDOFF.md` +| `formal/PRESERVATION-HANDOFF.adoc` | The diagnostic record describing the obstacle that led to the counterexample discovery. | Reads as a closure plan; isn't one. Useful only for understanding @@ -118,9 +122,13 @@ v2 layers below are where forward work goes). == Present — the four-layer redesign in progress The redesign separates four concerns that the legacy judgment -conflated. Each layer has its own judgment, its own invariants, its -own per-layer preservation theorem. The orthogonality matters: a -fix at one layer must not require changes at another. +conflated, but this is an architectural plan—not a completed soundness +result. L1's current unrestricted preservation claim is refuted, and the +current tree has no unconditional L2 preservation theorem. The existence +of an upstream theory (including `echo-types`) or shared conceptual +vocabulary does not prove that Ephapax's syntax, typing rules, and +operational semantics satisfy language soundness. State each local theorem +and its assumptions explicitly. [cols="1,3,2,2,2"] |=== @@ -129,9 +137,9 @@ fix at one layer must not require changes at another. | L1 | Region capabilities, capability environment threading | `formal/TypingL1.v` + `formal/Semantics_L1.v` -| Substantially complete — judgment is 100%; semantics carries the - 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). +| Judgment and some helper lemmas are mechanised; unrestricted preservation + is refuted, not merely unfinished +| `TypingL1.v`: **2 / 0**. `Semantics_L1.v`: current proof markers are inventoried in `PROOF-NEEDS.adoc`; the two remaining outer admits (`step_pop_disjoint_from_type_l1`, `preservation_l1`) have refuted unrestricted statements, pinned by `Counterexample_StepPop.v` and `Counterexample_PreservationL1.v`. The L1 judgment and helper lemmas are not a preservation proof. | L2 | Structural modality (Linear vs Affine) @@ -145,8 +153,8 @@ fix at one layer must not require changes at another. | `formal/Echo.v` (+ upstream `hyperpolymath/echo-types`) | 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). + and `preservation_l3` are Qed for the matching echo rule pairs. This + scoped result is not general L1/L2 preservation. | `Echo.v`: **12 / 0** (plus 3 new Qed in `Semantics_L1.v` for the wiring). | L4 @@ -154,60 +162,55 @@ fix at one layer must not require changes at another. | `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`. + theorems by design. Design in `PRESERVATION-DESIGN.adoc §7`. | `L4.v`: definitions only — no Qed, no Admitted. |=== [NOTE] ==== -.Why this works +.Design intent and current evidence The legacy judgment conflated structural discipline + region capabilities -+ echo residue + dyadic mode. The counterexample exploits the gap that -makes that conflation unsound: region exit invalidates sibling -assumptions without the judgment tracking the dependency. The four-layer -split makes those four concerns *first-class* and *orthogonal*. Each layer -proves its own preservation theorem against its own invariants. The -language gets the safety of all four without the unsoundness of the -combined form. ++ echo residue + dyadic mode. Its counterexample shows that region exit can +invalidate sibling assumptions when the judgment does not track the +dependency. The four-layer split makes the concerns explicit, but explicit +layering alone does not establish soundness: the L1 counterexamples refute +the current unrestricted L1 preservation statement, and L2 remains without +an unconditional preservation theorem. The L3 Qed results cover their +stated echo rule pairs only. The replacement language-level obligations are +open and must be proved locally against Ephapax's own rules. ==== [IMPORTANT] ==== -.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`). +.Reading the L3 layer status +L3 wiring has landed. The `Echo.v` calculus is consumed by the paired +L3 typing/step rules at the stated irreversible boundaries. +`preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, and +`preservation_l3` are Qed for those matching cases, with zero hidden claim +of general L1/L2 preservation. Additional L3 rule coverage and L4 design +remain separate work (`PRESERVATION-DESIGN.adoc §7`). ==== == Future — what comes next -=== 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. +=== Near-term (sound replacement statements; preserve regression witnesses) + +* Do not try to prove the unrestricted `preservation_l1` or + `step_pop_disjoint_from_type_l1` statements: each is refuted by a pinned + Coq witness. The open work is redesigning the L1 judgment / step interface + to carry temporal region-liveness or coherence, then stating and proving a + replacement theorem with explicit scope. +* There is no unconditional `preservation_l2` theorem in the current tree. + The L2 β-case helpers are conditional; the fresh-region and nested-`TFunEff` + counterexamples in `Counterexample_L2.v` and + `Counterexample_L2_nested.v` must stay visible when any replacement is + proposed. Do not infer a language theorem from a helper lemma or from + vocabulary/results in another repo. +* L3's Qed lemmas are limited to their stated echo-emitting rule pairs; they + are not a substitute for general L1/L2 preservation. +* Preserve all counterexample files as regression witnesses and report proof + assumptions / build evidence at the exact theorem boundary. Do not re-derive + the false legacy theorem. === Mid-term (L4 — Phase A landed, design ongoing) @@ -220,7 +223,7 @@ step rules. Mid-block work is L4 design (`PRESERVATION-DESIGN.md §7`). `#![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`. + per `PRESERVATION-DESIGN.adoc §7`. === Value-prop directions (committed and speculative) @@ -246,10 +249,10 @@ doesn't have. Their relative status: shape, different mode declaration. | **Debugging / provenance via Linear Echoes** -| Committed -| Mandatory-observed echo = receipt that cannot be forgotten = a - type-system guarantee that the preimage of a critical state change - was retained. +| Design intent; selected L3 rules landed +| The design aims for Linear Echoes to make selected state-change + preimages observable. Current Qed results cover matching echo rule + pairs only and do not prove an end-to-end provenance guarantee. | **Linear discipline on deterministic drop (Rust-style)** for critical resources (keys, sensitive buffers) requiring provable @@ -278,12 +281,13 @@ category error. == The fences (narrow by design) -These are the guardrails — and they are deliberately *narrow*. Items 1–5 -all fence off the **one** falsified v1 artefact (the legacy preservation -theorem and attempts to close it). Items 6–7 are two **design invariants** -that keep the v2 layers orthogonal. Nothing here closes off the live v2 -work: the per-layer proofs and the grammar phases remain open. Read this -as "mind these specific posts," not "the field is closed." +These guardrails fence off both the false legacy preservation theorem +and later unrestricted L1 statements refuted by pinned witnesses. They do +not block sound redesign work. The four-layer architecture is not itself a +proof, L2 has no unconditional preservation theorem, and matching-rule L3 +results remain scoped. Grammar phases and proof redesign are live work; +read this as preserving exact theorem boundaries, not as declaring the +field closed. * ❌ Closing the legacy `Theorem preservation` in `formal/Semantics.v`. It is FALSE. No proof closes it. @@ -302,11 +306,10 @@ as "mind these specific posts," not "the field is closed." == Where to read next -* **Design doctrine**: `formal/PRESERVATION-DESIGN.md` — the canonical - four-layer architecture, the missing-invariant statement, the - per-layer plan. -* **Proof debt**: `PROOF-NEEDS.md` — what's done, what's todo, what's - banned, separated for ephapax-linear and ephapax-affine sublanguages. +* **Design history**: `formal/PRESERVATION-DESIGN.adoc` — architecture + rationale and historical plans; not proof of a soundness result. +* **Current proof status**: `PROOF-NEEDS.adoc` and `EXPLAINME.adoc` — + counterexamples, scoped results, ledger, and replacement obligations. * **Agent guidance**: `CLAUDE.md` (root) — the 2026-05-27 owner directive, anti-pattern detector, escalation rule. * **Counterexample**: `formal/Counterexample.v` — the 5 Qed lemmas @@ -316,9 +319,9 @@ as "mind these specific posts," not "the field is closed." == Cross-references -* `formal/PRESERVATION-DESIGN.md §3` — "The four orthogonal concerns". -* `formal/PRESERVATION-DESIGN.md §6.2` — "Two modes, one type former". -* `formal/PRESERVATION-DESIGN.md §6.4` — "What L3 demands that L1+L2 +* `formal/PRESERVATION-DESIGN.adoc §3` — "The four orthogonal concerns". +* `formal/PRESERVATION-DESIGN.adoc §6.2` — "Two modes, one type former". +* `formal/PRESERVATION-DESIGN.adoc §6.4` — "What L3 demands that L1+L2 must not contradict". * `CLAUDE.md` "Owner directive 2026-05-27 — preservation work" — the DO and DO-NOT lists this document derives from. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index cacf4df0..d2c2deca 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -51,7 +51,7 @@ pass/fail enforced by `+rust-ci.yml+` `+formal/Semantics_L1.v+` — `+step_pop_disjoint_from_type_l1+` / `+preservation_l1+` — covering 2 internal `+admit.+` cases at lines 3315/3336; rebuilt `+coqc 8.18.0+` ground truth 2026-06-27). Single- -source breakdown lives in `+PROOF-NEEDS.md §4+`; +source breakdown lives in `+PROOF-NEEDS.adoc §4+`; `+scripts/status-gate.sh+` reads from there. ===== Crates with ZERO tests: @@ -70,7 +70,7 @@ source breakdown lives in `+PROOF-NEEDS.md §4+`; * 3 Admitted markers in Coq (1 in `+Semantics.v+` — provably-false legacy preservation, sacrosanct; 2 in `+Semantics_L1.v+` — `+step_pop_disjoint_from_type_l1+` + `+preservation_l1+`, the -eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.md §4) +eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.adoc §4) * 5 remaining tasks (#15-#19) from type checker audit * interp env-leak fix was made 2026-03-28 @@ -108,9 +108,11 @@ vendored). * [ ] panic-attack assail on own repo * [ ] Compile all .eph stdlib files as test suite -* [ ] 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) +* [ ] Establish sound replacement preservation theorems after L1/L2 +redesign. Keep the legacy `+preservation+` marker and the two L1 +`+Admitted.+` markers: their unrestricted statements are refuted and +must not be converted into fake proofs or ordinary debt entries. See +`+PROOF-NEEDS.adoc+`. === Priority diff --git a/V1-TO-V2.adoc b/V1-TO-V2.adoc index 2a727879..f36b7fc4 100644 --- a/V1-TO-V2.adoc +++ b/V1-TO-V2.adoc @@ -37,7 +37,8 @@ toc::[] Ephapax is a research language for compile-time-memory-safe WebAssembly with first-class irreversible boundaries (region exits, drops, key erasure, audit trails). It is mid-way through **two parallel second -drafts**, and both are going well: +drafts**; grammar work is active, while the proof track has identified +additional L1/L2 soundness gaps that require redesign: * **The grammar.** v1 was a flat surface fed straight to the parser. It worked for the core calculus but had no room to grow into modules, @@ -70,7 +71,7 @@ did, and the second draft is sharper for it. project.status = GESTATING # not dead, not abandoned, not frozen project.phase = v1 → v2 redesign, two tracks (grammar, proof) project.live_work = YES — see "Live work" below; engage with it -caution.scope = LEGACY ONLY — confined to two clearly-fenced v1 artefacts +caution.scope = preserve pinned false statements (legacy + current L1); design replacement theorems separately grammar.v1.status = SUPERSEDED (pest surface; works for core, does not scale) grammar.v2.status = ACTIVE (spec/ephapax-v2-grammar.ebnf; phases landing; tests green) @@ -78,37 +79,40 @@ grammar.v2.tractable = YES proof.v1.status = FALSIFIED (formal/Semantics.v preservation; Counterexample.v, 5 Qed) proof.v1.action = LEAVE AS Admitted; do NOT attempt to close (no closure exists) -proof.v2.status = ACTIVE (four-layer L1–L4; preservation re-derived per layer) -proof.v2.tractable = YES — L1 structural admits + unconditional preservation_l3 +proof.v2.status = REDESIGN IN PROGRESS (four-layer architecture is not yet a sound replacement) +proof.v2.tractable = OPEN DESIGN — current unrestricted L1 preservation is refuted; no unconditional L2 preservation theorem exists; L3 results are scoped # The single most common bot failure mode in this repo: # reading the "do not close the legacy theorem" guardrail as # "there is nothing to do here" and bailing. That is wrong. -# The guardrail fences off ONE false theorem. Everything in the v2 -# columns above is open, tractable, and wants work. +# The guardrails preserve multiple pinned false statements. Active +# v2 work is theorem redesign, not closure of those statements. ---- ==== -The prohibitions you will find in `CLAUDE.md` and `STATUS.adoc` are -**narrow**: they fence off exactly two v1 artefacts (the falsified -`Semantics.v` preservation theorem and the superseded v1 surface -grammar). They are not a statement about the project's health. Treat -them as "mind the wet paint on this one wall," not "the building is -condemned." +The guidance in `CLAUDE.md` and `STATUS.adoc` is about preserving +specific proof boundaries: the false legacy theorem, the separately +refuted unrestricted L1 statements, and historical grammar. This is not +a claim that the redesign is already sound. Active proof work means +reformulating judgments and theorem boundaries while retaining every +counterexample regression. [#live-work] === Live work (tractable, wants doing) -* **Proof, L1:** close the residual L1 structural admits in - `formal/Semantics_L1.v` (list/multiset bridge; `TFun` effect typing). - These are *v2 design follow-ups*, not legacy patching. See - `PROOF-NEEDS.md §4`. -* **Proof, L3:** state and prove the **unconditional** `preservation_l3` - (currently conditional on an L1 admit). +* **Proof, L1:** do not close the current unrestricted + `step_pop_disjoint_from_type_l1` or `preservation_l1`; both are refuted + by pinned counterexamples. The open work is a judgment/step redesign + with an explicit temporal invariant and a new theorem boundary. +* **Proof, L2:** no unconditional `preservation_l2` theorem exists; + retain the fresh-region and nested-`TFunEff` counterexamples and state + exact preconditions on any replacement. +* **Proof, L3:** selected matching echo rule-pair preservation lemmas are + Qed; this scoped result is not general L1/L2 preservation. * **Grammar, v2:** continue the phase work in `spec/ephapax-v2-grammar.ebnf` + the `v2_grammar_phase_*` CLI tests. * **Proof, L4:** Phase A scaffold has landed; the dyadic mother–child - semantics in `PRESERVATION-DESIGN.md §7` is the next design step. + semantics in `PRESERVATION-DESIGN.adoc §7` is the next design step. [#what-gestating-means] == What "gestating" means here @@ -220,34 +224,41 @@ deliberate**: it marks a theorem we have *proven cannot be closed*, not a gap we are too lazy to fill. ==== -=== v2: four orthogonal layers, preservation re-derived per layer +=== v2: four-layer architecture, soundness work still open -The redesign (`formal/PRESERVATION-DESIGN.md`) splits the four conflated -concerns into four first-class, orthogonal layers. Each has its own -judgment, its own invariants, and its own preservation theorem — so a fix -in one layer cannot silently break another. +The redesign (`formal/PRESERVATION-DESIGN.adoc`) separates the four +conflated concerns. This architecture is not itself a soundness result: +the current unrestricted L1 preservation statement is refuted, and there +is no unconditional L2 preservation theorem. L3's Qed result is scoped to +matching echo-emitting rule pairs. See `PROOF-NEEDS.adoc` before treating +any layer-level result as a language theorem. [cols="1,3,2"] |=== | Layer | Concern | v2 status -| **L1** | Region capabilities | Judgment complete; semantics carries a - small set of named structural admits (the live work). +| **L1** | Region capabilities | Judgment and helper infrastructure exist; + the unrestricted preservation statement is refuted. Two outer `Admitted.` + markers remain on false unrestricted statements, not routine proof debt; + redesign and restricted replacement are open. | **L2** | Structural modality (Linear vs Affine) | Core landed, `linear_to_affine` `Qed`, **zero axioms**. | **L3** | Echo / residue — what was *lost* at an irreversible step | Calculus - + wiring landed; `preservation_l3` `Qed` (conditional on one L1 admit). + + wiring landed; `preservation_l3` is Qed for matching echo-emitting + rule pairs only, not conditional on the removed L1 region-liveness admit + and not a general L1/L2 preservation theorem. | **L4** | Dyadic mode (mother–child) | Phase A scaffold landed; semantics design is the next step. |=== === What v1 taught v2 -The counterexample named the missing invariant precisely: *a step that -exits a region must not leave a sibling's typing assumptions standing.* -v1 had no place to state that. v2's L1 makes region-capability threading -first-class, which is exactly the place that invariant lives. The bug -became the blueprint. +The legacy counterexample named a missing invariant: *a step that exits +a region must not leave a sibling's typing assumptions standing.* L1 +makes region-capability threading explicit, but later pinned L1 +counterexamples show that this alone does not encode the required temporal +invariant. Treat the invariant as a redesign target, not as a property +already enforced by the current judgment. [#settled] == What is genuinely settled (the fully transparent list) @@ -266,25 +277,25 @@ are closed, and closed for good reasons: extending the flat v1 surface. The v1 EBNFs remain accurate for the *core* and stay in-tree as reference; they are not the growth surface. -Everything else — all of L1/L2/L3/L4's open theorems, every v2 grammar -phase not yet landed — is **live, tractable work**. The fence is two -posts wide. The field behind it is open. +The live work is the soundness redesign described above plus grammar +phases not yet landed. Its tractability and theorem boundaries must be +evaluated from the local Ephapax rules and counterexamples, not assumed +from the four-layer labels. [#one-thing] == If you only remember one thing -> Ephapax is not a failed language. It is a careful one, caught in the -> middle of its second draft, having done the rare thing of proving its -> own first draft's limits before building the better second. Read the -> warnings as *guardrails around two fenced-off v1 artefacts*, then go -> work on v2 — the grammar phases and the per-layer proofs are open and -> waiting. +> Ephapax's proof story is intentionally bounded. The legacy preservation +> statement and the current unrestricted L1 statements have pinned +> counterexamples; L2 preservation remains conditional/unestablished. +> Preserve those regressions, and work on explicit sound replacements rather +> than treating the redesign labels as proof. == Where to read next * `STATUS.adoc` — the operational past / present / future map. -* `formal/PRESERVATION-DESIGN.md` — the four-layer architecture in full. -* `PROOF-NEEDS.md` — per-sublanguage proof debt, with the explicit +* `formal/PRESERVATION-DESIGN.adoc` — the four-layer architecture in full. +* `PROOF-NEEDS.adoc` — per-sublanguage proof debt, with the explicit do-not-do list. * `spec/ephapax-v2-grammar.ebnf` — the v2 surface grammar specification. * `CLAUDE.md` — agent guidance; its prohibitions are the two fence posts diff --git a/brand/marr-levels.svg b/brand/marr-levels.svg index e4ac3ee5..36d2084b 100644 --- a/brand/marr-levels.svg +++ b/brand/marr-levels.svg @@ -1 +1 @@ -ephapax — at Marr's three levelsone system, read from intent down to substrateabstract → concrete?Computational — what & whyGuarantee resource safety — no leak, no use-after-free, exactly-once —for the whole neurosymbolic stack. A dyadic linear/affine language.Algorithmic — representation & processFour layers: L1 region capabilities · L2 modality (linear/affine) ·L3 echo residue · L4 dyadic mode. Preservation re-derived per layer.Implementational — physical substrateRust crate ephapax-linear + dual machine proofs (Coq formal/*.v,Idris2 src/abi). Compiles to typed-wasm — foundation of the chain. \ No newline at end of file +ephapax — at Marr's three levelsone system, read from intent down to substrateabstract → concrete?Computational — what & whyResearch target: accountable resource safety across a typed-WASM stack.Current proofs do not establish a whole-stack safety guarantee.Algorithmic — representation & processFour layers: L1 region capabilities · L2 modality (linear/affine) ·L3 echo residue · L4 dyadic mode. The architecture is not a proof.Implementational — physical substrateRust crate ephapax-linear + formal artifacts (Coq formal/*.v,Idris2 src/abi). L1 preservation is refuted; L2 is not unconditional. \ No newline at end of file diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index d942813f..6f5a9029 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -21,36 +21,43 @@ obligation has been discharged. * *Acceptance*: retain the counterexample regression and publish any replacement theorem with its exact restricted boundary and zero hidden escape hatches. -==== `+formal/Semantics_L1.v:3318+` — `+step_pop_disjoint_from_type_l1+` - -* *Status*: one internal `+admit.+` followed by one outer `+Admitted.+`; not - proved. -* *Obligation*: establish region-count coherence when a congruence step exits a - region still required by a sibling's type. Ten former sub-cases are closed; - this is the one residual case. -* *Obstacle*: the snapshot region environment and result type do not encode the - temporal distinction needed to show that the sibling's occurrence survives - the exit. The choreographic experiment in - `+formal/L1-ELIMINATOR-FORK.adoc+` showed that the first proposed formulation - relocates this obligation rather than discharging it. -* *Owner*: @hyperpolymath. -* *Plan and tracking*: continue the staged calculus work in issues #240, #241, - and #242; first require a coherent minimal counterexample/positive control, - then prove the supporting lemma without circularly assuming preservation. -* *Acceptance*: `+Qed.+`, a clean `+Print Assumptions - step_pop_disjoint_from_type_l1.+`, and a regression showing that an invalid - region exit is rejected. - -==== `+formal/Semantics_L1.v:3337+` — `+preservation_l1+` - -* *Status*: one internal `+admit.+` followed by one outer `+Admitted.+`; not - proved. -* *Dependency*: blocked by `+step_pop_disjoint_from_type_l1+` and the staged L2 - restrictions tracked in issues #240, #241, and #242. -* *Owner*: @hyperpolymath. -* *Acceptance*: the theorem ends in `+Qed.+`, `+Print Assumptions - preservation_l1.+` reports no project escape hatch, and the complete Coq - build plus counterexample suite passes. +==== Redesigned L1 preservation boundary — `+formal/Semantics_L1.v+` + +The source still contains two `+Admitted.+` declarations, but neither is a +routine open proof obligation. Their exact unrestricted statements are +refuted by pinned counterexamples: + +* `+step_pop_disjoint_from_type_l1+` (source near line 3318) is *false as + stated*: `+formal/Counterexample_StepPop.v+` proves that a typed step can + remove a region still free in the result type. Its `+Admitted.+` is not a + promise that this theorem should be finished. +* `+preservation_l1+` (source near line 3337) is *false as stated*: + `+formal/Counterexample_PreservationL1.v+` gives an input typed in both + modalities and a step whose post-state is untypable in the Linear + instance, refuting the theorem's modality-polymorphic quantification. + This closes the suggested value-anchored escape route as well; it does + not by itself refute a separate Affine-only theorem. + +The counterexamples are proof regressions, not proofs of an alternative +soundness theorem. The open work is to redesign or strengthen the judgment / +operational interface with an explicit temporal liveness/coherence invariant, +then state and prove a replacement theorem with its exact boundary. Do not +close either current statement by ad-hoc lemma work or change these `+Admitted.+` +markers into claimed proofs. Track that replacement separately from the +legacy archaeology below. + +==== L2 preservation boundary — `+formal/TypingL2.v+` + +There is no unconditional theorem named `+preservation_l2+` in the current +tree. `+preservation_l2_via_l1+` transparently depends on the refuted L1 +statement, while the β-case lemmas are proved only under their stated +preconditions. `+formal/Counterexample_L2.v+` (fresh-region scope crossing) +and `+formal/Counterexample_L2_nested.v+` (nested `+TFunEff+` lambda) record +distinct counterexample classes for broader L2 β-preservation. They do not +invalidate the conditional helper lemmas whose hypotheses exclude those +classes; nor do they establish full L2 preservation. Any future L2 theorem +must name and prove its restricted boundary without inheriting the L1 +counterexample by assumption. ==== `+idris2/src/Main.idr:22+` — global `+%default partial+` @@ -90,8 +97,8 @@ closure plan and lists `+step_preserves_type+` / `+formal/Semantics.v+` is _provably false_ (`+formal/Counterexample.v+`, five `+Qed+` lemmas) and its `+Admitted.+` is correct + durable. -*Canonical proof-debt sources*: - `+PROOF-NEEDS.md+` (root) - -`+formal/PRESERVATION-DESIGN.md §12+` - `+formal/PHASE-D-REDESIGN.md+` +*Canonical proof-debt sources*: - `+PROOF-NEEDS.adoc+` (root) - +`+formal/PRESERVATION-DESIGN.adoc §12+` - `+formal/PHASE-D-REDESIGN.md+` Retained for traceability against the https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc[trusted-base-reduction diff --git a/docs/vision/EPHAPAX-VISION.adoc b/docs/vision/EPHAPAX-VISION.adoc index eb514291..4fb2cc2d 100644 --- a/docs/vision/EPHAPAX-VISION.adoc +++ b/docs/vision/EPHAPAX-VISION.adoc @@ -9,24 +9,20 @@ Jonathan D.A. Jewell [IMPORTANT] .Post-counterexample reorientation 2026-05-27 ==== -This vision document is **the design rationale**. The architecture -described here was reframed on 2026-05-26 when a verified Coq -counterexample showed the original single-layer typing judgment was -*provably false*. The current architecture is a *four orthogonal -layers* design (region capabilities / structural modality / echo -residue / dyadic mode) where preservation is re-derived per layer -from explicit invariants. +This vision document is **design rationale, not proof evidence**. The +four-layer architecture (region capabilities / structural modality / +echo residue / dyadic mode) is a design program; preservation has not +been re-derived successfully for every layer. Later pinned Coq +counterexamples refute the legacy and unrestricted L1 statements, and no +unconditional L2 theorem is established. The intent below — dyadic +discipline, region-based memory, no tracing GC, and a WASM target — is +aspirational where it describes end-to-end safety. -The *intent* below — dyadic discipline, region-based memory, no -tracing GC, WASM target — survives the redesign intact. The -*mechanisation* is layered. - -For implementation status (per-layer counts, what's done, what's -todo, what's banned), read in this order: +For current implementation and proof status, read in this order: . link:../../STATUS.adoc[`STATUS.adoc`] — past/present/future map. -. link:../../formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`] — the four-layer architecture doctrine. -. link:../../PROOF-NEEDS.md[`PROOF-NEEDS.md`] — per-sublanguage proof debt. +. link:../../formal/PRESERVATION-DESIGN.adoc[`formal/PRESERVATION-DESIGN.adoc`] — architecture history. +. link:../../PROOF-NEEDS.adoc[`PROOF-NEEDS.adoc`] and `EXPLAINME.adoc` — current proof boundaries and ledger. ==== [NOTE] @@ -107,11 +103,10 @@ partners in the dyad: each is enforced independently, but each takes its | Layer | What the dyad says about it | L1 — Region capabilities -| Identical in both modes. Every live region is tracked in an - input/output capability environment threaded through every - compound expression. A sibling cannot reference a region a - previous sibling has exited. The mother and the child obey the - same L1 invariant; the soundness story is the same. +| Identical in both modes. The judgment threads an input/output region + environment through compound expressions, but later Coq counterexamples + refute unrestricted L1 preservation. The intended sibling-safety + invariant is not established by threading alone; see `PROOF-NEEDS.adoc`. | L2 — Structural modality | *This is the dyad itself.* The mother is `Linear`; the child is @@ -164,23 +159,20 @@ forks: linear enforcer | affine enforcer == The Workflow -This is the practical power of the dyad: +This is the intended workflow of the dyad, subject to the implementation +and proof boundaries above: -. *Plan and build in Affine* — write real, properly typed Ephapax code without - being blocked by linear obligations you are not ready to address. The affine - type checker is doing real work. You have genuine guarantees. You can think, - build, get a working thing, without solving problems that are not the - current problem. +. *Plan and build in Affine* — the checker can accept programs under the + Affine rules. This is an implementation-level type-checking result, not + a proved language-soundness or memory-safety guarantee. -. *Tighten to Linear when ready* — run the linear enforcer. It does not say - "rewrite this." It says precisely what does not satisfy linear discipline. - Because the syntax is identical and the code was always truly typed, the - path from affine to linear is a targeted, type-guided process — not a - rewrite. +. *Tighten to Linear when ready* — the linear checker reports violations + of its discipline. Shared syntax and checker behavior do not by themselves + prove a refinement relation or a complete proof of correctness. -You always have truly typed code. The affine stage is not a sketch or a -prototype you will throw away. It is a typed foundation that the linear -enforcer can read directly. +The affine stage is intended to support experimentation before enforcing +stricter obligations. Whether accepted programs enjoy end-to-end safety +requires separate local proofs and implementation correspondence. *The daughter grows up, but her freedom and adaptiveness must not be lost in that growing.* diff --git a/docs/wikis/Home.md b/docs/wikis/Home.md index 28a32688..79cbce68 100644 --- a/docs/wikis/Home.md +++ b/docs/wikis/Home.md @@ -18,8 +18,8 @@ This wiki is the *signpost* — canonical docs live in the repo. Edit [`docs/wik |---|---| | Understand what Ephapax is | [README.adoc](https://github.com/hyperpolymath/ephapax/blob/main/README.adoc) | | See the current proof status | [STATUS.adoc](https://github.com/hyperpolymath/ephapax/blob/main/STATUS.adoc) | -| Understand the four-layer redesign | [formal/PRESERVATION-DESIGN.md](https://github.com/hyperpolymath/ephapax/blob/main/formal/PRESERVATION-DESIGN.md) | -| See the per-sublanguage proof debt | [PROOF-NEEDS.md](https://github.com/hyperpolymath/ephapax/blob/main/PROOF-NEEDS.md) | +| Understand the four-layer redesign | [formal/PRESERVATION-DESIGN.adoc](https://github.com/hyperpolymath/ephapax/blob/main/formal/PRESERVATION-DESIGN.adoc) | +| See the per-sublanguage proof debt | [PROOF-NEEDS.adoc](https://github.com/hyperpolymath/ephapax/blob/main/PROOF-NEEDS.adoc) | | See the counterexample that invalidated the old design | [formal/Counterexample.v](https://github.com/hyperpolymath/ephapax/blob/main/formal/Counterexample.v) | | See architecture decisions | [docs/specs/DESIGN-DECISIONS.adoc](https://github.com/hyperpolymath/ephapax/blob/main/docs/specs/DESIGN-DECISIONS.adoc) | | See machine-readable state | [.machine_readable/6a2/STATE.a2ml](https://github.com/hyperpolymath/ephapax/blob/main/.machine_readable/6a2/STATE.a2ml) | @@ -51,7 +51,7 @@ The four layers and their current state: | Layer | Description | Status | |---|---|---| -| **L1** — Region capabilities | `R_in`, `R_out`, `In r R` threading | Substantially complete; `preservation_l1` proved conditional on L2 effect-typing | +| **L1** — Region capabilities | `R_in`, `R_out`, `In r R` threading | Judgment/helpers mechanised; unrestricted `preservation_l1` refuted by pinned counterexample; replacement redesign open | | **L2** — Structural modality | `m : Modality` in `has_type_l1`; `linear_to_affine` | Core landed (PRs #176+#177); `linear_to_affine` Qed, zero axioms; 6 supporting lemmas regressed to Admitted pending Phase D Stages 2–4 | | **L3** — Echo residue | What was lost at an irreversible step | `preservation_l3` + two companions Qed (conditional); wired into L1 | | **L4** — Dyadic mode | Project-level mode declaration | Phase A scaffold landed (`formal/L4.v`): `PModeLinear`/`PModeAffine`/`PModeBoundaryMix` + round-trip; definitions only by design | @@ -81,5 +81,5 @@ The four layers and their current state: - **Licence**: MPL-2.0 - **Machine-readable state**: [`.machine_readable/6a2/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/6a2/) - **Contractiles**: 6-verb governance in [`.machine_readable/contractiles/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/contractiles/) -- **Security policy**: [SECURITY.md](https://github.com/hyperpolymath/ephapax/blob/main/SECURITY.md) +- **Security policy**: [SECURITY.adoc](https://github.com/hyperpolymath/ephapax/blob/main/SECURITY.adoc) - **Open issues**: [github.com/hyperpolymath/ephapax/issues](https://github.com/hyperpolymath/ephapax/issues) diff --git a/ephapax-linear/README.adoc b/ephapax-linear/README.adoc index 592dc9a0..a994b94b 100644 --- a/ephapax-linear/README.adoc +++ b/ephapax-linear/README.adoc @@ -4,8 +4,9 @@ ____ === 🛑 First-read disambiguation This crate is part of *`+hyperpolymath/ephapax+`* — a research language -for compile-time WebAssembly memory safety, formally verified in Coq + -Idris2. +for compile-time WebAssembly memory safety with formal artifacts in Coq +and Idris2. Those artifacts do not establish general language soundness +or implementation refinement; see `+PROOF-NEEDS.adoc+`. *`+ephapax-linear+` is _not_ `+hyperpolymath/affinescript+`.* AffineScript is a separate, unrelated language (JS/TS/AffineScript @@ -34,7 +35,7 @@ are not different languages — they are two admissible-derivation regimes over the same syntax and semantics. See link:../docs/vision/EPHAPAX-VISION.adoc[`+docs/vision/EPHAPAX-VISION.adoc+`] for the dyad framing, and -link:../formal/PRESERVATION-DESIGN.md[`+formal/PRESERVATION-DESIGN.md §5+`] +link:../formal/PRESERVATION-DESIGN.adoc[`+formal/PRESERVATION-DESIGN.adoc §5+`] for the L2 layer in the four-layer architecture. ____ diff --git a/formal/Counterexample.v b/formal/Counterexample.v index 5ea5aebb..fbe62bed 100644 --- a/formal/Counterexample.v +++ b/formal/Counterexample.v @@ -14,11 +14,11 @@ *** load-bearing for the regression theorem; do not "fix" the *** *** legacy judgment to make these lemmas fail. *** *** *** - *** bad_input_untypable_l1 is also Qed under BOTH modalities, *** - *** showing that the new L1 judgment closes the gap regardless of *** - *** Linear vs Affine. *** + *** bad_input_untypable_l1 is also Qed under BOTH modalities. *** + *** It rejects this legacy witness only; later L1 preservation *** + *** counterexamples are pinned separately. *** *** *** - *** See `STATUS.adoc`, `formal/PRESERVATION-DESIGN.md §1`. *** + *** See `STATUS.adoc`, `formal/PRESERVATION-DESIGN.adoc §1`. *** ********************************************************************* *) @@ -42,7 +42,7 @@ Diagnoses the obstacle for preservation's 10 touches_region RIGHT branches: closing them requires a type-system change (Option 3 in - PRESERVATION-HANDOFF.md), not a proof technique. *) + PRESERVATION-HANDOFF.adoc), not a proof technique. *) From Ephapax Require Import Syntax Typing Semantics. Require Import Coq.Strings.String. @@ -153,18 +153,22 @@ Section Counterexample. a single-step reduction exists; [bad_post_untypable] shows the result of that reduction is untypable at the same outer type. - The 11 remaining preservation admits on the [touches_region] - RIGHT branches share this structure. A type-system change - (Option 3 in PRESERVATION-HANDOFF.md) is required. *) + Historical closure attempts recorded 11 remaining admits on the + [touches_region] RIGHT branches; that count is archival, not a + current proof obligation. This witness refutes the universal theorem. + Its [Admitted] remains durable; a different sound theorem requires + an approved redesign, not closure of this statement. See + [PRESERVATION-HANDOFF.adoc] for archaeology. *) End Counterexample. -(** * L1 regression: the redesigned typing blocks the bad input +(** * L1 regression: the redesigned typing blocks this legacy input - With the [has_type_l1] judgement from [TypingL1.v], the bad input - [e_bad] no longer has a derivation — the L1 fix replaces the - post-step untypability of the original counterexample with **input - untypability**. + With the [has_type_l1] judgement from [TypingL1.v], this particular + bad input [e_bad] has no derivation — for this witness, the L1 rules + replace post-step untypability with **input untypability**. This + regression is not a general L1 soundness or preservation theorem; + [Counterexample_PreservationL1.v] records a different L1 failure. Proof structure: - Invert [T_Pair_L1] on the assumed derivation: forces the diff --git a/formal/Counterexample_L2.v b/formal/Counterexample_L2.v index 3cb237ec..92deba02 100644 --- a/formal/Counterexample_L2.v +++ b/formal/Counterexample_L2.v @@ -2,22 +2,23 @@ (* Owner: Jonathan D.A. Jewell *) (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) -(** * Soundness gap (L2): preservation_l2 fails for TFunEff substituends +(** * L2 β-preservation counterexample: TFunEff substituends inside fresh-region scopes - The Phase D slice 4 Phase 4c β-case of preservation_l2 fails for - programs that substitute a TFunEff value into a body containing - [ERegion] (fresh-region) introduction. + This exact β-case witness shows that the proposed unrestricted + preservation claim fails for programs substituting a TFunEff value + into a body containing [ERegion] (fresh-region) introduction. No + unconditional [preservation_l2] theorem is declared in the current tree. This file mechanises the counterexample. It mirrors the structure of [Counterexample.v] (which exhibits the legacy preservation's soundness gap) but at the L1/L2 layer with the post-redesign - [has_type_l1] / [has_type_l2] judgments. The artifact justifies - the **conditional** preservation_l2 closure recommended in - [SUBST-LEMMA-GENERALIZATION-DESIGN.md] §"Phase 4c": preservation - holds only for programs satisfying - [regions_introduced_by(ebody) ⊆ R_in_v]; programs outside this - class form a documented soundness-gap subclass. + [has_type_l1] / [has_type_l2] judgments. The artifact motivates + the **conditional** β-case restriction proposed in + [SUBST-LEMMA-GENERALIZATION-DESIGN.md] §"Phase 4c": exclude programs + whose [regions_introduced_by(ebody)] are not contained in [R_in_v]. + This witness does not prove the restricted β-case theorem or general + L2 preservation; see [PROOF-NEEDS.adoc]. ===== Configuration ===== diff --git a/formal/Counterexample_L2_nested.v b/formal/Counterexample_L2_nested.v index 4c3be2ca..79846aba 100644 --- a/formal/Counterexample_L2_nested.v +++ b/formal/Counterexample_L2_nested.v @@ -4,9 +4,9 @@ (* hypatia: allow code_safety/admitted -- FALSE POSITIVE: this file has no Coq admit/Admitted/Axiom; all proofs are Qed-closed. The scanner substring-matched prose in the doc comment that NEGATES their presence ("No new [Axiom] or [Admitted] markers"). *) (* hypatia: allow coq_admit_tactic -- same false positive: substring match on documentation prose, not a Coq tactic. *) -(** * Soundness gap (L2): preservation_l2 fails for nested-TFunEff - substituends — the gap Phase 3b Stage 1's [tfuneff_lambda_free] - precondition correctly EXCLUDES. +(** * L2 β-preservation counterexample: nested-TFunEff substituends + — excluded by the Phase 3b Stage 1 [tfuneff_lambda_free] precondition. + No unconditional [preservation_l2] theorem is declared. Sibling artifact to [Counterexample_L2.v]. That earlier file witnessed the soundness gap for TFunEff substituends crossing @@ -23,10 +23,10 @@ (P2) [regions_introduced_by ebody ⊆ R_in_v] — rules out [Counterexample_L2.v]'s class (fresh region) - Stage 2 (#240) lifts (P1) by carrying [R_in / R_out] on [ELam]. - Stage 3 (#241) replaces (P1) with a CPS-style proof that closes - the inner-lambda case via a relaxed [declared_lambda_r_ins ⊆ R_in_v] - obligation. Stage 4 (#242) reaches an unconditional preservation_l2. + The Stage 2–4 sequence below is historical planning, not a verified + theorem route. In particular, Stage 4's proposed unconditional + [preservation_l2] is not established or declared in the current tree; + retain the counterexamples as controls for any redesign. ===== Configuration ===== diff --git a/formal/Counterexample_PreservationL1.v b/formal/Counterexample_PreservationL1.v index d3cea7a0..e82052c5 100644 --- a/formal/Counterexample_PreservationL1.v +++ b/formal/Counterexample_PreservationL1.v @@ -13,10 +13,13 @@ has_type_l1 m R G e T R_final G' -> has_type_l1 m R' G e' T R_final G'. - This file exhibits a configuration that types (in BOTH modalities), - steps, and whose post-state is UNTYPABLE at the same indices — [Qed], - zero axioms. Together with [Counterexample_StepPop.v]: BOTH remaining - L1 Admitted markers were hiding falsehoods, not unfinished proofs. + This file exhibits a configuration whose pre-state types in BOTH + modalities and which steps to a post-state that is untypable in the + Linear instance at the same indices — [Qed], zero axioms. This + refutes the modality-polymorphic [preservation_l1] theorem (which + quantifies over Linear). It does not by itself refute an Affine-only + theorem. Together with [Counterexample_StepPop.v], it shows that BOTH + remaining unrestricted L1 statements are false as stated. ** The witness (value-anchored — closes the StepPop file's open door) diff --git a/formal/Counterexample_StepPop.v b/formal/Counterexample_StepPop.v index b4f84957..b550187e 100644 --- a/formal/Counterexample_StepPop.v +++ b/formal/Counterexample_StepPop.v @@ -64,8 +64,11 @@ S_StringConcat_Step2, retypes an [ELoc _ r] VALUE whose [T_Loc_L1] typing already carried [In r R]; note the witness's dangling sibling is a VARIABLE, which no [S_*_Step2] case ever - needs to retype at R', suggesting the value-anchored restriction - may be provable); + needs to retype at R'. This only suggested a restriction; it did + not prove one. The later value-anchored witness in + [Counterexample_PreservationL1.v] also refutes the restricted + [step_pop_disjoint_from_type_l1] conclusion for the + [S_StringConcat_Step2] path; that proposed escape is closed. - the choreographic route's job description changes from "derive coherence from typing" (impossible — this file) to "make coherence a judgment-level input" — the foundational thesis, diff --git a/formal/ESCALATION-4.8-leaf-rule-region-liveness.adoc b/formal/ESCALATION-4.8-leaf-rule-region-liveness.adoc index f7f6ee33..cd3d0612 100644 --- a/formal/ESCALATION-4.8-leaf-rule-region-liveness.adoc +++ b/formal/ESCALATION-4.8-leaf-rule-region-liveness.adoc @@ -1,7 +1,9 @@ == Escalation: the §4.8 leaf-rule region-liveness decision (owner call) -*Status:* OPEN — needs an owner design decision before any further L1 -preservation proof work. Raised 2026-06-16. +*Status:* HISTORICAL / SUPERSEDED — raised 2026-06-16, before the later +pinned L1 counterexamples. Its candidate closure paths are not current +proof tasks and do not justify proving the refuted unrestricted statements. +Use `+PROOF-NEEDS.adoc+` and `+EXPLAINME.adoc+` for current boundaries. ____ === ⚠️ UPDATE 2026-06-16 — path (3) *proven insufficient*; the real fork is effect typing @@ -129,8 +131,10 @@ structural induction (the missing inner-typing premise is now present at the variable/loc leaves). . `+region_shrink_preserves_typing_l1_gen_m+`’s shadowed case closes via the commutation already proved for the descend case. -. `+preservation_l1+` is re-derived as the capstone (shape drafted in -PRESERVATION-DESIGN.md §4.5). +. The historical plan proposed re-deriving `+preservation_l1+` as a +capstone (shape drafted in `+PRESERVATION-DESIGN.adoc+` §4.5); later +counterexamples refuted the unrestricted theorem, so this is not a current +proof route. Path (1) — effect-typed `+TFunEff+` lambdas — is *already in the codebase* and additionally closes the `+S_App_Step2+` case; (3) is the diff --git a/formal/L1ChoreoExperiment2.v b/formal/L1ChoreoExperiment2.v index 73c11027..42908470 100644 --- a/formal/L1ChoreoExperiment2.v +++ b/formal/L1ChoreoExperiment2.v @@ -156,18 +156,16 @@ Proof. rewrite Hneutral in Hsuf. exact Hsuf. Qed. -(** ** (B) The decisive lemma — a sibling [Use] keeps the region live. - - THIS is the obligation [step_pop_disjoint_from_type_l1] relocates to, - proved here as a pure structural fact. If the surviving sibling uses - [rv] AFTER the stepping sibling's sub-trace [t1] (the whole - [t1 ++ Use :: t2] is coherent), then the balance after [t1] is forced - [>= 1]: the stepping sibling CANNOT have closed [rv] out of scope. In - [step_pop] terms, [rv] free in the result type (the surviving - sibling's [Use]) + [rv] live before the step ([k >= 1]) gives [rv] - live AFTER the step — exactly [In rv R'] — with NO appeal to - preservation. The snapshot cannot prove this because it does not carry - the order placing the [Use] after [t1]. *) +(** ** (B) A trace-model lemma — a sibling [Use] keeps the region live. + + This proves a pure structural fact in the experiment's trace model: + if the surviving sibling uses [rv] AFTER the stepping sibling's + sub-trace [t1], then the model's balance after [t1] is [>= 1]. It is + not a proof of [step_pop_disjoint_from_type_l1]: no verified + translation from the Coq operational step and typing derivation into + this trace model is established here. Later pinned L1 counterexamples + refute the unrestricted Coq statement, so this experiment is a + research artifact, not a closure route or soundness receipt. *) Theorem sibling_use_keeps_region_live : forall t1 t2 k, valid k (t1 ++ Use :: t2) -> final_balance k t1 >= 1. diff --git a/formal/PRESERVATION-DESIGN.adoc b/formal/PRESERVATION-DESIGN.adoc index 87be39cd..f3e02f41 100644 --- a/formal/PRESERVATION-DESIGN.adoc +++ b/formal/PRESERVATION-DESIGN.adoc @@ -1,17 +1,23 @@ == Preservation: principled redesign -Companion to `+PRESERVATION-HANDOFF.md+`. The handoff document is a +Companion to `+PRESERVATION-HANDOFF.adoc+`. The handoff document is a diagnostic record of attempted proof-engineering. This document is the -*design* rationale for the typing-layer change that the verified -counterexample (`+Counterexample.v+`, all three lemmas `+Qed.+`) now -makes unavoidable. +*design* rationale for the typing-layer change made necessary by the +legacy counterexample (`+Counterexample.v+`; its three core legacy-witness +lemmas are `+Qed+`, and the file now pins five Qed lemmas total including +the separate L1 regression). The handoff’s Option 3 ("`type-system change`") is here re-cast not as a patch but as the deliberate separation of four concerns that the current calculus conflates: *structural discipline*, *region capability tracking*, *dyadic interaction semantics*, and *echo / residue -semantics*. Preservation is derived from explicit invariants in the new -architecture; it is not forced through the old. +semantics*. This document records design rationale and historical proof +plans, not an established soundness result. Later pinned regressions +(`+Counterexample_StepPop.v+`, `+Counterexample_PreservationL1.v+`, +`+Counterexample_L2.v+`, and `+Counterexample_L2_nested.v+`) refute the +unrestricted L1 statement and expose L2 β-preservation gaps. See +`+PROOF-NEEDS.adoc+` for current status; upstream theories and conceptual +vocabulary do not discharge Ephapax-local soundness obligations. ''''' @@ -203,7 +209,11 @@ Under the new rules: `+R_out = remove_first r1 [r0; r1] = [r0]+`. * Now `+EPair+`’s second sibling `+ELoc l1 r1+` must type at `+R = [r0]+`. `+T_Loc+` requires `+region_active [r0] r1+`, false. -* *The `+EPair+` rule has no derivation.* Counterexample disappears. +* *The `+EPair+` rule has no derivation.* This is a proved regression +for this exact legacy input only. It does not establish general L1 +preservation: `+Counterexample_PreservationL1.v+` later exhibits a distinct +well-typed L1 input that steps to an untypable state. See +`+PROOF-NEEDS.adoc+` for the current theorem boundary. ==== 4.5 Preservation under the new judgment @@ -229,7 +239,15 @@ admit was asking "`how do I re-type the unchanged sibling under the shrunken R’?`". Under the new threading the sibling is typed at `+R'+` from the outset — there is nothing to re-type. -==== 4.6 Cost: which existing lemmas need re-proof +==== 4.6 Cost: historical projection of proof changes + +[NOTE] +==== +The counts and proof routes in this subsection are design-era estimates, +not a report of completed proofs. In particular, the proposed preservation +proof was not established; the current unrestricted L1 statement is refuted +by later pinned counterexamples. See `+PROOF-NEEDS.adoc+`. +==== The judgment shape changes, so every lemma that pattern-matches the old shape (`+R; G |- e : T -| G'+`) must be updated. The lemma count in the @@ -261,14 +279,23 @@ subsumed by the new judgment `+R'_final+`; `+step_preserves_type+` proves the new preservation statement directly -|`+preservation+` |1 |proved by structural induction on the new judgment +|`+preservation+` |1 |would require a new proof; no result established. The current unrestricted L1 theorem was later refuted. |=== The at-pre helper pattern survives because it is orthogonal to the threading change: the pre-step env is the new `+R_in+` of the diagonal typing rule. -==== 4.7 L1 closure status (2026-05-27) +==== 4.7 L1 closure status (historical snapshot, 2026-05-27) + +[NOTE] +==== +This subsection records the intermediate L1 state at 2026-05-27. Its admit +counts, debt classifications, and proposed closure routes are superseded by +later work and pinned counterexamples. They must not be read as current +proof debt or as evidence that the unrestricted theorem can be proved; +see `+PROOF-NEEDS.adoc+` and `+EXPLAINME.adoc+`. +==== Six follow-up PRs against `+proof/l1-region-threading-design+` (the design branch) landed the L1 implementation incrementally: @@ -327,10 +354,18 @@ induction. (`+region_shrink_preserves_typing_l1_gen+` and `+preservation_l1+`) — each closes the moment its internal admits close. -==== 4.8 Soundness finding: T_Lam_L1 + T_Var_*_L1 are too permissive +==== 4.8 Historical soundness diagnosis (incomplete): L1 rules and region presence + +[NOTE] +==== +This 2026-05 diagnosis predates `+Counterexample_StepPop.v+` and +`+Counterexample_PreservationL1.v+`. It is not a complete account of the +refuted theorem, and the resolution paths below are design ideas, not +proved repairs. Preserve the later regressions as authoritative controls. +==== -L1.E surfaced a genuine soundness issue, separate from the proof- -engineering gaps: +L1.E surfaced a soundness issue, originally described as separate from the +proof-engineering gaps: *The finding.* `+T_Lam_L1+` rigidly fixes the lambda body’s region environment `+R+` at lambda-creation time, with no mechanism to retype @@ -435,8 +470,9 @@ linear bindings |optional; produces an Affine-echo residue (see §6) [width="100%",cols="34%,33%,33%",options="header",] |=== |Property |Ephapax-Linear |Ephapax-Affine -|Preservation |✓ (L1 fix) |✓ (same fix; Affine derivations are L1-safe -by weakening) +|Preservation |✗ current modality-polymorphic L1 statement is refuted +by the Linear instance in `+Counterexample_PreservationL1.v+` |No separate +Affine-only preservation theorem is established or claimed by this witness |Progress |✓ |✓ @@ -582,13 +618,15 @@ change. === 8. Proof-need separation: Linear vs Affine +The following table is a list of target properties, not established +proofs. Current preservation status is recorded in `+PROOF-NEEDS.adoc+`. Where the layers’ proof needs differ: [width="100%",cols="34%,33%,33%",options="header",] |=== |Property |Ephapax-Linear |Ephapax-Affine -|*Preservation* (L1) |identical statement; proof via L1 threading -|identical statement; follows from Linear via modality-weakening +|*Preservation* (L1) |Current unrestricted statement is refuted; redesign/replacement theorem is open +|No separate Affine-only preservation theorem is established; the L1 counterexample is Linear and does not alone refute an Affine-only claim |*Progress* |values + closed contexts step |values + closed contexts step; affine "`ambient drop`" rule may fire @@ -622,10 +660,11 @@ genuinely split. === 9. Counterexample examination, revisited -The verified counterexample (`+Counterexample.v+`) was a _single_ -witness. The L1 architectural fix subsumes a family of related -configurations, all sharing the same shape. Cataloguing them sharpens -the design: +The legacy counterexample (`+Counterexample.v+`) is one pinned +witness, and `+bad_input_untypable_l1+` rejects that particular input. +This does not show that L1 subsumes the related configurations below: +later counterexamples refute unrestricted L1 preservation. The family +table is historical design analysis, not evidence of a general fix. [width="100%",cols="34%,33%,33%",options="header",] |=== @@ -671,18 +710,20 @@ require `+r ∈ R_in+`, but `+r ∉ R_in+` by `+T_Region+`’s premise — so this is well-typedness, not preservation, and the existing rules already reject it. -This confirms the diagnosis: *the asymmetry is region _exit_, not region -introduction*. L1’s left-to-right threading is the exactly- sufficient -mechanism. +This was the original diagnosis, not a proof that L1 threading enforces +sibling safety. The pinned L1 counterexamples show that the unrestricted +judgment still permits preservation failures; a sound replacement needs +additional, explicitly checked invariants. ''''' === 10. Implementation order [arabic] -. *L1 — region threading* (this design). Closes preservation. Days, not -weeks. The hard part is re-stating ~80 lemmas; the substance of each is -unchanged. +. *L1 — region threading* (this design). This was expected to support +preservation, but the unrestricted L1 theorem was later refuted by pinned +counterexamples. A sound judgment/step redesign and replacement proof are +still required; the old schedule estimate is not current. . *L2 — modality parameter* (already present _in_ the types via `+is_linear_ty+`; needs to be _promoted_ to a judgment parameter plus the Linear ⇒ Affine weakening). Orthogonal to L1; can be done before or @@ -693,10 +734,10 @@ preservation, progress, or the dyadic story). Bring in echo-types’ via decoration-commuting. . *L4 — module-level mode declaration* (UX, not proof). -Each step’s correctness is independent of the next. The decoration- -commuting recipe from echo-types (`+composition.md+` §Q5) guarantees -that adding L3 to a system that already has L1+L2 does not invalidate -any L1/L2 proof. +The design hoped for independent layer proofs. The decoration-commuting +recipe from echo-types (`+composition.md+` §Q5) is a conceptual +construction, not a proof that adding L3 preserves Ephapax's L1/L2 +properties; those local obligations must be proved against Ephapax rules. ''''' @@ -704,7 +745,7 @@ any L1/L2 proof. * The verified counterexample: `+formal/Counterexample.v+` (this repo). * The diagnostic record of attempted patches: -`+formal/PRESERVATION-HANDOFF.md+`. +`+formal/PRESERVATION-HANDOFF.adoc+`. * Echo definition: `+~/developer/repos/echo-types/proofs/agda/Echo.agda+` (line 14). * Echo residue + non-recovery: @@ -733,37 +774,38 @@ interesting story is the layering itself. This section catalogues the documents that frame "`what ephapax is`" and specifies the substantive edits required, with draft text where the framing matters. -The rollout deliberately leaves implementation untouched. Documentation -that promises the new architecture without it being built would be -dishonest; documentation that describes the *direction* alongside the -current state is a roadmap. The text below is the roadmap form. +The rollout deliberately leaves implementation untouched. This section +is an archival 2026-05 documentation plan: its draft quotations and +checklists are not current claims and must not be copied as evidence. Some +were superseded by later counterexamples and policy updates. Current proof +status is in `+PROOF-NEEDS.adoc+` and the ledger in `+EXPLAINME.adoc+`. ==== 12.1 Tagline and one-line description (used by many surfaces) The current GitHub repo description is: ____ -Dyadic linear+affine type system for compile-time WASM memory safety — -no use-after-free, no leaks, region-based allocation. Mechanically -proved in Coq and Idris2. +Research language exploring dyadic linear/affine typing and region-based +allocation for WebAssembly. Coq and Idris2 artifacts do not establish +whole-language memory safety or implementation refinement. ____ Proposed replacement (matches the four-layer story without overclaiming unbuilt layers): ____ -A dyadic programming language for WebAssembly, where four orthogonal -disciplines — structural (linear ↔ affine), region capabilities, -irreversibility residue, and dyadic interaction mode — compose to -guarantee compile-time memory safety without a garbage collector. -Mechanically formalised in Coq and Idris2. +A research language for WebAssembly exploring four design concerns — +structural modality, region capabilities, irreversibility residue, and +dyadic interaction. Formal artifacts exist in Coq and Idris2, but the +current preservation counterexamples mean no whole-language memory-safety +guarantee is established. ____ Short form (≤ 130 chars, for cards and `+site:+` listings): ____ -Ephapax: four-layer dyadic type system for WASM memory safety — -linearity, regions, echo residue, dyadic mode. Coq + Idris2 proofs. +Ephapax: research language exploring linear/affine typing, regions, +echo residue, and dyadic mode; Coq and Idris2 proof artifacts. ____ Lift this string verbatim into: @@ -802,7 +844,9 @@ the recipe). | **L1 — Region capabilities** | Every live region is tracked in an input/output environment threaded through every expression. A region cannot be referenced - after a sibling has exited it. Soundness proof in `formal/`. + after a sibling has exited it. This is the design goal; a general + soundness proof is not established, and current L1 counterexamples + refute the unrestricted preservation claim. | **L2 — Structural discipline (linear ↔ affine)** | The *modality* of the surrounding program decides whether linear @@ -835,11 +879,11 @@ ____ . *Replace "`Region-based memory`" row* with the L1 framing: + ____ -*Region-based memory (L1)* | Allocations live in named regions -(`+region r: ...+`). The type system threads a region-capability -environment through every expression so a sibling cannot read from a -region another sibling has just exited. When a region’s scope ends, the -runtime bulk-frees every resource in it. +*Region-based memory (L1)* | Allocations are designed around named regions +(`+region r: ...+`). The judgment threads a region-capability environment, +but unrestricted L1 preservation is refuted by pinned counterexamples; +sibling safety remains a design target, not an established guarantee. +The Rust runtime's region behavior is not proved to refine the calculus. ____ . *Add a footnote-style block* linking to this design document for readers who want the soundness story: @@ -851,9 +895,10 @@ readers who want the soundness story: The four-layer separation is **not** decorative — it exists because the original "linear+affine + regions" framing admitted a verified counterexample to preservation (see -`formal/Counterexample.v` and `formal/PRESERVATION-DESIGN.md`). -The four-layer redesign restores soundness by making each -discipline's invariants explicit and orthogonal. +`formal/Counterexample.v` and `formal/PRESERVATION-DESIGN.adoc`). +The four-layer redesign makes proposed disciplines explicit, but it does +not by itself restore soundness. Current L1 preservation is refuted and +unconditional L2 preservation is not established. **** ---- . *Do not* change the disambiguation block (lines 19–41). It is correct @@ -868,11 +913,11 @@ two new claims and weaken one: * *New (L1)*: "`The region capability environment is threaded through every compound expression.`" Evidence pointer: cite -`+formal/PRESERVATION-DESIGN.md §4+` and `+formal/Counterexample.v+` +`+formal/PRESERVATION-DESIGN.adoc §4+` and `+formal/Counterexample.v+` (until the Coq side is implemented, the evidence is the *design doc + counterexample*, not a passing proof — say so honestly). * *New (L3, planned)*: "`Irreversible operations produce residue -witnesses.`" Evidence pointer: `+formal/PRESERVATION-DESIGN.md §6+` and +witnesses.`" Evidence pointer: `+formal/PRESERVATION-DESIGN.adoc §6+` and the upstream echo-types proofs at `+~/developer/repos/echo-types/proofs/agda/EchoLinear.agda+`. Mark as *planned* until ephapax has its own `+formal/Echo.v+`. @@ -887,12 +932,14 @@ Add a new top-level section after "`Claim: Region-Based Memory`": == Claim: Sibling-safe region capabilities (L1) *Evidence*: Region capabilities are threaded as input/output -environments through every compound typing rule. A sibling cannot -reference a region a previous sibling has exited. - -* Counterexample at `formal/Counterexample.v` (all three lemmas - `Qed`) demonstrates the soundness gap the threading fixes. -* Design rationale at `formal/PRESERVATION-DESIGN.md §3-§4`. +environments through compound typing rules. This is not sufficient for +general preservation: the pinned L1 counterexamples refute the unrestricted +claim. The legacy regression rejects one specific input only. + +* The three core legacy-witness lemmas in `formal/Counterexample.v` + are `Qed`; the file pins five Qed lemmas total. They refute the legacy + statement and do not establish general L1 preservation. +* Design rationale at `formal/PRESERVATION-DESIGN.adoc §3-§4`. * Reference implementation: forthcoming — see `ROADMAP.adoc` for the order in which L1 lands in `formal/` and in `src/ephapax-typing/`. @@ -908,7 +955,7 @@ Affine mode permits silent lowering. * Upstream theory at `~/developer/repos/echo-types/proofs/agda/EchoLinear.agda` (lines 30–101), already mechanised. -* Forward-looking design at `formal/PRESERVATION-DESIGN.md §6`. +* Forward-looking design at `formal/PRESERVATION-DESIGN.adoc §6`. * Status: **planned** — no ephapax rule yet introduces `TEcho`. The L3 extension follows L1. ---- @@ -956,12 +1003,11 @@ each takes its **defaults** from which side of the dyad you are on. program has one. |=== -The four layers compose without coherence obligations because each -is a *thin poset* — propositional ordering kills the categorical -overhead that would otherwise demand pentagon laws and the like. The -construction is taken verbatim from -https://github.com/hyperpolymath/echo-types[echo-types]' -decoration-commuting recipe. +The design intends the four concerns to compose through a *thin-poset* +structure, reducing categorical coherence overhead. This architectural +argument is not an Ephapax soundness theorem. The construction is inspired +by the `+echo-types+` decoration-commuting development; upstream results do +not discharge Ephapax-local obligations. The dyad remains primary. The layers are how the dyad's promises are *enforced*. @@ -1010,7 +1056,7 @@ orthogonal layers; each is implemented in sequence. - No proof obligations. The previous "Preservation closure plan" section is **archived** — -see `formal/PRESERVATION-HANDOFF.md` for the historical record. +see `formal/PRESERVATION-HANDOFF.adoc` for the historical record. ---- ==== 12.6 spec/SPEC.md and spec/ephapax-spec.md — the canonical spec @@ -1045,7 +1091,7 @@ grammars. Add a banner at the top: > (Linear and Affine). The two are not different languages — they > are two admissible-derivation regimes over the same syntax and > semantics. See `docs/vision/EPHAPAX-VISION.adoc` for the dyad, -> and `formal/PRESERVATION-DESIGN.md §5` for the L2 layer. +> and `formal/PRESERVATION-DESIGN.adoc §5` for the L2 layer. ---- Update the comparison table title from "`Dual Substructural Grammars`" @@ -1071,7 +1117,7 @@ which layer a question touches is the first step in answering it: | L4 — Dyadic mode | "Is this a project-level mode declaration question?" | Most questions touch exactly one layer. The design rationale is in -`formal/PRESERVATION-DESIGN.md`. The verified counterexample that +`formal/PRESERVATION-DESIGN.adoc`. The verified counterexample that forced the redesign is in `formal/Counterexample.v`. Standing rule: if a proposed change appears to require a side @@ -1088,7 +1134,7 @@ that side condition *derivable*, not stated. ### Architecture -- **Four-layer typing redesign** (`formal/PRESERVATION-DESIGN.md`). +- **Four-layer typing redesign** (`formal/PRESERVATION-DESIGN.adoc`). The original "linear+affine + regions" framing admitted a verified counterexample to preservation (`formal/Counterexample.v`). The redesign separates four orthogonal disciplines: region capabilities @@ -1098,13 +1144,14 @@ that side condition *derivable*, not stated. ### Proof / theory -- Verified counterexample to preservation in the current rules - (`formal/Counterexample.v` — three lemmas `Qed`). The - counterexample is the canonical regression test for the L1 fix. +- Verified legacy preservation counterexample + (`formal/Counterexample.v`; see file for the pinned five-Qed inventory). + `bad_input_untypable_l1` rejects that particular input only; later L1 + regressions refute the unrestricted L1 preservation statement too. ### Docs -- New design document: `formal/PRESERVATION-DESIGN.md`. +- New design document: `formal/PRESERVATION-DESIGN.adoc`. - README, EXPLAINME, EPHAPAX-VISION, ROADMAP, CLAUDE updated to reflect the four-layer story. - Repo description and tagline updated. @@ -1121,18 +1168,23 @@ hero block: ---- # Ephapax -> Four-layer dyadic type system for WebAssembly memory safety. +> Research language exploring dyadic linear/affine typing and region-based +> memory management for WebAssembly. -Four orthogonal disciplines compose to guarantee compile-time -memory safety without a garbage collector: +The four layers are design concerns, not a soundness proof. Current +Coq counterexamples refute legacy and unrestricted L1 preservation; no +unconditional L2 preservation theorem is established. Selected L3 results +are scoped to matching echo-emitting rule pairs, and L4 is a scaffold. -- **Regions** (L1) — capabilities threaded through every expression. -- **Linear ↔ Affine** (L2) — the dyad, mother and child. -- **Echo** (L3, planned) — irreversibility leaves typed residue. -- **Dyadic mode** (L4) — declare which side you speak from. +- **Regions** (L1) — input/output capability threading; general preservation + remains an open redesign obligation. +- **Linear ↔ Affine** (L2) — modality and weakening artifacts; no unconditional + L2 preservation theorem. +- **Echo** (L3) — typed residue with scoped matching-rule results. +- **Dyadic mode** (L4) — declarations/design scaffold. Mechanically formalised in Coq and Idris2. See -[design](formal/PRESERVATION-DESIGN.md) · +[design](formal/PRESERVATION-DESIGN.adoc) · [vision](docs/vision/EPHAPAX-VISION.adoc) · [spec](spec/SPEC.md) · [roadmap](ROADMAP.adoc). @@ -1222,7 +1274,7 @@ upstream. Mark as "`planned`" prominently. fits. |`+Soundness+` |Index of what is proved, where, and at what status. -Cross-references `+formal/PRESERVATION-DESIGN.md+` and +Cross-references `+formal/PRESERVATION-DESIGN.adoc+` and `+Counterexample.v+`. |`+FAQ+` |Includes the disambiguation against AffineScript, the @@ -1236,30 +1288,27 @@ mode, thin-poset decoration. Wiki updates should happen *after* the repo-side docs land, so the wiki can link to merged sources rather than to in-flight files. -==== 12.14 Cross-cutting: language for new framing (drop-ins) - -These passages are written once and dropped wherever needed: - -*One-sentence what-this-is*: > Ephapax is a dyadic programming language -whose type system composes > four orthogonal disciplines — region -capabilities, structural > modality, irreversibility residue, and dyadic -mode — to guarantee > compile-time WebAssembly memory safety without a -garbage collector. - -*One-paragraph what-this-is*: > Ephapax is a programming language for -WebAssembly with a > mechanically verified type system. Four orthogonal -disciplines > compose to give the safety guarantees: *region -capabilities* (L1) > thread an explicit live-region set through every -expression so a > sibling cannot reference a region another sibling has -exited; > *structural modality* (L2) chooses between Linear (every -linear > binding must be consumed) and Affine (linear bindings may be > -dropped); *irreversibility residue* (L3, planned) makes the > -information lost by region exit and drop into a first-class, > -proof-relevant value; and *dyadic mode* (L4) declares, at the > project -level, which side of the linear/affine dyad the program > speaks from. -The four layers compose without coherence obligations > because each is -a thin-poset decoration, a construction borrowed > verbatim from the -`+echo-types+` mechanisation. +==== 12.14 Cross-cutting: qualified project framing (not a guarantee template) + +The following replaces the historical marketing-style framing. Use it +only with the explicit proof boundary below: + +*One-sentence*: Ephapax is a research language exploring region +capabilities, linear/affine modalities, irreversibility evidence, and +dyadic interaction for compile-time WebAssembly memory safety. + +*One-paragraph*: Ephapax is a research language for WebAssembly whose +type-system design explores four concerns: region capabilities (L1), +structural modality (L2), irreversibility residue (L3), and dyadic mode +(L4). The L1 judgment threads region environments, but later Coq +counterexamples refute unrestricted L1 preservation; no unconditional +L2 preservation theorem is established. The L2 β-case lemmas are +conditional, L3 preservation results are Qed only for matching +echo-emitting rule pairs, and L4 remains a definitions-only scaffold. +The architecture is design rationale, not a soundness proof. The Coq +artifacts do not prove the Rust implementation refines the calculus. +Do not infer Ephapax-specific guarantees from `+echo-types+` or other +upstream developments. *Why four layers (FAQ-shaped)*: > Q: Why four layers, not three or five? > > A: The four are what the soundness story demands. L1 is forced by > @@ -1291,93 +1340,103 @@ or by an agent. The architecture above describes the *target*; this subsection describes the *current state*, which is much narrower than the target. -===== 12.15.1 What is mechanised today +===== 12.15.1 Current proof inventory (summary) + +This table is an orientation only; exact propositions, checker +information, and trust boundaries are in the EXPLAINME proof ledger. [width="100%",cols="34%,33%,33%",options="header",] |=== -|Mechanisation |Scope |Status -|`+formal/Semantics.v+`, `+formal/Typing.v+`, `+formal/Syntax.v+` (Coq) -|A *single* typing judgment `+R; G ⊢ e : T -| G'+` and its small-step -operational semantics |Builds with `+coqc 8.18.0+` - -|`+formal/Counterexample.v+` |A verified counterexample to preservation -*as currently stated* |All three lemmas `+Qed+` - -|`+preservation+` theorem in `+Semantics.v+` |Soundness under the -current single judgment |*`+Admitted.+`* — 11 cascading goals open (see -`+PRESERVATION-HANDOFF.md+`) - -|`+src/abi/Ephapax/…/*.idr+` (Idris2) |Selected structural-safety claims -|Per file; see `+idris2 --check+` +|Artifact |Scope |Current status +|`+formal/Counterexample.v+` (Coq) +|Legacy preservation witness and separate L1 regression +|Five Qed lemmas total. The three core legacy-witness lemmas refute the +legacy theorem; `+bad_input_untypable_l1+` rejects only that input. + +|`+formal/Semantics.v+` (Coq) +|Legacy `+preservation+` +|False as stated; durable `+Admitted.+` retained. Not ordinary debt. + +|`+formal/TypingL1.v+`, `+Semantics_L1.v+` (Coq) +|Modality-indexed L1 judgment, structural helpers, L1 preservation claims +|The unrestricted `+step_pop_disjoint_from_type_l1+` and +`+preservation_l1+` statements are refuted; two outer `+Admitted.+` +markers are retained. Restricted helper results are not general +preservation. + +|`+formal/TypingL2.v+`, `+Counterexample_L2*.v+` (Coq) +|L2 β-case helpers and two distinct witnesses +|Conditional helpers only; no unconditional `+preservation_l2+` theorem +is declared. + +|`+formal/Echo.v+`, scoped L3 lemmas (Coq) +|Echo/residue calculus and matching rule-pair cases +|Selected Qed results only; no general L1/L2 preservation. + +|Mathesis Grade 3 status +|Agda local proof, no independent translation +|No Grade 3 receipt recorded. Existing Coq Qed results are not Grade 3. |=== -===== 12.15.2 What the single judgment *is not* - -The current `+has_type+` judgment *does not distinguish* Linear from -Affine ephapax. It is a single typing relation, parameterised over a -linearity context `+G+` whose entries carry a `+(ty, bool)+` consumption -flag. `+is_linear_ty+` returns a per-type tag. There is *no judgment -parameter* for L2 modality; there is *no proof* that Linear derivations -form a subset of Affine derivations; there is *no mechanised -ephapax-affine type system* at all. - -Concretely: the Rust crate `+ephapax-linear/+` contains a -`+LinearChecker+` and an `+AffineChecker+`, with EBNF grammars and -behavioural tests proving they diverge on identical programs. That is -the implementation side of the dyad. The *proofs side* has not caught -up: the Coq + Idris2 formalisation models _one_ judgment, which -behaviourally resembles the linear discipline (it requires linear-typed -bindings to be consumed) but is not labelled as such and has no proven -dual. - -===== 12.15.3 What this redesign *will* establish - -If executed as designed, the redesign closes: - -* *L1 — region capabilities*: a new threading discipline + a reproof of -preservation under the new rules. This is the central deliverable. The -verified counterexample becomes a passing regression. -* *L2 promotion*: the judgment gains an `+ℓ ∈ {Linear, Affine}+` -parameter, and a `+weaken_modality : Linear ⇒ Affine+` lemma. This is -what _introduces_ a mechanised ephapax-affine into the formal -development for the first time. - -===== 12.15.4 What this redesign *will not* establish - -Equally explicitly — so future sessions, agents, and PR reviewers do not -assume otherwise: - -* *The ephapax-affine type proofs are not done today, and the L1 -redesign on its own does not finish them.* L1 closes preservation under -the _single_ judgment that already exists. L2’s modality-weakening -lemma, once proved, will lift L1’s preservation to the affine side — but -that lift is a _separate_ lemma that has not been written and is not -part of the L1 patch. Until L2 lands _and_ the weakening lemma is -`+Qed+`, *no ephapax-affine soundness property is mechanised*. -* *No L3 (Echo / residue) proof obligation is closed.* L3 is -forward-looking. Until `+formal/Echo.v+` exists and references it from -the operational semantics, the Linear-echo "`mandatory observation`" -property and the Affine-echo "`non-duplicable residue`" property are -_aspirations_, not theorems. -* *No proof that the Rust `+AffineChecker+` agrees with any mechanised -affine judgment.* The implementation-side dual exists; the -mechanisation-side dual does not. Cross-checking the two is a third, -independent body of work. -* *No proof of the L4 mode declaration’s consistency* (e.g., that a -program declared Linear cannot accidentally invoke an Affine- typed -library through a hole in mode-elaboration). L4 is a UX layer in this -design; making it sound requires further work that is not scoped here. +No fresh Coq build was run in this editing environment (`+coqc+` is +unavailable); the current CI run did not execute the Coq job. The proof +ledger records that limitation explicitly. + +===== 12.15.2 What current artifacts do not establish + +The `+has_type_l1+` judgment is modality-indexed, and +`+linear_to_affine+` is Qed with zero axioms. These results do not imply +L1 or L2 preservation. In particular, the unrestricted L1 statements +are refuted, no unconditional L2 preservation theorem is declared, and +no separate Affine-only preservation theorem is established (the Linear +counterexample does not alone refute such a theorem). + +The Rust crate contains `+LinearChecker+` and `+AffineChecker+`, but no +proof shows that either checker or the compiler refines the Coq/Idris2 +calculus. Coq evidence is not an Agda Grade 3 receipt. For the +Mathesis/Standards grading boundary and exact checker status, see +`+PROOF-NEEDS.adoc+` and the EXPLAINME proof ledger. + +===== 12.15.3 Intended outcomes versus current evidence + +This subsection describes the earlier redesign target, not achieved +results. The current evidence is narrower: + +* *L1 — region capabilities*: the judgment and helpers exist, but + unrestricted `+step_pop_disjoint_from_type_l1+` and + `+preservation_l1+` are refuted as stated. A sound replacement theorem + remains open; the legacy-input regression is only a specific control. +* *L2 promotion*: modality indexing and `+linear_to_affine+` are + mechanised, but no unconditional `+preservation_l2+` theorem is + declared. β-case lemmas are conditional, and the two L2 witnesses + document distinct gaps. + +===== 12.15.4 Other proof boundaries + +* *Affine soundness*: the L1 counterexample refutes the modality- + polymorphic theorem through its Linear instance; it does not alone + refute an Affine-only theorem. No Affine-only preservation theorem or + implementation refinement is established. +* *L3 (Echo / residue)*: selected Qed results cover matching + echo-emitting typing/step rule pairs only. They do not establish + general L1/L2 preservation or end-to-end language soundness. +* *Rust implementation*: the Coq/Idris2 artifacts do not prove that the + Rust `+AffineChecker+` or compiler refines the formal calculus. +* *L4 mode declaration*: `+formal/L4.v+` is a definitions-only + scaffold; there is no mode-consistency preservation theorem. ===== 12.15.5 The honest one-line summary ____ -*Ephapax’s mechanised soundness story today is: one judgment, resembling -linear discipline, with preservation `+Admitted+`. The verified -counterexample shows preservation false as stated. The L1 redesign in -this document closes that counterexample. Ephapax- affine proofs as a -distinct mechanised body of theorems are not done, will not be done by -L1 alone, and will require L2 plus a follow-up weakening lemma before -any "`ephapax-affine is sound`" claim is honest.* +*Ephapax’s mechanised soundness story is bounded: the legacy preservation +statement is refuted and remains `+Admitted+`; the current unrestricted L1 +preservation statement is also refuted (`+Counterexample_PreservationL1.v+`), +and no unconditional L2 preservation theorem is established. The L1 +judgment rejects the specific legacy witness, but that regression is not a +soundness theorem. The Qed L2 β-case helpers have explicit preconditions; +the L2 counterexamples document gaps outside those restricted cases. +Ephapax-affine soundness is not established by the L1/L2 vocabulary or by +proofs in another repository.* ____ Cite this subsection by section number (`+§12.15+`) whenever the @@ -1419,9 +1478,10 @@ itself a research question. *Why this is staged separately from B:* [arabic] -. *B closes preservation in weeks; A is months.* Preservation is -currently `+Admitted+` with a verified counterexample. Closing it is -more urgent than v2 architectural exploration. +. *B was initially estimated as weeks; that estimate is obsolete.* +The legacy theorem is false, and later L1 counterexamples showed the +redesign also needs further work. The replacement proof boundary remains +open; v2 architectural exploration is a separate research track. . *B and A are not mutually exclusive.* Once B lands, A can be developed as a parallel branch using B’s primitives. The L3 echo layer in B is a _prerequisite_ for A’s foundation rewrite — nothing wasted. @@ -1471,7 +1531,7 @@ Add to `+ROADMAP.adoc+` under "`Future research tracks`": ---- === Echo as operational foundation (v2) -The four-layer redesign (`formal/PRESERVATION-DESIGN.md`) treats Echo +The four-layer redesign (`formal/PRESERVATION-DESIGN.adoc`) treats Echo as a residue layer (L3) over regions. A coherent v2 research direction makes Echo the *foundation* itself: `ERelease` as a primitive operation, regions desugared to sequenced releases, Linear-mode @@ -1479,7 +1539,7 @@ discharge as a termination invariant. **Not scheduled.** This is a months-long research effort, staged after the L1+L2+L3 layer-redesign lands. See -`formal/PRESERVATION-DESIGN.md §12.16` for the seed; an +`formal/PRESERVATION-DESIGN.adoc §12.16` for the seed; an `ECHO-AS-FOUNDATION.md` design doc will be opened when the work begins. ---- @@ -1490,7 +1550,7 @@ The user has not asked for these edits to be made yet. Execution order, when they are: [arabic] -. Land `+formal/PRESERVATION-DESIGN.md+` (this document). +. Land `+formal/PRESERVATION-DESIGN.adoc+` (this document). . Update README + EXPLAINME + EPHAPAX-VISION in one PR ("`docs: introduce four-layer framing`"). . Update ROADMAP + CHANGELOG in one PR ("`docs: roadmap reflects diff --git a/formal/PRESERVATION-HANDOFF.adoc b/formal/PRESERVATION-HANDOFF.adoc index e3908eb0..6f615e99 100644 --- a/formal/PRESERVATION-HANDOFF.adoc +++ b/formal/PRESERVATION-HANDOFF.adoc @@ -19,29 +19,29 @@ the 12 → 0 reduction story. - Extending the legacy `+Semantics.v+` with new lemmas to support any of the above (`+step_preserves_type_at_pre+`, `+step_output_context_eq_at_pre+`, etc. are all in this class). -The canonical design for the fix is the *four-layer redesign* in -`+formal/PRESERVATION-DESIGN.md+`. Preservation is re-derived per-layer -(`+preservation_l1+` in `+Semantics_L1.v+`, etc.), not closed against -the legacy judgment. The owner directive (2026-05-27) is in -`+CLAUDE.md+` at the repo root. +The four-layer architecture in `+formal/PRESERVATION-DESIGN.adoc+` is +design history, not an established fix. Later pinned counterexamples +refute unrestricted L1 preservation, and no unconditional L2 theorem is +established. Do not describe preservation as re-derived per layer. The +current boundary and policies are in `+PROOF-NEEDS.adoc+`, +`+EXPLAINME.adoc+`, and `+CLAUDE.md+`. This file is retained so the per-case diagnostic data (which congruence patterns hit which obstacle, etc.) remains available to inform the layered design — but reading it as a closure plan is the trap. ____ -Diagnostic + remediation log. The proof is still `+Admitted.+`, but as -of *2026-05-21* it’s *down from 910 open goals to 12* via four landed -PRs. This file tells whoever picks it up next exactly what’s open and -what the canonical closure path is. +Diagnostic + remediation log, frozen as historical closure-attempt +material. Its 2026-05-21 count (910 open goals to 12) is not current +proof status. The four-layer document records design rationale, not a +canonical closure path; later L1 counterexamples also refute unrestricted +redesign statements. Use `+PROOF-NEEDS.adoc+` and `+EXPLAINME.adoc+` for +current boundaries. This file remains useful only as per-case archaeology. ____ -*The canonical closure plan is now in `+formal/PRESERVATION-DESIGN.md+`* -(four-layer redesign; L1 region capability threading). The prior -"`Preservation closure plan`" in `+ROADMAP.adoc+` is superseded; this -file remains as the per-case diagnostic record. Read the design doc -first; come back here for case detail and the historical closure-attempt -log. +*Do not follow the closure plans in this file or infer a proof route from +the design history.* The legacy theorem is false as stated, and the +unrestricted L1 theorem is separately refuted. ____ === State at a glance diff --git a/formal/PROOF-STATUS.a2ml b/formal/PROOF-STATUS.a2ml index 669779ba..d9fbbb53 100644 --- a/formal/PROOF-STATUS.a2ml +++ b/formal/PROOF-STATUS.a2ml @@ -4,19 +4,30 @@ # # PROOF-STATUS.a2ml — machine-readable Coq proof state # -# Snapshot of formal/*.v as of 2026-05-27 (post-L1.A through L1.F). -# Consumed by automated proof-debt trackers, status dashboards, and -# CI gates that need to know "what counts as proven here". +# Historical schema snapshot from 2026-05-27 (post-L1.A through L1.F). +# Its legacy counts and classifications below are superseded by the +# current boundary block and PROOF-NEEDS.adoc. Do not consume historical +# L1 debt rows as open obligations without checking pinned counterexamples. # -# Human-readable companion: formal/PRESERVATION-DESIGN.md §4.7 and §4.8. +# Human-readable source of truth: PROOF-NEEDS.adoc and EXPLAINME.adoc. [metadata] version = "1.0.0" snapshot-date = "2026-05-27" design-branch = "proof/l1-region-threading-design" -spec-doc = "formal/PRESERVATION-DESIGN.md" +spec-doc = "formal/PRESERVATION-DESIGN.adoc" counterexample = "formal/Counterexample.v" +[current-proof-boundary] +status-date = "2026-11-01" +source-of-truth = "PROOF-NEEDS.adoc" +legacy-preservation = "refuted-as-stated; durable Admitted retained; five-Qed regression pinned" +step-pop-disjoint-from-type-l1 = "refuted-as-stated; Counterexample_StepPop.v" +preservation-l1 = "refuted-as-stated in Linear instance; Counterexample_PreservationL1.v" +preservation-l2 = "no unconditional theorem declared; see Counterexample_L2.v and Counterexample_L2_nested.v" +mathesis-grade = "not-claimed; current witnesses are Coq, not Grade 3 Agda receipts" +proof-policy = "hyperpolymath/mathesis/estate-mathematical-architecture; hyperpolymath/standards/3-practice/PROOF-POLICY.adoc" + # ============================================================================ # FILES — what's in formal/ and its proof-status posture # ============================================================================ @@ -56,17 +67,18 @@ key-lemmas = [ [[files]] path = "formal/Semantics.v" purpose = "operational step + legacy preservation" -status = "frozen-with-1-residual" +status = "frozen-refuted" admit-count = 1 -note = "Legacy preservation has 1 residual admit (S_Region_Step + T_Region_Active region weakening). Out of scope for L1 redesign." +note = "The legacy preservation statement is false as stated; its durable Admitted is pinned by the five-Qed formal/Counterexample.v regression. Do not treat as ordinary debt." [[files]] path = "formal/Semantics_L1.v" -purpose = "L1 preservation theorem + helpers" -status = "active" -admit-count = 4 -axiom-count = 1 +purpose = "L1 helper lemmas, false unrestricted theorem statements, and scoped regressions" +status = "active-with-refuted-preservation-statements" +admit-count = 2 +axiom-count = 0 admitted-lemma-count = 2 +note = "Current two outer Admitted lemmas are refuted as stated by Counterexample_StepPop.v and Counterexample_PreservationL1.v; replacements require redesign, not proof completion." landed-in = ["PR-157", "PR-158", "PR-159", "PR-160", "PR-161", "PR-162", "PR-163"] # ============================================================================ @@ -90,8 +102,8 @@ name = "region_shrink_preserves_typing_l1" file = "Semantics_L1.v" landed-in = "PR-159" swarm-stream = "L1.B" -purpose = "shrink region env for value typings (wraps _gen)" -depends-on-admitted = ["region_shrink_preserves_typing_l1_gen"] +purpose = "value-restricted region shrinking via region_shrink_msperm" +note = "The unrestricted general statement was refuted in Counterexample_RegionShrink.v; this Qed value corollary is the restricted replacement." [[qed-lemmas]] name = "subst_preserves_typing_l1" @@ -131,11 +143,11 @@ purpose = "corollary: In r R' implies In r R" file = "Semantics_L1.v" landed-in = "PR-161" swarm-stream = "L1.D" -status = "Admitted" +status = "Admitted; refuted-as-stated" cases-total = 33 cases-qed = 29 cases-admit = 4 -note = "All Qed cases use the four Qed helpers above. The 4 admits all surface a single structural class (see [proof-debt] below)." +note = "The theorem statement is refuted by Counterexample_PreservationL1.v (Linear instance). Case counts are historical; do not treat residual admits as unfinished routine proof debt." # ============================================================================ # OUTSTANDING PROOF DEBT @@ -144,57 +156,57 @@ note = "All Qed cases use the four Qed helpers above. The 4 admits all surface a [[proof-debt]] id = "L1.B-residual-1" file = "Semantics_L1.v" -line-anchor = "region_shrink_preserves_typing_l1_gen T_Region_Active_L1 shadowed" -class = "list-vs-multiset" -tractable = true -diagnosis = "set-equality bridges don't preserve remove_first_L1 output because the operation is positional, not set-theoretic" -closes-when = "redesign remove_first_L1 as a multiset operation, OR prove a position-aware bridge" +line-anchor = "historical region_shrink_preserves_typing_l1_gen T_Region_Active_L1 shadowed" +class = "counterexample-refuted-statement" +tractable = false +diagnosis = "The unrestricted helper is refuted by Counterexample_RegionShrink.v; duplicate ambient region entries make single-entry removal unsound even under strict syntactic freeness." +closes-when = "Do not prove the old statement. Restricted region_shrink_msperm and value/neutral corollaries replace it for current call sites." [[proof-debt]] id = "L1.D-StringConcat" file = "Semantics_L1.v" -line-anchor = "preservation_l1 S_StringConcat_Step2" -class = "operationally-sound-needs-supporting-lemma" -tractable = true -diagnosis = "value v1 left, e2 steps right. Need step_pop_disjoint_from_type_l1 lemma (operational claim: a step's R-pop doesn't pop a region appearing in any sibling's free regions)" -closes-when = "prove step_pop_disjoint_from_type_l1" +line-anchor = "historical preservation_l1 S_StringConcat_Step2 support claim" +class = "counterexample-refuted-statement" +tractable = false +diagnosis = "The unrestricted helper step_pop_disjoint_from_type_l1 is refuted by Counterexample_StepPop.v; Counterexample_PreservationL1.v also refutes the proposed value-anchored restriction along this path." +closes-when = "Do not prove the old conclusion. Define and prove a separately stated sound replacement after redesign." [[proof-debt]] id = "L1.D-App" file = "Semantics_L1.v" line-anchor = "preservation_l1 S_App_Step2" -class = "calculus-soundness-gap" +class = "counterexample-refuted-statement" tractable = false -diagnosis = "T_Lam_L1 rigidly fixes the lambda body's R at lambda-creation; T_Var_*_L1 permit typing TString r at empty R. Combined, the L1 typing is too permissive for preservation under R-shifting steps." -closes-when = "one of (1) effect-typed lambdas (L2/L3), (2) restrict T_Lam_L1 to region-pure bodies, (3) restrict T_Var_*_L1 to require In r R for variables of type containing r" -follow-up = "see PRESERVATION-DESIGN.md §4.8" +diagnosis = "Historical S_App_Step2 conjecture; the unrestricted preservation_l1 theorem is refuted by Counterexample_PreservationL1.v." +closes-when = "Not by proving this statement. State a sound replacement after judgment/step redesign." +follow-up = "see PROOF-NEEDS.adoc current L1 boundary" [[proof-debt]] id = "L1.D-Pair" file = "Semantics_L1.v" line-anchor = "preservation_l1 S_Pair_Step2" -class = "calculus-soundness-gap" +class = "counterexample-refuted-statement" tractable = false -diagnosis = "same as L1.D-App" -closes-when = "see L1.D-App" -follow-up = "see PRESERVATION-DESIGN.md §4.8" +diagnosis = "Historical S_Pair_Step2 conjecture; the unrestricted preservation_l1 theorem is refuted by Counterexample_PreservationL1.v." +closes-when = "Not by proving this statement. State a sound replacement after judgment/step redesign." +follow-up = "see PROOF-NEEDS.adoc current L1 boundary" [[proof-debt]] id = "L1.C-region-liveness" file = "Semantics_L1.v" -line-anchor = "region_liveness_at_split_l1 (Axiom)" -class = "carry-invariant-through-induction" -tractable = true -diagnosis = "subst_typing_gen_l1 needs to know that In rv R_inner at each compound-rule split point. The outer call provides In rv R; the inductive descent doesn't propagate it because T_Var_Lin_L1 doesn't enforce In rv R." -closes-when = "one of (1) strengthen T_Var_Lin_L1 to require In rv R, (2) add a side condition to subst_typing_gen_l1 stating In rv R at every R_inner reached, (3) prove a region-liveness corollary of L1.B's count monotonicity" +line-anchor = "historical region_liveness_at_split_l1 (removed 2026-06-26)" +class = "refuted-statement-replaced" +tractable = false +diagnosis = "The unconditional region-liveness claim was false in the active-region exit case and has been removed. The current true lemma carries an explicit no-exit premise." +closes-when = "No closure of the old statement. Preserve region_liveness_no_exit_l1_gen and val_region_no_exit as the restricted boundary." # ============================================================================ # DOCUMENTATION POINTERS # ============================================================================ [docs] -design = "formal/PRESERVATION-DESIGN.md" -handoff = "formal/PRESERVATION-HANDOFF.md" +design = "formal/PRESERVATION-DESIGN.adoc" +handoff = "formal/PRESERVATION-HANDOFF.adoc" roadmap = "ROADMAP.adoc" counterexample = "formal/Counterexample.v" disambiguation = "nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md" @@ -215,7 +227,8 @@ preservation-design-§12-16-roadmap = "v2 echo-as-foundation forward look" coq-version = "8.18.0" project-file = "formal/_CoqProject" invocation = "coq_makefile -f _CoqProject -o Makefile && make" -last-clean-build = "2026-05-27" +last-clean-build = "2026-05-27 (historical; no fresh build in 2026-11 audit)" +current-audit = "coqc unavailable; GitHub run 40435929887 (2026-10-27) succeeded overall but skipped Coq build job; not a proof-build receipt" modules = [ "Syntax", "Typing", diff --git a/formal/Semantics_L1.v b/formal/Semantics_L1.v index ea50031d..12497945 100644 --- a/formal/Semantics_L1.v +++ b/formal/Semantics_L1.v @@ -1,7 +1,7 @@ (* SPDX-License-Identifier: MPL-2.0 *) (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) -(* hypatia: allow code_safety/admitted -- TRACKED v2 proof-debt, not an honest-completion gap. The 2 remaining Admitted lemmas (step_pop_disjoint_from_type_l1, preservation_l1) and their internal `admit.` tactics are documented in PROOF-NEEDS.md and owner-fenced by CLAUDE.md (directive 2026-05-27): closing or extending them via ad-hoc patching is a banned anti-pattern. step_pop is open eliminator-fork research; preservation_l1 is the capstone gated on it. The former third admit, region_liveness_at_split_l1_gen, was provably FALSE as stated and has been REMOVED (2026-06-26) via the honest val_region_no_exit reformulation (routes through the TRUE region_liveness_no_exit_l1_gen, Qed). Build truth is the `Print Assumptions` CI gate, not this comment. *) +(* hypatia: allow code_safety/admitted -- tracked proof boundary; not an honest-completion claim. The two remaining outer Admitted markers (step_pop_disjoint_from_type_l1, preservation_l1) are each refuted as currently stated: see Counterexample_StepPop.v and Counterexample_PreservationL1.v. Do not try to close either unrestricted claim by ad-hoc patching or relabel them routine debt. Replacement work must reformulate the judgment/step interface with an explicit invariant and state a new theorem. The former region_liveness_at_split_l1_gen false statement was removed (2026-06-26) via val_region_no_exit / region_liveness_no_exit_l1_gen. See PROOF-NEEDS.adoc for current classification. Build truth is the `Print Assumptions` CI gate, not this comment. *) (* hypatia: allow coq_admit_tactic -- see preceding directive; same tracked admits. *) (** @@ -11,8 +11,9 @@ *** *** *** This is the post-counterexample L1 redesign. Extend HERE. *** *** *** - *** 3 `Admitted` lemmas remain (down from 7 mid-chain, 9 pre- *** - *** bullet-restoration). L2-β + L1 closures so far: *** + *** 2 outer `Admitted` lemmas remain; both unrestricted claims *** + *** are refuted by pinned regressions (see below). L1/L2 Qed *** + *** infrastructure is not a universal preservation theorem. *** *** - typing_preserves_bindings_l1 (now m-polymorphic) *** *** - unrestricted_flag_unchanged_l1 *** *** - shift_typing_gen_l1 (via shift_typing_gen_l1_m + wrapper) *** @@ -26,14 +27,11 @@ *** - typing_preserves_length_l1, output_shape_at_l1, *** *** loc_retype_at_R_l1 all generalised to m-polymorphic *** *** *** - *** Residual admits (L2-β follow-up): *** - *** 1. region_liveness_at_split_l1_gen — 1 narrow admit in the *** - *** T_Region_Active_L1 [r = rv] sub-case (genuinely false *** - *** per documented counterexample ERegion rv (EI32 5)) *** - *** 2. step_pop_disjoint_from_type_l1 — congruence cases *** - *** (S_Let_Step etc.) blocked on §4.8 lambda-rigidity *** - *** 3. preservation_l1 — capstone; depends on closing (1)+(2) *** - *** under L2 dispatch + lambda-rigidity gap resolution *** + *** Refuted statements still marked Admitted: *** + *** - step_pop_disjoint_from_type_l1 — Counterexample_StepPop.v *** + *** - preservation_l1 — Counterexample_PreservationL1.v *** + *** Their Admitted markers are transparency, not a proof plan. *** + *** Replacement theorems require an owner-approved redesign. *** *** *** *** DO NOT close them by: *** *** - introducing new `Axiom` declarations *** @@ -41,10 +39,10 @@ *** - strengthened lemma signatures dodging the L2 dispatch *** *** *** *** Cross-layer dependencies (L1's lambda-rigidity gap closes at *** - *** L2) are documented in `formal/PRESERVATION-DESIGN.md §5.1`. *** + *** L2) are documented in `formal/PRESERVATION-DESIGN.adoc §5.1`. *** *** *** - *** See `STATUS.adoc`, `PROOF-NEEDS.md`, and *** - *** `formal/PRESERVATION-DESIGN.md`. *** + *** See `STATUS.adoc`, `PROOF-NEEDS.adoc`, and *** + *** `formal/PRESERVATION-DESIGN.adoc`. *** ********************************************************************* *) @@ -55,7 +53,7 @@ judgment in [TypingL1.v]. The operational semantics [step] from [Semantics.v] is unchanged. - Per PRESERVATION-DESIGN.md §4.5, preservation under L1 is: + Per PRESERVATION-DESIGN.adoc §4.5, preservation under L1 is: [step (mu, R, e) (mu', R', e')] /\ [has_type_l1 R G e T R_final G'] @@ -77,29 +75,24 @@ [region_shrink_preserves_typing_l1_gen{,_m}] was FALSE-as-stated (witness pinned in [Counterexample_RegionShrink.v]) and is replaced by the multiset-permutation lemma; no residual admit here. - - [subst_preserves_typing_l1] — Qed (L1.C) with strengthened - statement (the original signature was demonstrably unsound — see - the lemma's header). Depended on a single isolated sub-Axiom - [loc_retype_at_R_l1] (task #27); the L1.F PR replaces that - unsound axiom with (i) a Qed-able [loc_retype_at_R_l1] requiring - [In r R_inner] and (ii) a narrower [region_liveness_at_split_l1] - axiom capturing only the genuine structural obligation that - remains. Two compound-rule cases (T_Lam_L1_Linear, T_Region_L1) are - discharged directly with no axiom; nine residual sites cite the - narrower axiom. See its header for closure approaches. - - [preservation_l1] — Admitted; the three swarm helpers above - unblock the per-case proof, but the bullet structure (per - design doc §4.5 + §12.16) is itself follow-up work (task #24). - - Per-case proof sketches were validated experimentally during this - file's authoring. The cases that close without any of the three - Admitted helpers are: S_StringNew (apply T_Loc_L1), S_StringConcat - (invert both T_Loc_L1 children, then apply T_Loc_L1), S_StringLen - (invert the borrow, apply T_I32_L1), S_If_True / S_If_False - (invert T_Bool_L1 on the condition, then assumption), S_Region_ - Enter (re-apply T_Region_Active_L1 with the same R_body), and - S_Drop (apply T_Unit_L1). These can be inlined once the bullet - structure accounts for the per-region typing cross-cases + - [subst_preserves_typing_l1] — Qed with a strengthened statement + (the original signature was demonstrably unsound; see the lemma + header). The former [region_liveness_at_split_l1] axiom was + removed as false-as-stated; current substitution routes through + the Qed no-exit formulation and explicit premises described by + [val_region_no_exit]. These helper results do not establish + preservation for every step. + - [preservation_l1] — still marked Admitted, but its unrestricted + statement is refuted by [Counterexample_PreservationL1.v]. Do not + treat the marker as unfinished routine proof debt. A replacement + requires an explicitly different judgment/step boundary or a + restricted theorem with proved premises; see [PROOF-NEEDS.adoc]. + + Older per-case proof sketches and closure estimates below are + historical authoring notes. The current theorem boundaries are the + pinned regressions and scoped lemmas identified above; local Qed + cases must not be read as evidence that the refuted universal + statement can be completed. (ERegion inverts to both T_Region_L1 and T_Region_Active_L1, doubling subgoals for the three region step rules). @@ -982,9 +975,8 @@ Qed. [k] in both input and output. R is unchanged at every rule. L2-β restoration 2026-05-27: generalised to modality-polymorphic - [has_type_l1 m] mirroring [region_liveness_at_split_l1_gen]'s - shape. The Linear-only wrapper [shift_typing_gen_l1] preserves - the original signature for callers. Body ported from commit + [has_type_l1 m]. The Linear-only wrapper [shift_typing_gen_l1] + preserves the original signature for callers. Body ported from commit 56f592f with new bullets for T_Lam_L1_Affine, T_Case_L1_Affine, T_If_L1_Affine — each Affine case mirrors its Linear counterpart since R and `insert_at` threading are modality-independent. *) @@ -2068,10 +2060,11 @@ Qed. (** The substituted value's region has no exit inside [e]. For a linear value (always an [ELoc _ r] by [linear_value_is_loc_l1]) this is the - honest no-exit side condition; for any other value it is vacuous. This - is the premise that lets the 13 substitution sites below discharge - region-liveness through the TRUE [region_liveness_no_exit_l1_gen] - instead of the false [region_liveness_at_split_l1_gen]. *) + explicit no-exit premise; for any other value it is vacuous. The + substitution theorem below requires it and uses the Qed + [region_liveness_no_exit_l1_gen] lemma. The former unconditional + [region_liveness_at_split_l1_gen] statement was false and has been + removed; this conditional lemma does not prove preservation by itself. *) Definition val_region_no_exit (v e : expr) : Prop := match v with | ELoc _ r => expr_no_exit_of_region r e @@ -2137,10 +2130,10 @@ Definition val_region_no_exit (v e : expr) : Prop := [formal/L1-REGION-REFOUNDATION-PLAN.md] (ADMIT 2 section). *) (** Generalized substitution: at depth [k] for a linear value [v]. - Mirrors legacy [subst_typing_gen]. The only L1-specific gap is the - need to retype [v = ELoc l r] at the inner region environment of - compound rules. Closed via [region_liveness_at_split_l1_gen] + - [loc_retype_at_R_l1_m]. + Mirrors legacy [subst_typing_gen] under the L1 judgment. The + strengthened theorem carries [val_region_no_exit] explicitly; its + Qed proof uses the no-exit liveness lemma and local retyping helpers. + It is conditional infrastructure, not a preservation theorem. L2-β follow-up #2 (closed): m-polymorphic generalisation mirroring [shift_typing_gen_l1_m]. The substituted value's typing @@ -3191,9 +3184,16 @@ Qed. (** ** Preservation under the L1 judgment. - Case-by-case inversion + reconstruction over [step]. The proof - closes 30 of 33 residual subgoals (post-automation chain + L1.E - [count_occ_le_l1]); the 3 remaining [admit.]s surface a deeper + HISTORICAL proof decomposition (pre-counterexample; case counts and + proposed closure route below are not current proof debt). The + unrestricted theorem is now refuted as stated by + [Counterexample_PreservationL1.v]. Its [Admitted] is a transparent + marker for a false statement, not a proof expected to be completed. + The old case-by-case diagnosis follows only as design archaeology. + + At the time, the proof sketch described 30 of 33 case subgoals as + closing; that accounting does not change the counterexample result or + establish any restricted replacement. The remaining diagnosis was a **soundness-class gap**: - S_StringConcat_Step2: TString r type — the lift is sound @@ -3227,15 +3227,16 @@ Qed. multiset-perm hypothesis (an active region strictly drops its r-count, so its output cannot be a multiset-perm of its input). - Until the lambda-rigidity gap is resolved (likely via effect- - typed lambdas as an L2/L3 extension), [preservation_l1] remains - [Admitted.] but the proof body documents exactly which sub-cases - remain and the structural reason for each. *) + This historical lambda-rigidity diagnosis is incomplete in light of + [Counterexample_PreservationL1.v]. Do not treat the old case map or + effect-typed-lambda route as a proof plan for the refuted theorem. + Any replacement must state its changed judgment and premises + explicitly and be checked against all pinned regressions. *) (** ** P06 — [step_pop_disjoint_from_type_l1] Auxiliary lemma for the S_StringConcat_Step2 case of - [preservation_l1]. Per [PRESERVATION-DESIGN.md §4.7]: the + [preservation_l1]. Per [PRESERVATION-DESIGN.adoc §4.7]: the operational [step] never pops a region that appears free in the type of the stepping expression. Combined with [In r R] from a [TString r] value's typing (via [linear_value_is_loc_l1] + @@ -3271,13 +3272,11 @@ Qed. to the static typing output — preservation itself (the §2 "same wall"). - **Verdict (§6).** RELOCATES, not closes — but now to ONE minimal, - precisely-stated obligation (count-coherence at a congruence region - exit), not eleven scattered §4.8 admits. The closure route is the - tropically-graded choreography over time segments in - [formal/L1-ELIMINATOR-FORK.md] §3–§7. The single outer [Admitted] - and [preservation_l1]'s [admit] are unchanged; this is a clarity + - isolation improvement, not an axiom-count reduction. *) + **Verdict (historical §6, superseded).** This analysis isolated a + count-coherence obligation but did not establish it. The unrestricted + lemma above is now refuted by [Counterexample_StepPop.v]; its outer + [Admitted] is not routine proof debt. The choreography documents a + redesign direction, not a proof route for the current statement. *) Lemma step_pop_disjoint_from_type_l1 : forall mu R e mu' R' e' m G T R_final G', (mu, R, e) -->> (mu', R', e') -> @@ -3309,9 +3308,9 @@ Proof. coherence at a region exit: the temporal/segment structure the snapshot env + result type cannot express, relocating to connecting the dynamic exit to the static typing output, i.e. preservation - itself. Open research; the §6 "relocates" verdict and the - choreographic route are recorded in - [formal/L1-ELIMINATOR-FORK.md]. *) + itself. This unrestricted statement is refuted by + [Counterexample_StepPop.v]; the choreographic route is a + redesign direction, not a proof plan for this lemma. *) subst r. admit. + (* r <> r0 : remove_first r keeps every r0. *) apply remove_first_preserves_other; [exact Hne | exact HinR]. @@ -3328,10 +3327,10 @@ Theorem preservation_l1 : has_type_l1 m R G e T R_final G' -> has_type_l1 m R' G e' T R_final G'. Proof. - (* L2 partial: re-state under modality. Linear and Affine cases - both Admitted in this PR — Linear branch had pre-L2 partial - proof (12 admits) which becomes harder to maintain after the - mode-split; full restoration deferred to L2-β. *) + (* Deliberately remains Admitted: the unrestricted theorem statement + is refuted by Counterexample_PreservationL1.v. Do not fill this + proof body without first replacing the false statement with an + owner-approved, explicitly restricted soundness theorem. *) intros m mu R e mu0 R0 e0 Hstep G T R_final G_out Ht. admit. Admitted. @@ -3347,8 +3346,8 @@ Admitted. Stated as two per-case lemmas + an umbrella theorem [preservation_l3] which is their conjunction. - Design constraint (PRESERVATION-DESIGN.md §6.3 + - PROOF-NEEDS.md §2): the L3 step rules are universally + Design constraint (PRESERVATION-DESIGN.adoc §6.3 + + PROOF-NEEDS.adoc §2): the L3 step rules are universally quantified over the witness type [T] in the [EEcho T v] residue. The non-determinism is resolved at the typing- derivation level — each L3 typing rule pins [T] to its body @@ -3519,26 +3518,17 @@ Print Assumptions preservation_l3. (** ** P06 — axiom-dependency audit of [step_pop_disjoint_from_type_l1]. - [step_pop_disjoint_from_type_l1] is [Admitted] in this commit (the - HARD cases — S_Let_Step, S_LetLin_Step, S_App_Step2, S_If_Step, - S_Pair_Step1/2, S_Inl_Step, S_Inr_Step, S_Case_Step, S_Region_Step - T_Region_L1 sub-case — are blocked on the §4.8 lambda-rigidity / - variable-typing strengthening, tracked at ephapax issues - #240 / #241 / #242). - - The EASY cases (atomic non-region step rules; S_Region_Enter / - Exit / Exit_Echo; S_StringConcat_Step1/2; S_App_Step1; - S_Fst_Step / S_Snd_Step; S_Borrow_Step; S_Drop_Step; S_Copy_Step) - are Qed-closed via direct case analysis. The lemma's overall - status is therefore "Admitted" but with a structured proof body - enumerating the obstacle per case. - - [Print Assumptions] will list the lemma itself as an axiom (the - Admitted form). When all internal admits close, this directive - will show only the remaining residual axioms - ([region_liveness_at_split_l1_gen] and the capstone - [preservation_l1]); the former region_shrink admit is now - closed (region_shrink_msperm, Qed). *) + Historical case analysis below records why the proof body was left + structured. It is superseded as a closure plan: the unrestricted + theorem is refuted by [Counterexample_StepPop.v], and a later + value-anchored witness in [Counterexample_PreservationL1.v] also + defeats the proposed restriction. Its [Admitted] is a transparency + marker for a false statement, not an unfinished routine proof. + + The Qed cases in the body remain local proof facts; they do not + salvage the universal theorem. [Print Assumptions] reports the + admitted theorem as an axiom. Current replacement status is in + [PROOF-NEEDS.adoc]. *) Print Assumptions step_pop_disjoint_from_type_l1. diff --git a/formal/TypingL1.v b/formal/TypingL1.v index ba8d0974..cb4e1c24 100644 --- a/formal/TypingL1.v +++ b/formal/TypingL1.v @@ -14,8 +14,8 @@ *** `has_type_l1` (L2-hybrid landing, PRs #176 + #177). *** *** `linear_to_affine` is Qed with zero axioms. *** *** *** - *** See `STATUS.adoc`, `PROOF-NEEDS.md`, *** - *** `formal/PRESERVATION-DESIGN.md`. *** + *** See `STATUS.adoc`, `PROOF-NEEDS.adoc`, *** + *** `formal/PRESERVATION-DESIGN.adoc`. *** ********************************************************************* *) @@ -23,11 +23,12 @@ (** * Ephapax Typing Rules — L1 redesign (region capability threading) This file contains the **new** typing judgment as specified in - [formal/PRESERVATION-DESIGN.md §4]. It coexists with the legacy + [formal/PRESERVATION-DESIGN.adoc §4]. It coexists with the legacy [Typing.v] (`has_type`) so that the migration is incremental: old lemmas in [Semantics.v] continue to compile against the legacy - judgment, and [Counterexample.v] gains a new lemma proving the - L1 fix blocks the bad input. + judgment, and [Counterexample.v] proves that this particular + legacy bad input is rejected. This regression is not a general + preservation or language-soundness theorem. The judgment shape is: @@ -47,7 +48,7 @@ beyond L1's scope. This is the same simplification echo-types makes by parameterising over a thin order rather than a fibration. - See [formal/PRESERVATION-DESIGN.md §4] for the full design + See [formal/PRESERVATION-DESIGN.adoc §4] for the full design rationale and [Counterexample.v]'s new [bad_input_untypable_l1] lemma for the regression. *) @@ -357,7 +358,7 @@ Inductive has_type_l1 T_Case_L1_Affine's per-branch disagreement. L3 echo residue: output [TBase TUnit] is a residue placeholder; - full residue mechanisation is L3 (PRESERVATION-DESIGN.md §6). *) + full residue mechanisation is L3 (PRESERVATION-DESIGN.adoc §6). *) | T_Drop_L1 : forall m R R' G G' e T, is_linear_ty T = true -> @@ -422,7 +423,7 @@ Inductive has_type_l1 irreversible step*, not recovery of the erased witness. The witness is, by construction, irrecoverable — see [Echo.no_section_collapse_to_residue] (Qed) and - [PRESERVATION-DESIGN.md §6.0.2.3]. *) + [PRESERVATION-DESIGN.adoc §6.0.2.3]. *) | T_Observe_L1 : forall m R R' G G' e T, R ; G |=L1[m] e : TEcho T -| R' ; G' -> @@ -471,7 +472,7 @@ Qed. Every derivation in [has_type_l1 Linear ...] is also a derivation in [has_type_l1 Affine ...]. This is the modality weakening - promised by PRESERVATION-DESIGN.md §5 — the "thin-poset + promised by PRESERVATION-DESIGN.adoc §5 — the "thin-poset decoration" lemma, mirror of [echo-types/proofs/agda/EchoLinear.agda:38-58] [weaken : LEcho linear → LEcho affine]. From 45dd8a8b2b60b3a691f19af5215dba07e651cfda Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 17:40:15 +0000 Subject: [PATCH 2/4] ci: point status gate at AsciiDoc ledgers Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/status-gate.yml | 10 +++++----- PROOF-NEEDS.adoc | 6 +++++- scripts/status-gate.sh | 18 +++++++++--------- 3 files changed, 19 insertions(+), 15 deletions(-) diff --git a/.github/workflows/status-gate.yml b/.github/workflows/status-gate.yml index 44a5ff60..06d5515b 100644 --- a/.github/workflows/status-gate.yml +++ b/.github/workflows/status-gate.yml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: MPL-2.0 # This workflow is managed by gh actions-lock. # Owner: Jonathan D.A. Jewell -# Status Gate — fail when the PROOF-NEEDS.md / TEST-NEEDS.md count markers +# Status Gate — fail when the PROOF-NEEDS.adoc / TEST-NEEDS.adoc count markers # drift from coqc/cargo ground truth. # # Split into two independent jobs so the slow one is cancellable without @@ -18,8 +18,8 @@ on: pull_request: paths: - 'formal/**' - - 'PROOF-NEEDS.md' - - 'TEST-NEEDS.md' + - 'PROOF-NEEDS.adoc' + - 'TEST-NEEDS.adoc' - 'scripts/status-gate.sh' - 'Cargo.toml' - 'Cargo.lock' @@ -36,7 +36,7 @@ concurrency: jobs: # CORE — fast, no toolchain. Keep this one required: a new Admitted that - # isn't reflected in PROOF-NEEDS.md fails here in ~1 second. + # isn't reflected in PROOF-NEEDS.adoc fails here in ~1 second. status-gate-core: name: status-gate-core runs-on: ubuntu-latest @@ -56,7 +56,7 @@ jobs: steps: - name: Notice — this is the slow, skippable job run: | - echo "::notice title=Slow check — safe to cancel::status-gate-tests runs a full cargo build just to verify the TEST-NEEDS.md test count. The core proof-count gate (status-gate-core) is a separate, independent job and is already enforced. If you're in a rush you can cancel THIS job without letting any core gating go." + echo "::notice title=Slow check — safe to cancel::status-gate-tests runs a full cargo build just to verify the TEST-NEEDS.adoc test count. The core proof-count gate (status-gate-core) is a separate, independent job and is already enforced. If you're in a rush you can cancel THIS job without letting any core gating go." - name: Checkout repository uses: actions/checkout@v7.0.1 - name: Install Rust toolchain diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index b4ac9902..c6932d07 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -513,7 +513,11 @@ the owner*: Coq `+Admitted.+` marker count: *3* (current source inventory): one legacy marker plus two in `+Semantics_L1.v+`. This is a marker count, not -a count of sound obligations still awaiting routine proof: +a count of sound obligations still awaiting routine proof. + +CI count marker only (source markers, not routine proof debt): +Coq admitted proofs remaining: 3 + * `+formal/Semantics.v+` `+preservation+`: false as stated; durable legacy archaeology, pinned by `+Counterexample.v+`. diff --git a/scripts/status-gate.sh b/scripts/status-gate.sh index 0a7e5786..96024a8a 100755 --- a/scripts/status-gate.sh +++ b/scripts/status-gate.sh @@ -8,10 +8,10 @@ # required gate and the expensive one as a separate, cancellable job: # # --proofs Proof-count only: greps formal/*.v for `Admitted.` and -# compares to PROOF-NEEDS.md. No toolchain, runs in ~1s. +# compares to PROOF-NEEDS.adoc. No toolchain, runs in ~1s. # This is the CORE gate — keep it required. # --tests Test-count only: `cargo test --all-targets -- --list` and -# compares to TEST-NEEDS.md. Needs a full Rust build (minutes). +# compares to TEST-NEEDS.adoc. Needs a full Rust build (minutes). # SAFE TO SKIP / CANCEL if you are in a rush — it never gates # soundness, only doc-count hygiene for the test inventory. # (no arg) Both (the local `just status-gate` default). @@ -38,30 +38,30 @@ extract_claim() { } check_proofs() { - # 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. + # Single-source claim: PROOF-NEEDS.adoc §4 carries the canonical + # `Coq admitted proofs remaining: ` marker (a source-marker count, + # not an assertion that each marker is routine proof debt). local claim actual - claim="$(extract_claim "PROOF-NEEDS.md" "Coq admitted proofs remaining")" + claim="$(extract_claim "PROOF-NEEDS.adoc" "Coq admitted proofs remaining")" actual="$( (grep -R --include='*.v' -n '^[[:space:]]*Admitted\.' formal || true) \ | wc -l | tr -d ' ' )" if [ "$claim" != "$actual" ]; then - fail "PROOF-NEEDS.md claims ${claim} admitted proofs, actual is ${actual}" + fail "PROOF-NEEDS.adoc claims ${claim} admitted markers, actual is ${actual}" fi echo "status-gate[proofs]: OK — admitted proofs: ${actual}" } check_tests() { local claim actual - claim="$(extract_claim "TEST-NEEDS.md" "Documented all-target tests")" + claim="$(extract_claim "TEST-NEEDS.adoc" "Documented all-target tests")" actual="$( cargo test --all-targets -- --list \ | grep ': test$' | wc -l | tr -d ' ' )" if [ "$claim" != "$actual" ]; then - fail "TEST-NEEDS.md claims ${claim} tests, actual is ${actual}" + fail "TEST-NEEDS.adoc claims ${claim} tests, actual is ${actual}" fi echo "status-gate[tests]: OK — all-target tests: ${actual}" } From 6ac91339b966ad585018ddfce1ed948caa1f39b5 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 17:48:50 +0000 Subject: [PATCH 3/4] docs: tighten proof ledger statuses and scope Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- EXPLAINME.adoc | 19 ++++++++++--------- V1-TO-V2.adoc | 9 ++++++--- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index ed901d2c..31aef6d8 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -339,7 +339,7 @@ helper is not proof debt. actual call sites. This restricted result does not restore unrestricted region shrinking or general preservation. -|L1 no-exit liveness and strengthened substitution helpers |proven (conditional) +|L1 no-exit liveness and strengthened substitution helpers |proven |Coq 8.18.0; project build recipe above |`+formal/Semantics_L1.v+`: `+region_liveness_no_exit_l1_gen+`, `+subst_preserves_typing_l1+` |No-exit premise is explicit; these lemmas support restricted substitution @@ -351,7 +351,7 @@ and do not prove preservation for arbitrary operational steps. |Shows the local modality weakening relation only. It does not prove L1/L2 preservation for either mode. -|L2 β-case helper family |proven (conditional) +|L2 β-case helper family |proven |Coq 8.18.0; project build recipe above |`+formal/TypingL2.v+`: `+preservation_l2_app_eff_beta_linear_l1+`, `+_linear+`, `+_ground_nonlinear_l1+`, `+_ground_nonlinear+`, `+_tfuneff_l1+`, `+_tfuneff+` |Requires the exact value/type/effect premises in each lemma. The @@ -359,11 +359,12 @@ L1/L2 preservation for either mode. subset condition, and closure below zero. These are restricted β-case lemmas, not unconditional L2 preservation. -|L3 matching echo-rule preservation results |proven (scoped) +|L3 matching echo-rule preservation results |proven |Coq 8.18.0; project build recipe above |`+formal/Semantics_L1.v+`: `+preservation_l3_region_active_echo+`, `+preservation_l3_drop_echo+`, `+preservation_l3+` -|Only matching echo-emitting typing/step-rule pairs; does not establish -general L1/L2 preservation or implementation refinement. +|Only matching echo-emitting typing/step-rule pairs. The region-echo case +additionally requires `+expr_strictly_free_of_region r v+`; it does not +establish general L1/L2 preservation or implementation refinement. |Fresh-region L2 β witness (input types, steps, result is untypable at L1) |proven |Coq 8.18.0; project build recipe above @@ -389,7 +390,7 @@ all L1 regressions remain mandatory controls. |Current β-case helpers are conditional; `+preservation_l2_via_l1+` transparently depends on the refuted L1 statement. -|Mathesis Grade 3 receipt for Ephapax language soundness |open (target) +|Mathesis Grade 3 receipt for Ephapax language soundness |open |Agda receipt required by the Mathesis architecture |No Agda Grade 3 proof currently recorded |The existing witnesses are Coq, not Grade 3. Standards classifies local @@ -500,7 +501,7 @@ so this is not a reproducibly pinned toolchain receipt. |`+src/formal/Ephapax/Formal/RegionLinear.idr:164+` |Transports a `+CannotEscape+` witness across a qualifier change in the local datatype. It is not a language preservation theorem. -|Region safety extraction `+regionSafetyExtract+` and GC extraction `+noGCExtract+` |proven (vacuous wrappers) +|Region safety extraction `+regionSafetyExtract+` and GC extraction `+noGCExtract+` |proven |Idris2 0.8.0; `%default total`; package build above (historically reported, not rerun here) |`+src/formal/Ephapax/Formal/RegionLinear.idr:139,151+` |Return supplied input witnesses unchanged. They prove no standalone runtime region-safety or GC-freedom property. @@ -520,10 +521,10 @@ so this is not a reproducibly pinned toolchain receipt. |`+src/abi/Ephapax/ABI/Foreign.idr:108+` |Case analysis for the local enum/int mapping only; not evidence that Rust/WASM compilation succeeds or preserves source typing. -|ABI seam E1/E2-control-flow/E3-runtime/E4/E5/E6 obligations |open / erased postulates +|ABI seam E1/E2-control-flow/E3-runtime/E4/E5/E6 obligations |open |Idris2 package build checks declarations, not discharged proofs |`+src/abi/Ephapax/ABI/Invariants.idr+`; register in `+PROOF-NEEDS.adoc+` §5.3 -|Declarations state owed obligations (type preservation, control-flow consumption, runtime no-escape, no-GC, WASM typing, IR semantics). They are not proof receipts; E2 position-form and E3 static form are separately discharged as above. +|These obligations remain open; some are represented by erased declarations/postulates, not proof terms. E2 position-form and E3 static form are separately discharged as above. The ledger row does not treat declarations as evidence that the operational or compiler-correctness obligations hold. |=== Idris2 evidence follows the Standards route for repository-specific diff --git a/V1-TO-V2.adoc b/V1-TO-V2.adoc index f36b7fc4..a4295d86 100644 --- a/V1-TO-V2.adoc +++ b/V1-TO-V2.adoc @@ -51,9 +51,12 @@ additional L1/L2 soundness gaps that require redesign: track regions, structural discipline, echo residue and dyadic mode all at once. That conflation was *unsound*, and — unusually — we **proved it unsound with a machine-checked counterexample** rather than shipping - the bug. v2 splits those four concerns into four orthogonal layers - (L1–L4) and **re-derives preservation per layer** from explicit - invariants. Three of the four layers already carry `Qed` theorems. + the bug. v2 separates those four concerns into four orthogonal layers + (L1–L4) as a **redesign target** for future, precisely stated + preservation results. The current unrestricted L1 preservation claim is + refuted, no unconditional L2 preservation theorem is established, and + L3 results are scoped to matching echo-rule pairs. Existing `Qed` + lemmas do not establish general preservation per layer. Discovering your own unsoundness *before* anyone depends on it, with a proof, and then redesigning around the lesson, is not failure. It is the From 1476b64b04f3676cc9738aa35693afeb349db1fd Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Sun, 1 Nov 2026 18:04:04 +0000 Subject: [PATCH 4/4] docs: document status gate proof and test count checks --- scripts/status-gate.sh | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/scripts/status-gate.sh b/scripts/status-gate.sh index 96024a8a..355c5ed9 100755 --- a/scripts/status-gate.sh +++ b/scripts/status-gate.sh @@ -37,6 +37,9 @@ extract_claim() { echo "$line" | grep -Eo '[0-9]+' | head -n 1 } +# Compare the first proof count marker with lines starting with `Admitted.` +# (after optional whitespace) in Coq files under formal/. Exit if the marker +# is missing or the counts differ. check_proofs() { # Single-source claim: PROOF-NEEDS.adoc §4 carries the canonical # `Coq admitted proofs remaining: ` marker (a source-marker count, @@ -53,6 +56,9 @@ check_proofs() { echo "status-gate[proofs]: OK — admitted proofs: ${actual}" } +# Compare the first test count marker with Cargo's listed lines ending in +# `: test`. Exit if the marker is missing, the counts differ, or the listing +# pipeline fails, including when no test lines match. check_tests() { local claim actual claim="$(extract_claim "TEST-NEEDS.adoc" "Documented all-target tests")"