fix(coq): preservation 910 -> 29 open goals via remember-cfg pattern (Refs standards#134) by hyperpolymath · Pull Request #102 · hyperpolymath/ephapax

hyperpolymath · 2026-05-20T18:41:45Z

Summary

97% reduction in preservation's open-goal count (910 → 29) by applying the standard preservation pattern. The proof remains Admitted. — this PR is the cross-case discharge mechanism + the per-case work list, not the full close.

This supersedes ephapax#98 (which proposed the 910-goal handoff but did not include the fix); #98 can be closed in favour of this PR.

The root cause

induction Hstep did not substitute the outer expression slot e to the constructor's form (e := EStringNew r s etc.). So inversion Htype produced all 26 typing arms per step rule — the full 35 × 26 = 910 cross-case combinatorial. Cross-cases had no discriminating equation in scope, so try solve [exfalso; discriminate | exfalso; congruence] couldn't fire.

Verified empirically with Show. Show Existentials. after inversion Htype; subst; — the existing try solve [...] chain at L3228–L3340 closes ZERO of the 910.

The fix

intros mu R e mu' R' e' Hstep.
remember (mu, R, e) as cfg eqn:Hcfg.
remember (mu', R', e') as cfg' eqn:Hcfg'.
induction Hstep; intros G0 T0 G0' Htype;
  inversion Hcfg; subst;
  inversion Hcfg'; subst;
  inversion Htype; subst;
  (* existing try-solve chain (unchanged) *)

remember turns Hstep : step (mu, R, e) (mu', R', e') into Hstep : step cfg cfg' with two side equations. After induction Hstep, Hcfg becomes (for S_StringNew) (mu0, R0, EStringNew r s) = (mu, R, e), which inversion Hcfg; subst decomposes — substituting e := EStringNew r s everywhere including in Htype. Then inversion Htype; subst only generates the diagonal T_StringNew arm; the 25 cross-arms are eliminated by inversion's constructor-mismatch check.

The earlier remember e_typed as e_orig was a misdiagnosis — it remembered the typing's e (already abstract) instead of the config's expression slot (which is what induction Hstep substitutes for).

What's left (29 real diagonal goals)

Category	Step rules	Tactic
Axiom + reconstruct	`S_StringNew`, `S_StringConcat`, `S_StringLen`	`eexists; eapply T_Loc/T_StringConcat/...`
β-reduction	`S_Let_Val`, `S_LetLin_Val`, `S_App_Fun`, `S_If_`, `S_Fst`, `S_Snd`, `S_Case_`	`eexists; eapply subst_preserves_typing; eauto`
Congruence	`S_*_Step` variants (~15)	`destruct (IHHstep ...); eexists; econstructor; eauto`
Region	`S_Region_Enter`, `S_Region_Step`, `S_Region_Exit`	existing `T_Region_Active` / `region_shrink_preserves_typing`; `S_Region_Step + T_Region_Active` needs a NEW region-env weakening lemma
Linear	`S_Drop`, `S_Copy`	`eexists; constructor`

Supporting lemmas already Qed: subst_preserves_typing, region_env_perm_typing, region_add_typing, region_shrink_preserves_typing, values_dont_step.

The region-env weakening lemma for non-values is the only genuine theory question; the other 28 are 1–2 days of standard tactic glue.

Files

formal/Semantics.v — apply the remember-cfg pattern. Replace the old remember e_typed as e_orig (the misdiagnosis) with the new remember (mu, R, e) as cfg / remember (mu', R', e') as cfg' before induction, plus inversion Hcfg; subst; inversion Hcfg'; subst; after intros ... Htype and before the existing inversion Htype; subst;. Update the in-file proof-status comment to reflect 910 → 29.
PROOF-NEEDS.md — preservation "what needs proving" entry updated to reflect the 910 → 29 reduction + pointer to the handoff doc.
formal/PRESERVATION-HANDOFF.md — full per-case checklist for the 29 remaining goals; supersedes the 910-goal version on PR#98.

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.

Refs

Refs standards#134 (NOT Closes — joint-close on agreement). Supersedes ephapax#98.

Test plan

cd formal && coq_makefile -f _CoqProject -o Makefile.coq && make -f Makefile.coq → exit 0 locally
Show. Show Existentials. immediately before Admitted. shows 29 goals (down from 910 on the prior state)
CI green on rust-ci.yml "Coq proofs" job
Close docs(coq): add PRESERVATION-HANDOFF.md with diagnosis of open goals (Refs standards#134) #98 in favour of this PR

🤖 Generated with Claude Code

…(Refs standards#134) 97% reduction in preservation's open-goal count by applying the standard preservation pattern (`remember (mu, R, e) as cfg eqn:Hcfg` + symmetric for cfg', then `inversion Hcfg; subst; inversion Hcfg'; subst;` inside each case before `inversion Htype; subst`). The proof remains `Admitted.` — this PR is the cross-case discharge mechanism + the per-case work list, not the full close. `induction Hstep` did not substitute the outer expression slot `e` to the constructor's form (`e := EStringNew r s` for the `S_StringNew` case etc.). So `inversion Htype` produced ALL 26 typing arms per step rule — the FULL 35 × 26 = 910 cross-case combinatorial — instead of just the diagonal arm. Cross-cases (e.g. `S_StringNew` step + `T_Unit` type) had no discriminating equation in scope, so `try solve [exfalso; discriminate | exfalso; congruence]` couldn't fire. Verified empirically (Coq 8.18.0) via `Show. Show Existentials.` immediately after `inversion Htype; subst;` — the existing `try solve [...]` chain at L3228–L3340 closes ZERO of the 910. ```coq intros mu R e mu' R' e' Hstep. remember (mu, R, e) as cfg eqn:Hcfg. remember (mu', R', e') as cfg' eqn:Hcfg'. induction Hstep; intros G0 T0 G0' Htype; inversion Hcfg; subst; inversion Hcfg'; subst; inversion Htype; subst; (* … existing try-solve chain (unchanged) … *) ``` `remember` turns `Hstep : step (mu, R, e) (mu', R', e')` into `Hstep : step cfg cfg'` with two side equations `Hcfg : ... = (mu, R, e)`, `Hcfg' : ... = (mu', R', e')`. After `induction Hstep`, `Hcfg` becomes (for `S_StringNew`) `(mu0, R0, EStringNew r s) = (mu, R, e)`, which `inversion Hcfg; subst` decomposes — substituting `e := EStringNew r s` everywhere including in `Htype`. Then `inversion Htype; subst` only generates the diagonal `T_StringNew` arm; the 25 cross-arms are eliminated by inversion's constructor- mismatch check. The earlier `remember e_typed as e_orig eqn:He_orig` was a misdiagnosis of the same problem — it remembered the *typing's* `e` (already abstract) instead of the *config's* expression slot (which is what `induction Hstep` substitutes for). | Category | Step rules | Tactic | |----------|-----------|--------| | Axiom + reconstruct | S_StringNew, S_StringConcat, S_StringLen | `eexists; eapply T_Loc/T_StringConcat/...` | | β-reduction | S_Let_Val, S_LetLin_Val, S_App_Fun, S_If_*, S_Fst, S_Snd, S_Case_* | `eexists; eapply subst_preserves_typing; eauto` | | Congruence | S_*_Step variants (~15) | `destruct (IHHstep ...); eexists; econstructor; eauto` | | Region | S_Region_Enter, S_Region_Step, S_Region_Exit | most via existing `T_Region_Active`/`region_shrink_preserves_typing`; S_Region_Step + T_Region_Active needs a NEW region-env weakening lemma | | Linear | S_Drop, S_Copy | `eexists; constructor` | Supporting lemmas already Qed: `subst_preserves_typing`, `region_env_perm_typing`, `region_add_typing`, `region_shrink_preserves_typing`, `values_dont_step`. The region-env weakening lemma for non-values is the only genuine theory question; the other 28 are 1–2 days of standard tactic glue. - `formal/Semantics.v` — apply the remember-cfg pattern; replace the old `remember e_typed as e_orig` (the misdiagnosis) with the new `remember (mu, R, e) as cfg` / `remember (mu', R', e') as cfg'` before `induction`, plus `inversion Hcfg; subst; inversion Hcfg'; subst;` after `intros ... Htype` and before the existing `inversion Htype; subst;`. Update the in-file proof-status comment to reflect 910 → 29. - `PROOF-NEEDS.md` — "what needs proving" entry for `preservation` updated to reflect the 910 → 29 reduction + pointer to PRESERVATION-HANDOFF.md. - `formal/PRESERVATION-HANDOFF.md` — full per-case checklist for the 29 remaining goals; supersedes the 910-goal version filed on PR#98. Verified locally (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. Refs standards#134 (NOT Closes — joint-close on agreement). Supersedes the still-open ephapax#98 (which proposed the 910-goal handoff but did not include the fix); #98 can be closed in favour of this PR. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

…andards#134) (#103) ## Summary `.machine_readable/6a2/STATE.a2ml` claimed: ``` # No active blockers. Formal proofs FULLY CLOSED (67 Qed, 0 Admitted). ``` This was wrong on both axes: - `formal/Semantics.v::preservation` carries `Qed.` but `coqc` 8.18.0 rejects it with "Attempt to save an incomplete proof (there are remaining open goals)" — the proof never actually closed. PR#92 (MERGED) marked it `Admitted.` to restore CI green; PR#102 (OPEN) reduces the open-goal count from 910 to ~29 via the standard remember-cfg preservation pattern. So there's at least 1 `Admitted`, not 0. - `src/formal/Ephapax/Formal/RegionLinear.idr::regionSafetyExtract` / `noGCExtract` are **vacuous tautological wrappers** (body is the input unchanged: `= ne` / `= (ne, lc)`). ROADMAP citing them as "regionSafetyTheorem"/"noGCTheorem" complete is overstated. The honest E3 (region no-escape) and E4 (no-runtime-GC) obligations are stated in `src/abi/Ephapax/ABI/Invariants.idr` (the Rust/SPARK seam landed via PR#95-MERGED). ## What changed - `phase`, `next_action`, `last_action`, `updated` brought to 2026-05-20. - `@blockers` block now lists the residual proof debt accurately: - Semantics.v `preservation` Admitted (with handoff doc pointer) - vacuous RegionLinear wrappers - E1–E6 invariant register from the new ABI seam ## What's not in this PR No source/proof changes. This is purely the machine-readable artefact catching up to the actual code state. The human-readable docs (`ROADMAP.adoc`, `PROOF-NEEDS.md`, `RUST-SPARK-STANCE.adoc`) already reflect this after the 2026-05-20 batch of PR#92 + #95 + #102. ## Refs Refs standards#134 (**NOT Closes** — joint-close on agreement). ## Test plan - [x] No `.v` / `.idr` / Rust files touched — build state unaffected - [x] STATE.a2ml syntax preserved (comment lines + `@state` block + `@blockers` block + matching `@end`s) - [ ] CI green (no jobs apply to machine-readable artefacts) 🤖 Generated with [Claude Code](https://claude.com/claude-code)

…losers (#106) ## Summary Builds on PR #102 (910 → 29 reduction). Closes 7 more residuals via two structural fixes. | State | Open goals | |---|---:| | Pre-#102 | 910 | | Post-#102 | 29 | | **This PR** | **22** | ## 1. Universal-IH revert (closes 6 congruence-case goals) PR #102's `remember (mu, R, e) as cfg` discharged cross-cases but left congruence-case IHs **unusable** — they inherited the OUTER cfg equation: ```coq IHHstep : (mu_inner, R_inner, e_inner) = (mu, R, EOuter ...) -> ... ``` which is inconsistent in general (the inner expression is not the outer compound). Fix: `revert mu R e mu' R' e' Hcfg Hcfg'` before `induction Hstep`. Each case's IH now carries clean universal quantification: ```coq IHHstep : 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 ``` The 6 congruence cases closed by this are the ones whose sibling typing premises don't need region/context bridging. ## 2. Per-class closing tactics (closes 1 axiom-case goal) The new T_Loc inversion tactic handles `S_StringConcat`'s "type mismatch: result is `ELoc l' r` but goal asks `TString r0`" — inverting the sibling `ELoc l1 r` typing yields `r0 = r`, then T_Loc applies. Added 5 more atomic closers (T_StringNew, T_I32, T_Unit, T_Pair, subst_preserves_typing) — these are pre-emptive for cases the existing chain may not have hit, but empirically contributed 0 closures in this PR's diff. ## Remaining 22 goals All need additional metatheoretic lemmas: 1. **Sibling typing under post-step region**: for `S_X_Step1` congruence cases, the unstepped sibling expression is typed under R but the reconstructed compound needs it under R'. Needs a "step preserves R unless inner expression is region-touching" lemma + a region-invariance application. 2. **Context bridging**: same congruence cases also need the sibling's typing context (G') to bridge to the new context (G_inner from IH). Needs a "step preserves linearity tracking on siblings" lemma — substantial. 3. **EBorrow inversion for `S_StringLen_Step`**: typing premise wraps `EBorrow e`, not `e` directly; needs an extra inversion step before IH application. 4. **`S_Region_Step + T_Region_Active`**: the documented language-design blocker — needs a region-env *weakening* lemma for non-values (~50–150 LOC by itself). Per `formal/PRESERVATION-HANDOFF.md` these are 1–2 days of tactic work plus the region-weakening lemma. The `Admitted.` stays on `preservation`; supporting lemmas already Qed. ## Verification ``` $ coqc -Q . Ephapax Semantics.v (builds clean, Admitted at the 22-goal residue) $ # Empirical count via Show Existentials: $ # (insert before Admitted, rebuild, grep '^Existential ') 22 ``` ## Refs - `standards#124` (proof-debt audit epic) - `ephapax#102` (910 → 29 reduction) - `ephapax#104` (PROOF STATUS docs correction) ## Test plan - [x] `coqc -Q . Ephapax Semantics.v` builds clean - [x] `Show Existentials.` before Admitted reports 22 (down from 29 on main) - [x] No new `Qed.`-proven lemmas added; no proof-engineering shortcuts via `assert` / `admit` - [ ] CI green 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ofs (#116) ## Summary **Preservation existential count: 22 → 12** (10 goals closed). Builds on the region-invariance lemma `step_R_eq_or_touches_region` (PR #114) by adding per-step-constructor manual proof scripts inside `Theorem preservation`. ## Closed (10 step constructors) | Constructor | Closure technique | |---|---| | `S_Let_Val`, `S_LetLin_Val` | β-reduction via `subst_preserves_typing` + `value_context_unchanged` | | `S_App_Fun` | Inversion of `ELam` typing + value-context invariance on arg | | `S_If_True`, `S_If_False` | Branch typing under `VBool`'s unchanged-ctx via `value_context_unchanged` | | `S_Fst`, `S_Snd` | `EPair` inversion → child typing match | | `S_Case_Inl`, `S_Case_Inr` | `EInl` / `EInr` typing inversion + body substitution | | `S_Copy` | `T_Pair` on non-linear value with equal pre/post context | ## Open (12 remaining) **11 congruence cases** (`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`). Root cause: the **linearity-context drift** I diagnosed earlier — even after `step_R_eq_or_touches_region` puts us in the `R = R'` branch, the IH's output context (a Skolem variable from `edestruct`) doesn't unify with the sibling premise's pre-context. So `eapply T_Foo; [exact Hout | exact Hsibling]` fails on the middle-context unification. The tactic-block scaffolding for these 11 cases is in place (poses `step_R_eq_or_touches_region`, dispatches the LEFT branch, specialises `IHHstep`), with the final reconstruction silently failing — they fall through to `Admitted`. The right next step is **lemma B**: a "step preserves output linearity context" or context-transfer re-typing via the existing `typing_ctx_transfer`/`type_determinacy` machinery. **1 region case** (`S_Region_Step` + `T_Region_Active`): the documented language-design blocker — region-env weakening for non-values. Tracked in `formal/PRESERVATION-HANDOFF.md`. ## Verification ``` $ coqc -Q . Ephapax Semantics.v (builds clean; Admitted preservation now at 12 existentials) ``` ## Refs - `standards#124` (proof-debt audit epic) - `ephapax#102` (910 → 29 via remember-cfg) - `ephapax#106` (29 → 22 via universal-IH revert) - `ephapax#114` (region-invariance lemma — used here) ## Cumulative | State | Open goals | |---|---:| | Pre-#102 | 910 | | Post-#102 | 29 | | Post-#106 | 22 | | **Post this PR** | **12** | 98.7% reduction across the day from start of campaign. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…122) Closure sweep after PR #116 took preservation from 22 → 12 open goals and PR #121 landed Phase 1 scaffold. Updates the preservation-count claims across docs to reflect 12, and adds a CHANGELOG entry summarising the full 2026-05-20 → 2026-05-21 reduction campaign. ## Files updated | File | What changed | |---|---| | `README.adoc` | Coq formal-foundations paragraph; reduction chain now lists all 8 PRs through #121; clear pointer to ROADMAP closure plan | | `ROADMAP.adoc` | Formal-proof status table row (`12 open goals`); v0.1 blocker entry; v1.0 status; 97.6% → 98.7% reduction figure | | `EXPLAINME.adoc` | Coq theorem table; reduction-story bullets extended through #114, #116, #121 | | `CHANGELOG.md` | New "Proof state" + "Documentation" sections under `[Unreleased]` tracking the full PR chain (#92, #102, #104, #106, #114, #115, #116, #117, #121) + the Idris2 totality campaign (#89–#100) + doc/wiki refresh (#113 + wiki) | ## Companion wiki update `Home.md`, `Proof-status.md`, `What-can-go-wrong.md` updated in the wiki repo with the same 22 → 12 figures + extended reduction story. Pushed separately to wiki master. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

This was referenced May 20, 2026

docs(coq): add PRESERVATION-HANDOFF.md with diagnosis of open goals (Refs standards#134) #98

Closed

chore(machine-readable): correct STATE.a2ml proof-status lie (Refs standards#134) #103

Merged

hyperpolymath force-pushed the proof-debt/standards-134-preservation-remember-fix branch from 57408c8 to 3af22e8 Compare May 20, 2026 19:26

hyperpolymath merged commit 8282857 into main May 20, 2026
0 of 8 checks passed

hyperpolymath deleted the proof-debt/standards-134-preservation-remember-fix branch May 20, 2026 19:26

hyperpolymath mentioned this pull request May 20, 2026

fix(coq): preservation 29 → 22 open goals via universal-IH + atomic closers #106

Merged

4 tasks

This was referenced May 20, 2026

Proof debt/standards 134 coq preservation admit #108

Closed

Proof debt/standards 134 coq preservation admit #110

Closed

proof(coq): close 10 of 22 preservation goals via per-case manual proofs #116

Merged

hyperpolymath mentioned this pull request May 21, 2026

docs: refresh stale "22 open" → "12 open" + CHANGELOG closure entry #122

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix(coq): preservation 910 -> 29 open goals via remember-cfg pattern (Refs standards#134)#102

fix(coq): preservation 910 -> 29 open goals via remember-cfg pattern (Refs standards#134)#102
hyperpolymath merged 1 commit into
mainfrom
proof-debt/standards-134-preservation-remember-fix

hyperpolymath commented May 20, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented May 20, 2026

Summary

The root cause

The fix

What's left (29 real diagonal goals)

Files

Verification (local, Coq 8.18.0)

Refs

Test plan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant