feat(proof_chain): ADR-0218 PR B — PromotionCertificate + pure replay verifier
Pure evidence substrate for proof-carrying coherence promotion. No promotion, no vault import, no status transition, no teaching-path change; ADR-0218 stays Proposed. - generate/proof_chain/certificate.py: frozen PromotionCertificate (version/claim_form/premise ids+forms+statuses/entailment_trace/ engine_pin/decision/reason, canonical_json with sort_keys+compact separators); build_certificate runs evaluate_entailment_with_trace over entry_id-sorted premises; verify_certificate rebuilds from the embedded forms and accepts iff byte-identical — tampered forms/claim/ trace/decision/reason/ordering/version all fail replay, structural breakage fails closed as malformed_certificate. - promotion_positive is necessary-not-sufficient: entailed over a non-empty all-coherent recorded premise set; REFUTED/UNKNOWN/REFUSED verify as themselves but are never positive; zero-premise tautology certificates fail-closed non-positive in v1. - engine_pin is recorded provenance; pin tampering is caught only via caller-supplied expected_engine_pin (P3 must pass the lane SHA) — limit pinned by dedicated tests. - entail.py: docstring-only fix removing the incorrect ADR-0206 attribution (numbering collision); now cites ADR-0218. Zero behavior change. generate_claims.py:74 still carries the label (serving-frozen surface, flagged for follow-up). - No xfail markers retire: every PR-A obligation binds to the P3 promoter, which must not exist before ratification. The certificate- shaped halves of O1/O7 are proven for real in tests/test_proof_chain_certificate.py (27 tests). ADR phasing bullet and obligations docstring record the reconciliation. Validation: certificate 27 passed; obligations 3 passed + 6 xfailed; architectural invariants 61 passed (INV-21/INV-29 green, allowlists unchanged); entail/builder/rules 61 passed; smoke files 95 passed.
This commit is contained in:
Shay
parent
b52e0e1c7e
commit
bdc4940e1e
7 changed files with 726 additions and 7 deletions
|
|
@ -154,12 +154,19 @@ the certificate, not just the status.
|
|||
- **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 B (landed: `generate/proof_chain/certificate.py`).**
|
||||
`PromotionCertificate` + builder + replay verifier as a pure,
|
||||
side-effect-free module with its own tests
|
||||
(`tests/test_proof_chain_certificate.py`). No promotion, no vault method,
|
||||
no status transition anywhere. Reconciliation against the PR-A wording
|
||||
("retires the certificate-shaped xfails only"): every PR-A xfail marker
|
||||
binds to the P3 promoter (`teaching.proof_promotion`), which must not
|
||||
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 the remaining xfails (strict-xpass forces it); INV-21 allowlist
|
||||
Retires all the 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
|
||||
|
|
|
|||
|
|
@ -4,7 +4,10 @@
|
|||
(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.
|
||||
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.
|
||||
**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
|
||||
|
|
|
|||
|
|
@ -5,6 +5,12 @@
|
|||
- Phase 2.3 (ADR-0205): the first inference rule + the wrong=0 mechanism —
|
||||
`evaluate_modus_ponens` / `evaluate_proof_conclusion` (modus_ponens + the
|
||||
disagreement/uniqueness rule), in `rules.py`.
|
||||
- Phase 2.4: the full sound+complete propositional entailment operator over the
|
||||
ADR-0201 ROBDD (`evaluate_entailment_with_trace`), in `entail.py` — committed
|
||||
home is ADR-0218 (its original "ADR-0206" label was a numbering collision).
|
||||
- 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.
|
||||
|
||||
Honesty boundary (load-bearing through 2.3): sound over declared atoms, not grounded
|
||||
in recognized input; the disagreement rule guarantees a unique conclusion among
|
||||
|
|
@ -20,6 +26,20 @@ from .builder import (
|
|||
ProofGraph,
|
||||
build_proof_graph,
|
||||
)
|
||||
from .certificate import (
|
||||
CERTIFICATE_VERSION,
|
||||
ENGINE_PIN_MISMATCH,
|
||||
MALFORMED_CERTIFICATE,
|
||||
PREMISE_STATUS_VOCAB,
|
||||
REPLAY_MATCH,
|
||||
REPLAY_MISMATCH,
|
||||
VERIFICATION_REASONS,
|
||||
CertificateVerification,
|
||||
PremiseRecord,
|
||||
PromotionCertificate,
|
||||
build_certificate,
|
||||
verify_certificate,
|
||||
)
|
||||
from .model import Proof, ProofError, ProofNode, proof_from_premises
|
||||
from .rules import (
|
||||
CONCLUSION_DISAGREEMENT,
|
||||
|
|
@ -48,19 +68,28 @@ from .entail import (
|
|||
)
|
||||
|
||||
__all__ = (
|
||||
"CERTIFICATE_VERSION",
|
||||
"CONCLUSION_DISAGREEMENT",
|
||||
"CONCLUSION_MISMATCH",
|
||||
"CertificateVerification",
|
||||
"ENGINE_PIN_MISMATCH",
|
||||
"MALFORMED_CERTIFICATE",
|
||||
"MISSING_IMPLICATION",
|
||||
"MP_REASONS",
|
||||
"MPOutcome",
|
||||
"MPVerdict",
|
||||
"PREMISE_STATUS_VOCAB",
|
||||
"PROOF_INTRODUCED_BY",
|
||||
"PROOF_NO_UNIT",
|
||||
"PROOF_SOURCE_ID",
|
||||
"PremiseRecord",
|
||||
"Proof",
|
||||
"ProofError",
|
||||
"ProofGraph",
|
||||
"ProofNode",
|
||||
"PromotionCertificate",
|
||||
"REPLAY_MATCH",
|
||||
"REPLAY_MISMATCH",
|
||||
"ENTAILMENT_REASONS",
|
||||
"Entailment",
|
||||
"EntailmentTrace",
|
||||
|
|
@ -72,10 +101,13 @@ __all__ = (
|
|||
"UNESTABLISHED_ANTECEDENT",
|
||||
"UNDETERMINED",
|
||||
"UNIQUE_CANONICAL_CONCLUSION",
|
||||
"VERIFICATION_REASONS",
|
||||
"build_certificate",
|
||||
"build_proof_graph",
|
||||
"evaluate_entailment",
|
||||
"evaluate_entailment_with_trace",
|
||||
"evaluate_modus_ponens",
|
||||
"evaluate_proof_conclusion",
|
||||
"proof_from_premises",
|
||||
"verify_certificate",
|
||||
)
|
||||
|
|
|
|||
273
generate/proof_chain/certificate.py
Normal file
273
generate/proof_chain/certificate.py
Normal file
|
|
@ -0,0 +1,273 @@
|
|||
"""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
|
||||
decides nothing about the vault and mutates nothing anywhere:
|
||||
|
||||
- no vault / teaching / session import — premises arrive as already-read
|
||||
``PremiseRecord`` values; binding them to real vault entries (fresh-read,
|
||||
ADR-0218 §D3.1) and checking reading certification (§D3.2) is the
|
||||
promoter's job, not this module's;
|
||||
- no status transition — INV-29's allowlist (``vault/store.py``) is untouched;
|
||||
- no clock, randomness, environment, or filesystem — a certificate is a pure
|
||||
function of ``(claim_form, premises, engine_pin)``, byte-stable under
|
||||
replay.
|
||||
|
||||
``build_certificate`` runs the sound+complete propositional engine
|
||||
(:func:`generate.proof_chain.entail.evaluate_entailment_with_trace`, the
|
||||
ADR-0201/0202 ROBDD keystone) and freezes the outcome plus its full
|
||||
``EntailmentTrace`` into the certificate. ``verify_certificate`` re-runs the
|
||||
engine from the embedded forms and accepts iff the rebuilt certificate is
|
||||
byte-identical under ``canonical_json()`` — any tamper with the claim form,
|
||||
a premise form, the trace, the decision, the reason, the premise ordering,
|
||||
or the version fails replay.
|
||||
|
||||
Honesty boundaries (load-bearing):
|
||||
|
||||
- ``promotion_positive`` is NECESSARY, never sufficient. It checks the
|
||||
*recorded* decision and statuses; the P3 promoter must additionally
|
||||
fresh-read premise statuses and reading certification from the vault
|
||||
(§D3.1–D3.2) and call ``verify_certificate`` (§D3.4) before any
|
||||
transition. ``entailed`` is the only positive decision; ``refuted`` /
|
||||
``unknown`` / ``refused`` certificates verify as their own outcomes but
|
||||
are never positive.
|
||||
- ``engine_pin`` is recorded provenance, carried verbatim through replay.
|
||||
It is independently checkable only against a caller-supplied
|
||||
``expected_engine_pin`` (the deductive-lane SHA in force) — pure replay
|
||||
cannot know the true pin, because this module has no filesystem.
|
||||
- Zero-premise certificates (tautology claims, entailed by the empty set)
|
||||
are never promotion-positive in v1; whether tautologies may promote is a
|
||||
ratification question, recorded fail-closed here.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import json
|
||||
from dataclasses import dataclass
|
||||
from typing import Final
|
||||
|
||||
from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
|
||||
|
||||
CERTIFICATE_VERSION: Final[int] = 1
|
||||
|
||||
# Mirrors the *values* of teaching.epistemic.EpistemicStatus. generate/ does
|
||||
# not import teaching/ (layering: teaching consumes generate, never the
|
||||
# reverse); the sync is pinned by
|
||||
# tests/test_proof_chain_certificate.py::test_status_vocab_matches_teaching_enum.
|
||||
PREMISE_STATUS_VOCAB: Final[frozenset[str]] = frozenset({
|
||||
"coherent",
|
||||
"contested",
|
||||
"speculative",
|
||||
"falsified",
|
||||
})
|
||||
_COHERENT: Final[str] = "coherent"
|
||||
|
||||
# Closed verification-reason vocabulary (the verifier makes exactly these
|
||||
# distinctions).
|
||||
REPLAY_MATCH: Final[str] = "replay_match"
|
||||
REPLAY_MISMATCH: Final[str] = "replay_mismatch"
|
||||
MALFORMED_CERTIFICATE: Final[str] = "malformed_certificate"
|
||||
ENGINE_PIN_MISMATCH: Final[str] = "engine_pin_mismatch"
|
||||
|
||||
VERIFICATION_REASONS: Final[frozenset[str]] = frozenset({
|
||||
REPLAY_MATCH,
|
||||
REPLAY_MISMATCH,
|
||||
MALFORMED_CERTIFICATE,
|
||||
ENGINE_PIN_MISMATCH,
|
||||
})
|
||||
|
||||
|
||||
def _require_str(value: object, what: str) -> str:
|
||||
"""Boundary type check for untyped callers; fail-closed replay needs
|
||||
tampered-type fields to raise ``ValueError``, never an arbitrary error."""
|
||||
if not isinstance(value, str):
|
||||
raise ValueError(
|
||||
f"certificate: {what} must be a str, got {type(value).__name__}"
|
||||
)
|
||||
return value
|
||||
|
||||
|
||||
def _require_entry_id(value: object) -> int:
|
||||
if isinstance(value, bool) or not isinstance(value, int):
|
||||
raise ValueError(
|
||||
f"certificate: premise entry_id must be an int, got "
|
||||
f"{type(value).__name__}"
|
||||
)
|
||||
return value
|
||||
|
||||
|
||||
def _require_record(value: object) -> "PremiseRecord":
|
||||
if not isinstance(value, PremiseRecord):
|
||||
raise ValueError(
|
||||
f"certificate: premises must be PremiseRecord values, got "
|
||||
f"{type(value).__name__}"
|
||||
)
|
||||
return value
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class PremiseRecord:
|
||||
"""One already-read premise: vault identity + certified form + status.
|
||||
|
||||
The record is a *claim about* a vault entry, not the entry itself — the
|
||||
P3 promoter is responsible for having fresh-read ``form`` and ``status``
|
||||
from the store (never from the proposer) before building a certificate.
|
||||
"""
|
||||
|
||||
entry_id: int
|
||||
form: str
|
||||
status: str
|
||||
|
||||
def __post_init__(self) -> None:
|
||||
_require_entry_id(self.entry_id)
|
||||
_require_str(self.form, "premise form")
|
||||
if self.status not in PREMISE_STATUS_VOCAB:
|
||||
raise ValueError(
|
||||
f"certificate: premise status {self.status!r} is not in the "
|
||||
f"closed vocabulary {sorted(PREMISE_STATUS_VOCAB)}"
|
||||
)
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class PromotionCertificate:
|
||||
"""Frozen, deterministic audit artifact for one entailment decision.
|
||||
|
||||
Premises are stored in canonical order (ascending ``entry_id``);
|
||||
``decision``/``reason`` mirror the embedded ``entailment_trace`` and the
|
||||
closed vocabularies of :mod:`generate.proof_chain.entail`. Tampering
|
||||
with any field is caught by :func:`verify_certificate`, not by interior
|
||||
immutability — the dataclass is frozen, but the certificate's authority
|
||||
comes from replay, never from trust in the object.
|
||||
"""
|
||||
|
||||
certificate_version: int
|
||||
claim_form: str
|
||||
premise_entry_ids: tuple[int, ...]
|
||||
premise_forms: tuple[str, ...]
|
||||
premise_statuses: tuple[str, ...]
|
||||
entailment_trace: dict[str, object]
|
||||
engine_pin: str
|
||||
decision: str
|
||||
reason: str
|
||||
|
||||
@property
|
||||
def promotion_positive(self) -> bool:
|
||||
"""Necessary-not-sufficient promotion precondition (module docstring).
|
||||
|
||||
``entailed`` over a non-empty, all-coherent *recorded* premise set.
|
||||
The P3 promoter must still fresh-read statuses, check reading
|
||||
certification, and replay-verify before any transition.
|
||||
"""
|
||||
return (
|
||||
self.decision == Entailment.ENTAILED.value
|
||||
and len(self.premise_statuses) > 0
|
||||
and all(status == _COHERENT for status in self.premise_statuses)
|
||||
)
|
||||
|
||||
def as_dict(self) -> dict[str, object]:
|
||||
return {
|
||||
"certificate_version": self.certificate_version,
|
||||
"claim_form": self.claim_form,
|
||||
"premise_entry_ids": self.premise_entry_ids,
|
||||
"premise_forms": self.premise_forms,
|
||||
"premise_statuses": self.premise_statuses,
|
||||
"entailment_trace": dict(self.entailment_trace),
|
||||
"engine_pin": self.engine_pin,
|
||||
"decision": self.decision,
|
||||
"reason": self.reason,
|
||||
}
|
||||
|
||||
def canonical_json(self) -> str:
|
||||
return json.dumps(self.as_dict(), sort_keys=True, separators=(",", ":"))
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class CertificateVerification:
|
||||
"""Replay verdict: ``verified`` + a reason from ``VERIFICATION_REASONS``."""
|
||||
|
||||
verified: bool
|
||||
reason: str
|
||||
|
||||
|
||||
def build_certificate(
|
||||
*,
|
||||
claim_form: str,
|
||||
premises: tuple[PremiseRecord, ...],
|
||||
engine_pin: str,
|
||||
) -> PromotionCertificate:
|
||||
"""Run the entailment engine and freeze the decision into a certificate.
|
||||
|
||||
Pure: same inputs → byte-identical certificate. Premises are
|
||||
canonicalized to ascending ``entry_id`` order before the engine runs, so
|
||||
caller ordering cannot perturb the artifact. Structural contract
|
||||
violations (duplicate entry ids, wrong types, empty engine pin) raise
|
||||
``ValueError``; *content* problems — malformed / out-of-regime forms,
|
||||
inconsistent premises — are the engine's authority and surface as a
|
||||
``refused`` decision, never as a vacuous entailment.
|
||||
"""
|
||||
_require_str(claim_form, "claim_form")
|
||||
if not _require_str(engine_pin, "engine_pin").strip():
|
||||
raise ValueError("certificate: engine_pin must be a non-empty str")
|
||||
checked = tuple(_require_record(record) for record in premises)
|
||||
entry_ids = [record.entry_id for record in checked]
|
||||
if len(set(entry_ids)) != len(entry_ids):
|
||||
raise ValueError(
|
||||
f"certificate: duplicate premise entry_ids {sorted(entry_ids)}"
|
||||
)
|
||||
|
||||
ordered = tuple(sorted(checked, key=lambda record: record.entry_id))
|
||||
forms = tuple(record.form for record in ordered)
|
||||
trace = evaluate_entailment_with_trace(forms, claim_form)
|
||||
return PromotionCertificate(
|
||||
certificate_version=CERTIFICATE_VERSION,
|
||||
claim_form=claim_form,
|
||||
premise_entry_ids=tuple(record.entry_id for record in ordered),
|
||||
premise_forms=forms,
|
||||
premise_statuses=tuple(record.status for record in ordered),
|
||||
entailment_trace=trace.as_dict(),
|
||||
engine_pin=engine_pin,
|
||||
decision=trace.outcome.value,
|
||||
reason=trace.reason,
|
||||
)
|
||||
|
||||
|
||||
def verify_certificate(
|
||||
certificate: PromotionCertificate,
|
||||
*,
|
||||
expected_engine_pin: str | None = None,
|
||||
) -> CertificateVerification:
|
||||
"""Re-run the engine from the embedded forms; accept iff byte-identical.
|
||||
|
||||
Rebuilds a certificate from ``(claim_form, premises, engine_pin)`` as
|
||||
embedded and compares ``canonical_json()`` byte-for-byte — a tampered
|
||||
premise form, claim form, swapped trace, forged decision/reason, broken
|
||||
ordering, or wrong version all fail replay. ``engine_pin`` is carried
|
||||
verbatim through the rebuild, so pin provenance is only checked when the
|
||||
caller supplies ``expected_engine_pin`` (P3 must pass the deductive-lane
|
||||
SHA in force). Structurally unusable certificates fail closed as
|
||||
``malformed_certificate``.
|
||||
"""
|
||||
if expected_engine_pin is not None and certificate.engine_pin != expected_engine_pin:
|
||||
return CertificateVerification(verified=False, reason=ENGINE_PIN_MISMATCH)
|
||||
try:
|
||||
records = tuple(
|
||||
PremiseRecord(entry_id=entry_id, form=form, status=status)
|
||||
for entry_id, form, status in zip(
|
||||
certificate.premise_entry_ids,
|
||||
certificate.premise_forms,
|
||||
certificate.premise_statuses,
|
||||
strict=True,
|
||||
)
|
||||
)
|
||||
rebuilt = build_certificate(
|
||||
claim_form=certificate.claim_form,
|
||||
premises=records,
|
||||
engine_pin=certificate.engine_pin,
|
||||
)
|
||||
replay_matches = rebuilt.canonical_json() == certificate.canonical_json()
|
||||
except (ValueError, TypeError):
|
||||
return CertificateVerification(verified=False, reason=MALFORMED_CERTIFICATE)
|
||||
if not replay_matches:
|
||||
return CertificateVerification(verified=False, reason=REPLAY_MISMATCH)
|
||||
return CertificateVerification(verified=True, reason=REPLAY_MATCH)
|
||||
|
|
@ -1,4 +1,12 @@
|
|||
"""ADR-0206 — Propositional entailment operator (proof_chain phase 2.4).
|
||||
"""Propositional entailment operator (proof_chain phase 2.4) — the
|
||||
proof-certificate substrate of ADR-0218 (Proof-Carrying Coherence Promotion).
|
||||
|
||||
Numbering note: this module originally carried an "ADR-0206" attribution —
|
||||
a three-way numbering collision. Committed ADR-0206 is the
|
||||
response-governance bridge; the old phase-2 plan's 2.4 referred to carrier
|
||||
grounding (still unbuilt). This operator's committed home is ADR-0218
|
||||
(§Context documents the collision; §D3–D4 specify how its
|
||||
``EntailmentTrace`` evidence is consumed by ``certificate.py``).
|
||||
|
||||
The multi-hop inference operator ``gaps.md`` asked for and ADR-0205 deferred. Where
|
||||
:func:`generate.proof_chain.rules.evaluate_modus_ponens` is **single-step** ("unique
|
||||
|
|
|
|||
|
|
@ -23,6 +23,13 @@ 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.
|
||||
"""
|
||||
|
|
@ -124,7 +131,8 @@ 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) will rely on."""
|
||||
PromotionCertificate replay verifier (PR B,
|
||||
generate/proof_chain/certificate.py — landed) relies on."""
|
||||
premises = ("p", "p -> q")
|
||||
first = evaluate_entailment_with_trace(premises, "q")
|
||||
second = evaluate_entailment_with_trace(premises, "q")
|
||||
|
|
|
|||
388
tests/test_proof_chain_certificate.py
Normal file
388
tests/test_proof_chain_certificate.py
Normal file
|
|
@ -0,0 +1,388 @@
|
|||
"""ADR-0218 PR B — PromotionCertificate + replay verifier (pure substrate).
|
||||
|
||||
PROMOTION IS STILL NOT LIVE. These tests prove the *certificate* substrate:
|
||||
build → freeze → replay-verify, fail-closed on every tamper. The promoter
|
||||
obligations (O1–O5, O7) remain strict-xfail in
|
||||
tests/test_proof_carrying_promotion_obligations.py — every one of them binds
|
||||
to `teaching.proof_promotion`, which must not exist before ADR-0218 is
|
||||
ratified (P3). What PR B retires is not a marker but a gap: the
|
||||
certificate-shaped halves of O1/O7 (replay re-verification, byte-stable
|
||||
determinism) are proven here for real instead of being asserted inside
|
||||
promoter xfails.
|
||||
|
||||
Tamper tests use `dataclasses.replace` deliberately: the certificate's
|
||||
authority comes from replay recomputation, never from trust in the frozen
|
||||
object — a forged field must fail `verify_certificate`, not be unrepresentable.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import ast
|
||||
import dataclasses
|
||||
import json
|
||||
from pathlib import Path
|
||||
|
||||
import pytest
|
||||
|
||||
from generate.proof_chain import (
|
||||
CERTIFICATE_VERSION,
|
||||
ENGINE_PIN_MISMATCH,
|
||||
INCONSISTENT_PREMISES,
|
||||
MALFORMED_CERTIFICATE,
|
||||
OUT_OF_REGIME_OR_MALFORMED,
|
||||
PREMISE_STATUS_VOCAB,
|
||||
REPLAY_MATCH,
|
||||
REPLAY_MISMATCH,
|
||||
TAUTOLOGICAL_IMPLICATION,
|
||||
TAUTOLOGICAL_REFUTATION,
|
||||
UNDETERMINED,
|
||||
VERIFICATION_REASONS,
|
||||
Entailment,
|
||||
PremiseRecord,
|
||||
PromotionCertificate,
|
||||
build_certificate,
|
||||
evaluate_entailment_with_trace,
|
||||
verify_certificate,
|
||||
)
|
||||
import generate.proof_chain.certificate as certificate_module
|
||||
|
||||
# Opaque to the module under test; the real deductive-lane SHA is supplied by
|
||||
# the P3 promoter from scripts/verify_lane_shas.py, never read from disk here.
|
||||
_PIN = "deductive_logic_v1@pinned-for-test"
|
||||
|
||||
_CERTIFICATE_SOURCE = Path(certificate_module.__file__).read_text(encoding="utf-8")
|
||||
|
||||
|
||||
def _coherent(*pairs: tuple[int, str]) -> tuple[PremiseRecord, ...]:
|
||||
return tuple(
|
||||
PremiseRecord(entry_id=entry_id, form=form, status="coherent")
|
||||
for entry_id, form in pairs
|
||||
)
|
||||
|
||||
|
||||
def _build(claim: str, premises: tuple[PremiseRecord, ...]) -> PromotionCertificate:
|
||||
return build_certificate(claim_form=claim, premises=premises, engine_pin=_PIN)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# 1. The positive path: entailed certificate verifies
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_entailed_certificate_verifies() -> None:
|
||||
cert = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
assert cert.certificate_version == CERTIFICATE_VERSION
|
||||
assert cert.decision == Entailment.ENTAILED.value
|
||||
assert cert.reason == TAUTOLOGICAL_IMPLICATION
|
||||
assert cert.promotion_positive is True
|
||||
|
||||
verdict = verify_certificate(cert)
|
||||
assert verdict.verified is True
|
||||
assert verdict.reason == REPLAY_MATCH
|
||||
|
||||
|
||||
def test_embedded_trace_matches_independent_recomputation() -> None:
|
||||
"""The O1 substrate half, proven for real: recomputing from the embedded
|
||||
forms reproduces the embedded EntailmentTrace exactly (ADR-0218 §D3.4)."""
|
||||
cert = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
recomputed = evaluate_entailment_with_trace(("p", "p -> q"), "q")
|
||||
assert cert.entailment_trace == recomputed.as_dict()
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# 2–4. Tampering fails replay
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_tampered_premise_form_fails_verification() -> None:
|
||||
cert = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
tampered = dataclasses.replace(cert, premise_forms=("p", "p -> r"))
|
||||
verdict = verify_certificate(tampered)
|
||||
assert verdict.verified is False
|
||||
assert verdict.reason == REPLAY_MISMATCH
|
||||
|
||||
|
||||
def test_tampered_claim_form_fails_verification() -> None:
|
||||
cert = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
tampered = dataclasses.replace(cert, claim_form="r")
|
||||
verdict = verify_certificate(tampered)
|
||||
assert verdict.verified is False
|
||||
assert verdict.reason == REPLAY_MISMATCH
|
||||
|
||||
|
||||
def test_tampered_certificate_version_fails_verification() -> None:
|
||||
cert = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
tampered = dataclasses.replace(cert, certificate_version=CERTIFICATE_VERSION + 1)
|
||||
verdict = verify_certificate(tampered)
|
||||
assert verdict.verified is False
|
||||
assert verdict.reason == REPLAY_MISMATCH
|
||||
|
||||
|
||||
def test_swapped_entailment_trace_fails_verification() -> None:
|
||||
"""Strongest form: graft a *valid, also-ENTAILED* trace from a different
|
||||
proof — same decision and reason, different evidence keys. Replay must
|
||||
reject the certificate on the evidence, not the verdict label."""
|
||||
cert = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
other = _build("b", _coherent((1, "a"), (2, "a -> b")))
|
||||
assert other.decision == Entailment.ENTAILED.value
|
||||
grafted = dataclasses.replace(cert, entailment_trace=other.entailment_trace)
|
||||
verdict = verify_certificate(grafted)
|
||||
assert verdict.verified is False
|
||||
assert verdict.reason == REPLAY_MISMATCH
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# 5. Non sequitur: an unentailed claim cannot be certified entailed
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_non_sequitur_does_not_verify_as_entailed() -> None:
|
||||
cert = _build("q", _coherent((1, "p"))) # consistent with {p}, not entailed
|
||||
assert cert.decision == Entailment.UNKNOWN.value
|
||||
assert cert.reason == UNDETERMINED
|
||||
assert cert.promotion_positive is False
|
||||
# It verifies as what it honestly is...
|
||||
assert verify_certificate(cert).verified is True
|
||||
|
||||
# ...and forging the decision (or its reason) fails replay.
|
||||
forged = dataclasses.replace(cert, decision=Entailment.ENTAILED.value)
|
||||
assert verify_certificate(forged).verified is False
|
||||
forged_reason = dataclasses.replace(cert, reason=TAUTOLOGICAL_IMPLICATION)
|
||||
assert verify_certificate(forged_reason).verified is False
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# 6–7. Refusal-first: inconsistency and malformed input never vacuously entail
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_inconsistent_premises_refuse_not_vacuously_entail() -> None:
|
||||
cert = _build("q", _coherent((1, "p"), (2, "~p")))
|
||||
assert cert.decision == Entailment.REFUSED.value
|
||||
assert cert.reason == INCONSISTENT_PREMISES
|
||||
assert cert.decision != Entailment.ENTAILED.value
|
||||
assert cert.promotion_positive is False
|
||||
verdict = verify_certificate(cert)
|
||||
assert verdict.verified is True # the refusal itself replays
|
||||
assert verdict.reason == REPLAY_MATCH
|
||||
|
||||
|
||||
@pytest.mark.parametrize(
|
||||
"claim, premises",
|
||||
[
|
||||
("q", _coherent((1, "p -> ("))), # malformed premise
|
||||
("q -> (", _coherent((1, "p"))), # malformed claim
|
||||
("q", _coherent((1, "forall x. p(x)"))), # out-of-regime (quantified)
|
||||
],
|
||||
)
|
||||
def test_malformed_or_out_of_regime_refuses(
|
||||
claim: str, premises: tuple[PremiseRecord, ...]
|
||||
) -> None:
|
||||
cert = _build(claim, premises)
|
||||
assert cert.decision == Entailment.REFUSED.value
|
||||
assert cert.reason == OUT_OF_REGIME_OR_MALFORMED
|
||||
assert cert.promotion_positive is False
|
||||
assert verify_certificate(cert).verified is True
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# 8–9. Determinism: canonical premise order, byte-stable canonical_json
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_premise_order_is_canonical_and_deterministic() -> None:
|
||||
forward = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
reversed_input = _build("q", _coherent((2, "p -> q"), (1, "p")))
|
||||
assert forward.canonical_json() == reversed_input.canonical_json()
|
||||
assert forward.premise_entry_ids == (1, 2)
|
||||
assert forward.premise_forms == ("p", "p -> q")
|
||||
|
||||
|
||||
def test_canonical_json_is_byte_stable_across_double_construction() -> None:
|
||||
first = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
second = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
assert first.canonical_json() == second.canonical_json()
|
||||
# Canonical form: sorted keys, compact separators — re-serializing the
|
||||
# parsed payload under the same policy must be a fixed point.
|
||||
payload = first.canonical_json()
|
||||
assert payload == json.dumps(
|
||||
json.loads(payload), sort_keys=True, separators=(",", ":")
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# 10. Only ENTAILED (non-empty, all-coherent) is promotion-positive
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
@pytest.mark.parametrize(
|
||||
"claim, premises, expected_decision, expected_reason",
|
||||
[
|
||||
("q", _coherent((1, "p"), (2, "p -> ~q")),
|
||||
Entailment.REFUTED.value, TAUTOLOGICAL_REFUTATION),
|
||||
("q", _coherent((1, "p")),
|
||||
Entailment.UNKNOWN.value, UNDETERMINED),
|
||||
("q", _coherent((1, "p"), (2, "~p")),
|
||||
Entailment.REFUSED.value, INCONSISTENT_PREMISES),
|
||||
("q", _coherent((1, "p -> (")),
|
||||
Entailment.REFUSED.value, OUT_OF_REGIME_OR_MALFORMED),
|
||||
],
|
||||
)
|
||||
def test_non_entailed_outcomes_are_never_promotion_positive(
|
||||
claim: str,
|
||||
premises: tuple[PremiseRecord, ...],
|
||||
expected_decision: str,
|
||||
expected_reason: str,
|
||||
) -> None:
|
||||
cert = _build(claim, premises)
|
||||
assert cert.decision == expected_decision
|
||||
assert cert.reason == expected_reason
|
||||
assert cert.promotion_positive is False
|
||||
# Each outcome verifies as itself — refusals and unknowns are replayable
|
||||
# evidence too, just never promotion-positive.
|
||||
assert verify_certificate(cert).verified is True
|
||||
|
||||
|
||||
def test_entailed_over_non_coherent_recorded_status_is_not_positive() -> None:
|
||||
"""Valid entailment over a speculative premise: the certificate is honest
|
||||
evidence (verifies) but never promotion-positive — the recorded status
|
||||
gate is part of positivity, before P3's fresh-read gate even runs."""
|
||||
premises = (
|
||||
PremiseRecord(entry_id=1, form="p", status="coherent"),
|
||||
PremiseRecord(entry_id=2, form="p -> q", status="speculative"),
|
||||
)
|
||||
cert = _build("q", premises)
|
||||
assert cert.decision == Entailment.ENTAILED.value
|
||||
assert cert.promotion_positive is False
|
||||
assert verify_certificate(cert).verified is True
|
||||
|
||||
|
||||
def test_zero_premise_tautology_is_entailed_but_not_positive() -> None:
|
||||
"""A tautology is entailed by the empty set — sound, but fail-closed out
|
||||
of v1 promotion scope (module docstring; ratification question)."""
|
||||
cert = _build("q | ~q", ())
|
||||
assert cert.decision == Entailment.ENTAILED.value
|
||||
assert cert.promotion_positive is False
|
||||
assert verify_certificate(cert).verified is True
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Engine pin: recorded provenance, checkable only against a supplied pin
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_engine_pin_is_checked_when_expected_pin_is_supplied() -> None:
|
||||
cert = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
assert verify_certificate(cert, expected_engine_pin=_PIN).verified is True
|
||||
mismatch = verify_certificate(cert, expected_engine_pin="other-pin")
|
||||
assert mismatch.verified is False
|
||||
assert mismatch.reason == ENGINE_PIN_MISMATCH
|
||||
|
||||
|
||||
def test_engine_pin_tamper_passes_pure_replay_documented_wrinkle() -> None:
|
||||
"""HONEST LIMIT, pinned on purpose: the pin is carried verbatim through
|
||||
the rebuild, so pure replay cannot detect pin tampering — the module has
|
||||
no filesystem and nothing true to compare against. P3 MUST pass
|
||||
expected_engine_pin (the deductive-lane SHA in force) to close this."""
|
||||
cert = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
tampered = dataclasses.replace(cert, engine_pin="forged-pin")
|
||||
assert verify_certificate(tampered).verified is True
|
||||
checked = verify_certificate(tampered, expected_engine_pin=_PIN)
|
||||
assert checked.verified is False
|
||||
assert checked.reason == ENGINE_PIN_MISMATCH
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Structural fail-closed: contract violations raise / verify malformed
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_structural_contract_violations_raise() -> None:
|
||||
with pytest.raises(ValueError, match="duplicate premise entry_ids"):
|
||||
_build("q", _coherent((1, "p"), (1, "p -> q")))
|
||||
with pytest.raises(ValueError, match="closed vocabulary"):
|
||||
PremiseRecord(entry_id=1, form="p", status="definitely_legit")
|
||||
with pytest.raises(ValueError, match="entry_id must be an int"):
|
||||
PremiseRecord(entry_id=True, form="p", status="coherent")
|
||||
with pytest.raises(ValueError, match="premise form must be a str"):
|
||||
PremiseRecord(entry_id=1, form=None, status="coherent") # type: ignore[arg-type]
|
||||
with pytest.raises(ValueError, match="engine_pin"):
|
||||
build_certificate(
|
||||
claim_form="q", premises=_coherent((1, "p")), engine_pin=" "
|
||||
)
|
||||
with pytest.raises(ValueError, match="claim_form"):
|
||||
build_certificate(
|
||||
claim_form=None, # type: ignore[arg-type]
|
||||
premises=_coherent((1, "p")),
|
||||
engine_pin=_PIN,
|
||||
)
|
||||
|
||||
|
||||
def test_structurally_broken_certificates_verify_malformed() -> None:
|
||||
cert = _build("q", _coherent((1, "p"), (2, "p -> q")))
|
||||
# Field-length mismatch (zip strict in the rebuild).
|
||||
short = dataclasses.replace(cert, premise_forms=("p",))
|
||||
assert verify_certificate(short).reason == MALFORMED_CERTIFICATE
|
||||
# Tampered status outside the closed vocabulary.
|
||||
bad_status = dataclasses.replace(cert, premise_statuses=("coherent", "trusted"))
|
||||
assert verify_certificate(bad_status).reason == MALFORMED_CERTIFICATE
|
||||
# Non-serializable trace payload.
|
||||
junk = dataclasses.replace(cert, entailment_trace={"outcome": object()})
|
||||
assert verify_certificate(junk).reason == MALFORMED_CERTIFICATE
|
||||
for broken in (short, bad_status, junk):
|
||||
assert verify_certificate(broken).verified is False
|
||||
|
||||
|
||||
def test_verification_reasons_are_a_closed_vocabulary() -> None:
|
||||
assert VERIFICATION_REASONS == frozenset(
|
||||
{REPLAY_MATCH, REPLAY_MISMATCH, MALFORMED_CERTIFICATE, ENGINE_PIN_MISMATCH}
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# 11–12. Boundary hygiene: pure imports, no status-transition surface
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_certificate_module_imports_are_pure() -> None:
|
||||
"""No vault / teaching / session / runtime-shell import, no I/O or
|
||||
nondeterminism module — the certificate is evidence, not an actor."""
|
||||
tree = ast.parse(_CERTIFICATE_SOURCE)
|
||||
roots: set[str] = set()
|
||||
for node in ast.walk(tree):
|
||||
if isinstance(node, ast.Import):
|
||||
roots.update(alias.name.split(".")[0] for alias in node.names)
|
||||
elif isinstance(node, ast.ImportFrom):
|
||||
assert node.level == 0, "use absolute imports in certificate.py"
|
||||
assert node.module is not None
|
||||
roots.add(node.module.split(".")[0])
|
||||
allowed = {"__future__", "json", "dataclasses", "typing", "generate"}
|
||||
assert roots <= allowed, f"impure imports in certificate.py: {roots - allowed}"
|
||||
|
||||
forbidden_calls = {"eval", "exec", "open", "__import__", "compile"}
|
||||
offenders = [
|
||||
node.func.id
|
||||
for node in ast.walk(tree)
|
||||
if isinstance(node, ast.Call)
|
||||
and isinstance(node.func, ast.Name)
|
||||
and node.func.id in forbidden_calls
|
||||
]
|
||||
assert offenders == [], f"forbidden calls in certificate.py: {offenders}"
|
||||
|
||||
|
||||
def test_certificate_module_has_no_status_transition_surface() -> None:
|
||||
"""INV-29's own detector, applied directly: zero epistemic-status
|
||||
transition writes in certificate.py (the tree-wide INV-29 scan covers it
|
||||
too; this pins the file explicitly so a future edit fails loudly here)."""
|
||||
from tests.test_architectural_invariants import _status_transition_writes
|
||||
|
||||
tree = ast.parse(_CERTIFICATE_SOURCE)
|
||||
assert _status_transition_writes(tree) == 0
|
||||
status_literals = [
|
||||
node
|
||||
for node in ast.walk(tree)
|
||||
if isinstance(node, ast.Constant) and node.value == "epistemic_status"
|
||||
]
|
||||
assert status_literals == [], (
|
||||
"certificate.py must not handle the epistemic_status key at all — "
|
||||
"status strings arrive pre-read in PremiseRecord.status"
|
||||
)
|
||||
|
||||
|
||||
def test_status_vocab_matches_teaching_enum() -> None:
|
||||
"""The local closed vocab mirrors teaching.epistemic.EpistemicStatus
|
||||
values (generate/ must not import teaching/; this test owns the sync)."""
|
||||
from teaching.epistemic import EpistemicStatus
|
||||
|
||||
assert PREMISE_STATUS_VOCAB == frozenset(s.value for s in EpistemicStatus)
|
||||
Loading…
Reference in a new issue