Derive runtime opacity evidence from observed execution

[Brad-Edwards]

The opacity probe labels a fixed transcript as backend-native evidence without observing the crossing mechanisms that transcript describes.

Acceptance criteria

• Collect the observations required by the published opacity profile from actual runtime execution and backend readback, with explicit runtime/backend/profile/configuration provenance.
• Exercise the claimed crossing, denial, retry, delivery, and scheduling behavior only within the profile's stated observation model. Identify synthetic finite-model evidence separately.
• Detect disagreement between instrumented execution and the reported transcript. Missing observations must not produce a successful native-realization claim.
• Preserve the profile's uniform-denial limits and bounded formal claims. Do not extend this issue into useful allowed-action opacity or unfinished bisimulation proof work.

Prerequisites: #1369, #1357, #1358.

References: Diagnosis, Opacity conformance harness.