feat(verified): P1-C — split bound_slots_digest into separate obligation

Adds bound_slots_digest as a distinct VerificationProof obligation before any serving wiring. Keeps the VERIFIED lane off-serving while separating derivation, stated-slot binding, and back-substitution.
This commit is contained in:
Shay 2026-06-08 17:17:31 -07:00 committed by GitHub
parent 05b83a57cf
commit 710743c38f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 62 additions and 1 deletions

View file

@ -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)

View file

@ -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

View file

@ -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

View file

@ -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"