From ec7c680cfc2710a73b41e4a1664605e4e9c520c8 Mon Sep 17 00:00:00 2001 From: Shay Date: Mon, 8 Jun 2026 16:20:19 -0700 Subject: [PATCH] =?UTF-8?q?feat(epistemic-disclosure):=20P1-A=20=E2=80=94?= =?UTF-8?q?=20the=20VERIFIED=20contract=20+=20meaningful-fail=20tests?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Defines what it MEANS for a result to earn DisclosureClaim.VERIFIED / EpistemicState.VERIFIED — the soundness≠correctness gate the whole VERIFIED lane rests on. Contract ONLY: no producer, no reader, no solver, no serving, no verify.py, no verified_serving_enabled, no claim emission in any serving path. core/epistemic_disclosure/verified_contract.py: - VerificationObligation — the declarative contract (4 load-bearing flags); VERIFICATION_OBLIGATION is fully strict. - VerificationProof — the replayable proof SHAPE P1-B+ will fill (two reads kept separate: distinct lineages for independence, matching digests for convergence). - evaluate_verification(proof, *, limitation, obligation) -> VerificationResult — refuse-preferring: VERIFIED only if EVERY obligation survives. - disclosure_for_verification(result) — the ONLY sanctioned route to (EpistemicState.VERIFIED, DisclosureClaim.VERIFIED); anything else -> UNDETERMINED/NONE. The mechanism that makes the lane safe: VERIFIED requires TWO INDEPENDENT reads (distinct lineages) that CONVERGE on one canonical structure. A faithful solve of a WRONG read is caught because the independent read disagrees (back-substitution alone cannot catch a read error); "same answer twice" is rejected as not independent. Neither gold-agreement nor no-refusal nor a second solver over one read can verify. 15 tests, all non-vacuous. THE central test rejects a faithful solve of a wrong read; one proves the wrong-read obligation is load-bearing (relax it -> poison slips the check); the full chain composes proof -> contract -> (VERIFIED, VERIFIED) -> P0-3 DISCLOSE, and the poison degrades to COMMIT. Off-serving; smoke 90/0. --- core/epistemic_disclosure/__init__.py | 20 ++ .../epistemic_disclosure/verified_contract.py | 196 +++++++++++++++++ tests/test_verified_contract.py | 201 ++++++++++++++++++ 3 files changed, 417 insertions(+) create mode 100644 core/epistemic_disclosure/verified_contract.py create mode 100644 tests/test_verified_contract.py diff --git a/core/epistemic_disclosure/__init__.py b/core/epistemic_disclosure/__init__.py index fd097981..90ca640b 100644 --- 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", ] diff --git a/core/epistemic_disclosure/verified_contract.py b/core/epistemic_disclosure/verified_contract.py new file mode 100644 index 00000000..92111833 --- /dev/null +++ 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", +] diff --git a/tests/test_verified_contract.py b/tests/test_verified_contract.py new file mode 100644 index 00000000..5d26d6e2 --- /dev/null +++ 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 == []