docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β

.machine_readable/6a2/STATE.a2ml

@@ -6,8 +6,8 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase D slice 4 Phase 4b — ground-non-linear T1 path for the `T_App_L2_Eff` β-case (uses Phase 2's `subst_typing_gen_l1_m_ground_nonlinear`). Then Phase 4c (TFunEff non-linear T1, blocked on Phase 3b per issue #225) and Phase 4d (compound, deferred to Phase 5). Phase 4a (this slot's predecessor) shipped `preservation_l2_app_eff_beta_linear_l1` + `preservation_l2_app_eff_beta_linear` in TypingL2.v, closing the β-case for linear T1. Phase 3b is still parked at issue #225 with three candidate solutions; Phase 4a prototyping confirmed the substitution shape used for linear T1 (k=0, raw cons in Gin/Gout, m-poly via `linear_value_retype_l1_m` for the Affine branch). For 3b, the actual subst shape will mirror Phase 4a's but with the value being a TFunEff lambda — the substitution premise will need a TFunEff-typed substituend at the threaded R, with the side condition propagating through. Recommend prototyping Phase 4c next (it forces 3b's design hand). Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
-last_action: "Phase D slice 4 Phase 4a LANDED (2026-05-30, this PR): `preservation_l2_app_eff_beta_linear_l1` + `preservation_l2_app_eff_beta_linear` added to `formal/TypingL2.v`. The L1-level kernel takes inverted T_App_L2_Eff premises (a TFunEff lambda + a value argument typed at linear T1) and produces the post-β L1 typing via `subst_typing_gen_l1_m` at k=0. The L2 wrapper inverts both has_type_l2 hypotheses through L2_lift_l1 (T_App_L2_Eff discriminates: lambda's head is ELam not EApp; argument is a value so cannot be EApp). Two structural reductions inside the kernel: inversion on Hlam forces T_Lam_L1_*_Eff (the only formation rules producing TFunEff), exposing body typing at R_in; `value_R_G_preserving_l1` on Harg collapses R_in→R, G''→G. Then subst at k=0 with raw cons in the `with` clause (ctx_extend was too opaque for unification of remove_at 0 _ = G'') — and for the Affine branch, the linear v2 is re-derived at Linear mode via local helper `linear_value_retype_l1_m` (because subst_typing_gen_l1_m's premise 5 uses the bare `|=L1` notation which is Linear-mode-only). The same PR hotfixes a duplicate `tfuneff_lambda_retype_l1_m` from PR #223 + PR #224 (parallel-session merge collision); kept the chronologically-first definition (Hval, Ht, HR' arg order) and removed the second. Coqc 8.18.0 clean rebuild across all 10 .v files. Zero new admits/axioms (Print Assumptions confirms only the pre-existing `region_liveness_at_split_l1_gen` axiom inherited via `subst_typing_gen_l1_m`). `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. Phase 4a is clean infrastructure composable with `preservation_l2_via_l1` toward full `preservation_l2` over has_type_l2."
+next_action: "Phase D slice 4 Phase 3b — implement `subst_typing_gen_l1_m_tfuneff` with option (a)'s precondition `(forall r, In r (regions_introduced_by e) -> In r R_in_v)`. Per the parallel session's analysis (PR #230's body), this is ~400 lines mirroring Phase 2 with `shift_typing_gen_l1_m` threading at every binder-descent case (Phase 2's `ground_nonlinear_value_shift_id_l1` shortcut doesn't apply to non-scalar TFunEff lambdas — `shift c 1 (ELam T0 e0) = ELam T0 (shift (S c) 1 e0)`, which changes body's de Bruijn indices). The precondition propagates through compound rules (sub-expressions' `regions_introduced_by` are subsets of the parent's) and discharges directly at the T_Region_L1 case. After Phase 3b: Phase 4c wraps preservation_l2's T_App_L2_Eff β-case CONDITIONALLY — requiring the precondition `regions_introduced_by(ebody) ⊆ R_in_v`. Programs not satisfying it form a documented soundness-gap class per `Counterexample_L2.v` (this slot's predecessor, this PR). Phase 4d (compound non-linear) deferred to Phase 5. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
+last_action: "Phase D slice 4 Phase 4c soundness-gap counterexample LANDED (2026-05-30, this PR): `formal/Counterexample_L2.v` with three Qed lemmas (`e_before_typed`, `e_step`, `e_after_untypable`) mechanising preservation_l2's failure for TFunEff substituends inside fresh-region scopes. Configuration: outer = ELam (TFunEff TUnit TUnit [] []) (ERegion r2 (EVar 0)); v2 = ELam TUnit EUnit; e_before = EApp outer v2 (types at TFunEff via T_App_L2_Eff); e_after = ERegion r2 v2 (β-result, does NOT type because T_Lam_L1_*_Eff's side condition `forall r, In r [r2] -> In r []` is violated). The structural mechanism: T_Region_L1's `~ In r (free_regions T)` premise prevents fresh r from being in R_in_v ⊆ free_regions(TFunEff), so the post-β term's inner TFunEff value cannot re-type at the new R. Phase 4b (parallel session #233) also LANDED on 2026-05-30. SUBST-LEMMA-GENERALIZATION-DESIGN.md gained a Phase 4c addendum documenting the conditional preservation_l2 path and three resolution options. Counterexample_L2.v added to formal/_CoqProject after TypingL2.v. Coqc 8.18.0 clean rebuild across all 11 .v files. Zero new admits/axioms (`Print Assumptions` confirms all three lemmas Closed under the global context). `Semantics.v`/`Typing.v`/`Counterexample.v` (legacy) untouched. The mechanised counterexample is the L1/L2 analogue of Counterexample.v for the legacy preservation, providing rigorous justification for the conditional Phase 4c statement."
 updated: 2026-05-30T00:00:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):

formal/Counterexample_L2.v

@@ -0,0 +1,202 @@
+(* SPDX-License-Identifier: PMPL-1.0-or-later *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
+
+(** * Soundness gap (L2): preservation_l2 fails for TFunEff substituends
+      inside fresh-region scopes
+
+    The Phase D slice 4 Phase 4c β-case of preservation_l2 fails for
+    programs that substitute a TFunEff value into a body containing
+    [ERegion] (fresh-region) introduction.
+
+    This file mechanises the counterexample. It mirrors the structure
+    of [Counterexample.v] (which exhibits the legacy preservation's
+    soundness gap) but at the L1/L2 layer with the post-redesign
+    [has_type_l1] / [has_type_l2] judgments. The artifact justifies
+    the **conditional** preservation_l2 closure recommended in
+    [SUBST-LEMMA-GENERALIZATION-DESIGN.md] §"Phase 4c": preservation
+    holds only for programs satisfying
+    [regions_introduced_by(ebody) ⊆ R_in_v]; programs outside this
+    class form a documented soundness-gap subclass.
+
+    ===== Configuration =====
+
+      T1_inner    := TFunEff TUnit TUnit [] []      (* substituee type, R_in_v = [] *)
+      outer       := ELam T1_inner (ERegion r2 (EVar 0))
+                                                    (* body introduces fresh r2, returns subst position *)
+      v2          := ELam TUnit EUnit               (* a value of type T1_inner *)
+      e_before    := EApp outer v2                  (* well-typed via T_App_L2_Eff at R = [] *)
+      e_after     := ERegion r2 v2                  (* β-result: subst 0 v2 (ERegion r2 (EVar 0)) *)
+
+    ===== Three theorems =====
+
+    - [e_before_typed] — the input types at outer type [T1_inner]
+      via T_App_L2_Eff with mode Affine.
+    - [e_step]         — operational step S_App_Fun reduces e_before
+      to e_after.
+    - [e_after_untypable] — no L1 derivation exists for e_after at
+      the same outer type. By inversion: the only ERegion-producing
+      rules at non-TEcho output are T_Region_L1 and T_Region_Active_L1;
+      T_Region_Active_L1 requires [In r2 []] (fails); T_Region_L1's
+      body premise requires v2 typed at [r2; nil], which only
+      [T_Lam_L1_*_Eff] can produce, and both rules' side condition
+      [forall r, In r [r2] -> In r R_in_v = []] is contradicted by
+      [In r2 [r2]].
+
+    ===== Owner-directive compliance =====
+
+    - Does not modify [Semantics.v] or [Counterexample.v] (the legacy
+      soundness-gap artifacts).
+    - Does not patch [Typing.v].
+    - Does not close any residual [Semantics_L1.v] admit.
+    - Adds NEW infrastructure (a new file in [formal/]) orthogonal
+      to legacy admits, mirroring the precedent of [Counterexample.v]
+      for the legacy preservation.
+    - No new [Axiom] or [Admitted] markers. *)
+
+From Ephapax Require Import Syntax Typing TypingL1 Modality Semantics Semantics_L1 TypingL2.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Import ListNotations.
+Open Scope string_scope.
+
+Section CounterexampleL2.
+
+  Definition r2 : region_name := "r2".
+
+  (** Substituee type — a TFunEff lambda with empty input region env. *)
+  Definition T1_inner : ty :=
+    TFunEff (TBase TUnit) (TBase TUnit) [] [].
+
+  (** Outer lambda: takes a [T1_inner]-typed argument, returns it
+      inside a fresh-region scope [ERegion r2]. The bound variable
+      is referenced at de Bruijn index 0 inside the region scope. *)
+  Definition outer : expr :=
+    ELam T1_inner (ERegion r2 (EVar 0)).
+
+  (** Argument: a TFunEff lambda of type [T1_inner]. The body
+      [EUnit] is trivially typed at any R. *)
+  Definition v2 : expr :=
+    ELam (TBase TUnit) EUnit.
+
+  (** Pre-step term. *)
+  Definition e_before : expr := EApp outer v2.
+
+  (** Post-β term: [subst 0 v2 (ERegion r2 (EVar 0))]
+      [= ERegion r2 (subst 0 v2 (EVar 0))]  (* ERegion isn't a binder *)
+      [= ERegion r2 v2]                     (* EVar 0 substitutes to v2 *) *)
+  Definition e_after : expr := ERegion r2 v2.
+
+  (** Helper: v2 types at [T1_inner] at any R (it's a closed value
+      whose formation side condition has R_in_v = [] so [R ⊆ []]
+      means R = []). For the proof below we only need v2 at R = []
+      and at R = [r2] — the latter is what fails. *)
+
+  Lemma v2_typed_at_empty :
+    has_type_l1 Affine [] [] v2 T1_inner [] [].
+  Proof.
+    unfold v2, T1_inner.
+    eapply T_Lam_L1_Affine_Eff with (u := false).
+    - intros r Hr; inversion Hr.
+    - apply T_Unit_L1.
+  Qed.
+
+  (** Outer lambda is well-typed at [TFunEff T1_inner T1_inner [] []]. *)
+
+  Lemma outer_typed :
+    has_type_l1 Affine [] [] outer
+                (TFunEff T1_inner T1_inner [] []) [] [].
+  Proof.
+    unfold outer.
+    eapply T_Lam_L1_Affine_Eff with (u := false).
+    - intros r Hr; inversion Hr.
+    - eapply T_Region_L1 with (R_body := [r2]).
+      + intros Hr; inversion Hr.
+      + simpl. intros Hr. inversion Hr.
+      + left; reflexivity.
+      + eapply T_Var_Unr_L1.
+        * unfold ctx_lookup; simpl. reflexivity.
+        * reflexivity.
+  Qed.
+
+  (** ===== (a) e_before is well-typed via T_App_L2_Eff ===== *)
+
+  Lemma e_before_typed :
+    has_type_l2 Affine [] [] e_before T1_inner [] [].
+  Proof.
+    unfold e_before.
+    eapply T_App_L2_Eff.
+    - apply L2_lift_l1. exact outer_typed.
+    - apply L2_lift_l1. exact v2_typed_at_empty.
+  Qed.
+
+  (** ===== (b) The β-step from e_before to e_after ===== *)
+
+  Lemma e_step :
+    forall mu, step (mu, [], e_before) (mu, [], e_after).
+  Proof.
+    intros mu. unfold e_before, e_after, outer.
+    (* [subst 0 v2 (ERegion r2 (EVar 0))] reduces to [ERegion r2 v2]
+       by the [subst] Fixpoint (ERegion is not a binder so no shift). *)
+    change (ERegion r2 v2) with (subst 0 v2 (ERegion r2 (EVar 0))).
+    apply S_App_Fun. unfold v2. apply VLam.
+  Qed.
+
+  (** ===== (c) e_after does NOT type at the same outer type =====
+
+      No L1 derivation exists for [[] ; [] |=L1[Affine] e_after :
+      T1_inner -| ?R_out; ?G_out].
+
+      Proof by inversion on the assumed derivation. ERegion expressions
+      are produced by exactly four constructors:
+      - [T_Region_L1]        — output type [T] (matches T1_inner)
+      - [T_Region_Active_L1] — output type [T] (matches but requires
+                                [In r2 []], false)
+      - [T_Region_L1_Echo]   — output type [TEcho T] (≠ T1_inner)
+      - [T_Region_Active_L1_Echo] — output type [TEcho T] (≠ T1_inner)
+
+      The two Echo cases discriminate on the output-type equation.
+      The T_Region_Active_L1 case fails [In r2 []].
+      The T_Region_L1 case requires v2 typed at [r2; nil]; v2 = ELam
+      types only via [T_Lam_L1_*_Eff], both of whose side conditions
+      [forall r, In r [r2] -> In r R_in_v = []] are contradicted by
+      [In r2 [r2]]. *)
+
+  Lemma e_after_untypable :
+    forall R_out G_out,
+      ~ has_type_l1 Affine [] [] e_after T1_inner R_out G_out.
+  Proof.
+    intros R_out G_out Ht.
+    unfold e_after, v2, T1_inner in Ht.
+    inversion Ht; subst.
+    - (* T_Region_L1 case: body v2 typed at [r2;nil]. *)
+      match goal with
+      | [ Hbody : has_type_l1 _ (r2 :: _) _ (ELam _ _) _ _ _ |- _ ] =>
+          rename Hbody into Hv2_inner
+      end.
+      inversion Hv2_inner; subst.
+      (* Only T_Lam_L1_Affine_Eff survives — T_Lam_L1_Linear / _Affine
+         produce TFun (discriminated), and T_Lam_L1_Linear_Eff is mode
+         Linear (discriminated against Hv2_inner's Affine mode). *)
+      match goal with
+      | [ Hside : forall r, In r (r2 :: nil) -> In r nil |- _ ] =>
+          specialize (Hside r2 (or_introl eq_refl)); inversion Hside
+      end.
+    - (* T_Region_Active_L1 case: requires In r2 nil, false. *)
+      match goal with
+      | [ Hr2_in_R : In r2 nil |- _ ] => inversion Hr2_in_R
+      end.
+  Qed.
+
+  (** ===== Soundness-gap witness =====
+
+      The three lemmas above ([e_before_typed] + [e_step] +
+      [e_after_untypable]) jointly witness preservation_l2's failure
+      for the TFunEff-substituee-inside-fresh-region class. No
+      top-level conjunction theorem is stated because [has_type_l2]
+      is Type-sorted (it is proof-relevant per L2's design) while
+      [step] and [~ has_type_l1] are Prop, so a Prop-conjunction over
+      the three would require either a [prod]-based product or
+      [inhabited]-wrapping. Keeping them as three separate lemmas
+      preserves the strongest form of each statement. *)
+
+End CounterexampleL2.

formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md

@@ -159,6 +159,50 @@ With the substitution machinery in place, the T_App_L2_Eff β-case in `preservat
 
 `EPair` / `EInl` / `EInr` / `EEcho` of non-linear components. Sub-component analysis. May require additional retype machinery. Realistically multiple sessions of work.
 
+## Phase 4c addendum (2026-05-30) — conditional preservation_l2 for TFunEff β
+
+Prototyping Phase 4c on paper (after Phase 4a / 4b landed at PRs #228 / #233) revealed a structural soundness gap that requires a **conditional** preservation_l2 statement for the TFunEff β-case. `formal/Counterexample_L2.v` mechanises the witness.
+
+### The obstacle (mechanised in `Counterexample_L2.v`)
+
+For any TFunEff lambda body that introduces a fresh region via `ERegion` AND references the substituted variable inside that region scope, β-reduction does **not** preserve typing:
+
+```
+T1_inner = TFunEff TUnit TUnit [] []                       (* substituee type, R_in_v = [] *)
+outer    = ELam T1_inner (ERegion r2 (EVar 0))             (* body introduces fresh r2 *)
+v2       = ELam TUnit EUnit                                (* a value of type T1_inner *)
+e_before = EApp outer v2     (* well-typed via T_App_L2_Eff at R = [] *)
+e_after  = ERegion r2 v2     (* β-result: subst 0 v2 (ERegion r2 (EVar 0)) *)
+```
+
+`e_before` types (Qed: `e_before_typed`); `e_step` reduces it to `e_after` (Qed: `e_step`); `e_after` does not type at the same outer type (Qed: `e_after_untypable`). The mechanism: T_Region_L1's `~ In r (free_regions T)` premise prevents the fresh `r` from being in `R_in_v` (since `R_in_v ⊆ free_regions(TFunEff)`). After β-substitution, the inner expression becomes a TFunEff value that must re-type at `r :: R`, requiring `r ∈ R_in_v` (false).
+
+### Resolution: Phase 4c ships **conditionally**
+
+Preservation_l2 for the T_App_L2_Eff β-case holds **only** for programs satisfying:
+
+```
+regions_introduced_by(ebody) ⊆ R_in_v
+```
+
+where `regions_introduced_by` is the `Fixpoint` already landed in `Syntax.v` (PR #230), `ebody` is the outer lambda's body, and `R_in_v` is the substituee's TFunEff input region env.
+
+The Phase 3b substitution lemma (`subst_typing_gen_l1_m_tfuneff`) ships with this precondition; the Phase 4c β-case wrapper propagates it. Programs not satisfying the precondition are a **documented soundness-gap subclass** — they witness the same fundamental "scoped resource cannot escape its scope" limitation that motivated the four-layer redesign in the first place.
+
+### Three resolution paths (broader than original (a)/(b)/(c) options)
+
+1. **Conditional preservation_l2 (recommended)**: Phase 3b lemma takes the precondition; Phase 4c β-case requires it; programs outside form a documented soundness-gap class. This is what `Counterexample_L2.v` justifies. Aligns with the legacy `Counterexample.v` precedent (preservation holds modulo a structural constraint that legitimate programs satisfy).
+2. **Region-polymorphic TFunEff**: change the type system so `TFunEff T1 T2 R_in R_out` permits implicit region extension at use sites. Major type-system change; defers to a future redesign.
+3. **L2 region-transfer combinator**: add an L2 typing rule that explicitly transfers a fresh region into a TFunEff lambda's R_in for the duration of a scope. Adds L2 expressiveness; defers to a future PR.
+
+### What ships in the Phase 4c PR
+
+- `formal/Counterexample_L2.v` — three Qed lemmas mechanising the soundness gap.
+- This addendum to `SUBST-LEMMA-GENERALIZATION-DESIGN.md`.
+- STATE.a2ml refresh to reflect the conditional path.
+
+Phase 3b implementation (the ~400-line `subst_typing_gen_l1_m_tfuneff` lemma body) and Phase 4c β-case wrapper remain follow-up work — but the design constraint they must satisfy is now mechanically witnessed.
+
 ## What this session ships
 
 This design document only. No code changes. STATE.a2ml shifts `next_action` to "Phase 1: implement `ground_nonlinear_retype_l1_m` per `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`".

formal/_CoqProject

@@ -13,4 +13,5 @@ Counterexample.v
 Echo.v
 Modality.v
 TypingL2.v
+Counterexample_L2.v
 L4.v