Skip to content

ROADMAP.adoc

Latest commit

 

History

History
341 lines (278 loc) · 14.4 KB

ROADMAP.adoc

File metadata and controls

341 lines (278 loc) · 14.4 KB

Ephapax Roadmap

Status snapshot (2026-06-02)

Ephapax is an early-development linear-type language implemented across ~19 Rust crates with a two-phase compiler pipeline (Idris2 type-checking → Rust/WASM backend). Lexer, parser, interpreter, REPL, CLI, S-expression IR, two-phase pipeline, Zig FFI, and conformance test suite are complete. Type checker and WASM code generation are in progress.

2026-06-01 → 02 proof + stdlib wave (13 PRs): canonical-forms L1 modality-polymorphic (P43, axiom-free, prerequisite for progress_l1); Print Assumptions audit framework across L1 + L3 keystones (P10/P32); step_pop_disjoint_from_type_l1 stated + EASY cases (P06, HARD cases blocked on issues #240/#241/#242); Rust↔Coq is_linear_ty bridge truth- table (P28); OwnershipKind from_byte/to_byte round-trip (P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions (D04), Allen’s interval algebra (D11), MessageHandle (D17), monoidal aggregates (D18). Stages 2-4 of the Phase 3b plan (#240/#241/#242) remain un-touched. See CHANGELOG.md for full enumeration and per-PR detail.

Four-layer redesign (2026-05-26 → )

The verified preservation counterexample (formal/Counterexample.v, five Qed lemmas) closed the original preservation closure plan as unreachable in the legacy single-layer typing judgment. The new plan separates four orthogonal layers; each is implemented in sequence and preservation is re-derived per layer from explicit invariants.

  1. L1 — Region capability threading

    • Restate the typing judgment to thread R_in / R_out (the region-capability environment) through every compound rule.

    • Land in formal/TypingL1.v + formal/Semantics_L1.v against Counterexample.v as a regression oracle.

    • Status: judgment landed, m-indexed post-L2-hybrid; 9 L1 supporting-lemma admits remain as L2-integration debt.

  2. L2 — Modality parameter

    • Promote the per-type is_linear_ty predicate to a judgment parameter m : Modality.

    • Mechanise linear_to_affine : Linear ≤ Affine as a single induction.

    • Status: landed in-place via PRs #176 + #177; linear_to_affine Qed with zero axioms.

  3. L3 — Echo residue

    • formal/Echo.v mirrors echo-types/proofs/agda/Echo.agda. The L3 calculus (modes, LEcho, weaken, degrade_mode) is mechanised locally.

    • Next: introduce TEcho ⟨op⟩ + the T_Observe rule into the typing judgment; modify S_Region_Exit and S_Drop to produce residue values.

    • Status: K-free scaffold landed via #166/#167/#173; typing-rule integration is the next-block work.

  4. L4 — Mode declaration

    • Project-level metadata (Cargo.toml or ephapax.toml). Type checker reads the declaration and selects the L2 modality.

    • No proof obligations of its own — see formal/L4-DYADIC.md.

    • Status: mechanical scaffold landed in formal/L4.v (ProgramMode + program_mode_to_modality); surface syntax not yet wired into the parser.

The previous Preservation closure plan section is archived — see formal/PRESERVATION-HANDOFF.md for the historical record. PRs #92 / #102 / #104 / #106 / #114 / #116 / #117 / #121 / #146 are pre-discovery; treat them as archaeology, not instructions.

Canonical design source: formal/PRESERVATION-DESIGN.md.

Formal-proof status

Coq (formal/)

The Coq side has the Tofte-Talpin region-linear calculus with small-step substitution semantics:

Theorem / lemma Status Notes

no_leaks

✅ Qed

Memory-safety property — every linear resource freed at region exit.

typing_ctx_transfer

✅ Qed

Context-transfer machinery used by preservation’s congruence cases.

subst_preserves_typing

✅ Qed

Substitution lemma — the core technical lemma underpinning preservation.

region_env_perm_typing

✅ Qed

Region-permutation invariance of typing.

region_add_typing

✅ Qed

Adding a fresh region to R preserves typing.

region_shrink_preserves_typing

✅ Qed

Closing a region scope preserves typing of the body’s value form.

preservation (legacy)

🔴 Admitted — provably false, do not attempt to close

formal/Counterexample.v exhibits five Qed. lemmas showing the theorem is genuinely false (bad_typable, bad_step, bad_post_untypable, t_loc_l1_R_preserving, bad_input_untypable_l1). The 11-goals story (PRs #92/#102/#104/#106/#114/#116/#117/#121/#146) is pre-discovery archaeology. The work is the four-layer redesign in formal/PRESERVATION-DESIGN.md, with preservation re-derived per-layer (preservation_l1 in Semantics_L1.v, etc.). See CLAUDE.md at repo root for the owner directive (2026-05-27).

Historical note: 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 (2026-05-20) corrected the status to Admitted. with honest framing. The "92%" progress proof referenced in older docs was deleted in the substitution- semantics rewrite and is not currently formalised in this tree.

Idris2 (idris2/src/Ephapax/)

The Idris2 side has totality-tightening across the entire parser / typechecker / encoder layer:

Module Default Notes

IR/SExpr

%default total

Fueled mutual parser; fuel = length input, every primitive consumes ≥1 char.

Parse/Stream

%default total

Fueled remaining/build; fuel = s.len - s.index.

Parse/Util

%default total

Fueled many + sepBy.sepTail; fuel = remaining tokens.

Parse/Lexer

%default total

Fueled lex.go across all 57 recursive call sites.

IR/AST

%default total

6 retained covering markers for showPrec / (/=) interface-dispatch loop (documented Idris2 0.8.0 SCT limit, not unsoundness).

IR/Decode

%default total

7 retained covering markers for map/traverse-through-recursive-type SCT limit.

Affine/Typecheck

%default total

Full type checker provably total. Incidental baseline-rot fix for an if-then-else layout.

Parse/Parser

%default covering

LL(k) recursive descent through ~30 mutually-recursive Stream-indexed parsers; fueling the whole parser is a deferred separate campaign.

Affine/Emit

%default total

One-line encode wrapper, covering matches Decode.encode.

Net post-campaign (PRs #89/#90/#91/#93/#94/#96/#97/#99/#100, all merged 2026-05-20): 80+ atomic functions provably total, zero assert_total / believe_me introduced anywhere in the source. 14 covering markers retained, each for a documented Idris2 0.8.0 SCT limit. No %default partial remains in idris2/src/Ephapax/.

Idris2 region-linearity layer (src/formal/)

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

  • noEscapeTheorem — region references cannot leak past their scope

  • regionSafetyExtract — typed expressions don’t dereference freed regions

  • noGCExtract — bulk deallocation at region exit is sound

  • orthogonalityLemma — the linear / region disciplines compose

  • splitLinearCoverage (PR #85, 2026-05-19) — generalises nonDiminishment from head-position to all linear bindings

All four headline theorems complete with zero believe_me / assert_total / postulates.

v0.1.0 — Core language (in progress)

  • ✓ Core type system design (affine + linear modes)

  • ✓ Lexer (logos-based tokenizer)

  • ✓ Parser (chumsky-based)

  • ✓ Tree-walking interpreter with env-leak fix (2026-03-28)

  • ✓ REPL

  • ✓ CLI (ephapax-cli)

  • ✓ Coq: no_leaks, subst_preserves_typing, region lemmas (all Qed)

  • ✓ Idris2: all four region-linearity theorems complete (zero unsafe)

  • ✓ Idris2: %default partial → total campaign for parser / typechecker / encoder layer (PR chain #89–#100, merged 2026-05-20)

  • ✓ S-expression IR (ephapax-ir)

  • ✓ Two-phase pipeline: Idris2 type-check → Rust/WASM backend

  • ✓ Zig FFI token buffer (Ephapax.Parse.ZigBuffer)

  • ✓ Conformance test suite (pass / fail cases)

  • ❏ Type checker completion (ephapax-typing)

  • ❏ WASM code generation: lambda/app compilation (closure conversion)

  • ✓ Coq: subst_preserves_typing (Qed)

  • ❏ Coq: re-derive preservation in the four-layer architecture — Theorem preservation in formal/Semantics.v is provably false (verified by formal/Counterexample.v, five Qed lemmas). The work is not to close that theorem; it is to derive preservation_l1 / preservation_l2 / preservation_l3 per-layer in the redesigned architecture documented in formal/PRESERVATION-DESIGN.md. Status (2026-06-01):

    • L1 (Semantics_L1.v preservation_l1): Admitted with 1 inner admit. covering S_StringConcat/S_App/S_Pair Step2 cases (lambda-rigidity gap closing via Phase 3b Stage 2+3+4);

    • L2 (in-place modality, PRs #176 + #177): linear_to_affine Qed zero axioms; preservation_l2_via_l1 Qed (conditional on preservation_l1); 3 β-case lemmas Qed for ground non-linear, Stage 1b TFunEff (conditional on side conditions), and Linear; unconditional preservation_l2 blocked on Phase 3b Stages 2/3/4 (#240/#241/#242);

    • L3 (Echo.v + slice 4 wiring): preservation_l3_region_active_echo, preservation_l3_drop_echo, and umbrella preservation_l3 all Qed (conditional on the region_shrink_preserves_typing_l1_gen_m structural admit that itself closes at Phase D);

    • L4 (L4.v): Phase A scaffold landed 2026-05-28 (Definitions only — PModeLinear / PModeAffine / PModeBoundaryMix
      program_mode_to_modality round-trip). See also CLAUDE.md at repo root and PROOF-NEEDS.md for the complete picture.

Preservation: superseded by four-layer redesign

This section formerly contained a 5-phase plan to close Theorem preservation in formal/Semantics.v to Qed. That plan is obsolete — the verified counterexample (formal/Counterexample.v) shows the theorem is provably false. No sequence of lemmas closes it because no proof exists.

Canonical path now:

  • Design source: formal/PRESERVATION-DESIGN.md (four orthogonal layers: L1 region capabilities / L2 modality / L3 echo / L4 dyadic mode).

  • Layered Coq files: TypingL1.v (now m-indexed post-#176), Semantics_L1.v, Modality.v, Echo.v — preservation re-derived per layer from explicit invariants.

  • Agent guidance: CLAUDE.md at the repo root.

  • Historical record: the per-case reduction story (910 → 11 goals) lives in formal/PRESERVATION-HANDOFF.md as archaeology. PRs #92 / #102 / #104 / #106 / #114 / #116 / #117 / #121 / #146 are pre-discovery; treat them as history, not instructions.

The git history of this file retains the original closure plan if diagnostic detail is ever needed.

v0.2.0 — Backend maturity

  • ✓ Closure conversion for WASM backend

  • ❏ Native backend via Cranelift

  • ❏ Region-based allocation in WASM linear memory

  • ❏ Bulk deallocation on region exit

  • ❏ Standard library foundation (ephapax-stdlib) — partial implementation

  • ❏ Surface syntax desugaring pipeline (ephapax-desugar)

  • ✓ Package system (ephapax-package) — complete core functionality

  • ❏ LSP server (ephapax-lsp) — basic diagnostics implemented, needs completion

v0.3.0 — PipeWire proving ground

PipeWire filter node as a real-world validation of linear types for audio buffer management:

  • ❏ PipeWire filter node implementation in Ephapax

  • ❏ Linear buffer types proving zero-copy audio safety

  • ❏ Real-time constraints validation (no GC pauses)

  • ❏ Integration with AmbientOps audio pipeline

v0.4.0 — Tooling and ecosystem

  • ❏ Tree-sitter grammar (editors/tree-sitter-ephapax) editor integration

  • ❏ LSP server — full features (hover, go-to-definition, completions)

  • ❏ Documentation generator (ephapax-doc)

  • ❏ VRAM cache for GPU-side linear resources (ephapax-vram-cache)

  • ❏ Static analysis module (ephapax-analysis)

  • ❏ Error recovery in parser for IDE use

v1.0.0 — Production ready

  • ❏ Per-layer preservation theorems closed: preservation_l1, preservation_l2 (unconditional, post-Phase-3b Stage 4), and preservation_l3 (umbrella) all Qed. in formal/Semantics_L1.v with clean Print Assumptions. See formal/PRESERVATION-DESIGN.md §12 and Phase 3b Stages 2/3/4 (#240/#241/#242).

    Note
    		 The legacy Theorem preservation in formal/Semantics.v is provably false (formal/Counterexample.v) and stays Admitted. by owner directive 2026-05-27. Closing it is NOT a v1.0 blocker — the four-layer redesign supersedes it.

  • ❏ Idris2 Parse/Parser.idr upgraded from %default covering to %default total (LL(k) fuel-refactor; deferred separate campaign)

  • ❏ Stable surface syntax (already locked, but confirm no changes needed)

  • ❏ Comprehensive standard library

  • ❏ Cross-platform WASM + native compilation

  • ❏ Performance benchmarks vs Rust/C for linear workloads

  • ❏ Published language specification (spec/)

Long-term

  • ❏ Session-sentinel integration (Ephapax rewrite of session management)

  • ❏ Gossamer integration for UI applications

  • ❏ IDApTIK migration to Ephapax where linear types add value

  • ❏ Self-hosting: Ephapax compiler written in Ephapax

Related documents

  • README — project overview + quickstart

  • EXPLAINME — "show me the receipts" for the README’s claims

  • PROOF-NEEDS — outstanding proof obligations + leverage

  • RUST-SPARK-STANCE — comparison + interop notes

  • PRESERVATION-HANDOFF — archaeology only: per-case Coq preservation checklist from the pre-discovery legacy-judgment closure plan. Retained for historical context. Not actionable; see formal/PRESERVATION-DESIGN.md for the four-layer redesign.

  • Vision document — design rationale

  • Design decisions — 17 ADRs

  • Language comparison — vs 10 other languages