The graph registry

GENERATED from crates/hale-graph/src/registry.rs and held byte-equal by registry_matches_spec. Do not edit: change the table and run HALE_REGEN_REGISTRY=1…

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

GENERATED from crates/hale-graph/src/registry.rs and held byte-equal by registry_matches_spec. Do not edit: change the table and run HALE_REGEN_REGISTRY=1 cargo test -p hale-graph --test registry_matches_spec. The contract this index serves is spec/model.md § The graph registry.

The families, their legacy producers, the spec rules and the frozen Debug-string sites are counted by registry_is_well_formed, not here: a rendered total moved with every change to any family, so two unrelated changes conflicted on one line at every rebase.

Answers. Which source units form the snapshot: the entry, every imported seed, their merge order and the spans’ virtual bases.

Inputs. .hl files; import directives; the workspace root (hale.toml); editor overlays (LSP)

Producer. crates/hale-frontend/src/frontend.rs · collect_checkable

Also owned. crates/hale-frontend/src/parse_cache.rs · ParseCache; crates/hale-syntax/src/shift.rs · shift_program; crates/hale-syntax/src/shift.rs · shift_item; crates/hale-syntax/src/shift.rs · erase_positions

Consumers. check; build; run; test; replay; bench; lsp; dna (via the CLI)

Invariants.

• one loader, one merge order, for every entry point
• an unresolved import is a diagnostic, never a silently smaller program
• one seed for every entry point: the editor’s load (LoadMode::Editor) is hale check <dir>’s — the open file’s directory, every import followed through the buffers (link_checkable) — and differs only in tolerance: a member that does not parse or will not read is recorded (Snapshot::unparsed, Snapshot::unreadable) and blocks the scope instead of failing the load, a link the import graph refuses keeps the members as they parsed with the refusal recorded (Snapshot::unlinked) and blocks the scope, which every request but the outline reads as the refused load (Snapshot::linked), and the LSP publishes an unreadable member as seed member <name>: <os error> against the member and the open file, never a clean seed the CLI cannot load
• parse reuse (F.40 phase 3, X1, hale_frontend::parse_cache): every file a load parses — a seed’s own (parse_files, the editor’s load), an imported library’s two parses (through its own effect-class table, then the load’s) — is parsed through the provider’s cache when it carries one (SourceProvider::parses: the LSP’s Overlay::reusing, one cache per server; the disk carries none). The cache holds the parser’s product alone: the program or the diagnostics parse_source_at_in gives for the text at base 0, and the effect-class table the parse left, keyed by the path, the exact text and the table the parse started from (#345: the load’s one table is an input of each file’s parse). Each load recreates the rest: the file’s base in its own source map, the product moved there (hale_syntax::shift::shift_program, exhaustive over the AST), then its own shaping and mint. Nothing shaped or minted is kept — shaping reads the whole load and its config, identities are snapshot-local — and the snapshot’s key, a whole load’s, is never a member’s. Nothing invalidates an entry (its product is a function of its key); a path keeps its four most recently used entries

Missing data. n/a

Focused tests. crates/hale-cli/tests/imports.rs (diamond_import, three_hop_import, import_library_key); crates/hale-cli/tests/source_map.rs; crates/hale-cli/tests/lsp.rs (lsp_and_check_agree_over_a_seed_that_imports, lsp_reports_an_unreadable_seed_member_as_check_does, lsp_outline_survives_a_link_failure); crates/hale-frontend/src/snapshot.rs (a_reused_parse_is_the_parse); crates/hale-syntax/src/shift.rs (the oracle over every .hl in the tree)

Spec. spec/projects.md

Guarded seams.

• parse_source_at_in( may be referenced from: crates/hale-syntax/src/lib.rs ×2, crates/hale-syntax/src/shift.rs ×2, crates/hale-frontend/src/parse_cache.rs ×2, crates/hale-types/src/effect_classes.rs ×2
• parse_in( may be referenced from: crates/hale-syntax/src/parser.rs ×2, crates/hale-syntax/src/lib.rs ×1, crates/hale-frontend/src/imports.rs ×2

Answers. What a qualified or aliased name denotes: the library identity, the mangled declaration, the construction target, the bus subject a path names.

Inputs. import aliases; the seed cache; hale_stdlib::PATH_RENAMES; declaration names

Producer. crates/hale-frontend/src/imports.rs · resolve_imports

Also owned. crates/hale-types/src/mangle.rs · resolve_construction_aliases; crates/hale-frontend/src/imports.rs · name_library; crates/hale-types/src/qualified_subjects.rs · resolve_qualified_bus_subjects

Consumers. check; build; lsp (hover, definition, references)

Invariants.

• a name resolves once per snapshot; the checker and lowering see the same target
• a construction path spelled with a type alias is resolved once, bundle-wide, in the desugar sequence before the check (resolve_construction_aliases), so the checker and lowering read the same target name; the checker follows no alias of its own, so a fragment checked without the sequence is not resolved a second way
• a qualified bus subject (subscribe / publish alias::Topic, alias::Topic <- v, a bindings entry) is resolved once, in the desugar sequence before the check (resolve_qualified_bus_subjects), to the single-segment topic the imported declaration ends up at: the checker (resolve_bus_subject keeps the leaf and an Unknown payload only for a path no rename names), the model and lowering read the rewritten program, and the resolved-program step does not resolve it again
• a qualified path in the checker is resolved through the scope’s one import table (KnownNames::import_target, built from the bundle’s renames): a qualified type, an imported fn (imported_fn) and an imported enum’s constructor arm (match_is_exhaustive) name the same declaration by the same row, compared by identity and never by the text of the merged name, and the checker holds no second scan of the rename vector for any of them
• a library’s name (AliasScopes::name_library) is a function of its own path alone — relative to the entry’s workspace root, else to the entry seed’s directory (library_basis), encoded injectively (library_id) — so no two libraries of a load share a name, and neither import order, the other imports of the build nor the tree’s absolute location changes the symbols a library is mangled under; a declaration’s full name (mangle::mangled) encodes the library, the file stem and the declaration as one injective tuple, so no two declarations of a load share one either

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-cli/tests/import_library_key.rs; crates/hale-cli/tests/import_library_names.rs; crates/hale-cli/tests/cross_seed_arity.rs; crates/hale-codegen/tests/cross_seed_imports.rs; crates/hale-types/tests/type_alias.rs; crates/hale-types/tests/qualified_subjects.rs; crates/hale-cli/tests/import_qualified_topic.rs

Spec. spec/semantics.md § Cross-seed namespace resolution; spec/projects.md

Guarded seams.

• resolve_construction_aliases( may be referenced from: crates/hale-types/src/mangle.rs ×1, crates/hale-types/src/desugar_sequence.rs ×1
• resolve_qualified_bus_subjects( may be referenced from: crates/hale-types/src/qualified_subjects.rs ×1, crates/hale-types/src/desugar_sequence.rs ×1
• name_library( may be referenced from: crates/hale-frontend/src/imports.rs ×2

Answers. Which rewrites the program receives before checking, in which order: the declaration-shaping passes only (JSON parsers, the serve and hub expansions, unit returns, construction aliases, qualified bus subjects, the omitted run, repr accessors). Sync inference is not a rewrite: its pick is a form row (sync_inference). The topic-reference and intra-locus rewrites are not desugars: they erase a written declaration reference the checker’s laws and the model read, and run in lowering’s resolved program, after the check.

Inputs. the merged program; –env (constitutions); the cross-seed rename table

Producer. crates/hale-types/src/desugar_sequence.rs · desugar_before_check

Also owned. crates/hale-types/src/resolved.rs · rewrite_intra_locus; crates/hale-types/src/resolved.rs · resolve_rewritten; crates/hale-syntax/src/desugar.rs · desugar_intra_locus_topics; crates/hale-syntax/src/desugar.rs · desugar_topics; crates/hale-types/src/desugar_sequence.rs · bundled_stdlib; crates/hale-syntax/src/desugar.rs · desugar_omitted_run; crates/hale-syntax/src/desugar.rs · desugar_repr_accessors

Consumers. check; build; run; test; replay; bench; lsp; codegen (crates/hale-codegen/src/codegen.rs · build_resolved)

Invariants.

• one order, run once per snapshot, before the first law is judged
• the sequence is called from the snapshot’s load (Snapshot::load, Snapshot::from_program) and from nowhere else: every entry point runs it before it mints its snapshot; the bundled stdlib goes through the same passes (bundled_stdlib)
• codegen never re-desugars
• the topic-reference and intra-locus rewrites are lowering’s, on lowering’s copy of the program, never the checked one, and each is recorded as a relation: TopicRewrite rows (topic_rewrites, and written_topics on the bus graph’s subjects) and IntraLocusRewrite rows (intra_locus, and direct_sends); the intra-locus rewrite is its own stage, rewrite_intra_locus (over the sequence’s program, its qualified bus subjects already resolved, keeping on the bus a publish into a field the placement table runs off its owner’s thread; the snapshot’s intra_locus count), which the check demands for rule 10 and lowering continues from, so the judgment and the lowering read one rewrite; resolve_rewritten runs the topic rewrite, appends the stdlib, mints and derives the tables
• a desugar that copies a subtree clears the copy’s identities (hale_syntax::sites::clear_ids_in_*): a verb mints after the sequence and the resolved program mints again after its rewrites, and two sites with one id is a panic; every corpus program is minted first and resolved second by a test
• the omitted run is synthesized in the sequence, before the check, and marked LifecycleDecl::synthesized: a rule about the run’s body reads the empty body and answers both spellings alike (spec semantics.md § run()); what lists the hooks the author wrote (the application model, whose function and phase tables are the artifact’s identity, the allocation summary, the effect contracts, the mint’s OmittedRun origin) reads the marker, never the absence of author text, and a synthesized run moves no artifact and no diagnostic

Missing data. n/a

Focused tests. crates/hale-cli/tests/api_description.rs; crates/hale-codegen/tests/framework_elision.rs; crates/hale-types/tests/topology_projection.rs (the_omitted_run_moves_no_artifact_and_no_diagnostic); crates/hale-types/tests/bus_graph.rs (a_rewritten_send_stays_on_the_resolved_graph, a_rewritten_topic_reference_stays_on_the_resolved_graph)

Spec. spec/semantics.md

Guarded seams.

• desugar_topics( may be referenced from: crates/hale-syntax/src/desugar.rs ×1, crates/hale-types/src/resolved.rs ×1
• desugar_before_check( may be referenced from: crates/hale-types/src/desugar_sequence.rs ×1, crates/hale-frontend/src/snapshot.rs ×1
• desugar_omitted_run( may be referenced from: crates/hale-syntax/src/desugar.rs ×1, crates/hale-types/src/desugar_sequence.rs ×1
• desugar_repr_accessors( may be referenced from: crates/hale-syntax/src/desugar.rs ×1, crates/hale-types/src/desugar_sequence.rs ×1
• rewrite_intra_locus( may be referenced from: crates/hale-types/src/resolved.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/lib.rs ×1
• resolve_rewritten( may be referenced from: crates/hale-types/src/resolved.rs ×1, crates/hale-frontend/src/snapshot.rs ×1
• desugar_intra_locus_topics( may be referenced from: crates/hale-syntax/src/desugar.rs ×1, crates/hale-types/src/resolved.rs ×1

Answers. Which sync discipline each @form declaration gets: one row per declaration with the author’s configuration (omitted, a written discipline, none included, or an argument naming none) and the effective discipline, inference’s pick for a hashmap form left unconfigured, from the domains each of its instances is called from; two queries, explicitly configured and safe for cross-domain access.

Inputs. placement (the table, per instance); top_scope; form declarations; method call sites

Producer. crates/hale-types/src/form_rows.rs · form_rows

Also owned. crates/hale-types/src/sync_inference.rs · infer_sync_for_bundle

Consumers. the snapshot (one row set per snapshot, after the mint, over its scope and placement table) (crates/hale-frontend/src/snapshot.rs · demand_forms); the allocation summary (sync_forms: the stdlib analysis copy’s, from that universe’s rows) (crates/hale-types/src/alloc_summary.rs · summarize_identified); check (F.31 cross-pool verdicts: the one predicate, safe for cross-domain access) (crates/hale-types/src/check.rs · check_placement_single_thread); check (instance aliasing: a field behind a sync discipline) (crates/hale-types/src/check.rs · locus_has_unsynchronized_state); the effects certificate engine (a call into a sync-bearing form or its holder can take its lock) (crates/hale-types/src/alloc_summary.rs · add_sync_forms); sync inference (its candidates: the forms not explicitly configured) (crates/hale-types/src/sync_inference.rs · infer_sync_for_bundle); model (sync_form, read by the depends law) (crates/hale-types/src/model_builder.rs · derive_application_model_over); the lowering view (the snapshot’s rows, and the merged stdlib’s as written) (crates/hale-types/src/resolved.rs · resolve_rewritten); codegen (the slot layout) (crates/hale-codegen/src/locus/decl.rs · sync_mode); lsp

Invariants.

• every entry point sees the same discipline for the same program
• one row per @form declaration, found by the identity the load minted (a monomorph by its template’s) or by name: the configuration and the effective discipline are separate columns
• an explicit sync = none is configuration: inference does not run over it, and the row does not call it safe for cross-domain access
• one predicate per question: inference’s candidates are the forms not explicitly configured, and the F.31 cross-pool exemption is safe for cross-domain access; sync inference runs once per snapshot, and the cross-pool diagnostic’s hint reads its reasoning from the rows
• nothing writes the discipline into the program: the check, the effects engine, the model and lowering read the row, and a declaration with no row (a bundle’s no row set holds) reads its written argument, except in lowering, whose view holds a row for every declaration it lowers and refuses one with none (F.40 phase 3’s exit)
• the stdlib’s analysis copy has its own universe’s rows (stdlib_bodies::forms, once per process, found by the identities the copy was minted with), each its written configuration, since nothing infers over the copy; the allocation summary’s sync_forms reads them and no sync = argument, and the effects engine adds the program’s own from the snapshot’s rows (add_sync_forms) (C3 rest)
• the readers that ask whether a form synchronizes as one question (the model’s sync_form, the effects engine, instance aliasing) ask safe for cross-domain access alone (FormRows::synchronizes): an explicit sync = none takes no lock and is not one
• inference is per instance (the placement correspondence’s K-5): an access self.f.m() is made from the domain of each instance of its enclosing locus and reaches that instance’s own f (a held one by its source row, so its holders share it); the rule is applied per accessed instance and a type gets the most synchronized discipline any instance needs, never a union of domains per type; what the table does not know (a dynamic literal of unknown domains, a held instance whose source is unlinked, the instance below one) is a domain apart from every other, never main

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · sync_inference_a_hashmap_without_its_row_is_refused_at_its_declaration

Focused tests. crates/hale-types/tests/form_rows.rs (the_summary_reads_the_copys_rows_and_the_engine_adds_the_programs); crates/hale-frontend/src/snapshot.rs (the_form_rows_are_one_family_by_identity); crates/hale-types/tests/placement.rs

Spec. spec/forms.md § Cross-pool sync disciplines; spec/semantics.md § A form’s sync discipline

Guarded seams.

• form_rows( may be referenced from: crates/hale-types/src/form_rows.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1

Answers. The user effect classes of a load: one table every seed is parsed through, so a class (its name, its identity in the program’s one class namespace) has one User(i) index in every seed; which were declared, which are composed, and the one expansion of a composed class.

Inputs. effect declarations and class references per seed; the load’s parse order (a seed after the seeds it imports)

Producer. crates/hale-syntax/src/ast.rs · EffectClasses

Also owned. crates/hale-syntax/src/lib.rs · parse_source_at_in; crates/hale-types/src/effect_classes.rs · EffectClassTable

Consumers. the load (own files, the editor’s members, every imported seed after its imports; through the provider’s parse cache when it carries one) (crates/hale-frontend/src/frontend.rs · parse_file); effects (contracts, phase contracts, the declared manifest) (crates/hale-types/src/effects.rs · EffectClassTable::of(); the effect rows (one table per snapshot, carried on the rows: the model’s effect-class rows and atoms, and the inferred manifest’s class names, read it there) (crates/hale-types/src/effect_rows.rs · EffectClassTable::of(); effects (causes) (crates/hale-types/src/frontier.rs · EffectClassTable::of(); alloc_summary (what @effects(is: …) carries) (crates/hale-types/src/alloc_summary.rs · EffectClassTable::of(); quantitative (user-class budgets) (crates/hale-types/src/quantitative.rs · EffectClassTable::of(); claims (lowering: class references, undeclared classes) (crates/hale-types/src/claim_lowering.rs · EffectClassTable::of(); topology (derived effect sets) (crates/hale-types/src/topology.rs · EffectClassTable::of()

Invariants.

• one class, one index, per load: every seed is parsed through the load’s one table (parse_source_at_in, parser::parse_in, or a parse the provider’s cache made from an equal table, which it keys on: parse_cache), so merging seeds renumbers nothing; an imported seed is numbered after the seeds it imports (it is parsed again, through the table, once they are), the order the classes have always been numbered in
• one expansion: a composed class’s mask, its atoms and whether its definition is cyclic are EffectClassTable’s; no analysis walks a definition itself or reads a program’s table directly

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-cli/tests/cross_seed_effects.rs; crates/hale-cli/tests/xseed_user_effects.rs; crates/hale-types/src/effect_classes.rs (one_table_one_expansion); crates/hale-frontend/src/snapshot.rs (a_seed_is_numbered_after_the_seeds_it_imports)

Spec. spec/verification.md § Default-on & opt-in analyses

Guarded seams.

• EffectClassTable::of( may be referenced from: crates/hale-types/src/effect_classes.rs ×1, crates/hale-types/src/effects.rs ×3, crates/hale-types/src/effect_rows.rs ×1, crates/hale-types/src/frontier.rs ×1, crates/hale-types/src/alloc_summary.rs ×1, crates/hale-types/src/quantitative.rs ×1, crates/hale-types/src/claim_lowering.rs ×1, crates/hale-types/src/topology.rs ×1
• effect_defs may be referenced from: crates/hale-syntax/src/ast.rs ×1, crates/hale-syntax/src/parser.rs ×9, crates/hale-frontend/src/frontend.rs ×3, crates/hale-types/src/effect_classes.rs ×2, crates/hale-types/src/resolved.rs ×1, crates/hale-syntax/src/shift.rs ×1

Answers. Exact rational relationships between resolved unit identities, cycle consistency witnesses, and coarsest widening-compatible denominations. A program’s catalogue is closed from its unit declarations and the stdlib’s time catalogue’s (the unit_declarations family); expression typing reads its factors through the quantities’ rules (unit_quantities, GH #1076 U3), Duration’s and Time’s among them (U4).

Inputs. unit declaration identities (UnitId: a SiteRef, the universe that minted the declaration and its SiteId); the stdlib’s time catalogue (hale-stdlib/hl/time.hl: ns us ms s min h day, from the stdlib’s analysis copy, SiteUniverse::StdlibAnalysis); equations with declaration identities and positive exact rational factors

Producer. crates/hale-types/src/unit_graph.rs · close

Also owned. crates/hale-types/src/unit_graph.rs · pub fn factor; crates/hale-types/src/unit_graph.rs · pub fn to_machine

Consumers. the unit declarations (the program’s catalogue, closed once from its equations; its inconsistent cycles are law 3’s witnesses; a point’s origin counted through factor) (crates/hale-types/src/units.rs · UnitGraph::close); conversion queries (reduced factor, exactness and equation witness) (crates/hale-types/src/unit_graph.rs · conversion); unpinned denomination queries (rational gcd and necessary input witnesses) (crates/hale-types/src/unit_graph.rs · meet); denomination values (a unit and an exact multiple; the factor between two, exact and as machine integers with an explicit overflow) (crates/hale-types/src/unit_graph.rs · pub fn factor); the quantities’ rules (every conversion’s exact factor, two denominations’ meet, a dimensionless denomination’s number: unit_quantities, U3) (crates/hale-types/src/unit_quantities.rs · pub fn factor); check –units (the witness report, U5: the headroom of an Int at a denomination, in the unit it is written against and in the coarsest unit of its component that still counts one, through factor) (crates/hale-types/src/unit_report.rs · catalogue.factor)

Invariants.

• unit identity is the declaration’s SiteRef (U4): its universe and its SiteId, never a display spelling, span or NodeId equality; the stdlib’s analysis copy numbers its sites on its own, so a stdlib unit and a program’s can share a SiteId and never a SiteRef, and the two catalogues are disjoint components joined only by an equation a program writes against a stdlib unit (unit tick = 10 ms;)
• factors are positive arbitrary-precision rationals; no machine overflow, rounding, runtime base unit or default loss policy
• every cycle has product one; an inconsistent catalogue returns only errors with witnessed cycles, never a partially usable closure
• a conversion between disconnected components or through an unknown unit has no answer
• denomination is the rational gcd of the input units, potentially unnamed, with an irredundant set of input witnesses; 6, 10 and 15 require three witnesses
• a denominator of one proves denomination conversion exactness only, not that a runtime range or representation width can hold the result
• a denomination is also a value (Denom: a unit and an exact positive multiple), stored and compared without the catalogue; whether two values denote one denomination, and the factor between them, are the catalogue’s (factor); the factor reaches machine integers only through Ratio::to_machine, whose overflow is an explicit FactorOverflow, never a truncation

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-types/src/unit_graph.rs; crates/hale-types/tests/unit_declarations.rs; crates/hale-types/tests/time_declarations.rs

Spec. spec/units.md § The catalogue

Answers. What each unit-dialect declaration is (GH #1076): every unit and its equation, every quantity, point, identity, range and refinement with its component, denomination, quantity, origin, policy and range, every unit a declaration names resolved, and the program’s catalogue closed from them; and whether the declarations obey the dialect’s structural laws.

Inputs. unit declarations and their equations (UnitDecl, UnitEquation); scalar type declarations (TypeDeclBody::Scalar: kind word, base, denomination, range: / round: / origin: clauses); the bundle’s other type, locus, interface and perspective names (what a base that is no scalar is); the stdlib’s seed declarations (hale-stdlib/hl/time.hl: the time catalogue, Duration, Time), from its analysis copy and its identities (U4); snapshot identities; unit_catalogue (the closure, and its witnessed cycles)

Producer. crates/hale-types/src/units.rs · derive_unit_rows

Also owned. crates/hale-types/src/units.rs · unit_laws; crates/hale-types/src/units.rs · declared_twice; crates/hale-types/src/units.rs · undeclared_units; crates/hale-types/src/units.rs · inconsistent_cycles; crates/hale-types/src/units.rs · second_quantity; crates/hale-types/src/units.rs · quantity_shape; crates/hale-types/src/units.rs · point_shape; crates/hale-types/src/units.rs · clauses; crates/hale-types/src/units.rs · identity_and_range_bases; crates/hale-types/src/units.rs · refinement_bases; crates/hale-types/src/units.rs · literal_suffix_names; crates/hale-types/src/units.rs · builtin_type_names; crates/hale-types/src/units.rs · typed_scalar_names; crates/hale-types/src/units.rs · stdlib_rows; crates/hale-types/src/units.rs · stdlib_literal; crates/hale-types/src/units.rs · quantity_tags; crates/hale-frontend/src/snapshot.rs · demand_units

Consumers. demand (one cell per snapshot, counted as this family) (crates/hale-frontend/src/snapshot.rs · derive_unit_rows); check (the twelve laws, through one entry, over the rows handed in: CheckInputs::units) (crates/hale-types/src/check.rs · unit_laws); check (the identities’ and ranges’ value rules, unit_values: each scalar’s kind, parent and range, from the rows handed in) (crates/hale-types/src/check.rs · ScalarTypes::new); check (the quantities’ and points’ value rules, unit_quantities: each row’s kind, component, denomination, quantity, origin and policy, a literal’s unit by name, read through the same ScalarTypes) (crates/hale-types/src/unit_quantities.rs · fn quantity_binop); the topic shape renderer (a quantity’s or a point’s wire tag, its denomination as written: quantity_tags, decision 9) (crates/hale-types/src/topic_identity.rs · quantity_tags); the resolver’s literal typing of a params initializer with no ascription (a time literal is a Duration: the stdlib’s rows, stdlib_literal, U4) (crates/hale-types/src/resolve.rs · stdlib_literal); codegen (a params or const initializer’s time literal, read without the typed bodies: its count of Duration from the stdlib’s rows, stdlib_literal, U4) (crates/hale-codegen/src/codegen.rs · stdlib_literal); codegen (a time literal in a body the checker types no row in, the stdlib’s own: its count from the stdlib’s rows, stdlib_literal, U4) (crates/hale-codegen/src/conversion.rs · stdlib_literal); check –units (the snapshot’s rows, handed to the report) (crates/hale-cli/src/verbs/check/run_impl.rs · demand_units); check –units (the witness report, U5: each of the program’s scalar declarations with its kind, its denomination and the declaration whose in fixed it, its policy and the declaration that writes it, a point’s origin, its range and the narrowest machine width that holds it; the rows read through ScalarTypes::of_rows, no re-check; a development report, outside the hashed model half) (crates/hale-types/src/unit_report.rs · pub fn report)

Invariants.

• one producer over the stdlib’s seed and then the programs after the desugar sequence, each row keyed by its declaration’s site in the universe that minted it (SiteRef: the stdlib’s analysis copy’s for the time catalogue and Duration and Time, U4; the snapshot’s for a program’s), demanded once per snapshot (Snapshot::demand_units), not gated on the typing: it reads declarations only. The stdlib’s own rows, alone, are derived once per process (stdlib_rows) for the readers that have no program’s: a time literal’s count of Duration (stdlib_literal)
• every unit a declaration names (an equation’s target, a denomination, an origin) is a reference row, resolved by name to the first unit of that name or to none; the components join the units of every equation whose target resolves, and the number one is a node of them, so every unit written against a number (unit pct = 1/100;) is in one dimensionless component (law 10)
• the catalogue is closed once, from the rows (the number one under an identity the snapshot’s mint never issues), and kept only when no catalogue law fails: a unit declared twice, an equation naming no declared unit, a cycle that does not multiply to one
• a scalar’s kind is its word’s (quantity, point, distinct), else its base’s: a refinement of a quantity is a quantity, of a point a point, of Int, an identity or a range a range, and Int in D a quantity missing its word. A quantity’s or a point’s denomination is its own in, else its parent’s; its component is its parent’s, else its denomination’s unit’s. Each component’s quantity is the first declared with quantity and no policy; every other quantity over the component is a boundary denomination of it and records it as its of. A point’s origin is a count of its own denomination, through the catalogue
• the laws are registered rules of spec/verification.md’s structural table, each a function over the rows producing law::Violations, run by the check through unit_laws: a unit is declared once; an equation, a denomination or an origin names a declared unit; every cycle of equations multiplies to one; a component has one quantity, and a refinement of a quantity stays in its component; a quantity counts an Int and names its denomination; a point is over a quantity, and its denomination and origin are in its component; round: names a policy, on a quantity or a point, and a range: is literal, non-empty and inside its parent’s; an identity is distinct Int and a range refines Int, an identity or a range; a refinement refines a scalar or Int, never a struct, an enum or itself; no unit takes a name the lexer reads before a unit (d, the Decimal literal’s suffix; e or E and a digit, a Float’s exponent: law 11, U4); no scalar declaration and no unit takes a builtin type’s name (a primitive’s, hale_syntax::parser::primitive_from_name, which a type position reads before any declaration, or a BUILTIN_TYPES row’s: law 12, U5; the stdlib’s Duration and Time are those primitives); a program’s unit of a name the stdlib’s time catalogue declares is that unit declared twice, the message naming the catalogue (its declaration is in no file of the program, so no witness points at it)
• every scalar’s values are typed: the scope registers each declaration whose chain reaches Int (an identity, a range, a quantity counting an Int in a denomination, a point over one, a refinement of any) as a nominal TypeKind::Scalar represented as an Int, which typed_scalar_names decides once from the declarations for every reader (the resolver, codegen’s alias table, the topic shape renderer); the stdlib’s Duration and Time (U4) are no such name: a type position reads them as the primitives, which keep their representation class (the shape tags u and t, the printing, the FFI classes, the runtime’s nanosecond entry points), and their scalar rows say so (ScalarRow::primitive), so the algebra answers for Ty::Prim(Duration) and Ty::Prim(Time) and the checker’s operator table holds no rule of theirs; the checker’s rules read the rows (unit_values for identities and ranges, U2; unit_quantities for quantities and points, U3); a declaration the laws refuse resolves to Unknown, so a use of it is no second error
• the algebra of quantities and points is one table (ScalarTypes::quantity_binop): a sum or a difference of one quantity is the quantity at the finer of the two denominations (the meet), each operand widened exactly; a quantity scales by an Int, and by a dimensionless quantity at the product of the two denominations, nothing rounded; a quantity divided by a runtime Int is integer division and by an integer literal other than one a narrowing; one quantity over another of its component is an Int; two points of one origin differ by their quantity, and a point moves by one; a comparison holds within one quantity, or between two points of one origin, exactly; everything else is refused naming both declarations
• an expression’s quantity type carries its denomination, and one no declaration names is synthesized (Money in 1/100 cent): the same kind keyed by its quantity, or its point’s frame, and the denomination, spelled by the first unit it is one of, else the unit it is the smallest whole multiple of, else a fraction of its quantity’s unit; it has no policy and no range. A quantity literal is its component’s quantity at the quantity’s denomination when it is a whole count of it, its value times its unit’s factor a whole number whatever the factor alone is (500ms is 500,000,000 of Duration, 1000mg of a quantity counted in grams 1, U4), else at its own unit, and a whole count no Int holds is refused at the literal; a unit’s name is a namespace of its own

Missing data. total: no stdlib row for a literal’s unit means the unit is no unit of the stdlib’s time catalogue: a params or const initializer of it is refused (param_value: set it in birth), and a literal of it in a body the checker types no row in is a missing required row (lower_quantity_literal)

Focused tests. crates/hale-types/tests/unit_declarations.rs; crates/hale-types/tests/unit_values.rs; crates/hale-types/tests/unit_quantities.rs; crates/hale-types/tests/time_declarations.rs; crates/hale-types/tests/time_literal_diagnostics.rs (a compound or retired time literal says what to write); crates/hale-types/tests/unit_report.rs; crates/hale-cli/tests/check_units.rs (the committed form’s report, pinned whole); crates/hale-codegen/tests/duration_scalar_arith.rs; crates/hale-types/tests/demand_gate.rs; tests/hale/unit_declarations_test.hl; tests/hale/identities_and_ranges_test.hl; tests/hale/unit_quantities_test.hl; crates/hale-types/tests/unit_acceptance.rs (the committed form’s example: each error it marks, its text where an earlier step decided otherwise, and no narrowing without a policy, per form); tests/hale/units_time_test.hl (the committed form’s stated results, U5, with the next four); tests/hale/units_money_test.hl; tests/hale/units_ticks_test.hl; tests/hale/units_identities_test.hl; tests/hale/units_temperature_test.hl

Spec. spec/units.md § Declarations; spec/units.md § The rows; spec/units.md § The laws; spec/units.md § The algebra; spec/units.md § Conversions; spec/units.md § The witness report; spec/verification.md § Structural & design rules

Guarded seams.

• derive_unit_rows( may be referenced from: crates/hale-types/src/units.rs ×2, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1
• unit_laws( may be referenced from: crates/hale-types/src/units.rs ×1, crates/hale-types/src/check.rs ×1
• typed_scalar_names( may be referenced from: crates/hale-types/src/resolve.rs ×1, crates/hale-codegen/src/codegen.rs ×1, crates/hale-types/src/topic_identity.rs ×1

Answers. What every top-level name denotes: the symbol table over the merged program.

Inputs. the merged program; import renames

Producer. crates/hale-types/src/resolve.rs · build_top_scope

Consumers. check (crates/hale-types/src/check.rs · check_bundle_scoped); check (type expressions: the scope’s name table) (crates/hale-types/src/check.rs · &top.names); demand (every verb, the LSP’s diagnostics and its requests: one scope per snapshot) (crates/hale-frontend/src/snapshot.rs · build_top_scope); model (the snapshot’s scope, handed in) (crates/hale-types/src/model_builder.rs · ModelInputs); resolved program (lowering: the snapshot’s scope, handed in; its topic rows, and the stdlib’s bus rows and typed-body pairs answered over it) (crates/hale-types/src/resolved.rs · top: &TopScope); the stdlib’s bus rows (the scope of no program, which holds the stdlib’s declarations alone: once per process) (crates/hale-types/src/stdlib_bodies.rs · build_top_scope); lsp (definition, placement, the allocation survey: the snapshot’s scope) (crates/hale-lsp/src/lib.rs · demand_scope); lsp (completion, hover, references, enforcement: the editor’s scope, over the members that parsed while one does not) (crates/hale-lsp/src/lib.rs · demand_editor_scope)

Invariants.

• one namespace decision: module-nested declarations and imported seeds resolve the same way everywhere
• the editor’s scope over a seed with a hole (demand_editor_scope) is the same producer over the members that parsed, counted as this family; the whole scope, the check and everything after it stay blocked, so no check runs over a partial program
• one name table: the checker resolves every type expression against the scope’s own (TopScope::names, the declared loci, types and perspectives with each alias’s expanded target and the bundle’s import renames), built once with the symbols, and keeps none of its own
• every production path demands the scope from a snapshot (demand_scope): every verb, the LSP (its diagnostics and every request), the check, the model and its graphs, and the lowering view (F.40 phase 3, C5); since the --sealable survey reads its snapshot’s rows (F.40 phase 4, W4), no production caller builds a program’s scope outside it (the stdlib’s bus rows read the scope of no program, which holds the stdlib’s declarations alone and is built once per process: F.40 phase 4, S9). No entry builds a scope beside the snapshot: the entries over a bundle or a program no snapshot holds, which only tests called (the bare-bundle check check_program, check_bundle, check_bundle_opts, check_bundle_opts_whole_program, check_bundle_opts_scoped and check_bundle_for_build; the bare model derive_application_model and the bundle forms of claim_law_diags, model_shape_hash and dump_topology over it; effect_certificates and resolve_program), left crates/hale-types/src once every test asked a snapshot instead (crates/hale-types/tests/support/entries.rs, F.40 phase 4, T3). check::check_bundle reads the scope its caller hands it and builds none. What else calls the producer is a unit test that builds a scope for the private item it tests (lib.rs, sync_inference.rs, lifecycle/derive.rs). The seam counts them

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-types/src/lifecycle/derive.rs (shared ancestry regression); crates/hale-types/tests/checks_inside_modules.rs; crates/hale-cli/tests/check_unknown_identifier.rs; crates/hale-types/tests/type_alias.rs

Spec. spec/semantics.md

Guarded seams.

• build_top_scope( may be referenced from: crates/hale-types/src/resolve.rs ×1, crates/hale-types/src/lib.rs ×1, crates/hale-types/src/sync_inference.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/lifecycle/derive.rs ×1, crates/hale-types/src/stdlib_bodies.rs ×1

Answers. The type of every expression, and the typed edges (calls, sends, field reads) the locus graph is built from.

Inputs. top_scope; declarations; bodies

Producer. crates/hale-types/src/check.rs · check_bundle_scoped

Also owned. crates/hale-types/src/resolve.rs · infer_literal_ty; crates/hale-types/src/typed_bodies.rs · typed_bodies; crates/hale-types/src/builtin_sigs.rs · BARE_BUILTIN_SIGS

Consumers. the snapshot (one typed-body table per snapshot, packaged on demand from the check’s record) (crates/hale-frontend/src/snapshot.rs · demand_typed_bodies); the check of a bundle no snapshot holds (the record packaged for the bare_fallible law) (crates/hale-types/src/check.rs · check_bundle_reporting); codegen (an accumulator slot’s element type, the closure’s typed-body row) (crates/hale-codegen/src/codegen.rs · accumulator_element_type); codegen (a bare builtin’s arity and result: its signature row) (crates/hale-codegen/src/codegen.rs · builtin_sig); the cross-pool value law (law_backstops, at the harness’s lowering view: the table’s omitted_args; the check reads its record’s) (crates/hale-frontend/src/snapshot.rs · omitted_args); the sealed rule (sealability: the param_accesses rows of each declaration, as its walk ends) (crates/hale-types/src/check.rs · settle_param_accesses); check –sealable (the snapshot’s table’s param_accesses) (crates/hale-cli/src/verbs/check/run_impl.rs · demand_typed_bodies); check –units (every narrowing’s conversions row, U5: its factor or its range, a literal’s count, its discharge, and whether the target type’s round: gave it; one line for the rows the evaluations of one default share) (crates/hale-types/src/unit_report.rs · conversion_sites); codegen (a conversion between an identity or a range and its family: its cast’s conversions row, by its call on the evaluation path being lowered (empty outside a default), read from the body being emitted; lower_conversion reads the kind, the range and the discharge; a call with no row is no conversion, lowered as the call the checker resolved, never decided by its callee’s name) (crates/hale-codegen/src/conversion.rs · conversion_operand); codegen (a quantity’s or a point’s change of denomination, U3: a cast’s, .in(u)’s and .split(u)‘s row by the call, a division by a literal by the division, a value converted where it stands, a literal’s count and a printed value by the span, each on the evaluation path being lowered (empty outside a default), and every row read from the body being emitted (current_body, the declaration the checker recorded it under), never another’s, so a stdlib body, whose spans overlap the first file’s, finds none of a user body’s, and a constant’s initializer, lowered again at each use, is read from the constant on no evaluation path, a default’s use included (in_const_body); lower_scale emits the factor’s one multiplication, a point’s shift and one division rounded or checked by the row’s policy; a quantity literal is its row’s count, and a literal with no row is refused as a missing required row, save in a body the checker types no row in (the stdlib’s own, U4), where a time literal is its count of Duration from the stdlib’s rows; a printed value’s row is the unit written after its count) (crates/hale-codegen/src/conversion.rs · convert_value); codegen (an arithmetic operator over a quantity or a point, U4: its Operator row, by its span on the evaluation path being lowered, names the result’s type, the representation lowering emits the operation in: Int * Duration a Duration, Time - Time a Duration, a quantity at a denomination no declaration names an Int; codegen keeps no operator table of its own) (crates/hale-codegen/src/conversion.rs · operator_result); the bare_fallible law (a narrowing nothing discharges, a quantity’s included: the conversions column, once per conversion however many evaluations of a default hold it) (crates/hale-types/src/bare_fallible.rs · judge_narrowing); the closures’ reach law (the recoveries column: which locus each recovery statement outside the handlers applies its event to, by the type the checker gave its receiver) (crates/hale-types/src/closure_events.rs · unreached_events); every layer

Invariants.

• expression typing is not a layer: it is the derivation inside layer 3 that produces typed edges, and it stays Rust (final direction)
• codegen types no value the checker typed: an accumulator’s element type is the closure’s typed-body row, and a hole is refused at its span
• the checker’s answers are carried, never re-derived: the check records them as it walks, and one typed-body table per snapshot packages the record (demand_typed_bodies, no second check but for a typing that reused a declaration, the snapshot family’s X2 row; the check demands it once, for the bare_fallible law), keyed by declaration identity (a body by its declaration’s site, a call by its Call site, a monomorph by its template’s site and type arguments, never by a name string), with nine columns: accumulator element types, generic calls’ type arguments and unified params, the monomorph table, conformance per (locus, interface) pair, fallible calls (the callee’s mark and what addresses the call), omitted_args (per call that leaves arguments to their defaults, the declaration the checker resolves the callee to, a method by its receiver’s type, and the first parameter it leaves; a type’s field defaults, which the checker does not type, have their calls recorded too), and param_accesses (per body, each read or write of a locus’s params through a receiver typed as that locus, with the reader and the receiver by declaration and the evaluation path and the specialization it was typed on: the sealability family’s rows), and conversions (GH #1076: per conversion between an identity or a range and its family, keyed by (kind, evaluation path): a cast by its call and an implicit widening by the value’s span, each on the evaluation path it was typed on (empty outside a default; every conversion in a default, whatever its kind, carries the path: a default is typed at each evaluation, the struct literal that leaves a field or the call that leaves a parameter, in the body of the declaration that evaluates it, and the path is every evaluation from the outermost inward, the literal or call that leaves a default and then each literal or call in it that leaves the next, so one default evaluated in two scopes has each scope’s answer, at the top or nested in another default), its kind (total, widening, narrowing), a narrowing’s range and what discharges it; lowering reads a cast’s row and decides nothing, emitting nothing for a total conversion or a widening, and a call with no row is no conversion, whatever its callee is named; U3: per change of a quantity’s or a point’s denomination, at a binding, an argument, a return, an operand, a default, an array literal’s element (from the element’s own type into the element type of the place the array flows into, or, where nothing types the array, into the elements’ meet, the finer of their denominations), .in(u), .split(u), a cast and a division by a literal, its exact factor and a point’s shift, widening when the factor is whole and else a narrowing discharged at the site (or a rounding, a substitute, a handler, raise) or by the target type’s round:, a quantity literal’s count converted at compile time (the literal counts in its quantity’s denomination when it is a whole count of it, else at its own unit: 500ms is 500,000,000 of Duration, 1000mg of a Mass counted in grams 1 of Mass, 5mg a Mass in mg, U4), and a printed quantity’s unit, each keyed as above, so a literal in a default has a count per evaluation, into what that scope flows it into; U4: per arithmetic operator over a quantity or a point, the stdlib’s Duration and Time among them, the algebra’s result type, keyed by the operator’s span, which lowering reads for the representation it emits the operation in), and recoveries (per body, each recovery statement written outside every on_failure body, recorded where the checker types it: its operation, whether it states a for bound, its parent locus by declaration, the type the checker gave its receiver (the first argument) and the locus that type names by declaration, a monomorph’s template’s, on the specialization it was typed in: the closures’ reach law reads it); a site the checker could not type is a hole with its reason
• the bare builtins (len, to_string, the Int / Float casts, abs / min / max, starts_with / contains) are typed by one signature table (BARE_BUILTIN_SIGS), lowering’s inference written down: the checker types a call by its row where lowering lowers it and leaves it Unknown where lowering refuses, and lowering reads each builtin’s arity and result from the same row

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/typed_body_rows.rs · an_accumulator_without_a_row_is_refused_at_its_expression; total: no conversions row for a call (inside a default, under the evaluation path being lowered): the call is no conversion, and is lowered as the call the checker resolved (a local, a parameter or a fn), whatever its callee is named; no Operator row for an arithmetic operator (U4): the operator is over no quantity or point, or in a body the checker types no row in (the stdlib’s own), and is lowered in its operands’ one type, operands of two types refused (binary op operands of mixed types)

Focused tests. crates/hale-types/tests/typed_bodies.rs; crates/hale-types/tests/codegen_fixtures_typecheck.rs; crates/hale-codegen/tests/corpus_check_build_agreement.rs; crates/hale-types/tests/unit_values.rs (the conversion rows, by shape); crates/hale-codegen/tests/unit_conversion_lowering.rs (the emitted shape per policy, a_cast_without_its_row_is_an_ordinary_call, a_defaults_cast_is_lowered_by_its_evaluations_row, and a_nested_defaults_cast_is_lowered_by_its_paths_row); crates/hale-types/tests/unit_quantities.rs (every site a denomination changes is a row); crates/hale-codegen/tests/unit_quantity_lowering.rs (the emitted shape per rounding, the checked division, the split, a point’s shift, a factor no Int holds, a_literal_in_a_default_is_each_evaluations_count, a_constants_cast_is_its_conversion_inside_a_default, a_mixed_array_literal_stores_each_elements_count, a_users_row_never_reaches_a_stdlib_expression_at_its_span, a_user_fn_named_like_the_stdlib_converts); crates/hale-types/src/typed_bodies.rs (a_body_reads_its_own_row_at_a_span_another_body_shares); crates/hale-codegen/tests/unit_dialect_unsupported.rs (a_quantity_literal_with_no_row_is_refused_where_it_is_written: the missing required row)

Spec. spec/types.md

Guarded seams.

• typed_bodies( may be referenced from: crates/hale-types/src/typed_bodies.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1

Answers. Which monomorph a generic call instantiates and how its bindings unify.

Inputs. generic declarations; call arguments; the mangled token vocabulary

Producer. crates/hale-types/src/check.rs · unify_generic_ty

Also owned. crates/hale-types/src/check.rs · monomorph_table; crates/hale-types/src/check.rs · specialize_generic_bodies; crates/hale-types/src/check.rs · record_specialized_type

Consumers. check (a mangled monomorph name: the table’s row) (crates/hale-types/src/check.rs · resolve_generic_monomorph); codegen (a generic fn call’s type arguments and specialization: the call’s typed-body row, and the monomorph table’s row for them) (crates/hale-codegen/src/codegen.rs · generic_call_instance); codegen

Invariants.

• one unification; the monomorph set is a row lowering reads
• lowering infers no generic argument: a generic fn call’s type arguments are its typed-body row (inside a fn or locus specialization, the owning body’s row typed for that monomorph, including params defaults in their declaring locus) and the specialization’s name is the monomorph table’s; a hole, or a call with no row, is refused at the call
• one monomorph table per snapshot (the typed-body table’s monomorphs), keyed by the template’s site and its type arguments, never by a name string: its producer parses a mangled name once, for each name the program spells (a written instantiation as the checker resolves it, an annotation, a struct literal’s path), against the bundle’s templates by identity; the checker’s lookups read the row
• a generic call inside a generic fn or locus body is typed again for each of the enclosing template’s monomorphs, the template’s parameters bound to its arguments, and recorded under them by its source body and call identities; that walk reports nothing and queues concrete instantiations reached in annotations for the same producer to walk
• omitted function and method defaults are typed at each invocation in the caller’s scope; their generic call rows retain the default’s source identity and distinguish the invocation path (nested defaults included) and the caller’s specialization, and lowering reads that corresponding row without inference; a supplied argument evaluates no default

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · generics_a_call_without_its_row_is_refused_at_the_call; total: no row means no specialization: a call with no specialized row for its enclosing body or locus reads its own, and a monomorph the table does not name is not queued ahead of the source walk

Focused tests. crates/hale-codegen/tests/generic_monomorph_agreement.rs; crates/hale-types/tests/typed_bodies.rs

Spec. spec/types.md

Answers. Which surface is visible at which depth edge: contract exposure, interface conformance, perspective designation and serves conformance.

Inputs. type, interface, contract, perspective declarations; locus members

Producer. crates/hale-types/src/check.rs · conformance_witness

Also owned. crates/hale-types/src/check.rs · conformance

Consumers. check (crates/hale-types/src/check.rs · check_contract_expose_validity); check (crates/hale-types/src/check.rs · check_serves_conformance); check (crates/hale-types/src/check.rs · check_reperspective); check (interface coercion, F.20) (crates/hale-types/src/check.rs · check_structural_impl); check (a bus adapter binding’s __StdBusAdapter contract) (crates/hale-types/src/check.rs · check_main_and_bindings); the typed-body table (the conformance column: every declared locus and interface pair, every generic locus specialization, the merged stdlib’s pairs in the lowering view) (crates/hale-types/src/typed_bodies.rs · typed_bodies); codegen (storage routing: the conformance column) (crates/hale-codegen/src/types/mod.rs · locus_satisfies_interface); codegen (vtable swap)

Invariants.

• F.8 compatibility, F.14 and F.20 satisfaction are judged once, with a witness
• one conformance function (conformance_witness), its witness the first requirement unmet in the interface’s method order, rendered by each caller in its own words; the bus adapter’s contract is judged without the error channel, as it always was
• storage routing asks the conformance column, never the method names, and requires the checker’s verdict that the locus satisfies the interface: a locus whose methods match the interface’s by name and not by signature, or a generic locus’s specialization, is no interface’s, so its literal stays the frame’s (a classified correction: the name comparison sent both to the program-lifetime payload arena; pinned in conformance_routing_correction.rs)

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · surfaces_a_pair_without_its_conformance_row_is_refused; total: no row means no interface: a name that declares none is satisfied by nothing

Focused tests. crates/hale-types/tests/perspective_serves.rs; crates/hale-types/tests/violate_fallible.rs; crates/hale-types/tests/duplicate_member.rs; crates/hale-types/tests/typed_bodies.rs; crates/hale-codegen/tests/conformance_routing_correction.rs

Spec. spec/types.md; spec/semantics.md

Answers. Whether a form’s shape, its capacity slots and its projection class are well formed, and which operation set closes each slot.

Inputs. @form arguments; capacity declarations; indexed_by; sync discipline (the sync_inference form rows)

Producer. crates/hale-types/src/check.rs · check_form_shape

Consumers. check; codegen (slot layout: the form row’s cap and sync discipline) (crates/hale-codegen/src/locus/decl.rs · ring_buffer_cap); sync_inference

Invariants.

• the operation set a form closes over a slot is a row: it is what a storage binding (F.44) will need
• the form row carries the form’s fixed capacity (FormRow::cap: a ring buffer’s or an LRU cache’s cap =, and a lockfree map’s), and codegen’s slot layout reads it and the sync discipline from the row (FormRows::of), never the form’s arguments (C3 rest); the view holds a row for every @form declaration it lowers, the merged stdlib’s as written, and a declaration with none is refused at its name (F.40 phase 3’s exit)

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · forms_a_form_without_its_row_is_refused_at_its_declaration

Focused tests. crates/hale-types/tests/reserved_locus_members.rs; crates/hale-codegen/tests/form_vec_bce.rs; crates/hale-types/tests/form_rows.rs (the_row_carries_the_forms_fixed_capacity)

Spec. spec/forms.md; spec/memory.md

Answers. What each stdlib function is: its signature, its effect classes, whether it blocks, how it lowers, and what a value of a type can be rendered as.

Inputs. one table of stdlib functions (SURFACES: one row per function, grouped by namespace: its name, whether user code may call it, its effect classes, its signature when it has one (with the error type of a function that can fail), and how it lowers: an intrinsic id, a Hale body by name, one Hale body per receiver type, a rename, or not at all); one rule of what prints (hale_types::printable: prints over a one-level PrintShape each reader maps its own type into); one table of the builtin types (BUILTIN_TYPES: per type its name, its fields in order as a name and a primitive, and when the checker injects it); hale_stdlib::PATH_RENAMES; the parsed stdlib source; std::time’s types, declared in the stdlib’s seed (crates/hale-stdlib/hl/time.hl, U4: the time catalogue, Duration, Time), which the table’s signatures name as SigTy::Duration and SigTy::Time

Producer. crates/hale-types/src/stdlib_surface.rs · SURFACES

Also owned. crates/hale-types/src/printable.rs · prints; crates/hale-types/src/builtin_types.rs · BUILTIN_TYPES

Consumers. effects (crates/hale-types/src/effects.rs · effects_for); frontier (crates/hale-types/src/frontier.rs · effects_for); resolve (the stdlib error-type shadow rule: which builtin error a path-call fails with is its row’s error column) (crates/hale-types/src/resolve.rs · stdlib_call_error); purity (a stdlib call is impure when its public row carries syscall, block or publish: the effect rows’ purity column reads the table and keeps no list of its own) (crates/hale-types/src/purity.rs · is_impure_stdlib); codegen; codegen (the printable rule: value_to_string_supports maps a CodegenTy into the rule’s shape before rendering) (crates/hale-codegen/src/codegen.rs · value_to_string_supports); check (the printable rule: ty_is_printable_at maps a Ty into the rule’s shape for println, to_string, an f-string and the String + x coercion) (crates/hale-types/src/check.rs · ty_is_printable_at); codegen (the builtin types’ structs, declared from their rows before the program’s types) (crates/hale-codegen/src/codegen.rs · declare_builtin_types); check (the builtin types injected into the top scope from their rows) (crates/hale-types/src/resolve.rs · inject_builtin_types); lsp (hover, completion); doc

Invariants.

• one row per stdlib function: the signature, the effect classes and the lowering of a path are columns of the same row, and every question the checker, the effects analysis, the catalogue and the LSP ask (lookup, the unknown-function diagnostic, the did-you-mean, the effect set, the signature) reads it; an internal row answers only the signature; whether a function can fail is its row’s error type, and every function lowering lowers only under or has one, so a bare call of one is the check’s bare-fallible error (F.40 phase 4, S5)
• every public row has a signature, the one its lowering enforces (F.40 phase 4, S6: the helper’s argument count, each argument’s type as the helper’s test accepts it, Any where it accepts more than one type the table can say, Any for a success the table cannot state), save 27 of the 39 renamed rows, which the check types against their Hale bodies’ own signatures (GH #470); of the table’s 432 rows (424 public, 8 internal), 353 lower by an intrinsic, 39 by a Hale body, 1 by one Hale body per receiver type and 39 by a rename, and the 8 internal rows carry no signature; the seven std::io::mirror cursor primitives are signed with the count and types their helper reads, though the helper does not count them, so the check refuses the extra arguments lowering ignored (S6’s ruling); std::io::udp::set_multicast_loop’s flag is Bool, the spec’s contract and its sibling set_option_bool’s, though the helper it shares with set_multicast_ttl also lowers an Int, so the check refuses an Int flag; for a checked call of any other row the helper’s own arity and argument tests are unreachable (kept, since the codegen tests lower programs the check refuses)
• codegen dispatches every stdlib call from its row, at all three positions: at statement or value position the position is a parameter (lower_std_call), an intrinsic’s id picks its arm in one exhaustive match with no catch-all (lower_std_intrinsic), a Hale body is called by the name its row gives, an overload on the first argument is the row’s (one body per receiver type, HaleBodyByReceiver: the receiver is lowered once and its type picks the body), and a renamed or unlowered row reaches the fallback, where a statement calls a body that returns nothing and is done; under or (lower_std_fallible_call) the id picks its arm in an exhaustive match of its own beside it (lower_std_intrinsic_fallible), because what it produces is the call’s success value and its error path, and any other row is not a stdlib fallible call; every intrinsic row is lowered at some position, every Hale-body row names a declared body, a renamed row is a rename, and the unlowered rows are named (parity test)
• lowering decides nothing about a stdlib call’s fallibility or its overload: which calls it refuses is the rows’ (no id list): a bare call of a function whose row can fail reaches one arm of lower_std_intrinsic (bare_call_of_a_fallible_row), and an or over one whose row cannot reaches the last arm of lower_std_intrinsic_fallible (or_over_an_infallible_row); the check refuses both first, so lowering’s answer is an internal error naming the row at the callee, save an or over an intrinsic row with an Any success (std::bytes::builder::__view / __text_view), which the check types permissively and lowering refuses (every public intrinsic row is signed, so an internal row, which user code cannot call, is the only one with none); no fallible row keeps a bare arm that lowers, and no row that cannot fail is lowered under or (parity test: which_calls_lowering_refuses_is_the_rows_fallibility)
• no ["std", path literal in crates/hale-codegen/src outside CODEGEN_STD_PATH_LITERALS, the registry’s allowance with its reason per file (registry_guard.rs: std_path_literals_in_codegen_are_the_registry_allowance): a stdlib call’s lowering is an arm of a match on its row’s id, never a match on its path
• the checker and codegen agree on every stdlib call shape (parity test)
• what prints is one rule, which the checker and lowering both read (F.40 phase 4, S7): hale_types::printable::prints, over the PrintShape each side maps its own type into, so hale check and hale build give one answer for println, to_string, an f-string and the String + x coercion; a record prints when every field does, a fixed array or a bounded when its element is a scalar, a StringView as its text (copied), and Bytes, its views, a locus, a function, a fallible and an unsized array do not; a type the checker cannot see (Unknown, an unresolved name) prints, which lowering never meets
• the builtin types are declared once (F.40 phase 4, S8): BUILTIN_TYPES holds each one’s fields in order, the checker injects each from its row (always, or BusUnmatchedKey only in a bundle with an on_unmatched: fail topic), the unknown-type-name rule accepts each name, the stdlib error-type shadow rule compares a user’s declaration against its row’s fields, and lowering builds each struct from the row; a declaration of the same name in the program wins on both sides; ClosureViolation is injected like the others since S8, so an on_failure handler’s reads of it are typed
• std::time’s two types and its catalogue are declarations of the stdlib’s seed (crates/hale-stdlib/hl/time.hl, GH #1076, U4: unit ns; through unit day = 24 h;, type Duration = quantity Int in ns;, type Time = point Duration;), not rows of this table: they are unit_declarations rows in the stdlib’s universe, and the unit dialect’s algebra types their arithmetic. A type position reads each name as its primitive, so the table’s std::time rows take and return them as SigTy::Duration and SigTy::Time, nanoseconds at the C boundary as they always were, and no signature changed with the declarations

Missing data. total: no row means the path is not one of the table’s functions: lowering calls the stdlib Hale declaration the path names by its mangled name (a Hale-source stdlib function, GH #470) and refuses any other path as not implemented, which the check’s unknown-function error refuses first (lower_std_unarmed); a type with no BUILTIN_TYPES row is the program’s own, and the printable rule answers every type

Focused tests. crates/hale-codegen/tests/stdlib_registry_parity.rs; crates/hale-codegen/tests/stdlib_table_answers.rs; crates/hale-codegen/tests/stdlib_statement_position.rs; crates/hale-types/tests/stdlib_sig_check.rs; crates/hale-codegen/tests/corpus_check_build_agreement.rs; crates/hale-codegen/tests/printable_rule.rs; crates/hale-codegen/tests/builtin_types.rs; crates/hale-types/tests/time_declarations.rs (the std::time types as the seed’s declarations, their FFI classes and an @ffi fn over them); crates/hale-cli/tests/doc_effects_catalogue.rs; crates/hale-graph/tests/registry_guard.rs (std_path_literals_in_codegen_are_the_registry_allowance)

Spec. spec/stdlib.md; spec/semantics.md § Rendering values as text

Answers. Which locus is the program’s main, whether the world is closed, and which declarations are imported.

Inputs. locus declarations (is_main, imported, module nesting); the top-level fn main; the minted sites

Producer. crates/hale-types/src/entry.rs · entry_row

Consumers. check (rule 1’s count reads the witness: the seed’s own mains, module-nested ones included) (crates/hale-types/src/check.rs · check_main_and_bindings); placement (the table is seeded from the row’s root, EntryRow::root: the entry, or the refused module-nested main of a seed with none, so the rules that read the table still judge it; the F.31 rule, the form rows’ sync inference, the blocking check, the pinned-in-a-loop rule, instance aliasing and the model’s arrangement read it) (crates/hale-types/src/placement.rs · derive_placement); check (decision 2’s refusal, a lowering law: a seed whose only main locus is module-nested, EntryRow::refused, is refused once at that locus’s name, by the check and by the harness’s lowering view) (crates/hale-types/src/lowering_laws.rs · module_nested_main_is_not_the_entry); check (rule 9’s closed world is a program with an entry, and its api exemption is the entry’s api: binding, never an imported main’s, which is inert) (crates/hale-types/src/check.rs · check_bus_graph); check (each main locus‘s own placement { } block is validated over the witness, deployed or not: an affinity on no named pool, two for one pool) (crates/hale-types/src/check.rs · check_pool_affinity); bus_graph (the closed world: the entry, or a top-level fn main) (crates/hale-types/src/bus_graph.rs · build_bus_graph); ownership (the closed world: the entry, or a top-level fn main, the bus graph’s test; the producer hands the walk its row, and the rows of a bundle no snapshot holds, OwnershipRows::of, build theirs; the stdlib’s rows have none) (crates/hale-types/src/ownership_graph.rs · collect_ownership_walk); effects (the async_io placement-implied advisory: the row’s root’s placement, the pools lowering spawns) (crates/hale-types/src/effects.rs · placement_implied_diags); check –matrix (a seed is an entrypoint when its row has an entry; the row is built over the seed’s own files, since no import holds the entry, so a seed whose import does not resolve is still counted and its pair reports the import) (crates/hale-cli/src/verbs/check/matrix.rs · seed_entry_kind); –env on check and the build paths (the load refuses an environment for a seed with no entry, after the mint, before the sequence’s own refusal) (crates/hale-frontend/src/snapshot.rs · demand_entry); build; dna; codegen (the deployment plan’s root is the placement table’s, the row’s entry) (crates/hale-codegen/src/codegen.rs · collect_main_placement); codegen (fn main is the row’s column, found by its site: the body in_main marks, whose return and assertion-failure exits key on it; a view with no row is refused before lowering, never given the row’s definition, top_level_fn_main) (crates/hale-codegen/src/codegen.rs · entry_fn); bindings (codegen’s binding term counts the entry’s entries, by the declaring locus’s site) (crates/hale-types/src/binding_rows.rs · binds_on_main); the lifecycle plan (the deferred main entry’s spine is the entry’s, by identity) (crates/hale-types/src/lifecycle/derive.rs · is_entry); the lowering view (the snapshot’s row, carried to codegen) (crates/hale-frontend/src/snapshot.rs · view.entry = Some(entry)); codegen (every comparison against the main locus reads the row’s entry, found in lowering’s program by its site: instantiation’s and the cascade’s placement overrides, the deferred entry’s pool join, the frame flush’s main-locus head before its pinned joins, whether the root’s literal hands it back so it keeps the join record of every replica of its pinned fields, and which struct carries those records (C52), the bindings prelude’s loss handler, and root_bindings, which the shm-ring subjects and the binding codec thunks read) (crates/hale-codegen/src/codegen.rs · is_entry_locus); –env and –matrix (an environment’s constitutions are adopted into the row’s root, the seed’s own main locus the build deploys: the entry, in every seed an environment may be bound to) (crates/hale-frontend/src/snapshot.rs · adopt_into_root); model (the header’s entrypoint names the root the arrangement is rooted at, the placement table’s, so the row’s root; main when there is none) (crates/hale-types/src/model_builder.rs · derive_application_model_over); lsp (hale/placement shows the row’s root’s params and placement block, a refused module-nested root included, never an imported library’s main locus) (crates/hale-lsp/src/lib.rs · placement_of); hale dna init (the seed’s entry and its file, by the row over the seed’s own files that parse, as seed_entry_kind reads it: no import is resolved, and none holds the entry) (crates/hale-cli/src/dna.rs · main_of); claims (the world tier: the row’s world(), every main locus the bundle declares, whose inline claims are the world law, an imported application’s included, GH #733; a bundle that closes a world refuses a top-level claims block of the closing seed’s own) (crates/hale-types/src/claims.rs · enumerate_clauses); the cross-seed rename (GH #774: an imported seed closes a world, so its constitutions’ vocabulary is its own, when the row over its own files, none of them renamed yet, has an entry) (crates/hale-types/src/mangle.rs · seed_declares_main)

Invariants.

• the checker builds no row: the snapshot demands it before the check and hands it in (CheckInputs::entry); a bundle no snapshot holds (the test entries) builds it once, the form rows read the snapshot’s (demand_forms), and the check matrix builds one over each seed’s own files (no import holds the entry, and a seed whose import does not resolve is still an entrypoint)
• what lands in the row’s root (EntryRow::root) before the mint (an environment’s constitutions) finds it by the producer’s row over the programs as they stand (entry_row_in, each program named by its index), and a reader handed programs and no bundle reads it there; an injection adds members and trailing top-level items, never a main locus or a module, so the snapshot’s row names the same declaration after the mint
• one row per snapshot (Snapshot::demand_entry, the entrypoint count): the entry by its minted site, and every main locus the bundle declares as the witness, each with whether it is imported and whether it is module-nested; it reads declarations only, so no diagnostic blocks it, and a seed with a hole (no identities) blocks it with its scope
• an imported main is not the entry (decision 1, E0): a library’s main locus is a declaration the importing seed does not run, and the entry is the importing seed’s own; a seed whose only main is imported has no entry (NoEntry::OnlyImported). Imported is one definition, the rename pass’s mark (imported, GH #1104 piece 5); the __lib_ name the same pass gives is spelling, not a second test of the entry, and lowering reads the mark too (L4), so a program handed in with an unmarked __lib_ main deploys it
• a module-nested main is not the entry (decision 2, E0): the entry is a top-level main locus of the seed’s own files, so rule 9’s closed world is the top-level one; a seed whose only main is module-nested has no entry (NoEntry::OnlyModuleNested), and a seed with both keeps the top-level one. Rule 1 still counts a module-nested main (GH #825): the count reads the witness, not the entry
• a seed whose only main locus is module-nested is refused (L4): one located error at that locus’s name (EntryRow::refused, the lowering_laws law), so the check, the build, the editor and the harness agree and no program reaches lowering with a root that is not the entry. It is one more diagnostic, never a replacement: the placement table is seeded from EntryRow::root, the entry or else the refused main, so the placement-safety rules (the F.31 rule, the pinned-in-a-loop rule) and every other rule still judge it (GH #825; the outside review of #1293, finding 1). A seed with an entry is not refused for a module-nested main beside it
• with more than one candidate (rule 1’s error) the entry is the last, as the checker’s pool map (since replaced by the placement table) took it before the row
• the checker, the environment, the model, the editor and the CLI read the row (F.40 phase 3, the entry’s consumers), and so does lowering (L4): what reads the root before the check refuses a seed (an environment’s constitutions, the model’s entrypoint, the editor’s placement view, the async_io advisory) reads EntryRow::root, the placement table’s root, which is the entry in every program that reaches lowering; no legacy site is left, and the row has one definition of the main locus and one of fn main (top_level_fn_main)
• lowering reads the entry (L4) and derives no main locus and no fn main: the lowering view carries the row (LoweringView::entry); codegen’s comparisons against the main locus read its entry by identity (is_entry_locus, root_bindings), never a type name or the first is_main && !__lib_; fn main is the row’s column (EntryRow::fn_main, by its site), so in_main marks that declaration’s body; the binding term (binds_on_main) counts the entry’s entries by the locus’s site, and the lifecycle plan’s deferred main entry is the entry by identity
• the world is wider than the entry, on purpose: EntryRow::world is every main locus the bundle declares (the entry’s, a module-nested one’s, an imported application’s), because decisions 1 and 2 say which declaration the seed runs, and an application’s inline law keeps binding when another seed imports it (GH #733, crates/hale-cli/tests/imported_main_claims.rs); the claims read the row’s column and gather no is_main of their own
• three readers of the main keyword read a property of each declaration and derive no entry fact, so they are no definition of the entry and no legacy row, whichever main is the entry: check_nested_long_running_child exempts every main locus, as a parent (parent.is_main) and as a child (!l.is_main), from the long-running-child rule, since a root is supervised by no parent; the ownership graph makes every main locus declaration a singleton (singleton |= l.is_main), one instance per declaration, deployed or not; and the allocation summary defers every main locus declaration, module-nested ones included, from eager reclamation (if l.is_main in its flat walk), conservatively. Each expression is a seam, so a second reader of the keyword in those files is a new row to classify
• every non-test reader of LocusDecl::is_main is the producer or one of the three per-declaration readers above; the binding rows copy the keyword into each row as a column (is_main: l.is_main), the parser’s main-only member rules are syntax and are not rows, and sync_inference’s test helper is test code

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · entrypoint_a_view_without_the_entry_row_is_refused; total: no entry in the row means no main locus is deployed, and no fn main column means the program has none, which lowering refuses as such

Focused tests. crates/hale-frontend/src/snapshot.rs (the_entry_row_is_the_seeds_own_top_level_main_locus); crates/hale-cli/tests/check_entry_decisions.rs; crates/hale-cli/tests/check_entry_consumers.rs (each consumer’s correction on the decided shapes, beside a control); crates/hale-lsp/src/lib.rs (the_placement_view_is_the_deployed_roots); crates/hale-cli/tests/nested_main_transition.rs (after the transition, end to end: a seed whose only main locus is module-nested is refused by check and build, beside its own errors, and the top-level control is deployed); crates/hale-types/tests/checks_inside_modules.rs (the refusal’s message and span; a module variant reports the control’s messages, and the refusal as its one addition); crates/hale-cli/tests/offthread_imported_main.rs (the binding term counts the entry’s entries); crates/hale-cli/tests/entry_point_placement.rs; crates/hale-types/tests/bus_graph.rs

Spec. spec/semantics.md § Bundle-wide rules

Guarded seams.

• entry_row( may be referenced from: crates/hale-types/src/entry.rs ×2, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1, crates/hale-cli/src/verbs/check/matrix.rs ×1, crates/hale-types/src/sync_inference.rs ×1, crates/hale-types/src/placement.rs ×1, crates/hale-types/src/ownership_graph.rs ×1, crates/hale-types/src/lifecycle/derive.rs ×1
• is_entry_locus( may be referenced from: crates/hale-codegen/src/codegen.rs ×3, crates/hale-codegen/src/locus/instantiation.rs ×2, crates/hale-codegen/src/locus/dissolve.rs ×2, crates/hale-codegen/src/locus/decl.rs ×1
• world() may be referenced from: crates/hale-types/src/claims.rs ×1
• parent.is_main may be referenced from: crates/hale-types/src/check.rs ×1
• !l.is_main) may be referenced from: crates/hale-types/src/check.rs ×1
• singleton |= l.is_main may be referenced from: crates/hale-types/src/ownership_graph.rs ×1
• if l.is_main { may be referenced from: crates/hale-types/src/alloc_summary.rs ×1, crates/hale-types/src/rpc_expand.rs ×1

Answers. Who owns each locus-producing expression and each instance: the tower, with its two relations accepts_ancestor and owner_of_site; and, per binding site, whether its value is handed back, moved by =, or a frame-local array.

Inputs. locus declarations (params, accept, release); bodies (let, assign, return, field initialisers, placement entries); fresh factories (one producer); returned bindings; placement (the table: each bubbling edge’s class, per instance)

Producer. crates/hale-types/src/ownership.rs · resolve_owners

Also owned. crates/hale-types/src/ownership.rs · resolve_binding_facts; crates/hale-types/src/ownership_graph.rs · bubble_plans; crates/hale-types/src/ownership_graph.rs · compute_forwarding_sets; crates/hale-types/src/ownership_graph.rs · classify_owner_kind; crates/hale-types/src/ownership_graph.rs · classify_edge; crates/hale-types/src/ownership.rs · fresh_factories

Consumers. codegen (crates/hale-codegen/src/locus/instantiation.rs · site_owner); codegen (a monomorph’s accept rows: its template’s, specialized at synthesis) (crates/hale-codegen/src/codegen.rs · specialized_accepts); codegen (whether the enclosing locus accepts the child it births) (crates/hale-codegen/src/locus/instantiation.rs · parent_accepts_us); borrow_lifetime (a bare literal’s enclosing locus accepts its child: accepts_ancestor, over the snapshot’s graph’s rows) (crates/hale-types/src/borrow_lifetime.rs · accepts_ancestor); lowering view (its graph: the snapshot’s rows through the correspondence, then the stdlib’s; the bubble plans, accepts and the accept rows lowering reads) (crates/hale-types/src/resolved.rs · lowering_ownership_graph); model (dynamic births: the snapshot’s graph) (crates/hale-frontend/src/snapshot.rs · demand_ownership_graph); a declaration’s dependents (X2: a locus’s births, accepts and instantiations make its neighbours through the ownership graph, the snapshot’s graph) (crates/hale-frontend/src/snapshot.rs · declaration_dependents); check (type-check rule 20, the unowned-subscriber rule: owner_of_site over the snapshot’s graph, handed in through CheckInputs) (crates/hale-types/src/check.rs · check_unowned_subscriber_locus); alloc_summary (eager-only accept sets); check and the harness (the cross-pool spawn law reads the bubble plan) (crates/hale-types/src/lowering_laws.rs · cross_pool_spawn_used_as_a_value); codegen (the handed-back column: a root some literal hands back keeps its pinned fields’ join records in their instances, C52) (crates/hale-codegen/src/codegen.rs · collect_main_placement)

Invariants.

• a locus instantiation with no row is a CodegenError (F.39)
• rule 20 is a law::Law over the graph and the placement table its construction paths come from (UnownedSubscriberRows); its finding is a law::Violation whose witness steps are the declaration judged when two share the child’s name and the construction path no accepting ancestor lies on (phase 4, W5)
• ids, not names or spans: declarations are cloned and the stdlib’s coordinates overlap user files
• the ownership matrix stays green with an empty KNOWN_OPEN
• the model’s Owns edges are the placement table’s owner column projected with the arrangement (P1 4 of 6, C3): an arranged instance is owned by the arranged instance its row names as owner; owns.push( has that one writer
• the model reads construction context from the ownership graph (C3): the shared walk records body births, field defaults and binding adapters with their explicit fields and literal identities. unarranged_births follows the defaults each construction actually evaluates; the same default can be arranged for one holder and dynamic for another, while an overridden default adds no birth. The arrangement projection (project_arrangement, which the model’s rows are made from) supplies the literal identities its placement rows represent, including held sources, and joins each remaining birth by resolved declaration site (name fallback only for unminted bundles). No model-side params-span test or free-function walk remains; copied API-binding expressions retain their construction context despite overlapping spans
• the graph keeps each accept param as a row of the declaring locus’s identity, its type as written (AcceptRows); a monomorph’s accept set is its template’s rows, asked for by the template’s identity and specialized by the instantiation’s substitution (AcceptRows::specialize, as FlowRows::specialize does for release clauses), filled at synthesis; lowering never reads a monomorph’s own accept_param for ownership
• fresh_factories is read by lowering and the checker with the bundle’s import renames; a factory’s returned name is the declaration the snapshot resolves it to, so a fn whose returned name an inner let shadows is a factory of the outer binding (the #1140 shape; its escape walk still reads every binding spelling the name as the returned one, the conservative side). The carrier-arm extension (extend_fresh_factories) is one set both read: lowering through the owner table, and the checker’s self-containment law through extended_factory_rows, which gives each fn the fold adds a row whose products are its arms’ (F.40 phase 3, C5: the decision measured no diagnostic moving over the corpus, tests/hale and the DNA seeds; the fold’s one addition there, in the DNA core, already had a row)
• which declaration a returned or escaping name denotes is read from the snapshot (Snapshot::declaration_of over binding_of, resolved once by the mint), never resolved again: returned_bindings (the binding facts and the pre-pass), fresh_factories, borrow_lifetime’s returned_decls and alloc_summary’s escape tags each key a binding by its declaration’s SiteId; a let or a use the snapshot did not mint answers by name in returned_bindings (the conservative side) and resolves to nothing elsewhere, and every entry point mints
• the checker builds no graph: the snapshot demands it before the check and hands it in (CheckInputs::ownership), so a check with a law builds it once for the checker and the model together; a bundle no snapshot holds (the test entries) builds it once, through the producer (build_ownership_graph), and the model over that bundle reads the same build
• one graph per snapshot (F.40 phase 3, C5): the graph keeps the rows it is assembled from (OwnershipRows), and lowering’s graph is the snapshot’s rows, each site and accepting locus found in the merged program through the view’s correspondence, followed by the stdlib’s rows over the merged program’s tail (stdlib_ownership_rows), the one part no snapshot holds; one procedure assembles either (lowering_ownership_graph)
• the tower’s accept relation is one relation, accepts_ancestor (OwnershipRows::accepts_ancestor): the climb finds an owner by it, and the borrow-lifetime law asks it of a bare literal’s enclosing locus, over the snapshot’s graph’s rows (a bundle no snapshot holds walks its own, OwnershipRows::of)
• rule 20 is judged by declaration identity (owner_of_site): the graph lists every locus declaration in declaration order, and a site carries the declaration its literal names (child_decl, joined by the shared resolver’s declaration identity, with a name fallback for unminted input) and the child an accept must name to own it (child_key: an import or std:: path resolved as an accept’s type is, a template specialized by its binding’s or field’s declared type); the nearest accepting ancestor owns a birth in a handler as it owns any other, but only if one accepts the child on every construction path of the enclosing locus (construction_paths, over the placement table: each instance row under its owner row’s declaration, a template’s top as a root with no ancestor, a literal directly in fn main included, each dynamic site under its enclosing locus or in a free fn whose callers are not followed; with the walk’s own body and params-default edges, since the table does not enumerate a dynamically built locus’s params subtree), and the diagnostic names a path with none. child_ty, resolution and bubble plans use the resolved child name, following imports and aliases and retaining a known generic specialization; plain records and unresolved paths are not births. Lowering’s bundle carries its minted snapshot, so the declaration join keeps its identity. Lowering’s instantiated_by still records no free-fn birth
• the holes: where the graph cannot decide, owner_of_site answers None and rule 20 does not fire, since unknown ownership is not proven absence: an open world (no entry, so a consumer may complete the tower), a generic template no declared type specializes, a qualified path that names no declaration, and an unanalyzable site; a literal assigned to a field of self is judged by the accept edges, since the graph records no assignment target. A construction path the placement table records as a hole cuts the other way, since an unknown path cannot prove an owner: a held instance the table does not link, a field whose initializer is no literal, a dynamic site of unknown domain and an owner row whose declaration does not resolve each count as a path with no ancestor, and so does a free fn; a held row the table links adds no path (its source row is the construction)
• a bubbling edge’s class reads the placement table per instance: each row of the enclosing locus is paired with the row that owns it, every other instance with every domain of the owner; SameTower when every pair shares its domain, CrossPool when none does and the owner has one, Mixed otherwise or where an instance runs where the table cannot say. The graph reads no placement { } block itself
• the owner is a fact of the site, the mechanism of the instance (U-1): a Mixed edge keeps its resolved owner, takes the same-tower birth or the cross-pool post per enclosing instance where the owner is a singleton on main (lotus_on_main_thread at the literal), and is refused at the literal (CodegenError::UnsupportedAt, naming every instance and its domain) for a value use or a non-singleton owner; it is never lowered as a transient birth

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · ownership_an_instantiation_without_its_owner_row_is_refused; total: no accept row means the enclosing locus does not accept the child, no bubble plan means no ancestor owns it, and no factory row means the fn is no fresh factory

Focused tests. crates/hale-types/tests/model_arrangement.rs; crates/hale-codegen/tests/owner_table.rs; crates/hale-codegen/tests/ownership_matrix.rs; crates/hale-codegen/tests/ownership_reclaim.rs (shadow_return_binding); crates/hale-codegen/tests/ownership_bubble.rs; crates/hale-cli/tests/check_unowned_subscriber.rs (rule 20, one test per class of the migration); crates/hale-types/tests/ownership_graph.rs (lowerings_graph_is_the_snapshots_rows_through_the_correspondence); crates/hale-types/tests/self_containing_locus.rs (a_factory_returning_a_carrier_is_reported, a_carrier_with_an_accessor_arm_is_not_a_cycle: the checker reads the extended factory set); crates/hale-cli/tests/check_borrow_lifetime.rs (the law over accepts_ancestor); crates/hale-types/tests/ownership_graph.rs (the O rows: nested under pinned, on the owner’s pool, per-instance pairing, adapter, mixed); crates/hale-codegen/tests/ownership_bubble_mixed.rs (U-1: both instances’ owner, count, retention, birth thread and teardown, both arms and ASan; the transient control; the located refusal); crates/hale-codegen/tests/ownership_bubble_crosspool.rs (O-1 under ASan)

Spec. spec/decisions.md F.39; spec/semantics.md § Dissolve timing rules; spec/semantics.md § Placement block (type-check rule 20); spec/semantics.md § Locus instantiation (accept bubbling: the owner per site, the delivery per instance); spec/runtime.md § Interest-based ownership (accept bubbling)

Guarded seams.

• resolve_owners( may be referenced from: crates/hale-types/src/resolved.rs ×1, crates/hale-types/src/ownership.rs ×1
• build_ownership_graph( may be referenced from: crates/hale-types/src/ownership_graph.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1
• stdlib_ownership_rows( may be referenced from: crates/hale-types/src/ownership_graph.rs ×1, crates/hale-types/src/resolved.rs ×1
• lowering_ownership_graph( may be referenced from: crates/hale-types/src/ownership_graph.rs ×1, crates/hale-types/src/resolved.rs ×1
• accepts_ancestor( may be referenced from: crates/hale-types/src/ownership_graph.rs ×3, crates/hale-types/src/borrow_lifetime.rs ×1
• fresh_factories( may be referenced from: crates/hale-types/src/resolved.rs ×1, crates/hale-types/src/ownership.rs ×2
• extended_factory_rows( may be referenced from: crates/hale-types/src/ownership.rs ×1, crates/hale-types/src/lowering_laws.rs ×1
• extend_fresh_factories( may be referenced from: crates/hale-types/src/ownership.rs ×3
• resolve_binding_facts( may be referenced from: crates/hale-types/src/ownership.rs ×1, crates/hale-types/src/resolved.rs ×1
• returned_bindings( may be referenced from: crates/hale-types/src/ownership.rs ×3
• bubble_plans( may be referenced from: crates/hale-types/src/ownership_graph.rs ×1, crates/hale-types/src/resolved.rs ×1, crates/hale-types/src/lowering_laws.rs ×1
• owns.push( may be referenced from: crates/hale-types/src/model_builder.rs ×1
• owner_of_site( may be referenced from: crates/hale-types/src/check.rs ×1
• demand_ownership_graph( may be referenced from: crates/hale-frontend/src/snapshot.rs ×8, crates/hale-cli/src/verbs/check/run_impl.rs ×1

Answers. The message graph: subjects, publishers, subscribers, handlers, and the per-subject devirtualization gates.

Inputs. topics; bus blocks; sends; bindings; placement (the table: every label, and so the direct-call gate)

Producer. crates/hale-types/src/bus_graph.rs · build_bus_graph

Also owned. crates/hale-types/src/bus_graph.rs · dispatch_gates; crates/hale-types/src/bus_graph.rs · cycle_from; crates/hale-types/src/bus_graph.rs · external_handlers

Consumers. check (rule 9: the wire rows, their bound, cross-seed and wildcard columns, over the entry row’s closed world; the snapshot’s graph, CheckInputs::bus) (crates/hale-types/src/check.rs · check_bus_graph); check (rule 10: the edges by declaration, through cycle_from, each edge’s send joined to the intra-locus relation by its id, CheckInputs::intra_locus) (crates/hale-types/src/check.rs · check_bus_cycles); check (rule 7: the placed declaration’s row, external_handlers) (crates/hale-types/src/check.rs · check_cooperative_pool_blocking); check (rules 11, 12, 19); model (subjects, endpoints and gates: the snapshot’s graph) (crates/hale-frontend/src/snapshot.rs · demand_bus_graph); topology; dispatch; lsp (hale/busGraph: the model’s graph, so eligibility is the diagnostics pass’s) (crates/hale-lsp/src/lib.rs · demand_bus_graph); codegen (a rewritten publish, found by its call’s id in the relation: the probes and the reclaimed subregion) (crates/hale-codegen/src/codegen.rs · intra_locus_rewrite); lowering view (its graph: the snapshot’s rows through the correspondence, each user site keyed by the topic rewrite’s wire, then the stdlib’s; the plan lowering reads is its gates) (crates/hale-types/src/resolved.rs · lowering_bus_graph); the check of a bundle no snapshot holds (check::check_bundle, the hale-types tests’ scope-taking entry): the producer itself, once per call, over the caller’s scope (crates/hale-types/src/check.rs · build_bus_graph)

Invariants.

• one graph, over one program shape, per snapshot; rule 10’s cycle graph is a query over it (cycle_from)
• rules 9 and 10 are law::Laws over the graph (BusLawRows: the graph, the entry row, the scope’s declared topics, the intra-locus rewrite relation), their findings law::Violations with no witness steps, rule 10 naming its cycle in its message (phase 4, W5)
• lowering derives no graph of the user’s program: its graph is the snapshot’s rows (BusRows), each user site found in the merged program through the view’s correspondence and keyed by the wire the topic rewrite gave it, followed by the stdlib’s rows over the merged program’s tail (stdlib_bus_rows), the one part no snapshot holds; the subjects and their gates are assembled from the rows by one procedure (BusRows::subjects) on both sides
• the dispatch gates (derive_dispatch_gates, the dispatch family’s) are the same rows keyed by wire with the stdlib’s after them, the stdlib’s derived once per process over its analysis copy (stdlib_bodies::bus_rows, by the same stdlib_bus_rows) rather than over a merged program: equal to lowering’s graph’s gates, column for column and in registration order, over the corpus examples, the lifecycle fixtures, tests/hale and the DNA mains, build and harness snapshots (dispatch_gates.rs)
• a bundle no snapshot holds builds its graph through the snapshot’s producer (build_bus_graph), never through a wrapper of its own
• the checker’s bus rules (7, 9, 10) compare subjects under the canonical key, the wire subject (Subject, wires): a topic published by name and subscribed by its literal subject is one subject; the gates and the model keep BusSubject::canonical()’s keys (subjects)
• an edge belongs to the locus declaration that wrote its handler (BusEdge::decl), never to a name: two loci of one name have their own edges
• a subject the graph cannot resolve is a hole (holes): it forms no edge and no rule calls it an orphan
• the intra-locus rewrite is a relation on the graph, never an erased publisher (boundary 7)
• lowering reads the relation (LoweringView::intra_locus) by the call’s id, which the call that replaces a send keeps (IntraLocusRewrite::send); it never classifies a call as a rewritten publish from the call’s shape
• rule 10 calls a cycle synchronous only where the relation holds every send of it (BusEdge::send, the snapshot’s intra_locus stage, the one lowering continues from); a same-declaration cycle with a send the relation does not hold is carried by the queue, and the subjects’ spelling never decides which
• a placement label is the placement table’s answer for the type, by the name lowering keys on: SameThread only when every instance runs on main (a nested instance inherits its owner’s domain, an adapter is pinned, an instance the table cannot place is Unknown and never main); the graph reads no placement { } block itself

Missing data. total: no row in the intra-locus relation means the call is the one the author wrote (the relation names every send the rewrite replaced, and the call keeps the send’s id); within the graph, an unresolved subject stays a hole (holes), and the plan’s subjects are the dispatch family’s

Focused tests. crates/hale-types/tests/bus_graph.rs (lowerings_graph_is_the_snapshots_rows_through_the_correspondence); crates/hale-types/tests/lowering_correspondence.rs; crates/hale-types/tests/bus_graph.rs (the B rows: nested, imported root, qualified field, last-segment collision, two domains, adapter); crates/hale-types/tests/bus_rules_over_graph.rs; crates/hale-types/tests/bus_payload_handler.rs; crates/hale-codegen/tests/bus_devirt_differential.rs; crates/hale-codegen/tests/nested_offthread_delivery.rs (the dispatch-plan flavor of a nested subscriber, a nested publisher and an adapter’s publication)

Spec. spec/semantics.md rules 7, 9-12, 19; spec/verification.md § Bus-graph property checks

Guarded seams.

• build_bus_graph( may be referenced from: crates/hale-types/src/bus_graph.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1
• collect_bus_walk( may be referenced from: crates/hale-types/src/bus_graph.rs ×2
• stdlib_bus_rows( may be referenced from: crates/hale-types/src/bus_graph.rs ×1, crates/hale-types/src/resolved.rs ×1, crates/hale-types/src/stdlib_bodies.rs ×1
• lowering_bus_graph( may be referenced from: crates/hale-types/src/bus_graph.rs ×1, crates/hale-types/src/resolved.rs ×1
• dispatch_gates( may be referenced from: crates/hale-types/src/bus_graph.rs ×2
• cycle_from( may be referenced from: crates/hale-types/src/bus_graph.rs ×1, crates/hale-types/src/check.rs ×2
• external_handlers( may be referenced from: crates/hale-types/src/bus_graph.rs ×1, crates/hale-types/src/check.rs ×1

Answers. What each topic is on the wire: its subject, payload contract, routing key, bounds and shed policy; and which topic a send’s subject names.

Inputs. topic declarations; send subjects; subscribe bounds; bindings (shm_ring)

Producer. crates/hale-types/src/topic_identity.rs · topic_wire_subjects

Also owned. crates/hale-types/src/topic_identity.rs · TopicRows::of; crates/hale-types/src/topic_identity.rs · by_wire

Consumers. check (the topic rows, built once per bundle on the TopScope) (crates/hale-types/src/resolve.rs · build_top_scope); model (the scope’s topic rows: each topic’s wire, and the gate merge per wire) (crates/hale-types/src/model_builder.rs · ModelInputs); codegen (the lowering view’s rows: dispatch, bindings, codecs, runtime shape registration) (crates/hale-codegen/src/codegen.rs · topics: &resolved.top.topics); codegen (the shm-ring bindings: each bound topic’s wire and payload, from its row) (crates/hale-codegen/src/codegen.rs · collect_shm_ring_subjects); codegen (the routing-key, on_full-fail and subscriber-bound tables, from the rows) (crates/hale-codegen/src/codegen.rs · collect_routing_key_subjects); topology (topic shapes); resolved program (the intra-locus relation’s wire subjects) (crates/hale-types/src/resolved.rs · topic_wire_subjects)

Invariants.

• delivery joins on the subject’s identity, never on the written topic name (spec/model.md rule 8)
• a literal subject at a delivery site (a literal subscription, a literal send) names only the topic that OWNS that wire subject, TopicRows::by_wire, never one whose declared segment or name it happens to spell; a topic reference names its declaration; a wire subject two topics carry names neither and is an error
• lowering reads the topic rows of the lowering view’s scope (Cx::topics, over the program it lowers): a topic’s wire subject, payload, routing key, bound and on_full policy come from its row, and codegen computes no wire subject of its own

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · topics_a_declared_topic_without_its_row_is_refused_at_its_name; total: no row for a subject means it is already a wire (topic_wire, after the topic rewrite); a topic declaration’s name, a binding entry’s topic and a rewritten send’s topic are required (Cx::topic_row)

Focused tests. crates/hale-codegen/tests/topic_declarations.rs; crates/hale-codegen/tests/replica_keys.rs; crates/hale-codegen/tests/serializer_shape.rs; crates/hale-types/src/topic_identity.rs (a_subject_names_its_topic_by_one_rule, a_shared_subject_names_no_topic)

Spec. spec/semantics.md § Topic declarations; spec/semantics.md § Phase 3: routing keys

Guarded seams.

• topic_wire_subjects( may be referenced from: crates/hale-types/src/topic_identity.rs ×2, crates/hale-types/src/resolved.rs ×1
• TopicRows::of( may be referenced from: crates/hale-types/src/topic_identity.rs ×1, crates/hale-types/src/resolve.rs ×1
• by_wire( may be referenced from: crates/hale-types/src/topic_identity.rs ×6, crates/hale-types/src/check.rs ×2

Answers. Which topics are bound to which transport, in which role, with which codec, and whether the transport can carry the payload.

Inputs. bindings blocks; topics; transport specs; purity (codecs)

Producer. crates/hale-types/src/binding_rows.rs · derive_binding_rows

Consumers. check (the binding rules walk the rows: topic, duplicate, role, adapter, ring layout, constraints, codec; the or wait legality check reads the bound-topic set) (crates/hale-types/src/check.rs · check_main_and_bindings); check (a binding’s where constraints are held to its transport’s guarantee: the capability module’s table, read through the row’s transport kind) (crates/hale-types/src/capability/transport.rs · guarantee); the transport’s cell on the effective target: RemoteTransport(kind) × the target row’s backend, read through the snapshot (verdict-neutral: the adapter’s wasm refusal is a late link refusal today, a known-open cell) (crates/hale-frontend/src/snapshot.rs · binding_cell); model (main’s binding thread domains: the role and the transport kind) (crates/hale-types/src/model_builder.rs · ModelInputs); bus graph (the bound-topic set, at both grains, is the rows’ projection) (crates/hale-types/src/bus_graph.rs · collect_bus_walk); codegen (the prelude, the shm-ring subjects, the codec thunks and the pinned adapter loci read each entry’s transport kind, role, codec and producer-versus-attach from its row, through the lowering view; the entry’s own text supplies the transport’s parameters; a missing row is an error) (crates/hale-codegen/src/codegen.rs · root_bindings); codegen (whether a thread crosses the bus boundary: an entry of the entry’s bindings { }, binds_on_main, beside the placement table’s domains) (crates/hale-codegen/src/codegen.rs · program_has_offthread)

Invariants.

• the check’s per-binding walk (check_main_and_bindings) runs over these rows; of the rules it judges, the two the registry lists over rows (codec purity, the foreign-ring payload shape) find law::Violations, rendered where the walk reaches them, so the walk’s order holds; the rest (topic existence, duplicates, role inference, adapter conformance, the ring-layout rules, the where constraint rules, the codec signatures) are checks of the entry as written (phase 4, W5)
• the transport-loss handler is named by the row: a unix entry’s row carries the stdlib locus its transport instantiates (loss_locus, by role), lowering instantiates that locus, and a connect entry’s is the locus whose failure the main locus’s on_failure handles, so the handler is main’s routing row for the locus the bindings row names, not one picked by a spelled name
• lowering holds the rows (LoweringView::bindings, the snapshot’s) and finds an entry’s by the id the mint kept (BindingRows::for_entry); it decides no transport, role, codec or producer-versus-attach itself, and an entry with no row is a CodegenError, not a guess
• F.36 and F.37: binding failure is structural; codec purity is a law over rows
• one row per snapshot (Snapshot::demand_bindings, the bindings count): one row per bindings { } entry of every locus of the bundle, an imported main’s and a module-nested one’s included, each with the entry’s site, the topic and its wire key, the transport kind, the role, the codec, whether the bundle produces the topic and the stdlib locus a transport’s loss surfaces through; the checker builds none (CheckInputs::bindings), and a bundle no snapshot holds builds it once
• the role is decided once, over the topic’s ends read by wire subject (desugar::role_from_ends over the row’s publishes and subscribes): the entry’s own role wins, otherwise publish-only is Connect and subscribe-only is Listen, and a unix entry with neither is the checker’s diagnostic. The checker, the model and lowering read it; the desugar’s in-place fill applies the same pure rule over the topic names before the topic rewrite erases them, and agrees with it over the corpus
• what a transport carries is data beside the matrix, not a branch in the checker: the transport kind’s guarantee for each where constraint (capability::transport::GUARANTEES, three rows of four cells, the former transport_satisfies cell for cell, its words verbatim), which does not vary by target; and whether a target realizes the transport at all is the matrix’s own RemoteTransport(kind) row, asked through the snapshot’s target row (Snapshot::binding_cell)
• the bound-topic set is the rows’ projection (bound_names, bound_subjects): the or wait legality check, the role law’s bound-topic rule and the bus graph’s eligibility gate read it, and none walks bindings { } itself. An imported main’s entries are in the set, as they were in each of the walks it replaces

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · bindings_an_entry_without_its_row_is_refused_at_its_topic; total: no entry in the entry row means no bindings { } to lower

Focused tests. crates/hale-cli/tests/binding_imported_main.rs; crates/hale-codegen/tests/bindings_codec_clause.rs

Spec. spec/decisions.md F.36, F.37; spec/semantics.md § Operational constraints (Form K)

Guarded seams.

• derive_binding_rows( may be referenced from: crates/hale-types/src/binding_rows.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1
• role_from_ends( may be referenced from: crates/hale-syntax/src/desugar.rs ×2, crates/hale-types/src/binding_rows.rs ×1

Answers. How each bus subject dispatches: dynamic, static bucket or static direct, given its gates and the arrangement.

Inputs. bus_graph (its rows, keyed by wire subject: the gates, the payload_flat column among them); the stdlib’s bus rows (the logger’s log.** and its sinks: once per process, over the stdlib’s analysis copy, stdlib_bodies::bus_rows); top_scope (each topic row’s wire); placement (each site’s label; and the domains: the arrangement projection, project_arrangement, with the ownership graph’s births outside it); –no-bus-devirt

Producer. crates/hale-model/src/dispatch_plan.rs · fn from_gates

Also owned. crates/hale-model/src/dispatch_plan.rs · domain_map; crates/hale-types/src/bus_graph.rs · derive_dispatch_gates; crates/hale-types/src/stdlib_bodies.rs · bus_rows

Consumers. demand (the family’s two cells: the gates, derive_dispatch_gates, and the plan, from_gates over them, derived once per snapshot) (crates/hale-frontend/src/snapshot.rs · demand_dispatch_plan); lowering view (the snapshot’s plan, handed in: the view derives none) (crates/hale-types/src/resolved.rs · plan: &DispatchPlan); codegen (crates/hale-codegen/src/codegen.rs · build_resolved); codegen (crates/hale-codegen/src/bus/dispatch.rs · bus_devirt); exec_digest (the view’s plan, the snapshot’s) (crates/hale-cli/src/shared/options.rs · resolved.plan.digest()); model (the snapshot’s plan, handed in, held projected onto the model’s subjects and loci: Analyses::dispatch_plan) (crates/hale-types/src/model_builder.rs · projected); model dump (the model’s projection) (crates/hale-types/src/model_builder.rs · analyses.dispatch_plan)

Invariants.

• which flavour a subject gets is a plan conclusion, never a model row (spec/model.md)
• one plan per snapshot, derived once (Snapshot::demand_dispatch_plan, from_gates) over one gate set (Snapshot::demand_dispatch_gates, derive_dispatch_gates): the bus graph’s rows, each keyed by the wire subject the program lowering walks spells it with (a topic reference by its topic row’s wire, which the topic rewrite writes), followed by the stdlib’s rows, assembled into subjects by the procedure lowering’s graph uses (BusRows::subjects); a subject’s subscribers in registration order, the order the direct lowering bakes and the digest frames. The stdlib’s rows enter every program’s gates, since lowering merges the whole bundled stdlib into every program; they are derived once per process over the stdlib’s analysis copy, so neither cell builds a lowering view, and a check that builds the model pays for no merge of the stdlib
• the gates are lowering’s graph’s (lowering_bus_graph’s, the merged program’s), column for column and in its order, and so the plan is the one lowering derived for itself before it held the family’s: over the corpus examples, the lifecycle fixtures, tests/hale and the DNA mains, build and harness snapshots (545 views)
• lowering lowers the snapshot’s plan, carried on the view; the execution digest frames that plan’s digest, which covers what lowering reads (each subject, its flavor and its subscribers) and keeps a reserved 0 byte where same_domain sat, until the same-domain flavors (GH #464) lower by it
• the model holds the same plan projected (DispatchPlan::projected): the rows of the subjects its own bus sites name, by wire, each subscriber column restricted to the loci the model declares and sorted, every other column the plan’s own; so the model’s tables gain no stdlib row, shape_hash reads none of it, and the stdlib’s log.** row is the model’s only where the program names log.** itself, without the stdlib’s sinks
• the domains come from one function, domain_map, over the arrangement projection (project_arrangement, the snapshot’s Snapshot::demand_arrangement): the arranged (locus, domain) pairs minus every locus the arrangement does not fully place (a template disagreement or a birth outside it), keyed by the gates’ spelling of a locus, the raw post-merge symbol, never a display name; a stdlib locus, which the projection arranges no instance of, forfeits same_domain
• the direct tier takes all three gate legs, same-thread, quiet and the payload_flat column (bus_graph::payload_is_flat, codegen’s flatness rule over resolved types); codegen reads the flavor and refuses a plan whose column disagrees with the lowered payload, and the codec’s own flatness equals the column at every publish over the corpus

Missing data. total: no row means the subject dispatches dynamically: no static plan row names it, at its publish and its register alike

Focused tests. crates/hale-cli/tests/dispatch_plan_cli.rs; crates/hale-codegen/tests/bus_devirt_direct.rs; crates/hale-cli/tests/dispatch_payload_flat.rs (every wire payload alternative through both publish arms against the codec, the column against the codec at every publish over the corpus, the plan change recorded as a compatibility change: –dump-model’s row, a pre-change recording refused by its exec digest and admitted with –allow-unverified-model, a post-change recording replayed); crates/hale-types/tests/dispatch_gates.rs (the snapshot’s gates are lowering’s graph’s over 545 views, the stdlib’s sinks closing log.** in each); crates/hale-types/tests/dispatch_plan_projection.rs (the model holds the snapshot’s plan projected and the dump prints it: the stdlib’s log.** row lowering’s alone where the program names no log.**, a shared row without the stdlib’s sinks, a DNA main whose registration order is not the model’s); crates/hale-types/tests/dispatch_plan.rs (an_imported_seeds_loci_have_their_domains: a two-seed fixture’s imported loci have their domains, same-domain on main); crates/hale-model/src/dispatch_plan.rs (same_domain_is_no_part_of_the_digest)

Spec. spec/model.md § Derived products; spec/decisions.md F.38; spec/runtime.md § Placement classes (the dispatch plan)

Guarded seams.

• from_gates( may be referenced from: crates/hale-model/src/dispatch_plan.rs ×1, crates/hale-frontend/src/snapshot.rs ×1
• domain_map( may be referenced from: crates/hale-types/src/arrangement.rs ×1
• derive_dispatch_gates( may be referenced from: crates/hale-types/src/bus_graph.rs ×1, crates/hale-frontend/src/snapshot.rs ×1

Answers. Which on_failure handler a failing child’s locus type reaches, and from which parent.

Inputs. failure declarations; declared loci and type aliases (the bundled stdlib’s loci included); import renames; ownership (the supervising parent instance, in lowering)

Producer. crates/hale-types/src/handler_routing.rs · handler_rows

Also owned. crates/hale-types/src/handler_routing.rs · child_locus_name; crates/hale-types/src/handler_routing.rs · resolve_locus_type

Consumers. lowering view (its rows: the snapshot’s through the correspondence, then the stdlib’s, the indexes rebuilt over the union) (crates/hale-types/src/resolved.rs · lowering_handler_routing); codegen (the handler table, one fn per row keyed by the row’s site) (crates/hale-codegen/src/locus/decl.rs · handlers_of_instance); codegen (handler bodies, by the row’s site) (crates/hale-codegen/src/locus/method.rs · handlers_of_instance); codegen (concrete handler rows at locus synthesis) (crates/hale-codegen/src/codegen.rs · self.handlers.specialize); codegen (a route: the row’s handler fn) (crates/hale-codegen/src/channels/mod.rs · failure_handler_for); codegen (__parent_on_failure) (crates/hale-codegen/src/channels/mod.rs · resolve_failure_route); codegen (the params-settle bracket: whether the locus has a handler) (crates/hale-codegen/src/locus/instantiation.rs · settles_failures); codegen (restart in place) (crates/hale-codegen/src/locus/restart.rs · restarts_in_place); model (supervises, over the snapshot’s rows: demand_handlers) (crates/hale-types/src/model_builder.rs · Supervises); check (duplicate handlers, over the snapshot’s rows handed in: CheckInputs) (crates/hale-types/src/check.rs · check_duplicate_failure_handlers); check (@supervised, over the same rows) (crates/hale-types/src/frontier.rs · supervised_diags); check (a recovery event no handler applies: each row’s child and the events its ops apply, over the snapshot’s rows, beside the typed bodies’ recovery statements) (crates/hale-types/src/closure_events.rs · unreached_events); ownership births (resolved child, declaring template and identity) (crates/hale-types/src/ownership_graph.rs · identify_child)

Invariants.

• the child type is resolved once, by child_locus_name; lowering, the checker and the model read the same row
• a row carries its parent declaration’s site (parent_id) and a reader holding a locus declaration asks for its rows by that identity (handlers_of_decl, route_decl): a monomorph keeps its template’s id and selects concrete rows by that identity and its specialization name (handlers_of_instance, route_instance); lowering’s handler fn is a column of the row, held per locus keyed by the row’s site (LocusInfo::failure_handlers), and the handler table, the body pass and a route each join by that site, never by the row’s ordinal
• a row carries the site of the declaration its child resolves to (child_decl, a monomorph’s template’s, from the same resolution as child: child_locus), qualified by the store that minted it; the model’s supervision rows join parent and child to its locus table by those sites, and a child declared outside the snapshot’s programs (a stdlib locus) is SupervisedRef::External, whose written name is its display, never a join key; only a bundle no entry point minted joins by name
• the model’s failure-handler function rows are keyed by the handler’s site (handler_fn_rows), the routing row’s identity; the signature string is the row’s name, which ranks it among the function rows (two handlers are two rows whatever their signatures spell), and no reader looks a handler up by it
• a generic supervisor’s child types are substituted at synthesis by the handler producer (specialize) using the same substitution as the locus; each concrete row preserves its template handler’s site and recovery ops, resolves the concrete child’s declaration in the original bundle, and is indexed by template identity and specialization name. Dispatch, handler body layouts and restart-in-place attribution read those concrete rows; the declaration-level snapshot rows are unchanged
• the checker builds no rows: the snapshot demands them before the check (CheckInputs), and the checker’s duplicate-handler rule, the @supervised law and the model read that one build; a bundle no snapshot holds (the test entries) builds them once, in bundle_handler_rows
• a build path derives the rows once (F.40 phase 4, Q1): the snapshot’s (demand_handlers, over the checked programs, the handler_routing count), which the check, the model and the lowering view read. The view reads them as C5 folded the ownership and bus graphs (lowering_handler_routing): every user row carried across, its handler and parent sites each the merged site’s Image::Checked (a row that is not is refused, by name); the stdlib’s rows derived over the merged program’s tail only (stdlib_handler_rows, its child types resolved against the whole merged program); and the indexes, the failure column and the span-keyed bounds rebuilt over the union, the stdlib’s entered after the user’s, as the walk over the merged program entered them (the stdlib writes no recovery bound, so none of its spans, which overlap the first file’s, answers for a user statement). A carried row’s child_decl is the snapshot’s (a stdlib child SiteRef::stdlib); no lowering reader reads it, and lowering’s joins (is_row_of, handlers_of_decl, specialize, instance_key) read site indexes the merged mint kept
• the recovery statements written outside every on_failure body are no column of the rows: which child each applies its operation to is the type the checker gives its receiver, so their rows are the typed bodies’ (recoveries, the expression_typing family), recorded where the checker types the statement; the walk here reads only their for bounds. A handler’s own statements stay its row’s ops on its row’s child
• a route’s parent instance is the lowering frame’s (resolve_failure_route): a runtime pointer (the supervising parent’s, else current_self, else params_init_self), which no snapshot row holds; its handler is the row’s, and the one join in it, the supervising parent a field literal records matched to the child, is by the child’s identity as the rows key a concrete locus (HandlerRouting::instance_key: its declaration’s site, a monomorph’s with the specialization specialize registered), never by name; a declaration no mint numbered is keyed by its name (C3 rest)

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · handler_routing_a_handler_without_its_row_is_refused; total: no route means the parent declares no handler for the child, whose failure takes the unhandled route, and no handler row means the locus settles no failures

Focused tests. crates/hale-codegen/tests/lifecycle_flow.rs (on_failure_dispatch_by_child_type); tests/hale/on_failure_per_child_type_test.hl; crates/hale-types/tests/violate.rs; crates/hale-types/tests/handler_routing_probes.rs

Spec. spec/semantics.md § failure; spec/runtime.md (failure delivery)

Guarded seams.

• handler_rows( may be referenced from: crates/hale-types/src/handler_routing.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/lib.rs ×1
• child_locus_name( may be referenced from: crates/hale-types/src/handler_routing.rs ×1, crates/hale-types/src/ownership_graph.rs ×2, crates/hale-types/src/ownership.rs ×1, crates/hale-types/src/flows.rs ×1
• child_locus( may be referenced from: crates/hale-types/src/handler_routing.rs ×3
• resolve_locus_type( may be referenced from: crates/hale-types/src/handler_routing.rs ×3, crates/hale-types/src/ownership_graph.rs ×2
• DeclaredNames::of( may be referenced from: crates/hale-types/src/handler_routing.rs ×2, crates/hale-types/src/ownership_graph.rs ×1, crates/hale-types/src/ownership.rs ×1, crates/hale-types/src/flows.rs ×1
• stdlib_handler_rows( may be referenced from: crates/hale-types/src/handler_routing.rs ×1, crates/hale-types/src/resolved.rs ×1
• lowering_handler_routing( may be referenced from: crates/hale-types/src/handler_routing.rs ×1, crates/hale-types/src/resolved.rs ×1

Answers. Which children are flows (released per completion) and which are resident; and, per locus declaration, whether its run() is long-running and whether it never returns.

Inputs. release declarations; accept declarations; run bodies; declared loci and type aliases (handler_routing’s resolver); import renames

Producer. crates/hale-types/src/flows.rs · survey

Consumers. check –flows (each flow type as written, with its clauses: the snapshot’s rows) (crates/hale-cli/src/verbs/check/run_impl.rs · demand_flows); check (a daemon-shaped locus that accepts a child type it releases no clause for: a law over the rows) (crates/hale-types/src/check.rs · check_accept_release); check (the run rows: the long-running-child rule’s long-running column, the starvation and birth-order laws’ never-returns column; the snapshot’s rows handed in, CheckInputs::flows, shared by all four) (crates/hale-types/src/check.rs · run_of); lowering view (the snapshot’s rows, handed in: lowering reads them by locus name, so they need no correspondence) (crates/hale-types/src/resolved.rs · let flows = flows.clone()); a declaration’s dependents (X2: a flow child and its release owners are neighbours, Snapshot::declaration_dependents) (crates/hale-frontend/src/snapshot.rs · fn dependency_index); the lifecycle plan (an accepted flow is torn down by the reclaim its run’s end runs, a resident by its owner’s cascade: the snapshot’s rows over the checked programs) (crates/hale-frontend/src/snapshot.rs · fn demand_lifecycle); codegen (run elision, run-end reclaim and the release call: Cx::is_flow, one row read) (crates/hale-codegen/src/codegen.rs · is_flow); codegen (the generic-instantiation queue: each locus specialization it creates asks the row for its template’s clauses, under the substitution its synthesis applies) (crates/hale-codegen/src/codegen.rs · specialize()

Invariants.

• pool starvation and the birth-order trap are registered rules run as law::Laws over the run rows’ columns and the placement table’s rows for the deployed root (RootRunRows), their findings law::Violations (phase 4, W5)
• a release clause’s child is resolved once, by child_locus_name (handler_routing’s resolver: aliases, generic instantiations, qualified paths), into the row (FlowClause::locus); lowering’s flow-ness is a row read (flows::is_flow), never a comparison of its own
• the flow facts cover the specializations lowering creates: a clause whose type mentions its owner’s type parameters names no locus by itself and carries its template (FlowClause::template: the owner’s identity, its parameters in order, the type as written); FlowRows::specialize answers for one specialization by resolving the template’s type under the substitution lowering’s synthesis applied, so Manager<Worker>’s release(c: T) makes Worker a flow exactly as a concrete release(c: Worker) does
• the checker’s accept/release rule judges over the rows: the release clauses a locus declares are the rows’ clauses inside its declaration
• every locus declaration, a module’s included, has a run row (RunRow: the declaration’s name and span, which FlowRows::run_of finds it by, and two columns, long-running and never-returns, the nonreturning family’s two definitions); the checker surveys no rows: its four readers share the snapshot’s, handed in (CheckInputs::flows)
• one survey per snapshot (F.40 phase 4, Q1): flows is a counted family (Snapshot::demand_flows, over the checked programs), and the check, the lifecycle plan, the lowering view, the editor’s dependents relation and check --flows read that one. The view needs no correspondence: lowering reads the rows by locus name (is_flow, specialize), the stdlib declares no release clause and no type alias, and the resolver’s declared loci hold the stdlib’s over either program, so the merged program’s survey was the checked one’s in every clause row; its run rows for the stdlib’s loci have no lowering reader. A bundle no snapshot holds (check::check_bundle, the tests’ scope-taking check) surveys for itself

Missing data. total: no row means the child is resident: no release clause names it, so its owner’s cascade tears it down (Cx::is_flow)

Focused tests. crates/hale-codegen/tests/release_reclaims_flow.rs; crates/hale-codegen/tests/release_two_parents.rs; crates/hale-codegen/tests/release_generic_owner.rs; tests/hale/release_generic_owner_test.hl; crates/hale-types/src/flows.rs (a_clause_names_the_locus_lowering_names, a_template_clause_names_the_specialization_s_argument); crates/hale-types/tests/demand_gate.rs (a_build_surveys_the_flows_once_and_lowering_reads_that_survey)

Spec. spec/semantics.md § release(c) and flow children

Guarded seams.

• flows::survey( may be referenced from: crates/hale-types/src/lib.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/lifecycle/derive.rs ×1

Answers. Which loci declare restart operations, which restart in place, and what the restart bound is.

Inputs. closure and birth-check declarations; handler_routing (the rows’ recovery ops)

Producer. crates/hale-types/src/handler_routing.rs · handler_rows

Also owned. crates/hale-types/src/handler_routing.rs · recovery_ops

Consumers. codegen (which loci get restart points: _restart, _resume) (crates/hale-codegen/src/locus/restart.rs · can_fail); codegen (the for N retry bound) (crates/hale-codegen/src/codegen.rs · retry_bound_at); codegen (_restart, _resume); model

Invariants.

• a recovery op is a row with a witness, per (parent, child)
• every for bound a recovery statement writes is an entry of the rows, keyed by the statement’s span (HandlerRouting::retry_bound_at): a literal is its value, any other expression the site of the expression written there, which lowering lowers once where the statement runs. The model’s retry_bound is the last literal of a handler’s entries, so the bound modelled and the bound lowered are one fact
• which loci a failure can originate in (a closure of any epoch, inline ones and so every violate included, or a birth_check) is a column of the rows per locus declaration (HandlerRouting::can_fail), over the merged program lowering walks; lowering emits restart points exactly where it answers yes. A monomorph is no declaration and is not in the column, so a generic locus that declares a closure gets no restart points (known open)

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · restart_a_bound_without_its_row_is_refused_at_the_statement; total: no row in the failure column means no failure can originate in the locus, so it gets no restart points (can_fail; a monomorph is no declaration and is in no column, known open), and no handler restarting it in place means none does

Focused tests. crates/hale-codegen/tests/restart_in_place_params.rs; crates/hale-codegen/tests/restart_bound.rs; crates/hale-types/tests/handler_routing_probes.rs (the failure column, the bounds); crates/hale-codegen/tests/restart_spine_ir.rs

Spec. spec/semantics.md § supervision

Guarded seams.

• recovery_ops( may be referenced from: crates/hale-types/src/handler_routing.rs ×2
• can_fail( may be referenced from: crates/hale-types/src/handler_routing.rs ×1, crates/hale-codegen/src/locus/restart.rs ×1
• retry_bound_at( may be referenced from: crates/hale-types/src/handler_routing.rs ×1, crates/hale-codegen/src/codegen.rs ×1

Answers. Whether each closure’s recovery-event clauses (persists_through, resets_on) are well formed and can take effect: every name in the closed alphabet, dissolve never persisted through, no event in both clauses, every event one a recovery of the closed world applies to the locus, and a persistence with something to keep.

Inputs. closure declarations (each clause’s names as the parser typed them: RecoveryEvents); handler_routing (each handler’s child and the events its ops apply); expression_typing (the typed bodies’ recoveries: each recovery statement outside the handlers, with the locus the checker typed its receiver as); entrypoint (whether the world is closed, as rule 9 asks)

Producer. crates/hale-types/src/closure_events.rs · closure_event_rows

Also owned. crates/hale-types/src/closure_events.rs · closure_event_laws; crates/hale-types/src/closure_events.rs · unreached_event_laws; crates/hale-types/src/closure_events.rs · outside_the_alphabet; crates/hale-types/src/closure_events.rs · persists_through_dissolve; crates/hale-types/src/closure_events.rs · in_both_clauses; crates/hale-types/src/closure_events.rs · unreached_events; crates/hale-types/src/closure_events.rs · nothing_to_keep

Consumers. check (the four laws over the clause rows alone, through one entry) (crates/hale-types/src/check.rs · closure_event_laws); check, verify, build, run, test, replay, bench, the LSP (the reach law, with the typing diagnostics, beside the bare_fallible law: over the snapshot’s handler rows, entry row and whole typed-body table) (crates/hale-frontend/src/snapshot.rs · unreached_event_laws); the check of a bundle no snapshot holds (the reach law over the table packaged from the typing’s record) (crates/hale-types/src/check.rs · unreached_event_laws); codegen (the accumulator reset: each closure’s typed persists_through events, compared as RecoveryEvents with the event a recovery statement lowers) (crates/hale-codegen/src/locus/decl.rs · persists_through)

Invariants.

• a recovery event is typed once, by the parser (parse_recovery_event_name): a RecoveryEventName keeps the name as written, with its span, and the RecoveryEvent it is when it is in the closed alphabet (restart, restart_in_place, quarantine); a name outside the alphabet is kept for the check to refuse, never a parse error; the clause carries its own span
• lowering compares no string: the per-closure persistence map holds RecoveryEvents (ClosureDecl::persists_through), and each recovery statement zeroes the accumulators of every closure that does not persist through its event (a spent restart(c) for N bound is quarantine). Nothing reads resets_on at run time: it states that default, and the laws hold it
• the laws are registered rules of spec/verification.md’s structural table, each a function over the clause rows producing law::Violations: the four over the clause rows alone run by the check through closure_event_laws, the reach law through unreached_event_laws over the whole typed-body table (a typing that reused a declaration holds no record of its bodies, so it never reads the check’s record); the errors (a name outside the alphabet, dissolve persisted through, an event in both clauses) for every locus the bundle declares; the warnings (an unreached event, a persistence with nothing to keep) for the loci of the program’s own seed only
• whether a recovery reaches a locus is read from the handler rows (a handler’s ops on its child, by the declaration the child resolves to) and from the typed bodies’ recoveries (a recovery statement outside handlers on the locus the checker typed its receiver as, by declaration: a param, a local, a field of another value, a call’s result alike; a generic body’s per specialization, whose rows name the statement in place of the template walk’s), never from the lifecycle plan, where one flag covers both restarts, quarantine has no obligation, and no check may build the plan. The world is closed as rule 9 asks (the entry row has an entry); an event some recovery applies to a child no row names (a generic supervisor’s handler’s type parameter, a receiver the checker typed as no locus: a value of a type parameter in a body no specialization was walked for) is not judged

Missing data. total: no persisted event means the closure persists through none: its accumulators are zeroed at every recovery event, the default resets_on states (emit_accumulator_reset_for_event)

Focused tests. crates/hale-types/tests/closure_events.rs; crates/hale-syntax/tests/closure_recovery_events.rs; crates/hale-codegen/tests/closure_recovery_events.rs (the reset at run time: default, resets_on, persists_through); crates/hale-types/tests/handler_routing_probes.rs (the recovery statements’ typed rows); crates/hale-codegen/tests/closure_resets_per_epoch.rs; crates/hale-types/tests/violate.rs

Spec. spec/semantics.md § Recovery events; spec/verification.md § Structural & design rules; spec/runtime.md § Closure-test infrastructure (recovery-event interaction)

Guarded seams.

• closure_event_rows( may be referenced from: crates/hale-types/src/closure_events.rs ×2
• closure_event_laws( may be referenced from: crates/hale-types/src/closure_events.rs ×1, crates/hale-types/src/check.rs ×1
• unreached_event_laws( may be referenced from: crates/hale-types/src/closure_events.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1

Answers. The role vocabulary: every role declaration of the bundle, with its includes, which a surface row’s requires and a hub binding’s requires: name.

Inputs. role declarations

Producer. crates/hale-types/src/roles.rs · role_rows

Also owned. crates/hale-types/src/roles.rs · role_rows; crates/hale-types/src/roles.rs · role_laws; crates/hale-frontend/src/snapshot.rs · demand_role_rows

Consumers. check –matrix (the roles an environment maps: the pair’s snapshot’s role rows, RoleRows::declared_roles, read once the pair’s check has demanded them, not gated on the typing; a pair the check refuses has no snapshot and is reported by its refusal alone, with no role coverage) (crates/hale-cli/src/verbs/check/matrix.rs · demand_role_rows); check (the three role rules, a law over the role rows, CheckInputs::roles) (crates/hale-types/src/check.rs · role_laws); check (the surface laws: a row’s requires names a declared role, law 4) (crates/hale-types/src/surfaces.rs · surface_laws)

Invariants.

• form, not params (I1): the vocabulary names what the program is, never where one copy listens
• perspective-invariant (I5)
• the role rows have one producer (F.40 phase 4, A4; R4: roles::role_rows), over the programs after the sequence, demanded once per snapshot (Snapshot::demand_role_rows, the role_rows count), not gated on the typing; a bundle no snapshot holds builds its own. Their columns: each role declaration (RoleDeclRow: the name and its span, each includes with its span, the declaration’s span and site), two declarations of one name kept as two rows. No implicit role joins them: owner is a role only a program that declares it has.
• the three role rules are registered rules (rows of spec/verification.md’s structural table) whose findings are law::Violations, one walk judging the three and reporting them in the order it reaches them (law::diags), a related location a finding carried being its witness step (phase 4, W5)
• the roles an environment maps are a projection of the rows (RoleRows::declared_roles, vocabulary), held equal to an independent walk of the declarations over the corpus, tests/hale and the DNA seeds

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-types/tests/api_binding_check.rs; crates/hale-types/tests/role_rows.rs

Spec. spec/api.md § Surfaces and their rows; spec/types.md § Roles

Answers. The program’s API as rows (GH #1417): one surface row per rpc line of an api block or @rpc handler (the surface, the member Locus::fn, the request, response and error types with their contract shape hashes, whether a failure is the server error, the pools the handler’s locus runs on, the required roles), each surface’s contract digest, each serve site’s exposure (its surface, transport instance, as: name, sources and receivers), and each hub binding’s stream row; R1 produces the rows and digests and names the serve sites and hub bindings for the description, R2 checks and serves the sites, R5 the hubs, and the family replaces api_surface at R4.

Inputs. api blocks and @rpc handlers (the parse: TopDecl::Api, FnDecl::rpc); the locus declarations the rows name (their member fns, lifecycle methods, modes and failure handlers); the contract shapes (topic_identity::Shapes, the shape hashes the digest folds); placement (the pools the handlers’ loci and the receivers run on); topics (a hub stream’s wire subject); serve sites: api::serve(…) and its named arguments (R1 names them for the description; R2a checks them, the five laws, and builds each one’s exposure); topic bindings to a hub with requires:, bound: and on_full:, and the ws::Hub literal they name (R5)

Producer. crates/hale-types/src/surfaces.rs · surface_rows

Also owned. crates/hale-types/src/surfaces.rs · surface_rows; crates/hale-types/src/surfaces.rs · select_members; crates/hale-types/src/surfaces.rs · surface_laws; crates/hale-frontend/src/snapshot.rs · demand_surface_rows

Consumers. check (the admission law over the rows: laws 1 to 5 and 7 of spec/api.md, beside the may-violate law, CheckInputs::surfaces) (crates/hale-types/src/check.rs · surface_laws); check (the snapshot’s check stage: the same laws over the snapshot’s rows) (crates/hale-frontend/src/snapshot.rs · surface_laws); check (the laws of a serve site: an exposure named once, every receiver type bound, a receiver that outlives its exposure, a bound type the rows name, a stated queue, no serve site in a main locus the program imports and builds) (crates/hale-types/src/check.rs · serve_laws); check (the snapshot’s check stage: the serve-site laws over the snapshot’s rows) (crates/hale-frontend/src/snapshot.rs · serve_laws); the model (the surfaces and surface_rows tables, projected; the digest law) (crates/hale-types/src/model_builder.rs · inputs.surfaces); build (a hub binding the expansion could not serve, and a serve site over a transport this compiler does not ship, are refused) (crates/hale-types/src/lib.rs · unserved_sites); check –api (the inventory; one exposure’s description for a caller holding --holds under its role source; law 6’s notes on stderr) (crates/hale-cli/src/verbs/check/run_impl.rs · api_document); the OpenAPI, JSON Schema and MCP forms of one surface (check --api --surface), projections of its rows (crates/hale-types/src/surface_doc.rs · openapi); api export (R8a: a surface’s bundle, its description, OpenAPI, JSON Schema, MCP and digest files, generated from its rows and checkable against a committed copy; hale api export) (crates/hale-types/src/surface_doc.rs · surface_description); api client (R8a: a typed client of one surface in Hale or TypeScript, generated from its rows and held current by --check; hale api client, crates/hale-cli/src/api_gen/) (crates/hale-types/src/surface_doc.rs · client_model); serve (R2a: a serve site’s exposure, its rows adapter, its receivers’ plumbing and the codecs of what the rows carry, written before the check by the desugar sequence) (crates/hale-types/src/rpc_expand.rs · expand); serve (R2a: lowering reads the call as its exposure’s handle, a read of the serving locus’s param the expansion wrote; it reads no row); serve (the runtime’s dispatch over a socket: Context, the digest check, requires before enqueue, decode by shape, R2b and R3); hubs (R5: a topic bound to a hub: the hub’s literal made the standard library’s, its listener, one adapter binding and JSON codec per stream row, the rows adapter and the description’s pieces, written before the check by the desugar sequence) (crates/hale-types/src/hub_expand.rs · expand); hubs (the runtime, api_hub.hl: admission against the row’s requires, delivery from a queue of bound frames under on_full, expiry and revocation, closed at stop(), R5); describe / call / watch / admin / mcp –app (R4 C: each reads the exposure’s description, {"describe": true} or GET /.description, and speaks the R0 wire; crates/hale-cli/src/api_client.rs, mcp.rs); ui (reserved)

Invariants.

• one row family for both spellings: an api block’s rpc line and an @rpc handler produce the same row, and nothing else about the locus is read
• the digest is the FNV-1a fold of the rows in canonical order (member, request, response and error shape hashes, sorted requires) and excludes the listener, the receivers, the serve site, the surface’s name, the build identity and the incarnation
• a row whose error type is ClosureViolation (a handler that may violate, fallible(ClosureViolation) under F.42 with no exemption) fails as the server error and its description carries no error schema; a row with any other error type fails as the handler error with that type’s schema; the digest’s error slot folds ClosureViolation’s shape hash like any error type’s
• a hub that serves no surface is an exposure of its stream rows, identified hub@<stream digest>/<name>; the stream digest is the FNV-1a fold of the stream rows sorted by topic (topic, payload shape hash, direction, codec, bound, on_full, replay, sorted requires) and excludes the listener, the hub’s name and sources, the build identity and the incarnation; its description has no surface and no member, and its outcome form is the ws frames
• a topic bound to a hub is a stream: the binding is one row of the hub (topic, payload shape, direction, codec, bound, on_full, no replay, requires) and joins the bus graph as an adapter binding, so the publish contract and the no-subscriber lint read it as bound outward; a stream’s on_full is drop_old or drop_new, never refuse; a subscription is admitted against the row’s requires from the Context established at connect (over UDP, by the credential on the subscribe datagram, every datagram of a subscriber carrying the id it chose), its queue holds at most bound frames and every event offered to it takes the next seq, delivered or shed; it ends, with one unauthorized frame and its buffer dropped, at the credential’s expiry and at a role-source revision its requires no longer holds under, and nothing is delivered under an authorization older than the revision or past the expiry
• authorization is evaluated before enqueue: a refused request never reaches the handler’s queue
• descriptions read the rows dispatch reads: a caller’s description under an exposure lists exactly the members whose requires that exposure’s role source grants it
• grants belong to the role-source instance a serve site names, never to a role name
• the outcome mappings are fixed per transport (v1): no row carries a status and the digest hashes none
• the rows have one producer (surfaces::surface_rows), demanded once per snapshot (Snapshot::demand_surface_rows, the surface count), not gated on the typing; a bundle no snapshot holds builds its own in the check’s entry. Its columns: each row’s surface, member (the locus in the row author’s spelling), the locus and fn it resolves to, the roles as written with their spans, and what the handler resolves to (a member fn with its key, its value parameters past a trailing ctx: std::api::Context, the request, response and error types, whether the error is ClosureViolation, the pools; or no locus, no fn, a lifecycle method, mode or failure handler, a free fn); an @rpc row feeds the seed’s default surface, named after the seed (an imported seed’s by its import alias); which member belongs to which surface is selected once (surfaces::select_members, by names alone), and surface_rows (which types and hashes the selection) and the @rpc adapter (rpc_expand, which expands it) both call it
• the admission law is a law over the rows (surfaces::surface_laws), in spec/api.md’s wordings: a row names a handler (1), takes one request (2), is its surface’s member once (3), requires declared roles (4), names types the JSON codec carries (5: an identity, a range, a quantity and the four scalars; a point is refused), and a handler that may violate is fallible(ClosureViolation) whatever it returns (7, F.42’s may-violate judgment over the summary); law 6 is a statement of the row (server_error_notes), not a refusal
• the serve-site laws are a law over the same rows and the serving locus’s params (surfaces::serve_laws), in spec/api.md’s wordings, and the exposure a site builds is the desugar sequence’s (rpc_expand::expand, before the check): it reads the surface’s rows and digest, the site’s named arguments, the transport’s principals: and roles:, and the serving locus’s params, and writes the exposure param, the rows adapter, the receivers’ plumbing (a number per exposure, written into the literals that build the instance; an incarnation stamp; the keyed call and hello subscriptions; the thunk that runs a call through the fallible ABI) and the five __api.rpc.* topics; the check reads the call as written and lowering reads the param
• the model holds the surfaces and their rows under one law: each surface’s digest is the fold of its own rows; neither table enters shape_hash, so a program with no surface hashes as it did
• a type’s contract shape is topic_identity::Shapes’ contract form, which agrees with the payload contract’s observation form on every flat struct (spec/model.md § The shape of a type)

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-cli/tests/api_contract_fixtures.rs; crates/hale-types/tests/api_hub_check.rs (one refusal per law of a hub binding in its wording, the binding admitted by the check and the build); crates/hale-codegen/tests/api_hub.rs (a publish reaches the hub once each, the address bound in the program’s birth, a stopped hub releases it); crates/hale-codegen/tests/api_hub_streams.rs (the witness’s stream half over sockets: admission and its refusals, delivery with increasing seq, revocation with nothing delivered after, expiry at its instant, closed at stop(), the served description against the fixtures, ASan); crates/hale-codegen/tests/api_hub_desk.rs (drop_old and drop_new shedding with the seq gap, rpcs on a subscriber’s connection, ASan); crates/hale-codegen/tests/api_hub_udp.rs (the stream half over datagrams: the id every datagram carries, admission and its refusals, revocation, expiry, unsubscribe, closed, the description by datagram); crates/hale-types/tests/api_rows_check.rs (one refusal per law in its wording, law 6’s statement, the fixture admitted); crates/hale-types/tests/surface_rows.rs (the fixture’s rows, digests and model rows; an @rpc row and an rpc line are one row); crates/hale-syntax/tests/api_surface_parse.rs (both spellings, the serve site, the hub binding, the refusals); crates/hale-model/src/surface.rs (the digest framings against digest.md)

Spec. spec/api.md; spec/api-description.schema.json; spec/model.md § The shape of a type

Guarded seams.

• surface_rows( may be referenced from: crates/hale-types/src/surfaces.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1
• select_members( may be referenced from: crates/hale-types/src/surfaces.rs ×3, crates/hale-types/src/rpc_expand.rs ×1
• surface_laws( may be referenced from: crates/hale-types/src/surfaces.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1
• serve_laws( may be referenced from: crates/hale-types/src/surfaces.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1

Answers. Which loci confine their state (@sealed), and which could.

Inputs. expression_typing (the typed bodies’ param_accesses column); top_scope (whether a receiver is sealed, and the methods it declares); locus declarations (the survey’s loci)

Producer. crates/hale-types/src/check.rs · record_param_access

Also owned. crates/hale-types/src/sealed_access.rs · sealed_access_law; crates/hale-types/src/sealed_access.rs · outside_access; crates/hale-types/src/sealability.rs · survey

Consumers. check (the sealed rule, a law over the rows, run as each top-level declaration’s walk ends, and once more after the walks per monomorph: each finding placed where the walk first reached the access, one per access however many evaluation paths or specializations reach it, and a default’s once per check however many declarations evaluate it) (crates/hale-types/src/check.rs · settle_param_accesses); check –sealable (the survey, a group-by over the snapshot’s rows: demand_typed_bodies) (crates/hale-cli/src/verbs/check/run_impl.rs · sealability::survey); claims (require sealed: the declaration’s sealed, not the rows)

Invariants.

• a diagnostic’s wording is never an input to a derivation
• the rows are the checker’s (F.40 phase 4, W4): one ParamAccess per read or write of a locus’s params field through a receiver the checker typed as that locus, recorded where it types the access (the field-read arm, an assignment target’s field segment), sealed or not, before any rule judges it: the reader (the locus whose member is walked, None in a free fn) and the receiver by declaration (LocusRef: the minting universe and the id, a std:: locus being the stdlib copy’s), the receiver’s scope name, the param, read or write, the span, the evaluation path it was typed on (ParamAccess::evaluation, a conversion’s path: empty outside a default) and the specialization (ParamAccess::specialization, the monomorph’s type arguments: empty on the ordinary walk). An access through self in the locus’s own members is a row whose reader is the receiver; a method or a capacity slot named on a locus is none; a receiver typed as a monomorph (Box_Int), which the scope declares no locus by, is resolved through the monomorph table to its template, and the row names the template
• a walk whose findings the check discards discards its accesses with them (walk_mark / discard_since): a receiver typed ahead of the call path that types it again. A generic body walked per monomorph keeps its accesses (keep_visits), a row per specialization in the template member’s body, settled once after the walks: an access through a value of a parameter type (self.inner.key, inner: T) reaches a locus only there, and is refused once however many monomorphs reach it. A fn param default is typed only at its invocations, and that walk keeps its accesses (keep_visits): a row per evaluation path, in the caller’s body with the caller’s reader, at the default (not on a type declaration’s walk of its fields’ calls, which is no evaluation). An access the walk reaches twice on one path is one row
• the sealed rule is a filter over the rows (sealed_access::outside_access, a registered law on the law type, no witness): a row whose receiver the scope says is @sealed and whose reader is not the receiver, rendered with the author’s spelling of the locus (std::secret::Signer for a stdlib locus) and the methods it declares; it decides nothing at the access
• the --sealable survey is a query over the same rows of the check the command ran, imports resolved: per locus the programs declare (a module’s included), the rows reaching it from outside its own members are its blockers, a locus with none is free; it re-checks nothing, so it agrees with the rule by construction

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-types/tests/sealed_locus.rs; crates/hale-types/tests/typed_bodies.rs (the_param_access_column_records_each_access_through_a_locus); crates/hale-types/tests/sealability_survey.rs; crates/hale-types/tests/sealable_survey_correction.rs

Spec. spec/verification.md § Secrets — confine, classify, claim; spec/verification.md § Structural & design rules; spec/projects.md (hale check --sealable)

Guarded seams.

• sealed_access_law( may be referenced from: crates/hale-types/src/sealed_access.rs ×1, crates/hale-types/src/check.rs ×1
• sealability::survey( may be referenced from: crates/hale-cli/src/verbs/check/run_impl.rs ×1

Answers. On whose authority a locus runs: the relation runs_under(locus, principal), with principals declared by the program.

Inputs. principal declarations (a later dialect); ownership (an undeclared locus inherits its owner’s principal)

Producer. none: reserved, computes nothing.

Consumers. claims (only reaches(effects(secret(..))) via { runs_under(P) }); placement (policy projections per principal); dna (positions instantiate principals)

Invariants.

• static, like ownership; a locus cannot run under a principal its owner does not hold
• the column is reserved so the tower’s table never changes twice

Missing data. n/a

Spec. RFC #1212, the authority comment

Answers. For an evented locus: the transition each handler is, input event to output set (F.41, after phase 2).

Inputs. @evented declarations; handler signatures

Producer. none: reserved, computes nothing.

Consumers. bus_graph (exact cycles); effects (rate bounds); lifecycle_order (finite products); replay

Invariants.

• at most one output per delivery, as a type; fan-out as self-events

Missing data. n/a

Spec. RFC #1212 §6 (F.41 sketch)

Answers. Which effect classes each fn and locus reaches (the callgraph fixpoint), the declared classes and their causes:/depends: DAG, and the certificate relating the two.

Inputs. effect annotations; the callgraph; stdlib_surface (leaf effects); effect_class_table; ffi names

Producer. crates/hale-types/src/effect_rows.rs · derive_effect_rows

Also owned. crates/hale-types/src/frontier.rs · infer_effects; crates/hale-types/src/frontier.rs · infer_effect_bounds; crates/hale-types/src/purity.rs · infer_purity_for_bundle; crates/hale-types/src/effect_rows.rs · EffectRows; crates/hale-types/src/evidence.rs · derive_certificate_evidence; crates/hale-types/src/evidence.rs · derive_certificate_evidence_over

Consumers. check (crates/hale-types/src/check.rs · check_decorator_stacks); claims (certificate, causes, depends, budget); the certificate evidence (the check’s effects certificate report, read by the check’s laws and the artifact’s) (crates/hale-frontend/src/snapshot.rs · demand_effect_certificates); check (a codec binding’s purity assertion reads the purity column, demanding the rows only when a codec reaches it) (crates/hale-types/src/check.rs · CheckInputs); check (the blocking warning: which helpers hold a cooperative worker, the BLOCK class with its leaves and resolved targets, demanding the rows only once a placed field has a run() to walk) (crates/hale-types/src/check.rs · worker_holding_fns); model (effect labels, lower bounds and direct contributions, the last read by the reachability judgment’s effects(C) test, and the summary the rows’ walk read: the snapshot’s rows, handed in) (crates/hale-types/src/model_builder.rs · ModelInputs); the effects manifest (--dump-effects-manifest, --check-effects-manifest: the snapshot’s rows, cross-seed calls resolved through the renames) (crates/hale-cli/src/verbs/check/run_impl.rs · demand_effects); replay (the live-effects gate reads the manifest over the snapshot’s rows, and refuses when they are blocked) (crates/hale-cli/src/verbs/replay.rs · demand_effects); doc

Invariants.

• derived ⊆ declared is the certificate; budgets are judged through evidence (spec/verification.md)
• effects run once per snapshot, not once per consumer: Snapshot::demand_effects runs derive_effect_rows once over the snapshot’s allocation summary (demand_alloc_summary: the checked programs and the stdlib’s analysis copy, cross-seed calls resolved through the import renames), counted as effects, blocked with the scope
• an unresolved edge is coverage, never a violation: a row’s effects saturates to UNCLASSIFIED when the walk reaches what it cannot name, its known set is the lower bound an unresolved edge never erases, and unknown says the walk reached such an edge
• an indirect call is one rule for every certificate and budget reader: a call through a function value the summary resolves (the alloc_summary family’s function-value rule) is its alternatives, each judged as the call of that fn, and one it does not resolve (CallEdge::indirect: a function-typed parameter, an unfollowed local or a computed callee no function value of the program can be) is a call that may do anything, never a call to nothing: the effects engine and the rows read it as UNCLASSIFIED, @budget and the quantitative dimensions as unbounded, the model as an IndirectCall hole, so every certificate over it is refused or uncertified (a classified correction, F.40 E5: a call through an unresolved local was a call to nothing, pinned in indirect_calls.rs)
• a row is keyed by its declaration’s identity (FnKey::decl, the snapshot_identity family’s site), its (locus, fn) name kept as the display
• a fn’s direct contribution is a column (direct; EffectRows::direct answers any key, a bodyless one by what it carries): the model’s function rows and absorbed paths, which the reachability judgment’s effects(C) destination test reads, take it from the rows, and nothing outside the producer folds a body for it
• purity and the lower bound are columns of the rows: one walk answers a fn’s saturating set and its lower bound (infer_effect_bounds), and the purity walk runs only inside the producer; which stdlib calls make a fn impure is the stdlib surface table’s (is_impure_stdlib reads effects_for: a public row carrying syscall, block or publish), the hand list it replaced (IMPURE_STDLIB_PATHS) having omitted syscall rows (among them tcp connect, connect_wait, accept_one, listen_socket and fs mkdir, rename, unlink) and named paths with no public row, so a codec calling tcp::connect was pure (a classified correction, pinned in bindings_codec_clause.rs); the checker’s codec law reads the purity column through CheckInputs::effects, a demand made only when a codec binding reaches the assertion, and the blocking check its BLOCK class, a demand made only once a placement entry puts a field with a run() on a classic pool or main, so a check of a program that does neither runs no effects fixpoint
• the effects certificate engine runs once per snapshot, in the check (check_bundle_reporting); the certificate evidence reads that report (Snapshot::demand_effect_certificates, handed to derive_certificate_evidence_over) and never runs the engine itself

Missing data. an unknown is a hole with a stated policy

Focused tests. crates/hale-types/tests/effect_assertions.rs; crates/hale-types/tests/effects_cross_seed_correction.rs; crates/hale-types/tests/indirect_calls.rs; crates/hale-cli/tests/effects_baseline_gate.rs; crates/hale-cli/tests/effects_manifest.rs

Spec. spec/verification.md § Default-on & opt-in analyses; spec/verification.md § Claims

Guarded seams.

• infer_effects( may be referenced from: crates/hale-types/src/frontier.rs ×4, crates/hale-types/src/claims.rs ×1, crates/hale-types/src/topology.rs ×1
• effect_manifest_with_inference( may be referenced from: crates/hale-types/src/effects.rs ×1, crates/hale-types/src/lib.rs ×1, crates/hale-cli/src/verbs/replay.rs ×1
• infer_purity_for_bundle( may be referenced from: crates/hale-types/src/purity.rs ×2, crates/hale-types/src/effect_rows.rs ×1
• infer_effect_bounds( may be referenced from: crates/hale-types/src/frontier.rs ×2, crates/hale-types/src/effect_rows.rs ×1
• direct_effects( may be referenced from: crates/hale-types/src/effect_rows.rs ×2
• effect_report_grouped( may be referenced from: crates/hale-types/src/effects.rs ×2, crates/hale-types/src/check.rs ×1
• derive_certificate_evidence( may be referenced from: crates/hale-types/src/evidence.rs ×1
• derive_certificate_evidence_over( may be referenced from: crates/hale-types/src/evidence.rs ×2, crates/hale-types/src/judgment.rs ×1, crates/hale-types/src/topology.rs ×1

Answers. Which fns block (a cooperative worker would be held), and whether the program places anything off the main thread.

Inputs. stdlib_surface (holds_cooperative_worker); effects (the rows’ BLOCK class, their resolved targets and unresolved leaves); placement (the table’s domains); bindings (the program’s own main’s entries)

Producer. crates/hale-types/src/check.rs · blocking_path_match

Also owned. crates/hale-types/src/check.rs · worker_holding_fns; crates/hale-types/src/placement.rs · places_off_main; crates/hale-types/src/binding_rows.rs · binds_on_main

Consumers. check (rules 7, 8); effects (@no_block); codegen (mark_pinned, no_pinned dispatch: program_has_offthread over the view’s placement table and binding rows) (crates/hale-codegen/src/codegen.rs · program_has_offthread)

Invariants.

• one leaf set (GH #830) and one propagation
• rules 7 and 8 are judged by one walk over the deployed root’s placed fields (check_cooperative_pool_blocking), which reports each finding as a law::Violation of its rule in the order it reaches them and hands the starvation law the pools rule 7 fired on (phase 4, W5)
• whether a thread crosses the bus boundary is read off rows, once, in lowering (program_has_offthread): a domain of the placement table that is not main (PlacementTable::places_off_main: a pinned anchor, a non-main pool, an adapter binding’s thread, the api binding’s synthesized pool) or an entry of the entry’s bindings { } (BindingRows::binds_on_main: the rows of the locus the entry row names, by its site, as lowering’s prelude lowers them); the lotus_bus_mark_pinned call and every static dispatch’s no_pinned flag are that one value and its negation
• an imported library’s main locus is never deployed, so its placement { } block places nothing and its bindings { } bind nothing: a program importing one is not off-thread for it (a classified correction, pinned in offthread_imported_main.rs); the entry’s binding makes its program off-thread, and a module-nested main, which the old binding term (top-level items only) missed, is no longer deployed: as a seed’s only main locus it is refused (L4)
• the helpers that block are the effect rows’ (worker_holding_fns, demanded through CheckInputs::effects only once a placed field has a run() to walk): a fn whose direct BLOCK comes from a leaf holds_cooperative_worker names (the BLOCK class includes std::time::sleep, which yields the worker, so the leaf test stays beside the row), closed over the rows’ resolved targets; the check folds no call graph of its own
• the rule’s horizon: the rows’ propagation sees what the old name-keyed walk did not (a qualified cross-seed call, a stdlib body behind a handle method, another locus’s method), but the run() walk consults the set only at a bare call or a self.m() call, so the horizon decides what a helper reaches and never which call in run() is looked at; the rule’s diagnostics over the corpus, tests/hale and the DNA seeds are the old walk’s (spec/verification.md § Concurrency & placement safety)

Missing data. total: no domain off main and no binding row of the entry means no thread crosses the bus boundary (program_has_offthread)

Focused tests. crates/hale-types/tests/placement.rs; crates/hale-codegen/tests/bus_devirt_no_pinned.rs; crates/hale-types/tests/checks_inside_modules.rs; crates/hale-cli/tests/offthread_imported_main.rs

Spec. spec/semantics.md rules 7, 8; spec/verification.md § Concurrency & placement safety; spec/semantics.md § The entry locus

Guarded seams.

• places_off_main( may be referenced from: crates/hale-types/src/placement.rs ×1, crates/hale-codegen/src/codegen.rs ×1
• binds_on_main( may be referenced from: crates/hale-types/src/binding_rows.rs ×1, crates/hale-codegen/src/codegen.rs ×1

Answers. Where each allocation lands and when it is reclaimed: per-fn allocation, escape, scratch eligibility, method-scratch elision, stack arrays, arena elision.

Inputs. bodies; signatures (non_allocating, fallible, ffi); the callgraph; ownership (accept sets)

Producer. crates/hale-types/src/alloc_summary.rs · derive_alloc_summary

Also owned. crates/hale-types/src/alloc_summary.rs · summarize_identified; crates/hale-types/src/alloc_routing.rs · derive_alloc_routing; crates/hale-types/src/alloc_routing.rs · scratch_local_free_fns

Consumers. the effects certificate engine (the check’s @effects, @phase_effects and placement diagnostics: the snapshot’s summary, handed in) (crates/hale-types/src/check.rs · CheckInputs); effects (the rows walk the snapshot’s summary and hold it, shared) (crates/hale-frontend/src/snapshot.rs · demand_effects); check (the unbounded-allocation advisory, --dump-alloc-summary and --report-unbounded-use: the snapshot’s summary) (crates/hale-cli/src/verbs/check/run_impl.rs · demand_alloc_summary); the editor’s typing stage (the advisory in the diagnostics, Config::alloc_advisory: the snapshot’s summary) (crates/hale-frontend/src/snapshot.rs · typing_stage); lsp (hale/allocSummary: the snapshot’s summary) (crates/hale-lsp/src/lib.rs · demand_alloc_summary); model (its function rows, dispatch sites and holes: the snapshot’s summary’s own rows) (crates/hale-types/src/model_builder.rs · program_rows); topology (the artifact’s fn sort, labels, derived effects and through-stdlib contraction: the snapshot’s summary, handed in) (crates/hale-types/src/topology.rs · dump_topology_over); check (the hot-path lint: a law over the program’s own rows and their columns, the snapshot’s summary, handed in) (crates/hale-types/src/check.rs · check_hot_path_alloc); claims (@budget: the counting engines over the snapshot’s summary’s own rows, handed to the evidence) (crates/hale-types/src/evidence.rs · derive_certificate_evidence_over); codegen (arena routing at an allocation) (crates/hale-codegen/src/codegen.rs · current_arena_ptr); lowering view (the routing rows’ scratch-local set: the snapshot’s summary’s, handed in) (crates/hale-frontend/src/snapshot.rs · summary.scratch_local); codegen (a free fn’s scratch: the view’s non-allocating and scratch-local rows) (crates/hale-codegen/src/codegen.rs · alloc_routing); codegen (a locus’s arena, and its hooks’, methods’ and modes’ scratch: the elision rows, a monomorph’s specialized) (crates/hale-codegen/src/codegen.rs · locus_elision); resource_budget (the fd sites and the fd-leak warnings: the snapshot’s summary’s own rows) (crates/hale-types/src/resource_budget.rs · program_rows); frontier (the causes: engine: the summary’s own rows) (crates/hale-types/src/frontier.rs · causes_inner); a declaration’s dependents (X2: the call edges of the rows and of the declaration bodies) (crates/hale-frontend/src/dependents.rs · declaration_bodies)

Invariants.

• one summary per snapshot: Snapshot::demand_alloc_summary runs derive_alloc_summary once over the checked programs with the stdlib’s analysis copy beside them (cross-seed calls resolved through the import renames), counted as alloc_summary, blocked with the scope; the check’s effects certificate engine reads it (CheckInputs::alloc_summary) and the effect rows walk it, so neither builds its own; summarize_identified is the one constructor, and derive_alloc_summary (which places the stdlib’s analysis copy beside the programs itself) its one caller outside tests, so no reader builds a summary variant of its own
• the checker’s reclaim model and codegen’s routing agree; a stale copy is a registry violation, not a comment: summarize_identified classifies each free fn’s frame (FnSummary::frame: ScratchLocal { recursive } or CallersArena; None for a method, a hook, a mode, main and an unclassified row) with the classifier lowering reads (alloc_routing::scratch_local_free_fns), over the declarations lowering lowers (the programs, their imported seeds under their mangled names, and the stdlib, beside the program whether or not the summary holds the analysis copy’s rows) with the same renames, so the frame is lowering’s row on every target (pinned in alloc_summary_reclaim_boundary.rs)
• that classifier runs once on a build path (F.40 phase 4, Q1): in the summary, which keeps the set it classified (AllocSummary::scratch_local, a set of fn names); demand_lowering hands the snapshot’s summary’s set to the view, and lowering’s rows (derive_alloc_routing) take it rather than classifying the merged program again (pinned by a thread-local count, scratch_local_derivations_on_this_thread, in demand_gate.rs). The two runs it replaced read the same declarations but one: a program that declares a top-level item named like one of the stdlib’s free fns (all __-prefixed) has the stdlib’s twin left out of the summary, where the merged program held both
• the reclaim boundary is relative to the loop analyzed (E3b, a classified correction, pinned per target in alloc_summary_reclaim_boundary.rs): a Local allocation of a scratch-local fn that is not recursive reclaims at its return (ReclaimScope::FnReturn), which ReclaimScope::accumulates_in_loop places inside each iteration of a caller’s loop and outside every iteration of the fn’s own (LoopAt); such a fn stops the scratchless long-lived propagation as a method’s per-call scratch does; Local is not scratch, so a Local of a CallersArena fn run once per iteration of an unbounded loop in a long-lived frame lands in that frame’s arena and accumulates (LeakReason::InCallersArena), a locus instantiation excepted; an escaping value keeps its boundary, and a recursive fn keeps the locus boundary; the model, the budgets and shape_hash read none of it
• lowering routes from the view’s rows (LoweringView::alloc_routing, derive_alloc_routing over merged with the view’s renames and the summary’s scratch-local set) and derives none: a free fn skips its per-call scratch when the rows call it non-allocating (FORM-3, a greatest fixpoint keyed by name), and its body allocates into its own subregion when they call it scratch-local (#1148); a locus’s arena is elided, and a lifecycle hook, fn method or mode lowers without its per-call scratch, when its elision row says so (LocusElision, keyed by the locus and the member’s position; a generic locus’s monomorph, which lowering synthesizes, takes AllocRouting::specialize over the synthesized declaration); the FORM-3 classifier (fn_body_definitely_non_allocating) is the rows’ own and lowering calls it nowhere; the two method-elision stages still classify a self field differently (stage 1, the per-member verdict, by its literal default or its ascription through aliases; stage 2, the self.m() sets, by a primitive ascription only), and a monomorph still has no stage-2 set, both as they were; a free fn’s entry publishes its caller’s arena to the caller-arena TLS when its row says so (caller_arena_publish: not non-allocating, and a call or a struct literal anywhere in its body, found by a structural walk, a string literal spelling Call { or Struct { counting as the Debug-string test it replaced counted it; a generic fn’s monomorph takes AllocRouting::specialize_fn), and no body’s Debug rendering decides it; the rows are #1208’s classification moved as it was, so its builtin list is still a hand-kept subset of the checker’s BARE_BUILTIN_CALLEES with no agreement test, its std:: namespaces a per-namespace claim no stdlib_surface row states, and its qualified-path lookup checks the import renames before PATH_RENAMES where resolved::lookup_qualified_path checks them in the other order
• a body’s escape tags key a binding by the declaration its escaping uses name (Snapshot::declaration_of), so an inner shadow of a returned name is its own, local binding (the #1140 shape), and close over let x = y; aliases to the declaration y names, as borrow_lifetime’s returned_decls does; programs minted by different snapshots are summarized each with its own identities (summarize_identified: a bundle’s programs beside the bundled stdlib’s analysis copy)
• each seed’s names resolve in its own scope: the programs minted with one set of identities are one scope, a body’s bare free-fn name (and the locus a call’s result is typed by) resolves only to a fn of its own scope, and the import renames are the bundle’s names (the stdlib’s analysis copy imports nothing), so a stdlib body’s builtin count(...) is the builtin, never a user fn called count (a classified correction, pinned per target in alloc_summary_construction_correction.rs)
• the unbounded-invocation fixpoint (AllocSummary::unbounded_invoked) seeds from what the program reaches: beside the stdlib’s analysis copy, AllocSummary::reached is the program’s own fns, what their calls reach (the interface fan-out included) and the hooks and bus handlers of every locus they start (a struct literal of it in a reached body, or a param field of a started locus by declared type or default literal; every locus of the program’s own is started), and only those seed it or call, so a stdlib loop the program never starts invokes nothing (a classified correction, pinned per target in alloc_summary_construction_correction.rs)
• the run-to-exit rule (a main and no long-lived entry: no leak sites) reads the program’s own entries, never the stdlib’s analysis copy’s (AllocSummary::analysis_copy names the copy’s fns, is_own the program’s), since the copy always carries run hooks (a classified correction, pinned per target in alloc_summary_construction_correction.rs)
• and it counts an entry only on a locus the program can start (GH #1490, AllocSummary::startable, loci_started_from_main): every locus of the program’s own seed, and every imported or stdlib locus a path written in a fn its main reaches, or in a started locus’s declaration, names (an import alias through the renames, a std:: path through the stdlib’s); a declaration that is neither a fn nor a locus starts what it names; a call through a function value the walk does not resolve leaves the set unknown, and the rule counts every own entry as before; it only narrows, so an imported seed’s loci a program never names make it no daemon (the host’s verb program), and a program with no own entry stays run-to-exit whatever stdlib locus it starts (a classified correction, pinned in alloc_summary_construction_correction.rs)
• a program’s declaration is the row where the stdlib’s analysis copy declares the same name: the copy’s top-level free fn, locus or interface of a name a checked program declares stays out of the summary, so a stdlib source file checked as itself keeps its own rows (its bodies, its spans, resolved in its own scope); only stdlib source shares such a name (a classified correction, pinned in alloc_summary_construction_correction.rs)
• the rows carry what the hot-path lint reads: a fn’s @hot and whether it is a mode (FnSummary::hot, mode), the order of the declarations (decl_index), where a site or a call is written (in_loop, which a return / fail payload does not reset as it resets loop_depth), a struct literal written as a whole statement (AllocSite::bare_stmt) or as the whole right side of a self.<field> = replace (self_replace, the statement’s span; an in-place replace, which allocates nothing, is in FnSummary::in_place_sites, not sites), the let a call is the value of (CallEdge::let_span), how a call is spelled (CallSpelling), and the allocating receives (CallEdge::allocating_recv, the one list, which @budget reads too)
• the hot-path lint is a law over the rows (check_hot_path_alloc, over the summary the check is handed): the program’s own fns, a mode aside, in declaration order, each finding where its site or call is written, a bus handler’s at any depth, @hot an error and @unbounded or @bounded_by(<name>) (GH #1490: one silenced set, AllocSummary::unbounded_fns, the bound kept beside it for display) silencing the advisory; no reader walks bodies for it, so it sees what the summary’s walk sees (a publish, a bare block, violate, a recovery and shm_write included, which the lint’s own walk skipped; an index expression’s subscript included, walked as any operand is, as the lint’s walk walked it, so a @hot fn keeps that rejection (a classified correction, pinned in hot_path_alloc.rs); a callee that is an expression of its own excluded, which it reached) and its diagnostics over the corpus, the targets and the lint’s pins are the lint’s, in order (pinned in hot_path_alloc.rs); it is a registered rule (the structural table’s “Hot-path allocation”) run as a law::Law, its finding a law::Violation, an error under @hot and a warning otherwise (phase 4, W5)
• a module-nested declaration is summarized like a top-level one: every declaration pass walks module { … } nesting (flat_decls; a module is a namespace, not an analysis boundary, GH #764), so a module-nested fn or locus member has a row and a call into it resolves, and the model holes out no module-nested body; the one body with no row is an on_failure handler, summarized as a declaration body (a classified correction, pinned in alloc_summary_construction_correction.rs)
• the advisory, --dump-alloc-summary and the editor’s hale/allocSummary read the snapshot’s summary and report the program’s own rows judged over the whole of it (the stdlib’s analysis copy and the renames included: a classified correction, pinned per target in alloc_summary_correction.rs); a leak site is the program’s own (AllocSummary::is_own) and is left out of the advisory only when it has no author position (AuthorPositions::has: its span at or beyond API_SYNTH_BASE, or in a declaration the origin rows mark synthesized whose offset no source file owns), never by its owner’s name; the check’s warnings, the editor’s diagnostics and the editor’s hale/allocSummary decide with one function (advisory_leak_sites)
• a call through a function value resolves to the program’s function values (F.40 E5): the summary marks a call through a function-typed parameter, a local its walk does not follow to a fn, or a computed callee CallEdge::indirect, and resolve_function_values rewrites it into one alternative per fn some expression of the bundle reads as a value (fn_values: every expression the identity walk reaches, a callee written as a name or a path and a name a binding in scope spells excluded; resolved as a let of it resolves) whose arity is the call’s and whose declared signature can be the parameter’s or the bound field’s declared type, sharing a dispatch group (CallEdge::via_value the callee as written); a call no such value can be stays indirect, and so does every call of a bundle that reads a locus’s method as a value, which this does not follow
• the model projects the program’s own rows; a call into the analysis copy is the unresolved row: the model, the @budget engines (budget_check, quantitative), the artifact’s user rows, the frontier’s causes: engine and the resource budget (its fd sites and fd-leak warnings) read the snapshot’s summary through AllocSummary::program_rows (own_rows with the appended api runtime, which the program declares and the walkers walk, kept as the program’s: the walked set is the summary set; the ownership judgments (is_own, own_rows) leave it out) (the program’s fns and loci; a call resolved into the stdlib’s analysis copy is the unresolved call by the method’s bare name, the receiver kept; a dispatch keeps its alternatives among the program’s own loci, renumbered in key order, through the copy’s interface is no dispatch, and through the program’s own with none of its conformers left is the dead site; a function-value dispatch keeps its alternatives among the program’s own fns and the leaves the program itself reads as values (AllocSummary::copy_alternative), its groups numbered after the interface groups, and with none left is the indirect call as written), which is the program-alone summary field for field, so the copy moves no shape_hash, the build and replay identity, and the copy’s fd-acquiring bodies are not the program’s resources (pinned per target in alloc_summary_own_rows.rs); what the model would gain from the copy’s rows is a separate correction
• a body the program writes that is no row is a declaration body (AllocSummary::declaration_bodies, DeclarationBody): an on_failure handler, a params block’s initializers, a constant’s value, a birth_check, a perspective’s fns, params and stable_when, a synthesized hook, each wherever it is declared (a module { }’s included, through flat_decls, as the rows are), and every subexpression a walk does not descend into (a callee that is no name; an index’s subscript is the row’s own, walked), each walked as a row is and keyed to the site of the declaration it is a member of; no judgment reads them, so the rows and every consumer’s answer are what they were without them (X2, a review fix: hale check with every dump over the corpus, tests/hale and every dna/**/main.hl unchanged), and the declaration dependents relation reads their call edges as the declaration’s own

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · alloc_summary_a_declaration_without_its_routing_rows_is_refused; total: no row in the routing sets means the conservative answer: a fn not proven non-allocating keeps its scratch, one not scratch-local allocates into its caller’s arena, and a member with no scratch entry keeps its scratch; a locus’s elision rows and a free fn’s caller-arena row are required, a generic fn’s monomorph taking the rows’ producer over its synthesized declaration

Focused tests. crates/hale-types/tests/hot_path_alloc.rs; crates/hale-types/tests/alloc_summary_construction_correction.rs; crates/hale-types/tests/alloc_summary_correction.rs; crates/hale-types/tests/alloc_summary_own_rows.rs; crates/hale-types/tests/alloc_summary_reclaim_boundary.rs; crates/hale-types/tests/demand_gate.rs (a_build_classifies_the_scratch_local_fns_once); crates/hale-codegen/tests/alloc_model_rss.rs; crates/hale-codegen/tests/scratch_local_free_fn.rs; crates/hale-codegen/tests/fn_nonalloc_add.rs; crates/hale-codegen/tests/method_scratch_elision.rs

Spec. spec/memory.md § Allocation routing; spec/verification.md § Memory-bound proofs (item 1): the reclaim boundary; spec/styleguide.md

Guarded seams.

• scratch_local_free_fns( may be referenced from: crates/hale-types/src/alloc_summary.rs ×1
• summarize_identified( may be referenced from: crates/hale-types/src/alloc_summary.rs ×4
• allocating_recv( may be referenced from: crates/hale-types/src/alloc_summary.rs ×2
• check_hot_path_alloc( may be referenced from: crates/hale-types/src/check.rs ×1
• derive_alloc_summary( may be referenced from: crates/hale-types/src/alloc_summary.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1, crates/hale-types/src/evidence.rs ×1, crates/hale-types/src/resource_budget.rs ×1
• own_rows( may be referenced from: crates/hale-types/src/alloc_summary.rs ×1
• program_rows( may be referenced from: crates/hale-types/src/alloc_summary.rs ×1, crates/hale-types/src/model_builder.rs ×1, crates/hale-types/src/budget_check.rs ×1, crates/hale-types/src/quantitative.rs ×1, crates/hale-types/src/frontier.rs ×1, crates/hale-types/src/resource_budget.rs ×2
• derive_alloc_routing( may be referenced from: crates/hale-types/src/alloc_routing.rs ×1, crates/hale-types/src/resolved.rs ×1
• fn_body_definitely_non_allocating( may be referenced from: crates/hale-types/src/alloc_routing.rs ×12
• unbounded_alloc_warnings( may be referenced from: crates/hale-types/src/lib.rs ×1, crates/hale-cli/src/verbs/check/run_impl.rs ×1, crates/hale-frontend/src/snapshot.rs ×1

Answers. Whether a borrowed handle outlives its holder (GH #730), decided from position over the owner structure.

Inputs. ownership (Borrowed rows); bodies

Producer. crates/hale-types/src/borrow_lifetime.rs · borrow_lifetime_diags

Consumers. check (crates/hale-cli/src/verbs/check/run_impl.rs · borrow_lifetime_diags); build, run, test, replay, bench (a build config’s snapshot check, Config::build_rules) (crates/hale-types/src/lib.rs · build_rule_diags)

Invariants.

• runs on every entry point: it does not run in the LSP or bench today (phase 2 closes that)
• which locus accepts which child is the ownership rows’ relation (accepts_ancestor, the snapshot’s graph’s rows, handed in); it builds no accept set of its own

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-cli/tests/check_borrow_lifetime.rs

Spec. spec/semantics.md § A borrow outlives its holder; spec/decisions.md F.39

Guarded seams.

• borrow_lifetime_diags may be referenced from: crates/hale-types/src/borrow_lifetime.rs ×3, crates/hale-types/src/lib.rs ×1, crates/hale-cli/src/verbs/check/run_impl.rs ×1

Answers. Whether a fallible call’s error is addressed.

Inputs. typed_bodies (the fallible_calls column: each call’s callee mark and what addresses it); typed_bodies (the conversions column: each narrowing’s discharge, GH #1076)

Producer. crates/hale-types/src/bare_fallible.rs · bare_fallible_calls

Consumers. check, verify, build, run, test, replay, bench, the LSP (the snapshot’s check, with the typing diagnostics) (crates/hale-frontend/src/snapshot.rs · bare_fallible_calls); the check of a bundle no snapshot holds (the tests’ entries) (crates/hale-types/src/check.rs · bare_fallible_calls)

Invariants.

• one rule for user and stdlib calls: only an or handles a fallible call; any other position (an argument, an operand, a match scrutinee, a let initializer, a statement, a returned value) is the GH #738 error, so hale check refuses what hale build refuses, save a call through an interface-typed local or parameter: the checker types that receiver Unknown, so the column holds no row for the call and only the build refuses it (a typing limitation to lift)
• the law reads the column, never the signature table or the syntax tree: the checker records each fallible call’s callee mark (Declared, Typed, Stdlib) and what addresses it as it walks
• an or’s handler takes the implicit or raise exactly where lowering does (expr_is_fallible_call): a Declared callee; any other fallible handler is refused with the nested spelling, a limitation to lift, not a rule
• the checker types a fallible value no or addresses as its success type, so a bare call reports the law’s one error and no type mismatch
• runs on every entry point, the LSP and bench included (the snapshot’s check)
• a narrowing into a range (Session(n), GH #1076) is fallible like a call: its conversions row records what its or discharges it with, and a narrowing nothing discharges is refused in the law’s own words (judge_narrowing), listing the five discharges; a change of denomination that divides (U3: d.in(s), Seconds(d), q / 2, an implicit conversion into a coarser type) has a remainder to say something about, at the site or by the target type’s round:, and with neither is refused naming the divisor (an implicit one, which has no or of its own, pointing at the explicit conversion or the policy)

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-cli/tests/check_strict_fallible.rs; crates/hale-types/tests/typed_bodies.rs; crates/hale-types/tests/unit_values.rs

Spec. spec/semantics.md § A bare fallible call is an error; spec/types.md

Guarded seams.

• bare_fallible_calls( may be referenced from: crates/hale-types/src/bare_fallible.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1

Answers. Whether a fn that may violate says so: a value-returning one is fallible(ClosureViolation) (F.42), and one returning nothing is warned about until a later release makes it the law.

Inputs. alloc_summary (each fn’s violates column, the violate statements of its own body, and its resolved call edges); fn declarations (each fn’s written return type and fallible clause, the program’s and the stdlib analysis copy’s)

Producer. crates/hale-types/src/violate_fallible.rs · violate_fallible_laws

Also owned. crates/hale-types/src/violate_fallible.rs · may_violate; crates/hale-types/src/violate_fallible.rs · verdicts

Consumers. check, verify, build, run, test, replay, bench, the LSP (the snapshot’s check, with the typing diagnostics, beside the bare_fallible law) (crates/hale-frontend/src/snapshot.rs · violate_fallible_laws); the check of a bundle no snapshot holds (the tests’ entries) (crates/hale-types/src/check.rs · violate_fallible_laws)

Invariants.

• may violate is the direct reading: a violate statement in the fn’s own body, or a resolved call to a value-returning fn that may violate and is not fallible; a violation in a method returning nothing is not the caller’s failure, so a call to one carries nothing, and a fallible callee is answered at its call by the bare_fallible law; an edge the summary cannot resolve contributes nothing
• three verdicts, over the program’s own fns only (the stdlib analysis copy is a callee; its fns are held to the law by tests/violate_fallible.rs): a value-returning fn that may violate and is not fallible is refused, naming the path (the closure, or the callee it goes through, with the call and the violate as notes); one declared fallible(E) with another E is refused; one returning nothing that is not fallible is warned about
• lifecycle bodies (no fn declaration), bus handlers (the summary’s entry kind) and fn main are exempt: the runtime is their caller
• a stated gap: a locus method serving a perspective fn (serves, matched by name as conformance matches it) is exempt from the law and the lint and carries nothing to its callers, and is warned about instead, until a fallible perspective call lowers (the build refuses one today, and conformance matches the perspective fn’s fallibility both ways, so no spelling of it both checks and runs); it keeps today’s lowering
• lowering agrees: in a fallible(ClosureViolation) fn a violate stores the record in the error slot and takes the failure return, after the owner’s on_failure (in place, or posted to the owner’s domain and awaited); the undef of the declared type is reached only by an exempt value-returning bus handler

Missing data. an unknown is a hole with a stated policy

Focused tests. crates/hale-types/tests/violate_fallible.rs; crates/hale-codegen/tests/violate_build.rs; tests/hale/violate_in_value_method_test.hl

Spec. spec/semantics.md § A value-returning method that may violate is fallible; spec/types.md § ClosureViolation, the error of a violating fn (F.42); spec/verification.md § Structural & design rules; spec/decisions.md F.42

Guarded seams.

• violate_fallible_laws( may be referenced from: crates/hale-types/src/violate_fallible.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1

Answers. Which run() bodies never return, which children are long-running, and whether the birth order or a pool starves because of it.

Inputs. flows (each locus declaration’s run row: the long-running and never-returns columns); params order; placement (the table’s rows for the deployed root’s fields)

Producer. crates/hale-types/src/flows.rs · run_statically_nonreturning

Also owned. crates/hale-types/src/check.rs · check_pool_starvation; crates/hale-types/src/check.rs · check_birth_order

Consumers. check (the nested-long-running-child rule reads the long-running column) (crates/hale-types/src/check.rs · check_nested_long_running_child); check (the starvation and birth-order laws read the never-returns column) (crates/hale-types/src/check.rs · never_returns)

Invariants.

• two definitions, two columns of the flow rows’ run row (flows::RunRow), named in spec/runtime.md § Typecheck enforcement: long-running is a run() body with a statement of its own (a nested child’s run() completes before its parent’s begins, so any body delays the parent, whether or not it returns), never-returns is a terminal while with no exit whose condition never flips false (only such a body starves the cells a pool runs after it); every body that never returns is long-running, not the converse, and a child whose run() is std::time::sleep(1min) keeps the long-running-child error
• the checker surveys the flow rows once per check and the three rules read the columns; none decides either question itself; a stdlib locus, whose body the checker does not see, is both when it is on the known-long-running allowlist (KNOWN_LONG_RUNNING_STDLIB_LOCI)

Missing data. an unknown is a hole with a stated policy

Focused tests. crates/hale-types/tests/birth_order_trap.rs; crates/hale-codegen/tests/birth_order_trap.rs; crates/hale-codegen/tests/nested_long_running_child.rs; crates/hale-types/src/flows.rs (long_running_and_never_returns_are_two_columns)

Spec. spec/semantics.md; spec/runtime.md § Typecheck enforcement

Guarded seams.

• run_statically_nonreturning( may be referenced from: crates/hale-types/src/flows.rs ×2

Answers. The estimated working set per locus and program, and the locality law over it.

Inputs. declared shapes; @locality

Producer. crates/hale-types/src/working_set.rs · compute_program_working_set

Also owned. crates/hale-types/src/working_set.rs · compute_locus_working_set; crates/hale-types/src/working_set.rs · compute_program_returns_entry_per_locus

Consumers. build (crates/hale-cli/src/verbs/build.rs · compute_program_working_set)

Invariants.

• build-only today, and a warning without –strict; layer 7 (layout) reads it later

Missing data. an unknown is a hole with a stated policy

Focused tests. crates/hale-cli/tests/target_model.rs

Spec. spec/memory.md

Answers. Which thread domain each instance runs in: pools, pinned threads, replicas, affinity, and the deployment plan.

Inputs. placement and topology blocks; entrypoint (the row’s root: the entry, or a seed’s refused module-nested main); the construction templates: the root’s literals, the entry’s implicit construction of a root no literal builds, fn main’s own literals, the root’s bindings { } adapters; the params towers each template builds; the minted sites of the snapshot and of the stdlib analysis copy; free fns and locus bodies (dynamic sites, their domains and bounds)

Producer. crates/hale-types/src/placement.rs · derive_placement

Consumers. check (rule 6, the lowering laws) (crates/hale-types/src/lowering_laws.rs · pinned_features); check (instance aliasing, #334: where each of the deployed root’s params fields runs, the table’s root and the domains of its rows) (crates/hale-types/src/check.rs · check_instance_aliasing); check (rule 17, the lowering laws: the root’s constructions and their bounds) (crates/hale-types/src/lowering_laws.rs · pinned_root_in_a_loop); check (rule 18, the lowering laws: the root and its constructions) (crates/hale-types/src/lowering_laws.rs · placement_entry_consumed); check (rules 2-5, 13-16); check (F.31: the caller per instance, the receiver by its row’s owner_relative) (crates/hale-types/src/check.rs · check_placement_single_thread); check (the blocking check and the starvation and birth-order laws: where each of the deployed root’s fields runs, its pool’s async_io, and the declarations it realizes) (crates/hale-types/src/check.rs · root_field_placements); check (type-check rule 20: the construction paths of a handler birth’s enclosing locus, OwnershipGraph::construction_paths over the table handed in, derived only when that locus does not accept the child itself) (crates/hale-types/src/check.rs · check_unowned_subscriber_locus); sync_inference (accessor domains per instance) (crates/hale-types/src/sync_inference.rs · infer_sync_for_bundle); dispatch (domains: the plan’s domain map, Arrangement::domains, over the arrangement projection) (crates/hale-types/src/arrangement.rs · fn domains); model (the arrangement: instances, owners, placed_in and affined_to, the table’s rows projected through project_arrangement, user-only: the snapshot’s projection, handed in) (crates/hale-types/src/model_builder.rs · derive_application_model_over); the intra-locus rewrite (a publish into a field off its owner’s thread stays on the bus: PlacementTable::off_owner_fields) (crates/hale-types/src/resolved.rs · rewrite_intra_locus); codegen (the deployment plan, the table’s lowering view: the root, and per root field an entry decides its schedule class, pool, NUMA node and replica cores; the pools’ async_io and affinity; the pinned anchors’ and pooled rows’ realized declarations, an adapter among the anchors) (crates/hale-codegen/src/codegen.rs · collect_main_placement); resource budget (the threads, partitioned by the scope that creates them: the root’s pinned anchors under their construction’s bound, the adapters once; the worker pools, main never one) (crates/hale-types/src/resource_budget.rs · budget_for_programs); codegen (whether a thread crosses the bus boundary: a domain that is not main, places_off_main, over the lowering view’s table, the snapshot’s, handed in) (crates/hale-codegen/src/codegen.rs · program_has_offthread); codegen (the registration route: the pinned anchors whose tree holds a subscriber, or whose thread may build one at run time (a dynamic site in the anchor’s domain, or in no known domain, whose locus subscribes or whose params defaults, transitively, build one), by lowered name, each given a mailbox the subscriptions made on its thread route to) (crates/hale-types/src/resolved.rs · route_anchors); bus_graph (every placement label and the direct-call gate: the set of each type’s instances’ domains) (crates/hale-types/src/bus_graph.rs · type_placements); check (a subscriber’s bounded(N, …), legal only where every instance runs on main: B-2, read only when a subscriber is bounded) (crates/hale-types/src/check.rs · check_bounded_bus); ownership (each bubbling edge’s class: the enclosing instances paired with their owner rows) (crates/hale-types/src/ownership_graph.rs · relate); lsp (hale/placement); deployment (reserved)

Invariants.

• placement is keyed by instance, never by type: one row per static instance of each construction template (a key is its origin, its field path, its replica), and a type’s answer is the set of its instances’ domains
• the entry is a construction scope: a root no literal builds is the entry’s implicit template (Origin::Entry, bound Once), and fn main’s own literals are templates bound by their statement’s loop context; an adapter is an origin of its own, built once
• nested rows inherit their owner’s domain unless a root field’s entry or a binding decides it; pinned domains are per anchor and per replica, pool domains one per name with at most one affinity
• the root is the entry row’s root (EntryRow::root): the entry, which lowering deploys, or in a seed with none the module-nested main the check refuses and still judges (RootRow::is_entry false); an imported main is never the root
• every root entry decides exactly one field family in each construction template, or it is a hole
• unknown is a hole, not a default: an unresolved declaration, an unenumerable initializer, a held instance (Reuse) and a dynamic site of unknown domain each carry their policy, and none is main
• a held instance’s subtree lives in its holder’s domain: the held row keeps its Reuse hole and its owner’s domain, the source’s actual rows (never the declaration’s defaults) are projected under it, inherited, and each of those rows names its own source row, the one it was built as (built_by); where the source is not linked, nothing below the held row is asserted, and an instance there runs in an unknown domain; a question of where an instance runs skips the source’s rows, a count of instances skips the held ones
• every site the table names carries the universe that minted it (SiteRef); lowering joins the stdlib’s into its merged mint once, totally and injectively
• the checker builds no table: the snapshot demands it and hands it to the check (CheckInputs::placement) and to the form rows; a bundle no snapshot holds (check::check_bundle, the tests’ scope-taking check) builds it once, over the bundle with_identities numbers (a copy of an unminted bundle, minted first, so the table names its sites)
• the model’s arrangement is the table’s rows projected (placed_in.push( and affined_to.push( have one writer): the deployed root’s templates, each instance where it runs, user declarations only; the table, not the arrangement, answers every placement question. The projection is one function, project_arrangement (F.40 phase 3, C5), run once per snapshot over its programs, table and ownership graph (Snapshot::demand_arrangement, the arrangement count, F.40 phase 4, Q1): the model builder makes its rows and placement holes from that one (ModelInputs::arrangement), and the dispatch plan reads its domains from it. It names each declaration by name, which is all either reads, so a snapshot holds it, and nothing else projects one
• a consumer asks where instances run of PlacementTable::running (the handed-off rows skipped): a type’s answer is the domains of its instances, compared per instance, never collapsed to one per type; an enclosing locus with no static instance is a hole that disables the F.31 proof, never a default to main or to pinned
• a count over the table is over templates: a domain belongs to a template, as the key that anchors it does, and has one anchor per live occurrence; a count sums the templates, each times its bound (Unbounded makes the count an uncertainty with its reason), takes the maximum over the alternatives of one step (one occurrence takes one), counts each replica row once and never multiplies it by K again, and counts an adapter once, never under a root construction’s bound (PlacementTable::templates, per_occurrence)
• the resource budget counts the resource, read from the table: OS threads are the pinned anchors (one per replica) times their construction’s bound, plus one per adapter; a pool is one worker however many instances it holds, an affinity is a column of its domain and never a thread, and main is never a pool; only the deployed root’s rows count, so an imported or non-root main’s entries cost nothing; a binding’s reader thread and a stdlib transport’s serve thread are not placement facts and are named as not counted
• lowering’s deployment plan is the table’s lowering view, read once before lowering (collect_main_placement over LoweringView::placement): no field name or written type decides a schedule class, a pool or a type set; a user site the table names is the node of the same index in the merged program, and the deciding entry’s written selector says only whether one core is emitted alone or as a set
• subscriptions follow the tower (U-6): a nested instance’s subscriptions register with its anchor’s route, the pinned anchor’s mailbox or the pool anchor’s pool, never the program-wide queue; the route exists before the anchor’s params are initialized and outlives every registration routed to it (each descendant deregisters in its dissolve, on the anchor’s thread, and the join retires what is left before it destroys the mailbox)
• a pinned anchor’s subtree initializes on the anchor’s thread: the instantiating thread creates the route and the thread, the thread initializes the params (every nested construction, registration, birth and inline run(), a yield draining the anchor’s mailbox) and reports ready, and the instantiating thread waits for it, servicing its own mailbox as a yield there would, before the literal completes; an override written at the literal is the instantiating code’s and is evaluated there, and a locus it builds as the field’s value is built on the anchor’s thread; the init’s temporaries are dissolved at its end, on the anchor’s thread
• a pool anchor’s subtree initializes on the pool’s worker, as the anchor’s first job there: the instantiating thread posts the params’ initialization to the pool and waits for it as for a pinned anchor, and the worker runs every nested construction, registration, birth and inline run(), and the params’ settle, a yield draining the pool’s queue; the job never parks (on an async_io pool it runs on the worker’s own stack), so the roots of one pool initialize in post order; a worker blocked on the instantiating thread’s decision runs the posted initialization in place; the anchor’s own birth() stays on the instantiating thread and its run() is posted behind the job
• the model’s arrangement projects the table but covers less than the table, and the table answers every placement question: a literal fn main builds besides the root is not arranged (M-7: its birth is a hole of the model’s dynamic births, the ownership family’s legacy row, and arranging it moves with that row), nor is a row realizing a stdlib declaration (U-4: Realizes names an entry of entities.loci, which the hashed half renders, so arranging one moves shape_hash; carrying them is a model schema change of its own)
• F.38: placement is semantics-free, so a backend may Approximate it
• placement is a choice point: v1’s declared placement is the single candidate
• the authored blocks are validated before they are rows: check_pool_affinity judges each main locus’s own placement { } block (an affinity on no named pool, two affinities for one pool), deployed or not, over the entry row’s witness (mains), and that judgment is what lets the table keep one affinity per pool domain (rule 16); the per-block pool-to-affinity map it keeps is the block’s well-formedness, not a placement fact, so it derives no row and no consumer reads it

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · placement_an_entry_without_its_root_row_is_refused_at_the_entry; total: no root where the entry row names no main locus means nothing is deployed; no entry deciding a field means it runs where its owner does; no realized declaration (a hole) means the row joins no thread set; and no anchor in the route set means it has no nested subscriber

Focused tests. crates/hale-types/tests/placement_golden.rs (static instance rows, root, template bounds, domains and holes, plus the dynamic domain and hole projection read by consumers, over the corpus, tests/hale, DNA and placement fixtures; each seed by id, shared row groups by hash; HALE_SHADOW_REGEN regenerates); crates/hale-types/tests/placement.rs; crates/hale-types/tests/placement_pairings.rs; crates/hale-codegen/tests/pool_affinity.rs; crates/hale-codegen/tests/placement_where_async_io.rs; crates/hale-types/tests/placement_table.rs (the table through the frontend’s load: the correspondence’s coverage cases 1 to 16, the two universes joined into lowering’s mint, the table’s laws over every clean fixture, and a check that demands it once); crates/hale-types/tests/form_rows.rs (sync inference per instance, K-5); crates/hale-codegen/tests/nested_offthread_delivery.rs (the receiving thread of a nested subscriber, recorded inside its handler and inside its birth() and run(), in both devirtualization arms; the startup handshake, a nested child waiting during its anchor’s initialization for a delivery through the anchor’s route, or for a reply from a subscriber on the instantiating thread (and its control with that thread’s drain off); a temporary of a pinned default, dissolved at the init’s end; the same startup under a pool anchor (the review’s program beside pinned, a child two levels down, two pool roots on one pool, an async_io pool, the round trip through main and its control, a worker blocked on a held failure running the init); the route’s IR, for both threads, and its teardown under ASan); crates/hale-types/tests/intra_locus_pool_safety.rs (the intra-locus rewrite keeps a publish into a field off its owner’s thread on the bus, through the lowering view); crates/hale-types/tests/model_arrangement.rs (the model’s arrangement as the table’s rows: M-1, M-3, M-5, M-7, M-9, U-4 and U-5, each against the old build’s ids and hashes); crates/hale-types/tests/resource_budget.rs (the budget’s rows R-1 to R-7 and checkpoint 4 through the frontend’s load: replicas, one worker per pool, affinity, imported roots, constructions times their bounds and the uncertainty, adapters once, main never a pool, the dump’s counted and not-counted lines); crates/hale-codegen/tests/placement_occurrences.rs (checkpoint 1: one template, one domain, its bound multiplying the budget; two live occurrences of one literal on two anchor threads, each nested subscriber on its own, in both devirtualization arms)

Spec. spec/semantics.md § Placement block (F.31); spec/decisions.md F.31, F.35, F.38; spec/runtime.md § Placement classes (m28b: subscriptions follow the tower)

Guarded seams.

• derive_placement( may be referenced from: crates/hale-types/src/placement.rs ×2, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1, crates/hale-types/src/sync_inference.rs ×1
• bundle_placement( may be referenced from: crates/hale-types/src/placement.rs ×1, crates/hale-types/src/lifecycle/derive.rs ×1
• collect_main_placement( may be referenced from: crates/hale-codegen/src/codegen.rs ×2
• route_anchors( may be referenced from: crates/hale-types/src/resolved.rs ×2
• placed_in.push( may be referenced from: crates/hale-types/src/model_builder.rs ×1
• affined_to.push( may be referenced from: crates/hale-types/src/model_builder.rs ×1
• project_arrangement( may be referenced from: crates/hale-frontend/src/snapshot.rs ×1
• check_pool_affinity( may be referenced from: crates/hale-types/src/check.rs ×2

Answers. What a target can lower and what it refuses: the wasm stdlib refusals, link refusals, per-site skips, async_io availability, FFI portability.

Inputs. –target; a source target declaration; stdlib_surface; FFI signatures

Producer. crates/hale-types/src/capability.rs · derive_capability_matrix

Also owned. crates/hale-types/src/capability/uses.rs · derive_capability_uses; crates/hale-types/src/capability/uses.rs · admission_diags

Consumers. check; build; docs (systems/webassembly.md § What wasm32 can do, and spec/ffi.md’s refused-namespace table: regions rendered from the cells) (crates/hale-types/src/capability.rs · render_markdown); the effective-target row, on the snapshot: the check’s target and its conflict refusal, the editor’s alike (crates/hale-frontend/src/snapshot.rs · demand_target); hale build’s backend and artifact naming, from the effective target (crates/hale-cli/src/verbs/build.rs · compile_target(row.effective)); hale run and replay refuse a program whose effective target is wasm32 (crates/hale-cli/src/shared/options.rs · refuse_unexecutable); the use rows, on the snapshot: the check’s input beside the row (crates/hale-frontend/src/snapshot.rs · demand_capability_uses); the admission law: every use’s cell for the effective target, in the check of every entry point (crates/hale-types/src/check.rs · admission_diags); hale check and hale build: every link input (–link, each package’s [ffi] link) held to LinkLibrary before any tool, located at its manifest line or flag (crates/hale-cli/src/shared/options.rs · link_refusals); a build handed link libraries (the harness, a library build): LinkLibrary read off the lowering view’s column before lowering and before any tool (crates/hale-codegen/src/codegen.rs · Capability::LinkLibrary); lowering: every behaviour and obligation emitted or omitted per target, read off the lowering view’s column (LoweringView::cells) (crates/hale-codegen/src/codegen.rs · self.cells.); the wasm32 link: the module’s fixed exports are ExportSurface’s lowering data (crates/hale-codegen/src/codegen.rs · Lowering::Exports(fixed)); the check of an @ffi or @export signature: the FfiType cells for its ABI on the effective target (crates/hale-types/src/check.rs · ffi_type_refusal); the teardown spines: the pool join, wait-abort and ingress quiesce each spine owes, in the lifecycle plan’s order (crates/hale-codegen/src/codegen.rs · emit_teardown_obligations)

Invariants.

• Approximate is legitimate only in layers 5 and 7; everywhere else a target lowers or rejects, with the row’s witness
• the docs’ target statement is generated, never hand-maintained
• every (target class, capability), (target class, invocation) and (target class, obligation) pair has exactly one written cell: no default arm, the musl column written out like the others
• behaviours and obligations are distinct types: an obligation is omitted only on a premise (a Reject behaviour, a Refused invocation, a registered proof) that holds on its own target, and a Lower behaviour requires only Lower behaviours
• a capability refusal depends only on the program, the configuration and the target; a failure that depends on the machine running the compiler stays a toolchain error
• a target’s class comes from its (arch, os, env), never from a triple’s name; the effective target is a function of the snapshot key’s configured target and its sources
• one effective target for analysis and emission alike (T1(b)): an explicit --target, else a written target wasm/browser_js declaration (wasm32), else the host; a --target of another class than a written declaration’s is refused at the declaration, and a declaration --wrap-main injects never selects
• every use is read off resolved identities (a call, a method through its receiver’s type, a cross-seed alias, a construction and the lifecycle it implies), never a std:: spelling of the call; a type-only mention is not a use
• the program’s own sources are the horizon: a use is refused once, at its first site in them, naming the capability, the target and its witness chain; a callee beyond it is refused at the call that crosses into it (the TCP connection substrate appended to a program that names it is beyond it, as the stdlib is: a std::http::Server or std::io::tcp::Listener is refused at its literal)
• an unresolved requirement is never an admission on a target that rejects anything in its family: a hole is refused there and recorded elsewhere
• a policy refusal comes before any tool is probed: a link input the target refuses is refused by the check and by the build before clang, wasm-ld or zig is looked up, located at its input (T4)
• emission configuration through TargetSpec only, every capability through the matrix: codegen’s remaining wasm-ness reads are the emission choices and the link path, and every behaviour and obligation it emits per target is a read of the lowering view’s cells, which the view takes from the effective target and lowering refuses options of another class against
• the matrix selects a target’s lifecycle obligations and the lifecycle plan orders them, alike in every teardown spine (the quiesce, then the wait-abort, then the pool join)
• the portable subset prints the same bytes natively and under node; the comparison proves agreement for its programs and admits nothing outside them

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-types/src/capability/laws.rs · every_pair_has_exactly_one_cell

Focused tests. crates/hale-types/tests/wasm_target_gating.rs; crates/hale-codegen/tests/wasm_target.rs; crates/hale-cli/tests/target_model.rs; crates/hale-cli/tests/wasm_package_csrc.rs (T4: a package’s [ffi] link refused by check and build alike at the manifest’s line; –link named as the flag; the refusal before any tool, on a PATH with no clang); crates/hale-cli/tests/target_precedence.rs (the precedence table: source x –target, check, build and the editor agreeing per cell; wasm-flower built for its declared target; run refusing a declared program; the agreement test: every wasm-relevant program’s located refusals equal on check, build and the editor, with and without –target wasm32); crates/hale-types/src/capability/laws.rs (the matrix’s laws: one cell per pair, anchored witnesses, premises, requires; KNOWN_OPEN empty since T2, T3 and T5 landed, a new entry held to today’s answer); crates/hale-types/src/target.rs (async_io_follows_the_libc: TargetSpec::has_async_io is the runtime’s shape, the AsyncIoPool cell what a program may ask for; they differ on wasm32 alone); crates/hale-types/tests/shadow_capability.rs (the checker rows against their cells over the corpus, tests/hale, the DNA seeds and the wasm programs, on three columns: 0 divergences); crates/hale-codegen/tests/shadow_capability_lowering.rs (the codegen rows, the thread behaviours and @ffi(“js”) against their cells, both targets built, a harness build refused by the admission before lowering; 7 classified divergences, all the design’s: 4 declared export-only programs and 3 declared @ffi(“js”) programs a harness lowers natively anyway, where codegen still says program has no fn main() and the native link fails); crates/hale-cli/tests/shadow_capability_cli.rs (run, replay, record and –wrap-main against their cells; 0 divergences); crates/hale-types/tests/capability_uses.rs (the use producer’s acceptance cases: a stdlib call, a construction with its lifecycle, a handle’s method, a wrapper refused once, module-nested and on_failure bodies, a hole, declaration rows, an export-only program, an exported run(); T2’s pinned, pool, async_io and transport refusals at the entry or binding; T3’s stub namespaces; T5’s @ffi(“js”) on a native target, called or not; each type-only variant admitted); crates/hale-types/tests/capability_doc_matches.rs (both document regions equal the rendered matrix); crates/hale-codegen/tests/target_lifecycle_cells.rs (the five teardown spines on both targets, each owing what its target’s cells select, in the plan’s order); crates/hale-codegen/tests/portable_subset.rs (the design’s programs and the playground’s examples print the same bytes natively and under node; skipped, naming what is missing, without node, clang or wasm-ld); crates/hale-codegen/tests/wasm_import_backstop.rs (T7: every module the wasm tests build imports only the loader’s writers, read from the loader’s source, plus its declared @ffi(“js”) names, or a known-open name from its stated callers (dprintf and fflush, the unabsorbed-violation report, until the loader has a stderr writer); a control module importing an undefined @ffi(“c”) name reported by name; each known-open name still imported; no observation probe emitted for wasm32, against the native build of the same program; skipped, naming what is missing, without clang or wasm-ld)

Spec. spec/decisions.md F.35; spec/ffi.md § The target declaration + stdlib gating; docs/src/systems/webassembly.md

Guarded seams.

• derive_capability_matrix( may be referenced from: crates/hale-types/src/capability.rs ×5, crates/hale-types/src/capability/transport.rs ×1, crates/hale-types/src/capability/laws.rs ×12, crates/hale-types/src/capability/uses.rs ×2, crates/hale-types/src/target.rs ×1, crates/hale-cli/src/shared/options.rs ×1
• derive_capability_uses( may be referenced from: crates/hale-types/src/capability/uses.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1
• target_row( may be referenced from: crates/hale-types/src/capability.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/check.rs ×1

Answers. A deployment as typed rows: root and horizon, component identities, instances and incarnations, resources and allocations, endpoints and routes, hosting and authority, persistence obligations (the habitat, after phase 2).

Inputs. placement; bindings; admitted artifacts; a deployment dialect (later)

Producer. none: reserved, computes nothing.

Consumers. fleet (today’s JSON as an input adapter); dna (the habitat); ui (reserved)

Invariants.

• habitat owns the hosting allocation and its obligations; the tenant keeps its own root and authority
• desired, admitted and observed stay distinct

Missing data. n/a

Spec. RFC #1212, the implementation plan §8; GH #262

Answers. The happens-before order per instance: birth sequence, params open and settle, failure delivery and its execution domain, reclaim prerequisites, drain, restart, teardown.

Inputs. placement (the instance templates: the static towers, replicas apart, and the dynamic sites with their domains and bounds; the domains); handler_routing (the owner’s handler for each child, and whether it restarts); flows (an accepted flow is reclaimed at its run’s end, a resident by its owner’s cascade); bus_graph (which instances subscribe); entrypoint (which main locus is the entry, whose deferred teardown is the main entry’s spine); the declarations each template realizes (run, the closures’ epochs, birth_check, violate sites, accept, on_failure, the params bracket); the decision lines (hale_types::lifecycle::DECISION_LINES) and the inventory rows they name; the runtime protocol (lotus_failure_hold / await / defer_reclaim; a run’s retention, queued or started, lotus_run_cancel_only / lotus_run_cancel_queued and deferred storage release); the delivery’s domain (lotus_failure_post: the owner’s domain recorded where its params open, a delivery off it posted there and awaited, its cell’s hold on the child; lotus_pinned_join and the pool join’s wait for the joined domain’s end)

Producer. crates/hale-types/src/lifecycle/derive.rs · derive_lifecycle

Also owned. crates/hale-types/src/lifecycle.rs · LifecyclePlan; crates/hale-types/src/lifecycle/trace.rs · Expected; crates/hale-types/src/lifecycle/project.rs · expected; crates/hale-types/src/lifecycle/spine.rs · birth_order; crates/hale-types/src/lifecycle/spine.rs · reclaim_order; crates/hale-types/src/lifecycle/spine.rs · cascade_order; crates/hale-types/src/lifecycle/spine.rs · cascade_fields; crates/hale-types/src/lifecycle/spine.rs · recovery_order; crates/hale-types/src/lifecycle/spine.rs · entry_order

Consumers. the lowering view (the snapshot’s plan, carried to the emitters) (crates/hale-frontend/src/snapshot.rs · view.lifecycle = Some(lifecycle)); codegen (the process rows of every teardown spine, in the plan’s order as the target’s cells select them: a spine’s head before its frame’s pre-drain, the pre-drain and the rows after it in a fn main exit’s flush) (crates/hale-codegen/src/codegen.rs · emit_process_rows); codegen (fn main’s three exits, the fall-through, the test failure and return, through one helper: the exit spine’s process rows, the frame, the process exit tail C24) (crates/hale-codegen/src/codegen.rs · emit_main_exit); codegen (a main-locus entry’s teardown in the plan’s order, LifecyclePlan::entry_order: the eager spine and the frame flush emit its head before its own pinned joins, the flush ahead of the first of them wherever its entry order puts it, and refuse a cascade the plan places earlier) (crates/hale-codegen/src/codegen.rs · head_before_pinned_joins); codegen (emission reads the order, spine by spine, through LifecyclePlan::spine); codegen (the restart and the resume: _restart, _resume) (crates/hale-codegen/src/locus/restart.rs · define_restart_fns); closures (the event alphabet); transitions (reserved); deployment (reserved)

Invariants.

• each order the emitters read (birth, reclaim, cascade, recovery, process, entry, readiness) is computed once per plan by the spine index (SpineIndex, built in build_resolved beside the plan), never per literal or per teardown: the plan’s own readers give the same answers by the same per-instance code, lifecycle_plan.rs holds the two equal over every corpus plan and their pair sets equal to a reference, and birth_spine_ir.rs bounds the readers’ passes over a plan by a constant
• equivalent parent execution contexts are represented once per owner (instantiating domain, queue domain, handler state); occurrence bounds still sum every owner, and domain claims retain every distinct context without enumerating ancestry paths
• a handler runs on its owner’s domain (decision L0-1, L5’s fourth part): a failure raised off it is posted there with the copied violation and the child retained, and the failing thread waits for the handler’s return servicing its own queue; the domain runs it wherever it services its queue (main’s drain, a pinned mailbox’s drains and yields, a pool worker between cells, every servicing wait, and the pinned and pool joins, which run nothing else); a domain that has ended runs nothing more, and a delivery to it runs where it was raised; the owner’s reclaim waits for the posted delivery and for the failing cell’s hold on the child, except that it never waits for a delivery only its own thread can run: reached inside a handler for a child whose delivery is held for that thread (a replaced failing sibling), it follows that delivery, after the running handler returns; wasm32 keeps the in-place call (failure_delivery_domain, the matrix’s C36 cells, jp_late_failure_*, l08_sibling_replaced_kept, cascade_model’s phases 3 and 4)
• a spec/implementation disagreement is settled as a named decision, never by extraction picking a side
• an obligation is keyed by its source site (the declaration and P1’s construction template); the runtime mints the instance and its incarnation, the table never does
• every obligation ends in exactly one of its named terminal alternatives; lifetime (what stays alive until which event) and progress (what makes it reach a terminal) are separate fields
• each rule says whether it is shipped, adopted, known open at an inventory row, or pending on a named condition
• the runtime’s protocol is checked by its trace, not trusted: a trace build reports the hold, the settle and each held delivery, and the trace oracle holds them to the plan’s edges (delivered after the owner’s settle, before its birth), with negative controls that remove or reorder a step and fail it, over the lifecycle fixtures, every runnable example (its departures named in the corpus oracle’s PLAN_KNOWN_OPEN, none today: the closure with no epoch clause whose dissolve-epoch rows the producer did not derive is closed, C37, and so is a statement-position literal’s teardown, which the plan now orders before the end of the lifecycle body whose statement built it as well as before its owner’s reclaim, so a run that exits inside that teardown owes nothing that waits for the body’s end, C13) and the lifecycle matrix’s program cells (a sample of 60 by default; all 121 under HALE_MATRIX=full)
• a run posted to a pool ends in exactly one of decision line 19’s named terminals (L5): it is retained against its child’s teardown, whose Reclaim begins by canceling the child’s queued runs (lotus_run_cancel_only, past the reclaim latch on every reclaim path, before storage release), so a run queued on any pool finds its child whole or ends NotStarted(Acknowledged), and physical release waits for the child’s started runs, each holding its child and owned descendants from admission until it returns; a queued main-thread handler defers physical release until it returns, while drain and dissolve remain before replacement construction; child Reclaim completion precedes owner Reclaim completion; a post refused at shutdown ends NotStarted(Shutdown(PoolShutdown)), a cell the pools’ teardown frees NotStarted(Shutdown(PoolTeardown)), and a run post that cannot allocate aborts; under replay the ordering gate drops a canceled run before comparing it with the recording and holds a live one without admitting it, in a hold buffer that is its consumer thread’s and is freed at the thread’s exit
• one plan per snapshot, over the placement table’s instance templates: a held row and the rows projected under it are their source’s and owe nothing of their own, a hole owes nothing, and a dynamic literal’s own fields are instances of their field literals in its domains, a field literal reached through several constructions of its owner’s declaration one template that keeps each one’s owner, domains and bound (its bound their sum, a nested field’s the product of its owner’s with its own placement), and a body or accepted literal one template whose owners are every template of its enclosing locus, each occurrence on the domain its enclosing occurrence runs it on (its bound the table’s, which covers every enclosing scope); no check builds the plan
• a failure’s rows are guarded, one set per source an instance can raise (a birth-epoch closure, the birth_check, a violate in run(), in a handler or in drain(), a dissolve-epoch closure, a closure with no epoch clause among them: its epoch is ClosureDecl::epoch’s, the rule the checker and lowering read): its delivery in place, the held alternative where the owner’s params can still be open, and the recovery decision and the restart, performed or refused under teardown; a path through the plan picks one
• existence, each edge and each domain claim carry their own rule and status, so a row shipped to exist can carry a claim known open or pending (line 3); a domain is claimed only where the placement table and the rule resolve one for every occurrence: one domain, or the set where a template’s occurrences are built under parents on different domains (each occurrence held to one of them), never one parent’s alone
• a failure’s delivery claims the owner occurrence’s domain, shipped (decision L0-1: in place there, or posted there and awaited), and a held one the thread settling the owner, a pool-placed owner’s worker included (line 1); where the owner’s domain has ended before the failure is raised (a static instance’s drain or dissolve on main after the pool join or its pinned anchor’s join, under a pool worker or a pinned thread) it claims the raising thread under the shutdown rule (join progress); the joins’ progress is shipped (C18, R20); a queued run’s cancellation claims the reclaiming thread (R19a: main for a static instance)
• the plan the trace oracle holds a lifecycle fixture’s, a matrix cell’s or a runnable example’s run to is the producer’s for its program, rendered along the run’s path (lifecycle::project::expected): no hand-written expectation stands beside it, the negative controls’ own plans aside and the hand-written plans of the fixtures the producer does not derive yet (UNDERIVED: a field replaced while its failure is posted, C29), and a run’s known departures are named per inventory row in the known-open tables
• occurrences of one declaration whose runs end differently in one execution are counted from the run’s path: a teardown’s cancellation is owed once per run the path cancels however many templates owe it, edges out of it are held only where every occurrence is canceled, and a run that never started is held to no domain (its not-started end is named where it was canceled or refused); a main locus built more than once enters its eager spine at each teardown, so those process rows name the literal (Obligation::per_occurrence_of) and are owed once per occurrence, and the first join owes no later construction’s run
• a row whose every terminal is a not-started one is owed by no subject: a restart refused under teardown (RD, C42), a run a resumed locus does not declare (line 13, C48)
• a pinned or pool anchor’s params initialize and settle on its own domain (C49/C50); each static nested field’s instantiating domain follows that initialization, and the anchor’s own birth runs there too (line 3, L4 5: a pool anchor’s as a second job its instantiating thread posts after its registrations and waits for, the held decision staying on that thread; claimed there only where the main locus is built once, since a later construction’s posted birth finds the pools joined and runs in place on the instantiating thread); a nested run inside a pool init is inline and owes no queue admission or queued-run cancellation
• an emitter reads its spine’s obligations for an instance template from the plan (LifecyclePlan::spine, birth_spine, birth_order, reclaim_order, cascade_order), on the path no failure takes, each after every row its entry edges reach and ties in the producer’s order; the steps it emits for a spine are exactly those, which the trace build shows per instance and spine over every fixture program with exact named departures in SPINE_KNOWN_OPEN (C29’s alternate field-replacement spine remains to be derived), the Reclaim on the spine the plan holds it on and a run’s Cancellation on its Reclaim’s, read on the shutdown path (shutdown_spine)
• the process edges are the plan’s (L4 3): the producer states every teardown spine’s process rows (the eager main locus’s C13, the deferred main entry’s C19, fn main’s fall-through, test-failure and return exits C21–C23) as the ingress quiesce, the wait-abort and, with pools, the pool join with its progress, the exits then their frame’s pre-drain (without pools the pre-drain before the wait-abort), and the edges between them; emission reads that order (process_order) and the capability matrix selects which rows a target emits (line 16); a run takes one of fn main’s exits, and a main locus a fn other than main builds owes its head before fn main’s exit
• one teardown order on every spine (L4 5): a main locus’s head (the ingress quiesce, the wait-abort, with pools the pool join) precedes the join and the drain of every pinned anchor its teardown joins, with a pool or without (line 7’s edges, which entry_order reads), so the deferred spine’s flush emits the head before the first of the entry’s own pinned joins (C14) as the eager spine does; a pinned field’s join precedes its owner’s drain (line 12), and a root handed back to its caller keeps its pinned fields’ join records in their instances and joins them in its own cascade, wherever the caller ends it, the building frame’s flush owning the join only when that frame owns the root at its exit (C52)
• a Run is owed exactly where lowering calls run() (C53): the producer and lowering read one test, lifecycle::run_is_called over lifecycle::body_is_empty (a body, or a flow’s run, whose wrapper reclaims it), and a pinned locus’s thread takes the step whatever the body; an empty run() { }, written or not, owes none
• the birth spine is emitted from the plan (L4 1): an instantiation’s steps from params settle to the run’s start (accept, registration, birth() with its birth-epoch closures and birth_check, readiness, the run’s start) come in the order birth_order reads from the plan’s rows and edges for its declaration, the registrations on the instantiating thread and the rest there or, for a pinned locus, on its thread; the emitter refuses a plan that puts a registration after the birth; a pinned locus’s birth_check runs on its thread before run() (C38)
• an instance’s header is initialized before anything can reach it (C54, a classified correction): its children list, restart, quarantine and drain latches, recpool fields, failure route, owner links, masks and reclaim slots, and a handed-back root’s join records for its pinned fields’ replicas (C52, cleared before any replica’s literal writes its own) are stored right after its arena, before the owner singleton publishes it, before its pointer reaches the observer, the runtime or a child, and before any param is built, on every instantiation path, the cross-pool create cell’s included (emit_instance_header, lowering’s own preamble, which the plan does not name); nothing after the params stores a header field again, so a child the params bubble to it stays accepted and is torn down with it; a restart keeps the header but the two latches the failure raised (C42)
• readiness is the plan’s (line 6): delivery to a subscriber is eligible once its birth and checks complete; what is published to it before is parked in order, never dropped (including a pinned subscriber, whose mailbox remains current for already-born nested subscribers), bounded at the queue’s cap for a publisher on another thread, and dropped with the subscriber if it is quarantined first; no direct call delivers to it during its birth (a rewritten send keeps its exact receiver and uses its registered route while that receiver is held, and a baked direct publish uses runtime dispatch while any window is open)
• the reclaim spine is emitted from the plan (L4 2): every teardown funnels into emit_locus_arena_destroy, which emits an instance’s reclaim in the order reclaim_order reads for its declaration: the owned children’s reclaims before physical release (line 14), guarded logical entry, cancellation of still-queued runs, waiting for admitted runs and deferred descendants in the retained release callback (line 19, R19), the arena’s release, then the struct’s; the emitter refuses cancellation before entry, a wait before cancellation, or any storage release before its dependencies; a field owned through a pool-placed owner’s params runs and subscribes on that pool (line 3, C12)
• the dissolve cascade is emitted from the plan (L4 2): an owner’s teardown around its fields comes in the order cascade_order reads (the fields’ drains, the owner’s drain, its dissolve, the fields’ dissolves, the reclaim), over the fields in the order cascade_fields reads (declaration order, line 12); a field typed by an interface or a perspective drains before its owner like any field (its slot holds the impl’s drain and rest halves, C32), and a pinned locus’s thread drains its fields before its own drain() (C9)
• restart and resume are emitted from the plan (L4 4): a restart’s steps come in the order recovery_order reads from the plan’s rows and edges for its declaration (the recovery decision once the handler has returned, the Restart after its completion (line RD), then the incarnation the restart begins: its rows owed once per incarnation, birth() with its birth-epoch closures, then run() only where the template declares one (line 13, C48)); a restart tears nothing down, the instance is the same one (C42); __restart_<L> emits the entry and the birth, the decision and the run stay with the caller on the spine that decides, and __resume_<L> starts a run only where the plan owes one (a flow’s run end, its reclaim, aside). Departures the trace shows are named in SPINE_KNOWN_OPEN: a held run() failure’s phase-0 resume the producer does not derive (C43), a held failure’s restart performed by the resume at settle where the producer holds it on PoolRun (C42), and a restart asked for under the owner’s teardown performed (C42, the adopted refusal’s mechanism L5’s)

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · lifecycle_order_a_view_without_the_plan_is_refused; total: no template of a declaration in the plan (one only the stdlib or an imported seed builds) means it reads each spine’s order from every template of the plan, then in the producer’s order, and owes no readiness

Focused tests. crates/hale-types/src/lifecycle/derive.rs (shared ancestry regression); crates/hale-codegen/tests/reclaim_spine_ir.rs (reclaim ordering through retained callbacks, contract teardown halves, pinned field drains and declaration order); crates/hale-codegen/tests/birth_spine_ir.rs (the birth spine’s IR per shape: a root child, a nested child, each replica, a pinned child with its birth_check before its run, a pool-placed child born on its pool’s worker as a posted job, a cross-pool bubble accepted before birth); crates/hale-codegen/tests/header_before_params.rs (the header before the params: children a params default bubbles to a main locus, a field owner in its owner’s arena and a pool-placed owner stay accepted and are torn down; a dirtied stack is never read; a pinned owner’s on_failure at settle reads its own latch clear); crates/hale-codegen/tests/restart_spine_ir.rs (the restart and resume spines’ IR per shape: a root child, a nested child, a pinned child, each replica, a pool-placed child, restart_in_place under a generic supervisor, a locus with no run() resumed without one); crates/hale-types/tests/lifecycle_plan.rs (a_restart_reads_decision_entry_birth_then_run); crates/hale-codegen/tests/topic_phase2.rs (a_births_own_publishes_are_delivered_after_it_in_order; sends directly in birth or in its helpers retain receiver identity and wait for readiness; pinned birth bursts and managed payloads run under ASan); crates/hale-types/tests/lifecycle_plan.rs (the plan through the snapshot: demanded once and built by no check; its laws over every corpus program the snapshot scopes, edges naming its own rows and acyclic on events, birth and teardown owed once per template, every line a decision line, every delivery to an owner of known domain naming its domain; the rows lines 1, 3, 7, 12, 13, 14, 18, 19 and RD are about; a cross-domain delivery’s claim, posted or under the shutdown rule; a main locus built twice; started-run retention through physical reclaim; statement-position subscribers torn down at frame exit); crates/hale-codegen/tests/lifecycle_flow.rs; crates/hale-codegen/tests/reclamation_spine.rs; crates/hale-codegen/tests/main_locus_deferred_pool_join.rs; crates/hale-codegen/tests/teardown_pinned_join_order.rs; crates/hale-codegen/tests/frame_flush_ir.rs (the frame flush per fn main exit, with and without a pool: the head’s rows, then the pre-drain and the rows after it, the entries subscription-less pinned first then reverse push; a deferred main entry’s head before its pinned joins, in a fn other than main and in fn main’s frame; a returned root’s pinned field joined by its owner’s teardown in the caller, and the control a frame keeps; another fn’s flush pre-drains and aborts no wait); crates/hale-codegen/tests/reclaim_cancel_ir.rs (queued cancellation precedes the storage callback on every spine, and its hold wait dominates physical releases); crates/hale-codegen/tests/replay_canceled_run.rs (a canceled run replays clean; a held run keeps its retention; the hold buffer is freed by each thread that held, under ASan with no suppression); crates/hale-types/src/lifecycle.rs (the schema’s laws: every decision line binds a kind, the Pending lines are the named ones, the doc table is the data); crates/hale-codegen/tests/lifecycle_fixtures.rs (a fixture per decision line under tests/fixtures/lifecycle/; KNOWN_OPEN pins today’s outcome where it differs from the adopted one; the trace oracle holds each run to the producer’s plan for the fixture’s program, rendered along the run’s path and its line’s known-open rules, the line-19 fixtures’ included, or, for a fixture in UNDERIVED (one field replacement, C29), to its hand-written plan; TRACE_KNOWN_OPEN names today’s departures, CONTROLS fail it; every_spine_emits_the_plans_obligations_in_order holds each instance’s emitted steps on the eight instance spines (the deferred entry’s and the deferred main entry’s among them) and reclaim/cancellation on every spine to the plan’s order); crates/hale-types/tests/lifecycle_plan.rs (every_declaration_reads_one_birth_order_over_the_corpus, the_reader_orders_each_spine_by_the_plans_edges); crates/hale-types/src/lifecycle/trace.rs (the trace’s parser and oracle); crates/hale-codegen/tests/corpus_oracle.rs (corpus_traces_keep_the_lifecycle_laws: every runnable example, traced, held to the trace’s laws and to its program’s plan along its run’s path, the path stated where the run is not the default one (a failure, a branch not taken, a default its literals replace); PLAN_KNOWN_OPEN names today’s departures); crates/hale-codegen/tests/lifecycle_matrix.rs (failure phase × tree position × domain, a generated program per cell held to its outcome, the producer’s plan for the program rendered along the cell’s run, ASan on the sample and the let-bound differential; KNOWN_OPEN names today’s failing cells, none since the producer claims the shutdown rule’s domain; HALE_MATRIX=full runs every cell); crates/hale-codegen/tests/target_lifecycle_cells.rs (the five teardown spines on both targets: each owes what its target’s cells select, in the order the plan’s process rows state, before the cascade; the call counts pinned per shape, variant and target); crates/hale-codegen/tests/failure_delivery_domain.rs (a pinned child’s handler on its owner’s thread, outside the owner’s window; an owner’s reclaim never under a delivery in flight; a pool-placed owner’s held and posted deliveries on its worker, by thread id; all under ASan in both dispatch modes); crates/hale-codegen/tests/cascade_model.rs (the GenMC model compiled with every control, run natively once: the in-place control fails the domain assertion)

Spec. spec/runtime.md (failure delivery; pool join rule b); spec/runtime.md § Lifecycle obligations (the decision lines, adopted and shipped told apart); spec/runtime.md § The lifecycle trace (a debug aid, not a contract); spec/runtime.md § Lossless recording mode (the replay hold and a canceled run); spec/semantics.md § lifecycle

Guarded seams.

• derive_lifecycle( may be referenced from: crates/hale-types/src/lifecycle/derive.rs ×1, crates/hale-frontend/src/snapshot.rs ×1
• process_order( may be referenced from: crates/hale-types/src/lifecycle/spine.rs ×3, crates/hale-codegen/src/codegen.rs ×1
• entry_order( may be referenced from: crates/hale-types/src/lifecycle/spine.rs ×3, crates/hale-codegen/src/codegen.rs ×1
• emit_main_exit( may be referenced from: crates/hale-codegen/src/codegen.rs ×4
• recovery_order( may be referenced from: crates/hale-types/src/lifecycle/spine.rs ×2, crates/hale-codegen/src/locus/restart.rs ×1

Answers. Whether the program can ever have a bus cell in flight, so drains can be elided.

Inputs. the user program’s declarations (topics, perspectives, bus and bindings blocks, accepts); the names the user program spells (hale_syntax::names); the stdlib’s bus-taint column (which std:: namespaces reach bus surface)

Producer. crates/hale-types/src/bus_inert.rs · bus_inert

Also owned. crates/hale-types/src/bus_inert.rs · bus_tainted_namespaces; crates/hale-syntax/src/names.rs · for_each_spelled

Consumers. the resolved program (a row of the lowering view, over the user program before the stdlib merge) (crates/hale-types/src/resolved.rs · bus_inert::bus_inert(); codegen (drain elision: the row, read) (crates/hale-codegen/src/codegen.rs · resolved.bus_inert); codegen (crates/hale-codegen/src/bus/runtime.rs · emit_bus_drain)

Invariants.

• a drain elision is a conclusion of structural rows, never of a rendering: the declarations the user program carries, and the names it spells (hale_syntax::names, an exhaustive walk) against the stdlib’s bus-taint column (bus_tainted_namespaces, a fixpoint over the stdlib’s declarations by the same walk); lowering reads the verdict (LoweringView::bus_inert) and derives none
• the test is by name and over-approximates (a local spelled like a tainted namespace keeps the drains); a query over the message graph that follows which stdlib subscribers a program actually reaches would elide more, and is a separate change with its own shadow

Missing data. total: no absence is possible: the verdict is a value of every view, and false keeps every drain

Focused tests. crates/hale-codegen/tests/drain_elision.rs; crates/hale-codegen/tests/log_routing.rs; crates/hale-types/src/bus_inert.rs (the_verdict_reads_declarations_and_names)

Spec. spec/runtime.md § drain

Guarded seams.

• bus_inert( may be referenced from: crates/hale-types/src/bus_inert.rs ×2, crates/hale-types/src/resolved.rs ×1

Answers. The laws that replaced lowering’s own refusals of rules the spec states.

Inputs. the AST; the placement table; the binding rows; the ownership graph; the typed-body table’s omitted_args; the entry row

Producer. crates/hale-types/src/lowering_laws.rs · lowering_laws

Consumers. the check (every verb and the LSP) (crates/hale-types/src/check.rs · lowering_laws); the harness’s lowering view (Config::harness), which is not gated on the check (crates/hale-frontend/src/snapshot.rs · lowering_laws); codegen (the backstop: a value use of a literal the plan posts to another thread, which the cross-pool value law judges, refused as its missing judgment) (crates/hale-codegen/src/locus/instantiation.rs · emit_crosspool_bubble_spawn)

Invariants.

• a law is judged once, with a span
• each law here is a registered rule (rules 6, 17 and 18, and the structural table’s module-nested entry, cross-pool spawn as a value and self-containing locus), run as a law::Law whose finding is a law::Violation; a related location a finding carried before is a witness step, in its order, so the rendering is unchanged (phase 4, W5)
• lowering judges no shape a law in lowering_laws covers: the check runs the laws among its rules, and the harness’s lowering view demands them before it lowers, so those refusals reach no entry point unlocated (C7)
• rule 6 is judged per pinned instance, by the locus it realizes (an override literal’s, a stdlib locus’s), over the placement table’s rows: a pinned entry’s field and each replica, and an adapter inline in bindings { } (C7, 1); its finding is a law::Violation whose witness is the walk’s chain, each step located: the entry that runs the instance pinned (the placement entry, or the binding entry), the declaration the instance realizes, and the conflicting member (the accept, or the closure’s assertion), a stdlib declaration’s steps in the stdlib’s space (phase 4, W2)
• rule 17 is judged per root construction over the placement table: a literal of the root declaration (as resolved) written inside a loop body, whose template holds a row a pinned entry decides (C7, 2)
• rule 18 is judged per entry of the placement table’s root over the inits its constructions supply, or the params default when one leaves the field or none builds the root (C7, 3)
• a cross-pool spawn is judged from the ownership graph’s resolved birth rows and bubble plan: bare_statement records whether that literal is a discarded expression statement; a value use in a locus’s own member bodies (birth checks and closure assertions included; an argument default’s literal is not one, it is judged where it is expanded) is refused at the literal. The law does not rewalk literals or join by their written final segments (C7, 4; C3)
• the cross-pool value rule holds at every expansion of a default, through one relation, the ownership graph’s expansions: each literal lowering builds from a default, with the locus it is lowered under (the plan’s key there) and the root in that locus’s own body that starts the expansion. A params default is expanded where a literal leaves its field unsupplied; a fn’s or a locus method’s argument default at each call that leaves the argument out (omitted_args; a call that supplies it expands nothing), so it is judged per invocation, in the caller’s locus; chains of either kind are followed, and a literal the plan posts to another thread expands no params default under its context. A params default’s literal is refused at the literal, once per context; an argument default’s at the root, once per root, so a caller on the owner’s thread is not refused. A const’s value and a type’s field default are lowered at every use under a locus no row names, so they are refused at the position whenever some locus’s plan posts the child (C3 rest and its review)
• lowering’s backstop is an error, not a judgment: a cross-pool construction in value position that reaches the post (emit_crosspool_bubble_spawn, whose instance is born on the owner’s thread and has no value here) is a CodegenError in every build profile, located at the literal, naming this law as the judgment that is missing; it never lowers a null value (C3 rest, the review of #1351)
• self-containment (GH #813, #870) is judged over every locus’s params defaults, keyed (locus, supplied fields) as lowering expands them, through every literal anywhere in a default (each branch of an if or match, each statement of a block) and every fresh-factory product: a cycle is refused at the param that closes it, and lowering keeps no re-entry guard (C7, 5)
• decision 2’s refusal (F.40 phase 3, L4): a seed whose only main locus is module-nested has no entry (EntryRow::refused) and is refused once, at that locus’s name, so the harness lowers no program whose root is not the entry; it is one more diagnostic, and the other laws still judge that main over the table it seeds

Missing data. required: a missing row is a CodegenError, pinned by crates/hale-codegen/tests/missing_rows.rs · law_backstops_a_value_use_the_law_did_not_judge_is_refused_at_the_literal

Focused tests. crates/hale-types/tests/placement.rs; crates/hale-cli/tests/check_lowering_laws.rs (hale check and hale build); crates/hale-cli/tests/nested_main_transition.rs (decision 2’s refusal at hale check and hale build); crates/hale-frontend/src/snapshot.rs (the_lowering_view_carries_the_entry_row: the refusal blocks the harness’s view too); crates/hale-codegen/tests/harness_lowering_laws.rs (the harness, which skips the check); crates/hale-codegen/tests/deferred_slot_per_iteration.rs (rule 17 at the harness); crates/hale-codegen/tests/placement_factory_default.rs (rule 18 at the harness); crates/hale-types/tests/ownership_graph.rs (the cross-pool spawn law, every expansion context of a default included); crates/hale-types/tests/self_containing_locus.rs; crates/hale-codegen/tests/self_containing_locus.rs

Spec. spec/semantics.md rules 6, 17, 18 and § accept bubbling; spec/types.md § A locus may not contain itself by value; GH #813, #870, #876

Guarded seams.

• emit_crosspool_bubble_spawn( may be referenced from: crates/hale-codegen/src/locus/instantiation.rs ×2

Answers. The canonical semantic model of a checked bundle: fifteen entity tables, seventeen relation tables, holes, capabilities, provenance (GH #476).

Inputs. a checked bundle; top_scope; bus_graph; ownership; handler_routing; placement; effects; alloc_summary; topics; bindings; dispatch (the snapshot’s plan, held projected: no model table hashes it)

Producer. crates/hale-types/src/model_builder.rs · derive_application_model_over

Also owned. crates/hale-types/src/model_builder.rs · ModelInputs

Consumers. demand (every verb and the LSP: the claims, over the snapshot’s scope and graphs) (crates/hale-frontend/src/snapshot.rs · derive_application_model_over); topology (hale check’s artifact and both gates: the snapshot’s model) (crates/hale-cli/src/verbs/check/run_impl.rs · dump_topology_over); model dump (the check’s snapshot) (crates/hale-cli/src/verbs/check/run_impl.rs · demand_model); the build identity: the model hash and the obs ids (build, run, replay: the snapshot’s model) (crates/hale-cli/src/shared/options.rs · demand_model); fleet (admits the artifact, never the model)

Invariants.

• one constructor; no artifact → model, no plan → model, no hand-authored model
• hale-model is rebuilt on hale-graph (phase 1.1a): its seed, source and provenance ids and its provenance store are the graph core’s, re-exported under the model’s paths; its canary allows that one dependency and no other
• demand-gated: a no-claims check builds no model (GH #476 criterion 1); demand_gate.rs pins it as per-family accounting over Snapshot::builds (the demand family): the LSP’s diagnostics path builds none, hale check of a program with claims builds one, which --dump-model reuses
• the model builds none of the families it reads beside the program (2.3): the scope with its topic rows, the bus graph, the ownership graph, the handler rows, the effect rows (with the stdlib-merged summary their walk read), the form rows and the placement table arrive as ModelInputs, each demanded once from the snapshot over the checked programs; the allocation summary it still re-runs for itself is listed under its family
• the arrangement is the placement table’s rows projected, under three identity contracts kept apart: shape identity (the arrangement is outside the shape half, so no change to it moves shape_hash); observation entity ids (they stamp subjects, locus declarations and the deployed root’s bindings, never instances); and arrangement-instance correspondence (LocusInstanceId is the index in path order, stable across no change of the arrangement; a consumer joins instances by path, and a replica index is the replica row’s own, never a descendant’s)

Missing data. an unknown is a hole with a stated policy

Focused tests. crates/hale-types/tests/demand_gate.rs; crates/hale-model/tests/architecture.rs; crates/hale-types/tests/topology_projection.rs; crates/hale-types/tests/model_arrangement.rs (the arrangement’s three identity contracts, each pinned against the build before the switch)

Spec. spec/model.md

Guarded seams.

• derive_application_model( may be referenced from:
• derive_application_model_over( may be referenced from: crates/hale-types/src/model_builder.rs ×1, crates/hale-frontend/src/snapshot.rs ×1

Answers. Every user law: lowered claim rows, the judged verdicts over the model and evidence, constitution identities, and the artifact’s law account.

Inputs. model; claim and constitution declarations; evidence (certificates, budgets); effects

Producer. crates/hale-types/src/judgment.rs · claim_law_diags_over

Consumers. check / verify; admission (hale topology graph, hale fleet: an artifact’s law account is validated against itself, with the family’s own functions; it recomputes the law digest and the evidence inputs digest, checks every reference against the artifact’s catalogs, re-renders every stated form with the model’s spelling (hale_model::claim_form) and recomputes a row’s verdict and the document’s with the model’s aggregation (certificate_row_verdict, document_verdict); its decoder is the artifact schema’s reader, since a payload carries no model ids and cannot rebuild a ClaimIr, held to the emitter by a round trip over every artifact the corpus emits, law_account_round_trip.rs, F.40 phase 4, A5) (crates/hale-cli/src/topology_law.rs · validate_law_account); the check’s law-selection diagnostics (the snapshot’s selection, handed in) (crates/hale-types/src/check.rs · laws.diags); the check’s laws stage (judged over the snapshot’s model, after its typing stage; its lowering reads the snapshot’s selection) (crates/hale-frontend/src/snapshot.rs · demand_laws); topology (law section: the law rows, the constitution identities projected from the adoption, and the environment label, all the snapshot’s selection, handed in) (crates/hale-cli/src/verbs/check/run_impl.rs · demand_law_selection); check –matrix (each pair’s identity comparison: the roots its snapshot’s selection adopted, LawSelection::identities, the projection the artifact reads; a pair the check refuses has no snapshot, so no constitution of its takes part) (crates/hale-cli/src/verbs/check/matrix.rs · adopted_roots); fleet; dna (dna_law.rs wording); model diff

Invariants.

• law selection runs once per snapshot (F.40 phase 4, A2): the law_selection cell (Snapshot::demand_law_selection) selects over the programs after the sequence, for the configuration’s environment (its label and the constitutions it injected, passed as data, never a binding on the thread), and the check’s selection diagnostics, the laws stage’s lowering and the artifact’s law rows, constitution identities (LawSelection::identities, a projection of the adoption) and environment label read that one selection, as does the environment matrix’s identity comparison, from the snapshot its pair’s check read (F.40 phase 4, A3: a pair loads its seed once, and a pair the check refuses, which has no snapshot, compares nothing); it is not gated on the typing, so a program that does not typecheck still answers it; a bundle no snapshot holds selects once per entry (bundle_law_selection)
• structural compiler laws are functions over family rows that the check runs, not queries over the model (F.40 phase 4, decision 3); their shared finding is law::Violation (crates/hale-types/src/law.rs): a registered rule’s RuleId, the span, the message, and a witness of located steps, made a diagnostic by Violation::into_diag alone, each step a related location with its note (W2); the judgment path stays for user claims (final direction)
• a registered rule without an evaluator fails the compiler’s own build
• a non-holds verdict is never silent
• admission evaluates no law; it refuses an artifact whose sections disagree (spec/verification.md)

Missing data. an unknown is a hole with a stated policy

Focused tests. crates/hale-types/tests/claim_diags_snapshot.rs; crates/hale-cli/tests/law_selection_reaches_the_artifact.rs; crates/hale-cli/tests/law_account_round_trip.rs; crates/hale-cli/tests/dna_law.rs; crates/hale-types/tests/one_reachability_engine.rs

Spec. spec/verification.md § Claims; spec/model.md § Adding a judgment family

Answers. A named query over the tables: a node selector, a relation set and an adequacy policy, rendered by a backend (hale ui, after phase 2).

Inputs. the resolved program’s tables; a view declaration (its own surface)

Producer. none: reserved, computes nothing.

Consumers. ui (reserved); bundle (reserved)

Invariants.

• a view is a query, not a claim: it yields a projection with an adequacy verdict
• adequate_for(RelationSet): a view may not show an absence its relations cannot see; a hole renders as a hole with its reason

Missing data. an unknown is a hole with a stated policy

Spec. RFC #1212, the UI comment

Answers. The identity of every semantic site in a snapshot: (seed, index), minted after the entry point’s desugars with the bundle’s source map, and again in the resolved-program step (numbered over the user program before the intra-locus rewrite, so the sends it records are numbered on every path, and minted over the merged program with the bundle’s seeds and a named seed for the bundled stdlib), idempotently (one numbering; a later mint numbers only what an earlier one did not see), with reliable provenance; and which declaration each use names (binding_of), resolved once by the mint.

Inputs. seed_loading; desugar_sequence

Producer. crates/hale-types/src/snapshot.rs · mint

Also owned. crates/hale-syntax/src/sites.rs · SiteKind; crates/hale-types/src/snapshot.rs · resolve_uses; crates/hale-types/src/snapshot.rs · declaration_of; crates/hale-types/src/snapshot.rs · number

Consumers. every table; the shadow facility (compares through an explicit correspondence, never raw id equality); lsp (a later incremental future); the resolved program (codegen’s input is minted over the merged program)

Invariants.

• addresses are not identities (declarations are cloned); spans are not (the stdlib’s coordinates overlap user files; desugars share spans)
• snapshot-local uniqueness and provenance are the requirement; persistent identity across editor revisions is a separate problem
• canonical ids need real equality and hashing; the AST’s structural NodeId equality stays separate
• the identity’s types are hale_graph::ids (SeedId, SiteId; phase 1.1a); hale_types::snapshot::mint numbers every site the AST walk hale_syntax::sites reaches with one counter: after the entry point’s last desugar, and again, idempotently, in the resolved-program step over the merged program, numbering only what an earlier mint did not see (phase 1.1b); before the intra-locus rewrite that step only numbers the user program (snapshot::number: the rewrite moves a send’s id onto its call and records it), which makes no snapshot of it; every entry point calls it after its last desugar with its source map and the bundle carries the result (every verb and the LSP through the snapshot’s load, the test harness through Snapshot::from_program, with no source map); the lowering view mints with the bundle’s seeds, the stdlib’s sites under the named seed snapshot::STDLIB_SEED (its spans overlap the first file’s); a generated site records the desugar that made it (Snapshot::origins); codegen’s generic instantiation keeps the template’s id, and the F.39 pre-pass numbers nothing: an unminted Struct or Call is an error
• every identifier expression is a Use site and every name a declaration with no site of its own binds (a fn’s or a hook’s parameter, a match pattern’s binding, a tuple let’s name, a shm_write binding) a Binder site, their ids on their Idents (use-site identity, phase 2)
• binding_of is one resolution per use, keyed by identity, never by name or span: the mint resolves each Use site, and each Assign site’s head, to the Let, For or Binder site it names under the checker’s scoping (check::ScopeStack), once per snapshot (the load’s, the lowering view’s, the bundled stdlib’s analysis copy’s once per process: demand_gate pins it); a use that names no local binding has no row; every reader asks Snapshot::declaration_of and resolves nothing itself, and every entry point mints
• a check of a bundle no entry minted (Bundle::new over parsed programs, a library caller’s or a test’s) mints a copy of its programs once, with its source map, before any family is derived (with_identities, the no-snapshot adapter of check::check_bundle): its bus graph’s sends and the intra-locus rewrite’s relation, whose own numbering keeps those ids, name a send by one id, so rule 10’s join answers on that path as on the snapshot’s; a send with no id reaching the join is refused as an internal failure naming the send, never judged as queued
• an analysis row (FnKey) is its declaration’s identity: decl, the site the universe that minted it numbered (the stdlib’s analysis copy is its own universe), for every fn-like member (a free fn, a locus method, a lifecycle hook, a mode; a failure handler, a perspective fn, a constant and a synthesized hook as declaration bodies); the (locus, fn) pair is the row’s display name and leads its order. A call reaches a row through the summary’s one resolution (AllocSummary::resolve), and every reader holding a declaration builds its key from that declaration’s site; a monomorph’s rows are its template’s. A key with no identity is a declaration no mint numbered, or frontier’s one fallback for a subscription’s handler the summary holds no row for (C3 rest)
• FunctionId is the model IR’s name-ordered id (spec/model.md law 2: a function row’s id is the rank of its canonical name, and validate’s sorted names hold); the row carries the declaration it is (Function::decl), never rendered and never hashed, and every builder join from an analysis row to its function reads that column (fn_of_site). A name answers only the resolution of author text (a group selector’s member, a claim’s function, an unresolved call’s callee by its shape) and a key no mint numbered: fn_id.get( is the model builder’s and the claim lowering’s alone (C3 rest)

Missing data. a missing required row is a compiler error

Focused tests. crates/hale-types/tests/fn_key_identity.rs; crates/hale-codegen/tests/ownership_reclaim.rs (shadow_return_binding); crates/hale-codegen/tests/owner_table.rs; crates/hale-types/tests/snapshot.rs (each_use_resolves_to_the_declaration_in_scope); crates/hale-types/tests/demand_gate.rs (each_snapshot_resolves_its_uses_once); crates/hale-syntax/tests/sites.rs

Spec. spec/decisions.md F.39, F.40

Guarded seams.

• mint( may be referenced from: crates/hale-types/src/resolved.rs ×1, crates/hale-frontend/src/snapshot.rs ×1, crates/hale-types/src/lib.rs ×1, crates/hale-types/src/stdlib_bodies.rs ×1, crates/hale-types/src/alloc_summary.rs ×1, crates/hale-types/src/sync_inference.rs ×1
• type_expr_identity( may be referenced from: crates/hale-types/src/check.rs ×7
• fn_id.get( may be referenced from: crates/hale-types/src/model_builder.rs ×9, crates/hale-types/src/claim_lowering.rs ×1
• FnKey::method(None may be referenced from: crates/hale-types/src/frontier.rs ×1

Answers. Which families a consumer’s request computes, and in which order: a snapshot owns one load (the programs and their keys, each member’s own program beside the merged one, the source map, the import renames, the config that shaped them, the sequence already run, the mint) and derives each family on request (Snapshot::demand_*: the scope, the checked programs’ bus graph, ownership graph, handler rows and flow rows, law selection, the role rows, the arrangement, the effect rows, the model, the check in its two stages with the effects certificate report its typing produced, the lowering view), each at most once, blocking a family whose prerequisite reported errors.

Inputs. seed_loading; desugar_sequence; snapshot_identity; the config (target, api, api roles, environment, the check’s rules); editor overlays (LSP); a consumer’s request

Producer. crates/hale-frontend/src/snapshot.rs · Snapshot

Also owned. crates/hale-frontend/src/snapshot.rs · demand_entry; crates/hale-frontend/src/snapshot.rs · demand_scope; crates/hale-frontend/src/snapshot.rs · demand_editor_scope; crates/hale-frontend/src/snapshot.rs · demand_bus_graph; crates/hale-frontend/src/snapshot.rs · demand_ownership_graph; crates/hale-frontend/src/snapshot.rs · demand_handlers; crates/hale-frontend/src/snapshot.rs · demand_flows; crates/hale-frontend/src/snapshot.rs · demand_law_selection; crates/hale-frontend/src/snapshot.rs · demand_role_rows; crates/hale-frontend/src/snapshot.rs · demand_arrangement; crates/hale-frontend/src/snapshot.rs · demand_effects; crates/hale-frontend/src/snapshot.rs · demand_effect_certificates; crates/hale-frontend/src/snapshot.rs · demand_model; crates/hale-frontend/src/snapshot.rs · demand_typing; crates/hale-frontend/src/snapshot.rs · demand_laws; crates/hale-frontend/src/snapshot.rs · demand_check; crates/hale-frontend/src/snapshot.rs · demand_lowering; crates/hale-frontend/src/snapshot.rs · from_program; crates/hale-frontend/src/snapshot.rs · SnapshotKey; crates/hale-frontend/src/snapshot.rs · declarations; crates/hale-frontend/src/snapshot.rs · declaration_dependents; crates/hale-frontend/src/dependents.rs · DependencyIndex; crates/hale-frontend/src/snapshot.rs · reusing_typing; crates/hale-frontend/src/snapshot.rs · typing_reuse; crates/hale-frontend/src/typing_reuse.rs · ReuseKey; crates/hale-frontend/src/typing_reuse.rs · plan

Consumers. check (crates/hale-cli/src/verbs/check/run_impl.rs · demand_check); the checker’s rules (the handler rows: duplicate handlers, @supervised; the entry row: rule 1 and rule 9; the placement table: the F.31 rule per instance, the blocking check, pinned-in-a-loop, rule 20’s construction paths; the bus graph: rules 7, 9 and 10, and the role law’s sites; the ownership graph: rule 20; law selection: the law-selection diagnostics; the role rows: the role rules; the sequence’s surface: the api entry’s rules), demanded before the check runs; the effect rows’ purity column for a codec binding, demanded only when one reaches the assertion (crates/hale-frontend/src/snapshot.rs · CheckInputs); topology (--dump-topology, --check-topology, --check-topology-shape: one artifact of the snapshot’s model) (crates/hale-cli/src/verbs/check/run_impl.rs · dump_topology_over); the model dump (--dump-model: the check’s own model when it judged a law) (crates/hale-cli/src/verbs/check/run_impl.rs · demand_model); the build identity (build, run, replay: the model hash and the obs ids from the snapshot’s model, the plan digest from its lowering view) (crates/hale-cli/src/shared/options.rs · model_identity); build (crates/hale-cli/src/verbs/build.rs · demand_lowering); run and run