feat(contracts): publish mixed-backend execution and readback contracts

[doublewhy]

Summary

Issue #1355 made the reference coordinator execute admitted mixed-backend edges and native handoffs, but it kept their inputs and evidence in raes_runtime: MixedEdgeExecutionBinding, MixedHandoffBinding and their bridge, time, delivery, observation and handoff carriers. A backend author therefore had no portable contract to implement against.

This PR publishes two draft contracts for those obligations. mixed-backend-execution-binding-v1 is the plain-data form of one installed bridge or native transfer service, its time coordinator and its readers for one admitted sem-234/rev1 edge or component-changing transition. Each role is pinned to a distinct service: no two roles in one binding share a service reference or digest. mixed-backend-stage-report-v1 carries one time-grant, execution, delivery, observation, handoff or owner-readback fact for one invocation of the #1360 backend operation protocol, and names the pinned service that produced it. Each report's sequence is its stage's fixed position in its chain, so independent producers number their reports without coordinating. Pure validators join bindings to the sealed profile, requests to shared contextual admission, and stage reports to the response transcript and to the caller's own committed time and composition readbacks.

The migration note states the stage and settlement model that the stage validator enforces. That model governs the published carriers only; it makes no claim about the in-process coordinator, which does not read them. No executable or runtime adoption is claimed; #1372 owns execution.

Because this changes source bound by the research evidence, both captures are republished at the next free releases (specification coverage 69.0.0, formal validation 70.0.0); retained outcomes, classifications and claim limits are unchanged.

Requirement UIDs

• None. Publish mixed-backend execution and readback contracts #1371 has no ## Requirements section, so this PR declares no requirement UID and changes no requirement record, and the branch carries no UID or scope file. The change does extend API-407 (participant feature support): it adds API-407 rules for the two contracts to specs/formal/runtime-contracts/participant-backend-contracts.md and edits manifest_authority.py and test_backend_manifest.py, which API-407 already traces, without changing its feature terms or support levels. Traceability below notes the schema owner that ci(policy): require every published contract to trace to a governing requirement #1422's gate will need.

Related Issues

Closes #1371

ADR Impact

• No ADR required. The contracts follow ADR-102 section 13 (the Define executable mixed-backend mapping and time contracts #1355 amendment) and ADR-061 publication rules; no ADR text changes.

Changes

• Contract models: raes_contracts/contracts/mixed_backend_binding.py (edge and handoff bindings with pinned services, a governed time requirement, declared mapping loss and evidence obligations; an edge's time requirement, MixedBackendEdgeTimeRequirementModel, also carries the admitted temporal_coupling) and mixed_backend_stages.py (six closed stage kinds bound to the invocation and request digest; every stage names its producer). An edge binding fixes compiled-identity, so the authorized action address is preserved, and names the destination provider's action allocation as effect owner without controller, disclosure or commit authority. Model validators refuse a binding that pins one service to two roles by service_ref or by digest: across an edge's bridge, coordinator, delivery reader and observation reader, and across a handoff's transfer service, coordinator and owner reader. A bridge therefore cannot grant its own order or read back its own delivery or observation, and a transfer service cannot grant its own order or read back its own owner.
• Binding validators: mixed_backend_validation.py requires exactly one matching binding per active edge and per one-to-one component-changing transition, with the edge's time coordinates and temporal coupling equal to the admitted edge. It refuses missing, foreign, duplicate and contradictory bindings, ungoverned order and other component changes. It also requires a request to commit to the binding, its operation kind and its pinned service before shared admission.
• Stage validator: validate_mixed_backend_stage_reports() in mixed_backend_transcript.py takes a MixedBackendStageContext that the caller resolves itself. It holds time_model with the time_model_ref and time_model_digest it was resolved under (both must equal the binding's time requirement), time_state (the committed time readback the coordinator received), post_time_state (RAES's own readback after the invocation, or None) and composition_state (required for a handoff). A supplied composition state must belong to the binding's profile and still be open for the obligation: the bound edge is active, or the handoff's source component is active and its destination is not. Each report's sequence must be its stage's fixed chain position (time grant 1, execution or handoff 2, delivery or owner readback 3, observation 4), and reports are accepted in ascending sequence whatever order they are supplied in, so producers that see neither each other's reports nor a shared counter can number them. Each stage must follow its prerequisite and name the coordinator, bridge, delivery reader, observation reader, transfer service or owner reader that the binding pins for it. Grant coordinates must equal time_state. A handoff must name the committed history head and phase revision, and its owner readback is judged against that revision. An invocation stage needs an ordered grant and an accepted acknowledgement. A proposed SUCCEEDED or FAILED outcome must equal the established state: success needs a post-invocation readback in which neither bound clock moved backwards (a handoff failure does too), and an incomparable grant with no invocation stage establishes FAILED. Shared evidence may cite only supplied reports.
• Public backend interfaces: raes_backend_protocols/mixed_backend.py adds MixedBackendBridge (on top of BackendOperationProvider), MixedTimeCoordinator, MixedStageReader and require_mixed_backend_service(), which checks declarations and call shapes without invoking code. Each producer method's docstring gives the sequence its reports carry.
• Declarations and publication: MIXED_BACKEND_CONTRACT_IDS joins BACKEND_SUPPORTED_CONTRACT_IDS, so the backend-manifest-v2 and backend-profile-v1 enums and entries change; the stub and reference backends exclude the IDs, and test_backend_manifest.py's expected stub list excludes them too. Two hand-governed schemas under contracts/schemas/control-plane/ carry x-raes-invariants naming the validators and their inputs, including time-runtime-state-v1 and the composition states of runtime-snapshot-v1. The binding schema's local-consistency invariant states the distinct-service rule, and the stage-transcript invariant states the fixed sequence per stage, the time-model identity and the open-obligation joins. Their publication entries are new, and schema_bundle() registers them through bundle_runtime.py. Exports go through a new _mixed_backend_exports.py spread inside _mixed_composition_exports.py, so _exports.py stays at 499 lines.
• Examples: binding and stage-report valid/, invalid/ and context-invalid/ fixtures. The binding's invalid/bridge-as-reader.json pins the bridge as both readers and invalid/transfer-as-owner-reader.json pins the transfer service as its own owner reader. Six request/response/stage transcripts (mixed-edge, mixed-edge-partial, mixed-edge-refused, mixed-edge-time-refused, mixed-handoff, mixed-handoff-stale) and two capability declarations sit beside the backend operation corpus. In mixed-edge-time-refused the destination clock sits in a later segment, the grant is incomparable, and the bridge accepts the start but reports no execution stage and proposes a known failure with no effect.
• Docs: new docs/migration/mixed-backend-execution.md (bindings and their distinct services, stage reports with their fixed sequence numbers and producers, the digest rule, producer and reader obligations, the stage and settlement model with its preconditions, compatibility, examples, limits) linked from docs/migration/README.md. It cites ADR-102 section 13 as the decision and the Define executable mixed-backend mapping and time contracts #1355 preflight as architecture guidance. Also a section in docs/explain/reference/mixed-participant-composition.md, API-407 rules in specs/formal/runtime-contracts/participant-backend-contracts.md, the public API page and one paragraph in docs/public/backends.md.
• Specification-coverage release 69.0.0 (execution-snapshot-v69.json, analysis-v69.json, issue-1371 bundle) replays the retained matrix against this branch's source.
• Formal-validation release 70.0.0 (execution-snapshot-v70.json, analysis-v70.json, retest-v70.json) replays the retained formal cases with baseline 69.0.0.
• Revision pins advanced in tools/check_specification_coverage.py, tools/formal_semantic_validation/, and the three evidence test modules. Both research indexes record the new releases.

Test Plan

• Unit tests pass
• Integration tests pass if applicable
• Full completion suite required in CI before merge
• No coverage regression

uv run --project implementations/python --frozen --all-extras python -m pytest implementations/python/tests/test_issue_1371_mixed_backend_contracts.py -q passed (145 passed); the module has no integration-marked tests, so -m integration selects none (145 deselected). With --cov-branch, the module covers every line and branch of the seven new modules (544 statements, 164 branches).

Reviewer probe for this revision. On df71248 the stage validator accepted the mixed-edge reports numbered 1, 2, 3, 4 or 10, 20, 30, 40, but refused them when each producer numbered its own report from 1 ("duplicate stage report sequence changed its content") and when the coordinator picked 5 and the bridge 3 ("mixed stage report precedes its prerequisite stage"). mixed-edge-partial (each producer from 1) and mixed-handoff (from 1, and coordinator 5 with transfer service 3) were refused the same way. On this head each of those numberings other than 1, 2, 3, 4 is refused with "stage report sequence differs from its stage's chain position", and chain-numbered reports supplied in reverse order are accepted.

The new tests were written before the source change. test_independent_producers_number_each_stage_by_its_chain_position has six cases, and each re-cites its renumbered reports so that the numbering is its only defect. With the retargeted case for a stage reported again under a second number, all 7 failed against the unchanged validator: 3 with "changed its content", 2 with "precedes its prerequisite stage", 1 accepted (10, 20, 30, 40) and 1 with "at most once". All pass after the fix. The previous revision's 128 tests, run unchanged against the fix, all pass except the two cases this PR retargets: the foreign-stage case now adds an owner readback at sequence 3, and the second-number case now expects the new message. All six fixture transcripts already use the chain numbers, so no fixture changed. The removed "at most once" branch can no longer be reached, because two reports of one stage now share a number.

Two in-memory mutants survived the previous tests: a bridge check that skips the bridge's own execution_binding and stage_reports methods, and a time confirmation that ignores the destination clock. The new bridge cases (a dropped or narrowed execution_binding or stage_reports, with every shared operation method installed) fail under the first mutant (4 failures), and the new destination-regressed readback cases fail under the second (3 failures). The earlier rounds' cases for distinct services, time-model identity, open obligations, the handoff fence and the grant and producer joins are unchanged and pass in the same run.

The new module ran together with the neighbouring modules for backend manifests (including the v2 adapter), backend profiles, facade exports, corpus packaging, #1004, #1014 (contracts and governance), #1016, #1330 schema coverage, #1355, #1360 (operations and rejections) and runtime contracts and boundaries: 592 passed, 14 deselected. The 14 deselected tests are the integration-marked tests in test_corpus_packaging.py, which build a wheel and install it into a throwaway virtual environment; they were not rerun locally, and CI's integration job runs them.

tools/check_generated_schemas.py and tools/check_schema_publication.py --base-rev origin/dev passed after mixed-backend-stage-report-v1.json and its entry were regenerated; only its description and stage-transcript invariant changed, and the binding schema did not change. nox -s contracts -- --base-rev origin/dev passed all 14 steps, including schema publication, generated schema drift, JSON artifact validation and both evidence steps. nox -s docs-local passed (Sphinx -W, Vale, public source boundary), and Vale run directly on the migration note reports no findings. make policy and nox -s lint passed. Requirement governance does not apply: python -m tools.requirement_context --branch 1371-mixed-backend-execution-contracts resolves no UID and the branch has no scope file, so CI's canonical lane passes --skip-requirement.

Both evidence checker CLIs pass (integrity and replay), and the republish helper's read-only check reports the branch evidence as current. The captures were regenerated at the same releases and bound to 1c42b73; only their source identity fields changed. The three evidence modules pass with default markers (209 passed, 19 deselected) and with -m integration (19 passed, 209 deselected). There are no formal deviations and no changed artifact pins. verify-fast-feedback -- --base-rev origin/dev passed on the final commit. CI run 38054240362 on 34fe98d passed all 32 checks with deploy skipped, and the SonarCloud quality gate is OK (0 new issues, 100% coverage of new code, 0% duplication).

Ground Control Checks

• Repository policy command passes
• Pre-push code review and test-quality review completed, or not run for this lane

make policy passed on the final tree. The maintainer's pre-push Codex review was not run for this lane.

Traceability

• IMPLEMENTS: implementations/python/packages/raes_contracts/contracts/mixed_backend_binding.py, mixed_backend_stages.py, mixed_backend_validation.py, mixed_backend_transcript.py, mixed_backend_schema.py, implementations/python/packages/raes_backend_protocols/mixed_backend.py
• TESTS: implementations/python/tests/test_issue_1371_mixed_backend_contracts.py, implementations/python/tests/test_backend_manifest.py
• No requirement record changes. If ci(policy): require every published contract to trace to a governing requirement #1422 (contract requirement tracing) merges first, its gate will need an IMPLEMENTS → SPEC owner for the two new schemas.

Checklist

• Code follows the project coding standards
• FM level classified if semantic change
• Published contract schemas regenerated if models changed
• PR title is a Conventional Commit (release-please derives the version and CHANGELOG.md from it)
• Architectural docs updated if applicable

FM3 (stateful and control semantics: a stage-report state machine and the result contract it settles). The abstract state-machine model is the "Stage and settlement model" section of docs/migration/mixed-backend-execution.md: its state (accepted stages, accepted acknowledgement, confirmed time), the preconditions on the trusted inputs, transitions with their prerequisites and joins, the settlement table, observation rules and invariants. Invariants: one binding per executable obligation; preserved compiled subject; a distinct pinned service for each role of a binding; pinned service, time, coupling and loss coordinates equal to the admitted edge or transition; every stage from its pinned producer; every report numbered by its stage's fixed chain position and accepted in ascending sequence; a trusted time model resolved under the binding's reference and digest; a composition state still open for the bound edge or handoff; grant coordinates equal to the committed time readback; a handoff fenced on the committed history head and phase revision; no invocation stage without an ordered grant and an accepted acknowledgement; a proposed success or known failure equal to the established state; citations only of supplied reports. Artifacts: typed closed models, contract validators with parametrized valid and invalid cases, the routed fixture corpus, the model above and the rule-removal and mutant checks in the Test Plan. No TLA+ or Alloy model is added. No executable or runtime adoption is claimed.

Documentation

Updated: docs/migration/mixed-backend-execution.md (new), docs/migration/README.md, docs/explain/reference/mixed-participant-composition.md, specs/formal/runtime-contracts/participant-backend-contracts.md, docs/public/api/contracts.rst, docs/public/backends.md, both research evidence indexes.

[Brad-Edwards]

• Bound composition readback to the invocation's run.
• Added edge and handoff regression tests.
• Merged dev and refreshed research evidence.

[Brad-Edwards]

• Merged origin/dev and resolved research release conflicts.
• Archived prior captures and refreshed research evidence.