From 39cf0779651e34ade24d7f0605c34b6d49252257 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 31 May 2026 00:40:36 +0100
Subject: [PATCH] =?UTF-8?q?docs(ROADMAP):=20add=20`Four-layer=20redesign`?=
 =?UTF-8?q?=20section=20per=20PRESERVATION-DESIGN=20=C2=A712.5?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Executes `formal/PRESERVATION-DESIGN.md` §12.5 — the ROADMAP rollout.

Insert a new top-level section between the status snapshot and the
formal-proof-status section titled `== Four-layer redesign
(2026-05-26 → )`. The section structures the L1/L2/L3/L4
implementation order with a per-layer status:

- L1 — Region capability threading: landed (judgment + step
  relation in `TypingL1.v` + `Semantics_L1.v`); 9 admits remain.
- L2 — Modality parameter: landed (PRs #176 + #177); `linear_to_affine`
  Qed zero axioms.
- L3 — Echo residue: calculus mechanised (`Echo.v`); typing-rule
  integration is next-block work.
- L4 — Mode declaration: mechanical scaffold landed (`L4.v`); surface
  syntax not yet wired.

Per the spec's §12.5 prescription, the previous "Preservation
closure plan" framing is acknowledged as archived (pointing to
`PRESERVATION-HANDOFF.md` for the historical record). The
pre-existing `[#preservation-closure-plan]` section was already
labelled superseded by a prior commit — this new top section
provides the *forward-looking* organisation that the old framing
lacked.

No proof, code, workflow, or schema changes. Pure documentation
rollout. Companion to README #256 (§12.2), EXPLAINME #257 (§12.3),
and vision #258 (§12.4).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 ROADMAP.adoc | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/ROADMAP.adoc b/ROADMAP.adoc
index 6202f37..6e9beed 100644
--- a/ROADMAP.adoc
+++ b/ROADMAP.adoc
@@ -18,6 +18,60 @@ Ephapax is an early-development linear-type language implemented across
 IR, two-phase pipeline, Zig FFI, and conformance test suite are
 complete. Type checker and WASM code generation are in progress.
 
+== Four-layer redesign (2026-05-26 → )
+
+The verified preservation counterexample
+(`formal/Counterexample.v`, three `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.
+
+. *L1 — Region capability threading*
++
+- Restate the typing judgment to thread `R_in / R_out` (the
+  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.
+
+. *L2 — Modality parameter*
++
+- Promote the per-type `is_linear_ty` predicate to a judgment
+  parameter `m : Modality`.
+- Mechanise `linear_to_affine : Linear ≤ Affine` as a single
+  induction.
+- Status: landed in-place via PRs #176 + #177; `linear_to_affine`
+  Qed with zero axioms.
+
+. *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.
+
+. *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`.
+- 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
+#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`.
+
 == Formal-proof status
 
 === Coq (`formal/`)