33.6. What a boundary claims — the provenance sweeps
The boundary audit asks where the calculus is left; the edge audits ask what it rests on. These ask whether a declared boundary is the one its members compute.
A Provenance.Contract is that declaration: the ports a boundary consumes, the exits it produces,
and the member steps that realize it. It can disagree with itself — an input the members read and
the contract never declared, a clause naming a supplier that answers no port — and the disagreement
is not visible in any type, because a contract is data about a computation rather than a constraint
on it.
Enrollment is by type, which is the design. Every constant whose type is headed by
Provenance.Contract under the swept namespaces is a subject, so declaring a boundary enrolls it.
There is no per-declaration command to remember and no registration to forget: a boundary cannot be
declared and left out of the sweep, which is the property a per-name command
(#kind_contract, one contract) cannot offer however diligently it is used.
#kind_contracts ns… re-checks every subject exactly as #kind_contract checks one — the
decider, aggregation and supplier clauses, then the declared boundary against the one the members
compute — and renders one line per contract in declaration-name order, as a single info message
suitable for #guard_msgs pinning. Namespaces elided, this is the validation probe's own pinned
output:
kind contracts — 4 contract(s), 1 violated, 1 exempted ✗ …Bad.forgottenInput: 'sweep probe forward, x forgotten' — undeclared input fwd/x : aK …Good.fwdBoundary: 'sweep probe forward' — 2 ports, 0 exits, 1 member step(s) …Good.invBoundary: 'sweep probe retrieval' — 2 ports, 0 exits, 1 member step(s) ⊘ …Exempt.keptCounterexample: counterexample, exempted
Three things in that header rather than one. Because it counts the subjects as well as the
violations, a pin fails on a boundary that vanished as readily as on one that broke; because it
counts the exemptions, exemption creep is a failed pin too. And a scope with no contracts pins
0 contract(s) rather than passing invisibly — the distinction between checked and clean and
nothing was checked, which an empty report cannot make.
#kind_contracts_decide ns… is the same sweep as a hard gate. A violation is an error rather than a
✗ row, so no reading of the output can state one, and each passing contract gains the kernel
theorem c.kindContractOk. Sweeping again re-proves nothing: a standing receipt reports as
already stands. The two tiers answer different questions — whether the boundaries in scope agree,
and whether the kernel has been made to say so.
The same three forms, per name. #kind_contract c and #kind_contract_decide c are the sweep's
singular siblings, and what they add over #kind_assembly is the comparison: the assembly says the
wiring holds together, the contract says the members are the ones the declared interface belongs to.
And the edges between boundaries. A Provenance.Relation states what one boundary claims of
another — an inversion, a bound. #kind_relation r checks one: a sorry-free witness, the conclusion
in the claimed shape, and the tolerance, hypothesis and license clauses each answered for by name.
Every failure throws, so that command is report and gate at once. #kind_relations ns… is its
by-type sweep, with the same ✗/⊘ rows and the same counted header.
#kind_discharges c d asks the tier question instead — what a deploying contract did with each
parameter the deployed one handed it — and #kind_discharges_decide proves the answer.
What is not kinded, and what is not propagated. Two commands report absences, which is the
thing a checker cannot notice on its own. #kind_unkinded c prints the naked positions and unkinded
flows in a contract's scope; pinned, it fails when a silence appears and when one is fixed,
which is what keeps the ledger honest about which direction it moved — and #kind_unkinded_clean is
the gate for a scope that has cleared them. #kind_budget b c checks an uncertainty budget's
attachment to a boundary and renders the influencing sources the budget omits as unbudgeted
source(s), so what the model is not propagating appears in the report rather than being absent from
it. #kind_contract_propagation and #kind_output_ledger are the reading aids beside them: which
source ports reach which produced ports, and the per-output assumption ledger.
33.6.1. @[kindCounterexample] — a deliberate misdeclaration, kept
A sweep that enrolls by type has one cost: a falsification probe — a contract written wrong on purpose, kept because its checker refuses it — enrolls too, and would fail the gate it exists to demonstrate. Deleting it would leave the checker's refusal untested; leaving it untagged would make the gate unpinnable.
/-- A deliberately misdeclared boundary, kept because the sweep must refuse it. -/ @[kindCounterexample] def keptCounterexample : Provenance.Contract := …
A tagged subject renders as a ⊘ row and is not checked, so the probe stands beside the gate it
exercises. The exemption is not a way out of the discipline, because it is counted: the header's
exemption count is part of the pin, so a contract quietly exempted to make a build pass changes the
pinned output. The mark reaches the generated tables on the same terms — a tagged contract is not a
coverage subject, and a tagged relation is not a witness, since a deliberate misdeclaration must not
discharge a real boundary's edge obligation.
The attribute checks what it is attached to, and says why:
`@[kindCounterexample]` expects a 'Provenance.Contract' or a 'Provenance.Relation' — '…stray' is neither. The mark exempts a declaration from the by-type provenance sweeps, and only those two types are swept.