Proof debt/standards 134 coq preservation admit

PROOF-NEEDS.md

@@ -2,25 +2,26 @@
 
 ## Current state
 - `formal/Syntax.v` — Coq formalization of Ephapax syntax (clean)
-- `formal/Semantics.v` — Coq operational semantics; `preservation` Qed (closed 2026-04-27, zero `Admitted` in this file)
+- `formal/Semantics.v` — Coq operational semantics; `preservation` **Admitted** (earlier in-file comment claiming "Qed, closed 2026-04-27" was unsubstantiated — `coqc` 8.18.0 rejects the proof script with remaining open goals)
 - `formal/Typing.v` — Coq typing rules (clean)
 - `src/formal/Ephapax/Formal/RegionLinear.idr` — Idris2 region-based linearity proof (explicitly states "REAL proof — not believe_me, not assert_total")
 - 17 Idris2 files across formal verification layer
 - No `believe_me`, `sorry`, or `assert_total` in Idris2 source code
-- Coq admitted proofs remaining in `formal/Semantics.v`: 0
+- Coq admitted proofs remaining in `formal/Semantics.v`: 1 (`preservation`)
 
 ## What needs proving
+- **`preservation`**: Close the remaining open goals in the proof script at `formal/Semantics.v` L3215–L3326 so the `Qed` lands and the file builds without `Admitted.` The supporting lemmas (`region_env_perm_typing`, `region_add_typing`, `region_shrink_preserves_typing`) are Qed; the residual gap is in the top-level case analysis on `step`.
 - **Linear type consumption**: Prove resources with linear types are consumed exactly once across all execution paths (region boundaries, exception handlers)
 - **Effect system soundness**: Prove the effect type system correctly tracks side effects and that effect-free terms are truly pure
 - **Region safety**: Prove that region-based memory management prevents use-after-free and dangling references across region boundaries
 - **Compiler correctness**: Prove the Rust compiler preserves Ephapax semantics (at minimum, type-preserving compilation)
 
-> Note: an earlier version of this list included "close `preservation` Admitted" and "complete `progress` proof". `preservation` was closed at Qed on 2026-04-27 (see in-file comment at `formal/Semantics.v` L3328); `progress` was deleted in the substitution-semantics rewrite and is not currently formalised in this tree. The previous "progress 92%" claim is stale.
+> Note: an earlier version of this list claimed `preservation` was closed at Qed on 2026-04-27 (citing the in-file comment at `formal/Semantics.v` L3328) and that the prior "progress 92%" ROADMAP entry was the only stale item. Both claims were wrong: the cited in-file comment was itself unsubstantiated — `coqc` 8.18.0 rejects the `Qed.` with "Attempt to save an incomplete proof (there are remaining open goals)", which is why `rust-ci.yml`'s "Coq proofs" job has been failing on every push. The honest mark is `Admitted`. `progress` was deleted in the substitution-semantics rewrite and is genuinely not currently formalised in this tree.
 
 ## Recommended prover
 - **Coq** for the existing soundness chain in `formal/` (already invested in Coq formalization)
 - **Idris2** for region linearity and effect system properties (already in use, fits dependent type style)
 - **Agda** as backup for metatheory if Coq proof terms become unwieldy
 
 ## Priority
-- **MEDIUM** — Ephapax is a programming language whose core value proposition is linear types and memory safety. With `preservation` closed, the immediate soundness blocker is gone; remaining work is breadth-first (effect system, region safety, compiler correctness) rather than depth-first.
+- **MEDIUM-HIGH** — Ephapax is a programming language whose core value proposition is linear types and memory safety. `preservation` remains `Admitted` (the immediate soundness blocker is still in place, contrary to the previously-claimed-but-incorrect "closed 2026-04-27" status). The next highest-leverage item is closing the open goals in the `preservation` proof script so the `Qed` lands and the Coq CI gate goes green.

ROADMAP.adoc

@@ -20,9 +20,10 @@ checker and WASM code generation are in progress.
 **Dual formalisation status:**
 
 * **Coq** (`formal/`): `no_leaks` (Qed), `typing_ctx_transfer` (Qed),
-  `subst_preserves_typing` (Qed), `preservation` (Qed, closed
-  2026-04-27 — see in-file comment at `formal/Semantics.v` L3328).
-* Coq admitted proofs remaining in `formal/Semantics.v`: 0
+  `subst_preserves_typing` (Qed), `preservation` (Admitted — earlier in-file
+  comment claiming "Qed, closed 2026-04-27" was unsubstantiated; `coqc` rejects
+  the proof script with remaining open goals).
+* Coq admitted proofs remaining in `formal/Semantics.v`: 1 (`preservation`)
 * **Idris2** (`src/formal/`): `noEscapeTheorem`, `regionSafetyTheorem`, `noGCTheorem`,
   `orthogonalityLemma` -- all complete with zero unsafe patterns. Added 2026-05-19:
   `splitLinearCoverage` in `Ephapax/Formal/Qualifier.idr` (PR #85) — generalises
@@ -50,7 +51,9 @@ chain are sound.
 * [ ] WASM code generation: lambda/app compilation (closure conversion)
 * [x] Coq: close `ctx_transfer` proof
 * [x] Coq: close `subst_lemma` proof
-* [x] Coq: close `preservation` proof (Qed, 2026-04-27)
+* [ ] Coq: close `preservation` proof (currently `Admitted` —
+  earlier in-file claim of "Qed, 2026-04-27" was unsubstantiated, `coqc`
+  rejects the proof script with remaining open goals)
 * [-] Coq: `progress` proof — N/A. `progress` was deleted in the
   substitution-semantics rewrite and is not currently formalised
   in this tree. The previous "92%" claim was stale.

formal/PRESERVATION-HANDOFF.md

@@ -0,0 +1,173 @@
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+
+# Hand-off: closing `preservation` in `formal/Semantics.v`
+
+Diagnostic written 2026-05-20 alongside the `Qed.` → `Admitted.`
+honesty fix (ephapax#92). Whoever picks this up next: read this file
+first; it tells you exactly what's open and why the existing proof
+script does not close it.
+
+## How this hand-off was produced
+
+The proof script ends at `Semantics.v` L3326. Replace the `Admitted.`
+on L3327 with:
+
+```coq
+    end).
+Show.
+Show Existentials.
+Admitted.
+```
+
+Then:
+
+```sh
+cd formal
+coq_makefile -f _CoqProject -o Makefile.coq && make -f Makefile.coq
+```
+
+`coqc` prints the goal count + every open existential. Restore the
+`Admitted.` afterwards.
+
+## What's actually open
+
+**910 goals** — exactly **35 (step rules) × 26 (typing rules)**, i.e.
+the *full combinatorial after `induction Hstep; inversion Htype;
+subst;`*. The chain of `try solve [...]` tactics in
+`Semantics.v` L3228–L3326 closes **zero** of them.
+
+The in-file comment block at L3269–L3296 says
+
+> Only ONE case remains open: S_Region_Step + T_Region_Active.
+
+That was true (or thought to be true) at one earlier moment of the
+proof development; it is **not true now**. Either:
+
+- the proof script regressed silently after the comment was written
+  (no CI gate caught it because the Coq job has been failing for ≥3
+  runs — see ephapax#92), **or**
+- the comment was always optimistic about how many `try solve`
+  branches actually fired.
+
+Either way: **the proof closes nothing as it stands; the goal is to
+write tactics that close the full 35 × 26 case split**, not just the
+single S_Region_Step case the comment names.
+
+## Why the existing `try solve` chain fails
+
+The current shape is:
+
+```coq
+induction Hstep; intros G0 T0 G0' Htype;
+  try (remember ... as e_orig eqn:He_orig);
+  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];
+  try solve [exfalso; ...inversion (EVar steps)...];
+  ...
+```
+
+The `try solve` blocks are applied to *all* `inversion Htype`
+subgoals. They fall into two outcomes:
+
+1. **Diagonal cases** (step rule and typing rule are about the same
+   expression head — e.g. `S_App_Fun` + `T_App`): need real
+   reconstruction. The `try solve [eexists; econstructor;
+   eassumption]` aims at these but `eassumption` rarely matches —
+   typically the IH gives `R'; G |- body : T -| G_out` for some `G_out`
+   but the reconstructor needs a fresh witness for the *step-result*
+   expression. **Not closing.**
+
+2. **Cross-cases** (step rule fires on one expression, typing rule
+   inverts to a different head — ~33/35 of each step rule's
+   cross-cases): should close as `exfalso` via `discriminate` /
+   `congruence` on the typing-rule equation. But after `inversion
+   Htype; subst`, the substitution direction can eliminate the
+   step-side expression variable before the discriminating equation is
+   in scope. The `remember ... as e_orig eqn:He_orig` was intended to
+   pin the form, but it sits inside `try (...)` and only fires when
+   the pattern matches; for many cross-cases it does not fire, and
+   the chain falls through to `try solve [exfalso; congruence]` which
+   then has no equation to discriminate on. **Not closing.**
+
+Both cases need surgery on the script, not "one more tactic".
+
+## What it would take to close
+
+A realistic plan:
+
+1. **Move the `remember` out of `try (...)`** — it should always fire.
+   Use a less fragile pattern (e.g. `set (e_orig := e) in *` before
+   `inversion`).
+
+2. **Rewrite cross-case closure** to use an explicit `inversion
+   Htype` arm-by-arm rather than `inversion Htype; subst; try solve
+   [exfalso; ...]`. The arm-by-arm form lets you control the subst
+   direction. Coq 8.18's `inv` tactic from `Coq.Program.Tactics` or
+   `dependent destruction` can help.
+
+3. **Write per-step-rule diagonal proofs**. For each of the 35 step
+   rules, the diagonal typing rule case needs its own tactic block.
+   The supporting lemmas already exist:
+   - `subst_preserves_typing` (`Typing.v` Qed)
+   - `region_env_perm_typing` (`Semantics.v` Qed, this proof's L~3100)
+   - `region_add_typing` (`Semantics.v` Qed, this proof's L~3120)
+   - `region_shrink_preserves_typing` (`Semantics.v` Qed, this
+     proof's L~3150)
+   - `values_dont_step` (`Semantics.v` Qed earlier in the file)
+
+   The diagonal-case glue is the missing piece for each of the 35
+   step rules. The author's comment block at L3269–L3296 has the
+   right shape for `S_Region_Step + T_Region_Active`; analogous
+   blocks are needed for the other 34.
+
+4. **`S_Region_Step + T_Region_Active`** (the comment's named case):
+   the proposed `apply T_Region + region_add_typing` to weaken `R'`
+   to `r :: R'` is **not obviously valid without extra invariants on
+   `e'`** — see the comment's own warning at L3281–L3284. This case
+   may need a *region-env weakening lemma for non-values* which does
+   not yet exist. Writing that lemma is a separable piece of work,
+   probably 50–150 lines.
+
+5. **Estimated effort**: not "one more tactic." A full close is on
+   the order of **days–weeks of proof engineering**, depending on
+   whether the region-env weakening lemma turns out to need
+   additional language invariants. The 34 non-region-related diagonal
+   cases are probably 1–2 days; the region-related ones are the hard
+   part.
+
+## What is not a fix
+
+- Adding more `try solve [...]` lines to the existing chain. The
+  problem isn't a missing single tactic — it's that the *structure*
+  of the proof script is wrong for the cross-case discharge.
+- Replacing `induction Hstep` with `inversion Hstep` — that loses
+  the inductive hypotheses needed for the diagonal cases (e.g.
+  `S_Region_Step` recurses on inner step).
+- Mass-`Admitted.` per case — defeats the point and conflicts with
+  the estate's "build is the only oracle" policy. The honest mark is
+  one `Admitted.` on `preservation`, not 35.
+
+## What to do until it's closed
+
+The PR ephapax#92 (this branch) marks `preservation` as `Admitted.`
+so the file builds. ROADMAP + PROOF-NEEDS reflect the honest state.
+The Coq CI job will then go green. **This file remains as the precise
+diagnosis** so the next session does not have to re-derive what is
+open.
+
+Once `preservation` is honestly closed:
+
+1. Replace `Admitted.` with `Qed.`
+2. Flip ROADMAP's admitted-proofs counter `1 → 0`
+3. Flip PROOF-NEEDS' status row + delete the "what needs proving"
+   item for `preservation`
+4. Delete this file
+5. Update `RUST-SPARK-STANCE.adoc`'s E1 row from OWED to DISCHARGED
+   (and remove the "honest gap" entry about preservation)
+6. Delete the comment block at `Semantics.v` L3328–L3336 (its
+   contents will be obsolete)

formal/Semantics.v

@@ -3324,9 +3324,16 @@ Proof.
               [ exact Hnotin' | exact Hfr | apply region_add_typing; exact Hout ] ]
         end
     end).
-Qed.
-(* PROOF STATUS [preservation] — FULLY CLOSED (2026-04-27). Zero Admitted.
-   region_env_perm_typing: Qed (new lemma — transfers typing across region-env permutations).
-   region_add_typing: Qed (new lemma — adding a region to R preserves typing).
-   region_shrink_preserves_typing: Qed (T_Region_Active shadowing case closed via in_dec).
-   preservation: Qed (S_Region_Step+T_Region_Active closed by in_dec on r ∈ R'). *)
+Admitted.
+(* PROOF STATUS [preservation] — ADMITTED.
+   Earlier in-file note claimed "FULLY CLOSED (2026-04-27). Zero Admitted." with
+   `Qed.` here, but `coqc` (8.18.0) rejects that with "Attempt to save an
+   incomplete proof (there are remaining open goals)" — the proof script's nested
+   tactic combinator does not discharge every case of the inductive predicate.
+   Until the open goals are identified and closed, the honest mark is `Admitted.`
+   so the Coq formalisation builds and downstream docs (ROADMAP, PROOF-NEEDS)
+   accurately reflect the proof state. Supporting lemmas remain Qed:
+     region_env_perm_typing: Qed (transfers typing across region-env permutations).
+     region_add_typing: Qed (adding a region to R preserves typing).
+     region_shrink_preserves_typing: Qed (T_Region_Active shadowing case closed via in_dec).
+   preservation itself: Admitted, pending discharge of the residual open goals. *)