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

Merge pull request #693 from AssetOverflow/feat/pccp-adr-0218

Browse source 
docs(adr-0218): Proof-Carrying Coherence Promotion — proposal, INV-29, strict-xfail obligations (PR A)
This commit is contained in:
Shay 2026-06-11 15:59:58 -07:00 committed by GitHub
commit b52e0e1c7e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 741 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -0,0 +1,211 @@
# ADR-0218 — Proof-Carrying Coherence Promotion (logical arm of ADR-0021 v2)
**Status:** Proposed — NOT ratified. No runtime mutation-path code is
authorized by this document. The PR that introduces this ADR ships only
(a) this proposal and (b) executable proof obligations
(`tests/test_proof_carrying_promotion_obligations.py`, strict-xfail) plus a
new structural invariant (INV-29) that pins the *current* promotion-site
surface before any new promoter exists.
**Date:** 2026-06-11
**Authors:** drafted by agent for architect review (Joshua Shay ratifies)
**Governing issue:** [docs/issues/proof-carrying-coherence-promotion.md](../issues/proof-carrying-coherence-promotion.md)
**Depends on:** ADR-0021 (Epistemic Grade Policy), ADR-0201/0202 (ROBDD
canonicalizer + representation contract), ADR-0203/0204/0205 (proof_chain
phases 2.1–2.3), the propositional entailment operator
(`generate/proof_chain/entail.py`, phase 2.4 — see §Context numbering note),
ADR-0148 (vault promotion policy wiring), INV-21/22/23.
---
## Context
PR #691 corrected the doctrine: a system's own *asserted* output has no
standing, but a claim *deductively entailed* by an already-`COHERENT`
premise set can be machine-certified as a coherence judgment, because for
that subclass the entailment proof **is** the coherence judgment ADR-0021 §3
requires. The governing issue specifies the capability; this ADR proposes
the rulings the issue (§9) demands before any code.
### What exists today (verified 2026-06-11, main@187b008b)
- **Sound + complete propositional engine.**
`generate/proof_chain/entail.py::evaluate_entailment_with_trace` decides
`premises ⊨ query` on the ADR-0201 ROBDD keystone. Refusal-first:
inconsistent premises and out-of-regime input refuse, never guess.
- **A deterministic proof-evidence artifact already exists.**
`EntailmentTrace` carries `premise_keys`, `conjunction_key`, `query_key`,
`entailment_check_key`, `refutation_check_key` and a `canonical_json()`
serialization. Replay re-verification = recompute from `(premises, query)`
and compare byte-for-byte.
- **proof_chain Phase 2 is NOT a pending prerequisite — it shipped.**
The issue (§5, §8 P2) treats binding-graph wiring, acyclicity refusal, and
modus_ponens as a prerequisite still to build. As of ADR-0203/0204/0205
(all Accepted, 2026-06-02) plus the phase-2.4 entailment operator, all of
it is implemented and tested (`tests/test_proof_chain_*.py`,
`tests/test_deductive_logic_entail.py`, `evals/deductive_logic/` SHA-pinned
lane). What P2 still owes is narrower: a *promotion certificate* binding an
`EntailmentTrace` to concrete vault entries, plus its replay verifier.
- **Numbering note (cleanup owed, not done here):** the entail.py module
docstring attributes phase 2.4 to "ADR-0206", which collides with the
committed `ADR-0206-response-governance-bridge.md`. Phase 2.4 has no
committed ADR of its own. The PR that lands P2 must fix that docstring to
cite this ADR's §Interface instead.
### The precedent the issue missed: ADR-0148 already automates a promotion
`VaultStore.promote_eligible_entries(policy)` (ADR-0148, Accepted
2026-05-25) already flips `SPECULATIVE → COHERENT` **in place**, gated by an
energy/coherence-residual policy, called from `chat/runtime.py` behind
`RuntimeConfig.vault_promotion_enabled` (default `False`). Two consequences:
1. "Promotion is curator-mediated today" is not strictly true — an
energy-arm precedent exists. This ADR positions the logical arm beside
it, not as the first automation.
2. **ADR-0148 exposed a blind spot in INV-21.** INV-21's AST scan catches
`*.store(...)` calls. An in-place `epistemic_status` metadata mutation is
*not* a `store()` call, so the most natural implementation shape for a
promoter — flip the status on an existing entry — would silently bypass
the one-mutation-path invariant as written. The issue names INV-21 as
"highest risk"; in fact INV-21 *cannot see* the riskiest shape.
**Therefore this proposal introduces INV-29 now** (status-transition
sites are allowlisted), in the same PR as this document, so the boundary
exists *before* any promoter does.
## Decision (proposed — each item requires ratification)
### D1. Extend the existing mutation owner; do not add a write path
Promotion is an epistemic-status *transition*, not a new vault write. The
split mirrors ADR-0148's accepted shape — policy decides, vault mutates:
- `teaching/proof_promotion.py` (new, P3): **pure decision logic.** Builds
and verifies the certificate; performs **no mutation** and holds no vault
write access. Not a parallel learning path: it produces a decision object
consumed by the single mutation owner.
- `vault/store.py` (existing INV-21/INV-29 allowlisted module): gains one
method, `apply_certified_promotion(entry_index, certificate)`, which
**independently re-verifies the certificate** (recompute the entailment
trace; compare byte-for-byte; re-check premise statuses) before flipping
the entry's status. A certificate that does not re-verify mutates nothing.
No INV-21 allowlist change. INV-29's allowlist stays `{vault/store.py}`.
### D2. The reading stays curator-mediated in the first cut
The hazard-bearing step is the NL→proposition reading, not the deduction
(issue §4). P3 ships with:
- Every premise's propositional form is a **curator-certified reading**
stored with the vault entry (`reading_certified: true` + the certified
form), never proposer-supplied at decision time.
- The candidate claim's propositional form is likewise a curator-certified
*reading* (certifying the translation is faithful certifies nothing about
the claim's coherence — that is exactly the relocation: human certifies
the reading, engine certifies the entailment).
- Any premise or claim without a certified reading → **refuse, no
promotion.** Fail-closed is the only failure mode.
A structural (non-curator) reading check is future work and requires its own
ADR; it is out of scope here.
### D3. Exact admissibility predicate
`certify_promotion` promotes **iff all** of the following hold; any failure
refuses (claim stays `SPECULATIVE`):
```text
1. Every premise ref resolves to a stored vault entry, fresh-read at
decision time, with epistemic_status == COHERENT.
2. Every premise form and the claim form are curator-certified readings
(D2); forms are taken from the store, never from the proposer.
3. evaluate_entailment_with_trace(premise_forms, claim_form).outcome
== ENTAILED. (REFUTED / UNKNOWN / REFUSED never promote.)
4. The embedded EntailmentTrace re-verifies: recomputing from the stored
forms reproduces canonical_json() byte-for-byte.
5. No proposer-supplied proof / status / confidence field is read by the
decision. (Echo-and-ignore, as demos/epistemic_truth_state does for
proposed_state.)
```
`REFUTED` does **not** auto-demote to `CONTESTED` in v1 — demotion is a
separate authority question, recorded as an open item, not smuggled in here.
### D4. The certificate is the audit artifact and folds into the trace hash
`PromotionCertificate` (provisional fields; the strict-xfail tests are the
executable spec and will be reconciled at P3):
```text
claim_form — certified propositional form of the claim
premise_entry_ids — vault identities of the premises
premise_forms — certified forms, as read from the store
premise_statuses — statuses observed at decision time
entailment_trace — EntailmentTrace.as_dict()
engine_pin — the deductive_logic lane SHA in force
decision / reason — promoted | refused + closed reason vocab
```
The certificate's canonical JSON SHA-256 folds into the turn `trace_hash`
(ADR-0021 §Schema impact already requires status there). Replay re-verifies
the certificate, not just the status.
## Phasing (maps to the PR stack)
- **PR A (this PR).** This proposal + strict-xfail obligations + INV-29.
No runtime change. Obligation tests xfail today; INV-29 and the honesty
pins pass today.
- **PR B.** `PromotionCertificate` + builder + replay verifier as a pure,
side-effect-free module with its own tests. No promotion, no vault method,
no status transition anywhere. Retires the certificate-shaped xfails only.
- **PR C (requires this ADR ratified).** `certify_promotion` +
`VaultStore.apply_certified_promotion` behind the existing mutation owner.
Retires the remaining xfails (strict-xpass forces it); INV-21 allowlist
unchanged; INV-29 allowlist unchanged; full + deductive lanes wrong=0.
- **PR D.** Local deterministic demo (`demos/` pattern): proposer submits
claim + proof candidate; CORE ignores the candidate, recomputes, promotes
or refuses on pinned verification only. No network, no model API, no side
effects outside the demo arena.
## Proof obligations ↔ tests
| # | Obligation (issue §7) | Test (PR A) | State today |
|---|---|---|---|
| O1 | Entailed-from-COHERENT promotes; artifact re-verifies | `test_O1_*` | xfail(strict) |
| O2 | Consistent-but-not-entailed stays SPECULATIVE | `test_O2_*` | xfail(strict) |
| O3 | Any non-COHERENT premise → refuse | `test_O3_*` | xfail(strict) |
| O4 | Misread premise fails closed | `test_O4_*` | xfail(strict) |
| O5 | Proposer proof/status/confidence ignored, byte-identical decision | `test_O5_*` | xfail(strict) |
| O6 | No new mutation path | INV-21 (existing) + INV-29 (this PR) | passing |
| O7 | Determinism + replay re-verification | `test_O7_*` (promoter: xfail) + `test_pin_entailment_trace_*` (substrate: passing) | split |
| O8 | wrong=0 lanes stay green | existing lane gates + `verify_lane_shas` | passing |
Honesty pins (pass today, flip red the moment the feature is wired without
conscious review): `review_correction` carries status as an input and does
not compute it; `teaching.proof_promotion` does not exist.
## Trust boundary
The untrusted inputs are the proposer's claim text and anything the proposer
attaches (proof candidate, status, confidence). All of it is **data, never
authority**: forms come from curator-certified store state, the proof is
recomputed by the pinned engine, and the decision must be byte-identical
with and without proposer attachments. The reading-certification step is the
explicit hazard surface and refuses on any gap.
## Non-goals
- The geometric arm (`cga_inner ≥ τ`) — separate ADR-0021 v2 work.
- Promotion of generated/asserted output — permanently forbidden.
- Source authority or confidence weighting — permanently forbidden.
- Auto-demotion on REFUTED — open item, not in scope.
- Any structural (non-curator) reading certification — future ADR.
## Ratification checklist (architect)
- [ ] D1 split (pure decider / vault-owned mutation) over the alternative
(new INV-21 allowlist entry).
- [ ] D2 first cut: reading stays curator-certified; entailment automated.
- [ ] D3 predicate exact as stated (including REFUTED → no transition).
- [ ] D4 certificate fields + trace-hash folding.
- [ ] INV-29 as the permanent transition-site boundary (already shipped in
the proposing PR as a passing invariant; ratification confirms it).

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

@ -1,6 +1,10 @@
# Issue — Proof-carrying coherence promotion (the logical arm of ADR-0021's v2 gap)
**Status:** Open — specification only, no code authorized
**Status:** Open — [ADR-0218 proposed](../decisions/ADR-0218-proof-carrying-coherence-promotion.md)
(2026-06-11, awaiting ratification); runtime code remains unauthorized.
Executable proof obligations shipped as strict-xfail in
`tests/test_proof_carrying_promotion_obligations.py`; INV-29 now pins the
status-transition-site allowlist.
**Raised:** 2026-06-11
**Surface:** `teaching/epistemic.py`, `teaching/review.py`, the deductive
engine (`deductive_logic_v1`), `vault/store.py`, INV-21 one-mutation-path

257
tests/test_architectural_invariants.py
View file

@ -1718,3 +1718,260 @@ class TestINV28MeaningGraphNeutrality:
"INV-28a predicate failed to flag a module known to import the "
"field engine — the neutrality check is vacuous."
)
# ===========================================================================
# INV-29 Epistemic-status transition sites are allowlisted
# ===========================================================================
#
# Claim (ADR-0021 §3 + ADR-0218 §Context):
# INV-21 polices `VaultStore.store(...)` callers, but a SPECULATIVE→COHERENT
# *transition* on an already-stored entry is not a store() call — it is an
# in-place assignment to the entry's `epistemic_status` metadata key.
# ADR-0148's `promote_eligible_entries` proved this shape exists and that
# INV-21's AST scan cannot see it. Without this invariant, a new promoter
# (including the ADR-0218 proof-carrying promoter, or any future fast-path)
# could flip stored claims to admissible-as-evidence without tripping any
# structural check.
#
# This test AST-asserts the write-site set: every production write of an
# `epistemic_status` key/attribute — direct assignment (incl. tuple-unpacking
# and the recall-reference backdoor) or mutation call (.update / .setdefault /
# __setitem__ / setattr) — must live in an allowlisted module. Adding a new
# transition site is allowed but must be intentional — edit the allowlist and
# document the justification here in the same commit.
#
# Allowlist rationale per site:
# vault/store.py — the single mutation owner. Two sites today:
# store() stamping at write time (param-only; callers
# cannot smuggle status via the metadata dict), and
# ADR-0148 promote_eligible_entries (energy-policy
# promotion, opt-in flag, default off). ADR-0218 proposes
# its proof-carrying transition land HERE too
# (apply_certified_promotion), keeping this list unchanged.
ALLOWED_STATUS_TRANSITION_SITES: frozenset[str] = frozenset({
"vault/store.py",
})
_STATUS_KEY = "epistemic_status"
def _flatten_assign_targets(target: ast.expr) -> list[ast.expr]:
"""Recurse through tuple/list/starred unpacking to the leaf targets,
so `meta["epistemic_status"], x = a, b` cannot hide a write."""
if isinstance(target, (ast.Tuple, ast.List)):
out: list[ast.expr] = []
for elt in target.elts:
out.extend(_flatten_assign_targets(elt))
return out
if isinstance(target, ast.Starred):
return _flatten_assign_targets(target.value)
return [target]
def _dict_literal_has_status_key(expr: ast.expr) -> bool:
return isinstance(expr, ast.Dict) and any(
isinstance(k, ast.Constant) and k.value == _STATUS_KEY for k in expr.keys
)
def _dict_ctor_has_status_kwarg(expr: ast.expr) -> bool:
return (
isinstance(expr, ast.Call)
and isinstance(expr.func, ast.Name)
and expr.func.id == "dict"
and any(kw.arg == _STATUS_KEY for kw in expr.keywords)
)
def _call_writes_status_key(node: ast.Call) -> bool:
"""True iff this call shape can write the `epistemic_status` key/attr.
Mutation-call shapes covered (the indirections an assignment scan misses):
m.update({"epistemic_status": ...}) dict-literal positional
m.update(epistemic_status=...) keyword
m.update(**{"epistemic_status": ...}) **-unpacked literal dict
m.update(dict(epistemic_status=...)) dict() ctor positional
m.setdefault("epistemic_status", ...) write-if-absent
m.__setitem__("epistemic_status", ...) bound __setitem__
dict.__setitem__(m, "epistemic_status", ...) unbound __setitem__
setattr(entry, "epistemic_status", ...) attribute write by name
"""
func = node.func
func_attr = func.attr if isinstance(func, ast.Attribute) else ""
func_name = func.id if isinstance(func, ast.Name) else ""
if func_attr == "update":
if any(
_dict_literal_has_status_key(arg) or _dict_ctor_has_status_kwarg(arg)
for arg in node.args
):
return True
for kw in node.keywords:
if kw.arg == _STATUS_KEY:
return True
if kw.arg is None and _dict_literal_has_status_key(kw.value):
return True
return False
# Key arrives as a positional constant: setdefault(key, v),
# m.__setitem__(key, v), dict.__setitem__(m, key, v), setattr(o, key, v).
# "Any positional constant equals the key" covers every arity without
# per-shape position logic; a literal "epistemic_status" positional in
# one of these writers is a transition write by definition.
if func_attr in ("setdefault", "__setitem__") or func_name == "setattr":
return any(
isinstance(arg, ast.Constant) and arg.value == _STATUS_KEY
for arg in node.args
)
return False
def _status_transition_writes(tree: ast.AST) -> int:
"""Count sites that write an `epistemic_status` key/attr.
Direct-assignment shapes:
meta["epistemic_status"] = ... (subscript with constant key)
entry.epistemic_status = ... (attribute assignment)
hit["metadata"]["epistemic_status"] = ... (recall-reference backdoor)
plus the mutation-call shapes in `_call_writes_status_key` and writes
hidden inside tuple-unpacking targets.
Uses AST so comments/docstrings/strings cannot trigger false positives.
Honest scope note: a *variable* key (`meta[k] = ...` where k happens to
equal "epistemic_status" at runtime), exec/eval, and C-level aliasing are
statically undetectable — those belong to review, not this scan. The scan
pins every plain-code write surface.
"""
count = 0
for node in ast.walk(tree):
targets: list[ast.expr] = []
if isinstance(node, ast.Assign):
for t in node.targets:
targets.extend(_flatten_assign_targets(t))
elif isinstance(node, (ast.AnnAssign, ast.AugAssign)):
targets = _flatten_assign_targets(node.target)
elif isinstance(node, ast.Call) and _call_writes_status_key(node):
count += 1
for target in targets:
if (
isinstance(target, ast.Subscript)
and isinstance(target.slice, ast.Constant)
and target.slice.value == _STATUS_KEY
):
count += 1
elif (
isinstance(target, ast.Attribute)
and target.attr == _STATUS_KEY
):
count += 1
return count
def _file_status_transition_count(path: Path) -> int:
try:
tree = ast.parse(path.read_text())
except (OSError, SyntaxError):
return 0
return _status_transition_writes(tree)
class TestINV29EpistemicStatusTransitionSites:
"""
Claim: Only modules in ALLOWED_STATUS_TRANSITION_SITES may assign to an
`epistemic_status` key or attribute. A new assignment site is a new
promotion/demotion authority over the revision graph and must be
reviewed — coherence stops being the only admission signal the moment an
unreviewed site can flip a claim to COHERENT (ADR-0021 §3, ADR-0218).
"""
def test_no_unallowlisted_status_transition_sites(self):
offenders: list[str] = []
for path in _enumerate_project_py_files():
if _file_status_transition_count(path) == 0:
continue
rel = str(path.relative_to(PROJECT_ROOT_FOR_INV21))
if rel not in ALLOWED_STATUS_TRANSITION_SITES:
offenders.append(rel)
assert not offenders, (
"New epistemic-status transition site(s) detected outside the "
"allowlist:\n " + "\n ".join(offenders)
+ "\n\nIf this is intentional, add the path to "
"ALLOWED_STATUS_TRANSITION_SITES in "
"tests/test_architectural_invariants.py with a one-line "
"justification in the comment block above the set. Every "
"additional transition site is a new promotion authority over "
"the epistemic schema (ADR-0021 §3, ADR-0218)."
)
def test_allowlist_is_actually_used(self):
"""Drift guard — if an allowlisted module no longer assigns status,
remove it to keep the trust surface tight."""
used: set[str] = set()
for path in _enumerate_project_py_files():
if _file_status_transition_count(path) > 0:
rel = str(path.relative_to(PROJECT_ROOT_FOR_INV21))
if rel in ALLOWED_STATUS_TRANSITION_SITES:
used.add(rel)
unused = ALLOWED_STATUS_TRANSITION_SITES - used
assert not unused, (
f"Allowlisted site(s) no longer assign epistemic_status: "
f"{sorted(unused)}\nRemove from ALLOWED_STATUS_TRANSITION_SITES."
)
def test_detector_is_non_vacuous(self):
"""29b — prove 29a can fail: the predicate flags every covered write
shape — direct assignments (incl. the recall-reference backdoor and
tuple-unpacking) AND mutation-call indirections."""
shapes = (
# direct assignment
"meta['epistemic_status'] = 'coherent'",
"entry.epistemic_status = STATUS",
"hit['metadata']['epistemic_status'] = 'coherent'",
"meta['epistemic_status'], x = 'coherent', 1",
# mutation calls
"metadata.update({'epistemic_status': 'coherent'})",
"entry.metadata.update(epistemic_status='coherent')",
"metadata.update(**{'epistemic_status': 'coherent'})",
"metadata.update(dict(epistemic_status='coherent'))",
"hit['metadata'].update({'epistemic_status': 'coherent'})",
"metadata.setdefault('epistemic_status', 'coherent')",
"metadata.__setitem__('epistemic_status', 'coherent')",
"dict.__setitem__(metadata, 'epistemic_status', 'coherent')",
"setattr(entry, 'epistemic_status', status)",
)
missed = [
s for s in shapes if _status_transition_writes(ast.parse(s)) != 1
]
assert not missed, (
"INV-29 predicate failed to flag known status-write shape(s):\n "
+ "\n ".join(missed)
+ "\n— the transition-site scan has gone partially blind."
)
def test_detector_ignores_reads_and_unrelated_writes(self):
"""29b' — the widened predicate must not cry wolf: reads, other keys,
and dict-literal *construction* (serialization builders) stay clean."""
clean = (
"x = meta['epistemic_status']\n"
"meta['energy_class'] = 'E0'\n"
"meta.update({'energy_raw': 0.5})\n"
"d = {'epistemic_status': self.epistemic_status.value}\n"
"getattr(entry, 'epistemic_status')\n"
)
assert _status_transition_writes(ast.parse(clean)) == 0, (
"INV-29 predicate flagged a read/unrelated write — false "
"positives would train people to allowlist reflexively."
)
def test_vault_store_sites_are_visible(self):
"""29c — the scan actually sees the two known vault/store.py sites
(store-time stamp + ADR-0148 promotion). If this drops to zero the
scan went blind, not clean."""
vault_path = PROJECT_ROOT_FOR_INV21 / "vault" / "store.py"
assert _file_status_transition_count(vault_path) >= 2, (
"Expected the store() stamp and the ADR-0148 promotion site in "
"vault/store.py to be visible to the INV-29 scan."
)

268
tests/test_proof_carrying_promotion_obligations.py Normal file
View file

@ -0,0 +1,268 @@
"""ADR-0218 PR A — executable proof obligations for proof-carrying coherence
promotion. THE FEATURE IS NOT LIVE.
Two kinds of tests, per the strict-xfail gate convention
(see tests/test_edge_budget_gate.py):
- HONESTY PINS (pass today). They assert the *current* truth the governing
issue documents: promotion is not computed, the promoter module does not
exist, and the entailment substrate the future promoter will consume is
replay-stable. The moment someone wires promotion without consciously
revisiting this file, a pin flips red.
- OBLIGATIONS O1–O5, O7 (xfail today, strict). Executable spec for the
ADR-0218 P3 promoter (`teaching/proof_promotion.py`). Each body imports
the not-yet-existing module, so today they xfail on ImportError. When P3
lands, strict=True turns any still-marked passing test into a loud XPASS
failure — the P3 PR must retire the markers and make every obligation pass
for real. A test that passes under a broken implementation is decoration
(CLAUDE.md §Schema-Defined Proof Obligations); these cannot pass at all
until the implementation exists.
O6 (no new mutation path) is enforced continuously by INV-21 + INV-29 in
tests/test_architectural_invariants.py, not here. O8 (wrong=0 lanes) is
enforced by the existing lane gates + scripts/verify_lane_shas.py.
API surface used in the xfail bodies is PROVISIONAL per ADR-0218 §D3/§D4 —
P3 may adjust signatures, but must preserve each obligation's semantics.
"""
from __future__ import annotations
import importlib
import importlib.util
import numpy as np
import pytest
from algebra.cga import embed_point
from generate.intent import DialogueIntent, IntentTag
from generate.proof_chain import Entailment, evaluate_entailment_with_trace
from teaching.correction import CorrectionCandidate
from teaching.epistemic import EpistemicStatus
from teaching.review import review_correction
from vault.store import VaultStore
_PROMOTER_MODULE = "teaching.proof_promotion"
_XFAIL_REASON = (
"ADR-0218 is Proposed, not ratified — the proof-carrying promoter "
f"({_PROMOTER_MODULE}) does not exist. This test is the executable "
"obligation; the P3 PR must retire this marker and make it pass."
)
def _promoter():
"""Import the future promoter. Raises ModuleNotFoundError today (→ xfail)."""
return importlib.import_module(_PROMOTER_MODULE)
def _versor(seed: int) -> np.ndarray:
rng = np.random.default_rng(seed)
return embed_point(rng.standard_normal(3).astype(np.float32))
def _store_premise(
vault: VaultStore,
seed: int,
form: str,
status: EpistemicStatus,
*,
certified: bool = True,
) -> int:
"""Store a premise entry carrying a curator-certified reading (ADR-0218 §D2)."""
return vault.store(
_versor(seed),
{
"propositional_form": form,
"reading_certified": certified,
},
epistemic_status=status,
)
# ---------------------------------------------------------------------------
# Honesty pins — pass today, flip red when reality changes
# ---------------------------------------------------------------------------
def test_pin_promoter_module_does_not_exist_yet() -> None:
"""The feature is designed-but-unwired. This pin goes red in the same PR
that creates the module, forcing the xfail markers below to be revisited
(and this pin deleted) consciously rather than by drift."""
assert importlib.util.find_spec(_PROMOTER_MODULE) is None, (
f"{_PROMOTER_MODULE} now exists — ADR-0218 P3 is landing. Delete this "
"pin AND retire every xfail marker in this file in the same PR; each "
"obligation below must now pass on its own."
)
def test_pin_review_correction_carries_status_it_does_not_compute() -> None:
"""Issue §1: `epistemic_status` is a passed-in parameter of
review_correction, not a computed coherence judgment. If a coherence
computation is ever added there, this pin flips and the change must be
reconciled with ADR-0218 (which routes computed promotion through the
vault transition owner, NOT through review_correction)."""
candidate = CorrectionCandidate(
correction_text="the sky is blue",
intent=DialogueIntent(tag=IntentTag.CORRECTION, subject="sky"),
prior_surface="the sky is green",
prior_turn=1,
candidate_id="pin-0001",
)
defaulted = review_correction(candidate)
assert defaulted.epistemic_status is EpistemicStatus.SPECULATIVE
# The curator-supplied input flows through verbatim — no computation runs.
echoed = review_correction(candidate, epistemic_status=EpistemicStatus.COHERENT)
assert echoed.epistemic_status is EpistemicStatus.COHERENT, (
"review_correction no longer carries the curator-supplied status "
"verbatim — a computation was added. Reconcile with ADR-0218 before "
"merging: promotion logic must not fork into a parallel path here."
)
def test_pin_entailment_trace_substrate_is_replay_stable() -> None:
"""O7's substrate half, testable today: the engine's proof evidence is
deterministic and re-verifies by recomputation — the property the
PromotionCertificate replay verifier (PR B) will rely on."""
premises = ("p", "p -> q")
first = evaluate_entailment_with_trace(premises, "q")
second = evaluate_entailment_with_trace(premises, "q")
assert first.outcome is Entailment.ENTAILED
assert first.canonical_json() == second.canonical_json(), (
"EntailmentTrace is not replay-stable — PR B's certificate "
"re-verification has no substrate to stand on."
)
# A non-entailed query must be UNKNOWN, not promoted-shaped evidence.
unknown = evaluate_entailment_with_trace(("p",), "q")
assert unknown.outcome is Entailment.UNKNOWN
# ---------------------------------------------------------------------------
# Obligations — xfail(strict) until ADR-0218 is ratified and P3 lands
# ---------------------------------------------------------------------------
@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON)
def test_O1_entailed_from_coherent_premises_promotes_with_reverifiable_proof() -> None:
"""Issue §7.1 — a claim deductively entailed by an all-COHERENT premise
set promotes, and the embedded proof re-verifies by recomputation."""
mod = _promoter()
vault = VaultStore(reproject_interval=0)
idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT)
idx_pq = _store_premise(vault, 2, "p -> q", EpistemicStatus.COHERENT)
decision = mod.certify_promotion(
claim_form="q",
premise_entry_indices=(idx_p, idx_pq),
vault=vault,
)
assert decision.promoted is True
# Replay re-verification: recomputing from the stored forms must
# reproduce the embedded trace byte-for-byte (ADR-0218 §D3.4).
recomputed = evaluate_entailment_with_trace(("p", "p -> q"), "q")
assert decision.certificate.entailment_trace == recomputed.as_dict()
@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON)
def test_O2_consistent_but_not_entailed_stays_speculative() -> None:
"""Issue §7.2 — mere consistency with the field is not entailment;
UNKNOWN never promotes."""
mod = _promoter()
vault = VaultStore(reproject_interval=0)
idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT)
decision = mod.certify_promotion(
claim_form="q", # consistent with {p}, not entailed by it
premise_entry_indices=(idx_p,),
vault=vault,
)
assert decision.promoted is False
@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON)
def test_O3_any_non_coherent_premise_refuses() -> None:
"""Issue §7.3 — a SPECULATIVE premise poisons the proof for promotion
purposes even when the entailment itself is valid."""
mod = _promoter()
vault = VaultStore(reproject_interval=0)
idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT)
idx_pq = _store_premise(vault, 2, "p -> q", EpistemicStatus.SPECULATIVE)
decision = mod.certify_promotion(
claim_form="q",
premise_entry_indices=(idx_p, idx_pq),
vault=vault,
)
assert decision.promoted is False
assert "premise" in decision.reason # closed reason vocab names the gate
@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON)
def test_O4_uncertified_reading_fails_closed() -> None:
"""Issue §7.4 — the reading is the hazard-bearing step. A premise whose
propositional form lacks reading certification must refuse, never fall
through to admission (ADR-0218 §D2)."""
mod = _promoter()
vault = VaultStore(reproject_interval=0)
idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT)
idx_pq = _store_premise(
vault, 2, "p -> q", EpistemicStatus.COHERENT, certified=False
)
decision = mod.certify_promotion(
claim_form="q",
premise_entry_indices=(idx_p, idx_pq),
vault=vault,
)
assert decision.promoted is False
assert "reading" in decision.reason
@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON)
def test_O5_proposer_supplied_proof_status_confidence_are_ignored() -> None:
"""Issue §7.5 — proposer attachments are data, never authority. The
decision must be byte-identical with and without them (echo-and-ignore,
as demos/epistemic_truth_state does for proposed_state)."""
mod = _promoter()
vault = VaultStore(reproject_interval=0)
idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT)
bare = mod.certify_promotion(
claim_form="q",
premise_entry_indices=(idx_p,),
vault=vault,
)
adorned = mod.certify_promotion(
claim_form="q",
premise_entry_indices=(idx_p,),
vault=vault,
proposer_payload={
"proof": "trust me, q follows",
"status": "coherent",
"confidence": 0.99,
},
)
assert bare.promoted is adorned.promoted is False
assert bare.certificate.canonical_json() == adorned.certificate.canonical_json()
@pytest.mark.xfail(strict=True, reason=_XFAIL_REASON)
def test_O7_promotion_decision_is_deterministic_and_replayable() -> None:
"""Issue §7.7 — double-run byte-identical; the certificate is the audit
artifact replay re-verifies (its hash folds into trace_hash at P3)."""
mod = _promoter()
def run():
vault = VaultStore(reproject_interval=0)
idx_p = _store_premise(vault, 1, "p", EpistemicStatus.COHERENT)
idx_pq = _store_premise(vault, 2, "p -> q", EpistemicStatus.COHERENT)
return mod.certify_promotion(
claim_form="q",
premise_entry_indices=(idx_p, idx_pq),
vault=vault,
)
first, second = run(), run()
assert first.certificate.canonical_json() == second.certificate.canonical_json()