refactor(proof_chain): read the #529 MP oracle fixture, not a re-transcription

test_proof_chain_rules.py carried a 24-case inline copy of the same modus_ponens
contract oracle #529 committed as tests/fixtures/proof_chain/modus_ponens_cases.json.
Load the fixture instead — it is now the single source of truth. Its expected.reason
is already the ADR-0205 closed set (closed_reasons == MP_REASONS), so this is a pure
de-dup: the loaded cases were verified byte-for-byte against the prior inline table
(24/24, 0 diffs). The pooling tests (DISAGREE-007/010/003) now pull premises from the
oracle by id too, so no case is re-transcribed anywhere. Added a contract guard
(24 cases; reasons subset of MP_REASONS; closed_reasons == MP_REASONS); dropped the
now-unused closed-reason imports.

tests/test_proof_chain_rules.py

@@ -1,66 +1,100 @@
 """ADR-0205 — modus_ponens + disagreement rule (phase 2.3).
 
-The 24 adversarial corpus cases (GPT-5.5's independent oracle) transcribed for a
+The 24 adversarial cases are loaded from the committed contract oracle
-committed, reproducible cross-check against the real rule: 6 valid / 8 invalid /
+(``tests/fixtures/proof_chain/modus_ponens_cases.json``, added in #529) —
-10 disagreement. The disagreement cases are the wrong=0 guard — 007/010 in
+GPT-5.5's independent oracle, authored against the ADR-0202/0205 contract and
-particular pin the pooling semantics: pool ALL admissible MP derivations and
+cross-checked 24/24 against the real rule. This module is the reproducible
-require a unique key. A filter-to-declared-conclusion-first rule would admit them
+cross-check: it runs ``evaluate_modus_ponens`` against the oracle's expected
-(admit-by-assertion); pool-first refuses. That test failing under filter-first is
+``(outcome, reason)`` per case. There is no second transcription of the cases
-the proof the soundness mechanism is load-bearing.
+here — the fixture is the single source of truth.
+
+The disagreement cases are the wrong=0 guard — DISAGREE-007/010 in particular
+pin the pooling semantics: pool ALL admissible MP derivations and require a
+unique key. A filter-to-declared-conclusion-first rule would admit them
+(admit-by-assertion); pool-first refuses. Those tests failing under filter-first
+is the proof the soundness mechanism is load-bearing.
 """
 
 from __future__ import annotations
 
+import json
+from pathlib import Path
+
 import pytest
 
 from generate.proof_chain import (
     CONCLUSION_DISAGREEMENT,
-    CONCLUSION_MISMATCH,
-    MISSING_IMPLICATION,
     MP_REASONS,
     Proof,
     ProofNode,
-    UNESTABLISHED_ANTECEDENT,
     UNIQUE_CANONICAL_CONCLUSION,
     MPOutcome,
     evaluate_modus_ponens,
     evaluate_proof_conclusion,
 )
 
-# (id, premises, conclusion, expected_outcome, expected_reason)  — reasons are the
+_CORPUS_PATH = (
-# CLOSED set; the corpus's finer labels collapse onto them (ADR-0205 §reason-set).
+    Path(__file__).resolve().parent
-CASES = [
+    / "fixtures"
-    # --- valid (admit) ---
+    / "proof_chain"
-    ("VALID-001", ("P", "P -> Q"), "Q", "admit", UNIQUE_CANONICAL_CONCLUSION),
+    / "modus_ponens_cases.json"
-    ("VALID-002", ("P_rains", "P_rains -> Q_ground_wet"), "Q_ground_wet", "admit", UNIQUE_CANONICAL_CONCLUSION),
+)
-    ("VALID-003", ("P and R", "(P and R) -> Q"), "Q", "admit", UNIQUE_CANONICAL_CONCLUSION),
-    ("VALID-004", ("P_switch_on", "P_switch_on -> (Q_lamp_lit or R_alarm_on)"), "Q_lamp_lit or R_alarm_on", "admit", UNIQUE_CANONICAL_CONCLUSION),
-    ("VALID-005", ("P", "P -> (Q -> R)"), "Q -> R", "admit", UNIQUE_CANONICAL_CONCLUSION),
-    ("VALID-006", ("(P or Q) and not R", "((P or Q) and not R) -> S"), "S", "admit", UNIQUE_CANONICAL_CONCLUSION),
-    # --- invalid (refuse, typed) ---
-    ("INVALID-001", ("P", "P -> Q"), "R", "refuse", CONCLUSION_MISMATCH),
-    ("INVALID-002", ("P",), "Q", "refuse", MISSING_IMPLICATION),
-    ("INVALID-003", ("Q", "P -> Q"), "P", "refuse", UNESTABLISHED_ANTECEDENT),  # corpus: affirming_consequent
-    ("INVALID-004", ("R", "P -> Q"), "Q", "refuse", UNESTABLISHED_ANTECEDENT),  # corpus: antecedent_mismatch
-    ("INVALID-005", ("P", "Q -> P"), "Q", "refuse", UNESTABLISHED_ANTECEDENT),  # corpus: implication_direction_mismatch
-    ("INVALID-006", ("P", "(P or R) -> Q"), "Q", "refuse", UNESTABLISHED_ANTECEDENT),  # corpus: antecedent_mismatch
-    ("INVALID-007", ("P", "P -> (Q or R)"), "Q", "refuse", CONCLUSION_MISMATCH),
-    ("INVALID-008", ("P -> Q",), "Q", "refuse", UNESTABLISHED_ANTECEDENT),  # corpus: missing_antecedent
-    # --- disagreement (admit: collapse to one key; refuse: distinct keys) ---
-    ("DISAGREE-001", ("A", "A -> C", "B", "B -> C"), "C", "admit", UNIQUE_CANONICAL_CONCLUSION),
-    ("DISAGREE-002", ("A", "A -> (P and Q)", "B", "B -> (Q and P)"), "P and Q", "admit", UNIQUE_CANONICAL_CONCLUSION),
-    ("DISAGREE-003", ("A", "A -> (Q -> R)", "B", "B -> (not Q or R)"), "Q -> R", "admit", UNIQUE_CANONICAL_CONCLUSION),
-    ("DISAGREE-004", ("A", "A -> Q", "B", "B -> (Q and (R or not R))"), "Q", "admit", UNIQUE_CANONICAL_CONCLUSION),
-    ("DISAGREE-005", ("A", "A -> (P and Q)", "B", "B -> (P or Q)"), "P and Q", "refuse", CONCLUSION_DISAGREEMENT),
-    ("DISAGREE-006", ("A", "A -> Q_ground_wet", "B", "B -> Q_ground_damp"), "Q_ground_wet", "refuse", CONCLUSION_DISAGREEMENT),
-    ("DISAGREE-007", ("A", "A -> (R or not R)", "B", "B -> Q"), "Q", "refuse", CONCLUSION_DISAGREEMENT),
-    ("DISAGREE-008", ("A", "A -> Q", "B", "B -> not Q"), "Q", "refuse", CONCLUSION_DISAGREEMENT),
-    ("DISAGREE-009", ("A", "A -> (P -> Q)", "B", "B -> (Q -> P)"), "P -> Q", "refuse", CONCLUSION_DISAGREEMENT),
-    ("DISAGREE-010", ("A", "A -> Q", "B", "B -> (Q and R)"), "Q", "refuse", CONCLUSION_DISAGREEMENT),
-]
 
 
-@pytest.mark.parametrize("cid,premises,conclusion,outcome,reason", CASES, ids=[c[0] for c in CASES])
+def _load_corpus() -> tuple[dict, list[tuple]]:
+    """Load the committed MP oracle into parametrize tuples.
+
+    Each tuple is ``(id, premises, conclusion, expected_outcome, expected_reason)``.
+    The corpus's ``expected.reason`` is already the ADR-0205 closed reason set
+    (see its ``closed_reasons``), so no label mapping is needed.
+    """
+    data = json.loads(_CORPUS_PATH.read_text(encoding="utf-8"))
+    cases: list[tuple] = []
+    for case in data["cases"]:
+        sc = case["semantic_content"]
+        ex = case["expected"]
+        cases.append(
+            (
+                case["id"],
+                tuple(sc["premises"]),
+                sc["conclusion"],
+                ex["outcome"],
+                ex["reason"],
+            )
+        )
+    return data, cases
+
+
+_CORPUS, CASES = _load_corpus()
+
+
+def _inputs_for(case_id: str) -> tuple[tuple[str, ...], str]:
+    """Return ``(premises, conclusion)`` for a corpus case id.
+
+    Lets the pooling tests below reference oracle cases by id instead of
+    re-transcribing their premises — the fixture stays the only source.
+    """
+    for case in _CORPUS["cases"]:
+        if case["id"] == case_id:
+            sc = case["semantic_content"]
+            return tuple(sc["premises"]), sc["conclusion"]
+    raise KeyError(case_id)
+
+
+def test_corpus_contract_is_the_committed_oracle() -> None:
+    """Guard the fixture shape the rest of this file leans on (#529 oracle)."""
+    assert len(CASES) == 24, "oracle is the 24-case contract corpus"
+    # Every expected reason is in the ADR-0205 closed set, and the corpus's own
+    # declared closed set agrees with the rule's MP_REASONS.
+    assert {reason for *_, reason in CASES} <= set(MP_REASONS)
+    assert set(_CORPUS["closed_reasons"]) == set(MP_REASONS)
+
+
+@pytest.mark.parametrize(
+    "cid,premises,conclusion,outcome,reason",
+    CASES,
+    ids=[c[0] for c in CASES],
+)
 def test_corpus_case(cid, premises, conclusion, outcome, reason) -> None:
     v = evaluate_modus_ponens(premises, conclusion)
     assert v.outcome.value == outcome, cid
@@ -80,28 +114,33 @@ def test_admit_yields_the_canonical_conclusion_key() -> None:
 # admit deriving a second distinct key, so pool-first refuses. A filter-first rule
 # (keep only derivations whose key == declared conclusion, then check uniqueness)
 # would admit both — admit-by-assertion. These assertions fail under that mutation.
+# Inputs come from the oracle (no re-transcription); the derived_keys counts are
+# the extra structural property this corpus case doesn't itself pin.
 # ---------------------------------------------------------------------------
 
 
 def test_pooling_refuses_unrelated_tautology_path() -> None:
-    # 007: one path yields T (R or not R), the substantive path yields Q.
+    # DISAGREE-007: one path yields T (R or not R), the substantive path yields Q.
-    v = evaluate_modus_ponens(("A", "A -> (R or not R)", "B", "B -> Q"), "Q")
+    premises, conclusion = _inputs_for("MP-DISAGREE-007")
+    v = evaluate_modus_ponens(premises, conclusion)
     assert v.outcome is MPOutcome.REFUSE
     assert v.reason == CONCLUSION_DISAGREEMENT
     assert len(v.derived_keys) == 2  # T and key(Q) — distinct, pooled
 
 
 def test_pooling_refuses_stronger_conclusion_path() -> None:
-    # 010: paths yield Q and (Q and R) — distinct keys.
+    # DISAGREE-010: paths yield Q and (Q and R) — distinct keys.
-    v = evaluate_modus_ponens(("A", "A -> Q", "B", "B -> (Q and R)"), "Q")
+    premises, conclusion = _inputs_for("MP-DISAGREE-010")
+    v = evaluate_modus_ponens(premises, conclusion)
     assert v.outcome is MPOutcome.REFUSE
     assert v.reason == CONCLUSION_DISAGREEMENT
     assert len(v.derived_keys) == 2
 
 
 def test_equivalent_paths_collapse_not_disagree() -> None:
-    # 003: Q->R and (not Q or R) are equivalent → one key → admit.
+    # DISAGREE-003: Q->R and (not Q or R) are equivalent → one key → admit.
-    v = evaluate_modus_ponens(("A", "A -> (Q -> R)", "B", "B -> (not Q or R)"), "Q -> R")
+    premises, conclusion = _inputs_for("MP-DISAGREE-003")
+    v = evaluate_modus_ponens(premises, conclusion)
     assert v.outcome is MPOutcome.ADMIT
     assert len(v.derived_keys) == 1