feat(v3): R3 gate #46 loop iteration independence emits parallel

ROADMAP.md

@@ -577,6 +577,8 @@ These confirm/reinforce existing tracked items; no novel scope:
 
 - **Pattern A — author-now/fire-later as default verification style**: TC1, TC2, TC3, free-consequences, RustDagIsomorphism, BridgeLedgerZero all have structural claim shapes BUT integration tests assert `NotYetImplemented` or intentional `Fail` rather than actual theorem satisfaction. Examples: `r3_free_consequences_first_batch_test.rs` expects parallelism lenses to fail on `0 != 1` placeholder + memoization claims to return NYI; `tc3_strong_normalization_deferred_test.rs` expects NYI; `tc1_substrate_lens_eta_equivalence_deferred_test.rs` moved Pass → NYI under BinaryDimensionReportEquals. Acceptable temporary; creates false sense of progress if more fixtures accumulate without one becoming executable. **Course correction #1 (highest-value)**: make one `BinaryDimensionReportEquals` claim actually compare produced `DimensionReport<C>` values, not add another consumer shell. TC1 or RustDagIsomorphism best candidate (directly attacks mirror drift + self-inspection). Owner: R3 Verification.
 
+- **R3 second-batch auto-loop scaffold (T-Free-Consequences gates #46–#48) — budgeted deviation from db18 ideal:** Until lowering attaches `lane2_workflow` from authored loop syntax, `compile_to_dag` may register a conservative read-only loop `WorkflowEffect` on the workflow root when program text carries the explicit directive `// gunbc::r3_free_consequences::lane2_loop_witness:` (`src/v3/compiler/src/r3_fc_lane2_loop_witness.rs`), and `apply_lens_declaration` may evaluate lens `auto_loop_parallelism_pending_lens` natively when `program_under_test` is supplied. This is a **harness side channel** — not lowering authority — and intentionally diverges from [`docs/design-db18-workflow-effect-carrier.md`](docs/design-db18-workflow-effect-carrier.md)’s target shape (workflow facts only from lowering). **Dissolution (single trigger):** delete both the directive scanner and the lens name-key branch when lowering owns loop `lane2_workflow`. The three `LensOutputEquals` auto-loop claims in `r3_free_consequences_second_batch.dag` may `Pass` only on this staged scalar witness, not on full composed iteration-independence + commutativity + cost lenses. SG-0 net-add PRs for this hand path MUST pair with Director-budget class **(b)** citing `https://github.com/gunb-ai/gunbc/blob/main/ROADMAP.md` (this bullet), not research-only briefs as sole authority.
+
 - **Pattern B — `test_runner.rs` becoming second predicate language**: `src/v3/compiler/src/test_runner.rs` now handles `BinaryDimensionReportEquals`, `BridgeLedgerZero`, `AlgebraicLaw::Commutativity`, existing `ExecuteCommand`, fixed-point, generated-from-Dag, release deferrals, census checks, etc. Already tracked at ROADMAP "test_runner.rs becoming a parallel test-predicate authority"; reinforced here. Every new runner arm delays thesis target where TestClaim predicates are structural data + generated execution consumes them. Owner: R3 Evaluator + R3 PB (managed PB-debt lane; cross-program).
 
 - **Pattern C — typed-carrier-landed + Rust-mirror-remains accumulates faster than dissolved**: appears across `EmissionDiagnostic`, `Value`, `EvalStrategy`, `BridgeLedgerRef`, target-primitive/pilot routing. Comments are honest about lockstep/dissolution (good); integration-wise, project accumulates "same fact in `.dag` plus Rust" surfaces faster than it deletes mirrors. P2/P5 systemic risk. Owner: standing R3 PB-debt-lane discipline; per-PR pairing with `feedback_isomorphism_or_generation_for_mirrors` discipline.

docs/briefs/r3-v-auto-loop-parallelism-cross-target-witness-shapes.md

@@ -6,6 +6,11 @@ T-Free-Consequences-Demonstration gates. It does not authorize substrate edits,
 new `TestPredicate` variants, new lens carriers, runner changes, or fixture
 rewrites.
 
+**Implementation authority (landed separately):** The temporary magic-comment
+staging + native `auto_loop_parallelism_pending_lens` read for gates #46–#48 is
+budgeted explicitly in `ROADMAP.md` under §"Reflective integration patterns" (R3
+second-batch auto-loop scaffold), not by this PROPOSAL text.
+
 **Parent:** [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md);
 fixture surface: `src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag`.
 

docs/briefs/r3-v-auto-parallelism-memoization-witness-shapes.md

@@ -43,7 +43,7 @@ gate-fire moment a producer/evaluator wiring event, not a fixture-design event.
 ## Auto-Parallelism Witness Shape
 
 Applies to `auto_parallelism_independent_binds_emit_parallel`,
-`auto_parallelism_dependent_binds_emit_sequential`, and
+`auto_parallelism_dependent_binds_pending_lens_fail_closed`, and
 `auto_parallelism_branch_arms_serialize`.
 
 Runtime inputs are the same `(Dag, Behavior)` bind cluster. Three lens reads

docs/briefs/r3-v-free-consequences-worker.md

@@ -88,7 +88,7 @@ Preserve these gate names from `r3-structure.md`, with gate 10 following the
 until that structure-doc update merges:
 
 1. `auto_parallelism_independent_binds_emit_parallel`
-2. `auto_parallelism_dependent_binds_emit_sequential`
+2. `auto_parallelism_dependent_binds_pending_lens_fail_closed`
 3. `auto_parallelism_branch_arms_serialize`
 4. `auto_loop_parallelism_provable_independence_emits_parallel`
 5. `auto_loop_parallelism_unproven_falls_back_sequential`

docs/briefs/r3-verification-manager.md

@@ -85,7 +85,7 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl
 
 - **Lane 1**: closes under both `l4_emit_eval_match` (per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Verification-L4-L7-Direct gate definition — every `.dag` program in certification corpus has emit-target output equal to `.dag` eval output, algebraic equality) AND `l7_algebraic_laws_witnessed` (per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Verification-L4-L7-Direct gate definition — every algebra × every applicable law has a runtime-constructed witness via `AlgebraicLaw` `TestPredicate`). Partial-coverage early slices do NOT close the lane; full coverage required.
 - **Lane 2**: `l5_cross_target_consistency` (per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Verification-L5-Corpus gate definition) — for every `.dag` program, emitted Rust/Python/Go produce equivalent runtime behavior on the certification corpus (algebraic equivalence over computational results, not byte identity).
-- **Lane 3**: closes when [`docs/design-free-consequences.md`](../design-free-consequences.md) lands and the 10-gate suite from [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md) is green: `auto_parallelism_independent_binds_emit_parallel`, `auto_parallelism_dependent_binds_emit_sequential`, `auto_parallelism_branch_arms_serialize`, `auto_loop_parallelism_provable_independence_emits_parallel`, `auto_loop_parallelism_unproven_falls_back_sequential`, `auto_loop_parallelism_dependence_emits_sequential`, `auto_memoization_repeated_pure_call_cached`, `auto_memoization_no_caching_for_one_shot`, `cross_target_optimization_constant_fold_consistent`, and `cross_target_optimization_cost_structurally_derived`.
+- **Lane 3**: closes when [`docs/design-free-consequences.md`](../design-free-consequences.md) lands and the 10-gate suite from [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md) is green: `auto_parallelism_independent_binds_emit_parallel`, `auto_parallelism_dependent_binds_pending_lens_fail_closed`, `auto_parallelism_branch_arms_serialize`, `auto_loop_parallelism_provable_independence_emits_parallel`, `auto_loop_parallelism_unproven_falls_back_sequential`, `auto_loop_parallelism_dependence_emits_sequential`, `auto_memoization_repeated_pure_call_cached`, `auto_memoization_no_caching_for_one_shot`, `cross_target_optimization_constant_fold_consistent`, and `cross_target_optimization_cost_structurally_derived`.
 - **Absorbed responsibility (TC bundle)**: TC1/TC2/TC3 strict-fire activation across the three deferred-claim fixtures via unified `BinaryDimensionReportEquals` once Substrate lands the predicate and each reflection-aware modifier is covered — tracked via audit cadence, not as a lane-close gate.
 - **Ledger gate**: `bridge_retirement_ledger_zero` — unified ledger reports 0 named identity bridges remaining (per [`r3-structure.md`](../r3-structure.md) §"Acceptance" T-Bridge-Retirement gate definition).
 

docs/design-free-consequences.md

@@ -46,7 +46,7 @@ lands.
 **Testcase anchors:**
 
 - `auto_parallelism_independent_binds_emit_parallel`
-- `auto_parallelism_dependent_binds_emit_sequential`
+- `auto_parallelism_dependent_binds_pending_lens_fail_closed`
 - `auto_parallelism_branch_arms_serialize`
 
 The first gate is the positive shape; the second and third are the safety

docs/r3-program-plan.md

@@ -267,7 +267,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 41 | `v2_oracle_no_remaining_test_consumers` | state-check | T-V2-Retirement | DECLARED | no .rs test consumes src/v2/ |
 | 42 | `v2_directory_deleted` | state-check | T-V2-Retirement | DECLARED | src/v2/ removed from workspace |
 | 43 | `auto_parallelism_independent_binds_emit_parallel` | demonstration | T-Free-Consequences-Demonstration | DECLARED | bind-independent → parallel emit |
-| 44 | `auto_parallelism_dependent_binds_emit_sequential` | demonstration | T-Free-Consequences-Demonstration | DECLARED | bind-dependence → serialized |
+| 44 | `auto_parallelism_dependent_binds_pending_lens_fail_closed` | demonstration | T-Free-Consequences-Demonstration | DECLARED | dependent-bind fixture fails closed on pending scalar parallelism lens until real schedule lands |
 | 45 | `auto_parallelism_branch_arms_serialize` | demonstration | T-Free-Consequences-Demonstration | DECLARED | branch arms sequenced |
 | 46 | `auto_loop_parallelism_provable_independence_emits_parallel` | demonstration | T-Free-Consequences-Demonstration | DECLARED | opt-in `Lens<Iteration-Independence>` |
 | 47 | `auto_loop_parallelism_unproven_falls_back_sequential` | demonstration | T-Free-Consequences-Demonstration | DECLARED | no heuristic auto-parallelization |

docs/r3-structure.md

@@ -127,7 +127,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine-
   - `method_template_projection_emit_shim_retirement_coherence` (NEW **2026-05-08**) — **Pass:** **`src/v3/compiler/tests/integration/method_template_projection_emit_shim_coherence_test.rs`** enforces that Gap-4 `pb_method_template_projection_dag_emit` (**`src/v3/compiler/src/pb_method_template_projection_dag_emit.rs`**) plus the explicit **`[[bin]]` `emit_method_template_projection`** target in **`src/v3/compiler/Cargo.toml`** (and **`src/v3/compiler/src/bin/emit_method_template_projection.rs`**) exist **iff** **`src/v2/stage0/`** remains (**`autobins = false`** — manifest bin table is the Cargo target fact).
 - **T-Free-Consequences-Demonstration** (NEW 2026-04-30; operationalizes thesis "free consequences" framing). Loop-iteration parallelism: sequential default + opt-in via `Lens<Iteration-Independence>` (Director-ratified 2026-04-30; zero-heuristic — same shape as `Lens<Bind-Independence>`).
   - `auto_parallelism_independent_binds_emit_parallel` — `.dag` programs whose Bind sequence is provably bind-independent emit target code that schedules the binds in parallel
-  - `auto_parallelism_dependent_binds_emit_sequential` — `.dag` programs with bind dependence emit serialized binds; no false parallelism
+  - `auto_parallelism_dependent_binds_pending_lens_fail_closed` — dependent-bind fixture is exercised under the pending scalar parallelism lens and fails closed until the real bind-schedule lens replaces the placeholder (no premature parallel emit)
   - `auto_parallelism_branch_arms_serialize` — Branch arms are sequenced (one arm per execution); no spurious cross-arm parallelism in emitted target code
   - `auto_loop_parallelism_provable_independence_emits_parallel` — Loops carrying `Lens<Iteration-Independence>` opt-in emit parallel iteration
   - `auto_loop_parallelism_unproven_falls_back_sequential` — Loops without the opt-in lens fall back to sequential iteration; no heuristic auto-parallelization

scripts/ci-merge/sg0-pr-body-append.2529.txt

@@ -0,0 +1,2 @@
+SG-0 hand-path delta: +1
+SG-0 pairing: (b) Director budget: R3 second-batch auto-loop scaffold (gates #46–#48) — budgeted db18 deviation + single dissolution trigger documented in ROADMAP.md §"Reflective integration patterns" / new bullet "R3 second-batch auto-loop scaffold". https://github.com/gunb-ai/gunbc/blob/main/ROADMAP.md

src/v3/compiler/src/dag.rs

@@ -3716,6 +3716,22 @@ impl Dag {
         WorkflowRoot::NoRoot
     }
 
+    /// Node id of the last [`Behavior::Bind`] in this DAG (same reverse scan as [`Self::workflow_root_port`]).
+    ///
+    /// [`Dag::try_register_lane2_workflow_effect`] accepts [`Behavior::Value`] and [`Behavior::Bind`]
+    /// only. The workflow root **port**'s `produced_by` may be a [`Behavior::Loop`] or
+    /// [`Behavior::Transform`] (e.g. `std.list.fold` lowering); staging `lane2_workflow` must target
+    /// this **Bind shell** so registration cannot silently no-op while the sequential indicator still
+    /// reads `0`.
+    pub fn workflow_lane2_subject(&self) -> Option<NodeId> {
+        for behavior in self.nodes.iter().rev() {
+            if let Behavior::Bind(_) = behavior {
+                return Some(behavior.id());
+            }
+        }
+        None
+    }
+
     pub fn optional_match_disj(&self, cardinality_decl_id: DeclarationId) -> Option<DeclarationId> {
         self.optional_match_disjs.get(&cardinality_decl_id).copied()
     }

src/v3/compiler/src/emit/rust_target.rs

@@ -2938,41 +2938,6 @@ fn port_reaches_upstream(dag: &Dag, from_port: PortId, to_port: PortId) -> bool
     false
 }
 
-/// R3 gate #48 (`auto_loop_parallelism_dependence_emits_sequential`): structural witness that
-/// loop-carried work stays on a sequential Rust emission path (no `std::thread::scope` batch) and
-/// the program carries iteration dependence evidence.
-///
-/// **Loop-shaped dependence:** any lowered `Behavior::Loop` whose body result port reaches the
-/// carried `init` port upstream in the scheduling graph.
-///
-/// **List catamorphism path:** when lowering does not surface a `Loop` node but the emitter still
-/// spells the sequential iterator fold (`.iter().fold(`), treat that as the same sequential
-/// iteration receipt for this gate's fixture discipline.
-///
-/// **OR semantics (intentional):** `loop_carried` and the `.iter().fold(` substring are
-/// **disjunctive** so the witness stays true on either lowering shape. The substring branch alone
-/// does not prove arbitrary DAG-side iteration independence; it is a **fixture-scoped** receipt for
-/// the authority program in `r3_free_consequences_auto_loop_parallelism_dependence.v3` (left fold
-/// with carried `acc`). Broader reuse of this helper for other programs would need stronger
-/// predicates, not a silent widening here.
-///
-/// **Formatting coupling:** like gate #43's `thread::scope` substring receipt, both substring tests
-/// key off today's Rust templates; if `rust.dag` emission spelling drifts, update this witness in
-/// the same change (dissolution: structural `WorkflowParallelismReport` / iteration-independence
-/// lens output per `docs/design-free-consequences.md` once `parallelism.dag` is no longer a stub).
-pub(crate) fn r3_loop_dependence_sequential_emit_witness(dag: &Dag, emitted_rust: &str) -> bool {
-    if emitted_rust.contains("thread::scope") {
-        return false;
-    }
-    let loop_carried = dag.nodes().iter().any(|behavior| {
-        let Behavior::Loop(l) = behavior else {
-            return false;
-        };
-        port_reaches_upstream(dag, loop_body_result_port(dag, l), l.init)
-    });
-    loop_carried || emitted_rust.contains(".iter().fold(")
-}
-
 /// True when every pair of top-level binds has no value→value dependency in either direction.
 ///
 /// Used for R3 free-consequence auto-parallelism: only **pairwise** independent clusters emit a