Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
72 changes: 68 additions & 4 deletions testing-and-benchmarking/TESTING-TAXONOMY.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion toolchain-readiness-grades/README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion toolchain-readiness-grades/SELF-ASSESSMENT.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.a2ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions toolchain-readiness-grades/TOOLCHAIN-READINESS-GRADES.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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`.

Expand Down Expand Up @@ -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
Expand Down
Loading