MockBackedInvariant wiring

src/v3/compiler/src/test_runner.rs

@@ -154,8 +154,9 @@ impl<'a> TestRunner<'a> {
                     "CostBounded" => self.eval_cost_bounded(claim, &payload),
                     "LensOutputEquals" => self.eval_lens_output_equals(claim, &payload),
                     "AlgebraicLaw" => self.eval_algebraic_law(claim, &payload),
-                    _ => ClaimResult::NotYetImplemented(format!(
-                        "TestPredicate `{label}` is not implemented in the Rust test runner"
+                    "MockBackedInvariant" => self.eval_mock_backed_invariant(claim, &payload),
+                    other => ClaimResult::NotYetImplemented(format!(
+                        "TestPredicate::{other} is not wired in the Rust runner yet"
                     )),
                 },
                 None => ClaimResult::Fail("predicate is not a structural variant".to_string()),
@@ -274,15 +275,15 @@ impl<'a> TestRunner<'a> {
                 payload.len()
             ));
         };
-        let lens_id = match self.resolve_declaration_ref_edge(lens_fv, "lens_ref") {
+        let lens_id = match self.resolve_declaration_ref_id(lens_fv, "lens_ref") {
             Ok(id) => id,
             Err(msg) => return ClaimResult::Fail(msg),
         };
-        let input_id = match self.resolve_declaration_ref_edge(input_fv, "input_ref") {
+        let input_id = match self.resolve_declaration_ref_id(input_fv, "input_ref") {
             Ok(id) => id,
             Err(msg) => return ClaimResult::Fail(msg),
         };
-        let expected_id = match self.resolve_declaration_ref_edge(expected_fv, "expected_ref") {
+        let expected_id = match self.resolve_declaration_ref_id(expected_fv, "expected_ref") {
             Ok(id) => id,
             Err(msg) => return ClaimResult::Fail(msg),
         };
@@ -328,7 +329,7 @@ impl<'a> TestRunner<'a> {
         ))
     }
 
-    fn resolve_declaration_ref_edge(
+    fn resolve_declaration_ref_id(
         &self,
         value: &FieldValue,
         field_label: &str,
@@ -369,7 +370,7 @@ impl<'a> TestRunner<'a> {
         };
         if law_label != "Associativity" {
             return ClaimResult::NotYetImplemented(format!(
-                "AlgebraicLaw: law `{law_label}` is not implemented in the Rust test runner yet"
+                "AlgebraicLaw::{law_label} is not wired in the Rust runner yet"
             ));
         }
         if !law_payload.is_empty() {
@@ -431,6 +432,51 @@ impl<'a> TestRunner<'a> {
         }
     }
 
+    fn eval_mock_backed_invariant(
+        &self,
+        _claim: &TestClaimValue,
+        payload: &[FieldValue],
+    ) -> ClaimResult {
+        let [subject, invariant] = payload else {
+            return ClaimResult::Fail(
+                "MockBackedInvariant payload should be (subject: DeclarationRef, invariant: DeclarationRef)"
+                    .to_string(),
+            );
+        };
+        let subject = match self.resolve_mock_declaration_ref_edge(subject, "subject") {
+            Ok(name) => name,
+            Err(reason) => return ClaimResult::Fail(reason),
+        };
+        let invariant = match self.resolve_mock_declaration_ref_edge(invariant, "invariant") {
+            Ok(name) => name,
+            Err(reason) => return ClaimResult::Fail(reason),
+        };
+        ClaimResult::NotYetImplemented(format!(
+            "MockBackedInvariant mock simulation is not wired in the Rust runner yet for subject `{subject}` and invariant `{invariant}`"
+        ))
+    }
+
+    fn resolve_mock_declaration_ref_edge(
+        &self,
+        value: &FieldValue,
+        label: &str,
+    ) -> Result<String, String> {
+        match value {
+            FieldValue::Reference(id) => Ok(self
+                .dag
+                .declaration(*id)
+                .name
+                .clone()
+                .unwrap_or_else(|| format!("Declaration#{}", id.raw()))),
+            FieldValue::Record(fields) if fields.is_empty() => Err(format!(
+                "MockBackedInvariant `{label}` must be a DeclarationRef edge, got empty record literal"
+            )),
+            other => Err(format!(
+                "MockBackedInvariant `{label}` must be a DeclarationRef edge, got {other:?}"
+            )),
+        }
+    }
+
     fn diagnostic_matches(&self, actual_dag: &Dag, reference: &FieldValue) -> Result<bool, String> {
         let reference = self.diagnostic_reference(reference)?;
         Ok(actual_dag

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

@@ -0,0 +1,29 @@
+// Minimal MockBackedInvariant gate fixture.
+// Lives under tests/fixtures/ -- NOT src/v3/std/ -- not auto-staged into bootstrap.
+//
+// **requires: [] is intentional.** A real MockBackedInvariant claim puts its mock
+// transport on TestClaim.requires. The runner's requires gate (run_claim) currently
+// fails-closed on non-empty requires, so this fixture reaches the typed
+// MockBackedInvariant NYI path until T-TestGen wires real mock simulation.
+
+module std.r1_mock_backed_invariant_gate
+
+import std.verification { TestClaim, TestSuite }
+
+data mock_subject_ref: Int = 0
+data mock_invariant_ref: Int = 0
+
+data mock_backed_invariant_gate: TestClaim = {
+  name: "testgen_mock_backed_integration_safe",
+  source: "let _: Int = 0\n",
+  file_name: "mock_backed_placeholder.v3",
+  // Struct-variant field names are schema metadata today; the surface parser
+  // accepts positional payload syntax for authored values.
+  predicate: MockBackedInvariant(mock_subject_ref, mock_invariant_ref),
+  requires: []
+}
+
+data mock_backed_invariant_suite: TestSuite = {
+  name: "mock_backed_invariant_suite",
+  claims: [mock_backed_invariant_gate]
+}

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

@@ -22,6 +22,8 @@ use v3_compiler::dag::{Dag, FieldValue, LiteralBits, ValueBody};
 use v3_compiler::CompileError;
 
 const R1_GATES_SOURCE: &str = include_str!("../fixtures/r1_gates.dag");
+const R1_MOCK_BACKED_INVARIANT_GATE_SOURCE: &str =
+    include_str!("../fixtures/r1_mock_backed_invariant_gate.dag");
 const R1_LENS_OUTPUT_EQUALS_GATE_SOURCE: &str =
     include_str!("../fixtures/r1_lens_output_equals_gate.dag");
 const ON_DISK_LENS: &str = include_str!("../../../lenses/named_function_count.dag");
@@ -73,6 +75,15 @@ fn r1_gates_fixture_compiles_against_bootstrap_context() {
     );
 }
 
+#[test]
+fn r1_mock_backed_invariant_gate_fixture_compiles_against_bootstrap_context() {
+    assert_compile_clean(
+        R1_MOCK_BACKED_INVARIANT_GATE_SOURCE,
+        "src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag",
+        "gate fixture `r1_mock_backed_invariant_gate.dag`",
+    );
+}
+
 #[test]
 fn r1_lens_output_equals_gate_fixture_compiles_against_bootstrap_context() {
     assert_compile_clean(

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

@@ -7,6 +7,11 @@ use v3_compiler::test_runner::TestClaimValue;
 use v3_compiler::test_runner::{ClaimResult, TestRunner};
 use v3_compiler::{compile_to_dag, CompileError};
 
+const MOCK_BACKED_INVARIANT_FIXTURE: &str =
+    include_str!("../fixtures/r1_mock_backed_invariant_gate.dag");
+const R1_LENS_OUTPUT_EQUALS_FIXTURE: &str =
+    include_str!("../fixtures/r1_lens_output_equals_gate.dag");
+
 fn compile_clean(source: &str, file: &str) -> v3_compiler::dag::Dag {
     match compile_to_dag(source, file) {
         Ok(dag) => dag,
@@ -281,12 +286,12 @@ data suite: TestSuite = {
 fn test_runner_marks_non_day_one_predicates_not_yet_implemented() {
     let source = r#"
 data claim_nyi: TestClaim = {
-  name: "mock backed invariant",
+  name: "behavioral observation",
   source: "let x: Int = 0",
   file_name: "runner_nyi.v3",
   // Struct-variant field names are schema metadata today; the surface parser
   // accepts positional payload syntax for authored values.
-  predicate: MockBackedInvariant(Int, Bool),
+  predicate: BehavioralObservation(Int, Int, Int),
   requires: []
 }
 
@@ -301,9 +306,72 @@ data suite: TestSuite = {
     assert_eq!(results.len(), 1);
     assert!(matches!(
         &results[0].result,
-        ClaimResult::NotYetImplemented(msg)
-            if msg.contains("MockBackedInvariant")
-                && msg.contains("not implemented in the Rust test runner")
+        ClaimResult::NotYetImplemented(reason)
+            if reason.contains("BehavioralObservation")
+    ));
+}
+
+#[test]
+fn mock_backed_invariant_predicate_accepts_declaration_ref_like_lens_output_equals() {
+    let source = r#"
+data claim: TestClaim = {
+  name: "c",
+  source: "let _: Int = 0",
+  file_name: "f.v3",
+  predicate: MockBackedInvariant(Int, Int),
+  requires: []
+}
+"#;
+    compile_clean(source, "mock_backed_invariant_harness.v3");
+}
+
+#[test]
+fn test_runner_dispatches_mock_backed_invariant_claim() {
+    let dag = compile_clean(
+        MOCK_BACKED_INVARIANT_FIXTURE,
+        "src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag",
+    );
+    let results = TestRunner::new(&dag).run_suite("mock_backed_invariant_suite");
+
+    assert_eq!(results.len(), 1);
+    assert!(matches!(
+        &results[0].result,
+        ClaimResult::NotYetImplemented(reason)
+            if reason.contains("mock simulation is not wired")
+                && reason.contains("mock_subject_ref")
+                && reason.contains("mock_invariant_ref")
+    ));
+}
+
+#[test]
+fn test_runner_mock_backed_invariant_does_not_fabricate_pass_for_clean_source() {
+    let source = r#"
+data subject_ref: Int = 0
+data invariant_ref: Int = 0
+
+data claim: TestClaim = {
+  name: "mock backed clean source",
+  source: "let x: Int = 1",
+  file_name: "clean_mock_subject.v3",
+  predicate: MockBackedInvariant(subject_ref, invariant_ref),
+  requires: []
+}
+
+data suite: TestSuite = {
+  name: "clean_mock_subject_suite",
+  claims: [claim]
+}
+"#;
+    let dag = compile_clean(source, "clean_mock_subject_harness.v3");
+    let results = TestRunner::new(&dag).run_suite("suite");
+
+    assert_eq!(results.len(), 1);
+    assert!(matches!(
+        &results[0].result,
+        ClaimResult::NotYetImplemented(reason)
+            if reason.contains("mock simulation is not wired")
+                && reason.contains("subject_ref")
+                && reason.contains("invariant_ref")
     ));
 }
 
@@ -326,9 +394,6 @@ data suite: TestSuite = {
     compile_clean(source, "lens_output_equals_int_harness.v3");
 }
 
-const R1_LENS_OUTPUT_EQUALS_FIXTURE: &str =
-    include_str!("../fixtures/r1_lens_output_equals_gate.dag");
-
 #[test]
 fn test_runner_dispatches_r1_gates_lens_output_equals_claim() {
     let dag = compile_clean(
@@ -376,9 +441,8 @@ data suite: TestSuite = {
     assert_eq!(results.len(), 1);
     assert!(matches!(
         &results[0].result,
-        ClaimResult::NotYetImplemented(msg)
-            if msg.contains("Commutativity")
-                && msg.contains("not implemented in the Rust test runner")
+        ClaimResult::NotYetImplemented(reason)
+            if reason.contains("AlgebraicLaw::Commutativity")
     ));
 }