33.2. The commands at a glance
What the annotations declare, the commands ask. There are three forms of asking, and a command's suffix names which form it is — so the table below reads in pairs and triples, each base command followed by its suffixed siblings.
-
A bare command reads: the answer goes to the InfoView, for a person.
-
A reading frozen with
#guard_msgsbecomes a record. The whole answer is now reviewable in the diff, and a changed answer is a failed build. This is the form most of the audits take. -
A
_cleancommand is the gate that a record cannot be, and the distinction is the reason it exists as a separate command rather than as a stricter pin. A record can be re-blessed: re-pinning a message whose summary reads⚠ UNTAGGED — invariant 6/7 violationleaves the build green with the invariant dead, and nothing about the pin itself distinguishes that from a legitimate update. The mechanism that makes an inventory reviewable is exactly the mechanism that lets the invariant be signed away. So a_cleancommand carries no message and pins nothing: it throws. There is nothing there to re-bless.
_decide is the fourth suffix and a different axis: the same check run in the kernel, leaving a
theorem behind rather than a message. #kind_contract_decide does not print that a boundary agrees
— it adds c.kindContractOk and lets #print axioms answer for it.
Reading the table, then: the Pinned column says what freezing a command's answer buys, and reads
— for the commands whose job is to be run by hand.
Command | Library | What it answers | Pinned |
|---|---|---|---|
| Walks every compute definition in the namespaces and reports each that mints or erases a registered carrier, with the kinds it mints and the tier that sanctions it; an untagged boundary site is reported as a violation. | a new anonymous interior mint fails the build, the way a new axiom fails a pinned axiom profile | |
| The invariant rather than the inventory: throws when any boundary-active declaration in scope carries no tier attribute. It carries no message and pins nothing, so re-blessing the audit's pin cannot silence it. | the command is the gate; there is no message to re-bless | |
| Throws on a raw carrier mint inside a @[kindCrossing] or @[carrierVocab] body, where every mint must instead be a licensed derivation or a Quantity.attest whose reason is harvested. @[kindConst], @[kindIngest] and @[kindEmission] keep raw mints legal at the declaration granularity. | the command is the gate; at the ratcheted tiers a new anonymous mint fails the build instead of joining a list nobody re-reads | |
| Enumerates the tagged boundary registry — every sanctioned site with the first line of its docstring, grouped by tier. | — | |
|
Prints every authored kind-algebra edge mentioning the kind | the complete set of edges a kind supports is fixed, so a new one is a visible change | |
| Resolves every authored edge's kinds to their declared DimensionedKind and evaluates the family's dimensional rule, reporting each edge as coherent, parametric, undimensioned, conflicting, or incoherent. | an edge over a kind carrying no dimension, or one whose dimensions do not balance, fails the build | |
| The coverage invariant rather than its record: throws while any edge in scope is undimensioned, conflicting or incoherent. Parametric generic vocabulary is not a violation. Its one false alarm is an under-imported closure, which the error says. | the command is the gate; there is no message to re-bless | |
|
Walks every dimension-one | a dimension-one kind declared without a principle or a mark fails the pin | |
| The census as a gate: throws while any dimension-one kind in scope carries neither an examination principle nor a declared exemption. Records an audit receipt exactly when it does not fire, which is what lets a document's M6 read green only in a build where the census ran. | the command is the gate; there is no message to re-bless | |
|
Walks every | a boundary declared anywhere in scope that no edge names fails the pin | |
| The census as a gate: throws while any declared boundary in scope is unwitnessed and unexempted. Records an audit receipt exactly when it does not fire. | the command is the gate; there is no message to re-bless | |
|
Walks every produced port ( |
a produced port with no | |
| The census as a gate: throws while any produced port in scope carries no aggregation class. Records an audit receipt exactly when it does not fire. | the command is the gate; there is no message to re-bless | |
|
Walks every | an inverted boundary with no conditional port and no exemption fails the pin | |
| The census as a gate: throws while any inverted boundary in scope is unguarded and unexempted. Records an audit receipt exactly when it does not fire. | the command is the gate; there is no message to re-bless | |
|
Walks every | an inverts edge declaring neither a well-posedness nor an ambiguity fails the pin | |
|
The census as a gate: throws while any | the command is the gate; there is no message to re-bless | |
|
Walks every | a marked kind no declared boundary exports fails the pin | |
| The census as a gate: throws while any diagnostic kind in scope is carried by no produced port. Records an audit receipt exactly when it does not fire. | the command is the gate; there is no message to re-bless | |
| The kind-level component report: the authored kinds in scope, their licensed-derivation edge count, every inter-derivability cluster of two or more kinds with the edges that wire it, and whether the kind digraph is acyclic. | the reviewed enumeration to pin beside #kind_edges — a new cluster is a visible change | |
| Inter-derivability as a gate: every cluster of two or more mutually derivable kinds must be declared as a parenthesized group at the same size; an undeclared cluster throws with its wiring printed. | a new witness registration that merges two kind roles fails the build at the vocabulary level, before any value walks the new cycle | |
|
Writes the D2 diagram sources of the component findings into a directory — the condensation and one file per inter-derivability cluster. The script-facing twin of #kind_scc, run from a | — | |
| The SCC footprint of a declared boundary against the kind graph: the component partition of its port and interior kinds, the same-kind port groups, the review-strength sites, and the verdict naming where the module's guarantee comes from. | the boundary's exposure to inter-derivability is fixed, so a widened footprint is a visible change | |
| Prints every port a declaration's kind-typed signature states — inputs, configuration reads, outputs, each with its stated kind — followed by the signature's unkinded positions. | a port that changes kind, or an unkinded position that appears, fails the pin | |
| Prints every authored license discharged inline in a declaration's value — each consuming application's edge with the operand quantities that met there, in body order, with multiplicity. | the licenses a body actually discharges are fixed, so a new one is a visible change | |
| Prints the constructed step graph — ports, introduction events, wired occurrences with their assumed/partial markers, exits — and the evaluated well-formedness verdict. | the wiring is fixed, so a rewired body is a visible change | |
|
Reflects the constructed graph into a term and adds the theorem | the command is the gate; the pin freezes the kernel receipt | |
| Assembles the listed declarations into one multi-step graph and prints it — each level with its inclusion mode, the union graph, the citation relation, and the evaluated verdict. | the assembled wiring is fixed across the whole set, not one declaration at a time | |
|
Reflects the assembled union graph into a term and adds the theorem | the command is the gate; the pin freezes the kernel receipt | |
| Assembles the members a contract declares and compares that assembly's boundary with the boundary the contract declares — parameters and decided conditional ports, then what each side has and the other does not, then the verdict. Where #kind_assembly says the wiring holds together, this says the members are the ones the declared interface belongs to. | a boundary that stops being the one its members compute fails the pin | |
|
Adds the theorem | the command is the gate; the pin freezes the kernel receipt | |
|
Surveys every | a boundary declared anywhere in scope and inconsistent with what its members compute fails the pin, including one nobody remembered to check by name | |
|
The same sweep as a hard gate with kernel receipts: any violation is an error, and each passing contract gains the kernel theorem | the command is the gate; the pin freezes the kernel receipts | |
|
Checks the theorem edge a | every failure throws, so the command is the report and the gate at once — there is no reading of it that states a violation | |
|
The by-type edge survey: every | a newly violated edge fails the pin, and so does a vanished one or an exemption nobody declared | |
| Compares two contracts with no graph and no harvest: what the deploying contract did with each parameter the deployed contract handed it, and whether anything was left unanswered. | a parameter that stops being answered is a visible change | |
|
Adds the theorem | the command is the gate; the pin freezes the kernel receipt | |
| Prints the unkinded ledger of the scope a contract declares: the count, then one line per naked position and per unkinded flow, deduplicated by member. | the pin fails when a silence appears AND when one is fixed, which is what keeps the ledger honest about which direction it moved | |
| The ledger as a gate: errors unless the scope's ledger is empty. Separate from the pin above for the reason every violation-capable pin needs a separate gate — pinning a violation is how it stops being noticed. | the command is the gate; there is no message to re-bless | |
| The propagation relation of a contract over the assembly its members compute: which source ports reach which produced ports. | — | |
| The per-output assumption ledger and trust decomposition of every produced port of a contract, over the assembly its members compute. | — | |
|
Checks an uncertainty budget's attachment to a boundary and renders it: the port must be a produced port at the budget's kind, the assembly acyclic, every term naming a source that influences the port — and the influencing sources the budget omits render as | every violation throws, so the command is the report and the gate at once | |
| Prints one generated index as plain text — the same table a document renders, available without building a document. | a derived table that stops matching is a build failure rather than an absence nobody notices | |
| Reports the docstrings an index table quotes whose first paragraph is too long for the column that quotes it, widest first. | — | |
| Writes the named indexes into the elaborating module's own module docstring, so doc-gen4 renders them as that module's page. | — |