C

.github/workflows/ci.yml

@@ -73,7 +73,9 @@ jobs:
 
   v3:
     runs-on: ubuntu-latest
-    timeout-minutes: 15
+    # Full suite is capped at 750s, plus clippy + lens gates + cold compile — 15m
+    # can cancel the job before the final steps finish.
+    timeout-minutes: 25
     steps:
       - name: Checkout
         uses: actions/checkout@v4
@@ -100,6 +102,12 @@ jobs:
 
       # Layer 1 (coarse CI): wall-clock gates on `cargo test -p v3-compiler`.
       #
+      # Full-suite budget is 750s (upstream). Warm local runs are often ~520–560s for
+      # `cargo test -p v3-compiler`, but cold GitHub runners + cache misses still
+      # need headroom beyond a tight 600s-style cap (Layer 1 ratchet history).
+      # Regressions show up when integration tests redo full `compile_to_dag` per
+      # `#[test]` (see `lane2_stage_2e_parallelism_test`: shared `OnceLock` + clone).
+      #
       # 120s gate: applies to the lane2 Stage 2d symbolic-cost integration
       # binary only — that is the ζ (#537) regression surface (many `#[test]`
       # each doing full compile). A warm full `cargo test -p v3-compiler` is

ROADMAP.md

@@ -592,6 +592,20 @@ Cleared (prior PR #521): `DerivedOpEffect { method, path_template, shape }` coll
 
 **Follow-up — hand-maintained `SymbolicCost` Rust mirror drift ratchet (not blocking, authority unification gates graduation).** PR #537 ChatGPT review (`sha:0f8c215c0`) call-out: the `SymbolicCost` / `SizeVariable` carriers + the composition functions (`sequential`, `iterate`, `max_path`, `normalize`, `dominates`, `reduce_sum`, `reduce_product`, `combine_binary_product`, `drop_dominated_in_sum`) are hand-maintained in `src/v3/compiler/src/dag.rs` because `emit_rust_module`'s `is_bootstrap_file` filter excludes `src/v3/std/` declarations from Rust emission. The scope is bounded (9 fns + 2 carrier types) and the current surface matches `src/v3/std/algebra.dag` modulo the documented composite-dominance gap (Follow-up above). The risk is future consumers attaching to the Rust mirror and not noticing when it drifts from the .dag authority — "declaration is the implementation" gets quietly replaced by "declaration + stronger hand-maintained Rust version" as the operating pattern. **Dissolution trigger:** the same substrate extension that closes the composite-dominance gap — once termination analysis admits cross-type mutual-recursion clusters, the .dag side matches Rust's richness and the hand-maintained mirror becomes `emit_rust_module`-generated like every other substrate type. Until then, a lightweight ratchet (e.g., a test that greps `src/v3/compiler/src/dag.rs` for fn signatures starting with `SymbolicCost::*` / `pub fn sequential|iterate|...` and cross-checks the count against `src/v3/std/algebra.dag` top-level `fn` decls) would catch silent expansion of the Rust surface. **Yellow-flag threshold: when a tenth hand-maintained fn is added to the mirror** — nine current fns is the baseline; a tenth without matching .dag growth is the signal that the scaffold is growing faster than the authority and needs explicit ratchet wiring.
 
+### Lane 2 Stage 2e — parallelism-as-lens
+
+**Umbrella status (single authority):** “Stage 2e” here names **two slices**. **DB-20** (workflow `ParallelEffect` parallel-composition safety) is **shipped** in the bullet below. **Thesis-facing** graph parallelism / commutative reduction / dependency-graph acceptance is **not** shipped; it stays **open** and is the sole subject of the **deferral** bullet after DB-20. Do not read the subsection title or the DB-20 bullet as marking all of Stage 2e complete.
+
+**DB-20 — shipped (workflow `ParallelEffect` parallel composition safety only).** Closes [design-db18-workflow-effect-carrier.md](docs/design-db18-workflow-effect-carrier.md) §Open question 1: commutativity is **derived** from per-`OperationEffect` algebra (no additive `ParallelEffect` substrate field). Report carrier `WorkflowParallelismReport` (`ParallelCompositionVerdict(CompositionVerdict) | ParallelismUnsupported(...)`) in `src/v3/std/effects.dag`; Rust analysis `v3_compiler::analyze_parallelism` in `src/v3/compiler/src/workflow_parallelism.rs` (exported via `lens_parallelism`). **v1 scope:** `ParallelEffect` whose branches are each `LinearEffect`; nested non-linear branches return explicit `ParallelismUnsupported`. Lens stub: `src/v3/lenses/parallelism.dag` (same reflection boundary as `idempotency.dag`). Design: [design-db20-lane2-stage2e-parallelism-lens.md](docs/design-db20-lane2-stage2e-parallelism-lens.md). Fixtures: `src/v3/compiler/tests/lane2_stage_2e_parallelism_test.rs` (commutative reads; Upsert×Upsert cross-branch fail-closed; distinct path-param names fail-closed; read vs upsert non-commute; append → `BrokenBy`; `NonSingletonList` singleton rejection; non-`ParallelEffect` root).
+
+**Deferral — Lane 2 Stage 2e thesis slice: graph parallelism / commutative reduction (not DB-20).** DB-20 intentionally narrowed **this roadmap’s** Stage 2e **workflow** work to [`ParallelEffect`](docs/design-db20-lane2-stage2e-parallelism-lens.md) parallel-composition safety. The **pre-DB-20** Stage 2e surface — structural dependency-graph parallelism (`thesis_parallelism_test.rs` / `has_transitive_dependency`), commutative-monoid fold reducibility (`parallel_fold_on_commutative_monoid_is_reducible`), map/fold promotion, `ParallelizationOpportunity`-style lens **data** — was **not** deleted; it is **owned here** until shipped. Authority: acceptance bullets and follow-up prose in [lane2-compile-time-proofs.md](docs/lane2-compile-time-proofs.md) §Stage 2e (thesis slice) and §Cross-cutting acceptance. **Dissolution trigger:** lens + fixtures land; checklist rows in lane2-compile-time-proofs can be checked off. **Relationship to DB-20:** orthogonal — DB-20 closes commutativity over **declared** parallel workflow branches; this deferral closes **graph-shaped** parallelism in lowered user code. Size: S–M depending on algebra surface.
+
+**DB number reservation:** **`DB-19`** has no `docs/design-db19-*.md` in-tree yet — hold the number for the next effects/lane-2 consumer that needs a DB doc so allocation stays collision-free alongside DB-18 (carrier) and DB-20 (parallelism lens).
+
+**Follow-up — Lane B reflection (`lane2_workflow` on reflected `Behavior`, e.g. PR #545):** when that debt clears, `src/v3/lenses/parallelism.dag` can graduate from stub to real `.dag` consumer (same dissolution as `idempotency.dag`); `workflow_parallelism.rs` stays the Rust authority until emit+match can walk user sums on the reflected surface.
+
+**Follow-up — cross-lens workflow-analysis unsupported carrier (M–L, paydown lane; not blocking DB-20 / #543 merge).** Stage 2b still encodes “unsupported workflow” cases in `IdempotencyUnsupportedDetail` (including a **string** `variant_name` alongside `reason`). Stage 2e adds **`ParallelismUnsupportedDetail { kind: ParallelismUnsupportedKind, downstream_stage, reason }`** — typed `kind` for parallelism, but **two** lens-local unsupported stories remain side-by-side. The recurring risk (ChatGPT + meta-review on #543, 2026-04-19) is **cross-layer convention** if more workflow lenses or emit consumers must **dispatch** on unsupported causes structurally, not only read prose. **Dissolution trigger:** a **third** workflow-analysis lens lands, or the first consumer needs structural discrimination across Stage 2b vs Stage 2e unsupported paths. **Target shape (pick one in the paydown PR):** introduce a shared `WorkflowAnalysisUnsupportedDetail` (name TBD) in `std.effects` and migrate both reports, **or** graduate `IdempotencyUnsupportedDetail` with per-cause variants and align naming — goal is to remove “overload `variant_name` / duplicate conventions” as the long-term interface. **Explicitly deferred from #543** so DB-20 ships without conflating Stage 2e delivery with cross-lens carrier surgery.
+
 
 ### Lane 1 Stage 1b
 

docs/design-db20-lane2-stage2e-parallelism-lens.md

@@ -0,0 +1,89 @@
+> Part of: [lane2-compile-time-proofs.md](./lane2-compile-time-proofs.md) (Lane 2) | Closes: [design-db18-workflow-effect-carrier.md](./design-db18-workflow-effect-carrier.md) §Open question 1 | Companion: [design-composed-effect-reshape.md](./design-composed-effect-reshape.md) (`CompositionVerdict` authority)
+
+# Design DB-20 — Lane 2 Stage 2e: parallelism-as-lens (parallel composition safety)
+
+**Status:** Implemented — `analyze_parallelism` in `src/v3/compiler/src/workflow_parallelism.rs`, report carrier in `src/v3/std/effects.dag`, lens stub `src/v3/lenses/parallelism.dag`.
+**Scope boundary:** DB-20 covers **workflow** `ParallelEffect` + op-level commutativity only. Thesis Stage 2e items (dependency-graph parallelism, commutative fold reducibility) are **not** orphaned: see [ROADMAP.md](../ROADMAP.md) §Lane 2 Stage 2e — **Deferral: thesis graph-parallelism slice**, and [lane2-compile-time-proofs.md](./lane2-compile-time-proofs.md) §Cross-cutting acceptance.
+**Consumers:** CI fixtures (`lane2_stage_2e_parallelism_test.rs`); future `.dag` lens once `match` on user sums + `lane2_workflow` reflection land (same boundary as Stage 2b).
+
+---
+
+## Summary
+
+DB-18 locks `WorkflowEffect::ParallelEffect { branches: NonSingletonList<WorkflowEffect> }` as the concurrent-product (⊗) introduction form. Stage 2e answers DB-18 §Open question 1: **whether safe parallel scheduling requires a stored commutativity witness on the carrier** versus **derivation from existing operation-level algebra**.
+
+**Decision (path (b), preferred by substrate Q3):** do **not** add `commutativity: …` to `ParallelEffect`. Pairwise commutativity for concurrent branches is **derived** from `OperationEffect` / `EffectShape` / `KeySource` data already carried on each operation. The lens is the sole place that combines those facts into a judgment; nothing new is duplicated into the workflow substrate.
+
+**Output shape:** `WorkflowParallelismReport = ParallelCompositionVerdict(CompositionVerdict) | ParallelismUnsupported(ParallelismUnsupportedDetail)` where `ParallelismUnsupportedDetail` carries a typed `ParallelismUnsupportedKind` (not Stage 2b’s `IdempotencyUnsupportedDetail`, which names an unsupported *workflow* variant). The **algebra verdict** stays `CompositionVerdict` only (PR #529 / DB-18 constraint — no parallel verdict carrier). Unsupported paths stay explicit and fail-closed (C-8), including “pairwise non-commute” and “non-`ParallelEffect` root.”
+
+**Scope v1:** `ParallelEffect` whose **every branch is `LinearEffect`** (each branch’s `ops` is DB-18’s `List<OperationEffect>` — the shipped carrier still allows **empty** `ops`; Stage 2e does not tighten that yet). Nested `ParallelEffect` / `BranchEffect` / `LoopEffect` as direct parallel children return `ParallelismUnsupported` with a reason — not a silent `None`.
+
+---
+
+## DB-18 §Open question 1 — resolution
+
+| Option | Verdict |
+|--------|---------|
+| (a) Additive `commutativity: CommutativityWitness` on `ParallelEffect` | **Rejected for Stage 2e.** Would duplicate facts derivable from per-op shapes (Q3), unless a future consumer proves a witness is *not* derivable from the op algebra alone. |
+| (b) Derive from op-level algebra without a substrate field | **Adopted for read/delete pairwise checks.** **Upsert×Upsert** cross-branch pairs are **not** certified in v1: `UpsertEffect` carries key provenance only (no value / merge-law witness), so parallel scheduling treats **all** Upsert×Upsert as **non-commute** (fail-closed) until the algebra exposes an explicit concurrent-write witness. **Different** `KeySource` values (including different `PathParam` *names*) do **not** imply runtime key disjointness without a witness (fail-closed). |
+
+---
+
+## Commutativity model (derived)
+
+For parallel branches that are each linear sequences of operations, **safe concurrent scheduling** requires that for **every** operation `a` taken from branch `i` and **every** operation `b` taken from branch `j` with `i ≠ j`, the two operations **commute** as state updates: reordering `a` before `b` does not change the observable outcome relative to `b` before `a`, under the effect algebra’s state model.
+
+**Precedence:** if **any** operation is breaking (`IsBreaking`), parallel reorder is unsound regardless of pairwise checks — the report projects through `CompositionVerdict::BrokenBy { first_breaker: BreakingOperation }` (same breaker discovery order as linear `compose_effects`: branch order, then op order within each branch).
+
+**Idempotent pairs** use a conservative partial function `idempotent_pair_commutes` on `IdempotentShape`:
+
+- `ReadEffect` ∘ `ReadEffect` — commutes.
+- `DeleteEffect` ∘ `DeleteEffect` — **same** `KeySource` commutes (same cell deleted).
+- `UpsertEffect` ∘ `UpsertEffect` — **never** commutes in v1 (no payload / merge-law witness on the carrier; concurrent upserts are fail-closed).
+- **Distinct** `PathParam` parameter names do not prove disjoint runtime keys (`{id}` vs `{user_id}` can alias); inequality on `KeySource` → **not** commute in v1.
+- Mixed `Upsert`/`Delete` or `CompositeKey`/`InputField` combinations default to **not** commuting until a richer key-disjointness story exists (conservative).
+
+This is **physics in the op algebra**, not a heuristic re-invented inside the lens body — the lens only combines facts already on `OperationEffect` (`feedback_lenses_not_passes`).
+
+---
+
+## Substrate principle audit (Q1–Q6)
+
+**Q1 — Cardinality:** No change to `ParallelEffect.branches: NonSingletonList<…>`; empty or singleton parallel workflows remain unrepresentable at the type level.
+
+**Q2 — Typed handles:** No new raw `PortId` surfaces; analysis uses `OperationEffect` and `WorkflowEffect` only.
+
+**Q3 — Duplicated fact:** No commutativity field on `ParallelEffect`; derivation-only.
+
+**Q4 — Coproduct dissolution:** No new coproduct; report sum `WorkflowParallelismReport` is a **lens boundary** sum (same class as `WorkflowIdempotencyReport`), not a second effect-algebra verdict type.
+
+**Q5 — Construction authority:** Workflow shape remains from `Dag::try_register_lane2_workflow_effect`; the lens only reads.
+
+**Q6 — Representation duality:** Single report path per `(dag, root)` analysis; unsupported carries reason text, not parallel “maybe” fields.
+
+---
+
+## `CompositionVerdict` projection map
+
+| Situation | `ParallelCompositionVerdict` payload |
+|-----------|--------------------------------------|
+| All branches linear, no breaking op, all cross-branch pairs commute | `IdempotentComposition` |
+| Any breaking op in any branch | `BrokenBy { first_breaker }` |
+| Non-linear branch, wrong root variant, or pairwise non-commute | Not a `CompositionVerdict` — use `ParallelismUnsupported` with typed `kind` + `reason` |
+
+---
+
+## STOP-AND-ESCALATE (Lane C)
+
+Escalate to a DB revision if:
+
+- Extending `WorkflowEffect` beyond DB-18’s four variants becomes necessary (not done here).
+- `ParallelEffect.branches` cardinality must change (not observed in Stage 2e v1).
+- A stored witness field becomes **provably** non-derivable from `OperationEffect` (would reopen path (a)).
+
+---
+
+## Related paths
+
+- Rust entry: `v3_compiler::analyze_parallelism` (re-exported from `lens_parallelism`).
+- Tests: `src/v3/compiler/tests/lane2_stage_2e_parallelism_test.rs`.

docs/lane2-compile-time-proofs.md

@@ -185,30 +185,11 @@ Emits diagnostic for unexpected complexity (e.g., hidden O(n²) via captured lis
 
 **Escalation:** if recognition rules for O(n²) require solving arbitrary symbolic arithmetic, scope tighter — recognize the thesis doc's two patterns (nested fold, sort-before-commutative) and document what's not recognized. Don't build a full symbolic math library.
 
-### Stage 2e — Parallelism-as-lens (S)
+### Stage 2e — Parallelism-as-lens (DB-20 shipped; thesis graph slice still open)
 
-**Scope:** `thesis_parallelism_test.rs` already asserts structural parallelism via `has_transitive_dependency`. Stage 2e promotes that structural fact to a lens output users can see.
+**Delivered (DB-20):** [design-db20-lane2-stage2e-parallelism-lens.md](./design-db20-lane2-stage2e-parallelism-lens.md). The lens consumes `WorkflowEffect::ParallelEffect` from DB-18 and checks **pairwise commutativity** of `OperationEffect` values across concurrent linear branches, projecting through `CompositionVerdict` (no parallel verdict carrier). Facts are **derived** from existing op shapes and `KeySource`; **Upsert×Upsert** cross-branch pairs are **fail-closed** (no merge/value witness on `UpsertEffect`). Entry point: `v3_compiler::analyze_parallelism`; report: `WorkflowParallelismReport`; stub: `src/v3/lenses/parallelism.dag` (Rust authority until reflection + `match` on user sums land).
 
-New lens `src/v3/lenses/parallelism.dag`:
-```
-fn analyze_parallelism(d: Dag, workflow: NodeId) -> List<ParallelizationOpportunity>
-
-type ParallelizationOpportunity
-  = IndependentBindings(NodeId, NodeId)     // "a and b have no dep, run in parallel"
-  | MapPromotion(NodeId)                     // "this fold is actually a map"
-  | CommutativeReduction(NodeId, AlgebraRef) // "this fold reduces on a commutative monoid — tree-reducible"
-```
-
-Unignores `parallel_fold_on_commutative_monoid_is_reducible`.
-
-**Acceptance:**
-- Structural parallelism tests from `thesis_parallelism_test.rs` now emit a corresponding `ParallelizationOpportunity` entry in the lens's output
-- Commutative monoid fold produces `CommutativeReduction` entry
-- Lens output is **data, not a diagnostic**. Per INVARIANTS.md:410-417 there is no "info" severity. IDE tooling reads the lens output and may surface "this fold is parallelizable" as an inline hint; the compiler itself treats the output as structured data, not as a diagnostic
-
-**Severity discipline**: parallelism-as-lens output is DATA. Not a warning, not an info, not a diagnostic. Downstream tooling (IDE, docs generation, compile-time parallelization passes) consume it. If user code declares `where parallel_reducible` and the analysis disagrees, THAT declaration mismatch IS an error — but "this could be parallelized" on unconstrained code is just information the lens produces.
-
-**Escalation:** if commutative-monoid detection requires algebra-awareness the `.dag` compiler doesn't have yet (operator-on-declared-Monoid-instance lookup), surface. That primitive might live in algebra.dag; if it doesn't, it's a prerequisite.
+**Still open (thesis Stage 2e, not DB-20):** `thesis_parallelism_test.rs` structural parallelism (`has_transitive_dependency`), fold-on-commutative-monoid promotion, `parallel_fold_on_commutative_monoid_is_reducible`, and `ParallelizationOpportunity`-style **data** outputs — orthogonal to the workflow `ParallelEffect` carrier. **Tracker:** [ROADMAP.md](../ROADMAP.md) §Lane 2 Stage 2e — **Deferral: thesis graph-parallelism slice** (single authority; avoids orphaning this work after DB-20 narrowed the Stage 2e heading).
 
 ### Stage 2f — User-declared dimensions (S)
 
@@ -253,7 +234,7 @@ XL aggregate (six stages), overlaps Lane 1 starting after 1b. Per-stage sizes:
 - 2b: L
 - 2c: M
 - 2d: M
-- 2e: S
+- 2e: split — DB-20 workflow slice S; **thesis graph-parallelism deferral** (see ROADMAP) additional S–M
 - 2f: S
 
 Some internal parallelism possible if 2+ implementers.