Skip to content

docs(proof-status): correct stale preservation/progress claims #87

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
May 20, 2026
Merged

docs(proof-status): correct stale preservation/progress claims #87

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions PROOF-NEEDS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,25 +2,25 @@

## Current state
- `formal/Syntax.v` — Coq formalization of Ephapax syntax (clean)
- `formal/Semantics.v` — Coq operational semantics (`preservation` currently `Admitted`)
- `formal/Semantics.v` — Coq operational semantics; `preservation` Qed (closed 2026-04-27, zero `Admitted` in this file)
- `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: 1
- Coq admitted proofs remaining in `formal/Semantics.v`: 0

## What needs proving
- **Close remaining Admitted in Semantics.v**: `preservation`
- **Type soundness end-to-end**: Complete progress + preservation proof chain (preservation currently admitted)
- **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.

## Recommended prover
- **Coq** for closing existing Admitted gaps (already invested in Coq formalization)
- **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
- **HIGH** — Ephapax is a programming language whose core value proposition is linear types and memory safety. The remaining `Admitted` in `preservation` blocks a fully closed soundness chain.
- **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.
19 changes: 12 additions & 7 deletions ROADMAP.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,10 +20,13 @@ 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` currently `Admitted`.
* Coq admitted proofs remaining: 1
`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
* **Idris2** (`src/formal/`): `noEscapeTheorem`, `regionSafetyTheorem`, `noGCTheorem`,
`orthogonalityLemma` -- all complete with zero unsafe patterns.
`orthogonalityLemma` -- all complete with zero unsafe patterns. Added 2026-05-19:
`splitLinearCoverage` in `Ephapax/Formal/Qualifier.idr` (PR #85) — generalises
`nonDiminishment` from head-position to all linear bindings.

**Interpreter:** Environment-leak fix applied (2026-03-28). Proofs chain and effects
chain are sound.
Expand All @@ -47,8 +50,10 @@ chain are sound.
* [ ] WASM code generation: lambda/app compilation (closure conversion)
* [x] Coq: close `ctx_transfer` proof
* [x] Coq: close `subst_lemma` proof
* [ ] Coq: close `preservation` proof (currently `Admitted`)
* [ ] Coq: `progress` proof completion (currently 92%)
* [x] Coq: close `preservation` proof (Qed, 2026-04-27)
* [-] 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.

== v0.2.0 -- Backend Maturity

Expand Down Expand Up @@ -81,8 +86,8 @@ PipeWire filter node as a real-world validation of linear types for audio buffer

== v1.0.0 -- Production Ready

* [ ] All Coq `Admitted` proofs closed (zero remaining)
* [ ] Full `preservation` and `progress` proofs (Qed)
* [x] All Coq `Admitted` proofs closed in `formal/Semantics.v` (zero remaining as of 2026-04-27).
* [x] `preservation` proof (Qed, 2026-04-27). `progress` is not currently formalised; if it re-enters scope post-rewrite, add it back here.
* [ ] Stable surface syntax (already locked, but confirm no changes needed)
* [ ] Comprehensive standard library
* [ ] Cross-platform WASM + native compilation
Expand Down
Loading