β

ROADMAP.md

@@ -516,13 +516,19 @@ Closed (DB-16, PR #522):
 
 Follow-up (not blocking): emission for narrowed ports currently errors if `emit_rust` is invoked on a DAG whose narrow ports lack a producer. Acceptable today because Lane 1e's single-emitter consolidation hasn't landed and the 3a.3 acceptance is compile-only; wire a Bind-alias or emission-local name shim alongside Lane 1e when it lands. DB-16's substituted-refined carriers inherit the same narrowed-port shim requirement.
 
-### Lane 2 Stage 2c — test infrastructure
+### Lane 2 Stage 2b — workflow idempotency lens
+
+**DB-18 landed — effects algebra + native Rust analysis.** This delivers the **`.dag` + Rust carrier story** and `v3_compiler::analyze_workflow`; it does **not** complete thesis-grade **declared-substrate self-inspection** for workflow facts (that requires reflecting `lane2_workflow` — see **Reflection boundary** below). Do not treat Stage 2b as “fully self-hosted through `.dag` lenses” until that reflection ships. `src/v3/std/effects.dag`: `WorkflowEffect` (linear / branch / loop / parallel), `BranchPredicateRef` + `BranchArm { condition: BranchPredicateRef, ... }`, `WorkflowIdempotencyReport` (`WorkflowCompositionVerdict(CompositionVerdict) | IdempotencyUnsupported(...)`), helpers `nel_to_operation_effect_list`, `report_unsupported_workflow_variant`. `src/v3/compiler/src/dag.rs`: Rust mirrors + `Dag::branch_arm_of` (packages a Bool-resolved port as `BranchPredicateRef` — same Track 9 handle pattern as `param_of` / `as_transform_ref`, not a raw `PortId` on the arm). Consumer: `v3_compiler::analyze_workflow(d, workflow_root: NodeId)` reads workflow facts only from native `Value`/`Bind` node fields (`lane2_workflow` — no parallel side table), set by lowering or staging `Dag::try_register_lane2_workflow_effect` until service lowering attaches the same fields — [`workflow_idempotency.rs`](src/v3/compiler/src/workflow_idempotency.rs) + thin [`lens_idempotency.rs`](src/v3/compiler/src/lens_idempotency.rs); [`src/v3/lenses/idempotency.dag`](src/v3/lenses/idempotency.dag) holds the API + staging note (user-module `match` on `WorkflowEffect` not yet emit-table — full dispatcher is Rust until the class-5 gap closes). Tests: [`lane2_stage_2b_db18_test.rs`](src/v3/compiler/tests/lane2_stage_2b_db18_test.rs). Framing: [lane2-compile-time-proofs.md](docs/lane2-compile-time-proofs.md) Stage 2b.
+
+**Reflection boundary (named staging).** `lane2_workflow` exists only on **compiler-native** `ValueNode` / `BindNode`; it is **not** part of the reflected `Behavior` vocabulary in `substrate.dag` that `.dag` lenses introspect today — so Stage 2b does **not** yet claim full “self-inspection through declared substrate” for that pocket. **Dissolution (tracked):** reflect a workflow-fact carrier through substrate (+ realization wiring) so Rust and `.dag` lenses consume the same inspectable fact; until then `try_register_lane2_workflow_effect` is the explicit test/native hook (documented, not a silent parallel authority).
 
-**Deferral: DB-15 tests-as-declarations extensions (M, blocks Lane 2 Stage 2c).** Design doc (R2 draft): [design-test-infra.md](docs/design-test-infra.md). R2 consumes the compiler-as-dependency-analyzer thesis: tests are declarations (extending the existing `src/v3/std/verification.dag` `TestClaim`/`TestSuite` authority), resources are references to `dsl/std/resources.dag`, sharing/caching/incremental execution fall out of the compiler's existing dependency walk. No new caches or runner mechanisms — DB-15 names HOW things depend, then the walk does the rest.
+- **[PR #534] Lane 2 Stage 2b — reflect workflow facts in substrate.** Staging debt: native `lane2_workflow` on `Value`/`Bind` plus `Dag::try_register_lane2_workflow_effect` remain authoritative **only until** the same fact exists on reflected `Behavior` and `src/v3/lenses/idempotency.dag` can stop delegating to Rust. **Clears when:** follow-up PR lands substrate (+ realization) support and removes or demotes the native-only pocket as primary authority. Cross-refs: bullets above; [lane2-compile-time-proofs.md](docs/lane2-compile-time-proofs.md) Stage 2b.
+
+### Lane 2 Stage 2c — test infrastructure
 
-Implementation scope (M, once design locks): extend `TestClaim` with `requires: List<ResourceReference>` and two new `TestPredicate` variants (`BehavioralObservation`, `MockBackedInvariant`); apply tautology-avoidance rule structurally; one-file migration proof. Yellow-flag threshold: design must lock before Lane 2 Stage 2c kickoff.
+**DB-15 (R2) — ✅ implementation landed (test-runner wiring remains follow-up).** Design doc: [design-test-infra.md](docs/design-test-infra.md). `src/v3/std/verification.dag`: `TestClaim.requires: List<ResourceReference>` (sole obligation surface for mock transports — `MockBackedInvariant` does not duplicate `ResourceReference`); `TestPredicate` extends with `BehavioralObservation` / `MockBackedInvariant` (tautology-avoiding predicate shapes per R2); `TestObligation` + `materialize_test_obligations` (dependency-walk projection over declared claims — not workflow-structure). **`v3.std.resources`** (`src/v3/std/resources.dag`): minimal `ResourceHandle` / `ResourceReference` carriers — `ResourceHandle` uses the same field labels as `dsl/std/resources.dag` (`type` / `resource_id` / `key` / `cap: Secret`); module name avoids clashing with `dsl/std/resources.dag`'s `std.resources` during bootstrap; full `resource { }` port remains a dissolution item toward single authority with dsl.
 
-**Prerequisite deferral: `dsl/std/resources.dag` → v3 reconciliation (S).** Zero references to `Resource`/`acquire`/`release` under `src/v3/` today. DB-15's `requires: List<ResourceReference>` is authored but unconsumed until this lands. Options: port declaration into `src/v3/std/resources.dag`, OR make `dsl/std/resources.dag` bootstrap-consumable by v3. Preferring the latter for single-authority. Separable from DB-15 implementation — can land independently. This is also a dissolution-of-dual-representation item; consider parking it in §Scheduled deletions if dsl/v3 duplication is the framing, or keep as a prerequisite deferral here. Preferring here for now since it's narrowly scoped.
+**Remaining Stage 2c consumer:** generated test execution / runner integration (out of scope for the DB-15 schema PR).
 
 ### Lane 2 Stage 2a / Track 17a boundary
 

docs/design-dimension-abstraction.md

@@ -128,16 +128,11 @@ fn witness_idempotency(d: Dag, behavior: Behavior) -> Witness<ComposedEffect> {
   }
 }
 
-// Lane 2b's analyze_workflow becomes:
-fn analyze_workflow(d: Dag, workflow: NodeId) -> WorkflowIdempotencyReport {
-  let report = analyze(d, workflow, idempotency_dimension)
-  WorkflowIdempotencyReport {
-    idempotent: is_empty(report.violations),
-    breaking_op: first_breaking_op(report.witnesses),
-    evidence_chain: report.witnesses,
-    diagnostic: first(report.violations)
-  }
-}
+// Lane 2b — shipped Rust API: analyze_workflow(d, workflow_root: NodeId);
+// WorkflowIdempotencyReport is the sum type in std.effects (not a flat record).
+// Analysis reads WorkflowEffect facts from substrate Value/Bind fields (lane2_workflow),
+// not a parallel map; idempotency.dag remains a staging stub for self-hosted match.
+// Dimension<> wiring is future work. See lane2-compile-time-proofs.md Stage 2b.
 ```
 
 ### Side effects as Dimension instance (Lane 4 Stage 4b)

docs/design-test-infra.md

@@ -4,7 +4,7 @@
 
 **Design blocker:** DB-15 (test infrastructure that consumes the compiler's dependency-analysis machinery)
 **Consumer:** Lane 2 Stage 2c (test obligation materialization) — forcing function
-**Status:** Revision 2 (discussion draft). R1 was rejected — see Correction history below.
+**Status:** R2 **locked for schema** — `src/v3/std/verification.dag` implements `TestClaim.requires`, `BehavioralObservation`, `MockBackedInvariant`, `TestObligation`, and `materialize_test_obligations`; `src/v3/std/resources.dag` supplies `ResourceReference` / `ResourceHandle` (including `cap: Secret` aligned with `dsl/std/resources.dag`). Test-runner wiring and doc-only checkboxes below remain follow-ups. R1 was rejected — see Correction history below.
 **Existing v3 authority being extended:** [`src/v3/std/verification.dag`](../src/v3/std/verification.dag) — quoted inline in §"What DB-15 extends" below.
 
 **Two verification.dag files exist in the repo** — this is important:
@@ -93,7 +93,7 @@ R2 keeps the above shapes and adds two things:
 1. **New `TestPredicate` variants for behavioral / mock-backed claims** — the case where a property holds by observation, not by lens re-reading. Matches Lane 2 Stage 2c's mandate.
 2. **A `requires: List<ResourceReference>` field (or equivalent)** — lets the claim declare what must be acquired to run it. This is NOT a new sharing mechanism; it's a declaration that the compiler's existing dependency walk reads to place acquires.
 
-Shape (preliminary — open question #1 below on exact syntax):
+Shape (**implemented** in `src/v3/std/verification.dag`):
 
 ```dag
 // src/v3/std/verification.dag — extensions, not replacement
@@ -102,7 +102,7 @@ type TestClaim {
   source: String
   file_name: String
   predicate: TestPredicate
-  requires: List<ResourceReference>   // NEW — declared dependencies
+  requires: List<ResourceReference>   // declared dependencies (per-claim)
 }
 
 type TestPredicate
@@ -116,11 +116,12 @@ type TestPredicate
     }
   | MockBackedInvariant {             // NEW — for Lane 2 Stage 2c
       subject: DeclarationRef
-      mock_transport: ResourceReference
       invariant: DeclarationRef
     }
 ```
 
+For mock-backed tests, declare mock `ResourceReference` targets only on `TestClaim.requires` (obligation authority) — not again inside `MockBackedInvariant`.
+
 `BehavioralObservation` encodes "the test runs the subject on a sample and compares to an independently-declared expected output." That's not rerunning a lens; it's running the subject and checking a separately-declared fact.
 
 `MockBackedInvariant` encodes "the test runs the subject against a mocked resource (e.g., a mock HTTP backend) and checks that a separately-declared invariant holds." That's the runtime-mock Lane 2 Stage 2c requires.
@@ -145,14 +146,7 @@ This is the difference between `CostBounded { bind_name, comparator, bound }` (e
 
 ## Prerequisite: `dsl/std/resources.dag` → v3 reconciliation
 
-**Blocker for R2's resource references:** v3 does not yet consume `dsl/std/resources.dag`. Grep confirms zero references to `Resource`/`acquire`/`release` under `src/v3/`.
-
-This is a standalone dissolution-of-dual-representation item and belongs in ROADMAP §"Scheduled deletions" as its own row. Options:
-
-1. **Port the declaration into `src/v3/std/resources.dag`** (direct v3 port; dsl/std/resources.dag remains v2 reference).
-2. **Make `dsl/std/resources.dag` consumable by v3 bootstrap** (single authority across v2 and v3).
-
-Preferring option (2) for the single-authority reason. Either way, the work is **separable from DB-15**. DB-15's `requires: List<ResourceReference>` field is authored but unconsumed until resources.dag lands in v3 — and the `TestClaim` scaffold for `requires` should carry a 🟡 dissolution marker with a named trigger (the resources-in-v3 port PR).
+**Update:** `src/v3/std/resources.dag` (module `v3.std.resources`) provides `ResourceHandle` (including `cap: Secret` per `dsl/std/resources.dag`) and `ResourceReference { target: DeclarationRef }` for v3 bootstrap so `TestClaim.requires` has typed carriers. Full `resource { }` syntax, acquire/release insertion, and loading `dsl/std/resources.dag` in the same bootstrap pass as v3-only files remain ROADMAP-tracked dissolution work — see [ROADMAP.md](../ROADMAP.md) Stage 2c / resources.
 
 ## Runtime cost — three sharing classes, all derived from dependency placement
 
@@ -191,34 +185,38 @@ The "more efficient than typical" intuition cashes out from ALL THREE collapses,
 
 ---
 
-## Open questions (for this draft)
+## Open questions — lock state (2026-04)
+
+Questions **1–3** from R2 draft are **resolved** by the shipped `src/v3/std/verification.dag` coproduct and `ResourceReference` shape:
 
-1. **Exact syntax for `requires: List<ResourceReference>` on `TestClaim`.** Structural: should ResourceReference be a typed declaration reference (`DeclarationRef`) or a typed resource type (`ResourceHandle` in resources.dag terminology)? Probably the former — handles are runtime artifacts, not compile-time declarations. Verify at implementation time.
+1. **`requires` syntax.** `TestClaim.requires: List<ResourceReference>` with `ResourceReference { target: DeclarationRef }` — compile-time declaration edges, not raw `ResourceHandle` literals in claims (handles remain the runtime minted carrier in `dsl/std/resources.dag` / `v3.std.resources`).
 
-2. **Which existing `TestPredicate` variants need the `requires` declaration, and which are self-contained?** `PortStateExpectation` and `CostBounded` are compile-time assertions with no runtime resource needs. `BehavioralObservation` needs a test-runner resource. `MockBackedInvariant` needs both a test-runner AND a mock-transport resource. Open: is `requires` per-claim or per-predicate-variant?
+2. **Per-claim vs per-predicate.** `requires` is **per `TestClaim`** (one list on the claim). Predicates that need runtime backing declare resources at the claim level; compile-time-only predicates (`PortHasState`, `CostBounded`, etc.) may use empty `requires` where applicable.
 
-3. **Tautology-avoidance enforcement.** The rule "predicate cannot rerun the producing lens" is currently prose. Can it be enforced structurally — e.g., the predicate variants are explicitly behavioral/observational by type, and "rerun lens X" is not even expressible? Needs a pass to confirm no variant sneaks in that permits the pattern.
+3. **Tautology avoidance.** Enforced by **construction**: behavioral/mock variants (`BehavioralObservation`, `MockBackedInvariant`) point at `DeclarationRef` edges for subject / (for mocks: invariant, with mock carriers on `requires` only); there is no `TestPredicate` variant meaning “invoke lens L and compare.” Prose rule matches the expressible surface.
 
-4. **Lane 2 Stage 2c generation surface.** Stage 2c generates `TestClaim` declarations from lens outputs. What's the structural shape of "this lens's output, materialized into a `TestPredicate`"? Likely one generation rule per `(lens, predicate-variant)` pair, declared once per lens. Out of scope for DB-15's design; in scope for Stage 2c's implementation.
+4. **Lane 2 Stage 2c generation surface.** Still open for **implementation** — how each lens materializes into `TestPredicate` (generation rules). Out of scope for this design doc’s schema lock; tracked under Stage 2c / testgen.
 
 ---
 
-## Acceptance (for when this graduates from draft)
+## Acceptance — schema locked; execution follow-ups
+
+**R2 schema** (verification + minimal resources carriers) is **locked** — this section tracks **test-runner / generation** work, not unresolved design questions.
 
-- [ ] Open questions 1–3 locked with explicit answers.
-- [ ] Extensions to `src/v3/std/verification.dag` sketched with exact field shapes (`requires`, new `TestPredicate` variants).
-- [ ] Resources-in-v3 reconciliation scheduled — named PR or ROADMAP row identifying the upstream path.
+- [x] Open questions 1–3 locked with explicit answers (see section above).
+- [x] Extensions to `src/v3/std/verification.dag` with field shapes (`requires`, `BehavioralObservation`, `MockBackedInvariant`, obligations).
+- [x] Minimal resources surface in v3 (`src/v3/std/resources.dag`); full dsl merge / `resource { }` lowering still ROADMAP-tracked.
 - [ ] One existing test file (e.g., `m2_feature_parity_test.rs`'s 3a.2 tests) re-expressed as `TestClaim` declarations, showing the structural form consuming the compiler's dependency walk.
 - [ ] Lane 2 Stage 2c plan updates: generation emits `TestClaim` declarations via the R2 shape, not Rust functions.
-- [ ] Cost invariant phrased as derived from resource placement, not as a standalone claim.
+- [x] Cost / sharing narrative: derived from dependency walk (§Runtime cost); no standalone O(…) claim as primitive.
 
 ---
 
 ## Associations
 
 - **Compiler-as-dependency-analyzer thesis** (tonight's framing) — DB-15 is the testing-scope consequence. Tests are declarations; the dependency walk handles them like anything else.
 - **`src/v3/std/verification.dag`** — the existing authority DB-15 extends. `TestClaim`, `TestPredicate`, `TestSuite` stay as-authored.
-- **`dsl/std/resources.dag`** — the existing acquire/release model DB-15 references via `requires: List<ResourceReference>`. Prerequisite for consumption: reconcile into v3.
+- **`dsl/std/resources.dag`** — acquire/release authority; **`src/v3/std/resources.dag`** supplies bootstrap `ResourceHandle` / `ResourceReference` with **matching `ResourceHandle` field labels** until full `resource { }` / merged bootstrap is ROADMAP-tracked.
 - **Lane 2 Stage 2c** ([lane2-compile-time-proofs.md](./lane2-compile-time-proofs.md)) — forcing function; generates `TestClaim` declarations from lens outputs.
 - **`src/v3/compiler/pipeline.dag`** — analogous pattern for non-test declarations (compiler stages consume the dependency walk); DB-15 applies the same shape to test-scope declarations.
 - **E-9 (INVARIANTS.md)** — sibling invariant. DB-15 doesn't need a new invariant; the rule "tests are declarations that consume the dependency walk" is implied by the thesis. If a future PR wants to bank it load-bearingly, it would be something like E-10 "tests as first-class declarations."