syntax: expr_strictly_free_of_region (closes blocker 5)

Reformulates the region-freedom predicate to drop the shadow short-
circuit in [ERegion r' body], which the 2026-05-28 audit (task #29)
identified as the cause of blocker 5 (predicate-too-weak in L1
region-shrinkage lemma family).

Changes:
* formal/Syntax.v
  - new Fixpoint expr_strictly_free_of_region : same shape as
    expr_free_of_region except the [ERegion _ body] case recurses
    UNCONDITIONALLY (no String.eqb shadow short-circuit).
  - new Lemma expr_strictly_free_implies_free : Qed via structural
    induction. Trivial implication establishing the strict variant
    is a conservative strengthening.

* formal/Semantics_L1.v
  - migrate preconditions of region_shrink_preserves_typing_l1_gen_m,
    region_shrink_preserves_typing_l1_gen, region_shrink_preserves_typing_l1,
    preservation_l3_region_active_echo, and preservation_l3 from
    expr_free_of_region to expr_strictly_free_of_region.
  - update the [T_Region_L1] / [T_Region_L1_Echo] rr<>r descend
    sub-cases' IH-discharge comments (proof body uses the same
    simpl + destruct pattern, now with strict Hfree).

Audit constraints honored:
* Zero new Admitted or Axiom declarations (4 admits / 3 Admitted
  preserved exactly per main).
* The shadowed sub-case admits at Semantics_L1.v:553/621 REMAIN —
  they are blocked by list-vs-multiset structural mismatch
  (Phase D work), NOT by predicate weakness. The strict variant
  does NOT close them.
* No patching of legacy Theorem preservation in Semantics.v (false
  per Counterexample.v) or the legacy Typing.v judgment.

Out of scope (follow-up):
* The step rules S_Region_Exit / S_Region_Exit_Echo in Semantics.v
  still emit the weak expr_free_of_region premise. Migrating those
  to strict is a separate concern (legacy operational semantics)
  and intentionally NOT done here per task instruction.

Build: all 9 .v files compile clean under coqc 8.18.0 from a fresh
.vo state.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

formal/Semantics_L1.v

@@ -428,11 +428,21 @@ Qed.
     (analog of [region_env_perm_typing] and [region_add_typing])
     is needed to close it; bridging options are listed in the
     case's own comment. *)
+(** Migrated to [expr_strictly_free_of_region] as the precondition
+    (blocker 5 reformulation, 2026-05-28). The strict predicate gives
+    the body strictly MORE information than the weak one — in
+    particular, the [T_Region_*_L1] cases no longer rely on a
+    shadow-short-circuited [True] in the [rr = r] subcase. The
+    residual [admit] at the [T_Region_Active_L1] [rr = r] sub-case
+    is blocked by a list-vs-multiset structural mismatch (Phase D
+    work, NOT by predicate weakness — strengthening the predicate
+    does not close it). The [admit] remains; see the case's own
+    comment for resolution options. *)
 Lemma region_shrink_preserves_typing_l1_gen_m :
   forall m R G e T R' G',
     R ; G |=L1[m] e : T -| R' ; G' ->
     forall r,
-      expr_free_of_region r e ->
+      expr_strictly_free_of_region r e ->
       remove_first r R ; G |=L1[m] e : T -| remove_first r R' ; G'.
 Proof.
   intros m R G e T R' G' Ht.
@@ -532,7 +542,11 @@ Proof.
       * intro Hin. apply H. eapply remove_first_subset; exact Hin.
       * exact H0.
       * apply remove_first_preserves_other; [intro Hbad; apply Heq; exact Hbad | exact H1].
-      * specialize (IHHt rr Hfree).
+      * (* Strict-predicate migration: [Hfree] is uniformly the body's
+           strict-freedom (no conditional to discharge). Still need
+           [simpl in IHHt] to unfold [remove_first rr (r :: R)] into
+           [r :: remove_first rr R] via the [rr <> r] guard. *)
+        specialize (IHHt rr Hfree).
         simpl in IHHt.
         destruct (String.eqb rr r) eqn:Heq2.
         -- exfalso. apply String.eqb_eq in Heq2. apply Heq. exact Heq2.
@@ -601,7 +615,9 @@ Proof.
       * intro Hin. apply H. eapply remove_first_subset; exact Hin.
       * exact H0.
       * apply remove_first_preserves_other; [intro Hbad; apply Heq; exact Hbad | exact H1].
-      * specialize (IHHt rr Hfree).
+      * (* Strict-predicate migration: same as T_Region_L1 above —
+           [simpl in IHHt] still needed to unfold [remove_first]. *)
+        specialize (IHHt rr Hfree).
         simpl in IHHt.
         destruct (String.eqb rr r) eqn:Heq2.
         -- exfalso. apply String.eqb_eq in Heq2. apply Heq. exact Heq2.
@@ -656,7 +672,7 @@ Lemma region_shrink_preserves_typing_l1_gen :
   forall R G e T R' G',
     has_type_l1_linear R G e T R' G' ->
     forall r,
-      expr_free_of_region r e ->
+      expr_strictly_free_of_region r e ->
       has_type_l1_linear (remove_first r R) G e T (remove_first r R') G'.
 Proof.
   intros R G e T R' G' Ht r Hfree.
@@ -668,7 +684,7 @@ Lemma region_shrink_preserves_typing_l1 :
     is_value v ->
     has_type_l1_linear R G v T R' G' ->
     ~ In r (free_regions T) ->
-    expr_free_of_region r v ->
+    expr_strictly_free_of_region r v ->
     has_type_l1_linear (remove_first r R) G v T (remove_first r R') G'.
 Proof.
   intros R G v T R' G' r Hv Ht HnotT Hfree.
@@ -1741,15 +1757,23 @@ Admitted.
     Region shrinkage then provides the post-step witness typing
     at [remove_first r R], and [T_Echo_L1] wraps it. *)
 
+(** Strict-predicate migration (blocker 5, 2026-05-28): the
+    region-shrinkage helper this lemma calls now requires
+    [expr_strictly_free_of_region], so the corresponding premise
+    here is also tightened. The legacy step rules
+    [S_Region_Exit_Echo] in [Semantics.v] still emit the weak
+    [expr_free_of_region]; bridging the step-rule premise to the
+    L1 lemma precondition is a follow-up (legacy operational
+    semantics — see PR description). *)
 Lemma preservation_l3_region_active_echo :
   forall m R G r v T R_body G',
     (* T_Region_Active_L1_Echo premises *)
     In r R ->
     ~ In r (Typing.free_regions T) ->
     has_type_l1 m R G v T R_body G' ->
-    (* S_Region_Exit_Echo premises *)
+    (* S_Region_Exit_Echo premises (strict variant per blocker 5) *)
     is_value v ->
-    expr_free_of_region r v ->
+    expr_strictly_free_of_region r v ->
     (* Conclusion: post-step types at [TEcho T] *)
     has_type_l1 m (remove_first r R) G
       (EEcho T v) (TEcho T) (remove_first_L1 r R_body) G'.
@@ -1806,7 +1830,7 @@ Theorem preservation_l3 :
       ~ In r (Typing.free_regions T) ->
       has_type_l1 m R G v T R_body G' ->
       is_value v ->
-      expr_free_of_region r v ->
+      expr_strictly_free_of_region r v ->
       has_type_l1 m (remove_first r R) G
         (EEcho T v) (TEcho T) (remove_first_L1 r R_body) G')
   /\

formal/Syntax.v

@@ -187,6 +187,94 @@ Fixpoint expr_free_of_region (r : region_name) (e : expr) : Prop :=
   | EObserve e' => expr_free_of_region r e'
   end.
 
+(** ** Strict Region-Freedom (reformulation, closes blocker 5)
+
+    [expr_strictly_free_of_region r e] mirrors [expr_free_of_region]
+    EXCEPT in the [ERegion r' body] case, where it recurses
+    UNCONDITIONALLY (no shadow short-circuit on [r = r']).
+
+    Why a strict variant exists. The weak [expr_free_of_region]
+    short-circuits to [True] when [ERegion r' body] shadows [r]
+    (the [String.eqb r r'] guard). That weakness is sound for the
+    plain capability-list reading of [R], where a nested
+    [ERegion r ...] statically masks the outer [r] and the body
+    cannot "reach back." But under the L1 [T_Region_Active_L1]
+    judgment — and more sharply under L3 re-entry semantics —
+    a body can witness the outer [r] through count-monotonicity /
+    multiset accounting that the syntactic shadow does NOT
+    discharge. The audit (task #29, 2026-05-28, blocker 5) traced
+    one class of "predicate too weak" failures in the region-
+    shrinkage lemma family to exactly this short-circuit accepting
+    expressions whose body legitimately references the outer [r].
+
+    The strict variant is the conservative reading: an expression
+    is strictly free of [r] iff [r] never appears anywhere inside,
+    even under a same-named [ERegion r ...] shadow. It implies the
+    weak variant (see [expr_strictly_free_implies_free] below).
+
+    Scope. The strict predicate is intended to replace the weak one
+    in the L1 region-shrinkage lemma family
+    ([region_shrink_preserves_typing_l1_gen_m] and friends in
+    [Semantics_L1.v]) and downstream consumers
+    ([preservation_l3_region_active_echo]). The legacy step rules
+    [S_Region_Exit] / [S_Region_Exit_Echo] in [Semantics.v] still
+    emit the weak [expr_free_of_region] premise; migrating those
+    is a separate concern (legacy operational semantics) and may
+    or may not happen in this PR (see PR description for current
+    scope).
+
+    Note. The L1 shadowed-sub-case [admit] at
+    [Semantics_L1.v:553/621] is blocked by a list-vs-multiset
+    structural mismatch (Phase D work), NOT by predicate weakness.
+    Strengthening to [expr_strictly_free_of_region] does NOT close
+    those admits. *)
+
+Fixpoint expr_strictly_free_of_region (r : region_name) (e : expr) : Prop :=
+  match e with
+  | EUnit | EBool _ | EI32 _ | EVar _ => True
+  | EStringNew r' _ => r <> r'
+  | EStringConcat e1 e2 | ELet e1 e2 | ELetLin e1 e2
+  | EApp e1 e2 | EPair e1 e2 =>
+      expr_strictly_free_of_region r e1 /\ expr_strictly_free_of_region r e2
+  | EStringLen e' | EFst e' | ESnd e' | EInl _ e' | EInr _ e'
+  | EBorrow e' | EDeref e' | EDrop e' | ECopy e' | ELam _ e' =>
+      expr_strictly_free_of_region r e'
+  | EIf e1 e2 e3 | ECase e1 e2 e3 =>
+      expr_strictly_free_of_region r e1 /\ expr_strictly_free_of_region r e2
+      /\ expr_strictly_free_of_region r e3
+  (** The strictness difference: no [String.eqb] shadow short-circuit.
+      Always descend into the body. *)
+  | ERegion _ e' => expr_strictly_free_of_region r e'
+  | ELoc _ r' => r <> r'
+  | EEcho _ e' => expr_strictly_free_of_region r e'
+  | EObserve e' => expr_strictly_free_of_region r e'
+  end.
+
+(** [expr_strictly_free_of_region] strictly strengthens
+    [expr_free_of_region]: every strictly-free expression is also
+    weakly-free. The converse fails on (e.g.)
+    [ERegion r (EStringNew r _)] where the weak variant accepts
+    via shadow short-circuit but the strict variant rejects.
+
+    Proof. Structural induction. The only non-trivial case is
+    [ERegion r' body]: the weak version short-circuits to [True]
+    when [r = r'], which is implied by anything; the strict
+    version's recursive hypothesis discharges the weak version's
+    recursive case when [r <> r']. *)
+Lemma expr_strictly_free_implies_free :
+  forall r e, expr_strictly_free_of_region r e -> expr_free_of_region r e.
+Proof.
+  intros r e. induction e; simpl; intros H; try exact I; try assumption;
+    try (apply IHe; exact H);
+    try (destruct H as [H1 H2]; split; [apply IHe1 | apply IHe2]; assumption);
+    try (destruct H as [H1 [H2 H3]]; split;
+         [apply IHe1; assumption | split; [apply IHe2 | apply IHe3]; assumption]).
+  - (* ERegion r' e *)
+    destruct (String.eqb r r0) eqn:Heq.
+    + exact I.
+    + apply IHe; exact H.
+Qed.
+
 (** ** Typing Contexts (De Bruijn) *)
 
 (** A typing context is a list of (type, used?) pairs.