core-labs/core
1
0
Fork 0
Code Issues Pull requests 1 Projects Releases Packages Wiki Activity Actions

feat(teaching): ADR-0218 P3 — proof-carrying coherence promotion

Browse source 
The ratified capability, through the existing mutation owner only:

- teaching/proof_promotion.py — pure decider. Fresh-reads every premise AND
  the claim from the store (claim_entry_index; forms never proposer-supplied),
  strict status compares (no parse-defaulting), reading_certified must be the
  boolean True, engine certification via the pinned deductive engine,
  proposer_payload accepted and provably never read (del before use; poisoned-
  mapping test), certificate digest emitted for D4 trace-hash folding. Zero
  mutation; zero vault.store calls; zero status writes (proven with the
  INV-21/INV-29 detectors themselves).
- vault/store.py::apply_certified_promotion — the single transition site.
  Independently re-verifies: byte-for-byte replay under DEDUCTIVE_ENGINE_PIN,
  promotion_positive, live claim form/reading/status cross-checks, live
  premise form/reading/status cross-checks (staleness refuses). Fabricated or
  tampered certificates flip nothing; authority is live store state plus
  recomputation, never the artifact.
- generate/proof_chain/engine_pin.py — DEDUCTIVE_ENGINE_PIN mirrors the
  deductive_logic_v1 lane SHA; sync pinned by AST test against
  scripts/verify_lane_shas.py.
- Consistency fix found in lookback: both promotion sites now stamp
  epistemic_state alongside epistemic_status (the ADR-0148 site left the
  stored state tag stale; recall recomputed it, but the stored key lied).

Obligations: all six strict-xfail markers retired and live (O1/O2
strengthened to prove the transition through the vault owner); the
module-existence pin deleted per its own docstring; the two remaining
honesty pins kept. INV-21 allowlist unchanged; INV-29 allowlist unchanged
({vault/store.py}); INV-29's 29c visibility floor raised 2 -> 3 to cover the
new site.

No runtime turn path calls promotion; the deterministic demo is PR D.

Validation: new suite 49 passed; obligations 8 passed (0 xfail remaining);
invariants 66 passed; certificate 27 passed; 0148 6 passed; epistemic 20
passed; smoke files green; lane SHAs verified.
This commit is contained in:
Shay 2026-06-11 17:02:45 -07:00
parent 1524fcc3c8
commit e473f5b55f
12 changed files with 1248 additions and 145 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md
View file

@ -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

17
docs/issues/proof-carrying-coherence-promotion.md
View file

@ -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

7
generate/proof_chain/__init__.py
View file

@ -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",

8
generate/proof_chain/certificate.py
View file

@ -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

30
generate/proof_chain/engine_pin.py Normal file
View file

@ -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"
)

18
teaching/epistemic.py
View file

@ -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"

248
teaching/proof_promotion.py Normal file
View file

@ -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,
)

3
tests/test_adr_0148_vault_promotion.py
View file

@ -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"
# ---------------------------------------------------------------------------

689
tests/test_adr_0218_proof_promotion.py Normal file
View file

@ -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"

25
tests/test_architectural_invariants.py
View file

@ -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."
)

199
tests/test_proof_carrying_promotion_obligations.py
View file

@ -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

139
vault/store.py
View file

@ -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.