warrantlib

A column of PASS cannot say whether anything was decided. A grid sample over a continuous range and an exhaustive enumeration over a declared finite set can both come back clean. Only the second settled the question. warrantlib is a small vocabulary for keeping that difference in a check suite's output instead of losing it there.

pip install warrantlib

Python 3.10 and up. The standard library is the only dependency.

Warrant

Warrant says how well a claim is warranted, by the prover class behind it.

CERTIFIED sits between the other two. Validated numerics prove a universal over a compact domain, and the proof carries the bound it was computed with. Borrowing PROVED overclaims. Borrowing CORROBORATED throws the bound away.

An action sweep over a continuous range is a finite grid over an infinite domain, so it samples. A policy enumeration over a declared finite set enumerates. The warrant follows from which of those the check did, not from how clean the answer looked.

Outcome

Outcome says what a registered falsifier did. A falsifier does not pass. It fires or it does not, and PASS is absent from the vocabulary rather than disambiguated by a column beside it.

Collapsing the last three loses the survivor accounting, and burns the word a real tie needs. The last two never ran, so they carry no warrant, and CheckReport enforces that.

The rest

Tier says what the check was measured against. EXACT against a closed form, BOUNDED against a stated bar, COMPUTED where there is no bar to state. It cuts across the other two rather than ranking them.

CheckReport is what a check emits. Frozen, because editing a report after the check ran is editing the finding. It refuses PROVED with nothing behind it.

Evidence comes in two kinds, one per decisive prover. CompletenessCertificate backs an exhaustive enumeration, recording the domain it covered against the count it visited. SymbolicReduction backs a theorem or a symbolic identity, and names where the symbolic setup was checked by hand against the analytic problem it stands for. A CAS establishes that one expression equals another. Whether those are the right expressions is a human obligation, and this is where it is discharged rather than assumed.

check_summary prints a run as counts per (warrant, outcome).

Use

from warrantlib import (
    CheckReport, Outcome, SymbolicReduction, Tier, Warrant, check_summary,
)

report = CheckReport(
    name="second gap coefficient",
    warrant=Warrant.PROVED,
    outcome=Outcome.NOT_TRIGGERED,
    tier=Tier.EXACT,
    detail="the CAS reduces the integral to the quoted constant",
    evidence=(
        SymbolicReduction(
            claim="the second gap coefficient equals the quoted constant",
            correspondence="hand derivation, section 3",
            assumptions=("the expansion is formal, not convergent",),
        ),
    ),
)

print(check_summary([report]))

1 registered, 1 tested here, none fired
   PROVED        NOT TRIGGERED   1

Registering four falsifiers and testing two is a different claim from testing four, and one number cannot carry both. The header separates them.

Where it comes from

warrantlib was factored out of cpomdp, where it labels a research programme's falsification battery. It is developed in that repository and released separately. The API reference is at cpomdp.inferogenesis.com/api/warrant.