diff --git a/spec/CRG-PROFILE.adoc b/spec/CRG-PROFILE.adoc new file mode 100644 index 00000000..d40780a4 --- /dev/null +++ b/spec/CRG-PROFILE.adoc @@ -0,0 +1,267 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + += CRG-PROFILE — Ephapax +:toc: left +:toclevels: 2 + +[cols="1,3"] +|=== +| Field | Value + +| Language | Ephapax +| Repository | https://github.com/hyperpolymath/ephapax +| Current CRG Grade | *D* (X \| F \| E \| D \| C \| B \| A) +| Assessed | 2026-05-28 +| Assessor | Jonathan D.A. Jewell +| CRG Spec Version | 2.2 +| ARG Profile | spec/ARG-PROFILE.adoc +| TRG Profile | spec/TRG-PROFILE.adoc +| FRG Profile | spec/FRG-PROFILE.adoc +|=== + +== About this profile + +This profile applies the *CRG v2.2 (STRICT)* baseline to Ephapax +released components. *No Ephapax crate is yet published to +crates.io.* The CRG grade is *D* by extension of the existing CRG +audit (`docs/governance/CRG-AUDIT-2026-04-18.adoc`), which recommended +demotion C → D under CRG v2.0 STRICT. This profile carries that +recommendation forward at v2.2 and updates the evidence. + +CRG = *D*. The full chain of axes: + +* ARG: *E* (research artefact, narrow adopter base) +* TRG: *D* (per spec/TRG-PROFILE.adoc) +* FRG: *D* (active mechanised-proof line) +* CRG: *D* (this profile) +* RSR: assessed elsewhere + +== Released components + +A *released component* is any unit of work this repository publishes +under its own name + version: crate, library, binary, plugin, schema, +or vendored artefact. Each is graded independently against CRG. + +The list below is the published surface as of 2026-05-28. All +entries are *workspace-internal* — no Ephapax crate is yet on +crates.io. Per CRG §1, the language-level CRG is graded on the +binary artefacts that ship under the `ephapax-cli` package + the +internal workspace crates that consumers can pull as git +dependencies (e.g. `typed-wasm` already does this). + +[cols="2,1,3,4", options="header"] +|=== +| Component | Grade | Release stage | Evidence + +| `ephapax` binary (via `ephapax-cli`) +| *D* +| Pre-alpha +| Compiler driver. Built from the Rust workspace. Contract / aspect / E2E tests in `src/ephapax-cli/tests/`. CI green per `.github/workflows/`. + +| `ephapax-lsp` binary +| *D* +| Pre-alpha +| LSP server. `src/ephapax-lsp/src/main.rs` (~34KB, tower-lsp). Hover, goto, completions. Inline tests only. + +| `ephapax-syntax` workspace crate +| *D* +| Workspace-internal +| 23KB AST library; unit tests. Consumed by typed-wasm via git dependency. + +| `ephapax-ir` workspace crate +| *C* +| Workspace-internal +| 38KB IR library; unit tests + JSON round-trip tests. + +| `ephapax-typing` workspace crate +| *C* +| Workspace-internal +| ~159KB type checker; extensive unit tests, contract tests (`invariant_*`), property tests. Heaviest single crate. + +| `ephapax-wasm` workspace crate +| *C* +| Workspace-internal +| ~195KB WASM encoder; E2E + contract tests (magic-byte validation). + +| `ephapax-runtime` workspace crate +| *D* +| Workspace-internal +| ~10KB wasmtime integration; runtime tests. + +| `ephapax-linear` workspace crate (sublanguage) +| *D* +| Workspace-internal +| 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). + +| Other internal crates (lexer, parser, surface, desugar, interp, repl, stdlib, package, analysis, tools, externs) +| *D* +| Workspace-internal +| Each has its own unit tests; collectively form the compiler pipeline. See spec/TRG-PROFILE.adoc for per-crate detail. +|=== + +== Per-component evidence (deep) + +`docs/governance/CRG-AUDIT-2026-04-18.adoc` is the prior CRG audit +under v2.0 STRICT. Its grade-by-criterion analysis remains +substantively valid for v2.2 (the criteria did not regress); the +recommended demotion C → D was driven by the v2.0 *new* CI-green + +per-directory-README + dogfooding-status clauses. + +`.machine_readable/6a2/STATE.a2ml` still self-declares +`crg-grade = "C"` as of last update 2026-04-11. This profile +recommends updating that flat-form claim to `D` with +`grade-previous = "C"` and a note referencing the 2026-04-18 audit ++ this profile. + +No per-component `audits/audit-.md` files exist yet under +v2.2 STRICT. + +== Grade rationale + +[cols="2,1,4", options="header"] +|=== +| Grade clause (CRG §4) | Met? | Evidence + +| *E1 — At least one test exists* +| YES +| Multiple test suites across every workspace crate. + +| *E2 — Failures documented* +| YES +| `PROOF-NEEDS.md`, `TEST-NEEDS.md`, `formal/PRESERVATION-HANDOFF.md`. + +| *D1 — Test matrix documented* +| YES +| `TEST-NEEDS.md` (357-test matrix per the prior audit). + +| *D2 — Scope documented* +| YES +| `README.md`, `CLAUDE.md`, `EXPLAINME.adoc`, `TOPOLOGY.adoc`. + +| *D3 — RSR compliance* +| YES +| RSR baseline files present. + +| *C1 — Dogfooded* +| PARTIAL +| Ephapax is used internally for proof research; typed-wasm consumes `ephapax-syntax` as a git dependency. No external consumer beyond first-party tooling. + +| *C2 — CI green* +| YES +| CI green per `.github/workflows/`. + +| *C3 — Deep annotation (per-file + per-dir)* +| NO +| No v2.2 STRICT per-file / per-directory audit. Prior audit doc is per-component but at v2.0 strictness. + +| *B1 — ≥6 diverse external targets* +| NO +| External target list: typed-wasm only. + +| *B2 — Issues fed back from external use* +| NO +| Closed-issue trail is internal. + +| *A1 — Confirmed real-world value, no harm* +| NO +| No external feedback corpus. + +| *VeriSimDB attestation (grade C+)* +| NO +| Ephapax is not yet `DECLARE`'d to VeriSimDB. +|=== + +== Language-specific tightening (this profile only) + +For Ephapax, the following additional CRG obligations apply at the +stated grades: + +* *Grade C tightening:* `ephapax-typing` MUST have a published + soundness statement (currently in flight via `formal/`). Either a + Qed preservation theorem for at least L1, or an explicit + "preservation by counter-example refinement" theorem reflecting + the design doctrine at `formal/PRESERVATION-DESIGN.md`. +* *Grade C tightening:* `ephapax-wasm` MUST have a published + conformance report against the typed-wasm carrier ABI surface + (currently being drafted at typed-wasm#76). +* *Grade B tightening:* At least one workspace crate MUST be + published to crates.io with a v1.0 release and external-consumer + evidence. +* *Grade A tightening:* Registered VeriSimDB instance + public + health check + third-party-maintained Ephapax library. + +These tightenings are *additional* to the baseline — none of the +baseline evidence is waived. + +== What is NOT yet met (honest gaps) + +* *No crates.io publication*. Every workspace crate is internal. + Grade C asks for "released components"; this profile is treating + the binary artefacts + git-dep-consumed crates as released, but a + stricter reading would gate language CRG at X until crates.io + publication. +* *No per-component v2.2 STRICT audits*. Update + `docs/governance/CRG-AUDIT-2026-04-18.adoc` to v2.2 strictness or + author per-crate audits under `audits/`. +* *No VeriSimDB attestation*. Needed for grade C onward. +* *No external consumers beyond typed-wasm*. ARG-C / CRG-C both + stall here. + +== Path to next grade (*C*) + +* Publish at least `ephapax-syntax` to crates.io as v0.1.0 (so + external consumption is on the registry, not git-dep only). + (~1-2 weeks if API is stable enough) +* Land L1 preservation Qed (in flight per `formal/`). (~weeks) +* Update `docs/governance/CRG-AUDIT-2026-04-18.adoc` to v2.2 STRICT + or author per-crate audits under `audits/`. (~2-3 weeks) +* Land VeriSimDB attestation. (~1 week) +* Update `.machine_readable/6a2/STATE.a2ml` to `crg-grade = "D"` + with the recommended note (mechanical, ~1 day). + +*Realistic timeline estimate:* 2-3 months from current state. + +== Path to grade beyond that (*B*) + +* Publish a v1.0 of at least one workspace crate (likely + `ephapax-syntax` or `ephapax-ir`). +* External consumers beyond typed-wasm. +* Issue-feedback pipeline with external reporters. + +== Demotion risk + +* *Lowest:* Any workspace crate CI flips to red and stays red. +* *Medium:* The `ephapax-typing` invariant-test suite regresses + significantly. +* *Catastrophic:* A consumer (e.g. typed-wasm) is broken by a + released-component change and the change is *not* rolled back. + +== Iteration history + +[cols="1,1,4", options="header"] +|=== +| Date | Grade | Notes + +| 2026-04-04 | C | Earlier internal audit (CRG v1.x). +| 2026-04-18 | D | CRG v2.0 STRICT audit `docs/governance/CRG-AUDIT-2026-04-18.adoc` recommended demotion C → D. +| 2026-05-28 | D | Initial CRG-PROFILE per CRG v2.2 STRICT. Carries forward 2026-04-18 grade. +|=== + +== Review cycle + +* *Routine:* Reassess on every release cycle (per CRG §6.3). +* *Immediate:* Reassess within 7 days of any released-component + regression. +* *VeriSimDB drift alert:* Reassess within 24 hours of any drift + alert. + +== Footer + +Run `just crg-badge` in this repo to generate the shields.io badge +for the README. + +This profile is itself a VCL-total proposition. Its content is +`DECLARE`'d to VeriSimDB on each commit. Drift between the claimed +grade above and the underlying evidence surfaces as a grade-stale +alert. diff --git a/spec/TRG-PROFILE.adoc b/spec/TRG-PROFILE.adoc new file mode 100644 index 00000000..8256b770 --- /dev/null +++ b/spec/TRG-PROFILE.adoc @@ -0,0 +1,239 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + += TRG-PROFILE — Ephapax +:toc: left +:toclevels: 2 + +[cols="1,3"] +|=== +| Field | Value + +| Language | Ephapax +| Repository | https://github.com/hyperpolymath/ephapax +| Current TRG Grade | *D* (X \| F \| E \| D \| C \| B \| A) +| Assessed | 2026-05-28 +| Assessor | Jonathan D.A. Jewell +| TRG Spec Version | 1.0 +| ARG Profile | spec/ARG-PROFILE.adoc +| FRG Profile | spec/FRG-PROFILE.adoc +| CRG Profile | spec/CRG-PROFILE.adoc +|=== + +== About this profile + +This profile applies the *TRG v1.0* baseline to Ephapax. The +toolchain is unusually complete for a research language: a 14-crate +Rust workspace covering lexer (logos), parser (chumsky), AST (core + +surface), desugarer, type checker (159KB), IR, WASM codegen (195KB), +interpreter, REPL (rustyline), LSP (tower-lsp), formatter, package +manager, runtime (wasmtime), and 4-layer Coq formalisation in +`formal/`. Most TRG MUST components are present and tested. The +overall grade lands at *D* rather than C primarily because of three +gating issues: + +* M3 *type-checker oracle* and M4 *proof dispatcher* are *both + ambiguous* for a verified language. The Coq formalisation in + `formal/` proves *properties of* the type system at L1-L4, but + does not act as an oracle that the Rust type checker dispatches + obligations to. Per TRG §3.2, this is an *implicit* implementation + of M3, not a discrete component — grade E at best for both. +* T8 *standard library* is minimal (`ephapax-stdlib`: list ops, + `I32`, bool only). +* No `audits/audit-.md` per TRG §3 / §4. + +The chain of axes: + +* ARG: *E* (research artefact, narrow adopter base) +* TRG: *D* (this profile) +* FRG: *D* (active mechanised-proof line at `formal/`, multi-layer + redesign, counterexample-verified preservation invariants) +* CRG: *D* (per spec/CRG-PROFILE.adoc; no published external + components yet, recommended demotion C→D per + `docs/governance/CRG-AUDIT-2026-04-18.adoc`) +* RSR: assessed elsewhere + +Cross-axis rule: ARG ≤ TRG holds (TRG = D ≥ ARG = E). + +== Component grades + +The toolchain decomposes into components drawn from TRG §3. Each +component is graded independently against the four-tier audit format +of TRG §4 (Must / Should / Could / Aspirational → grades E / D / C / B). +The overall TRG grade is the *worst* of any MUST component. + +=== Front-end (TRG §3.1) + +[cols="1,3,1,4", options="header"] +|=== +| # | Component | Grade | Evidence + +| F1 | Grammar / Syntax | *D* | `spec/ephapax-v2-grammar.ebnf` (EBNF, draft) + `spec/SPEC.md`. CLI grammar tests `v2_grammar_phase_*.rs`. Draft status pulls grade off C. +| F2 | Lexer / Tokeniser | *C* | `src/ephapax-lexer/src/lib.rs` (31KB, `logos`-based). Unit tests + full `TokenKind` enum coverage. +| F3 | Parser | *C* | `src/ephapax-parser/src/lib.rs` (87KB, `chumsky`). Unit tests + property tests + grammar phase tests. +| F4 | AST | *C* | `src/ephapax-syntax/src/lib.rs` (23KB, core AST) + `src/ephapax-surface/src/lib.rs` (18KB, surface AST). `src/ephapax-desugar/src/lib.rs` (71KB) lowers surface → core. All three with unit tests. +| F5 | Macro expander | N/A | Ephapax has no macros. +| F6 | Import resolver / Modules | *D* | `src/ephapax-cli/src/import_resolver.rs`. Embedded in CLI; not a separate auditable component. +| F7 | Diagnostics / Errors | *D* | `src/ephapax-parser/src/error.rs` (LexerError, ParseError). CLI error reporting in `main.rs`. No published error-code index. +|=== + +=== Middle-end (TRG §3.2) + +[cols="1,3,1,4", options="header"] +|=== +| # | Component | Grade | Evidence + +| M1 | Semantic analyser | *D* | `src/ephapax-analysis/src/lib.rs` (7KB). Basic tests; small surface relative to the type checker. +| M2 | Type checker | *B* | `src/ephapax-typing/src/lib.rs` (~159KB). Bidirectional checker with linear + affine discipline. Extensive unit tests, contract tests (`invariant_*`), property tests. Heaviest single component in the codebase. +| M3 | Type-checker oracle | *E* | Embedded in M2 (`check_*` functions). The Coq formalisation in `formal/` proves *properties of* the type system but is not invoked as an oracle by the Rust checker. Per TRG §3.2, this is an implicit M3 — grade E. +| M4 | Proof dispatcher | *E* | No automated dispatcher from the Rust checker to the Coq proofs. Proofs are authored by hand; the design doctrine lives at `formal/PRESERVATION-DESIGN.md` and tracks the four-layer redesign. For a *verified* language this is the load-bearing gap. +| M5 | Semantics document | *C* | `spec/SPEC.md` + `formal/PRESERVATION-DESIGN.md` (canonical doctrine, 4-layer architecture) + `formal/PRESERVATION-HANDOFF.md` + `formal/PHASE-D-REDESIGN.md` + `formal/L4-DYADIC.md`. Operational semantics in `Semantics.v`, `Semantics_L1.v`. Comprehensive but evolving. +|=== + +=== Back-end (TRG §3.3) + +[cols="1,3,1,4", options="header"] +|=== +| # | Component | Grade | Evidence + +| B1 | Intermediate representation | *C* | `src/ephapax-ir/src/lib.rs` (38KB). JSON serialisation in `src/ephapax-ir/src/json.rs`. Unit tests + JSON round-trip tests. +| B2 | Code generator | *C* | `src/ephapax-wasm/src/lib.rs` (~195KB, WebAssembly encoder). `ownership.rs`, `debug.rs` accompanying modules. E2E WASM tests + contract tests (magic-byte validation). +| B3 | Backend registry | *D* | Partial — currently only the `ephapax-wasm` backend exists; `ownership.rs` + `debug.rs` act as the cross-component registry surface. +| B4 | Linker / JIT / eval | *C* | `src/ephapax-runtime/src/lib.rs` (~10KB, `wasmtime` integration). Runtime tests covering list operations. +| B5 | ABI / FFI surface | *D* | `ExternItem`, `Visibility` in `src/ephapax-syntax/src/lib.rs`. Extern blocks in syntax. FFI parsing tests + ownership verification tests. Idris2 ABI surface (per estate convention) not yet declared. +| B6 | Runtime | *D* | `src/ephapax-runtime/src/lib.rs` + `src/ephapax-stdlib/src/lib.rs` (8KB). Minimal — list ops, `I32`, bool only. +|=== + +=== Tool surface (TRG §3.4) + +[cols="1,3,1,4", options="header"] +|=== +| # | Component | Grade | Evidence + +| T1 | Compiler driver | *C* | `src/ephapax-cli/src/main.rs` (clap CLI; subcommands `check`, `compile`, `run`, `repl`). Contract, aspect, and E2E tests in `src/ephapax-cli/tests/`. +| T2 | Interpreter | *C* | `src/ephapax-interp/src/lib.rs` (~68KB). Unit tests. +| T3 | REPL | *D* | `src/ephapax-repl/src/lib.rs` (~15KB, rustyline-based). Basic tests. +| T4 | Formatter | *D* | `src/ephapax-tools/src/formatter.rs`. Unit tests. +| T5 | LSP server | *D* | `src/ephapax-lsp/src/main.rs` (~34KB, tower-lsp; hover, goto, completions). Minimal inline tests; no LSP protocol coverage suite. +| T6 | Debugger | N/A | Absent. SHOULD per TRG §3.4; not blocking grade D. +| T7 | Package manager | *D* | `src/ephapax-package/src/{registry,manifest,resolver}.rs`. Tests for each. +| T8 | Standard library | *E* | `src/ephapax-stdlib/src/lib.rs` (~8KB). Basic list ops, `I32`, `bool`. Minimal coverage. +| T9 | Pipeline orchestrator | *D* | Implicit via CLI main orchestrating lex → parse → desugar → type-check → codegen. Covered by contract tests. +|=== + +== Language-specific tightening (this profile only) + +TRG §1.1 permits per-language tightening. For Ephapax, the +following additional obligations apply at the stated grades: + +* *Grade D tightening:* The type checker MUST reject every linear- + discipline violation in the test corpus (currently in + `src/ephapax-typing/`). The `Counterexample.v` Qed result and the + L1 region-threading design MUST be in agreement with the Rust + checker's behaviour. +* *Grade C tightening:* The four-layer formalisation (L1 regions / + L2 modality / L3 echo / L4 dyadic) MUST be fully connected to the + Rust type checker in at least one direction — either an oracle + bridge (Rust → Coq) or a refinement-checked extraction + (Coq → Rust). Closing M3 / M4 is the gate. +* *Grade B tightening:* preservation_l1 / preservation_l2 / + preservation_l3 lemmas MUST be Qed (not Admitted) for the load- + bearing layer (currently L1 + L2 in flight per + `formal/PRESERVATION-DESIGN.md`). + +These tightenings are *additional* to the baseline — none of the +baseline evidence is waived. + +== Canonical Proof Suite extension + +Ephapax is a verified-aspirational language. The Canonical Proof +Suite extension lives at `formal/`: + +* L1 region-threading: `formal/TypingL1.v`, `formal/Semantics_L1.v`, + `formal/Counterexample.v` (preservation provably false for legacy + formulation — Qed) +* L2 modality: `formal/TypingL2.v`, `formal/Modality.v` + (`linear_to_affine` Qed zero axioms; preservation_l1 stated + ∀modality, both branches currently Admitted) +* L3 echo / residue: `formal/Echo.v` (scaffold) +* L4 dyadic interaction: `formal/L4.v` (design only, not landed) + +Current proof debt is tracked in `PROOF-NEEDS.md` and the four-layer +design doctrine at `formal/PRESERVATION-DESIGN.md`. + +== What is NOT yet met (honest gaps) + +Gating gaps for grade *C*: + +* *M3 oracle bridge*. Coq proofs are not connected to the Rust + type checker as a live oracle. The proofs cover properties of + the type system, not obligations dispatched at check time. +* *M4 proof dispatcher*. No automated dispatcher from typechecker + to prover. +* *T8 standard library expansion*. Current coverage is minimal + (list, `I32`, `bool`); grade C requires demonstrably useful + language usage which requires a richer stdlib. +* *No `audits/audit-.md` per TRG §3 + §4*. Per-component + audit format not yet adopted. + +== Path to next grade (*C*) + +* Land the L1 + L2 preservation lemmas as Qed (currently in flight + per `formal/PRESERVATION-DESIGN.md`). (~weeks — open mathematical + work) +* Either: implement an oracle bridge that lets the Rust checker + *invoke* a Coq judgment via extracted code (closes M3); OR: + document the deliberate decoupling and accept M3 = E + permanently with a tightening that says "Ephapax's verification + story is property-based, not obligation-dispatching." +* Expand `ephapax-stdlib` to cover `String`, `List`, `Option`, + `Result`, `Vec`, basic numerics. (~3-4 weeks) +* Author per-component audits under `audits/`. + +*Realistic timeline estimate:* 2-4 months from current state. + +== Path to grade beyond that (*B*) + +* preservation_l1, preservation_l2, preservation_l3 all Qed. +* `linear_to_affine` proven Qed at L2 (already done — confirm not + regressed). +* External adoption: at least one published consumer of Ephapax + not maintained by the Ephapax team. +* Published soundness theorem for the released verifier crate + (if and when it ships). + +== Demotion risk + +* *Lowest:* `ephapax-typing` contract tests regress. +* *Medium:* L1 preservation work demoted from Qed to Admitted in + a load-bearing rule. +* *Catastrophic:* `Counterexample.v` is found to invalidate not just + the legacy formulation but also L1 / L2 / L3 — would force + TRG demotion to X pending redesign. + +== Iteration history + +[cols="1,1,4", options="header"] +|=== +| Date | Grade | Notes + +| 2026-05-28 | D | Initial TRG assessment per TRG v1.0. Gating items: M3 oracle implicit, M4 dispatcher absent, T8 stdlib minimal. +|=== + +== Review cycle + +* *Routine:* Reassess on every release cycle (per TRG §8). +* *Immediate:* Reassess within 7 days of any MUST-component + regression or formal/ Qed-to-Admitted regression. +* *VeriSimDB drift alert:* Reassess within 24 hours of any drift + alert. + +== Footer + +Run `just trg-badge` in this repo to generate the shields.io badge +for the README. + +This profile is itself a VCL-total proposition. Its content is +`DECLARE`'d to VeriSimDB on each commit. Drift between the claimed +grade above and the underlying evidence surfaces as a grade-stale +alert.