diff --git a/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md b/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md index e7ca0f96..a8f7254d 100644 --- a/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md +++ b/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md @@ -167,10 +167,12 @@ the certificate, not just the status. exist before ratification — so PR B retires **no** markers; the certificate-shaped halves of O1/O7 are instead proven for real in the dedicated test file. -- **PR C (requires this ADR ratified).** `certify_promotion` + - `VaultStore.apply_certified_promotion` behind the existing mutation owner. - Retires all the xfails (strict-xpass forces it); INV-21 allowlist - unchanged; INV-29 allowlist unchanged; full + deductive lanes wrong=0. +- **PR C (landed with ratification, same PR).** `certify_promotion` + (`teaching/proof_promotion.py`) + `VaultStore.apply_certified_promotion` + behind the existing mutation owner. All xfails retired (strict-xpass + forced it); INV-21 allowlist unchanged; INV-29 allowlist unchanged; full + + deductive lanes wrong=0. The engine pin lives in + `generate/proof_chain/engine_pin.py`, sync-pinned to the lane registry. - **PR D.** Local deterministic demo (`demos/` pattern): proposer submits claim + proof candidate; CORE ignores the candidate, recomputes, promotes or refuses on pinned verification only. No network, no model API, no side diff --git a/docs/issues/proof-carrying-coherence-promotion.md b/docs/issues/proof-carrying-coherence-promotion.md index 14bfd799..c059aecb 100644 --- a/docs/issues/proof-carrying-coherence-promotion.md +++ b/docs/issues/proof-carrying-coherence-promotion.md @@ -1,13 +1,14 @@ # Issue — Proof-carrying coherence promotion (the logical arm of ADR-0021's v2 gap) -**Status:** Open — [ADR-0218 proposed](../decisions/ADR-0218-proof-carrying-coherence-promotion.md) -(2026-06-11, awaiting ratification); runtime code remains unauthorized. -Executable proof obligations shipped as strict-xfail in -`tests/test_proof_carrying_promotion_obligations.py`; INV-29 now pins the -status-transition-site allowlist. PR B landed the pure evidence substrate: -`generate/proof_chain/certificate.py` (`PromotionCertificate` + -`build_certificate` / `verify_certificate` replay verifier) — no promotion, -no vault import, no status transition; promoter obligations remain xfail. +**Status:** Capability landed — [ADR-0218 ratified 2026-06-11](../decisions/ADR-0218-proof-carrying-coherence-promotion.md). +PR A shipped the obligations + INV-29; PR B the pure evidence substrate +(`generate/proof_chain/certificate.py`); PR C (post-ratification) the P3 +promoter: `teaching/proof_promotion.py` (pure decider, fresh-read store +state, proposer payload provably unread) + +`VaultStore.apply_certified_promotion` (independent re-verification, the +only transition site — INV-21/INV-29 allowlists unchanged). All strict-xfail +obligations are retired and pass live. No runtime turn path calls promotion +yet; the deterministic demo is PR D. **Raised:** 2026-06-11 **Surface:** `teaching/epistemic.py`, `teaching/review.py`, the deductive engine (`deductive_logic_v1`), `vault/store.py`, INV-21 one-mutation-path diff --git a/generate/proof_chain/__init__.py b/generate/proof_chain/__init__.py index 624ae4cd..58c5596f 100644 --- a/generate/proof_chain/__init__.py +++ b/generate/proof_chain/__init__.py @@ -11,6 +11,11 @@ - ADR-0218 PR B: `PromotionCertificate` + pure replay verifier (`build_certificate` / `verify_certificate`), in `certificate.py`. Evidence substrate only — no promotion, no vault import, no status transition. +- ADR-0218 P3 (ratified): `engine_pin.py` carries `DEDUCTIVE_ENGINE_PIN`, the + deductive-lane SHA the promoter stamps into certificates and the vault + demands back at apply time. The promoter itself lives in + `teaching/proof_promotion.py`; the transition owner is + `VaultStore.apply_certified_promotion`. Honesty boundary (load-bearing through 2.3): sound over declared atoms, not grounded in recognized input; the disagreement rule guarantees a unique conclusion among @@ -26,6 +31,7 @@ from .builder import ( ProofGraph, build_proof_graph, ) +from .engine_pin import DEDUCTIVE_ENGINE_PIN from .certificate import ( CERTIFICATE_VERSION, ENGINE_PIN_MISMATCH, @@ -72,6 +78,7 @@ __all__ = ( "CONCLUSION_DISAGREEMENT", "CONCLUSION_MISMATCH", "CertificateVerification", + "DEDUCTIVE_ENGINE_PIN", "ENGINE_PIN_MISMATCH", "MALFORMED_CERTIFICATE", "MISSING_IMPLICATION", diff --git a/generate/proof_chain/certificate.py b/generate/proof_chain/certificate.py index 9d4d6ebf..633bbe92 100644 --- a/generate/proof_chain/certificate.py +++ b/generate/proof_chain/certificate.py @@ -1,8 +1,10 @@ """ADR-0218 PR B — ``PromotionCertificate`` + pure replay verifier. -THE PROMOTION FEATURE IS NOT LIVE. ADR-0218 is Proposed, not ratified; this -module is the side-effect-free *evidence substrate* the future P3 promoter -(``teaching/proof_promotion.py``, which does not exist) will consume. It +ADR-0218 is ratified (2026-06-11) and the P3 promoter exists +(``teaching/proof_promotion.py``; the transition owner is +``VaultStore.apply_certified_promotion``). THE FEATURE HAS NO RUNTIME CALLER +YET — no chat/runtime turn path invokes promotion (the deterministic demo is +PR D). This module remains the side-effect-free *evidence substrate*: it decides nothing about the vault and mutates nothing anywhere: - no vault / teaching / session import — premises arrive as already-read diff --git a/generate/proof_chain/engine_pin.py b/generate/proof_chain/engine_pin.py new file mode 100644 index 00000000..2a1ef008 --- /dev/null +++ b/generate/proof_chain/engine_pin.py @@ -0,0 +1,30 @@ +"""Deductive-engine provenance pin (ADR-0218 §D4). + +``DEDUCTIVE_ENGINE_PIN`` mirrors ``PINNED_SHAS["deductive_logic_v1"]`` in +``scripts/verify_lane_shas.py`` — the SHA-256 of the deductive lane report +produced by the engine build in force. It is the value the P3 promoter +stamps into every ``PromotionCertificate`` (``engine_pin``) and the value +``VaultStore.apply_certified_promotion`` demands back via +``verify_certificate(..., expected_engine_pin=...)``. + +Why a mirrored constant instead of reading the registry: ``scripts/`` is not +an importable runtime package, and the certificate module is deliberately +filesystem-free (PR B honesty boundary: pure replay cannot *know* the true +pin). The sync is pinned by +``tests/test_adr_0218_proof_promotion.py::test_engine_pin_matches_lane_registry``, +which AST-parses the registry — drift between the two fails the suite. + +When the deductive lane re-pins (an intentional engine change), update this +constant in the same commit. Certificates built under the old pin then fail +apply-time pin verification — that is the desired alarm: an entailment proved +by a different engine build must be re-certified, not trusted across the +engine change. +""" + +from __future__ import annotations + +from typing import Final + +DEDUCTIVE_ENGINE_PIN: Final[str] = ( + "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f" +) diff --git a/teaching/epistemic.py b/teaching/epistemic.py index 8fe3b8e1..eff2b45f 100644 --- a/teaching/epistemic.py +++ b/teaching/epistemic.py @@ -24,15 +24,17 @@ class EpistemicStatus(Enum): function of coherence with the existing reviewed field, never of source authority, credentials, or the system's own asserted output. - The *judgment behind* a transition is curator-mediated today — + The *judgment behind* a transition is curator-mediated by default — ``review_correction`` carries the resulting status as an input, it does - not yet compute it. ADR-0021's "Named gap (v2 work)" commits to - replacing curator mediation with a structural coherence metric; one - arm of that successor (proof-carrying promotion for the deductively - *entailed* subclass, via the sound ``deductive_logic_v1`` engine) is - specified but not yet wired — see - ``docs/issues/proof-carrying-coherence-promotion.md``. Until it lands, - do not read this enum as evidence of an automated coherence computation. + not compute it. One arm of ADR-0021's "Named gap (v2 work)" is now + wired (ADR-0218, ratified 2026-06-11): for the deductively *entailed* + subclass, ``teaching/proof_promotion.py`` certifies entailment over an + all-COHERENT, curator-certified premise set via the sound + ``deductive_logic_v1`` engine, and + ``VaultStore.apply_certified_promotion`` owns the SPECULATIVE→COHERENT + transition after independent re-verification. No runtime turn path + invokes it yet. Every other transition remains curator-mediated — see + ``docs/issues/proof-carrying-coherence-promotion.md``. """ COHERENT = "coherent" diff --git a/teaching/proof_promotion.py b/teaching/proof_promotion.py new file mode 100644 index 00000000..96a56f9f --- /dev/null +++ b/teaching/proof_promotion.py @@ -0,0 +1,248 @@ +"""teaching/proof_promotion.py — ADR-0218 P3: the pure proof-carrying +promotion decider. + +``certify_promotion`` decides whether a stored SPECULATIVE claim is +promotable to COHERENT because it is *deductively entailed* by an +all-COHERENT, curator-certified premise set (ADR-0218 §D3). This module is +**pure decision logic**: + +- it performs NO mutation and holds no vault write access — INV-21's and + INV-29's allowlists are untouched (the structural proof lives in + ``tests/test_adr_0218_proof_promotion.py``); +- the only mutation owner is ``VaultStore.apply_certified_promotion`` + (vault/store.py), which **independently re-verifies** the certificate and + the live store state before flipping anything — a decision object from + this module is a recommendation, never authority; +- it is not a parallel learning path: it produces a decision consumed by the + single existing mutation owner, exactly the ADR-0148 policy/owner split. + +Admissibility predicate (ADR-0218 §D3, exact): + +1. Every premise ref resolves to a stored vault entry, fresh-read at + decision time, with ``epistemic_status == "coherent"`` (strict string + compare — no parse-defaulting anywhere in this module). +2. Every premise form AND the claim form are curator-certified readings + (``reading_certified is True`` + a non-empty ``propositional_form``), + taken from the store, never from the proposer. The claim is itself a + stored entry (``claim_entry_index``); a proposer cannot supply a form. +3. The engine outcome is ENTAILED. REFUTED / UNKNOWN / REFUSED never + promote; REFUTED also never demotes (no status is written here at all). +4. The built certificate replay-verifies under the pinned engine + (``DEDUCTIVE_ENGINE_PIN``). +5. ``proposer_payload`` is data, never authority: it is accepted so + proposers can attach proof candidates / statuses / confidences, and it + is provably never read — the decision is byte-identical with and + without it. + +Any failure refuses with a typed reason from ``DECISION_REASONS``; the claim +stays SPECULATIVE. Fail-closed is the only failure mode. +""" + +from __future__ import annotations + +import hashlib +from dataclasses import dataclass +from typing import TYPE_CHECKING, Final, Mapping + +from generate.proof_chain.certificate import ( + PremiseRecord, + PromotionCertificate, + build_certificate, + verify_certificate, +) +from generate.proof_chain.engine_pin import DEDUCTIVE_ENGINE_PIN +from teaching.epistemic import EpistemicStatus + +if TYPE_CHECKING: + from vault.store import VaultStore + +# Closed decision-reason vocabulary. O3/O4 obligation contract: the premise +# gates name "premise", the reading gates name "reading". +PROMOTED_ENTAILED: Final[str] = "promoted_entailed_from_coherent_premises" +REFUSED_NO_PREMISES: Final[str] = "refused_no_premises" +REFUSED_DUPLICATE_PREMISES: Final[str] = "refused_duplicate_premise_entries" +REFUSED_PREMISE_MISSING: Final[str] = "refused_premise_entry_missing" +REFUSED_PREMISE_NOT_COHERENT: Final[str] = "refused_premise_not_coherent" +REFUSED_PREMISE_READING: Final[str] = "refused_premise_reading_uncertified" +REFUSED_CLAIM_MISSING: Final[str] = "refused_claim_entry_missing" +REFUSED_CLAIM_NOT_SPECULATIVE: Final[str] = "refused_claim_not_speculative" +REFUSED_CLAIM_READING: Final[str] = "refused_claim_reading_uncertified" +REFUSED_NOT_ENTAILED: Final[str] = "refused_not_entailed" +REFUSED_MALFORMED_INPUT: Final[str] = "refused_malformed_input" +REFUSED_CERTIFICATE_REPLAY: Final[str] = "refused_certificate_replay_failed" + +DECISION_REASONS: Final[frozenset[str]] = frozenset({ + PROMOTED_ENTAILED, + REFUSED_NO_PREMISES, + REFUSED_DUPLICATE_PREMISES, + REFUSED_PREMISE_MISSING, + REFUSED_PREMISE_NOT_COHERENT, + REFUSED_PREMISE_READING, + REFUSED_CLAIM_MISSING, + REFUSED_CLAIM_NOT_SPECULATIVE, + REFUSED_CLAIM_READING, + REFUSED_NOT_ENTAILED, + REFUSED_MALFORMED_INPUT, + REFUSED_CERTIFICATE_REPLAY, +}) + + +@dataclass(frozen=True, slots=True) +class PromotionDecision: + """Outcome of one promotion certification. + + ``certificate`` is attached whenever the engine ran (including refused + outcomes — the refusal is audit evidence too); it is ``None`` when a + store-state gate refused before the engine could run. + ``certificate_digest`` is the SHA-256 of ``certificate.canonical_json()`` + — the value ADR-0218 §D4 folds into the turn ``trace_hash`` once a + runtime caller exists. + """ + + promoted: bool + reason: str + claim_entry_index: int + certificate: PromotionCertificate | None + certificate_digest: str | None + + +def certificate_digest(certificate: PromotionCertificate) -> str: + """SHA-256 hex digest of the certificate's canonical JSON (D4 folding).""" + return hashlib.sha256(certificate.canonical_json().encode("utf-8")).hexdigest() + + +def _is_index(value: object) -> bool: + """Vault entry indices are non-negative ints; bool is not an index.""" + return isinstance(value, int) and not isinstance(value, bool) and value >= 0 + + +def _fresh_read(vault: "VaultStore", index: object) -> Mapping[str, object] | None: + """Fresh-read one entry's metadata from the store (read-only view). + + Uses the sanctioned ``iter_metadata`` read surface; returns None when the + index does not resolve. Decision-time freshness is the point: nothing + cached, nothing proposer-supplied. + """ + if not _is_index(index): + return None + for i, meta in vault.iter_metadata(): + if i == index: + return meta + return None + + +def _certified_form(meta: Mapping[str, object]) -> str | None: + """The curator-certified reading, or None if certification is absent. + + ``reading_certified`` must be the boolean ``True`` — a truthy stand-in + (``1``, ``"yes"``) is not a curator certification. The form must be a + non-empty string. Fail-closed: any gap returns None. + """ + if meta.get("reading_certified") is not True: + return None + form = meta.get("propositional_form") + if not isinstance(form, str) or not form.strip(): + return None + return form + + +def _refusal(reason: str, claim_entry_index: int) -> PromotionDecision: + return PromotionDecision( + promoted=False, + reason=reason, + claim_entry_index=claim_entry_index, + certificate=None, + certificate_digest=None, + ) + + +def certify_promotion( + *, + claim_entry_index: int, + premise_entry_indices: tuple[int, ...], + vault: "VaultStore", + proposer_payload: object = None, +) -> PromotionDecision: + """Decide promotability of one stored SPECULATIVE claim. Pure: no + mutation; the caller hands the decision's certificate to + ``VaultStore.apply_certified_promotion``, which re-verifies independently. + """ + # D3.5 — data, never authority. Accepted so proposers can attach proof / + # status / confidence; deleted unread, so the decision cannot depend on it. + del proposer_payload + + safe_index = claim_entry_index if _is_index(claim_entry_index) else -1 + + if not isinstance(premise_entry_indices, tuple) or not all( + _is_index(i) for i in premise_entry_indices + ): + return _refusal(REFUSED_MALFORMED_INPUT, safe_index) + if len(premise_entry_indices) == 0: + # Zero-premise (tautology) certificates never promote in v1 — D3.1 is + # vacuous over the empty set, so the empty set refuses (ratified D3.b). + return _refusal(REFUSED_NO_PREMISES, safe_index) + if len(set(premise_entry_indices)) != len(premise_entry_indices): + return _refusal(REFUSED_DUPLICATE_PREMISES, safe_index) + + claim_meta = _fresh_read(vault, claim_entry_index) + if claim_meta is None: + return _refusal(REFUSED_CLAIM_MISSING, safe_index) + if claim_meta.get("epistemic_status") != EpistemicStatus.SPECULATIVE.value: + # Strict compare: a garbage status must not read as "speculative". + return _refusal(REFUSED_CLAIM_NOT_SPECULATIVE, claim_entry_index) + claim_form = _certified_form(claim_meta) + if claim_form is None: + return _refusal(REFUSED_CLAIM_READING, claim_entry_index) + + records: list[PremiseRecord] = [] + for index in premise_entry_indices: + meta = _fresh_read(vault, index) + if meta is None: + return _refusal(REFUSED_PREMISE_MISSING, claim_entry_index) + form = _certified_form(meta) + if form is None: + return _refusal(REFUSED_PREMISE_READING, claim_entry_index) + if meta.get("epistemic_status") != EpistemicStatus.COHERENT.value: + # Also structurally bars self-premising: the claim is required + # SPECULATIVE above, so it can never pass this COHERENT gate. + return _refusal(REFUSED_PREMISE_NOT_COHERENT, claim_entry_index) + records.append( + PremiseRecord( + entry_id=index, + form=form, + status=EpistemicStatus.COHERENT.value, + ) + ) + + try: + certificate = build_certificate( + claim_form=claim_form, + premises=tuple(records), + engine_pin=DEDUCTIVE_ENGINE_PIN, + ) + except ValueError: + # Unreachable given the gates above; kept as a typed fail-closed + # refusal rather than an escaping exception. + return _refusal(REFUSED_MALFORMED_INPUT, claim_entry_index) + + digest = certificate_digest(certificate) + verification = verify_certificate( + certificate, expected_engine_pin=DEDUCTIVE_ENGINE_PIN + ) + if not verification.verified: + return PromotionDecision( + promoted=False, + reason=REFUSED_CERTIFICATE_REPLAY, + claim_entry_index=claim_entry_index, + certificate=certificate, + certificate_digest=digest, + ) + + promoted = certificate.promotion_positive + return PromotionDecision( + promoted=promoted, + reason=PROMOTED_ENTAILED if promoted else REFUSED_NOT_ENTAILED, + claim_entry_index=claim_entry_index, + certificate=certificate, + certificate_digest=digest, + ) diff --git a/tests/test_adr_0148_vault_promotion.py b/tests/test_adr_0148_vault_promotion.py index db1a3d77..48682087 100644 --- a/tests/test_adr_0148_vault_promotion.py +++ b/tests/test_adr_0148_vault_promotion.py @@ -97,6 +97,9 @@ def test_promote_eligible_entries_promotes_coherent_entry() -> None: assert vault._metadata[0]["epistemic_status"] == EpistemicStatus.COHERENT.value, ( "Entry should be promoted to COHERENT" ) + # Consistency fix shipped with ADR-0218 PR C: the stored state tag is + # updated alongside the status, so the stamped pair never goes stale. + assert vault._metadata[0]["epistemic_state"] == "decoded" # --------------------------------------------------------------------------- diff --git a/tests/test_adr_0218_proof_promotion.py b/tests/test_adr_0218_proof_promotion.py new file mode 100644 index 00000000..c1048499 --- /dev/null +++ b/tests/test_adr_0218_proof_promotion.py @@ -0,0 +1,689 @@ +"""ADR-0218 P3 — proof-carrying coherence promotion: decider + transition owner. + +Covers the ratified admissibility predicate end-to-end: + +- the pure decider (``teaching/proof_promotion.py``) — fresh-read premises, + strict status/reading gates, engine certification, proposer payload + provably unread, certificate digest emission, zero mutation; +- the single mutation owner (``VaultStore.apply_certified_promotion``) — + independent re-verification (replay + pin + live store cross-checks), + staleness refusals, tamper refusals, idempotency; +- the structural guarantees — no parallel learning path (the promoter has + zero status-write sites and zero vault-store calls, proven with the + INV-21/INV-29 detectors themselves), and the engine pin stays in sync + with the deductive-lane registry. + +Wrong=0 framing: every refusal path here is an input class that COULD have +admitted a bad promotion; each test pins the refusal so a later change that +weakens a gate fails loudly. +""" + +from __future__ import annotations + +import ast +import dataclasses +import hashlib +from pathlib import Path + +import numpy as np +import pytest + +from algebra.cga import embed_point +from generate.proof_chain import Entailment, evaluate_entailment_with_trace +from generate.proof_chain.certificate import ( + PremiseRecord, + build_certificate, +) +from generate.proof_chain.engine_pin import DEDUCTIVE_ENGINE_PIN +from teaching import proof_promotion +from teaching.epistemic import EpistemicStatus +from vault.store import CERTIFIED_PROMOTION_REASONS, VaultStore + +_REPO_ROOT = Path(__file__).resolve().parent.parent + + +# --------------------------------------------------------------------------- +# Helpers +# --------------------------------------------------------------------------- + +def _versor(seed: int) -> np.ndarray: + rng = np.random.default_rng(seed) + return embed_point(rng.standard_normal(3).astype(np.float32)) + + +def _store( + vault: VaultStore, + seed: int, + form: str, + status: EpistemicStatus, + *, + certified: object = True, + include_form: bool = True, +) -> int: + metadata: dict = {"reading_certified": certified} + if include_form: + metadata["propositional_form"] = form + return vault.store(_versor(seed), metadata, epistemic_status=status) + + +def _coherent_premises(vault: VaultStore, *forms: str) -> tuple[int, ...]: + return tuple( + _store(vault, 100 + i, form, EpistemicStatus.COHERENT) + for i, form in enumerate(forms) + ) + + +def _speculative_claim(vault: VaultStore, form: str, **kwargs) -> int: + return _store(vault, 7, form, EpistemicStatus.SPECULATIVE, **kwargs) + + +def _statuses(vault: VaultStore) -> list[str]: + return [meta["epistemic_status"] for _, meta in vault.iter_metadata()] + + +class _PoisonedPayload(dict): + """A proposer payload that detonates on ANY read — proves D3.5's + "ignored completely" rather than merely "did not change the outcome".""" + + def _boom(self, *args, **kwargs): + raise AssertionError( + "certify_promotion read the proposer payload — D3.5 violated" + ) + + __getitem__ = _boom + __iter__ = _boom + __len__ = _boom + __contains__ = _boom + get = _boom + keys = _boom + values = _boom + items = _boom + + +# --------------------------------------------------------------------------- +# The positive path +# --------------------------------------------------------------------------- + +def test_entailed_from_coherent_promotes_end_to_end() -> None: + vault = VaultStore(reproject_interval=0) + idx_p, idx_pq = _coherent_premises(vault, "p", "p -> q") + idx_q = _speculative_claim(vault, "q") + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is True + assert decision.reason == proof_promotion.PROMOTED_ENTAILED + assert decision.certificate is not None + assert decision.certificate_digest == hashlib.sha256( + decision.certificate.canonical_json().encode("utf-8") + ).hexdigest() + + result = vault.apply_certified_promotion(idx_q, decision.certificate) + assert result.applied is True and result.reason == "applied" + + claim_meta = dict(vault.iter_metadata())[idx_q] + assert claim_meta["epistemic_status"] == EpistemicStatus.COHERENT.value + assert claim_meta["epistemic_state"] == "decoded" + assert claim_meta["promotion_certificate_digest"] == decision.certificate_digest + + # The promoted claim is now admissible as evidence on the read side. + hits = vault.recall( + vault._versors[idx_q], top_k=3, min_status=EpistemicStatus.COHERENT + ) + assert any(hit["index"] == idx_q for hit in hits) + + +def test_certify_alone_never_mutates() -> None: + """The decider is pure: a promoted=True decision changes no store state + until the vault owner applies it — no parallel mutation path.""" + vault = VaultStore(reproject_interval=0) + idx_p, idx_pq = _coherent_premises(vault, "p", "p -> q") + idx_q = _speculative_claim(vault, "q") + before = _statuses(vault) + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is True + assert _statuses(vault) == before + + +def test_decision_is_deterministic_and_digest_stable() -> None: + def run() -> proof_promotion.PromotionDecision: + vault = VaultStore(reproject_interval=0) + idx_p, idx_pq = _coherent_premises(vault, "p", "p -> q") + idx_q = _speculative_claim(vault, "q") + return proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + + first, second = run(), run() + assert first.certificate is not None and second.certificate is not None + assert first.certificate.canonical_json() == second.certificate.canonical_json() + assert first.certificate_digest == second.certificate_digest + + +# --------------------------------------------------------------------------- +# Engine outcomes that never promote +# --------------------------------------------------------------------------- + +def test_consistent_but_not_entailed_stays_speculative() -> None: + vault = VaultStore(reproject_interval=0) + (idx_p,) = _coherent_premises(vault, "p") + idx_q = _speculative_claim(vault, "q") + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p,), + vault=vault, + ) + assert decision.promoted is False + assert decision.reason == proof_promotion.REFUSED_NOT_ENTAILED + assert decision.certificate is not None + assert decision.certificate.decision == Entailment.UNKNOWN.value + + result = vault.apply_certified_promotion(idx_q, decision.certificate) + assert result.applied is False + assert result.reason == "certificate_not_promotion_positive" + assert _statuses(vault)[idx_q] == EpistemicStatus.SPECULATIVE.value + + +def test_refuted_never_promotes_and_never_demotes() -> None: + vault = VaultStore(reproject_interval=0) + idx_p, idx_pnq = _coherent_premises(vault, "p", "p -> ~q") + idx_q = _speculative_claim(vault, "q") + before = _statuses(vault) + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pnq), + vault=vault, + ) + assert decision.promoted is False + assert decision.certificate is not None + assert decision.certificate.decision == Entailment.REFUTED.value + + result = vault.apply_certified_promotion(idx_q, decision.certificate) + assert result.applied is False + # No transition in EITHER direction: refutation is not demotion authority + # (ADR-0218 open item) and certainly not promotion. + assert _statuses(vault) == before + + +def test_inconsistent_coherent_premises_refuse_never_vacuously_entail() -> None: + """Two individually-COHERENT entries can still be mutually inconsistent; + the engine refuses (everything follows from ⊥) rather than promoting.""" + vault = VaultStore(reproject_interval=0) + idx_p, idx_np = _coherent_premises(vault, "p", "~p") + idx_q = _speculative_claim(vault, "q") + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_np), + vault=vault, + ) + assert decision.promoted is False + assert decision.certificate is not None + assert decision.certificate.decision == Entailment.REFUSED.value + assert vault.apply_certified_promotion(idx_q, decision.certificate).applied is False + + +# --------------------------------------------------------------------------- +# Store-state gates at certify time +# --------------------------------------------------------------------------- + +@pytest.mark.parametrize( + "bad_status", + [EpistemicStatus.SPECULATIVE, EpistemicStatus.CONTESTED, EpistemicStatus.FALSIFIED], +) +def test_any_non_coherent_premise_refuses(bad_status: EpistemicStatus) -> None: + vault = VaultStore(reproject_interval=0) + (idx_p,) = _coherent_premises(vault, "p") + idx_pq = _store(vault, 2, "p -> q", bad_status) + idx_q = _speculative_claim(vault, "q") + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is False + assert decision.reason == proof_promotion.REFUSED_PREMISE_NOT_COHERENT + assert decision.certificate is None # refused before the engine ran + + +@pytest.mark.parametrize("bad_index", [99, -1, True]) +def test_missing_premise_entry_refuses(bad_index: object) -> None: + vault = VaultStore(reproject_interval=0) + (idx_p,) = _coherent_premises(vault, "p") + idx_q = _speculative_claim(vault, "q") + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, bad_index), # type: ignore[arg-type] + vault=vault, + ) + assert decision.promoted is False + assert decision.reason in { + proof_promotion.REFUSED_PREMISE_MISSING, + proof_promotion.REFUSED_MALFORMED_INPUT, + } + + +def test_missing_claim_entry_refuses() -> None: + vault = VaultStore(reproject_interval=0) + (idx_p,) = _coherent_premises(vault, "p") + + decision = proof_promotion.certify_promotion( + claim_entry_index=42, + premise_entry_indices=(idx_p,), + vault=vault, + ) + assert decision.promoted is False + assert decision.reason == proof_promotion.REFUSED_CLAIM_MISSING + + +@pytest.mark.parametrize( + "claim_status", + [EpistemicStatus.COHERENT, EpistemicStatus.CONTESTED, EpistemicStatus.FALSIFIED], +) +def test_claim_not_speculative_refuses(claim_status: EpistemicStatus) -> None: + """Only SPECULATIVE→COHERENT is authorized; an already-transitioned + claim refuses (this is also the idempotency guard).""" + vault = VaultStore(reproject_interval=0) + idx_p, idx_pq = _coherent_premises(vault, "p", "p -> q") + idx_q = _store(vault, 7, "q", claim_status) + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is False + assert decision.reason == proof_promotion.REFUSED_CLAIM_NOT_SPECULATIVE + + +@pytest.mark.parametrize("bad_certified", [False, 1, "yes", None]) +def test_uncertified_premise_reading_refuses(bad_certified: object) -> None: + """reading_certified must be the boolean True — truthy stand-ins are not + curator certifications (D2 fail-closed).""" + vault = VaultStore(reproject_interval=0) + (idx_p,) = _coherent_premises(vault, "p") + idx_pq = _store( + vault, 2, "p -> q", EpistemicStatus.COHERENT, certified=bad_certified + ) + idx_q = _speculative_claim(vault, "q") + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is False + assert decision.reason == proof_promotion.REFUSED_PREMISE_READING + + +def test_uncertified_or_formless_claim_refuses() -> None: + vault = VaultStore(reproject_interval=0) + idx_p, idx_pq = _coherent_premises(vault, "p", "p -> q") + + idx_uncertified = _store( + vault, 7, "q", EpistemicStatus.SPECULATIVE, certified=False + ) + idx_formless = _store( + vault, 8, "q", EpistemicStatus.SPECULATIVE, include_form=False + ) + for idx in (idx_uncertified, idx_formless): + decision = proof_promotion.certify_promotion( + claim_entry_index=idx, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is False + assert decision.reason == proof_promotion.REFUSED_CLAIM_READING + + +def test_zero_and_duplicate_premises_refuse() -> None: + vault = VaultStore(reproject_interval=0) + (idx_p,) = _coherent_premises(vault, "p") + idx_q = _speculative_claim(vault, "q | ~q") # a tautology claim + + empty = proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(), vault=vault + ) + assert empty.promoted is False + assert empty.reason == proof_promotion.REFUSED_NO_PREMISES + + dup = proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(idx_p, idx_p), vault=vault + ) + assert dup.promoted is False + assert dup.reason == proof_promotion.REFUSED_DUPLICATE_PREMISES + + +def test_claim_cannot_be_its_own_premise() -> None: + """p ⊨ p, but the claim must be SPECULATIVE and every premise COHERENT — + one entry cannot be both, so self-promotion is structurally refused.""" + vault = VaultStore(reproject_interval=0) + idx_q = _speculative_claim(vault, "q") + + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_q,), + vault=vault, + ) + assert decision.promoted is False + assert decision.reason == proof_promotion.REFUSED_PREMISE_NOT_COHERENT + + +# --------------------------------------------------------------------------- +# Proposer attachments are data, never authority (D3.5) +# --------------------------------------------------------------------------- + +def test_proposer_payload_is_never_read_and_never_changes_the_decision() -> None: + vault = VaultStore(reproject_interval=0) + idx_p, idx_pq = _coherent_premises(vault, "p", "p -> q") + idx_q = _speculative_claim(vault, "q") + + bare = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + adorned = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + proposer_payload=_PoisonedPayload(), # raises on ANY read + ) + assert bare.promoted is adorned.promoted is True + assert bare.certificate is not None and adorned.certificate is not None + assert bare.certificate.canonical_json() == adorned.certificate.canonical_json() + + +def test_no_source_trust_fast_path_for_refused_claims() -> None: + """A proposer asserting proof/status/confidence cannot rescue a + non-entailed claim — the refusal is byte-identical.""" + vault = VaultStore(reproject_interval=0) + (idx_p,) = _coherent_premises(vault, "p") + idx_q = _speculative_claim(vault, "q") + + bare = proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(idx_p,), vault=vault + ) + adorned = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p,), + vault=vault, + proposer_payload={ + "proof": "trust me, q follows", + "status": "coherent", + "confidence": 0.99, + "propositional_form": "p", # a lie about the claim form + }, + ) + assert bare.promoted is adorned.promoted is False + assert bare.certificate is not None and adorned.certificate is not None + assert bare.certificate.canonical_json() == adorned.certificate.canonical_json() + # The certificate's claim form is the STORED certified reading. + assert bare.certificate.claim_form == "q" + + +# --------------------------------------------------------------------------- +# The mutation owner re-verifies independently +# --------------------------------------------------------------------------- + +def _certified_decision(vault: VaultStore) -> proof_promotion.PromotionDecision: + idx_p, idx_pq = _coherent_premises(vault, "p", "p -> q") + idx_q = _speculative_claim(vault, "q") + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is True and decision.certificate is not None + return decision + + +def test_tampered_certificate_refused_at_apply() -> None: + vault = VaultStore(reproject_interval=0) + decision = _certified_decision(vault) + assert decision.certificate is not None + before = _statuses(vault) + + forged_decision = dataclasses.replace(decision.certificate, claim_form="r") + swapped_trace = dataclasses.replace( + decision.certificate, + entailment_trace=evaluate_entailment_with_trace(("p",), "p").as_dict(), + ) + for tampered in (forged_decision, swapped_trace): + result = vault.apply_certified_promotion( + decision.claim_entry_index, tampered + ) + assert result.applied is False + assert result.reason == "certificate_replay_failed" + + # Statuses are caller-recorded data carried verbatim through rebuild, so + # a status tamper yields an internally CONSISTENT certificate: it passes + # replay and is refused by the promotion_positive gate instead. + demoted_status = dataclasses.replace( + decision.certificate, premise_statuses=("coherent", "speculative") + ) + result = vault.apply_certified_promotion( + decision.claim_entry_index, demoted_status + ) + assert result.applied is False + assert result.reason == "certificate_not_promotion_positive" + assert _statuses(vault) == before + + +def test_statuses_forged_to_coherent_cannot_beat_the_live_check() -> None: + """The dangerous tamper direction: recording 'coherent' for a premise + that is actually SPECULATIVE. The forged certificate is promotion- + positive and passes replay — the vault's fresh-read of the LIVE premise + status is what refuses it (live state is the authority, D3.1).""" + vault = VaultStore(reproject_interval=0) + (idx_p,) = _coherent_premises(vault, "p") + idx_pq = _store(vault, 2, "p -> q", EpistemicStatus.SPECULATIVE) + idx_q = _speculative_claim(vault, "q") + + forged = build_certificate( + claim_form="q", + premises=( + PremiseRecord(entry_id=idx_p, form="p", status="coherent"), + PremiseRecord(entry_id=idx_pq, form="p -> q", status="coherent"), + ), + engine_pin=DEDUCTIVE_ENGINE_PIN, + ) + assert forged.promotion_positive is True # the artifact LOOKS promotable + result = vault.apply_certified_promotion(idx_q, forged) + assert result.applied is False and result.reason == "premise_not_coherent" + assert _statuses(vault)[idx_q] == EpistemicStatus.SPECULATIVE.value + + +def test_non_certificate_object_refused_at_apply() -> None: + vault = VaultStore(reproject_interval=0) + decision = _certified_decision(vault) + result = vault.apply_certified_promotion( + decision.claim_entry_index, {"decision": "entailed"} # type: ignore[arg-type] + ) + assert result.applied is False and result.reason == "not_a_certificate" + + +def test_wrong_engine_pin_refused_at_apply() -> None: + """A certificate from a different engine build replays internally but + fails the vault's pin demand — engine drift is an alarm, not a pass.""" + vault = VaultStore(reproject_interval=0) + idx_p, idx_pq = _coherent_premises(vault, "p", "p -> q") + idx_q = _speculative_claim(vault, "q") + + stale_pin_cert = build_certificate( + claim_form="q", + premises=( + PremiseRecord(entry_id=idx_p, form="p", status="coherent"), + PremiseRecord(entry_id=idx_pq, form="p -> q", status="coherent"), + ), + engine_pin="sha-of-some-other-engine-build", + ) + result = vault.apply_certified_promotion(idx_q, stale_pin_cert) + assert result.applied is False and result.reason == "certificate_replay_failed" + assert _statuses(vault)[idx_q] == EpistemicStatus.SPECULATIVE.value + + +def test_fabricated_certificate_over_unstored_forms_cannot_flip() -> None: + """A valid, replay-passing certificate whose premises the store does NOT + hold as certified-COHERENT entries mutates nothing — authority is live + store state, never the artifact.""" + vault = VaultStore(reproject_interval=0) + idx_q = _speculative_claim(vault, "q") + + fabricated = build_certificate( + claim_form="q", + premises=( + PremiseRecord(entry_id=5, form="q", status="coherent"), + ), + engine_pin=DEDUCTIVE_ENGINE_PIN, + ) + assert fabricated.promotion_positive is True # the artifact LOOKS perfect + result = vault.apply_certified_promotion(idx_q, fabricated) + assert result.applied is False and result.reason == "premise_entry_missing" + assert _statuses(vault)[idx_q] == EpistemicStatus.SPECULATIVE.value + + +def test_stale_premise_status_refuses_at_apply() -> None: + """A premise contested between certify and apply poisons the proof — + fresh-read at the mutation boundary, not just at decision time.""" + vault = VaultStore(reproject_interval=0) + decision = _certified_decision(vault) + assert decision.certificate is not None + + premise_idx = decision.certificate.premise_entry_ids[0] + vault._metadata[premise_idx]["epistemic_status"] = ( + EpistemicStatus.CONTESTED.value + ) + + result = vault.apply_certified_promotion( + decision.claim_entry_index, decision.certificate + ) + assert result.applied is False and result.reason == "premise_not_coherent" + assert ( + _statuses(vault)[decision.claim_entry_index] + == EpistemicStatus.SPECULATIVE.value + ) + + +def test_stale_premise_form_refuses_at_apply() -> None: + vault = VaultStore(reproject_interval=0) + decision = _certified_decision(vault) + assert decision.certificate is not None + + premise_idx = decision.certificate.premise_entry_ids[0] + vault._metadata[premise_idx]["propositional_form"] = "p & r" + + result = vault.apply_certified_promotion( + decision.claim_entry_index, decision.certificate + ) + assert result.applied is False and result.reason == "premise_form_mismatch" + + +def test_stale_claim_refuses_at_apply() -> None: + vault = VaultStore(reproject_interval=0) + decision = _certified_decision(vault) + assert decision.certificate is not None + claim_idx = decision.claim_entry_index + + # Re-applying after a successful promotion refuses (no double transition). + assert vault.apply_certified_promotion(claim_idx, decision.certificate).applied + second = vault.apply_certified_promotion(claim_idx, decision.certificate) + assert second.applied is False and second.reason == "claim_not_speculative" + + +def test_claim_form_mismatch_refuses_at_apply() -> None: + """Pointing a legitimate certificate at a different entry refuses — the + stored certified reading must equal the certified claim form.""" + vault = VaultStore(reproject_interval=0) + decision = _certified_decision(vault) + assert decision.certificate is not None + idx_other = _store(vault, 9, "r", EpistemicStatus.SPECULATIVE) + + result = vault.apply_certified_promotion(idx_other, decision.certificate) + assert result.applied is False and result.reason == "claim_form_mismatch" + assert _statuses(vault)[idx_other] == EpistemicStatus.SPECULATIVE.value + + +@pytest.mark.parametrize("bad_index", [99, -1, True]) +def test_apply_with_bad_entry_index_refuses(bad_index: object) -> None: + vault = VaultStore(reproject_interval=0) + decision = _certified_decision(vault) + assert decision.certificate is not None + result = vault.apply_certified_promotion( + bad_index, decision.certificate # type: ignore[arg-type] + ) + assert result.applied is False and result.reason == "claim_entry_missing" + + +# --------------------------------------------------------------------------- +# Structural guarantees — no parallel path, closed vocabs, pin sync +# --------------------------------------------------------------------------- + +def test_promoter_module_is_pure_no_status_writes_no_vault_store_calls() -> None: + """No parallel learning path: the INV-29 status-write detector and the + INV-21 vault-store-call detector both report zero on the promoter.""" + from tests.test_architectural_invariants import ( + _file_has_vault_store_call, + _status_transition_writes, + ) + + promoter_path = _REPO_ROOT / "teaching" / "proof_promotion.py" + tree = ast.parse(promoter_path.read_text()) + assert _status_transition_writes(tree) == 0 + assert _file_has_vault_store_call(promoter_path) is False + + +def test_decision_reasons_are_closed_vocabularies() -> None: + assert proof_promotion.PROMOTED_ENTAILED in proof_promotion.DECISION_REASONS + assert len(proof_promotion.DECISION_REASONS) == 12 + assert "applied" in CERTIFIED_PROMOTION_REASONS + assert len(CERTIFIED_PROMOTION_REASONS) == 12 + + +def test_engine_pin_matches_lane_registry() -> None: + """DEDUCTIVE_ENGINE_PIN mirrors scripts/verify_lane_shas.py — AST-parsed + so the runtime never imports scripts/. Drift between the lane registry + and the promotion pin fails here, in the same suite that gates merges.""" + registry = _REPO_ROOT / "scripts" / "verify_lane_shas.py" + tree = ast.parse(registry.read_text()) + pinned: dict[str, str] = {} + for node in ast.walk(tree): + if isinstance(node, ast.AnnAssign) and isinstance(node.target, ast.Name): + if node.target.id == "PINNED_SHAS" and isinstance(node.value, ast.Dict): + for key, value in zip(node.value.keys, node.value.values): + if isinstance(key, ast.Constant) and isinstance(value, ast.Constant): + pinned[key.value] = value.value + assert "deductive_logic_v1" in pinned, "lane registry shape changed" + assert DEDUCTIVE_ENGINE_PIN == pinned["deductive_logic_v1"], ( + "generate/proof_chain/engine_pin.py is out of sync with " + "scripts/verify_lane_shas.py — update the constant in the same commit " + "as the lane re-pin." + ) + + +def test_adr_0148_promotion_keeps_epistemic_state_consistent() -> None: + """Consistency fix shipped with PR C: BOTH promotion sites stamp + epistemic_state alongside epistemic_status (the stored key must not go + stale even though recall recomputes it).""" + vault = VaultStore(reproject_interval=0) + decision = _certified_decision(vault) + assert decision.certificate is not None + assert vault.apply_certified_promotion( + decision.claim_entry_index, decision.certificate + ).applied + meta = vault._metadata[decision.claim_entry_index] + assert meta["epistemic_state"] == "decoded" diff --git a/tests/test_architectural_invariants.py b/tests/test_architectural_invariants.py index 49cea70a..cfcaa8c3 100644 --- a/tests/test_architectural_invariants.py +++ b/tests/test_architectural_invariants.py @@ -1742,13 +1742,14 @@ class TestINV28MeaningGraphNeutrality: # document the justification here in the same commit. # # Allowlist rationale per site: -# vault/store.py — the single mutation owner. Two sites today: +# vault/store.py — the single mutation owner. Three sites today: # store() stamping at write time (param-only; callers -# cannot smuggle status via the metadata dict), and -# ADR-0148 promote_eligible_entries (energy-policy -# promotion, opt-in flag, default off). ADR-0218 proposes -# its proof-carrying transition land HERE too -# (apply_certified_promotion), keeping this list unchanged. +# cannot smuggle status via the metadata dict), ADR-0148 +# promote_eligible_entries (energy-policy promotion, +# opt-in flag, default off), and ADR-0218 (ratified +# 2026-06-11) apply_certified_promotion (proof-carrying +# promotion, independent re-verification before the flip). +# The list stays unchanged: all three live HERE. ALLOWED_STATUS_TRANSITION_SITES: frozenset[str] = frozenset({ "vault/store.py", @@ -1967,11 +1968,13 @@ class TestINV29EpistemicStatusTransitionSites: ) def test_vault_store_sites_are_visible(self): - """29c — the scan actually sees the two known vault/store.py sites - (store-time stamp + ADR-0148 promotion). If this drops to zero the - scan went blind, not clean.""" + """29c — the scan actually sees the three known vault/store.py sites + (store-time stamp + ADR-0148 promotion + ADR-0218 certified + promotion). If this drops below three the scan went blind, not + clean.""" vault_path = PROJECT_ROOT_FOR_INV21 / "vault" / "store.py" - assert _file_status_transition_count(vault_path) >= 2, ( - "Expected the store() stamp and the ADR-0148 promotion site in " + assert _file_status_transition_count(vault_path) >= 3, ( + "Expected the store() stamp, the ADR-0148 promotion site, and " + "the ADR-0218 apply_certified_promotion site in " "vault/store.py to be visible to the INV-29 scan." ) diff --git a/tests/test_proof_carrying_promotion_obligations.py b/tests/test_proof_carrying_promotion_obligations.py index 8d5eba5a..3ec05b7b 100644 --- a/tests/test_proof_carrying_promotion_obligations.py +++ b/tests/test_proof_carrying_promotion_obligations.py @@ -1,75 +1,52 @@ -"""ADR-0218 PR A — executable proof obligations for proof-carrying coherence -promotion. THE FEATURE IS NOT LIVE. +"""ADR-0218 — executable proof obligations for proof-carrying coherence +promotion. THE OBLIGATIONS ARE LIVE: ADR-0218 was ratified 2026-06-11 and +P3 landed (`teaching/proof_promotion.py` + `VaultStore.apply_certified_promotion`), +so every former strict-xfail marker in this file is retired and each +obligation now passes on its own. -Two kinds of tests, per the strict-xfail gate convention -(see tests/test_edge_budget_gate.py): +Retirement record (PR C): -- HONESTY PINS (pass today). They assert the *current* truth the governing - issue documents: promotion is not computed, the promoter module does not - exist, and the entailment substrate the future promoter will consume is - replay-stable. The moment someone wires promotion without consciously - revisiting this file, a pin flips red. - -- OBLIGATIONS O1–O5, O7 (xfail today, strict). Executable spec for the - ADR-0218 P3 promoter (`teaching/proof_promotion.py`). Each body imports - the not-yet-existing module, so today they xfail on ImportError. When P3 - lands, strict=True turns any still-marked passing test into a loud XPASS - failure — the P3 PR must retire the markers and make every obligation pass - for real. A test that passes under a broken implementation is decoration - (CLAUDE.md §Schema-Defined Proof Obligations); these cannot pass at all - until the implementation exists. +- `test_pin_promoter_module_does_not_exist_yet` is DELETED per its own + docstring — the promoter module now exists, consciously. +- The remaining two honesty pins still pass and still guard what they always + guarded: `review_correction` carries status as an input (promotion did NOT + fork into a parallel path there), and the entailment substrate is + replay-stable. +- O1–O5/O7 bodies were adjusted from the PR-A provisional API + (`claim_form=...`) to the ratified surface (`claim_entry_index=...`), + sanctioned by PR A's provisional-API note and ratified D3 note (a): the + claim form is fresh-read from the claim's own stored entry — forms come + from the store, never from the proposer. Each obligation's semantics are + preserved and O1/O2 are strengthened to prove the transition (or its + absence) through the single mutation owner. O6 (no new mutation path) is enforced continuously by INV-21 + INV-29 in tests/test_architectural_invariants.py, not here. O8 (wrong=0 lanes) is -enforced by the existing lane gates + scripts/verify_lane_shas.py. - -PR B note: the certificate-substrate halves of O1/O7 (replay re-verification, -byte-stable determinism) are now proven for real in -tests/test_proof_chain_certificate.py against -generate/proof_chain/certificate.py. NO xfail marker retires here — every -obligation below binds to the P3 promoter (`teaching.proof_promotion`), which -must not exist before ADR-0218 is ratified. - -API surface used in the xfail bodies is PROVISIONAL per ADR-0218 §D3/§D4 — -P3 may adjust signatures, but must preserve each obligation's semantics. +enforced by the existing lane gates + scripts/verify_lane_shas.py. The +exhaustive P3 suite (staleness, tamper, pin drift, structural purity) is +tests/test_adr_0218_proof_promotion.py. """ from __future__ import annotations -import importlib -import importlib.util - import numpy as np -import pytest from algebra.cga import embed_point from generate.intent import DialogueIntent, IntentTag from generate.proof_chain import Entailment, evaluate_entailment_with_trace +from teaching import proof_promotion from teaching.correction import CorrectionCandidate from teaching.epistemic import EpistemicStatus from teaching.review import review_correction from vault.store import VaultStore -_PROMOTER_MODULE = "teaching.proof_promotion" - -_XFAIL_REASON = ( - "ADR-0218 is Proposed, not ratified — the proof-carrying promoter " - f"({_PROMOTER_MODULE}) does not exist. This test is the executable " - "obligation; the P3 PR must retire this marker and make it pass." -) - - -def _promoter(): - """Import the future promoter. Raises ModuleNotFoundError today (→ xfail).""" - return importlib.import_module(_PROMOTER_MODULE) - def _versor(seed: int) -> np.ndarray: rng = np.random.default_rng(seed) return embed_point(rng.standard_normal(3).astype(np.float32)) -def _store_premise( +def _store_entry( vault: VaultStore, seed: int, form: str, @@ -77,7 +54,7 @@ def _store_premise( *, certified: bool = True, ) -> int: - """Store a premise entry carrying a curator-certified reading (ADR-0218 §D2).""" + """Store an entry carrying a curator-certified reading (ADR-0218 §D2).""" return vault.store( _versor(seed), { @@ -88,27 +65,19 @@ def _store_premise( ) -# --------------------------------------------------------------------------- -# Honesty pins — pass today, flip red when reality changes -# --------------------------------------------------------------------------- +def _status_of(vault: VaultStore, index: int) -> str: + return dict(vault.iter_metadata())[index]["epistemic_status"] -def test_pin_promoter_module_does_not_exist_yet() -> None: - """The feature is designed-but-unwired. This pin goes red in the same PR - that creates the module, forcing the xfail markers below to be revisited - (and this pin deleted) consciously rather than by drift.""" - assert importlib.util.find_spec(_PROMOTER_MODULE) is None, ( - f"{_PROMOTER_MODULE} now exists — ADR-0218 P3 is landing. Delete this " - "pin AND retire every xfail marker in this file in the same PR; each " - "obligation below must now pass on its own." - ) +# --------------------------------------------------------------------------- +# Honesty pins — still true, still load-bearing +# --------------------------------------------------------------------------- def test_pin_review_correction_carries_status_it_does_not_compute() -> None: """Issue §1: `epistemic_status` is a passed-in parameter of - review_correction, not a computed coherence judgment. If a coherence - computation is ever added there, this pin flips and the change must be - reconciled with ADR-0218 (which routes computed promotion through the - vault transition owner, NOT through review_correction).""" + review_correction, not a computed coherence judgment. ADR-0218 routed + computed promotion through the vault transition owner, NOT through + review_correction — this pin proves the path did not fork.""" candidate = CorrectionCandidate( correction_text="the sky is blue", intent=DialogueIntent(tag=IntentTag.CORRECTION, subject="sky"), @@ -129,17 +98,16 @@ def test_pin_review_correction_carries_status_it_does_not_compute() -> None: def test_pin_entailment_trace_substrate_is_replay_stable() -> None: - """O7's substrate half, testable today: the engine's proof evidence is - deterministic and re-verifies by recomputation — the property the - PromotionCertificate replay verifier (PR B, - generate/proof_chain/certificate.py — landed) relies on.""" + """O7's substrate half: the engine's proof evidence is deterministic and + re-verifies by recomputation — the property the PromotionCertificate + replay verifier relies on.""" premises = ("p", "p -> q") first = evaluate_entailment_with_trace(premises, "q") second = evaluate_entailment_with_trace(premises, "q") assert first.outcome is Entailment.ENTAILED assert first.canonical_json() == second.canonical_json(), ( - "EntailmentTrace is not replay-stable — PR B's certificate " - "re-verification has no substrate to stand on." + "EntailmentTrace is not replay-stable — certificate re-verification " + "has no substrate to stand on." ) # A non-entailed query must be UNKNOWN, not promoted-shaped evidence. @@ -148,58 +116,66 @@ def test_pin_entailment_trace_substrate_is_replay_stable() -> None: # --------------------------------------------------------------------------- -# Obligations — xfail(strict) until ADR-0218 is ratified and P3 lands +# Obligations — live since ADR-0218 ratification + P3 # --------------------------------------------------------------------------- -@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON) def test_O1_entailed_from_coherent_premises_promotes_with_reverifiable_proof() -> None: """Issue §7.1 — a claim deductively entailed by an all-COHERENT premise - set promotes, and the embedded proof re-verifies by recomputation.""" - mod = _promoter() + set promotes (through the single mutation owner), and the embedded proof + re-verifies by recomputation.""" vault = VaultStore(reproject_interval=0) - idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT) - idx_pq = _store_premise(vault, 2, "p -> q", EpistemicStatus.COHERENT) + idx_p = _store_entry(vault, 1, "p", EpistemicStatus.COHERENT) + idx_pq = _store_entry(vault, 2, "p -> q", EpistemicStatus.COHERENT) + idx_q = _store_entry(vault, 3, "q", EpistemicStatus.SPECULATIVE) - decision = mod.certify_promotion( - claim_form="q", + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(idx_p, idx_pq), vault=vault, ) assert decision.promoted is True + assert decision.certificate is not None # Replay re-verification: recomputing from the stored forms must # reproduce the embedded trace byte-for-byte (ADR-0218 §D3.4). recomputed = evaluate_entailment_with_trace(("p", "p -> q"), "q") assert decision.certificate.entailment_trace == recomputed.as_dict() + # The transition itself happens only inside the vault owner. + result = vault.apply_certified_promotion(idx_q, decision.certificate) + assert result.applied is True + assert _status_of(vault, idx_q) == EpistemicStatus.COHERENT.value + -@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON) def test_O2_consistent_but_not_entailed_stays_speculative() -> None: """Issue §7.2 — mere consistency with the field is not entailment; - UNKNOWN never promotes.""" - mod = _promoter() + UNKNOWN never promotes, and the claim's stored status does not move.""" vault = VaultStore(reproject_interval=0) - idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT) + idx_p = _store_entry(vault, 1, "p", EpistemicStatus.COHERENT) + idx_q = _store_entry(vault, 3, "q", EpistemicStatus.SPECULATIVE) - decision = mod.certify_promotion( - claim_form="q", # consistent with {p}, not entailed by it + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(idx_p,), vault=vault, ) assert decision.promoted is False + assert decision.certificate is not None + result = vault.apply_certified_promotion(idx_q, decision.certificate) + assert result.applied is False + assert _status_of(vault, idx_q) == EpistemicStatus.SPECULATIVE.value -@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON) def test_O3_any_non_coherent_premise_refuses() -> None: """Issue §7.3 — a SPECULATIVE premise poisons the proof for promotion purposes even when the entailment itself is valid.""" - mod = _promoter() vault = VaultStore(reproject_interval=0) - idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT) - idx_pq = _store_premise(vault, 2, "p -> q", EpistemicStatus.SPECULATIVE) + idx_p = _store_entry(vault, 1, "p", EpistemicStatus.COHERENT) + idx_pq = _store_entry(vault, 2, "p -> q", EpistemicStatus.SPECULATIVE) + idx_q = _store_entry(vault, 3, "q", EpistemicStatus.SPECULATIVE) - decision = mod.certify_promotion( - claim_form="q", + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(idx_p, idx_pq), vault=vault, ) @@ -207,20 +183,19 @@ def test_O3_any_non_coherent_premise_refuses() -> None: assert "premise" in decision.reason # closed reason vocab names the gate -@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON) def test_O4_uncertified_reading_fails_closed() -> None: """Issue §7.4 — the reading is the hazard-bearing step. A premise whose propositional form lacks reading certification must refuse, never fall through to admission (ADR-0218 §D2).""" - mod = _promoter() vault = VaultStore(reproject_interval=0) - idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT) - idx_pq = _store_premise( + idx_p = _store_entry(vault, 1, "p", EpistemicStatus.COHERENT) + idx_pq = _store_entry( vault, 2, "p -> q", EpistemicStatus.COHERENT, certified=False ) + idx_q = _store_entry(vault, 3, "q", EpistemicStatus.SPECULATIVE) - decision = mod.certify_promotion( - claim_form="q", + decision = proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(idx_p, idx_pq), vault=vault, ) @@ -228,22 +203,21 @@ def test_O4_uncertified_reading_fails_closed() -> None: assert "reading" in decision.reason -@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON) def test_O5_proposer_supplied_proof_status_confidence_are_ignored() -> None: """Issue §7.5 — proposer attachments are data, never authority. The decision must be byte-identical with and without them (echo-and-ignore, as demos/epistemic_truth_state does for proposed_state).""" - mod = _promoter() vault = VaultStore(reproject_interval=0) - idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT) + idx_p = _store_entry(vault, 1, "p", EpistemicStatus.COHERENT) + idx_q = _store_entry(vault, 3, "q", EpistemicStatus.SPECULATIVE) - bare = mod.certify_promotion( - claim_form="q", + bare = proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(idx_p,), vault=vault, ) - adorned = mod.certify_promotion( - claim_form="q", + adorned = proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(idx_p,), vault=vault, proposer_payload={ @@ -253,24 +227,27 @@ def test_O5_proposer_supplied_proof_status_confidence_are_ignored() -> None: }, ) assert bare.promoted is adorned.promoted is False + assert bare.certificate is not None and adorned.certificate is not None assert bare.certificate.canonical_json() == adorned.certificate.canonical_json() -@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON) def test_O7_promotion_decision_is_deterministic_and_replayable() -> None: """Issue §7.7 — double-run byte-identical; the certificate is the audit - artifact replay re-verifies (its hash folds into trace_hash at P3).""" - mod = _promoter() + artifact replay re-verifies (its digest is emitted for trace-hash + folding at the first runtime caller).""" - def run(): + def run() -> proof_promotion.PromotionDecision: vault = VaultStore(reproject_interval=0) - idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT) - idx_pq = _store_premise(vault, 2, "p -> q", EpistemicStatus.COHERENT) - return mod.certify_promotion( - claim_form="q", + idx_p = _store_entry(vault, 1, "p", EpistemicStatus.COHERENT) + idx_pq = _store_entry(vault, 2, "p -> q", EpistemicStatus.COHERENT) + idx_q = _store_entry(vault, 3, "q", EpistemicStatus.SPECULATIVE) + return proof_promotion.certify_promotion( + claim_entry_index=idx_q, premise_entry_indices=(idx_p, idx_pq), vault=vault, ) first, second = run(), run() + assert first.certificate is not None and second.certificate is not None assert first.certificate.canonical_json() == second.certificate.canonical_json() + assert first.certificate_digest == second.certificate_digest diff --git a/vault/store.py b/vault/store.py index cdc06a99..ba974f00 100644 --- a/vault/store.py +++ b/vault/store.py @@ -13,6 +13,7 @@ O(N) np.array_equal scans. from __future__ import annotations from collections import deque +from dataclasses import dataclass from typing import TYPE_CHECKING import numpy as np @@ -25,6 +26,7 @@ from teaching.epistemic import ADMISSIBLE_AS_EVIDENCE, EpistemicStatus if TYPE_CHECKING: from core.physics.learning import VaultPromotionPolicy + from generate.proof_chain.certificate import PromotionCertificate # ADR-0006 §"Integration Points": @@ -123,6 +125,36 @@ def _status_admits(entry_status: EpistemicStatus, min_status: EpistemicStatus) - return entry_status is min_status +# ADR-0218 — closed reason vocabulary for apply_certified_promotion. Each +# refusal names the exact gate that fired; "applied" is the only positive. +CERTIFIED_PROMOTION_REASONS: frozenset[str] = frozenset({ + "applied", + "not_a_certificate", + "certificate_replay_failed", + "certificate_not_promotion_positive", + "claim_entry_missing", + "claim_form_mismatch", + "claim_reading_uncertified", + "claim_not_speculative", + "premise_entry_missing", + "premise_form_mismatch", + "premise_reading_uncertified", + "premise_not_coherent", +}) + + +@dataclass(frozen=True, slots=True) +class CertifiedPromotionResult: + """Outcome of one ``apply_certified_promotion`` call. + + ``applied`` is True iff the entry's status was flipped; ``reason`` is + drawn from ``CERTIFIED_PROMOTION_REASONS``. A refusal mutates nothing. + """ + + applied: bool + reason: str + + def _parse_entry_status(raw_status: object) -> EpistemicStatus: if isinstance(raw_status, EpistemicStatus): return raw_status @@ -373,9 +405,116 @@ class VaultStore: decision = policy.decide(energy) if decision.promote: meta["epistemic_status"] = EpistemicStatus.COHERENT.value + # Keep the stored state tag consistent with the status it was + # stamped beside at store() time (recall recomputes it on the + # fly, but the stored key must not go stale). + meta["epistemic_state"] = epistemic_state_for_vault_status( + EpistemicStatus.COHERENT + ).value promoted += 1 return promoted + def apply_certified_promotion( + self, + entry_index: int, + certificate: "PromotionCertificate", + ) -> CertifiedPromotionResult: + """Flip one SPECULATIVE entry to COHERENT iff its promotion + certificate independently re-verifies against the live store. + + ADR-0218 §D1: this is the proof-carrying transition's single mutation + site — the pure decider (``teaching/proof_promotion.py``) recommends, + this method **re-verifies everything itself** and trusts neither the + decider nor the certificate's provenance: + + 1. The certificate replay-verifies under the pinned engine + (byte-for-byte recomputation + ``DEDUCTIVE_ENGINE_PIN`` check) and + is promotion-positive (ENTAILED over a non-empty all-COHERENT + recorded premise set). + 2. The target entry's stored, curator-certified ``propositional_form`` + equals the certificate's claim form, and the entry is currently + SPECULATIVE (strict string compare — stale or already-transitioned + claims refuse). + 3. Every certificate premise re-resolves fresh: stored certified form + byte-equal to the certificate's, ``reading_certified is True``, and + current status COHERENT (a premise contested/falsified since + certification refuses — staleness is a refusal, not a race). + + Authority comes from live store state plus recomputation — a + fabricated certificate over forms the store does not actually hold as + certified COHERENT premises cannot flip anything. Any refusal + mutates nothing. + + Entry indices are live deque positions (see ``iter_metadata``); on a + bounded vault, eviction shifts indices, and the form/status + cross-checks above are what keep a shifted index from flipping a + different claim. Certified promotion is intended for the unbounded + tier (``max_entries=None``). + """ + # Lazy import, matching this module's Proposition/EnergyProfile + # precedent: keeps vault load time lean and load-order acyclic. + from generate.proof_chain.certificate import ( + PromotionCertificate as _Certificate, + verify_certificate as _verify_certificate, + ) + from generate.proof_chain.engine_pin import DEDUCTIVE_ENGINE_PIN + import hashlib as _hashlib + + if not isinstance(certificate, _Certificate): + return CertifiedPromotionResult(False, "not_a_certificate") + verification = _verify_certificate( + certificate, expected_engine_pin=DEDUCTIVE_ENGINE_PIN + ) + if not verification.verified: + return CertifiedPromotionResult(False, "certificate_replay_failed") + if not certificate.promotion_positive: + return CertifiedPromotionResult( + False, "certificate_not_promotion_positive" + ) + + if ( + isinstance(entry_index, bool) + or not isinstance(entry_index, int) + or not (0 <= entry_index < len(self._metadata)) + ): + return CertifiedPromotionResult(False, "claim_entry_missing") + claim_meta = self._metadata[entry_index] + if claim_meta.get("reading_certified") is not True: + return CertifiedPromotionResult(False, "claim_reading_uncertified") + if claim_meta.get("propositional_form") != certificate.claim_form: + return CertifiedPromotionResult(False, "claim_form_mismatch") + if claim_meta.get("epistemic_status") != EpistemicStatus.SPECULATIVE.value: + return CertifiedPromotionResult(False, "claim_not_speculative") + + for premise_id, premise_form in zip( + certificate.premise_entry_ids, certificate.premise_forms + ): + if not (0 <= premise_id < len(self._metadata)): + return CertifiedPromotionResult(False, "premise_entry_missing") + premise_meta = self._metadata[premise_id] + if premise_meta.get("reading_certified") is not True: + return CertifiedPromotionResult( + False, "premise_reading_uncertified" + ) + if premise_meta.get("propositional_form") != premise_form: + return CertifiedPromotionResult(False, "premise_form_mismatch") + if ( + premise_meta.get("epistemic_status") + != EpistemicStatus.COHERENT.value + ): + return CertifiedPromotionResult(False, "premise_not_coherent") + + claim_meta["epistemic_status"] = EpistemicStatus.COHERENT.value + claim_meta["epistemic_state"] = epistemic_state_for_vault_status( + EpistemicStatus.COHERENT + ).value + # D4 audit trail: the digest replay re-verifies (and, once a runtime + # caller exists, folds into the turn trace_hash). + claim_meta["promotion_certificate_digest"] = _hashlib.sha256( + certificate.canonical_json().encode("utf-8") + ).hexdigest() + return CertifiedPromotionResult(True, "applied") + def reproject(self) -> None: """ Re-project all stored versors onto the null cone.