Warrant

Warrant is a property of the check, not of the number. A grid sample over a continuous action range and an exhaustive enumeration over a declared finite set can both report that no policy flips. Only the second decided it.

Prover	What it does	Label
1	pen-and-paper theorem, within stated hypotheses	PROVED
2	symbolic computation: closed-form identities, algebraic non-existence	PROVED
3 · enumeration	exhaustive enumeration over a finite domain	PROVED, with a completeness certificate
3 · validated	validated numerics over a compact domain	CERTIFIED
3 · sample	sampling a continuum	CORROBORATED

research/warrant_ledger.md carries the canonical version of this table, with the evidence each warrant requires and the tier a number is known to. 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. EFESelector reports CORROBORATED and EnumeratedEfeSearch reports PROVED for that reason.

CERTIFIED sits between the 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.

Warrant

Bases: Enum

How well a claim is warranted, by the prover class that produced it.

PROVED — the claim is decided. A pen-and-paper theorem within its stated hypotheses (Prover 1), a symbolic identity (Prover 2), or a finite domain enumerated in full, where ¬∃ ≡ ∀¬ (Prover 3 · enumeration). Under that last one it is earned only with a completeness certificate. Without one the enumeration is a sample wearing a decision's label.

CERTIFIED — validated numerics prove a universal over a compact domain by construction (Prover 3 · validated). Stronger than a sample, weaker than a decision, and it carries the bound it was computed with. Collapsing it into PROVED overclaims. Collapsing it into CORROBORATED throws the bound away.

CORROBORATED — a sample of a continuum (Prover 3 · sample). It exhibits existence and refutes a universal by counterexample. It never decides one, at any sample count.

Orthogonal to outcome. A check reports both, and the three levels print in distinct vocabulary so a corroborative green run is visibly that.

What a check emits

A registered 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.

Outcome has five values because five things can happen to a falsifier, and they are not interchangeable. It ran and did not fire, so the claim survives it. It fired, and the refutation is the result. It ran and the ordering came out genuinely undetermined, because the two quantities' intervals overlap. It was void by construction and could not have fired here, so it is evidence for nothing and is not a survivor. Or it was measured elsewhere and did not run here at all. Collapsing the last three loses the survivor accounting, and burns the word a real tie needs.

Tier says what the check was measured against, and cuts across the other two rather than ranking them. An EXACT closed-form reference can be sampled, and an exhaustive enumeration can produce a COMPUTED number.

A report carries two names. name is prose and reads in a summary line, so it is reworded whenever the wording improves. check_id is the key: dot-separated segments of letters, digits and underscores, refused at construction if anything else appears in it. The separation is what lets a manifest declare a check before the run and a later run be joined to an earlier one. Deriving the key from the prose would tie the two together, and the first reworded name would read as one check dropped and one added.

A check that never ran carries no warrant. CORROBORATED means sampling-grade evidence was obtained, so attributing it to a falsifier that sampled nothing claims evidence that does not exist. The warrant is None there and prints as —, enforced at construction.

A PROVED report needs evidence, enforced at construction. There are two families, one per decisive prover. CompletenessEvidence backs an exhaustive enumeration over a finite domain, and its leaves differ only in the shape of that domain. SymbolicReduction backs a theorem or a symbolic identity (Provers 1 and 2), which decide by argument and enumerate nothing, so a certificate is the wrong evidence for them rather than a missing one. The weaker levels need none, because a bound and a sample carry their story in detail. Report PROVED with nothing behind it and the constructor raises.

Those two families are the only things the evidence tuple accepts. A path naming where the proof lives is the plausible substitute, and it satisfies a presence check exactly as well as a certificate does. So the constructor checks every item's kind. Checking only the first would let a claim over several enumerations carry one certificate and three references to a write-up. The weaker levels are held to the same rule. They need no evidence, so a tuple on one of them is something the report says it is carrying.

Outcome

Bases: Enum

What a registered falsifier did, independent of how well it was warranted.

A falsifier does not pass. It fires or it does not, and the words are chosen so that a run cannot be read as a column of PASS with the interesting distinctions flattened out of it.

NOT_TRIGGERED — it ran, the condition did not obtain, the claim survives it. FIRED — the condition obtained. The claim is refuted, and that is the result. NOT_RESOLVED — it ran and the ordering is genuinely undetermined, because the two quantities' intervals overlap. Narrow on purpose: this is a measured tie, not a stand-in for a check that did not run. NOT_APPLICABLE — void by construction. It could not have fired here, so it is evidence for nothing and does not count among the survivors. NOT_RUN_HERE — measured elsewhere, or not yet. The detail says where.

The last two never ran, so they carry no warrant. CheckReport enforces that.

Tier

Bases: Enum

What the check was measured against.

EXACT — a closed-form reference at machine precision. BOUNDED — a stated bar, or a certified bracket. COMPUTED — no statable bar. The word for such a number is computed, never certified.

Cuts across warrant and outcome rather than ranking them. An EXACT reference can be sampled (Prover 3 · sample) and a COMPUTED number can come out of an exhaustive enumeration (Prover 3 · enumeration).

A completeness claim has two predicates and several possible domains. CompletenessEvidence holds the predicates: expected is the declared set's own cardinality, and visited reaches it. Each leaf under it says what its domain means and nothing else, so the PROVED gate is written once and a leaf cannot weaken it by forgetting to run it.

CompletenessCertificate is a tree, |A|^H over one versioned action set. ProductCompletenessCertificate is a cross, the product of declared axes. A bare count distinguishes neither: 81 is 9**2 and 3**4, and 12 is 3 x 4 and 2 x 6. Both carry their factors and their versions, so an addition after results are seen shows up in the diff.

CompletenessEvidence dataclass

CompletenessEvidence(
    expected: int, visited: int, warrant: Warrant
)

Bases: ABC

Evidence a finite domain was enumerated in full, whatever shape the domain is.

Two independent facts, and a PROVED claim needs both. Domain: expected is the declared set's own cardinality, so the set quantified over is the declared one. Coverage: visited == expected, so it was enumerated in full. They come apart wherever visited is a loop-carried counter rather than an array's length, which is where a padding bug lives, and coverage alone is what carries the Prover 3 · enumeration licence.

A leaf says what its domain means and nothing else. The gate is held here once, so a leaf cannot weaken it by forgetting to run it. A leaf defining its own __post_init__ is refused at class creation for the same reason.

A partial enumeration sampled its set, so its warrant is CORROBORATED. Pairing PROVED with a shortfall does not construct.

Parameters:

Name	Type	Description	Default
expected	int	the count the claim was obliged to visit, supplied rather than derived, so the domain check compares two routes.	required
visited	int	how many it actually visited.	required
warrant	Warrant	the prover class the enumeration earns.	required

Raises:

Type	Description
ValueError	if the warrant is PROVED and either precondition fails.

domain_declared abstractmethod property

domain_declared: bool

Whether expected is the cardinality the declared domain gives.

set_description abstractmethod property

set_description: str

The declared set in one line, for the error that says it disagrees.

complete property

complete: bool

Whether every expected member was visited.

__init_subclass__

__init_subclass__(**kwargs: object) -> None

Refuse a leaf that validates itself.

Parameters:

Name	Type	Description	Default
**kwargs	object	whatever the class statement passed along.	{}

Raises:

Type	Description
TypeError	if the leaf's own body defines __post_init__.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __init_subclass__(cls, **kwargs: object) -> None:
    """Refuse a leaf that validates itself.

    Args:
        **kwargs: whatever the class statement passed along.

    Raises:
        TypeError: if the leaf's own body defines ``__post_init__``.
    """
    super().__init_subclass__(**kwargs)
    if "__post_init__" in cls.__dict__:
        raise TypeError(
            f"{cls.__name__} defines __post_init__, and validation lives in "
            "CompletenessEvidence. A leaf that defines its own shadows the base's, "
            "so the PROVED preconditions stop running and no test of that leaf "
            "would notice. Override _validate_declaration instead."
        )

__post_init__

__post_init__() -> None

Reject a PROVED certificate failing domain or coverage.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __post_init__(self) -> None:
    """Reject a ``PROVED`` certificate failing domain or coverage."""
    self._validate_declaration()
    if self.warrant is not Warrant.PROVED:
        return
    if not self.domain_declared:
        raise ValueError(
            f"a PROVED certificate must quantify over the declared set, got "
            f"expected={self.expected} against {self.set_description}. "
            "The count and the set have come apart."
        )
    if not self.complete:
        raise ValueError(
            f"a PROVED certificate must be complete, got expected="
            f"{self.expected} against visited={self.visited}. A partial "
            "enumeration sampled its set, so its warrant is CORROBORATED."
        )

CompletenessCertificate dataclass

CompletenessCertificate(
    expected: int,
    visited: int,
    warrant: Warrant,
    action_set_size: int,
    horizon: int,
    action_set_version: str,
)

Bases: CompletenessEvidence

A domain enumerated as a tree: expected == |A|^H (ADR-030).

The certificate names its set. expected on its own conflates the base with the exponent — 81 is 9**2 and 3**4 — so a bare count is not self-describing and two certificates over different sets cannot be told apart. Carrying the size, the horizon and the version fixes that at the type rather than in the surrounding prose (standing prohibition 9).

Parameters:

Name	Type	Description	Default
expected	int	the policy count the search was obliged to visit — |A|^H, supplied rather than derived, so the domain check compares two routes.	required
visited	int	how many it actually visited.	required
warrant	Warrant	the prover class the enumeration earns.	required
action_set_size	int	the declared action count — |A|.	required
horizon	int	the sequence length — H.	required
action_set_version	str	the declared set's version tag.	required

Raises:

Type	Description
ValueError	if the warrant is PROVED and either precondition fails.

domain_declared property

domain_declared: bool

Whether expected is the declared set's own |A|^H.

set_description property

set_description: str

The tree the count is checked against, and the set it was declared on.

__str__

__str__() -> str

The certificate as a one-line warrant string in its own vocabulary.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __str__(self) -> str:
    """The certificate as a one-line warrant string in its own vocabulary."""
    return (
        f"{self.warrant.value} (set {self.action_set_version}, "
        f"|A|^H = {self.action_set_size}^{self.horizon} = {self.expected}, "
        f"visited {self.visited})"
    )

AxisDeclaration dataclass

AxisDeclaration(name: str, size: int, version: str)

One axis of a product domain: what it is, how many, and which version.

Parameters:

Name	Type	Description	Default
name	str	what the axis ranges over, non-empty.	required
size	int	its member count, at least one.	required
version	str	the declared set's version tag, non-empty, so a member added after results are seen shows up in the diff (standing prohibition 9).	required

Raises:

Type	Description
ValueError	on an empty name, an empty version, or a size below one.

__post_init__

__post_init__() -> None

Reject an unnamed, unversioned or empty axis.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __post_init__(self) -> None:
    """Reject an unnamed, unversioned or empty axis."""
    if not isinstance(self.name, str) or not self.name:
        raise ValueError(
            "name must be a non-empty string — an axis nobody can name is not a "
            "declared set"
        )
    if not isinstance(self.version, str) or not self.version:
        raise ValueError(
            f"version must be a non-empty string — the axis {self.name!r} is "
            "declared and versioned"
        )
    if self.size < 1:
        raise ValueError(
            f"the axis {self.name!r} has size {self.size}; an axis with no members "
            "contributes nothing to enumerate and empties the product"
        )

ProductCompletenessCertificate dataclass

ProductCompletenessCertificate(
    expected: int,
    visited: int,
    warrant: Warrant,
    axes: tuple[AxisDeclaration, ...],
)

Bases: CompletenessEvidence

A domain enumerated as a cross: expected is the product of the axis sizes.

A product needs its factors for the reason a tree needs its base and exponent. 12 is 3 × 4 and 2 × 6, so a bare count says neither which axes were crossed nor which version of each. Every axis carries its own version, so an axis that gained a member after results were seen shows up in the diff (standing prohibition 9).

One axis is legal. A ladder or a seed list is a product of one, and reporting it here keeps it in the same vocabulary as the cross it will later join.

Parameters:

Name	Type	Description	Default
expected	int	the cell count the enumeration was obliged to visit, supplied rather than derived, so the domain check compares two routes.	required
visited	int	how many it actually visited.	required
warrant	Warrant	the prover class the enumeration earns.	required
axes	tuple[AxisDeclaration, ...]	the declared axes, at least one.	required

Raises:

Type	Description
ValueError	if axes is not a tuple, is empty, or holds anything but an AxisDeclaration, or if the warrant is PROVED and either precondition fails. The shape checks are ValueError rather than TypeError because every other malformed field here is, and because the failures they replace are a silent unequal round-trip and an AttributeError raised from inside domain_declared.

domain_declared property

domain_declared: bool

Whether expected is the product of the declared axis sizes.

set_description property

set_description: str

The cross the count is checked against, naming every axis and version.

The product the axes give, not the count the certificate declares. This is the right-hand side of the disagreement the domain error reports.

__str__

__str__() -> str

The certificate as a one-line warrant string in its own vocabulary.

The count rendered is expected, the declared one, so a certificate whose declaration disagrees with its axes shows the disagreement rather than hiding it behind the product. The tree leaf renders its own expected likewise.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __str__(self) -> str:
    """The certificate as a one-line warrant string in its own vocabulary.

    The count rendered is ``expected``, the declared one, so a certificate whose
    declaration disagrees with its axes shows the disagreement rather than hiding
    it behind the product. The tree leaf renders its own ``expected`` likewise.
    """
    return (
        f"{self.warrant.value} ({self._factors} = {self.expected}, "
        f"visited {self.visited})"
    )

CheckReport dataclass

CheckReport(
    name: str,
    check_id: str,
    warrant: Warrant | None,
    outcome: Outcome,
    tier: Tier,
    detail: str,
    evidence: tuple[Evidence, ...] = (),
    provenance: tuple[Provenance, ...] = (),
)

One check's result: what it found, how well, and against what.

A record rather than a return value. Frozen, because editing a report after the check ran is editing the finding.

Parameters:

Name	Type	Description	Default
name	str	which check this is, as it appears in the summary.	required
check_id	str	the same check as a key, in dot-separated segments of letters, digits and underscores. The name is prose and is reworded; this is what a manifest declares and what two runs are joined on, so it is not.	required
warrant	Warrant | None	the prover class behind the claim, or None where the check produced no evidence to classify.	required
outcome	Outcome	what the falsifier did.	required
tier	Tier	what the check was measured against.	required
detail	str	why it reports what it reports, in one line. Required, so a report cannot be a bare outcome with extra fields.	required
evidence	tuple[Evidence, ...]	what backs the claim, as a tuple of CompletenessEvidence and SymbolicReduction. Required non-empty when the warrant is PROVED and unused otherwise. A tuple rather than one item because a claim quantified over several enumerations rests on all their certificates, and carrying one of them understates what was checked. Which completeness leaf each one is says what shape its domain had, and nothing here branches on it.	()
provenance	tuple[Provenance, ...]	which ref registered the claim and which one measured it, as a tuple. Required non-empty when the warrant is PROVED, unused otherwise. A tuple on the same argument the evidence is one: a claim resting on two registrations rests on both, and carrying one of them understates what a reviewer has to check.	()

Raises:

Type	Description
ValueError	if the warrant is PROVED and no evidence or no provenance was given, if a check that never ran here carries a warrant anyway, if the evidence or the provenance is not a tuple, or if an item in either is not one of the kinds it accepts.

__post_init__

__post_init__() -> None

Reject a claim with nothing behind it, at either of two strengths.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __post_init__(self) -> None:
    """Reject a claim with nothing behind it, at either of two strengths."""
    subject = f"check {self.name!r}"
    _reject_unreadable(
        subject,
        "name",
        self.name,
        "A row nobody can attribute is a result with no claim beside it, and it "
        "reads in the summary as a blank where the check should be.",
    )
    _reject_unreadable(
        subject,
        "detail",
        self.detail,
        "A report with no reason is the bare outcome this field exists to stop, "
        "and the outcome alone says what happened without saying what was found.",
    )
    _reject_unreadable(
        subject,
        "check_id",
        self.check_id,
        "The id is what a manifest declares and what joins one run's report to "
        "the next. A report without one is reconcilable with nothing.",
    )
    if not _CHECK_ID.fullmatch(self.check_id):
        raise ValueError(
            f"{subject} has check_id={self.check_id!r}, which is not a key. An id "
            "is dot-separated segments of letters, digits and underscores, as in "
            "gap_series.c2_closed_form or R10.crossover_flip. The prose name is "
            "the other field. A key carrying prose moves whenever the prose is "
            "reworded, and a ledger comparing two runs then reads one check as "
            "one dropped and one added."
        )
    if not isinstance(self.evidence, tuple):
        raise ValueError(
            f"check {self.name!r} passed evidence as "
            f"{type(self.evidence).__name__}. Evidence is a tuple, so a claim "
            "resting on several enumerations can carry all of their certificates. "
            "Wrap a single one: (certificate,)."
        )
    if self.evidence:
        for item in self.evidence:
            if not isinstance(item, _EVIDENCE_TYPES):
                raise ValueError(
                    f"check {self.name!r} carries a "
                    f"{type(item).__name__} as evidence. There are two "
                    "families, one per decisive prover: a CompletenessEvidence for "
                    "an exhaustive enumeration (Prover 3 · enumeration), whose "
                    "leaves are CompletenessCertificate over a tree and "
                    "ProductCompletenessCertificate over a cross, and a "
                    "SymbolicReduction for a theorem or a symbolic identity "
                    "(Provers 1 and 2). Anything "
                    "else satisfies the PROVED precondition by being present and "
                    "backs nothing."
                )
    if not isinstance(self.provenance, tuple):
        raise ValueError(
            f"check {self.name!r} passed provenance as "
            f"{type(self.provenance).__name__}. Provenance is a tuple, so a claim "
            "resting on two registrations can carry both. Wrap a single one: "
            "(provenance,)."
        )
    for item in self.provenance:
        if not isinstance(item, Provenance):
            raise ValueError(
                f"check {self.name!r} carries a {type(item).__name__} as "
                "provenance. A bare ref, or a sentence saying the bar came first, "
                "satisfies the precondition by being present and leaves a reviewer "
                "with one end of an ordering and no way to check it. Pass a "
                "Provenance, which validates both refs and says what was "
                "registered at the first of them."
            )
    if self.warrant is Warrant.PROVED and len(self.evidence) == 0:
        raise ValueError(
            f"check {self.name!r} reports PROVED with no evidence. A decided "
            "universal needs something statable behind it: a completeness "
            "certificate for an exhaustive enumeration (Prover 3 · enumeration), a "
            "SymbolicReduction for a theorem or a symbolic identity (Provers 1 "
            "and 2). Report CERTIFIED for a bound over a compact domain, "
            "CORROBORATED for a sample."
        )
    if self.warrant is Warrant.PROVED and len(self.provenance) == 0:
        raise ValueError(
            f"check {self.name!r} reports PROVED with no provenance. A decided "
            "universal says which ref registered the claim and which one measured "
            "it, so a reader can check that the bar was fixed before the number "
            "existed rather than take the ordering on trust. Registering and "
            "measuring at one ref is allowed and renders as such. Report CERTIFIED "
            "or CORROBORATED where there was no registration at all."
        )
    if self.outcome not in _TESTED_HERE and self.warrant is not None:
        raise ValueError(
            f"check {self.name!r} is {self.outcome.value} and carries the warrant "
            f"{self.warrant.value}. It produced no evidence here, so there is no "
            "prover class to report. Leave the warrant None."
        )

__str__

__str__() -> str

The report as one summary line, in the warrant's own vocabulary.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __str__(self) -> str:
    """The report as one summary line, in the warrant's own vocabulary."""
    warrant = self.warrant.value if self.warrant else "—"
    line = (
        f"{self.name}: {self.outcome.value} "
        f"({warrant}, tier {self.tier.value}). {self.detail}"
    )
    if not self.provenance:
        return line
    return f"{line} {' '.join(str(item) for item in self.provenance)}"

Evidence a symbolic claim carries

A CAS is a checker, not a witness. It establishes that one expression equals another, and it has nothing to say about whether those expressions are the ones the analytic claim is about. The warrant ledger records that step as a human obligation, which is the condition on Prover 2 being theorem-grade at all.

SymbolicReduction is where the obligation is discharged rather than assumed. correspondence names where the setup was analytically checked against the problem: a hand derivation by file and line, or a dated registration result. A field that cannot be filled honestly is the signal to report CORROBORATED and say why, so the type is not a formality. Blank fields do not construct.

Blank means blank to a reader rather than empty to str.strip(), which strips the whitespace and leaves the zero-width formatting characters behind. A field that is not text, one holding only whitespace, one holding only zero-width characters, and one carrying a line break into a one-line render are all refused. assumptions is checked entry by entry, and the message names which entry.

assumptions carries the scope. An identity contingent on smoothness, on positivity, or on an expansion being formal rather than convergent is a different claim from one that is not, and the difference belongs beside the evidence instead of in the algebra a reader would have to redo.

SymbolicReduction dataclass

SymbolicReduction(
    claim: str,
    correspondence: str,
    assumptions: tuple[str, ...] = (),
)

What backs a Prover 2 claim: the correspondence a CAS cannot supply.

A CAS checks that one expression equals another. It does not check that those expressions are the ones the analytic claim is about. That step is a human obligation, named as such in the warrant ledger, and this is where it is recorded instead of assumed. A reduction is evidence for CheckReport on the same terms as a completeness certificate, and the two are interchangeable there.

Parameters:

Name	Type	Description	Default
claim	str	the analytic statement, in words, that the symbolic identity stands for.	required
correspondence	str	where the symbolic setup was analytically checked against the problem it stands for. A hand derivation by file and line, or a dated registration result.	required
assumptions	tuple[str, ...]	what the reduction assumed, one condition per entry. The scope travels with the evidence, so the contingency is visible without reading the algebra.	()

Raises:

Type	Description
ValueError	if the assumptions are not a tuple, or if the claim, the correspondence or any assumption is not one-line text with a visible character in it.

__post_init__

__post_init__() -> None

Reject a reduction that records no obligation to have discharged.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __post_init__(self) -> None:
    """Reject a reduction that records no obligation to have discharged."""
    if not isinstance(self.assumptions, tuple):
        raise ValueError(
            "symbolic reduction passed assumptions as "
            f"{type(self.assumptions).__name__}. Assumptions are a tuple, so a "
            "bare string records one condition per character and the identity's "
            "scope reads as gibberish. Wrap a single one: (assumption,)."
        )
    for name, value in (
        ("claim", self.claim),
        ("correspondence", self.correspondence),
    ):
        _reject_unreadable(
            "symbolic reduction",
            name,
            value,
            "Prover 2 is theorem-grade only where the symbolic setup was hand "
            "derived against the analytic problem, so a reduction naming neither "
            "the statement nor where it was checked backs nothing. Fill both, or "
            "report CORROBORATED and say why in the check's detail.",
        )
    for position, assumption in enumerate(self.assumptions, start=1):
        _reject_unreadable(
            "symbolic reduction",
            f"assumption {position}",
            assumption,
            "An entry nobody filled in is scope a reader cannot check, and it "
            "renders as a gap in the list rather than as a caveat. Say what the "
            "condition is, or drop the entry.",
        )

__str__

__str__() -> str

The reduction as one line: the claim, where it was checked, its scope.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __str__(self) -> str:
    """The reduction as one line: the claim, where it was checked, its scope."""
    scope = (
        f"assuming {'; '.join(self.assumptions)}"
        if self.assumptions
        else "no assumptions recorded"
    )
    return f"symbolic: {self.claim} (per {self.correspondence}, {scope})"

Registration, and the ordering it claims

Evidence says a claim was decided. It does not say when the bar was set, and a bar chosen after the number is visible decides nothing at all. Provenance is the pointer a reviewer follows to check: the ref where the prediction, the bar or the derivation was registered, the ref whose tree produced the number, and one line saying what they will find at the first of them.

A ref is a git commit SHA, an http(s) URL or a DOI. A path, a branch, a tag and HEAD are refused. Each of them satisfies a presence check exactly as well as a commit does, and each resolves to a different tree every time it is read. A URL is taken to be a permalink; one that tracks a branch has the same defect and the type cannot tell the two apart.

Where the two refs name one commit, the render says the ordering is not established by history. Registering and measuring together is not refused. It is what happens whenever a check and the derivation behind it land in one go, and the honest reading is that the ordering rests on the surrounding prose rather than on anything a reviewer can verify. An abbreviated ref counts as the same commit, or lengthening one of the two hashes would walk away from the marker while naming the same thing.

What the type cannot do is order two refs. Equality is checkable in a string and ordering is not, so a registration written after the fact renders exactly like one written before. That is a git merge-base --is-ancestor away, which is a reviewer's job or a test's, and is the reason the refs are refs.

Provenance dataclass

Provenance(
    registered_at: str, measured_at: str, registered: str
)

Which ref registered a claim, and which one measured it.

A number checked against a bar is worth reading only if the bar was fixed before the number existed. A report says what was decided and how well it was decided, and nothing in it says when the bar was set. This is the ref a reviewer opens to find out.

Where the two refs name one commit, the render says so. Registering and measuring together is not refused. The ordering then rests on the account the surrounding prose gives, and the marker is what stops a reader taking it for something the history shows.

History orders two refs. A string cannot. Equality is checkable here and ordering is not, so a registered_at that in fact came after measured_at renders exactly like one that came before. Establishing the direction is a reviewer, or a test, running git merge-base --is-ancestor.

Parameters:

Name	Type	Description	Default
registered_at	str	the ref where the prediction, the bar or the derivation was registered. A git commit SHA, an http(s) URL, or a DOI. A URL is taken to be a permalink. One that tracks a branch moves, which is the defect that rules a bare path out.	required
measured_at	str	the ref whose tree produced the number, in the same three shapes.	required
registered	str	what a reviewer will find at registered_at, in one line. A ref on its own sends them to a diff and leaves them to work out which part of it was the registration.	required

Raises:

Type	Description
ValueError	if either ref is not one-line text in one of the three shapes, or if registered is not one-line text with a visible character in it.

same_ref property

same_ref: bool

Whether the two refs name one commit, so history orders nothing.

An abbreviation counts. Without that, lengthening one of the two hashes walks away from the marker while still naming the same commit.

__post_init__

__post_init__() -> None

Reject a ref that resolves to nothing, and a statement nobody wrote.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __post_init__(self) -> None:
    """Reject a ref that resolves to nothing, and a statement nobody wrote."""
    for name, value in (
        ("registered_at", self.registered_at),
        ("measured_at", self.measured_at),
    ):
        _reject_unreadable(
            "provenance",
            name,
            value,
            "The ordering is the whole content of a provenance, so one end of it "
            "missing records no ordering at all. Give the ref, or report "
            "CORROBORATED and say in the check's detail why there is none.",
        )
        _reject_unresolvable(name, value)
    _reject_unreadable(
        "provenance",
        "registered",
        self.registered,
        "A bare ref sends a reviewer to a diff and leaves them to work out which "
        "part of it was the registration. Say what they will find there.",
    )

__str__

__str__() -> str

The provenance as one line: what was registered, where, against what.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def __str__(self) -> str:
    """The provenance as one line: what was registered, where, against what."""
    if self.same_ref:
        return (
            f"provenance: {self.registered} (registered and measured at "
            f"{self.registered_at}, so the ordering is not established by history)"
        )
    return (
        f"provenance: {self.registered} "
        f"(registered at {self.registered_at}, measured at {self.measured_at})"
    )

The evidence union

Evidence names the completeness base and the symbolic reduction together. CheckReport.evidence is annotated as a tuple of it, so the admissible types are declared once, and a caller building reports of its own has a name to annotate against.

The union and the runtime guard are separate declarations. A kind outside the completeness family needs a member added to both. A type added to one alone annotates as evidence and then refuses to construct, or constructs and reads as evidence of a kind nothing declared. A new completeness leaf needs neither, since both already name the base, and needs a serialiser entry instead.

Evidence module-attribute

Evidence = CompletenessEvidence | SymbolicReduction

What backs a PROVED claim, one member per decisive prover the suite runs.

A completeness certificate decides by exhausting a finite domain. A symbolic reduction decides by identity (Provers 1 and 2) and enumerates nothing, so a certificate is the wrong evidence for it rather than a missing one.

Reading a run

Registering four falsifiers and testing two is a different claim from testing four, and one number cannot carry both. The header separates them and names how many fired. The rows underneath say what warrant the tested ones carried, so a run that survived everything without deciding anything reads as exactly that.

4 registered, 2 tested here, none fired
   PROVED        NOT TRIGGERED   2
   —             NOT APPLICABLE  1
   —             NOT RUN HERE    1

check_summary

check_summary(reports: Sequence[CheckReport]) -> str

Counts per (warrant, outcome) across a run, as a block of lines.

The header carries the accounting a reader needs first: how many falsifiers were registered, how many this run actually tested, and how many fired. Registering four and testing two is a different claim from testing four, and one number cannot say both. The rows underneath say what warrant the tested ones carried, so a run that survived everything without deciding anything prints as exactly that.

Pairs with no checks are left out, so the block is as long as the run was varied. Ordering follows the enum declarations rather than the input, so two runs of the same suite produce the same text. Checks with no warrant sort last, under —.

Parameters:

Name	Type	Description	Default
reports	Sequence[CheckReport]	the run's reports, in any order.	required

Returns:

Type	Description
str	A newline-separated block: the accounting line, then one row per occupied pair.

Source code in packages/warrantlib/src/warrantlib/_vocabulary.py

def check_summary(reports: Sequence[CheckReport]) -> str:
    """Counts per ``(warrant, outcome)`` across a run, as a block of lines.

    The header carries the accounting a reader needs first: how many falsifiers were
    registered, how many this run actually tested, and how many fired. Registering four
    and testing two is a different claim from testing four, and one number cannot say
    both. The rows underneath say what warrant the tested ones carried, so a run that
    survived everything without deciding anything prints as exactly that.

    Pairs with no checks are left out, so the block is as long as the run was varied.
    Ordering follows the enum declarations rather than the input, so two runs of the
    same suite produce the same text. Checks with no warrant sort last, under ``—``.

    Args:
        reports: the run's reports, in any order.

    Returns:
        A newline-separated block: the accounting line, then one row per occupied pair.
    """
    counts = Counter((report.warrant, report.outcome) for report in reports)
    tested = sum(1 for report in reports if report.outcome in _TESTED_HERE)
    fired = sum(1 for report in reports if report.outcome is Outcome.FIRED)
    lines = [
        f"{len(reports)} registered, {tested} tested here, "
        f"{f'{fired} fired' if fired else 'none fired'}"
    ]
    lines += [
        f"   {(warrant.value if warrant else '—'):<13} "
        f"{outcome.value:<15} {counts[warrant, outcome]}"
        for warrant in (*Warrant, None)
        for outcome in Outcome
        if counts[warrant, outcome]
    ]
    return "\n".join(lines)

Writing a run down

A run that prints and exits leaves nothing to compare against. Two questions need the record on disk: whether a registered check quietly stopped reporting, and whether one changed status between two versions of the work. Both are joins on check_id, and both fail if the form the record takes moves underneath them.

report_to_dict writes one report as a JSON-ready mapping. Every value is a string, an integer, a list, a mapping or None, and the key order is fixed rather than taken from the input, so two runs of one suite produce the same bytes and a diff shows what changed rather than what moved. Enums travel as their values, which is why those values are words.

report_from_dict reads one back through the constructor rather than around it. Every precondition still applies: a record naming PROVED with its evidence stripped does not construct. A wire form that could bypass the guard would make the guard optional.

Reading refuses what it cannot read. A record from a schema version this one does not know, an evidence kind with no class behind it, an enum value that has since been renamed: each raises rather than resolving to the nearest thing that fits. Tier.A became Tier.EXACT once already, and a reader that had guessed its way through that rename would have reported a status change nobody made.

Nothing here touches a filesystem. The caller decides where the bytes go.

SCHEMA_VERSION module-attribute

SCHEMA_VERSION = '1.0'

The version of the serialised form, carried on every record.

Bumped whenever a field is added, removed or renamed, or an enum value changes spelling. Enum members are additive: a new one is readable by an older version only in the sense that the older version refuses it by name, which is the intended behaviour. A record whose version this module does not know is refused.

An evidence kind is additive under one version and does not move it. The kind field self-describes, and a reader meeting an unknown one refuses it by name, which is the designed failure rather than a gap. The version moves when the record envelope changes. report_from_dict compares it exactly, so an undocumented bump orphans every record already in a ledger.

report_to_dict

report_to_dict(report: CheckReport) -> dict[str, Any]

A report as a JSON-ready record, carrying the schema version.

Every value is a string, an integer, a list, a mapping or None, so the result passes through json.dumps unchanged. Key order is fixed rather than taken from the input, so two runs of one suite produce the same bytes and a diff shows what changed rather than what moved.

Parameters:

Name	Type	Description	Default
report	CheckReport	the report to write.	required

Raises:

Type	Description
TypeError	if the report carries evidence no kind writes. CheckReport admits any CompletenessEvidence, so a leaf defined outside this package constructs and reaches here. _evidence_from_dict refuses an unknown kind with a ValueError; this is the other direction and an unknown class, which is why the two differ.

Returns:

Type	Description
dict[str, Any]	The record.

Source code in packages/warrantlib/src/warrantlib/_serialise.py

def report_to_dict(report: CheckReport) -> dict[str, Any]:
    """A report as a JSON-ready record, carrying the schema version.

    Every value is a string, an integer, a list, a mapping or ``None``, so the result
    passes through ``json.dumps`` unchanged. Key order is fixed rather than taken from
    the input, so two runs of one suite produce the same bytes and a diff shows what
    changed rather than what moved.

    Args:
        report: the report to write.

    Raises:
        TypeError: if the report carries evidence no kind writes. `CheckReport` admits
            any `CompletenessEvidence`, so a leaf defined outside this package
            constructs and reaches here. `_evidence_from_dict` refuses an unknown
            *kind* with a `ValueError`; this is the other direction and an unknown
            *class*, which is why the two differ.

    Returns:
        The record.
    """
    return {
        "schema_version": SCHEMA_VERSION,
        "check_id": report.check_id,
        "name": report.name,
        "warrant": report.warrant.value if report.warrant else None,
        "outcome": report.outcome.value,
        "tier": report.tier.value,
        "detail": report.detail,
        "evidence": [_evidence_to_dict(item) for item in report.evidence],
        "provenance": [_provenance_to_dict(item) for item in report.provenance],
    }

report_from_dict

report_from_dict(data: Mapping[str, Any]) -> CheckReport

A record as a report, through the constructor rather than around it.

Every precondition the type enforces applies on the way in. A record naming PROVED with its evidence stripped does not construct, or the wire form would be a route around the guard the type exists to be.

Parameters:

Name	Type	Description	Default
data	Mapping[str, Any]	the record, as report_to_dict wrote it.	required

Returns:

Type	Description
CheckReport	The report.

Raises:

Type	Description
ValueError	if the record's schema version is not this one, if a field is missing, if an enum value has no member, or if the report's own preconditions refuse what the record describes.

Source code in packages/warrantlib/src/warrantlib/_serialise.py

def report_from_dict(data: Mapping[str, Any]) -> CheckReport:
    """A record as a report, through the constructor rather than around it.

    Every precondition the type enforces applies on the way in. A record naming
    ``PROVED`` with its evidence stripped does not construct, or the wire form would be
    a route around the guard the type exists to be.

    Args:
        data: the record, as `report_to_dict` wrote it.

    Returns:
        The report.

    Raises:
        ValueError: if the record's schema version is not this one, if a field is
            missing, if an enum value has no member, or if the report's own
            preconditions refuse what the record describes.
    """
    version = _require(data, "schema_version")
    if version != SCHEMA_VERSION:
        raise ValueError(
            f"record has schema_version={version!r}, and this is {SCHEMA_VERSION!r}. "
            f"Reading it would mean guessing which fields moved, and a differ that "
            f"guesses reports changes nobody made."
        )
    warrant = _require(data, "warrant")
    return CheckReport(
        name=_require(data, "name"),
        check_id=_require(data, "check_id"),
        warrant=_member(Warrant, warrant, "warrant") if warrant is not None else None,
        outcome=_member(Outcome, _require(data, "outcome"), "outcome"),
        tier=_member(Tier, _require(data, "tier"), "tier"),
        detail=_require(data, "detail"),
        evidence=tuple(
            _evidence_from_dict(item) for item in _sequence(data, "evidence")
        ),
        provenance=tuple(
            Provenance(
                registered_at=_require(item, "registered_at"),
                measured_at=_require(item, "measured_at"),
                registered=_require(item, "registered"),
            )
            for item in _sequence(data, "provenance")
        ),
    )

A JSON Schema for the record ships beside the code, at warrantlib/report.schema.json. It is there for a consumer reading a ledger without Python, so it states what it can of the preconditions the constructor enforces: the key's shape, that a PROVED record carries evidence and a registration, and that a check which never ran carries no warrant. The test suite validates the writer's own output against it, since a schema nothing checks drifts from the writer without saying so.

Running checks under pytest

pip install "warrantlib[pytest]" adds a plugin, loaded through pytest's pytest11 entry point. It needs no configuration to do the first half of its job.

A test hands its findings over with the record_check fixture, and the run reports them in the vocabulary the check used rather than as a column of dots.

def test_the_coefficient_is_closed_form(record_check):
    record_check(measure_c2())

A fired check fails its test. So does an unresolved one, because a falsifier that ran and could not decide has not left the claim standing. The two that never ran here skip, and the progress letters keep them apart: v for void by construction, e for measured elsewhere. Under -v the row reads NOT TRIGGERED where it would have read PASSED, and the run closes with the registered / tested here / fired accounting.

The pytest outcome underneath is one of pytest's own three, and so is the counting category. junitxml branches on the outcome and reads nothing else, so a fourth value writes the row as no row at all. A fresh category would move every check out of N passed into a name no existing tool reads. The vocabulary is worth carrying. A broken tally is not the price to pay for it.

Declaring what a suite is registered to report

The other half needs a manifest. A count of checks says a suite got shorter. It cannot say which check left, and a check renamed or swapped for another leaves the count untouched, so the gate passes on a suite that is now measuring something else.

warrantlib.manifest declares them instead. The file names each suite's entry point and every id it reported when the file was written.

schema_version = "1.0"

[suites.series_kernel]
entry_point = "research.checks.series_kernel:run_checks"
checks = [
  "series_kernel.first_cumulant_is_the_mean",
]

Point pytest at it with the warrant_manifest ini option and give it the path to collect. Every declared check becomes an item, and the item exists because the manifest declares it rather than because the suite reported it. A check that stops reporting still has a row, and the row fails naming the check and the entry point it went missing from. A second item per suite fails on any id the run reported that the manifest does not carry, so a rename reports as one drop and one addition, which is what it is.

The suite runs once per session however many checks it declares, so a suite costing half a minute costs that once rather than once per row.

--warrant-detail prints every check's own line: its outcome, its warrant, its tier, the reason it gives and the refs it was registered at. -vv does the same, which is pytest's own spelling for more detail than -v and is why the plugin claims no short flag of its own. The row a run prints without either carries the verdict and not the reason, which is the half a reader acts on.

A check that fires reads like any other failing test. It gets a FAILURES block naming the check and carrying its reason, a row in the short summary, and the run's accounting prints underneath with the fired count in it. No flag is needed for that.

pytest's own total counts those reconciliation items and the warrant accounting does not, because they are not checks and carry no warrant. Seventy declared checks across three suites collect as seventy-three items, and the summary says which three so the difference is not left as arithmetic.

Regenerate the file with python -m warrantlib.manifest <path> after a suite changes, and ask whether it is current with --check, which returns non-zero on a stale one. It compares as text, so a layout the writer no longer produces counts as stale too.

Reading a suite's ids means running it, so --check costs a full run. --layout-only restricts either form to the layout question, answers it from the ids the file already declares, and runs nothing. It is the form to put on a fast job where the ids are reconciled elsewhere.