docs(adr): ratify ADR-0218 — proof-carrying coherence promotion

Architect-directed ratification: D1 (pure decider / vault-owned mutation),
D2 (reading stays curator-certified in the first cut), D3 (exact predicate,
including REFUTED -> no transition), D4 (certificate fields + trace-hash
folding), and INV-29 as the permanent transition-site boundary, all ACCEPTED.

Two fail-closed realizations recorded under D3: the claim form is fresh-read
from the claim's own stored entry (never proposer-supplied), and zero-premise
tautology certificates refuse rather than promote in v1.

Docs-only: no runtime behavior changes in this commit. P3 implementation
(teaching/proof_promotion.py + VaultStore.apply_certified_promotion) follows
in the same PR as separate commits.
This commit is contained in:
Shay 2026-06-11 16:51:18 -07:00
parent 28916f2d0d
commit 1524fcc3c8

View file

@ -1,12 +1,15 @@
# ADR-0218 — Proof-Carrying Coherence Promotion (logical arm of ADR-0021 v2) # ADR-0218 — Proof-Carrying Coherence Promotion (logical arm of ADR-0021 v2)
**Status:** Proposed — NOT ratified. No runtime mutation-path code is **Status:** Accepted (ratified 2026-06-11) — D1D4 accepted as proposed; the
authorized by this document. The PR that introduces this ADR ships only completed ratification checklist at the bottom of this document records the
(a) this proposal and (b) executable proof obligations per-decision acceptance notes, including two fail-closed realizations
(`tests/test_proof_carrying_promotion_obligations.py`, strict-xfail) plus a confirmed under D3. Ratification authorizes the P3 implementation (PR C)
new structural invariant (INV-29) that pins the *current* promotion-site through the existing mutation owner only: `teaching/proof_promotion.py` as a
surface before any new promoter exists. pure decider plus `VaultStore.apply_certified_promotion` with independent
**Date:** 2026-06-11 re-verification. INV-29 is confirmed as the permanent transition-site
boundary; its allowlist stays `{vault/store.py}` and INV-21's allowlist is
unchanged.
**Date:** 2026-06-11 (proposed and ratified)
**Authors:** drafted by agent for architect review (Joshua Shay ratifies) **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) **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 **Depends on:** ADR-0021 (Epistemic Grade Policy), ADR-0201/0202 (ROBDD
@ -71,7 +74,7 @@ energy/coherence-residual policy, called from `chat/runtime.py` behind
sites are allowlisted), in the same PR as this document, so the boundary sites are allowlisted), in the same PR as this document, so the boundary
exists *before* any promoter does. exists *before* any promoter does.
## Decision (proposed — each item requires ratification) ## Decision (ratified 2026-06-11 — see the completed checklist below)
### D1. Extend the existing mutation owner; do not add a write path ### D1. Extend the existing mutation owner; do not add a write path
@ -207,12 +210,39 @@ explicit hazard surface and refuses on any gap.
- Auto-demotion on REFUTED — open item, not in scope. - Auto-demotion on REFUTED — open item, not in scope.
- Any structural (non-curator) reading certification — future ADR. - Any structural (non-curator) reading certification — future ADR.
## Ratification checklist (architect) ## Ratification checklist (architect) — completed 2026-06-11
- [ ] D1 split (pure decider / vault-owned mutation) over the alternative - [x] D1 ACCEPTED: split (pure decider / vault-owned mutation) over the
(new INV-21 allowlist entry). alternative (new INV-21 allowlist entry). `teaching/proof_promotion.py`
- [ ] D2 first cut: reading stays curator-certified; entailment automated. decides and never mutates; `vault/store.py` independently re-verifies
- [ ] D3 predicate exact as stated (including REFUTED → no transition). and owns the flip. No INV-21 allowlist change.
- [ ] D4 certificate fields + trace-hash folding. - [x] D2 ACCEPTED: reading stays curator-certified in the first cut
- [ ] INV-29 as the permanent transition-site boundary (already shipped in (`reading_certified: true` + the certified `propositional_form` stored
the proposing PR as a passing invariant; ratification confirms it). on the entry); the entailment is automated. A structural (non-curator)
reading certifier remains future work under its own ADR.
- [x] D3 ACCEPTED: predicate exact as stated, including REFUTED → no
transition (and no auto-demotion — open item stays open). Two
fail-closed realizations are confirmed with it:
(a) clause 2's "forms are taken from the store, never from the
proposer" applies to the **claim** as well — the P3 surface takes a
`claim_entry_index` and fresh-reads the claim's certified form from
its stored entry, adjusting the PR-A provisional API (sanctioned by
the obligations file's provisional-API note) in the strengthening
direction; and
(b) zero-premise (tautology) certificates do not promote in v1 —
D3.1 is vacuous over an empty premise set, so the empty set is
refused rather than waved through (matches PR B's fail-closed
`promotion_positive`).
- [x] D4 ACCEPTED: certificate fields as landed in PR B
(`generate/proof_chain/certificate.py`; plus `certificate_version`,
additive). Reconciliation per this section's "provisional fields"
note: the certificate's `decision`/`reason` carry the engine's closed
vocabulary (`entailed`/`refuted`/`unknown`/`refused`), and the
promoted-vs-refused decision lives on the P3 decision object.
Trace-hash folding: P3 emits the certificate's canonical-JSON SHA-256
on the decision object; folding into a turn `trace_hash` binds on the
first runtime caller (PR D or later) — no runtime turn path performs
promotion at P3.
- [x] INV-29 ACCEPTED as the permanent transition-site boundary; allowlist
stays `{vault/store.py}` (shipped passing in the proposing PR;
ratification confirms it).