Link the effect-namespace-grants design doc (fix main-red doc-orphan wall)

DESIGN.md

@@ -94,6 +94,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`
 - **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** Stages 1–3 LANDED (#6373): `DescentEvidence` consolidated onto its single authority `dag/std/termination.dag` (§7 ruling, parent 2026-07-03), `loop_multiplicity` is node-aware (termination derived from the `^loop_bound_edge` measure, fail-closed to `DescentUnknown`; FLAG B asymmetry rationale in-code), `04_infer` has a Loop arm typing the iteration fold `τ→τ` with refinement-shaped loops refused, never fabricated (FLAG C), and fold-family calls desugar to seam `Loop` nodes (`fold_lowering.dag`). FLAGs D/E/F operator-SIGNED 2026-07-10 and the within-body FACT layer LANDED (#6443): one sugar rule table (`SugarKey` = surface-atom | production identity, type_alias_rhs migrated as proof), the 3-edge seam Loop (`^loop_carrier_edge`, at-most-one, excluded from the iteration fold in one motion; the lens carrier read is a named-edge lookup, the surface navigation deleted), the lexeme-stamped let binder, and the lens definition closure (`let grown = acc` a PROVEN suspect, transitively; pure-literal RHS decides clean; unbound RHS still refuses — the may_alias false-alarm class is dead; `^fold_accumulator_unread` narrowed to the named-step residue, a Stage-B callee-resolution fact). FLAG D condition: the binding-key re-grounding is REQUIRED cleanup before the feature closes. Remaining keystone: the **general body producer** — real ingested fn bodies still never become substrate behaviors (the MVP `03_body_producer` is fixture-bound to bespoke flat-token productions); the fn_decl→Arrow producer rows + scaffold dissolution are gated on the namespace lane's containment `SymbolIndex`, staged behind a typed wrapper-retained frontier (lowered | wrapper-retained{cause}, counted, corpus stays green). Fix = the forward reading of the same `GrammarRelationRow` rows the emitter reads backward (§4 one-grammar-both-directions): one row-selected fold in normalize, exactly-one selection fail-closed, staged within-body → cross-decl → per-op derivation, each stage priced by the refusal buckets it zeroes with RED controls kept live. → [body-lowering design](docs/plans/body-lowering-design.md) · [general body producer design](docs/plans/general-body-producer-design.md)
 - **namespace-only name resolution — the containment tree is the single naming authority (operator-signed 2026-07-06).** Supersedes resolver-graph-major §1c's *import-name-universe* ("own declarations ∪ direct import lists" visibility), carrying forward its mechanics unchanged (binding-edge owner, unbound/double-bound = error, patterns-via-scrutinee, no expected-type picker). One structure — **syntactic containment** — induces everything at once: qualified name = nesting position (`T{a}` → `a` *is* `T.a`; `T{a{a}}` → inner *is* `T.a.a`, so Rule-2 no-ambiguity holds by construction), reference = lexical lookup up the ancestor chain (a sibling module is visible, its members projected `node.Symbol`), `.` = projection one level down (field / module-member / variant — one op), and `.` *is* the `std.induction` sub-value relation (descent evidence). So one content-addressed tree grounds THREE consumers — resolution *walks* it, content-addressing *hashes* it, termination reads its *sub-value* edges (§2 Realization: one structure, N consumers). Frontend BUILDS the tree from nesting (pure structure, zero resolution logic); backend WALKS it (lexical up, project down) — no heuristics to tune (the tuning risk = resolving against a flat index instead of the tree). Two governing rules (operator, 2026-07-06): **no dual representation / minimal at every layer; no ambiguity at any layer.** Rides on `SymbolIndex` = "the containment tree materialized" (`type-env-single-authority`, lively-raven lane), gated on loyal-heron's scaling receipt before any resolver surgery; `import-scoped` (§1c, today) and `namespace-only-Y` (position-info uniqueness: expected type filters a variant to one, never picks) are two walk-rules over one *fill-agnostic* index (fill = whole tree; policy gates lookup, never fill). Census: 98% of names globally unique → always bare; the residue is v1-seed forks (resolve by subtree, free) + github-style variants ((Y) context-resolves); no consolidate-now forks (the census's 2 same-name flags proved to be a homonym + whole-file v1-seed duplication, not genuine cross-tree §3 forks). Terminal step: delete the `import` grammar + supporting code → `import` becomes a *parse error*, deps derived from `container.member` references (Rule-1 end-state). → [namespace-only resolution design](docs/plans/namespace-resolution-design.md)
 - **fleet-reconcile spine — one grain-agnostic membership diff (deploy · fleet · session).** ONE `membership_reconcile<M,K>` reuses `std.change.keyed_two_way_diff` verbatim (no fork): desired set vs observed set keyed by member IDENTITY — Added/Modified → upsert, Removed → teardown-or-refuse, Unchanged → noop (absence of a hunk). A member may be a service/unit/host OR a Session (operator: 'it should all be the same'), so a new member type is a new instantiation of the same fn with its own `(key_of, key_eq, value_eq, ownership_of)` bundle — zero spine change (a Realization, §2; a forked reconcile means the genericity bought nothing). R5 teardown-owned-only is a CONSTRUCTION WALL: a Removed non-owned member yields `MemberTeardownRefused`, which has no effect arm in any apply dispatch, so the bad state is unwritable — never a post-check, never 'assume owned' (the absorbing fallback §5 forbids); ownership-unknown REFUSES too, typed/located/counted. Ownership is extracted as its own single authority (`gunbc.ownership.Ownership`) and `live_deploy`'s `DeploymentStep` re-grounds onto it (pass 2, a declared dissolution trigger — never a second `Owned|Ensured`). Pass 1 (spine + R5 + a synthetic discriminating witness the degenerate apply/retract poles cannot exercise) landed. → [membership-diff reconcile spine design](docs/plans/membership-diff-reconcile-spine-design.md)
+- **effect grants over namespaces — dissolve `Hermetic | Wet` into (frame × verb × subtree).** The 2-valued `Hermetic | Wet` enum conflates four axes (input closure / replayability, output reach / interference, handler binding, selection eligibility) — a §3 state-space conflation with proto-envelopes already forked (the hand-rolled `workspace_root` containment gate, `std.resources.ResourceHandle`, `AuthScope`, `LiveTreeDisposition`). End shape (§3, cited not minted): an effect target is a position in a containment tree that already exists — filesystem paths, URIs, `/proc`, service-operation paths, and the unifying case **code names themselves** (the containment tree the namespace-resolution lane makes the single naming authority); permission is a grant of (verb × subtree) attached to a `Frame`; admissibility is the namespace prefix relation — the same `⊑` the resolver walks, content-addressing hashes, and termination reads, so effects become the **fourth consumer** of the one containment structure. Dispatch checks the envelope fail-closed (`EffectOutsideGrant`, a typed/located/counted refusal, never a silent widen — §5); *replayable* / *isolated* / `LiveTreeDisposition` become **derived** projections, and `Hermetic | Wet | Record` survive only as named envelope presets, deleted at the end. Frame-containment is graded on the §5 construction/validation axis (`LifecycleByConstruction` vs `LifecycleByConvention`). No code lands from the design doc; the FLAG-A interim is the only near-term consumer. → [effect-namespace-grants design](docs/plans/effect-namespace-grants.md)
 
 ## Building & checks
 

dag/gunbc/design_document.dag

@@ -146,6 +146,7 @@ fn open_threads_blocks() -> List<MarkdownBlock> {
       li(text: "**body-lowering — make v2's inferred tree faithfully represent runtime iteration.** Stages 1–3 LANDED (#6373): `DescentEvidence` consolidated onto its single authority `dag/std/termination.dag` (§7 ruling, parent 2026-07-03), `loop_multiplicity` is node-aware (termination derived from the `^loop_bound_edge` measure, fail-closed to `DescentUnknown`; FLAG B asymmetry rationale in-code), `04_infer` has a Loop arm typing the iteration fold `τ→τ` with refinement-shaped loops refused, never fabricated (FLAG C), and fold-family calls desugar to seam `Loop` nodes (`fold_lowering.dag`). FLAGs D/E/F operator-SIGNED 2026-07-10 and the within-body FACT layer LANDED (#6443): one sugar rule table (`SugarKey` = surface-atom | production identity, type_alias_rhs migrated as proof), the 3-edge seam Loop (`^loop_carrier_edge`, at-most-one, excluded from the iteration fold in one motion; the lens carrier read is a named-edge lookup, the surface navigation deleted), the lexeme-stamped let binder, and the lens definition closure (`let grown = acc` a PROVEN suspect, transitively; pure-literal RHS decides clean; unbound RHS still refuses — the may_alias false-alarm class is dead; `^fold_accumulator_unread` narrowed to the named-step residue, a Stage-B callee-resolution fact). FLAG D condition: the binding-key re-grounding is REQUIRED cleanup before the feature closes. Remaining keystone: the **general body producer** — real ingested fn bodies still never become substrate behaviors (the MVP `03_body_producer` is fixture-bound to bespoke flat-token productions); the fn_decl→Arrow producer rows + scaffold dissolution are gated on the namespace lane's containment `SymbolIndex`, staged behind a typed wrapper-retained frontier (lowered | wrapper-retained\{cause\}, counted, corpus stays green). Fix = the forward reading of the same `GrammarRelationRow` rows the emitter reads backward (§4 one-grammar-both-directions): one row-selected fold in normalize, exactly-one selection fail-closed, staged within-body → cross-decl → per-op derivation, each stage priced by the refusal buckets it zeroes with RED controls kept live. → [body-lowering design](docs/plans/body-lowering-design.md) · [general body producer design](docs/plans/general-body-producer-design.md)"),
       li(text: "**namespace-only name resolution — the containment tree is the single naming authority (operator-signed 2026-07-06).** Supersedes resolver-graph-major §1c's *import-name-universe* (\"own declarations ∪ direct import lists\" visibility), carrying forward its mechanics unchanged (binding-edge owner, unbound/double-bound = error, patterns-via-scrutinee, no expected-type picker). One structure — **syntactic containment** — induces everything at once: qualified name = nesting position (`T\{a\}` → `a` *is* `T.a`; `T\{a\{a\}\}` → inner *is* `T.a.a`, so Rule-2 no-ambiguity holds by construction), reference = lexical lookup up the ancestor chain (a sibling module is visible, its members projected `node.Symbol`), `.` = projection one level down (field / module-member / variant — one op), and `.` *is* the `std.induction` sub-value relation (descent evidence). So one content-addressed tree grounds THREE consumers — resolution *walks* it, content-addressing *hashes* it, termination reads its *sub-value* edges (§2 Realization: one structure, N consumers). Frontend BUILDS the tree from nesting (pure structure, zero resolution logic); backend WALKS it (lexical up, project down) — no heuristics to tune (the tuning risk = resolving against a flat index instead of the tree). Two governing rules (operator, 2026-07-06): **no dual representation / minimal at every layer; no ambiguity at any layer.** Rides on `SymbolIndex` = \"the containment tree materialized\" (`type-env-single-authority`, lively-raven lane), gated on loyal-heron's scaling receipt before any resolver surgery; `import-scoped` (§1c, today) and `namespace-only-Y` (position-info uniqueness: expected type filters a variant to one, never picks) are two walk-rules over one *fill-agnostic* index (fill = whole tree; policy gates lookup, never fill). Census: 98% of names globally unique → always bare; the residue is v1-seed forks (resolve by subtree, free) + github-style variants ((Y) context-resolves); no consolidate-now forks (the census's 2 same-name flags proved to be a homonym + whole-file v1-seed duplication, not genuine cross-tree §3 forks). Terminal step: delete the `import` grammar + supporting code → `import` becomes a *parse error*, deps derived from `container.member` references (Rule-1 end-state). → [namespace-only resolution design](docs/plans/namespace-resolution-design.md)"),
       li(text: "**fleet-reconcile spine — one grain-agnostic membership diff (deploy · fleet · session).** ONE `membership_reconcile<M,K>` reuses `std.change.keyed_two_way_diff` verbatim (no fork): desired set vs observed set keyed by member IDENTITY — Added/Modified → upsert, Removed → teardown-or-refuse, Unchanged → noop (absence of a hunk). A member may be a service/unit/host OR a Session (operator: 'it should all be the same'), so a new member type is a new instantiation of the same fn with its own `(key_of, key_eq, value_eq, ownership_of)` bundle — zero spine change (a Realization, §2; a forked reconcile means the genericity bought nothing). R5 teardown-owned-only is a CONSTRUCTION WALL: a Removed non-owned member yields `MemberTeardownRefused`, which has no effect arm in any apply dispatch, so the bad state is unwritable — never a post-check, never 'assume owned' (the absorbing fallback §5 forbids); ownership-unknown REFUSES too, typed/located/counted. Ownership is extracted as its own single authority (`gunbc.ownership.Ownership`) and `live_deploy`'s `DeploymentStep` re-grounds onto it (pass 2, a declared dissolution trigger — never a second `Owned|Ensured`). Pass 1 (spine + R5 + a synthetic discriminating witness the degenerate apply/retract poles cannot exercise) landed. → [membership-diff reconcile spine design](docs/plans/membership-diff-reconcile-spine-design.md)"),
+      li(text: "**effect grants over namespaces — dissolve `Hermetic | Wet` into (frame × verb × subtree).** The 2-valued `Hermetic | Wet` enum conflates four axes (input closure / replayability, output reach / interference, handler binding, selection eligibility) — a §3 state-space conflation with proto-envelopes already forked (the hand-rolled `workspace_root` containment gate, `std.resources.ResourceHandle`, `AuthScope`, `LiveTreeDisposition`). End shape (§3, cited not minted): an effect target is a position in a containment tree that already exists — filesystem paths, URIs, `/proc`, service-operation paths, and the unifying case **code names themselves** (the containment tree the namespace-resolution lane makes the single naming authority); permission is a grant of (verb × subtree) attached to a `Frame`; admissibility is the namespace prefix relation — the same `⊑` the resolver walks, content-addressing hashes, and termination reads, so effects become the **fourth consumer** of the one containment structure. Dispatch checks the envelope fail-closed (`EffectOutsideGrant`, a typed/located/counted refusal, never a silent widen — §5); *replayable* / *isolated* / `LiveTreeDisposition` become **derived** projections, and `Hermetic | Wet | Record` survive only as named envelope presets, deleted at the end. Frame-containment is graded on the §5 construction/validation axis (`LifecycleByConstruction` vs `LifecycleByConvention`). No code lands from the design doc; the FLAG-A interim is the only near-term consumer. → [effect-namespace-grants design](docs/plans/effect-namespace-grants.md)"),
     ]),
   ]
 }