The model

Most compilers have an IR that describes how the program runs — blocks, instructions, registers. Hale has one of those too. This is about the other one: a…

Most compilers have an IR that describes how the program runs — blocks, instructions, registers. Hale has one of those too. This is about the other one: a typed description of what the program is, derived once per snapshot by the frontend and read by everything downstream (the graph registry names what still derives its own).

A semantic fact about a program — who calls whom, which handlers a publish reaches, which locus owns which instance — has exactly one right answer. So it gets derived in exactly one place, and every consumer projects or queries that value.

That is the whole principle. In-process, it means hale check’s verdict on a law and the verdict recorded in the topology artifact are the same computation — not two computations held in agreement by a test. DispatchPlan, which decides how a bus subject dispatches, is derived from the same model that answered the verification questions.

Out of process it is necessarily weaker, and worth being precise about. The fleet tier, reasoning across binaries, cannot hold an ApplicationModel — it decodes a deliberately smaller ComponentModel from admitted artifact JSON. What it shares with the single-binary checker is the reachability engine and the admitted contract, not the value. That’s the boundary, and it’s where the wire form would earn its keep.

Eight concepts stay distinct: source, plan, model, the lowered law (ClaimIr), evidence, artifact, lowering plan, execution evidence. Keeping them un-conflated is what lets each one be simple.

The principle was first enforced for the model’s consumers: artifact and fleet code cannot walk source for a modeled fact. It now covers every semantic fact the compiler acts on, in every crate, through the graph registry (F.40): one entry per family — ownership, the bus graph, dispatch, placement, effects, allocation, lifecycle order and the rest — naming its authoritative producer, the legacy producers still permitted while it migrates, its consumers and its tests. A build fails when the tree grows a derivation-shaped function, a new reference to a guarded producer, or a bare Debug rendering the registry does not name. The rendered index is spec/registry.md; the contract is spec/model.md § The graph registry.

The interesting design choice isn’t the entity tables. It’s that a model records what it could not determine, as data:

Hole {
    at:    Function(cache_lookup),
    kind:  IndirectCall,
    hides: CALLS | EFFECTS | COSTS,
    reason: "call through `f`",
}

A graph that stores only what it found cannot distinguish there is no such edge from I could not see. Those are opposite answers to every question worth asking. “Does this handler reach a syscall?” — if the walk met a function pointer and stopped, the honest answer is not “no”.

So Hale’s verdicts have four values rather than two:

uncertified fails the build, exactly like violated. The difference is what you do about it: one is a bug in your program, the other is a limit of what the compiler can see, and those are different repairs.

The dual of a hole is a capability — a positive statement that some family of facts is complete. Positive on purpose: absence of recorded unknowns is not evidence of completeness, so a model that never noticed a gap does not get to claim exactness by default. Whether the model is adequate for a given question is then answerable directly, rather than inferred from the absence of warnings.

Holding the whole arrangement in one typed value makes properties checkable that a per-function analysis cannot express.

Effects that travel over the bus. A call graph stops at a publish. Hale’s message graph is declared over a closed topic set, so the compiler continues across it: this handler, by publishing orders, can transitively cause a filesystem write in the audit subscriber. You state the causal set, and omitting one is the error. A system whose message graph isn’t declared cannot ask the question at all.

Influence arriving. The backward direction is the more useful one. A locus that subscribes only to SumLookup looks isolated from Recalled in every declaration it carries — but if some third locus subscribes to Recalled and republishes onto SumLookup, the influence arrives anyway, and nothing in the depending locus’s source mentions it. @effects(depends: {…}) is the complete set of subjects that can reach you, and the diagnostic names the path.

Amplification. @budget(fanout = 8) bounds the subscriber deliveries one call can cause — transitively, per message, over runtime registrations. Publishing once to a 200-subscriber subject is a fan-out of 200. That is a property of the arrangement, and no per-function count reveals it.

Each of these is a statement about the whole system. They are checkable because something holds the whole system.

Bounds like fanout are quantitative, and quantitative analysis over a graph is easy to get approximately right in ways that matter. Two distinctions do most of the work.

A set is not a quantity. Reachability asks can this happen; a budget asks how many times. A handler that calls one publishing helper twice publishes twice — the reachable set says once. One subscribe declaration on a locus arranged with replicas = 3 is three runtime registrations. And a message carries one key, so a keyed publish reaches the subscriptions that key selects, not the union of every subscription it might ever reach.

This is why call and publish rows in the model are site-grained: two calls to one callee are two rows, because the callee runs twice. Collapsing them into a set computes reachability where the language means executions.

Aggregate last. Fan-out takes a maximum — over the key values a site can produce, and over the conformers of one interface dispatch. Taking that maximum early and continuing gives a different number:

max(immediate) + union(downstream)    ≠   max(immediate + downstream)
Σ over sites of max over alternatives ≠   max over alternatives of Σ

The left-hand forms pick one key for the immediate count and then follow every key’s downstream branch, or let two conformers both contribute when one dispatch runs one. So a whole scenario — one key, one conformer — is costed end to end, and only then compared. A call through a function value is the exception for now: it can reach each function of its type the program passes around as a value, and the model records each as a call site of its own, so a count over them adds where only one runs — an over-count, never an under-count.

Neither point is exotic. Both are the kind of thing that reads as obviously correct in one form and is quietly wrong in another, which is precisely why the semantics live in a written contract rather than in whichever walk happened to be written first.

The instance tables — which locus instances exist, who owns each, the thread each runs on, the CPUs a thread may use — are not the model’s own walk. They are the placement table’s rows, projected: the compiler decides where every instance runs once, and the model reads that decision rather than deriving a second one.

So the arrangement holds the instances of the main locus the build deploys, each where it runs:

type Held = Holder;

main locus App {
    params {
        h: Held = Holder { };          // App.h, realizing Holder
        r: Router = RouterV1 { };      // App.r, realizing RouterV1
        workers: Worker = Worker { };
    }
    placement {
        h: pinned;                     // App.h and all below it: pinned:App.h
        workers: pinned(cores = 0..4, replicas = 4);
    }
}

An aliased field is arranged as the locus the alias names, and an interface-typed one as the locus that was actually built. A replica carries its own index (App.workers[2]), and the instances under it carry it in their path. affined_to gives each pinned replica, and each pool, the CPUs it may run on — a set of cores is something a thread has, never a thread itself.

Some instances are deliberately not arranged, and the gap is stated rather than hidden. An instance of a standard-library locus (a std::io::udp::Reader field) is placed by the compiler but not arranged, since the model’s declarations are the program’s own. An imported library’s main locus is never the root. A locus fn main builds besides the root is a birth outside the arrangement, recorded as a hole. The placement table, not the arrangement, answers every placement question the checker asks.

A served surface or a hub keeps the placement of its generated adapters in the model’s dispatch report, including the adapters’ I/O pool. Initializer expressions copied from a binding remain params defaults even though their diagnostic locations point back to the binding. Connection peers created as requests arrive still carry dynamic-placement holes.

An instance’s id is its position in path order, so adding a field renumbers what sorts after it. Join instances across builds by path, never by id. None of this is in the shape hash: rearranging instances never changes a program’s shape_hash or its observation ids.

The model lives inside the compiler process. There is one way to build one — deriving it from checked source — and no way to load one from anywhere else.

The topology artifact is a projection: it carries the model half under a shape hash, plus typed law, capability and adequacy sections, and it is what every out-of-process consumer reads. It is lossy by construction, and a model cannot be rebuilt from it. Giving the IR a reversible wire form is real work rather than a weekend: every table would have to serialise, provenance would have to survive, and admission would have to be impossible to trick into producing a model that no program denotes.

For now: in-process consumers query the model; everyone else reads the artifact and checks the digests that tie it to the compiler that produced it.

The contract — sorts, relations, the hole and capability laws, the identity rules, and the discipline a new judgment family follows — is in spec/model.md.

For what an individual row holds, field by field, the API reference is at /api/hale_model.