Correct v0.8 §9.7.3: the binding correspondence as first cut could never pass

secrets-engine found, and access-engine and approval-engine reported
independently within hours, that GH-DEC-2026-008 as written was
unimplementable. Where a claim travels inside the hashed request — the
dual-control pattern it was written for — embedding the claim changes the
digest of the request carrying it, so a digest recorded at issue can
never equal the final one. It is a hash cycle. A fail-closed consumer
obeying the rule would have denied destroy permanently.

The comparison is now against the digest the PDP publishes for the
request with the approval evidence excluded (flex-auth's
binding.approval_binding_digest, verified present in its schema and
tests). The exclusion rule is the PDP's to publish and a consumer MUST
NOT guess it: a digest computed under an assumed rule fails open toward
accepting a claim bound to a different request — the same failure
direction as an invented vocabulary mapping, by another road.

§6.4 obligation 5 gains the general property access-engine flagged as a
near miss rather than a request: an evidence-bearing input may be
excluded from a correspondence digest but never from the replay identity.
Two requests differing only in which approval was presented decide
differently, so collapsing them lets an allow obtained with a valid claim
be replayed against a request carrying none — a fail-open hole reached by
a refactor that looks like simplification.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WtJBr77gMFLrN93iEevqQJ

Assistant: claude-code
Assistant-Model: opus
Assistant-Process: 425128@bnt-lap001
Assistant-Session: f5944d8b-dac4-4e1a-87eb-8b3d8f314a63

canon/standards/security-layer-model_v0.8.md

@@ -548,6 +548,21 @@ Four obligations, and they are normative:
    way that still produces a confident answer, it fails open, and it would be a
    third authority on what a request *is*.
 
+   **An evidence-bearing input may be excluded from a correspondence digest, but
+   never from the replay identity.** These are two digests over one request and
+   they are deliberately different. A correspondence digest answers *"is this the
+   action the approval was granted for"* and must exclude the evidence, or it
+   cannot be computed before the evidence exists. A replay identity answers *"is
+   this the same request"* and MUST cover every input the decision depends on,
+   evidence included — two requests differing only in which approval was
+   presented decide differently, one allowing and one denying, so collapsing them
+   would let an allow obtained with a valid claim be replayed against a request
+   carrying none. That is a fail-open hole reached by a refactor that looks like
+   simplification, which is why the property is stated rather than left to be
+   rediscovered. The shape recurs wherever evidence travels inside a hashed
+   request. Raised by `access-engine`, which nearly took the unsafe simplification
+   and reported the near miss.
+
    **A consumer of a summary predicate trusts the issuer's evaluation of
    everything folded into it.** Where the split reduces what a PEP verifies
    independently — as `valid_now` does for an approver threshold the claim
@@ -956,15 +971,36 @@ deciding wrongly. The model has had no temporal law, and the approval race in
    action is spent. Reversibility would reopen replay, which is the failure the
    mutation exists to close.
 
-   **The correspondence is the PDP digest.** A consumer on this path MUST verify
-   that `claim.binding.pdp_digest` equals the decision's
-   `NewDecisionBinding.request_digest`, and MUST NOT use a claim carrying none.
-   Recomputing the approval engine's native binding from a `CheckRequest` is not
-   a permitted fallback: it requires translating between two vocabularies, no
-   mapping is published, and a wrong translation fails open by silently
-   accepting a claim approved for something else. Without this, `valid_now: true`
-   plus an ALLOW establishes *approved* and *permitted* but never *approved for
-   this request*. Settled in `GH-DEC-2026-008`.
+   **The correspondence is a digest, and it is the PDP's to define.** A consumer
+   on this path MUST verify that the approval's recorded PDP digest equals the
+   digest the PDP publishes **for the request with the approval evidence
+   excluded** — `binding.approval_binding_digest` in `access-engine` — and MUST
+   NOT use a claim that carries no such digest. Recomputing the approval engine's
+   native binding from a `CheckRequest` is not a permitted fallback: it requires
+   translating between two vocabularies, no mapping is published, and a wrong
+   translation fails open by silently accepting a claim approved for something
+   else. Without this, `valid_now: true` plus an ALLOW establishes *approved* and
+   *permitted* but never *approved for this request*.
+
+   **The comparison cannot be against the full request digest.** Where a claim
+   travels inside the hashed request — the dual-control pattern — embedding it
+   changes the digest of the request carrying it, so a digest recorded at issue
+   can never equal the final one. That is a hash cycle and the resolution is
+   forced, not chosen: the recorded digest is necessarily of the underlying
+   action before any claim was embedded. A standard that mandates the naive
+   comparison mandates a check that can never pass, and a fail-closed consumer
+   then denies the action permanently.
+
+   **The exclusion rule is the PDP's to publish, and until it does the path is
+   incomplete rather than complete.** A consumer MUST NOT guess which fields are
+   excluded: a digest computed under an assumed rule produces a confident wrong
+   answer, and comparing two digests derived under different rules fails open
+   toward accepting a claim bound to a different request — the same failure
+   direction as an invented vocabulary mapping, reached by another road.
+
+   Settled in `GH-DEC-2026-008`, amended on an implementability defect found by
+   `secrets-engine` and reported independently by `access-engine` and
+   `approval-engine` within hours of the ruling.
 
    Settled in `GH-DEC-2026-003`; the protocol is
    `gate-house/docs/contracts/approval-consumption.md`.
@@ -1300,12 +1336,22 @@ v0.7 → v0.8:
    v0.7's stated order left the CAS able to prevent only the second record, never
    the second side effect. Protocol correction, not a retraction of the forensic
    claim (`GH-DEC-2026-003`).
-2. **§9.7.3 gains the binding correspondence** — `claim.binding.pdp_digest` MUST
-   equal the decision's request digest, and a claim without one is unusable on
-   that path. No cross-engine vocabulary mapping is published: a translation can
-   be confidently wrong and fails open, where a digest is identity
-   (`GH-DEC-2026-008`, raised by `access-engine`, which declined to close it
-   locally).
+2. **§9.7.3 gains the binding correspondence** — the approval's recorded PDP
+   digest MUST equal the digest the PDP publishes for the request with the
+   approval evidence excluded, and a claim without one is unusable on that path.
+   No cross-engine vocabulary mapping is published: a translation can be
+   confidently wrong and fails open, where a digest is identity. The comparison
+   is against an exclusion-scoped digest because a claim travelling inside a
+   hashed request cannot name the digest of the request containing it — a hash
+   cycle, found by `secrets-engine` and reported independently by two engines
+   within hours of the ruling, which as first written mandated a check that could
+   never pass (`GH-DEC-2026-008`, raised by `access-engine`, which declined to
+   close it locally).
+2b. **§6.4 obligation 5 gains the replay-identity property** — an evidence-bearing
+   input may be excluded from a correspondence digest but never from the replay
+   identity, because two requests differing only in which approval was presented
+   decide differently. Flagged by `access-engine` as a near miss rather than a
+   request.
 3. **§6.4 obligation 5 added** — validation by owning layer, and correspondence
    by identity rather than translation. A PIP MUST NOT republish the PDP's
    decision. Carries the consequence that a consumer of a summary predicate