diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 850e7f7..64a5213 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -16,7 +16,12 @@ is used after being freed, no resource is leaked, and region-scoped allocations are deallocated in bulk at scope exit. ____ -== Claim: Dyadic Type System +== Claim: Dyadic Type System (L2) + +The dyad is L2 in the four-layer architecture (see +`README.adoc#the-four-layers` and `docs/vision/EPHAPAX-VISION.adoc`). +This section presents the Rust-side evidence for the L2 discipline; +L1 / L3 / L4 evidence follows below. *Evidence*: The type checker (`src/ephapax-typing/src/lib.rs`) tracks `BindingForm` per context entry: @@ -29,6 +34,9 @@ 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`. +The Coq-side L2 evidence is `linear_to_affine : Linear ≤ Affine` (Qed, +zero axioms) in `formal/Modality.v`. + == Claim: Two-Layer AST (Surface + Core) *Evidence*: Two separate crates: @@ -77,6 +85,56 @@ demonstrate where they diverge on identical programs (e.g. 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 three 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; 9 L1 supporting-lemma admits remain as + L2-integration debt (tracked in `PROOF-NEEDS.md`). + +== Claim: Irreversibility residue is first-class (L3, planned) + +*Evidence (planned)*: Operations that erase information (region +exit, drop) will 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. + +* 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`. +* Status: **planned** integration — `Echo.v` is wired up + internally, but no ephapax typing rule yet introduces `TEcho`. + The L3 extension follows L1's residual admit closure. + +== Claim: Dyadic mode is project-level only (L4) + +*Evidence*: L4 is a labelling discipline, not a proof layer. +`formal/L4.v` carries `ProgramMode` (three-constructor enum) and +`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`. +* Surface syntax for the L4 declaration + (`#![ephapax_linear]` / `#![ephapax_affine]` / + `#![module_boundary_mix(...)]`) is not yet wired into the parser + or borrow checker; the mechanical scaffold is a citable type for + downstream tools (Idris2 ABI, Rust borrow checker, surface + parser). + == Technology Choices [cols="1,2"] diff --git a/README.adoc b/README.adoc index e1cd6c8..a4ad123 100644 --- a/README.adoc +++ b/README.adoc @@ -63,7 +63,9 @@ link:formal/PRESERVATION-DESIGN.md[`formal/PRESERVATION-DESIGN.md`] Quick read: **L1** (region capabilities) substantially complete; **L2** (Linear/Affine modality) core landed with zero axioms; **L3** (echo / residue) calculus done locally, integration into the typing -judgment is the next-block work; **L4** (dyadic mode) not started. +judgment is the next-block work; **L4** (dyadic mode) mechanical +scaffold landed (`formal/L4.v` — definitions only by design; no proof +obligations). ==== Ephapax is a research language for **principled handling of @@ -100,15 +102,19 @@ Ephapax is a programming language with: |=== | Property | What this means -| **Dyadic discipline** +| **Dyadic discipline (L2)** | Each binding is *either* affine (`let` — used at most once, weakening allowed) *or* linear (`let!` — used exactly once, - weakening forbidden). Type checker enforces. + weakening forbidden). Type checker enforces. See "The four layers" + below for how this composes with L1/L3/L4. -| **Region-based memory** -| Allocations live in named regions (`region r: ...`); when the - region's scope ends, the runtime bulk-frees every resource in it. - No allocator overhead per object; no per-object frees. +| **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. | **Second-class borrows** | `&x` gives temporary access without consuming `x`. Borrows cannot @@ -127,6 +133,57 @@ Ephapax is a programming language with: reference counting, no allocator-per-object metadata. |=== +== 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). + +[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`. + +| **L2 — Structural discipline (linear ↔ affine)** +| The *modality* of the surrounding program decides whether linear + bindings must be consumed (Linear: ephapax-linear) or may be dropped + (Affine: ephapax-affine). Same syntax, same semantics — different + admissible derivations. Linear ⊆ Affine, proved by `linear_to_affine` + Qed in `formal/Modality.v`. + +| **L3 — Irreversibility residue (Echo)** +| Operations that erase information (region exit, drop) produce + proof-relevant residue — `Echo f y := Σ A (λ x → f x ≡ y)`. In + Linear mode the residue must be observed; in Affine mode it may be + silently lowered. Calculus mechanised in `formal/Echo.v`; + integration into the typing judgment is the next-block work. + +| **L4 — Dyadic interaction mode** +| A project-level declaration of which side of the dyad the program + speaks from (`ephapax_linear` / `ephapax_affine` / + `module_boundary_mix`). Selects the L2 modality and the L3 + observation discipline. No proof obligations of its own — mechanical + scaffold in `formal/L4.v` carries definitions only by design. +|=== + +.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. +**** + == Three superpowers The L3 echo / residue layer (Ephapax's contribution to the four-layer