From 60b7e63e95b6a2de54f1911ca382cd08fe9ee3ec Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 29 Jul 2026 07:45:19 +0100
Subject: [PATCH] docs(testing): tests and benches must be drawn from
 proven-tests-and-benches first

The taxonomy defines 16 test categories, 14 aspect dimensions and a benchmark
taxonomy, but said nothing about WHERE an implementation should come from -- and
referenced hyperpolymath/proven-tests-and-benches zero times, despite that repo
holding 38 .idr files and 4 .ipkg of Idris2 tests and benchmarks.

Adds an explicit provenance rule before Part I, with an ordered preference:

  1. proven-tests-and-benches -- the Idris2 suite. Adapt it.
  2. The Appendix C reference implementation.
  3. A sibling repo already assessed at CRG C or better.
  4. Write a new one -- and contribute it BACK, so the next repo inherits it.

Why the Idris2 suite ranks first: a test that type-checks has discharged its
obligation in the type system, so it cannot silently degrade into a test that
passes without asserting anything. And copying a shared test is how a shared
expectation STAYS shared -- writing a fresh one per repo is how sixteen subtly
different definitions of 'the same' test appear, which is the
one-template-copied-N-times failure this estate keeps paying for.

Carries an explicit caution: a test written to make a gate go green rather than
to establish a fact is WORSE than no test, because it is read as evidence. Where
no honest test exists yet, mark the category N/A with justification as Scope
already requires. That is a truthful state; a passing-but-vacuous test is not.

Verified: asciidoctor renders clean.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .../TESTING-TAXONOMY.adoc                     | 34 +++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/testing-and-benchmarking/TESTING-TAXONOMY.adoc b/testing-and-benchmarking/TESTING-TAXONOMY.adoc
index 44415fbe..077b8589 100644
--- a/testing-and-benchmarking/TESTING-TAXONOMY.adoc
+++ b/testing-and-benchmarking/TESTING-TAXONOMY.adoc
@@ -35,6 +35,40 @@ This taxonomy applies to every assessable component in the hyperpolymath estate.
 A component must declare which categories apply and demonstrate evidence for each.
 Categories that do not apply must be explicitly marked N/A with justification.
 
+
+=== Provenance: draw from `proven-tests-and-benches` FIRST
+
+IMPORTANT: Before writing a new test or benchmark for any category or aspect
+below, look for an existing one in the *Idris2 suite* at
+https://github.com/hyperpolymath/proven-tests-and-benches[`hyperpolymath/proven-tests-and-benches`].
+That repository is the *first* place to draw from — ahead of this document's
+examples, ahead of a sibling repo, and ahead of writing something new.
+
+Why it ranks first:
+
+* The suite is *proven*, not merely present. An Idris2 test that type-checks has
+  discharged its obligation in the type system, so it cannot silently degrade
+  into a test that passes without asserting anything.
+* Copying a test is how a shared expectation stays shared. Writing a fresh one
+  per repo is how 16 subtly different definitions of "the same" test appear —
+  the one-template-copied-N-times failure this estate keeps paying for.
+* It gives a category a single reference answer, so "does this repo satisfy
+  category 3?" has one meaning estate-wide.
+
+Order of preference when instantiating any category in Part I, any aspect in
+Part II, or any benchmark in Part IV:
+
+. `proven-tests-and-benches` — the Idris2 suite. Adapt it.
+. The reference implementation in Appendix C.
+. A sibling repo already assessed at CRG C or better.
+. Write a new one — and contribute it *back* to `proven-tests-and-benches` so
+  the next repo inherits it rather than reinventing it.
+
+CAUTION: A test written to make a gate go green, rather than to establish a
+fact, is worse than no test — it is read as evidence. If no honest test exists
+for a category yet, mark it N/A with justification, as Scope requires above.
+That is a truthful state; a passing-but-vacuous test is not.
+
 == Part I: Test Categories
 
 === 1. Unit Tests