hyperpolymath
diff --git a/‎PROOF-NEEDS.md‎
Lines changed: 16 additions & 9 deletions b/‎PROOF-NEEDS.md‎
Lines changed: 16 additions & 9 deletions
diff --git a/‎formal/Semantics.v‎
Lines changed: 62 additions & 9 deletions b/‎formal/Semantics.v‎
Lines changed: 62 additions & 9 deletions
@@ -56,7 +56,7 @@ For the architectural background see
 | L1 judgment indexed by modality `m : Modality` | `formal/TypingL1.v` | landed via PRs #176 + #177 |
 | L2 modality core (`Modality.v`, `linear_to_affine`) | `formal/Modality.v` | 1 Qed, zero axioms |
 | L3 calculus (echo / residue fiber + degrade + no-section proof) | `formal/Echo.v` | 12 Qed, 0 admits |
-| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 15 Qed (subset of the 24 lemmas; 9 in transition) |
+| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 23 Qed; 3 residual admits (L2-β follow-up) |
 | Counterexample regression witness | `formal/Counterexample.v` | 5 Qed (`bad_input_untypable_l1` proved under both modes) |
 | Operational checker (Rust, ephapax-linear sublanguage) | `ephapax-linear/src/linear.rs` | working — discharges resource-exact obligation |
 
@@ -68,7 +68,7 @@ For the architectural background see
 | Linear ⇒ Affine weakening | `formal/TypingL1.v` `linear_to_affine` | Qed, zero axioms |
 | Operational checker (Rust, ephapax-affine sublanguage) | `ephapax-linear/src/affine.rs` | working — permits weakening / graceful abandonment |
 | Affine-mode echo discipline (LEcho Affine = lowered triple) | `formal/Echo.v` (calculus) | calculus done; rule wiring pending |
-| Affine forward progress lemmas | `formal/Semantics_L1.v` | bullet-structure rewrite for new Affine-only constructors — **9 admits queued** (see §2) |
+| Affine forward progress lemmas | `formal/Semantics_L1.v` | bullet-structure rewrites + subst_typing_gen_l1_m + region_shrink_preserves_typing_l1_gen_m m-polymorphic generalisations landed 2026-05-27; remaining 3 admits are L2-β deeper-than-bullet debt (see §2) |
 
 ### Counterexample regression
 
@@ -87,8 +87,12 @@ For the architectural background see
 
 | Item | File | Estimate |
 |---|---|---|
-| Close 9 Affine-only bullet-structure regressions in supporting lemmas | `formal/Semantics_L1.v` | ~2-3 hours |
-| State and prove `preservation_l1` for both modes | `formal/Semantics_L1.v` | ~3-4 sessions after the 9 supporting lemmas land |
+| ✅ Close 3 pure bullet-structure regressions (typing_preserves_bindings_l1, unrestricted_flag_unchanged_l1, shift_typing_gen_l1) | `formal/Semantics_L1.v` | done 2026-05-27 |
+| ✅ Generalise typing_preserves_length_l1 to modality-polymorphic | `formal/Semantics_L1.v` | done 2026-05-27 |
+| ✅ Generalise subst_typing_gen_l1 to modality-polymorphic + Linear wrapper (also generalised typing_preserves_bindings_l1, output_shape_at_l1, loc_retype_at_R_l1) | `formal/Semantics_L1.v` | done 2026-05-27 (L2-β follow-up #2) |
+| ✅ Restore region_shrink_preserves_typing_l1_gen bullet structure via m-polymorphic helper (residual list-vs-multiset structural admit isolated to T_Region_Active_L1 shadowed case inside _gen_m) | `formal/Semantics_L1.v` | done 2026-05-27 (L2-β follow-up #3) |
+| Close T_Region_Active_L1 [rr = r] shadowed sub-case of region_shrink_preserves_typing_l1_gen_m (list-vs-multiset bridge — option (a) L1 perm lemma, (b) multiset reformulation, or (c) T_Region_*_L1 redesign per the case's own note) | `formal/Semantics_L1.v` | structural; non-trivial — investigation owed; lambda-body's shadowing internal ERegion is the obstacle |
+| State and prove `preservation_l1` for both modes | `formal/Semantics_L1.v` | depends on region_shrink + region_liveness narrow admit |
 
 ### Near-term (L3 wiring — design + mechanisation)
 
@@ -99,10 +103,13 @@ enters the typing rules" and (for the diagram) in §6 (to be added).
 
 | Item | What it does | Notes |
 |---|---|---|
-| Add `T_Observe` to `has_type_l1` | Consumes a Linear echo / permits Affine lowering | Modality-aware: Linear ⇒ mandatory observation; Affine ⇒ optional silent lowering |
-| Add collapse-function emission to step rules at irreversible boundaries | `S_Region_Exit` emits `Echo (LiveAt_r) (ExitedAt_r) v_pre`; `S_Drop` emits `Echo T ⊤ v_pre` | Each irreversible step has an associated collapse function `f : A → B`; the echo is the proof-relevant preimage |
-| Thread `G` (echo context) alongside `R` (region context) through compound rules | New context parameter on every L1 compound rule | Parallel to R-threading; no overlap |
-| State and prove `preservation_l3` | Per-layer preservation theorem against the L3 invariants | Cross-layer dependency annotated in `PRESERVATION-DESIGN.md §5.1` |
+| ✅ Extend AST with [TEcho : ty -> ty] and [EEcho : ty -> expr -> expr] | Type former + runtime value form for L3 echoes | done 2026-05-27 (L3 wiring slice 1 — Syntax.v + free_regions + value/shift/subst cases) |
+| ✅ Add `T_Observe_L1` typing rule + `EObserve` expr form | Consumes a `TEcho T` echo, returns `TBase TUnit` | done 2026-05-27 (L3 wiring slice 2 — modality-polymorphic single rule; mandatoriness via `is_linear_ty TEcho`/implicit-drop discipline is a follow-up) |
+| ✅ Add `T_Echo_L1` typing rule | Types runtime [EEcho T v] residue values at `TEcho T` | done 2026-05-27 (L3 wiring slice 3a — typing-side counterpart of forthcoming `S_Region_Exit_Echo` / `S_Drop_Echo` step rules; mode-polymorphic) |
+| ✅ Add parallel typing rules `T_Region_L1_Echo` / `T_Region_Active_L1_Echo` / `T_Drop_L1_Echo` | Output `TEcho T` instead of `T` / `TBase TUnit`. Programs choose at typing time which path | done 2026-05-27 (L3 wiring slice 3b — owner-approved parallel-rule strategy). +3 internal admits in [region_shrink_preserves_typing_l1_gen_m] + [region_liveness_at_split_l1_gen] are parallel-rule MIRRORS of pre-existing structural admits, NOT new structural debt |
+| ✅ Add collapse-function emission to step rules at irreversible boundaries | `S_Region_Exit_Echo` emits `EEcho T v` paralleling `S_Region_Exit` (untouched); `S_Drop_Echo` emits `EEcho T (ELoc l r)` paralleling `S_Drop` | done 2026-05-27 (L3 wiring slice 3c — owner-approved parallel-rule strategy in Semantics.v; updated `step_from_eregion` to 4-disjunct classification + `step_R_change_shape` + `no_leaks_gen` cascade); rules quantified over witness type T |
+| ~~Thread `G` (echo context) alongside `R` (region context) through compound rules~~ | ~~New context parameter on every L1 compound rule~~ | **OBSOLETE 2026-05-27**: under the owner-approved parallel-rules design (slices 3a–3c), echoes are values of type `TEcho T` that flow through the existing `ctx` G. No separate echo-context parameter is needed. |
+| State and prove `preservation_l3` | Per-layer preservation theorem against the L3 invariants for the new echo-emitting step rules + echo-typed paths | Cross-layer dependency annotated in `PRESERVATION-DESIGN.md §5.1`. The four prerequisite slices (1, 2, 3a, 3b, 3c) all landed; `preservation_l3` is the capstone. |
 
 ### Mid-term (L4 — not started)
 
@@ -219,7 +226,7 @@ to the owner**:
 | `formal/Typing.v` (legacy) | n/a | 0 | 🛑 archaeology — `Counterexample.v` depends on falsity |
 | `formal/Counterexample.v` | **5** | 0 | ✅ pinned regression witness |
 | `formal/TypingL1.v` | **2** | 0 | ✅ active — L1 judgment, modality-indexed |
-| `formal/Semantics_L1.v` | **15** | **9** | ✅ active — 9 admits are L2-integration debt, not legacy patching |
+| `formal/Semantics_L1.v` | **23** | **3** | ✅ active — bullet-structure regressions + subst_typing_gen_l1_m + region_shrink_preserves_typing_l1_gen_m closed 2026-05-27; 3 residual admits are deeper L2-β debt (region_shrink T_Region_Active_L1 list-vs-multiset case now isolated in _gen_m internal admit, region_liveness_at_split narrow admit per ERegion counterexample, preservation_l1 cap) |
 | `formal/Modality.v` | **1** | 0 | ✅ active — L2 core, zero axioms |
 | `formal/Echo.v` | **12** | 0 | ✅ active — L3 calculus, not yet wired into L1 |
 | `formal/TypingL2.v` | (wrapper) | (wrapper) | ✅ thin re-indexing through `TypingL1.has_type_l1` |
 
@@ -249,6 +249,28 @@ Inductive step : config -> config -> Prop :=
       (mu, R, ERegion r v) -->>
         (mem_free_region mu r, remove_first r R, v)
 
+  (** L3 — parallel echo-emitting region-exit rule. Same trigger as
+      [S_Region_Exit] but the output is [EEcho T v] instead of [v],
+      packaging the pre-collapse witness in a runtime echo residue
+      for downstream [EObserve] consumption. Quantified universally
+      over the witness type [T]; preservation_l3 (slice 4) picks the
+      T that matches the typing derivation in [T_Region_L1_Echo] /
+      [T_Region_Active_L1_Echo].
+
+      The legacy [S_Region_Exit] above is untouched — programs that
+      typed via [T_Region_L1] (non-echo path) reduce via that rule;
+      programs that typed via [T_Region_L1_Echo] reduce via this
+      one. Non-deterministic at the relation level, but each typing
+      derivation pins the path. See [PRESERVATION-DESIGN.md §6.3]
+      and [formal/Echo.v]. *)
+
+  | S_Region_Exit_Echo : forall mu R r v T,
+      is_value v ->
+      In r R ->
+      expr_free_of_region r v ->
+      (mu, R, ERegion r v) -->>
+        (mem_free_region mu r, remove_first r R, EEcho T v)
+
   | S_Region_Step : forall mu R r e e' mu' R',
       In r R ->
       (mu, R, e) -->> (mu', R', e') ->
@@ -267,6 +289,16 @@ Inductive step : config -> config -> Prop :=
       (mu, R, EDrop (ELoc l r)) -->>
         (mem_write mu l CFree, R, EUnit)
 
+  (** L3 — parallel echo-emitting drop rule. Same trigger as
+      [S_Drop] but the output is [EEcho T (ELoc l r)] instead of
+      [EUnit], packaging the (pre-free) location witness in a
+      runtime echo residue. Quantified over witness type [T] —
+      preservation_l3 (slice 4) picks T to match [T_Drop_L1_Echo]. *)
+
+  | S_Drop_Echo : forall mu R l r T,
+      (mu, R, EDrop (ELoc l r)) -->>
+        (mem_write mu l CFree, R, EEcho T (ELoc l r))
+
   | S_Drop_Step : forall mu R e e' mu' R',
       (mu, R, e) -->> (mu', R', e') ->
       (mu, R, EDrop e) -->> (mu', R', EDrop e')
@@ -325,21 +357,28 @@ Proof.
     + destruct l; simpl in Hread; [discriminate | eapply IHmu; eassumption].
 Qed.
 
-(** Classify steps from ERegion — avoids hypothesis naming issues *)
+(** Classify steps from ERegion — avoids hypothesis naming issues.
+    L3 (slice 3c) adds a fourth disjunct for the [S_Region_Exit_Echo]
+    rule, which mirrors Exit's memory + region effects but packages
+    the post-step value in an [EEcho] residue. *)
 Lemma step_from_eregion :
   forall mu R r e mu1 R1 e1,
     (mu, R, ERegion r e) -->> (mu1, R1, e1) ->
-    (* Enter *) (mu1 = mu /\ R1 = r :: R /\ e1 = ERegion r e)
-    (* Exit *)  \/ (In r R /\ is_value e /\ mu1 = mem_free_region mu r
-                    /\ R1 = remove_first r R /\ e1 = e)
-    (* Step *)  \/ (In r R /\ exists e',
-                    (mu, R, e) -->> (mu1, R1, e')
-                    /\ e1 = ERegion r e').
+    (* Enter *)     (mu1 = mu /\ R1 = r :: R /\ e1 = ERegion r e)
+    (* Exit *)      \/ (In r R /\ is_value e /\ mu1 = mem_free_region mu r
+                        /\ R1 = remove_first r R /\ e1 = e)
+    (* Exit_Echo *) \/ (In r R /\ is_value e /\ mu1 = mem_free_region mu r
+                        /\ R1 = remove_first r R
+                        /\ exists T, e1 = EEcho T e)
+    (* Step *)      \/ (In r R /\ exists e',
+                        (mu, R, e) -->> (mu1, R1, e')
+                        /\ e1 = ERegion r e').
 Proof.
   intros. inversion H; subst.
   + left. auto.
   + right. left. repeat (split; [auto; fail|]). auto.
-  + right. right. split; [assumption|].
+  + right. right. left. repeat (split; [auto; fail|]). eexists. reflexivity.
+  + right. right. right. split; [assumption|].
     eexists. split; [eassumption | reflexivity].
 Qed.
 
@@ -384,7 +423,8 @@ Proof.
     destruct Hcases as
       [[-> [-> ->]]
       | [[_ [Hval_e [-> [-> ->]]]]
-      | [_ [e' [Hsub ->]]]]].
+      | [[_ [Hval_e [-> [-> [TT ->]]]]]
+      | [_ [e' [Hsub ->]]]]]].
     + (* Enter *)
       eapply (IH r mu (r :: R) e eq_refl mu' v l s Hcc Hval Hread).
     + (* Exit: body is a value, memory freed *)
@@ -396,6 +436,17 @@ Proof.
       assert (mem_free_region mu r = mu') by congruence.
       assert (e = v) by congruence.
       subst. eapply mem_free_region_clears. eassumption.
+    + (* Exit_Echo: mirror of Exit, but cc ends at the EEcho residue
+         (also a value via VEcho). Memory is freed the same way. *)
+      assert (Hcc2: cc = (mem_free_region mu r, remove_first r R, EEcho TT e)).
+      { inversion Hmulti.
+        - reflexivity.
+        - destruct c2 as [[? ?] ?].
+          exfalso. eapply values_dont_step.
+          + apply VEcho. exact Hval_e.
+          + eassumption. }
+      assert (mem_free_region mu r = mu') by congruence.
+      subst. eapply mem_free_region_clears. eassumption.
     + (* Step *)
       eapply (IH r _ _ e' eq_refl mu' v l s Hcc Hval Hread).
 Qed.
@@ -3676,6 +3727,8 @@ Proof.
     right; left; exists r; split; [reflexivity | assumption].
   - (* S_Region_Exit: R0' = remove_first r R0, In r R0 *)
     right; right; exists r; split; [reflexivity | assumption].
+  - (* S_Region_Exit_Echo: same R-shape as S_Region_Exit *)
+    right; right; exists r; split; [reflexivity | assumption].
 Qed.
 
 (** [output_ctx_det_across_step]: a generalization of [output_ctx_det]