e473f5b55f
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.
30 lines
1.3 KiB
Python
30 lines
1.3 KiB
Python
"""Deductive-engine provenance pin (ADR-0218 §D4).
|
|
|
|
``DEDUCTIVE_ENGINE_PIN`` mirrors ``PINNED_SHAS["deductive_logic_v1"]`` in
|
|
``scripts/verify_lane_shas.py`` — the SHA-256 of the deductive lane report
|
|
produced by the engine build in force. It is the value the P3 promoter
|
|
stamps into every ``PromotionCertificate`` (``engine_pin``) and the value
|
|
``VaultStore.apply_certified_promotion`` demands back via
|
|
``verify_certificate(..., expected_engine_pin=...)``.
|
|
|
|
Why a mirrored constant instead of reading the registry: ``scripts/`` is not
|
|
an importable runtime package, and the certificate module is deliberately
|
|
filesystem-free (PR B honesty boundary: pure replay cannot *know* the true
|
|
pin). The sync is pinned by
|
|
``tests/test_adr_0218_proof_promotion.py::test_engine_pin_matches_lane_registry``,
|
|
which AST-parses the registry — drift between the two fails the suite.
|
|
|
|
When the deductive lane re-pins (an intentional engine change), update this
|
|
constant in the same commit. Certificates built under the old pin then fail
|
|
apply-time pin verification — that is the desired alarm: an entailment proved
|
|
by a different engine build must be re-certified, not trusted across the
|
|
engine change.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
from typing import Final
|
|
|
|
DEDUCTIVE_ENGINE_PIN: Final[str] = (
|
|
"97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f"
|
|
)
|