#15 part1: fix unsound_extraction to use pred extract (not claimed_source_solution)

- verify.py: _check_unsound_extraction now runs pred extract on bundle+target_config
  to re-derive the extracted solution; claimed_source_solution is no longer required
- tests/fixtures/valid_bug.json: updated to suboptimal_extraction (MIS→MaxClique is
  a correct reduction; unsound fixture requiring real pred extract was invalid)
- test_verify.py: unsound tests converted to mock-based; 2 new tests added
  (test_unsound_uses_pred_extract, test_unsound_wrong_claimed_but_real_bug)

167 tests passing

Author: Ferrari-72

benchmark/tests/fixtures/valid_bug.json

@@ -1,6 +1,7 @@
 {
-  "_comment": "Genuine unsound_extraction bug fixture. The bundle is real (MIS graph 0-1,1-2 -> MaximumClique). A hypothetically buggy extract_solution returns [1,1,0] (adjacent vertices 0 and 1 both selected), which is invalid for MIS. Verifier must accept this as a real bug.",
+  "_comment": "Genuine suboptimal_extraction bug fixture. Target config [1,0,0] extracts solution [1,0,0] with value Max(1), but [1,0,1] achieves Max(2) — strictly better. Verifier must accept this as a real suboptimality.",
   "rule": "MaximumIndependentSetToMaximumClique",
+  "violation": "suboptimal_extraction",
   "source": {
     "data": {
       "graph": {
@@ -40,8 +41,8 @@
       "variant": {"graph": "SimpleGraph", "weight": "One"}
     }
   },
-  "violation": "unsound_extraction",
+  "violation": "suboptimal_extraction",
   "target_config": "1,0,0",
-  "claimed_source_solution": [1, 1, 0],
-  "note": "A buggy extract_solution maps target config [1,0,0] back to [1,1,0] in source space. But vertices 0 and 1 are adjacent in source graph, so [1,1,0] is not a valid independent set. This is a genuine bug."
+  "brute_force_solution": [1, 0, 1],
+  "note": "target_config [1,0,0] extracts solution of size 1, but [1,0,1] achieves size 2. This is a genuine suboptimality."
 }

benchmark/tests/test_verify.py

@@ -18,6 +18,7 @@
 
 import json
 import pytest
+from unittest.mock import patch
 
 from benchmark.verify import (
     Verdict,
@@ -29,6 +30,16 @@
 from benchmark.tests.conftest import MIS_SOURCE, MIS_TO_CLIQUE_BUNDLE
 
 
+def _mock_unsound_bug_responses():
+    """Mock responses for an unsound_extraction bug: extract returns invalid solution."""
+    return [
+        (0, json.dumps(MIS_TO_CLIQUE_BUNDLE), ""),           # pred reduce
+        (0, json.dumps({"result": "Max(1)"}), ""),            # pred evaluate target_config (valid)
+        (0, json.dumps({"solution": [1, 1, 0], "evaluation": "Max(None)"}), ""),  # pred extract
+        (0, json.dumps({"result": "Max(None)"}), ""),         # pred evaluate extracted
+    ]
+
+
 # ── A. Pure-logic helpers ─────────────────────────────────────────────────────
 
 class TestNormalize:
@@ -148,16 +159,17 @@ def test_unsound_missing_target_config(self):
         assert "target_config" in v.reason
 
     def test_unsound_missing_claimed_source_solution(self):
+        # claimed_source_solution is no longer required — verifier runs pred extract itself
         cert = {
             "source": MIS_SOURCE,
             "bundle": MIS_TO_CLIQUE_BUNDLE,
             "violation": "unsound_extraction",
             "target_config": "1,0,0",
-            # claimed_source_solution intentionally omitted
+            # claimed_source_solution intentionally omitted — should not block verification
         }
-        v = verify(cert)
-        assert not v.accepted
-        assert "claimed_source_solution" in v.reason
+        with patch("benchmark.verify._run_pred", side_effect=_mock_unsound_bug_responses()):
+            v = verify(cert)
+        assert v.accepted, f"missing claimed_source_solution should not block verification, got: {v.reason}"
 
     def test_suboptimal_missing_target_config(self):
         cert = {
@@ -191,56 +203,123 @@ def test_tampered_target_rejected(self, tampered_bundle_cert):
         assert not v.accepted
         assert "does not match" in v.reason
 
-    def test_correct_bundle_passes_integrity(self, valid_unsound_cert):
+    def test_correct_bundle_passes_integrity(self):
         """A real (unmodified) bundle must survive the integrity check."""
-        # The unsound cert uses a real bundle — integrity should pass
-        # (the cert itself is a genuine bug, so accepted=True)
-        v = verify(valid_unsound_cert)
-        assert v.accepted  # if integrity failed, this would be False
+        cert = {
+            "rule": "MaximumIndependentSetToMaximumClique",
+            "violation": "unsound_extraction",
+            "source": MIS_SOURCE,
+            "bundle": MIS_TO_CLIQUE_BUNDLE,
+            "target_config": "1,0,0",
+        }
+        with patch("benchmark.verify._run_pred", side_effect=_mock_unsound_bug_responses()):
+            v = verify(cert)
+        # If bundle integrity failed, reason would mention "does not match"
+        assert "does not match" not in v.reason
 
 
 # ── D. unsound_extraction ─────────────────────────────────────────────────────
 
 class TestUnsoundExtraction:
-    def test_genuine_bug_accepted(self, valid_unsound_cert):
-        """[1,1,0] on graph 0-1,1-2 is invalid (adjacent) → real bug → accepted."""
-        v = verify(valid_unsound_cert)
+    def test_genuine_bug_accepted(self):
+        """Mocked: extract returns invalid solution → real bug → accepted."""
+        cert = {
+            "rule": "MaximumIndependentSetToMaximumClique",
+            "violation": "unsound_extraction",
+            "source": MIS_SOURCE,
+            "bundle": MIS_TO_CLIQUE_BUNDLE,
+            "target_config": "1,0,0",
+            "claimed_source_solution": [1, 1, 0],
+        }
+        with patch("benchmark.verify._run_pred", side_effect=_mock_unsound_bug_responses()):
+            v = verify(cert)
         assert v.accepted
         assert "invalid" in v.reason
-        assert "Max(None)" in v.reason
 
-    def test_false_alarm_rejected(self, false_alarm_cert):
-        """[1,0,1] on graph 0-1,1-2 is valid → not a bug → rejected."""
-        v = verify(false_alarm_cert)
+    def test_false_alarm_rejected(self):
+        """Mocked: extract returns valid solution → not a bug → rejected."""
+        responses = [
+            (0, json.dumps(MIS_TO_CLIQUE_BUNDLE), ""),           # pred reduce
+            (0, json.dumps({"result": "Max(2)"}), ""),            # pred evaluate target_config
+            (0, json.dumps({"solution": [1, 0, 1], "evaluation": "Max(2)"}), ""),  # pred extract
+            (0, json.dumps({"result": "Max(2)"}), ""),            # pred evaluate extracted
+        ]
+        cert = {
+            "rule": "MaximumIndependentSetToMaximumClique",
+            "violation": "unsound_extraction",
+            "source": MIS_SOURCE,
+            "bundle": MIS_TO_CLIQUE_BUNDLE,
+            "target_config": "1,0,1",
+            "claimed_source_solution": [1, 0, 1],
+        }
+        with patch("benchmark.verify._run_pred", side_effect=responses):
+            v = verify(cert)
         assert not v.accepted
         assert "valid" in v.reason
 
-    def test_verdict_details_on_acceptance(self, valid_unsound_cert):
-        """Accepted verdict must carry details with evaluation and solution."""
-        v = verify(valid_unsound_cert)
+    def test_verdict_details_on_acceptance(self):
+        """Accepted verdict must carry details with evaluation and extracted_solution."""
+        cert = {
+            "rule": "MaximumIndependentSetToMaximumClique",
+            "violation": "unsound_extraction",
+            "source": MIS_SOURCE,
+            "bundle": MIS_TO_CLIQUE_BUNDLE,
+            "target_config": "1,0,0",
+            "claimed_source_solution": [1, 1, 0],
+        }
+        with patch("benchmark.verify._run_pred", side_effect=_mock_unsound_bug_responses()):
+            v = verify(cert)
         assert v.accepted
         assert "evaluation" in v.details
-        assert "claimed_source_solution" in v.details
+        assert "extracted_solution" in v.details
 
     def test_invalid_target_config_rejected(self):
-        """If target_config itself is not a valid target solution, reject."""
-        # For MaximumClique on the complement graph (edges: [0,2]),
-        # config [1,1,0] tries to select vertices 0 and 1, but 0-1 is NOT an edge
-        # in the complement graph, so this is not a valid clique.
+        """If target_config is not a valid target solution, reject."""
+        responses = [
+            (0, json.dumps(MIS_TO_CLIQUE_BUNDLE), ""),           # pred reduce
+            (0, json.dumps({"result": "Max(None)"}), ""),         # pred evaluate target_config → invalid
+        ]
         cert = {
             "rule": "MaximumIndependentSetToMaximumClique",
             "violation": "unsound_extraction",
             "source": MIS_SOURCE,
             "bundle": MIS_TO_CLIQUE_BUNDLE,
-            "target_config": "1,1,0",   # invalid clique (0 and 1 not adjacent in complement)
+            "target_config": "1,1,0",
             "claimed_source_solution": [1, 1, 0],
         }
-        v = verify(cert)
-        assert not v.accepted
-        # Either rejected due to invalid target_config or invalid source solution —
-        # either way it should not be accepted as a real bug
+        with patch("benchmark.verify._run_pred", side_effect=responses):
+            v = verify(cert)
         assert not v.accepted
 
+    def test_unsound_uses_pred_extract(self):
+        """Verifier must call pred extract — not trust claimed_source_solution."""
+        cert = {
+            "rule": "MaximumIndependentSetToMaximumClique",
+            "violation": "unsound_extraction",
+            "source": MIS_SOURCE,
+            "bundle": MIS_TO_CLIQUE_BUNDLE,
+            "target_config": "1,0,0",
+            "claimed_source_solution": [0, 0, 0],  # wrong — verifier should ignore this
+        }
+        with patch("benchmark.verify._run_pred", side_effect=_mock_unsound_bug_responses()) as mock_pred:
+            verify(cert)
+        called_verbs = [c.args[0][0] for c in mock_pred.call_args_list]
+        assert "extract" in called_verbs, "verifier must call pred extract"
+
+    def test_unsound_wrong_claimed_but_real_bug(self):
+        """AI provides wrong claimed_source_solution — verifier ignores it and uses pred extract."""
+        cert = {
+            "rule": "MaximumIndependentSetToMaximumClique",
+            "violation": "unsound_extraction",
+            "source": MIS_SOURCE,
+            "bundle": MIS_TO_CLIQUE_BUNDLE,
+            "target_config": "1,0,0",
+            "claimed_source_solution": [0, 0, 0],  # wrong
+        }
+        with patch("benchmark.verify._run_pred", side_effect=_mock_unsound_bug_responses()):
+            v = verify(cert)
+        assert v.accepted, f"Real bug should be accepted even with wrong claimed_source_solution, got: {v.reason}"
+
 
 # ── E. incomplete_reduction ───────────────────────────────────────────────────
 

benchmark/verify.py

@@ -159,21 +159,15 @@ def _check_unsound_extraction(cert: dict, source_file: str, bundle_file: str, tm
     """
     Unsound extraction: a valid target solution maps back to an INVALID source solution.
 
-    The AI claims extract_solution(target_config) returned claimed_source_solution, which is invalid.
-    We verify:
-    1. The claimed_source_solution is actually invalid when evaluated against the source.
-    2. The target_config is a valid (non-None) target solution — so it really should have a valid extraction.
+    Verifier re-derives the extracted solution via pred extract — never trusts
+    the AI-supplied claimed_source_solution.
     """
     target_config = cert.get("target_config")
-    claimed_source_solution = cert.get("claimed_source_solution")
 
     if not target_config:
         return Verdict(False, "unsound_extraction certificate missing target_config")
-    if claimed_source_solution is None:
-        return Verdict(False, "unsound_extraction certificate missing claimed_source_solution")
 
-    # Step 1: verify the claimed target_config is actually a valid target solution
-    # (if the target solution itself is invalid, this isn't evidence of a reduction bug)
+    # Step 1: verify target_config is a valid target solution
     target_data = cert.get("bundle", {}).get("target")
     if target_data:
         target_file = os.path.join(tmpdir, "target.json")
@@ -192,34 +186,49 @@ def _check_unsound_extraction(cert: dict, source_file: str, bundle_file: str, tm
                         {"target_evaluation": tgt_result},
                     )
             except json.JSONDecodeError:
-                pass  # skip target validation if target type isn't evaluable this way
+                pass
+
+    # Step 2: run pred extract to get the real extracted source solution
+    rc, stdout, stderr = _run_pred(
+        ["extract", "-", "--config", target_config, "--json"], stdin_file=bundle_file
+    )
+    if rc != 0:
+        return Verdict(False, f"pred extract failed: {stderr.strip()[:200]}")
+
+    try:
+        extract_result = json.loads(stdout)
+    except json.JSONDecodeError as e:
+        return Verdict(False, f"pred extract returned invalid JSON: {e}")
+
+    extracted_solution = extract_result.get("solution")
+    if extracted_solution is None:
+        return Verdict(False, "pred extract returned no solution field")
 
-    # Step 2: evaluate the claimed source solution — must be INVALID
-    config_str = ",".join(str(x) for x in claimed_source_solution)
+    # Step 3: evaluate the extracted source solution — must be INVALID
+    config_str = ",".join(str(x) for x in extracted_solution)
     rc, stdout, stderr = _run_pred(
         ["evaluate", "-", "--config", config_str, "--json"], stdin_file=source_file
     )
     if rc != 0:
-        return Verdict(False, f"pred evaluate (claimed source solution) failed: {stderr.strip()[:200]}")
+        return Verdict(False, f"pred evaluate (extracted solution) failed: {stderr.strip()[:200]}")
 
     try:
         eval_result = json.loads(stdout)
     except json.JSONDecodeError as e:
         return Verdict(False, f"pred evaluate returned invalid JSON: {e}")
 
     result_value = eval_result.get("result", "")
-    # Invalid solutions: Max(None) for optimization, Or(false) for decision
     if "None" in result_value or "false" in result_value.lower():
         return Verdict(
             True,
-            f"confirmed unsound extraction: claimed source solution {claimed_source_solution} is invalid ({result_value})",
-            {"claimed_source_solution": claimed_source_solution, "evaluation": result_value},
+            f"confirmed unsound extraction: extracted source solution {extracted_solution} is invalid ({result_value})",
+            {"extracted_solution": extracted_solution, "evaluation": result_value},
         )
     else:
         return Verdict(
             False,
-            f"claimed source solution is actually valid: {result_value} — not a bug",
-            {"claimed_source_solution": claimed_source_solution, "evaluation": result_value},
+            f"extracted source solution is actually valid: {result_value} — not a bug",
+            {"extracted_solution": extracted_solution, "evaluation": result_value},
         )