syntax: expr_strictly_free_of_region (closes blocker 5) (#201)

## Summary

Reformulates the region-freedom predicate to drop the shadow short-
circuit in `ERegion r' body`, addressing **blocker 5** (predicate-
too-weak in the L1 region-shrinkage lemma family) identified by the
2026-05-28 audit (task #29).

- New `expr_strictly_free_of_region` in `Syntax.v` — identical to
  `expr_free_of_region` except the `ERegion _ body` case recurses
  unconditionally (no `String.eqb` shadow short-circuit).
- New `expr_strictly_free_implies_free` lemma (Qed) — trivial
  structural induction establishing that strict freedom implies
  weak freedom.
- L1 lemma family migrated to take `expr_strictly_free_of_region` as
  the precondition: `region_shrink_preserves_typing_l1_gen_m`,
  `region_shrink_preserves_typing_l1_gen`,
  `region_shrink_preserves_typing_l1`,
  `preservation_l3_region_active_echo`, and the top-level
  `preservation_l3` theorem.

## Audit constraints honored

- **Zero new** `Admitted` / `Axiom` declarations. Counts preserved
  exactly versus `main`: 4 `admit.` + 3 `Admitted.` in
  `Semantics_L1.v`, 1 `Admitted.` in `Semantics.v`.
- The shadowed-sub-case admits at `Semantics_L1.v:553/621` (now
  shifted by added comments) **remain**. They are blocked by a
  list-vs-multiset structural mismatch (Phase D), **not** by
  predicate weakness. Strengthening the predicate does **not**
  close them — confirmed by the audit and verified empirically
  here (same admit counts after migration).
- No patching of legacy `Theorem preservation` in `Semantics.v`
  (provably false per `Counterexample.v`) or the legacy `Typing.v`
  judgment, per the 2026-05-27 owner directive.

## Scope clarification

This PR **does not** close blocker 3 — that requires Phase D
(L2 effect-typed `TFun` work, branch
`phase-d-slice-1-tfun-eff`).

The 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 is intentionally **not** done in this
PR per the task brief. The L1 lemma chain
(`preservation_l3_*` -> `region_shrink_preserves_typing_l1_*`)
is internally consistent on the strict predicate; bridging the
weak step-rule premise to the strict L1 lemma precondition is a
follow-up.

## Build

All 9 `.v` files compile clean under `coqc 8.18.0` from a fresh
`.vo` state (Syntax, Typing, TypingL1, Modality, Semantics,
Semantics_L1, Counterexample, Echo, TypingL2).

## Test plan

- [x] `coqc 8.18.0` clean build of all 9 `.v` files from scratch
- [x] No new `Admitted` / `Axiom` declarations (counts match main)
- [x] Pre-existing 2 inner admits at `Semantics_L1.v:553/621`
      remain unchanged (line-shifted by added comments)
- [x] Pre-existing outer `Admitted` at `Semantics_L1.v` (region
      shrink helper) remains unchanged
- [x] Commit GPG-signed

Audit reference: task #29 (2026-05-28). Blocker 5 closure.

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

@@ -208,6 +208,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.