diff --git a/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md b/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md new file mode 100644 index 00000000..76fe1b7c --- /dev/null +++ b/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md @@ -0,0 +1,211 @@ +# ADR-0218 — Proof-Carrying Coherence Promotion (logical arm of ADR-0021 v2) + +**Status:** Proposed — NOT ratified. No runtime mutation-path code is +authorized by this document. The PR that introduces this ADR ships only +(a) this proposal and (b) executable proof obligations +(`tests/test_proof_carrying_promotion_obligations.py`, strict-xfail) plus a +new structural invariant (INV-29) that pins the *current* promotion-site +surface before any new promoter exists. +**Date:** 2026-06-11 +**Authors:** drafted by agent for architect review (Joshua Shay ratifies) +**Governing issue:** [docs/issues/proof-carrying-coherence-promotion.md](../issues/proof-carrying-coherence-promotion.md) +**Depends on:** ADR-0021 (Epistemic Grade Policy), ADR-0201/0202 (ROBDD +canonicalizer + representation contract), ADR-0203/0204/0205 (proof_chain +phases 2.1–2.3), the propositional entailment operator +(`generate/proof_chain/entail.py`, phase 2.4 — see §Context numbering note), +ADR-0148 (vault promotion policy wiring), INV-21/22/23. + +--- + +## Context + +PR #691 corrected the doctrine: a system's own *asserted* output has no +standing, but a claim *deductively entailed* by an already-`COHERENT` +premise set can be machine-certified as a coherence judgment, because for +that subclass the entailment proof **is** the coherence judgment ADR-0021 §3 +requires. The governing issue specifies the capability; this ADR proposes +the rulings the issue (§9) demands before any code. + +### What exists today (verified 2026-06-11, main@187b008b) + +- **Sound + complete propositional engine.** + `generate/proof_chain/entail.py::evaluate_entailment_with_trace` decides + `premises ⊨ query` on the ADR-0201 ROBDD keystone. Refusal-first: + inconsistent premises and out-of-regime input refuse, never guess. +- **A deterministic proof-evidence artifact already exists.** + `EntailmentTrace` carries `premise_keys`, `conjunction_key`, `query_key`, + `entailment_check_key`, `refutation_check_key` and a `canonical_json()` + serialization. Replay re-verification = recompute from `(premises, query)` + and compare byte-for-byte. +- **proof_chain Phase 2 is NOT a pending prerequisite — it shipped.** + The issue (§5, §8 P2) treats binding-graph wiring, acyclicity refusal, and + modus_ponens as a prerequisite still to build. As of ADR-0203/0204/0205 + (all Accepted, 2026-06-02) plus the phase-2.4 entailment operator, all of + it is implemented and tested (`tests/test_proof_chain_*.py`, + `tests/test_deductive_logic_entail.py`, `evals/deductive_logic/` SHA-pinned + lane). What P2 still owes is narrower: a *promotion certificate* binding an + `EntailmentTrace` to concrete vault entries, plus its replay verifier. +- **Numbering note (cleanup owed, not done here):** the entail.py module + docstring attributes phase 2.4 to "ADR-0206", which collides with the + committed `ADR-0206-response-governance-bridge.md`. Phase 2.4 has no + committed ADR of its own. The PR that lands P2 must fix that docstring to + cite this ADR's §Interface instead. + +### The precedent the issue missed: ADR-0148 already automates a promotion + +`VaultStore.promote_eligible_entries(policy)` (ADR-0148, Accepted +2026-05-25) already flips `SPECULATIVE → COHERENT` **in place**, gated by an +energy/coherence-residual policy, called from `chat/runtime.py` behind +`RuntimeConfig.vault_promotion_enabled` (default `False`). Two consequences: + +1. "Promotion is curator-mediated today" is not strictly true — an + energy-arm precedent exists. This ADR positions the logical arm beside + it, not as the first automation. +2. **ADR-0148 exposed a blind spot in INV-21.** INV-21's AST scan catches + `*.store(...)` calls. An in-place `epistemic_status` metadata mutation is + *not* a `store()` call, so the most natural implementation shape for a + promoter — flip the status on an existing entry — would silently bypass + the one-mutation-path invariant as written. The issue names INV-21 as + "highest risk"; in fact INV-21 *cannot see* the riskiest shape. + **Therefore this proposal introduces INV-29 now** (status-transition + sites are allowlisted), in the same PR as this document, so the boundary + exists *before* any promoter does. + +## Decision (proposed — each item requires ratification) + +### D1. Extend the existing mutation owner; do not add a write path + +Promotion is an epistemic-status *transition*, not a new vault write. The +split mirrors ADR-0148's accepted shape — policy decides, vault mutates: + +- `teaching/proof_promotion.py` (new, P3): **pure decision logic.** Builds + and verifies the certificate; performs **no mutation** and holds no vault + write access. Not a parallel learning path: it produces a decision object + consumed by the single mutation owner. +- `vault/store.py` (existing INV-21/INV-29 allowlisted module): gains one + method, `apply_certified_promotion(entry_index, certificate)`, which + **independently re-verifies the certificate** (recompute the entailment + trace; compare byte-for-byte; re-check premise statuses) before flipping + the entry's status. A certificate that does not re-verify mutates nothing. + +No INV-21 allowlist change. INV-29's allowlist stays `{vault/store.py}`. + +### D2. The reading stays curator-mediated in the first cut + +The hazard-bearing step is the NL→proposition reading, not the deduction +(issue §4). P3 ships with: + +- Every premise's propositional form is a **curator-certified reading** + stored with the vault entry (`reading_certified: true` + the certified + form), never proposer-supplied at decision time. +- The candidate claim's propositional form is likewise a curator-certified + *reading* (certifying the translation is faithful certifies nothing about + the claim's coherence — that is exactly the relocation: human certifies + the reading, engine certifies the entailment). +- Any premise or claim without a certified reading → **refuse, no + promotion.** Fail-closed is the only failure mode. + +A structural (non-curator) reading check is future work and requires its own +ADR; it is out of scope here. + +### D3. Exact admissibility predicate + +`certify_promotion` promotes **iff all** of the following hold; any failure +refuses (claim stays `SPECULATIVE`): + +```text +1. Every premise ref resolves to a stored vault entry, fresh-read at + decision time, with epistemic_status == COHERENT. +2. Every premise form and the claim form are curator-certified readings + (D2); forms are taken from the store, never from the proposer. +3. evaluate_entailment_with_trace(premise_forms, claim_form).outcome + == ENTAILED. (REFUTED / UNKNOWN / REFUSED never promote.) +4. The embedded EntailmentTrace re-verifies: recomputing from the stored + forms reproduces canonical_json() byte-for-byte. +5. No proposer-supplied proof / status / confidence field is read by the + decision. (Echo-and-ignore, as demos/epistemic_truth_state does for + proposed_state.) +``` + +`REFUTED` does **not** auto-demote to `CONTESTED` in v1 — demotion is a +separate authority question, recorded as an open item, not smuggled in here. + +### D4. The certificate is the audit artifact and folds into the trace hash + +`PromotionCertificate` (provisional fields; the strict-xfail tests are the +executable spec and will be reconciled at P3): + +```text +claim_form — certified propositional form of the claim +premise_entry_ids — vault identities of the premises +premise_forms — certified forms, as read from the store +premise_statuses — statuses observed at decision time +entailment_trace — EntailmentTrace.as_dict() +engine_pin — the deductive_logic lane SHA in force +decision / reason — promoted | refused + closed reason vocab +``` + +The certificate's canonical JSON SHA-256 folds into the turn `trace_hash` +(ADR-0021 §Schema impact already requires status there). Replay re-verifies +the certificate, not just the status. + +## Phasing (maps to the PR stack) + +- **PR A (this PR).** This proposal + strict-xfail obligations + INV-29. + No runtime change. Obligation tests xfail today; INV-29 and the honesty + pins pass today. +- **PR B.** `PromotionCertificate` + builder + replay verifier as a pure, + side-effect-free module with its own tests. No promotion, no vault method, + no status transition anywhere. Retires the certificate-shaped xfails only. +- **PR C (requires this ADR ratified).** `certify_promotion` + + `VaultStore.apply_certified_promotion` behind the existing mutation owner. + Retires the remaining xfails (strict-xpass forces it); INV-21 allowlist + unchanged; INV-29 allowlist unchanged; full + deductive lanes wrong=0. +- **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 + effects outside the demo arena. + +## Proof obligations ↔ tests + +| # | Obligation (issue §7) | Test (PR A) | State today | +|---|---|---|---| +| O1 | Entailed-from-COHERENT promotes; artifact re-verifies | `test_O1_*` | xfail(strict) | +| O2 | Consistent-but-not-entailed stays SPECULATIVE | `test_O2_*` | xfail(strict) | +| O3 | Any non-COHERENT premise → refuse | `test_O3_*` | xfail(strict) | +| O4 | Misread premise fails closed | `test_O4_*` | xfail(strict) | +| O5 | Proposer proof/status/confidence ignored, byte-identical decision | `test_O5_*` | xfail(strict) | +| O6 | No new mutation path | INV-21 (existing) + INV-29 (this PR) | passing | +| O7 | Determinism + replay re-verification | `test_O7_*` (promoter: xfail) + `test_pin_entailment_trace_*` (substrate: passing) | split | +| O8 | wrong=0 lanes stay green | existing lane gates + `verify_lane_shas` | passing | + +Honesty pins (pass today, flip red the moment the feature is wired without +conscious review): `review_correction` carries status as an input and does +not compute it; `teaching.proof_promotion` does not exist. + +## Trust boundary + +The untrusted inputs are the proposer's claim text and anything the proposer +attaches (proof candidate, status, confidence). All of it is **data, never +authority**: forms come from curator-certified store state, the proof is +recomputed by the pinned engine, and the decision must be byte-identical +with and without proposer attachments. The reading-certification step is the +explicit hazard surface and refuses on any gap. + +## Non-goals + +- The geometric arm (`cga_inner ≥ τ`) — separate ADR-0021 v2 work. +- Promotion of generated/asserted output — permanently forbidden. +- Source authority or confidence weighting — permanently forbidden. +- Auto-demotion on REFUTED — open item, not in scope. +- Any structural (non-curator) reading certification — future ADR. + +## Ratification checklist (architect) + +- [ ] D1 split (pure decider / vault-owned mutation) over the alternative + (new INV-21 allowlist entry). +- [ ] D2 first cut: reading stays curator-certified; entailment automated. +- [ ] D3 predicate exact as stated (including REFUTED → no transition). +- [ ] D4 certificate fields + trace-hash folding. +- [ ] INV-29 as the permanent transition-site boundary (already shipped in + the proposing PR as a passing invariant; ratification confirms it). diff --git a/docs/issues/proof-carrying-coherence-promotion.md b/docs/issues/proof-carrying-coherence-promotion.md index 25d25281..3b93fa1f 100644 --- a/docs/issues/proof-carrying-coherence-promotion.md +++ b/docs/issues/proof-carrying-coherence-promotion.md @@ -1,6 +1,10 @@ # Issue — Proof-carrying coherence promotion (the logical arm of ADR-0021's v2 gap) -**Status:** Open — specification only, no code authorized +**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. **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/tests/test_architectural_invariants.py b/tests/test_architectural_invariants.py index c4b845b1..aa022a37 100644 --- a/tests/test_architectural_invariants.py +++ b/tests/test_architectural_invariants.py @@ -1718,3 +1718,144 @@ class TestINV28MeaningGraphNeutrality: "INV-28a predicate failed to flag a module known to import the " "field engine — the neutrality check is vacuous." ) + + +# =========================================================================== +# INV-29 Epistemic-status transition sites are allowlisted +# =========================================================================== +# +# Claim (ADR-0021 §3 + ADR-0218 §Context): +# INV-21 polices `VaultStore.store(...)` callers, but a SPECULATIVE→COHERENT +# *transition* on an already-stored entry is not a store() call — it is an +# in-place assignment to the entry's `epistemic_status` metadata key. +# ADR-0148's `promote_eligible_entries` proved this shape exists and that +# INV-21's AST scan cannot see it. Without this invariant, a new promoter +# (including the ADR-0218 proof-carrying promoter, or any future fast-path) +# could flip stored claims to admissible-as-evidence without tripping any +# structural check. +# +# This test AST-asserts the assignment-site set: every production assignment +# whose target is an `epistemic_status` subscript key or attribute must live +# in an allowlisted module. Adding a new transition site is allowed but must +# be intentional — edit the allowlist and document the justification here in +# the same commit. +# +# Allowlist rationale per site: +# vault/store.py — the single mutation owner. Two 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. + +ALLOWED_STATUS_TRANSITION_SITES: frozenset[str] = frozenset({ + "vault/store.py", +}) + + +def _status_assignment_targets(tree: ast.AST) -> int: + """Count assignment targets that write an `epistemic_status` key/attr. + + Catches both shapes that can flip a stored entry's tier: + meta["epistemic_status"] = ... (subscript with constant key) + entry.epistemic_status = ... (attribute assignment) + including the mutate-via-recall-reference backdoor + hit["metadata"]["epistemic_status"] = ... + Uses AST so comments/docstrings/strings cannot trigger false positives. + """ + count = 0 + for node in ast.walk(tree): + targets: list[ast.expr] = [] + if isinstance(node, ast.Assign): + targets = list(node.targets) + elif isinstance(node, (ast.AnnAssign, ast.AugAssign)): + targets = [node.target] + for target in targets: + if ( + isinstance(target, ast.Subscript) + and isinstance(target.slice, ast.Constant) + and target.slice.value == "epistemic_status" + ): + count += 1 + elif ( + isinstance(target, ast.Attribute) + and target.attr == "epistemic_status" + ): + count += 1 + return count + + +def _file_status_transition_count(path: Path) -> int: + try: + tree = ast.parse(path.read_text()) + except (OSError, SyntaxError): + return 0 + return _status_assignment_targets(tree) + + +class TestINV29EpistemicStatusTransitionSites: + """ + Claim: Only modules in ALLOWED_STATUS_TRANSITION_SITES may assign to an + `epistemic_status` key or attribute. A new assignment site is a new + promotion/demotion authority over the revision graph and must be + reviewed — coherence stops being the only admission signal the moment an + unreviewed site can flip a claim to COHERENT (ADR-0021 §3, ADR-0218). + """ + + def test_no_unallowlisted_status_transition_sites(self): + offenders: list[str] = [] + for path in _enumerate_project_py_files(): + if _file_status_transition_count(path) == 0: + continue + rel = str(path.relative_to(PROJECT_ROOT_FOR_INV21)) + if rel not in ALLOWED_STATUS_TRANSITION_SITES: + offenders.append(rel) + assert not offenders, ( + "New epistemic-status transition site(s) detected outside the " + "allowlist:\n " + "\n ".join(offenders) + + "\n\nIf this is intentional, add the path to " + "ALLOWED_STATUS_TRANSITION_SITES in " + "tests/test_architectural_invariants.py with a one-line " + "justification in the comment block above the set. Every " + "additional transition site is a new promotion authority over " + "the epistemic schema (ADR-0021 §3, ADR-0218)." + ) + + def test_allowlist_is_actually_used(self): + """Drift guard — if an allowlisted module no longer assigns status, + remove it to keep the trust surface tight.""" + used: set[str] = set() + for path in _enumerate_project_py_files(): + if _file_status_transition_count(path) > 0: + rel = str(path.relative_to(PROJECT_ROOT_FOR_INV21)) + if rel in ALLOWED_STATUS_TRANSITION_SITES: + used.add(rel) + unused = ALLOWED_STATUS_TRANSITION_SITES - used + assert not unused, ( + f"Allowlisted site(s) no longer assign epistemic_status: " + f"{sorted(unused)}\nRemove from ALLOWED_STATUS_TRANSITION_SITES." + ) + + def test_detector_is_non_vacuous(self): + """29b — prove 29a can fail: the predicate flags every known + assignment shape, including the recall-reference backdoor.""" + snippet = ( + "meta['epistemic_status'] = 'coherent'\n" + "entry.epistemic_status = STATUS\n" + "hit['metadata']['epistemic_status'] = 'coherent'\n" + ) + assert _status_assignment_targets(ast.parse(snippet)) == 3, ( + "INV-29 predicate failed to flag known status-assignment shapes " + "— the transition-site scan is vacuous." + ) + + 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.""" + 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 " + "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 new file mode 100644 index 00000000..b0d2eff1 --- /dev/null +++ b/tests/test_proof_carrying_promotion_obligations.py @@ -0,0 +1,268 @@ +"""ADR-0218 PR A — executable proof obligations for proof-carrying coherence +promotion. THE FEATURE IS NOT LIVE. + +Two kinds of tests, per the strict-xfail gate convention +(see tests/test_edge_budget_gate.py): + +- 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. + +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. + +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. +""" + +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.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( + vault: VaultStore, + seed: int, + form: str, + status: EpistemicStatus, + *, + certified: bool = True, +) -> int: + """Store a premise entry carrying a curator-certified reading (ADR-0218 §D2).""" + return vault.store( + _versor(seed), + { + "propositional_form": form, + "reading_certified": certified, + }, + epistemic_status=status, + ) + + +# --------------------------------------------------------------------------- +# Honesty pins — pass today, flip red when reality changes +# --------------------------------------------------------------------------- + +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." + ) + + +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).""" + candidate = CorrectionCandidate( + correction_text="the sky is blue", + intent=DialogueIntent(tag=IntentTag.CORRECTION, subject="sky"), + prior_surface="the sky is green", + prior_turn=1, + candidate_id="pin-0001", + ) + defaulted = review_correction(candidate) + assert defaulted.epistemic_status is EpistemicStatus.SPECULATIVE + + # The curator-supplied input flows through verbatim — no computation runs. + echoed = review_correction(candidate, epistemic_status=EpistemicStatus.COHERENT) + assert echoed.epistemic_status is EpistemicStatus.COHERENT, ( + "review_correction no longer carries the curator-supplied status " + "verbatim — a computation was added. Reconcile with ADR-0218 before " + "merging: promotion logic must not fork into a parallel path here." + ) + + +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) will rely 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." + ) + + # A non-entailed query must be UNKNOWN, not promoted-shaped evidence. + unknown = evaluate_entailment_with_trace(("p",), "q") + assert unknown.outcome is Entailment.UNKNOWN + + +# --------------------------------------------------------------------------- +# Obligations — xfail(strict) until ADR-0218 is ratified and P3 lands +# --------------------------------------------------------------------------- + +@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() + vault = VaultStore(reproject_interval=0) + idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT) + idx_pq = _store_premise(vault, 2, "p -> q", EpistemicStatus.COHERENT) + + decision = mod.certify_promotion( + claim_form="q", + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is True + + # 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() + + +@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() + vault = VaultStore(reproject_interval=0) + idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT) + + decision = mod.certify_promotion( + claim_form="q", # consistent with {p}, not entailed by it + premise_entry_indices=(idx_p,), + vault=vault, + ) + assert decision.promoted is False + + +@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) + + decision = mod.certify_promotion( + claim_form="q", + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is False + 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( + vault, 2, "p -> q", EpistemicStatus.COHERENT, certified=False + ) + + decision = mod.certify_promotion( + claim_form="q", + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + assert decision.promoted is False + 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) + + bare = mod.certify_promotion( + claim_form="q", + premise_entry_indices=(idx_p,), + vault=vault, + ) + adorned = mod.certify_promotion( + claim_form="q", + premise_entry_indices=(idx_p,), + vault=vault, + proposer_payload={ + "proof": "trust me, q follows", + "status": "coherent", + "confidence": 0.99, + }, + ) + assert bare.promoted is adorned.promoted is False + 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() + + def run(): + 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", + premise_entry_indices=(idx_p, idx_pq), + vault=vault, + ) + + first, second = run(), run() + assert first.certificate.canonical_json() == second.certificate.canonical_json()