From 7404fbde35d5b95fda428f596753185346c91831 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 21:52:02 +0100 Subject: [PATCH] =?UTF-8?q?proof(L3):=20preservation=5Fl3=20capstone=20?= =?UTF-8?q?=E2=80=94=20slice=204=20(closes=20L3=20wiring)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per-layer preservation theorem for the two L3-specific echo-emitting step rules (S_Region_Exit_Echo / S_Drop_Echo) paired with their matching L3 typing rules (T_Region_Active_L1_Echo / T_Drop_L1_Echo + T_Echo_L1). Three new Qed in formal/Semantics_L1.v: - preservation_l3_region_active_echo For (T_Region_Active_L1_Echo, S_Region_Exit_Echo) pair: value_R_G_preserving_l1 pins body output context, then region_shrink_preserves_typing_l1_gen_m + T_Echo_L1 close. - preservation_l3_drop_echo For (T_Drop_L1_Echo, S_Drop_Echo) pair: value invariance (VLoc) + T_Echo_L1 directly. - preservation_l3 (umbrella) Conjunction of the two per-case lemmas. Each conjunct corresponds to one (L3 typing rule, L3 step rule) matched pair. Per-case alignment forced by T_Echo_L1's witness- type premise — non-deterministic crossover cases are non-preserving by design (typing derivation pins the path). Seam audit + slice-4 tightening (no new debt, one debt closed): - region_shrink_preserves_typing_l1_gen_m: tightened from 3 internal admits to 2. The avoidable T_Region_L1_Echo case (parallel mirror of a fully-closed T_Region_L1 case) is now Qed-style via count-monotonicity (shadowed sub-case) + remove_first commutation (descend sub-case). The descend sub-case of T_Region_Active_L1_Echo is also Qed-style now — only the shadowed sub-case remains as a true parallel mirror of the pre-existing T_Region_Active_L1 list-vs-multiset structural admit at line 553. - All 5 remaining internal admit. cases classified: Pre-existing L1 structural: lines 553, 1256, 1694 True parallel mirrors: lines 621, 1276 (mirrors close when originals close — same structural debt) - All 3 outer Admitted. markers track the internal admit set; no new outer Admitted introduced. - Semantics.v's legacy preservation Admitted. is sacrosanct (provably false per Counterexample.v) and untouched. Per CLAUDE.md owner directive 2026-05-27: ✓ Zero new Admitted. or Axiom. declarations ✓ No legacy Semantics.v patching ✓ No cross-layer reasoning to close L1 admits ✓ Re-uses pre-existing infrastructure only PROOF-NEEDS.md updates: - §2 L3 wiring row marked ✅ done with full disposition - §1 Linear-mode forward progress count 23 → 26 Qed - §4 file-by-file table updated - NEW §4 "Seam audit (slice 4, 2026-05-27)" subsection classifies every admit/axiom in formal/*.v explicitly Build status: full clean rebuild (coqc 8.18.0) passes for all 9 .v files in dependency order — Syntax, Typing, Modality, TypingL1, Semantics, Echo, Semantics_L1, Counterexample, TypingL2. Co-Authored-By: Claude Opus 4.7 (1M context) --- PROOF-NEEDS.md | 33 ++++++- formal/Semantics_L1.v | 206 +++++++++++++++++++++++++++++++++++++++--- 2 files changed, 223 insertions(+), 16 deletions(-) diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 072ed62a..9c44762a 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -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` | 23 Qed; 3 residual admits (L2-β follow-up) | +| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 26 Qed (incl. 3 new from L3 slice 4: `preservation_l3_region_active_echo` / `preservation_l3_drop_echo` / `preservation_l3` umbrella); 3 outer `Admitted.` markers cover 5 internal `admit.` cases — all pre-existing L1 structural debt OR true parallel mirrors | | 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 | @@ -106,10 +106,10 @@ enters the typing rules" and (for the diagram) in §6 (to be added). | ✅ 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 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). Initial +3 internal admits in [region_shrink_preserves_typing_l1_gen_m] + [region_liveness_at_split_l1_gen] were parallel-rule MIRRORS of pre-existing structural admits; the avoidable T_Region_L1_Echo mirror was CLOSED in slice 4 — only the two true T_Region_Active_*_L1_Echo shadowed-case mirrors remain, both blocked by the same pre-existing list-vs-multiset structural debt as the originals | | ✅ 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. | +| ✅ State and prove `preservation_l3` | Per-layer preservation theorem against the L3 invariants for the new echo-emitting step rules + echo-typed paths | done 2026-05-27 (L3 wiring slice 4 — capstone). Two per-case Qed lemmas (`preservation_l3_region_active_echo` for `S_Region_Exit_Echo` × `T_Region_Active_L1_Echo`, and `preservation_l3_drop_echo` for `S_Drop_Echo` × `T_Drop_L1_Echo`) plus an umbrella `preservation_l3` (their conjunction, Qed). Zero new admits or axioms. Per-case alignment forced by `T_Echo_L1`'s witness-type premise; non-deterministic crossover cases are non-preserving by design (typing derivation pins the path). Conditionally Qed under the pre-existing `region_shrink_preserves_typing_l1_gen_m` L1 structural admit per PRESERVATION-DESIGN.md §5.1. | ### Mid-term (L4 — not started) @@ -226,12 +226,37 @@ 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` | **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/Semantics_L1.v` | **26** | **3** | ✅ active — bullet-structure regressions + subst_typing_gen_l1_m + region_shrink_preserves_typing_l1_gen_m closed 2026-05-27; 3 residual outer `Admitted.` markers cover 5 internal `admit.` cases — all pre-existing L1 structural debt OR true parallel mirrors (T_Region_Active_*_L1_Echo shadowed sub-cases mirror T_Region_Active_L1's debt; the avoidable T_Region_L1_Echo mirror was closed in slice 4). Slice 4 added 3 new Qed: `preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, `preservation_l3` (umbrella). Zero new admits. | | `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` | | `src/abi/Ephapax/…` (Idris2) | n/a | n/a | ✅ active — ABI, Region linearity, no `believe_me` / `sorry` / `assert_total` | +### Seam audit (slice 4, 2026-05-27): every admit/axiom classified + +Every `admit.` and `Admitted.` in `formal/*.v` after L3 slice 4 +landed. No new debt was introduced; the avoidable T_Region_L1_Echo +mirror was closed. The remaining set is exactly the **pre-existing +L1 structural debt** (with two true parallel mirrors that close +when their originals close) plus the **sacrosanct legacy +preservation** (provably false per `Counterexample.v`). + +| Location | Class | Closes when | +|---|---|---| +| `Semantics_L1.v:553` (`admit.`) | **Pre-existing** L1 structural — `region_shrink_preserves_typing_l1_gen_m` / T_Region_Active_L1 shadowed sub-case; list-vs-multiset gap | L1 perm/multiset bridge OR `T_Region_*_L1` redesign | +| `Semantics_L1.v:621` (`admit.`) | **Parallel mirror** of `:553` — T_Region_Active_L1_Echo shadowed sub-case; structurally identical | Same as `:553` (mechanical replay) | +| `Semantics_L1.v:653` (`Admitted.`) | **Outer marker** — depends on internal `:553` + `:621` | When both internal admits close | +| `Semantics_L1.v:1256` (`admit.`) | **Pre-existing** L1 structural — `region_liveness_at_split_l1_gen` / T_Region_Active_L1 `r = rv` sub-case; "GENUINELY FALSE" counterexample documented at site | L2 effect-typed `TFun` per `PRESERVATION-DESIGN.md §5.1` | +| `Semantics_L1.v:1276` (`admit.`) | **Parallel mirror** of `:1256` — T_Region_Active_L1_Echo `r = rv` sub-case | Same as `:1256` (mechanical replay) | +| `Semantics_L1.v:1290` (`Admitted.`) | **Outer marker** — depends on internal `:1256` + `:1276` | When both internal admits close | +| `Semantics_L1.v:1694` (`admit.`) | **Pre-existing** — `preservation_l1` body; lambda-rigidity gap per `PRESERVATION-DESIGN.md §4.8` | L2 effect-typed `TFun` (Phase 2) | +| `Semantics_L1.v:1695` (`Admitted.`) | **Outer marker** — depends on internal `:1694` | When `:1694` closes | +| `Semantics.v:9257` (`Admitted.`) | **🛑 Sacrosanct** — legacy `Theorem preservation`, **provably false** per `Counterexample.v` (owner directive 2026-05-27) | Never. The `Admitted.` is correct. | + +No `Axiom` declarations in `formal/*.v`. Counterexample.v carries 5 +Qed; TypingL1.v / Modality.v / Echo.v / TypingL2.v are all +admit-free. + ### Idris2 side (proof carriers, not Coq mechanisation) | Concern | File(s) | Status | diff --git a/formal/Semantics_L1.v b/formal/Semantics_L1.v index e67cefc7..7eec61fa 100644 --- a/formal/Semantics_L1.v +++ b/formal/Semantics_L1.v @@ -564,18 +564,74 @@ Proof. * exact H0. * apply remove_first_preserves_other; [intro Hbad; apply Heq; exact Hbad | exact H1]. * eapply IHHt. exact Hfree. - - (* T_Region_L1_Echo — same structural shape as T_Region_L1; the - proof is identical modulo the output-type [TEcho T] vs [T]. - Both subcases (shadowed + descend) follow the original's - analysis. Admitted here as the outer lemma is already - [Admitted] and the structural residual (shadowed sub-case in - T_Region_Active_L1_Echo) bridges the same list-vs-multiset - gap documented above. *) - admit. - - (* T_Region_Active_L1_Echo — parallels T_Region_Active_L1 - including the residual structural admit in the shadowed - sub-case (PROOF-NEEDS.md §2). *) - admit. + - (* T_Region_L1_Echo — structurally identical to T_Region_L1 + modulo the output-type [TEcho T] vs [T]. Both subcases close + directly (shadowed via count-monotonicity vacuity, descend + via remove_first/remove_first_L1 commutation). Closed in + slice 4 to honor the "no parallel-rule admit-debt" seam-audit + directive — the original T_Region_L1 case has zero admits, + so its mirror has zero admits too. *) + destruct (String.eqb rr r) eqn:Heq. + + (* rr = r: shadowed. *) + apply String.eqb_eq in Heq. subst r. + rewrite (remove_first_not_in_id _ _ H). + destruct (in_dec string_dec rr (remove_first_L1 rr R_body)) as [Hin | Hnotin]. + * (* Multiple rr's in R_body — VACUOUS by count monotonicity. *) + exfalso. + pose proof (count_occ_le_l1_m _ _ _ _ _ _ _ Ht rr) as Hle. + unfold cnt in Hle. simpl in Hle. + destruct (string_dec rr rr) as [_|Hbad]; [|apply Hbad; reflexivity]. + apply (count_occ_In string_dec) in Hin. + pose proof (remove_first_L1_count_eq_self rr R_body) as Hself. + unfold cnt in Hself. rewrite Hself in Hin. + apply (count_occ_not_In string_dec) in H. + lia. + * (* At most one rr in R_body. *) + rewrite (remove_first_not_in_id _ _ Hnotin). + eapply T_Region_L1_Echo; eauto. + + (* rr <> r: descend. *) + apply String.eqb_neq in Heq. + assert (Hgoal_eq : remove_first rr (remove_first_L1 r R_body) = + remove_first_L1 r (remove_first rr R_body)). + { rewrite (remove_first_eq_l1 r R_body). + rewrite (remove_first_eq_l1 r (remove_first rr R_body)). + apply remove_first_comm. } + rewrite Hgoal_eq. + eapply T_Region_L1_Echo. + * 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). + simpl in IHHt. + destruct (String.eqb rr r) eqn:Heq2. + -- exfalso. apply String.eqb_eq in Heq2. apply Heq. exact Heq2. + -- exact IHHt. + - (* T_Region_Active_L1_Echo — parallels T_Region_Active_L1. + The descend sub-case closes directly; the shadowed sub-case + (rr = r) is the same list-vs-multiset structural residual as + in T_Region_Active_L1 above. Per slice 4 seam audit: the + shadowed sub-case admit is a TRUE MIRROR of the pre-existing + L1 structural admit at line 553. The descend sub-case is + closed Qed-style in slice 4 (not an admit). *) + destruct (String.eqb rr r) eqn:Heq. + + (* rr = r: shadowed — list-vs-multiset mirror of line 553. + Resolution path is identical to its non-Echo counterpart: + option (a) L1 perm lemma, (b) multiset reformulation, or + (c) T_Region_*_L1 redesign. See line 542-552 design note. *) + admit. + + (* rr <> r: descend. *) + apply String.eqb_neq in Heq. + assert (Hgoal_eq : remove_first rr (remove_first_L1 r R_body) = + remove_first_L1 r (remove_first rr R_body)). + { rewrite (remove_first_eq_l1 r R_body). + rewrite (remove_first_eq_l1 r (remove_first rr R_body)). + apply remove_first_comm. } + rewrite Hgoal_eq. + eapply T_Region_Active_L1_Echo. + * apply remove_first_preserves_other; [intro Hbad; apply Heq; exact Hbad | exact H]. + * exact H0. + * apply remove_first_preserves_other; [intro Hbad; apply Heq; exact Hbad | exact H1]. + * eapply IHHt. exact Hfree. - (* T_Borrow_L1 *) eapply T_Borrow_L1. exact H. - (* T_Borrow_Val_L1 *) @@ -1637,3 +1693,129 @@ Proof. intros m mu R e mu0 R0 e0 Hstep G T R_final G_out Ht. admit. Admitted. + +(** ** L3 preservation theorem (slice 4 of L3 wiring — capstone) + + Per-layer preservation theorem for the two L3-specific + echo-emitting step rules [S_Region_Exit_Echo] and [S_Drop_Echo] + (Semantics.v slice 3c) paired with their matching L3 typing + rules [T_Region_Active_L1_Echo] / [T_Drop_L1_Echo] + + [T_Echo_L1] for the result (TypingL1.v slices 2 / 3a / 3b). + + Stated as two per-case lemmas + an umbrella theorem + [preservation_l3] which is their conjunction. + + Design constraint (PRESERVATION-DESIGN.md §6.3 + + PROOF-NEEDS.md §2): the L3 step rules are universally + quantified over the witness type [T] in the [EEcho T v] + residue. The non-determinism is resolved at the typing- + derivation level — each L3 typing rule pins [T] to its body + type. The per-case lemmas state preservation for the + matching (typing-rule, step-rule) pairs only; "cross-path" + pairs (e.g. legacy [T_Region_Active_L1] + L3 + [S_Region_Exit_Echo]) are non-preserving by design and not + well-typed at the umbrella's [TEcho T] output. + + Per CLAUDE.md owner directive 2026-05-27, slice 4: + - introduces ZERO new [Admitted.] or [Axiom] declarations; + - does NOT patch legacy [Semantics.v] preservation; + - re-uses already-proved infrastructure + ([value_R_G_preserving_l1] Qed, + [region_shrink_preserves_typing_l1_gen_m] — admitted at + the L1 layer for the T_Region_Active_L1 shadowed + sub-case; cross-layer dependency annotated in + PRESERVATION-DESIGN.md §5.1). + + Cross-layer accounting: the [region_shrink_preserves_typing_l1_gen_m] + dependency is a pre-existing L1 structural admit (closes at + L2-effect-typed-TFun per design doc §5.1). Slice 4 does NOT + widen, duplicate, or open it — preservation_l3 is + *conditionally* Qed under that pre-existing L1 obligation. *) + +(** *** Case 1: [S_Region_Exit_Echo] paired with + [T_Region_Active_L1_Echo]. + + The typing premise extracts the body's typing + [R; G |=L1[m] v : T -| R_body; G']; since [v] is a value, + [value_R_G_preserving_l1] forces [R_body = R] and [G' = G]. + Region shrinkage then provides the post-step witness typing + at [remove_first r R], and [T_Echo_L1] wraps it. *) + +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 *) + is_value v -> + expr_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'. +Proof. + intros m R G r v T R_body G' HinR HnotT Htbody Hv Hfree. + (* Value-invariance: R_body = R and G' = G. *) + pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hv Htbody) + as [HR HG]. + subst R_body G'. + (* Bridge [remove_first_L1] (typing-side) to [remove_first] + (semantics-side) — both pointwise equal by + [remove_first_eq_l1] (Qed). *) + replace (remove_first_L1 r R) with (remove_first r R) + by (symmetry; apply remove_first_eq_l1). + (* Goal: (remove_first r R); G |- EEcho T v : TEcho T + -| (remove_first r R); G *) + apply T_Echo_L1; [ exact Hv | ]. + (* Goal: (remove_first r R); G |- v : T + -| (remove_first r R); G + This is exactly region shrinkage at [v] (free of [r]). *) + apply (region_shrink_preserves_typing_l1_gen_m m _ _ _ _ _ _ Htbody _ Hfree). +Qed. + +(** *** Case 2: [S_Drop_Echo] paired with [T_Drop_L1_Echo]. + + The typing premise extracts + [R; G |=L1[m] ELoc l r : T -| R'; G']. Since [ELoc l r] is + a value (VLoc), value-invariance forces [R' = R] and + [G' = G]. Then [T_Echo_L1] applies directly — no region + shrinkage needed (step does not change [R]). *) + +Lemma preservation_l3_drop_echo : + forall m R G l r T R' G', + (* T_Drop_L1_Echo premises *) + is_linear_ty T = true -> + has_type_l1 m R G (ELoc l r) T R' G' -> + (* Conclusion: post-step types at [TEcho T] *) + has_type_l1 m R G (EEcho T (ELoc l r)) (TEcho T) R' G'. +Proof. + intros m R G l r T R' G' Hlin Htbody. + pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ _ + (VLoc l r) Htbody) as [HR HG]. + subst R' G'. + apply T_Echo_L1; [ apply VLoc | exact Htbody ]. +Qed. + +(** *** Umbrella: [preservation_l3] is the conjunction of the + two per-case lemmas above. Each conjunct corresponds to one + (L3 typing rule, L3 step rule) matched pair. *) + +Theorem preservation_l3 : + (forall m R G r v T R_body G', + In r R -> + ~ 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 -> + has_type_l1 m (remove_first r R) G + (EEcho T v) (TEcho T) (remove_first_L1 r R_body) G') + /\ + (forall m R G l r T R' G', + is_linear_ty T = true -> + has_type_l1 m R G (ELoc l r) T R' G' -> + has_type_l1 m R G (EEcho T (ELoc l r)) (TEcho T) R' G'). +Proof. + split. + - exact preservation_l3_region_active_echo. + - exact preservation_l3_drop_echo. +Qed.