From 75c57f57500390b0f82f97e988e782f10f550830 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 21 May 2026 07:18:36 +0100 Subject: [PATCH] docs: canonicalise the preservation closure plan in ROADMAP MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit After PR #116 brought preservation to 12 open goals (from 910 at start-of-session), set the 5-phase closure plan as the canonical path in ROADMAP.adoc. Any session picking up the proof work follows this plan. ## Plan summary (full detail in ROADMAP §"Preservation closure plan") Phase 1 — Lemma B (linearity-context invariance for siblings) — ~3-4 hours; closes the IH-vs-sibling context mismatch blocking the 11 congruence cases. Phase 2 — Apply Lemma B → close 11 congruence cases — ~2 hours, parallelizable to 4 agents. Brings 12 → 1. Phase 3 — Region-env weakening lemma for non-values — 1-2 days, genuine metatheoretic work. Defines a `safe_for_region_weakening` predicate + proves the weakening lemma. Phase 4 — Apply Phase 3 → close S_Region_Step + T_Region_Active — ~1 hour. Brings 1 → 0. Phase 5 — `Admitted.` → `Qed.` + docs sweep — ~1 hour, parallelizable to 2 agents (repo + wiki). Total: 3 sessions / ~10 hours wall-clock with fan-out, ~3 days sequential. Risk-adjusted forecast also captured. ## Other docs updated - PROOF-NEEDS.md: the "what needs proving" entry now points at the ROADMAP plan and lists the 5 phases in summary form. - formal/PRESERVATION-HANDOFF.md: header now points readers at the ROADMAP plan; the existing per-case diagnostic record retained as a complementary file. State-at-a-glance table extended through 2026-05-21 (12 open). No proof changes. Phase 1 commences in a fresh PR on top of this plan. Co-Authored-By: Claude Opus 4.7 (1M context) --- PROOF-NEEDS.md | 16 ++- ROADMAP.adoc | 219 ++++++++++++++++++++++++++++++++- formal/PRESERVATION-HANDOFF.md | 18 ++- 3 files changed, 241 insertions(+), 12 deletions(-) diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 891562ba..8d941f61 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -7,10 +7,22 @@ - `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`: 1 (`preservation`) +- Coq admitted proofs remaining in `formal/Semantics.v`: 1 (`preservation` — 12 open goals, plan below) ## What needs proving -- **`preservation`**: Close the remaining ~29 open goals in the proof script at `formal/Semantics.v` L3215–L3339 so the `Qed` lands and the file builds without `Admitted.` Down from 910 open goals (full 35×26 cross-case combinatorial) after introducing 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). The remaining 29 are real diagonal cases — see `formal/PRESERVATION-HANDOFF.md` for the per-case checklist. Supporting lemmas already Qed (`subst_preserves_typing`, `region_env_perm_typing`, `region_add_typing`, `region_shrink_preserves_typing`, `values_dont_step`). The S_Region_Step + T_Region_Active case still blocks on a region-env *weakening* lemma for non-values, which does not yet exist. An earlier ~40-goal diagnostic (PR #104) measured the PRE-`remember-cfg`-pattern state and is superseded. +- **`preservation`**: Close the remaining **12 open goals** in `formal/Semantics.v` so the `Qed` lands. Down from 910 at session start (98.7% reduction). Reduction story: 910 → 29 via remember-cfg (PR #102) → 22 via universal-IH revert (PR #106) → 12 via per-case manual closures (PR #116). The remaining 12 are 11 congruence cases (`S_*_Step` variants) + 1 region case (`S_Region_Step + T_Region_Active`). + + **Canonical closure path: `ROADMAP.adoc` § Preservation closure plan** — 5 phases: + + 1. **Lemma B (linearity-context invariance for siblings)** — closes the IH-vs-sibling context mismatch blocking the 11 congruence cases. ~3–4 hours. + 2. **Apply Lemma B → close 11 congruence cases** — per-case manual proof scripts (PR #116 pattern). ~2 hours, parallelizable. + 3. **Region-env weakening lemma for non-values** — defines `safe_for_region_weakening` predicate + proves the weakening lemma. 1–2 days, genuine metatheoretic work. + 4. **Apply Phase 3 lemma → close S_Region_Step** — ~1 hour. + 5. **`Admitted.` → `Qed.` + docs sweep** — mechanical, ~1 hour. + + Total: 3 sessions / ~10 hours wall-clock with fan-out. See ROADMAP for full effort estimates and risk-adjusted forecast. + + Supporting lemmas already Qed: `subst_preserves_typing`, `region_env_perm_typing`, `region_add_typing`, `region_shrink_preserves_typing`, `values_dont_step`, and **`step_R_eq_or_touches_region`** (PR #114, the region-invariance lemma used by the per-case closures and required by Phase 2). - **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 diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 87cd9ece..0a7d9253 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -150,11 +150,220 @@ All four headline theorems complete with **zero `believe_me` / * [ ] Type checker completion (`ephapax-typing`) * [ ] WASM code generation: lambda/app compilation (closure conversion) * [x] Coq: `subst_preserves_typing` (Qed) -* [ ] **Coq: close `preservation` to Qed** — the v0.1 blocker. 22 open - goals remain (down from 910); needs region-invariance + context- - preservation lemmas + the documented region-env weakening lemma - for non-values. Multi-day proof engineering. Tracked in - `formal/PRESERVATION-HANDOFF.md`. +* [ ] **Coq: close `preservation` to Qed** — the v0.1 blocker. **12 + open goals remain** as of 2026-05-21 (down from 910 at session + start). Full closure plan in + <> below. + +[#preservation-closure-plan] +== Preservation closure plan (current canonical path) + +The 5-phase plan to close `formal/Semantics.v` `preservation` to +`Qed.` Each phase has a concrete deliverable, time estimate, and +dependency chain. This is the **rightful path** any session picking +up the proof should follow. + +=== Reduction story so far + +[cols="3,1,2"] +|=== +| Stage | Open goals | Mechanism + +| Pre-campaign (in-file "Qed 2026-04-27" claim was unsubstantiated) +| 910 +| Documented honestly by PR #92. + +| After `remember (mu, R, e) as cfg` +| 29 +| Standard preservation pattern. PR #102. + +| After `revert mu R e mu' R' e' Hcfg Hcfg'` (universal-IH) +| 22 +| Clean IH quantification across congruence cases. PR #106. + +| After region-invariance lemma `step_R_eq_or_touches_region` +| 22 +| Infrastructure landed; no goals closed alone. PR #114. + +| After per-case manual closures +| **12** +| 10 β-reduction / value-step cases discharged. PR #116. +|=== + +98.7% reduction across one day. Remaining 12 = 11 congruence cases +(`S_*_Step` variants) + 1 region case (`S_Region_Step + T_Region_Active`). + +=== Phase 1 — Lemma B: linearity-context invariance for siblings + +**Goal**: a Coq lemma that lets `T_StringConcat`-style reconstruction +succeed in congruence cases. + +**Statement (sketch)**: + +[source,coq] +---- +Lemma sibling_typing_transfers_across_step : + forall mu R e mu' R' e' G G_end T G_out, + (mu, R, e) -->> (mu', R', e') -> + R; G |- e : T -| G_end -> (* original typing *) + R'; G |- e' : T -| G_out -> (* stepped typing from IH *) + G_end = G_out. (* linearity contexts coincide *) +---- + +The linearity-context evolution induced by `e` is invariant under +step. With this, sibling typing premises like +`H6 : R; G' |- e2 : ...` become typable at `R; G_out |- e2 : ...` +via `G' = G_out`. + +**Approach**: induction on `step` with `type_determinacy` per case. +Same pattern as `step_R_eq_or_touches_region`. + +**Effort**: 3–4 hours focused session. + +**Risk**: `G_end = G_out` may need weakening to "context-equivalent up +to flag positions" via the existing `types_agree` machinery. If so, +the lemma is slightly harder but still tractable. + +=== Phase 2 — Apply Lemma B → close 11 congruence cases + +**Goal**: 12 → 1 open goals. + +**Approach**: extend the PR #116 per-case manual proof pattern to the +11 `S_X_Step` cases. Each: + +. `pose proof (step_R_eq_or_touches_region ... Hstep)` → dispatch + the `R = R'` branch via `subst`. +. `edestruct (IHHstep ...)` → get `Hout : R'; G0 |- e1' : T -| Gout`. +. `pose proof (sibling_typing_transfers_across_step ...)` → get + `Gout = G'` (or the context-equivalence variant). +. `rewrite <- (sibling lemma result) in H6` or equivalent. +. `eexists; eapply T_Foo; [exact Hout | exact H6]`. + +**Effort**: ~2 hours (11 near-identical bullets). + +**Parallelizable**: yes — one agent per typing-constructor cluster +(string ops, let / app, conditionals, products, sums). + +=== Phase 3 — Region-env weakening for non-values + +**Goal**: discharge the language-design item documented since the +start of the campaign. + +**Statement (sketch)**: + +[source,coq] +---- +Lemma region_add_typing_for_non_values : + forall R e G G' T r, + R; G |- e : T -| G' -> + ~ In r R -> + safe_for_region_weakening e -> (* new predicate *) + (r :: R); G |- e : T -| G'. +---- + +**The hard part**: defining `safe_for_region_weakening`. Naive +weakening is unsound for `EBorrow` (borrows whose region escape the +weakened scope), `EDrop` of a region-bound resource, `EStringNew r' s` +where `r' = r` (shadowing). The predicate rules these out +syntactically. + +**Approach**: + +. Define the predicate (~30 LOC). +. Prove the lemma by induction on `has_type` (~80–150 LOC). +. Cross-check that the step rule `S_Region_Step + T_Region_Active` + produces an `e'` satisfying the predicate, given the typing + derivation. + +**Effort**: 1–2 days. Genuine metatheoretic work. + +**Risk**: may need predicate to depend on typing derivation, not just +expression shape. Mitigation: start with the simplest possible +predicate (no `ERegion r` or `EStringNew r` syntactically anywhere); +check if it passes the S_Region_Step case. Refine only if it fails. + +=== Phase 4 — Close S_Region_Step + T_Region_Active + +**Goal**: 1 → 0 open goals. + +**Approach**: replace `apply region_add_typing` with +`apply region_add_typing_for_non_values` in the existing +`T_Region_Active` `try solve` block at `formal/Semantics.v:3300`-ish. + +**Effort**: ~1 hour. + +=== Phase 5 — `Admitted.` → `Qed.` + docs sweep + +**Goal**: campaign closure. Mechanical (~1 hour). + +. **`formal/Semantics.v`** — replace `Admitted.` at the end of + `Theorem preservation` with `Qed.` Remove the PROOF STATUS + comment block. +. **`formal/PRESERVATION-HANDOFF.md`** — collapse to a one-line + "preservation is Qed as of YYYY-MM-DD" tombstone. +. **`PROOF-NEEDS.md`** — flip "Coq admitted proofs remaining: 1" to + "0". Drop the "what needs proving" entry for `preservation`. +. **`ROADMAP.adoc`** — flip the v0.1 checkbox; update the Coq table + row; remove this entire "Preservation closure plan" section + (replace with a 1-line "completed" note). +. **`README.adoc`** — flip the Component status table row; remove + the "22 open / 910 closed" qualifiers in Formal foundations. +. **`EXPLAINME.adoc`** — flip Coq theorem table; remove reduction + story. +. **`CHANGELOG.md`** — entry: "Coq `preservation` closed to `Qed.` + via the 910 → 0 reduction chain (PRs #92, #102, #104, #106, + #114, #116, [Phase 1 PR], [Phase 2 PR], [Phase 3 PR], + [Phase 4 PR])". +. **Wiki `Proof-status.md`** + **`Home.md`** — flip preservation + row to ✅ Qed; replace the reduction story with a one-line + "fully discharged" note. +. **Memory** — + `project_ephapax_preservation_closure_plan.md` → mark CAMPAIGN + COMPLETE. +. **`standards#124`** — post closure comment with full PR chain. +. **GitHub repo description** — drop "preservation 22 open" + qualifier. + +=== Effort + parallelization summary + +[cols="1,2,2"] +|=== +| Phase | Solo effort | Parallelizable? + +| 1 (Lemma B) +| 3–4 hours +| Single agent task. + +| 2 (Apply Lemma B) +| 2 hours +| 4 agents × ~30 min (one per typing-constructor cluster). + +| 3 (Region-env weakening) +| 1–2 days +| Single agent (research-level). + +| 4 (Close S_Region_Step) +| 1 hour +| No. + +| 5 (Qed flip + docs) +| 1 hour +| 2 agents (repo docs + wiki). +|=== + +**Sequential ceiling**: ~3 days of focused work. +**With fan-out**: ~5–7 calendar hours over 2–3 sessions. + +=== Risk-adjusted forecast + +* **80% likely**: Phases 1+2 land in one session. Phase 3 takes ~1 + day. Total: 3 sessions, ~10 hours wall-clock. +* **15% likely**: Lemma B needs context-equivalence (not equality); + phase 1 spills into a refinement session. +* **5% likely**: Phase 3 hits a language-design issue (e.g., need to + add a syntactic invariant to the typing rules). If so, the rules + get amended and all earlier `Qed`-proofs need re-checking (~1 day + detour). == v0.2.0 — Backend maturity diff --git a/formal/PRESERVATION-HANDOFF.md b/formal/PRESERVATION-HANDOFF.md index 9131b83d..d5d693f0 100644 --- a/formal/PRESERVATION-HANDOFF.md +++ b/formal/PRESERVATION-HANDOFF.md @@ -2,10 +2,15 @@ # Hand-off: closing `preservation` in `formal/Semantics.v` -Diagnostic + remediation log. The proof is still `Admitted.`, but as of -2026-05-20 it's **down from 910 open goals to ~29 real ones** via the -standard preservation pattern. This file tells whoever picks it up -next exactly what's open and why. +Diagnostic + remediation log. The proof is still `Admitted.`, but as +of **2026-05-21** it's **down from 910 open goals to 12** via four +landed PRs. This file tells whoever picks it up next exactly what's +open and what the canonical closure path is. + +> **The canonical closure plan is now in `ROADMAP.adoc` § +> "Preservation closure plan".** This file remains as the per-case +> diagnostic record. Read ROADMAP first; come back here for case +> detail. ## State at a glance @@ -13,7 +18,10 @@ next exactly what's open and why. |------|-----------:|-------| | 2026-04-27 | "fully closed" | In-file comment — but `coqc` rejected the `Qed.`. The claim was unsubstantiated; the proof never closed. | | 2026-05-20 (am) | 910 | Discovered via `Show. Show Existentials.` before the `Admitted.`. Exactly 35 (step rules) × 26 (typing rules). The existing `try solve [...]` chain closes ZERO. | -| 2026-05-20 (pm) | **29** | After the standard preservation pattern (`remember (mu, R, e) as cfg` + symmetric for cfg', then `inversion Hcfg; subst; inversion Hcfg'; subst;` inside each case). 97% reduction. | +| 2026-05-20 (pm) | 29 | After the standard preservation pattern (`remember (mu, R, e) as cfg` + symmetric for cfg', then `inversion Hcfg; subst; inversion Hcfg'; subst;` inside each case). 97% reduction. PR #102. | +| 2026-05-20 (eve) | 22 | After `revert mu R e mu' R' e' Hcfg Hcfg'` before `induction Hstep` so each case's IH carries universal quantification over the inner step's config. PR #106. | +| 2026-05-20 (eve) | 22 | Region-invariance lemma `step_R_eq_or_touches_region` landed as infrastructure (no goal closures). PR #114. | +| 2026-05-20 (night) | **12** | 10 β-reduction / value-step cases discharged via per-case manual proofs using the lemma. PR #116. **98.7% reduction across one day.** | ## What the 910 → 29 fix did