Repository navigation
Machine-check finite participant-crossing bisimulation #974
Description
Parent: #811
Bounded outcome
Run the pinned mCRL2 finite equivalence decision for the complete quantified carrier of participant-crossing-dpbb-finite-v1 using ltscompare --equivalence=dpbranching-bisim with the exact governed tau partition. Publish a model-check assurance record only if independent inputs, complete counts, provenance, mutations, and drift gates all pass.
Negative cases
- Truncated, sampled, depth-limited, or timeout-trimmed carrier.
- Floating tool version, mutable tag, or missing archive/container digest.
- Abstract and concrete LTS generated from one authority.
- Tau set or projection differs from the governed profile.
- Positive exit promoted to a proof certificate.
- Mutation expected to fail is accepted.
Evidence required
- mCRL2 202607.0 provenance plus verified archive checksum or immutable container digest.
- Fixed non-shell, offline verification command and bounded resources/output.
- Exact input/source/profile/mapping digests and state/transition counts.
- Positive result or safe negative counterexample.
- All required mutation outcomes and a model-check claim binding.
- CI artifact publication through canonical bounded paths.
Explicit nonclaims
- The finite decision applies only to the complete named carrier.
- It is model-check evidence, not an unbounded proof.
- No live-runtime realization, backend conformance, noninterference, or opacity result.
Dependencies
- Blocked by Implement independent participant-crossing proof models #971, Map shared runtime crossings to the finite proof model #972, and Build the participant-crossing bisimulation counterexample corpus #973.
- Parent design: Design a proof-bearing participant-control bisimulation result #811.
Requirements
- SEM-232
- ASR-535
- SEM-230
- API-423
- RUN-319
Activity
[-]Machine-check finite participant-crossing bisimulation[/-][+]Deferred: Machine-check finite participant-crossing bisimulation[/+][-]Deferred: Machine-check finite participant-crossing bisimulation[/-][+]Machine-check finite participant-crossing bisimulation[/+]Brad-Edwards commentedon Oct 31, 2026
🛠️ Picked up by /implement - driver codex, branch
974-finite-crossing-bisimulation, 2026-10-31T00:06:34.279Z.Brad-Edwards commentedon Oct 31, 2026
gc workflow phase recorded:
preflight(issue #974). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.Brad-Edwards commentedon Oct 31, 2026
gc workflow phase recorded:
preflight(issue #974). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.Brad-Edwards commentedon Oct 31, 2026
gc workflow phase recorded:
preflight(issue #974). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.22 remaining items
Brad-Edwards commentedon Oct 31, 2026
Document consistency before push
Issue #974; branch
974-finite-crossing-bisimulation; pickup 6536221514.Design digest:
49da95faed2007f64fb19206921191fe1b99a929be9442748578734e10a6899b.specs/formal/participant-semantics/participant-crossing-machine-check.md(d2678327cc2e15f706341906fcbc1297d6a3706c08e0cf39254398841c21b329)docs/decisions/issue-974-finite-crossing-bisimulation-preflight.md(2dcb63aa8870347595675619ca77f73086f3d0acf826344ed5bd10e5c1847b1f)Reviewed the finite machine-check design, issue preflight, formal README, semantic family locator, requirement traceability, and implementation after the Sonar repair. The refactor preserves the immutable ordered proof-tool inventory, offline refusal behavior, complete finite model scope, and model-check-only claim. Refreshed the corpus, finite decision, proof-tool source digests, and current runtime observations without changing prior captures or the reviewed mutation subject. Native finite replay and required controls passed. Targeted corpus, machine-check, publication, and proof evidence tests passed; tooling validator launcher tests, Ruff formatting/lint, file-local repository policy, exact requirement scope, and runtime observation validation passed. SEM-232 remains DRAFT, with independent reproduction and public completion outside this finite result. The design documents remain consistent and require no content changes.
Candidate tree:
adc733e942a85a229cd1a13d37a7d03ec7e8ecf7.Document check: vale: server-owned baseline (Vale.Repetition)
Checker identity:
a9749df8f46a9b49cf48ed4d14b737dd480f2c3a1a933959433a535c894408b7.Brad-Edwards commentedon Oct 31, 2026
Pre-PR base synchronization
refs/remotes/origin/devat73bec010f4fe842ad9c42711f14a7ccdfe8deb1ealready_current7678e407b2ddc9f31903891e804815aaf0fdc6afadc733e942a85a229cd1a13d37a7d03ec7e8ecf7Brad-Edwards commentedon Oct 31, 2026
Document consistency before push
Issue #974; branch
974-finite-crossing-bisimulation; pickup 6536221514.Design digest:
49da95faed2007f64fb19206921191fe1b99a929be9442748578734e10a6899b.specs/formal/participant-semantics/participant-crossing-machine-check.md(d2678327cc2e15f706341906fcbc1297d6a3706c08e0cf39254398841c21b329)docs/decisions/issue-974-finite-crossing-bisimulation-preflight.md(2dcb63aa8870347595675619ca77f73086f3d0acf826344ed5bd10e5c1847b1f)The design documents and finite claim remain unchanged and consistent. Added five focused nox entry-point tests covering replay/publication dispatch, rejection of unknown or extra arguments before execution, and propagation plus summary of process failure. Targeted tests cover all lines and branches of this entry point; Ruff, file-local repository policy, exact requirement scope, and fresh runtime observation capture pass. The runtime mapping capture was regenerated after the test-source change; prior captures, native finite pins, mutation subject, and proof identities are preserved. SEM-232 remains DRAFT. Earlier native replay, hosted finite publication, proof replay, all eight test shards, and integration passed; this repair addresses only the measured new-code coverage gap.
Candidate tree:
925c67d124cc600ac1cfaf21ad6ff116d711c591.Document check: vale: server-owned baseline (Vale.Repetition)
Checker identity:
a9749df8f46a9b49cf48ed4d14b737dd480f2c3a1a933959433a535c894408b7.Brad-Edwards commentedon Oct 31, 2026
Pre-PR base synchronization
refs/remotes/origin/devat73bec010f4fe842ad9c42711f14a7ccdfe8deb1ealready_currentf85a3f2cfc2a34155b685477838009881419b177925c67d124cc600ac1cfaf21ad6ff116d711c591Brad-Edwards commentedon Oct 31, 2026
Ready for review — issue #974
PR: #1755
Plan: #974 (comment)
Outcome
Maintainers can replay the complete finite participant-crossing equivalence check offline and retain a bounded artifact with source, toolchain, model, and mutation provenance. The check confirms the pinned finite models are equivalent and rejects the required defective variants.
Added a pinned mCRL2 finite decision, strict evidence admission, offline replay, and qualified hosted artifact publication for the complete rev2 crossing models. SEM-232 remains DRAFT because independent reproduction and public completion are separate work.
In-scope requirements
Proposed state in this PR — authoritative only after merge.
SEM-232(Proof-Bearing Participant-Crossing Bisimulation) — DRAFT (proposed) — Finite model-check evidence only; no independent-reproduction or public-completion claim.ASR-535(Participant Information-Flow And Relation Assurance) — ACTIVE (proposed)SEM-230(Participant Information-Flow And Control Semantics) — ACTIVE (proposed)API-423(Participant Crossing Policy And Evidence Contracts) — ACTIVE (proposed)RUN-319(Participant Information-Flow Policy Enforcement) — ACTIVE (proposed)Files changed
Added:
docs/decisions/issue-974-finite-crossing-bisimulation-preflight.mddocs/governance/requirement-scopes/974.jsonimplementations/formal/participant_crossing/machine_check.pyimplementations/formal/participant_crossing/machine_check_evidence.pyimplementations/formal/participant_crossing/machine_check_publication.pyimplementations/python/tests/test_issue_974_machine_check.pyimplementations/python/tests/test_issue_974_machine_check_publication.pyspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/abstract.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/abstract.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/cases.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/concrete.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/concrete.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/finite-stutter.left.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/finite-stutter.right.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-denial.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-denial.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-denial.mcfspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-divergence.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-divergence.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-divergence.witness.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-observation.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-observation.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-observation.mcfspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/internal-divergence.left.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/internal-divergence.right.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/later-cut-replay.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/later-cut-replay.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/later-cut-replay.mcfspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/manifest.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/removed-delivery.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/removed-delivery.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/removed-delivery.mcfspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/results.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/weak-choice.left.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/weak-choice.right.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/abstract.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/abstract.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/cases.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/concrete.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/concrete.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/finite-stutter.left.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/finite-stutter.right.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-denial.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-denial.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-denial.mcfspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-divergence.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-divergence.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-divergence.witness.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-observation.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-observation.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-observation.mcfspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/internal-divergence.left.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/internal-divergence.right.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/later-cut-replay.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/later-cut-replay.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/later-cut-replay.mcfspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/manifest.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/removed-delivery.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/removed-delivery.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/removed-delivery.mcfspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/results.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/weak-choice.left.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/weak-choice.right.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/abstract.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/abstract.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/cases.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/concrete.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/concrete.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/finite-stutter.left.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/finite-stutter.right.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-denial.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-denial.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-denial.mcfspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-divergence.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-divergence.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-divergence.witness.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-observation.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-observation.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-observation.mcfspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/internal-divergence.left.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/internal-divergence.right.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/later-cut-replay.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/later-cut-replay.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/later-cut-replay.mcfspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/manifest.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/removed-delivery.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/removed-delivery.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/removed-delivery.mcfspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/results.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/weak-choice.left.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/weak-choice.right.autspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/abstract.autspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/abstract.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/concrete.autspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/concrete.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/corpus-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/model-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/mutation-results.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/result.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/abstract.autspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/abstract.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/concrete.autspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/concrete.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/corpus-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/model-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/mutation-results.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/result.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/abstract.autspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/abstract.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/concrete.autspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/concrete.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/corpus-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/manifest.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/model-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/mutation-results.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/result.jsonspecs/formal/participant-semantics/machine-check/pin.jsonspecs/formal/participant-semantics/participant-crossing-machine-check.mdspecs/formal/participant-semantics/runtime-mapping/capture-63e728d7bc32a198fb30969458e4efa0461850f34b09477688e655b3af2ac2a6/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-63e728d7bc32a198fb30969458e4efa0461850f34b09477688e655b3af2ac2a6/manifest.jsonspecs/formal/participant-semantics/runtime-mapping/capture-6f99f4e7d179c521754f32bd74fba39ddfcd0391e385e1f71d109c0540b2def2/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-6f99f4e7d179c521754f32bd74fba39ddfcd0391e385e1f71d109c0540b2def2/manifest.jsonspecs/formal/participant-semantics/runtime-mapping/capture-7270b57b21ee1ed3e842b3161dbfd2864fb550823b5cabff282f471306565420/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-7270b57b21ee1ed3e842b3161dbfd2864fb550823b5cabff282f471306565420/manifest.jsonspecs/formal/participant-semantics/runtime-mapping/capture-9e62b2402a9f271aa85bf2e3d8b61c0abc50115ea8b82afc39a223f92f576343/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-9e62b2402a9f271aa85bf2e3d8b61c0abc50115ea8b82afc39a223f92f576343/manifest.jsontools/nox_support/machine_check_lane.pyModified:
.github/workflows/canonical-verification.ymldocs/requirements/API-423/requirement.mddocs/requirements/ASR-535/requirement.mddocs/requirements/RUN-319/requirement.mddocs/requirements/SEM-230/requirement.mddocs/requirements/SEM-232/requirement.mdimplementations/formal/participant_crossing/README.mdimplementations/formal/participant_crossing/counterexample_corpus.pyimplementations/python/tests/test_issue_973_model_check_workflow.pyimplementations/python/tests/test_repo_policy_tools.pynoxfile.pyspecs/formal/participant-semantics/counterexamples/pin.jsonspecs/formal/participant-semantics/participant-opacity-proof-evidence.jsonspecs/formal/participant-semantics/semantic-coverage/family-rows.mdtools/check_participant_opacity_proof.pytools/mcrl2_tool.pytools/policy/requirement_order.yamltools/tooling_policy_gate.pyReviews
Traceability reconciliation
Proposed in this PR — verified against the merged tree in Phase E.
Status
Brad-Edwards commentedon Oct 31, 2026
Delivery readiness recorded — Phase E finalizes issue #974 automatically when PR #1755 merges.
Brad-Edwards commentedon Oct 31, 2026
Document consistency before push
Issue #974; branch
974-finite-crossing-bisimulation; pickup 6536221514.Design digest:
49da95faed2007f64fb19206921191fe1b99a929be9442748578734e10a6899b.specs/formal/participant-semantics/participant-crossing-machine-check.md(d2678327cc2e15f706341906fcbc1297d6a3706c08e0cf39254398841c21b329)docs/decisions/issue-974-finite-crossing-bisimulation-preflight.md(2dcb63aa8870347595675619ca77f73086f3d0acf826344ed5bd10e5c1847b1f)Resolved the counterexample pin conflict by running the native producer against the real merge with dev at 0db2482. Preserved both parents' immutable captures and the identical reviewed mutation subject. Regenerated finite decision and current runtime observations for the merged contracts and runtime code. Native finite comparison and every required control pass; 86 targeted machine-check, publication, and runtime-mapping tests pass. Existing proof evidence admits without changes. File-local repository policy and staged whitespace checks pass. No design document or claim-scope change is needed: the pinned complete rev2 finite carrier and model-check-only outcome remain the same, and SEM-232 remains DRAFT. Updated exact requirement-scope bindings for the new captures.
Candidate tree:
3fa48ca31ea008d548e5dbed008b792a3cda74b9.Document check: vale: server-owned baseline (Vale.Repetition)
Checker identity:
a9749df8f46a9b49cf48ed4d14b737dd480f2c3a1a933959433a535c894408b7.Brad-Edwards commentedon Oct 31, 2026
Pre-PR base synchronization
refs/remotes/origin/devat0db2482e2901af5d74f65769acd8fc287e0b45femerged_conflicts_resolved1d0b914789b97c8a96cab364c20e8f3efe536ed63fa48ca31ea008d548e5dbed008b792a3cda74b9Brad-Edwards commentedon Oct 31, 2026
Document consistency before push
Issue #974; branch
974-finite-crossing-bisimulation; pickup 6536221514.Design digest:
49da95faed2007f64fb19206921191fe1b99a929be9442748578734e10a6899b.specs/formal/participant-semantics/participant-crossing-machine-check.md(d2678327cc2e15f706341906fcbc1297d6a3706c08e0cf39254398841c21b329)docs/decisions/issue-974-finite-crossing-bisimulation-preflight.md(2dcb63aa8870347595675619ca77f73086f3d0acf826344ed5bd10e5c1847b1f)Reviewed the merged tree and design documents after the second dev synchronization at 4c55e9c. This additional merge brings the ADR immutability policy fix and its tests; no design or finite-model changes are required. Refreshed current runtime observations for the changed tool/test sources and updated exact scope bindings. The previously refreshed native corpus and finite evidence remain valid and admit unchanged; the first synchronization passed native finite comparison, required controls, 86 targeted tests, and proof-evidence admission. The second synchronization passed all 112 selected ADR-policy and runtime-mapping tests, runtime capture validation, file-local repository policy, exact requirement scope, and staged whitespace checks. Historical captures and reviewed mutation identity are preserved. The finite model-check claim and SEM-232 DRAFT status remain accurate.
Candidate tree:
e549b954c23f58decf7cf47feae0e01ca152512d.Document check: vale: server-owned baseline (Vale.Repetition)
Checker identity:
a9749df8f46a9b49cf48ed4d14b737dd480f2c3a1a933959433a535c894408b7.Brad-Edwards commentedon Oct 31, 2026
Pre-PR base synchronization
refs/remotes/origin/devat4c55e9c6f2ee5de27f581a1a947957be345471dfmerged_cleanddf94c436d3becc06bb69f8ddec04ecf2f3e1552e549b954c23f58decf7cf47feae0e01ca152512dBrad-Edwards commentedon Oct 31, 2026
Ready for review — issue #974
PR: #1755
Plan: #974 (comment)
Outcome
Maintainers can replay the complete finite participant-crossing equivalence check offline and retain a bounded artifact with source, toolchain, model, and mutation provenance. The check confirms the pinned finite models are equivalent and rejects the required defective variants.
Added a pinned mCRL2 finite decision, strict evidence admission, offline replay, and qualified hosted artifact publication for the complete rev2 crossing models. SEM-232 remains DRAFT because independent reproduction and public completion are separate work.
In-scope requirements
Proposed state in this PR — authoritative only after merge.
SEM-232(Proof-Bearing Participant-Crossing Bisimulation) — DRAFT (proposed) — Finite model-check evidence only; no independent-reproduction or public-completion claim.ASR-535(Participant Information-Flow And Relation Assurance) — ACTIVE (proposed)SEM-230(Participant Information-Flow And Control Semantics) — ACTIVE (proposed)API-423(Participant Crossing Policy And Evidence Contracts) — ACTIVE (proposed)RUN-319(Participant Information-Flow Policy Enforcement) — ACTIVE (proposed)Files changed
Added:
docs/decisions/issue-974-finite-crossing-bisimulation-preflight.mddocs/governance/requirement-scopes/974.jsonimplementations/formal/participant_crossing/machine_check.pyimplementations/formal/participant_crossing/machine_check_evidence.pyimplementations/formal/participant_crossing/machine_check_publication.pyimplementations/python/tests/test_issue_974_machine_check.pyimplementations/python/tests/test_issue_974_machine_check_publication.pyspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/abstract.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/abstract.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/cases.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/concrete.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/concrete.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/finite-stutter.left.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/finite-stutter.right.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-denial.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-denial.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-denial.mcfspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-divergence.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-divergence.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-divergence.witness.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-observation.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-observation.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/hidden-observation.mcfspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/internal-divergence.left.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/internal-divergence.right.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/later-cut-replay.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/later-cut-replay.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/later-cut-replay.mcfspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/manifest.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/removed-delivery.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/removed-delivery.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/removed-delivery.mcfspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/results.jsonspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/weak-choice.left.autspecs/formal/participant-semantics/counterexamples/capture-1270466c1b97a9673c7fd3949cecaf0f75a009a2c852be8d534d1ba2edcfc401/weak-choice.right.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/abstract.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/abstract.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/cases.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/concrete.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/concrete.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/finite-stutter.left.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/finite-stutter.right.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-denial.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-denial.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-denial.mcfspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-divergence.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-divergence.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-divergence.witness.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-observation.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-observation.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/hidden-observation.mcfspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/internal-divergence.left.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/internal-divergence.right.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/later-cut-replay.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/later-cut-replay.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/later-cut-replay.mcfspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/manifest.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/removed-delivery.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/removed-delivery.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/removed-delivery.mcfspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/results.jsonspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/weak-choice.left.autspecs/formal/participant-semantics/counterexamples/capture-7ad0404c155d86e5f70b7866cce5438296cb974c3b2ce75bb371a1754fa2a5ec/weak-choice.right.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/abstract.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/abstract.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/cases.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/concrete.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/concrete.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/finite-stutter.left.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/finite-stutter.right.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-denial.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-denial.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-denial.mcfspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-divergence.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-divergence.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-divergence.witness.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-observation.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-observation.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/hidden-observation.mcfspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/internal-divergence.left.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/internal-divergence.right.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/later-cut-replay.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/later-cut-replay.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/later-cut-replay.mcfspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/manifest.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/removed-delivery.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/removed-delivery.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/removed-delivery.mcfspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/results.jsonspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/weak-choice.left.autspecs/formal/participant-semantics/counterexamples/capture-7f8b68a1ef7d5aea9086ca0d4e2542d85c40cccfc9686032d5e7f1d1afd79bdc/weak-choice.right.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/abstract.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/abstract.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/cases.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/concrete.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/concrete.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/finite-stutter.left.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/finite-stutter.right.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/hidden-denial.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/hidden-denial.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/hidden-denial.mcfspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/hidden-divergence.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/hidden-divergence.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/hidden-divergence.witness.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/hidden-observation.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/hidden-observation.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/hidden-observation.mcfspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/internal-divergence.left.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/internal-divergence.right.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/later-cut-replay.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/later-cut-replay.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/later-cut-replay.mcfspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/manifest.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/removed-delivery.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/removed-delivery.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/removed-delivery.mcfspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/results.jsonspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/weak-choice.left.autspecs/formal/participant-semantics/counterexamples/capture-fb889b995414cf051e4b05ed6431ae6c1f41237d1ea61b09cef13c445d4fb0d0/weak-choice.right.autspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/abstract.autspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/abstract.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/concrete.autspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/concrete.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/corpus-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/model-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/mutation-results.jsonspecs/formal/participant-semantics/machine-check/capture-2bc4a26a483d1a647abcd9d2ce9a25c90a2c0594976dc04661dc141cf3d2d9b6/result.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/abstract.autspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/abstract.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/concrete.autspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/concrete.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/corpus-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/model-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/mutation-results.jsonspecs/formal/participant-semantics/machine-check/capture-2d7f2bb82ac26bf99284a42459e51faedb0dbcf7f31a46227d8082661b153520/result.jsonspecs/formal/participant-semantics/machine-check/capture-76422aebb1413e345677eeaa4bea67005e74aa3d9289d185f63f4c69dc838339/abstract.autspecs/formal/participant-semantics/machine-check/capture-76422aebb1413e345677eeaa4bea67005e74aa3d9289d185f63f4c69dc838339/abstract.jsonspecs/formal/participant-semantics/machine-check/capture-76422aebb1413e345677eeaa4bea67005e74aa3d9289d185f63f4c69dc838339/concrete.autspecs/formal/participant-semantics/machine-check/capture-76422aebb1413e345677eeaa4bea67005e74aa3d9289d185f63f4c69dc838339/concrete.jsonspecs/formal/participant-semantics/machine-check/capture-76422aebb1413e345677eeaa4bea67005e74aa3d9289d185f63f4c69dc838339/corpus-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-76422aebb1413e345677eeaa4bea67005e74aa3d9289d185f63f4c69dc838339/manifest.jsonspecs/formal/participant-semantics/machine-check/capture-76422aebb1413e345677eeaa4bea67005e74aa3d9289d185f63f4c69dc838339/model-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-76422aebb1413e345677eeaa4bea67005e74aa3d9289d185f63f4c69dc838339/mutation-results.jsonspecs/formal/participant-semantics/machine-check/capture-76422aebb1413e345677eeaa4bea67005e74aa3d9289d185f63f4c69dc838339/result.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/abstract.autspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/abstract.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/concrete.autspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/concrete.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/corpus-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/manifest.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/model-manifest.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/mutation-results.jsonspecs/formal/participant-semantics/machine-check/capture-c4f5a586393d1dc787136b0f691f90263c993f32b27c6afbbd92757931818575/result.jsonspecs/formal/participant-semantics/machine-check/pin.jsonspecs/formal/participant-semantics/participant-crossing-machine-check.mdspecs/formal/participant-semantics/runtime-mapping/capture-14e83704e16d62ea9cacd1a23ffeef85229c95fe1c87b83a6a3e4a58a9c9c467/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-14e83704e16d62ea9cacd1a23ffeef85229c95fe1c87b83a6a3e4a58a9c9c467/manifest.jsonspecs/formal/participant-semantics/runtime-mapping/capture-63e728d7bc32a198fb30969458e4efa0461850f34b09477688e655b3af2ac2a6/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-63e728d7bc32a198fb30969458e4efa0461850f34b09477688e655b3af2ac2a6/manifest.jsonspecs/formal/participant-semantics/runtime-mapping/capture-6f99f4e7d179c521754f32bd74fba39ddfcd0391e385e1f71d109c0540b2def2/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-6f99f4e7d179c521754f32bd74fba39ddfcd0391e385e1f71d109c0540b2def2/manifest.jsonspecs/formal/participant-semantics/runtime-mapping/capture-7270b57b21ee1ed3e842b3161dbfd2864fb550823b5cabff282f471306565420/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-7270b57b21ee1ed3e842b3161dbfd2864fb550823b5cabff282f471306565420/manifest.jsonspecs/formal/participant-semantics/runtime-mapping/capture-9e62b2402a9f271aa85bf2e3d8b61c0abc50115ea8b82afc39a223f92f576343/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-9e62b2402a9f271aa85bf2e3d8b61c0abc50115ea8b82afc39a223f92f576343/manifest.jsonspecs/formal/participant-semantics/runtime-mapping/capture-ce949b8c1683fad05a4dd780491b05af5f00a1d8368eadf66e2cce09e9719dc0/cases.jsonspecs/formal/participant-semantics/runtime-mapping/capture-ce949b8c1683fad05a4dd780491b05af5f00a1d8368eadf66e2cce09e9719dc0/manifest.jsontools/nox_support/machine_check_lane.pyModified:
.github/workflows/canonical-verification.ymldocs/requirements/API-423/requirement.mddocs/requirements/ASR-535/requirement.mddocs/requirements/RUN-319/requirement.mddocs/requirements/SEM-230/requirement.mddocs/requirements/SEM-232/requirement.mdimplementations/formal/participant_crossing/README.mdimplementations/formal/participant_crossing/counterexample_corpus.pyimplementations/python/tests/test_issue_973_model_check_workflow.pyimplementations/python/tests/test_repo_policy_tools.pynoxfile.pyspecs/formal/participant-semantics/counterexamples/pin.jsonspecs/formal/participant-semantics/participant-opacity-proof-evidence.jsonspecs/formal/participant-semantics/semantic-coverage/family-rows.mdtools/check_participant_opacity_proof.pytools/mcrl2_tool.pytools/policy/requirement_order.yamltools/tooling_policy_gate.pyReviews
Traceability reconciliation
Proposed in this PR — verified against the merged tree in Phase E.
Status
Brad-Edwards commentedon Oct 31, 2026
Delivery readiness recorded — Phase E finalizes issue #974 automatically when PR #1755 merges.
github-actions commentedon Oct 31, 2026
Phase E could not finalize PR #1755
The merge was detected and the delivery-readiness record was read, but finalization did
not complete. This issue is intentionally left open.
delivery_readiness_head_mismatchre_record_phase_d_readiness_for_the_merged_head_and_rerun_phase_eRepair the cause, then re-run the Ground Control Phase E workflow for this pull request.