diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index 1bb6069..45734eb 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -149,21 +149,70 @@ for refutation budgets (`docs/proof-debt.adoc` §(b) in that repo). close — namely the affine side, which needs L2 + the weakening lemma). +=== `formal/Semantics_L1.v` — in-flight L1 admits (post-#176 L2 hybrid) + +After the L2 hybrid landing (#176), main's `Semantics_L1.v` carries +the following escape-hatch sites. All are tracked, structurally +diagnosed, and sequenced under the four-layer redesign plan. + +NOTE: line numbers are point-in-time and may shift with subsequent +edits. The substring match is `file:line`; entries below cover the +current positions on main. + +* **`formal/Semantics_L1.v:343`** — `Admitted.` capping one of the + region-shrink helpers (T_Region_Active_L1 shadowed case at the + list-vs-multiset boundary). Three documented closure approaches + in-file. +* **`formal/Semantics_L1.v:400`** — `Admitted.` (related + region-shrink admit; same structural class as L343). +* **`formal/Semantics_L1.v:412`** — `Admitted.` (related). +* **`formal/Semantics_L1.v:520`** — `Admitted.` (related). +* **`formal/Semantics_L1.v:608`** — `Axiom region_liveness_at_split_l1`. + Documented in-file as universally false; the residual obstacle is + T_Region_Active_L1 with binder=rv. Three closure paths documented: + (i) restate with `no_region_active_pop_of rv e` side condition, + (ii) multi-set `region_env`, (iii) weaker contextual signature. + L1.G follow-up converts this to a Lemma + 1 narrow admit (per + PR #178 / its main re-port). +* **`formal/Semantics_L1.v:632`** — `Admitted.` capping + `preservation_l1` (related to L1.G's gap above; L2-gated per + §5.1 — closes once L2 Phase 2's effect-typed `TFun` lands). +* **`formal/Semantics_L1.v:703`** — `admit.` inside `preservation_l1` + for one of the lambda-rigidity admits (S_App_Step2 / S_Pair_Step2 + per §4.8 + §5.1). +* **`formal/Semantics_L1.v:704`** — `Admitted.` capping + `preservation_l1` (same lambda-rigidity gap). + +All are tracked in the L1 closure plan and sequenced under the +four-layer redesign. None are soundness-relevant in the legacy +`Semantics.v`; they live entirely on the L1 redesign side. + +=== `formal/Echo.v` — L3 layer K dependency CLOSED 2026-05-27 + +PR #173 (design branch) / its main re-port discharged the +`Eqdep.Eq_rect_eq` (K / UIP) dependency in `mode_le_trans` + +`degrade_mode_comp` via the motive-trick K-free template from +`formal/Modality.v`. **All Echo.v lemmas are now closed under the +global context** — zero K, zero UIP, zero axioms. Entry kept here +for historical visibility; no current escape hatch in `Echo.v`. + == What this repo does *not* establish today Per `formal/PRESERVATION-DESIGN.md` §12.15.4, even after the in-flight L1 work lands, the following remain open and are tracked here so downstream consumers do not overclaim: -* The `ephapax-affine` sublanguage is not separately mechanised. - Rust `LinearChecker` and `AffineChecker` are independent - (behavioural tests only); the Coq judgment covers a single - judgment resembling linear discipline. The Linear ⇒ Affine lemma - is L2 work, not L1. -* No mechanised correspondence between the Rust checkers and the Coq - judgment. -* L3 `formal/Echo.v` does not exist; the theory lives upstream at - `hyperpolymath/echo-types`. +* The `ephapax-affine` sublanguage's mechanisation in `formal/` + exists (post-#176: `has_type_l1` carries the modality parameter, + `linear_to_affine : has_type_l1 Linear ... → has_type_l1 Affine ...` + is Qed, mode-specific T_Lam_L1_*, T_Case_L1_*, T_If_L1_* land). + The Rust `AffineChecker` is independent (behavioural tests only); + no mechanised correspondence between the Rust checkers and the + Coq judgment. +* L3 `formal/Echo.v` mechanises the residue type former layer per + PRESERVATION-DESIGN.md §6 (Mode, LEcho, weaken, EchoR + headline + `no_section_collapse_to_residue`). Type-former integration into + Syntax.v / Typing.v / Semantics.v is forward-looking. * L4 mode-elaboration soundness is a research track, not scheduled. Per the policy schema, these are *plan items* rather than (d) DEBT diff --git a/formal/PRESERVATION-DESIGN.md b/formal/PRESERVATION-DESIGN.md index 8768114..83b45d4 100644 --- a/formal/PRESERVATION-DESIGN.md +++ b/formal/PRESERVATION-DESIGN.md @@ -317,6 +317,35 @@ proof-engineering gap but a calculus-design gap. The L1.E PR documents this in-source. None of (1)/(2)/(3) is in scope for the L1 minimal-fix; each is a follow-up. See ROADMAP for sequencing. +### 4.8.1 Resolution path (3) landed 2026-05-27 — and what it does not close + +`T_Var_Lin_L1` and `T_Var_Unr_L1` were strengthened with the premise +`forall r, In r (free_regions T) -> In r R` (originally as PR #170 +on the design branch, subsumed into the m-indexed main via #176). +The strengthening: + +- **Closes the source-level soundness gap**: programs like + + let_lin x = (ELoc 0 "r") in (ELet (ERegion "r" (EI32 5)) (EDrop (EVar 1))) + + no longer type, because the `EDrop (EVar 1)` site fails the + variable rule's new well-formedness premise at R = `[]`. + +What the strengthening does **not** close: the +`region_liveness_at_split_l1` lemma's residual admit (formerly the +opaque `Axiom`, converted to an Admitted Lemma with 28-of-29 cases +proved concretely in the L1.G follow-up). An empirical closure +attempt closes most cases trivially via the IH chain, but the +T_Region_Active_L1 case with `binder = rv` exhibits a real +counterexample even under the strengthened judgment: + + ERegion rv (EI32 5) : TBase TI32 — In rv R, In rv R' = False + (because remove_first_L1 pops the only rv) + +Three follow-up paths (side-conditioned lemma, multi-set R, +contextual weaker signature) remain L1 follow-up work, independent +of and additional to this §4.8 resolution. + --- ## 5. Layer 2 in detail — Linear vs Affine modality @@ -376,7 +405,7 @@ recipe (echo-types' `degradeMode-comp`, `EchoLinear.agda:93-101`). | Property | Ephapax-Linear | Ephapax-Affine | |---|---|---| -| Preservation | ✓ (L1 fix) | ✓ (same fix; Affine derivations are L1-safe by weakening) | +| Preservation | ✓ (L1 fix, *conditional on §5.1*) | ✓ (same fix; Affine derivations are L1-safe by weakening) | | Progress | ✓ | ✓ | | **No-leak** (every introduced linear value is consumed) | proved | does **not** hold; replaced by "no-duplicate" | | **No-duplicate** | trivially (Linear ⇒ no-duplicate) | proved as a structural property | @@ -387,6 +416,69 @@ Cross-mode: the Linear ⇒ Affine weakening lemma is a single induction. Combined with monomode preservation, this gives Affine preservation for free. +### 5.1 Cross-layer dependency: L1's lambda-rigidity gap closes at L2 + +The "Preservation ✓ (L1 fix)" cell above is **not realised by L1 alone**. +`formal/Semantics_L1.v`'s `preservation_l1` is currently `Admitted` +because of three internal admits in its proof body: + +- `S_StringConcat_Step2` — tractable; needs a + `step_pop_disjoint_from_type_l1` lemma. +- `S_App_Step2` and `S_Pair_Step2` — the **lambda-rigidity gap** per + §4.8: `T_Lam_L1_*` fixes the body's region environment at lambda- + creation time; the rules give no way to re-derive the lambda's + typing at a shifted `R'` after the inner step. + +§4.8.1 records that path (3) — strengthening `T_Var_*_L1` — landed +2026-05-27 via PR #170 (and subsumed via #176). It closes the +source-level *variable* soundness gap but leaves the lambda-body +case open because the body's typing is fixed at `T_Lam_L1_*`- +introduction, not at variable-use. Path (3) is necessary but **not +sufficient**. + +**Path (1) — effect-typed lambdas — is L2 Phase 2's mechanism.** The +mode-specific `T_Lam_L1_Linear` / `T_Lam_L1_Affine` constructors +should carry an annotation of the body's region effect (how `R` +shifts through the body). Concretely, the lambda type would extend +from + +``` +TFun T1 T2 +``` + +to + +``` +TFun T1 T2 (R_in : region_env) (R_out : region_env) +``` + +(or an equivalent abstract `Effect` parameter). At application time, +`T_App_L1` would consume `R_in` and produce `R_out`, threading the +region change properly. This lets `S_App_Step2`'s preservation +close: the lambda's typing at the post-step `R'` is derived from the +recorded effect, not blocked by rigid `T_Lam` introduction. + +**Sequencing.** The current `T_Lam_L1_*` rules (per the L2 mode- +split table above) carry only the per-type-flag changes. The +effect-typed `TFun` is an additional, orthogonal extension planned +for L2 Phase 2. When it lands, the L1 preservation closure can +return and discharge the lambda-rigidity admits in +`Semantics_L1.v`. + +**Why this isn't L1's job.** Effect-typed function types are a +typing-layer property, not a region-layer property. Adding them to +L1's unparameterised judgment would conflate the two. L2 is the +natural home: the modality parameter is *already* a typing-layer +decoration; the effect annotation rides alongside it. After L2's +effect-typed TFun lands, L1's gap closes by importation, not by +re-deriving L1. + +Until that follow-up lands, the §5 table's "Preservation ✓" should +be read as "achievable under the L1 architecture once L2 effect- +typed lambdas are introduced". The Linear ⇒ Affine weakening +(`linear_to_affine` Qed, PR #176) is independent of this dependency +and already ships. + --- ## 6. Layer 3 — Echo / residue, in design diff --git a/formal/PROOF-STATUS.a2ml b/formal/PROOF-STATUS.a2ml index dddef64..6f6b71a 100644 --- a/formal/PROOF-STATUS.a2ml +++ b/formal/PROOF-STATUS.a2ml @@ -3,18 +3,20 @@ # # PROOF-STATUS.a2ml — machine-readable Coq proof state # -# Snapshot of formal/*.v as of 2026-05-27 (post-L1.A through L1.F). +# Snapshot of formal/*.v as of 2026-05-27 (post-L1.A through L1.F, +# post-#176 L2 hybrid, post-#180 K-free Echo.v, post-#181 Axiom→Lemma). # Consumed by automated proof-debt trackers, status dashboards, and # CI gates that need to know "what counts as proven here". # -# Human-readable companion: formal/PRESERVATION-DESIGN.md §4.7 and §4.8. +# Human-readable companion: formal/PRESERVATION-DESIGN.md §4.7, §4.8, +# §4.8.1, §5.1. [metadata] -version = "1.0.0" +version = "1.1.0" snapshot-date = "2026-05-27" -design-branch = "proof/l1-region-threading-design" spec-doc = "formal/PRESERVATION-DESIGN.md" counterexample = "formal/Counterexample.v" +note = "Design-branch is superseded by main's L2 hybrid (#176/#177). All L1+L2+L3 work now lives on main." # ============================================================================ # FILES — what's in formal/ and its proof-status posture @@ -61,12 +63,36 @@ note = "Legacy preservation has 1 residual admit (S_Region_Step + T_Region_Activ [[files]] path = "formal/Semantics_L1.v" -purpose = "L1 preservation theorem + helpers" +purpose = "L1 preservation theorem + helpers (now m-indexed per #176)" status = "active" -admit-count = 4 -axiom-count = 1 -admitted-lemma-count = 2 -landed-in = ["PR-157", "PR-158", "PR-159", "PR-160", "PR-161", "PR-162", "PR-163"] +admit-count = 4 # post-#181: 1 in region_liveness_at_split_l1_gen + 3 lambda-rigidity in preservation_l1 +axiom-count = 0 # post-#181: Axiom region_liveness_at_split_l1 → Lemma + 1 admit +admitted-lemma-count = 3 # region_shrink_..._gen + region_liveness_at_split_l1_gen + preservation_l1 +landed-in = ["PR-157", "PR-158", "PR-159", "PR-160", "PR-161", "PR-162", "PR-163", "PR-176", "PR-181"] + +[[files]] +path = "formal/Modality.v" +purpose = "L2 modality datatype + thin-poset (Linear ≤ Affine)" +status = "stable" +qed-only = true +landed-in = ["PR-168", "PR-176"] +note = "K-free throughout. All Qed lemmas (refl/trans/prop) closed under the global context." + +[[files]] +path = "formal/TypingL2.v" +purpose = "L2 has_type_l2 modality-indexed judgment skeleton" +status = "stable" +qed-only = true +landed-in = "PR-168" +note = "Single L2_lift_l1 constructor + weaken_modality Qed (zero axioms). Mode-specific T_Lam_*, T_Case_*, T_If_* now live directly on m-indexed has_type_l1 per #176; this file's role is to be the cross-layer entry point for callers wanting the L2 framing explicitly." + +[[files]] +path = "formal/Echo.v" +purpose = "L3 residue/echo type former — forward-looking scaffold" +status = "stable" +qed-only = true +landed-in = ["PR-166", "PR-167", "PR-180"] +note = "K-free throughout (post-#180/#173). Headlines: Echo fiber, LEcho mode-polymorphic carrier, weaken Linear→Affine, EchoR + collapse_to_residue + no_section_collapse_to_residue (the irreversibility theorem; closed under the global context, zero axioms)." # ============================================================================ # L1 PROOF CHAIN — Qed lemmas @@ -181,11 +207,12 @@ follow-up = "see PRESERVATION-DESIGN.md §4.8" [[proof-debt]] id = "L1.C-region-liveness" file = "Semantics_L1.v" -line-anchor = "region_liveness_at_split_l1 (Axiom)" -class = "carry-invariant-through-induction" +line-anchor = "region_liveness_at_split_l1_gen T_Region_Active_L1 r=rv (post-#181)" +class = "structurally-false-as-universal" 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" +diagnosis = "ERegion rv (EI32 5) at R = [rv] gives In rv R but In rv R' = False (the rule pops the only rv from R_body). The Lemma's universal statement is false in this sub-case; 28/29 cases proved concretely via PR #181." +closes-when = "one of (i) restate with a no_region_active_pop_of rv e side condition + discharge at the 9 call sites in subst_typing_gen_l1, (ii) multi-set region_env, (iii) weaker contextual signature" +status-history = "Axiom (pre-#181) → Lemma with 1 narrow admit (post-#181). Transparency improvement, not soundness." # ============================================================================ # DOCUMENTATION POINTERS