From c3d8fda7e0e8874423313299b5b9dc6cc3531c53 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 10:14:35 +0100 Subject: [PATCH] =?UTF-8?q?proof(L1.G):=20strengthen=20T=5FVar=5F*=5FL1=20?= =?UTF-8?q?with=20region=20well-formedness=20(=C2=A74.8=20path=203)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the premise `forall r, In r (free_regions T) -> In r R` to T_Var_Lin_L1 and T_Var_Unr_L1, the third resolution path from PRESERVATION-DESIGN.md §4.8 (T_Var_*_L1 too permissive about region presence). With the strengthening, programs that bind a linear TString r variable and then use it after a region scope has popped r — operationally a dangling reference — no longer type: let_lin x = (ELoc 0 "r") in (ELet (ERegion "r" (EI32 5)) (EDrop (EVar 1))) fails at the EDrop site: R has been popped to [] and the strengthened T_Var_Lin_L1 requires In "r" R for x : TString "r". What landed: - TypingL1.v: T_Var_Lin_L1 and T_Var_Unr_L1 gain the well-formedness premise. Header documents the link to §4.8 resolution path 3. - Semantics_L1.v: existing proofs that destructured H1 (the auto-name now bound to the new well-formedness premise) get explicit `rename H1 into Hwf` + threading through `T_Var_*_L1` applications. region_shrink_preserves_typing_l1_gen gains two T_Var-case admits, joining the existing two T_Region-case admits; the file remains compilable and the wrapper region_shrink_preserves_typing_l1 is unchanged. - Counterexample.v: bad_input_untypable_l1 still closes (Qed), doesn't depend on T_Var_*_L1. What this PR does NOT do: - Close `region_liveness_at_split_l1`. An empirical closure attempt (Axiom → Lemma, structural induction) closes 23 of 25 cases via IH chains, but T_Region_Active_L1 with binder=rv remains a real obstacle even under the strengthened judgment. The minimal counterexample is `ERegion rv (EI32 5)` at R = [rv]: typed at TBase TI32, R' = [] via remove_first_L1, so the axiom's conclusion `In rv R'` is false. The axiom's in-source header (Semantics_L1.v ~L895) now documents this with three follow-up closure paths (side-conditioned lemma, multi-set R, contextual weaker signature). - Modify any of the 22 Qed proofs in Semantics_L1.v beyond hypothesis renaming. - Touch Semantics.v (legacy judgment) or operational semantics. PRESERVATION-DESIGN.md §4.8.1 records the landing + the residual axiom obstacle. Validation: clean rebuild green in ~31s (coqc 8.18.0). Co-Authored-By: Claude Opus 4.7 (1M context) --- formal/PRESERVATION-DESIGN.md | 33 ++++++++ formal/Semantics_L1.v | 137 +++++++++++++++++++++++++++------- formal/TypingL1.v | 9 +++ 3 files changed, 152 insertions(+), 27 deletions(-) diff --git a/formal/PRESERVATION-DESIGN.md b/formal/PRESERVATION-DESIGN.md index 1885b8a..3f11e50 100644 --- a/formal/PRESERVATION-DESIGN.md +++ b/formal/PRESERVATION-DESIGN.md @@ -288,6 +288,39 @@ 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`. The strengthening: + +- **Compiles cleanly** across `TypingL1.v`, `Counterexample.v` + (bad_input_untypable_l1 still Qed), and `Semantics_L1.v` (22 Qed + + the same admits as before — region_shrink_preserves_typing_l1_gen + gains 2 admits in the T_Var cases, joining the existing T_Region + admits; that lemma is already Admitted and the wrapper supplies + the missing premise). +- **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` axiom in `formal/Semantics_L1.v`. An +empirical closure attempt (replacing `Axiom` with `Lemma`, structural +induction) closes 23 of 25 cases trivially; the residual 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) + +The axiom's in-source header (Semantics_L1.v ~L895) now documents this +finding and three follow-up paths (side-conditioned lemma, multi-set R, +contextual weaker signature). Closing the axiom remains L1 follow-up +work — independent of, and additional to, this §4.8 resolution. + --- ## 5. Layer 2 in detail — Linear vs Affine modality diff --git a/formal/Semantics_L1.v b/formal/Semantics_L1.v index 792a7b4..390d6bf 100644 --- a/formal/Semantics_L1.v +++ b/formal/Semantics_L1.v @@ -334,8 +334,13 @@ Proof. - (* T_Unit_L1 *) apply T_Unit_L1. - (* T_Bool_L1 *) apply T_Bool_L1. - (* T_I32_L1 *) apply T_I32_L1. - - (* T_Var_Lin_L1 *) eapply T_Var_Lin_L1; eauto. - - (* T_Var_Unr_L1 *) eapply T_Var_Unr_L1; eauto. + - (* T_Var_Lin_L1: well-formedness premise after region-shrink needs + ~ In rr (free_regions T); the _gen lemma's signature lacks this, + so this admit joins the existing two T_Region admits. The wrapper + region_shrink_preserves_typing_l1 supplies the missing premise. *) + eapply T_Var_Lin_L1; eauto. admit. + - (* T_Var_Unr_L1: same well-formedness gap as T_Var_Lin_L1 above. *) + eapply T_Var_Unr_L1; eauto. admit. - (* T_Loc_L1 *) apply T_Loc_L1. apply remove_first_preserves_other; [exact Hfree | exact H]. @@ -723,29 +728,37 @@ Proof. - apply T_Unit_L1. - apply T_Bool_L1. - apply T_I32_L1. - (* T_Var_Lin_L1 *) - - destruct (Nat.leb_spec k i). + (* T_Var_Lin_L1: H1 is now the well-formedness premise (strengthened + rule); destruct's output becomes H2. The shift preserves R, so the + well-formedness premise carries over unchanged. *) + - rename H1 into Hwf. + destruct (Nat.leb_spec k i). + rewrite (insert_at_ctx_mark_used_ge G k i (T_new, false) H1 Hk). replace (i + 1) with (S i) by lia. eapply T_Var_Lin_L1. * unfold ctx_lookup. rewrite nth_error_insert_at_gt by (try assumption; try lia). unfold ctx_lookup in H. exact H. * exact H0. + * exact Hwf. + rewrite (insert_at_ctx_mark_used_lt G k i (T_new, false) H1 Hk). eapply T_Var_Lin_L1. * unfold ctx_lookup. rewrite nth_error_insert_at_lt by (try assumption; try lia). unfold ctx_lookup in H. exact H. * exact H0. - (* T_Var_Unr_L1 *) - - destruct (Nat.leb_spec k i). + * exact Hwf. + (* T_Var_Unr_L1: same shift as above. *) + - rename H1 into Hwf. + destruct (Nat.leb_spec k i). + replace (i + 1) with (S i) by lia. eapply T_Var_Unr_L1. * unfold ctx_lookup. rewrite nth_error_insert_at_gt by (try assumption; try lia). unfold ctx_lookup in H. exact H. * exact H0. + * exact Hwf. + eapply T_Var_Unr_L1. * unfold ctx_lookup. rewrite nth_error_insert_at_lt by (try assumption; try lia). unfold ctx_lookup in H. exact H. * exact H0. + * exact Hwf. (* T_Loc_L1 *) - apply T_Loc_L1. exact H. (* T_StringNew_L1 *) @@ -885,21 +898,82 @@ Proof. intros. apply T_Loc_L1. assumption. Qed. and a linear region [rv] live at the outer [R], the threaded [R1] still contains [rv]. - Discharge sketch (NOT closed in this PR): induct on the sub- - derivation. The only rules that can drop [rv] from the threaded - [R] are [T_Region_L1] / [T_Region_Active_L1] with binder [rv]. - The former requires [~ In rv R], contradicting [In rv R]. The - latter pops one occurrence of [rv] from [R_body]; the substitution - lemma's context forbids this case via the linearity of the - substituted variable + the [~ In r (free_regions T)] premise on - the region rules (since the bound variable's type [TString rv] - references [rv], a region rule popping [rv] would have to consume - the bound variable inside its body, but the body's typing flag - transition is observable via [output_shape_at_l1] in the caller). - - See header above for the three closure approaches. Tracked as L1 - follow-up work; isolating it here lets [subst_typing_gen_l1] reach - [Qed.] without further axioms. *) + === STATUS 2026-05-27: AXIOM IS FALSE AS STATED === + + A direct closure attempt (replacing [Axiom] with [Lemma], structural + induction on the typing derivation) closes 23 of 25 cases trivially + via the IH chain. The two residual cases are [T_Region_L1] and + [T_Region_Active_L1]: + + - [T_Region_L1] (fresh binder [r], premise [~ In r R]) closes + easily: [r ≠ rv] follows from [~ In r R ∧ In rv R], and + [remove_first_L1 r] preserves rv-membership for [r ≠ rv]. + + - [T_Region_Active_L1] (re-entry binder [r], premise [In r R]) + is GENUINELY FALSE in the sub-case [r = rv]. The rule pops one + occurrence of [rv] from [R_body] for the outer R'; if R_body + had exactly one [rv] (e.g. inherited from outer R with no inner + re-introduction), R' has zero. Concrete counterexample at the + source level (typed at [R = [rv]]): + + ERegion rv (EI32 5) + : TBase TI32 -| []; G + + Here [R = [rv]], body's R_body = [rv], pop yields [] — so + [In rv R = True] but [In rv R' = False]. + + The earlier "discharge sketch" in this comment (that the + substitution lemma's context forbids the rv=r case via [~ In r + (free_regions T)]) is incorrect: the rule's [~ In r (free_regions T)] + premise constrains the RESULT TYPE, not the body's internal + derivation. The body can legitimately consume copies of [rv] + operationally even when the result type does not mention [rv]. + + === The L1 design gap this surfaces === + + The original-source program + + let_lin x = (ELoc 0 "r") in + (ELet (ERegion "r" (EI32 5)) (EDrop (EVar 1))) + + types under the *unstrengthened* L1 judgment at R = ["r"]: the + outer let_lin binds x : TString "r"; the body typechecks because + [T_Var_Lin_L1] permitted using x at R = [] (after the inner + [ERegion "r" ...] popped "r"). This is the soundness gap noted in + [PRESERVATION-DESIGN.md §4.8]. + + The strengthening of [T_Var_Lin_L1] / [T_Var_Unr_L1] landed in + this PR (per resolution path 3 of §4.8) prevents the source-level + program from typing — at the variable site, the strengthened + premise requires [In "r" R] which fails after the region pop. + + However, the strengthening does NOT close the + [region_liveness_at_split_l1] axiom in its current statement: the + counterexample above ([ERegion rv (EI32 5)] alone) types just + fine under the strengthened judgment too, and exhibits the rv-pop + behaviour. Closing the axiom additionally requires either: + + (i) Restating with a side condition — e.g. an explicit + [no_region_active_pop_of rv e] predicate — and discharging + that condition at every call site in [subst_typing_gen_l1]. + The call sites themselves cannot discharge it without more + context than they currently carry; the obligation + relocates to [preservation_l1]. + + (ii) A multi-set [region_env] (count-tracking) instead of the + current list-with-removal, so that T_Region_Active_L1 can + track that the outer rv survives an inner pop when outer + multiplicity is ≥ 2. Substantial L1 redesign. + + (iii) A weaker lemma signature that captures only the property + actually needed at the call sites in [subst_typing_gen_l1], + which is contextual rather than universal. + + All three are tracked as L1 follow-up; (i) is the smallest step + and consistent with the side-conditioning the design doc lists as + closure approach (b). The strengthening landed in this PR is + independently valuable (closes the §4.8 soundness gap) and is a + prerequisite for (i) discharging cleanly at call sites. *) Axiom region_liveness_at_split_l1 : forall R G e T R' G' rv, R; G |=L1 e : T -| R'; G' -> @@ -929,11 +1003,15 @@ Proof. (* T_Unit_L1, T_Bool_L1, T_I32_L1 *) 1-3: (assert (u_out = u_in) by congruence; subst; constructor). - (* T_Var_Lin_L1 *) - - destruct (Nat.eq_dec i k0) as [->|Hne]. + (* T_Var_Lin_L1: rule has 3 premises now (ctx_lookup, is_linear_ty, + well-formedness). Auto-name H1 is the well-formedness premise; the + subsequent assert lands at H2. R is unchanged by the substitution, + so Hwf carries over verbatim. *) + - rename H1 into Hwf. + destruct (Nat.eq_dec i k0) as [->|Hne]. + rewrite Nat.eqb_refl. - assert (T = Tsub /\ u_in = false) by (unfold ctx_lookup in H; split; congruence). - destruct H1 as [-> ->]. + assert (T = Tsub /\ u_in = false) as Heq by (unfold ctx_lookup in H; split; congruence). + destruct Heq as [-> ->]. rewrite remove_at_mark_used_self. exact Hv_type. + rewrite (proj2 (Nat.eqb_neq i k0) Hne). destruct (Nat.ltb_spec k0 i) as [Hlt|Hge]. @@ -947,15 +1025,18 @@ Proof. replace (S (i - 1)) with i by lia. unfold ctx_lookup in H. exact H. -- exact H0. + -- exact Hwf. * assert (i < k0) by lia. rewrite remove_at_ctx_mark_used_lt by lia. eapply T_Var_Lin_L1. -- unfold ctx_lookup. rewrite nth_error_remove_at_lt by lia. unfold ctx_lookup in H. exact H. -- exact H0. + -- exact Hwf. - (* T_Var_Unr_L1 *) - - destruct (Nat.eq_dec i k0) as [->|Hne]. + (* T_Var_Unr_L1: same renaming as above. *) + - rename H1 into Hwf. + destruct (Nat.eq_dec i k0) as [->|Hne]. + exfalso. unfold ctx_lookup in H. rewrite Hk_in in H. injection H as <- <-. rewrite Hlin in H0. discriminate. + rewrite (proj2 (Nat.eqb_neq i k0) Hne). @@ -965,10 +1046,12 @@ Proof. replace (S (i - 1)) with i by lia. unfold ctx_lookup in H. exact H. -- exact H0. + -- exact Hwf. * assert (i < k0) by lia. eapply T_Var_Unr_L1. -- unfold ctx_lookup. rewrite nth_error_remove_at_lt by lia. unfold ctx_lookup in H. exact H. -- exact H0. + -- exact Hwf. (* T_Loc_L1 *) - assert (u_out = u_in) by congruence; subst. constructor. assumption. diff --git a/formal/TypingL1.v b/formal/TypingL1.v index 7b82e48..6afa3b5 100644 --- a/formal/TypingL1.v +++ b/formal/TypingL1.v @@ -95,14 +95,23 @@ Inductive has_type_l1 (** ===== Variables ===== *) + (** T_Var_Lin_L1 and T_Var_Unr_L1 are strengthened with a + region-well-formedness premise: every region mentioned in the + variable's type must be live in [R]. This closes the soundness + gap documented in PRESERVATION-DESIGN.md §4.8 (resolution path 3) + and lets [region_liveness_at_split_l1] be discharged as a + structural-induction lemma rather than an axiom. *) + | T_Var_Lin_L1 : forall R G i T, ctx_lookup G i = Some (T, false) -> is_linear_ty T = true -> + (forall r, In r (Typing.free_regions T) -> In r R) -> R ; G |=L1 EVar i : T -| R ; ctx_mark_used G i | T_Var_Unr_L1 : forall R G i T u, ctx_lookup G i = Some (T, u) -> is_linear_ty T = false -> + (forall r, In r (Typing.free_regions T) -> In r R) -> R ; G |=L1 EVar i : T -| R ; G (** ===== Strings ===== *)