Merge pull request #662 from AssetOverflow/feat/p1-a-verified-contract

feat(epistemic-disclosure): P1-A — the VERIFIED contract + meaningful-fail tests
2026-06-08 16:29:26 -07:00 · 2026-06-08 16:29:26 -07:00 · 05a044d9a5
commit 05a044d9a5
parent 4fc251da2d ec7c680cfc
3 changed files with 417 additions and 0 deletions
--- a/core/epistemic_disclosure/init.py
+++ b/core/epistemic_disclosure/init.py
@ -19,6 +19,10 @@ Shipped so far (all off-serving — nothing here imports ``generate.derivation``
    ``EpistemicState × LimitationAssessment × DisclosureClaim → ServedDisposition``.
    Mapping scaffold only — no rendering, no bus, no ``verify.py``; nothing consumes
    it yet.
+  * :mod:`~core.epistemic_disclosure.verified_contract` (P1-A) — the VERIFIED contract:
+    the obligation, the proof shape, the validator, and the single sanctioned route to
+    ``EpistemicState.VERIFIED`` / ``DisclosureClaim.VERIFIED``. Contract only — no
+    producer; a faithful solve of a WRONG read must not verify.
 """

 from __future__ import annotations
@ -40,17 +44,33 @@ from core.epistemic_disclosure.limitation import (
    assess_from_family,
    terminal_for_action,
 )
+from core.epistemic_disclosure.verified_contract import (
+    VERIFICATION_OBLIGATION,
+    VerificationObligation,
+    VerificationProof,
+    VerificationResult,
+    VerificationVerdict,
+    disclosure_for_verification,
+    evaluate_verification,
+)

 __all__ = [
    "DEFAULT_DISCLOSURE_CLAIM",
    "PENDING_Q1B_RECLASSIFICATION",
+    "VERIFICATION_OBLIGATION",
    "DisclosureClaim",
    "LimitationAssessment",
    "LimitationKind",
    "ResolutionAction",
    "ServedDisposition",
+    "VerificationObligation",
+    "VerificationProof",
+    "VerificationResult",
+    "VerificationVerdict",
    "assess_from_attempt",
    "assess_from_family",
    "choose_served_disposition",
+    "disclosure_for_verification",
+    "evaluate_verification",
    "terminal_for_action",
 ]
--- a/core/epistemic_disclosure/verified_contract.py
+++ b/core/epistemic_disclosure/verified_contract.py
@ -0,0 +1,196 @@
+"""P1-A — the VERIFIED contract (the meaning of "verified", before any producer).
+
+This module defines WHAT IT MEANS for a result to earn ``DisclosureClaim.VERIFIED`` /
+``EpistemicState.VERIFIED`` — the soundness≠correctness gate the whole VERIFIED lane
+rests on. It ships ONLY the contract: the obligation, the proof SHAPE a producer must
+fill, the validator that enforces the obligation, and the single sanctioned route from
+a validated proof to the verified state/claim.
+
+It does NOT produce proofs. There is no reader, no solver, no back-substitution
+computation, no serving, no ``verify.py`` call, no ``verified_serving_enabled``. P1-B+
+fill :class:`VerificationProof` with real digests; P1-A only fixes the rules a proof
+must satisfy — and, above all, the rule that makes the lane safe:
+
+    A faithful solve of a WRONG read must NOT verify.
+
+**The mechanism.** Verification requires TWO INDEPENDENT reads (distinct reader
+lineages) that CONVERGE on the same canonical structure:
+
+  * a *wrong* primary read is caught because the independent read **disagrees** —
+    back-substitution alone cannot catch a read error (it only proves the solver was
+    faithful to whatever structure it was handed);
+  * a single reader run twice ("same answer twice") is rejected as **not independent**.
+
+Neither gold-agreement, nor absence-of-refusal, nor a second solver over ONE read can
+earn VERIFIED; only this contract can. (See [[VERIFIED-canonical-comparison-scoping-2026-06-06]]:
+"independence must be in the READING, not the solving".)
+
+**Discipline.** ``EpistemicState.VERIFIED`` must be reached ONLY via
+:func:`disclosure_for_verification` over a VERIFIED :class:`VerificationResult` — never
+constructed directly by producer/serving code. A future architectural invariant can
+scan for direct emission; P1-A establishes the route.
+
+Off-serving: imports no ``generate.derivation`` / ``core.reliability_gate``.
+"""
+
+from __future__ import annotations
+
+from dataclasses import dataclass
+from enum import Enum, unique
+
+from core.epistemic_disclosure.disclosure_claim import DisclosureClaim
+from core.epistemic_disclosure.limitation import LimitationAssessment
+from core.epistemic_state import EpistemicState
+
+
+@unique
+class VerificationVerdict(str, Enum):
+    """Whether a result earns the VERIFIED claim. There is no middle state — a result
+    either survives every obligation or it does not verify (refuse-preferring)."""
+
+    VERIFIED = "verified"
+    NOT_VERIFIED = "not_verified"
+
+
+@dataclass(frozen=True, slots=True)
+class VerificationObligation:
+    """The declarative contract: which checks a proof must survive to be VERIFIED.
+
+    A schema naming proof obligations (CLAUDE.md "Schema-Defined Proof Obligations").
+    The canonical :data:`VERIFICATION_OBLIGATION` sets every flag ``True``; the flags
+    exist so a test can prove each obligation is LOAD-BEARING — relax exactly one and
+    the corresponding poison case slips through (see ``test_verified_contract.py``).
+    """
+
+    requires_independent_read: bool  # two DISTINCT reader lineages — not the same read twice
+    rejects_wrong_read_even_if_solved: bool  # the two reads must CONVERGE — catches a wrong read
+    requires_back_substitution: bool  # the answer back-substitutes into the canonical structure
+    requires_boundary_clear: bool  # no organ boundary fired in the chain
+
+
+#: The canonical, fully-strict obligation. VERIFIED requires ALL of it.
+VERIFICATION_OBLIGATION: VerificationObligation = VerificationObligation(
+    requires_independent_read=True,
+    rejects_wrong_read_even_if_solved=True,
+    requires_back_substitution=True,
+    requires_boundary_clear=True,
+)
+
+
+@dataclass(frozen=True, slots=True)
+class VerificationProof:
+    """The replayable proof shape a producer (P1-B+) must fill. P1-A defines the shape
+    and the rules; it computes none of these digests.
+
+    The two reads are kept separate ON PURPOSE: ``primary_reader_lineage`` /
+    ``independent_reader_lineage`` must DIFFER (independence), and ``primary_read_digest``
+    / ``independent_read_digest`` must MATCH (convergence on one canonical structure).
+    Independence + convergence together are what reject a faithful solve of a wrong read.
+    """
+
+    source_problem_digest: str  # provenance: hash of the problem text
+    primary_reader_lineage: str  # identity of the primary reader
+    independent_reader_lineage: str  # identity of the independent cross-check reader
+    primary_read_digest: str  # canonical structure the primary read produced
+    independent_read_digest: str  # canonical structure the independent read produced
+    derivation_digest: str  # the derivation from the STATED quantities
+    back_substitution_digest: str  # back-substitution into the canonical structure
+    boundary_clear: bool  # no organ boundary fired
+    contradiction_clear: bool  # no contradiction family fired
+
+
+# Reason codes for a failed obligation — each names exactly one violated rule.
+REASON_READS_NOT_INDEPENDENT = "reads_not_independent"  # same reader lineage twice
+REASON_READS_DISAGREE = "reads_disagree"  # the wrong-read catcher
+REASON_NO_BACK_SUBSTITUTION = "no_back_substitution"
+REASON_BOUNDARY_FIRED = "boundary_fired"
+REASON_CONTRADICTION_PRESENT = "contradiction_present"
+REASON_INCOMPLETE_PROOF = "incomplete_proof_digest"
+REASON_UNRESOLVED_LIMITATION = "unresolved_limitation"
+
+
+@dataclass(frozen=True, slots=True)
+class VerificationResult:
+    """The verdict plus the specific obligations that failed (empty iff VERIFIED)."""
+
+    verdict: VerificationVerdict
+    failed_checks: tuple[str, ...]
+
+
+def evaluate_verification(
+    proof: VerificationProof,
+    *,
+    limitation: LimitationAssessment | None,
+    obligation: VerificationObligation = VERIFICATION_OBLIGATION,
+) -> VerificationResult:
+    """Apply the VERIFIED contract to a proof. Refuse-preferring: VERIFIED only if
+    EVERY obligation survives; otherwise NOT_VERIFIED with the failed checks.
+
+    Pure logic over the proof fields — it does NOT compute or trust any digest, it only
+    enforces the rules a producer's proof must satisfy. ``limitation`` is the
+    contemplation outcome: a verified answer cannot coexist with an unresolved
+    limitation (a contradiction, an ambiguity, a missing datum).
+    """
+    failed: list[str] = []
+
+    if obligation.requires_independent_read and (
+        proof.primary_reader_lineage == proof.independent_reader_lineage
+    ):
+        failed.append(REASON_READS_NOT_INDEPENDENT)
+
+    if obligation.rejects_wrong_read_even_if_solved and (
+        proof.primary_read_digest != proof.independent_read_digest
+    ):
+        failed.append(REASON_READS_DISAGREE)
+
+    if obligation.requires_back_substitution and not proof.back_substitution_digest:
+        failed.append(REASON_NO_BACK_SUBSTITUTION)
+
+    if obligation.requires_boundary_clear and not proof.boundary_clear:
+        failed.append(REASON_BOUNDARY_FIRED)
+
+    # Non-negotiable checks (NOT gated by the obligation flags):
+    if not proof.contradiction_clear:
+        failed.append(REASON_CONTRADICTION_PRESENT)
+
+    if not (
+        proof.source_problem_digest
+        and proof.primary_read_digest
+        and proof.derivation_digest
+    ):
+        failed.append(REASON_INCOMPLETE_PROOF)
+
+    if limitation is not None:
+        failed.append(REASON_UNRESOLVED_LIMITATION)
+
+    verdict = (
+        VerificationVerdict.VERIFIED if not failed else VerificationVerdict.NOT_VERIFIED
+    )
+    return VerificationResult(verdict=verdict, failed_checks=tuple(failed))
+
+
+def disclosure_for_verification(
+    result: VerificationResult,
+) -> tuple[EpistemicState, DisclosureClaim]:
+    """The ONLY sanctioned route to a verified state/claim.
+
+    VERIFIED verdict → (``EpistemicState.VERIFIED``, ``DisclosureClaim.VERIFIED``);
+    anything else → (``UNDETERMINED``, ``NONE``). Producer/serving code must reach
+    ``EpistemicState.VERIFIED`` THROUGH this gate, never by constructing it directly —
+    that is what keeps "gold agreement" / "same answer twice" / "no refusal" from ever
+    masquerading as verified.
+    """
+    if result.verdict is VerificationVerdict.VERIFIED:
+        return EpistemicState.VERIFIED, DisclosureClaim.VERIFIED
+    return EpistemicState.UNDETERMINED, DisclosureClaim.NONE
+
+
+__all__ = [
+    "VERIFICATION_OBLIGATION",
+    "VerificationObligation",
+    "VerificationProof",
+    "VerificationResult",
+    "VerificationVerdict",
+    "disclosure_for_verification",
+    "evaluate_verification",
+]
--- a/tests/test_verified_contract.py
+++ b/tests/test_verified_contract.py
@ -0,0 +1,201 @@
+"""P1-A — tests for the VERIFIED contract.
+
+The central, non-negotiable test is :func:`test_verified_contract_rejects_faithful_solve_of_wrong_read`:
+a wrong semantic read that is arithmetically faithfully solved (back-substitutes,
+boundary-clear) must NOT verify, because an independent read disagrees. Every other
+test pins one obligation. The contract is contract-only — no producer, no serving.
+"""
+
+from __future__ import annotations
+
+import ast
+import pathlib
+from dataclasses import replace
+
+from core.epistemic_disclosure.disclosure_claim import DisclosureClaim
+from core.epistemic_disclosure.disposition import (
+    ServedDisposition,
+    choose_served_disposition,
+)
+from core.epistemic_disclosure.limitation import LimitationAssessment
+from core.epistemic_disclosure.verified_contract import (
+    REASON_BOUNDARY_FIRED,
+    REASON_CONTRADICTION_PRESENT,
+    REASON_INCOMPLETE_PROOF,
+    REASON_NO_BACK_SUBSTITUTION,
+    REASON_READS_DISAGREE,
+    REASON_READS_NOT_INDEPENDENT,
+    REASON_UNRESOLVED_LIMITATION,
+    VERIFICATION_OBLIGATION,
+    VerificationProof,
+    VerificationVerdict,
+    disclosure_for_verification,
+    evaluate_verification,
+)
+from core.epistemic_state import EpistemicState
+
+
+def _valid_proof(**overrides) -> VerificationProof:
+    """A proof that survives the full contract: two independent reads converging on one
+    canonical structure, a faithful derivation that back-substitutes, no boundary, no
+    contradiction. Override one field to construct each poison case."""
+    base = dict(
+        source_problem_digest="prob#1",
+        primary_reader_lineage="reader_primary",
+        independent_reader_lineage="reader_independent",
+        primary_read_digest="canonical_structure_C",
+        independent_read_digest="canonical_structure_C",
+        derivation_digest="deriv#1",
+        back_substitution_digest="backsub#1",
+        boundary_clear=True,
+        contradiction_clear=True,
+    )
+    base.update(overrides)
+    return VerificationProof(**base)
+
+
+# --- the positive case: the ONLY route to VERIFIED --------------------------------- #
+
+def test_fully_valid_proof_verifies():
+    result = evaluate_verification(_valid_proof(), limitation=None)
+    assert result.verdict is VerificationVerdict.VERIFIED
+    assert result.failed_checks == ()
+
+
+# --- THE central hazard ------------------------------------------------------------ #
+
+def test_verified_contract_rejects_faithful_solve_of_wrong_read():
+    """A WRONG primary read, an arithmetically faithful solve over it (back-substitutes
+    into the wrong structure, no boundary fires) — but the INDEPENDENT read sees the
+    correct structure and disagrees. Must NOT verify. This is the gate that stops P1-B
+    from degenerating into a 'second solver agrees' rubber stamp."""
+    poison = _valid_proof(
+        primary_read_digest="structure_from_WRONG_read",
+        independent_read_digest="structure_from_CORRECT_read",  # the reads disagree
+    )
+    result = evaluate_verification(poison, limitation=None)
+    assert result.verdict is VerificationVerdict.NOT_VERIFIED
+    assert REASON_READS_DISAGREE in result.failed_checks
+
+
+def test_verified_requires_independent_read_not_same_read_twice():
+    same_read_twice = _valid_proof(
+        primary_reader_lineage="reader_X",
+        independent_reader_lineage="reader_X",  # same lineage → not independent
+    )
+    result = evaluate_verification(same_read_twice, limitation=None)
+    assert result.verdict is VerificationVerdict.NOT_VERIFIED
+    assert REASON_READS_NOT_INDEPENDENT in result.failed_checks
+
+
+# --- each remaining obligation ----------------------------------------------------- #
+
+def test_verified_requires_back_substitution():
+    result = evaluate_verification(_valid_proof(back_substitution_digest=""), limitation=None)
+    assert result.verdict is VerificationVerdict.NOT_VERIFIED
+    assert REASON_NO_BACK_SUBSTITUTION in result.failed_checks
+
+
+def test_verified_requires_boundary_clear():
+    result = evaluate_verification(_valid_proof(boundary_clear=False), limitation=None)
+    assert result.verdict is VerificationVerdict.NOT_VERIFIED
+    assert REASON_BOUNDARY_FIRED in result.failed_checks
+
+
+def test_contradiction_blocks_verification():
+    result = evaluate_verification(_valid_proof(contradiction_clear=False), limitation=None)
+    assert result.verdict is VerificationVerdict.NOT_VERIFIED
+    assert REASON_CONTRADICTION_PRESENT in result.failed_checks
+
+
+def test_incomplete_proof_digest_blocks_verification():
+    for field in ("source_problem_digest", "derivation_digest"):
+        result = evaluate_verification(_valid_proof(**{field: ""}), limitation=None)
+        assert result.verdict is VerificationVerdict.NOT_VERIFIED, field
+        assert REASON_INCOMPLETE_PROOF in result.failed_checks, field
+
+
+def test_verified_rejects_any_limitation_assessment():
+    blocking = LimitationAssessment(
+        limitation_kind="missing_information",
+        resolution_action="ask_question",
+        epistemic_state=EpistemicState.UNDETERMINED,
+        owner_organ="r2",
+        blocking_reason="cmb_underdetermined",
+    )
+    result = evaluate_verification(_valid_proof(), limitation=blocking)
+    assert result.verdict is VerificationVerdict.NOT_VERIFIED
+    assert REASON_UNRESOLVED_LIMITATION in result.failed_checks
+
+
+# --- the obligations are LOAD-BEARING (schema-obligation discipline) ---------------- #
+
+def test_canonical_obligation_is_fully_strict():
+    assert VERIFICATION_OBLIGATION.requires_independent_read
+    assert VERIFICATION_OBLIGATION.rejects_wrong_read_even_if_solved
+    assert VERIFICATION_OBLIGATION.requires_back_substitution
+    assert VERIFICATION_OBLIGATION.requires_boundary_clear
+
+
+def test_relaxing_wrong_read_obligation_would_admit_the_poison():
+    """Proves ``rejects_wrong_read_even_if_solved`` is load-bearing, not decoration: the
+    canonical obligation catches the poison; relaxing exactly that one flag stops the
+    check from firing (CLAUDE.md: a test must fail under the violation it guards)."""
+    poison = _valid_proof(independent_read_digest="different_structure")
+    canonical = evaluate_verification(poison, limitation=None)
+    assert canonical.verdict is VerificationVerdict.NOT_VERIFIED
+    assert REASON_READS_DISAGREE in canonical.failed_checks
+
+    relaxed = replace(VERIFICATION_OBLIGATION, rejects_wrong_read_even_if_solved=False)
+    relaxed_result = evaluate_verification(poison, limitation=None, obligation=relaxed)
+    assert REASON_READS_DISAGREE not in relaxed_result.failed_checks
+
+
+# --- the sanctioned route to the verified state/claim ------------------------------ #
+
+def test_verified_claim_requires_epistemic_state_verified():
+    verified = evaluate_verification(_valid_proof(), limitation=None)
+    state, claim = disclosure_for_verification(verified)
+    assert state is EpistemicState.VERIFIED
+    assert claim is DisclosureClaim.VERIFIED
+
+
+def test_not_verified_routes_to_safe_defaults():
+    poison = evaluate_verification(_valid_proof(independent_read_digest="diff"), limitation=None)
+    state, claim = disclosure_for_verification(poison)
+    assert state is not EpistemicState.VERIFIED
+    assert claim is not DisclosureClaim.VERIFIED
+    assert (state, claim) == (EpistemicState.UNDETERMINED, DisclosureClaim.NONE)
+
+
+# --- composition with the Phase-0 bus (the whole chain) ---------------------------- #
+
+def test_verified_proof_routes_through_bus_to_disclose():
+    """proof → contract → (VERIFIED state, VERIFIED claim) → P0-3 disposition = DISCLOSE."""
+    result = evaluate_verification(_valid_proof(), limitation=None)
+    state, claim = disclosure_for_verification(result)
+    disp = choose_served_disposition(epistemic_state=state, limitation=None, disclosure_claim=claim)
+    assert disp is ServedDisposition.DISCLOSE
+
+
+def test_unverified_proof_never_discloses_through_bus():
+    result = evaluate_verification(_valid_proof(independent_read_digest="diff"), limitation=None)
+    state, claim = disclosure_for_verification(result)
+    disp = choose_served_disposition(epistemic_state=state, limitation=None, disclosure_claim=claim)
+    assert disp is not ServedDisposition.DISCLOSE
+    assert disp is ServedDisposition.COMMIT
+
+
+# --- hygiene ----------------------------------------------------------------------- #
+
+def test_verified_contract_does_not_import_serving_or_verify():
+    import core.epistemic_disclosure.verified_contract as mod
+
+    module_path = mod.__file__
+    assert module_path is not None
+    src = pathlib.Path(module_path).read_text()
+    mods = [n.module or "" for n in ast.walk(ast.parse(src)) if isinstance(n, ast.ImportFrom)]
+    forbidden = [
+        m for m in mods if "generate.derivation" in m or "reliability_gate" in m or m.endswith("verify")
+    ]
+    assert forbidden == []