docs(briefs): R3 bug-fix worker briefs — 4 stranded tasks (gpt-5-5-pro reflective findings)

docs/briefs/r3-bug-callgraph-forward-only-authority-worker.md

@@ -0,0 +1,94 @@
+# R3 Bug-Fix Worker Brief — CallGraph forward-only authority
+
+**Owner**: Substrate Mgr (warm-wolf-698 / gunbc#2068) lane scope; worker dispatch via Substrate Mgr standing authority.
+**Authority parent**: gpt-5-5-pro reflective analysis on `main@cf1d523` Finding 3; PM dispatch at gunbc#846 #issuecomment-4413207527.
+**Priority**: MEDIUM — illegal-state-representable; clean refactor.
+
+---
+
+## §0. Problem statement
+
+`CallGraph` at `dsl/std/graph.dag:15-26` stores both forward AND reverse adjacency as parallel authorities:
+
+```
+type CallGraph {
+  forward: Map<String, List<String>>
+  reverse: Map<String, List<String>>
+}
+```
+
+`build_call_graph_from_proof_edges` (`dsl/std/graph.dag:57-75`) derives both from the same `ProofEdge` list in one pass. `graph_has_multi_node_scc` (`dsl/std/graph.dag:121-136`) reads `graph.forward` in pass 1 and `graph.reverse` in pass 2.
+
+The builder keeps them aligned; **the type itself admits incoherent values**. A user or later `.dag` stage can construct `CallGraph { forward: A, reverse: B }` where `B` is not the reverse of `A`. INVARIANTS P2 single-authority violation inside the data model.
+
+## §1. Required outcome
+
+Store edges as single authority; reverse derived as needed.
+
+## §2. Fix options
+
+PM recommends **Option A** (edges-as-authority) — cleanest dissolution; `forward` and `reverse` become derived views.
+
+### Option A — store edges only (preferred)
+
+```
+type CallGraph {
+  edges: List<ProofEdge>
+}
+
+fn forward_adjacency(graph: CallGraph) -> Map<String, List<String>> = ...
+fn reverse_adjacency(graph: CallGraph) -> Map<String, List<String>> = ...
+```
+
+Consumers call `forward_adjacency(graph)` / `reverse_adjacency(graph)` instead of accessing field. Builder constructs `CallGraph { edges }`; reverse computation moves to derivation function.
+
+**Performance note**: if `graph_has_multi_node_scc` (or other consumers) need both adjacencies in tight loops, the derivation can return both at once via `fn build_adjacency_views(graph: CallGraph) -> { forward, reverse }`, OR consumers cache locally. Not a substrate-shape concern.
+
+### Option B — forward-only with derived reverse
+
+```
+type CallGraph {
+  forward: Map<String, List<String>>
+}
+
+fn reverse_adjacency(graph: CallGraph) -> Map<String, List<String>> = ...
+```
+
+Smaller diff but less clean — `forward` is still potentially constructible inconsistently with the original edges (e.g., direct map construction omitting an edge). Option A pushes the authority all the way back to the edge list.
+
+## §3. Files (expected scope)
+
+**Option A**:
+- `dsl/std/graph.dag` (CallGraph shape + build_call_graph_from_proof_edges + graph_has_multi_node_scc + new derivation functions)
+- Any callers of `CallGraph.forward` / `CallGraph.reverse` field accesses (grep audit)
+- Cementing test pinning that `forward_adjacency(build_call_graph_from_proof_edges(edges))` recovers expected adjacency
+- If parallel v3 mirror exists (`src/v3/std/graph.dag`?), reconcile
+
+**Option B**: similar but smaller — keep forward field; only delete reverse.
+
+## §4. Cross-cutting constraints
+
+- **No new hand-Rust tests** — `.dag` TestClaim form preferred per locked design `docs/design-tests-as-data-completeness.md` §C5 / §C1.
+- **STOP-and-PING via PM inbox (#846)** if grep reveals consumers that depend on `CallGraph.reverse` for performance-critical paths and derivation introduces unacceptable cost. Likely not — but if so, the fix is to provide both views via single derivation function, not to keep the dual-authority field.
+- **Substrate authority canonical**: `dsl/std/graph.dag` is canonical; if v3 mirror exists, reconcile.
+
+## §5. Receipt
+
+When work lands:
+- `CallGraph` cannot represent inconsistent forward/reverse state (illegal state unrepresentable structurally)
+- Cementing test pinning that derived adjacencies are coherent with edge list
+- INVARIANTS P2 strengthened: dual-authority inside data model dissolved
+- Substrate + Rust mirror synchronized (if applicable)
+- SG-0 census: any new test entries marked with dissolution-trigger comment
+
+## §6. Dispatch trigger
+
+PM-authored brief; awaiting worker dispatch. Illegal-state representability remains live on main until fixed.
+
+## §7. Risk note
+
+Smaller scope than the other 3 bug-fix tasks (Tasks 1-3). Substrate-shape change but contained — `CallGraph` is internal substrate, not user-facing. Should be a single small PR.
+
+---
+
+**End of brief.**

docs/briefs/r3-bug-fieldproject-dual-authority-dissolution-worker.md

@@ -0,0 +1,105 @@
+# R3 Bug-Fix Worker Brief — FieldProject dual-authority dissolution
+
+**Owner**: Substrate Mgr (warm-wolf-698 / gunbc#2068) lane scope; worker dispatch via Substrate Mgr standing authority.
+**Authority parent**: gpt-5-5-pro reflective analysis on `main@b09e0c8` Finding 2; PM dispatch at gunbc#846 #issuecomment-4413207527.
+**Priority**: HIGH — concrete soundness bug; illegal-state-representable.
+
+---
+
+## §0. Problem statement
+
+`TransformTarget::FieldProject` carries both a string label and an optional typed child declaration:
+
+```rust
+// src/v3/compiler/src/dag.rs:1890-1892
+FieldProject {
+    field_label: String,
+    field_child: Option<DeclarationId>,
+},
+```
+
+Substrate mirror at `src/v3/std/substrate.dag:311-316` repeats the dual shape.
+
+The intended semantics (per code comments at `src/v3/compiler/src/dag.rs:1880-1888`): inference walks the input through `Instantiation`/`ResolvedIdentifier` edges, looks up `field_label` on the reached `Conj`, and populates `field_child` post-resolution.
+
+**Concrete soundness bug**: actual code paths disagree on which field is authoritative:
+
+- **Inference** (`src/v3/compiler/src/infer.rs:4198-4204`): trusts `field_child` directly when present
+- **Builder** (`src/v3/compiler/src/dag/builder.rs:300-310`): only checks `field_child` exists, not that it matches `field_label` on the input's record type
+- **Emission** (`src/v3/compiler/src/emit/rust_target.rs:3571-3594`): renders from the string label
+
+So an inconsistent `FieldProject { field_label: "x", field_child: y_decl }` lets:
+- inference resolve output as `y_decl` (uses `field_child`)
+- emission project `"x"` (uses `field_label`)
+
+Illegal state representable; consumers can disagree on what the projection means.
+
+## §1. Required outcome
+
+Split lifecycle OR collapse authority such that label and field_child cannot disagree.
+
+## §2. Fix options
+
+PM recommends **Option A** (split lifecycle) — explicit pre/post-resolution states; alignment enforced structurally.
+
+### Option A — split lifecycle (preferred)
+
+Replace single variant with:
+
+```rust
+FieldProject = UnresolvedFieldProject { field_label: String }
+             | ResolvedFieldProject { field_ref: FieldDeclRef }
+```
+
+Lifecycle:
+- Builder constructs `UnresolvedFieldProject { field_label }`
+- Inference transitions `Unresolved → Resolved` via lookup against parent Conj; constructs `ResolvedFieldProject { field_ref }` where `field_ref` is a typed witness
+- `transform_output_shape` requires `Resolved` (panics on `Unresolved` — invariant: post-infer, all FieldProjects are Resolved)
+- Emission consumes `field_ref` directly; label retained only on `Unresolved` for diagnostic provenance OR extracted via `field_ref.label()` accessor
+
+If `field_ref` needs to expose label (for diagnostic spans), make label a derived view, not a stored authority.
+
+### Option B — collapse to single authority
+
+Keep single `FieldProject` variant; drop `field_label` entirely after lookup. `field_child` becomes the single authority. Diagnostic provenance preserved via `SourceSpan`.
+
+Smaller PR but loses diagnostic-quality info (debug error messages can't say "field 'x' not found" without re-walking declaration).
+
+## §3. Files (expected scope)
+
+**Option A**:
+- `src/v3/std/substrate.dag` (TransformTarget shape — substrate authority)
+- `src/v3/compiler/src/dag.rs` (Rust mirror at line 1890-1892)
+- `src/v3/compiler/src/dag/builder.rs` (builder at line 300-310 + 762-766; constructs Unresolved)
+- `src/v3/compiler/src/infer.rs` (inference at line 4198-4208; transitions Unresolved → Resolved)
+- `src/v3/compiler/src/emit/rust_target.rs` (emission at line 3571-3594; consumes Resolved.field_ref)
+- Cementing test pinning shape (`.dag` TestClaim form preferred)
+
+**Option B**:
+- Same files as Option A but smaller diffs (variant payload change only, not split)
+
+## §4. Cross-cutting constraints
+
+- **No new hand-Rust tests** — `.dag` TestClaim form preferred per locked design `docs/design-tests-as-data-completeness.md` §C5 / §C1.
+- **STOP-and-PING via PM inbox (#846)** if substrate-shape change introduces variants that parser cannot lower (data-body limitations).
+- **Substrate authority canonical**: `src/v3/std/substrate.dag` is canonical; Rust mirror at `dag.rs` reflects.
+
+## §5. Receipt
+
+When work lands:
+- `FieldProject` cannot represent inconsistent label/child state (illegal state unrepresentable structurally)
+- Cementing test pinning that inference + emission agree on field identity for any constructed FieldProject
+- Substrate + Rust mirror synchronized
+- SG-0 census: any new test entries marked with dissolution-trigger comment
+
+## §6. Dispatch trigger
+
+PM-authored brief; awaiting worker dispatch. Bug remains live on main until fixed.
+
+## §7. Risk note
+
+This is a **substrate-shape change** — touches `substrate.dag` + Rust mirror + 3 consumers. Coordinate with Substrate Mgr; brief authoring + dispatch likely needs cross-Mgr sign-off (Substrate authoring + Verification consumer-wiring) for safety. Single PR feasible if scope contained.
+
+---
+
+**End of brief.**

docs/briefs/r3-bug-resolve-producer-opt-typed-return-worker.md

@@ -0,0 +1,117 @@
+# R3 Bug-Fix Worker Brief — `resolve_producer_opt` typed return (P3 fail-closed)
+
+**Owner**: Substrate Mgr (warm-wolf-698 / gunbc#2068) lane scope; worker dispatch via Substrate Mgr standing authority.
+**Authority parent**: gpt-5-5-pro reflective analysis on `main@1211e453` Finding 2; PM dispatch at gunbc#846 #issuecomment-4413207527.
+**Priority**: HIGH — concrete P3 fail-closed violation.
+
+---
+
+## §0. Problem statement
+
+`Dag::resolve_producer_opt` at `src/v3/compiler/src/dag.rs:3766-3799` returns `Option<&Behavior>`. The current implementation collapses **four distinct states** into `None`:
+
+```rust
+let port = self.port_opt(&current_port)?;       // ← MissingPort → None
+let producer_id = port.produced_by?;            // ← legitimate NoProducer → None
+let behavior = self.node_opt(&producer_id)?;    // ← MissingNode → None
+// ...
+// Cycle in the Bind chain — malformed substrate. Surface as miss
+None                                            // ← BindCycle → None
+```
+
+Then `lens_apply.rs:51-56` treats miss as eligibility:
+
+```rust
+let Some(producer) = dag.resolve_producer_opt(&port) else {
+    return true;  // ← treats malformed-substrate states as "yes, eligible"
+};
+```
+
+**Concrete fail-closed violation** (INVARIANTS P3): a malformed substrate fact is converted into plausible "absence" + downstream consumer proceeds with wrong eligibility result.
+
+The four states are NOT semantically equivalent:
+- **legitimate NoProducer** (parameter port has no producer): consumer should treat as eligible
+- **MissingPort** (PortId doesn't resolve in DAG): consumer should fail-closed (broken substrate)
+- **MissingNode** (`produced_by` references missing node): consumer should fail-closed (broken substrate)
+- **BindCycle** (cyclic Bind chain): consumer should fail-closed (broken substrate)
+
+Today they all → "eligible".
+
+## §1. Required outcome
+
+Typed return discriminates legitimate-absence from malformed states; consumers handle each explicitly.
+
+## §2. Fix steps
+
+1. Replace return type with typed sum:
+
+```rust
+enum ProducerLookup<'a> {
+    /// Legitimate: parameter port has no producer. Consumer treats as appropriate per context.
+    NoProducer,
+
+    /// Found a non-Bind producer in the chain.
+    Found(&'a Behavior),
+
+    /// Substrate-malformed: PortId doesn't resolve in DAG.
+    MissingPort { port: PortId },
+
+    /// Substrate-malformed: `produced_by` references a NodeId not in DAG.
+    MissingNode { producer: NodeId },
+
+    /// Substrate-malformed: cyclic Bind chain detected during walk.
+    BindCycle { detected_at: NodeId },
+}
+
+pub fn resolve_producer_lookup(&self, port: &PortId) -> ProducerLookup<'_>
+```
+
+2. **Update `lens_apply.rs:51-56`** consumer to discriminate:
+   - `NoProducer` → eligible (current behavior preserved)
+   - `Found(b)` → check eligibility on b (current behavior preserved)
+   - `MissingPort` / `MissingNode` / `BindCycle` → **fail-closed**: return diagnostic to caller; do NOT default to "eligible"
+
+3. **Audit other callers** — grep for `resolve_producer_opt` and `produced_by` usage. Each call site must handle the malformed states explicitly. Possible call sites (verify):
+   - `src/v3/compiler/src/lens_apply.rs`
+   - `src/v3/compiler/src/lower.rs`
+   - `src/v3/compiler/src/infer.rs`
+   - `src/v3/compiler/src/dag/builder.rs`
+
+4. **Cementing test** (`.dag` TestClaim form preferred): pin discriminator behavior — fixture with deliberately malformed substrate (cyclic Bind, missing node, missing port) → consumer fails-closed, not eligible.
+
+5. Optional: add `compat::resolve_producer_opt` thin wrapper that returns `Option<&Behavior>` (for any callers that legitimately need just legitimate-NoProducer-or-Found semantics), with explicit comment "this collapses malformed states; only use when malformed-substrate equivalence to absence is the intended semantics."
+
+## §3. Files (expected scope)
+
+- `src/v3/compiler/src/dag.rs` (resolve_producer_opt → resolve_producer_lookup signature + return type)
+- `src/v3/compiler/src/lens_apply.rs` (consumer at line 51-56)
+- All other callers of `resolve_producer_opt` (grep audit; ~5-10 sites estimated)
+- `src/v3/std/substrate.dag` (if `ProducerLookup` mirror needed for `.dag` consumers)
+- Cementing test (`.dag` TestClaim form preferred)
+
+## §4. Cross-cutting constraints
+
+- **No new hand-Rust tests** — `.dag` TestClaim form preferred. Cementing test could fixture with a substrate-fixture demonstrating each malformed state + assert lens_apply diagnostic on each.
+- **STOP-and-PING via PM inbox (#846)** if grep reveals callers that genuinely need the old absence-collapse semantics for legitimate reasons (would need shape decision; possibly the optional `compat::` wrapper above).
+- **Fail-closed discipline** (INVARIANTS P3): malformed substrate must not convert to plausible absence.
+
+## §5. Receipt
+
+When work lands:
+- `resolve_producer_opt` returns typed `ProducerLookup` discriminating legitimate-absence from malformed states
+- All call sites handle each variant explicitly (no `_ => default-to-eligible` shortcuts)
+- Cementing test pins fail-closed behavior on each malformed state
+- INVARIANTS P3 strengthened: this fail-open API surface is closed
+- SG-0 census: any new test entries marked with dissolution-trigger comment
+
+## §6. Dispatch trigger
+
+PM-authored brief; awaiting worker dispatch. Fail-closed violation remains live on main until fixed.
+
+## §7. Risk note
+
+The grep audit may reveal call sites that have IMPLICITLY relied on the absence-collapse semantics for years (silent-acceptance code). Fix-forward may surface latent bugs in those call sites where they "worked" because malformed substrate states are rare in practice. Surface unexpected findings via STOP-and-PING — don't paper over with `_ => default` matches.
+
+---
+
+**End of brief.**