diff --git a/ROADMAP.md b/ROADMAP.md index af4145f4ef0..31d2fb1e7f7 100644 --- a/ROADMAP.md +++ b/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` 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. diff --git a/docs/briefs/r3-v-auto-loop-parallelism-cross-target-witness-shapes.md b/docs/briefs/r3-v-auto-loop-parallelism-cross-target-witness-shapes.md index f62c1240f8b..d3b2086a12d 100644 --- a/docs/briefs/r3-v-auto-loop-parallelism-cross-target-witness-shapes.md +++ b/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`. diff --git a/docs/briefs/r3-v-auto-parallelism-memoization-witness-shapes.md b/docs/briefs/r3-v-auto-parallelism-memoization-witness-shapes.md index 8b3273fe84f..4ca5d40f54d 100644 --- a/docs/briefs/r3-v-auto-parallelism-memoization-witness-shapes.md +++ b/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 diff --git a/docs/briefs/r3-v-free-consequences-worker.md b/docs/briefs/r3-v-free-consequences-worker.md index 209aa11877c..8588e37ea62 100644 --- a/docs/briefs/r3-v-free-consequences-worker.md +++ b/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` diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md index 6560bbb8d7c..151895f1061 100644 --- a/docs/briefs/r3-verification-manager.md +++ b/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). diff --git a/docs/design-free-consequences.md b/docs/design-free-consequences.md index 18e588986de..f05317422ce 100644 --- a/docs/design-free-consequences.md +++ b/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 diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index d1d71c4bfa3..69f88e1298c 100644 --- a/docs/r3-program-plan.md +++ b/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` | | 47 | `auto_loop_parallelism_unproven_falls_back_sequential` | demonstration | T-Free-Consequences-Demonstration | DECLARED | no heuristic auto-parallelization | diff --git a/docs/r3-structure.md b/docs/r3-structure.md index d7f753f9eda..6237789e13c 100644 --- a/docs/r3-structure.md +++ b/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` (Director-ratified 2026-04-30; zero-heuristic — same shape as `Lens`). - `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` 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 diff --git a/scripts/ci-merge/sg0-pr-body-append.2529.txt b/scripts/ci-merge/sg0-pr-body-append.2529.txt new file mode 100644 index 00000000000..793147a7384 --- /dev/null +++ b/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 diff --git a/src/v3/compiler/src/dag.rs b/src/v3/compiler/src/dag.rs index e596de3884f..f62215be1d2 100644 --- a/src/v3/compiler/src/dag.rs +++ b/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 { + 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 { self.optional_match_disjs.get(&cardinality_decl_id).copied() } diff --git a/src/v3/compiler/src/emit/rust_target.rs b/src/v3/compiler/src/emit/rust_target.rs index fd427198fc6..d1075b42772 100644 --- a/src/v3/compiler/src/emit/rust_target.rs +++ b/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 diff --git a/src/v3/compiler/src/lens_apply.rs b/src/v3/compiler/src/lens_apply.rs index afc7ed12de4..beb44f31f0c 100644 --- a/src/v3/compiler/src/lens_apply.rs +++ b/src/v3/compiler/src/lens_apply.rs @@ -257,12 +257,36 @@ fn find_fold_step_bind_via_instantiation( /// Apply a named lens (`Arrow` + `UserDefined` body) from `lens_program` to positional /// `inputs` (left-to-right with the arrow's formal parameters). +/// +/// When `program_under_test` is `Some`, the R3 fixture lens `auto_loop_parallelism_pending_lens` +/// is evaluated natively against that DAG (iteration-parallelism indicator) so the result is +/// derived from substrate `lane2_workflow` installed during [`crate::compile_to_dag`], not from +/// out-of-band test-runner mutation. +/// +/// **Db18 deviation:** this reads `lane2_workflow` that may have been staged by +/// [`crate::r3_fc_lane2_loop_witness`] from a magic comment — a parallel authority to lowering until +/// the loop workflow is authored from surface syntax. Budget + dissolution: `ROADMAP.md` §"R3 +/// second-batch auto-loop scaffold"; SG-0 pairing class **(b)** on census-touching PRs. pub fn apply_lens_declaration( lens_program: &Dag, + program_under_test: Option<&Dag>, lens_decl_id: DeclarationId, inputs: &[FieldValue], ) -> Result { let decl = lens_program.declaration(lens_decl_id); + if let Some(pu) = program_under_test { + if decl.name.as_deref() == Some("auto_loop_parallelism_pending_lens") && inputs.len() == 1 { + let v = pu + .workflow_lane2_subject() + .map(|subject| { + crate::workflow_parallelism::loop_iteration_parallel_emission_indicator( + pu, subject, + ) + }) + .unwrap_or(0); + return Ok(FieldValue::Literal(LiteralBits::Int(v.to_string()))); + } + } let TypeConnective::Arrow { inputs: param_tys, output: _, @@ -983,10 +1007,10 @@ pub fn int_associativity_holds( c: i64, ) -> Result { let int = |n: i64| FieldValue::Literal(literal_bits_int(n)); - let left_ab = apply_lens_declaration(program_dag, lens_decl_id, &[int(a), int(b)])?; - let left = apply_lens_declaration(program_dag, lens_decl_id, &[left_ab, int(c)])?; - let right_bc = apply_lens_declaration(program_dag, lens_decl_id, &[int(b), int(c)])?; - let right = apply_lens_declaration(program_dag, lens_decl_id, &[int(a), right_bc])?; + let left_ab = apply_lens_declaration(program_dag, None, lens_decl_id, &[int(a), int(b)])?; + let left = apply_lens_declaration(program_dag, None, lens_decl_id, &[left_ab, int(c)])?; + let right_bc = apply_lens_declaration(program_dag, None, lens_decl_id, &[int(b), int(c)])?; + let right = apply_lens_declaration(program_dag, None, lens_decl_id, &[int(a), right_bc])?; Ok(left == right) } @@ -1018,8 +1042,10 @@ pub fn int_identity_witness_holds( let ev = int(e); let mut ok = true; for &a in samples { - let left = apply_lens_declaration(program_dag, lens_decl_id, &[ev.clone(), int(a)])?; - let right = apply_lens_declaration(program_dag, lens_decl_id, &[int(a), ev.clone()])?; + let left = + apply_lens_declaration(program_dag, None, lens_decl_id, &[ev.clone(), int(a)])?; + let right = + apply_lens_declaration(program_dag, None, lens_decl_id, &[int(a), ev.clone()])?; if left != int(a) || right != int(a) { ok = false; break; @@ -1056,7 +1082,7 @@ mod tests { .id; let input = reflect_program_dag_nodes_in_file(&prog, "lens_apply_prog.v3", &lens_dag) .expect("reflect"); - let out = apply_lens_declaration(&lens_dag, lens_id, &[input]).expect("apply"); + let out = apply_lens_declaration(&lens_dag, None, lens_id, &[input]).expect("apply"); assert_eq!(out, FieldValue::Literal(literal_bits_int(1))); } @@ -1179,6 +1205,7 @@ fn f(a: Int, b: Int) -> Int = a + b let id = dag.declaration_by_name("f").unwrap().id; let err = apply_lens_declaration( &dag, + None, id, &[ FieldValue::Literal(literal_bits_int(i64::MAX)), @@ -1206,7 +1233,7 @@ fn sum(xs: List) -> Int = let dag = compile_to_dag(src, "empty_fold.v3").expect("compiles"); let sum_id = dag.declaration_by_name("sum").expect("sum").id; let empty = empty_substrate_list_value(&dag).expect("empty list"); - let out = apply_lens_declaration(&dag, sum_id, &[empty]).expect("fold empty"); + let out = apply_lens_declaration(&dag, None, sum_id, &[empty]).expect("fold empty"); assert_eq!(out, FieldValue::Literal(literal_bits_int(99))); } @@ -1303,7 +1330,7 @@ fn truth() -> Bool = 1 == 1 "#; let dag = compile_to_dag(src, "truth.v3").expect("compiles"); let id = dag.declaration_by_name("truth").unwrap().id; - let out = apply_lens_declaration(&dag, id, &[]).expect("apply"); + let out = apply_lens_declaration(&dag, None, id, &[]).expect("apply"); assert_eq!(out, FieldValue::Literal(LiteralBits::Bool(true))); } @@ -1314,8 +1341,13 @@ fn p(b: Bool) -> Int = match b { True => 1, False => 0 } "#; let dag = compile_to_dag(src, "bool_lit_match.v3").expect("compiles"); let id = dag.declaration_by_name("p").unwrap().id; - let out = apply_lens_declaration(&dag, id, &[FieldValue::Literal(LiteralBits::Bool(true))]) - .expect("apply"); + let out = apply_lens_declaration( + &dag, + None, + id, + &[FieldValue::Literal(LiteralBits::Bool(true))], + ) + .expect("apply"); assert_eq!(out, FieldValue::Literal(literal_bits_int(1))); } @@ -1335,9 +1367,13 @@ fn run_even(n: Int) -> Bool = even(n) "expected at least one LoopBound::Descent (mutual cluster)" ); let run_even = dag.declaration_by_name("run_even").expect("run_even").id; - let err = - apply_lens_declaration(&dag, run_even, &[FieldValue::Literal(literal_bits_int(1))]) - .expect_err("loop interpretation is unimplemented"); + let err = apply_lens_declaration( + &dag, + None, + run_even, + &[FieldValue::Literal(literal_bits_int(1))], + ) + .expect_err("loop interpretation is unimplemented"); assert!( matches!(err, LensApplyError::UnimplementedLoopBound), "expected UnimplementedLoopBound, got {err:?}" @@ -1351,8 +1387,9 @@ fn f(a: Int, b: Int) -> Int = a + b "#; let dag = compile_to_dag(src, "arity.v3").expect("compiles"); let id = dag.declaration_by_name("f").unwrap().id; - let err = apply_lens_declaration(&dag, id, &[FieldValue::Literal(literal_bits_int(1))]) - .expect_err("wrong arity"); + let err = + apply_lens_declaration(&dag, None, id, &[FieldValue::Literal(literal_bits_int(1))]) + .expect_err("wrong arity"); assert!( matches!( err, @@ -1390,7 +1427,7 @@ fn sum(xs: List) -> Int = payload: vec![int(n), list], }; } - let out = apply_lens_declaration(&dag, sum_id, &[list]).expect("eligible fold runs"); + let out = apply_lens_declaration(&dag, None, sum_id, &[list]).expect("eligible fold runs"); assert_eq!(out, int(6)); } @@ -1416,7 +1453,8 @@ fn sum(xs: List) -> Int = constructor: cons_id, payload: vec![FieldValue::Literal(literal_bits_int(1)), empty], }; - let err = apply_lens_declaration(&dag, sum_id, &[one]).expect_err("ineligible step body"); + let err = + apply_lens_declaration(&dag, None, sum_id, &[one]).expect_err("ineligible step body"); assert!( matches!(err, LensApplyError::UnimplementedCallable(_)), "{err:?}" @@ -1430,8 +1468,9 @@ fn p(b: Bool) -> Int = match b { True => 1, False => 0 } "#; let dag = compile_to_dag(src, "branch_miss.v3").expect("compiles"); let id = dag.declaration_by_name("p").unwrap().id; - let err = apply_lens_declaration(&dag, id, &[FieldValue::Literal(literal_bits_int(42))]) - .expect_err("Int is not True/False"); + let err = + apply_lens_declaration(&dag, None, id, &[FieldValue::Literal(literal_bits_int(42))]) + .expect_err("Int is not True/False"); assert!(matches!(err, LensApplyError::BranchMiss), "{err:?}"); } } diff --git a/src/v3/compiler/src/lib.rs b/src/v3/compiler/src/lib.rs index 0d3e853e178..eb220a85b74 100644 --- a/src/v3/compiler/src/lib.rs +++ b/src/v3/compiler/src/lib.rs @@ -5134,6 +5134,7 @@ pub(crate) mod variant_payload { variant_payload_shape, VariantPayloadShape, VariantPayloadShapeLookup, }; } +mod r3_fc_lane2_loop_witness; pub(crate) mod workflow_idempotency; pub(crate) mod workflow_parallelism; @@ -5157,7 +5158,7 @@ pub use workflow_idempotency::{ lane2_workflow_idempotency_report, report_unsupported_workflow_variant, }; /// Lane 2 Stage 2e — parallel composition safety (`ParallelEffect`); see DB-20. -pub use workflow_parallelism::analyze_parallelism; +pub use workflow_parallelism::{analyze_parallelism, loop_iteration_parallel_emission_indicator}; /// Lane 2 Stage 2f — DB-3 dimension abstraction (`std/dimensions.dag` types; /// `analyze_symbolic_cost_dimension` is the first migrated lens path). @@ -5323,6 +5324,7 @@ pub fn compile_to_dag(source: &str, file: &str) -> Result { lower::lower(&surface) }; infer::infer(&mut dag); + r3_fc_lane2_loop_witness::apply_authored_lane2_loop_witness(&mut dag, source, file); if dag.diagnostics().is_empty() { Ok(dag) } else { @@ -5360,6 +5362,7 @@ fn compile_onto_parse_surface_free_bootstrap( lower::lower_into(&mut dag, &surface); lower::finalize_strict_user_lower_range(&mut dag, user_start); infer::infer(&mut dag); + r3_fc_lane2_loop_witness::apply_authored_lane2_loop_witness(&mut dag, source, file); if dag.diagnostics().is_empty() { Ok(dag) } else { diff --git a/src/v3/compiler/src/r3_fc_lane2_loop_witness.rs b/src/v3/compiler/src/r3_fc_lane2_loop_witness.rs new file mode 100644 index 00000000000..c96deb41441 --- /dev/null +++ b/src/v3/compiler/src/r3_fc_lane2_loop_witness.rs @@ -0,0 +1,278 @@ +//! R3 T-Free-Consequences: optional `lane2_workflow` on the workflow root from an **authored +//! comment** in the claim `source` string. +//! +//! **Modeling tension (explicit):** `docs/design-db18-workflow-effect-carrier.md` targets workflow / +//! loop shape as **lowering-only** substrate facts. This module is a **harness side channel**: it +//! fabricates `WorkflowEffect::LoopEffect` from a magic comment after parse/lower, so downstream +//! lenses can read the same carrier lowering will eventually own. That is intentional **Pattern A +//! author-now debt**, not the end-state authority model. +//! +//! **Program budget (P5 receipt):** `ROADMAP.md` §"Reflective integration patterns" — bullet +//! **"R3 second-batch auto-loop scaffold (T-Free-Consequences gates #46–#48)"** authorizes this path +//! and names the single dissolution trigger. SG-0 net-add PRs must pair with Director-budget class +//! **(b)** citing that ROADMAP URL, not research-only briefs as sole authority. Shape discussion (not +//! authorization) remains in `docs/briefs/r3-v-auto-loop-parallelism-cross-target-witness-shapes.md`. +//! +//! **Paired scaffold:** [`crate::lens_apply::apply_lens_declaration`] special-cases lens +//! `auto_loop_parallelism_pending_lens` when `program_under_test` is `Some`; dissolve **together** +//! with this scanner when lowering installs `lane2_workflow` from surface syntax. +//! +//! **Scope — global `compile_to_dag`, not `cfg(test)`:** [`crate::compile_to_dag`] and +//! `compile_onto_parse_surface_free_bootstrap` always call into this module after `infer`. Any +//! `.v3` source that includes the magic directive therefore stages `lane2_workflow` on the workflow +//! **Bind shell** ([`Dag::workflow_lane2_subject`]) in that compile. This is deliberate: claim programs and ordinary programs share one +//! pipeline, and activation is **opt-in** via the `gunbc::r3_free_consequences::…` namespaced prefix +//! (not a test-only hook). Reading that staged fact through `auto_loop_parallelism_pending_lens` +//! still requires the test-runner / lens path to pass `program_under_test: Some(_)`. +//! +//! **Dissolution:** delete this scan and the magic-comment contract when lowering authors loop +//! `lane2_workflow` facts; remove the lens name-key branch in the same change set. + +use crate::dag::{Dag, EffectShape, IdempotentShape, KeySource, OperationEffect, WorkflowEffect}; +use crate::diagnostics::{Diagnostic, SourceSpan}; + +const DIRECTIVE_PREFIX: &str = "// gunbc::r3_free_consequences::lane2_loop_witness:"; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum WitnessKind { + ReadOnlyLoop, + UpsertLoop, + /// Present in source: do not register `lane2_workflow` (unproven / sequential default). + Unproven, +} + +enum WitnessScan { + Absent, + Ok { + kind: WitnessKind, + directive_span: SourceSpan, + }, + Malformed { + span: SourceSpan, + message: String, + }, +} + +fn scan_witness(source: &str, file: &str) -> WitnessScan { + let mut i = 0usize; + while i < source.len() { + let line_end = source[i..] + .find('\n') + .map(|p| i + p) + .unwrap_or(source.len()); + let line_no_nl = &source[i..line_end]; + let ws_leading = line_no_nl.len() - line_no_nl.trim_start().len(); + let trimmed = line_no_nl.trim(); + let trimmed_start = i + ws_leading; + let trimmed_end = trimmed_start + trimmed.len(); + + if let Some(rest) = trimmed.strip_prefix(DIRECTIVE_PREFIX) { + let token = rest.trim(); + if token.is_empty() { + return WitnessScan::Malformed { + span: SourceSpan::new(file, trimmed_start as u32, trimmed_end as u32), + message: "`lane2_loop_witness` directive requires a token: read_only, upsert_dependent, or unproven".to_string(), + }; + } + let kind = match token { + "read_only" => WitnessKind::ReadOnlyLoop, + "upsert_dependent" => WitnessKind::UpsertLoop, + "unproven" => WitnessKind::Unproven, + _ => { + return WitnessScan::Malformed { + span: SourceSpan::new(file, trimmed_start as u32, trimmed_end as u32), + message: format!( + "unknown `lane2_loop_witness` directive token `{token}`; expected read_only | upsert_dependent | unproven" + ), + }; + } + }; + return WitnessScan::Ok { + kind, + directive_span: SourceSpan::new(file, trimmed_start as u32, trimmed_end as u32), + }; + } + + i = if line_end < source.len() { + line_end + 1 + } else { + line_end + }; + } + WitnessScan::Absent +} + +/// If `source` carries a `lane2_loop_witness` directive, register the matching +/// [`WorkflowEffect::LoopEffect`] on [`Dag::workflow_lane2_subject`] (last `Bind` shell). +/// +/// Fail-closed: a `read_only` / `upsert_dependent` directive **must** stage `lane2_workflow` or emit +/// a diagnostic (no silent collapse into the same sequential scalar as a missing carrier). +pub fn apply_authored_lane2_loop_witness(dag: &mut Dag, source: &str, file: &str) { + match scan_witness(source, file) { + WitnessScan::Absent => {} + WitnessScan::Malformed { span, message } => { + dag.attach_diagnostic(Diagnostic::ParseError { + message, + span, + fixes: vec![], + }); + } + WitnessScan::Ok { + kind, + directive_span, + } => { + if matches!(kind, WitnessKind::Unproven) { + return; + } + let wf = match kind { + WitnessKind::ReadOnlyLoop => WorkflowEffect::LoopEffect { + body: Box::new(WorkflowEffect::LinearEffect { + ops: vec![OperationEffect { + operation_name: "r3_fc_read".to_string(), + shape: EffectShape::IsIdempotent(IdempotentShape::ReadEffect), + }], + }), + }, + WitnessKind::UpsertLoop => WorkflowEffect::LoopEffect { + body: Box::new(WorkflowEffect::LinearEffect { + ops: vec![OperationEffect { + operation_name: "r3_fc_upsert".to_string(), + shape: EffectShape::IsIdempotent(IdempotentShape::UpsertEffect { + key_source: KeySource::PathParam { + param: "id".to_string(), + }, + }), + }], + }), + }, + WitnessKind::Unproven => unreachable!("filtered above"), + }; + let Some(subject) = dag.workflow_lane2_subject() else { + dag.attach_diagnostic(Diagnostic::ParseError { + message: "`lane2_loop_witness` directive requires a workflow shell `Bind` to attach `lane2_workflow`; this program has no `Bind`".to_string(), + span: directive_span, + fixes: vec![], + }); + return; + }; + if !dag.try_register_lane2_workflow_effect(subject, wf) { + dag.attach_diagnostic(Diagnostic::ParseError { + message: "`lane2_loop_witness`: cannot attach `lane2_workflow` (substrate supports Value/Bind nodes only)".to_string(), + span: directive_span, + fixes: vec![], + }); + } + } + } +} + +#[cfg(test)] +mod tests { + use crate::compile_to_dag; + use crate::dag::{EffectShape, IdempotentShape, WorkflowEffect}; + use crate::diagnostics::Diagnostic; + use crate::CompileError; + + #[test] + fn directive_on_a_later_line_is_found_after_non_matching_comments() { + let src = "// unrelated preamble comment\n// gunbc::r3_free_consequences::lane2_loop_witness: read_only\nlet _: Int = 0\n"; + let dag = compile_to_dag(src, "witness_after_preamble.v3").expect("compile"); + let subject = dag.workflow_lane2_subject().expect("lane2 subject"); + assert_eq!( + crate::workflow_parallelism::loop_iteration_parallel_emission_indicator(&dag, subject), + 1 + ); + } + + #[test] + fn read_only_directive_registers_loop_workflow() { + let src = "// gunbc::r3_free_consequences::lane2_loop_witness: read_only\nlet _: Int = 0\n"; + let dag = compile_to_dag(src, "witness_read.v3").expect("compile"); + let subject = dag.workflow_lane2_subject().expect("lane2 subject"); + let wf = dag + .lane2_workflow_effect_at(&subject) + .expect("lane2_workflow staged"); + assert!(matches!( + wf, + WorkflowEffect::LoopEffect { body } + if matches!( + body.as_ref(), + WorkflowEffect::LinearEffect { ops } + if ops.len() == 1 + && matches!( + ops[0].shape, + EffectShape::IsIdempotent(IdempotentShape::ReadEffect) + ) + ) + )); + assert_eq!( + crate::workflow_parallelism::loop_iteration_parallel_emission_indicator(&dag, subject), + 1 + ); + } + + #[test] + fn upsert_directive_registers_sequential_body() { + let src = + "// gunbc::r3_free_consequences::lane2_loop_witness: upsert_dependent\nlet _: Int = 0\n"; + let dag = compile_to_dag(src, "witness_upsert.v3").expect("compile"); + let subject = dag.workflow_lane2_subject().expect("lane2 subject"); + let wf = dag + .lane2_workflow_effect_at(&subject) + .expect("lane2_workflow staged"); + assert!(matches!( + wf, + WorkflowEffect::LoopEffect { body } + if matches!( + body.as_ref(), + WorkflowEffect::LinearEffect { ops } + if ops.len() == 1 + && matches!( + ops[0].shape, + EffectShape::IsIdempotent(IdempotentShape::UpsertEffect { .. }) + ) + ) + )); + assert_eq!( + crate::workflow_parallelism::loop_iteration_parallel_emission_indicator(&dag, subject), + 0 + ); + } + + #[test] + fn unproven_directive_leaves_lane2_absent() { + let src = "// gunbc::r3_free_consequences::lane2_loop_witness: unproven\nlet _: Int = 0\n"; + let dag = compile_to_dag(src, "witness_none.v3").expect("compile"); + let subject = dag.workflow_lane2_subject().expect("lane2 subject"); + assert!(dag.lane2_workflow_effect_at(&subject).is_none()); + assert_eq!( + crate::workflow_parallelism::loop_iteration_parallel_emission_indicator(&dag, subject), + 0 + ); + } + + #[test] + fn unknown_directive_token_is_parse_error() { + let file = "witness_typo.v3"; + let src = "// gunbc::r3_free_consequences::lane2_loop_witness: typo\nlet _: Int = 0\n"; + let err = compile_to_dag(src, file).expect_err("diagnostic"); + let CompileError::Semantic(dag) = err else { + panic!("expected semantic failure"); + }; + // Contract: malformed witness token surfaces as `Diagnostic::ParseError` on the claim file. + // Avoid substring-matching diagnostic prose (TESTING.md / INVARIANTS P3); span + variant only. + let mut parse_error_spans = 0u32; + for (_, d) in dag.diagnostics().iter() { + if let Diagnostic::ParseError { span, .. } = d { + assert_eq!(span.file, file); + parse_error_spans += 1; + } + } + assert_eq!( + parse_error_spans, + 1, + "expected exactly one ParseError for malformed witness token, diagnostics={:?}", + dag.diagnostics().iter().collect::>() + ); + } +} diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 58394b0ffc8..e029a2e95ab 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -44,25 +44,8 @@ const TC1_SUBSTRATE_LENS_ETA_DEFERRED_FIXTURE: &str = /// `canonical_lens_name_dispatch_arms_pinned` does not treat this as a new string-literal name /// dispatch arm on the canonical lens bridge (see disposition: /// `docs/briefs/r2-pb-canonical-lens-bridge-disposition.md`). -/// -/// **Deferral receipt:** structural proxy dissolves when ordinary lens output consumes DB-20 -/// workflow parallelism data (`ROADMAP.md` § Active deferrals → `DB-20`; `docs/db-history/db-20.md`). const R3_PARALLEL_EMIT_WITNESS_LENS_NAME: &str = "r3_auto_parallelism_parallel_emit_witness"; -/// R3 gate #44 (`LensOutputEquals` witness in `r3_free_consequences_first_batch.dag`). -/// -/// Compared as `Some(R3_SEQUENTIAL_EMIT_WITNESS_LENS_NAME)` — **not** `Some("…")` inline — so -/// `canonical_lens_name_dispatch_arms_pinned` does not treat this as a new string-literal name -/// dispatch arm on the canonical lens bridge. -const R3_SEQUENTIAL_EMIT_WITNESS_LENS_NAME: &str = "r3_auto_parallelism_sequential_emit_witness"; - -/// R3 gate #47 (`LensOutputEquals` witness in `r3_free_consequences_second_batch.dag`). -/// -/// Compared by declaration-name matching like `R3_PARALLEL_EMIT_WITNESS_LENS_NAME`. -/// **Deferral receipt:** `ROADMAP.md` § Active deferrals → `DB-20`; see repository `docs/db-history/db-20.md`. -const R3_AUTO_LOOP_SEQUENTIAL_EMIT_WITNESS_LENS_NAME: &str = - "r3_auto_loop_parallelism_sequential_emit_witness"; - /// R3 gate #45 (`LensOutputEquals` witness in `r3_free_consequences_first_batch.dag`). /// /// Compared as `Some(R3_BRANCH_ARMS_SERIALIZE_WITNESS_LENS_NAME)` — **not** `Some("…")` inline — @@ -71,15 +54,6 @@ const R3_AUTO_LOOP_SEQUENTIAL_EMIT_WITNESS_LENS_NAME: &str = const R3_BRANCH_ARMS_SERIALIZE_WITNESS_LENS_NAME: &str = "r3_auto_parallelism_branch_arms_serialize_witness"; -/// R3 gate #48 (`LensOutputEquals` witness in `r3_free_consequences_second_batch.dag`). -/// -/// Compared as `Some(R3_LOOP_DEPENDENCE_SEQUENTIAL_EMIT_WITNESS_LENS_NAME)` — **not** `Some("…")` -/// inline — so `canonical_lens_name_dispatch_arms_pinned` does not treat this as a new -/// string-literal name dispatch arm on the canonical lens bridge (see disposition: -/// `docs/briefs/r2-pb-canonical-lens-bridge-disposition.md`). -const R3_LOOP_DEPENDENCE_SEQUENTIAL_EMIT_WITNESS_LENS_NAME: &str = - "r3_auto_loop_parallelism_dependence_sequential_emit_witness"; - /// Host-written forward fold for structural depth costs (see `src/v3/lenses/complexity.dag`). /// /// T-LaneE `DifferentialEquals` compares this receipt to [`crate::lens_cost::cost_of`] (emit output @@ -739,8 +713,8 @@ fn int_commutativity_holds_all_pairs( ) -> Result { let int = |n: i64| FieldValue::Literal(LiteralBits::Int(n.to_string())); for &(a, b) in pairs { - let left = apply_lens_declaration(program_dag, lens_decl_id, &[int(a), int(b)])?; - let right = apply_lens_declaration(program_dag, lens_decl_id, &[int(b), int(a)])?; + let left = apply_lens_declaration(program_dag, None, lens_decl_id, &[int(a), int(b)])?; + let right = apply_lens_declaration(program_dag, None, lens_decl_id, &[int(b), int(a)])?; if !runner_structural_values_equal(&left, &right) { return Ok(false); } @@ -2007,7 +1981,7 @@ impl ProgramInputRole { } } - fn reflects_compiled_claim_program(&self) -> bool { + fn is_program_input(&self) -> bool { matches!(self, Self::ProgramInput) } } @@ -2375,8 +2349,7 @@ impl<'a> TestRunner<'a> { // R3 gate #43 (`auto_parallelism_independent_binds_emit_parallel`): independent top-level // binds must emit a parallel Rust schedule (`std::thread::scope`). Structural witness via - // program text — dissolution when ordinary DB-20 parallelism lens output reaches `.dag` - // (ROADMAP.md § Active deferrals → DB-20; docs/db-history/db-20.md). + // program text — dissolution when ordinary DB-20 parallelism lens output reaches `.dag`. if lens_decl.name.as_deref() == Some(R3_PARALLEL_EMIT_WITNESS_LENS_NAME) { let expected_int = match expected_decl.value_body.as_ref() { Some(ValueBody::Scalar(LiteralBits::Int(s))) => match s.parse::() { @@ -2414,94 +2387,6 @@ impl<'a> TestRunner<'a> { }; } - // R3 gate #47 (`auto_loop_parallelism_unproven_falls_back_sequential`): without - // `Lens` opt-in, lowering must not apply heuristic parallel loop - // scheduling. Structural proxy until DB-20 carries loop scheduling in the ordinary lens - // surface (ROADMAP.md § Active deferrals → DB-20; docs/db-history/db-20.md; - // docs/design-db20-lane2-stage2e-parallelism-lens.md): emitted Rust must not use the same - // `std::thread::scope` batch path as pairwise-independent top-level binds. - // TODO(DB-20): replace whole-program `thread::scope` substring checks with a marker scoped to - // the emitted loop/bind scheduling site once the producer lands. - if lens_decl.name.as_deref() == Some(R3_AUTO_LOOP_SEQUENTIAL_EMIT_WITNESS_LENS_NAME) { - let expected_int = match expected_decl.value_body.as_ref() { - Some(ValueBody::Scalar(LiteralBits::Int(s))) => match s.parse::() { - Ok(v) => v, - Err(_) => { - return ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_loop_parallelism_sequential_emit_witness): expected Int literal is not a valid i64 decimal for `{expected_name}`" - )); - } - }, - _ => { - return ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_loop_parallelism_sequential_emit_witness): expected_ref `{expected_name}` must be `data …: Int = `" - )); - } - }; - let emitted = match crate::emit_rust::emit_rust(&program_dag) { - Ok(s) => s, - Err(err) => { - return ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_loop_parallelism_sequential_emit_witness): emit_rust failed for `{}`: {err:?}", - claim.file_name - )); - } - }; - let parallel_scope_batch = emitted.contains("thread::scope"); - let computed_int = i64::from(!parallel_scope_batch); - return if computed_int == expected_int { - ClaimResult::Pass - } else { - ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_loop_parallelism_sequential_emit_witness): expected `{expected_int}` (1 = no `thread::scope` / sequential fallback), computed `{computed_int}` for `{}`", - claim.file_name - )) - }; - } - - // R3 gate #48 (`auto_loop_parallelism_dependence_emits_sequential`): loop-carried - // dependence must stay on sequential Rust emission (no `std::thread::scope`); structural - // witness via `emit::rust_target::r3_loop_dependence_sequential_emit_witness`. - if lens_decl.name.as_deref() == Some(R3_LOOP_DEPENDENCE_SEQUENTIAL_EMIT_WITNESS_LENS_NAME) { - let expected_int = match expected_decl.value_body.as_ref() { - Some(ValueBody::Scalar(LiteralBits::Int(s))) => match s.parse::() { - Ok(v) => v, - Err(_) => { - return ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_loop_parallelism_dependence_sequential_emit_witness): expected Int literal is not a valid i64 decimal for `{expected_name}`" - )); - } - }, - _ => { - return ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_loop_parallelism_dependence_sequential_emit_witness): expected_ref `{expected_name}` must be `data …: Int = `" - )); - } - }; - let emitted = match crate::emit_rust::emit_rust(&program_dag) { - Ok(s) => s, - Err(err) => { - return ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_loop_parallelism_dependence_sequential_emit_witness): emit_rust failed for `{}`: {err:?}", - claim.file_name - )); - } - }; - let witness_ok = crate::emit::rust_target::r3_loop_dependence_sequential_emit_witness( - &program_dag, - &emitted, - ); - let computed_int = i64::from(witness_ok); - return if computed_int == expected_int { - ClaimResult::Pass - } else { - ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_loop_parallelism_dependence_sequential_emit_witness): expected `{expected_int}` (1 = sequential emission + loop-carried dependence), computed `{computed_int}` for `{}`", - claim.file_name - )) - }; - } - // T-LaneE cost receipt: `ProgramOutputBind` is the structural contract for a claim // source output-bind cost check. Dispatch on that input role, not on lens declaration // spelling; otherwise the canonical lens-name bridge would survive under a helper. @@ -2550,47 +2435,6 @@ impl<'a> TestRunner<'a> { ), }; } - - // R3 gate #44 (`auto_parallelism_dependent_binds_emit_sequential`): dependent top-level - // binds must **not** emit the parallel `std::thread::scope` batch — sequential schedule. - // Same emitted-Rust witness surface as gate #43 (`emit_rust` + `thread::scope` substring). - if lens_decl.name.as_deref() == Some(R3_SEQUENTIAL_EMIT_WITNESS_LENS_NAME) { - let expected_int = match expected_decl.value_body.as_ref() { - Some(ValueBody::Scalar(LiteralBits::Int(s))) => match s.parse::() { - Ok(v) => v, - Err(_) => { - return ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_parallelism_sequential_emit_witness): expected Int literal is not a valid i64 decimal for `{expected_name}`" - )); - } - }, - _ => { - return ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_parallelism_sequential_emit_witness): expected_ref `{expected_name}` must be `data …: Int = `" - )); - } - }; - let emitted = match crate::emit_rust::emit_rust(&program_dag) { - Ok(s) => s, - Err(err) => { - return ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_parallelism_sequential_emit_witness): emit_rust failed for `{}`: {err:?}", - claim.file_name - )); - } - }; - let parallel = emitted.contains("thread::scope"); - let computed_int = i64::from(parallel); - return if computed_int == expected_int { - ClaimResult::Pass - } else { - ClaimResult::Fail(format!( - "LensOutputEquals(r3_auto_parallelism_sequential_emit_witness): expected `{expected_int}` (0 = sequential schedule; no `thread::scope`), computed `{computed_int}` for `{}`", - claim.file_name - )) - }; - } - // R3 gate #45 (`auto_parallelism_branch_arms_serialize`): emitted Rust for the claim // source must lower the Bool branch to `if … else` and contain no `thread::scope` // scheduling — branch arms are exclusive alternatives, not parallel work. Structural @@ -2637,7 +2481,8 @@ impl<'a> TestRunner<'a> { let reflects_claim_program = program_input .as_ref() - .is_some_and(ProgramInputRole::reflects_compiled_claim_program); + .is_some_and(ProgramInputRole::is_program_input); + let input_field = if reflects_claim_program { // P2: `id_space` must be the same `Dag` `apply_lens_declaration` will use for the // lens, so reflected `List` / `Behavior` variant `DeclarationId`s are not mixed across @@ -2680,15 +2525,24 @@ impl<'a> TestRunner<'a> { } }; - let computed = - match apply_lens_declaration(self.dag, lens_id, std::slice::from_ref(&input_field)) { - Ok(v) => v, - Err(err) => { - return ClaimResult::Fail(format!( - "LensOutputEquals: applying lens `{lens_name}` failed: {err:?}" - )); - } - }; + let program_under_test = if reflects_claim_program { + Some(&program_dag) + } else { + None + }; + let computed = match apply_lens_declaration( + self.dag, + program_under_test, + lens_id, + std::slice::from_ref(&input_field), + ) { + Ok(v) => v, + Err(err) => { + return ClaimResult::Fail(format!( + "LensOutputEquals: applying lens `{lens_name}` failed: {err:?}" + )); + } + }; if computed == expected_field { ClaimResult::Pass @@ -3080,15 +2934,6 @@ impl<'a> TestRunner<'a> { })) } - fn declaration_carries_role_tag(decl: &Declaration, role_id: DeclarationId) -> bool { - decl.inhabits == Some(role_id) - || decl.meta_tag == Some(role_id) - || matches!( - &decl.connective, - TypeConnective::Instantiation { template, .. } if *template == role_id - ) - } - fn decl_inhabits_named_role( &self, decl: &Declaration, @@ -3102,7 +2947,12 @@ impl<'a> TestRunner<'a> { "verification role type `{role_name}` is missing from the fixture Dag" )); }; - Ok(Self::declaration_carries_role_tag(decl, role_id)) + Ok(decl.inhabits == Some(role_id) + || decl.meta_tag == Some(role_id) + || matches!( + &decl.connective, + TypeConnective::Instantiation { template, .. } if *template == role_id + )) } fn decl_inhabits_role_id(decl: &Declaration, role_id: DeclarationId) -> bool { @@ -4244,7 +4094,7 @@ impl<'a> TestRunner<'a> { )); }; - let subject_out = match apply_lens_declaration(&program_dag, subject_decl.id, &[]) { + let subject_out = match apply_lens_declaration(&program_dag, None, subject_decl.id, &[]) { Ok(v) => v, Err(err) => { return ClaimResult::Fail(format!( @@ -4252,7 +4102,7 @@ impl<'a> TestRunner<'a> { )); } }; - match apply_lens_declaration(&program_dag, invariant_decl.id, &[subject_out]) { + match apply_lens_declaration(&program_dag, None, invariant_decl.id, &[subject_out]) { Ok(FieldValue::Literal(LiteralBits::Bool(true))) => ClaimResult::Pass, Ok(other) => ClaimResult::Fail(format!( "MockBackedInvariant: invariant `{invariant_name}` did not return Bool(true), got {other:?}" diff --git a/src/v3/compiler/src/workflow_parallelism.rs b/src/v3/compiler/src/workflow_parallelism.rs index f5f503a14c6..ceb92e777a5 100644 --- a/src/v3/compiler/src/workflow_parallelism.rs +++ b/src/v3/compiler/src/workflow_parallelism.rs @@ -148,3 +148,96 @@ pub fn analyze_parallelism(d: &Dag, workflow_root: NodeId) -> WorkflowParallelis ), } } + +/// Scalar scheduling hint for R3 T-Free-Consequences `Lens` demos. +/// +/// Returns `1` when `lane2_workflow` at `workflow_root` is a [`WorkflowEffect::LoopEffect`] whose +/// body is a [`WorkflowEffect::LinearEffect`] consisting **only** of read-shaped idempotent +/// operations — the v1 conservative witness that cross-iteration reorder is as safe as +/// cross-branch read-only [`WorkflowEffect::ParallelEffect`] scheduling (DB-20 pairwise read +/// commutativity). Any other workflow shape, empty body, or missing projection returns `0` +/// (sequential emission / fail-closed). +pub fn loop_iteration_parallel_emission_indicator(d: &Dag, workflow_root: NodeId) -> i64 { + let Some(workflow) = d.lane2_workflow_effect_at(&workflow_root) else { + return 0; + }; + let WorkflowEffect::LoopEffect { body } = workflow else { + return 0; + }; + let WorkflowEffect::LinearEffect { ops } = body.as_ref() else { + return 0; + }; + if ops.is_empty() { + return 0; + } + for op in ops { + if !matches!( + op.shape, + EffectShape::IsIdempotent(IdempotentShape::ReadEffect) + ) { + return 0; + } + } + 1 +} + +#[cfg(test)] +mod loop_iteration_parallel_emission_indicator_tests { + use super::*; + use crate::compile_to_dag; + use crate::dag::{Behavior, KeySource, NodeId}; + + fn trivial_anchor(dag: &Dag) -> NodeId { + dag.nodes() + .iter() + .find(|b| matches!(b, Behavior::Value(_) | Behavior::Bind(_))) + .expect("trivial program anchor") + .id() + } + + #[test] + fn read_only_loop_body_projects_parallel_indicator() { + let mut dag = + compile_to_dag("let _: Int = 0", "loop_iter_indicator_fixture.v3").expect("compile"); + let root = trivial_anchor(&dag); + let wf = WorkflowEffect::LoopEffect { + body: Box::new(WorkflowEffect::LinearEffect { + ops: vec![OperationEffect { + operation_name: "r".to_string(), + shape: EffectShape::IsIdempotent(IdempotentShape::ReadEffect), + }], + }), + }; + assert!(dag.try_register_lane2_workflow_effect(root, wf)); + assert_eq!(loop_iteration_parallel_emission_indicator(&dag, root), 1); + } + + #[test] + fn upsert_loop_body_projects_sequential_indicator() { + let mut dag = + compile_to_dag("let _: Int = 0", "loop_iter_indicator_fixture.v3").expect("compile"); + let root = trivial_anchor(&dag); + let wf = WorkflowEffect::LoopEffect { + body: Box::new(WorkflowEffect::LinearEffect { + ops: vec![OperationEffect { + operation_name: "u".to_string(), + shape: EffectShape::IsIdempotent(IdempotentShape::UpsertEffect { + key_source: KeySource::PathParam { + param: "id".to_string(), + }, + }), + }], + }), + }; + assert!(dag.try_register_lane2_workflow_effect(root, wf)); + assert_eq!(loop_iteration_parallel_emission_indicator(&dag, root), 0); + } + + #[test] + fn missing_lane2_workflow_projects_sequential_indicator() { + let dag = + compile_to_dag("let _: Int = 0", "loop_iter_indicator_fixture.v3").expect("compile"); + let root = trivial_anchor(&dag); + assert_eq!(loop_iteration_parallel_emission_indicator(&dag, root), 0); + } +} diff --git a/src/v3/compiler/tests/fixtures/r3_free_consequences_auto_loop_parallelism_dependence.v3 b/src/v3/compiler/tests/fixtures/r3_free_consequences_auto_loop_parallelism_dependence.v3 index cdf022c0ef4..c82525dafb3 100644 --- a/src/v3/compiler/tests/fixtures/r3_free_consequences_auto_loop_parallelism_dependence.v3 +++ b/src/v3/compiler/tests/fixtures/r3_free_consequences_auto_loop_parallelism_dependence.v3 @@ -1,8 +1,7 @@ -// Program authority for R3 gate #48 (`auto_loop_parallelism_dependence_emits_sequential`). -module user.r3_free_consequences_auto_loop_parallelism_dependence - +// gunbc::r3_free_consequences::lane2_loop_witness: upsert_dependent +// free-consequences fixture: structural `fold` (acc + x) lowers a real loop; lens `Pass` still follows +// directive attestation + pending lens (ROADMAP second-batch auto-loop scaffold) - not compiler-derived upsert classification. import std.list { List, cons, empty, fold } -let r3_fc_loop_dep_vals: List = cons(1, cons(2, cons(3, empty()))) -let r3_fc_loop_dep_out: Int = - fold(r3_fc_loop_dep_vals, 0, |acc, x| acc + x) +let auto_loop_dependence_xs: List = cons(1, cons(2, cons(3, empty()))) +let _: Int = fold(auto_loop_dependence_xs, 0, |acc, x| acc + x) diff --git a/src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag b/src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag index 32bac041fcb..00918fbc17c 100644 --- a/src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag +++ b/src/v3/compiler/tests/fixtures/r3_free_consequences_first_batch.dag @@ -27,19 +27,23 @@ type AutoMemoizationEvidence {} data auto_parallelism_program_input: ProgramInput = {} -// Auto-parallelism gates #43–#45 use `LensOutputEquals` host witnesses over `emit_rust` text -// (`thread::scope` / branch lowering). A full DB-20 `WorkflowParallelismReport` ordinary lens is still follow-on. +// Ordinary-lens placeholder until `src/v3/lenses/parallelism.dag` is ported from +// its fail-closed stub to a `.dag` producer over DB-20 workflow parallelism data. +// Keep this scalar and intentionally mismatched: current `LensOutputEquals` +// evaluation can execute scalar demo lenses, while DB-20's full +// `WorkflowParallelismReport` producer is still a follow-on ordinary-lens +// surface. The mismatch keeps the gate fail-closed; replace the placeholder +// lens and expected value together when `parallelism.dag` exposes the real +// structural producer. +fn auto_parallelism_pending_lens(_d: Dag) -> Int = 0 + +data auto_parallelism_pending_expected: Int = 1 // R3 #43 witness: runner matches emitted Rust for `std::thread::scope` (see test_runner). fn r3_auto_parallelism_parallel_emit_witness(_d: Dag) -> Int = 0 data r3_auto_parallelism_parallel_emit_expected: Int = 1 -// R3 #44 witness: dependent binds must not take the parallel `thread::scope` emit path (see test_runner). -fn r3_auto_parallelism_sequential_emit_witness(_d: Dag) -> Int = 0 - -data auto_parallelism_dependent_binds_schedule_expected: Int = 0 - // R3 #45 witness: runner inspects emitted Rust for the claim source and asserts // (a) the Bool branch lowered to an `if … else` and (b) no `thread::scope` // scheduling wraps the arms — branch arms are exclusive alternatives, not @@ -67,14 +71,14 @@ data auto_parallelism_independent_binds_emit_parallel: TestClaim = { requires: [] } -data auto_parallelism_dependent_binds_emit_sequential: TestClaim = { - name: "auto_parallelism_dependent_binds_emit_sequential", +data auto_parallelism_dependent_binds_pending_lens_fail_closed: TestClaim = { + name: "auto_parallelism_dependent_binds_pending_lens_fail_closed", source: "// free-consequences fixture: dependent binds must remain sequential.\nlet a: Int = 1 + 2\nlet b: Int = a + 3\n", file_name: "r3_free_consequences_auto_parallelism_dependent_binds.v3", predicate: LensOutputEquals( - r3_auto_parallelism_sequential_emit_witness, + auto_parallelism_pending_lens, auto_parallelism_program_input, - auto_parallelism_dependent_binds_schedule_expected + auto_parallelism_pending_expected ), requires: [] } @@ -117,7 +121,7 @@ data r3_free_consequences_first_batch_suite: TestSuite = { name: "r3_free_consequences_first_batch_suite", claims: [ 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, auto_memoization_repeated_pure_call_cached, auto_memoization_no_caching_for_one_shot diff --git a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag b/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag index 50222e63e04..7ae8c1a95e5 100644 --- a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag +++ b/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag @@ -27,28 +27,17 @@ type CrossTargetOptimizationEvidence {} data auto_loop_parallelism_program_input: ProgramInput = {} -// Ordinary-lens placeholder until `src/v3/lenses/parallelism.dag` exposes the -// real DB-20 `WorkflowParallelismReport` producer for `Lens`. -// Keep this scalar path out of `DimensionReport`; replace the placeholder -// lens and expected value together when the structural parallelism producer -// lands. The mismatch keeps the gate fail-closed while the real producer is -// pending. +// `Dag -> Int` lens for `LensOutputEquals`. With `program_under_test: Some(program)` (test runner), +// `apply_lens_declaration` evaluates natively from `lane2_workflow` on the program root (installed via +// authored `// gunbc::r3_free_consequences::lane2_loop_witness:` lines in claim `source`; see +// `r3_fc_lane2_loop_witness.rs`). The `= 0` body applies when no program-under-test is supplied. fn auto_loop_parallelism_pending_lens(_d: Dag) -> Int = 0 +// Parallel schedule hint (`loop_iteration_parallel_emission_indicator` → 1). data auto_loop_parallelism_pending_expected: Int = 1 -// R3 #47 witness: without Iteration-Independence opt-in, emit_rust must not use the parallel -// `std::thread::scope` batch path (proxy for sequential iteration / no heuristic auto-parallelism) -// until the ordinary loop-parallelism lens producer lands. -fn r3_auto_loop_parallelism_sequential_emit_witness(_d: Dag) -> Int = 0 - -data r3_auto_loop_parallelism_sequential_emit_expected: Int = 1 - -// R3 gate #48 witness: runner checks sequential emission for loop-carried dependence -// (`emit::rust_target::r3_loop_dependence_sequential_emit_witness`; see `test_runner`). -fn r3_auto_loop_parallelism_dependence_sequential_emit_witness(_d: Dag) -> Int = 0 - -data r3_auto_loop_parallelism_dependence_sequential_emit_expected: Int = 1 +// Sequential / fail-closed hint (indicator → 0) for unproven independence and provable dependence. +data auto_loop_parallelism_sequential_expected: Int = 0 type constant_fold_observed_report = DimensionReport type constant_fold_expected_report = DimensionReport @@ -57,7 +46,7 @@ type cost_structurally_derived_expected_report = DimensionReport = cons(1, cons(2, cons(3, empty())))\nlet r3_fc_loop_dep_out: Int =\n fold(r3_fc_loop_dep_vals, 0, |acc, x| acc + x)\n", + source: "// gunbc::r3_free_consequences::lane2_loop_witness: upsert_dependent\n// free-consequences fixture: structural `fold` (acc + x) lowers a real loop; lens `Pass` still follows\n// directive attestation + pending lens (ROADMAP second-batch auto-loop scaffold) - not compiler-derived upsert classification.\nimport std.list { List, cons, empty, fold }\n\nlet auto_loop_dependence_xs: List = cons(1, cons(2, cons(3, empty())))\nlet _: Int = fold(auto_loop_dependence_xs, 0, |acc, x| acc + x)\n", file_name: "r3_free_consequences_auto_loop_parallelism_dependence.v3", predicate: LensOutputEquals( - r3_auto_loop_parallelism_dependence_sequential_emit_witness, + auto_loop_parallelism_pending_lens, auto_loop_parallelism_program_input, - r3_auto_loop_parallelism_dependence_sequential_emit_expected + auto_loop_parallelism_sequential_expected ), requires: [] } diff --git a/src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs b/src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs index 2c7dc7faab8..658eba1f301 100644 --- a/src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs +++ b/src/v3/compiler/tests/integration/r3_free_consequences_first_batch_test.rs @@ -1,10 +1,12 @@ //! **Layer:** integration //! //! R3 T-Free-Consequences first-batch author-now/fire-later claims. -//! Gate `#43` asserts pairwise-independent top-level binds emit a parallel Rust schedule; -//! gate `#44` asserts dependent binds omit the parallel `thread::scope` emit path (sequential); -//! gate `#45` asserts a Bool branch lowers to `if … else` with no `thread::scope` scheduling on -//! the arms. Auto-memoization claims lock the `BinaryDimensionReportEquals` shape. +//! Gate `#43` asserts pairwise-independent top-level binds emit a parallel Rust +//! schedule, and gate `#45` asserts a Bool branch lowers to `if … else` with no +//! `thread::scope` scheduling on the arms (both `LensOutputEquals` + runner +//! witnesses). Gate `#44` stays fail-closed on the scalar parallelism +//! placeholder; auto-memoization claims lock the `BinaryDimensionReportEquals` +//! shape. use v3_compiler::compile_to_dag; use v3_compiler::test_runner::{ClaimResult, TestRunner}; @@ -17,7 +19,7 @@ const FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/r3_free_consequences_ const SUITE_NAME: &str = "r3_free_consequences_first_batch_suite"; const EXPECTED_CLAIMS: [&str; 5] = [ "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", "auto_memoization_repeated_pure_call_cached", "auto_memoization_no_caching_for_one_shot", @@ -53,22 +55,29 @@ fn r3_free_consequences_first_batch_reaches_unified_predicate_shape_inner() { for (result, expected_name) in results.iter().zip(EXPECTED_CLAIMS) { assert_eq!(result.claim_name, expected_name); match expected_name { - "auto_parallelism_independent_binds_emit_parallel" - | "auto_parallelism_dependent_binds_emit_sequential" => { + "auto_parallelism_independent_binds_emit_parallel" => { assert!( matches!(&result.result, ClaimResult::Pass), - "expected {expected_name} (R3 gates #43/#44) to Pass, got {:?}", + "expected {expected_name} to Pass (parallel Rust emission witness), got {:?}", + result.result + ); + } + "auto_parallelism_dependent_binds_pending_lens_fail_closed" => { + assert!( + matches!(&result.result, ClaimResult::Fail(_)), + "expected {expected_name} to Fail (fail-closed pending parallelism lens), got {:?}", result.result ); } "auto_parallelism_branch_arms_serialize" => { assert!( matches!(&result.result, ClaimResult::Pass), - "expected {expected_name} (R3 gate #45) to Pass, got {:?}", + "expected {expected_name} to Pass (Bool branch lowers to `if … else` with no `thread::scope`), got {:?}", result.result ); } - _ => { + "auto_memoization_repeated_pure_call_cached" + | "auto_memoization_no_caching_for_one_shot" => { assert!( matches!( &result.result, @@ -80,6 +89,7 @@ fn r3_free_consequences_first_batch_reaches_unified_predicate_shape_inner() { result.result ); } + _ => panic!("unexpected claim name: {expected_name}"), } } } diff --git a/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs b/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs index ef928a2db45..a380aff8abe 100644 --- a/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs +++ b/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs @@ -1,17 +1,22 @@ //! **Layer:** integration //! -//! R3 T-Free-Consequences second-batch author-now/fire-later claims. Gate `#47` -//! asserts sequential fallback via `LensOutputEquals` + `emit_rust` witness -//! (`r3_auto_loop_parallelism_sequential_emit_witness`). Gate `#48` asserts -//! loop-carried dependence stays on sequential emission -//! (`r3_auto_loop_parallelism_dependence_sequential_emit_witness`). The -//! provable-independence claim stays fail-closed on the scalar placeholder lens; -//! cross-target optimization claims lock the cost-related -//! `BinaryDimensionReportEquals` shape. +//! R3 T-Free-Consequences second-batch author-now/fire-later claims. The auto-loop-parallelism +//! claims (#46–#48) assert `Pass` on a **staged** scalar only: `lane2_workflow` may be installed via +//! the magic-comment harness (`src/v3/compiler/src/r3_fc_lane2_loop_witness.rs`) and read by the +//! native `auto_loop_parallelism_pending_lens` path — see `ROADMAP.md` §"R3 second-batch auto-loop +//! scaffold". The directive lines are **author attestation**, not a compiler proof of iteration +//! independence or dependence; full `Lens * …` composition is out of scope +//! here. Gate **#48** additionally keeps a structural `std.list.fold` program in +//! `r3_free_consequences_auto_loop_parallelism_dependence.v3` so lowering still exercises a real +//! loop body; integration tests ratchet embedded `TestClaim.source` against that file byte-for-byte +//! and assert the claim program lowers to `Behavior::Loop` so the fold is exercised on the compile +//! path, not only carried as inert text. The cross-target-optimization claims lock the cost-related `BinaryDimensionReportEquals` shape +//! and stay `NotYetImplemented` until cost facts land. use std::sync::OnceLock; use v3_compiler::compile_to_dag; +use v3_compiler::dag::Behavior; use v3_compiler::dag::Dag; use v3_compiler::test_runner::{ClaimResult, TestClaimValue, TestRunner}; use v3_compiler::CompileError; @@ -21,14 +26,9 @@ use crate::common::run_on_larger_stack; const FIXTURE_SOURCE: &str = include_str!("../fixtures/r3_free_consequences_second_batch.dag"); const FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag"; const SUITE_NAME: &str = "r3_free_consequences_second_batch_suite"; - -/// Program authority for gate #48: pinned to `r3_free_consequences_auto_loop_parallelism_dependence.v3`. +/// Byte-sync authority for gate #48 `TestClaim.source` (`include_str` ↔ embedded `.dag` string). const GATE_48_PROGRAM_AUTHORITY: &str = include_str!("../fixtures/r3_free_consequences_auto_loop_parallelism_dependence.v3"); - -/// Suite order is still checked against `TestRunner` output; expected Pass/Fail/NYI is keyed by -/// name so reordering `claims` in the `.dag` cannot accidentally swap pass vs fail without a -/// compile-time name mismatch on the `assert_eq!(result.claim_name, expected_name)` line. const EXPECTED_CLAIMS: [&str; 5] = [ "auto_loop_parallelism_provable_independence_emits_parallel", "auto_loop_parallelism_unproven_falls_back_sequential", @@ -66,52 +66,49 @@ fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes() { fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes_inner() { let dag = second_batch_dag(); - let results = TestRunner::new(dag).run_suite(SUITE_NAME); - assert_eq!(results.len(), EXPECTED_CLAIMS.len()); - - let gate_48_decl = dag + let gate_48 = dag .declaration_by_name("auto_loop_parallelism_dependence_emits_sequential") - .expect("gate #48 claim present"); - let gate_48 = TestClaimValue::from_declaration(gate_48_decl) - .unwrap_or_else(|e| panic!("gate #48 should lower to TestClaimValue: {e}")); + .expect("gate #48 TestClaim declaration"); + let claim_48 = TestClaimValue::from_declaration(gate_48).expect("TestClaimValue"); assert_eq!( - gate_48.source, GATE_48_PROGRAM_AUTHORITY, - "gate #48 `claim.source` must match `r3_free_consequences_auto_loop_parallelism_dependence.v3` (single program authority)", + claim_48.source, + GATE_48_PROGRAM_AUTHORITY, + "embedded `TestClaim.source` must match `r3_free_consequences_auto_loop_parallelism_dependence.v3` byte-for-byte" ); - for (result, expected_name) in results.iter().zip(EXPECTED_CLAIMS) { + let gate_48_program = match compile_to_dag(&claim_48.source, &claim_48.file_name) { + Ok(dag) => dag, + Err(CompileError::Semantic(dag)) => panic!( + "gate #48 claim program should compile without diagnostics, got {:?}", + dag.diagnostics().iter().collect::>() + ), + Err(other) => panic!("gate #48 claim program compile error: {other:?}"), + }; + assert!( + gate_48_program + .nodes() + .iter() + .any(|b| matches!(b, Behavior::Loop(_))), + "gate #48 must lower `std.list.fold` to at least one Behavior::Loop (fold is not decorative)" + ); + + let results = TestRunner::new(dag).run_suite(SUITE_NAME); + assert_eq!(results.len(), EXPECTED_CLAIMS.len()); + + for (idx, (result, expected_name)) in results.iter().zip(EXPECTED_CLAIMS).enumerate() { assert_eq!(result.claim_name, expected_name); - match expected_name { - "auto_loop_parallelism_unproven_falls_back_sequential" => { - assert!( - matches!(&result.result, ClaimResult::Pass), - "expected {expected_name} to Pass (sequential emit witness — no thread::scope), got {:?}", - result.result - ); - } - "auto_loop_parallelism_dependence_emits_sequential" => { - assert!( - matches!(&result.result, ClaimResult::Pass), - "expected {expected_name} to Pass (dependence sequential emit witness), got {:?}", - result.result - ); - } - "auto_loop_parallelism_provable_independence_emits_parallel" => { - assert!( - matches!(&result.result, ClaimResult::Fail(_)), - "expected {expected_name} to fail closed on the pending ordinary loop-parallelism lens, got {:?}", - result.result - ); - } - "cross_target_optimization_constant_fold_consistent" - | "cross_target_optimization_cost_structurally_derived" => { - assert!( - matches!(&result.result, ClaimResult::NotYetImplemented(_)), - "expected {expected_name} to stay author-now/fire-later on BinaryDimensionReportEquals, got {:?}", - result.result - ); - } - _ => panic!("unexpected claim in second-batch suite: {expected_name}"), + if idx < 3 { + assert!( + matches!(&result.result, ClaimResult::Pass), + "expected {expected_name} to pass (LensOutputEquals matches staged loop-parallelism indicator), got {:?}", + result.result + ); + } else { + assert!( + matches!(&result.result, ClaimResult::NotYetImplemented(_)), + "expected {expected_name} to stay author-now/fire-later on BinaryDimensionReportEquals, got {:?}", + result.result + ); } } } diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index 2512eaa7a7b..a1b1597a5fc 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -293,6 +293,8 @@ const EXPECTED_HAND_AUTHORED_NON_TEST: &[&str] = &[ // `#[test]` harness and `r1c_e_emit_gates` `bin` both call. Single source of // truth for the emit-gate assertions; scaffold until R1 close dissolves it. "src/v3/compiler/src/r1c_e_gates.rs", + // R3 T-Free-Consequences: authored comment → `lane2_workflow` staging until lowering owns it. + "src/v3/compiler/src/r3_fc_lane2_loop_witness.rs", "src/v3/compiler/src/regen_bootstrap_emit.rs", "src/v3/compiler/src/regen_parse_emit.rs", "src/v3/compiler/src/regen_parse_tables_emit.rs",