Proven-Tests: Type-Safe and Beyond Testing Framework

Overview

Proven-Tests is the testing framework for the hyperpolymath ecosystem, implemented in Idris2. Its organising idea: a test’s warrant — the strength of evidence behind it — is a first-class, machine-checked value, not a label. Coverage is likewise derived from executed tests at typed coordinates, so a claimed-covered cell cannot be faked.

Key principles:

• Tests are written in Idris2; provenance is evidence-carrying by construction (src/ProvenTests/Types.idr: an Actually-Proven classification requires a non-empty proof ladder — the type system rejects the claim without the evidence)

• Three-tier classification: Actually-Proven, Provisionally-Proven, Unproven (see docs/CHARACTERISTICS.adoc for the evidence-spectrum philosophy: example → property → proof)

• A 17-category × 14-aspect test taxonomy, traversed as a co-creation lattice (docs/ZIGZAG-REGIMEN.adoc). NOTE: the estate standard defines 16 categories; the 17th, TypeSafeTest, is a local extension to this repository and exists in no standard. The drift is intentional but unratified — see DEBT.md S-4.

• A machine-checked tropical (min-plus) semiring for cost-aware test routing (src/ProvenTests/Tropical.idr — total proofs, no escape hatches)

• Honest status reporting: see docs/STATE-OF-THINGS.adoc (the self-audit) and READINESS.adoc (Component Readiness Grade)

Classification System

Tier 1: Actually-Proven

Tests backed by a full proof ladder: the property holds for all inputs because a total, machine-checked proof exists. Example in-repo: the tropical semiring laws (ProvenTests.Baton.tropicalLawsClassification cites the theorems in Tropical.idr by name).

Tier 2: Provisionally-Proven

Tests whose framework and assertions are type-safe (totality-checked Idris2, typed assertions) but whose subject property is demonstrated by example or property checks rather than proof. Most of this repo’s suite sits here — and says so.

Tier 3: Unproven

Regular tests without type-safety guarantees. The goal is to migrate all tests to at least Provisionally-Proven.

Type-Safe Testing Categories

Specialized testing for advanced type systems. Source names the type theory that inspired each category; except where noted, the implementations here are self-contained Idris2 property suites, not live integrations.

Category	Description	Inspiration
Tropical	Min-plus semiring resource bounds	typed-wasm extension
Epistemic	Information-theoretic access control	typed-wasm extension
Choreographic	Multi-party session types	TypeLL
Dependent	Dependent type verification	Idris2 core
Effects	Effect system properties	Idris2 core
Decorative	Type-level annotations	Custom
Ceremonial	Protocol/ritual types	Custom
Dyadic	Binary relation types	Custom
Echo-Types	Stand-in contract for future echo-types integration (see note)	echo-types repo

Note	The Echo-Types "bridge" (src/ProvenTests/TypeSafe/Bridge.idr) is a stand-in: a hardcoded contract record with structural checks. There is no dependency on the echo-types repository yet, and its tests are graded accordingly (nothing above Provisionally-Proven).

Repository Structure

proven-tests-and-benches/
├── README.adoc
├── READINESS.adoc            # Component Readiness Grade (estate CRG convention)
├── Justfile                  # build/test/bench/ci recipes (real, working)
├── proven-tests.ipkg         # the framework library + self-test executable
├── proven-tests-suite.ipkg   # type-safe category test suite (depends = proven-tests)
├── proven-spec-suite.ipkg    # Proven laws, AffineScript, HigherOrder, SetTheory
├── benchmarks/benchmark.ipkg # the benchmark harness
├── integrations/proven/…ipkg # the external-subject report
│                             # (five packages in total, not one)
├── DEBT.md                   # every known gap, with the command that found it
├── ROADMAP.md                # what happens next, and why in that order
├── TEST-NEEDS.md             # every category graded REAL / THIN / ABSENT
├── PROOFS.adoc               # the proof catalogue, per suite
├── ARCHITECTURE.md           # structure + a standing list of known defects
├── AGENTS.md                 # read this before changing anything with an agent
├── src/ProvenTests/          # 32 modules: the framework
│   ├── Types.idr             # evidence-carrying provenance (the core idea)
│   ├── Classification.idr    # tier constructors and honest promotion
│   ├── Taxonomy.idr          # 17 categories × 14 aspects × 12 kategoria levels
│   ├── Tropical.idr          # machine-checked min-plus semiring (total proofs)
│   ├── Zigzag.idr            # co-phase × actor × category × aspect lattice
│   ├── Baton.idr             # cross-repo contract: coord + provenance + cost
│   ├── Coverage.idr          # self-deriving coverage (cannot be faked)
│   ├── Cells.idr             # the populated lattice cells (real tests)
│   ├── Framework.idr         # Runnable interface, suites, assertions
│   ├── Runners.idr           # comprehensive suite runner
│   ├── Report.idr            # report types
│   ├── Main.idr              # self-test entry point
│   └── TypeSafe/             # 9 category property suites + Bridge stand-in
├── tests/TypeSafeTests/      # suite package sources (per-category tests + Main)
├── benchmarks/               # honest benchmark harness (defeats dead-code elim)
├── scripts/                  # install-idris2.sh, ci-build.sh (the CI gate),
│                             # owned-compute-gate.sh, wire-zero-minute-gate.sh
└── docs/                     # CHARACTERISTICS, STATE-OF-THINGS (self-audit),
                              # ZIGZAG-REGIMEN, CROSS-REPO-UNIFICATION, ZERO-MINUTE-CI

Quick Start

Prerequisites

• Idris2 (0.7.0 or later; CI uses scripts/install-idris2.sh)

• Chez Scheme + GMP development libraries

Build and test

git clone https://github.com/hyperpolymath/proven-tests-and-benches
cd proven-tests-and-benches

# Everything, exactly as CI runs it:
bash scripts/ci-build.sh

# Or piecewise:
just build          # idris2 --build proven-tests.ipkg
just test           # self-test suite + type-safe suite package
just bench          # benchmark harness

Using in Your Project

1. idris2 --install proven-tests.ipkg (after building)

2. Add depends = proven-tests to your .ipkg

3. import ProvenTests.Framework and write provenance-graded tests (see tests/TypeSafeTests/ for worked examples)

License

Code is licensed under MPL-2.0; documentation under CC-BY-SA-4.0. See LICENSE and LICENSES/.

Where to look next

Document	What it answers
ARCHITECTURE.md	How the pieces fit — and a standing, maintained list of known architectural defects. The most reliably honest document here.
TEST-NEEDS.md	How good the tests actually are. Every category graded REAL / THIN / ABSENT, with the gaps in priority order. Four categories are THIN and say so.
PROOFS.adoc	The proof catalogue: what is machine-checked, per suite.
READINESS.adoc	The Component Readiness Grade, its evidence, and what is not yet met. The single source of truth for the grade. The badge above is generated from it by just crg-badge and must not be hand-edited; CI does not yet enforce that agreement, which is ROADMAP.md item 2b.
DEBT.md	Every known gap across licence, docs, code, proof, test, CI/CD and supply chain, each with the command that produced the evidence.
ROADMAP.md	What happens next and why in that order.
AGENTS.md	The non-negotiables. Read before changing anything with an agent.
docs/CHARACTERISTICS.adoc	What makes a test or benchmark good: the example → property → proof spectrum.
docs/TEST-DOCTRINE.adoc	When a test is admissible at all: the harness/payload split — the harness must never trigger, the payload must always trigger for its declared class — with the silence/firing fixtures, three-outcome checks, certified-absence residue rule and scanner excludability.

Tip	the project wiki carries the conceptual introductions — provenance tiers, the Zigzag lattice, what actually gates. It links to these files rather than restating them, so it cannot drift out of step with the repository.

References

• Idris2

• proven — the verified safety library this framework is being pointed at (see integrations/)

• Standards — estate conventions (CRG grading, licensing)

• echo-types — future integration (stand-in contract only today)