image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/ephapax"] image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: MPL-2.0,link="https://www.mozilla.org/MPL/2.0/"] image:https://img.shields.io/badge/Philosophy-Palimpsest-indigo.svg[Palimpsest,link="https://github.com/hyperpolymath/palimpsest-license"] image:https://github.com/hyperpolymath/ephapax/actions/workflows/codeql.yml/badge.svg?branch=main[CodeQL,link="https://github.com/hyperpolymath/ephapax/actions/workflows/codeql.yml"] image:https://api.thegreenwebfoundation.org/greencheckimage/ephapax.org[Green Hosting,link="https://www.thegreenwebfoundation.org/green-web-check/?url=ephapax.org"]

// SPDX-License-Identifier: CC-BY-SA-4.0 // Owner: Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk :toc: macro :toclevels: 3 :icons: font :source-highlighter: rouge :experimental:

= Ephapax

ἐφάπαξ — once for all.

[IMPORTANT] .Not to be confused with AffineScript

This is Ephapax, a research language for WebAssembly memory safety. It is not https://github.com/hyperpolymath/affinescript[AffineScript], a separate language at hyperpolymath/affinescript that succeeds JS / TS / ReScript.

The two share exactly one thing: both target https://github.com/hyperpolymath/typed-wasm[typed-wasm]. They have separate ASTs, separate type checkers, separate compilers, separate proof stories. The word affine overlaps in both names because it names a substructural- logic property — that's a logic-family fact, not a project relationship.

Internal note: Ephapax is itself dyadic — ephapax-linear (strict core) and ephapax-affine (versatile prototyping companion) are both inside this repo, one Rust crate, one AST, two structural disciplines. ephapax-affine is not AffineScript. When ambiguous, write "ephapax-affine sublanguage" vs "AffineScript language".

Canonical disambiguation (read this before applying any cross-repo lesson): link:https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md[nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md].

[NOTE] .🌱 Ephapax is gestating — second-draft in progress, and going well (start with V1-TO-V2.adoc)

This language is not dead, abandoned, or frozen — it is mid-way through a deliberate second draft, on two independent tracks, and both are landing. The full story (and why the older "provably false / archaeology" wording misled readers into writing the project off) is in link:V1-TO-V2.adoc[V1-TO-V2.adoc]. Read that first; this box is the short version.

The grammar (v1 → v2). The flat v1 surface worked for the core but could not grow into modules / generics / effects / comptime. v2 adds the missing layer — surface → desugar → core — and is landing in phases, tests green (spec/ephapax-v2-grammar.ebnf + the v2_grammar_phase_* suite).

The soundness proof (v1 → v2). On 2026-05-26 a machine-checked Coq counterexample (link:formal/Counterexample.v[formal/Counterexample.v], 5 Qed lemmas) proved that preservation as stated in the legacy single-judgment design is unsound — a region exit could invalidate a sibling's assumptions untracked. Discovering that with a proof, before anyone depended on it, is the rare correct thing, not a failure. The redesign re-derives preservation across four orthogonal layers (regions / modality / echo / dyadic mode), each from its own explicit invariants. The legacy theorem stays Admitted on purpose — it is proven unclosable, so it is fenced off, not abandoned.

Quick proof-status read: L1 (region capabilities) substantially complete; L2 (Linear/Affine modality) core landed with zero axioms; L3 (echo / residue) wiring landed (slice 4, 2026-05-27) — preservation_l3 + preservation_l3_region_active_echo + preservation_l3_drop_echo all Qed (conditional on L1 structural admits, see PROOF-NEEDS.md §4); L4 (dyadic mode) Phase A scaffold landed 2026-05-28 (formal/L4.v, definitions by design).

For anyone (human or bot) doing the work: the only fenced-off artefacts are the one falsified legacy theorem and the one superseded flat grammar. Everything in the v2 columns — the grammar phases and the per-layer proofs — is open and tractable. Authoritative maps: link:V1-TO-V2.adoc[V1-TO-V2.adoc] (the frame), link:STATUS.adoc[STATUS.adoc] (operational past/present/future), link:formal/PRESERVATION-DESIGN.md[formal/PRESERVATION-DESIGN.md] (four-layer architecture), link:PROOF-NEEDS.md[PROOF-NEEDS.md] (proof debt + do-not-do list). Anything dated before 2026-05-26 describing a "preservation closure plan" or "910 → 12 goals" is the record of how the first draft hit its wall — read it as history, not instructions.

Ephapax is a research language for principled handling of irreversible boundaries (region exits, drops, key erasure, audit trails) in compile-time-memory-safe WebAssembly. Real systems are irreversible — operating systems deallocate, databases drop tables, security systems erase keys, compilers collapse high-level distinctions. Ephapax gives a disciplined, machine-checkable framework to handle those boundaries responsibly: the type system tracks not just what is owned but what was lost when it was given up, so reclamation can carry mandatory evidence where it matters (audit, compliance, cryptographic erasure) and degrade to free where it doesn't (inference loops, hot paths).

The core calculus is mechanically formalised. Soundness theorems on the dynamic side (Coq) and structural-safety theorems on the type side (Idris2) are checked by their respective proof assistants on every push.

toc::[]

== Why "Ephapax"?

The Greek ἐφάπαξ ("ephapax") means once for all. It is the guarantee linear types make: every resource is used exactly once. You consume it, or you transfer ownership of it, or you drop it — but you cannot reach for it twice, and you cannot forget about it.

== What this is

Ephapax is a programming language with:

[cols="1,3"] |=== | Property | What this means

| Dyadic discipline (L2) | Each binding is either affine (let — used at most once, weakening allowed) or linear (let! — used exactly once, weakening forbidden). Type checker enforces. See "The four layers" below for how this composes with L1/L3/L4.

| Region-based memory (L1) | Allocations live in named regions (region r: ...). The type system threads a region-capability environment through every expression so a sibling cannot read from a region another sibling has just exited. When a region's scope ends, the runtime bulk-frees every resource in it. No allocator overhead per object; no per-object frees.

| Second-class borrows | &x gives temporary access without consuming x. Borrows cannot be stored, escape their introduction scope, or be used after the borrowed resource is freed.

| Compile-time memory safety | No use-after-free, no double-free, no leaks of linear resources — caught at type-check time, before a binary is produced.

| WebAssembly target | wasm32-unknown-unknown primary; native via Cranelift secondary.

| No GC, no allocator runtime | Region exits do the bulk deallocation. No tracing collector, no reference counting, no allocator-per-object metadata. |===

== The four layers

Ephapax composes four orthogonal disciplines. Each is a thin-poset refinement, so they compose without coherence obligations (https://github.com/hyperpolymath/echo-types[echo-types] supplies the recipe).

[cols="1,3"] |=== | Layer | What it enforces

| L1 — Region capabilities | Every live region is tracked in an input/output environment threaded through every expression. A region cannot be referenced after a sibling has exited it. Soundness proof in formal/TypingL1.v + formal/Semantics_L1.v.

| L2 — Structural discipline (linear ↔ affine) | The modality of the surrounding program decides whether linear bindings must be consumed (Linear: ephapax-linear) or may be dropped (Affine: ephapax-affine). Same syntax, same semantics — different admissible derivations. Linear ⊆ Affine, proved by linear_to_affine Qed in formal/Modality.v.

| L3 — Irreversibility residue (Echo) | Operations that erase information (region exit, drop) produce proof-relevant residue — Echo f y := Σ A (λ x → f x ≡ y). In Linear mode the residue must be observed; in Affine mode it may be silently lowered. Calculus mechanised in formal/Echo.v; integration into the typing judgment is the next-block work.

| L4 — Dyadic interaction mode | A project-level declaration of which side of the dyad the program speaks from (ephapax_linear / ephapax_affine / module_boundary_mix). Selects the L2 modality and the L3 observation discipline. No proof obligations of its own — mechanical scaffold in formal/L4.v carries definitions only by design. |===

.Soundness story

---

The four-layer separation is not decorative — it exists because the original "linear+affine + regions" framing admitted a verified counterexample to preservation (see formal/Counterexample.v and formal/PRESERVATION-DESIGN.md). The four-layer redesign restores soundness by making each discipline's invariants explicit and orthogonal: preservation is re-derived per layer from explicit invariants rather than forced through a single judgment that hides them.

---

== Three superpowers

The L3 echo / residue layer (Ephapax's contribution to the four-layer design) opens three things proper reversible programming struggles with:

[cols="1,3"] |=== | Superpower | What it gives you

| A. Accountability of irreversible reclamation | You can free memory (S_Region_Exit, S_Drop) and the type system knows you lost the data — and tracks what depended on it. Under the Linear modality the reclamation event carries a mandatory evidence-bearing Echo value; under Affine you opt out for performance. Pairs cleanly with region-based memory management (deterministic bulk free) to deliver high-assurance reclamation that tracing GC cannot — by design, tracing GC hides the reclamation evidence.

| B. Selective reversibility (thin-poset) | Linear ≤ Affine is a two-point thin poset at the L2 modality. You pick per-region (or per-project) which discipline applies. Same code shape, different evidence obligations. Concrete examples: Linear during backpropagation (must keep the gradient residue); Affine during inference (drop the residue, save memory). You get the safety of reversibility where you need it, and the performance of irreversibility where you don't.

| C. Debugging + provenance | Attach Linear Echoes to critical state changes. The type system guarantees the receipt (preimage) of that state change was retained — so when a bug fires, the inputs that produced the error are recoverable by construction. In Affine mode you opt out of this debugging info, with the same code shape. The evidence is a theorem-level guarantee, not a runtime convention. |===

[CAUTION] .Echo Types are NOT a tracing-GC replacement

Echo Types do not solve reachability or cycles. They are not a "fire-and-forget" automatic memory manager. Their strength is accountability of irreversible reclamation in systems that already know when and how to deallocate (regions, explicit drop, deterministic ownership). Treating them as competition for mark-and-sweep or generational GC is a category error.

The committed v1 direction is Linear Echo + Region-Based Memory Management (deterministic bulk free with mandatory certified evidence). A speculative future direction is an optional Linear discipline on deterministic Rust-style drop for critical resources (keys, sensitive buffers requiring provable erasure) — flagged but not committed.

== What this enables

The three superpowers translate to concrete use cases the type system can prove properties about:

• Mandatory evidence for critical actions. By making certain echoes Linear (mandatory observation), the type system guarantees that a region exit always emits an audit trail, or that a drop always triggers a required cleanup.

• GDPR "right to be forgotten" with certified evidence of erasure. Linear-echo discipline on the S_Drop of a personal-data resource is a type-level proof that erasure happened and that the required notification / log was produced. Auditors get a machine-checkable artefact instead of a process attestation.

• Verified resource management for keys, secrets, and sensitive buffers. Linear-echo on the deallocation of a key buffer guarantees provable erasure; the typing rule cannot be silenced.

• Selective reversibility without redesigning your language. The thin-poset means you don't redesign the runtime to be bijective. You add one type former (the fiber) and layer existing L2 modalities over it. Orthogonal and compositional.

• Machine-checkable foundation for policy enforcement. The thin-poset Linear ≤ Affine + the proven non-invertibility (EchoResidue.no-section-collapse-to-residue) gives sharp, proof-relevant reasoning: weakening obligations is allowed, strengthening them back is impossible. Clean logical foundation for compliance work.

== What this isn't

• Not Rust. Rust uses ownership + borrowing with a single discipline (affine-ish, with linearisation via Drop). Ephapax separates the two disciplines explicitly: let is affine, let! is linear, and the user chooses per-binding.
• Not a research vapourware. 17 active Rust workspace crates + tests/fuzz (with src/ephapax-tools/ outside the workspace and src/ephapax-vram-cache/ explicitly disabled — needs hyperpolymath/ephapax-proven); the lexer, parser, interpreter, REPL, CLI, S-expression IR, two-phase pipeline, Zig FFI, and conformance test suite are complete. Type checker and WASM codegen are in progress. See ROADMAP.adoc.
• Not yet self-hosting. The compiler is written in Rust. The formalisation is in Coq + Idris2. Self-hosting is a v1.0+ goal.

== Hello, world

[source,ephapax]

fn main() -> i32 { let x = 1 + 2; let y = x * 3; y }

A region with linear strings:

[source,ephapax]

region r: let s1 = String.new@r("hello, ") let s2 = String.new@r("world")

-- Borrow s1 to get length (does not consume)
let len = String.len(&s1)

-- Concatenation consumes both strings
let result = String.concat(s1, s2)

-- result is consumed by being returned
result

-- Region exits: any remaining allocations bulk-freed.

A linear binding (must consume):

[source,ephapax]

fn process(input: i32) -> i32 { let! z = copy(input) in z + 1 -- z is consumed exactly once }

More examples in examples/ and conformance/valid/.

== Quickstart

[source,bash]

Build all crates

just build

Build the Idris2 affine stage

just idris-build

Verify Coq proofs

just proofs

Run conformance tests + build + proofs

just golden

Compile an .eph file through Idris2 + WASM backend

just compile-affine input.eph affine output.wasm

Prerequisites:

• Rust 1.83+ with wasm32-unknown-unknown target
• Coq 8.18+ (for proof verification)
• Idris2 0.8.0 (needs IDRIS2_PREFIX pointing at a prefix with TTCs)
• https://just.systems/[just] (task runner)

== Project structure

[source]

ephapax/ ├── formal/ # Coq operational semantics + soundness │ ├── Syntax.v # AST and types │ ├── Typing.v # Region-linear typing rules │ ├── Semantics.v # Small-step substitution semantics │ └── PRESERVATION-HANDOFF.md # Per-case checklist for preservation ├── idris2/ # Idris2 frontend (parser + typechecker) │ ├── src/Ephapax/IR/ # AST, decode/encode, S-expression IR │ ├── src/Ephapax/Parse/ # Lexer, parser, stream, ZigBuffer FFI │ └── src/Ephapax/Affine/ # Type checker, emitter ├── src/formal/ # Idris2 region-linearity theorems │ └── Ephapax/Formal/ # noEscape, regionSafety, noGC, orthogonality ├── src/ # Rust implementation │ ├── ephapax-syntax/ # Core AST (Coq-proven shape) │ ├── ephapax-surface/ # Surface AST (data, match, patterns) │ ├── ephapax-desugar/ # Surface → Core │ ├── ephapax-typing/ # Dyadic type checker │ ├── ephapax-parser/ # Pest PEG parser │ ├── ephapax-lexer/ # logos tokenizer │ ├── ephapax-interp/ # Tree-walking interpreter │ ├── ephapax-wasm/ # WASM code generator │ ├── ephapax-runtime/ # no_std WASM runtime with regions │ ├── ephapax-cli/ # CLI │ ├── ephapax-lsp/ # Language server │ └── ephapax-analysis/ # Escape / free-vars / liveness analysis ├── ephapax-linear/ # Standalone dual-discipline checker ├── ffi/zig/ # Zig FFI implementation ├── conformance/ # Type-system conformance tests ├── spec/ # Language specification └── docs/ # Vision, ADRs, comparisons, reports

== Formal foundations

The type system is grounded in:

• Intuitionistic linear logic — resource-sensitive reasoning
• Separation logic — memory ownership and framing
• Tofte-Talpin region calculus — scoped allocation

Two complementary formalisations, both run on every push:

=== Coq (formal/)

Operational semantics with small-step reduction over a substitution- based calculus. Post-2026-05-26 the formalisation is layered:

• Legacy (formal/Semantics.v, formal/Typing.v) — the original pre-discovery judgment. Theorem preservation here is provably false (the counterexample at formal/Counterexample.v is 5 Qed lemmas proving it). The Admitted. is correct. Do not extend. Treat as archaeology — see link:STATUS.adoc[STATUS.adoc] for the pre-discovery PR list and the explicit do-not-do reasoning.

• Layer 1 — region capabilities (formal/TypingL1.v, formal/Semantics_L1.v). The new judgment is modality-indexed (has_type_l1 m : ...) and threads a capability environment R through compound rules. Judgment 100% (0 admits, 2 Qed); semantics carries 3 outer Admitted. markers covering 5 internal admit. cases — pre-existing L1 structural debt (multiset / list-perm bridge

  • L2 effect-typed TFun per PRESERVATION-DESIGN.md §5.1) and two parallel mirrors, not legacy patching. See PROOF-NEEDS.md §4 for the file:line classification.

• Layer 2 — structural modality (formal/Modality.v). Linear vs Affine as a K-free thin-poset decoration. linear_to_affine is Qed with zero axioms. Landed via PRs #176 + #177.

• Layer 3 — echo / residue (formal/Echo.v). 12 Qed lemmas covering the fiber calculus, degrade map, and the no-section-collapse-to-residue irreversibility theorem (mirrors the upstream Agda development at https://github.com/hyperpolymath/echo-types[`hyperpolymath/echo-types`]). Wiring into the L1 typing rules landed via slice 4 (2026-05-27): preservation_l3_region_active_echo, preservation_l3_drop_echo, and the preservation_l3 umbrella are all Qed (conditional on the region_shrink_preserves_typing_l1_gen_m L1 structural admit).

• Layer 4 — dyadic interaction. Phase A scaffold landed 2026-05-28: formal/L4.v defines ProgramMode (PModeLinear / PModeAffine / PModeBoundaryMix) and the program_mode_to_modality round-trip. No theorems by design (definitions only — labelling discipline, not a proof layer). Design in link:formal/PRESERVATION-DESIGN.md[formal/PRESERVATION-DESIGN.md §7].

Per-sublanguage proof debt with explicit do-not-do list lives in link:PROOF-NEEDS.md[PROOF-NEEDS.md]. The four-layer architecture rationale is in link:formal/PRESERVATION-DESIGN.md[formal/PRESERVATION-DESIGN.md]. The counterexample itself is link:formal/Counterexample.v[formal/Counterexample.v] (5 Qed).

[source,bash]

Verify Coq proofs

just proofs # via Makefile.coq

Or per-file:

cd formal && coqc -Q . Ephapax Semantics.v

=== Idris2 (idris2/src/Ephapax/ + src/formal/)

Two Idris2 developments:

• idris2/src/Ephapax/ — the actual frontend (parser, type checker, IR codec). As of 2026-05-20, the entire layer is under %default total (8 of 9 files) or %default covering (the recursive-descent parser, where fueling 30 mutually-recursive combinators is a deferred separate campaign). Zero assert_total, zero believe_me, zero assert_smaller introduced; 14 covering markers retained for documented Idris2 0.8.0 SCT limits.

• src/formal/ — region-linearity theorems on the type side: noEscapeTheorem, regionSafetyExtract, noGCExtract, orthogonalityLemma, plus splitLinearCoverage generalising the non-diminishment property (PR #85). All four headline theorems complete with zero unsafe patterns.

[source,bash]

Verify Idris2 frontend total/covering

just idris-build

Verify Idris2 region-linearity theorems

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

== Surface syntax (locked)

[source]

// Function declaration fn main() -> i32 { let x = 1 + 2; let y = x * 3; y }

// Linear binding let! z = copy(x) in z

// Region scope region r: let s = String.new@r("data") String.len(&s)

Grammar highlights:

• Functions: fn name(params) -> Ty { ... } or fn name(params) : Ty { ... }
• Affine bindings: let x = expr in expr
• Linear bindings: let! x = expr in expr
• Block expressions: { expr1; expr2; …; exprN } (final expr is the result)
• Newlines are statement separators (equivalent to ;)
• Comments: // and -- to end-of-line

Full grammar: spec/ephapax-spec.md. The v2 grammar work (modules, generics, effects, traits, comptime, contracts) lives on feat/v2-grammar-cross-module branches; see GitHub PRs for status.

== Build targets

[cols="1,2,1"] |=== | Target | Description | Status

| WebAssembly | wasm32-unknown-unknown | Primary

| Native | Via Cranelift | Secondary |===

== Component status

[cols="2,1,2"] |=== | Component | Status | Notes

| Core type-system design (affine + linear) | ✅ Complete | Locked in formal/Typing.v

| Lexer (logos) | ✅ Complete |

| Parser (chumsky + Pest) | ✅ Complete |

| Interpreter (tree-walking) | ✅ Complete | Environment-leak fix applied 2026-03-28

| REPL | ✅ Complete |

| CLI (ephapax-cli) | ✅ Complete |

| Idris2 frontend (S-expression IR) | ✅ Complete (%default total 8/9) | Parser is covering; total upgrade deferred

| Type checker (ephapax-typing) | 🚧 In progress |

| WASM code generation | 🚧 In progress | Lambda/app closure conversion landed; some pair/sum cases use i32 placeholder representation

| Conformance test suite | ✅ Complete | Pass/fail cases; covers dyadic discipline

| Coq no_leaks + region lemmas | ✅ Qed |

| Coq legacy preservation | 🛑 Admitted — provably false | Counterexample at formal/Counterexample.v (5 Qed). Not closable. Archaeology.

| Coq L1 (region capabilities) | ✅ Judgment 100%; 🟡 semantics 3 Admitted (5 inner admits) | 3 outer Admitted. markers cover 5 internal admit. cases — pre-existing L1 structural debt + parallel mirrors. Refresh PROOF-NEEDS.md §4 for the file:line breakdown.

| Coq L2 (modality) | ✅ Core landed (PRs #176 + #177); 0 axioms | linear_to_affine Qed. Integration debt absorbed by L1 admits above.

| Coq L3 (echo / residue calculus) | ✅ Wiring landed (slice 4, 2026-05-27); 0 admits in Echo.v | preservation_l3 (umbrella) + preservation_l3_region_active_echo + preservation_l3_drop_echo all Qed (conditional on region_shrink_preserves_typing_l1_gen_m L1 structural admit). 12 Qed in Echo.v for the underlying calculus.

| Coq L4 (dyadic interaction) | ✅ Phase A scaffold landed (formal/L4.v, 2026-05-28); definitions only | PModeLinear / PModeAffine / PModeBoundaryMix + program_mode_to_modality round-trip. No theorems by design; design in formal/PRESERVATION-DESIGN.md §7.

| Idris2 region-linearity theorems | ✅ Complete (zero unsafe) |

| LSP server | 🟡 Partial | Basic diagnostics; completion in progress

| Standard library | 🔲 Planned | ephapax-stdlib skeleton exists |===

== Documentation map

[cols="1,3"] |=== | Document | What it covers

| link:README.adoc[README] | You are here. Overview + quickstart.

| link:STATUS.adoc[STATUS.adoc] | Past / present / future map. Single page that answers "where are we?" Read this before any .v file or any PR comment dated before 2026-05-26.

| link:PROOF-NEEDS.md[PROOF-NEEDS.md] | Per-sublanguage proof debt audit. What's done (Qed), what's todo, what's banned (anti-pattern detector). Separated for ephapax-linear and ephapax-affine sublanguages.

| link:formal/PRESERVATION-DESIGN.md[formal/PRESERVATION-DESIGN.md] | Canonical four-layer design doctrine. Why the counterexample forced the redesign, the four orthogonal concerns, per-layer plans.

| link:formal/Counterexample.v[formal/Counterexample.v] | The 5 Qed lemmas that pin the soundness gap of the legacy judgment. Authoritative source of the gap; future proofs must coexist with it.

| link:CLAUDE.md[CLAUDE.md] | Agent guidance. Carries the 2026-05-27 owner directive, anti-pattern detector, escalation rule.

| link:EXPLAINME.adoc[EXPLAINME.adoc] | "Show me the receipts" — every claim in this README backed by a specific file, test, or proof.

| link:ROADMAP.adoc[ROADMAP.adoc] | Milestones (v0.1.0 → v1.0.0), per-version checklists, current open work. Note: any pre-2026-05-26 closure-plan content is superseded by STATUS.adoc + PRESERVATION-DESIGN.md.

| link:formal/PRESERVATION-HANDOFF.md[formal/PRESERVATION-HANDOFF.md] | Archaeology only — historical diagnostic record of the pre-counterexample closure attempts. Reads as a closure plan; isn't one. Useful only for understanding why the redesign happened.

| link:RUST-SPARK-STANCE.adoc[RUST-SPARK-STANCE.adoc] | Stance on Rust + SPARK interop and where Ephapax fits.

| link:TOPOLOGY.md[TOPOLOGY.md] | Module dependency graph + crate layering.

| link:TEST-NEEDS.md[TEST-NEEDS.md] | Outstanding test coverage gaps.

| link:CHANGELOG.md[CHANGELOG.md] | Per-release change log.

| link:docs/vision/EPHAPAX-VISION.adoc[docs/vision/EPHAPAX-VISION.adoc] | Design rationale — why dyadic, why regions, why WASM.

| link:docs/specs/DESIGN-DECISIONS.adoc[docs/specs/DESIGN-DECISIONS.adoc] | 17 architecture decision records with rationale.

| link:docs/specs/LANGUAGE-COMPARISON.adoc[docs/specs/LANGUAGE-COMPARISON.adoc] | Comparison against 10 other languages on the linear/affine axis.

| link:spec/[spec/] | Language specification + grammar EBNF.

| link:CONTRIBUTING.adoc[CONTRIBUTING.adoc] | Contribution guide.

| link:CODE_OF_CONDUCT.md[CODE_OF_CONDUCT.md] | Code of conduct.

| link:SECURITY.md[SECURITY.md] | Security policy. |===

== Quickstart files by audience

[cols="1,3"] |=== | Audience | Start here

| End user (just want to compile .eph files) | link:QUICKSTART-USER.adoc[QUICKSTART-USER.adoc]

| Developer (extending the compiler / language) | link:QUICKSTART-DEV.adoc[QUICKSTART-DEV.adoc]

| Maintainer (release / governance) | link:QUICKSTART-MAINTAINER.adoc[QUICKSTART-MAINTAINER.adoc]

| Outside observer (what is this even?) | Read this README → EXPLAINME.adoc → docs/vision/EPHAPAX-VISION.adoc |===

== Seam analysis

Key interfaces where correctness and stability matter:

• Idris2 → S-expression IR (Ephapax.IR.Decode encoding/decoding)
• Zig FFI token buffer → Idris2 parser stream (Ephapax.Parse.ZigBuffer)
• S-expression IR → Rust/WASM backend (ephapax-ir and ephapax-wasm)
• Surface AST → Core AST (ephapax-desugar — proofs target core only)

The proven library is a dependency so string-handling paths over the IR boundary harden over time (JSON-style escaping, etc.).

== Related work

• https://www.rust-lang.org/[Rust] — ownership and borrowing
• https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html[Linear Haskell] — linear types in GHC
• https://www.cl.cam.ac.uk/research/mvg/tom/mlkit/[MLKit] — region-based memory management
• https://cyclone.thelanguage.org/[Cyclone] — safe C dialect with regions
• https://github.com/granule-project/granule[Granule] — graded modal types with linear/affine ledger
• Tofte-Talpin 1997 — region calculus original paper

docs/specs/LANGUAGE-COMPARISON.adoc has a feature-by-feature comparison against ten of these.

== Contributing

Contributions welcome. Please see:

• link:CONTRIBUTING.adoc[CONTRIBUTING.adoc] — getting started
• link:CODE_OF_CONDUCT.md[CODE_OF_CONDUCT.md] — community standards

The highest-leverage open work, in priority order:

1. Phase 3b Stages 2 → 4 (issues #240/#241/#242) — ELam annotation extension, CPS-form substitution, then compound non-linear values + unconditional preservation_l2. The path forward; see formal/PRESERVATION-DESIGN.md §12.15 and formal/PHASE-D-REDESIGN.md.
2. Progress for L1 — state and prove progress_l1 plus the L1 canonical_* lemmas (currently legacy-only at Semantics.v:603-630). Combined with the conditional preservation_l1, this gives conventional type-soundness in conditional form.
3. Fuel-refactor Parse/Parser.idr from %default covering to %default total. Substantial — ~30 mutually-recursive combinators threaded through a Stream record.
4. Type-checker completion (ephapax-typing) and WASM codegen for lambda/app (ephapax-wasm).
5. Native backend via Cranelift (v0.2.0).

[NOTE]

Closing the legacy Theorem preservation in formal/Semantics.v is NOT a valid contribution. That theorem is provably false (sealed by formal/Counterexample.v); its Admitted. is correct and durable per owner directive 2026-05-27. formal/PRESERVATION-HANDOFF.md is archaeology kept for context. The path forward is the per-layer preservation theorems (preservation_l1, preservation_l2, preservation_l3) on the redesigned judgment in formal/Semantics_L1.v. See formal/PRESERVATION-DESIGN.md §12 and PROOF-NEEDS.md §3.

== Licence

PMPL-1.0-or-later — see link:LICENSES/PMPL-1.0-or-later.txt[PMPL-1.0-or-later.txt].

MPL-2.0 fallback available — see link:LICENSES/MPL-2.0.txt[MPL-2.0.txt].

== Author

Jonathan D.A. Jewell

---

"Once for all" — every resource used exactly once.