docs(impl): isolate global HIR type validation

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