gunbc Director

docs/briefs/r1-surface-manager.md

@@ -1,5 +1,18 @@
 # R1 Surface Manager Brief
 
+> **🔄 SUPERSEDED 2026-04-26 by [`r1-closure-manager.md`](r1-closure-manager.md).**
+> R1 gate-close authority now lives with the R1 Closure Manager (PR #847)
+> under strict-interpretation reading: every gate in `ROADMAP.md §"Lane
+> acceptance — .dag gates"` must be a `.dag` `TestClaim` that compiles AND
+> evaluates true. Implementation receipts are necessary but **not sufficient**.
+> The "Working state" section below was originally written under a more
+> permissive reading where receipt-landed counted as gate-closed; that
+> conflation is corrected in the table — implementation receipts and `.dag`
+> gate status are now tracked as separate columns. Gates remain owned by
+> R1 Closure Manager lanes (R1C-A through R1C-F) until they evaluate.
+> This brief stays in-tree as a historical receipt of the lane sequencing;
+> new R1 dispatch happens under R1 Closure Manager, not here.
+
 ## Orient before reading
 
 - Product direction: [PR #672](https://github.com/gunb-ai/gunbc/pull/672)
@@ -120,45 +133,39 @@ for a principal engineer to verify in one evening.
 
 ## Working state
 
-Lane-owner dispatch status (update as sub-deliverables close):
-
-**T-P0 (closed on current ancestry):**
-- [x] `repeat_string` fix landed (brief: `p0-render-repeat-string.md`)
-- [x] `REST_OPS` drift resolved (brief: `p0-rest-ops-drift.md`)
-- [x] `no_profile_sentinel` audit completed (brief: `p0-bug-no-profile-sentinel.md`)
-
-**T-Sub:**
-- [x] `sub_match_over_user_sum` gate compiles + passes (Day-1)
-      (PR #702, merged 2026-04-24 — `TestClaim` + suite in
-      `src/v3/compiler/tests/fixtures/r1_gates.dag` run through
-      `TestRunner`; #690 prior receipt confirmed structural match)
-- [x] `sub_type_alias_where_lowers` parse + lower receipt landed
-      (DB-11 parse + lower substrate landed in PR #703, 2026-04-24 —
-      `SurfaceItem::TypeAlias` carries `refinement`; formal `.dag`
-      gate remains tied to the [ext] predicate path if release wants
-      a first-class `TestClaim` for this surface)
-- [ ] `sub_charclass_in_std_unicode` phase-2 handed off with concrete
-      substrate/load-set blockers
-      (phase-1 tokenizer half landed in PR #693 + ROADMAP row #706,
-      2026-04-24 — `CharClass` + `char_in_class` in `std.unicode`,
-      tokenizer calls `tokenize_char_class::byte_matches`; quiet-gull-882
-      confirmed structural `CharClass` consumption from lowered
-      `tokenize.dag` is blocked by top-level `ValueBody` list/sum support
-      plus a `std.unicode` bootstrap/load-set decision)
-
-**T-Emit:**
-- [x] Rust harden — `emit_rust_fixtures_rustc_green` gate test landed
-      (PR #694, merged 2026-04-24 — `#[ignore]`d named gate sweeps
-      9 program fixtures + 5 reflected-module fixtures through the
-      batched rustc roundtrip; baseline `rustc_roundtrip_*` tests all
-      green)
-- [ ] PR #650 generic-bound fidelity — `emit_generic_bounds_survive`
-      passes (PR #676 in review — session `vivid-cat-794`)
-- [ ] Python/Go reconcile — `emit_omni_demo_fixtures_green` passes
-      across all three targets (cross-target progress 2026-04-24:
-      `Behavior::Loop` emission for Python + Go in #692; Python
-      operator-realization parity for `*` / `!=` / int comparisons
-      in #691; omni gate still pending)
+> **Reading note (2026-04-26 SUPERSEDED amendment).** Implementation receipts
+> (`Impl` column) record that the underlying feature work is in-tree. `.dag`
+> gate status (`Gate` column) records whether the corresponding `TestClaim`
+> in `ROADMAP.md §"Lane acceptance — .dag gates"` exists, compiles, and
+> evaluates true under the strict-interpretation reading. Gate columns are
+> closed only when both halves are true; the implementation-only `[x]` markings
+> below are deliberately separated from gate close so the conflation that
+> existed before this amendment doesn't recur. Gate-close authority is
+> R1 Closure Manager (`docs/briefs/r1-closure-manager.md`).
+
+**T-P0 — implementation closed on current ancestry; `.dag` gates owned by R1 Closure R1C-B:**
+
+| Item | Impl | Gate (`.dag` TestClaim) | Owner |
+|---|---|---|---|
+| `repeat_string` | [x] (brief: `p0-render-repeat-string.md`) | [ ] `p0_repeat_string_correct` `[Day 1]` | R1C-B |
+| `REST_OPS` drift | [x] (brief: `p0-rest-ops-drift.md`) | [ ] `p0_rest_ops_aligned` `[ext]` | R1C-B |
+| `no_profile_sentinel` | [x] (brief: `p0-bug-no-profile-sentinel.md`) | [ ] `p0_no_fabrication_sentinel` `[ext]` | R1C-B |
+
+**T-Sub — `.dag` gates: 1 closed, 1 receipt-only, 1 substrate-deferred:**
+
+| Item | Impl | Gate (`.dag` TestClaim) | Owner |
+|---|---|---|---|
+| `sub_match_over_user_sum` (Day-1) | [x] PR #702 | [x] `TestClaim` + suite in `r1_gates.dag` runs through `TestRunner` | gate evaluates; closed |
+| `sub_type_alias_where_lowers` (`[ext]`) | [x] PR #703 (DB-11 parse+lower) | [ ] `[ext]` predicate path TestClaim **not yet authored** | R1C-C (#879 in flight) |
+| `sub_charclass_in_std_unicode` phase-2 | [x partial] PR #693 (phase-1 tokenizer half) | [ ] reclassified to **R2 T-Substrate** per 2026-04-24 amendment (Class 5 Gap 3) — no longer an R1 gate | R2 Substrate Manager |
+
+**T-Emit — implementation in flight; all three `.dag` gates owned by R1 Closure R1C-E:**
+
+| Item | Impl | Gate (`.dag` TestClaim) | Owner |
+|---|---|---|---|
+| Rust harden | [x] PR #694 (host-harness gate test, `#[ignore]`-able sweep) | [ ] `emit_rust_fixtures_rustc_green` `[ext: ExecuteCommand]` — host harness is **not** the `.dag` gate; R1C-E wraps it | R1C-E |
+| Generic-bound fidelity | [partial] PR #676 in review | [ ] `emit_generic_bounds_survive` `[ext]` | R1C-E |
+| Python/Go reconcile | [partial] #691 (Python parity) + #692 (`Behavior::Loop`) | [ ] `emit_omni_demo_fixtures_green` `[ext: ForAllTargets + ExecuteCommand]` | R1C-E |
 
 Decisions log (append as they happen):
 

docs/briefs/r2-impossible-bugs-nested-optional-flatten-worker.md

@@ -18,8 +18,8 @@
 - **[`THESIS.md` lines 342-344](../../THESIS.md)** — class definition.
 - **[`src/v3/compiler/src/dag.rs:408-411`](../../src/v3/compiler/src/dag.rs)** — `TypeConnective::Cardinality { element, bound }` first-class.
 - **[`src/v3/compiler/src/dag_scalar_generated.rs:21-25`](../../src/v3/compiler/src/dag_scalar_generated.rs)** — `CardinalityBound::AtMostOne` (the carrier for `Option`).
-- **[`src/v3/compiler/src/lower.rs:1949-1968, :2044-2047`](../../src/v3/compiler/src/lower.rs)** — `SurfaceType::Optional` lowering arms (call sites).
-- **[`src/v3/compiler/src/infer.rs:2902-2916`](../../src/v3/compiler/src/infer.rs)** — `concretize_decl_with_subst` (the **killer construction site** per design doc — substitution path that bypasses `lower.rs`).
+- **[`src/v3/compiler/src/lower.rs:2129, :2226`](../../src/v3/compiler/src/lower.rs)** — `SurfaceType::Optional` lowering arms (lowering path + TypeConnective construction). Verify by grep `SurfaceType::Optional` at HEAD before editing.
+- **[`src/v3/compiler/src/infer.rs:3129`](../../src/v3/compiler/src/infer.rs)** — `concretize_decl_with_subst` definition (the **killer construction site** per design doc — substitution path that bypasses `lower.rs`); call sites at `:2643, :2645, :3104, :3152, :3162, :3190` (grep `concretize_decl_with_subst` at HEAD for the live set).
 - **[`docs/modeling-discipline.md`](../modeling-discipline.md)** practice 6 — API-level enforcement over convention.
 - **`feedback_state_space_vs_behavioral_invariants`** — illegal states unrepresentable, not validated.
 

docs/briefs/r2-impossible-bugs-unenumerated-effects-worker.md

@@ -65,7 +65,7 @@ Per design doc default: retire (path ii).
 
 ## STOP-AND-ESCALATE (per design doc Q6 STOPs)
 
-- **OperationEffect retirement decision (path (i) vs (ii))** — if Slice §2 audit produces the existence-proof for path (ii) (any primitive whose signature doesn't structurally reveal its effect after resource-threading migration), STOP and surface retirement scope to Director. Substrate retirement (`OperationEffect` enum + `derive_op_effect` + `idempotency.dag` re-anchor) is its own dedicated sub-lane; this lane should not absorb it. If audit confirms path (i) (all primitives derive cleanly from signature shape), surface that finding for re-decision.
+- **OperationEffect retirement decision (path (i) vs (ii)) is NOT a STOP — the audit verdict IS this lane's deliverable.** Slice §2 + Acceptance §2 own producing the verdict (path-i existence-proof OR path-ii existence-proof) with structural justification + per-primitive receipt in PR body. The follow-up — actual `OperationEffect` enum retirement (path ii: enum + `derive_op_effect` + `idempotency.dag` re-anchor) or normalized-derived-view authoring (path i) — dispatches as a **sibling sub-lane** to Impossible-Bugs Manager based on the verdict; Director does not need to be in the loop for the verdict itself. **STOP only if** the audit reveals a primitive whose signature shape can't be made to derive cleanly **even after resource-threading migration (Slice §3)** — i.e., a substrate gap not anticipated by the design doc Q5.5 binary. That's an unscoped substrate-shape question, not a retain-vs-retire pick.
 - **Redundancy proof needs a `pure: Bool` carrier** — if the lens can't distinguish pure from impure Transforms inline, STOP. May need a sibling carrier on Transform targets. (Note: the deeper closed-system framing is that "pure" should also be derivable from signature shape — pure functions don't return modified resources — so this STOP may itself dissolve under further design.)
 - **Asymmetric-tightening structural gap** — if caller can't actually pin effect-set constraints structurally today (i.e., the type system doesn't yet express "I require callee body's signature-shape composition ⊆ {read-shaped}"), STOP — that's its own substrate sub-lane.
 - **Q4.5 P1 (extdeps typed-primitive bypass) — surfaced via lens findings**: lens reports structural-coverage-gap on `dsl/extdeps/llm/openai.dag:92-110`, `anthropic.dag:104-124`, `github/auth.dag:13-24` (and any others the audit finds). **NOT a STOP**; this is the lens delivering its closed-system-foundation-gap-visibility value. Director routes P1 closure to a dedicated extdeps-typed-primitive-consumption lane. Surface findings in PR body.

docs/briefs/r2-impossible-bugs-unhandled-diagnostic-paths-worker.md

@@ -20,9 +20,9 @@
 - **[`THESIS.md` lines 175, 348-350, 391](../../THESIS.md)** — class definition + the "made total" branch the design doc closes against.
 - **[`dsl/std/algebra.dag:182`](../../dsl/std/algebra.dag)** — `OrderedRing.div: fn(T, T) -> T` (the line to retype to total form).
 - **[`src/v3/compiler/src/infer.rs:3975-3977`](../../src/v3/compiler/src/infer.rs)** — algebra-Conj dispatch site for `Int / Int`.
-- **[`src/v3/spec/rust.dag:816`](../../src/v3/spec/rust.dag)** — `rust_int_div` realization (renders bare `{lhs} / {rhs}`).
-- **[`src/v3/spec/go.dag:742`](../../src/v3/spec/go.dag)** — `go_int_div` realization (same shape).
-- **[`src/v3/spec/python.dag:486`](../../src/v3/spec/python.dag)** — `python_int_div` realization (renders via `__v3_idiv` helper at `python_target.rs:680`; pinned by `m1_4_emit_python_test.rs:108-109`).
+- **[`src/v3/spec/rust.dag:832`](../../src/v3/spec/rust.dag)** — `rust_int_div` realization (renders bare `{lhs} / {rhs}`). (`:816` is `rust_int_sub` — verify by grep `rust_int_div` at HEAD.)
+- **[`src/v3/spec/go.dag:758`](../../src/v3/spec/go.dag)** — `go_int_div` realization (same shape). (`:742` is `go_int_sub`.)
+- **[`src/v3/spec/python.dag:500`](../../src/v3/spec/python.dag)** — `python_int_div` realization (renders via `__v3_idiv` helper at `src/v3/compiler/src/emit/python_target.rs:680`; pinned by `m1_4_emit_python_test.rs:108-109`). (`:486` is inside `python_int_sub`.)
 - **[`dsl/std/algebra.dag:477-478`](../../dsl/std/algebra.dag)** — `OrderedRing.quotient` / `OrderedRing.remainder` (separate per-class sub-lane candidates per design doc audit).
 - **`feedback_totality_by_omission`** — discipline anchor: partial-op classes close by removing the partial form; coexistence-with-paired-total is the trap.
 
@@ -47,9 +47,9 @@ Per design doc §4: the bug class closes by **removing the partial form**. For `
 2. **Per-row decision** — for `Int / Int`: pick Result-shape `Result<T, DivError>` where `DivError = DivideByZero | Overflow` (or worker-equivalent typed split that preserves distinct failure modes). **NOT a single-error `Result<T, DivideByZero>`** — signed integer division has two structurally distinct failure modes (zero divisor + signed overflow on `MIN / -1`), and collapsing them violates fail-closed C-8 (per `feedback_fail_closed_discipline`: each detectable problem is its own typed Diagnostic). **Option-shape (`Option<T>`) also rejected** for the same reason — `None` carries no failure-mode information. **STOP-AND-ESCALATE for NonZero-typed-input shape** (e.g., `a / nz` rather than `divide_nz(a, nz)`) — that's a per-operand type-variance question deferred to a separate substrate brief.
 3. **Algebra retype**: one-line change at `algebra.dag:182` to the total return type. **The total return type carries a typed-split error carrier** (e.g., `DivError`) per Slice §2 — surface the carrier declaration's location (likely `dsl/std/errors.dag` or a sibling under `dsl/std/algebra.dag`).
 4. **Per-target realization migration** — each target reshapes from bare division to construct the typed-split Result idiomatically; **must distinguish divide-by-zero from overflow** (do NOT collapse to a single error variant):
-   - `rust.dag:816` — `rust_int_div` reshapes to explicit branching: `if rhs == 0 { Err(DivError::DivideByZero) } else if /* overflow check */ { Err(DivError::Overflow) } else { Ok(lhs / rhs) }`. Note: `i64::checked_div` collapses both failures to `None`, so it's NOT a one-line `ok_or` — the realization must split the cases. Worker authors the exact Rust idiom; surface in PR.
-   - `go.dag:742` — `go_int_div` reshapes to Go-idiomatic typed-split Result; same case-split discipline.
-   - `python.dag:486` + `python_target.rs:680` helper — reshape `__v3_idiv` to return typed-split Result; update test pin at `m1_4_emit_python_test.rs:108-109`. (Python's overflow semantics differ from Rust's — surface the per-target equivalence in PR body.)
+   - `rust.dag:832` (`rust_int_div`) — reshapes to explicit branching: `if rhs == 0 { Err(DivError::DivideByZero) } else if /* overflow check */ { Err(DivError::Overflow) } else { Ok(lhs / rhs) }`. Note: `i64::checked_div` collapses both failures to `None`, so it's NOT a one-line `ok_or` — the realization must split the cases. Worker authors the exact Rust idiom; surface in PR.
+   - `go.dag:758` (`go_int_div`) — reshapes to Go-idiomatic typed-split Result; same case-split discipline.
+   - `python.dag:500` (`python_int_div`) + `src/v3/compiler/src/emit/python_target.rs:680` helper — reshape `__v3_idiv` to return typed-split Result; update test pin at `m1_4_emit_python_test.rs:108-109`. (Python's overflow semantics differ from Rust's — surface the per-target equivalence in PR body.)
 5. **Audit fallback path** — `infer.rs:4003-4015` Rust-side primitive scaffold (general fallback for types whose `inhabits` chain doesn't reach an algebra Conj). Slice §1 audit confirms whether any types still resolve `Arithmetic(Div)` through that fallback; close those paths separately if so.
 6. **Regression tests:**
    - `Int / Int` returns `Result<Int, DivError>` with both `DivideByZero` and `Overflow` variants reachable.
@@ -76,7 +76,7 @@ Per design doc §4: the bug class closes by **removing the partial form**. For `
 - **NonZero-typed-input shape chosen** (`a / nz` operator-syntax rather than `divide_nz(a, nz)` function syntax) — STOP. Per-operand type variance in algebra-operator carrier is a separate substrate brief.
 - **Audit reveals additional partial forms not enumerated in design doc** — surface; queue as sibling sub-lanes; do not subsume in this PR.
 - **Realization migration breaks emission for an existing target idiom** — surface; this is a target-realization design call, not a worker call.
-- **`Result<T, DivideByZero>` requires authoring `DivideByZero` declaration** — verify it doesn't exist via audit; if not, surface placement decision (`std.errors.dag`?).
+- **`Result<T, DivError>` requires authoring `DivError` (with `DivideByZero | Overflow` variants) declaration** — verify the typed-split carrier doesn't exist via audit; if not, surface placement decision (`dsl/std/errors.dag`?). Single-error `Result<T, DivideByZero>` shape is explicitly rejected per Slice §2; STOP if any reading drifts back to a single-variant carrier.
 - **Asymmetric-operator interaction** — if the totality migration affects symmetric operators (`>`, `<`, etc.) that DB-11 explicitly strips refinements from, surface — the design doc treats those as separate; this PR shouldn't broaden.
 - **DB-8 drifts** — STOP immediately.
 

docs/briefs/r2-modeling-tokenizer-charclass-phase2-worker.md

@@ -14,7 +14,7 @@
 - **[`src/v3/std/tokenize.dag`](../../src/v3/std/tokenize.dag)** — tokenizer authority; phase-1 lands the structural shape, phase-2 retypes consumers to `Char` / `List<Char>` / `CharClass`.
 - **[#662](https://github.com/gunb-ai/gunbc/pull/662)** — "tokenize: reframe character-level scaffold as consumption gap" (merged); confirm phase-1 baseline.
 - **[`docs/thesis/the-substrate-two-coordinated-shapes.md`](../thesis/the-substrate-two-coordinated-shapes.md)** — connective vocabulary; `Cardinality` / `Disj` semantics for charclass sum-types.
-- **[`src/v3/std/unicode.dag`](../../src/v3/std/unicode.dag)** (if exists) — unicode authority; charclass dependency.
+- **[`dsl/std/unicode.dag`](../../dsl/std/unicode.dag)** — unicode authority; charclass dependency.
 
 ## Frame
 

docs/briefs/r2-substrate-nominal-opaque-for-secret-subset.md

@@ -12,7 +12,9 @@
 
 ## Read first
 
-- **[`THESIS.md`](../../THESIS.md)** §"Enumerable impossible-bug classes" — `Secret<T>` is one of the R2+ Tier 1 thesis claims; structural opacity is the impossible-bug-by-construction guarantee.
+- **[`docs/r2-structure.md`](../r2-structure.md)** §Goal 2 (lines 36, 42) + §Lane structure (`Secret<T>` graduation) — locked R2 authority for the `Secret<T>` nominal-opaque graduation as a Modeling-faithfulness Tier-1 R2 commitment.
+- **[`ROADMAP.md:424`](../../ROADMAP.md)** post-merge-debt row — `Secret<T>` nominal-wrapper graduation: `dsl/std/types.dag:237` declares `Secret = String` (alias); the substrate distinction between nominal-opaque and alias is the structural delta. **Cited by R2 Goal 2.**
+- **[`docs/thesis/compositional-modeling.md` Part 4](../thesis/compositional-modeling.md)** — original thesis-doc surface; structural opacity argument. (THESIS.md §"Enumerable impossible-bug classes" lists `[R2+]` nested-optional / unenumerated-effects / unhandled-diagnostic-paths; `Secret<T>` is **not** in that list — claim authority lives in r2-structure.md + ROADMAP, not THESIS.md, until/unless THESIS.md adds the entry.)
 - **[`dsl/std/types.dag`](../../dsl/std/types.dag)** — current type system; how named types are namespaces (`feedback_naming_is_aliasing`); how `inhabits` edges work for algebra attachment.
 - **[`src/v3/std/substrate.dag`](../../src/v3/std/substrate.dag)** — live substrate authority for `TypeConnective` + Declaration shape.
 - **[`src/v3/spec/v3_l1.dag`](../../src/v3/spec/v3_l1.dag)** — sentinel meta-types; precedent for cross-cutting substrate fields like `DeclarationRef`.