From 610919206dbde49c64acdd73626cf27a83766b85 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 28 May 2026 13:11:10 +0100 Subject: [PATCH] feat(spec): add ARG + TRG + FRG + CRG profiles for typed-wasm MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the four-axis maturation grading for typed-wasm, scored against the framework introduced in hyperpolymath/standards#232 (ARG + FRG) and the templates introduced in hyperpolymath/standards#229 (TRG + CRG profile templates). Compilation target treated as a language-shaped artefact: it has a defined grammar (binary + textual), instruction AST, operational semantics, layered type system (L1-L17), and runtime contract. "Adoption" means downstream languages targeting it as a compilation backend (ephapax, AffineScript). Grade: - ARG-D — README/EXPLAINME/QUICKSTART present, 6 example modules, 3 consumer-feature surfaces (boj-server, panic-attacker, ssg); no public playground / error-code index / educator-facing curriculum. - TRG-C — front-end (F1-F4, F6, F7), middle-end (M1, M2, M3 via Idris2 oracle, M5 strongest in cohort), back-end (B1 = Idris2 ABI as IR, B2 WASM emission, B5 Zig FFI + Idris2 ABI per estate convention); T1-T5 N/A (target, not compiler). 88/88 parser tests pass at v1.5. - FRG-C — 22 Idris2 files at src/abi/ encoding safety protocol with QTT linearity + dependent types, zero believe_me / assert_total in ABI files, A10 closure landed PR #79 inhabiting VerifierSpecAgreement + SourceVerifierAgreement. Gated below B by absence of explicit L1-L10 preservation lemmas (per PROOF-NEEDS.md handoff). - CRG-D — typed-wasm-verify v0.1.0 (workspace-internal, not yet on crates.io), Idris2 ABI surface at C (consumed as source by ephapax + AffineScript), Parser.affine + Zig FFI at D. Cross-axis rule: ARG ≤ TRG holds (TRG = C ≥ ARG = D). Co-Authored-By: Claude Opus 4.7 (1M context) --- spec/ARG-PROFILE.adoc | 202 +++++++++++++++++++++++++++++++++++++ spec/CRG-PROFILE.adoc | 211 +++++++++++++++++++++++++++++++++++++++ spec/FRG-PROFILE.adoc | 226 ++++++++++++++++++++++++++++++++++++++++++ spec/TRG-PROFILE.adoc | 223 +++++++++++++++++++++++++++++++++++++++++ 4 files changed, 862 insertions(+) create mode 100644 spec/ARG-PROFILE.adoc create mode 100644 spec/CRG-PROFILE.adoc create mode 100644 spec/FRG-PROFILE.adoc create mode 100644 spec/TRG-PROFILE.adoc diff --git a/spec/ARG-PROFILE.adoc b/spec/ARG-PROFILE.adoc new file mode 100644 index 0000000..b08a2af --- /dev/null +++ b/spec/ARG-PROFILE.adoc @@ -0,0 +1,202 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + += ARG-PROFILE — typed-wasm +:toc: left +:toclevels: 2 + +[cols="1,3"] +|=== +| Field | Value + +| Artefact | typed-wasm (compilation target, language-shaped) +| Repository | https://github.com/hyperpolymath/typed-wasm +| Current ARG Grade | *D* (X \| F \| E \| D \| C \| B \| A) +| Assessed | 2026-05-28 +| Assessor | Jonathan D.A. Jewell +| ARG Spec Version | 1.0 +| TRG Profile | spec/TRG-PROFILE.adoc +| FRG Profile | spec/FRG-PROFILE.adoc +| CRG Profile | spec/CRG-PROFILE.adoc +|=== + +== About this profile + +typed-wasm is not a user-facing language but a *language-shaped +compilation target*: it has a defined grammar (binary + textual +form per `spec/grammar.ebnf`), instruction AST, operational +semantics (per `spec/type-safety-levels-for-wasm.adoc`), a layered +type system (L1-L10 checked, L11-L12 draft, L13-L16 live in v1.4 +and v1.5 per `LEVEL-STATUS.md`, L17 reserved), and a runtime +contract (WebAssembly executor + verifier crate). ARG applies to +it the same way it applies to a language, with the understanding +that *"adoption"* means *"downstream languages targeting it as a +compilation backend"* rather than end-users writing it. + +ARG = *D*. The full chain of axes: + +* ARG: *D* (this profile) +* TRG: *C* (per `spec/TRG-PROFILE.adoc`) +* FRG: *C* (per `spec/FRG-PROFILE.adoc` — 22 Idris2 verifier files + with QTT linearity + dependent types; A10 closure landed PR #79 + inhabiting `VerifierSpecAgreement` + `SourceVerifierAgreement`) +* CRG: *D* (per `spec/CRG-PROFILE.adoc`; `typed-wasm-verify` v0.1.0 + not yet on crates.io) +* RSR: Compliant at TRG-C level + +Cross-axis rule: ARG ≤ TRG holds (TRG = C ≥ ARG = D). ARG can +climb to C without TRG promotion because TRG is already C. + +== Grade rationale (evidence for D) + +[cols="2,1,4", options="header"] +|=== +| Criterion | Met? | Evidence + +| *D1 — Landing page / README* +| YES +| `README.adoc` (sectioned: Specification and surface syntax / Proofs and implementation / Examples / Status and strategy) + `EXPLAINME.adoc` + `QUICKSTART.adoc`. + +| *D2 — Elevator pitch* +| YES +| README header pitches typed-wasm as a layered safety-bearing compilation target for hyperpolymath languages. + +| *D3 — Provenance* +| YES +| `LICENSE` (MPL-2.0), `CHANGELOG.md`, `LEVEL-STATUS.md` tracks active version (v1.5), `Cargo.toml` workspace shape. + +| *Required TRG grade (ARG-D ⇒ TRG ≥ D)* +| YES +| TRG-C — see spec/TRG-PROFILE.adoc. + +| *Onboarding O1 — 5-minute hello-world* +| PARTIAL +| `examples/01-single-module.twasm` + 5 more example modules; consumer-side QUICKSTART exists but not measured against a 5-minute floor. + +| *Onboarding O2 — Tutorial covering distinctive features* +| YES +| The 6 example `.twasm` files cover module structure, multi-module, ownership/linearity, ECS, tropical cost, epistemic sync — the load-bearing safety dimensions. + +| *Onboarding O3 — Playground* +| PARTIAL +| `examples/web-project-deno.json` ships a runnable Deno-based playground harness; no public web playground yet. + +| *Onboarding O4 — Cookbook in ≥ 2 substantive domains* +| YES +| `features/{boj-server,panic-attacker,ssg}/` — three substantive consumer surfaces; examples span 6 domains. + +| *Reference R1 — Reference manual* +| YES +| `spec/type-safety-levels-for-wasm.adoc` (load-bearing) + `spec/L13-L16-reserved-syntax.adoc` + `spec/async-convergence-abi.adoc` + `docs/proposals/`. + +| *Reference R2 — Stdlib reference* +| YES +| `src/abi/Layout/Stdlib.idr` — typed stdlib surface declared at Idris2 level. + +| *Reference R3 — Formal grammar* +| YES +| `spec/grammar.ebnf` (load-bearing) + parsing handled by `Parser.affine` in the AffineScript surface. + +| *Reference R4 — Operational/denotational semantics* +| YES +| `spec/type-safety-levels-for-wasm.adoc` covers the per-level operational semantics. Mechanised semantics in 22 Idris2 files at `src/abi/`. + +| *Reference R5 — Stable error-code index* +| NO +| Verifier errors are typed (`thiserror`-based) but no public error-code index. + +| *Community C1-C5* +| PARTIAL +| CONTRIBUTING + CoC + SECURITY present. Discussion venues + RFC list partial: `docs/proposals/0001-*.md`, `docs/proposals/0002-*.md` are the current RFC process. + +| *Distribution Δ1-Δ5* +| PARTIAL +| `Cargo.toml` ships `typed-wasm-verify` v0.1.0 (unpublished). SemVer policy implicit. No deprecation log. `SECURITY.md` present. + +| *Education E1-E4 (grade-dependent)* +| NO +| No curriculum / external educators. + +| *Ecosystem X1-X4 (grade B+)* +| PARTIAL +| 2 known consumer languages (ephapax via `ephapax-syntax` git-dep; AffineScript via Parser.affine integration). Below the B threshold. + +| *Diversity metrics (grade C+)* +| NO +| Single-maintainer; no diversity surface. + +| *VeriSimDB attestation (grade C+)* +| NO +| typed-wasm not yet `DECLARE`'d. + +| *Founder bus-factor test (grade A only)* +| N/A +| Not at grade A. +|=== + +== Language-specific tightening (this profile only) + +ARG §1.1 permits per-language tightening. For typed-wasm: + +* *Grade C tightening:* Every level L1-L17 MUST be either checked + (with a status entry in `LEVEL-STATUS.md`) or explicitly + reserved (not silently absent). Currently met: v1.5 ships + L1-L10 + L13-L16 checked, L11-L12 draft-only, L17 reserved. +* *Grade B tightening:* At least one consumer language MUST run + its own CI as a typed-wasm consumer (i.e. typed-wasm release + changes are surfaced as CI failures in the consumer). +* *Grade A tightening:* Registered VeriSimDB instance + third- + party language adopter not maintained by hyperpolymath. + +== What is NOT yet met (honest gaps) + +* No public error-code index (R5). +* No public playground beyond the Deno harness. +* No educator-facing curriculum. +* Below the B-threshold for downstream consumer count (2 known). +* No VeriSimDB attestation. + +== Path to next grade (*C*) + +* Publish error-code index. (~1 week) +* Publish a web playground. (~3-4 weeks) +* Land VeriSimDB attestation. (~1 week) +* Document the implicit RFC process at `docs/proposals/` as a + discoverable contributor surface. (~1 week) + +*Realistic timeline estimate:* 6-8 weeks. + +== Path to grade beyond that (*B*) + +* Land ≥6 downstream language consumers (or document with rationale + why typed-wasm is a hyperpolymath-internal target and the + ≥6-target metric is interpreted as ≥6 downstream surfaces such + as `features/{boj-server,panic-attacker,ssg}/`). +* Consumer-language CI integration. + +== Demotion risk + +* *Lowest:* `typed-wasm-verify` CI flips to red. +* *Medium:* A verifier-level regression invalidates a closed proof + obligation (e.g. A10's `VerifierSpecAgreement` regresses). +* *Catastrophic:* A consumer (ephapax or AffineScript) is broken + by a typed-wasm release and the breakage is not rolled back. + +== Iteration history + +[cols="1,1,4", options="header"] +|=== +| Date | Grade | Notes + +| 2026-05-28 | D | Initial ARG assessment per ARG v1.0. Compilation target treated as language-shaped artefact. +|=== + +== Review cycle + +* *Routine:* Reassess on every release cycle (per ARG §6). +* *Immediate:* Reassess within 7 days of any demotion trigger. +* *VeriSimDB drift alert:* Reassess within 24 hours. + +== Footer + +Run `just arg-badge` in this repo to generate the shields.io badge. diff --git a/spec/CRG-PROFILE.adoc b/spec/CRG-PROFILE.adoc new file mode 100644 index 0000000..01b2041 --- /dev/null +++ b/spec/CRG-PROFILE.adoc @@ -0,0 +1,211 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + += CRG-PROFILE — typed-wasm +:toc: left +:toclevels: 2 + +[cols="1,3"] +|=== +| Field | Value + +| Artefact | typed-wasm (compilation target, language-shaped) +| Repository | https://github.com/hyperpolymath/typed-wasm +| 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 typed-wasm +released components. The only externally-released component is the +Rust verifier crate `typed-wasm-verify` v0.1.0 (workspace-internal, +not yet on crates.io). The Idris2 ABI files at `src/abi/` are +consumed as a source surface by downstream languages via the +existing AffineScript / ephapax integrations. + +CRG = *D*. The full chain of axes: + +* ARG: *D* +* TRG: *C* +* FRG: *C* +* CRG: *D* (this profile) +* RSR: Compliant at TRG-C level + +== 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. + +[cols="2,1,3,4", options="header"] +|=== +| Component | Grade | Release stage | Evidence + +| `typed-wasm-verify` (Rust crate) v0.1.0 +| *D* +| Pre-alpha (workspace-internal, unpublished) +| `crates/typed-wasm-verify/Cargo.toml`. Post-codegen verifier for L7 (aliasing) + L10 (linearity). 2221 lines (cross 535, lib 180, section 681, verify 825). Feature gate `unstable-l2` pre-stages the L2 region-binding carrier codec for proposal #76. Pinned to wasmparser =0.250.0 / wasm-encoder =0.250.0. + +| Idris2 ABI surface at `src/abi/` +| *C* +| Consumed-as-source +| 22 Idris2 files acting as the typed ABI surface that downstream languages target. Consumed by ephapax + AffineScript today. Not a Cargo/npm/opam package — the release shape is "stable source files within the typed-wasm repo at a tagged version." + +| `Parser.affine` (AffineScript-implemented parser) +| *D* +| Workspace-internal +| Parser implementation referenced by `LEVEL-STATUS.md` (Parser.affine:2088 etc). 88/88 parser tests pass at v1.5. Distributed within the typed-wasm repo, not as a separate AffineScript package. + +| Zig FFI surface at `ffi/zig/` +| *D* +| Workspace-internal +| `ffi/zig/{build.zig, src, test}`. Acts as the canonical Zig binding per the estate-wide convention (Zig for APIs/FFIs). + +| Examples (`.twasm` corpus + `.affine` integration) +| *E* +| Documentation surface +| 6 `.twasm` examples + `SafeDOMExample.affine` + `web-project-deno.json`. Documentation rather than consumable release. +|=== + +== Per-component evidence (deep) + +For `typed-wasm-verify` at grade D, the v2.2 STRICT deep-annotation +requirements (CRG §4.5+) are not yet met: + +* No `audits/audit-typed-wasm-verify.md` exists. +* `crates/typed-wasm-verify/README.md` covers usage; no per-file + CRG annotation. +* CI runs the verifier against the proposal-0001 4-fixture corpus + (per the standards#130 long-tail tracker referenced in + CHANGELOG.md). + +For the Idris2 ABI surface at grade C, the v2.2 STRICT clauses are +substantially met via the `PROOF-NEEDS.md` reconciliation block + +the LEVEL-STATUS surface table — these together act as a +per-file + per-level annotation surface. + +== Grade rationale + +[cols="2,1,4", options="header"] +|=== +| Grade clause (CRG §4) | Met? | Evidence + +| *E1 — At least one test exists* +| YES +| 88/88 parser tests pass at v1.5; verifier crate has test suite. + +| *E2 — Failures documented* +| YES +| `PROOF-NEEDS.md` is the canonical record of "what is not yet proven." + +| *D1 — Test matrix documented* +| YES +| `LEVEL-STATUS.md` documents per-level + per-feature test status. + +| *D2 — Scope documented* +| YES +| `README.adoc`, `EXPLAINME.adoc`, `QUICKSTART.adoc`, `ROADMAP.adoc`. + +| *D3 — RSR compliance* +| YES +| RSR baseline files present. + +| *C1 — Dogfooded* +| YES +| typed-wasm is dogfooded by ephapax + AffineScript (both are downstream consumer languages of typed-wasm as a compilation target). + +| *C2 — CI green* +| YES +| CI per `.github/workflows/`. + +| *C3 — Deep annotation (per-file + per-dir)* +| PARTIAL +| Idris2 ABI surface effectively documented via `PROOF-NEEDS.md` + LEVEL-STATUS; the verifier crate has no per-file CRG audit. + +| *B1 — ≥6 diverse external targets* +| PARTIAL +| Downstream language consumers: ephapax + AffineScript. The `features/{boj-server,panic-attacker,ssg}/` give 3 substantive feature surfaces. Below the conventional ≥6-target threshold but meaningful for a compilation target. + +| *B2 — Issues fed back from external use* +| YES +| ephapax CI surfaces typed-wasm version-pin drift; AffineScript fixture corpus catches verifier-side breakage. Closed-issue trail per the standards#130 tracker. + +| *A1 — Confirmed real-world value, no harm* +| PARTIAL +| Real internal value confirmed (multiple downstream consumers); no external (non-hyperpolymath) adopters. + +| *VeriSimDB attestation (grade C+)* +| NO +| typed-wasm not yet `DECLARE`'d. +|=== + +== Language-specific tightening (this profile only) + +For typed-wasm, the following additional CRG obligations apply at +the stated grades: + +* *Grade C tightening:* `typed-wasm-verify` MUST keep + wasmparser + wasm-encoder version pins explicit + bumped in a + visible Cargo.toml diff (currently met via the `=0.250.0` exact + pin convention). +* *Grade B tightening:* `typed-wasm-verify` MUST be published on + crates.io as v1.0 with at least one external consumer not + maintained by hyperpolymath. +* *Grade A tightening:* Registered VeriSimDB instance + public + health check + third-party language adopter. + +These tightenings are *additional* to the baseline. + +== What is NOT yet met (honest gaps) + +* `typed-wasm-verify` not yet on crates.io. +* No `audits/audit-typed-wasm-verify.md` per CRG §4.5 + TRG §3. +* No external (non-hyperpolymath) consumer languages. +* No VeriSimDB attestation. + +== Path to next grade (*C*) + +* Author `audits/audit-typed-wasm-verify.md` covering the verifier + crate at v2.2 STRICT depth. (~2-3 weeks) +* Land VeriSimDB attestation. (~1 week) + +*Realistic timeline estimate:* 4-6 weeks. + +== Path to grade beyond that (*B*) + +* Publish `typed-wasm-verify` v1.0 on crates.io. +* Onboard ≥1 external consumer language. + +== Demotion risk + +* *Lowest:* `typed-wasm-verify` CI flips to red. +* *Medium:* wasmparser API drift breaks the build despite the pin + (e.g. transitive dep break). +* *Catastrophic:* A consumer of `typed-wasm-verify` is broken by + a release change and the change is not rolled back. + +== Iteration history + +[cols="1,1,4", options="header"] +|=== +| Date | Grade | Notes + +| 2026-05-28 | D | Initial CRG-PROFILE per CRG v2.2 STRICT. Single externally-released component (`typed-wasm-verify` v0.1.0, workspace-internal, unpublished). +|=== + +== 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. + +== Footer + +Run `just crg-badge` in this repo to generate the shields.io badge. diff --git a/spec/FRG-PROFILE.adoc b/spec/FRG-PROFILE.adoc new file mode 100644 index 0000000..88af79f --- /dev/null +++ b/spec/FRG-PROFILE.adoc @@ -0,0 +1,226 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + += FRG-PROFILE — typed-wasm +:toc: left +:toclevels: 2 + +[cols="1,3"] +|=== +| Field | Value + +| Artefact | typed-wasm (compilation target, language-shaped) +| Repository | https://github.com/hyperpolymath/typed-wasm +| Current FRG Grade | *C* (X \| F \| E \| D \| C \| B \| A) +| Assessed | 2026-05-28 +| Assessor | Jonathan D.A. Jewell +| FRG Spec Version | 1.0 +| ARG Profile | spec/ARG-PROFILE.adoc +| TRG Profile | spec/TRG-PROFILE.adoc +| CRG Profile | spec/CRG-PROFILE.adoc +| Formalisation Directory | `src/abi/TypedWasm/ABI/` + `src/abi/Layout/` (22 Idris2 files) +| Qualifying Prover(s) | Idris2 (with QTT linearity) +|=== + +== About this profile + +typed-wasm is the strongest of the audit-cohort artefacts on the +foundations axis. Its formalisation surface comprises *22 Idris2 +files* in `src/abi/` encoding a safety protocol using QTT +linearity + dependent types, zero `believe_me`/`assert_total` in +the ABI files (per `PROOF-NEEDS.md` 2026-04-13 audit), and the +A10 closure (PR #79) which inhabited the previously-residual +`VerifierSpecAgreement` and `SourceVerifierAgreement` records with +totally-proven bodies. + +FRG = *C*. The grade is not yet B because — per the load-bearing +honesty statement in `PROOF-NEEDS.md`: + +[quote] +____ +typed-wasm has eleven Idris2 files encoding a safety protocol using +QTT linearity and dependent types, zero dangerous patterns, but +almost no explicit theorems — most of the guarantees are +structural consequences of the type encoding rather than +propositions that have been stated and mechanically proven. +____ + +(Note: the file count is now 22, not 11, post-2026-04-13.) Grade +C is reached because the structural guarantees + A10 agreement +records + 88/88 parser tests + explicit Idris2 theorems for +L13-L16 (per `LEVEL-STATUS.md`) clear the C-bar. Grade B requires +per-level preservation lemmas, which is open work. + +The chain of axes: + +* ARG: *D* (per `spec/ARG-PROFILE.adoc`) +* TRG: *C* (per `spec/TRG-PROFILE.adoc`) +* FRG: *C* (this profile) +* CRG: *D* (per `spec/CRG-PROFILE.adoc`) +* RSR: Compliant at TRG-C level + +== Formalisation inventory + +[cols="2,1,5", options="header"] +|=== +| Surface | File count | Path + +| Level theorems (L1-L10 + L13-L16) +| 13 +| `src/abi/TypedWasm/ABI/{Levels,Region,Lifetime,Effects,Layout,Linear,Pointer,Tropical,Epistemic,ModuleIsolation,SessionProtocol,ResourceCapabilities,Choreography}.idr` + +| Echo / multi-module / typed-access composition +| 3 +| `src/abi/TypedWasm/ABI/{Echo,MultiModule,TypedAccess}.idr` + +| Verifier + bridge +| 4 +| `src/abi/TypedWasm/ABI/{Proofs,VerifierSpec,ABI,Types}.idr` + +| Stdlib + concrete-feature corpus +| 2 +| `src/abi/TypedWasm/ABI/{Stdlib,AirborneSubmarineSquadron}.idr` + +| Layout-side +| 4 +| `src/abi/Layout/{Types,ABI,Stdlib,AirborneSubmarineSquadron}.idr` + +| TOTAL +| 22 +| +|=== + +Hygiene status (per `PROOF-NEEDS.md` audit 2026-04-13): + +* Zero live uses of `believe_me` in ABI files. +* Zero live uses of `assert_total` in ABI files. +* No hole-filled (`?foo`) productions in committed code. +* QTT linearity discipline enforced via dependent types. + +== Grade rationale (evidence for C) + +[cols="2,1,4", options="header"] +|=== +| Criterion | Met? | Evidence + +| *E1 — Formal artefact exists* +| YES +| 22 Idris2 files at `src/abi/`. + +| *E2 — Prover qualifies under FRG* +| YES +| Idris2 with QTT is on the qualifying-prover list. + +| *D1 — Artefact is named + located + version-pinned* +| YES +| `Cargo.toml` workspace pins; CHANGELOG tracks levels per release. + +| *D2 — Artefact compiles + checks* +| YES +| CI per `.github/workflows/`. Idris2 typecheck runs in CI. + +| *C1 — Documented design rationale* +| YES +| `README.adoc` "Proofs and implementation" section + `spec/type-safety-levels-for-wasm.adoc` + `docs/proposals/0001-*.md` + `docs/proposals/0002-*.md`. + +| *C2 — Documented proof-debt* +| YES +| `PROOF-NEEDS.md` is the canonical handoff doc; `docs/proof-debt.md` companion. + +| *C3 — Audit cadence* +| YES +| 2026-04-13 audit + 2026-05-27 RECONCILIATION block (A10 closure) + ongoing. + +| *B1 — Per-level preservation lemmas (explicit, not structural)* +| PARTIAL +| L13-L16 have explicit Idris2 theorems (DistinctCaps, ContainedIn, CallCompatible, etc. per LEVEL-STATUS); L1-L10 carry structural guarantees but no separately-stated preservation lemmas. + +| *B2 — Verifier ↔ spec refinement theorem* +| PARTIAL +| A10 closure inhabits the agreement records (`VerifierSpecAgreement`, `SourceVerifierAgreement`); the formal refinement claim is implicit in the inhabitation. + +| *B3 — External review of the formalisation* +| NO +| No published external review of the Idris2 corpus. + +| *A1 — Published soundness for the whole stack* +| NO +| Not yet. + +| *VeriSimDB attestation (grade C+)* +| NO +| typed-wasm not yet `DECLARE`'d. +|=== + +== Language-specific tightening (this profile only) + +For typed-wasm, the following additional FRG obligations apply at +the stated grades: + +* *Grade C tightening:* No `believe_me` / `assert_total` in + `src/abi/`. Currently met. +* *Grade B tightening:* Every level L1-L17 has an explicit + preservation lemma. Currently met for L13-L16; L1-L12 open. +* *Grade A tightening:* External audit by a third party of the + Idris2 corpus. + +These tightenings are *additional* to the baseline. + +== What is NOT yet met (honest gaps) + +Gating gaps for grade *B*: + +* *L1-L10 preservation lemmas not yet stated as theorems.* Most + guarantees are structural consequences of the type encoding. + This is the load-bearing PROOF-NEEDS handoff. +* *L11 (Tropical) and L12 (Epistemic) remain draft-only at v1.1.* +* *No external review.* + +== Path to next grade (*B*) + +* State + prove L1-L10 preservation lemmas per level. Per + PROOF-NEEDS, this is the work that turns "the types forbid it + at compile time" into "here is a lemma proving it is forbidden." + (~weeks per level) +* Promote L11 + L12 from draft to checked. +* State the verifier-spec refinement theorem explicitly citing + A10's agreement records. + +*Realistic timeline estimate:* 3-6 months for the L1-L10 +preservation work; L11/L12 independent timeline. + +== Path to grade beyond that (*A*) + +* External review of the Idris2 corpus. +* Published soundness theorem for the whole stack. +* Registered VeriSimDB instance. + +== Demotion risk + +* *Lowest:* A new `*.idr` file commits a `believe_me` or + `assert_total`. +* *Medium:* The A10 agreement records are found to be inhabitable + only via an unspoken assumption. +* *Catastrophic:* A consumer language's CI detects that an + Idris2-encoded invariant is actually violated at the WASM + emission layer — would force FRG and TRG demotion together. + +== Iteration history + +[cols="1,1,4", options="header"] +|=== +| Date | Grade | Notes + +| 2026-05-28 | C | Initial FRG assessment per FRG v1.0. The strongest foundation surface in the audit cohort; gated below B by absence of explicit L1-L10 preservation lemmas. +|=== + +== Review cycle + +* *Routine:* Reassess on every release cycle (per FRG §6). +* *Immediate:* Reassess within 7 days of any `believe_me` / + `assert_total` introduction in `src/abi/`. +* *VeriSimDB drift alert:* Reassess within 24 hours. + +== Footer + +Run `just frg-badge` in this repo to generate the shields.io badge. diff --git a/spec/TRG-PROFILE.adoc b/spec/TRG-PROFILE.adoc new file mode 100644 index 0000000..c495136 --- /dev/null +++ b/spec/TRG-PROFILE.adoc @@ -0,0 +1,223 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + += TRG-PROFILE — typed-wasm +:toc: left +:toclevels: 2 + +[cols="1,3"] +|=== +| Field | Value + +| Artefact | typed-wasm (compilation target, language-shaped) +| Repository | https://github.com/hyperpolymath/typed-wasm +| Current TRG Grade | *C* (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 + +typed-wasm is a compilation target — graded under TRG with the +interpretation that *front-end* components apply to its binary ++ textual surface, *middle-end* applies to the per-level type +checker (L1-L17), *back-end* applies to encoding into the WebAssembly +binary format (which is itself the load-bearing emission target), +and *tool surface* applies to the verifier crate + embedder ABI. + +The toolchain is C-grade: 22 Idris2 verifier files spanning the +layered safety levels (Levels, Region, Lifetime, Effects, Layout, +Linear, Pointer, Tropical, Epistemic, ModuleIsolation, +SessionProtocol, ResourceCapabilities, Choreography, Echo, Proofs, +MultiModule, TypedAccess, VerifierSpec, ABI, Types, Stdlib, +AirborneSubmarineSquadron), a Rust verifier crate +(`typed-wasm-verify` v0.1.0 — `cross.rs` 535, `lib.rs` 180, +`section.rs` 681, `verify.rs` 825; 2221 lines total), a Zig FFI +(`ffi/zig/{build.zig, src, test}`), 88/88 parser tests passing +(per LEVEL-STATUS.md v1.5 entry), 6 example modules, and a proposals +RFC process under `docs/proposals/`. + +The chain of axes: + +* ARG: *D* (per `spec/ARG-PROFILE.adoc`) +* TRG: *C* (this profile) +* FRG: *C* (per `spec/FRG-PROFILE.adoc` — Idris2 verifier files + + A10 closure landed PR #79) +* CRG: *D* (per `spec/CRG-PROFILE.adoc` — `typed-wasm-verify` + v0.1.0 not yet on crates.io) +* RSR: Compliant at TRG-C level + +Cross-axis rule: ARG ≤ TRG holds (TRG = C ≥ ARG = D). + +== Component grades + +The toolchain decomposes into components drawn from TRG §3 with +the compilation-target interpretation noted above. + +=== Front-end (TRG §3.1) + +[cols="1,3,1,4", options="header"] +|=== +| # | Component | Grade | Evidence + +| F1 | Grammar / Syntax | *C* | `spec/grammar.ebnf` (EBNF) + `spec/L13-L16-reserved-syntax.adoc`. 88/88 parser tests pass at v1.5 (per `LEVEL-STATUS.md` 2026-04-18 verification). +| F2 | Lexer / Tokeniser | *C* | Lexing handled by the surface-level `Parser.affine` (AffineScript-implemented parser); per-keyword + reserved-keyword tests pass. +| F3 | Parser | *C* | `Parser.affine` per `LEVEL-STATUS.md`. 88/88 parser tests verified 2026-04-18 at v1.5. +| F4 | AST | *C* | `Ast.ConstDecl`, `Ast.MatchStmt`, `Ast.BlockIfExpr`, `regionDecl.layout` (striated), function-decl `caps` per LEVEL-STATUS surface table; invariants encoded in Idris2 ABI at `src/abi/TypedWasm/ABI/Types.idr`. +| F5 | Macro expander | N/A | typed-wasm has no macros. +| F6 | Import resolver / Modules | *C* | Per `src/abi/TypedWasm/ABI/MultiModule.idr` + `ModuleIsolation.idr`. Multi-module example at `examples/02-multi-module.twasm`. +| F7 | Diagnostics / Errors | *C* | `thiserror`-based typed errors in `typed-wasm-verify`; per-section error reporting at `crates/typed-wasm-verify/src/section.rs` (681 lines). +|=== + +=== Middle-end (TRG §3.2) + +[cols="1,3,1,4", options="header"] +|=== +| # | Component | Grade | Evidence + +| M1 | Semantic analyser | *C* | Per-level checkers `Checker.checkIsolatedModule`, `checkSession`, `checkCapabilities`, `checkChoreography` per LEVEL-STATUS. +| M2 | Type checker | *C* | Per-level type judgements in `src/abi/TypedWasm/ABI/{Levels,Region,Lifetime,Effects,Layout,Linear,Pointer,Tropical,Epistemic,ModuleIsolation,SessionProtocol,ResourceCapabilities,Choreography}.idr` (14 typed-AST files). +| M3 | Type-checker oracle | *C* | The Idris2 ABI files act as the oracle: the Rust verifier (`typed-wasm-verify`) checks emitted WASM against the Idris2-encoded properties; A10 closure (PR #79) inhabits `VerifierSpecAgreement` + `SourceVerifierAgreement`. +| M4 | Proof dispatcher | *D* | Differential constructor at `VerifierAccepts` (per PROOF-NEEDS.md reconciliation block) packages structural witnesses inline via `TrustedFixture`. Not an automated dispatcher in the Coq/Lean sense; oracle-side encoding is the operational equivalent. +| M5 | Semantics document | *B* | `spec/type-safety-levels-for-wasm.adoc` is the canonical operational + denotational doc; `spec/async-convergence-abi.adoc` covers async; `docs/proposals/0001-*.md` + `docs/proposals/0002-*.md` are the live RFC corpus. Strongest M5 in the audit cohort. +|=== + +=== Back-end (TRG §3.3) + +[cols="1,3,1,4", options="header"] +|=== +| # | Component | Grade | Evidence + +| B1 | Intermediate representation | *C* | The 22 Idris2 ABI files are themselves the IR-with-documented-invariants surface (Layout, Linear, Pointer, etc). +| B2 | Code generator | *C* | Emission into WebAssembly binary format; per-section encoding tested via the verifier on emitted output. +| B3 | Backend registry | N/A | Single back-end (WebAssembly binary). +| B4 | Linker / JIT / eval | *D* | Linking delegated to the host WebAssembly runtime; typed-wasm does not bundle its own JIT/eval. +| B5 | ABI / FFI surface | *C* | Idris2 ABI declared at `src/abi/TypedWasm/ABI/*.idr` (load-bearing). Zig FFI at `ffi/zig/{build.zig, src, test}`. Per estate convention this is the canonical pair (per the user's directive: Zig for APIs/FFIs, Idris2 for ABIs). +| B6 | Runtime | *D* | typed-wasm targets host WebAssembly runtimes (Wasmtime, browser engines, etc); no bundled runtime. Verifier crate guards what runtimes accept. +|=== + +=== Tool surface (TRG §3.4) + +[cols="1,3,1,4", options="header"] +|=== +| # | Component | Grade | Evidence + +| T1 | Compiler driver | N/A | typed-wasm is a target, not a compiler. Producer languages (ephapax, AffineScript) ship their own drivers. +| T2 | Interpreter | N/A | Same reason as T1; host runtimes interpret/JIT. +| T3 | REPL | N/A | Not applicable to a compilation target. +| T4 | Formatter | N/A | The textual surface (.twasm) is formatted via WAT conventions; no bespoke formatter. +| T5 | LSP server | N/A | LSPs live in producer languages. +| T6 | Debugger | *D* | Debugger surface covered by source-map propagation through the toolchain; no typed-wasm-specific debugger. +| T7 | Package manager | N/A | typed-wasm versions are managed via the consumer language's package manager + the `typed-wasm-verify` Cargo manifest. +| T8 | Standard library | *C* | `src/abi/Layout/Stdlib.idr` declares the typed stdlib surface. +| T9 | Pipeline orchestrator | *C* | `Justfile` + `contractile.just` + `setup.sh`. CI per `.github/workflows/`. +|=== + +The N/A entries above are explicitly declared per TRG §3 "MUST +declare it absent and justify the absence." + +== Language-specific tightening (this profile only) + +TRG §1.1 permits per-language tightening. For typed-wasm: + +* *Grade C tightening:* Every level L1-L17 MUST have either an + Idris2 `*.idr` file in `src/abi/TypedWasm/ABI/` OR a documented + status (draft / reserved) in `LEVEL-STATUS.md`. Currently met + for L1-L16; L11/L12 draft, L17 reserved. +* *Grade B tightening:* The verifier crate's `verify.rs` MUST be + paired with a published soundness theorem covering the + load-bearing levels. A10 closure (`VerifierSpecAgreement` + + `SourceVerifierAgreement`) is the start; preservation-style + theorems for each level are next. +* *Grade A tightening:* Every level L1-L17 has a Qed soundness + theorem; verifier is a refinement of the Idris2 ABI. + +These tightenings are *additional* to the baseline — none of the +baseline evidence is waived. + +== Canonical Proof Suite extension + +typed-wasm is a verified compilation target. Its Canonical Proof +Suite extension lives at `src/abi/TypedWasm/ABI/` (Idris2): + +* Level theorems: `Levels.idr`, `Region.idr`, `Lifetime.idr`, + `Effects.idr`, `Layout.idr`, `Linear.idr`, `Pointer.idr`, + `Tropical.idr`, `Epistemic.idr` +* Module-discipline theorems: `ModuleIsolation.idr`, + `SessionProtocol.idr`, `ResourceCapabilities.idr`, + `Choreography.idr` +* Composition: `Echo.idr`, `MultiModule.idr`, `TypedAccess.idr` +* Bridge: `Proofs.idr`, `VerifierSpec.idr`, `ABI.idr`, `Types.idr`, + `Stdlib.idr` +* Concrete-feature corpus: `AirborneSubmarineSquadron.idr` +* Layout-side: `src/abi/Layout/{Types,ABI,Stdlib, + AirborneSubmarineSquadron}.idr` + +Proof debt + non-trivial gaps tracked at `PROOF-NEEDS.md` ++ `docs/proof-debt.md`. + +== What is NOT yet met (honest gaps) + +Gating gaps for grade *B*: + +* *Per-level preservation theorems*. Most safety claims are + structural consequences of the Idris2 type encoding; explicit + preservation lemmas exist for L13-L16 (per LEVEL-STATUS) but + L1-L10 are not separately stated. PROOF-NEEDS.md is the load- + bearing handoff document. +* *L11 (Tropical) and L12 (Epistemic)* are draft-only at v1.1 + and have not promoted to checked-in-package. +* *Verifier ↔ specification refinement theorem* not yet stated as + a single citable lemma (A10 closure inhabits the agreement record + but the formal refinement claim is implicit). + +== Path to next grade (*B*) + +* State + prove per-level preservation lemmas for L1-L10 in + Idris2. (~weeks per level, ongoing) +* Promote L11 and L12 from draft to checked. (~independent of + L13-L16 trajectory) +* Land an explicit verifier-spec refinement theorem citing the + A10 agreement records. + +*Realistic timeline estimate:* 3-6 months. + +== Path to grade beyond that (*A*) + +* Every level has a Qed soundness theorem. +* `typed-wasm-verify` published to crates.io. +* External adopter not maintained by hyperpolymath. + +== Demotion risk + +* *Lowest:* `typed-wasm-verify` CI flips to red. +* *Medium:* A consumer language's CI flags a typed-wasm release + as breaking; the breakage is recorded but rollback delayed. +* *Catastrophic:* The A10 agreement records (`VerifierSpecAgreement` + + `SourceVerifierAgreement`) are found to be inhabitable only + via a hidden axiom or `believe_me` — would force TRG demotion + and FRG demotion in lockstep. + +== Iteration history + +[cols="1,1,4", options="header"] +|=== +| Date | Grade | Notes + +| 2026-05-28 | C | Initial TRG assessment per TRG v1.0. Compilation target treated as language-shaped artefact; the strong M5 + Idris2 ABI surface carries the grade. +|=== + +== Review cycle + +* *Routine:* Reassess on every release cycle (per TRG §8). +* *Immediate:* Reassess within 7 days of any MUST-component + regression. +* *VeriSimDB drift alert:* Reassess within 24 hours. + +== Footer + +Run `just trg-badge` in this repo to generate the shields.io badge.