From 1524fcc3c8be8ddd22af08a19a867a5f1ba25274 Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 11 Jun 2026 16:51:18 -0700 Subject: [PATCH] =?UTF-8?q?docs(adr):=20ratify=20ADR-0218=20=E2=80=94=20pr?= =?UTF-8?q?oof-carrying=20coherence=20promotion?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- ...0218-proof-carrying-coherence-promotion.md | 62 ++++++++++++++----- 1 file changed, 46 insertions(+), 16 deletions(-) diff --git a/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md b/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md index 80de9273..e7ca0f96 100644 --- a/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md +++ b/docs/decisions/ADR-0218-proof-carrying-coherence-promotion.md @@ -1,12 +1,15 @@ # 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 +**Status:** Accepted (ratified 2026-06-11) — D1–D4 accepted as proposed; the +completed ratification checklist at the bottom of this document records the +per-decision acceptance notes, including two fail-closed realizations +confirmed under D3. Ratification authorizes the P3 implementation (PR C) +through the existing mutation owner only: `teaching/proof_promotion.py` as a +pure decider plus `VaultStore.apply_certified_promotion` with independent +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) **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 @@ -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 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 @@ -207,12 +210,39 @@ explicit hazard surface and refuses on any gap. - Auto-demotion on REFUTED — open item, not in scope. - 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 - (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). +- [x] D1 ACCEPTED: split (pure decider / vault-owned mutation) over the + alternative (new INV-21 allowlist entry). `teaching/proof_promotion.py` + decides and never mutates; `vault/store.py` independently re-verifies + and owns the flip. No INV-21 allowlist change. +- [x] D2 ACCEPTED: reading stays curator-certified in the first cut + (`reading_certified: true` + the certified `propositional_form` stored + 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).