Delete flatten_visible_bindings + merge_envs + env-counter instrument: one-level visibility by construction (floor resolve 286.7s -> 2.4s)

.gitignore

@@ -111,6 +111,7 @@ out.txt
 # --- Python local dev scripts ---
 # Python is used only for local dev tooling; never committed to the .dag/.rs substrate
 *.py
+!docs/plans/witness-subject-execution-audit.py
 
 # --- CPython bytecode cache (PEP 3147) [cited: python.org/peps/pep-3147] ---
 __pycache__/

dag/extdeps/accounting/budget.dag

@@ -1,6 +1,7 @@
 module extdeps.accounting.budget
 
 import std.measure { Measure, measure_add, measure_le }
+import std.nat { Nat }
 import extdeps.external_authority { ExternalAuthority }
 import extdeps.uri { Uri, Https }
 

dag/extdeps/cloud/gcp/iam.dag

@@ -2,7 +2,7 @@ module extdeps.cloud.gcp.iam
 
 import extdeps.cloud.gcp.gcp { GcpServiceAccount, GcpProject, GcpProjectId, ServiceAccountEmail }
 import extdeps.cloud.gcp.errors { GcpErrorShape }
-import std.types { HttpMethod, AuthScheme }
+import std.types { HttpMethod, AuthScheme, NonEmptyStr }
 
 import extdeps.external_authority { ExternalAuthority }
 import extdeps.uri { Uri, Https }

dag/extdeps/cloud/gcp/iam_admin.dag

@@ -2,7 +2,7 @@ module extdeps.cloud.gcp.iam_admin
 
 import extdeps.cloud.gcp.gcp { GcpProjectId, GcpServiceAccount, GcpOperation, ServiceAccountEmail }
 import extdeps.cloud.gcp.errors { GcpErrorShape }
-import std.types { HttpMethod, AuthScheme }
+import std.types { HttpMethod, AuthScheme, NonEmptyStr }
 
 import extdeps.external_authority { ExternalAuthority }
 import extdeps.uri { Uri, Https }

dag/extdeps/cloud/gcp/secret_manager.dag

@@ -3,7 +3,7 @@ module extdeps.cloud.gcp.secret_manager
 import extdeps.cloud.gcp.gcp { GcpProject, GcpProjectId }
 import extdeps.cloud.gcp.iam { GcpBinding, GcpPolicy }
 import extdeps.cloud.gcp.errors { GcpErrorShape }
-import std.types { HttpMethod, AuthScheme, Bytes, Secret }
+import std.types { HttpMethod, AuthScheme, Bytes, Secret, NonEmptyStr }
 import std.encoding { utf8_decode_bytes }
 
 import extdeps.external_authority { ExternalAuthority }

dag/gunbc/accelerator_demo_realize.dag

@@ -2,6 +2,7 @@ module gunbc.accelerator_demo_realize
 
 import std.types { Bool, Int, List, Float }
 import std.numerical_contract {
+  FmaContractionPolicy,
   NumericalContract,
   FloatApproximate,
   FmaContractionRefused,

dag/gunbc/assimilate/bmc_token_federation.dag

@@ -20,6 +20,7 @@ import extdeps.languages.yaml.types { YamlKeyValue, kv, yaml_string }
 import extdeps.languages.yaml.emit { serialize_yaml }
 import extdeps.languages.yaml.gha_workflow { project_workflow_to_yaml }
 import gunbc.runner_spec_from_offer { gunbc_ci_runner_spec }
+import std.types { NonEmptyStr }
 
 data bmc_secrets_project_id: GcpProjectId = "gunbai-secrets"
 

dag/gunbc/design_document.dag

@@ -101,7 +101,7 @@ fn section_5_blocks() -> List<MarkdownBlock> {
   [
     h2(text: "5. Fail-closed (§1's safety axis — harm reduction)"),
     p(text: "Minimizing cost and complexity (§2–§4) is worthless if a wrong thing passes silently — this is §1's safety axis made concrete. This code is digital: a wrong answer is a **loud error, never a warning** — a bridge collapses, it does not warn. Every path succeeds fully or fails with a typed, located diagnostic; no fabricated plausible output (a bounded \"forever\" ≠ an \"unknown\" error). Relax toward application-layer leniency only under protest, and lean to infra so others can build on your work. Stronger than *catching* a wrong state is making it **unwritable** — **correctness by construction, not validation.** A check that re-states a constraint the model already carries is a *second representation* of it (§2/§3): so prefer a single authority from which the realization is *derived* — the bad state cannot be written — over a check that flags it after the fact, which concedes the bad state *is* writable. The tell that a check was validation standing where construction was available: it can be satisfied by editing the *declaration* while the realization still lies (a key-completeness check went green when the spec was edited while the realizer kept faking the cache key). Reserve post-hoc checks for the genuinely **unstructurable** residue (§6 complexity / necessity — you cannot structurally forbid an *unnecessary* loop). Construction makes a class unwritable only when membership is **decidable**, so every class is one of three: a *wall now* (decidable and grounded — nicknaming, dead scaffolds, effect leaks); a *wall after grounding* (decidable but waiting on its single authority — the cross-representation `==` straddle is one only once `Int = GroupCompletion<Nat>` grounds it); or a *ratchet forever* (undecidable — optimality, by Rice, never reaches \"never\"). The word **\"never\" is the trap**: it lets a ratchet masquerade as a wall, so check decidability before claiming one — the undecidable residue is the §6 lens, honestly and permanently. The deepest trap is **specification-without-execution**: a typecheck and a `.contains()` grep are *not* consumers — \"done\" means a real consumer **green by execution** plus a discriminating input that goes *red* when the behavior is wrong. (For the LLM agent: fluent, type-checking, grep-passing output is precisely the artifact that looks finished without running. Treat your own output as unverified until a consumer runs it green.)"),
-    p(text: "A third named trap, the subtlest because it wears this section's own name: **the absorbing fallback — degradation is disguised fail-open.** When a mechanism cannot compute its precise answer, the tempting failure arm substitutes the *superset* instead: can't compute the affected set → rerun the entire suite; cache key uncertain → scan all keys; provenance unavailable → always run. Nothing is *missed*, so the arm gets labeled fail-closed — but it is the fabricated plausible output one level up: **⊤-as-answer conflated with ⊤-as-ignorance** (state-space conflation on the answer lattice — \"everything is affected\" and \"I could not compute what is affected\" are different states whose remedies differ), and it fails open twice. On safety: absorption destroys the only signal that the precise mechanism has a deficit — the failure's frequency is zero *by construction*, so the deficit never ranks for fixing (§6 prices by displaced cost, and a masked cost displaces nothing) and the anemia compounds (the scan-all-keys heuristic in the receipt below was this exact absorption; removing it exposed 8 deficits its silence had hidden). On cost: the fallback is denominated in the *corpus*, not the *change*, so it grows with the repo until the *budget* breaks instead of the build — later, loudly, at interest: §1's safety debt paid in §1's cost currency. And the confidence **threshold** that selects such an arm is a smuggled heuristic — §4 already rules a heuristic never necessary in a closed system — so the threshold's very existence *locates* the anemic modeling it papers over: a solution that must keep degrading to stay green is not a solution being cautious, it is a model being wrong. The rule, and the review tell: **a failure arm must refuse, never widen** — every degradation a typed, located, *countable* diagnostic, so its frequency is observable and prioritizable, never an absorbed rerun. Two neighbors are not this pattern (check the *trigger*: structure vs failure-state): a structural over-approximation computed *as* the answer (a dependency-closure superset is the model's precision frontier, not an absorption), and a deliberate interim fallback that is loud, budget-bounded, and lands with its §6 dissolution trigger. Silent unbounded absorption is never the third."),
+    p(text: "A third named trap, the subtlest because it wears this section's own name: **the absorbing fallback — degradation is disguised fail-open.** When a mechanism cannot compute its precise answer, the tempting failure arm substitutes the *superset* instead: can't compute the affected set → rerun the entire suite; cache key uncertain → scan all keys; provenance unavailable → always run. Nothing is *missed*, so the arm gets labeled fail-closed — but it is the fabricated plausible output one level up: **⊤-as-answer conflated with ⊤-as-ignorance** (state-space conflation on the answer lattice — \"everything is affected\" and \"I could not compute what is affected\" are different states whose remedies differ), and it fails open twice. On safety: absorption destroys the only signal that the precise mechanism has a deficit — the failure's frequency is zero *by construction*, so the deficit never ranks for fixing (§6 prices by displaced cost, and a masked cost displaces nothing) and the anemia compounds (the scan-all-keys heuristic in the receipt below was this exact absorption; removing it exposed 8 deficits its silence had hidden). On cost: the fallback is denominated in the *corpus*, not the *change*, so it grows with the repo until the *budget* breaks instead of the build — later, loudly, at interest: §1's safety debt paid in §1's cost currency. And the confidence **threshold** that selects such an arm is a smuggled heuristic — §4 already rules a heuristic never necessary in a closed system — so the threshold's very existence *locates* the anemic modeling it papers over: a solution that must keep degrading to stay green is not a solution being cautious, it is a model being wrong. The rule, and the review tell: **a failure arm must refuse, never widen** — every degradation a typed, located, *countable* diagnostic, so its frequency is observable and prioritizable, never an absorbed rerun. Two neighbors are not this pattern (check the *trigger*: structure vs failure-state): a structural over-approximation computed *as* the answer (a dependency-closure superset is the model's precision frontier, not an absorption), and a deliberate interim fallback that is loud, budget-bounded, and lands with its §6 dissolution trigger. Silent unbounded absorption is never the third. A corollary on the refusal itself: **no escape hatches** — a toggle whose only effect is \"proceed as if the refusal had not fired\" (an env var, a flag, a silence mode) re-opens the arm §5 just closed, one config edit from silent (operator ruling, 2026-07-05). The operative discipline is the **factory model — and it is a merge requirement, not a preference** (operator ruling, 2026-07-05): a deficit stops the line (typed, located refusal); the stopped line is analyzed before it restarts; the only sanctioned second mode is a *stopped-line audit* that replays the run to ledger every deficit (typed, located, counted) for that analysis — it reports, it does not green. Diagnostic modes read state; no mode writes \"keep going.\" **Review bar:** a diff that lands a non-fail-closed failure arm — a silent widen, a fabricated default, an uncounted degradation, an escape hatch — is a **hard reject** in code review, regardless of what else the PR delivers. The reviewer's three questions: does the line stop? is the stop typed and located? does analysis precede restart?"),
     ul(items: [
       li(text: "*e.g.* a compiler-sized `.dag` corpus typechecked and passed its grep claims, yet `emit` hung >600s on `fn add` → rebuilt `emit = serialize_target ∘ translate` (43 lines), proven by *running* `emit(add)` against the literal `fn add(x: i32, y: i32) -> i32 \{ x + y \}`. Removing a scan-all-keys fail-open heuristic (`0331b526ee`) exposed 8 real inference deficits its fabrication had hidden; the parser's dummy `LitNull` nodes once fed inference bogus types. The absorbing fallback, formerly live in tree: `floor_witness_run_disposition` (`src/v2/workflow/affected_set_floor_runner.dag`) answered `DiffObservationFailClosed`, `FrontierFailClosed`, *and* the empty diff with `RunWitness` — one arm literally `\"empty diff — run full corpus (fail-closed)\"`, with tests *asserting the string* so the degradation was enshrined as the contract — and the corpus-denominated cost duly surfaced as CI's 90-minute timeout, not as a diagnostic. Repaired in two halves: the Building-&-checks enrollment inversion (the loud half), then the arms converted to typed refusals — `Refused` with per-cause variants, per-row counted, siblings continue — with the empty diff dissolved into the general disposition, never a special arm (operator rulings, 2026-07-05)."),
     ]),
@@ -148,6 +148,7 @@ fn open_threads_blocks() -> List<MarkdownBlock> {
       li(text: "the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)"),
       li(text: "floor shared-computation memoization — make the double-paid full-tree compile UNREPEATABLE by construction (M1: within-walk resolve memo ~105s; M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md)"),
       li(text: "**body-lowering — make v2's inferred tree faithfully represent runtime iteration.** The substrate models a `Loop` faithfully (measure `^loop_bound_edge` + iteration-fold body, §4), but the inferred tree drops both loop facts: `behavior_multiplicity(Loop)` decides termination **tag-only** (never reading the measure) so every raw loop is `Violates` regardless of its descent evidence (`cardinality.dag:219-228`), the `LoopBound\{measure,termination\}` carrier that would bind measure→proof is consumed only by the cost/complexity lenses (`cost.dag:168`) which read its `measure` for sizing but **never** its `termination` — and that `termination` field is itself computed **measure-blind** (tag-only, `cardinality.dag:284`), so **no inference consumes the loop's termination fact** (`loop_bound_witness_for_node`, `cardinality.dag:278`), and `04_infer` has **no Loop arm** so the body is typed as an opaque conjunction with no per-iteration `τ→τ` relation. Fix = derive termination from the measure (fail-closed to `DescentUnknown`) + type the body as a repeated transform, both as `Loop` sugar readers (so `For`/`While`/`Retry`/recursion type at once). Blocked-on: a `DescentEvidence` §3 fork (`cardinality.dag:108` bare vs `dag/std/termination.dag` lattice) consolidates first — **authority ruled `dag/std/termination.dag`** (§7; parent 2026-07-03), landing held for the operator's *standing* v2↔dag-fork confirm. FLAG B (Loop-multiplicity asymmetry) SIGNED; FLAG C (refinement loops fail-closed, not fabricated `τ→τ`) SIGNED. → [body-lowering design](docs/plans/body-lowering-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)"),
     ]),
   ]
 }

dag/gunbc/network_identity_subsumption.dag

@@ -4,6 +4,7 @@ import std.types { NonEmptyStr, Bool, List, String }
 import std.disposition { Disposition, Terminal }
 import extdeps.dhcp.v4 {
   DhcpLeaseObservation,
+  DhcpClientHostNameOption12,
   DynamicDhcpLease,
   StaticDhcpReservation,
   Active,
@@ -39,7 +40,7 @@ data srv3_fleet_slot_host_name: HostName = HostName {
 }
 
 fn dynamic_lease_hostname_subsumes_fleet_slot(
-  reported: HostName,
+  reported: DhcpClientHostNameOption12,
   fleet_slot: HostIdentity,
 ) -> Bool {
   match deployed_intent_v1_desired_hostname_short(fleet_slot: fleet_slot) {

dag/std/resources.dag

@@ -2,6 +2,7 @@ module std.resources
 
 import std.filesystem { FileClassification }
 import std.types { Timestamp, FilePath, TextFilePath }
+import std.integer { UInt8 }
 import std.measure { ByteSize }
 
 type ResourceHandle {

dag/test/claim/budget_tree_witness_test.dag

@@ -1,6 +1,7 @@
 module test.claim.budget_tree_witness
 
 import std.logic { Bool }
+import std.nat { Nat }
 import std.measure { byte_size, Memory, One }
 import extdeps.accounting.budget {
   Appropriation, LineItem, BudgetBalance, Surplus, Balanced, Deficit,

dag/test/claim/compile_source_model_witness_test.dag

@@ -1,6 +1,7 @@
 module test.claim.compile_source_model_witness
 
 import gunbc.compile_source_model {
+  SourceRootRole,
   StrictPoolIndex,
   PrimaryPrecedencePoolIndex,
   EntrySourceRoot,

dag/test/claim/hardware_selection_witness_test.dag

@@ -2,7 +2,7 @@ module test.claim.hardware_selection
 
 import std.logic { Bool }
 import std.types { Int, List }
-import std.measure { byte_size, byte_size_count, bit_width, watt, watt_count, hardware_thread_count, hertz, money_amount_micro }
+import std.measure { ByteSize, byte_size, byte_size_count, bit_width, watt, watt_count, hardware_thread_count, hertz, money_amount_micro }
 import product.hardware_selection { milliwatt }
 import extdeps.cpu.types { CpuModelCatalogRow, CpuSocket, SocketPackage }
 import extdeps.toolchain.types { Architecture }

dag/test/claim/roadmap_dispatch_actuator_witness_test.dag

@@ -1,6 +1,7 @@
 module test.claim.roadmap_dispatch_actuator
 
 import ctrl.process_algebra { ProcessNodeId }
+import std.types { NonEmptyStr, GitRef, FilePath }
 import gunbc.roadmap_model {
   RoadmapNode, RoadmapEdge,
   IntricacyHigh, VolumeMedium,