|
| 1 | +// SPDX-License-Identifier: MPL-2.0 OR CC-BY-SA-4.0 |
| 2 | +// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +// Authoring standard: hyperpolymath/standards docs/AFFIRMATION-STANDARD.adoc |
| 5 | += AFFIRMATION — ephapax, as of 2026-06-16 |
| 6 | +:toc: macro |
| 7 | +:toclevels: 2 |
| 8 | + |
| 9 | +_the No-Bullshit file: what we affirm was true and checkable at this moment_ |
| 10 | + |
| 11 | +[NOTE] |
| 12 | +==== |
| 13 | +*Genre.* An *affirmation* is a solemn declaration of the truth of a statement, |
| 14 | +made by someone who _declines to swear an oath_. That is exactly what this is: |
| 15 | +our truth-as-best-believed at a stamped instant — binding on our honesty, not a |
| 16 | +claim of infallibility. It is not the README and not the EXPLAINME: |
| 17 | +
|
| 18 | +[cols="1,3,2",options="header"] |
| 19 | +|=== |
| 20 | +| File | Answers | Tense |
| 21 | +| `README` | _Where is this going, and why?_ — state of thinking, steering, intent | future / aspirational |
| 22 | +| `EXPLAINME` | _How is it built, and what's the evidence?_ — engineering underpinnings | descriptive / mechanism |
| 23 | +| *`AFFIRMATION`* (this file) | _What can we honestly affirm was *true and checkable* at a stamped moment?_ | a frozen instant, falsifiable |
| 24 | +|=== |
| 25 | +
|
| 26 | +It is deliberately small, dated, and signed, so a reader can hold us to exactly |
| 27 | +what we affirmed, when we affirmed it. |
| 28 | +==== |
| 29 | + |
| 30 | +toc::[] |
| 31 | + |
| 32 | +== What this is, and how it is designed to work |
| 33 | + |
| 34 | +*What it is.* A short, dated, jointly-signed snapshot of what we can _honestly |
| 35 | +and verifiably_ claim about this repo at one exact commit. Nothing here is |
| 36 | +marketing and nothing is a promise about the future — both of those live in the |
| 37 | +README. This file is the receipt. |
| 38 | + |
| 39 | +*How it is designed to work.* Three moving parts make it trustworthy: |
| 40 | + |
| 41 | +. *Ground truth, not memory.* Every claim below was produced by _running the |
| 42 | + tool in the session that wrote this file_ — the Coq build, the Rust test |
| 43 | + suite, the WASM validator, the Idris build. Status docs (`PROOF-NEEDS.md`, |
| 44 | + `TEST-NEEDS.md`), memory, and prior sessions are *not* evidence; where the |
| 45 | + live run disagreed with them, the run wins and we flag it. |
| 46 | +. *A frozen anchor.* The file names the exact commit SHA, branch, UTC timestamp, |
| 47 | + and toolchain (see <<Verifiable anchor>>), so "true" always means "true _at |
| 48 | + this point_". Move the SHA and the file becomes a draft until re-run. |
| 49 | +. *A real signature.* It is landed by a *signed git commit*; that signature over |
| 50 | + this content at the anchored SHA is what makes the affirmation tamper-evident |
| 51 | + and attributable — not the prose alone. |
| 52 | + |
| 53 | +*We are fallible.* We can be wrong, stale, or simply mistaken about our own |
| 54 | +work. This file is our best honest belief, not a proof of its own correctness. |
| 55 | +Treat it as a falsifiable claim, not gospel. |
| 56 | + |
| 57 | +== The epistemic contract (read this before you trust _or_ attack) |
| 58 | + |
| 59 | +This document records our *best joint belief* at the timestamp below. It is |
| 60 | +*not a guarantee of correctness.* We may be wrong. We may have missed something |
| 61 | +— a hole, a stale doc, a proof that checks a calculus we then fail to match in |
| 62 | +the implementation. |
| 63 | + |
| 64 | +*No intentional overclaim.* That is the only guarantee here: we have not |
| 65 | +_knowingly_ inflated anything. Where something is tested-but-not-proved, we say |
| 66 | +so. Where a proof covers an idealised core and _not_ the production code, we say |
| 67 | +so. Where something is refuted, vacuous, or does not even build right now, we |
| 68 | +say so. An honest claim that turns out false is an error to fix — not a lie. |
| 69 | + |
| 70 | +*Standing invitation to refute.* You are _invited_ to bulldoze any claim here. |
| 71 | +We want that. The fair form of the attack is: |
| 72 | + |
| 73 | +. Read this file at the stamped commit. |
| 74 | +. Reproduce (or fail to reproduce) the checks in <<reproduce,Reproduce it yourself>>. |
| 75 | +. _Then_ tell us where the discrepancy is, against the artefact as it stood at |
| 76 | + this moment — so we can either justify it or concede it on the record. |
| 77 | + |
| 78 | +An attack that skips steps 1–2 is attacking a strawman of a different date. |
| 79 | + |
| 80 | +*No fights before the facts are cleared up.* We are not interested in a dispute |
| 81 | +over a claim until the discrepancy has actually been checked against the |
| 82 | +artefact at this commit and we have had the chance to either justify it or |
| 83 | +concede it on the record. Good faith both ways: bring a reproducible |
| 84 | +discrepancy and we will fix the claim, the doc, or the code — promptly and |
| 85 | +without defensiveness. The goal is a corrected record, not a won argument. |
| 86 | + |
| 87 | +== Verifiable anchor |
| 88 | + |
| 89 | +[cols="1,3"] |
| 90 | +|=== |
| 91 | +| *Repo* | `hyperpolymath/ephapax` (the Rust + Coq + Idris2 language, `.eph`, `Cargo.toml` at root — *not* `hyperpolymath/affinescript`, and the internal `ephapax-affine` sublanguage is *not* AffineScript) |
| 92 | +| *Branch* | `main` |
| 93 | +| *Commit (HEAD)* | `2c2df186dea3907a7f7eea1376216f869e04be1b` (the `//`→`--` Idris-header build fix; this affirmation is committed as its child, so the SHA here is this file's parent) |
| 94 | +| *Permalink* | https://github.com/hyperpolymath/ephapax/tree/2c2df186dea3907a7f7eea1376216f869e04be1b |
| 95 | +| *Verified (UTC)* | 2026-06-16, 11:52Z–12:07Z (this session). Coq + Rust + WASM first ran cold at 11:52; after the Idris fix all four were re-confirmed green *at this commit* at 12:07:04Z–12:07:09Z (warm caches make the re-confirmation fast — a cold reproduce rebuilds from scratch). |
| 96 | +| *Working-tree delta at verification* | one *untracked* directory `docs/reports/perf/` (not build/test/proof relevant), plus this file being added. The results below are this commit + that delta. |
| 97 | +| *Toolchain* | Coq 8.18.0 · Idris2 0.8.0 · Rust (cargo/rustc) 1.95.0 · wasm-tools 1.249.0 · just 1.50.0 |
| 98 | +|=== |
| 99 | + |
| 100 | +[IMPORTANT] |
| 101 | +If you are reading this at a _later_ commit, the claims may have drifted. |
| 102 | +Re-run <<reproduce>> and write a fresh affirmation; do not trust a stale one. |
| 103 | + |
| 104 | +== Companion documents and repo metadata (cross-check) |
| 105 | + |
| 106 | +Read this affirmation against the repo's own public claims. Where they drift |
| 107 | +from what we verified, we say so here rather than leave the reader to find out. |
| 108 | + |
| 109 | +* *`README.adoc`* — present (sells the language; the aspirational view). |
| 110 | +* *`EXPLAINME.adoc`* — present (the engineering-evidence document). The estate |
| 111 | + README / EXPLAINME / AFFIRMATION trio is therefore complete for this repo. |
| 112 | +* *GitHub repo description* — _"Dyadic linear+affine type system for |
| 113 | + compile-time WASM memory safety — no use-after-free, no leaks, region-based |
| 114 | + allocation. *Mechanically proved in Coq and Idris2.*"_ Honest caveats on the |
| 115 | + emphasised phrase: |
| 116 | +** *Coq:* the development *does* build green this session (5 `Admitted.` |
| 117 | + remain — 4 open L1 region obligations + 1 deliberately-false legacy |
| 118 | + theorem; see below). The memory-safety theorems proved are about the |
| 119 | + *calculus*, not the Rust implementation. |
| 120 | +** *Idris2:* **builds green this session** — both `src/abi/ephapax-abi.ipkg` |
| 121 | + and `src/formal/ephapax-formal.ipkg` (`idris2 --build`, exit 0), restored at |
| 122 | + the anchor commit by a `//`→`--` header fix. So both halves of "mechanically |
| 123 | + proved in Coq and Idris2" now build. The Idris ABI register it carries is |
| 124 | + *partial*, though: E2a/E3-static are discharged, but E5 (wasm-compilation |
| 125 | + correctness) / E6 (IR lowering) are unformalised and E4 is a vacuous wrapper |
| 126 | + (see <<outstanding>>). |
| 127 | +* *GitHub topics* — `coq`, `memory-safety`, `type-system`, `affine-types`, |
| 128 | + *`agda`*, `compiler`, `formal-verification`, `idris2`, `programming-language`. |
| 129 | + Cross-check: **`agda` is drift** — ephapax's proofs are *Coq + Idris2*; Agda |
| 130 | + belongs to the upstream foundation repos (echo-types / epistemic-types), not |
| 131 | + to ephapax itself. `formal-verification` is *earned for the Coq core* (built |
| 132 | + green here), qualified by the open admits and the broken Idris build. |
| 133 | + |
| 134 | +== The honest state (one breath) |
| 135 | + |
| 136 | +*ephapax is a dyadic substructural-typed research language (a linear core and an |
| 137 | +affine companion sublanguage) compiling to WebAssembly, with a genuinely |
| 138 | +machine-checked Coq metatheory core — yet pre-1.0: the Rust implementation is |
| 139 | +not proved to match that calculus, the L1 region layer carries 4 open admits, |
| 140 | +the Idris2 proof side does not currently build, and the module system (its |
| 141 | +keystone) is not wired, so the stdlib and coprocessor API cannot be consumed and |
| 142 | +no real multi-module program can be written yet.* |
| 143 | + |
| 144 | +=== What is solid (and how we checked) |
| 145 | + |
| 146 | +* *The Coq metatheory builds green, this session.* `just proofs` |
| 147 | + (`coq_makefile` + `make`, Coq 8.18.0) exits *0*. Machine-checked (`Qed`): |
| 148 | + L2 modality `linear_to_affine` (zero axioms); the L3 echo preservation |
| 149 | + capstone (`preservation_l3`, conditional on one L1 admit); the L1 support |
| 150 | + lemmas; and the regression witnesses in `Counterexample{,_L2,_L2_nested}.v`. |
| 151 | +* *The Idris2 ABI + formal proofs typecheck, this session.* `idris2 --build` |
| 152 | + (Idris2 0.8.0) exits *0* for both `src/formal/ephapax-formal.ipkg` |
| 153 | + (`Region` / `Qualifier` / `RegionLinear`) and `src/abi/ephapax-abi.ipkg` |
| 154 | + (`Types` / `Invariants` / `Foreign`) — so the Idris-side proofs |
| 155 | + (`noEscapeTheorem`, `splitLinearCoverage`, `compileResultRoundTrip`, |
| 156 | + `outlivesTransitive`) machine-check here. (One harmless deprecation warning |
| 157 | + about ipkg version-number format; build is green.) |
| 158 | +* *The Rust pipeline builds and its tests pass.* `cargo test --workspace` |
| 159 | + (`CARGO_INCREMENTAL=0`, Rust 1.95.0) exits *0*: *489 passed, 0 failed, |
| 160 | + 0 ignored* across the workspace. |
| 161 | +* *Every WASM module ephapax emits is structurally valid.* `just validate-wasm` |
| 162 | + (wasm-tools 1.249.0) exits *0* — every fixture in `tests/v2-grammar/fixtures/` |
| 163 | + plus the `hypatia-port/bridge.eph` integration target passes |
| 164 | + `wasm-tools validate`. |
| 165 | + |
| 166 | +=== The honest nuance you must not lose |
| 167 | + |
| 168 | +The Coq proofs establish properties of an *idealised four-layer calculus* |
| 169 | +(L1 region capabilities / L2 modality / L3 echo residue / L4 dyadic mode). They |
| 170 | +do *not* prove that the Rust implementation (`ephapax-linear/src/{linear,affine}.rs`, |
| 171 | +the codegen) _refines_ that calculus. "Proved core" + "tested implementation" is |
| 172 | +exactly that — two things, with an unverified bridge between them. Anyone |
| 173 | +claiming "ephapax is proven memory-safe" full-stop is overclaiming. |
| 174 | + |
| 175 | +=== Known-incomplete but honestly fenced (loud failure, never silent miscompile) |
| 176 | + |
| 177 | +* *Algebraic effects (`perform`/`handle`)* are unimplemented in both the |
| 178 | + interpreter and the wasm backend: they emit a WASM `unreachable` / a runtime |
| 179 | + "not yet implemented" — they *refuse*, they do not silently miscompile. |
| 180 | +* *Named-field access and record types* are rejected at parse with an explicit |
| 181 | + "not yet supported", not mis-lowered. |
| 182 | + |
| 183 | +[#outstanding] |
| 184 | +=== Outstanding / weak / refuted (no spin) |
| 185 | + |
| 186 | +* *Provenance note (Idris build):* at the *parent* of the anchor commit |
| 187 | + (`818492f3…`) the Idris build was *broken* — `//` header delimiters on line 2 |
| 188 | + of 8 ABI/formal files made `idris2 --build` die at tokenisation |
| 189 | + (`Error: Can't recognise token`). It was repaired *this session* by the |
| 190 | + anchor commit's delimiter-only `//`→`--` fix and re-runs green (see |
| 191 | + <<Solid,What is solid>>). Recorded so the history is honest, not hidden. |
| 192 | +* *Four open L1 region admits* (`formal/Semantics_L1.v`): |
| 193 | + `region_shrink_preserves_typing_l1_gen_m` (:441), |
| 194 | + `region_liveness_at_split_l1_gen` (:1942 — *provably false as written*), |
| 195 | + `step_pop_disjoint_from_type_l1` (:3178 — the eliminator fork, ~9 internal |
| 196 | + cases), `preservation_l1` (:3439 — capstone). Closure route is committed |
| 197 | + (tropical-graded carrier refactor → choreographic-over-time-segments) but |
| 198 | + *not yet done*. |
| 199 | +* *The legacy `formal/Semantics.v` `preservation` is deliberately false — |
| 200 | + refuted on purpose.* `Counterexample.v` `Qed`-proves a configuration that |
| 201 | + types, steps, and lands untypable. Its single `Admitted.` is *correct* and |
| 202 | + durable; that is a _result_, not a gap. (1 of the 5 `Admitted.`) |
| 203 | +* *L4 dyadic semantics: scaffold only* (`ProgramMode` + round-trip mapping; |
| 204 | + definitions, no theorems). |
| 205 | +* *ABI E5 (WASM compilation correctness) and E6 (IR lowering correctness): |
| 206 | + unformalised;* E4 (`noGCExtract`) is a tautological wrapper, not a proof. |
| 207 | +* *The module system — `import M; M.f()` — is not wired,* so the `.eph` stdlib |
| 208 | + (only 2 of 9 files parse) and the typed coprocessor API cannot be consumed. |
| 209 | + This is the keystone gap between ephapax and "actually usable". |
| 210 | +* *Count-marker note:* `TEST-NEEDS.md` records *486* all-target tests (via |
| 211 | + `cargo test --all-targets -- --list`); this session's `cargo test --workspace` |
| 212 | + reports *489* passed. The two count slightly different target sets; neither |
| 213 | + shows a failure. Flagged, not hidden. |
| 214 | + |
| 215 | +[#reproduce] |
| 216 | +== Reproduce it yourself |
| 217 | + |
| 218 | +From the repo root, at the commit above: |
| 219 | + |
| 220 | +[source,sh] |
| 221 | +---- |
| 222 | +just proofs # Coq: expect exit 0 (5 Admitted. = 4 open L1 + 1 deliberately-false legacy) |
| 223 | +cargo test --workspace # expect exit 0; 489 passed, 0 failed, 0 ignored (CARGO_INCREMENTAL=0) |
| 224 | +just validate-wasm # expect: "validate-wasm: all modules structurally valid" |
| 225 | +---- |
| 226 | + |
| 227 | +The Idris side (green at the anchor commit; both packages): |
| 228 | + |
| 229 | +[source,sh] |
| 230 | +---- |
| 231 | +( cd src/formal && idris2 --build ephapax-formal.ipkg ) # expect exit 0 |
| 232 | +( cd src/abi && idris2 --build ephapax-abi.ipkg ) # expect exit 0 |
| 233 | +---- |
| 234 | + |
| 235 | +== One-line characterisation (quote this) |
| 236 | + |
| 237 | +[quote] |
| 238 | +____ |
| 239 | +"A dyadic linear+affine → WebAssembly research language with a machine-checked |
| 240 | +*Coq + Idris2 core* (Coq L2 + L3 + L1-support `Qed`, and both Idris2 ABI/formal |
| 241 | +packages, all build green this session) over a *tested — not proved-to-match* — |
| 242 | +Rust implementation (489 tests pass); every emitted WASM module is structurally |
| 243 | +valid; four open L1 region admits (one provably false as written) with a |
| 244 | +committed closure route; the module-system keystone is not yet wired, so it is |
| 245 | +not usable end-to-end. A serious verified-core research artifact, not a |
| 246 | +production language. No intentional overclaim." |
| 247 | +____ |
| 248 | + |
| 249 | +== Joint attestation |
| 250 | + |
| 251 | +We, the undersigned, assert that *to the best of our joint belief at the |
| 252 | +timestamp above, every claim in this file is true and was checked as described* |
| 253 | +— with no intentional overclaim, and with the open gaps stated rather than |
| 254 | +hidden. |
| 255 | + |
| 256 | +* *Engineering party (AI):* Claude Opus 4.8 (`claude-opus-4-8[1m]`) — ran the |
| 257 | + Coq build, both `idris2 --build` packages, the `cargo test --workspace` suite, |
| 258 | + and `just validate-wasm` recorded here (this session: first cold run 11:52Z, |
| 259 | + all four re-confirmed green at the anchor commit 12:07Z) and stands behind the |
| 260 | + wording above as a faithful report of those runs. |
| 261 | +* *Owner / maintainer:* Jonathan D.A. Jewell — _signs by committing this file |
| 262 | + with `-S` (`id_ed25519_signing`); the git commit signature over this content, |
| 263 | + at the commit SHA recorded above, is the cryptographic form of this |
| 264 | + affirmation._ |
| 265 | ++ |
| 266 | +Signed-off-date: 2026-06-16 |
| 267 | + |
| 268 | +[TIP] |
| 269 | +The authoritative, tamper-evident signature is the *signed git commit* that |
| 270 | +lands this file. If the SHA in <<Verifiable anchor>> matches the parent of that |
| 271 | +commit and the commit verifies, this affirmation is anchored. If they don't |
| 272 | +match, treat the file as a draft. |
0 commit comments