Commit graph

1 commit

Author SHA1 Message Date
Shay
e473f5b55f feat(teaching): ADR-0218 P3 — proof-carrying coherence promotion
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.
2026-06-11 17:02:45 -07:00