diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 3738709..380824c 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,8 +6,8 @@ @state(version="2.0"): phase: "implementation" -next_action: "Phase D slice 4 Phase 3b Stage 1 (per #239): implement leaf-only Phase 3b. (a) NEW Fixpoint `tfuneff_lambda_free : expr -> bool` in `formal/Syntax.v` (~10 lines). (b) NEW `subst_typing_gen_l1_m_tfuneff` Qed in `formal/Semantics_L1.v` mirroring `subst_typing_gen_l1_m_ground_nonlinear` (~300 lines); inner T_Lam_L1_*_Eff cases exfalso via the `tfuneff_lambda_free` precondition; direct (P1, P2) hypothesis form (no CPS yet — Stage 3 introduces CPS). (c) NEW `preservation_l2_app_eff_beta_tfuneff_l1` + L2 wrapper Qed in `formal/TypingL2.v` under the 2-condition statement: `tfuneff_lambda_free ebody = true ∧ regions_introduced_by ebody ⊆ R_in_v`. (d) NEW `formal/Counterexample_L2_nested.v` (parallel to Counterexample_L2.v) mechanising the nested-TFunEff soundness gap — 3 Qed lemmas, zero axioms. (e) Add to `_CoqProject` after `Counterexample_L2.v`. (f) STATE/design-doc updates. Owner-approved 2026-05-30 PM via the 4-stage staged plan superseding the original three options. Stages 2-4 (#240/#241/#242) tracked but NOT actioned this session. 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 — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority." -last_action: "Phase D slice 4 Phase 3b 4-stage resolution plan LANDED (2026-05-30 PM, this PR + cross-issue filings): SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b addendum (gap finding + 3-options framing) + Phase 3b resolution addendum (4-stage plan superseding 3-options) + STATE.a2ml refresh. Cross-issue filings: #235 (parent finding) + #239 (Stage 1 leaf-only Phase 3b, green-lit) + #240 (Stage 2 ELam annotation, parallel L4 track) + #241 (Stage 3 relaxed Phase 3b + CPS, blocked on #240) + #242 (Stage 4 compound non-linear + unconditional preservation_l2, blocked on #241). The 4-stage plan harvests all three Interesting values: L4-alignment (Stage 2 via ELam annotation), higher-order proof style (Stage 3 via CPS), principled deferral + honest 2-condition statement (Stage 1 immediate). Stage 1 ships unblocked preservation_l2 β-case for leaf-only ebody with two mechanised counterexamples (`Counterexample_L2.v` for fresh-region gap, new `Counterexample_L2_nested.v` for nested-lambda gap). No `formal/*.v` changes in this PR (Stage 1 implementation ships next session). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ escalation-then-resolution per CLAUDE.md §DO #4; ✅ anti-pattern detector clean across all four stages. Coqc 8.18.0 unaffected (no code changes)." +next_action: "Phase D slice 4 Phase 3b Stage 1b (sibling to #239 — file as follow-up sub-issue): implement the deferred substitution-lemma half. (a) `closed_value_typing_G_poly_l1_m` helper in `formal/Semantics_L1.v` (G-polymorphic retype for closed TFunEff values, addressing the structural blocker discovered in Stage 1a). (b) `subst_typing_gen_l1_m_tfuneff` Qed mirroring `subst_typing_gen_l1_m_ground_nonlinear` (~300 lines); inner T_Lam_L1_*_Eff cases exfalso via the `tfuneff_lambda_free` precondition; direct (P1, P2) hypothesis form (no CPS yet — Stage 3 introduces CPS). May add a third precondition `expr_closed_below 0 v = true` to handle the G-mismatch at compound binder rules; document as Stage 1 restriction lifted in Stage 3/4. (c) `preservation_l2_app_eff_beta_tfuneff_l1` + L2 wrapper Qed in `formal/TypingL2.v` under the 2-condition statement: `tfuneff_lambda_free ebody = true ∧ regions_introduced_by ebody ⊆ R_in_v`. 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 — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority." +last_action: "Phase D slice 4 Phase 3b Stage 1a LANDED (2026-05-30 PM, this PR): mechanised soundness-gap witness + Stage 1 syntactic infrastructure. (1) `tfuneff_lambda_free : expr -> bool` Fixpoint added to `formal/Syntax.v` (conservative leaf-only predicate; `false` on every `ELam`, compositional `andb` propagation through compound forms). (2) `formal/Counterexample_L2_nested.v` — three Qed lemmas (`e_before_typed`, `e_step`, `e_after_untypable`) mechanising the nested-TFunEff soundness gap with `outer = ELam T_v (ELam (TBase TUnit) (EVar 1))` configuration where inner R_in_inner = [r2] but substituent R_in_v = []; e_after = ELam TUnit v fails to retype the body at `[r2] ⊄ [] = R_in_v`. (3) Wired into `_CoqProject` after `Counterexample_L2.v`. (4) `SUBST-LEMMA-GENERALIZATION-DESIGN.md` gained a 'Phase 3b Stage 1a (landed) — split from Stage 1' subsection inside the Phase 3b resolution section, documenting the Stage 1a / Stage 1b split and the structural blocker (G-mismatch at compound binder rules — `tfuneff_lambda_retype_l1_m` preserves G but IH expects post-e1 G' with different used-flags) that motivated the split. Stage 1b (substitution lemma + preservation_l2 wrapper) ships next session via a follow-up sub-issue. Build oracle: coqc 8.18.0 clean across all 12 .v files; Print Assumptions on all three new Qed lemmas reports 'Closed under the global context' (zero new admits/axioms). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ no residual Semantics_L1.v admit closure attempted; ✅ anti-pattern detector clean. Sibling counterexample artifact to `Counterexample_L2.v` (PR #234) for the nested-lambda soundness-gap class; the two together justify the two-condition (P1 = `tfuneff_lambda_free`, P2 = `regions_introduced_by ⊆ R_in_v`) preservation_l2 statement Stage 1b delivers." updated: 2026-05-30T00:00:00Z @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"): diff --git a/formal/Counterexample_L2_nested.v b/formal/Counterexample_L2_nested.v new file mode 100644 index 0000000..73e71cf --- /dev/null +++ b/formal/Counterexample_L2_nested.v @@ -0,0 +1,244 @@ +(* SPDX-License-Identifier: PMPL-1.0-or-later *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) + +(** * Soundness gap (L2): preservation_l2 fails for nested-TFunEff + substituends — the gap Phase 3b Stage 1's [tfuneff_lambda_free] + precondition correctly EXCLUDES. + + Sibling artifact to [Counterexample_L2.v]. That earlier file + witnessed the soundness gap for TFunEff substituends crossing + a fresh-region scope ([ERegion]). This file witnesses a + DIFFERENT gap class: TFunEff substituends placed inside an + inner [TFunEff] lambda whose declared [R_in_inner] is too + small to accommodate the substituent's required formation env. + + The two together justify the **two**-condition statement of + Phase 3b Stage 1's [preservation_l2_app_eff_beta_tfuneff_l1]: + + (P1) [tfuneff_lambda_free ebody = true] + — rules out THIS counterexample's class (inner lambda) + (P2) [regions_introduced_by ebody ⊆ R_in_v] + — rules out [Counterexample_L2.v]'s class (fresh region) + + Stage 2 (#240) lifts (P1) by carrying [R_in / R_out] on [ELam]. + Stage 3 (#241) replaces (P1) with a CPS-style proof that closes + the inner-lambda case via a relaxed [declared_lambda_r_ins ⊆ R_in_v] + obligation. Stage 4 (#242) reaches an unconditional preservation_l2. + + ===== Configuration ===== + + T_v := TFunEff TUnit TUnit [] [] (* substituent type, R_in_v = [] *) + v := ELam TUnit EUnit (* value of type T_v *) + inner_body := ELam TUnit (EVar 1) (* inner lambda; body refs outer var *) + T_inner := TFunEff TUnit T_v [r2] [r2] (* inner lambda's annotated type *) + outer := ELam T_v inner_body (* outer lambda; param of type T_v *) + T_outer := TFunEff T_v T_inner [] [] (* outer type *) + e_before := EApp outer v (* well-typed via T_App_L2_Eff at R = [] *) + e_after := ELam TUnit v (* β-result: subst 0 v inner_body *) + + ===== Why this configuration witnesses the gap ===== + + Pre-β [outer] is well-typed because the inner lambda's body + [EVar 1] references the outer variable (de-Bruijn index 1 + skipping the inner binder) at type [T_v]. Per [T_Var_Unr_L1] + on a non-linear type ([is_linear_ty T_v = false]), the reference + types at any region env; in particular at [R_in_inner = [r2]]. + Side condition [R_in_outer ⊆ R_in_inner] passes vacuously when + [R_in_outer = []]. + + Post-β substitutes [v] for the outer variable. The inner lambda + body becomes [shift 0 1 v = v] (closed value). So + [e_after = ELam TUnit v]. For [e_after] to type at [T_inner], + [v] would need to retype at [R = [r2]] via [T_Lam_L1_*_Eff], + which requires [[r2] ⊆ R_in_v = []]. This fails on [r2 ∈ [r2]] + vs. [r2 ∉ []]. + + The structural mechanism: [tfuneff_lambda_retype_l1_m] + (Semantics_L1.v:1257) carries the obligation [R' ⊆ R_in_v]; + inside a nested [TFunEff] lambda the [R'] is the INNER + [R_in_inner], not the OUTER formation env — and inner [R_in] + annotations are invisible to Phase 3b Stage 1's syntactic + [regions_introduced_by] over-approximation. Stage 1 therefore + refuses ebody-with-inner-lambdas via [tfuneff_lambda_free]. + + ===== Three theorems ===== + + - [e_before_typed] — outer at [T_outer] via T_Lam_L1_Affine_Eff + cascaded with inner; full e_before via T_App_L2_Eff. + - [e_step] — operational [S_App_Fun] β-reduction. + - [e_after_untypable] — no L1 derivation exists for e_after at + T_inner. Inversion forces [T_Lam_L1_*_Eff] + (only formation rule producing TFunEff); + both modes' side condition + [forall r, In r [r2] -> In r []] is + contradicted by [In r2 [r2]]. + + ===== Owner-directive compliance ===== + + - Does not modify [Semantics.v] or [Counterexample.v] (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 and [Counterexample_L2.v] for the + fresh-region soundness-gap class. + - 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 CounterexampleL2Nested. + + Definition r2 : region_name := "r2". + + (** Substituent type — a TFunEff lambda with empty input region env. *) + Definition T_v : ty := + TFunEff (TBase TUnit) (TBase TUnit) [] []. + + (** Substituent value — a closed [TUnit -> TUnit] lambda. *) + Definition v : expr := + ELam (TBase TUnit) EUnit. + + (** Inner lambda type — annotated with [R_in = R_out = [r2]]. *) + Definition T_inner : ty := + TFunEff (TBase TUnit) T_v [r2] [r2]. + + (** Inner lambda body — references the outer-bound variable via + [EVar 1] (de Bruijn index 1 skips the inner [ELam] binder). *) + Definition inner_body : expr := + ELam (TBase TUnit) (EVar 1). + + (** Outer lambda — parameter of type [T_v], body is [inner_body]. *) + Definition outer : expr := + ELam T_v inner_body. + + (** Outer lambda's type. *) + Definition T_outer : ty := + TFunEff T_v T_inner [] []. + + Definition e_before : expr := EApp outer v. + + (** Post-β term: [subst 0 v (ELam TUnit (EVar 1))] + = [ELam TUnit (subst 1 (shift 0 1 v) (EVar 1))] + = [ELam TUnit (shift 0 1 v)] (* EVar 1 substitutes to shift 0 1 v *) + = [ELam TUnit v] (* v is a closed value, shift is identity on its body *) *) + Definition e_after : expr := ELam (TBase TUnit) v. + + (** Helper: [v] types at [T_v] at any sufficiently small R. *) + + Lemma v_typed_at_empty : + has_type_l1 Affine [] [] v T_v [] []. + Proof. + unfold v, T_v. + 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 [T_outer]. *) + + Lemma outer_typed : + has_type_l1 Affine [] [] outer T_outer [] []. + Proof. + unfold outer, T_outer, T_inner, inner_body. + eapply T_Lam_L1_Affine_Eff with (u := false). + - intros r Hr; inversion Hr. + - (* Inner lambda formation at outer body context. + Outer body context: [ctx_extend [] T_v = (T_v, false) :: []]. + Inner lambda forms at TFunEff (TBase TUnit) T_v [r2] [r2]. *) + eapply T_Lam_L1_Affine_Eff with (u := false). + + intros r Hr; inversion Hr. + + (* Body of inner: [EVar 1] at R = [r2], context = + ctx_extend ((T_v, false) :: []) (TBase TUnit) + = ((TBase TUnit, false) :: (T_v, false) :: []). + [EVar 1] looks up [T_v] at index 1; output type [T_v]. *) + 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 T_inner [] []. + Proof. + unfold e_before. + eapply T_App_L2_Eff. + - apply L2_lift_l1. exact outer_typed. + - apply L2_lift_l1. exact v_typed_at_empty. + Qed. + + (** ===== (b) The β-step from e_before to e_after ===== + + [subst 0 v (ELam TUnit (EVar 1))] + = [ELam TUnit (subst 1 (shift 0 1 v) (EVar 1))] (* binder descent *) + = [ELam TUnit (shift 0 1 v)] (* EVar 1 substitutes *) + + We need [shift 0 1 v = v]. Since [v = ELam TUnit EUnit] and + [shift c d (ELam T0 e0) = ELam T0 (shift (S c) 1 e0)], we get + [shift 0 1 (ELam TUnit EUnit) = ELam TUnit (shift 1 1 EUnit) = + ELam TUnit EUnit = v]. *) + + Lemma e_step : + forall mu, step (mu, [], e_before) (mu, [], e_after). + Proof. + intros mu. unfold e_before, e_after, outer, inner_body. + change (ELam (TBase TUnit) v) + with (subst 0 v (ELam (TBase TUnit) (EVar 1))). + apply S_App_Fun. unfold v. apply VLam. + Qed. + + (** ===== (c) e_after does NOT type at T_inner ===== + + No L1 derivation exists for [[] ; [] |=L1[Affine] e_after : + T_inner -| ?R_out; ?G_out]. + + Proof by inversion: e_after = ELam (TBase TUnit) v is an [ELam] + whose annotated TFunEff type carries [R_in = [r2]]. Only + [T_Lam_L1_Linear_Eff] and [T_Lam_L1_Affine_Eff] produce + TFunEff types ([T_Lam_L1_Linear] and [T_Lam_L1_Affine] produce + [TFun], discriminated). Both _Eff rules form the body of e_after + ([v]) at [R = R_in = [r2]] and require [v] to type at + [TFunEff (TBase TUnit) (TBase TUnit) [] []]; the body + [v = ELam (TBase TUnit) EUnit] re-enters [T_Lam_L1_*_Eff], + whose side condition [forall r, In r [r2] -> In r []] is + contradicted by [In r2 [r2]]. *) + + Lemma e_after_untypable : + forall R_out G_out, + ~ has_type_l1 Affine [] [] e_after T_inner R_out G_out. + Proof. + intros R_out G_out Ht. + unfold e_after, T_inner, v in Ht. + inversion Ht; subst. + (* Only T_Lam_L1_Affine_Eff survives (mode matches, output type + structure matches). The body [ELam (TBase TUnit) EUnit] at + [R = [r2]] must produce a TFunEff. *) + match goal with + | [ Hbody : has_type_l1 _ (r2 :: nil) _ + (ELam (TBase TUnit) EUnit) _ _ _ |- _ ] => + rename Hbody into Hv_inner + end. + inversion Hv_inner; subst. + (* Only T_Lam_L1_Affine_Eff survives — T_Lam_L1_Affine produces + TFun (discriminated against output type + TFunEff (TBase TUnit) (TBase TUnit) [] []). *) + match goal with + | [ Hside : forall r, In r (r2 :: nil) -> In r nil |- _ ] => + specialize (Hside r2 (or_introl eq_refl)); inversion Hside + 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 nested-TFunEff substituent class. No top-level + conjunction theorem is stated for the same Type/Prop-sort reason + documented in [Counterexample_L2.v]. *) + +End CounterexampleL2Nested. diff --git a/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md b/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md index f2d53c9..ff5f162 100644 --- a/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md +++ b/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md @@ -198,6 +198,21 @@ The staged plan: (3) ships today's value, (1) lands L4's value at L4's timeline, **Sequencing**: Stage 1 implementation green-lit. Stages 2-4 tracked. Stage 3 blocked on Stage 2; Stage 4 blocked on Stage 3; Stage 2 independent of Stage 1. +#### Phase 3b Stage 1a (2026-05-30 PM, landed) — split from Stage 1 + +Stage 1's deliverables split into two slices for shipping cadence: + +**Stage 1a (this PR, landed)** — Infrastructure + soundness-gap witness: +- `tfuneff_lambda_free : expr -> bool` Fixpoint in `formal/Syntax.v`. Conservative leaf-only predicate: `false` on every `ELam`, `true` elsewhere; propagates compositionally through compound forms via `andb`. +- `formal/Counterexample_L2_nested.v` — three `Qed` lemmas (`e_before_typed`, `e_step`, `e_after_untypable`) mechanising the nested-TFunEff soundness gap. Configuration: `outer = ELam T_v (ELam (TBase TUnit) (EVar 1))` with inner `R_in_inner = [r2]`; `v = ELam TUnit EUnit` at `TFunEff TUnit TUnit [] []`. Post-β `e_after = ELam TUnit v` cannot retype the body at `[r2] ⊄ [] = R_in_v`. Sibling artifact to `Counterexample_L2.v`: together the two files justify the **two-condition** preservation_l2 statement Stage 1 ships (P1 = `tfuneff_lambda_free ebody`, P2 = `regions_introduced_by ebody ⊆ R_in_v`). +- Wired into `_CoqProject` after `Counterexample_L2.v`. +- Zero new admits / axioms (Print Assumptions: all three lemmas Closed under the global context). + +**Stage 1b (follow-up issue, deferred)** — Substitution lemma + preservation wrapper: +- `subst_typing_gen_l1_m_tfuneff` Qed in `formal/Semantics_L1.v` mirroring `subst_typing_gen_l1_m_ground_nonlinear` (~300 lines); inner `T_Lam_L1_*_Eff` cases exfalso via `tfuneff_lambda_free`; direct (P1, P2) hypothesis form. +- `preservation_l2_app_eff_beta_tfuneff_l1` + L2 wrapper Qed in `formal/TypingL2.v`. +- The structural blocker requiring deferral: the substitution lemma's compound rule cases (T_Let_L1, T_LetLin_L1, T_Case_L1_*) need to retype the substituent value `v` at a different G (post-e1 used-flag updates). Phase 2's analog uses `ground_nonlinear_retype_l1_m` (R-poly AND G-poly); Phase 3b's `tfuneff_lambda_retype_l1_m` preserves G. The Stage 1b machinery needs EITHER (a) a closed-value G-polymorphism helper (`closed_value_typing_G_poly_l1_m` — provable via inversion on T_Lam_L1_*_Eff formation rules but lengthy), OR (b) a G-flag-polymorphic retype variant. Either path is its own sub-deliverable. + ### Phase 4: close `preservation_l2` β-case using Phases 1-3 With the substitution machinery in place, the T_App_L2_Eff β-case in `preservation_l2` closes by: diff --git a/formal/Syntax.v b/formal/Syntax.v index e407142..5363412 100644 --- a/formal/Syntax.v +++ b/formal/Syntax.v @@ -516,6 +516,43 @@ Fixpoint regions_introduced_by (e : expr) : list region_name := | ERegion r e' => r :: regions_introduced_by e' end. +(** Syntactic predicate: the expression contains no [ELam] subterm. + + Used by Phase D slice 4 Phase 3b Stage 1's substitution lemma + [subst_typing_gen_l1_m_tfuneff] to exfalso-eliminate the inner + [T_Lam_L1_Linear_Eff] / [T_Lam_L1_Affine_Eff] cases. The principle + is "leaf-only": Stage 1's lemma only fires when the substituee + body has no inner lambdas, so the conditional [R_in_inner ⊆ R_in_v] + obligation that Stage 3 (CPS) and Stage 2 (annotated ELam) address + cannot arise. + + A [TFunEff] lambda is, in the current AST, indistinguishable from + a [TFun] lambda at the [ELam] node (the type annotation slot carries + only the parameter type, not the function type). Hence the predicate + is conservatively false on EVERY [ELam], not only TFunEff-typed + ones. Stage 2 (#240) reshapes [ELam] to carry [R_in] / [R_out] and + refines this predicate to TFunEff-specific. + + Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 3b Stage 1 + and ephapax issue #239. *) +Fixpoint tfuneff_lambda_free (e : expr) : bool := + match e with + | EUnit | EBool _ | EI32 _ | EVar _ + | EStringNew _ _ | ELoc _ _ => true + | EStringConcat e1 e2 | ELet e1 e2 | ELetLin e1 e2 + | EApp e1 e2 | EPair e1 e2 => + andb (tfuneff_lambda_free e1) (tfuneff_lambda_free e2) + | EStringLen e' | EFst e' | ESnd e' + | EBorrow e' | EDeref e' | EDrop e' | ECopy e' | EObserve e' => + tfuneff_lambda_free e' + | EInl _ e' | EInr _ e' | EEcho _ e' | ERegion _ e' => + tfuneff_lambda_free e' + | EIf e1 e2 e3 | ECase e1 e2 e3 => + andb (andb (tfuneff_lambda_free e1) (tfuneff_lambda_free e2)) + (tfuneff_lambda_free e3) + | ELam _ _ => false + end. + (** Check if all linear variables in context have been used *) Fixpoint ctx_all_linear_used (G : ctx) : Prop := match G with diff --git a/formal/_CoqProject b/formal/_CoqProject index 5ef3236..970f074 100644 --- a/formal/_CoqProject +++ b/formal/_CoqProject @@ -14,4 +14,5 @@ Echo.v Modality.v TypingL2.v Counterexample_L2.v +Counterexample_L2_nested.v L4.v