diff --git a/testing-and-benchmarking/TESTING-TAXONOMY.adoc b/testing-and-benchmarking/TESTING-TAXONOMY.adoc index 077b8589a..4af8a0481 100644 --- a/testing-and-benchmarking/TESTING-TAXONOMY.adoc +++ b/testing-and-benchmarking/TESTING-TAXONOMY.adoc @@ -260,6 +260,61 @@ Can the new API serve old clients? **Applies to:** Every repo with formal proofs. +=== 17. Type-Safe Tests + +**Definition:** Verify that a property is enforced by the *type system* rather than by a +runtime assertion — the test is that the ill-typed program does not compile. The canonical +form is a negative witness: a deliberately wrong expression inside a compiler-checked +`failing` block that pins the expected error text, so the rejection cannot be satisfied by +an unrelated error such as a typo or a scope mistake. + +**Purpose:** A runtime check can be skipped, mocked, compiled out, or simply never reached. +A type-level obligation cannot. Category 17 records the properties a repo has moved from +the first class to the second, and prevents a later refactor from silently demoting one. + +**Subcategories** (nine, as implemented in `proven-tests-and-benches`): Tropical, +Epistemic, Choreographic, Dependent, Effects, Decorative, Ceremonial, Dyadic, EchoTypes. + +**Tools:** Idris2 `failing` blocks, Rust `compile_fail` doctests and `trybuild`, Haskell +`ShouldNotTypecheck`, Scala `illTyped`, TypeScript `@ts-expect-error`, Lean `#guard_msgs`. + +**Applies to:** Any repo in a language with a type system strong enough to carry the +property. Required from CRG C+ where the repo claims type-level guarantees in its README. + +**⚠ Pin the error text, not merely the failure.** A negative test that asserts only "this +does not compile" passes for every reason including the wrong one, and is a fake gate. + +=== 18. Coupling / Drift-freedom Tests + +**Definition:** Verify that two or more artefacts which must agree *do* agree, where +nothing in the build already forces them to. The artefacts are independently editable and +their agreement is maintained by discipline alone: mirror enums, a hand-written list that +is supposed to enumerate a type, a serde implementation beside a custom `Display`, a +redundant parser, a count asserted in both code and documentation, a lockfile beside the +manifest it pins. + +**Purpose:** Drift between two copies of one fact is silent by construction — each copy is +internally consistent, the build is green, and the disagreement surfaces only when a reader +trusts the stale one. This is the failure mode least likely to be caught by any other +category, because every other category tests one artefact against its own specification. + +**Tools:** Generated-vs-committed diffs (generate the second copy at test time and compare), +exhaustiveness proofs linking a list literal to its enum (Idris2 `Data.List.Elem`, Rust +`strum::EnumIter`, Haskell `Bounded`/`Enum`), schema round-trip properties, and +manifest-derived fixtures shared by both sides. + +**Applies to:** Every repo holding the same fact in two editable places. In practice this is +nearly all of them, which is why the category exists. + +**Relationship to Part VI.** CR-1 (mirror-enum drift), CR-2 (foreign-enum exhaustive-match +lint) and CR-9 (schema-surface drift detector) are the *cross-repo* instances of this +category; Category 18 is its repo-local form. A repo may satisfy 18 internally and still +fail CR-1 against an upstream. + +**⚠ The strongest form deletes rather than reconciles.** Where one of the two copies has no +consumers, the correct repair is to remove it and let the type system carry the fact once. +A drift test over a duplicate that did not need to exist institutionalises the duplication. + == Part II: Aspect Test Dimensions Aspect tests are cross-cutting non-functional concerns. Each aspect can be tested @@ -747,10 +802,15 @@ with a `fixtures/` or `corpora/` directory. Recorded at the same time as the cross-repo ideas above, things that feel under-specified in this document itself: -- **No "coupling test" category.** Tests that assert drift-freedom between - two independent artefacts (mirror enums, redundant parsers, serde + custom - Display, etc.) don't fit cleanly into the 16 categories. Proposal: add - Category 17 "Coupling / Drift-freedom" in v1.1. +- ✅ **RESOLVED 2026-09-14 — "coupling test" category added as Category 18.** + The original note read: *"Tests that assert drift-freedom between two independent + artefacts (mirror enums, redundant parsers, serde + custom Display, etc.) don't fit + cleanly into the 16 categories. Proposal: add Category 17 'Coupling / Drift-freedom' + in v1.1."* The proposal is adopted and promoted to a full normative section, but + numbered **18**, not 17: `TypeSafeTest` had already shipped as Category 17 in + `proven-tests-and-benches` before this proposal was ratified, and is itself now + ratified here as § 17. Appending at 18 renumbers no shipped code and changes the + meaning of no already-serialised artefact. - **Proof-regression is single-prover.** Category 16 catches "Coq no longer accepts proof P" but not "Coq and Lean give different counterexamples for the same formula". Cross-prover regression deserves its own sub-category. @@ -797,6 +857,8 @@ under-specified in this document itself: | Chaos/Resilience | CHS | B+ (if applicable) | Compatibility | CMP | B+ (if applicable) | Proof Regression | PRF | C+ (if proofs exist) +| Type-Safe | TSF | C+ (if the language carries the property) +| Coupling/Drift-freedom | CDF | C+ |=== == Appendix B: Aspect Quick Reference @@ -827,6 +889,8 @@ The **K9 Coordination Protocol** (`standards/k9-coordination-protocol/`) serves reference implementation for this taxonomy. It demonstrates: - **Full blitz assessment** against all 16 test categories and 14 aspect dimensions + that existed at the time of assessment (Categories 17 and 18 were ratified later, + on 2026-09-14, and K9 has not yet been reassessed against them) - **79 tests** across 8 test files covering 9 applicable categories (7 N/A with justification) - **Mutation testing** with 15 mutations (9 killed, 6 documented equivalents, 100% applicable score) - **Six Sigma benchmarks** baselined on real hardware diff --git a/toolchain-readiness-grades/README.adoc b/toolchain-readiness-grades/README.adoc index 9f740d01c..be82f2bee 100644 --- a/toolchain-readiness-grades/README.adoc +++ b/toolchain-readiness-grades/README.adoc @@ -95,7 +95,7 @@ E:: pre-alpha. All Must passed. Banned constructs ZERO. panic-attack D:: pre-alpha+. All Must + Should + the *Canonical Proof Suite* (this is the foundational gate). RSR-FULL. panic-attack zero across all severities. Fuzzing harness exists. -C:: *alpha*. All Must + Should + Could. Full Testing-Taxonomy 16×14 +C:: *alpha*. All Must + Should + Could. Full Testing-Taxonomy 18×14 coverage in Six Sigma range. Continuous fuzzing 14d. 5 fully-proven programs. 3-nines on top-4 priority axes. B:: *beta*. All four tiers passed. Multi-prover cross-validation (≥2 of diff --git a/toolchain-readiness-grades/SELF-ASSESSMENT.adoc b/toolchain-readiness-grades/SELF-ASSESSMENT.adoc index ef81cc95b..daefcac7b 100644 --- a/toolchain-readiness-grades/SELF-ASSESSMENT.adoc +++ b/toolchain-readiness-grades/SELF-ASSESSMENT.adoc @@ -91,7 +91,7 @@ standard's gate to leave grade E is unenforceable in practice. After grade D, the path to C requires: . *All Could rows PASSED.* -. *Full Testing-Taxonomy 16 × 14 coverage* per +. *Full Testing-Taxonomy 18 × 14 coverage* per `testing-and-benchmarking/TESTING-TAXONOMY.adoc`. . *Six-Sigma test passing* — all tests in the Six-Sigma range (≤ 3.4 failures per million test runs) for at least 14 consecutive diff --git a/toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.a2ml b/toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.a2ml index a4321986e..8efd24a0a 100644 --- a/toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.a2ml +++ b/toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.a2ml @@ -61,8 +61,8 @@ (release-stage "alpha") (stability-posture "stable-in-home-context") (ordinal 4) - (description "Alpha gate. All Could rows. Full Testing-Taxonomy 16x14 in Six-Sigma range for >=14 days. Continuous fuzzing 14 days. 5 fully-proven programs. 10 dogfood users meeting diversity-metrics. 3-nines on top 4 priority axes. VeriSimDB instance present.") - (evidence-required "all D + Could rows + Testing-Taxonomy 16x14 in Six-Sigma range 14 days + fuzz 14 days + 5 fully-proven programs + 10 dogfood users meeting diversity-metrics + 3-nines on dependability/security/interop/usability + VeriSimDB instance + launch-scaffolder mint wired + Stapeln containers") + (description "Alpha gate. All Could rows. Full Testing-Taxonomy 18x14 in Six-Sigma range for >=14 days. Continuous fuzzing 14 days. 5 fully-proven programs. 10 dogfood users meeting diversity-metrics. 3-nines on top 4 priority axes. VeriSimDB instance present.") + (evidence-required "all D + Could rows + Testing-Taxonomy 18x14 in Six-Sigma range 14 days + fuzz 14 days + 5 fully-proven programs + 10 dogfood users meeting diversity-metrics + 3-nines on dependability/security/interop/usability + VeriSimDB instance + launch-scaffolder mint wired + Stapeln containers") (minimum-for "alpha")) (grade (code B) diff --git a/toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.adoc b/toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.adoc index 62ace4e4b..6d4ed4a78 100644 --- a/toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.adoc +++ b/toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.adoc @@ -75,7 +75,7 @@ or relax any TRG-baseline requirement. * *RSR* — Rhodium Standard Repositories baseline. * *Immaculate Guide* — `immaculate-guide/IMMACULATE-GUIDE.adoc`. * *Testing Taxonomy* — `testing-and-benchmarking/TESTING-TAXONOMY.adoc` - (16 categories × 14 aspects × 4 proof systems × 12 type levels). + (18 categories × 14 aspects × 4 proof systems × 12 type levels). * *Standing priority order* (all hyperpolymath work, ranked): `dependability > security > interop > usability > performance > versatility > functional-extension`. @@ -265,7 +265,7 @@ Repository discipline:: All grade-D requirements carried forward, plus Tests:: Every Could row has a behavioural test; component is dogfooded by the project's own CI on every push. CI green for at least 7 consecutive days at assessment time. *Full Testing-Taxonomy - coverage* — 16 categories × 14 aspects (per + coverage* — 18 categories × 14 aspects × 4 proof systems × 12 type levels (per `testing-and-benchmarking/TESTING-TAXONOMY.adoc`) wired up and passing for the component. Six-Sigma test passing:: All passing tests above MUST be in the *Six