diff --git a/HANDOFF.md b/HANDOFF.md
index 789470cb..b04b7e8a 100644
--- a/HANDOFF.md
+++ b/HANDOFF.md
@@ -5,12 +5,14 @@ about the present state, the next decision, and operational facts. The former
 per-PR journal is preserved in
 [`docs/archive/HANDOFF-2026-07-25.md`](docs/archive/HANDOFF-2026-07-25.md).
 
-_Last updated: 2026-07-30. `main` includes the shipped wave through #674.
+_Last updated: 2026-07-31. `main` includes the shipped wave through #675.
 #667 adds the canonical recursive Drop plan and sound `Option<string>` fields;
 #668 admits one direct recursively Move payload per tagged arm; #669 admits multiple Move payloads;
 #670 completes nested tagged payload representation and the exact pkg.db L1b acceptance shape.
 #672 carries L2a parameter modes and explicit empty return-provenance facts through AST, HIR, MIR,
 interfaces, caches, and separate compilation without enabling the borrow ABI.
+#673 infers named direct/imported parameter-root provenance; #674 refines product projections; #675
+closes MIR continuation after every terminating eager child.
 #653 adds stable compaction for callable primitive-scalar `where` stages before
 `par_map`; #654 adds a measure-first task-group record probe without changing
 production behavior. The width/stride probe now covers scalar fused and
@@ -93,6 +95,9 @@ facts must live in this repository.
 #669  multiple Move payload partial construction
 #670  nested tagged payload representation and exact pkg.db L1b shape
 #672  L2a parameter modes and return-provenance representation
+#673  named/direct/imported parameter-root inference
+#674  product return-provenance refinement
+#675  eager MIR continuation closure
 ```
 
 #639 fixes Unit-call values across direct, indirect, pipeline, and per-unit
@@ -190,7 +195,7 @@ PR    observable wall time    production / test / docs changed lines
 #672  8h42m                   4,468 / 2,068 / 72
 #673  23h27m                  7,380 / 3,057 / 549
 #674  2h20m                   1,150 / 620 / 113
-#675  4h06m at audit          4,595 / 295 / 258
+#675  4h14m                   4,595 / 295 / 258
 ```
 
 These wall times exclude work before the first commit and may include idle
@@ -333,12 +338,13 @@ borrow-preserving `if`/`match` sources retain selected owner roots until action;
 success payload and a value-producing loop instead transfer and null their old container/source.
 Terminating return and outer-break paths remove the analysis snapshot from current and saved loop
 states.
-L2b-a2-s is complete in #674. The remaining L2b-a2 work is split by its closure matrix into seven
-mergeable verticals. L2b-a2-ac first closes MIR continuation after every terminating eager child.
-L2b-a2-am-g then validates global type/function tables, callable symbol identity, declarations,
-and every stored-function header before direct handcrafted-HIR lowering. L2b-a2-am-b validates
-every statement, expression type relation and target, action discriminator, id, path, arity, and
-result wrapper. L2b-a2-af adds validated fixed-array formation and exact/dynamic element and element-field
+L2b-a2-s is complete in #674 and L2b-a2-ac in #675. The next independently complete vertical is
+L2b-a2-am-g-t: validate only the global type domain, concrete roots, references, template
+reachability, and inline cycles before direct handcrafted-HIR lowering. The former combined am-g
+plan is reopened after am-g-t. No implementation of its remaining placement, nominal, callable
+namespace, declaration/header, or body boundary may start until one new public-contract ledger
+splits those surfaces and receives a fresh adversarial review. L2b-a2-af then adds validated
+fixed-array formation and exact/dynamic element and element-field
 selection/replacement on that completed substrate. L2b-a2-ar closes retained storage across
 non-fixed index/range, `ArrayChunks`, and `HttpRespHeader` actions. L2b-a2-ap separately closes
 pipeline `Project`/`WhereField` under an explicit stage/terminal state machine. L2b-a2-t completes
@@ -387,25 +393,30 @@ every recursive parent family, and their whole/per-unit tests are therefore one
 boundary and the smallest independently correct vertical. A fresh adversarial preflight found
 that the original matrix also promised fail-closed checks for every handcrafted-HIR action family
 while the implementation only hardened the two lookups touched by ac. The matrix was reopened:
-the broad contract is now L2b-a2-am-g/am-b. A second revised-matrix review found that action-only
-validation still omitted callable symbol uniqueness and universal `Expr.ty`/operator consistency,
-so the boundary was redesigned instead of patched again. Am-g validates MIR-reachable global type
-graphs, callable symbols, declarations, and stored-function headers, returning a canonical
-all-empty MIR program on failure; producer-permitted unreachable generic-template tagged entries
-remain allowed and omitted. Its roots are table entries, declarations, and stored-function
-headers only. Am-b exclusively owns every body-local type/id reference and callable-symbol use,
-derives the only permitted type for every expression discriminator, and validates each body,
-emitting an Unreachable-only function for invalid action metadata while
-preserving neighboring valid source, monomorphized, and lifted functions. A valid caller of such a
-rejected function reaches its Unreachable-only body. Valid MIR remains byte-identical. Am-g is one
-independent global/header fail-closed slice and fixes the exact link-name and callable-symbol byte
-predicates before any MIR/LLVM/link side effect. Am-b uses an iterative enter/exit worklist so the
-validator cannot replace ac's lowered-expression stack improvement with a new recursive overflow.
-Am-b's exhaustive discriminator walk and mutation
-owners may exceed 1,000 hand-written lines, but activation is atomic: a partial body validator would
-leave the same direct-lowering claim able to panic on an unchecked family. If it cannot remain one
-reviewable exhaustive match, dormant construction and final activation must be re-split before
-coding. Both distinct mergeable boundaries must land after ac and before af.
+the broad contract was first split as L2b-a2-am-g/am-b. A second revised-matrix review found that
+action-only validation still omitted callable symbol uniqueness and universal
+`Expr.ty`/operator consistency. Implementation then proved the global half itself too broad: the
+combined type plus nominal/link checkpoint measured 1,535 changed hand-written lines. Type-domain
+validation has no atomic dependency on nominal/link validation, so am-g-t is now the only
+authorized next slice. It returns a canonical all-empty MIR program only for an invalid global type
+domain and leaves every placement, nominal, namespace, declaration/header, and body predicate
+unchanged.
+
+The broader remainder is deliberately reopened rather than patched again. Reviews found that a
+body-free validator must not claim body-derived Drop facts; inline-layout cycles must be separated
+from valid header-mediated nominal recursion; generic-template roots must remain producer-compatible;
+and current HIR cannot distinguish source functions from generic monomorphs. Post-open review then
+found two more missing invariants: graph-valid types still need exact per-position producer
+admissibility, and callable validation must cover logical runtime lookup keys plus body-generated
+`$fnval`, `$clos`, task-trampoline, and parallel-kernel identities. It also found that rejecting
+source-accepted exact compiler/runtime spellings as malformed HIR would be a hidden semantic
+change. The new remainder ledger must resolve that namespace design without silently reserving
+names, enumerate every placement predicate, assign every generated identity to an implementation
+and owner test, and fix the final PR count before code begins. This is a strategy-level matrix
+reopen, not an ordinary patch loop.
+
+Am-g-t's type-domain implementation is preserved separately. The split applies the existing
+review-size and closure-matrix rules; it does not justify a new process rule.
 The final L2b-a2-s vertical is approximately 1,900 lines because its adversarial review required
 malformed constructor/read/write fail-closed validation, common eager-child source-order snapshots,
 snapshot-generation invalidation, checked-expression identity, action-boundary validation, and
@@ -415,9 +426,10 @@ Its final local provenance benchmark reports 3.147 ms/check, 22,848 interface by
 1.844 ms/import on Apple Silicon.
 Do not begin a
 SQLite/PostgreSQL driver or add database-named compiler
-variants before L1a–L7 are complete. L2 is implemented as seven conceptual milestones in fourteen
-closed PRs so no incomplete borrow surface is exposed: L2a parameter-mode and provenance-summary
-representation, L2b-a1/a2-s/a2-ac/a2-am-g/a2-am-b/a2-af/a2-ar/a2-ap/a2-t/b
+variants before L1a–L7 are complete. L2 requires at least fifteen implementation PRs; the final
+count remains open until the post-am-g-t remainder ledger is complete. The current minimum
+sequence is L2a parameter-mode and provenance-summary representation,
+L2b-a1/a2-s/a2-ac/a2-am-g-t/a2-am-r/a2-af/a2-ar/a2-ap/a2-t/b
 return-provenance slices, L2c cleanup-ABI record plus dynamic Move-return bit, L2d shared borrow,
 then L2e
 mutable borrow/out and all-peer
diff --git a/docs/impl/17-library-boundary-prerequisites.md b/docs/impl/17-library-boundary-prerequisites.md
index b5dfa19b..c45b4173 100644
--- a/docs/impl/17-library-boundary-prerequisites.md
+++ b/docs/impl/17-library-boundary-prerequisites.md
@@ -1490,10 +1490,11 @@ Scope:
 - interface codec/hash support;
 - per-unit parity.
 
-L2 ships through seven conceptual milestones in fourteen closed implementation PRs; L2b-a2 is split
-into product, MIR action-continuation, malformed-HIR global/header validation, malformed-HIR body
-validation, fixed-array, eager-receiver lifetime, pipeline, and tagged verticals below. A PR may add dormant representation or tighten
-existing provenance, but it must
+L2 requires at least fifteen implementation PRs; the final count remains open until the
+post-am-g-t malformed-HIR remainder ledger is complete. L2b-a2 first isolates product, MIR
+action-continuation, and global type-domain validation. Placement, nominal, callable namespace,
+declaration/header, and body validation remain behind the explicit am-r design gate below. A PR may
+add dormant representation or tighten existing provenance, but it must
 not accept source syntax whose complete safety contract belongs to a later milestone.
 
 | Slice | Exact closure | Public exposure at merge | Required gate |
@@ -1502,8 +1503,8 @@ not accept source syntax whose complete safety contract belongs to a later miles
 | L2b-a1 | Infer parameter roots for named functions and preserve conservative flattened roots across recursion, direct/imported calls, control flow, and interfaces | No new borrow mode; aggregate projections and indirect calls retain all-compatible-input unions | scalar direct/imported matrix, semantic interface validation, and summary-inference size/time evidence |
 | L2b-a2-s | Add the projection fact and refine named summaries through structs, tuples, block/`if`/loop, field assignment, and destructuring | No new borrow mode; array, pipeline, tagged/control residuals, and indirect calls retain the L2b-a1 all-compatible-input fallback | direct/imported product-view projection matrix and per-unit parity |
 | L2b-a2-ac | Close MIR fallthrough propagation after every terminating eager expression child, including enclosing consumers and later siblings | No new borrow mode or provenance precision; source semantics are unchanged; the normal driver still supplies semantically checked HIR | exhaustive recursive-call-site classification, representative family-level no-action assertions, runtime twins, and whole/per-unit continuation parity |
-| L2b-a2-am-g | Validate every global type/function table, symbol identity, declaration, and stored-function header before MIR construction | No source, semantic, HIR, MIR, interface, or ABI change; direct handcrafted-HIR lowering returns a canonical empty program for invalid global/header metadata while body validation remains the semantic-checker contract | exhaustive global graph/symbol/header mutation matrix across all lowering entrypoints and unchanged valid-program MIR |
-| L2b-a2-am-b | Validate every statement, expression type relation, symbol target, action discriminator, id, path, arity, and result wrapper before lowering a function body | No public change; direct handcrafted-HIR lowering now has the complete fail-closed boundary | exhaustive table-driven malformed-body matrix, per-function Unreachable-only isolation, and unchanged valid-program MIR/codegen |
+| L2b-a2-am-g-t | Validate concrete roots through every global type table before MIR construction | No source, semantic, HIR, MIR, interface, or ABI change; direct handcrafted-HIR lowering returns a canonical empty program only for an invalid global type domain while every placement, nominal, namespace, declaration/header, and body predicate remains the semantic-checker contract | exhaustive type-domain/root/reference/cycle mutation matrix across all lowering entrypoints and unchanged valid-program MIR |
+| L2b-a2-am-r | Design gate only: before any remaining malformed-HIR implementation, complete one new public-contract ledger that splits per-position type admissibility, nominal/link metadata, callable logical/emitted/generated namespaces, declarations/headers, and body validation into independently correct verticals | No implementation is authorized by this row. The ledger must preserve current producer acceptance or explicitly update every source of truth for a deliberate semantic/ABI change; it fixes the final PR count and prerequisites before code begins | fresh independent adversarial ledger review covering every producer placement predicate, runtime lookup key, exact compiler/native emitted identity, generated helper family, validation order, valid producer twin, and owner test |
 | L2b-a2-af | Extend the projection fact through validated fixed arrays and exact/dynamic element reads/writes | No new borrow mode; pipeline, tagged/control, non-fixed collection, and indirect-call residuals retain the L2b-a1 all-compatible-input fallback | direct/imported fixed-array projection matrix and per-unit parity |
 | L2b-a2-ar | Close eager retained-storage lifetime for non-fixed `Index`, `ElemField`, `SliceRange`, `ArrayChunks`, and `HttpRespHeader`; make non-fixed `ElemField` receiver-first | No new borrow mode or projection precision; non-fixed results remain flattened | invalidated eager-action matrix, terminating-operand twins, runtime source-order checks, malformed-HIR rejection, and per-unit parity |
 | L2b-a2-ap | Extend the projection fact through pipeline `Project`/`WhereField` and terminal formation | No new borrow mode; tagged/control and indirect calls retain the L2b-a1 all-compatible-input fallback; unsupported stages and terminals widen explicitly | direct/imported pipeline-view projection matrix and per-unit parity |
@@ -1556,15 +1557,17 @@ both the closed and open-world effects `Impure`; a direct external callback para
 field call remains legal. L2b replaces those conservative boundaries with recursive target-relative
 provenance through function-value joins.
 
-L2b is implemented as ten independently sound vertical PRs. L2b-a1 owns named/direct/imported
+L2b requires at least eleven independently sound implementation PRs; the final number depends on
+the am-r split. L2b-a1 owns named/direct/imported
 parameter-root inference, semantic interface validation, and whole/per-unit parity while retaining
 flattened all-compatible-input unions for aggregates, indirect calls, and unanalyzed extern
 targets. L2b-a2-s adds the projection fact and closes struct/tuple construction, selection,
 replacement, destructuring, and ordinary block/branch/loop flow while retaining conservative
 array, pipeline, and tagged residuals. L2b-a2-ac next closes MIR continuation after every
-terminating eager expression child for semantically checked HIR. L2b-a2-am-g then closes global,
-symbol, declaration, and stored-function-header validation for direct lowering; L2b-a2-am-b closes
-the separate body/expression/action boundary. L2b-a2-af closes validated fixed-array formation and
+terminating eager expression child for semantically checked HIR. L2b-a2-am-g-t then closes only the
+global type domain for direct lowering. L2b-a2-am-r is a required authoring and review gate that
+splits the remaining placement, nominal/link, callable namespace, declaration/header, and body
+surfaces before any of them are implemented. L2b-a2-af closes validated fixed-array formation and
 element reads/writes while retaining conservative non-fixed and pipeline residuals. L2b-a2-ar
 closes the affected non-fixed index/range, chunks, and response-header retained-storage actions.
 L2b-a2-ap closes pipeline `Project`/`WhereField` propagation and terminal formation. L2b-a2-t
@@ -1638,7 +1641,7 @@ unreachable return shape (`Operand::Const(Const::Unit)`, `None`, `false`, or `()
 | structured control continuation | `if`, `match`, `else`, `?`, `map_err`, short-circuit boolean, loop, arena, task-group, unsafe, and nested block helpers distinguish a terminated arm from an explicitly created reachable join. They may switch `Builder.cur` only to a block with a real predecessor or an operation-defined early-return edge. A fully terminating construct propagates termination; a mixed construct yields only its fallthrough alternatives; no placeholder supplies a join value. | fully terminating/mixed/all-fallthrough triples for each control family; exact predecessor, phi/store, cleanup, and result assertions; nested eager parent around each triple |
 | pipeline and callback action | Existing source/stage/terminal continuation gates remain authoritative. Required-child checks cover source, stage operand/capture, terminal argument/capture, initializer, reducer, destination, and JSON-scanner callbacks before allocation, loop state, callback call, source nulling, or cleanup transfer. Ac does not reorder a pipeline operand or change effect/provenance inference. | cumulative `terminating_pipeline_operand_emits_no_terminal_state`, capture-order, source-shape, driver runtime, and effect-source-order matrices, each nested under a strict eager parent |
 | owner, cleanup, and allocation parity | A terminating child owns the cleanup and control edge it already emitted. Its parent performs no Drop, drop-flag write, source nulling, cleanup transfer, allocation, owner inheritance, or action-side restoration. Completed earlier operands retain only cleanup required on the terminating edge. Fallthrough allocation and Drop order are byte-for-byte unchanged. | owned earlier-operand + terminating-later-operand Drop-count twins; MIR drop-flag/null/transfer assertions; allocation counter parity on all-fallthrough twins |
-| narrow malformed-HIR defense | Ac may replace a direct index or shape assumption touched by its continuation edits with a checked lookup, but this is defense in depth rather than a complete handcrafted-HIR contract. Missing indirect-function type metadata and an invalid element-field path terminate before the parent action. L2b-a2-am-g/am-b own the complete structural boundary. | `malformed_hir_continuation_metadata_fails_closed` covers exactly the indirect-function signature and fixed/dynamic/SoA element-field-path cases, including no dynamic/SoA length action before rejection; no broader malformed-HIR claim is attached to ac |
+| narrow malformed-HIR defense | Ac may replace a direct index or shape assumption touched by its continuation edits with a checked lookup, but this is defense in depth rather than a complete handcrafted-HIR contract. Missing indirect-function type metadata and an invalid element-field path terminate before the parent action. L2b-a2-am-g-t owns only the global type domain; am-r must settle and split the remaining structural boundary. | `malformed_hir_continuation_metadata_fails_closed` covers exactly the indirect-function signature and fixed/dynamic/SoA element-field-path cases, including no dynamic/SoA length action before rejection; no broader malformed-HIR claim is attached to ac |
 | public and artifact boundary | No AST/HIR/MIR/LLVM/interface type, tag, codec, fingerprint, cache identity, source syntax, ownership rule, or runtime ABI changes. Whole-program and per-unit lowering call the same internal continuation implementation. | interface/hash goldens remain cumulative; focused whole-program and per-unit runtime twins agree, the existing single-unit gate retains MIR/object identity, and the high-CFG lowering row records continuation cost |
 
 The author-side matrix-to-diff pass must account for every recursive child-lowering entrypoint after
@@ -1658,64 +1661,52 @@ claims would depend on that gap. Reachability state, the caller-local guard, eve
 family, and their whole/per-unit owners are therefore one compatibility boundary. A fresh
 adversarial preflight found that the original matrix also attached a much broader handcrafted-HIR
 validation contract to this slice. That contract is independently mergeable and would require
-checks across every HIR family, so it is re-split as L2b-a2-am-g/am-b rather than expanding ac further.
-
-### L2b-a2-am-g/am-b malformed-HIR closure matrix
-
-L2b-a2-am-g and L2b-a2-am-b form the internal fail-closed boundary between handcrafted HIR and MIR. Normal compiler
-input is unchanged: semantic checking still owns user diagnostics and supplies valid HIR. Direct
-`lower_program` callers, tests, and future tooling may construct inconsistent HIR, so am has two
-independently mergeable validation phases before MIR construction. Am-g owns program/declaration
-validation across every global type table, function-type table, symbol namespace, `extern`,
-imported declaration, link-library record, and complete stored-function header before any MIR
-record is copied or any function is lowered. Any failure returns the
-canonical empty MIR `Program`—all vectors empty—so no malformed declaration can reach codegen.
-Am-b then validates bodies and actions by walking every stored `Program.fns` entry—source functions, generic
-monomorphs, and lifted lambdas—in vector order and each body in HIR preorder. A body failure
-preserves its already-validated signature but replaces only that function
-with an entry block terminated by `Unreachable`; valid functions before and after it lower
-normally. A valid caller may retain a call to that signature; entering the rejected callee reaches
-only `Unreachable`. No prefix action, allocation, ownership transfer, native call, or partial
-control graph from the invalid function is retained. No diagnostic or new public result type is
-introduced. Valid HIR produces byte-for-byte identical MIR.
+checks across every HIR family, so it is not part of ac.
+
+### L2b-a2-am-g-t immediate closure and am-r design gate
+
+Only am-g-t is authorized for implementation by this section. Normal compiler input is unchanged:
+semantic checking still owns user diagnostics and supplies valid HIR. Direct `lower_program`
+callers, tests, and future tooling may construct an invalid global type graph, so am-g-t validates
+the complete type domain before any MIR record is copied or any function is lowered. Any am-g-t
+failure returns the canonical empty MIR `Program` with every vector empty. Valid HIR produces
+byte-for-byte identical MIR.
+
+The former combined am-g/am-b design is reopened after am-g-t. Its implementation checkpoint mixed
+type-domain validation with nominal/link validation and reached 1,535 changed hand-written lines.
+A fresh boundary review proved those phases have no atomic dependency. Later post-open reviews also
+found that the broader matrix omitted exact per-position producer type admissibility and the full
+callable namespace: compiler runtime lookup keys, exact emitted identities, and body-generated
+`$fnval`, `$clos`, task-trampoline, and parallel-kernel names. Rejecting source-accepted exact
+compiler/runtime spellings as malformed HIR would itself be a hidden semantic change. Am-r must
+therefore publish and pass a new public-contract ledger before any placement, nominal/link,
+namespace, declaration/header, or body implementation begins. The ledger fixes the exact remaining
+PR split and count; this section deliberately does not guess either.
 
 | Slice / malformed-HIR cell | Required closure | Exact owner evidence |
 |---|---|---|
-| am-g program type and declaration metadata | Before copying any record, validate all tuple/struct/enum/tagged-type and function-type table identities and complete shapes, every concrete scalar width/tag and nested type reference rooted in those table entries, every `extern`/imported signature and mode/summary record, every stored-function header type, and each link-library string. Traverse type tables in stored order, then function types, with an explicit worklist and visit colors rather than native recursion. Every struct/enum internal `name` and `source_name` is non-empty UTF-8 without U+0000; identity and collision use exact UTF-8 bytes with no normalization. Internal nominal names are unique across the combined struct/enum namespace. A repeated `source_name` is permitted only for the same nominal kind with an identical complete recursively id-free ABI shape; every conflicting shape or struct/enum collision rejects. Field and variant names match `[A-Za-z_][A-Za-z0-9_]*` and are unique within their declaration. A struct alignment is `None` or a power of two in `1..=2^29`. Enum variants are in tag order; the first `field_base` is `1`, each next base is the checked sum of the preceding base and payload length, and the final flattened field count must fit `u32`. Producer-permitted unreachable generic-template `tagged_types` entries may contain `Scalar::Param`; preserve the existing canonicalization rule by allowing and omitting those entries. A `Param`, missing id, or cycle rooted in a concrete table entry, declaration, or stored-function header is an am-g failure. A raw type/id reference that occurs only in a function body is never an am-g root and belongs exclusively to am-b. A link-library name is accepted exactly when it is non-empty, does not start with `-`, and every byte is ASCII alphanumeric or one of `._+-`; `String` already guarantees UTF-8, while spaces, slash, controls including U+0000, and all non-ASCII bytes reject before any MIR record or link input is copied. | wrong/missing/cyclic table/header/declaration type references; empty/NUL/colliding nominal identities, repeated source identities with equal and unequal structural ABI shapes, invalid/duplicate field and variant names, zero/non-power-of-two/over-limit alignment, and wrong/overflowing enum field bases; malformed extern/import signatures and summaries; every invalid link-library byte class and boundary position; and first/middle/final declaration mutations. Valid identity twins contain equal-shape origin-specific source-name repeats and unused generic-template tagged entries and assert they remain permitted/canonicalized; invalid results have every vector empty in all four entrypoints |
-| am-g symbol-table identity | Build one canonical callable namespace before lowering. Stored functions are visited in vector order, then externs, then imported declarations. Stored and imported names are non-empty UTF-8 `String` values with no U+0000; their emitted/collision identity is the exact UTF-8 byte sequence already produced by sema, with no normalization or remangling. An extern name must additionally match the source identifier grammar `[A-Za-z_][A-Za-z0-9_]*`. Exact emitted identities must be unique within each class and disjoint wherever LLVM would emit the same symbol. Record the closed compiler-owned builtin/native target set, but do not resolve any body use in this slice. The first invalid byte/name, duplicate, or collision returns the canonical empty program before any name is passed to LLVM or a linker. | empty and embedded-NUL stored/import names, every invalid extern first/continuation byte, duplicate and cross-class exact-byte collisions in every order, invalid stored/lifted/extern/import declaration identities, distinct UTF-8 byte names without normalization, and valid same-source display names with distinct canonical symbols |
-| am-g stored-function header metadata | Before `lower_fn`, validate parameter/local counts and ids, parameter modes, lifted-parameter partition, return type and summaries, drop-local ids/subsets, individual-drop records, exportability constraints, and every header-owned type reference for source functions, generic monomorphs, and lifted lambdas. Each local id equals its vector ordinal; local names are non-empty UTF-8 without U+0000 and use exact-byte identity; parameter local names match the source identifier grammar; local alignment is `None` or a power of two in `1..=2^29` and is present only on the currently supported numeric-scalar fixed-array storage shape. Any invalid header is a program/declaration failure because codegen would otherwise observe invalid slot/signature metadata. | one mutation per header field, local name/id/alignment predicate, subset invariant, and stored-function origin; mixed valid/invalid function order always returns the canonical empty program before lowering any body |
-| am-b statement, local, and place metadata | Validate every local/slot id and its exact declared type, destination kind, struct/tuple/element path, field/lane/index discriminator, writable-place shape, and assignment result assumption reachable from statements, returns, breaks, and block tails. | table-driven mutations for every statement and place discriminator, including first/middle/final positions; each invalid function is Unreachable-only |
-| am-b universal expression consistency | One total `ExprKind` match validates every child first and derives the only permitted result type. The traversal uses an explicit enter/exit worklist, bounded per-node result state, and no native recursion, so every semantically checked HIR up to the parser's expression-depth ceiling remains stack-bounded. Every raw type/id reference reached from a body—including `Expr.ty`—is resolved against the already validated am-g tables here; a missing, cyclic, template-only, or wrong-kind body reference is an am-b failure and never changes the program-global result. Require `Expr.ty`, referenced local type, operand types, operator discriminator, scalar width/sign, cast endpoints, vector lane/arity, unary/binary/int-arithmetic/math arity and type rules, and literal payload to agree exactly. `FnValue`, closure/lifted targets, and direct calls resolve body uses through the am-g canonical namespace; indirect calls agree with their validated function type. No wildcard arm or default type is permitted. | one missing/wrong-kind body type id, wrong-result, and wrong-operand mutation for every expression discriminator; every unary/binary/cast/int-arithmetic/math operator/type/arity boundary; unresolved/wrong-kind call and lifted body targets; valid local ids carrying wrong expression types; direct maximum-checked-depth HIR validation and end-to-end `within_limit_chain_compiles_and_runs` |
-| am-b aggregate, capture, and call metadata | Validate body-local aggregate/type ids, field and payload ordinals, constructor arity, capture ids and types, direct/indirect callable signatures, parameter modes/counts, result types, and constant-array contents before lowering. | missing/wrong body-local ids, paths, arities, signatures, captures, and result types across array/struct/tuple/tagged/closure/direct/indirect call families; every failure replaces only its function |
-| am-b storage, view, vector, and pipeline metadata | Validate collection/view/source discriminators, element/layout facts, scalar widths, vector lanes, chunk/range shapes, stage/terminal kinds, callback signatures, accumulator/result shapes, and every producer-owned pipeline table reference. | exhaustive discriminator mutations for fixed/dynamic/SoA/view/vector storage plus every stage and terminal; no helper CFG or terminal state on rejection |
-| am-b native and runtime metadata | Validate every helper discriminator, argument/result ABI shape, wrapper enum/tag id, and operation-specific checked record used by JSON, I/O, filesystem, network, process, regex, HTTP, task, crypto/compression, time/random, and unsafe lowering. | one valid and every invalid metadata form per helper family, including `Option`/`Result` wrapper mismatches; rejection occurs before runtime allocation or call |
-| am-b structured-control metadata | Validate branch/result types, match variant and binding records, `else`/`?`/`map_err` wrapper shapes, loop target/result records, and arena/task-group/unsafe control metadata without trusting an ordinal or table index. | malformed fully terminating, mixed, and all-fallthrough control records; each rejects deterministically before any MIR for the function |
-| am-b function isolation | A body-metadata failure changes only the invalid function body. Its validated signature, linkage, provenance summaries, and neighboring valid functions remain unchanged; invalid functions in first, middle, and final declaration positions behave identically. Program/header failures remain all-or-nothing because their records can shape every function and emitted declaration. | valid-before/invalid/valid-after triples for source, monomorphized, and lifted functions compare neighboring MIR byte-for-byte with the all-valid twin and require an Unreachable-only invalid body |
-| am-g/am-b public, valid-input, and cost boundary | No source syntax, semantic acceptance, HIR/MIR variant, interface byte, fingerprint, cache key, ownership rule, LLVM ABI, or runtime ABI changes. Each validator is linear in its stored input plus referenced type metadata and performs no runtime allocation. | `valid_hir_global_metadata_preflight_is_mir_identity` and `valid_hir_body_metadata_preflight_is_mir_identity` compare validated and internal unchecked lowering paths; the complete `align_mir` owner suite and whole/per-unit codegen suite remain clean; the benchmark records each phase with the continuation-lowering row |
-
-Am-g is independently complete for metadata copied outside function bodies and activates only its
-canonical all-empty rejection. Am-b may exceed roughly 1,000 changed hand-written lines because
-its one total expression/body validator must match every statement, expression, pipeline-stage,
-terminal, and native-helper discriminator before the public `lower_program` entrypoints can claim
-fail-closed handcrafted bodies. A partial family validator would still let another body
-discriminator panic under the same claim and would duplicate traversal/type-derivation state.
-The total match, Unreachable-only function replacement, exhaustive mutation matrix, valid-input
-identity proof, and four-entrypoint parity therefore form one atomic body boundary. If am-b cannot
-remain reviewable as one exhaustive match plus table-driven owners, reopen this matrix and split
-dormant validator construction from activation; do not activate a partially complete body claim.
+| am-g-t concrete type roots and total type domain | Before copying any record, validate tuples, structs, enums, and every type reachable from those tables, an `extern`/imported declaration, or a stored-function header. Every stored struct, enum, and tuple is a concrete root. Every stored tagged-type and function-type entry is also a concrete root unless it belongs to an abstract template graph: a node that contains `Scalar::Param`/`Ty::Param` or transitively depends on such a node. An unreachable abstract template graph is permitted because the producer retains generic-template interner entries that MIR omits; a concrete root that reaches one rejects. Every non-template tagged/function entry remains a root even when otherwise unreachable, so a missing id, inline cycle, or invalid concrete scalar cannot hide in discarded state. Every tagged reference and every function-type reference must be in range even inside a permitted template graph. Traverse with an explicit enter/exit worklist and visit colors rather than native recursion. `IntTy.bits` is exactly `8`, `16`, `32`, or `64`; `FloatTy.bits` is exactly `32` or `64`; the same widths apply inside every `PrimScalar`. `Vec`/`Mask` accepts only an integer/float scalar and exactly `2`, `4`, `8`, or `16` lanes. Every `Struct`/`Enum`/`Tuple`/`Tagged`/`Fn` discriminator resolves to its matching table, every struct-bearing collection resolves a struct, and `DictEncoded(id, field)` resolves an in-range `str` key field. `Ty::IntVar`, `Ty::FloatVar`, `Ty::Error`, and HIR-reachable `Ty::StrFinder` reject. Fixed arrays, tuples, structs, enums, `Option`, `Result`, and nested tagged payloads extend the active inline-layout path and reject an inline cycle. `Box`, slices, dynamic arrays, `ArrayBuilder`, `Task`, dynamic struct arrays, SoA, scanners, dictionary headers, and function closures validate their referenced entries but break that inline path; header-mediated nominal recursion is valid. Am-g-t validates graph formation only: it does not claim that every valid type is admissible in every field, payload, tuple element, parameter, return, local, or body position. | one mutation for every `Ty`, `Scalar`, and `PrimScalar` discriminator; every width/lane boundary; missing/wrong-kind table id and dictionary field; inline-cycle rejection and `Box`/dynamic-array/task/function-header positive cycle twins; reachable/unreachable `Param` tagged and function-type twins; unused malformed non-template tagged and function-type entries; first/middle/final concrete roots; placement-invalid but graph-valid positive twins remain unchanged for am-r; invalid results have every vector empty in all four entrypoints |
+| am-r reopened remainder | No implementation contract is authorized yet. The author ledger must enumerate the exact producer predicate for every field, payload, tuple element, parameter, return, local, and body position; nominal/link identities and validation order; logical callable keys; stored/imported/extern emitted identities; compiler/native declarations and compatible reuse; every `$fnval`, `$clos`, task-trampoline, and parallel-kernel identity; source encoding/NUL rules; ownership/allocation; cache and ABI effects; error precedence; and every valid producer twin. It must choose explicitly between preserving current source acceptance and a fully specified source/ABI change, then update every affected source of truth before implementation. | one owner row per placement and generated-symbol family; exact compiler/runtime spelling positives; duplicate/cross-class/multi-invalid precedence; whole/per-unit/cache identity; fresh independent adversarial review of the completed ledger and proposed PR boundaries |
+
+Am-g-t is independently complete and activates only its global type-domain all-empty rejection. It
+is linear in stored type metadata and allocates only compiler-owned validation worklists and visit
+maps. `valid_hir_global_type_preflight_is_mir_identity` compares the validated and internal
+unchecked lowering paths. The complete `align_mir` owner suite and whole/per-unit codegen suite
+remain clean, and `mir-global-type-validation` records the phase beside the existing
+`mir-continuation-lowering` benchmark row.
 
 L2b-a2-s owns the base fact shape, parameter/local formation, struct/tuple
 construction/selection/replacement, destructuring, ordinary block/`if`/loop flow, liveness parity,
 and the product half of the public boundary. L2b-a2-ac first closes the MIR continuation
-prerequisite above without changing a projection fact. L2b-a2-am-g then closes direct handcrafted-HIR
-global/header validation and L2b-a2-am-b closes body/action validation without changing valid HIR.
-L2b-a2-af adds validated fixed-array paths
+prerequisite above without changing a projection fact. L2b-a2-am-g-t closes only direct
+handcrafted-HIR global type-domain validation without changing valid HIR. Am-r must settle and split
+all remaining malformed-HIR work before L2b-a2-af adds validated fixed-array paths
 and exact/dynamic element selection and replacement. L2b-a2-ar closes eager retained-storage
 actions for non-fixed reads. L2b-a2-ap adds pipeline `Project`/`WhereField` and terminal formation.
 L2b-a2-t owns tagged construction/binding, `match`, `else`, `?`, `map_err`, and the final
 public/projection-malformed-boundary pass. Every extending projection PR must add malformed
 type/path/ordinal fallback owners for its new projection kinds and selected/unselected liveness
-owners to the shared focused targets. All eight retain the scope-boundary row.
+owners to the shared focused targets. Every implementation slice retains the scope-boundary row.
 
 | L2b-a2 path | Exact analysis contract | Owner evidence |
 |---|---|---|
@@ -1731,22 +1722,18 @@ owners to the shared focused targets. All eight retain the scope-boundary row.
 | public and malformed boundary | `ReturnBorrowSummary` and `ReturnRegionSummary` remain the L2a codec and hash shape and remain equal in L2b-a2. Semantic import keeps the L2b-a1 validation order. No projection trie, local id, span, raw nominal id, or control-state bit is serialized. Because the codec carries parameter indices only, an imported aggregate result and any later projection from one aggregate actual deliberately retain that actual's complete compatible owner set. | unchanged codec/hash goldens, interface corruption suite, aggregate-actual precision-limit fixture, and summary byte-size benchmark row |
 | scope boundary | Indirect calls, closure captures, function-value joins/moves, target-relative capture slots, and direct calls without a settled named/imported summary—including unanalyzed extern targets—retain the documented all-compatible-input fallback. No `borrow`, `borrow mut`, cleanup ABI, resource, region, or database surface is enabled. | existing deferred-function-value and compatibility/extern fixtures plus disabled-mode regressions |
 
-L2b-a2-s, L2b-a2-ac, L2b-a2-am-g, L2b-a2-am-b, L2b-a2-af, L2b-a2-ar, L2b-a2-ap, and
-L2b-a2-t are the smallest independently correct verticals. The first PR
+L2b-a2-s, L2b-a2-ac, and L2b-a2-am-g-t are independently correct completed or authorized
+verticals. The first PR
 publishes an exact product summary while array, pipeline, and tagged/control forms deliberately
 retain the shipped flattened result. It must include product construction, reads, partial writes,
 destructuring, ordinary control joins, direct/imported consumption, and whole/per-unit parity
 together: omitting a writer or join can under-approximate the same public product fact. The second
-PR closes the general MIR continuation invariant for checked HIR. The third PR adds global graph,
-symbol, declaration, and stored-function-header validation. The fourth PR adds total body and
-expression consistency validation. The fifth PR adds validated fixed-array formation plus
-exact/dynamic reads and writes on that substrate. The sixth closes eager retained-storage lifetime
-for non-fixed reads. The seventh closes the explicit pipeline stage/terminal state machine. The
-eighth PR replaces
-the remaining tagged fallbacks atomically across constructors, pattern bindings, `else`, `?`, and
-`map_err`: splitting its explicit and implicit `Result` edges would let one value produce
-contradictory summaries. No PR may exceed roughly 1,000 changed hand-written lines without first
-updating this matrix with a narrower safe boundary and a concrete reason that boundary fails.
+PR closes the general MIR continuation invariant for checked HIR. The third adds only global
+type-domain validation. Am-r must define the later verticals before implementation; af, ar, ap, and
+t retain their existing dependency order after that completed boundary. The tagged slice still
+replaces its explicit and implicit `Result` fallbacks atomically. No PR may exceed roughly 1,000
+changed hand-written lines without first updating this matrix with a narrower safe boundary and a
+concrete reason that boundary fails.
 The final L2b-a2-s diff is approximately 1,900 changed hand-written lines after adversarial review
 required fail-closed constructor/read/write validation, common eager-child source-order snapshots,
 snapshot-generation invalidation, checked-expression identity, action-boundary validation, and
@@ -2055,8 +2042,8 @@ their first owning slice and remain cumulative gates afterward.
 | L2b-a1 | `cargo test -p align_interface --test summary`; `cargo test -p align_sema ty_may_borrow_is_cycle_safe_for_header_mediated_nominals`; `cargo test -p align_sema lifted_function_origin_metadata_is_explicit`; `cargo test -p align_sema checked_break_acceptance_is_preserved_in_hir`; `cargo test -p align_sema rejected_break_effect_payload_is_visited_without_loop_result_join`; `cargo test -p align_sema effect_source_order_closure_matrix`; `cargo test -p align_sema pipeline_terminal_snapshot_action_order_matrix`; `cargo test -p align_sema pipeline_terminal_diagnostic_order`; `cargo test -p align_sema pipeline_terminal_dead_state_isolated_across_analyses`; `cargo test -p align_sema pipeline_terminal_dead_hir_is_finalized_and_linted`; `cargo test -p align_sema pipeline_capture_owner_invalidation_is_rejected`; `cargo test -p align_sema pipeline_source_snapshot_owner_invalidation_matrix`; `cargo test -p align_codegen_llvm malformed_mir_type_graphs_fail_before_llvm_construction`; `cargo test -p align_mir rejected_checked_break_lowers_to_unreachable`; `cargo test -p align_mir terminating_break_payload_emits_no_outer_edge`; `cargo test -p align_mir mixed_break_payload_preserves_outer_edge`; `cargo test -p align_mir terminating_pipeline_operand_emits_no_terminal_state`; `cargo test -p align_mir pipeline_terminal_snapshot_action_order_matrix`; `cargo test -p align_mir pipeline_terminal_source_shape_parity`; `cargo test -p align_driver --test return_provenance --test analysis_coverage --test interface_param_modes --test per_unit`; `cargo test -p align_driver --test m5 json_scan_reduce_fold`; `cargo test -p align_driver --test zip_pipeline pipeline_terminal_source_order` | `bench/library_boundary/run.sh provenance`: `summary-inference`, `import-validation` |
 | L2b-a2-s | `cargo test -p align_sema projected_return_provenance_fails_closed`; `cargo test -p align_driver --test return_provenance --test per_unit` | `bench/library_boundary/run.sh provenance`: `summary-inference` |
 | L2b-a2-ac | `cargo test -p align_mir eager_expression_termination_matrix`; `cargo test -p align_mir malformed_hir_continuation_metadata_fails_closed`; `cargo test -p align_driver --test mir_continuation`; `cargo test -p align_driver --test expr_depth within_limit_chain_compiles_and_runs`; `cargo test -p align_driver --test per_unit_codegen eager_expression_termination` | `bench/library_boundary/run.sh provenance`: `mir-continuation-lowering` |
-| L2b-a2-am-g | `cargo test -p align_mir malformed_hir_global_metadata_fails_closed`; `cargo test -p align_mir valid_hir_global_metadata_preflight_is_mir_identity`; `cargo test -p align_mir`; `cargo test -p align_driver --test per_unit_codegen` | `bench/library_boundary/run.sh provenance`: `mir-global-validation`, `mir-continuation-lowering` |
-| L2b-a2-am-b | `cargo test -p align_mir malformed_hir_body_metadata_fails_closed`; `cargo test -p align_mir valid_hir_body_metadata_preflight_is_mir_identity`; `cargo test -p align_mir max_checked_hir_depth_body_preflight_is_stack_bounded`; `cargo test -p align_mir`; `cargo test -p align_driver --test expr_depth within_limit_chain_compiles_and_runs`; `cargo test -p align_driver --test per_unit_codegen` | `bench/library_boundary/run.sh provenance`: `mir-body-validation`, `mir-continuation-lowering` |
+| L2b-a2-am-g-t | `cargo test -p align_mir malformed_hir_global_type_metadata_fails_closed`; `cargo test -p align_mir valid_hir_global_type_preflight_is_mir_identity`; `cargo test -p align_mir`; `cargo test -p align_driver --test per_unit_codegen` | `bench/library_boundary/run.sh provenance`: `mir-global-type-validation`, `mir-continuation-lowering` |
+| L2b-a2-am-r | design-only ledger review; no implementation test or benchmark is authorized until the ledger fixes the split | none |
 | L2b-a2-af | `cargo test -p align_sema projected_return_provenance_fails_closed`; `cargo test -p align_mir eager_expression_termination_matrix`; `cargo test -p align_driver --test return_provenance --test per_unit` | `bench/library_boundary/run.sh provenance`: `summary-inference` |
 | L2b-a2-ar | `cargo test -p align_mir eager_expression_termination_matrix`; `cargo test -p align_driver --test return_provenance --test borrow_liveness --test struct_index --test chunks --test soa --test m11_http --test m11_http_get_many` | `bench/library_boundary/run.sh provenance`: `summary-inference` |
 | L2b-a2-ap | `cargo test -p align_sema projected_return_provenance_fails_closed`; `cargo test -p align_mir eager_expression_termination_matrix`; `cargo test -p align_driver --test return_provenance --test per_unit` | `bench/library_boundary/run.sh provenance`: `summary-inference` |