|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | + |
| 4 | += CRG-PROFILE — Ephapax |
| 5 | +:toc: left |
| 6 | +:toclevels: 2 |
| 7 | + |
| 8 | +[cols="1,3"] |
| 9 | +|=== |
| 10 | +| Field | Value |
| 11 | + |
| 12 | +| Language | Ephapax |
| 13 | +| Repository | https://github.com/hyperpolymath/ephapax |
| 14 | +| Current CRG Grade | *D* (X \| F \| E \| D \| C \| B \| A) |
| 15 | +| Assessed | 2026-05-28 |
| 16 | +| Assessor | Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 17 | +| CRG Spec Version | 2.2 |
| 18 | +| ARG Profile | spec/ARG-PROFILE.adoc |
| 19 | +| TRG Profile | spec/TRG-PROFILE.adoc |
| 20 | +| FRG Profile | spec/FRG-PROFILE.adoc |
| 21 | +|=== |
| 22 | + |
| 23 | +== About this profile |
| 24 | + |
| 25 | +This profile applies the *CRG v2.2 (STRICT)* baseline to Ephapax |
| 26 | +released components. *No Ephapax crate is yet published to |
| 27 | +crates.io.* The CRG grade is *D* by extension of the existing CRG |
| 28 | +audit (`docs/governance/CRG-AUDIT-2026-04-18.adoc`), which recommended |
| 29 | +demotion C → D under CRG v2.0 STRICT. This profile carries that |
| 30 | +recommendation forward at v2.2 and updates the evidence. |
| 31 | + |
| 32 | +CRG = *D*. The full chain of axes: |
| 33 | + |
| 34 | +* ARG: *E* (research artefact, narrow adopter base) |
| 35 | +* TRG: *D* (per spec/TRG-PROFILE.adoc) |
| 36 | +* FRG: *D* (active mechanised-proof line) |
| 37 | +* CRG: *D* (this profile) |
| 38 | +* RSR: assessed elsewhere |
| 39 | + |
| 40 | +== Released components |
| 41 | + |
| 42 | +A *released component* is any unit of work this repository publishes |
| 43 | +under its own name + version: crate, library, binary, plugin, schema, |
| 44 | +or vendored artefact. Each is graded independently against CRG. |
| 45 | + |
| 46 | +The list below is the published surface as of 2026-05-28. All |
| 47 | +entries are *workspace-internal* — no Ephapax crate is yet on |
| 48 | +crates.io. Per CRG §1, the language-level CRG is graded on the |
| 49 | +binary artefacts that ship under the `ephapax-cli` package + the |
| 50 | +internal workspace crates that consumers can pull as git |
| 51 | +dependencies (e.g. `typed-wasm` already does this). |
| 52 | + |
| 53 | +[cols="2,1,3,4", options="header"] |
| 54 | +|=== |
| 55 | +| Component | Grade | Release stage | Evidence |
| 56 | + |
| 57 | +| `ephapax` binary (via `ephapax-cli`) |
| 58 | +| *D* |
| 59 | +| Pre-alpha |
| 60 | +| Compiler driver. Built from the Rust workspace. Contract / aspect / E2E tests in `src/ephapax-cli/tests/`. CI green per `.github/workflows/`. |
| 61 | + |
| 62 | +| `ephapax-lsp` binary |
| 63 | +| *D* |
| 64 | +| Pre-alpha |
| 65 | +| LSP server. `src/ephapax-lsp/src/main.rs` (~34KB, tower-lsp). Hover, goto, completions. Inline tests only. |
| 66 | + |
| 67 | +| `ephapax-syntax` workspace crate |
| 68 | +| *D* |
| 69 | +| Workspace-internal |
| 70 | +| 23KB AST library; unit tests. Consumed by typed-wasm via git dependency. |
| 71 | + |
| 72 | +| `ephapax-ir` workspace crate |
| 73 | +| *C* |
| 74 | +| Workspace-internal |
| 75 | +| 38KB IR library; unit tests + JSON round-trip tests. |
| 76 | + |
| 77 | +| `ephapax-typing` workspace crate |
| 78 | +| *C* |
| 79 | +| Workspace-internal |
| 80 | +| ~159KB type checker; extensive unit tests, contract tests (`invariant_*`), property tests. Heaviest single crate. |
| 81 | + |
| 82 | +| `ephapax-wasm` workspace crate |
| 83 | +| *C* |
| 84 | +| Workspace-internal |
| 85 | +| ~195KB WASM encoder; E2E + contract tests (magic-byte validation). |
| 86 | + |
| 87 | +| `ephapax-runtime` workspace crate |
| 88 | +| *D* |
| 89 | +| Workspace-internal |
| 90 | +| ~10KB wasmtime integration; runtime tests. |
| 91 | + |
| 92 | +| `ephapax-linear` workspace crate (sublanguage) |
| 93 | +| *D* |
| 94 | +| Workspace-internal |
| 95 | +| Linear + affine discipline checkers, dyadic interaction semantics. Per the disambiguation hook, `ephapax-affine` here is *not* `affinescript` (different syntax, different IR, shared logic-family terminology). |
| 96 | + |
| 97 | +| Other internal crates (lexer, parser, surface, desugar, interp, repl, stdlib, package, analysis, tools, externs) |
| 98 | +| *D* |
| 99 | +| Workspace-internal |
| 100 | +| Each has its own unit tests; collectively form the compiler pipeline. See spec/TRG-PROFILE.adoc for per-crate detail. |
| 101 | +|=== |
| 102 | + |
| 103 | +== Per-component evidence (deep) |
| 104 | + |
| 105 | +`docs/governance/CRG-AUDIT-2026-04-18.adoc` is the prior CRG audit |
| 106 | +under v2.0 STRICT. Its grade-by-criterion analysis remains |
| 107 | +substantively valid for v2.2 (the criteria did not regress); the |
| 108 | +recommended demotion C → D was driven by the v2.0 *new* CI-green + |
| 109 | +per-directory-README + dogfooding-status clauses. |
| 110 | + |
| 111 | +`.machine_readable/6a2/STATE.a2ml` still self-declares |
| 112 | +`crg-grade = "C"` as of last update 2026-04-11. This profile |
| 113 | +recommends updating that flat-form claim to `D` with |
| 114 | +`grade-previous = "C"` and a note referencing the 2026-04-18 audit |
| 115 | ++ this profile. |
| 116 | + |
| 117 | +No per-component `audits/audit-<crate>.md` files exist yet under |
| 118 | +v2.2 STRICT. |
| 119 | + |
| 120 | +== Grade rationale |
| 121 | + |
| 122 | +[cols="2,1,4", options="header"] |
| 123 | +|=== |
| 124 | +| Grade clause (CRG §4) | Met? | Evidence |
| 125 | + |
| 126 | +| *E1 — At least one test exists* |
| 127 | +| YES |
| 128 | +| Multiple test suites across every workspace crate. |
| 129 | + |
| 130 | +| *E2 — Failures documented* |
| 131 | +| YES |
| 132 | +| `PROOF-NEEDS.md`, `TEST-NEEDS.md`, `formal/PRESERVATION-HANDOFF.md`. |
| 133 | + |
| 134 | +| *D1 — Test matrix documented* |
| 135 | +| YES |
| 136 | +| `TEST-NEEDS.md` (357-test matrix per the prior audit). |
| 137 | + |
| 138 | +| *D2 — Scope documented* |
| 139 | +| YES |
| 140 | +| `README.md`, `CLAUDE.md`, `EXPLAINME.adoc`, `TOPOLOGY.adoc`. |
| 141 | + |
| 142 | +| *D3 — RSR compliance* |
| 143 | +| YES |
| 144 | +| RSR baseline files present. |
| 145 | + |
| 146 | +| *C1 — Dogfooded* |
| 147 | +| PARTIAL |
| 148 | +| Ephapax is used internally for proof research; typed-wasm consumes `ephapax-syntax` as a git dependency. No external consumer beyond first-party tooling. |
| 149 | + |
| 150 | +| *C2 — CI green* |
| 151 | +| YES |
| 152 | +| CI green per `.github/workflows/`. |
| 153 | + |
| 154 | +| *C3 — Deep annotation (per-file + per-dir)* |
| 155 | +| NO |
| 156 | +| No v2.2 STRICT per-file / per-directory audit. Prior audit doc is per-component but at v2.0 strictness. |
| 157 | + |
| 158 | +| *B1 — ≥6 diverse external targets* |
| 159 | +| NO |
| 160 | +| External target list: typed-wasm only. |
| 161 | + |
| 162 | +| *B2 — Issues fed back from external use* |
| 163 | +| NO |
| 164 | +| Closed-issue trail is internal. |
| 165 | + |
| 166 | +| *A1 — Confirmed real-world value, no harm* |
| 167 | +| NO |
| 168 | +| No external feedback corpus. |
| 169 | + |
| 170 | +| *VeriSimDB attestation (grade C+)* |
| 171 | +| NO |
| 172 | +| Ephapax is not yet `DECLARE`'d to VeriSimDB. |
| 173 | +|=== |
| 174 | + |
| 175 | +== Language-specific tightening (this profile only) |
| 176 | + |
| 177 | +For Ephapax, the following additional CRG obligations apply at the |
| 178 | +stated grades: |
| 179 | + |
| 180 | +* *Grade C tightening:* `ephapax-typing` MUST have a published |
| 181 | + soundness statement (currently in flight via `formal/`). Either a |
| 182 | + Qed preservation theorem for at least L1, or an explicit |
| 183 | + "preservation by counter-example refinement" theorem reflecting |
| 184 | + the design doctrine at `formal/PRESERVATION-DESIGN.md`. |
| 185 | +* *Grade C tightening:* `ephapax-wasm` MUST have a published |
| 186 | + conformance report against the typed-wasm carrier ABI surface |
| 187 | + (currently being drafted at typed-wasm#76). |
| 188 | +* *Grade B tightening:* At least one workspace crate MUST be |
| 189 | + published to crates.io with a v1.0 release and external-consumer |
| 190 | + evidence. |
| 191 | +* *Grade A tightening:* Registered VeriSimDB instance + public |
| 192 | + health check + third-party-maintained Ephapax library. |
| 193 | + |
| 194 | +These tightenings are *additional* to the baseline — none of the |
| 195 | +baseline evidence is waived. |
| 196 | + |
| 197 | +== What is NOT yet met (honest gaps) |
| 198 | + |
| 199 | +* *No crates.io publication*. Every workspace crate is internal. |
| 200 | + Grade C asks for "released components"; this profile is treating |
| 201 | + the binary artefacts + git-dep-consumed crates as released, but a |
| 202 | + stricter reading would gate language CRG at X until crates.io |
| 203 | + publication. |
| 204 | +* *No per-component v2.2 STRICT audits*. Update |
| 205 | + `docs/governance/CRG-AUDIT-2026-04-18.adoc` to v2.2 strictness or |
| 206 | + author per-crate audits under `audits/`. |
| 207 | +* *No VeriSimDB attestation*. Needed for grade C onward. |
| 208 | +* *No external consumers beyond typed-wasm*. ARG-C / CRG-C both |
| 209 | + stall here. |
| 210 | + |
| 211 | +== Path to next grade (*C*) |
| 212 | + |
| 213 | +* Publish at least `ephapax-syntax` to crates.io as v0.1.0 (so |
| 214 | + external consumption is on the registry, not git-dep only). |
| 215 | + (~1-2 weeks if API is stable enough) |
| 216 | +* Land L1 preservation Qed (in flight per `formal/`). (~weeks) |
| 217 | +* Update `docs/governance/CRG-AUDIT-2026-04-18.adoc` to v2.2 STRICT |
| 218 | + or author per-crate audits under `audits/`. (~2-3 weeks) |
| 219 | +* Land VeriSimDB attestation. (~1 week) |
| 220 | +* Update `.machine_readable/6a2/STATE.a2ml` to `crg-grade = "D"` |
| 221 | + with the recommended note (mechanical, ~1 day). |
| 222 | + |
| 223 | +*Realistic timeline estimate:* 2-3 months from current state. |
| 224 | + |
| 225 | +== Path to grade beyond that (*B*) |
| 226 | + |
| 227 | +* Publish a v1.0 of at least one workspace crate (likely |
| 228 | + `ephapax-syntax` or `ephapax-ir`). |
| 229 | +* External consumers beyond typed-wasm. |
| 230 | +* Issue-feedback pipeline with external reporters. |
| 231 | + |
| 232 | +== Demotion risk |
| 233 | + |
| 234 | +* *Lowest:* Any workspace crate CI flips to red and stays red. |
| 235 | +* *Medium:* The `ephapax-typing` invariant-test suite regresses |
| 236 | + significantly. |
| 237 | +* *Catastrophic:* A consumer (e.g. typed-wasm) is broken by a |
| 238 | + released-component change and the change is *not* rolled back. |
| 239 | + |
| 240 | +== Iteration history |
| 241 | + |
| 242 | +[cols="1,1,4", options="header"] |
| 243 | +|=== |
| 244 | +| Date | Grade | Notes |
| 245 | + |
| 246 | +| 2026-04-04 | C | Earlier internal audit (CRG v1.x). |
| 247 | +| 2026-04-18 | D | CRG v2.0 STRICT audit `docs/governance/CRG-AUDIT-2026-04-18.adoc` recommended demotion C → D. |
| 248 | +| 2026-05-28 | D | Initial CRG-PROFILE per CRG v2.2 STRICT. Carries forward 2026-04-18 grade. |
| 249 | +|=== |
| 250 | + |
| 251 | +== Review cycle |
| 252 | + |
| 253 | +* *Routine:* Reassess on every release cycle (per CRG §6.3). |
| 254 | +* *Immediate:* Reassess within 7 days of any released-component |
| 255 | + regression. |
| 256 | +* *VeriSimDB drift alert:* Reassess within 24 hours of any drift |
| 257 | + alert. |
| 258 | + |
| 259 | +== Footer |
| 260 | + |
| 261 | +Run `just crg-badge` in this repo to generate the shields.io badge |
| 262 | +for the README. |
| 263 | + |
| 264 | +This profile is itself a VCL-total proposition. Its content is |
| 265 | +`DECLARE`'d to VeriSimDB on each commit. Drift between the claimed |
| 266 | +grade above and the underlying evidence surfaces as a grade-stale |
| 267 | +alert. |
0 commit comments