Build the participant-crossing bisimulation counterexample corpus #973

Parent: #811

Bounded outcome

Publish a deterministic safe mutation and counterexample corpus for participant-crossing-dpbb-finite-v1. At minimum cover a hidden visible denial, added hidden divergence, removed delivery branch, and later-cut replay incorrectly permitted. Distinguish strong, weak, branching, and divergence-preserving results without treating a trace mismatch alone as the selected relation decision.

Negative cases

• Visible refusal or redacted occurrence incorrectly classified as tau.
• Infinite internal loop added behind a finite visible trace.
• Enabled delivery/observation branch removed.
• Replay admitted after policy-cut advancement.
• Sanitized error, deadlock, or termination collapsed into bookkeeping.
• Counterexample artifact leaks model payload or host/process details.

Evidence required

• One independently reviewed mutation per required failure shape.
• Pinned model/profile/tool digests and expected negative result.
• Bounded sanitized Hennessy-Milner witness when supported.
• An independent checked negative-result path for exact divergence cases.
• Canonical counterexample artifact digests and regression tests.

Explicit nonclaims

• A mutation corpus does not establish the positive relation.
• No proof, runtime realization, backend conformance, noninterference, or opacity claim.

Dependencies

• Blocked by Implement independent participant-crossing proof models #971 and Map shared runtime crossings to the finite proof model #972.
• Parent design: Design a proof-bearing participant-control bisimulation result #811.

Requirements

• SEM-232
• ASR-535
• SEM-230