From 5b338c2d5b7215c9bdfa507e0c7d6b725c9a7c59 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 19:40:20 +0100 Subject: [PATCH] proof(L3): add T_Echo_L1 typing rule for runtime echo values (slice 3a) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Slice 3a of the L3 wiring sequence. Slices 1 + 2 (PRs #190, #191) added the AST surface and the observation consumer; this slice closes the typing for the runtime echo VALUE form so that the forthcoming step rules (S_Region_Exit_Echo, S_Drop_Echo — slice 3b) have a type-preserving target. Changes (formal/TypingL1.v) * New typing rule T_Echo_L1 : has_type_l1 m R G (EEcho T v) (TEcho T) R G when [is_value v] and [has_type_l1 m R G v T R G]. Modality- polymorphic. Echoes are runtime values that preserve both R and G (no resource state change at the typing layer), mirroring T_Borrow_Val_L1's value-of-value pattern. Cascade fixes (formal/Semantics_L1.v) * value_R_G_preserving_l1 VEcho case: was [inversion Ht] expecting vacuity; now inverts to T_Echo_L1 which gives R_out = R and G_out = G directly. * shift_typing_gen_l1_m: explicit T_Echo_L1 bullet (uses shift_preserves_value for the value premise + IH for the witness typing). * subst_typing_gen_l1_m: explicit T_Echo_L1 bullet (uses subst_preserves_value + IH). * region_shrink_preserves_typing_l1_gen_m: explicit T_Echo_L1 bullet before Admitted (closes via IH on the witness; the is_value premise is preserved by structure). The new constructor's insertion BEFORE T_Observe_L1 in the inductive declaration shifted the bullet indices in three proofs; each now has the matching T_Echo_L1 bullet. What is NOT in this slice (still deferred) * S_Region_Exit_Echo / S_Drop_Echo step rules in Semantics.v (slice 3b — parallel-rule strategy approved by owner). * T_Region_L1_Echo / T_Drop_L1_Echo (parallel typing rules matching the new step-rule output type) — slice 3b. * G (echo context) threading through compound rules — slice 3c. * preservation_l3 — slice 4. Build oracle * coqc 8.18.0 closes the full formal/ tree. * Net debt unchanged (3 Admitted in Semantics_L1.v, all pre-existing). Refs PROOF-NEEDS.md §2 (L3 wiring). Refs PRESERVATION-DESIGN.md §6.3. Co-Authored-By: Claude Opus 4.7 (1M context) --- PROOF-NEEDS.md | 1 + formal/Semantics_L1.v | 27 ++++++++++++++++++++++----- formal/TypingL1.v | 19 +++++++++++++++++++ 3 files changed, 42 insertions(+), 5 deletions(-) diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index f81ab3d..7860fc6 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -105,6 +105,7 @@ 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 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` | diff --git a/formal/Semantics_L1.v b/formal/Semantics_L1.v index 44bc58a..67f471d 100644 --- a/formal/Semantics_L1.v +++ b/formal/Semantics_L1.v @@ -188,11 +188,10 @@ Proof. inversion Hv. + (* T_Borrow_Val_L1 *) split; reflexivity. - - (* VEcho T v — no L1 typing rule produces EEcho yet (L3 wiring is - a separate slice; see PROOF-NEEDS.md §2). The hypothesis [Ht] - on [EEcho T v] is therefore vacuous: [inversion] discharges - all impossible constructor cases. *) - inversion Ht. + - (* VEcho T v — T_Echo_L1 (slice 3a) types this at [TEcho T] + with R_out = R and G_out = G by construction; both invariants + hold immediately. *) + inversion Ht; subst; split; reflexivity. Qed. (** ** Helper: region-environment shrinkage for value typings. @@ -548,6 +547,11 @@ Proof. eapply T_Drop_L1; [exact H | eapply IHHt; auto]. - (* T_Copy_L1 *) eapply T_Copy_L1; [exact H | eapply IHHt; auto]. + - (* T_Echo_L1 — region shrink under an echo value preserves the + value structure (region-free witness implies a region-free echo). *) + eapply T_Echo_L1. + + exact H. + + eapply IHHt; auto. - (* T_Observe_L1 — region shrink commutes with the witness sub-expression *) eapply T_Observe_L1. eapply IHHt; auto. Admitted. @@ -940,6 +944,12 @@ Proof. - eapply T_Drop_L1; [exact H |]. apply IHHtype. assumption. (* T_Copy_L1 *) - eapply T_Copy_L1; [exact H |]. apply IHHtype. assumption. + (* T_Echo_L1 — runtime echo value typing; shift commutes with the + witness sub-expression. The is_value premise is preserved by + [shift_preserves_value]. *) + - eapply T_Echo_L1. + + apply shift_preserves_value. exact H. + + apply IHHtype. assumption. (* T_Observe_L1 — shift commutes with the witness sub-expression *) - eapply T_Observe_L1. apply IHHtype. assumption. Qed. @@ -1446,6 +1456,13 @@ Proof. (* T_Copy_L1 *) - eapply T_Copy_L1; [exact H |]. eapply IHHtype; eassumption. + (* T_Echo_L1 — substitution under an echo value: the witness is a + value, so [subst_preserves_value] preserves [is_value]. The + witness's typing is preserved by the IH. *) + - eapply T_Echo_L1. + + apply subst_preserves_value. assumption. + + eapply IHHtype; eassumption. + (* T_Observe_L1 *) - eapply T_Observe_L1. eapply IHHtype; eassumption. Qed. diff --git a/formal/TypingL1.v b/formal/TypingL1.v index de29ad3..7c83622 100644 --- a/formal/TypingL1.v +++ b/formal/TypingL1.v @@ -291,6 +291,25 @@ Inductive has_type_l1 R ; G |=L1[m] e : T -| R' ; G' -> R ; G |=L1[m] ECopy e : TProd T T -| R' ; G' + (** ===== L3 — Echo / residue value typing ===== + + [T_Echo_L1] types the runtime [EEcho T v] residue at [TEcho T], + provided the witness [v] is itself a value typed at [T]. This + is the typing-side counterpart of the (forthcoming, slice 3b / + 3c) step rules that emit echoes at irreversible boundaries: + [S_Region_Exit_Echo] and [S_Drop_Echo] will both produce + [EEcho T v_pre] residues which must be typable for preservation + to hold. + + Modality-polymorphic: holds in both [Linear] and [Affine]. The + [is_value v] premise mirrors [T_Borrow_Val_L1] — echoes are + runtime-only values, not surface syntax. *) + + | T_Echo_L1 : forall m R G v T, + is_value v -> + R ; G |=L1[m] v : T -| R ; G -> + R ; G |=L1[m] EEcho T v : TEcho T -| R ; G + (** ===== L3 — Echo / residue observation ===== [T_Observe_L1] discharges an echo by witnessing it. The rule is