The canonical semantic model

The typed intermediate representation every structural consumer reads. GH #476 built it; this document is its contract.

Reference material, synced from the compiler repo’s spec/. The guide is the gentler path in.

The typed intermediate representation every structural consumer reads. GH #476 built it; this document is its contract.

spec/verification.md specifies what the compiler checks and what the topology artifact serialises. This one specifies the value sitting between them: what a model contains, what it is allowed to not know, the laws it must satisfy, and the rules a new consumer has to obey.

The crate is hale-model — 106 public types, no dependency on the AST, the checker, or codegen. Its identity and provenance mechanics (SeedId, SourceId, ProvenanceId, Provenance, SourceUnit, ProvenanceTable) are hale-graph’s, the graph core F.40 rebuilds it on, re-exported under the model’s own paths.

checked Bundle                      -->  ApplicationModel
Bundle + Model                      -->  ClaimIrTable
Bundle + Model + ClaimIrTable       -->  EvidenceTable
Model + ClaimIrTable [+ Evidence]   -->  Judged verdicts
ApplicationModel                    -->  model-half projection (artifact)
dispatch gates + arrangement        -->  DispatchPlan (the model holds it projected)
admitted Artifact                   -->  ComponentModel --> fleet ModelGraph

Derive a modeled semantic fact once. Downstream consumers project or query it; they do not walk the AST, the artifact JSON, or codegen state to rediscover it.

Note what that does not say. ClaimIrTable is not a projection of the model alone — lower_claims takes the bundle too, because clause enumeration, constitution adoption and annotation surfaces are read from source. EvidenceTable is likewise derived from all three, and for the certificate and budget families it is an INPUT to judgment rather than its result: those engines measure, and the judgment decides over what they measured. And the fleet tier shares selected ALGORITHMS and admitted contracts, not the value: it decodes a ComponentModel from artifact JSON and composes its own ModelGraph.

Eight concepts stay distinct and un-conflated: source, plan, model, ClaimIr, evidence, artifact, lowering plan, and execution evidence. Each answers a different question, and keeping them separate is what lets each one be simple — and what keeps a second authority for one question from existing at all.

The law above was written for the model’s consumers: artifact, fleet and claim code cannot walk source for a modeled fact. It never reached the producers, codegen or the CLI, which is why the bus graph is built eight times per build, ownership has three accounts, and a fixpoint over the call graph could land inside codegen without tripping anything (GH #1208). F.40 (spec/decisions.md) extends the law to every semantic fact the compiler acts on, in every crate, and makes it checkable:

One authoritative producer per semantic fact within a resolved compilation snapshot. Consumers ask for the fact by name; they do not re-encode its meaning from the AST, from another table’s raw rows, or from a Debug string.

The registry is the index of that law. spec/registry.md — rendered from crates/hale-graph/src/registry.rs and held byte-equal by a test — lists every semantic family with its contract:

• what it answers, in one sentence, and what it reads;
• its producer: the authoritative one, or today’s, or none yet;
• its legacy producers, each with the condition under which it is deleted — the exact inventory of what is permitted while the family migrates;
• its consumers, named, so a new reader is a registry change before it is a code change;
• its invariants and missing-data policy: whether a missing row is a compiler error or a hole with a stated policy; and, for a family lowering reads, which of two things each of lowering’s reads is: required (the snapshot always provides the row, so a missing one is a CodegenError naming the family and the row, pinned by a test that removes it from a lowering view) or total (absence is itself the fact, and the registry says what no row means), never a default or a second derivation; lowering_reads_are_classified holds every family lowering reads to one of the two;
• its focused tests, the ones a contributor runs to know a change to that family is right;
• where the spec states the contract.

Each family is in one of three states, so the inventory can be exact without banning what exists today: Reserved (a future family or consumer, computing nothing), Migrating (the canonical producer is under development and the legacy list is complete), or Canonical (one production producer; consumers cannot reconstruct its meaning). The registry also lists the spec’s numbered rules with the code that evaluates each — a registered rule with no evaluator fails the compiler’s own build — and freezes the format!("{:?}", ..) sites that decide a fact from a Debug string, so no new one can appear.

The guard (crates/hale-graph/tests/registry_guard.rs) makes the wrong workflow fail: a derivation-shaped function the registry does not name, a reference to a family’s guarded seam from an unlisted file, a new Debug-string scan, a cited site that no longer exists. The right workflow is the one the registry describes: change the authoritative derivation or rule, update its contract tests, exercise the registered interactions and consumers, and never patch a second interpretation into codegen or the CLI.

Reserved entries exist so the tables never change twice: the runs_under(locus, principal) relation column on the tower, the view family and its adequate_for law, the evented transitions, the deployment families, and ui and bundle as consumers beside the LSP, --dump-topology and the description. A reservation creates no production demand.

A model is known facts plus an explicit account of what it does not know, closed at a horizon:

• typed entity tables — not one homogeneous node kind;
• typed relation tables — calls, owns and publishes are different rows with different fields and different witness renderings, never interchangeable string edges;
• typed holes — unresolved residue as data, each naming the relation families it hides;
• positive capabilities — what is exact, stated, so a consumer can ask “is this model adequate for my question?” without reverse-engineering the absence of strings;
• provenance on the fact-bearing rows — entities, relations, holes, labels and weights; source-neutral, and scoped precisely below.

The last two are the load-bearing ones. A graph that records only what it found cannot distinguish “there is no such edge” from “I could not see”. Every judgment in the language rests on that distinction — see Unknown is not absent.

There is exactly one constructor:

hale_types::model_builder::derive_application_model_over(&Bundle, &ModelInputs) -> ApplicationModel

It runs over a checked bundle. A model of an ill-typed program describes nothing, so consumers that judge gate on the bundle having no non-Claim errors first.

It builds none of the families it reads beside the program: ModelInputs hands it the top scope with its topic rows, the bus graph, the ownership graph and the handler rows, each built once over the checked programs. Every verb demands them, and the model, from its snapshot (Snapshot::demand_model, F.40 phase 2.3), and so does every test: no entry builds them for a bundle no snapshot holds.

There is no other way in. In particular:

• No artifact → model. The topology artifact is a projection, not a serialisation. It carries the model half (hashed by shape_hash) plus typed law, capability and adequacy sections, but several tables — costs, locus_instances, the analyses, the provenance interner — have no wire form. hale topology graph and the fleet tier admit an artifact by validating its JSON against the same rules; they do not reconstruct an ApplicationModel.
• No plan → model. Fleet composition admits deployment plans and reads artifacts; it does not elaborate a plan into an application model. What it builds instead is instructive: ComponentModel, a separate string-level structure reconstructed from artifact JSON — vertex names, (from, to) call pairs, name-level publish and subscribe relations, and the component’s own residue. It is deliberately weaker than an ApplicationModel because that is all the wire form carries, and it is the concrete price of the boundary below.
• No hand-authored model format. Tests that need a shape the builder cannot yet infer derive a real model and then edit its tables. That is deliberate: it keeps the builder the only thing that decides what a model of a program is.

The consequence is worth stating plainly, because it bounds every out-of-process consumer: anything outside the compiler process reads the artifact, not the model, and the artifact is lossy by construction. Giving the model a reversible wire form is a real piece of future work, not a small one — it would need every table to serialise, the provenance table to survive, and an admission path that cannot be tricked into producing a model no program denotes.

One slice of the model does have a wire form, and it is deliberately a form slice: the description of a served surface (spec/api.md § The description; the format is spec/api-description.schema.json). It is rendered from the surface family: one row per rpc line of an api block or @rpc handler (the surface, the member, the request, response and error types with their contract shape hashes (§ The shape of a type), whether the error is the server error, the pools and the required roles), from which the surface’s contract digest is folded and every description is written, per exposure, from the rows dispatch reads. The type declarations supply the field schemas the model does not hold. It does not consult the model’s other tables: it describes the same declarations the model is built from, so the two cannot disagree about which locus a row names.

Three properties are the contract:

• Form, not params (I1, not I2). The program-wide inventory (hale check --api) names what the program offers and never who holds a role: it is a deployment inventory, not an authorization statement for any caller. A served exposure adds the listener it was given and the caller it established, and says so: the identity of an exposure is its surface, its digest and its name.
• Perspective-invariant (I5). Every entry is a form claim over the program’s declarations, so a perspective swap, a placement change or a second deployment describe themselves in the same bytes; two builds of one source produce one description, and a running exposure serves the document the compiler’s rows write for the caller it names (the Unix {"describe": true} and GET /.description answer it whole).
• Boundary honesty. The document carries its notes in its own text: requires is a boundary check at the serve site, never a proof over internal call paths (unless the program states one: a group { role R } names the handlers a holder of R may call, and a claim over it is checked over the call and bus paths; docs/src/claims.md § group), and a request accepted runs to completion whatever becomes of the caller’s wait. A client renders the notes; it does not present a check as a certificate.

Its shape is pinned by tests/api-contract/ (the R0 fixtures) and by crates/hale-cli/tests/fixtures/api_description/; the OpenAPI 3.1, JSON Schema and MCP forms are projections of a surface’s rows (hale check --api --surface NAME). It is not a reversible wire form of the model — the boundary above stands — and it admits nothing: a consumer reads it, never builds a model from it. The model holds the surfaces and their rows (the surfaces and surface_rows tables, below).

Entities holds seventeen tables. A row’s id is its index in its own table, wrapped in a newtype (FunctionId, SubjectId, …) — not a field stored on the row.

Identity is per table, and deliberately not uniform. Many rows carry a raw canonical name plus an author-facing display (functions, loci, topics, groups); several do not. LocusInstance is identified by path (App.workers[3]) with a decl and a replica index; Subject by its wire pattern; PayloadContract by its shape and hash; Binding by its typed subject, transport and role; Phase, Seed and ThreadDomain carry a name with no separate display. Consumers should read the table’s own definition rather than assume a common shape.

A functions row’s id is the rank of its name; the row also carries decl, the site its snapshot minted for the declaration. A join from an analysis row (an allocation-summary or effect row, keyed by that site) to its function reads decl, never the name. decl is never rendered and never hashed, so it moves no dump and no digest.

The surface family has one law of its own beside canonical order (by surface name; rows by surface, then member): a surface’s digest is the fold of its rows (hale_model::surface::surface_digest, the framing of spec/api.md § The contract digest), so a row added, removed or changed without the digest moving is not a model. Neither table enters shape_hash: a program with no surface hashes as it did, and one with surfaces gains these rows and no hash.

Two distinctions in that table are load-bearing:

• subjects vs topics. A subject is the delivery identity. A literal "t" <- v send carries declared_topic: None even when its text matches a declared topic’s wire subject, because after lowering the runtime cannot tell the two spellings apart. Any query that decides delivery joins on SubjectId; declared_topic is a syntactic link to a declaration and decides nothing.
• loci vs locus_instances. A declaration says what may exist; an instance is a statically exact birth in the arrangement. LocusDecl::params records what a locus may hold even where no instance is born; LocusInstance::replica is the 0-based index the runtime pins, not a count.

A type has a shape, a string, and a shape hash, the 64-bit FNV-1a fold of the string’s bytes (hale_graph::identity::Fnv64: offset basis 0xcbf29ce484222325, prime 0x100000001b3, each byte xor-ed in and then multiplied), written as sixteen lowercase hex digits. One renderer (hale_types::topic_identity::Shapes) renders it in two forms; the payload contract reads one and the surface rows the other, and neither renders a shape of its own.

Both forms tag a field the same way when its type is flat:

A struct’s shape is its fields in declaration order, each <field>:<tag>, joined by ;. A flat struct is one whose every field has a tag of the table; it has one shape whichever form reads it, so one shape hash: type OrderReceipt { order: OrderId; notional: Money; } is order:i;notional:q(cent), bb4f99639cf069af, in both.

The observation form is the topic’s observation identity (the topics section of the artifact, PROTOCOL.md §4, mirrored byte for byte by the runtime’s obs_fnv, which folds the wire subject, : and this string) and the payloads table’s contract. Only a bare, non-generic declared struct has one, and any field whose type is not in the table is tagged struct, name-free, so the hash never depends on a declaring binary’s local type names. A payload with no observation shape (an enum, a scalar, an array, a builtin record, a type the seed cannot see) is the opaque contract opaque:<type>. This form is a wire identity and does not move.

The contract form is what a surface row’s request, response and error are, which the contract digest folds (spec/api.md § The contract digest). Every type has one, and it is deep, so a field changed inside a nested struct, or a variant added to an enum, moves the hash of every type that reaches it:

• a declared struct: its fields, each <field>:<tag>, joined by ;;
• a builtin record (ClosureViolation, IndexError, … the records the compiler declares, hale_types::builtin_types): its fields as a struct’s, ClosureViolation being locus:s;closure:s;diff:i (36c7f0561125943e); a declaration of the name in the program replaces it, as it does in the checker;
• an enum: =enum( its variants in declaration order joined by |, a variant written <Name> or <Name>(<tag>,…) ): type Side = enum { Buy, Sell(Int, String) } is =enum(Buy|Sell(i,s));
• an alias, and a scalar that is neither an identity, a range, a quantity nor a point (distinct Float): the shape of what it stands for;
• any other type: = and its tag (=i for an OrderId a row names by itself, =q(cent) for a Money).

A field’s tag in the contract form is the table’s, or:

The nested type’s slot is its hash, not its fields inlined, so a type’s contract shape is a function of its own fields and of the hashes of the types it names; and because a flat struct’s fields are all tagged by the shared table, its contract shape is its observation shape and no flat struct’s hash differs between the two forms. A struct with a compound field is the one kind whose two hashes differ: type Outer { id: Int; body: Inner; } is id:i;body:struct as a payload and id:i;body:#e661911904a01160 as a row’s type.

locus_instances, realizes, owns, placed_in, thread_domains and affined_to are the placement table’s rows, projected (F.40 phase 3, the placement family); the builder walks no declaration of its own for them.

• What is arranged. The instances of the root lowering deploys (the entry row’s entry, never an imported main): one template per literal of the root, or the entry’s implicit construction of a root no literal builds. Each instance is arranged where it runs: a held instance under its holder, as the rows its source actually built. A field is arranged as the declaration the table says it realizes, so an aliased field is the aliased locus and a contract-typed field the implementation that was built.
• Paths and replicas. A path is the fields from the root, with the replica index after the replicated field (App.f[2].k). A path has no construction component: it is arranged when every template and alternative enumerates it and agrees on the declaration and the domain; otherwise it is left out with everything under it, each declaration realized there a RuntimeInheritedPlacement hole naming the path. An unenumerable subtree in any template or alternative is disagreement, even if the other templates agree. LocusInstance::replica is the replica row’s own index; an instance under a replica carries the index in its path and None in its replica.
• Domains. thread_domains are the domains the arranged instances run in (main, pool:<name>, pinned:<anchor path>) and one binding:<topic> per entry of the deployed root’s bindings { }. affined_to gives a domain its resolved CPU set (a cores range or set, or a node / l3 affinity resolved against the root’s topology { }): a pool’s is the set its one worker may run on, a pinned replica’s its own thread’s. A CPU set is a column of a domain, never a domain; two entries naming one pool give one row, and a domain with no affinity has none.
• What is not arranged. The projection is user-only and partial by design: a row realizing a stdlib declaration is left out with its subtree (its declaration is no entity of this model, and adding one would be shape), with no hole for it; an adapter of the root’s bindings { } is no instance; a literal fn main builds besides the root is a birth outside the arrangement, a RuntimeInheritedPlacement hole on its declaration. Every placement question the checker and lowering ask is answered by the table, never by the arrangement.

Dynamic-birth provenance comes from the ownership graph (F.40 phase 3, C3). Its walk records whether a locus-body literal belongs to a params initializer and records free-function births alongside the owning-locus sites. The model does not classify births by comparing source spans or walk free functions again. In particular, expressions copied from API bindings into generated params retain their source spans and their params-default provenance. They do not add dynamic-placement holes; connection peers created in bodies still do. A birth’s resolved child joins the model’s declaration table by site, so a qualified stdlib name cannot create a hole on a user locus with the same final name segment.

Three identity contracts hold the projection, each separately:

1. Shape identity. The arrangement is outside the shape half: shape_hash reads none of these tables, so no change to the arrangement moves it.
2. Observation entity ids. obs_entity_ids stamps subjects, locus declarations and bindings, never instances; the bindings are the deployed root’s.
3. Arrangement-instance correspondence. LocusInstanceId is the index in path order, so an added or removed path renumbers every later instance. No numeric instance id is stable across builds; a consumer that holds an instance across builds joins by path.

Relations holds seventeen tables. The invariant that matters is grain.

Call and publish rows are site-grained: they carry an authored site ordinal, two calls to one callee are two rows because the callee executes twice, and alternatives of one interface dispatch share that ordinal because one dispatch runs one conformer. A consumer that collapses either into a set is computing reachability where the language means executions. A call through a function value resolves to the program’s function values of its type (F.40 E5; spec/verification.md), and the model has no function-value dispatch kind: each alternative is a Direct row at a site of its own, so a count over them is a sum where one execution runs one of them (the @budget engines, which read the analysis’s dispatch group, take the max), and the site ordinals after such a call move when the set of function values does. The same holds for alternatives inside a stdlib_absorption interior.

costs is mixed-grain and carries no site ordinal at all; its rows are distinguished by (function, dimension, provenance). See below.

costs needs care, because its two grains have different semirings:

• Alloc and Block are OCCURRENCE rows. One row per allocation site or blocking call, distinguished by provenance, carrying in_loop. A per-call budget is a statement about one invocation, so whether an occurrence sits inside a loop is the difference between a finite count and an unbounded one.
• FrameBytes is a FUNCTION-level row. Exactly one per analysed function, in_loop always false, consumed by a longest-stack-path computation rather than summed over executions. A frame is reused across iterations; multiplying it as if it were an occurrence is a category error.

Neither carries an authored site ordinal — CostSite is (function, dimension, amount, in_loop, provenance).

A hole is unresolved residue, as data:

Hole { at: EntityRef, kind: HoleKind, hides: RelationSet,
       authored_site: Option<u32>, reason: String, provenance }

Ten kinds: IndirectCall, UntypedReceiver, ComputedSubject, UnknownKeyDomain, OpenInterface, RuntimeInheritedPlacement, DynamicEndpoint, ExternalOpaque, UnsupportedArtifactSemantics, UnanalyzedBody.

hides names the relation families the hole withdraws. allowed_hole_families is a shape law, validated: each (entity, kind) pair has a required minimum and a permitted maximum mask. An unfollowable call hides CALLS ∪ EFFECTS ∪ COSTS — all three are required, because a call whose target the caller chooses is exactly where an effect walk and a quantitative bound must refuse.

A hole withdraws a proof only where it is relevant to the question being asked. A hole on an unrelated topic says nothing about a purely local claim, and a global “is there any hole?” scan turns one dynamically-born locus into an unbounded answer for the whole program.

Relevance has two grains, and consumers need both:

• Endpoint-scoped — is the possible-delivery STRUCTURE beyond this endpoint, in this direction, fully modeled? model_query::endpoint_incomplete answers exactly that and no more: downstream it reads SUBSCRIBES | KEY_FILTERS | DELIVERY holes, upstream PUBLISHES | DELIVERY, plus the typed routes that leave the application (a connect binding is a downstream boundary, a listen binding an upstream one; neither emits a hole, so a consumer reading only holes fails open on both).

  It is not the whole completeness question, and a consumer must not treat it as such. It deliberately says nothing about subscriber CARDINALITY or locus population, because those do not affect which effect classes a publish reaches — another instance of one locus runs the same handler. A judgment that counts deliveries rather than reachability needs its own account, and @budget(fanout) has one: subject/topic-grained CARDINALITY residue, and locus-grained OWNS | CARDINALITY residue through population_of, whose three outcomes (exactly zero, exactly n, not knowable) must stay distinct.

  The rule generalises: scope every family in your required_relations, not just the ones this shared query covers. endpoint_incomplete is one question asked once; it is not every question.

• Reachability-scoped — residue in a function nothing can execute withdraws nothing. An unfollowable call in dead code cannot invoke anything.

The rule the language runs on, stated once:

A reachable relevant hole always defeats a proof of absence.

Note what that does not say. Whether a concrete counterexample found later in a walk outranks a hole found earlier is a per-tier policy, not a universal rule, and the shared reachability engine exposes both:

• HolePolicy::Halt — stop at the first reachable hole. The application checker takes this: the repair is to make that edge resolvable, and the diagnostic names the edge.
• HolePolicy::PathWins — keep walking known edges, so a concrete counterexample outranks the refusal and the hole decides only if no path is found. The fleet checker takes this: a cross-binary path is worth more than “cannot tell”.

Both are sound; they differ in what is more useful to report. A new judgment picks one deliberately — inheriting the wrong one silently changes what an application law means.

Its most common violation is subtle. Where a query returns three states — exactly none, exactly n, not knowable — collapsing the last two reads as “no such thing” and certifies. Population, effect sets, subscriber counts and key domains all have this shape, and the collapse reads as a proof of absence.

Capabilities is the positive completeness account: eleven independent booleans (exact_calls, exact_publishes, exact_subscribes, exact_key_filters, exact_ownership, exact_placement, exact_routes, exact_effects, exact_cardinality, exact_delivery_guarantees, exact_costs), each vouching a RelationSet.

The account is positive on purpose. Absence of recorded unknowns is not proof of completeness, so an unvouched family reads degraded whether or not a hole happens to exist. validate cross-checks the two: a capability claiming exactness over a family some hole hides is a CapabilityContradiction, and the canonical unresolved_relation_mask is the authority for what a hole or an absorption residue hides. A producer’s private bookkeeping agreeing with itself is not enough; every consumer is entitled to rely on validate().

Adequacy is derived, per judgment family: exact when capabilities vouch every relation family that family’s projection consumes, else degraded. Each family declares that set in JudgmentFamily::required_relations, and the declaration must name what the queries actually read — extending an engine’s reads extends the declaration in the same change.

Entity, relation, hole, label and weight rows carry a ProvenanceId into a table with three variants:

• Source { source, span } — a SourceId and a byte range relative to that source unit’s own content, not to any bundle-global space. A consumer renders a global span by adding the unit’s base;
• Synthetic { origin } — a named origin for a fact no source line produced;
• ForeignSpan { span } — a span in a FOREIGN offset space (stdlib parse space, another seed). It is the discriminator that keeps stdlib evidence from being resolved against application files, where numeric overlap would misfile it.

Two rules:

• The model never sees the AST. Spans are bytes and SourceIds.
• Foreign offset spaces stay foreign, by construction rather than by convention — hence the third variant.

The guarantee is scoped to those row families. Analysis products are coarser: a StdlibAbsorption carries entry_provenance for its authored entry site, and its interior nodes and events do not each carry their own.

Analyses carries products the model does not derive itself but that no other table holds:

• dispatch_plan — the program’s one dispatch plan (below), projected onto the subjects the program’s own bus sites name and the loci the model declares: each kept row’s subscriber column holds only those loci, sorted; every other column is the plan’s. The stdlib’s log.** row appears only where the program names log.** itself, and never with the stdlib’s sinks.
• stdlib_absorption — what a merged-summary walk sees inside stdlib bodies reachable from a user fn.

Absorption is kept as a graph, not a flattened summary, and its grain matters twice over. One StdlibAbsorption row is one authored entry site (with entry_group marking alternatives of one dispatch); its nodes are AbsorbedNodes forming an interior graph, each carrying AbsorbedEvents in walk order — a Call (with its own dispatch group, targeting an AbsorbedTarget: another interior node or a user re-emergence), a Publish, or one of the three residues: CallHole, PublishHole, Truncated. An interior can publish — std::log::Logger.info computes log.<path> and sends from inside its own body — so a consumer reading only relations.publishes misses real publishers.

The contracted ViaStdlib rows in relations.calls are the endpoint pair for the same paths. They collapse several entry sites into one, so a consumer counting executions reads the absorption account and skips them; counting both double-counts.

An interior publish to a computed subject is a PublishHole, and it carries the wildcard publish patterns its locus declared. The language admits a computed subject only under such a declaration and the publish site enforces it, so those patterns bound the hole: one declared io.tcp.** cannot explain a publisher of app.order.

This is what keeps exact_publishes from being the only answer available. That capability is one bit for the whole program, so reading it alone means a single stdlib I/O call — std::io::tcp logs to a runtime-chosen subject — withdraws the publisher account for every topic, degrading every family. A subject-specific question instead asks whether any residue can reach that subject. Three kinds cannot be bounded and still answer yes everywhere: an unfollowable interior call, a truncated frontier, and an interior publish whose subject expression resolves to no subject row (the absorption records the send’s subject expression, so a computed one appears as the variable’s name — comparing that as though it were a wire subject would certify straight through the publish it stands for).

Overlap between two patterns is not the same question as whether a subject matches a pattern: a subscription may itself be declared on log.**. Two ** patterns overlap when one root is a prefix of the other on a segment boundary.

ApplicationModel::validate() enforces eighteen error kinds. They group into four families:

Structural. NotCanonical (every table sorted and deduplicated by its canonical key — the model’s identity depends on it), DanglingId, DanglingProvenance, InvalidProvenanceRecord.

Residue. EmptyHole (a hole hiding nothing is not residue), CapabilityContradiction, UnrepresentedUnknown (an unknown the tables imply but no hole records).

Semantic. InvalidBound, RealizesDisagrees, RealizesIncomplete, ReplicaIndicesNotContiguous (the replicas of one field form a contiguous 0-based set — codegen bakes those indices and keyed delivery reads them), BindingSubjectDisagrees, IllegalFallback, FallbackUncovered, KeyContract, DeclaredTopicDisagrees, EndpointPayloadDisagrees.

Coverage. CoverageLaw — the ownership partition and the analysis-coverage bits, in one shared validator that both the model and the evidence sidecar call. A model whose ownership account is corrupted cannot certify anything, digests notwithstanding.

Three values sit beside a model without being part of it. Only one is derived from the model ALONE — see the layering above:

• ClaimIrTable — the lowered law, from (bundle, model): one typed row per clause, with its ordinal, origin, judgment family, typed operands (each reference carrying raw identity, author spelling and resolution state), and the GroupSelection status carried from selection rather than re-inferred.

• EvidenceTable — the certificate sidecar, from (bundle, table, model). Deliberately outside the model, because a model must not carry a cached prior judgment of itself. For the certificate and budget families it is an INPUT to judgment rather than its output: those engines measure, and the judgment decides over what they measured.

  It is tied to what it answers by five independent checks, not four: model_shape, law_digest, inputs_digest, coverage_digest, and exact equality of the source-unit list — path plus content digest — across the evidence, the model and the law table. The fifth is not implied by the others: without it, locally valid offsets could be rendered against a different source snapshot. It ties to the model by model_shape, law_digest, inputs_digest and coverage_digest; a judgment refuses evidence whose ties disagree rather than replaying it.

• DispatchPlan — (GH #476 Change 8) derived once per program from one gate set, the bus graph’s sites keyed by wire subject with the bundled stdlib’s after them, and the arrangement’s thread domains. It decides how a BUS SUBJECT dispatches — dynamic, static bucket, or static direct — not how calls in general lower. Lowering lowers it and the model holds it projected (Analyses::dispatch_plan); which flavour a subject gets is a plan conclusion, never a model row.

Eight identities and two version constants. They answer different questions and cover different data; conflating any two is a trap, and the coverage below is what the digest functions actually hash — not what their names suggest.

Two rules that are easy to get wrong.

EvidenceTable::validate compares digests; it does not hash the implementation. A sidecar produced by an older toolchain can share the source, the model shape, the law digest and the coverage digest while carrying a verdict the current compiler disagrees with. So whenever a producer change alters results — including correcting a bug — ANALYSIS_SEMANTICS_VERSION moves in the same change. It went 3 → 6 across GH #476 Change 5h alone.

And making an artifact field required is a decoding-contract change, not an additive one: an artifact written before the change passes the schema gate and is then refused for omitting something its schema never demanded. That is a TOPOLOGY_SCHEMA transition.

hale model diff <a.topology> <b.topology> [--json|--text] is the semantic difference between two topology artifacts (GH #527). It is defined over artifacts, not in-process models: both inputs are byte-reproducible, digest-verified documents a caller can keep as evidence, so the diff is replayable by anyone holding them. Each input passes the renderer’s admission gates — canonical top-level order, artifact_digest, semantics, recomputed shape_hash, exact TOPOLOGY_SCHEMA — and an artifact that fails any of them is refused, never diffed.

The output is a versioned document (TOPOLOGY_DIFF_SCHEMA, now 1.0) naming both inputs by path, artifact_digest and shape_hash, with these sections:

• declarations — one row per (kind, name) across loci, topics, fns, groups and claims: persisted, moved (same name and kind, a different source unit), renamed, split, joined, added, removed, or ambiguous. Rows carry both sides’ source sites (unit, span), with units taken relative to each artifact’s common source root so two checkouts of one program compare.
• contracts — per paired locus, facet by facet, as set differences (removed / added): sealed, params, methods, publishes, subscribes (with the subscription’s queue bound and shed policy), supervises, and the ownership (who owns its instances) and placement (which thread domains) — by owner and domain, not by instance path, so a param rename does not echo here. Plus, per paired topic, its subject and payload shape when they moved: a wider payload is a contract change for every locus on the topic. These facets are read from the artifact’s contracts and topics sections (schema 1.18+), the per-locus regrouping of facts the model already holds. A param’s type is rendered in author spelling (dna::Leader, never the mangled cross-seed symbol), like every other name in the artifact.
• effects — per paired fn, classes gained / dropped; per fn present on one side only with a non-empty effect set, a row with change: added (its classes as gained) or change: removed (as dropped) — an added locus whose handler reaches a declared class widens what the program does, and the paired rows alone would miss it; and per fn-grained certificate (lowered rows keyed by subject and form), added / removed / result changed.
• law — per paired claim, form / result / verdict / family changes; claims added and removed with their result; adequacy changes per family; the overall verdict when it moved.
• classification — identical (same artifact_digest); source-only (same shape_hash, no contract or effect rows: comments, moved lines, re-spelt law); contract (same shape_hash, but a contract facet or an effect set moved — a payload that gained a field, a param added — which the hash does not cover); or model-shape.

Matching is deterministic and names what it compared. The matching section of every document states the rules; they are:

1. Declarations pair by (kind, name). Loci are matched first.
2. A removed and an added declaration of one kind pair as a rename only when each is the other’s unique shape- signature match. A locus’s signature is its contract facets minus the instance paths (which embed its name); a topic’s is subject and payload shape; a fn’s is owner, kind and effect classes; a group’s is its members; a claim’s is its rendered form. More than one candidate on either side is reported as ambiguous, with the candidates, and the declarations stay removed / added.
3. An accepted locus or group rename is read through wherever the name recurs on the A side — fn owners (Old::m pairs with New::m), group members, param types, supervised children, claim forms — so a rename does not echo as a contract or law delta in every declaration that mentions it.
4. A split is one removed locus whose local method set is exactly partitioned by two or more added loci; a join is the mirror. Anything short of an exact partition is not a split.

Nothing is guessed. The rule about joins that make wrong hypotheses feel evidenced applies with full force to a tool whose output is a review view: a wrong “renamed” row would hide a removal and an addition behind one reassuring line.

The discipline below is contract, not style. Each rule states a property a consumer of this model is entitled to rely on.

1. Ask each question in one place. The shared queries in model_query exist because the same rule was settled in one engine and left stale in its sibling four times: delivery joined on wire identity here and on the syntactic topic link there; uncertainty was endpoint-scoped in one check and global in another.
2. Declare required_relations as what you read, then ship the adequacy entry and the schema transition together. A family a row can declare, over which the document cannot state exactness, is an internally contradictory artifact.
3. Never be silent. The check path appends diagnostics, not verdicts. A non-holds row with no diagnostic compiles clean while the artifact records law_failed — and leaves the row with no evidence for admission to find. Every non-holds verdict carries its reason, including the “this subject is outside the analyzable universe” case.
4. Scope residue to the question. Relevant reachable residue withdraws a proof; residue anywhere in the document authorises nothing.
5. Preserve the three states. None, n, not knowable are three answers. Collapsing the last two into the first is a fail-open.
6. Respect grain. Sites are executions. Sets are reachability. A quantitative law wants the former.
7. Aggregate last. Cost a whole scenario — one key, one conformer — end to end before taking any maximum. max(a) + union(b) is not max(a + b), and Σ max is not max Σ.
8. Join on the right identity for the question. For DELIVERY, the identity is SubjectId: declared_topic is a syntactic link and a literal send carries None there. But declared_topic is not vestigial — it decides declaration-sensitive questions (typed endpoint identity, require publishes / subscribes), which is why the schema keeps both. Use the wire identity for what the runtime does, the declaration link for what the author wrote. Separately: Function::name is the raw canonical identity and Function::display the demangled author spelling; joins take the former.
9. Move the semantics version when results move.

Everything above describes how the model behaves. This is what it contains: every public type, so nothing in the crate is reachable-but-undescribed.

Field-level documentation is the rustdoc — every public field carries a doc comment, and a test fails if one lands without. It is published with the book at /api/hale_model, so reading a row does not require cloning the compiler.

application — the model itself and its sidecars. ApplicationModel, ModelHeader, ModelHashKind, Entities, Relations, Analyses, LabelRow, WeightRow, ModelError. Absorption: StdlibAbsorption, AbsorbedNode, AbsorbedEvent, AbsorbedTarget, AbsorbedHoleKind. Evidence: EvidenceTable, EvidenceRow, CertificateEvidence, VerdictIr. Plus DispatchGate.

entity — the fifteen sorts. Function, FunctionKind, LocusDecl, LocusParam, LocusInstance, Topic, Subject, PayloadContract, Phase, Seed, ThreadDomain, Binding, BindingRole, TransportKind, Group, TypeDecl, InterfaceDecl, EffectClassDecl, EffectClassDefinition, Declaration, DeclKind.

surface — the surface family (GH #1417): Surface, SurfaceRow, RowType, and the digest framings (surface_digest_input, stream_digest_input) with their folds.

relation — the seventeen relation row types. Structure: MemberOf, PhaseOf, DeclaredIn, Realizes, Owns. Behaviour: Call, DispatchKind, DeadInterfaceCall, Publish, Subscribe, DeclaresPublish. Placement: PlacedIn, AffinedTo, CoreSet. Wiring: TopicBinding. Supervision: Supervises, SupervisedRef, SupervisionPolicy. Groups: GroupMember, GroupSelector, SelectorForm. Cost: CostSite, CostDimension.

keys — delivery’s typed vocabulary. KeyDomain, KeyValue, KeyPredicate, TopicKey, KeyOnUnmatched, PublishDisposition, Capacity, ShedPolicy, TopicBound, TopicOnFull, BindingLossBehavior.

claim_ir — lowered law. ClaimIrTable, ClaimRow, ClaimIr, ClaimOrigin, ClaimIrError, LoweringIssue. Operands: NameRef, GroupRef, TopicIrRef, PhaseIrRef, SeedIrRef, EffectClassRef, BusSelector, GrantIr, SetIr, CountCmpIr, QuantDimIr.

hole — Hole, HoleKind, RelationSet.

capability — Capabilities.

provenance — Provenance, ProvenanceTable, SourceUnit.

ids — the newtype ids and EntityRef. A row’s id is its index in its own table.

dispatch_plan — DispatchPlan, SubjectPlan, DispatchFlavor. Conclusions derived from the dispatch gates and the arrangement, never authored facts.

obs_ids — ObsEntityId, ObsEntityKind, the join back from an observed record to a model row.

Three of these are easy to mistake for each other, and the difference is load-bearing:

• GroupMember is resolved membership; GroupSelector is the authored selector list. { lib::* } and { lib::A, lib::B } can resolve identically and must still hash differently.
• Publish is a send expression; DeclaresPublish is the declared endpoint. A locus that declares an end and never sends still publishes in the endpoint sense.
• Call’s DispatchKind is the fact of the mechanism; DispatchFlavor in the lowering plan is the conclusion drawn from it.

Stated so nobody mistakes them for oversights:

• The model is in-process only — see Obtaining a model. No wire form, no reconstruction from an artifact.
• CostDimension::Block and FrameBytes are recorded, but the quantitative engines still measure over their own summary; the model carries the facts and the judgment reads the engines’ evidence.
• Frame sizes are estimated from declared shapes, not measured from codegen. The bound is a structural over-approximation and the diagnostic says so.
• Absorption interiors are explored to a frontier. Beyond it the account is Truncated, which withdraws rather than assumes.