feat(verified): P1-C — split bound_slots_digest into a separate VERIFIED obligation
Proof-object hardening before any serving wiring (review of #663): the "from the stated quantities" obligation is now THREE separable digests, not folded into derivation_digest — for replay, audit, and failure localization. core/epistemic_disclosure/verified_contract.py: - VerificationProof gains bound_slots_digest (the answer binds to a STATED slot — the asked unknown — not a phantom), between derivation_digest and back_substitution_digest. - VerificationObligation gains requires_bound_slots (VERIFICATION_OBLIGATION strict); evaluate_verification adds the REASON_NO_BOUND_SLOTS check. evals/constraint_oracle/verified_producer.py: populates bound_slots_digest from unknowns_signature + query_signature + the bound solution, ONLY when the asked unknown is in the solution (empty for a phantom answer). A complete derivation does NOT imply the answer bound to a declared slot, so the two are distinct obligations: test_derivation_digest_alone_is_insufficient_without_bound_slots proves it (relaxing requires_bound_slots is what admits the gap — load-bearing). All 7 real r2_gold 'solved' problems still VERIFY (bound_slots populated); wrong=0. Contract+producer suites 106/0; smoke 90/0. Still off-serving.
This commit is contained in:
parent
05b83a57cf
commit
e1e8426d97
4 changed files with 62 additions and 1 deletions
|
|
@ -64,6 +64,7 @@ class VerificationObligation:
|
|||
|
||||
requires_independent_read: bool # two DISTINCT reader lineages — not the same read twice
|
||||
rejects_wrong_read_even_if_solved: bool # the two reads must CONVERGE — catches a wrong read
|
||||
requires_bound_slots: bool # the answer binds to the STATED slots (query/unknowns), not phantom ones
|
||||
requires_back_substitution: bool # the answer back-substitutes into the canonical structure
|
||||
requires_boundary_clear: bool # no organ boundary fired in the chain
|
||||
|
||||
|
|
@ -72,6 +73,7 @@ class VerificationObligation:
|
|||
VERIFICATION_OBLIGATION: VerificationObligation = VerificationObligation(
|
||||
requires_independent_read=True,
|
||||
rejects_wrong_read_even_if_solved=True,
|
||||
requires_bound_slots=True,
|
||||
requires_back_substitution=True,
|
||||
requires_boundary_clear=True,
|
||||
)
|
||||
|
|
@ -86,6 +88,14 @@ class VerificationProof:
|
|||
``independent_reader_lineage`` must DIFFER (independence), and ``primary_read_digest``
|
||||
/ ``independent_read_digest`` must MATCH (convergence on one canonical structure).
|
||||
Independence + convergence together are what reject a faithful solve of a wrong read.
|
||||
|
||||
The "from the stated quantities" obligation is split into THREE separable digests
|
||||
(P1-C hardening — for replay, audit, and failure localization):
|
||||
``derivation_digest`` (a solve happened from the structure), ``bound_slots_digest``
|
||||
(the answer binds to a STATED slot — the asked unknown — not a phantom), and
|
||||
``back_substitution_digest`` (the answer satisfies the constraints). A complete
|
||||
derivation does NOT imply the answer bound to a declared slot, so the two are
|
||||
distinct obligations (``test_derivation_digest_alone_is_insufficient_without_bound_slots``).
|
||||
"""
|
||||
|
||||
source_problem_digest: str # provenance: hash of the problem text
|
||||
|
|
@ -93,7 +103,8 @@ class VerificationProof:
|
|||
independent_reader_lineage: str # identity of the independent cross-check reader
|
||||
primary_read_digest: str # canonical structure the primary read produced
|
||||
independent_read_digest: str # canonical structure the independent read produced
|
||||
derivation_digest: str # the derivation from the STATED quantities
|
||||
derivation_digest: str # the derivation (solve) from the STATED quantities
|
||||
bound_slots_digest: str # the answer binds to the STATED slots (asked unknown), not a phantom
|
||||
back_substitution_digest: str # back-substitution into the canonical structure
|
||||
boundary_clear: bool # no organ boundary fired
|
||||
contradiction_clear: bool # no contradiction family fired
|
||||
|
|
@ -102,6 +113,7 @@ class VerificationProof:
|
|||
# Reason codes for a failed obligation — each names exactly one violated rule.
|
||||
REASON_READS_NOT_INDEPENDENT = "reads_not_independent" # same reader lineage twice
|
||||
REASON_READS_DISAGREE = "reads_disagree" # the wrong-read catcher
|
||||
REASON_NO_BOUND_SLOTS = "no_bound_slots" # answer did not bind to a stated slot
|
||||
REASON_NO_BACK_SUBSTITUTION = "no_back_substitution"
|
||||
REASON_BOUNDARY_FIRED = "boundary_fired"
|
||||
REASON_CONTRADICTION_PRESENT = "contradiction_present"
|
||||
|
|
@ -143,6 +155,9 @@ def evaluate_verification(
|
|||
):
|
||||
failed.append(REASON_READS_DISAGREE)
|
||||
|
||||
if obligation.requires_bound_slots and not proof.bound_slots_digest:
|
||||
failed.append(REASON_NO_BOUND_SLOTS)
|
||||
|
||||
if obligation.requires_back_substitution and not proof.back_substitution_digest:
|
||||
failed.append(REASON_NO_BACK_SUBSTITUTION)
|
||||
|
||||
|
|
|
|||
|
|
@ -52,6 +52,8 @@ from core.epistemic_state import EpistemicState
|
|||
from evals.constraint_oracle.signature import (
|
||||
constraint_setup_signature,
|
||||
constraints_signature,
|
||||
query_signature,
|
||||
unknowns_signature,
|
||||
)
|
||||
from generate.constraint_comprehension.model import ConstraintProblem
|
||||
from generate.constraint_comprehension.reader import read_constraint_problem
|
||||
|
|
@ -139,6 +141,7 @@ def verify_r2(text: str, gold_setup: ConstraintProblem) -> R2VerificationOutcome
|
|||
if isinstance(solution, Refusal):
|
||||
boundary_clear = False
|
||||
derivation_digest = ""
|
||||
bound_slots_digest = ""
|
||||
back_substitution_digest = ""
|
||||
else:
|
||||
boundary_clear = True
|
||||
|
|
@ -146,6 +149,23 @@ def verify_r2(text: str, gold_setup: ConstraintProblem) -> R2VerificationOutcome
|
|||
derivation_digest = _sha(
|
||||
repr(("derivation", constraints_signature(primary.constraints), bound))
|
||||
)
|
||||
# bound_slots: the answer binds to a STATED slot — the asked unknown — among the
|
||||
# declared unknowns. Empty if the asked unknown was not solved (a phantom answer);
|
||||
# a complete derivation does NOT by itself prove this (P1-C: separable obligation).
|
||||
bound_slots_digest = (
|
||||
_sha(
|
||||
repr(
|
||||
(
|
||||
"bound_slots",
|
||||
unknowns_signature(primary.unknowns),
|
||||
query_signature(primary.query),
|
||||
bound,
|
||||
)
|
||||
)
|
||||
)
|
||||
if primary.query.symbol in solution
|
||||
else ""
|
||||
)
|
||||
back_substitution_digest = (
|
||||
_sha(repr(("back_substitution", bound)))
|
||||
if _back_substitutes(primary, solution)
|
||||
|
|
@ -159,6 +179,7 @@ def verify_r2(text: str, gold_setup: ConstraintProblem) -> R2VerificationOutcome
|
|||
primary_read_digest=_sha(repr(constraint_setup_signature(primary))),
|
||||
independent_read_digest=_sha(repr(constraint_setup_signature(gold_setup))),
|
||||
derivation_digest=derivation_digest,
|
||||
bound_slots_digest=bound_slots_digest,
|
||||
back_substitution_digest=back_substitution_digest,
|
||||
boundary_clear=boundary_clear,
|
||||
# Setup-only verification has no answer-key path, so no contradiction can arise
|
||||
|
|
|
|||
|
|
@ -23,6 +23,7 @@ from core.epistemic_disclosure.verified_contract import (
|
|||
REASON_CONTRADICTION_PRESENT,
|
||||
REASON_INCOMPLETE_PROOF,
|
||||
REASON_NO_BACK_SUBSTITUTION,
|
||||
REASON_NO_BOUND_SLOTS,
|
||||
REASON_READS_DISAGREE,
|
||||
REASON_READS_NOT_INDEPENDENT,
|
||||
REASON_UNRESOLVED_LIMITATION,
|
||||
|
|
@ -46,6 +47,7 @@ def _valid_proof(**overrides) -> VerificationProof:
|
|||
primary_read_digest="canonical_structure_C",
|
||||
independent_read_digest="canonical_structure_C",
|
||||
derivation_digest="deriv#1",
|
||||
bound_slots_digest="bound#1",
|
||||
back_substitution_digest="backsub#1",
|
||||
boundary_clear=True,
|
||||
contradiction_clear=True,
|
||||
|
|
@ -96,6 +98,27 @@ def test_verified_requires_back_substitution():
|
|||
assert REASON_NO_BACK_SUBSTITUTION in result.failed_checks
|
||||
|
||||
|
||||
def test_verified_requires_bound_slots():
|
||||
result = evaluate_verification(_valid_proof(bound_slots_digest=""), limitation=None)
|
||||
assert result.verdict is VerificationVerdict.NOT_VERIFIED
|
||||
assert REASON_NO_BOUND_SLOTS in result.failed_checks
|
||||
|
||||
|
||||
def test_derivation_digest_alone_is_insufficient_without_bound_slots():
|
||||
"""P1-C hardening: a complete derivation does NOT imply the answer bound to a STATED
|
||||
slot — they are SEPARATE obligations. A proof with a derivation but no bound-slots must
|
||||
not verify; and relaxing exactly the bound-slots obligation stops that check firing
|
||||
(so the obligation is load-bearing, not decoration)."""
|
||||
proof = _valid_proof(derivation_digest="deriv#1", bound_slots_digest="")
|
||||
canonical = evaluate_verification(proof, limitation=None)
|
||||
assert canonical.verdict is VerificationVerdict.NOT_VERIFIED
|
||||
assert REASON_NO_BOUND_SLOTS in canonical.failed_checks
|
||||
|
||||
relaxed = replace(VERIFICATION_OBLIGATION, requires_bound_slots=False)
|
||||
relaxed_result = evaluate_verification(proof, limitation=None, obligation=relaxed)
|
||||
assert REASON_NO_BOUND_SLOTS not in relaxed_result.failed_checks
|
||||
|
||||
|
||||
def test_verified_requires_boundary_clear():
|
||||
result = evaluate_verification(_valid_proof(boundary_clear=False), limitation=None)
|
||||
assert result.verdict is VerificationVerdict.NOT_VERIFIED
|
||||
|
|
@ -133,6 +156,7 @@ def test_verified_rejects_any_limitation_assessment():
|
|||
def test_canonical_obligation_is_fully_strict():
|
||||
assert VERIFICATION_OBLIGATION.requires_independent_read
|
||||
assert VERIFICATION_OBLIGATION.rejects_wrong_read_even_if_solved
|
||||
assert VERIFICATION_OBLIGATION.requires_bound_slots
|
||||
assert VERIFICATION_OBLIGATION.requires_back_substitution
|
||||
assert VERIFICATION_OBLIGATION.requires_boundary_clear
|
||||
|
||||
|
|
|
|||
|
|
@ -173,6 +173,7 @@ def test_all_proof_digests_populated_on_verified():
|
|||
p.primary_read_digest,
|
||||
p.independent_read_digest,
|
||||
p.derivation_digest,
|
||||
p.bound_slots_digest,
|
||||
p.back_substitution_digest,
|
||||
):
|
||||
assert digest, "every replay-critical digest must be populated on a VERIFIED proof"
|
||||
|
|
|
|||
Loading…
Reference in a new issue