|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
| 3 | +SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
| 5 | + |
| 6 | +# What Is This? |
| 7 | + |
| 8 | +Ephapaxiser analyses code for resource handles, inserts |
| 9 | +[Ephapax](https://github.com/hyperpolymath) linear type wrappers around |
| 10 | +them, and enforces **exactly-once usage** at compile time. The result: |
| 11 | +resource leaks, double-frees, and use-after-free bugs become |
| 12 | +*impossible* in wrapped code. |
| 13 | + |
| 14 | +Ephapax (from Greek *ἐφάπαξ* — "once for all") is hyperpolymath’s linear |
| 15 | +type language where every value must be used exactly once. Ephapaxiser |
| 16 | +brings those guarantees to existing Rust, C, and Zig codebases without |
| 17 | +requiring the developer to learn Ephapax itself. |
| 18 | + |
| 19 | +# How It Works |
| 20 | + |
| 21 | +Describe your resources in an `ephapaxiser.toml` manifest. Ephapaxiser |
| 22 | +then: |
| 23 | + |
| 24 | +1. **Analyses** your source code for resource acquisition and release |
| 25 | + patterns (file handles, sockets, database connections, GPU buffers, |
| 26 | + crypto keys) |
| 27 | + |
| 28 | +2. **Generates** Ephapax linear type wrappers that structurally enforce |
| 29 | + single-use semantics on each resource |
| 30 | + |
| 31 | +3. **Proves** linearity via the Idris2 ABI layer — dependent types |
| 32 | + guarantee that every resource is consumed exactly once |
| 33 | + |
| 34 | +4. **Bridges** proofs into executable code via the Zig FFI — zero |
| 35 | + runtime overhead, proofs are erased at compile time |
| 36 | + |
| 37 | +5. **Emits** target-language wrapper code that the developer can drop |
| 38 | + in place |
| 39 | + |
| 40 | +If a resource is used after consumption, leaked, or double-freed, you |
| 41 | +get a **compile-time error** — not a runtime crash. |
| 42 | + |
| 43 | +# Key Value |
| 44 | + |
| 45 | +- **Resource leaks become compile errors** — files always closed, keys |
| 46 | + always zeroised, connections always released |
| 47 | + |
| 48 | +- **Use-after-free impossible** — linear types structurally prevent it |
| 49 | + |
| 50 | +- **Double-free impossible** — consumption proof means the resource |
| 51 | + cannot be freed twice |
| 52 | + |
| 53 | +- **Crypto key safety** — keys used exactly once then destroyed (perfect |
| 54 | + forward secrecy enforcement) |
| 55 | + |
| 56 | +- **GPU buffer lifecycle** — allocate, use, release: compile-time |
| 57 | + guarantee the buffer is not accessed after release |
| 58 | + |
| 59 | +- **Database connection pooling** — connections checked out exactly |
| 60 | + once, always returned |
| 61 | + |
| 62 | +- **Session token safety** — tokens consumed on use, preventing replay |
| 63 | + |
| 64 | +- **Gradual adoption** — wrap one resource type at a time in existing |
| 65 | + code |
| 66 | + |
| 67 | +# Architecture |
| 68 | + |
| 69 | +Ephapaxiser follows the hyperpolymath [-iser |
| 70 | +pattern](https://github.com/hyperpolymath/iseriser): |
| 71 | + |
| 72 | + ephapaxiser.toml manifest |
| 73 | + │ |
| 74 | + ▼ |
| 75 | + Resource Analysis (Rust CLI) |
| 76 | + ── identify acquire/release patterns |
| 77 | + │ |
| 78 | + ▼ |
| 79 | + Idris2 ABI (src/interface/abi/) |
| 80 | + ── LinearResource, UsageCount, ConsumeProof |
| 81 | + ── dependent types PROVE linearity invariants |
| 82 | + │ |
| 83 | + ▼ |
| 84 | + Zig FFI (src/interface/ffi/) |
| 85 | + ── C-ABI bridge, zero overhead |
| 86 | + │ |
| 87 | + ▼ |
| 88 | + Ephapax Codegen (src/codegen/) |
| 89 | + ── emit target-language wrappers |
| 90 | + ── Rust / C / Zig output |
| 91 | + |
| 92 | +## Idris2 ABI Layer |
| 93 | + |
| 94 | +The Idris2 ABI layer (`src/interface/abi/`) is the formal specification: |
| 95 | + |
| 96 | +- `Types.idr` — `LinearResource`, `UsageCount`, `ResourceLifecycle`, |
| 97 | + `ConsumeProof` — types that express "this resource is used exactly |
| 98 | + once" |
| 99 | + |
| 100 | +- `Layout.idr` — memory layout for resource tracking structs, with |
| 101 | + padding and alignment proofs |
| 102 | + |
| 103 | +- `Foreign.idr` — FFI declarations for resource analysis and linearity |
| 104 | + enforcement operations |
| 105 | + |
| 106 | +## Idris2 Wins Rule |
| 107 | + |
| 108 | +> [!IMPORTANT] |
| 109 | +> **When Idris2 proofs conflict with Ephapax linear types, Idris2 always |
| 110 | +> wins.** |
| 111 | +> |
| 112 | +> This is a standing project rule across all hyperpolymath repositories. |
| 113 | +> The formally verified Idris2 proofs are the source of truth. If an |
| 114 | +> Ephapax wrapper would violate a proven Idris2 invariant, the wrapper |
| 115 | +> must be adjusted — never the proof. |
| 116 | +
|
| 117 | +## Zig FFI Layer |
| 118 | + |
| 119 | +The Zig FFI layer (`src/interface/ffi/`) implements the C-ABI bridge |
| 120 | +declared by the Idris2 ABI. It provides: |
| 121 | + |
| 122 | +- Resource handle lifecycle (init/free with linearity tracking) |
| 123 | + |
| 124 | +- Resource consumption operations (use-once semantics enforced) |
| 125 | + |
| 126 | +- Thread-local error reporting |
| 127 | + |
| 128 | +- Cross-platform compilation (Linux, macOS, Windows, WASM) |
| 129 | + |
| 130 | +# Use Cases |
| 131 | + |
| 132 | +- **File handle management** — ensure every opened file is closed |
| 133 | + exactly once |
| 134 | + |
| 135 | +- **Database connections** — prevent connection leaks in pooled |
| 136 | + environments |
| 137 | + |
| 138 | +- **GPU buffer lifecycle** — allocate, compute, release — no dangling |
| 139 | + buffers |
| 140 | + |
| 141 | +- **Session tokens** — single-use tokens that cannot be replayed |
| 142 | + |
| 143 | +- **Crypto key material** — keys consumed on use, then securely zeroised |
| 144 | + |
| 145 | +- **Network sockets** — no forgotten open connections |
| 146 | + |
| 147 | +# Status |
| 148 | + |
| 149 | +**Codebase in progress.** Architecture defined, Rust CLI scaffolded, |
| 150 | +Idris2 ABI and Zig FFI stubs in place. Resource analysis and Ephapax |
| 151 | +codegen are the active development frontier. |
| 152 | + |
| 153 | +See [ROADMAP](ROADMAP.adoc) for the full phase plan. |
| 154 | + |
| 155 | +# Quick Start |
| 156 | + |
| 157 | +```bash |
| 158 | +# Initialise a manifest in your project |
| 159 | +ephapaxiser init --path . |
| 160 | + |
| 161 | +# Edit ephapaxiser.toml to describe your resources |
| 162 | +# Then generate wrappers |
| 163 | +ephapaxiser generate --manifest ephapaxiser.toml --output generated/ |
| 164 | + |
| 165 | +# Validate your manifest |
| 166 | +ephapaxiser validate --manifest ephapaxiser.toml |
| 167 | +``` |
| 168 | + |
| 169 | +# Build |
| 170 | + |
| 171 | +```bash |
| 172 | +cargo build --release |
| 173 | +cargo test |
| 174 | +``` |
| 175 | + |
| 176 | +# License |
| 177 | + |
| 178 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
0 commit comments