Proof status

Proof status

This page is the canonical "what's proven / what's open" status for Ephapax's mechanical formalisation. Updated 2026-05-21.

For per-case detail on the open work, see formal/PRESERVATION-HANDOFF.md and PROOF-NEEDS.md.

---

Coq (formal/Semantics.v + formal/Typing.v + formal/Syntax.v)

The Coq side has a small-step substitution-based calculus over the Tofte-Talpin region-linear type system. Substitution-based (not environment-based) since a 2026-03-28 rewrite that eliminated an environment-leaking bug.

Closed (Qed)

Lemma / theorem	Where	What it says
values_dont_step	Semantics.v:268	Values are normal forms.
mem_free_region_clears	:283	Region exit drops the whole region.
no_leaks_gen	:339	Generalised no-leaks induction.
no_leaks	:374	Soundness headline — every linear resource freed at region exit.
flags_only_increase	:407	Consumption flags are monotone.
ctx_mark_used_* (5 lemmas)	:455–:707	Context-marking technology.
typing_preserves_bindings	:485	Typing preserves binding shape.
canonical_{bool, fun, prod, sum, string}	:523–:550	Canonical-forms lemma per type.
consumption_chain	:783	Consumption flag propagation.
typing_preserves_types_agree	:841	Types-agree preservation.
borrow_preserves_ctx	:905	Borrows don't consume.
stringlen_preserves_ctx	:910	StringLen via borrow.
type_determinacy	:919	Typing is functional.
no_consumption_at_true_linear	:990	Linear-flag invariant.
region_env_perm_typing	:2960	Region-env permutation preserves typing.
region_add_typing	:3042	Adding a region preserves typing.
region_shrink_preserves_typing	:3107	Shrinking a region preserves typing of value-form bodies.
subst_typing_gen	:2592	Substitution lemma (general form).
subst_preserves_typing	:2808	Headline substitution lemma — used by preservation's beta-reduction cases.

(+ ~50 supporting lemmas — see formal/Semantics.v.)

Admitted

Theorem	Where	What's open
preservation	Semantics.v:3207	12 open goals as of 2026-05-21 — see below.

The preservation reduction story

The theorem preservation has had five substantial reduction passes across 2026-05-20 → 2026-05-21:

Start: 910 open goals

The original induction Hstep; intros G0 T0 G0' Htype; inversion Htype; subst; ... produced the full 35 × 26 = 910 cross-case combinatorial. induction Hstep did not substitute the outer expression slot e to the constructor's form, so inversion Htype produced all 26 typing arms per step rule instead of just the diagonal. Cross-cases (e.g. S_StringNew step + T_Unit typing) had no discriminating equation in scope, so try solve [exfalso; discriminate | exfalso; congruence] couldn't fire on any of them.

An earlier in-file comment claimed preservation was Qed-closed on 2026-04-27. That claim was unsubstantiated; coqc 8.18.0 rejected the proof script. PR #92 corrected the status with Admitted. and honest framing.

910 → 29 via remember-cfg (PR #102)

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 — substitutes the constructor's "from"/"to" expression into e/e' and discriminates the cross-cases. 97% reduction.

29 → 22 via universal-IH revert (PR #106)

The remember (mu, R, e) as cfg baked the OUTER cfg equation into every child IH, making the IHs unusable for congruence cases:

IHHstep : (mu_inner, R_inner, e_inner) = (mu, R, EOuter ...) -> ...

— inconsistent in general (e_inner 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 over the inner step's config:

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

Plus a targeted T_Loc inversion tactic for the S_StringConcat axiom case (sibling typing's T_Loc inversion derives r = r0, unblocking the result type). Closes 7 goals; 22 remain.

Region-invariance lemma — infrastructure only (PR #114)

Lands step_R_eq_or_touches_region: forall step, R = R' ∨ touches_region e. Qed-closed. No goals closed in preservation directly, but the lemma is the building block the per-case proofs use.

22 → 12 via per-case manual proofs (PR #116)

10 β-reduction / value-step cases discharged manually using the new region-invariance lemma + existing subst_preserves_typing / value_context_unchanged / typing-inversion machinery:

• S_Let_Val, S_LetLin_Val — β-reduction via substitution
• S_App_Fun — inversion of ELam typing + value-context invariance
• S_If_True, S_If_False — branch typing under VBool invariance
• S_Fst, S_Snd — EPair inversion → child typing match
• S_Case_Inl, S_Case_Inr — sum-inversion + body substitution
• S_Copy — T_Pair on non-linear value

Cumulative: 98.7% reduction across one day (910 → 12).

Phase 1 scaffold — Lemma B stated (PR #121)

Adds the canonical statement of step_output_context_eq (Lemma B of the closure plan) with induction-on-step skeleton; per-case discharges deferred to a focused session via Admitted scaffold.

12 → 0 (canonical closure plan — see ROADMAP)

The remaining 12 goals split as:

• 11 congruence cases blocked on Lemma B's per-case discharges (step_output_context_eq — the IH-vs-sibling linearity-context mismatch). Phase 2 of the closure plan.

• 1 region case (S_Region_Step + T_Region_Active) blocked on the documented region-env weakening for non-values. Phase 3 of the closure plan — needs a safe_for_region_weakening predicate (~30 LOC) + weakening lemma (~80–150 LOC).

Per ROADMAP, total remaining effort: ~3 sessions / ~10 hours wall-clock with fan-out, ~3 days sequential.

---

Idris2 frontend (idris2/src/Ephapax/)

The Idris2-side of the two-phase compiler pipeline: parser, typechecker, IR codec. All 9 files compile under %default total or %default covering. Zero assert_total, zero believe_me, zero assert_smaller introduced anywhere in the frontend.

Outcome of the 2026-05-20 totality campaign

File	Default	Lemma-class status
IR/SExpr.idr	%default total	Fueled mutual parser; fuel = length input.
Parse/Stream.idr	%default total	Fueled remaining/build; fuel = s.len - s.index.
Parse/Util.idr	%default total	Fueled many + sepBy.sepTail.
Parse/Lexer.idr	%default total	Fueled lex.go across 57 recursive call sites.
IR/AST.idr	%default total + 6 covering	Show/Eq instances hit the showPrec/(/=) interface-dispatch loop.
IR/Decode.idr	%default total + 7 covering	encodeExpr / decodeExpr recurse through map / traverse on List Expr — SCT can't trace it.
Affine/Typecheck.idr	%default total	Provably total; required incidental baseline-rot layout fix.
Parse/Parser.idr	%default covering	LL(k) recursive descent through ~30 mutually-recursive Stream-indexed parsers; fueling deferred.
Affine/Emit.idr	%default total + 1 covering	One-line encode wrapper; covering inherits from Decode.encode.

Lemma upgrade: 80+ atomic functions are now provably total that were previously implicitly partial (atomic encode/decode helpers, all atomic Eq/Show instances, isLinear, the entire check typechecker function).

Retained escapes: 14 covering markers total. Each one corresponds to a documented Idris2 0.8.0 SCT limit:

• showPrec / (/=) interface-dispatch loop (6 markers in AST)
• map / traverse through recursive types (7 markers in Decode)
• 1-line encode wrapper inherits from Decode (1 marker in Emit)

These are strictly stronger than the previous %default partial: covering asserts exhaustive pattern matching has been verified; only termination is deferred.

PRs: #89 (SExpr), #90 (Stream), #91 (Util), #93 (Lexer), #94 (AST), #96 (Decode), #97 (Typecheck), #99 (Parser), #100 (Emit) — all merged 2026-05-20.

---

Idris2 region-linearity (src/formal/)

Separate Idris2 development proving structural properties of the region-linear calculus.

Theorem	Where	Status
noEscapeTheorem	Ephapax/Formal/RegionLinear.idr:129	✅ Complete, zero unsafe
regionSafetyExtract	Ephapax/Formal/RegionLinear.idr:139	✅ Complete, zero unsafe
noGCExtract	Ephapax/Formal/RegionLinear.idr:151	✅ Complete, zero unsafe
orthogonalityLemma	Ephapax/Formal/RegionLinear.idr:164	✅ Complete, zero unsafe
splitLinearCoverage	Ephapax/Formal/Qualifier.idr:213	✅ Complete (PR #85, 2026-05-19) — generalises nonDiminishment from head-position to all linear bindings

All five with zero believe_me, zero postulates, under %default total.

---

How to verify locally

Coq

cd formal
coqc -Q . Ephapax Syntax.v
coqc -Q . Ephapax Typing.v
coqc -Q . Ephapax Semantics.v   # ~1 minute, builds with Admitted

Or via the project's Just recipe:

just proofs

Idris2 frontend

cd idris2/src
IDRIS2_PREFIX=/path/to/idris2-0.8.0 idris2 --check Main.idr   # builds 11/11 modules

The IDRIS2_PREFIX is required because the asdf install of Idris2 0.8.0 has no compiled TTCs for base. The tools/provers install does.

Idris2 region-linearity

cd src/formal
idris2 --build ephapax-formal.ipkg

---

Last updated: 2026-05-20 evening (after PR #106 filed).