Claims & the law

The effects chapter taught one function to make a promise. This chapter is the complete reference for the promises no single function can make: claims…

The effects chapter taught one function to make a promise. This chapter is the complete reference for the promises no single function can make: claims — named sentences over the assembled program graph, declared on the main locus, evaluated by hale check as errors, and lowered to zero runtime code.

The chapter is organized as a reference: the grammar first, then each declaration and verb with its exact semantics, the evaluation model, every diagnostic the surface can produce, and the topology artifact. If you want the workflow story instead — write the law first, let countermodels drive implementation — read Claim-Driven Development in Hale.

One program exercises most of the surface. Two wings, one boundary temptation. It is written to be refused, so the build stops at its claim:

type Task { id: Int; }
type Metric { n: Int; }
topic Tasks   { payload: Task; }
topic Metrics { payload: Metric; }

locus DeltaTriage {
    params { seen: Int = 0; }
    bus { subscribe Tasks as on_task; publish Metrics; }
    fn on_task(t: Task) {
        self.seen = self.seen + 1;
        Metrics <- Metric { n: t.id };
    }
}

locus GammaResearch {
    params { total: Int = 0; }
    bus { subscribe Metrics as on_metric; }
    fn on_metric(m: Metric) { self.total = self.total + m.n; }
}

group delta_wing = { DeltaTriage };
group gamma_wing = { GammaResearch };

main locus Org {
    params {
        triage: DeltaTriage = DeltaTriage { };
        research: GammaResearch = GammaResearch { };
    }
    claims {
        iso_dg: forbid reaches(delta_wing, gamma_wing);
    }
}

fn main() { Org { }; }

This program fails to check, and the diagnostic returns the route:

claim `iso_dg` violated: `delta_wing` reaches `gamma_wing` —
witness: `DeltaTriage::on_task` -(publishes "Metrics")-> `GammaResearch::on_metric`

Everything below is the precise definition of what just happened, plus every other sentence the surface can state.

The complete surface, as it appears in spec/grammar.ebnf:

group_decl        = "group" , IDENTIFIER , "=" , "{" ,
                    [ group_member , { "," , group_member } , [ "," ] ] ,
                    "}" , [ "may_be_empty" ] , ";" ;
group_member      = IDENTIFIER , { "::" , IDENTIFIER } , [ "::" , "*" ]
                  | "role" , IDENTIFIER ;

domain_decl       = "domain" , IDENTIFIER , "=" , "{" ,
                    IDENTIFIER , { "," , IDENTIFIER } , [ "," ] ,
                    "}" , ";" ;
effect_family_decl
                  = "effect" , IDENTIFIER , "(" , IDENTIFIER , ")" , ";" ;

claims_block      = "claims" , "{" , { claim_entry } , "}" ;
                  (* inside main locus: the world tier;
                     at top level: the library tier (#392) *)
claim_entry       = ( IDENTIFIER , ":" , claim_form , ";" )
                  | ( "adopt" , IDENTIFIER , ";" ) ;
claim_form        = forbid_form | only_edges_form | bound_form
                  | require_form | cover_form | route_form
                  | count_form ;

forbid_form       = "forbid" , "reaches" , "(" , claim_set , "," ,
                    claim_set , ")" ,
                    { via_clause | during_clause | avoiding_clause } ;
via_clause        = "via" , "{" , via_relation ,
                    { "," , via_relation } , [ "," ] , "}" ;
via_relation      = "calls" | "bus" ;
during_clause     = "during" , IDENTIFIER ;
avoiding_clause   = "avoiding" , IDENTIFIER ;

only_edges_form   = "only" , "edges" , IDENTIFIER , "->" ,
                    IDENTIFIER , "{" , { edge_grant } , "}" ;
edge_grant        = ( "publish" | "subscribe" ) , topic_ref , ";" ;

bound_form        = "bound" , effect_class_ref , "<=" , INT_LIT ,
                    "on" , "paths" , "from" , IDENTIFIER ;

require_form      = require_endpoint | require_sealed
                  | require_attributed | require_no_silent_loss ;
require_endpoint  = "require" , ( "subscribes" | "publishes" ) ,
                    "(" , "some" , IDENTIFIER , "," , "topic" ,
                    topic_ref , ")" ;
require_sealed    = "require" , "sealed" ,
                    "(" , "all" , IDENTIFIER , ")" ;
require_attributed = "require" , "attributed" ,
                    "(" , "all" , IDENTIFIER , ")" ;
require_no_silent_loss
                  = "require" , "no_silent_loss" , "(" ,
                    ( ( "topic" , topic_ref ) | ( "all" , IDENTIFIER ) ) ,
                    ")" ;

cover_form        = "cover" , "topic" , "in" , "seed" , "(" ,
                    IDENTIFIER , ")" , ":" , "subscribed_by" ,
                    "(" , "some" , IDENTIFIER , ")" ;

route_form        = "cover" , "keys" , "(" , "topic" , topic_ref ,
                    [ "in" , key_bound , "..=" , key_bound ] , ")" ,
                    ":" , "delivered_to" , "(" , "exactly_one" ,
                    IDENTIFIER , ")" ;
key_bound         = [ "-" ] , INT_LIT ;
count_form        = "count" , ( "publishers" | "subscribers" ) ,
                    "(" , "topic" , topic_ref , ")" ,
                    ( "==" | "<=" | ">=" ) , INT_LIT ;

claim_set         = IDENTIFIER
                  | "effects" , "(" , effect_class_ref , ")" ;
topic_ref         = IDENTIFIER , { "::" , IDENTIFIER } ;
effect_class_ref  = IDENTIFIER , [ "(" , ( IDENTIFIER | "*" ) , ")" ] ;

Every introducer — group, domain, claims, forbid, reaches, via, during, avoiding, only, edges, bound, require, cover, count, seed, may_be_empty, and the predicate words — is a contextual keyword: recognized in position, still usable as an ordinary identifier everywhere else. The exceptions are words that were already hard keywords (bus, publish, subscribe, on, in), which simply appear as themselves.

group delta_wing = { delta::*, DeltaStore, helper_fn };
group gamma_wing = { gamma::Research };
group probes     = { } may_be_empty;

A group names declared program elements: loci, free functions, and imported declarations. Membership is spelled out, never pattern-matched.

Member forms.

Types, topics, and constants matched by a glob are silently skipped — they are not path vertices, so they contribute nothing a reaches walk could use. A glob still counts as resolved if the alias exists at all.

Guards. Every one of these is an error, not a silent degradation:

• an unknown single-segment member — with a did-you-mean over declared loci and fns;
• a qualified member matching no import (does not resolve);
• a glob over an alias this bundle never imports;
• a nested glob (parse error: the glob is trailing-only, like ** in bus subjects);
• a role member naming a role nothing declares — with a did-you-mean over the declared roles;
• a role member whose role no surface row requires, unless the group says may_be_empty;
• a group declared twice;
• a group that resolves to zero declarations, unless it says may_be_empty — a claim quantifying over an empty group holds vacuously, which is a fail-open wearing formal clothing;
• a group whose declarations have no executable surface (all pure-data loci), used at a forbid or only edges endpoint or a bound source — projection vacuity: the vocabulary is non-empty but the fn-grained walk would prove nothing, so the claim refuses instead of passing.

Projection. Claims evaluate at the function grain. A locus in a group projects to all of its methods, lifecycle hooks (birth, accept, release, run, drain, dissolve), and modes. Projection only ever adds sources and sinks — the conservative direction. A free fn projects to itself.

requires on a surface row is a check at the serve site; it says nothing about what the handler reaches. A role member makes the claim you actually mean statable: which code can a caller with this role set in motion?

role reader;
role editor includes reader;

type Change { what: String; }
type Query { n: Int; }
topic TodoChanged { payload: Change; }

locus Todos {
    params { n: Int = 0; }
    bus { publish TodoChanged; }
    fn add(q: Query) -> Int {
        self.n = self.n + q.n;
        TodoChanged <- Change { what: "added" };
        return self.n;
    }
    fn list(q: Query) -> Int { return self.n; }
}

locus Feed {
    params { seen: Int = 0; }
    bus { subscribe TodoChanged as on_change; }
    fn on_change(c: Change) { self.seen = self.seen + 1; }
}

api Todo {
    rpc Todos::add requires: [editor];
    rpc Todos::list requires: [reader];
}

group read_side = { role reader };
group changes   = { Feed };

main locus App {
    params { todos: Todos = Todos { }; feed: Feed = Feed { }; }
    claims {
        a_reader_publishes_nothing: forbid reaches(read_side, changes);
    }
}
fn main() { App { }; }

role reader resolves, through the same selection the surfaces use (surfaces::select_members, over every surface of the program), to the handler of every member a caller holding reader may call. A caller holds the role and every role it includes, so role editor names Todos::add and Todos::list, while role reader names Todos::list alone. A member that requires nothing is callable by anyone, so it is in every role’s group. A handler that is a locus method resolves to that one method — not the whole locus, whose other methods other roles reach — and a handler shared by two surfaces is in a group once. Every verb then works over it unchanged. Make list publish TodoChanged and the claim above is violated, the witness naming Todos::list → TodoChanged → Feed::on_change.

This is a proof over the program, about the roles the program states: who actually holds reader is still the role source’s business at the serve site.

domain wing = { delta, gamma };

effect llm;
effect knowledge(wing);

@effects(is: {knowledge(delta)})
fn read(key: String) -> Idea { ... }

domain declares a closed index set. effect NAME(domain); declares an indexed family: every instantiation (knowledge(delta), knowledge(gamma)) is interned as an ordinary declared class, and NAME(*) as a composed class whose mask is the union of every instantiation. Because the reduction lands on the ordinary class machinery, everything composes with no new rules:

• instantiations appear anywhere a class name does — @effects(is:/only:/none:/causes:) lists, composed-class definitions (effect sensitive = { knowledge(delta) };), claim sinks (effects(knowledge(delta)), effects(knowledge(*))), bound, and @budget keys;
• a misspelt index (knowledge(delt)) interns a name nothing declared and is rejected with a did-you-mean over declared instantiations;
• an @effects(only: {knowledge(delta), …}) contract computes its complement from the live class universe over atomic classes, so a domain member added later lands outside every existing contract — the fail-closed direction, inherited rather than re-derived;
• instantiations travel across seed boundaries through the merged class table like any user class.

Rules. The domain must be declared earlier in the same file as the family (this is what lets every instantiation be expanded eagerly). An empty domain is a parse error (every family over it would be vacuous). A duplicate domain is a parse error. Family instantiations count against the same effect-mask capacity as every class — a family over a large domain that overflows the mask is rejected at the declaration, fail-closed.

The companion budget. @budget(<user class> = N) bounds calls to declared carriers of the class along any path, with the standard per-call rules: a carrier inside a loop is unbounded, an unresolvable edge is unbounded, an undeclared class name is an error with a did-you-mean, a duplicate dimension is a parse error, and a built-in class as a key is a parse error (the counted built-ins keep their own spellings: alloc_per_call, publish, block_points, stack_bytes, fanout).

The block has two homes, one per tier:

• Inside main locus — the WORLD tier. Main is the closed-world gate: bundle-wide sentences cannot be evaluated before the whole application graph exists, and one-main-per-bundle makes the claims root unique. Inside any other locus it is a parse error.
• At top level in a LIBRARY seed — the library tier (see Library-tier claims below): a seed swears about itself and its own boundary, and the block travels with the import. A seed that declares main locus writing the top-level form is a check error — world law belongs in main.

A main locus may carry several claims { } blocks; their entries concatenate. An inline claim resolves the groups it names in the seed that declares it, so importing a whole application — as its own tests do — leaves its law meaning exactly what it meant when the seed was checked on its own, and a group of the same name in the importing seed is never substituted for it.

That holds for a group the seed never declared, too: a claim naming an undeclared group is an error in the seed that wrote it, and stays one however the seed is imported. An importing seed that happens to declare group guests = { … }; does not answer another seed’s guests — the error you saw checking the seed alone is the error the closing build reports, naming the group you wrote. The same goes for a library-tier claims { } block, and for a constitution in a seed that declares its own main locus.

A constitution in a seed with no main is the exception, and the one place an open name is deliberate: that seed closes no world, so its clauses are adopted somewhere else and each adopting entrypoint declares the vocabulary — see One law, many entrypoints.

Every entry is name: form;. The name is the contract of record — it is what the diagnostic, the CI check, the review policy, and the topology artifact cite — and it must be unique across all blocks (a duplicate is an error). Claims gate hale check as errors; there is no advisory tier, because a warning that reads “tenant isolation is false” is a law that doesn’t bind. Weakening a claim requires a source diff — deleting a forbid, widening a grant list, raising a bound — and that diff is the review event.

iso: forbid reaches(delta_wing, gamma_wing);
iso_calls: forbid reaches(delta_wing, gamma_wing) via { calls };
data_iso: forbid reaches(delta_wing, effects(knowledge(gamma)));
quiet_boot: forbid reaches(positions, effects(llm)) during birth;
gated: forbid reaches(public_api, ledger) avoiding authorization_gate;

Sets. SRC must be a group. DST is a group or effects(<class>) — the class may be a built-in, a user class, a composed class, a family instantiation, or a family star (effects(...) in source position is an error).

The relation. The walk starts from every fn in SRC’s projection and composes two edge kinds:

• calls — resolved call-graph edges: free-fn calls, self methods, handle methods on typed receivers, interface-slot defaults, calls into imported seeds, and calls through the Hale-source stdlib (its bodies are merged into the walk, so a chain through a stdlib locus resolves rather than stopping at the boundary).
• bus — for each publish site in the visited fn’s own body with a statically-known subject, an edge to every subscriber handler of that subject — including subscribers whose ** wildcard pattern covers it (a log.** sink is an edge from every log.x publish; more edges is the conservative direction).

via { calls } or via { bus } restricts the composition; omitting via selects both — the conservative default. via { } with no relations is a parse error. Note the precise meaning of via { bus }: it composes declared wiring — a publish reached only through a call chain needs calls in the relation to be seen.

Hits. A visited fn is a violation if it is in DST’s projection (group form) or if its direct effects intersect the class mask (effects form: its is: classification, its allocation sites, its publish sites, its classified stdlib and FFI leaf calls). Roots are tested too: a declaration in both groups is a zero-length path and reports as a violation — boundary confusion is surfaced, not skipped.

Vacuity. An empty DST group (via may_be_empty) forbids nothing: the claim holds. An empty SRC likewise. Both are only reachable through the explicit opt-out; everything else fails the group guards first.

during <phase>. Restricts SRC’s projection to the members of <phase> in the model’s phase relation: lifecycle hooks (birth, accept, release, run, drain, dissolve) and modes (bulk, harmonic, resolution) are hook-phases the runtime drives; any method or handler name is its own source-slice phase. Free fns have no phases and drop out. If the filter empties a non-empty projection, that is an error (“phase names nothing in group”), not a vacuous pass. The relation is exported in the topology artifact (phases), which is what makes a during row independently re-derivable; it is still a source slice, not a temporal logic.

avoiding <group>. Masks the named group’s vertices out of the walk entirely — neither traversed nor tested. This is the interposition form: “every path from A to B passes through G” is literally “no path from A to B exists while G is masked”. The mask must be disjoint from both endpoints: masking the target would hold vacuously, masking a source silently drops roots, and either overlap is an error.

Modifiers stack in any order: forbid reaches(a, b) via { calls } during birth avoiding gate;.

The witness. One minimal countermodel per violated claim: the path from a source root to the hit, calls rendered ->, bus hops rendered -(publishes "subject")->, every name in author spelling (cross-seed symbols demangled).

Where to edit. The witness names who; secondary diagnostics point at where — the call that crosses the boundary (or, for a bus hop, the publish site and the subscription declaration) and the forbidden destination’s declaration, in the effect system’s root + leaf shape. A hop whose source lives inside a stdlib body renders by name alone: stdlib source parses in its own offset space, and a span from there would point at the wrong line of your file.

grant: only edges gamma_wing -> delta_wing {
    publish t::ResearchDigest;
};

Every direct edge from A into B must match a granted line; every un-granted edge is reported (all of them, not just the first — the grant list is the review surface, so the full diff matters).

• A grant names a declared topic. publish T and subscribe T admit the same edge — the verb documents which end’s declaration a reviewer should go read. A grant naming a topic that does not exist is an error (with a did-you-mean hint), not a grant that quietly does nothing: a dropped grant would evaluate a weaker claim than the one you wrote and report its violations as if you had chosen them.
• Call edges are never grantable. A direct call from A into B is always an un-granted edge: a permitted cross-domain dependency should be a named bus edge, not an invisible method call.
• A subscriber outside B is not an A→B edge — the shared log.** sink needs no grant.
• An edge on a literal or wildcard subject cannot be granted (grants name declared topics) and therefore fails closed if it lands in B — restructure onto a declared topic.
• Direction matters: only edges A -> B says nothing about B→A edges. And it is a direct-boundary property, not an exception to forbid: a granted edge still creates a path, so a blanket forbid reaches(A, B) over the same direction would reject it, and a boundary enumeration does not exclude transitive routes through a third group. Write the sentence the architecture means.

one_call: bound llm <= 1 on paths from positions;

C must be a user-declared class or secret_use (any other built-in here is an error pointing at the @budget spellings); composed classes and family instantiations work through their masks. The quantity is the per-invocation aggregate — a call-tree sum, exactly @budget’s semantics: if a handler calls two helpers and each reaches the model once, the count is two. It does not become one because each root-to-leaf chain contains one call. Bus hops are followed: a publish contributes every subscriber’s count.

Unbounded — and therefore a violation of any finite bound — are: a carrier reachable inside a loop, a carrier under recursion, an indirect call, an unresolvable receiver, a computed publish subject. An operation that might hide a carrier must prevent certification rather than count as zero.

The violation carries the measured count and a representative heaviest chain; the unbounded case names which condition made it uncountable.

wired: require subscribes(some delta_wing, topic t::Tasks);
feeds: require publishes(some delta_wing, topic t::Done);

At least one locus member of the group must declare the subscription (or publication) in its bus { } block — “wired” is a declaration property, checked over the declared bus ends. The violation names the group and the topic. The topic reference must resolve to a declared topic (qualified refs canonicalize at the mangle stage; unknown names error with a did-you-mean).

payments_arrive: require no_silent_loss(topic Payments);
money_is_safe:   require no_silent_loss(all money);

A route is a wire subject: a topic’s, or the subject a literal endpoint names. topic T claims one route; all G claims every route a member of G publishes or subscribes — through its sends, its declared publish ends and its subscription handlers (a group that touches no route is an error, not a vacuous truth). The claim is that no boundary on the route is configured to discard silently. It reads the settings the model records, at every boundary on the route, whoever owns it — a subscriber outside the group still sits on the route.

A wildcard endpoint is a route for every wire it covers. A group member subscribing "pay.**" (or declaring publish "pay.**") brings in each modeled address the pattern matches — pay.event’s topic policy, its sends and its bindings are judged as if the member had named it — and the pattern itself, for the remainder no modeled endpoint names. Addresses match the way the bus matches them: an address is the literal text a send carries, so a topic whose own subject is spelled "pay.inner.**" is a wire under "pay.**" and is judged like any other.

on_unmatched: fail and fallback are not silent: the first makes the send fallible, the second delivers the unmatched message to the where key == _ subscriber. A refusal the caller can see is not a silent discard — or raise, or wait, or a plain send on a topic that can refuse nothing. A violation lists every silent setting, naming the boundary and what it is set to.

What the claim does not prove, and says so rather than holding:

• A send that routes its refusal into a custom handler (or println("…"), or fail … on an on_unmatched: fail topic) is reported uncertified, naming the send. The model records that a handler exists, not what it does with the refusal, and the mere presence of a handler proves little.
• A connect binding drops the publishes of a window in which its link is lost, and whether that is handled is supervision policy (on_failure on the main locus). The route is uncertified unless every send on it is or wait. A listen binding fails the binding instead, and holds.
• A hole that hides the route’s subscribers, publishers or delivery (an adapter transport, an unanalyzed publisher) leaves the route uncertified.
• A publisher the model cannot resolve is route evidence it does not have. A send to a computed subject (self.subject <- v) is admitted only under its locus’s declared publish patterns, so it may reach every route one of those patterns covers, with a subject and a refusal policy the model does not know: the route is uncertified, naming the function. The declaration bounds it — the publish site enforces the pattern — so a send declared under "audit.**" says nothing about pay.event. A body the analysis did not walk, or a stdlib interior that may publish on the route, is unproven the same way.

A silent setting always beats an unproven one: a route that is configured to discard is violated however many handlers it also has.

This is a configuration claim. It says no modeled boundary is set to lose; it does not account for an accepted message through to its processing, and it promises nothing across a process failure or from a dependency that is down — those need durability and acknowledgement semantics the model does not have.

Here is a route that fails the claim, then the same route configured so it holds:

type Payment { account: Int = 0; cents: Int = 0; }

topic Payments {
    payload: Payment;
    subject: "payments";
    keyed_by account;
}

locus Ledger {
    params { booked: Int = 0; }
    bus { subscribe Payments as on_payment bounded(64, drop_old) where key == 1; }
    fn on_payment(p: Payment) { self.booked = self.booked + p.cents; }
}

locus Gateway {
    bus { publish Payments; }
    fn pay(account: Int, cents: Int) {
        Payments <- Payment { account: account, cents: cents };
    }
}

group money = { Ledger, Gateway };

main locus App {
    params { ledger: Ledger = Ledger { }; gate: Gateway = Gateway { }; }
    claims {
        payments_arrive: require no_silent_loss(topic Payments);
        money_is_safe:   require no_silent_loss(all money);
    }
    run() { self.gate.pay(1, 500); }
}
fn main() { App { }; }

claim `payments_arrive` violated: route `Payments` is configured to discard silently — topic `Payments` keyed by `account` is `on_unmatched: swallow`; subscriber `Ledger::on_payment` on `Payments` is `bounded(64), on_full: drop_old`
claim `money_is_safe` violated: a route of `money` is configured to discard silently — topic `Payments` keyed by `account` is `on_unmatched: swallow`; subscriber `Ledger::on_payment` on `Payments` is `bounded(64), on_full: drop_old`

The repair is in the configuration, not the claim. An unmatched payment now fails the send, the sender raises it, and the ledger’s queue is unbounded:

topic Payments {
    payload: Payment;
    subject: "payments";
    keyed_by account;
    on_unmatched: fail;
}
// Ledger:  subscribe Payments as on_payment where key == 1;
// Gateway: Payments <- Payment { account: account, cents: cents } or raise;

Replace or raise with or println("dropped") and both claims turn uncertified — “the send in Gateway::pay on Payments routes its refusal into a custom handler” — until the handler is replaced by something the claim can read.

no_orphans: cover topic in seed(t): subscribed_by(some positions);

Every topic declared by the seed imported as t (the claiming file’s own import alias — there is no global seed namespace) must have a subscriber in the group. The violation lists every uncovered topic. An alias that names no imported topic vocabulary is an error: an empty coverage domain would hold vacuously.

single_writer: count publishers(topic t::Tasks) == 1;
consumed: count subscribers(topic t::Done) >= 1;
capped: count subscribers(topic t::Audit) <= 2;

Counts distinct declared loci on the chosen end of the topic. == 1 is the single-writer invariant. A violation reports the actual count and names the participating loci. These are counts over declarations, not a runtime census of replicated instances — exact instance counts are a fleet claim (count_publisher_instances in a fleet plan; see Checking the whole deployment).

one_worker: cover keys(topic Orders in 0..=3): delivered_to(exactly_one workers);
whole_type: cover keys(topic Orders): delivered_to(exactly_one workers);

A keyed topic routes each message by one field, and each subscriber says which keys it takes: where key == 3, where key == replica, or where key == _ (the fallback). Nothing in those declarations says that every key lands somewhere, or that no key lands in two places. This claim does: for every permitted key, the registrations of the group that receive it number exactly one.

type Order { shard: Int = 0; qty: Int = 0; }
topic Orders { payload: Order; subject: "orders"; keyed_by shard; }

locus Worker {
    params { seen: Int = 0; }
    bus { subscribe Orders as on_order where key == replica; }
    fn on_order(o: Order) { self.seen = self.seen + o.qty; }
}

locus Audit {
    params { n: Int = 0; }
    bus { subscribe Orders as on_any; }
    fn on_any(o: Order) { self.n = self.n + 1; }
}

group workers = { Worker };

main locus App {
    params { w: Worker = Worker { }; audit: Audit = Audit { }; }
    placement { w: pinned(cores = 0..4, replicas = 4); }
    bus { publish Orders; }
    claims {
        one_worker: cover keys(topic Orders in 0..=5): delivered_to(exactly_one workers);
    }
    run() { Orders <- Order { shard: 1, qty: 2 }; }
}
fn main() { App { }; }

Four pinned replicas answer keys 0 through 3; the claim says keys 0 through 5 are permitted, so two are nobody’s:

claim `one_worker` violated: not every key of `Orders` reaches exactly
one registration of `workers` — uncovered: no registration of `workers`
receives keys 4..=5 (the publish is silently swallowed; its recipients
lie outside the group: `Audit::on_any`)

Change the interval to 0..=3 and the claim holds, even though Audit also receives every key: the claim counts recipients in the named group, so an audit or metrics subscriber outside workers cannot break the worker group’s uniqueness. Put Audit in the group and the same claim is violated — Audit::on_any and the replica it shares each key with are named as the two registrations.

The permitted keys. in LO..=HI states an inclusive integer interval (a leading - is allowed: in -3..=3; an empty interval is a parse error). Without it, the permitted keys are what the topic’s publish sites can produce: the whole Int range for an Int key, {false, true} for Bool, every value of the type otherwise. An Int topic with four replicas and no stated interval is therefore violated on -9223372036854775808..=-1, 4..=9223372036854775807 — state the interval you mean, or give the group a where key == _ fallback subscriber on an on_unmatched: fallback topic, which receives every key nothing else matched and covers the rest.

That derived domain is only as complete as the publish sites the model can see. A publisher the model could not resolve that may send on the topic’s wire — a send to a subject computed at runtime whose locus declares a covering pattern (publish "pay.**" of type Pay beside a topic on pay.event), a body the model did not walk, a stdlib interior — may send keys outside it, so without in LO..=HI the claim is uncertified and names that publisher. A stated interval is the domain whatever such a publisher sends, so with one the claim is judged as usual.

What counts as a registration. One instance of a subscribing locus. Three arranged replicas of one subscribe are three registrations; two instances of a locus with where key == 7 are two recipients of key 7, and the overlap names both by instance path. Recipients are computed by the same query the @budget(fanout) budget uses, so the two cannot disagree about who a key reaches.

Fail-closed cases (never holds; the diagnostic says what to resolve). Where the graph has an unknown, the result is uncertified; where the statement itself is malformed, it is invalid:

An unknown filter on a subscriber outside the group still withdraws the answer: a fallback hears only what no filter anywhere matched, so a filter nobody can evaluate may absorb any key.

What it proves, and what it does not. It proves a fact about the modeled arrangement: each permitted key selects exactly one registration of the group. It does not cover replacement, restart or a runtime birth — those change the live registrations, and preserving uniqueness across them needs a stronger invariant over live registrations and incarnations. It is not exactly-once processing, which needs request identity, retry, persistence and acknowledgement. It does not say a publisher only produces permitted keys: a key outside the interval is outside the claim, and the topic’s on_unmatched policy governs it. And a cell a full queue sheds or a binding drops is a separate question (loss policy).

A library seed states its own law in a top-level claims { } block — no main locus required:

type Charge { amount: Int; }
topic Charges { payload: Charge; }

locus Wire {
    params { seen: Int = 0; }
    bus { subscribe Charges as on_charge; }
    fn on_charge(c: Charge) { self.seen = self.seen + c.amount; }
}

group settlers = { Wire };

claims {
    single_settle: count subscribers(topic Charges) <= 1;
    wired: require subscribes(some settlers, topic Charges);
}

Two properties make this the library tier:

• The law travels. Import the seed and its claims come along, re-evaluating in every closing build over the merged world. Checked standalone, the seed satisfies itself; when an app quietly wires a second subscriber onto Charges, the library’s own single_settle refuses the build — reported with seed attribution (claim `pay::single_settle` violated, never a mangled symbol) and pointing at the library’s own claim line. Getting stricter as the world grows is the point: the claim quantifies over whatever the merge added.
• The tier is the enforcement surface. A seed swears about itself and its own boundary — it can only name what it can see: its own decls, its own imports. World-quantification stays main’s, and a seed that declares main locus writing the top-level form is a check error. A dependency cannot brick a downstream build with world-claims because it has no way to state one.

Claim names stay per-seed (pay::single_settle and your own single_settle coexist); group and topic references inside a traveling block canonicalize across the seed boundary exactly as group declarations do.

What the sentences quantify over:

sorts:      fns, loci, topics (+ subjects)
relations:  calls        resolved call edges, stdlib bodies merged
            publishes    fn -> statically-known subject
            subscribes   subject -> (locus, handler), wildcards included
labels:     effect classes (declared carriers via is:), groups
weights:    carrier-site counts (bound, @budget)

Groups name declarations; each verb projects them onto the sorts its relation needs; evaluation is fn-grained. Each claim produces one of three results — holds, violated, or invalid (a vocabulary or reference error prevented evaluation) — and the result set is what the artifact records.

The fail-closed rules. Deriving the graph is the trust root, and the direction is fixed: uncertainty may add possible edges; it may never delete an edge and report success. Concretely, any judgment that traverses calls refuses to certify over:

• an indirect call that no function value of the program can answer. A call through a function value — a function-typed parameter, a local the compiler can’t pin to one function, a computed callee — is judged as a call of each function the program reads as a value whose signature fits (the router’s add_fn handlers are the everyday case), and a call through a local bound to a function by let is the call of that function (let f = pid; f() is judged as the call of pid it is); only a call none of them can be stays unknowable;
• a method call on a receiver the compiler cannot type. The summarizer types bare vars, self fields, chained fields (through locus and struct field maps), struct-literal receivers, known-fn call results, uniform if/else values, or-unwrapped values, single-slot collection .get(i) results, and for-binders over array fields, capacity slots, array params, array literals, and the implicit accepted-children collection. What remains — an index result, a match value, a foreign expression — fails closed, with a diagnostic that says how to fix it: bind the receiver to a typed field or local. The same rule applies in the effect and budget walkers, so a fn-level certificate and a bundle-level claim always agree;
• a computed publish subject (it could route to any subscriber);
• a walk exceeding the step ceiling.

Interface dispatch fans out. A method call on an interface-typed value — route.handler.handle(ctx), the stdlib router’s own shape — is not an unknown: the world is closed, so the implementor set is enumerable. The summarizer fans the one written edge out to every conforming locus (structural name-and-arity conformance over the declarations — a superset of the checker’s typed conformance, safe because over-approximation only adds edges). Reachability and effect judgments walk every alternative; counting judgments (bound, @budget, the quantitative dims) take the max over one dispatch site’s alternatives, because an invocation dispatches to exactly one target — a sum would count phantom calls no execution performs.

An interface-typed field narrows to what is stored in it. A call through a field of interface type (self.h.dep.apply(x)) fans out to the loci the program stores into that field, not to every conformer: every Locus { field: Impl { } } literal at any instantiation site (a parameter default is one: fn take(h: Holder = Holder { dep: Real { } }) stores Real whenever take() omits the argument), and the declaration’s default when some literal of the locus omits the field (or none is seen), intersected with the interface’s conformers. Only a struct literal of a locus narrows. A field the program also writes from somewhere the pre-pass cannot name — a literal whose value is a parameter, a call result, an if/match value or a local (Holder { dep: g } with g: Gate), a default that is not a literal, any assignment place.dep = g — keeps every conformer: the set is closed only when every write is seen, and a write that is not seen puts the whole conformer set back. An assignment’s receiver is not typed, so it is read as a write to the dep of every locus that has one. A literal of an imported seed’s locus (lib::Holder { dep: lib::Real { } }) counts like any other. A seed with no main locus closes no world, so none of its slots narrow: its loci are built by whoever imports it. Slots of standard-library loci are never narrowed. A parameter, a local or a function result of interface type is not a field and always fans to every conformer.

An interface no locus conforms to is different again: an interface value only ever arises by coercing a conforming locus, so in a closed world an uninhabited interface has no values and its call sites are dead — they contribute nothing to any judgment (the router’s m.before(cur) over an empty middleware list is the everyday case). The artifact records each such site (uninhabited_interface_call:<interface>.<callee>) inside the hashed model half, so a conformer appearing in a later build changes shape_hash.

The complete catalog, grouped by stage. Parse errors:

Vocabulary and reference errors (evaluation refuses; the claim’s result is invalid):

Violations (the claim’s result is violated):

World law — a claims { } block over the whole program — is only legal inside main locus, and that rule is load-bearing: such claims are closed-world statements, and main is the only place a world is closed. But that constrains evaluation, not authoring. Copy-pasting a law into twenty main loci means the copy somebody forgets fails open, silently.

A constitution is a named claimset declared once, outside any main, and adopted by each entrypoint:

type Settlement { n: Int; }
topic Settled { payload: Settlement; }

locus Billing {
    bus { publish Settled; }
    fn settle(n: Int) { Settled <- Settlement { n: n }; }
}

locus Ledger {
    params { total: Int = 0; }
    bus { subscribe Settled as on_settled; }
    fn on_settled(s: Settlement) { self.total = self.total + s.n; }
}

locus Research {
    params { notes: Int = 0; }
    fn note() { self.notes = self.notes + 1; }
}

group billing  = { Billing };
group research = { Research };

constitution Core {
    tenant_iso: forbid reaches(billing, research);
    one_writer: count publishers(topic Settled) == 1;
}

main locus App {
    params {
        b: Billing = Billing { };
        l: Ledger = Ledger { };
        r: Research = Research { };
    }
    claims {
        adopt Core;
        local_rule: require publishes(some billing, topic Settled);
    }
}

fn main() { App { }; }

Every clause is still evaluated here, in this entrypoint’s closed world. One text, N evaluations, N worlds — nothing about the soundness argument changes.

constitution Dev extends Core {
    no_real_payments: forbid reaches(app, payment_provider);
}

An environment may add laws, never drop them. Development wanting stricter law than production is the safe direction and a genuinely useful one — “nothing reaches the real payment provider”, satisfied by the dev entrypoint wiring a stub. The dangerous direction is the reverse: a law in production that development lacks means development never exercised production’s architecture, and the first violation surfaces at the production build.

Composition is union, and nothing else. A derived constitution cannot replace an inherited clause:

constitution B extends A { rule: count publishers(topic T) == 9; }
//                         ^ error if `A` also declares `rule`

That looks like a restriction and is actually the point. If override were allowed, weakening would be expressible and would read exactly like ordinary composition at the adoption site — and telling strengthening from weakening means proving one sentence implies another, which fails open when it gets that wrong. With union only, a stricter bound is simply a second named claim that coexists with the inherited one. Both are checked; the stricter one does the work. Weakening isn’t rejected, it’s unexpressible.

Two mechanics follow. Claim names are one flat namespace, so two constitutions declaring one name is an error naming both origins — and so is a local clause shadowing an adopted one. A diamond (two constitutions extending a common base) contributes the shared base exactly once, deduped by origin rather than by name, so a real two-origin collision still surfaces.

adopt Core; in source means always, everywhere. But an entrypoint deployed to two environments must satisfy both claimsets, and it cannot write two conflicting adopt lines. So the environment binding lives in hale.toml, where the deployment facts already are:

[claims]
base = "Core"                 # carried by EVERY environment

[environments.dev]
constitution = "Dev"          # …and dev adds this
entrypoints  = ["apps/prober", "apps/dashboard"]

[environments.prod]
constitution = "Prod"
entrypoints  = ["apps/prober"]

The base is what makes “an environment may add law, never drop it” true of the mechanism rather than of convention — every evaluation carries it by construction. A workspace with environments must decide explicitly: base = "…" or no_base = true. An environment adding nothing of its own says source_only = true. In each case an omission would be indistinguishable from a typo.

hale check apps/prober --env prod    # adopts Prod for this run
hale check --matrix                  # every (entrypoint, environment) pair

--env injects the environment’s constitution exactly as if the source had written adopt — same evaluation, same closed world, union with whatever the source already adopts. So one entrypoint gets two verdicts, one per environment, without the source knowing where it will be deployed.

--matrix checks every pair. An entrypoint listed in no environment is an error, not a skip — that is the one hole composition cannot close by construction, since no single compilation can see that a sibling was left out. A seed with no main locus of its own at the top level is not an entrypoint and is not demanded of the manifest — one that only imports a library’s main locus, or keeps its main locus inside a module { }, included — and --env refuses it as a deployment target. List one in an environment anyway and its pair fails with that refusal and nothing more: there is no entrypoint for the environment’s roles to be mapped to, so the matrix reports no role coverage for it, and it does not compare that seed’s constitutions with the entrypoints’.

A constitution applied to every entrypoint cannot name any one application’s internals. It names shared vocabulary — but that vocabulary has to exist in each adopting entrypoint, and an undeclared name is an error, not an empty set:

type error: claim `iso` names group `payment_provider`, which is never
declared. Add `group payment_provider = { … };` at the top level.

may_be_empty applies only to a group that IS declared and resolves to zero members. So an entrypoint that genuinely lacks a component declares the vocabulary and says so:

group payment_provider = { } may_be_empty;

The usual way to satisfy this is for the entrypoints to import the same seed that declares both the constitution and its groups — then the vocabulary arrives with the law. An entrypoint that deliberately lacks a component writes the empty group explicitly, which is a line a reviewer can see rather than an absence they must infer.

Leaving a name for the adopter to answer is the job of a policy seed — one that declares no main locus, so it closes no world and someone else always adopts its clauses. A constitution written in a seed that does declare main locus is adopted by that main and nobody else, so its vocabulary is that seed’s own: a name it leaves undeclared is its error, and importing the seed does not let an importer’s same-named group answer it.

Once environments can add laws, two kinds of sentence live in one block with opposite lifetimes: product laws, true everywhere, and environment rails like “nothing reaches the real payment provider”, deliberately false in production. They read identically.

So the artifact records which constitution each clause came from rather than asking you to mark them:

{"name": "tenant_iso", "form": "…", "result": "holds", "source": "Core"}

A clause written in the main itself has no source. The distinction is structural and cannot drift from reality the way a hand-applied marker can.

hale check operates on one seed and does not recurse — a directory is one compilation unit, and that is the right unit for a closed-world check. The consequence is that a repository with several seeds needs something to enumerate them, or a claim is enforced only where somebody remembered to point check.

hale check --workspace .        # every seed under `.`, each on its own
hale verify --workspace .       # same, with advisories gated too

Every seed runs even if an earlier one fails — a runner that stopped at the first failure would report a subset of the truth. The summary names which seeds failed, and the exit status is the worst of them, so a usage error is not masked by an ordinary check failure elsewhere.

vendor/, target/ and dot-directories are skipped: a seed you do not own is not yours to gate.

What this does not do is connect seeds to each other. Each stays its own closed world with its own model. Two binaries that publish and subscribe the same topic are not linked by this command — nothing about a deployment is visible from source alone, and inventing those edges would certify a system nobody deploys. Per-seed artifact flags (--dump-topology, --check-topology*, the effects and budget equivalents) are therefore rejected in combination with --workspace: N seeds are N models, and there is no single artifact to emit or gate.

The checked model exports, diffs, and gates:

hale check app --dump-topology > .hale.topology
hale check app --dump-topology=.hale.topology     # or write it directly
hale check app --check-topology .hale.topology    # exact snapshot gate
hale check app --check-topology-shape .hale.topology   # model-only gate

The two gate flags take their operand either way (--flag value or --flag=value), and a missing operand is a usage error rather than a silent no-op — as is an unknown flag or a second target.

--dump-topology is the exception: its destination is the =<path> form only, and a bare --dump-topology writes to stdout. Its operand is optional, so “take the next token” has no safe reading — hale check --dump-topology app.hl would be asking whether app.hl is the destination or the target, and guessing wrong overwrites your source.

Dumping does not change what the command means: a program whose claims fail still exits non-zero with its witnesses, it just prints the artifact on the way.

A committed artifact can be drawn (experimental surface, pre-1.0):

hale topology graph .hale.topology                          # SVG to stdout
hale topology graph .hale.topology --format mermaid
hale topology graph .hale.topology --view claim --claim apart -o claim.svg

Views: system (loci, functions with phase/effect chips, topics, publish/subscribe/call edges), code (functions and calls only), bus (endpoints only), claim (system view with the named claim’s groups highlighted and its verdict on a card), residue (unresolved holes rendered as first-class nodes — never silently omitted; other views note them on a card). A --config file.json can retitle, focus, hide, or highlight — presentation choices only, never new semantics.

The renderer admits before it draws, in the fleet loader’s order: the whole-body artifact_digest must verify (a hand-edited artifact is refused, not rendered under a stale identity), the model semantics must match the build, the shape_hash must recompute from the model half, and the schema must be exactly the one this build emits — before 1.0 there is no additive-minor promise, so an older artifact is re-dumped, not read. It does not require a clean verdict — violations are worth drawing.

The renderer is an artifact client: it reads exactly the JSON a third party reads, never your source, and its output is deterministic by construction — fixed text metrics (no font measurement), stable IDs derived from artifact names, no timestamps. Rendering the same artifact twice is byte-identical, and moving source lines doesn’t move a pixel (provenance spans change; the model shape doesn’t) — which is what makes generated diagrams safe to commit and regression-test.

Two committed artifacts can be compared semantically — the review view of a change, rather than a text diff of two JSON documents:

hale model diff before.topology after.topology --text
hale model diff before.topology after.topology          # versioned JSON

hale model diff  before.topology  ->  after.topology
classification: model-shape  (shape_hash 560bb0… -> 578951…)
legend: + added  - removed  ~ renamed  > moved  * split/joined  ? ambiguous  ! changed in place
classes: identical · source-only (no model or contract change) · contract (a contract or effect moved, shape_hash unmoved) · model-shape
declarations:
  ~ locus Worker -> Crew  (renamed; shape unchanged)
  + locus Pager  (main.hl bytes 248..253)
  + topic Alerts  (main.hl bytes 71..77)
contracts:
  ! locus App params: +limit: Int
  ! locus App publishes: +Alerts
effects:
  ! fn Crew::on_e gains publish
law:
  + claim quiet: count publishers(topic Out) == 0  [violated]

A fn present on one side only with a non-empty effect set is an effect row too: + fn Mailer::on_mail reaches outbound_email for an added handler, - fn … reached … for a removed one, so an added locus that widens what the program does is not hidden behind the paired rows.

Declarations are persisted, moved, renamed, split, joined, added or removed; a rename is reported only when exactly one added declaration has the removed one’s shape, and anything with more than one candidate is reported as ambiguous with the candidates rather than guessed. Contract deltas are per locus (params, methods, publishes, subscribes with queue bounds, supervision, ownership, placement); effect deltas per function; law deltas per claim, plus adequacy and the overall verdict. A comment-only edit classifies as source-only; the same artifact twice as identical. Both inputs go through the same admission gates as the renderer, so an edited artifact is refused.

Bundle claims and fn-grained certificates (@effects, @budget, @phase_effects) are the same kind of statement at different granularity, so they report in the same words. Four states, told apart by what you should do about each:

violated and uncertified used to be one value, because unknown ⇒ violation: an indirect call fails closed rather than certifying an absence nothing established. That rule is unchanged and both still fail the build. What changed is that the artifact records which happened, because the repairs are different — and because composing models across binaries needs a propagated unknown to make a claim uncertified rather than report it as disproved when nothing disproved it.

The document’s own verdict is clean only if every row — claims and lowered alike — reports holds. uncertified does not pass: a law that could not be checked has not been satisfied. It says nothing about whether the program typechecks, because it doesn’t have to — an artifact is only emitted for a program that does.

Two different hashes, and conflating them is a trap:

• shape_hash is an identity. It covers the model half only, so claim renames, moved comments, and the topics/provenance sections don’t churn it. That’s what makes --check-topology-shape usable in CI.
• artifact_digest is an integrity check. It covers the entire body — model, topics, provenance and claim results alike — and is the final key, so everything before it is exactly what was hashed.

You need the second as soon as anything trusts an artifact it didn’t produce. A gate that greps shape_hash out of a committed baseline can be defeated by editing that one line; and a cross-binary consumer joining endpoints on the topics rows would otherwise be joining on data outside the hash it verified. Both baseline gates reject a file whose digest doesn’t match its contents, as corrupt rather than as a mismatch.

An artifact with no artifact_digest (anything before schema 1.3) reports as unverifiable rather than as valid — a consumer may choose to accept it, but must never read “nothing to check” as “checked and intact”.

The digest is only the integrity gate. Past it, every in-tree consumer — hale topology graph and hale fleet check alike — runs the same law-account admission: it recomputes both digests (law_digest from the canonical-JSON law rows; inputs_digest against the consuming binary’s own analysis-inputs snapshot), decodes each law row’s typed payload against a closed per-kind shape, resolves every reference against the artifact’s canonical catalogs (exact (name, display) pairs, closed under exact bijection with the public sections), recomputes bus-selector candidate sets with the compiler’s own matching rule, requires the lowered evidence and law.legacy report to project from the typed account, requires each law row that renders a compatibility form to STATE it (and re-renders it from the typed payload, so substituting an operand orphans the row), validates every diagnostic and requires non-holds verdicts to retain their judgment’s evidence, lets static invalidity (unresolved operands, undeclared or cyclic classes) dominate every replayed engine result, joins claims rows to law rows one-to-one in both directions, refuses fleet-family rows outright, and recomputes the document verdict. A restamped artifact whose sections disagree with each other is refused even though its digest verifies.

The artifact is a projection of the compiler’s canonical model — see The model for what that value is and why it records what it could not determine.

The artifact shape (schema 1.19):

{
  "schema": "1.19",
  "semantics": <model semantics version>,
  "shape_hash": "<fnv1a-64 over the model half>",
  "sorts":     { "loci": […], "fns": […], "topics": […] },
  "sealed":    [ <@sealed loci> ],
  "relations": {
    "calls": [ {"from", "to",
                "loop"?: true, "unbounded"?: true,
                "via_interface"?: "<iface>"} ],
    "calls_via_stdlib": [ {"from", "to", "loop"?: true} ],
    "publishes": […], "subscribes": […]
  },
  "groups":    { "<name>": [members as declared] },
  "labels":    { "<fn>": [declared effect classes] },
  "phases":    { "<fn>": {"phase", "kind": "hook"|"method"} },
  "seeds":     { "<alias>": [member decls] },
  "effects":   { "<fn>": [derived effect classes] },
  "supervision": [ {"locus", "child", "err", "ops": […],
                  "retry_bound"?} ],
  "unknowns":  [ {"fn": …, "reasons": ["indirect_call" |
                  "untyped_receiver_call:<callee>" |
                  "uninhabited_interface_call:<iface>.<callee>" |
                  "computed_publish"]} ],
  "endpoint_identity": [ {"verb", "fn" | "locus", "site"?,
                          "wire", "topic"?} ],   // HASHED
  "sources":   [ {"id", "path", "digest"} ],
  "provenance": { "calls": [+span], "publishes": [+span],
                  "subscribes": [+span],
                  "decls": {name: span, topics included},
                  "supervision": [+span] },
  "topics":    [ {"name", "subject", "shape", "payload_hash"} ],
  "endpoints": [ {"verb": "publish" | "subscribe", "subject",
                  "via": "site" | "declaration",
                  "fn"?, "site"?, "locus"?, "topic"?,
                  "file"?, "span"?} ],
  "declares_publish": [ {"locus", "subject", "topic"?,
                         "file"?, "span"?} ],
  "contracts": [ {"locus", "sealed", "params", "methods",
                  "publishes", "subscribes", "supervises",
                  "instances", "file", "span"} ],   // 1.18
  "bindings":  [ <declared bindings: topic, transport, role> ],  // 1.19
  "claims":    [ {"name", "form", "result": <verdict>,
                  "ordinal", "source"?} ],
  "lowered":   [ {"subject", "form", "result": <verdict>,
                  "ordinal", "cert"?} ],
  "law":       { "law_digest", "inputs_digest",
                 "fn_universe": [ {"name", "display",
                                   "analyzed", "summarized",
                                   "kind", "owner"?} ],
                 "loci":     [ {"name", "display",
                                "analyzable"} ],
                 "groups":   [ {"name", "display"} ],
                 "topics":   [ {"name", "display", "subject"} ],
                 "subjects": [patterns],
                 "effect_classes": [ {"name", "declared",
                                      "cyclic"} ],
                 "legacy": [ {"ordinal", "form", "result"} ],
                 //   ^ EMPTY since 1.17: every family is judged
                 //     over the model. The section survives so an
                 //     older artifact still decodes.
                 "issues": [ {"message", "file"?, "span"?} ],
                 "rows": [ {"ordinal", "name", "origin",
                            "family", "verdict",
                            "form"?,   // REQUIRED when the law
                                       // renders one; re-rendered
                                       // from the typed operands
                                       // at admission
                            "law": {"kind", …typed operand refs,
                                    each with name/display/
                                    resolved and provenance…},
                            "certs"?: [ {"ordinal", "form",
                                         "result",
                                         "evidence"?} ],
                            "evidence"?: [ {"message",
                                            "file"?, "span"?} ],
                            "file"?, "span"?} ] },
  "capabilities": { "exact_calls": bool, … },
  "adequacy":  { "<family>": "exact" | "degraded" },
  //   families: reachability, boundary, endpoint, bound,
  //   certificate, causes, depends, budget — every migrated
  //   family carries an account, and admission requires exactly
  //   the set its schema version names
  "evaluation": { "environment"?, "roots": […], "closure": […] },
  "verdict":   "clean" | "law_failed",
  "artifact_digest": "<over everything above>"
}

Everything renders in author spelling (cross-seed symbols demangled). shape_hash covers the model half — sorts, relations (with weights and the through-stdlib contraction), groups, labels, phases, seeds, derived effects, unknowns — and excludes claim results and provenance: one topology under a different law keeps one shape, and moving code changes every span but no identity, while any graph, vocabulary, carrier, phase, or new fail-closed or dead-dispatch site changes it. Two gates, named for what they compare:

• --check-topology — an exact artifact snapshot: law, model and provenance. Strictest, and the right default when you want every change to the file reviewed. Note that it therefore fires on a claim rename or a comment that shifts spans, even though the model is identical.
• --check-topology-shape — the model identity (shape_hash) only. Renames and source motion pass; a changed graph, vocabulary, carrier, phase, or new fail-closed site fails. Use this when baseline churn from provenance is costing more than it catches.

Either way the gate separates two review questions: does the program still satisfy the law? and did the graph change in a way reviewers should see? A program that does not typecheck has no model to compare, so both gates refuse it, as --dump-topology does.

The pieces worth knowing:

• Weights. A call row marked "loop": true sits inside a loop; "unbounded": true inside a loop with no compile-time trip bound. bound replay reads these. A "via_interface" row is one fanned-out dispatch alternative — alternatives sharing (from, interface, method) fold with max, one dispatch invokes one target.
• calls_via_stdlib. The evaluator walks stdlib bodies; the artifact serializes user rows. Every user→user path whose interior is stdlib collapses to one contracted edge (loop flag conservative: true if any such path crosses a loop), so reachability over the artifact matches reachability as evaluated.
• phases / seeds / effects. What during, cover, and effect-class endpoints evaluate against, exported — the rows that used to be compiler-certified-only.
• provenance. Byte-offset spans ([start, end]) for every user edge and decl, each with the source id of the file it sits in (the sources rows carry each file’s path and digest) — the “where to edit” data, unhashed by design. A path is never absolute: it is relative to the nearest hale.toml when every file is under it, and otherwise to the deepest directory holding them all, so one tree checked out anywhere gives one artifact.
• lowered. Every fn-grained certificate — each @effects assert, each @phase_effects phase contract, each @budget — as the claim form it is pointwise sugar for, with the verdict of the same evaluation that gates the build: forbid reaches({F}, effects(money)), bound alloc <= N on paths from {F}, only effects {…} on {L} during birth. One schema of record: the artifact carries all law, bundle-quantified and fn-grained, in one place. Unhashed like the claim results.
• topics. The per-topic OBSERVATION identity: the wire subject, the canonical payload shape, and payload_hash — exactly the (name, shape_hash) pair the runtime manifest fuses on (iris PROTOCOL §4), so a recording/WAL segment names the checked topology it ran under. subject is deliberately RAW (it is the byte-exact join key; a subject-less imported topic registers under its mangled local name — declare subject: on shared topics to fuse across binaries). Unhashed by ruling: payload field shape does not affect claim evaluation, so it is not part of the model identity — the artifact document is the reference between the two identities, not a fusion of them.

v2 scope: every claim verb replays independently over the exported relations. Still compiler-certified: bound over built-in classes (site counting through the stdlib interior, deliberately not serialized) and any walk past the step ceiling.

Not tests — a test executes one case; a claim quantifies over every represented path, and the two compose (test-first for behavior, claim-first for the architecture the behavior lives in). Not design-by-contract — a pre/postcondition surrounds one operation; a claim’s witness may cross files, seeds, and message boundaries. Not a runtime policy engine — claims lower to no code, inspect no traffic, and authorize no requests; what is not knowable statically (a computed subject, an un-elaborated deployment) is exposed as a boundary, never silently approximated in the unsafe direction.

And the fixed division underneath all of it:

The program owns the law. The compiler owns the proof.

Reference semantics: spec/verification.md § Claims. The workflow treatment: Claim-Driven Development in Hale.