From dedbb6ddde456efaec4cbdfc13df7e241784a8da Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 07:29:55 +0000 Subject: [PATCH 1/2] fix(formal): retire the three refuted Admitted statements to Prop (D0, D0b) Owner-ratified 2026-11-05. While Semantics.preservation, step_pop_disjoint_from_type_l1 and preservation_l1 were Admitted next to Qed refutations, the build could derive False. - Semantics.preservation -> preservation_stmt : Prop; Counterexample.v adds preservation_false : ~ preservation_stmt (Qed). The 700-line partial proof script is removed (kept in git history). - step_pop_disjoint_from_type_l1 and preservation_l1 -> ..._stmt : Prop; their _FALSE refutations are restated against them. - preservation_l2_via_l1 / preservation_l2_lift_case take preservation_l1_stmt as an explicit hypothesis. - coq-build.yml: the Print Assumptions step becomes a no-False gate (no Admitted/Axiom/Parameter in _CoqProject files; 6/6 results closed). - CLAUDE.md fence, PROOF-NEEDS (marker 3 -> 0), EXPLAINME and V1-TO-V2 record the retirement. Retired, not closed: no refuted statement is proved. Verified locally: coqc 8.18.0 full build exit 0; 0 Admitted, 0 Axiom; 30/30 Print Assumptions in the build closed; the gate fails on a planted Admitted; status-gate --proofs OK (0). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- .github/workflows/coq-build.yml | 51 +- CLAUDE.md | 44 +- EXPLAINME.adoc | 20 +- PROOF-NEEDS.adoc | 69 ++- V1-TO-V2.adoc | 23 +- formal/Counterexample.v | 21 +- formal/Counterexample_PreservationL1.v | 7 +- formal/Counterexample_StepPop.v | 6 +- formal/Semantics.v | 784 +------------------------ formal/Semantics_L1.v | 82 +-- formal/TypingL2.v | 8 +- 11 files changed, 190 insertions(+), 925 deletions(-) diff --git a/.github/workflows/coq-build.yml b/.github/workflows/coq-build.yml index a7546a1b..951fe216 100644 --- a/.github/workflows/coq-build.yml +++ b/.github/workflows/coq-build.yml @@ -16,10 +16,9 @@ # `coq_makefile`-driven compilation of `formal/_CoqProject` fails # here BEFORE the admin-merge button is reachable for the auto-bot. # -# The job also `Print Assumptions`-checks the four Phase D top-level -# results (preservation_l1 at L1; preservation_l2_via_l1 plus the two -# Ξ²-case lemmas at L2) so any new `Admitted.` / `Axiom` slippage shows -# up as a diff in the workflow output. +# The job also runs the no-False gate: no `Admitted.` / `Axiom` / +# `Parameter` in any `_CoqProject` file, and the refutations plus the +# conditional L2 results must print "Closed under the global context". # # **Why an aggregator gate?** The `coq-build` job is path-filtered: it # only does real work when `formal/**` or this workflow file changes. @@ -128,26 +127,40 @@ jobs: coq_makefile -f _CoqProject -o build.mk make -f build.mk - - name: Print Assumptions of Phase D theorems + - name: No-False gate (D0/D0b, owner-ratified 2026-11-05) working-directory: formal run: | - # Surfaces any new Admitted / Axiom additions feeding into - # the four Phase D top-level results. A diff in this output - # between PRs is the canonical "did this PR introduce a new - # admit" signal. - # preservation_l1 (Semantics_L1.v) - # preservation_l2_via_l1 (TypingL2.v) - # preservation_l2_app_eff_beta_linear (TypingL2.v, #228) - # preservation_l2_app_eff_beta_ground_nonlinear (TypingL2.v, #233) - # Single coqtop session amortises ML startup across four prints. - coqtop -R . Ephapax 2>&1 <<'EOF' | tail -160 - From Ephapax Require Import Semantics_L1. - From Ephapax Require Import TypingL2. - Print Assumptions preservation_l1. + # The build is axiom-free: no `Admitted.` and no `Axiom` / + # `Parameter` in any `_CoqProject` file. While a refuted + # statement was `Admitted`, the build could derive `False` + # (see docs/reports/2026-11-04-v2-survey, F0/F1). Assuming + # Coq's own consistency, an axiom-free build cannot. + set -euo pipefail + FILES=$(grep -E '\.v$' _CoqProject) + if grep -nE '^[[:space:]]*(Admitted\.|Axiom[[:space:]]|Parameter[[:space:]])' $FILES; then + echo "no-False gate: Admitted/Axiom/Parameter found above -> FAIL" + exit 1 + fi + # Every headline and refutation must be closed under the global + # context; any `Axioms:` block fails the gate. + OUT=$(coqtop -R . Ephapax 2>&1 <<'EOF2' + From Ephapax Require Import Semantics Semantics_L1 TypingL2. + From Ephapax Require Import Counterexample Counterexample_StepPop Counterexample_PreservationL1. + Print Assumptions Counterexample.preservation_false. + Print Assumptions Counterexample_StepPop.step_pop_disjoint_from_type_l1_FALSE. + Print Assumptions Counterexample_PreservationL1.preservation_l1_FALSE. Print Assumptions preservation_l2_via_l1. Print Assumptions preservation_l2_app_eff_beta_linear. Print Assumptions preservation_l2_app_eff_beta_ground_nonlinear. - EOF + EOF2 + ) + echo "$OUT" | tail -60 + if echo "$OUT" | grep -qE '^Axioms:|Error'; then + echo "no-False gate: a printed result depends on an axiom, or coqtop errored -> FAIL" + exit 1 + fi + test "$(echo "$OUT" | grep -c 'Closed under the global context')" -eq 6 + echo "no-False gate: PASS (0 Admitted, 0 Axiom, 6/6 closed)" # Always-on aggregator. This is the ONLY job listed in the Base ruleset's # required_status_checks rule (#244). If detect-relevant-changes determined diff --git a/CLAUDE.md b/CLAUDE.md index a99657ee..b290cb23 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -100,7 +100,18 @@ redesign and state sound replacement theorems, not to prove refuted ones. - **Proof, L4** β€” Phase A scaffold landed; mother–child dyadic semantics (`PRESERVATION-DESIGN.adoc Β§7`) is the next design step. -## πŸ›‘ Owner directive snapshot (2026-05-27) β€” legacy fence plus later L1 regressions +## πŸ›‘ Owner directive snapshot (2026-05-27, revised 2026-11-05) β€” legacy fence plus later L1 regressions + +> **2026-11-05 revision (owner-ratified D0 and D0b).** The three refuted +> statements are retired, not closed: `Semantics.preservation` is now +> `preservation_stmt : Prop`, refuted by `Counterexample.preservation_false`; +> `step_pop_disjoint_from_type_l1` and `preservation_l1` are now +> `…_stmt : Prop`, refuted by `Counterexample_StepPop.v` and +> `Counterexample_PreservationL1.v`. While they were `Admitted`, the build +> could derive `False`. `formal/` now has **0 `Admitted` and 0 `Axiom`**, +> and CI's no-False gate (`coq-build.yml`) blocks any new +> `Admitted`/`Axiom`/`Parameter`. The fence below is unchanged in spirit: +> never try to prove a refuted statement. > The guardrails below protect pinned counterexamples and the false > statements they refute. They do **not** mean "skip this repo." The @@ -113,10 +124,10 @@ redesign and state sound replacement theorems, not to prove refuted ones. Ephapax preservation as originally stated in `formal/Semantics.v` is **provably false** β€” and that is a *result*, not a defeat: `formal/Counterexample.v` exhibits a concrete configuration that types, -steps, and lands at an untypable post-state (5 lemmas `Qed`), which +steps, and lands at an untypable post-state (now 6 lemmas `Qed`, incl. `preservation_false`), which named an invariant missing from the legacy judgment. So the work is **not** -to close `Theorem preservation` in `Semantics.v` (no closure exists; the -`Admitted` is deliberate). Nor should the current unrestricted L1 +to close the legacy preservation in `Semantics.v` (no closure exists; it +is retired to `preservation_stmt : Prop`, refuted by `preservation_false`). Nor should the current unrestricted L1 preservation be treated as routine debt: `Counterexample_StepPop.v` and `Counterexample_PreservationL1.v` refute its supporting claim and capstone. There is no unconditional L2 preservation theorem; the L2 Ξ²-case helpers @@ -130,9 +141,11 @@ counterexample and state any replacement theorem with its exact boundary. These are anti-patterns that have wasted real session time. Refuse them if asked; if asked anyway, push back and link this section. -1. **DO NOT close `Theorem preservation` in `formal/Semantics.v`.** - It is FALSE. No proof technique closes it because no proof - exists. The `Admitted.` is correct. +1. **DO NOT prove or restate the legacy preservation in + `formal/Semantics.v`.** It is FALSE and is refuted by + `Counterexample.preservation_false`. It stays `preservation_stmt : Prop`; + never turn it back into a `Theorem`/`Lemma`, and never re-add an + `Admitted.` for it. 2. **DO NOT extend `formal/Semantics.v`** with new lemmas aimed at closing the legacy preservation: not Lemma B variants @@ -144,10 +157,12 @@ them if asked; if asked anyway, push back and link this section. invariant the counterexample demands; no lemma collection bolted onto it will help. -3. **DO NOT try to complete the current unrestricted - `step_pop_disjoint_from_type_l1` or `preservation_l1` statements in - `formal/Semantics_L1.v`.** Both are refuted by pinned witnesses; their - `Admitted.` markers are transparent boundaries, not ordinary debt. +3. **DO NOT try to prove the unrestricted + `step_pop_disjoint_from_type_l1_stmt` or `preservation_l1_stmt` + statements in `formal/Semantics_L1.v`.** Both are refuted by pinned + witnesses and retired to `Prop`; they are not debt. Results that need + them take them as explicit hypotheses (as `preservation_l2_via_l1` + now does). Do not route around the counterexamples with ad-hoc side conditions or helper-signature changes. A separately stated sound theorem after an owner-approved judgment/step redesign is allowed and expected. @@ -162,7 +177,7 @@ them if asked; if asked anyway, push back and link this section. 5. **DO NOT patch the legacy `Typing.v` judgment.** It is the pre-redesign judgment. `Counterexample.v` depends on its - falsity for the regression theorem. Leave it. + falsity for `preservation_false`. Leave it. ### DO @@ -212,8 +227,9 @@ escalate to the owner: - region-weakening predicates indexed on syntactic shape, - admit-shuffling between `Semantics.v` and a new lemma, - "the previous-PR-line-of-attack just needs one more lemma," -- proposing to close `Theorem preservation` in `Semantics.v` to - `Qed.` by any chain of reasoning, +- proposing to prove `preservation_stmt` (or turn it back into a + `Theorem`) by any chain of reasoning, +- re-adding any `Admitted.` to `formal/` (the no-False gate will fail), - adding new `Axiom` declarations to discharge L1/L2 gaps. ### If you're unsure diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 31aef6d8..48c2222f 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -224,10 +224,14 @@ the exact preservation boundary is recorded below. .Post-counterexample 2026-05-26 β€” read this before any older proof claim ==== The legacy preservation theorem in `formal/Semantics.v` is **provably -false**. `formal/Counterexample.v` (5 Qed lemmas) demonstrates a +false**. `formal/Counterexample.v` (6 Qed lemmas) demonstrates a configuration that types under the legacy judgment, steps via the -operational semantics, and lands at an untypable post-state. The -`Admitted.` on `Theorem preservation` is correct β€” no proof closes it. +operational semantics, and lands at an untypable post-state, and +`preservation_false` refutes the statement outright. No proof closes it: +since the owner-ratified D0b (2026-11-05) it is retired to +`preservation_stmt : Prop` rather than kept `Admitted`, because an +`Admitted` false statement let the build derive `False`. `formal/` now has +0 `Admitted` and 0 `Axiom`. The post-discovery architecture is a design program, not yet a sound replacement. The unrestricted L1 preservation statement is refuted by @@ -257,7 +261,7 @@ Qed results are scoped to matching echo rule pairs. | L1 semantics | πŸ›‘ Current unrestricted preservation statements refuted -| `formal/Semantics_L1.v` has two outer `Admitted.` markers: `step_pop_disjoint_from_type_l1` and `preservation_l1`. Both unrestricted statements have pinned Coq counterexamples; they are not routine open proof debt. See `PROOF-NEEDS.adoc`. +| `formal/Semantics_L1.v` retires `step_pop_disjoint_from_type_l1` and `preservation_l1` to `Prop` statements (`…_stmt`, D0, 2026-11-05); it has no `Admitted`. Both unrestricted statements have pinned Coq counterexamples; they are not open proof debt. See `PROOF-NEEDS.adoc`. | L2 modality (`Modality.v`) | βœ… Core landed (1 Qed, 0 axioms) @@ -272,8 +276,8 @@ Qed results are scoped to matching echo rule pairs. | `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` enum + `program_mode_to_modality` round-trip. No theorems by design. Design in `formal/PRESERVATION-DESIGN.adoc Β§7`. | Legacy `Theorem preservation` (`formal/Semantics.v`) -| πŸ›‘ Provably false (Admitted) -| Pinned by `Counterexample.v`. **Do not attempt closure.** Archaeology. +| πŸ›‘ Provably false (retired to `preservation_stmt : Prop`, D0b 2026-11-05) +| Refuted by `Counterexample.preservation_false`. **Do not attempt closure.** Archaeology. |=== What's done = `Modality.linear_to_affine` (Linear β‡’ Affine weakening, @@ -310,8 +314,8 @@ documentation comments were clarified. |Coq 8.18.0; project build recipe above |`+formal/Counterexample.v+`: `+bad_typable+`, `+bad_step+`, `+bad_post_untypable+` |Concrete witness refutes the legacy universal statement only. It proves -no redesign or implementation refinement; retain the separate legacy -`+Admitted.+` unchanged. +no redesign or implementation refinement. The legacy statement is +retired to `+preservation_stmt+` and refuted by `+preservation_false+`. |`+step_pop_disjoint_from_type_l1+` is false as stated |proven |Coq 8.18.0; project build recipe above diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index c6932d07..6f4a5d75 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -33,9 +33,24 @@ This file is the proof-status audit for Ephapax. It supersedes earlier versions that treated the legacy preservation closure plan as viable. Keep these categories distinct: -* *Legacy archaeology*: the original `+preservation+` statement is false; - its durable `+Admitted.+` and pinned five-`+Qed+` regression in - `+formal/Counterexample.v+` are intentional and must remain together. +* *Legacy archaeology*: the original `+preservation+` statement is false. + Since the owner-ratified D0b (2026-11-05) it is retired to + `+preservation_stmt : Prop+` (not closed) and refuted outright by + `+preservation_false+` in `+formal/Counterexample.v+` (6 `+Qed+`). + +[IMPORTANT] +==== +*D0/D0b retirement (owner-ratified 2026-11-05).* `+formal/+` now has +*0* `+Admitted.+` and *0* `+Axiom+`. The three refuted statements +(`+Semantics.preservation+`, `+step_pop_disjoint_from_type_l1+`, +`+preservation_l1+`) are `+Prop+` definitions, each refuted by a `+Qed+` +counterexample. While they were `+Admitted+`, the build could derive +`+False+`; CI's no-False gate (`+coq-build.yml+`) now blocks any new +`+Admitted+`/`+Axiom+`/`+Parameter+`. The L2 corollaries +`+preservation_l2_via_l1+` and `+preservation_l2_lift_case+` take +`+preservation_l1_stmt+` as an explicit hypothesis. Dated sections below +that count outer `+Admitted.+` markers are historical. +==== * *Redesigned judgments*: L1/L2 change typing interfaces; conceptual vocabulary or results from another repo do not discharge Ephapax's language-soundness obligations. @@ -51,13 +66,12 @@ The current preservation boundary is: [cols="18%,26%,56%",options="header"] |=== |Layer |Status |Evidence / boundary -|Legacy |*False as stated; pinned archaeology* |`+Counterexample.v+` has -5 `+Qed+` lemmas. Keep the one durable `+Admitted.+` in -`+Semantics.v+`; do not relabel it ordinary debt or replace it with a fake -proof. -|L1 |*Current universal statement false as stated* |`+Counterexample_StepPop.v+` -refutes `+step_pop_disjoint_from_type_l1+`; `+Counterexample_PreservationL1.v+` -refutes the modality-polymorphic `+preservation_l1+` via its Linear +|Legacy |*False as stated; retired, refuted* |`+Counterexample.v+` has +6 `+Qed+` lemmas, including `+preservation_false : ~ preservation_stmt+`. +The statement is a `+Prop+`, not a theorem; never state it as proved. +|L1 |*Current universal statement false as stated; retired* |`+Counterexample_StepPop.v+` +refutes `+step_pop_disjoint_from_type_l1_stmt+`; `+Counterexample_PreservationL1.v+` +refutes the modality-polymorphic `+preservation_l1_stmt+` via its Linear instance (the pre-state witness types in both modes). It does not by itself refute a separate Affine-only theorem. The existing `+bad_input_untypable_l1+` only rejects the original legacy witness; it does @@ -136,8 +150,8 @@ link:formal/PRESERVATION-DESIGN.adoc[`+formal/PRESERVATION-DESIGN.adoc+`]. |`+formal/Echo.v+` |12 Qed, 0 admits |Linear-mode forward progress lemmas |`+formal/Semantics_L1.v+` |37 Qed; -*2* outer `+Admitted.+` markers (`+step_pop_disjoint_from_type_l1+` / -`+preservation_l1+`) cover *2* internal `+admit.+` cases at current +0 `+Admitted.+` since D0 (2026-11-05). Historical note: *2* outer `+Admitted.+` markers (`+step_pop_disjoint_from_type_l1+` / +`+preservation_l1+`) covered *2* internal `+admit.+` cases at then-current lines 3315/3336 (rebuilt `+coqc 8.18.0+` ground truth 2026-06-27; the earlier 5-internal / lines-576/646/1994/2014/3132 figure is pre-dissolution, superseded by the Β§4 marker = 3 total). Phase 3b Stage @@ -201,9 +215,9 @@ graceful abandonment |Stage 3b and Ξ²-case helpers landed with explicit premises; they are not unconditional preservation theorems. The unrestricted region-shrink helper and former region-liveness lemma were refuted and removed; the restricted -`+region_shrink_msperm+`/value/neutral results are Qed. Two outer L1 -`+Admitted+` markers remain, and both unrestricted statements are now -refuted by pinned counterexamples (see Β§1 boundary and Β§4 seam audit). +`+region_shrink_msperm+`/value/neutral results are Qed. The two former +outer L1 `+Admitted+` markers are retired to `+Prop+` statements (D0, +2026-11-05); both are refuted by pinned counterexamples. |=== ==== Counterexample regression @@ -429,8 +443,10 @@ These are not preferences. They are explicit, durable, owner-issued ==== A. Do not close the legacy preservation theorem -* ❌ `+Theorem preservation+` in `+formal/Semantics.v+` is *provably -false*. No proof closes it. The `+Admitted.+` is correct. Leave it. +* ❌ The legacy preservation statement in `+formal/Semantics.v+` is *provably +false*. No proof closes it. Since D0b (2026-11-05) it is +`+preservation_stmt : Prop+`, refuted by `+Counterexample.preservation_false+`; +do not restate it as a `+Theorem+` or `+Lemma+`. * ❌ Do not add lemmas to `+formal/Semantics.v+` aimed at that closure. Examples that have wasted real session time: ** Lemma B variants (`+step_preserves_type+`, @@ -511,20 +527,19 @@ the owner*: === Β§4. Counts + file-by-file map -Coq `+Admitted.+` marker count: *3* (current source inventory): one -legacy marker plus two in `+Semantics_L1.v+`. This is a marker count, not -a count of sound obligations still awaiting routine proof. +Coq `+Admitted.+` marker count: *0* (D0/D0b retirement, 2026-11-05). +The build is axiom-free; CI's no-False gate enforces it. CI count marker only (source markers, not routine proof debt): -Coq admitted proofs remaining: 3 +Coq admitted proofs remaining: 0 -* `+formal/Semantics.v+` `+preservation+`: false as stated; durable - legacy archaeology, pinned by `+Counterexample.v+`. -* `+formal/Semantics_L1.v+` `+step_pop_disjoint_from_type_l1+` and - `+preservation_l1+`: both unrestricted statements are refuted by - `+Counterexample_StepPop.v+` and - `+Counterexample_PreservationL1.v+`; neither is ordinary proof debt. +* `+formal/Semantics.v+` `+preservation_stmt+`: false as stated; retired + to a `+Prop+` and refuted by `+Counterexample.preservation_false+`. +* `+formal/Semantics_L1.v+` `+step_pop_disjoint_from_type_l1_stmt+` and + `+preservation_l1_stmt+`: both unrestricted statements are retired to + `+Prop+` and refuted by `+Counterexample_StepPop.v+` and + `+Counterexample_PreservationL1.v+`; neither is proof debt. * The false unrestricted region-shrink helper was replaced by `+region_shrink_msperm+` and proved value/neutral corollaries. The false unconditional region-liveness helper was removed and replaced at diff --git a/V1-TO-V2.adoc b/V1-TO-V2.adoc index a4295d86..a0bfa5c9 100644 --- a/V1-TO-V2.adoc +++ b/V1-TO-V2.adoc @@ -80,8 +80,8 @@ grammar.v1.status = SUPERSEDED (pest surface; works for core, does not scal grammar.v2.status = ACTIVE (spec/ephapax-v2-grammar.ebnf; phases landing; tests green) grammar.v2.tractable = YES -proof.v1.status = FALSIFIED (formal/Semantics.v preservation; Counterexample.v, 5 Qed) -proof.v1.action = LEAVE AS Admitted; do NOT attempt to close (no closure exists) +proof.v1.status = FALSIFIED (formal/Semantics.v preservation_stmt; Counterexample.v, 6 Qed incl. preservation_false) +proof.v1.action = RETIRED to Prop (D0b, 2026-11-05); do NOT attempt to close (no closure exists) proof.v2.status = REDESIGN IN PROGRESS (four-layer architecture is not yet a sound replacement) proof.v2.tractable = OPEN DESIGN β€” current unrestricted L1 preservation is refuted; no unconditional L2 preservation theorem exists; L3 results are scoped @@ -222,9 +222,11 @@ dependency. A machine-checked counterexample to your own soundness theorem is a *good day* in language design. It converts "we think this is sound" into "we know exactly where and why it is not," which is the only solid ground -to redesign from. The `Admitted.` on the legacy theorem is **correct and -deliberate**: it marks a theorem we have *proven cannot be closed*, not a -gap we are too lazy to fill. +to redesign from. The legacy theorem marks a statement we have *proven +cannot be closed*, not a gap we are too lazy to fill. Since D0b +(2026-11-05) it is a `Prop` (`preservation_stmt`), refuted outright by +`preservation_false`, rather than an `Admitted` theorem: an `Admitted` +false statement let the build derive `False`. ==== === v2: four-layer architecture, soundness work still open @@ -241,9 +243,9 @@ any layer-level result as a language theorem. | Layer | Concern | v2 status | **L1** | Region capabilities | Judgment and helper infrastructure exist; - the unrestricted preservation statement is refuted. Two outer `Admitted.` - markers remain on false unrestricted statements, not routine proof debt; - redesign and restricted replacement are open. + the unrestricted preservation statement is refuted. The two false + unrestricted statements are retired to `Prop` (D0, 2026-11-05), so + `formal/` has no `Admitted`; redesign and restricted replacement are open. | **L2** | Structural modality (Linear vs Affine) | Core landed, `linear_to_affine` `Qed`, **zero axioms**. | **L3** | Echo / residue β€” what was *lost* at an irreversible step | Calculus @@ -269,8 +271,9 @@ already enforced by the current judgment. This is the part that is *no less transparent than before*. Two things are closed, and closed for good reasons: -. **Legacy preservation (`formal/Semantics.v`) is false.** Keep the - `Admitted.`. Do not attempt to close it, strengthen lemmas toward it, +. **Legacy preservation (`formal/Semantics.v`) is false.** It is retired + to `preservation_stmt : Prop` (D0b, 2026-11-05). Do not restate it as a + theorem or attempt to close it, strengthen lemmas toward it, add side conditions for it, or follow any pre-2026-05-26 "closure plan." `formal/Counterexample.v` depends on its falsity. This wall is load-bearing. diff --git a/formal/Counterexample.v b/formal/Counterexample.v index fbe62bed..e14dcb25 100644 --- a/formal/Counterexample.v +++ b/formal/Counterexample.v @@ -6,7 +6,8 @@ ********************************************************************* *** πŸ“Œ PINNED REGRESSION WITNESS *** *** *** - *** 5 Qed lemmas. Authoritative source of the 2026-05-26 *** + *** 6 Qed lemmas, incl. preservation_false (D0b, 2026-11-05). *** + *** Authoritative source of the 2026-05-26 *** *** soundness gap. *** *** *** *** This file SHOULD NOT BE WEAKENED. Any future proof work must *** @@ -156,8 +157,10 @@ Section Counterexample. Historical closure attempts recorded 11 remaining admits on the [touches_region] RIGHT branches; that count is archival, not a current proof obligation. This witness refutes the universal theorem. - Its [Admitted] remains durable; a different sound theorem requires - an approved redesign, not closure of this statement. See + The legacy statement is retired to [Semantics.preservation_stmt] + and refuted outright by [preservation_false] below (D0b, + 2026-11-05); a different sound theorem requires an approved + redesign, not closure of this statement. See [PRESERVATION-HANDOFF.adoc] for archaeology. *) End Counterexample. @@ -254,3 +257,15 @@ Section L1Fix. Qed. End L1Fix. + + +(** D0b retirement (owner-ratified 2026-11-05): the legacy preservation + statement is refuted outright. *) +Theorem preservation_false : ~ preservation_stmt. +Proof. + unfold preservation_stmt. intro H. + destruct (H _ _ _ _ _ _ (bad_step nil) _ _ _ bad_typable) as [G_out Hg]. + exact (bad_post_untypable _ _ Hg). +Qed. + +Print Assumptions preservation_false. diff --git a/formal/Counterexample_PreservationL1.v b/formal/Counterexample_PreservationL1.v index e82052c5..67e5d7df 100644 --- a/formal/Counterexample_PreservationL1.v +++ b/formal/Counterexample_PreservationL1.v @@ -152,12 +152,9 @@ Qed. (** ** THE REFUTATION *) Theorem preservation_l1_FALSE : - ~ (forall m mu R e mu' R' e', - step (mu, R, e) (mu', R', e') -> - forall G T R_final G', - has_type_l1 m R G e T R_final G' -> - has_type_l1 m R' G e' T R_final G'). + ~ Semantics_L1.preservation_l1_stmt. Proof. + unfold Semantics_L1.preservation_l1_stmt. intro H. apply wit2_post_untypable. eapply (H Linear [] [rv] wit2). diff --git a/formal/Counterexample_StepPop.v b/formal/Counterexample_StepPop.v index b550187e..e6012a7e 100644 --- a/formal/Counterexample_StepPop.v +++ b/formal/Counterexample_StepPop.v @@ -143,11 +143,9 @@ Proof. simpl. auto. Qed. (** ** THE REFUTATION *) Theorem step_pop_disjoint_from_type_l1_FALSE : - ~ (forall mu R e mu' R' e' m G T R_final G', - step (mu, R, e) (mu', R', e') -> - has_type_l1 m R G e T R_final G' -> - forall r, In r (Typing.free_regions T) -> In r R -> In r R'). + ~ Semantics_L1.step_pop_disjoint_from_type_l1_stmt. Proof. + unfold Semantics_L1.step_pop_disjoint_from_type_l1_stmt. intro H. assert (Hin : In rv ([] : region_env)). { eapply (H [] [rv] wit (mem_free_region [] rv) [] (EPair (EI32 5) wit_e2) diff --git a/formal/Semantics.v b/formal/Semantics.v index 9a1b2635..48abd4a2 100644 --- a/formal/Semantics.v +++ b/formal/Semantics.v @@ -7,9 +7,9 @@ ********************************************************************* *** πŸ›‘ ARCHAEOLOGY -- DO NOT EXTEND *** *** *** - *** This is the LEGACY operational semantics. The `preservation` *** - *** theorem here is PROVABLY FALSE -- verified by *** - *** `formal/Counterexample.v` (5 Qed lemmas). *** + *** This is the LEGACY operational semantics. Its preservation *** + *** claim is PROVABLY FALSE (`formal/Counterexample.v`). It is *** + *** retired to `preservation_stmt : Prop` (D0b, 2026-11-05). *** *** *** *** Do NOT add lemmas to close it. Do NOT add `Admitted` or *** *** `Axiom` declarations. Do NOT extend with Lemma B variants, *** @@ -8553,777 +8553,17 @@ Proof. end). Qed. -Theorem preservation : +Definition preservation_stmt : Prop := forall mu R e mu' R' e', (mu, R, e) -->> (mu', R', e') -> forall G T G', R; G |- e : T -| G' -> exists G_out, R'; G |- e' : T -| G_out. -Proof. - intros mu R e mu' R' e' Hstep. - (* Remember the configs so `induction Hstep` generates explicit equations on - the outer expression slots. Without these remembers, `induction Hstep` - leaves the outer `e`/`e'` abstract β€” for an axiom step rule like - S_StringNew the constructor pre-conditions land in the context but the - equation `e = EStringNew r s` does not, so cross-cases (e.g. S_StringNew - step + T_Unit typing) have no discriminating equation in scope and the - `try solve [exfalso; discriminate | exfalso; congruence]` chain below - cannot close them. - Empirically (Coq 8.18.0, 2026-05-20): without these remembers, - `inversion Htype; subst` produces the FULL 35 Γ— 26 = 910 cross-case - combinatorial and the `try solve [...]` chain closes ZERO of them. - With these remembers + `inversion Hcfg; subst; inversion Hcfg'; subst;`, - `inversion Htype` only generates the diagonal arm per step rule (since - the expression slot is concrete after substitution), and the chain - closes the trivially-dischargeable ones, leaving ~29 real proof - obligations. Standard preservation pattern; cf. Software Foundations - `Stlc.preservation`. The prior `remember e_typed as e_orig` was a - misdiagnosis of the same problem β€” it remembered the WRONG expression - (the typing's `e`, which was already abstract) instead of the config's - expression slot (which is what `induction Hstep` substitutes for). *) - remember (mu, R, e) as cfg eqn:Hcfg. - remember (mu', R', e') as cfg' eqn:Hcfg'. - (* Generalise mu/R/e/mu'/R'/e' and their cfg-equations so the IHs - emitted by `induction Hstep` get clean universal quantification - over each inner step's config β€” not the outer cfg pair (which - would make the IH non-applicable, since (mu_inner, R_inner, - e_inner) β‰  (mu, R, EOuter ...) in general). Without this revert, - the 28 congruence cases left after the cross-case discriminate - pass have unusable IHs. *) - revert mu R e mu' R' e' Hcfg Hcfg'. - induction Hstep; intros mu0 R0 e0 mu0' R0' e0' Hcfg Hcfg'; - intros G0 T0 G0' Htype; - inversion Hcfg; subst; - inversion Hcfg'; subst; - inversion Htype; subst; - try solve [eexists; econstructor; eassumption]; - try solve [eexists; eassumption]; - try solve [eapply subst_preserves_typing; eassumption]; - try solve [exfalso; eapply values_dont_step; eassumption]; - try solve [exfalso; congruence]; - try solve [exfalso; discriminate]; - (* EVar cannot step β€” no step constructor has EVar i as the redex expression. - This closes T_Borrow cross-cases in S_Borrow_Step (after inversion gives EVar - as the inner expression, the inner step hypothesis is immediately impossible). *) - try solve [exfalso; - match goal with [ H : (_, _, EVar _) -->> _ |- _ ] => inversion H end]. - (* Congruence: IH + reconstruct *) - all: try solve [match goal with [ IH : forall _ _ _, _ -> exists _, _ |- _ ] => - match goal with [ H : has_type _ _ _ _ _ |- _ ] => - destruct (IH _ _ _ H) as [? ?]; - eexists; econstructor; try eassumption end end]. - all: try solve [eexists; econstructor; try eassumption]. - all: try solve [eexists; eassumption]. - all: try solve [exfalso; congruence]. - all: try solve [exfalso; discriminate]. - all: try solve [exfalso; eapply values_dont_step; eassumption]. - all: try solve [exfalso; - match goal with [ H : (_, _, EVar _) -->> _ |- _ ] => inversion H end]. - (* S_Region_Step + T_Region and S_Region_Exit + T_Region are contradictory: - step premiss has In r R while T_Region requires ~ In r R. `tauto` closes. - S_Region_Enter + T_Region_Active is also contradictory (step has ~ In r R, - typing has In r R). *) - all: try solve [exfalso; tauto]. - (* S_Region_Enter + T_Region: The step changes region env R to r :: R while the - expression stays ERegion r e. T_Region gives (r :: R); G |- e : T -| G'. - T_Region_Active applies with In r (r :: R) (left; reflexivity) and that inner - typing to produce (r :: R); G |- ERegion r e : T -| G'. *) - all: try solve [eexists; eapply T_Region_Active; [left; reflexivity | assumption | eassumption]]. - (* T_Borrow cross-cases generated by inversion Htype in S_Borrow_Val / S_Borrow_Step: - (a) S_Borrow_Val / T_Borrow: after subst v = EVar i, have is_value (EVar i) β€” impossible. - Close by inversion on is_value (EVar _) which has no matching constructor. - (b) S_Borrow_Step / T_Borrow: after subst e = EVar i, have step c1 c2 where c1 contains - EVar i β€” no step constructor fires on EVar, so inversion gives 0 cases. - Use `solve [inversion H]` which only succeeds when inversion closes the goal (0 cases). *) - all: try solve [match goal with [H: is_value (EVar _) |- _] => inversion H end]. - all: try solve [match goal with [H: step _ _ |- _] => inversion H end]. - (* REMAINING CASE (2026-04-19, post Option-B scaffolding): - - Only ONE case remains open: S_Region_Step + T_Region_Active. - - Given: inner step (mu, R, e) -->> (mu', R', e') with `In r R` - (from T_Region_Active) and `~ In r (free_regions T)`. - IH: exists G_out, R'; G |- e' : T -| G_out. - Goal: exists G_out', R'; G |- ERegion r e' : T -| G_out'. - - Case-split on `In r R'`: - - If In r R': reapply T_Region_Active. - - If ~ In r R': need T_Region with `(r :: R'); G |- e' : T -| G_out`, - but IH only gives `R'; G |- e' : T -| G_out`. Requires region-env - WEAKENING (add r to R') β€” a lemma in the opposite direction from - the shrink lemma and not obviously valid without extra - invariants on e'. - - S_Region_Exit + T_Region_Active IS NOW CLOSED (see "try solve" - above), using: - - expr_free_of_region r v (new premise on S_Region_Exit, landed - this session as Option B) - - region_shrink_preserves_typing (proven above, 1 remaining admit - for T_Region_Active shadowing case inside the lemma itself). - - Full closure of this preservation admit now blocks on the - region-env weakening lemma for non-values, which is a narrower, - better-understood piece of work than the original language-design - question. *) - (* S_Region_Exit + T_Region_Active closes via region_shrink_preserves_typing - using the new step-premise expr_free_of_region. *) - all: try solve [eexists; eapply region_shrink_preserves_typing; - [eassumption | assumption]]. - (* S_Region_Step + T_Region_Active: the last open goal. - IH gives exists G_out, R'; G |- e' : T -| G_out. - Case-split on whether r is still in R': - - If In r R': apply T_Region_Active directly. - - If ~ In r R': apply T_Region + region_add_typing to weaken - the IH body typing from R' to r :: R'. - After all `all: try solve [...]` steps above, exactly one goal - remains: S_Region_Step + T_Region_Active. - Use `eassumption` to feed the correct has_type hyp into the IH. - Then case-split; construct T_Region or T_Region_Active. *) - (* S_Region_Step + T_Region_Active: the final goal. - IHHstep is the IH from induction on the inner step of S_Region_Step. - It has type: forall G T G', R; G |- e : T -| G' -> exists G_out, R'; G |- e' : T -| G_out. - Apply it to the body typing from T_Region_Active inversion. *) - all: try ( - match goal with - | [ |- exists _ : ctx, has_type _ _ (ERegion _ _) _ _ ] => - match goal with - | [ Hbody : has_type _ _ _ _ _, Hfr : ~ In _ (free_regions _) |- _ ] => - destruct (IHHstep _ _ _ Hbody) as [G_out Hout]; - destruct (in_dec string_dec r R') as [Hin' | Hnotin']; - [ eexists; eapply T_Region_Active; [exact Hin' | exact Hfr | exact Hout] - | eexists; eapply T_Region; - [ exact Hnotin' | exact Hfr | apply region_add_typing; exact Hout ] ] - end - end). - (* === Goal-closing chain for the post-remember-cfg 29 residuals === - Added 2026-05-20 evening per formal/PRESERVATION-HANDOFF.md per-case - checklist. Each `all: try solve [...]` targets one residual class. *) - - (* Axiom cases (S_StringNew / S_StringConcat): result is `ELoc l r` - and the *goal's* type is `TString r0` (named from inversion of - the OUTER typing). To close, invert the sibling-location's typing - premise (`H : R; G |- ELoc _ r : TString r0 -| G'`) which is - itself a T_Loc β€” that derives `r0 = r` and `region_active R r`. - Then T_Loc applies. *) - all: try solve [ - match goal with - | [ H : has_type _ _ (ELoc _ _) (TString _) _ - |- exists _ : ctx, has_type _ _ (ELoc _ _) (TString _) _ ] => - inversion H; subst; eexists; apply T_Loc; assumption - end - ]. - - (* S_StringNew: result is `ELoc l r` at `TString r` (no sibling - typing in scope, but the step's `In r R` is). *) - all: try solve [eexists; apply T_Loc; unfold region_active in *; assumption]. - - (* S_StringLen: result is `EI32 (String.length s)` at `TBase TI32`. *) - all: try solve [eexists; apply T_I32]. - - (* S_Drop: result is `EUnit` at `TBase TUnit`. *) - all: try solve [eexists; apply T_Unit]. - - (* S_Copy: result is `EPair v v` at `TProd T T`. Constructor + - assumption on the value's typing premise (carried over by the - inversion of T_Copy). *) - all: try solve [eexists; apply T_Pair; eassumption]. - - (* Ξ²-reduction cases (S_Let_Val, S_LetLin_Val, S_App_Fun, S_Fst, - S_Snd, S_Case_Inl/Inr): close via the existing - subst_preserves_typing lemma. *) - all: try solve [eexists; eapply subst_preserves_typing; eassumption]. - - (* S_If_True / S_If_False: pick the appropriate branch's typing premise. *) - all: try solve [eexists; eassumption]. - - (* Congruence cases (S_*_Step variants): the IH (after the revert) - is universally quantified over each inner step's config β€” we - specialise with the constructor's inner-step args + reflexivity - on the cfg equations. Pattern after revert mu/R/e/mu'/R'/e'/Hcfg/Hcfg': - - IH : forall mu R e mu' R' e', - (?mu_in, ?R_in, ?e_in) = (mu, R, e) -> - (?mu_out, ?R_out, ?e_out) = (mu', R', e') -> - forall G T G', R; G |- e : T -| G' -> - exists G_out, R'; G |- e' : T -| G_out - - We use edestruct + eq_refl x 2 on the universal cfg equations, - supply the inner-expr typing premise from inversion, then close - by econstructor + eauto. The eauto fallback handles cases where - the sibling premises need light glue (e.g. region invariance - follows from the step's region-non-change). *) - all: try solve [ - match goal with - | [ IH : forall _ _ _ _ _ _, _ = _ -> _ = _ -> forall _ _ _, _ -> _, - Hi : has_type _ _ ?e_inner _ _ |- _ ] => - let G_out_inner := fresh "G_out_inner" in - let Hout_inner := fresh "Hout_inner" in - edestruct (IH _ _ _ _ _ _ eq_refl eq_refl _ _ _ Hi) as [G_out_inner Hout_inner]; - eexists; econstructor; eauto - end - ]. - - (* === Region-invariance-driven closure for congruence cases === - Lemma [step_R_eq_or_touches_region] (proved above) gives a clean - case-split on the inner step: either the region environment is - preserved (so the sibling typing premises and the constructor - can be re-applied to the post-step expression with the same R) - or the stepped subexpression contains a region operation (which - needs region weakening β€” left open). - - For each S_*_Step constructor, we discharge the LEFT branch by: - 1. pose the disjunction, destruct, - 2. in the [HeqR] branch, [subst] R0' so the post-step region - equals the pre-step region, - 3. specialise IHHstep with eq_refl/eq_refl on cfg-equations - and the inner-expr's typing premise (named explicitly to - avoid pattern-match ambiguity with sibling premises), - 4. close the goal by [eexists; econstructor; ...] with the - stepped-expr typing + any sibling premises. - The RIGHT branch (touches_region) is left to fall through to - [Admitted.] β€” these still need a region-env weakening lemma - for non-values, separately tracked in PRESERVATION-HANDOFF.md. *) - - (* Ξ²-reduction cases that need explicit hypothesis-named applications - of subst_preserves_typing because the implicit eassumption - doesn't pick the right has_type for the body (multiple - R; _ |- _ : _ -| _ premises live in scope and the lemma's first - arg requires the body's typing, not v's). *) - - (* S_Let_Val and S_LetLin_Val: same shape (modulo linearity - premise β€” both succeed without it). H_v: typing of v1 in (G0 β†’ G'). - value_context_unchanged on H_v β‡’ G' = G0, so the body typing - becomes (T1, false) :: G0 |- e2 : ... and subst_preserves_typing - applies. *) - all: try solve [ - match goal with - | [ Hv : is_value ?v, - Hev : ?R; ?G |- ?v : ?T1 -| ?Gmid, - Hbody : ?R; ctx_extend ?Gmid ?T1 |- ?e2 : ?T0 -| (?T1, true) :: _ - |- exists _ : ctx, ?R; ?G |- subst 0 ?v ?e2 : ?T0 -| _ ] => - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - eapply subst_preserves_typing; eassumption - end - ]. - - (* S_App_Fun: H4: R0'; G0 |- ELam T ebody : TFun T1 T0 -| G', - H7: R0'; G' |- v2 : T1 -| G0', - H : is_value v2. *) - all: try solve [ - match goal with - | [ Hv : is_value ?v2, - Hlam : ?R; ?G |- ELam ?T ?ebody : TFun ?T1 ?T0 -| ?Gmid, - Harg : ?R; ?Gmid |- ?v2 : ?T1 -| ?Ge - |- exists _ : ctx, ?R; ?G |- subst 0 ?v2 ?ebody : ?T0 -| _ ] => - inversion Hlam; subst; - assert (Hgeq: Ge = Gmid) by (eapply value_context_unchanged; eassumption); - subst Ge; - eapply subst_preserves_typing; eassumption - end - ]. - - (* S_If_True / S_If_False: branch typing exists but in (G' β†’ G0') - context; the bool's typing gives G0 β†’ G', and EBool b is a value - so G' = G0. Then the branch's typing matches the goal. *) - all: try solve [ - match goal with - | [ Hbool : has_type ?R ?G (EBool ?b) (TBase TBool) ?Gmid, - Hbr : has_type ?R ?Gmid ?ebr ?T ?G' - |- exists _ : ctx, has_type ?R ?G ?ebr ?T _ ] => - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; [exact Hbool | constructor]); - subst Gmid; eexists; exact Hbr - end - ]. - - (* S_Case_Inl: H5: EInl T v : TSum T1 T2, H8: e1 body under extended ctx. - inversion H5; subst gives R0'; G0 |- v : T1 -| G' (named some Hi). - value_context_unchanged β‡’ G' = G0; then subst + Gmid = G0; - then subst_preserves_typing closes. *) - all: try solve [ - match goal with - | [ Hv : is_value ?vv, - Hsum : has_type ?R ?G (EInl ?Tann ?vv) (TSum ?T1 ?T2) ?Gmid - |- exists _ : ctx, has_type ?R ?G (subst 0 ?vv ?ebody) ?T0 _ ] => - inversion Hsum; subst; - match goal with - | [ Hvt2 : has_type ?R ?G ?vv ?T1 ?Ge, - Hbr2 : has_type ?R (ctx_extend ?Ge ?T1) ?ebody ?T0 ((?T1, true) :: _) - |- _ ] => - assert (Hgex: Ge = G) by (eapply value_context_unchanged; eassumption); - subst Ge; - eapply subst_preserves_typing; [ exact Hbr2 | exact Hvt2 | exact Hv ] - end - end - ]. - - (* S_Case_Inr: symmetric β€” pick the RIGHT branch body via ?T2. *) - all: try solve [ - match goal with - | [ Hv : is_value ?vv, - Hsum : has_type ?R ?G (EInr ?Tann ?vv) (TSum ?T1 ?T2) ?Gmid - |- exists _ : ctx, has_type ?R ?G (subst 0 ?vv ?ebody) ?T0 _ ] => - inversion Hsum; subst; - match goal with - | [ Hvt2 : has_type ?R ?G ?vv ?T2 ?Ge, - Hbr2 : has_type ?R (ctx_extend ?Ge ?T2) ?ebody ?T0 ((?T2, true) :: _) - |- _ ] => - assert (Hgex: Ge = G) by (eapply value_context_unchanged; eassumption); - subst Ge; - eapply subst_preserves_typing; [ exact Hbr2 | exact Hvt2 | exact Hv ] - end - end - ]. - - (* S_Fst: Hp: EPair v1 v2 : TProd T0 T2, goal: v1 typing. - Inverting Hp gives v1 : T0 -| ?Gmid and v2 : T2 -| G'. - eassumption matches the v1 typing (post-context is irrelevant - since the goal's post-context is existential). *) - all: try solve [ - match goal with - | [ Hp : has_type ?R ?G (EPair ?v1 ?v2) (TProd ?T0 ?T2) ?G' - |- exists _ : ctx, has_type ?R ?G ?v1 ?T0 _ ] => - inversion Hp; subst; eexists; eassumption - end - ]. - - (* S_Snd: Hp: EPair v1 v2 : TProd T1 T0 (G0 β†’ G0'), goal: v2 typing - under (G0 β†’ G_out). After inverting Hp, the first child v1 typing - has post-context Gmid; value_context_unchanged on it β‡’ Gmid = G0 - (since v1 is a value); then the second child's typing - (Gmid β†’ G0') becomes (G0 β†’ G0'), which matches the goal. *) - all: try solve [ - match goal with - | [ Hv : is_value ?v1, - Hp : has_type ?R ?G (EPair ?v1 ?v2) (TProd ?T1 ?T0) ?G' - |- exists _ : ctx, has_type ?R ?G ?v2 ?T0 _ ] => - inversion Hp; subst; - match goal with - | [ Hv1t : has_type ?R ?G ?v1 ?T1 ?Gmid |- _ ] => - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; eexists; eassumption - end - end - ]. - - (* S_Copy: H4: R0'; G0 |- v : T -| G0' (single typing of v), - H1: is_linear_ty T = false, - H : is_value v. - Goal: exists G_out, R0'; G0 |- EPair v v : TProd T T -| G_out. - value_context_unchanged on H4 β‡’ G0' = G0; then T_Pair applies - with both child typings being H4 (now (G0 β†’ G0)). *) - all: try solve [ - match goal with - | [ Hv : is_value ?v, - Hvt : has_type ?R ?G ?v ?T ?G', - Hnl : is_linear_ty ?T = false - |- exists _ : ctx, has_type ?R ?G (EPair ?v ?v) (TProd ?T ?T) _ ] => - assert (Hgeq: G' = G) by (eapply value_context_unchanged; eassumption); - subst G'; - eexists; eapply T_Pair; eassumption - end - ]. - - (* === Congruence cases (S_*_Step) === - KNOWN BLOCKER (2026-05-21): These tactic blocks pose the - region-invariance disjunction and specialise the IH, but the - final [eapply T_Foo; [exact Hout | exact Hsibling]] fails - because the IH's output context (a Skolem variable from the - existential) is not in general equal to the sibling premise's - pre-context. Closing these would require either: - (a) a "step preserves output context" lemma that says: if - [R; G |- e : T -| G'] and [(mu, R, e) -->> (mu', R', e')], - then the IH's existential output equals G'; or - (b) using [typing_ctx_transfer] / [type_determinacy] + - [typing_types_agree] to re-type the sibling under the - IH's output context. - Both are non-trivial extra lemmas. The blocks below remain in - place as documentation of the intended pattern; the [fail] in - the RIGHT branch + the output-context mismatch in the LEFT - branch leaves them unclosed, so they fall through to Admitted. - RIGHT branch (touches_region) is independently open β€” needs - region weakening for non-values. *) - - (* S_StringConcat_Step1: inner step on e1. 3-way via [step_R_change_shape]: - - LEFT (R = R'): close via [step_output_context_eq] oracle. - - MIDDLE (R' = rw :: R): same oracle + [region_add_typing] lifts sibling. - - RIGHT (R' = remove_first rw R, pop): idtac β€” needs Brief C. - Uses [rw] (not [r]) to avoid collision with the existing TString - region [r] already bound by outer inversion. *) - all: try ( - match goal with - | [ H1 : has_type ?R ?G ?e1 (TString ?r0) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 (TString ?r0) ?Gout1 - |- exists _ : ctx, has_type ?R' ?G (EStringConcat ?e1' ?e2) (TString ?r0) _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[rw [Hadd Hnotin]] | [rw [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - eexists; eapply T_StringConcat; [exact Hout | exact H2] - | subst R'; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - pose proof (region_add_typing _ _ _ _ _ rw H2) as H2lift; - eexists; eapply T_StringConcat; [exact Hout | exact H2lift] - | idtac ] - end). - - (* S_StringConcat_Step2: inner on e2; v1 value β‡’ Gmid = G via - value_context_unchanged. 3-way (uses [rw] to avoid name clash with - the outer TString region [r]): - - LEFT (R = R'): IH on H2 gives Hout at input G; direct. - - MIDDLE (R' = rw :: R): lift the value-sibling H1 via region_add_typing. - - RIGHT (pop): idtac β€” needs Brief C. *) - all: try ( - match goal with - | [ Hv : is_value ?v1, - H1 : has_type ?R ?G ?v1 (TString ?r0) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 (TString ?r0) ?G' - |- exists _ : ctx, has_type ?R' ?G (EStringConcat ?v1 ?e2') (TString ?r0) _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[rw [Hadd Hnotin]] | [rw [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2) as [Gout Hout]; - eexists; eapply T_StringConcat; [exact H1 | exact Hout] - | subst R'; - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2) as [Gout Hout]; - pose proof (region_add_typing _ _ _ _ _ rw H1) as H1lift; - eexists; eapply T_StringConcat; [exact H1lift | exact Hout] - | idtac ] - end). - - (* S_StringLen_Step is VACUOUS: T_StringLen wraps e at type - [TBorrow (TString r)], and T_Borrow forces the inner of [EBorrow] - to be [EVar i] (no step rule fires on EVar) while T_Borrow_Val - forces it to be a value (values don't step). So the inner Hstep - premise of S_StringLen_Step has no model β€” close vacuously like - S_Borrow_Step elsewhere in this proof. *) - all: try solve [ - match goal with - | [ Hin : (_, _, _) -->> (_, _, _), - Hte : has_type _ _ (EBorrow _) _ _ |- _ ] => - inversion Hte; subst; - [ inversion Hin - | exfalso; - match goal with - | [ Hv : is_value ?v |- _ ] => - eapply values_dont_step; [exact Hv | exact Hin] - end - ] - end - ]. - - (* S_Let_Step β€” 3-way via [step_R_change_shape]: - - LEFT (R = R'): close via [step_output_context_eq] oracle. - - MIDDLE (R' = r :: R, push): same oracle + lift sibling H2 via - [region_add_typing] (preserves both ctx_extend and output). - - RIGHT (R' = remove_first r R, pop): idtac β€” needs Brief C. *) - all: try ( - match goal with - | [ H1 : has_type ?R ?G ?e1 ?T1 ?Gmid, - H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e2 ?T0 ((?T1, true) :: ?G') - |- exists _ : ctx, has_type ?R' ?G (ELet ?e1' ?e2) ?T0 _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - eexists; eapply T_Let; [exact Hout | exact H2] - | subst R'; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - pose proof (region_add_typing _ _ _ _ _ r H2) as H2lift; - eexists; eapply T_Let; [exact Hout | exact H2lift] - | idtac ] - end). - - (* S_LetLin_Step β€” 3-way (parallel to S_Let_Step). LEFT + MIDDLE close; - RIGHT (pop) idtac β€” needs Brief C. *) - all: try ( - match goal with - | [ Hlin : is_linear_ty ?T1 = true, - H1 : has_type ?R ?G ?e1 ?T1 ?Gmid, - H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e2 ?T0 ((?T1, true) :: ?G') - |- exists _ : ctx, has_type ?R' ?G (ELetLin ?e1' ?e2) ?T0 _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - eexists; eapply T_LetLin; [exact Hlin | exact Hout | exact H2] - | subst R'; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - pose proof (region_add_typing _ _ _ _ _ r H2) as H2lift; - eexists; eapply T_LetLin; [exact Hlin | exact Hout | exact H2lift] - | idtac ] - end). - - (* S_App_Step1 β€” 3-way. LEFT + MIDDLE close via oracle + region_add_typing. - RIGHT (pop) idtac β€” needs Brief C. *) - all: try ( - match goal with - | [ H1 : has_type ?R ?G ?e1 (TFun ?T1 ?T0) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T1 ?G' - |- exists _ : ctx, has_type ?R' ?G (EApp ?e1' ?e2) ?T0 _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - eexists; eapply T_App; [exact Hout | exact H2] - | subst R'; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - pose proof (region_add_typing _ _ _ _ _ r H2) as H2lift; - eexists; eapply T_App; [exact Hout | exact H2lift] - | idtac ] - end). - - (* S_App_Step2: v1 value β‡’ Gmid = G. 3-way: - - LEFT (R = R'): IH on H2 gives Hout at input G; direct. - - MIDDLE (R' = r :: R): lift the value-sibling H1 via region_add_typing. - - RIGHT (pop): idtac β€” needs Brief C. *) - all: try ( - match goal with - | [ Hv : is_value ?v1, - H1 : has_type ?R ?G ?v1 (TFun ?T1 ?T0) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T1 ?G' - |- exists _ : ctx, has_type ?R' ?G (EApp ?v1 ?e2') ?T0 _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2) as [Gout Hout]; - eexists; eapply T_App; [exact H1 | exact Hout] - | subst R'; - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2) as [Gout Hout]; - pose proof (region_add_typing _ _ _ _ _ r H1) as H1lift; - eexists; eapply T_App; [exact H1lift | exact Hout] - | idtac ] - end). - - (* S_If_Step β€” 3-way. LEFT + MIDDLE close (both branches lifted via - region_add_typing in MIDDLE). RIGHT (pop) idtac β€” needs Brief C. *) - all: try ( - match goal with - | [ H1 : has_type ?R ?G ?e1 (TBase TBool) ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T0 ?G', - H3 : has_type ?R ?Gmid ?e3 ?T0 ?G' - |- exists _ : ctx, has_type ?R' ?G (EIf ?e1' ?e2 ?e3) ?T0 _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - eexists; eapply T_If; [exact Hout | exact H2 | exact H3] - | subst R'; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - pose proof (region_add_typing _ _ _ _ _ r H2) as H2lift; - pose proof (region_add_typing _ _ _ _ _ r H3) as H3lift; - eexists; eapply T_If; [exact Hout | exact H2lift | exact H3lift] - | idtac ] - end). - - (* S_Pair_Step1 β€” 3-way. LEFT + MIDDLE close. RIGHT (pop) idtac. *) - all: try ( - match goal with - | [ H1 : has_type ?R ?G ?e1 ?T1 ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T2 ?G' - |- exists _ : ctx, has_type ?R' ?G (EPair ?e1' ?e2) (TProd ?T1 ?T2) _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - eexists; eapply T_Pair; [exact Hout | exact H2] - | subst R'; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - pose proof (region_add_typing _ _ _ _ _ r H2) as H2lift; - eexists; eapply T_Pair; [exact Hout | exact H2lift] - | idtac ] - end). - - (* S_Pair_Step2: v1 value β‡’ Gmid = G. 3-way: - - LEFT (R = R'): IH on H2 gives Hout at G; direct. - - MIDDLE (R' = r :: R): lift the value-sibling H1. - - RIGHT (pop): idtac. *) - all: try ( - match goal with - | [ Hv : is_value ?v1, - H1 : has_type ?R ?G ?v1 ?T1 ?Gmid, - H2 : has_type ?R ?Gmid ?e2 ?T2 ?G' - |- exists _ : ctx, has_type ?R' ?G (EPair ?v1 ?e2') (TProd ?T1 ?T2) _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2) as [Gout Hout]; - eexists; eapply T_Pair; [exact H1 | exact Hout] - | subst R'; - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2) as [Gout Hout]; - pose proof (region_add_typing _ _ _ _ _ r H1) as H1lift; - eexists; eapply T_Pair; [exact H1lift | exact Hout] - | idtac ] - end). - - (* S_Case_Step β€” 3-way. LEFT + MIDDLE close (both branch typings lifted - via region_add_typing in MIDDLE). RIGHT (pop) idtac β€” needs Brief C. *) - all: try ( - match goal with - | [ H1 : has_type ?R ?G ?e (TSum ?T1 ?T2) ?Gmid, - H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e1 ?T0 ((?T1, true) :: ?G'), - H3 : has_type ?R (ctx_extend ?Gmid ?T2) ?e2 ?T0 ((?T2, true) :: ?G') - |- exists _ : ctx, has_type ?R' ?G (ECase ?e' ?e1 ?e2) ?T0 _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; - [ rewrite <- HeqR in *; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - eexists; eapply T_Case; [exact Hout | exact H2 | exact H3] - | subst R'; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - assert (Heq_out : Gmid = Gout) by - (eapply step_output_context_eq; - [ exact Hstep | exact H1 | exact Hout ]); - subst Gmid; - pose proof (region_add_typing _ _ _ _ _ r H2) as H2lift; - pose proof (region_add_typing _ _ _ _ _ r H3) as H3lift; - eexists; eapply T_Case; [exact Hout | exact H2lift | exact H3lift] - | idtac ] - end). - -(* Show Existentials. *) (* uncomment to dump the remaining open goals. - Post-MIDDLE narrowing (2026-05-26 late eve): - 10 POP sub-cases (`Hrem : R0' = remove_first r R0` - and `HinR : In r R0` in scope) + 1 S_Region_Step - = 11 admits. The 10 POP cases share the same - shape: stepped child reaches R0' = remove_first r R0 - with surviving sibling still typed at R0; needs - non-value region-env weakening (Brief C structural - lemma; the [typing_free_of_absent_region] lemma - at Semantics.v:3346 is the kernel). *) -Admitted. -(* PROOF STATUS [preservation] β€” ADMITTED, down to 12 open goals - (from 910 cross-case, via PR #102's remember-cfg + PR #106's - universal-IH revert + 2026-05-21 per-case per-step closures for - Ξ²-reduction, projection, branch-selection, and linear-copy cases). - A region-invariance lemma [step_R_eq_or_touches_region] now lives - just before this theorem and dispatches the non-region-step half - of congruence cases (left branch only β€” see CLOSURE STATUS below). - - CLOSURE STATUS (2026-05-21): - Closed (via per-case [all: try solve [match goal ...]]): - S_Let_Val, S_LetLin_Val (Ξ² with subst_preserves_typing) - S_App_Fun (Ξ² with inversion of ELam typing) - S_If_True, S_If_False (branch-select via VBool unchanged-ctx) - S_Fst, S_Snd (projection via pair-inversion) - S_Case_Inl, S_Case_Inr (Ξ² with inversion of EInl/EInr typing) - S_Copy (linear via value_context_unchanged + T_Pair) - Still open (12 goals β€” see Existential dump above): - S_StringConcat_Step1/2, S_StringLen_Step, - S_Let_Step, S_LetLin_Step, S_App_Step1/2, - S_If_Step, S_Pair_Step1/2, S_Case_Step - BLOCKER: the IH's output context (a Skolem variable) is - not in general equal to the sibling premise's pre-context, - so the [exact Hout; exact Hsibling] closure fails at - T_Foo's middle-context unification. Either a "step - preserves output context" lemma OR a context-transfer - re-typing of the sibling is needed. - S_Region_Step - BLOCKER: needs region-env weakening for non-values - (touches_region branch of step_R_eq_or_touches_region). - Tactic blocks for all twelve open S_*_Step cases remain in place - as documentation of the intended pattern β€” they pose the - disjunction lemma and dispatch the left branch, but [fail] in - the right (touches_region) branch and silently fail in the left - branch when the output-context mismatch blocks the final eapply. *) -(* PROOF STATUS PRIOR HISTORY: - - PRIOR STATE (before the `remember (mu, R, e) as cfg` introduction at L3232): - `induction Hstep; intros G0 T0 G0' Htype; inversion Htype; subst; ...` - left **910 goals open** = 35 (step rules) Γ— 26 (typing rules) β€” the FULL - cross-case combinatorial, because `induction Hstep` did not substitute - the outer expression slot `e` to the constructor's form, so `inversion - Htype` produced all 26 arms instead of just the diagonal. Cross-cases - (e.g. S_StringNew step + T_Unit type) had no discriminating equation in - scope, so `try solve [exfalso; discriminate | exfalso; congruence]` closed - none of them. - - CURRENT STATE: ~29 real diagonal goals remain β€” one per step rule, modulo - the 6 that the existing `try solve [...]` chain closes once the expression - slots are concrete. Remediation per case: - - Axiom cases needing explicit reconstruction: S_StringNew, S_StringConcat, - S_StringLen (typing the result location/literal via T_Loc/T_I32). - - Ξ²-reduction cases needing `subst_preserves_typing`: S_Let_Val, - S_LetLin_Val, S_App_Fun, S_If_True/False, S_Fst, S_Snd, - S_Case_Inl/Inr. - - Congruence cases needing IH + reconstruction: S_*_Step variants. - - Region: S_Region_Enter, S_Region_Step, S_Region_Exit (the prior named - "remaining case" + 2 the in-file comment did not name). - - Linear: S_Drop, S_Copy. - - Supporting lemmas already Qed: subst_preserves_typing, - region_env_perm_typing, region_add_typing, region_shrink_preserves_typing, - values_dont_step. Per the handoff doc, the S_Region_Step + T_Region_Active - case still blocks on a region-env *weakening* lemma for non-values, which - does not yet exist. The other 28 are per-case tactic glue. - - 97% reduction (910 β†’ 29) via the standard preservation pattern (remember - the configs so `induction Hstep`'s substitution is recovered through - `inversion Hcfg; subst`). See formal/PRESERVATION-HANDOFF.md for the - per-case checklist (the handoff doc's 910-goal diagnostic captures the - PRIOR state; the same Show. recipe applied here yields the 29-goal - diagnostic for ongoing work). *) +(** [preservation_stmt] β€” RETIRED, not closed (owner-ratified D0b, + 2026-11-05). The legacy [Theorem preservation] was [Admitted] and is + refuted by [Counterexample.preservation_false]. An [Admitted] proof of + a false statement let any file importing both derive [False], so the + statement is kept only as a [Prop] for the counterexample to refute. + The former 700-line partial proof script and its closure-status notes + (910 -> 12 open goals) are archaeology; see git history before this + change and [formal/PRESERVATION-HANDOFF.adoc]. *) diff --git a/formal/Semantics_L1.v b/formal/Semantics_L1.v index 12497945..90468aab 100644 --- a/formal/Semantics_L1.v +++ b/formal/Semantics_L1.v @@ -1,7 +1,7 @@ (* SPDX-License-Identifier: MPL-2.0 *) (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) -(* hypatia: allow code_safety/admitted -- tracked proof boundary; not an honest-completion claim. The two remaining outer Admitted markers (step_pop_disjoint_from_type_l1, preservation_l1) are each refuted as currently stated: see Counterexample_StepPop.v and Counterexample_PreservationL1.v. Do not try to close either unrestricted claim by ad-hoc patching or relabel them routine debt. Replacement work must reformulate the judgment/step interface with an explicit invariant and state a new theorem. The former region_liveness_at_split_l1_gen false statement was removed (2026-06-26) via val_region_no_exit / region_liveness_no_exit_l1_gen. See PROOF-NEEDS.adoc for current classification. Build truth is the `Print Assumptions` CI gate, not this comment. *) +(* hypatia: allow code_safety/admitted -- tracked proof boundary; not an honest-completion claim. The two former outer Admitted markers (step_pop_disjoint_from_type_l1, preservation_l1) are refuted as stated (Counterexample_StepPop.v, Counterexample_PreservationL1.v) and were retired to Prop statements (owner-ratified D0, 2026-11-05); this file now has no Admitted. Do not try to prove either unrestricted statement. Replacement work must reformulate the judgment/step interface with an explicit invariant and state a new theorem. The former region_liveness_at_split_l1_gen false statement was removed (2026-06-26) via val_region_no_exit / region_liveness_no_exit_l1_gen. See PROOF-NEEDS.adoc for current classification. Build truth is the `Print Assumptions` CI gate, not this comment. *) (* hypatia: allow coq_admit_tactic -- see preceding directive; same tracked admits. *) (** @@ -11,8 +11,8 @@ *** *** *** This is the post-counterexample L1 redesign. Extend HERE. *** *** *** - *** 2 outer `Admitted` lemmas remain; both unrestricted claims *** - *** are refuted by pinned regressions (see below). L1/L2 Qed *** + *** 0 `Admitted` (D0, 2026-11-05). Both unrestricted claims are *** + *** refuted by pinned regressions (see below). L1/L2 Qed *** *** infrastructure is not a universal preservation theorem. *** *** - typing_preserves_bindings_l1 (now m-polymorphic) *** *** - unrestricted_flag_unchanged_l1 *** @@ -27,10 +27,10 @@ *** - typing_preserves_length_l1, output_shape_at_l1, *** *** loc_retype_at_R_l1 all generalised to m-polymorphic *** *** *** - *** Refuted statements still marked Admitted: *** - *** - step_pop_disjoint_from_type_l1 β€” Counterexample_StepPop.v *** - *** - preservation_l1 β€” Counterexample_PreservationL1.v *** - *** Their Admitted markers are transparency, not a proof plan. *** + *** Refuted statements, retired to Prop (not closed): *** + *** - step_pop_disjoint_from_type_l1_stmt β€” Counterexample_StepPop.v *** + *** - preservation_l1_stmt β€” Counterexample_PreservationL1.v *** + *** They are kept only so the refutations can name them. *** *** Replacement theorems require an owner-approved redesign. *** *** *** *** DO NOT close them by: *** @@ -82,9 +82,9 @@ the Qed no-exit formulation and explicit premises described by [val_region_no_exit]. These helper results do not establish preservation for every step. - - [preservation_l1] β€” still marked Admitted, but its unrestricted - statement is refuted by [Counterexample_PreservationL1.v]. Do not - treat the marker as unfinished routine proof debt. A replacement + - [preservation_l1_stmt] β€” retired from [Admitted] to a [Prop] + statement (D0, 2026-11-05); its unrestricted form is refuted by + [Counterexample_PreservationL1.v]. It is not proof debt. A replacement requires an explicitly different judgment/step boundary or a restricted theorem with proved premises; see [PROOF-NEEDS.adoc]. @@ -3277,63 +3277,25 @@ Qed. lemma above is now refuted by [Counterexample_StepPop.v]; its outer [Admitted] is not routine proof debt. The choreography documents a redesign direction, not a proof route for the current statement. *) -Lemma step_pop_disjoint_from_type_l1 : +Definition step_pop_disjoint_from_type_l1_stmt : Prop := forall mu R e mu' R' e' m G T R_final G', (mu, R, e) -->> (mu', R', e') -> has_type_l1 m R G e T R_final G' -> forall r, In r (Typing.free_regions T) -> In r R -> In r R'. -Proof. - (* 2026 Β§6-experiment reduction. The original 255-line induction left - ELEVEN internal admits across the eliminator/erasing congruences - (Let / LetLin / App2 / If / Pair / Inl / Inr / Case / Region). They - all collapse through [step_R_change_shape] (Semantics.v, Qed): a single - step leaves [R] unchanged, prepends a fresh region, or removes exactly - one. So a region free in the result type survives UNLESS the step - exits that very region; the eleven admits become ONE. *) - intros mu R e mu' R' e' m G T R_final G' Hstep Ht r0 Hfree HinR. - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [Heq | [[r [Hadd Hnotin]] | [r [Hrem Hr_in]]]]. - - (* R = R' : no region change. *) subst R'. exact HinR. - - (* R' = r :: R : S_Region_Enter descent. *) subst R'. simpl. right. exact HinR. - - (* R' = remove_first r R : S_Region_Exit descent. *) subst R'. - destruct (string_dec r r0) as [Heqr | Hne]. - + (* r = r0 : the step exits the very region we need live. The single - residual obligation is [cnt r0 R >= 2] (i.e. [In r0 (remove_first - r0 R)]). Its DIRECT-exit sub-case is vacuous: a head redex - [ERegion r0 v] is typed by [T_Region_Active_L1], whose - [~In r0 (free_regions T)] premise contradicts [Hfree]. The residue - is the CONGRUENCE-exit case, where the exiting [ERegion r0] sits - under an eliminator and [r0] is supplied by a sibling's type β€” a - DISTINCT occurrence. Establishing that distinctness is region-count - coherence at a region exit: the temporal/segment structure the - snapshot env + result type cannot express, relocating to connecting - the dynamic exit to the static typing output, i.e. preservation - itself. This unrestricted statement is refuted by - [Counterexample_StepPop.v]; the choreographic route is a - redesign direction, not a proof plan for this lemma. *) - subst r. admit. - + (* r <> r0 : remove_first r keeps every r0. *) - apply remove_first_preserves_other; [exact Hne | exact HinR]. -Admitted. - -(** [Print Assumptions step_pop_disjoint_from_type_l1.] is emitted at - file end (alongside the other [Print Assumptions] audit calls) to - certify which axioms / admits this lemma depends on. *) - -Theorem preservation_l1 : + +(** [step_pop_disjoint_from_type_l1_stmt] and [preservation_l1_stmt] β€” + RETIRED, not closed (owner-ratified D0, 2026-11-05). Both were + [Admitted] and are refuted by [Counterexample_StepPop] and + [Counterexample_PreservationL1]; keeping them [Admitted] let the build + derive [False]. They remain as [Prop] statements so the refutations + and the conditional L2 corollaries can name them. *) + +Definition preservation_l1_stmt : Prop := forall m mu R e mu' R' e', step (mu, R, e) (mu', R', e') -> forall G T R_final G', has_type_l1 m R G e T R_final G' -> has_type_l1 m R' G e' T R_final G'. -Proof. - (* Deliberately remains Admitted: the unrestricted theorem statement - is refuted by Counterexample_PreservationL1.v. Do not fill this - proof body without first replacing the false statement with an - owner-approved, explicitly restricted soundness theorem. *) - 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) @@ -3511,7 +3473,7 @@ Print Assumptions tfuneff_lambda_retype_l1_m. Print Assumptions subst_typing_gen_l1_m. Print Assumptions subst_typing_gen_l1_m_ground_nonlinear. Print Assumptions subst_typing_gen_l1_m_tfuneff. -Print Assumptions preservation_l1. + Print Assumptions preservation_l3_region_active_echo. Print Assumptions preservation_l3_drop_echo. Print Assumptions preservation_l3. @@ -3530,7 +3492,7 @@ Print Assumptions preservation_l3. admitted theorem as an axiom. Current replacement status is in [PROOF-NEEDS.adoc]. *) -Print Assumptions step_pop_disjoint_from_type_l1. + (** ============================================================ Canonical forms for the L1 judgment (proof-debt P43) diff --git a/formal/TypingL2.v b/formal/TypingL2.v index 4046d824..3f928645 100644 --- a/formal/TypingL2.v +++ b/formal/TypingL2.v @@ -332,15 +332,16 @@ Proof. reflexivity. Qed. [preservation_l2] proof body. *) Theorem preservation_l2_via_l1 : + Semantics_L1.preservation_l1_stmt -> forall m mu R e mu' R' e', step (mu, R, e) (mu', R', e') -> forall G T R_final G', TypingL1.has_type_l1 m R G e T R_final G' -> has_type_l2 m R' G e' T R_final G'. Proof. - intros m mu R e mu' R' e' Hstep G T R_final G' Ht. + intros Hpres m mu R e mu' R' e' Hstep G T R_final G' Ht. apply L2_lift_l1. - eapply Semantics_L1.preservation_l1; eassumption. + eapply Hpres; eassumption. Qed. (** Corollary: the L2_lift_l1 case of [preservation_l2] over the @@ -348,12 +349,13 @@ Qed. [preservation_l2_via_l1] by destructuring the lift. *) Corollary preservation_l2_lift_case : + Semantics_L1.preservation_l1_stmt -> forall m mu R e mu' R' e', step (mu, R, e) (mu', R', e') -> forall G T R_final G' (H1 : TypingL1.has_type_l1 m R G e T R_final G'), has_type_l2 m R' G e' T R_final G'. Proof. - intros m mu R e mu' R' e' Hstep G T R_final G' H1. + intros Hpres m mu R e mu' R' e' Hstep G T R_final G' H1. eapply preservation_l2_via_l1; eassumption. Qed. From dd061c05908d90d27895dd97a8a236ffa7aab7e8 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 07:37:00 +0000 Subject: [PATCH 2/2] docs(test-needs): refresh stale test-count marker 488 -> 504 status-gate-tests has been red on main since 2026-10 because the documented count drifted (ground truth: cargo test --all-targets -- --list reports 504). Not caused by this PR, which changes no Rust; ported here so the PR's CI is green. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- TEST-NEEDS.adoc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index d2c2deca..a59ceaa6 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -21,9 +21,9 @@ compliance, 16 tests) performance, correctness, 13 tests) * Benchmarks: `+src/ephapax-parser/benches/parse_bench.rs+`, `+src/ephapax-vram-cache/benches/cache_bench.rs+` -* Total: *488 tests* (`+cargo test --workspace --all-targets+`); +* Total: *504 tests* (`+cargo test --workspace --all-targets+`); pass/fail enforced by `+rust-ci.yml+` -* Documented all-target tests: 488 +* Documented all-target tests: 504 === CRG Testing Taxonomy β€” Status