Protocol gap (tracked, not blocking)
In the merged Software-Authority / Hardware-Identity offline transfer (PR #578), the v2 acceptance
predicate does not itself establish Def-12 step 12 — σ^DSM over the transition plus the
whole-state consumption R_i → R_{i+1}.
anchor_core::accept::accept_offline calls DsmVerifier::verify_transition(transition_digest, prev_frontier, next_frontier) for step 12.
- The SDK adapter
DsmStateVerifier::verify_transition in
dsm_client/deterministic_state_machine/dsm_sdk/src/bluetooth/anchor_accept.rs returns true:
the relationship proofs (rel_proof_parent, rel_proof_child) that would prove R_i → R_{i+1}
are not carried in the OfflineRelease, so the check cannot be performed inside the predicate.
Current correctness basis
Correctness currently rests on caller ordering in the bilateral handler, not on the predicate:
handle_confirm_request verifies rel_proof_parent + rel_proof_child + the §C1 h_{n+1}
recompute, and accept_offline_release refuses to run the predicate unless the cert's device roots
equal the ones the handler verified. So the enforced check set is effectively fifteen, while the
predicate as written is seventeen — step 12 is a no-op inside the predicate.
To make the predicate self-contained
Carry the relationship proofs in the release object so verify_transition can verify
R_i → R_{i+1} without relying on the caller. That is a wire-format change to
dsm.anchor.OfflineRelease (add the relationship inclusion proofs), not a patch to the adapter
function. Do not "fix" it by inventing an equality check over the current verify_transition
arguments — they are frontiers (prev_frontier/next_frontier), already checked by the
accepted-frontier pin (check 2) and the h_{i+1} = H(h_i ‖ D) recompute (checks 8-11).
Scope
Follow-up (Stage 4/5 protocol hardening). Not the next implementation task; filed to track the
predicate-vs-code gap so it isn't lost. The gap is documented in-code (an honest comment in
verify_transition), so it is not silent — this issue makes it trackable.
Protocol gap (tracked, not blocking)
In the merged Software-Authority / Hardware-Identity offline transfer (PR #578), the v2 acceptance
predicate does not itself establish Def-12 step 12 —
σ^DSMover the transition plus thewhole-state consumption
R_i → R_{i+1}.anchor_core::accept::accept_offlinecallsDsmVerifier::verify_transition(transition_digest, prev_frontier, next_frontier)for step 12.DsmStateVerifier::verify_transitionindsm_client/deterministic_state_machine/dsm_sdk/src/bluetooth/anchor_accept.rsreturnstrue:the relationship proofs (
rel_proof_parent,rel_proof_child) that would proveR_i → R_{i+1}are not carried in the
OfflineRelease, so the check cannot be performed inside the predicate.Current correctness basis
Correctness currently rests on caller ordering in the bilateral handler, not on the predicate:
handle_confirm_requestverifiesrel_proof_parent+rel_proof_child+ the §C1h_{n+1}recompute, and
accept_offline_releaserefuses to run the predicate unless the cert's device rootsequal the ones the handler verified. So the enforced check set is effectively fifteen, while the
predicate as written is seventeen — step 12 is a no-op inside the predicate.
To make the predicate self-contained
Carry the relationship proofs in the release object so
verify_transitioncan verifyR_i → R_{i+1}without relying on the caller. That is a wire-format change todsm.anchor.OfflineRelease(add the relationship inclusion proofs), not a patch to the adapterfunction. Do not "fix" it by inventing an equality check over the current
verify_transitionarguments — they are frontiers (
prev_frontier/next_frontier), already checked by theaccepted-frontier pin (check 2) and the
h_{i+1} = H(h_i ‖ D)recompute (checks 8-11).Scope
Follow-up (Stage 4/5 protocol hardening). Not the next implementation task; filed to track the
predicate-vs-code gap so it isn't lost. The gap is documented in-code (an honest comment in
verify_transition), so it is not silent — this issue makes it trackable.