R1C-C T-Sub fixture

docs/briefs/r1-closure-manager.md

@@ -75,6 +75,10 @@ Pending: none. The R1 Closure Manager lane queue is fully authored — manager d
 
 Lane status table refreshes here as work lands. Initial state: all 6 lane worker briefs authored; dispatch sequence: R1C-A first (critical-path enabler), then R1C-D after R1C-A Sub-deliverable B lands; R1C-B/C/E/F parallel-dispatchable Day-1.
 
+| Lane | Gates (strict `.dag` receipts) | Status |
+| --- | --- | --- |
+| R1C-C | `sub_type_alias_where_lowers` (`DeclarationHasRefinement("PositiveInt")` on the DB-11 witness; `sub_type_alias_where_lowers_gate` in `r1_gates.template.dag` + `test_runner_runs_sub_type_alias_where_lowers_gate`) | **Proposed receipt — PR #879** (pre-merge; not main-truth until squash-merge lands — then set lane-closed here per matrix hygiene) |
+
 ## Cross-refs
 
 - Parent: [`ROADMAP.md §"Release R1 Program"`](../../ROADMAP.md) — R1 lane structure + acceptance authority.

docs/briefs/r1c-c-t-sub-fixture-worker.md

@@ -14,23 +14,23 @@
 
 PR #703 landed type-alias `where` lowering with `test_db11_type_alias_where_*` integration tests as the behavioral receipt. The `.dag` TestClaim wrapper just needs to author against that landed feature with the appropriate predicate.
 
-The `[ext]` tag in ROADMAP suggests a new predicate may be needed, but the simplest predicate (`Compiles` on a fixture program that exercises type-alias `where` lowering) is DB-15 schema and dispatchable Day-1. **Verify at brief authoring** which predicate the gate evaluates.
+The `[ext]` tag in ROADMAP originally allowed a new predicate. **`Compiles` alone is insufficient** for this gate name: it does not assert `Declaration.refinement` survives lowering. The landed receipt uses **`DeclarationHasRefinement("…")`** on the same witness program as `test_db11_type_alias_where_survives_parse_and_lower` (plus `test_runner` / M1.5 harness wiring).
 
 ## Single deliverable
 
-Author `sub_type_alias_where_lowers` TestClaim in `r1_gates.dag` (or sibling). Predicate: most likely `Compiles` on a fixture program declaring a type alias with a `where` clause that lowers correctly per PR #703 receipts. Wire runner dispatch in `test_runner.rs`.
+Author `sub_type_alias_where_lowers` TestClaim in `r1_gates.dag` (or sibling). Predicate: **`DeclarationHasRefinement`** on the alias identifier so the gate fails closed if alias-`where` lowering silently drops the refinement edge. Wire runner dispatch in `test_runner.rs`.
 
 ## Slice — single PR
 
 1. Read `test_db11_type_alias_where_*` integration tests for the canonical input/output pair.
 2. Author the `.dag` fixture program that exercises type-alias `where` lowering.
-3. Author the `sub_type_alias_where_lowers` TestClaim referencing the fixture; pick predicate (`Compiles` likely).
-4. Wire runner dispatch.
+3. Author the `sub_type_alias_where_lowers` TestClaim referencing the fixture; predicate **`DeclarationHasRefinement`** (not `Compiles` alone).
+4. Wire runner dispatch (`DeclarationHasRefinement` arm in `TestRunner::run_claim`).
 5. Verify gate evaluates `Pass`.
 
 ## Acceptance
 
-- [ ] `sub_type_alias_where_lowers` `.dag` TestClaim authored + runner dispatch + gate evaluates `Pass`.
+- [x] `sub_type_alias_where_lowers` `.dag` TestClaim authored + runner dispatch + gate evaluates `Pass`.
 - [ ] `cargo test --workspace --exclude v2-compiler-tests` clean.
 - [ ] DB-8 fixed-point converges bit-identically.
 - [ ] R1 Closure Manager lane status table updated to "R1C-C: 1/1 gates green."

src/v3/compiler/src/test_runner.rs

@@ -1424,6 +1424,9 @@ impl<'a> TestRunner<'a> {
                     "FailsWithDiagnostic" => self.eval_fails_with_diagnostic(claim, &payload),
                     "OutputEquals" => self.eval_output_equals(claim, &payload),
                     "PortHasState" => self.eval_port_has_state(claim, &payload),
+                    "DeclarationHasRefinement" => {
+                        self.eval_declaration_has_refinement(claim, &payload)
+                    }
                     "CostBounded" => self.eval_cost_bounded(claim, &payload),
                     "LensOutputEquals" => self.eval_lens_output_equals(claim, &payload),
                     "DifferentialEquals" => self.eval_differential_equals(claim, &payload),
@@ -1555,6 +1558,59 @@ impl<'a> TestRunner<'a> {
         }
     }
 
+    fn eval_declaration_has_refinement(
+        &self,
+        claim: &TestClaimValue,
+        payload: &[FieldValue],
+    ) -> ClaimResult {
+        let name = match payload {
+            [FieldValue::Literal(LiteralBits::String(name))] => name.clone(),
+            [single] => {
+                let Some(fields) = record_fields(single) else {
+                    return ClaimResult::Fail(
+                        "DeclarationHasRefinement: expected `{ declaration_name: String }` record \
+                         or a bare String payload"
+                            .to_string(),
+                    );
+                };
+                match string_field(fields, "declaration_name") {
+                    Ok(s) => s,
+                    Err(e) => return ClaimResult::Fail(e),
+                }
+            }
+            _ => {
+                return ClaimResult::Fail(format!(
+                    "DeclarationHasRefinement: expected one payload field, got {}",
+                    payload.len()
+                ));
+            }
+        };
+        let dag = match compile_to_dag(&claim.source, &claim.file_name) {
+            Ok(dag) => dag,
+            Err(CompileError::Semantic(_)) => {
+                return ClaimResult::Fail("compiled with diagnostics".to_string());
+            }
+            Err(err) => {
+                return ClaimResult::Fail(format!(
+                    "DeclarationHasRefinement: compile failed before structural check: {err:?}"
+                ));
+            }
+        };
+        let Some(decl) = dag.declaration_by_name(&name) else {
+            return ClaimResult::Fail(format!(
+                "DeclarationHasRefinement: declaration `{name}` not found in `{}`",
+                claim.file_name
+            ));
+        };
+        if decl.refinement.is_some() {
+            ClaimResult::Pass
+        } else {
+            ClaimResult::Fail(format!(
+                "DeclarationHasRefinement: declaration `{name}` has no lowered `refinement` edge"
+            ))
+        }
+    }
+
     fn eval_lens_output_equals(
         &self,
         claim: &TestClaimValue,

src/v3/compiler/tests/fixtures/r1_gates.dag

@@ -17,7 +17,7 @@
 // the rustc boundary receipt, so the named T-Sub gate has one program witness.
 //
 // merge-conflicts: union with `origin/main` — keep every `data` gate from main
-// (`sub_match_*`, `manual_*`, `testgen_structural_coverage*`) plus this file's
+// (`sub_match_*`, `sub_type_alias_where_*`, `manual_*`, `testgen_structural_coverage*`) plus this file's
 // `user_authored_lens_compiles_gate`; do not resolve conflicts by keeping only the lens gate.
 
 module std.r1_gates
@@ -28,6 +28,7 @@ import std.types { Int }
 import std.verification {
   AlgebraicLaw,
   Compiles,
+  DeclarationHasRefinement,
   DifferentialEquals,
   LensOutputEquals,
   ProgramInput,
@@ -50,6 +51,22 @@ data sub_match_over_user_sum_gate: TestSuite = {
   claims: [sub_match_over_user_sum]
 }
 
+// R1C-C / T-Sub — type-alias RHS `where` parse + lower (PR #703; DB-11:
+// `test_db11_type_alias_where_survives_parse_and_lower`). Same surface as integration receipt.
+// Predicate: `DeclarationHasRefinement` — fail-closed on silent refinement drop (not `Compiles` alone).
+data sub_type_alias_where_lowers: TestClaim = {
+  name: "sub_type_alias_where_lowers",
+  source: "type PositiveInt = Int where PositiveInt > 0\n",
+  file_name: "r1_sub_type_alias_where_lowers.v3",
+  predicate: DeclarationHasRefinement("PositiveInt"),
+  requires: []
+}
+
+data sub_type_alias_where_lowers_gate: TestSuite = {
+  name: "sub_type_alias_where_lowers_gate",
+  claims: [sub_type_alias_where_lowers]
+}
+
 // Naming stub for `DeclarationRef` resolution on `AlgebraicLaw(Associativity, lens_composition_op)`.
 // The runner resolves `lens_ref` by name from this fixture DAG, then looks up the same name in
 // the compiled `program_dag` (`TestClaim.source`). The stub body is unused at evaluation time —

src/v3/compiler/tests/fixtures/r1_gates.template.dag

@@ -17,7 +17,7 @@
 // the rustc boundary receipt, so the named T-Sub gate has one program witness.
 //
 // merge-conflicts: union with `origin/main` — keep every `data` gate from main
-// (`sub_match_*`, `manual_*`, `testgen_structural_coverage*`) plus this file's
+// (`sub_match_*`, `sub_type_alias_where_*`, `manual_*`, `testgen_structural_coverage*`) plus this file's
 // `user_authored_lens_compiles_gate`; do not resolve conflicts by keeping only the lens gate.
 
 module std.r1_gates
@@ -28,6 +28,7 @@ import std.types { Int }
 import std.verification {
   AlgebraicLaw,
   Compiles,
+  DeclarationHasRefinement,
   DifferentialEquals,
   LensOutputEquals,
   ProgramInput,
@@ -50,6 +51,22 @@ data sub_match_over_user_sum_gate: TestSuite = {
   claims: [sub_match_over_user_sum]
 }
 
+// R1C-C / T-Sub — type-alias RHS `where` parse + lower (PR #703; DB-11:
+// `test_db11_type_alias_where_survives_parse_and_lower`). Same surface as integration receipt.
+// Predicate: `DeclarationHasRefinement` — fail-closed on silent refinement drop (not `Compiles` alone).
+data sub_type_alias_where_lowers: TestClaim = {
+  name: "sub_type_alias_where_lowers",
+  source: "type PositiveInt = Int where PositiveInt > 0\n",
+  file_name: "r1_sub_type_alias_where_lowers.v3",
+  predicate: DeclarationHasRefinement("PositiveInt"),
+  requires: []
+}
+
+data sub_type_alias_where_lowers_gate: TestSuite = {
+  name: "sub_type_alias_where_lowers_gate",
+  claims: [sub_type_alias_where_lowers]
+}
+
 // Naming stub for `DeclarationRef` resolution on `AlgebraicLaw(Associativity, lens_composition_op)`.
 // The runner resolves `lens_ref` by name from this fixture DAG, then looks up the same name in
 // the compiled `program_dag` (`TestClaim.source`). The stub body is unused at evaluation time —

src/v3/compiler/tests/integration/m1_5_testgen_test.rs

@@ -313,6 +313,16 @@ fn predicate_holds(
                 expected_state,
             )
         }
+        "DeclarationHasRefinement" => {
+            let name = match payload {
+                [FieldValue::Literal(LiteralBits::String(name))] => name.clone(),
+                [FieldValue::Record(fields)] => string_field(fields, "declaration_name"),
+                _ => panic!("DeclarationHasRefinement payload should be String or record"),
+            };
+            let dag = compile_any(source, file_name);
+            dag.declaration_by_name(&name)
+                .is_some_and(|decl| decl.refinement.is_some())
+        }
         "CostBounded" => {
             let [FieldValue::Literal(LiteralBits::String(bind_name)), comparator, FieldValue::Literal(LiteralBits::Int(bound))] =
                 payload

src/v3/compiler/tests/integration/m1_5_verification_test.rs

@@ -127,6 +127,10 @@ fn bootstrap_loads_verification_authority_types() {
                 String::from("PortHasState"),
                 vec![String::from("bind_name"), String::from("state")],
             ),
+            (
+                String::from("DeclarationHasRefinement"),
+                vec![String::from("declaration_name")],
+            ),
             (
                 String::from("CostBounded"),
                 vec![
@@ -198,6 +202,7 @@ let pred_fails_kind: TestPredicate = FailsWithDiagnostic({ kind: TypeMismatch, d
 let pred_output: TestPredicate = OutputEquals("let x: Int = 1")
 let pred_port_resolved: TestPredicate = PortHasState("answer", Resolved)
 let pred_port_unresolved: TestPredicate = PortHasState("missing", Unresolved)
+let pred_decl_refine: TestPredicate = DeclarationHasRefinement("PositiveInt")
 let pred_cost_eq: TestPredicate = CostBounded("answer", Eq, 8)
 let pred_cost_above: TestPredicate = CostBounded("answer", Gt, 3)
 let pred_exec: TestPredicate = ExecuteCommand("true", empty(), 0)
@@ -219,9 +224,17 @@ let claim_fails: TestClaim = {
   requires: empty()
 }
 
+let claim_alias_refine: TestClaim = {
+  name: "alias_where_refine",
+  source: "type PositiveInt = Int where PositiveInt > 0",
+  file_name: "alias_refine.v3",
+  predicate: pred_decl_refine,
+  requires: empty()
+}
+
 let suite: TestSuite = {
   name: "verification_smoke",
-  claims: [claim_compiles, claim_fails]
+  claims: [claim_compiles, claim_fails, claim_alias_refine]
 }
 "#;
 
@@ -240,6 +253,7 @@ let suite: TestSuite = {
         "pred_output",
         "pred_port_resolved",
         "pred_port_unresolved",
+        "pred_decl_refine",
         "pred_cost_eq",
         "pred_cost_above",
         "pred_exec",
@@ -255,6 +269,10 @@ let suite: TestSuite = {
         bind_value_type_decl(&dag, "claim_fails"),
         find_named(&dag, "TestClaim")
     );
+    assert_eq!(
+        bind_value_type_decl(&dag, "claim_alias_refine"),
+        find_named(&dag, "TestClaim")
+    );
     assert_eq!(
         bind_value_type_decl(&dag, "suite"),
         find_named(&dag, "TestSuite")

src/v3/compiler/tests/integration/parse_corpus_manifest.txt

@@ -39,5 +39,5 @@ src/v3/std/substrate.dag	53	114503	acfa5e48ad6d553e
 src/v3/std/substrate_minimal.dag	8	5372	feeb314c735f4672
 src/v3/std/termination.dag	18	36478	d010232f0373dc99
 src/v3/std/tokenize.dag	8	38819	2e158a74f33c18cc
-src/v3/std/verification.dag	19	41879	0f4b7deb0f9940b9
+src/v3/std/verification.dag	19	42851	c8f5143ac92e80c1
 src/v3/std/workflows.dag	4	3135	bb6f9b042a02e8d6

src/v3/compiler/tests/integration/test_runner_test.rs

@@ -732,3 +732,15 @@ fn test_runner_runs_sub_match_over_user_sum_gate() {
 
     assert_all_pass(&results);
 }
+
+#[test]
+fn test_runner_runs_sub_type_alias_where_lowers_gate() {
+    let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
+    let gate = manifest_dir.join("tests/fixtures/r1_gates.dag");
+    let source =
+        std::fs::read_to_string(&gate).unwrap_or_else(|err| panic!("read {gate:?}: {err}"));
+    let dag = compile_clean(&source, "src/v3/compiler/tests/fixtures/r1_gates.dag");
+    let results = TestRunner::new(&dag).run_suite("sub_type_alias_where_lowers_gate");
+
+    assert_all_pass(&results);
+}

src/v3/std/verification.dag

@@ -87,6 +87,11 @@ type TestPredicate
       bind_name: String
       state: PortStateExpectation
     }
+  // Structural lowering receipt: named declaration must carry `refinement` after
+  // `compile_to_dag` on the claim program (DB-11 alias-RHS `where` survival).
+  | DeclarationHasRefinement {
+      declaration_name: String
+    }
   | CostBounded {
       bind_name: String
       comparator: ComparisonOp