|
| 1 | +<!-- SPDX-License-Identifier: PMPL-1.0-or-later --> |
| 2 | +<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> --> |
| 3 | + |
| 4 | +# Ephapax L4 — Dyadic mode (labelling discipline) |
| 5 | + |
| 6 | +> Scope: project / module-level labelling. **No proof obligations.** |
| 7 | +> Companion mechanical scaffold: [`formal/L4.v`](L4.v). |
| 8 | +> Canonical design source: [`formal/PRESERVATION-DESIGN.md §7`](PRESERVATION-DESIGN.md). |
| 9 | +
|
| 10 | +## What L4 is |
| 11 | + |
| 12 | +L4 is the outermost ring of the four-layer redesign. Where L1 / L2 / L3 |
| 13 | +each carry a typing-layer judgment or per-layer proof obligation, L4 |
| 14 | +carries **none of that**. It is a *labelling discipline* applied at the |
| 15 | +program / module boundary. |
| 16 | + |
| 17 | +A closed Ephapax program declares one of three program modes: |
| 18 | + |
| 19 | +| `ProgramMode` (L4) | Selects L2 modality | L3 echo discipline that follows | |
| 20 | +|---|---|---| |
| 21 | +| `EphapaxLinear` | `Linear` | Echoes must be **observed** before program end | |
| 22 | +| `EphapaxAffine` | `Affine` | Echoes may be observed or silently lowered | |
| 23 | +| `ModuleBoundaryMix` | per-module | Module's L2 modality determines its L3 echo discipline at each boundary crossing | |
| 24 | + |
| 25 | +The declaration tells the type checker which L2 modality `m` to thread |
| 26 | +through `has_type_l1`. Once `m` is selected, L3's echo observation |
| 27 | +discipline follows from L2 with no further user input. |
| 28 | + |
| 29 | +## Why L4 is not a separate proof layer |
| 30 | + |
| 31 | +The four-layer redesign assigns proof obligations as follows: |
| 32 | + |
| 33 | +| Layer | What it proves | Where the proof lives | |
| 34 | +|---|---|---| |
| 35 | +| **L1** | Region-capability soundness; preservation under R-threading | `formal/TypingL1.v` + `formal/Semantics_L1.v` | |
| 36 | +| **L2** | Modality lifting (Linear ⇒ Affine) | `formal/Modality.v` (`linear_to_affine` Qed) | |
| 37 | +| **L3** | Echo residue preservation under irreversible steps | `formal/Echo.v` + `preservation_l3` in `formal/Semantics_L1.v` | |
| 38 | +| **L4** | (nothing — labelling only) | `formal/L4.v` (Definitions only, no theorems) | |
| 39 | + |
| 40 | +L4 is the *user-facing surface* through which L1–L3's proofs are |
| 41 | +applied to a concrete program. Selecting `EphapaxLinear` at L4 instructs |
| 42 | +the system to: |
| 43 | + |
| 44 | +1. Choose `Linear : Modality` at L2. |
| 45 | +2. Enforce echo observation at L3. |
| 46 | +3. Apply L1's preservation theorem to the resulting derivation. |
| 47 | + |
| 48 | +No new theorem is needed at L4 because no new judgment is introduced. |
| 49 | + |
| 50 | +## The mother–child dyad |
| 51 | + |
| 52 | +The dyadic framing (PRESERVATION-DESIGN.md §7) reads the Linear / |
| 53 | +Affine pair as an **asymmetric dyad**: |
| 54 | + |
| 55 | +- **Linear** = the obligation-bearer (the *speaker* of the dyad). |
| 56 | + Linear-mode programs are responsible for discharging every echo |
| 57 | + before termination. |
| 58 | +- **Affine** = the obligation-relaxer (the *listener*). |
| 59 | + Affine-mode programs may accept, observe, or silently drop echoes — |
| 60 | + the listener has the option of not engaging. |
| 61 | + |
| 62 | +Both sides are needed because real systems contain both |
| 63 | +obligation-bearing components (resource owners, audit trails, GDPR |
| 64 | +deletion receipts) and obligation-relaxing components (loggers, UI, |
| 65 | +diagnostics that may safely vanish). |
| 66 | + |
| 67 | +The dyad **is not symmetric**: a Linear-mode component can call into |
| 68 | +an Affine-mode component (the listener silently relaxes), but an |
| 69 | +Affine-mode component cannot call into a Linear-mode component except |
| 70 | +through a designated obligation-handoff (a `ModuleBoundaryMix` |
| 71 | +declaration explicitly converts the obligation surface). |
| 72 | + |
| 73 | +This asymmetry is exactly what L2's `linear_to_affine` lemma |
| 74 | +mechanises: every Linear derivation can be viewed as an Affine |
| 75 | +derivation, but not vice versa. |
| 76 | + |
| 77 | +## Orthogonality to L1 / L2 / L3 |
| 78 | + |
| 79 | +L4 is orthogonal to the lower layers in the following sense: |
| 80 | + |
| 81 | +- **L1 (region capabilities)** is the *same* in both Linear and |
| 82 | + Affine — both must track region exit precisely for soundness. |
| 83 | + Switching L4 program mode does not change L1's invariants. |
| 84 | +- **L2 (modality)** gives the *direction* of the dyad — which side |
| 85 | + is obligation-bearing. L4 selects which L2 modality the program |
| 86 | + inhabits. |
| 87 | +- **L3 (echo)** is the *protocol* of obligation discharge — what |
| 88 | + the observer must do with the residue. L4 selects the L3 |
| 89 | + discipline indirectly through L2. |
| 90 | + |
| 91 | +## What L4 declarations look like (illustrative) |
| 92 | + |
| 93 | +L4 is currently a *design layer*. Surface syntax has not yet been |
| 94 | +wired into the parser or borrow checker. The intended shape: |
| 95 | + |
| 96 | +```ephapax |
| 97 | +// Top of a closed program, before any imports |
| 98 | +#![ephapax_linear] |
| 99 | +
|
| 100 | +// — or — |
| 101 | +
|
| 102 | +#![ephapax_affine] |
| 103 | +
|
| 104 | +// — or, at the boundary of a multi-module project — |
| 105 | +
|
| 106 | +#![module_boundary_mix(default = "ephapax_affine")] |
| 107 | +mod critical_section { |
| 108 | + #![ephapax_linear] |
| 109 | + // every echo here must be observed before this module returns |
| 110 | +} |
| 111 | +``` |
| 112 | + |
| 113 | +The mechanical surface for downstream tools is in [`formal/L4.v`](L4.v): |
| 114 | + |
| 115 | +- `ProgramMode` — three-constructor enum (`PModeLinear` / |
| 116 | + `PModeAffine` / `PModeBoundaryMix`). |
| 117 | +- `program_mode_to_modality` — total function `ProgramMode -> Modality` |
| 118 | + (with `PModeBoundaryMix` mapped to a default; per-module modality is |
| 119 | + read from the surrounding declaration). |
| 120 | +- No theorems; no admit; no axiom. |
| 121 | + |
| 122 | +## What L4 does NOT do |
| 123 | + |
| 124 | +L4 introduces **zero** new proof obligations. In particular: |
| 125 | + |
| 126 | +- L4 does NOT introduce a new typing judgment. |
| 127 | +- L4 does NOT introduce a new step relation. |
| 128 | +- L4 does NOT introduce a new preservation theorem. |
| 129 | +- L4 does NOT introduce a new echo discipline. |
| 130 | +- L4 does NOT change the L1 region-threading invariants. |
| 131 | +- L4 does NOT change the L2 modality-lifting lemma. |
| 132 | + |
| 133 | +If a question about L4 leads to a proof obligation, the question is |
| 134 | +not about L4 — it is about whichever lower layer the obligation lives |
| 135 | +in (probably L2 if it concerns modality lifting, or L3 if it concerns |
| 136 | +echo discipline). |
| 137 | + |
| 138 | +## Cross-references |
| 139 | + |
| 140 | +- [`formal/PRESERVATION-DESIGN.md §7`](PRESERVATION-DESIGN.md) — |
| 141 | + canonical design source. |
| 142 | +- [`formal/PRESERVATION-DESIGN.md §8`](PRESERVATION-DESIGN.md) — |
| 143 | + per-layer proof-need separation between Linear and Affine. |
| 144 | +- [`formal/L4.v`](L4.v) — the mechanical scaffold (Definitions only). |
| 145 | +- [`formal/Modality.v`](Modality.v) — L2 thin poset; selected by L4. |
| 146 | +- [`formal/Echo.v`](Echo.v) — L3 echo calculus; discipline selected |
| 147 | + by L2. |
| 148 | +- [`CLAUDE.md`](../CLAUDE.md) — agent guidance; owner directive |
| 149 | + 2026-05-27 (no patching of legacy preservation). |
| 150 | +- [`PROOF-NEEDS.md`](../PROOF-NEEDS.md) — proof-debt accounting. |
0 commit comments