fix(coq): mark preservation Admitted to restore rust-ci Coq job (Refs standards#134) (#92)

## Summary

- `formal/Semantics.v`'s `preservation` proof carried `Qed.` with an
in-file comment claiming "FULLY CLOSED (2026-04-27). Zero Admitted." —
but the proof does not close: `coqc` 8.18.0 rejects it with **"Attempt
to save an incomplete proof (there are remaining open goals)"**.
- Consequence: the **rust-ci.yml "Coq proofs" job has been failing on
every push to main** (3 most-recent runs all `conclusion: failure`, back
to 2026-05-19).
- PR #87 then propagated the comment's bogus "Qed, closed 2026-04-27"
claim from the source into `ROADMAP.adoc` + `PROOF-NEEDS.md`.

This PR restores honesty + build green:

- `formal/Semantics.v` — `Qed.` → `Admitted.` for `preservation`.
In-file status comment rewritten to record what `coqc` actually says.
Supporting lemmas (`region_env_perm_typing`, `region_add_typing`,
`region_shrink_preserves_typing`) remain Qed.
- `ROADMAP.adoc` — Coq status row + v0.1.0 checkbox flipped to reflect
`Admitted`; admitted-proofs counter `0 → 1`.
- `PROOF-NEEDS.md` — "current state" row + admitted counter corrected;
`preservation` added as the top "what needs proving" item with a precise
pointer to L3215–L3326 of the proof script; reconciliation note
rewritten to record the propagated-lie failure mode; priority raised
`MEDIUM → MEDIUM-HIGH`.

## Verification (local, Coq 8.18.0)

```
cd formal && coq_makefile -f _CoqProject -o Makefile.coq && make -f Makefile.coq
# → exit 0; Syntax.vo + Typing.vo + Semantics.vo all produced.
```

After this lands, the rust-ci.yml Coq job should go green; the proof
state will be honestly carrying one `Admitted` (the `preservation` proof
script's open goals), which is now the highest-leverage proof-debt item
on the repo per the updated PROOF-NEEDS priority.

## Refs

Refs standards#134 (NOT Closes — joint-close on agreement). #134 also
has ephapax#88 open for the 14 `idris2/src/*.idr` SPDX headers
(independent of this).

## Test plan

- [x] `cd formal && coq_makefile -f _CoqProject -o Makefile.coq && make
-f Makefile.coq` → exit 0 locally
- [ ] CI green on `rust-ci.yml` "Coq proofs" job (currently failing on
main)
- [ ] No surprise consumer of `preservation`'s Qed-status downstream

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: hyperpolymath

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/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. *)