- Claim: Dyadic Type System (L2)
- Claim: Two-Layer AST (Surface + Core)
- Claim: Pattern Matching Desugars to Binary Sums
- Claim: Dual Substructural Grammars
- Claim: Region-Based Memory
- Claim: Sibling-safe region capabilities (L1)
- Claim: Irreversibility residue is first-class (L3, wired)
- Claim: Dyadic mode is project-level only (L4)
- Technology Choices
- Dogfooded Across The Account
- File Map
- Claim: Mechanically Proved Soundness
- Test Evidence
- Design Documents
- Questions?
The README makes claims. This file backs them up — every assertion in README.adoc is tied to a specific file, test, or proof obligation.
A dyadic linear+affine type system for compile-time WebAssembly memory safety. Resources are tracked through the type system so the compiler can guarantee — without a garbage collector — that no value is used after being freed, no resource is leaked, and region-scoped allocations are deallocated in bulk at scope exit.
The dyad is L2 in the four-layer architecture (see
README.adoc#the-four-layers and docs/vision/EPHAPAX-VISION.adoc).
This section presents the Rust-side evidence for the L2 discipline;
L1 / L3 / L4 evidence follows below.
Evidence: The type checker (src/ephapax-typing/src/lib.rs) tracks
BindingForm per context entry:
-
BindingForm::Let— affine discipline,demands_consumption()returnsfalse -
BindingForm::LetBang— linear discipline,demands_consumption()returnstrue -
BindingForm::Param— follows type linearity
Tests test_let_allows_unconsumed_linear and test_let_bang_rejects_unconsumed
verify the distinction. test_let_bang_rejects_unconsumed_unrestricted proves
that let! enforces exactly-once even for unrestricted types like I32.
The Coq-side L2 evidence is linear_to_affine : Linear ≤ Affine (Qed,
zero axioms) in formal/Modality.v.
Evidence: Two separate crates:
-
src/ephapax-surface/— Surface AST withDataDecl,Match,Construct,Pattern,SurfaceTy::Named -
src/ephapax-syntax/— Core AST with binary sums,case/inl/inr -
src/ephapax-desugar/— Transforms surface to core
The Coq formal proofs (formal/) reason about the core AST only. New surface
features (pattern matching, named constructors) never invalidate the proofs.
Test integration_desugar_typecheck_no_parser in ephapax-desugar verifies the
full pipeline: surface AST → desugar → core AST → type check.
Evidence: src/ephapax-desugar/src/lib.rs implements:
-
data Option(a) = None | Some(a)→ type() + a(right-nested binary sums) -
None→inl(()),Some(x)→inr(x)(constructor injection chains) -
match … of→ nestedcase/inl/inr(case tree generation)
Tests: desugar_option_i32, desugar_color_green, desugar_color_blue,
desugar_match_color (verifies nested case for 3-variant match),
desugar_non_exhaustive_match (rejects incomplete patterns).
Evidence: ephapax-linear/ contains two EBNF grammar specifications:
-
grammar/linear.ebnf— no weakening, no contraction, branch agreement required -
grammar/affine.ebnf— weakening OK, no contraction, branches may disagree
LinearChecker and AffineChecker in Rust enforce these grammars. 14 tests
demonstrate where they diverge on identical programs (e.g.
linear_rejects_unconsumed_let_bang vs affine_allows_unconsumed_let).
Evidence: check_region in src/ephapax-typing/src/lib.rs enforces:
-
NoRegionInType — return type must not reference the region (no escape)
-
Consumption at region exit — only bindings that
demands_consumption()must be consumed; affine bindings are implicitly dropped
Test test_region_non_escaping verifies escape detection.
Test test_region_string_allocation verifies in-region allocation.
Evidence: Region capabilities are threaded as input/output environments through every compound typing rule. A sibling cannot reference a region a previous sibling has exited — this is the soundness invariant the legacy judgment was missing.
-
Counterexample at
formal/Counterexample.v(all five lemmasQed) demonstrates the soundness gap the threading fixes. -
The new
has_type_l1judgment lives informal/TypingL1.vand carries the R-threading directly. Step relation atformal/Semantics_L1.v. -
Design rationale at
formal/PRESERVATION-DESIGN.md §3-§4. -
Status: judgment landed;
Semantics_L1.vcarries 3 outerAdmitted.markers covering 5 inneradmit.cases — pre-existing L1 structural debt + parallel mirrors (file:line breakdown inPROOF-NEEDS.md §4).
Evidence: Operations that erase information (region exit, drop) produce typed residue witnesses, following the echo-types formulation. Linear mode requires the residue to be observed; Affine mode permits silent lowering.
-
Upstream theory at
~/developer/repos/echo-types/proofs/agda/EchoLinear.agda(lines 30–101), already mechanised. -
Local mirror at
formal/Echo.v— the L3 calculus is mechanised here (modes,LEcho,weaken,degrade_mode, allQed). -
Forward-looking design at
formal/PRESERVATION-DESIGN.md §6. -
Status: wiring landed (slice 4, 2026-05-27).
preservation_l3_region_active_echo,preservation_l3_drop_echo, and thepreservation_l3umbrella inSemantics_L1.vare all Qed, each conditional on theregion_shrink_preserves_typing_l1_gen_mL1 structural admit. Remaining L3 work is unconditionalpreservation_l3(Phase 3b Stage 2).
Evidence: L4 is a labelling discipline, not a proof layer.
formal/L4.v carries ProgramMode (three-constructor enum) and
program_mode_to_modality (total mapping to L2’s modality). No
theorems, no admits, no axioms — by design.
-
Companion design note:
formal/L4-DYADIC.md. -
Canonical design source:
formal/PRESERVATION-DESIGN.md §7. -
Surface syntax for the L4 declaration (
![ephapax_linear]/![ephapax_affine]/#![module_boundary_mix(…)]) is not yet wired into the parser or borrow checker; the mechanical scaffold is a citable type for downstream tools (Idris2 ABI, Rust borrow checker, surface parser).
| Technology | Why |
|---|---|
Rust |
Compiler implementation language |
Pest (PEG) |
Parser generator — surface + core grammars |
WASM |
Compilation target — portable, sandboxed, near-native |
Coq |
Formal proofs of core calculus soundness |
Idris 2 |
ABI definitions with dependent type proofs |
Zig |
FFI implementation (C-compatible, cross-compilation) |
| Technology / Pattern | Role in Ephapax | Also Used In |
|---|---|---|
Dyadic type discipline (let / let!) |
Core language design — affine ( |
gossamer ( |
Coq formal proofs |
|
ephapax-pipewire proving ground (PipeWire filter-node linearity); proven repo ( |
Idris2 ABI + Zig FFI standard |
|
gossamer (HandleLinearity.idr, IPCIntegrity.idr), burble (src/Burble/ABI/), verisimdb, typed-wasm, standards monorepo |
Two-layer AST (Surface / Core) |
|
AffineScript (surface/core split in the OCaml compiler); 007 (dual-AST safety design pattern) |
Pattern matching desugared to binary sums |
|
Tangle language (braid-word case trees); k9-rs (sum-type dispatch) |
| Path | What’s There |
|---|---|
|
Core AST (minimal, Coq-proven) |
|
Surface AST (data, match, patterns) |
|
Surface → Core transformation |
|
Dyadic type checker (let/let!/BindingForm) |
|
PEG parser (core + surface module) |
|
WASM code generator with closure conversion |
|
no_std WASM runtime with regions |
|
Tree-walking interpreter |
|
Command-line interface |
|
Language server (completion, diagnostics) |
|
Escape analysis, free vars, liveness |
|
Standard library (Prelude, Region, IO) |
|
Dual discipline checker (linear + affine grammars) |
|
Coq proofs (Typing.v, progress/preservation) |
|
Idris 2 ABI definitions |
|
Language specification (v2 grammar, specs) |
|
Design decisions, language comparison |
|
Example programs (pattern_matching.eph) |
|
Conformance test suite (valid/invalid programs) |
Evidence: Two complementary formalisations, both run on every push.
|
Important
|
Post-counterexample 2026-05-26 — read this before any older proof claim
The legacy preservation theorem in The post-discovery work is the four-layer principled redesign
documented in |
The Coq formalisation is now layered. Each layer has its own judgment, its own invariants, and its own per-layer preservation theorem.
| Component | Status | Where |
|---|---|---|
Counterexample regression (5 Qed) |
✅ Pinned |
|
L1 judgment ( |
✅ 100% (2 Qed, 0 admits) |
|
L1 semantics |
🟡 37 Qed, 3 Admitted (5 inner admits — pre-existing L1 structural debt + parallel mirrors) |
|
L2 modality ( |
✅ Core landed (1 Qed, 0 axioms) |
|
L3 echo / residue calculus |
✅ Calculus 12 Qed + wiring landed (slice 4, 2026-05-27) |
|
L4 dyadic interaction |
✅ Phase A scaffold landed ( |
|
Legacy |
🛑 Provably false (Admitted) |
Pinned by |
What’s done = Modality.linear_to_affine (Linear ⇒ Affine weakening,
zero axioms), the L1 judgment, L3 fiber + degrade calculus, L3
wiring into the L1 step rules (slice 4 — preservation_l3 umbrella
Qed conditional on the L1 structural admit), L4 Phase A scaffold
(definitions only), and the counterexample regression witness.
What’s todo = close the 3 Semantics_L1 outer Admitteds (pre-existing
L1 structural debt: multiset/list-perm bridge + L2-effect-typed
TFun + lambda-rigidity at preservation_l1), then state
unconditional preservation_l3 (Phase 3b Stage 2). What’s banned =
closing the legacy theorem, adding new Axiom declarations to
discharge L1/L2 gaps, conflating ephapax-affine (this repo’s
sublanguage) with AffineScript (a separate language at
hyperpolymath/affinescript). Full per-sublanguage breakdown in
PROOF-NEEDS.md.
Two Idris2 developments:
Frontend (parser / typechecker / IR codec) —
idris2/src/Ephapax/ is the actual Idris2-side of the two-phase
pipeline. As of 2026-05-20, all 9 files compile under %default
total (8 files) or %default covering (1 file, the recursive-
descent parser).
| Module | Default | Notes |
|---|---|---|
|
|
Fueled mutual recursion where Idris2 SCT couldn’t trace structural
decrease through |
|
|
|
|
|
LL(k) recursive descent through ~30 mutually-recursive Stream- indexed parser combinators. Fueling all of them is a substantial separate refactor, deferred to a later campaign. |
Zero believe_me, zero assert_total, zero assert_smaller in
the entire frontend. The campaign that achieved this (PRs #89, #90,
#91, #93, #94, #96, #97, #99, #100, all merged 2026-05-20) is
documented in the project memory.
Region-linearity theorems — src/formal/ proves structural
properties of the region-linear calculus:
| Theorem | Where |
|---|---|
|
|
|
|
|
|
|
|
|
|
All five with zero believe_me, zero postulates, under %default
total.
357 tests across 17 active workspace crates + tests/fuzz, 0
failures (per cargo test --all-targets; see TEST-NEEDS.md for
the per-crate breakdown). Key test categories:
-
Type checker dyadic tests:
letvslet!semantics, branch agreement, region exit (ephapax-typing) -
Desugar tests: constructor encoding, match desugaring, exhaustiveness (
ephapax-desugar) -
Parser tests: surface syntax (data, match, constructors, named types) (
ephapax-parser) -
Discipline tests: linear vs affine checker divergence (
ephapax-linear) -
Integration tests: parse → desugar → typecheck end-to-end
-
Conformance tests:
conformance/valid/programs must type-check,conformance/invalid/programs must be rejected
-
spec/ephapax-v2-grammar.ebnf— complete v2 grammar (modules, generics, effects, traits, comptime, contracts) — work in flight onfeat/v2-grammar-*branches -
docs/specs/DESIGN-DECISIONS.adoc— 17 ADRs with rationale -
docs/specs/LANGUAGE-COMPARISON.adoc— comparison against 10 languages -
docs/vision/EPHAPAX-VISION.adoc— design rationale, why dyadic
regions + WASM -
formal/PRESERVATION-HANDOFF.md— archaeology only: per-case checklist from the pre-2026-05-26 legacy-judgment closure plan, retained for historical context. The legacypreservationis provably false; the path forward is the per-layer theorems documented informal/PRESERVATION-DESIGN.md. -
PROOF-NEEDS.md— outstanding proof obligations + leverage