From 450704250d78e50af629055615e631be5c05f12b Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 31 May 2026 00:15:46 +0100 Subject: [PATCH] =?UTF-8?q?docs(README):=20add=20`=3D=3D=20The=20four=20la?= =?UTF-8?q?yers`=20section=20per=20PRESERVATION-DESIGN=20=C2=A712.2=20+=20?= =?UTF-8?q?L4=20truth=20fix?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Executes `formal/PRESERVATION-DESIGN.md` §12.2 steps 1-4 verbatim: 1. Add a new `== The four layers` section between `== What this is` and `== Three superpowers`, listing L1-L4 in a `[cols="1,3"]` table. 2. Update the "Dyadic discipline" row to label `(L2)` and cross-reference the new section. 3. Replace the "Region-based memory" row with the L1 framing (capability threading + sibling region-exit invariant). 4. Add the "Soundness story" footnote block linking the four-layer separation to the verified counterexample. Also fixes a stale truth claim on line 66: "`L4` (dyadic mode) not started" → scaffold has landed (`formal/L4.v` carries `ProgramMode` + `program_mode_to_modality`). Source authority: `formal/PRESERVATION-DESIGN.md §12.2` (the rollout spec) + `formal/L4-DYADIC.md` (which prescribes L4 as definitions-only by design, hence no proof obligations claim in the README table). No proof, code, or workflow changes. Pure documentation rollout. Closes the README half of `PRESERVATION-DESIGN.md §12.2`; companion edits to EXPLAINME.adoc / ROADMAP.adoc / SPEC.md are §12.3-12.7 and not in scope of this PR. Co-Authored-By: Claude Opus 4.7 (1M context) --- README.adoc | 71 +++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 64 insertions(+), 7 deletions(-) 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