A Property Kind Calculus for Measurement Metrology

33.5. What one declaration wires — the graph and incidence commands🔗

The audits so far sweep namespaces. These read a single declaration, or the kind vocabulary as a whole, and they are what an author runs while writing rather than what a probe pins — though most of them pin, because a wiring that changes silently is the thing worth catching.

What a signature states, and what a body does. #kind_ports d prints the ports the declaration's kind-typed signature states — inputs, configuration reads, outputs, each with its kind — and then the signature's unkinded positions, which is the half a reader forgets to ask for. #kind_occurrences d prints the other side: every authored license the body discharges inline, each consuming application's edge with the operands that met there, in body order and with multiplicity. #kind_graph d puts the two together as the constructed step graph and evaluates its well-formedness, and #kind_graph_decide d proves that verdict in the kernel, leaving d.kindGraphWf behind. #kind_assembly and #kind_assembly_decide are the same pair over a list of declarations, assembled into one multi-step graph — which is what a boundary spanning several definitions needs.

What the kind vocabulary looks like as a graph. #kind_scc [ns…] reports the kinds in scope, their licensed-derivation edges, and — the finding it exists for — every inter-derivability cluster: a set of two or more kinds each manufacturable from the others by licensed steps. Inside such a cluster the kind algebra alone cannot refuse a substitution, so a cluster is a real weakening of the discipline and one worth knowing about. #kind_scc_clean is its gate, and it is declarative rather than absolute: every cluster must be declared as a parenthesized group at its exact size, so a new witness registration that merges two kind roles fails the build at the vocabulary level, before any value walks the new cycle. #kind_scc_d2 writes the same findings as D2 diagram sources for rendering, and #kind_footprint c ns… asks the question a module owner asks: which of those clusters this boundary's own kinds land in, and therefore where the module's guarantee actually comes from.