Implement independent participant-crossing proof models

[Brad-Edwards]

Parent: #811

Bounded outcome

Implement the complete finite abstract SEM-230 participant-crossing LTS and the independently derived concrete API-423/RUN-319 crossing-kernel LTS for profile participant-crossing-dpbb-finite-v1. Use separate transition authorities and deterministic exporters; share only the closed governed label/projection profile.

Negative cases

• Reject incomplete carrier declarations and depth/sample truncation.
• Reject duplicate or overlapping visible/tau labels.
• Reject a shared self-confirming transition table.
• Reject unsafe or unbounded model identifiers and paths.
• Reject model/profile/source digest drift.

Evidence required

• Revision-pinned model sources and generated .aut artifacts.
• Complete domain, state, transition, and initial-state counts.
• Independent construction review and drift checks.
• Valid and invalid fixtures using synthetic bounded identifiers.
• Reproducible export commands and canonical digests.

Explicit nonclaims

• No bisimulation result is established by constructing the models.
• No live-runtime realization, backend conformance, noninterference, opacity, timing, probability, concurrency, or controller-handoff result.

Dependencies

• Parent design: Design a proof-bearing participant-control bisimulation result #811.
• No child dependency; this is the first implementation package.

Requirements

• SEM-232
• SEM-230
• API-423
• RUN-319

[Brad-Edwards]

🛠️ Picked up by /implement - driver codex, branch 971-participant-crossing-models, 2026-09-27T05:31:56.812Z.

[Brad-Edwards]

gc workflow phase recorded: preflight (issue #971). 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]

gc workflow phase recorded: preflight (issue #971). 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]

gc workflow phase recorded: preflight (issue #971). 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]

gc workflow phase recorded: preflight (issue #971). 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]

Execution obligation FINITE-REQUEST-HISTORY-SEMANTICS — Opened

Category: quality
Observed state: The rev1 design allows fresh requests from terminal with one request identity and four history-head values, but does not define identity reuse or head exhaustion. Decision/change sequencing and per-crossing completion need explicit target-state rules.
Impact: An implicit interpretation changes the quantified reachable carrier and may silently truncate or alter the intended theorem.
Current obligation: Resolve the finite request/history interpretation in the governed authority before implementing and verifying the independent complete models.

Evidence

• specs/formal/participant-semantics/participant-crossing-bisimulation.md
• docs/decisions/issue-971-participant-crossing-models-preflight.md