diff --git a/docs/decisions/adrs/adr-102-mixed-cross-backend-participant-control.md b/docs/decisions/adrs/adr-102-mixed-cross-backend-participant-control.md index 597004dfc..d55b77ba0 100644 --- a/docs/decisions/adrs/adr-102-mixed-cross-backend-participant-control.md +++ b/docs/decisions/adrs/adr-102-mixed-cross-backend-participant-control.md @@ -284,6 +284,66 @@ distinct. No result is promoted between them silently. - #1018 executes ASR-537 after #1015, #1016, and #1017. - #1019 reconciles claims after #1016, #1017, and #1018. +### 13. Executable mapping and time amendment (#1355, 2026-09-24) + +The DRAFT statuses in section 1 record the original #813 decision; SEM-234 is +now ACTIVE. The published `sem-234/rev1` profile remains a sealed statement of +intent. Its edge, time, loss, and evidence references are not executable +services. An admitted mixed action now requires an installed, revision-pinned +`MixedEdgeExecutionBinding` for its exact directed edge. The binding joins the +admitted route and time mapping to one source action subject, one destination +subject, an executable mapper, a time service, and a bridge. The current +reference runtime requires both compiled action addresses to equal the +governed request and the destination provider's admitted action allocation. +The bridge may translate its pinned backend-native subject internally, but +the mapper cannot alter the portable request's participant identity, action, +authority, audience, terminal-outcome demand, or other governed fields. A +missing or mismatched binding refuses before a provider call. + +The control plane retains operation ownership and commits the RUN-310/API-423 +decision and exact provider attempt before the bridge runs. The bridge receives +the owning operation id and may call the selected provider once. The installed +time service reads the admitted two-clock state, provides a correlated order +grant, and reads back after execution. Mapping and timing evidence must satisfy +the admitted edge obligations. The current executable profile admits a proved +comparison within one clock segment; an incomparable or unproved relation +refuses. This uses shared time semantics and does not imply a common physical +clock, hard real-time synchronization, or physical-OT timing guarantees. + +Backend execution, destination delivery, and participant observation remain +separate facts. A correlated bridge execution report requires backend readback; +delivery additionally requires a destination receipt read through its own +installed service; observation additionally requires exact participant and +audience readback. The bridge result, a timestamp, an evidence reference, or +`ApplyResult.success` alone cannot create either later fact. An authorized +declared mapping loss appears only with the correlated execution report. A +known partial result or unresolved delivery is `INDETERMINATE` under the shared +operation lifecycle, retaining known evidence and blocking dependent work +until explicit resolution. Idempotent replay returns the original operation; +it never invokes the bridge again. + +A staged membership change requires an installed handoff binding with exact +source and destination native owners. Its admitted clock mapping receives a +correlated order grant and typed readback before transfer. A committed native +transfer must be followed by destination-owner and time readback at the +expected phase revision before the new phase and handoff fact commit. Failed +or stale transfer with old-owner readback keeps the prior phase; pending or +uncertain transfer is `INDETERMINATE` and blocks dependent effects. The store +claims phase transitions and other mixed effects under one run-scoped +conflict boundary before external calls. Native ownership remains distinct +from the RUN-310 acting controller and disclosure authority. + +Compatibility is fail closed. Existing `sem-234/rev1` plans and historical +reference-only records remain readable with their original meaning; their +mapping refs, success booleans, and timestamps are not reinterpreted as +executed delivery, observation, or handoff. Pure paths continue under their +existing operation contract, but also make no unsupported delivery or +observation claim. This amendment does not change a published schema; the +executable services are trusted runtime bindings to the already admitted +profile. Another bridge implementation can use the same binding seam after +provider-local capability and conformance admission. It receives no authority +from its name, installation, or manifest claim alone. + ## Consequences RAES can represent both backend substitution and mixed composition without @@ -321,3 +381,9 @@ problem and leaves a versioned seam for later work. - [Architecture preflight](../issue-813-cross-backend-participant-control-preflight.md) - [Research and implementation program](../../research/cross-backend-participant-control/) - [SEM-234 and ASR-537 formal design](../../../specs/formal/participant-semantics/cross-backend-participant-control.md) + +## Amendments + +| Date | Commit/PR | Summary | +| --- | --- | --- | +| 2026-09-24 | #1355 | Required executable mixed mappings, bridge and time coordination, independent stage readback, and native staged handoff while preserving historical reference-only meaning. | diff --git a/docs/decisions/adrs/adr-index.yaml b/docs/decisions/adrs/adr-index.yaml index 2716cce36..207c63025 100644 --- a/docs/decisions/adrs/adr-index.yaml +++ b/docs/decisions/adrs/adr-index.yaml @@ -579,7 +579,11 @@ adrs: summary: "Rebind the #1354 publication reference to ADR-114 after ADR-113 was assigned to #1350; semantics are unchanged." - id: ADR-102 path: docs/decisions/adrs/adr-102-mixed-cross-backend-participant-control.md - pin: cfcb0f5b7291b47fe6ff6096bb18dd9063b83ee5d4f7f6a9cafbdd06f21bf716 + pin: e00772b8642d117da413cceb3767e865ebaf3cecd55d2d8f04d8d43205d79027 + amendments: + - date: 2026-09-24 + ref: "#1355" + summary: "Required executable mixed mappings, bridge and time coordination, independent stage readback, and native staged handoff while preserving historical reference-only meaning." - id: ADR-103 path: docs/decisions/adrs/adr-103-branch-aware-python-coverage-policy.md pin: a44acbc2db1b5349ba316ba0d09bd9b46310db016cb87937b08bc6bc107755aa diff --git a/docs/decisions/issue-1355-executable-mixed-mapping-time-preflight.md b/docs/decisions/issue-1355-executable-mixed-mapping-time-preflight.md new file mode 100644 index 000000000..1532942fe --- /dev/null +++ b/docs/decisions/issue-1355-executable-mixed-mapping-time-preflight.md @@ -0,0 +1,320 @@ +# Issue #1355 — Executable mixed mapping and time preflight + +Date: 2026-09-24. Inspection baseline: `b00aba06389a`. +Scope: architecture guidance for the issue #1355 decision, not an accepted +normative amendment or an implementation plan. +This note does not activate a backend, publish a new contract, or establish a +mixed-execution conformance claim. The issue's title, body and acceptance +criteria remain the delivery contract. The supplied diagnosis is corroborated +by `raes_runtime/mixed_runtime_dispatch.py`: an edge's mapping and loss are +recorded but not executed, and one backend `success` value produces delivery and observation +facts. The existing reference explanation describes this behavior; it is not +evidence that those later stages occurred. +`MixedCompositionEdgeModel` carries routing and time references but no +executable subject translation, bridge invocation or result/readback binding. +`mixed_runtime_phase.py` also derives a `handoff` event from a permitted phase +evaluator; that fact alone cannot prove native responsibility transfer. + +## Decision boundary + +Keep the admitted `sem-234/rev1` profile as sealed intent and the one +`RuntimeControlPlane` as state authority. Resolve each active directed edge to +an executable, version/digest-matched mapping and bridge responsibility at the +existing trusted `MixedRuntimeBinding` / selected `RuntimeTarget` boundary. +The binding must identify the source semantic action or observation subject, +destination subject, owning operation and component, transformation, invocation +and readback contract, time-domain/order service, declared loss, failure +disposition and evidence obligations. An edge reference, callable method, +timestamp, manifest claim or backend name alone cannot establish any of these. +Use the existing compiled identities and admitted allocation/edge/time-model +refs; do not add apparatus choice or backend commands to portable SDL. + +Execute the binding under the existing RUN-310 action/control, +RUN-319/API-423 crossing and final-sink gates. A direction or handoff does not +itself invoke an effect. Exact subject mapping must preserve participant, +episode, controlled scope, action-family and audience identity, and refuse +unmapped, ambiguous, conflicting or out-of-scope subjects before invocation. +Native addresses may change; their join to those semantic identities must not. +Validate both source and translated destination shapes and the final sink's +exact subject/policy cut. Bind units, cardinality, value ranges and lossy or +non-invertible transformations explicitly; never assume a reverse edge or +round-trip equivalence. A declared loss is acceptable only under admitted +requirements and authorized weakening, not because it was logged afterward. +The component that owns a native object or the destination of a directed edge +does not thereby become acting controller, release authority or owner of the +RAES operation. A bridge may narrow an authorized projection; it cannot +broaden it, transform an unauthorized value into an authorized one, or supply +an absent policy decision. Each actual edge crossing needs its own invocation +and result correlation; an edge in the profile does not imply a bridge call. + +Time execution must use the incumbent `TimeModelDeclarationModel`, +`TimeRuntimeStateModel`, `TimeCoordinateModel`, progression/transition checks +and component `TimeRuntime` readback. Bind source and destination clock/domain, +segment, mapping direction, required comparison, ordering basis and selected +progression or synchronization service to the operation cut. Obtain grants or +barrier/serialization evidence where that admitted service is required; read +back the resulting state before asserting the comparison or delivery order. +An affine or identity declaration is a coordinate relation, not a scheduling +service. Partial order permits only demonstrated comparisons; incomparable +events remain incomparable. A timestamp-only source can support only its +declared weak claim. Operational monotonic supervision budgets remain separate +from authored scenario time. Physical or operational components may refuse +pause, reset, rollback, lookahead or tight coupling; the profile must admit +that limitation or the operation must be refused. No common clock, hard real +time, or physical-OT timing guarantee follows from shared time semantics. +Clock conversion must retain exact rational and segment/microstep semantics; +never round a fractional coordinate into an asserted exact tick. Cyclic coupling +needs an admitted progress basis and bounded stall disposition; topology alone +proves neither deadlock freedom nor safe rollback. Control-loop posture, world +assumption and membership remain independent axes. + +## Outcome and handoff invariants + +| Boundary | Owning evidence and permissible claim | +| --- | --- | +| Request accepted | `OperationReceipt`/`ControlPlaneOperationRecord` and immutable admission context prove acceptance only. Recheck effective capability and contextual willingness before dispatch. | +| Decision and attempt committed | RUN-310/API-423 decision plus composition history and complete history-head/snapshot CAS prove authority for one attempt, not execution. A failed commit invokes nothing. | +| Backend execution | Correlated provider result and validated typed readback prove only the established effects. A contract-satisfying no-op need not change state. A boolean, exception-free return or echoed request is insufficient. | +| Directed delivery | API-423 delivery attempt and a destination receipt or equivalent admitted sink evidence prove delivery to that boundary. Mapping/bridge success alone does not. | +| Participant observation | API-423 observation is emitted only after its own participant/audience projection and observation evidence. Delivery, status-view construction, audit retention and experiment collection do not imply observation. | + +Use the shared operation lifecycle (`ACCEPTED`, `RUNNING`, `SUCCEEDED`, +`FAILED`, `CANCELLED`, `INDETERMINATE`) and its supervision semantics for +settlement. Preserve known partial effects as correlated evidence and select +the terminal state from requirement satisfaction and cessation evidence; do +not add a `PARTIAL` state. At bounded settlement, unknown required effect, +delivery or observation is `INDETERMINATE`; a known, quiescent partial failure +retains its validated residual effects. A committed terminal parent is immutable: +later evidence belongs to an authorized linked resolution. Timeout cannot prove +zero effects or success. Pre-claim refusal remains audit-only; contextual refusal +after acceptance and before dispatch follows the shared cancellation rule. +Do not re-invoke an effect through idempotent replay, restart or phase +progression. Retain conflicting-effect +exclusion while cessation is unknown. Commit terminal operation, snapshot, +owning histories and safe audit through the incumbent store transaction; an +uncertain store acknowledgement poisons readiness until authoritative readback. +Correlation must distinguish operation, invocation/stage, directed edge, +component, phase revision and the original authority/time cut. Recover every +invoked stage from its persisted responsibility; the current single-component +`mixed_recovery_target()` alone cannot reconcile a multi-stage bridge operation. +Local atomic publication does not make effects across components atomic or +exactly once. Repeated, reordered or late receipts cannot create a second +effect or rewrite terminal history. + +Use [the shared supervision semantics](../../specs/formal/runtime-control-plane/supervision.md) +for all external calls, including capability checks, bridge invocation, time +grants/barriers, handoff evaluators and readback. They require finite budgets, +retained conflicting-effect exclusion and a serviceable supervision path. +At this baseline, `RuntimeMutationAuthority.external_call()` prevents re-entry +but retains the logical mutation permit; it supplies neither interruption nor +the supervision guarantee. The #1348 tests are design-model witnesses. Treat +the shared supervision implementation as a dependency for any such positive +claim; do not hide a second timeout/worker engine in mixed dispatch. A finite +phase count or evaluator attempt bound does not bound callback duration. + +For staged phases, quiesce outstanding attempts and deliveries under their +original provider before committing the next phase. Native responsibility +handoff has requested/offered/pending/committed/failed/expired/cancelled/stale +dispositions under MCB-013–017; only an evidenced, revision-fenced commit +changes responsibility. RUN-310 controller handoff is a separate API-409 +occurrence and never follows from native ownership transfer. A stale +controller, authority, capability, policy, state/history head or governed +order refuses a new effect. Failed or unknown handoff leaves the last committed +responsibility fact unchanged and blocks dependent work. Unknown native transfer +does not prove the former provider can safely continue: quarantine that scope +until both responsibility and cessation are reconciled. Quiescence includes +lifecycle work, pending deliveries, time services and callbacks, not just the +action/crossing records currently scanned by `_mixed_runtime_is_quiescent()`. +Inter-trial changes retain distinct plan-entry/run identities and source lineage. + +## Canonical owners and compatibility + +Package-qualified paths below are relative to `implementations/python/packages/`. + +| Concern | Existing owner to extend or reuse | +| --- | --- | +| Authored meaning and admission | `specs/formal/participant-semantics/cross-backend-participant-control.md` MCB-001–045, ADR-102, `MixedParticipantCompositionProfileModel`, bounded `parse_mixed_composition_profile()`, `validate_mixed_composition_context()`, `AdmittedTrialPlanModel`, `revalidate_admitted_trial_plan()` and trial compiler apparatus/capability admission. An evidence ref must resolve to evidence that supports its specific obligation; presence of the ref alone is insufficient. | +| Effective support | API-407 `BackendManifestV2Model` / `ParticipantFeatureSupportModel`, `manifest_authority.py`, `raes_backend_protocols/participant_feature_admission.py`, `capability_admission.py::time_model_capability_gaps`, `participant_control_admission.py`, registry component/method checks and selected realization envelopes. Separate declaration, installed implementation, per-context willingness, conformance evidence and authorized downgrade; no union of component manifests. | +| Runtime and persistence | `MixedRuntimeBinding`, `mixed_runtime_dispatch.py`, `RuntimeTarget`, `backend_calls.py`, `backend_snapshot_contracts.py`, `RuntimeMutationAuthority`, `ControlPlaneOperationRecord`, `ControlPlaneStoreCommitAdapter`, lease/CAS/recovery and `MixedCompositionRuntimeEventModel`. Composition history cites owning facts; it is not another operation, crossing or control ledger. | +| Policy and results | `participant_control_mediation.py`, `participant_crossing_{mediation,commit,egress}.py`, `participant_flow_sink.py`, `ParticipantActionAdmissionRequest`, API-423 contextual validation and API-408 projections. Use their final sinks and distinction between attempt, delivery and observation. | +| Time and evidence | `raes_contracts/contracts/time_model.py`, `raes_runtime/time_control.py`, `time_coordinator.py`, `ParticipantRuntimeOrderingBasis`, `TimeRuntime` and runtime readback; `raes_conformance/time_semantics.py` and the existing conformance probe/report framework, scoped observation demand, apparatus evidence and ASR-537 claim separation. Preserve declared loss and uncertainty through result and history. | +| Publication and verification | `ContractModel(extra="forbid")`, `schema_bundle()`, `contracts/schemas/`, schema publication manifest/entries/fixtures, ADR-061 compatibility, `.ground-control.yaml`, `.gc/plan-rules.md`, canonical nox/policy checks and targeted #1014–#1016, time, crossing and #1348 tests. | + +The accepted issue decision should amend SEM-234's executable edge/handoff +meaning, API-407's effective mapping/time/bridge support obligations, and +ADR-102's reference-only boundary as needed, without silently changing the +meaning of an existing published `sem-234/rev1` profile or manifest. If an old +carrier cannot express a required executable binding or correlated stage +outcome, publish a versioned, closed contract and explicit reader/compatibility +rule. Historical reference-only records remain reference-only; do not +reinterpret their `success`, mapping refs or timestamps as delivery, +observation or governed timing proof. Keep supported old single-target/pure +paths working, while refusing a mixed arrangement whose new obligations have +no effective implementation. Executable examples must drive the actual +control-plane/target boundary, with positive and negative cases for pure, +simultaneous mixed, linked inter-trial and pre-admitted staged arrangements; +assert the call count, distinct stage facts, readback, loss and final state. + +Use `specs/formal/runtime-contracts/participant-backend-contracts.md` for +API-407 changes. Keep its governed feature terms, scope/required-contract maps, +model/dataclass adapters and JSON Schema parity aligned; unknown extension +terms must not gain vacuous exact support from an empty required-contract set. +Support strength alone cannot compare incompatible constraints. Resolve evidence +and downgrade authority in trusted context; the existing feature resolver checks +reference presence and strength, not the truth of executable obligations. +Per-edge bindings belong outside the open capability `constraints` map. Reuse +API-424 mechanism/effect bindings where applicable without confusing mechanism +identity with SEM-234 apparatus identity. + +### API-407 declaration boundary + +Apply the incumbent [API-407 declaration/admission guardrails](issue-1072-api-407-feature-support-preflight.md) +to #1355. `capabilities.participant_runtime.feature_support` remains the sole +participant strength declaration, using the existing four-level scale +(`unsupported < disclosed_weak < bounded < exact`). Partial or constrained support is expressed through that level and +its constraint, limitation, disclosure and evidence references, not a new +`partial` enum or mixed-backend support block. Those four reference roles are +not interchangeable. SEM-218 `realization_support` and the selected realization +envelope remain independent cross-domain requirements. Neither establishes +participant support; participant support cannot waive them. + +Shared time already has `TimeCapabilities` and +`capability_admission.py::time_model_capability_gaps`, covering domain, +authority, progression, synchronization, mapping, capacity, reset and replay +declarations. Reuse these for the applicable component time obligations; +do not copy their fields into API-407 or make every component support every +other component's clock. An exact participant feature claim does not establish +a barrier, bridge, serialization service or timing guarantee. Effective support +requires their installed implementation and evidence for the particular +provider, directed edge and phase. The mapping-kind check currently recognizes +`identity` and `affine_rational`; partial-order semantics cannot be introduced +as an arbitrary new string or inferred from timestamp ordering. + +Two current validator seams need explicit treatment in the accepted design: + +- `resolve_participant_feature_support()` returns `None` for a legacy listed + feature outside the evidence-required set when no entry exists. This makes + no strength claim. Preserve that legacy behavior outside the newly claimed + scope, but require an explicit entry for a mixed obligation needing a + strength. Unsupported never becomes an executable downgrade. +- Unknown governed extension terms can resolve to an empty required-contract + set. Vocabulary syntax alone must not confer executable support. If new + terms are necessary, align the vocabulary, scope, required-contract map, + backend-contract allowlist, evidence-required set, schema and dataclass/model + adapters. `BackendManifestV2Model._validate_participant_policy_contracts` + currently indexes the **behavior** map for every evidence-required term; + adding an interaction term to that set alone is invalid. Declaration-only + terms must not enter `PARTICIPANT_RUNTIME_POLICY_FEATURES`, which also drives + runtime policy behavior and reference-backend declarations. + +The resolver compares strength and checks reference presence; trusted +`MixedCompositionResolutionContext` joins must establish evidence satisfaction +and exact downgrade authorization. Apply constraints to the selected binding: +equal strength does not make incompatible units, bounds or services compatible. +Keep requested and effective support distinct, retain weakening provenance, +and recheck current willingness before effects. A runtime refusal or unknown +operation outcome is not a new manifest support level. Use the existing +planner gaps and conformance runner, with provider-local negative cases in +`test_backend_manifest.py`, `test_issue_1014_mixed_composition_contracts.py` +and `test_issue_1015_mixed_staged_trial_admission.py`; declared references alone +cannot replace executed mapping/time probes. + +ADR-059 requires an ADR-102 amendment row and matching `adr-index.yaml` record +and pin for any accepted-text change. ADR-061 and +`contracts/schema-publication/README.md` govern schema evolution: update the +owning `contracts/schema-publication/entries/` record (the root manifest is an +index), generated bundle parity and fixtures. Keep semantic revision, wire +version and evidence release distinct; preserve immutable historical evidence. +This preflight leaves those normative artifacts unchanged. + +## Cross-cutting gates + +1. **Ingress and configuration:** keep bounded JSON parsing, duplicate/depth + checks through `json_ingress.py`, closed profile/plan models, digest and + exact-context joins. Bound translated payloads, graph/context traversal and + fan-out too. Direct Python inputs require the same validation; frozen + dataclasses and mapping proxies do not deeply freeze nested models. + `ControlPlaneConfiguration`, `MixedRuntimeBinding`, `RuntimeTarget` registry + signatures and manifest/envelope identity checks validate the installed + binding. Neither HTTP fields nor environment variables select a component, + bridge, clock or mapping. New executable parameters belong in the trusted + binding of an admitted edge, so another conforming adapter does not require + changes to SDL, the dispatcher's semantic selection or store ownership. + Parameterize that seam by pinned mapping/bridge version, source/destination + subjects, service/readback contract and admissible bounds. Resolve installed + implementations through the existing registry/protocol boundary; portable + refs are not module imports, scripts, filesystem paths or fetchable URLs. +2. **HTTP and authorization:** retain `create_control_plane_app()`, + `RequestSizeLimitMiddleware`, closed request DTOs, bounded queues, + `Idempotency-Key`, `_ControlPlaneApiAuth`, + `ControlPlaneSecurityConfig.strict_defaults()`, logical target binding and + participant/controller/audience subjects. No backend token, native owner, + component id or bridge identity supplies participant authority. +3. **Secrets, environment and host:** retain `RuntimeEnvironmentVariable` + name/value versus `value_from`, classification and redaction validators, + `secret_references.py`, runtime-fact binding policy, credential sanitizers + and `control_plane_store_paths.py`/`control_plane_store_lease.py` checks. + Environment names must be nonblank and exclude `=`; `value` and `value_from` + are exclusive, generated values cannot claim `operator_secret`, and redacted + or operator-secret values cannot carry plaintext. Keep these authored runtime + shapes distinct from host credential injection. Carry safe ids, refs and bounded + diagnostics, not secret values, payloads, host paths or low-entropy secret + digests. The coordinator adds no subprocess, shell, socket or argv/env + authority; backend-owned native I/O must stay behind admitted endpoints and + host permissions, never arbitrary request-selected destinations. Never expose + tokens or action data in process arguments, logs or tracebacks. Existing + `require_single_worker_configuration()` and store ownership, link and private + file/sidecar permission gates still apply. + If an adapter consumes generated environment values, it must also pass + `raes_processor/planner/stateful_admission.py`'s exact projection keys, + delivery mode, node/output, consumer and sensitivity joins. Reuse + `prepared_node_projection.py`; an arbitrary environment dictionary cannot + bypass these checks merely because the SDL value shape was valid. +4. **Backend and publication:** keep deep-copy call isolation, backend result + type/ownership/changed-address checks, time readback, strict snapshot codec, + history-head and revision CAS. `Diagnostic` and existing result envelopes + use `backend_result_diagnostics.py`, `backend_account_credentials.py` and + `portable_diagnostic_payload()` for stable value-free codes; + `control_plane_api/_responses.py` and `_operation_routes.py` keep conflict, + validation and 500 responses redacted. Preserve `StrictJsonIngressError`, + validation errors and `SnapshotRevisionConflict` instead of adding a bridge + exception hierarchy. `AuditEvent` and the existing module loggers record safe + operational facts, not participant observation or experimental evidence. + `portable_diagnostic_payload()` checks the portable shape, not redaction. + Manifest/admission validation messages can interpolate rejected terms; + new public responses, audit and logs must not forward raw exception text, + rejected values or exception causes. Sanitize addresses as well as messages. + Apply the existing plane/audience projections to capability reasons, evidence + refs, membership and timing metadata too; a safe string can still disclose + information to an unauthorized participant. + +## Gotchas, non-goals and assurance boundary + +Avoid a second bridge policy engine, operation ledger, exception hierarchy, +schema base, clock, store, controller state or workflow engine. Do not infer +execution from a method signature, feature declaration, source timestamp, +edge presence, profile evidence ref, `ApplyResult.success`, receipt order or +metadata. Do not manufacture delivery/observation from backend success; do not +erase prior knowledge on retraction/replay or use audit as participant evidence. +Do not turn partial order into total order, weaken an exact requirement because +one backend is weak, or use runtime fallback after contextual refusal. + +This issue does not require a generic federation framework, backend-native +HLA/FMI/HELICS support, a new physical backend, multi-controller or leased +authority, distributed transactions, universal rollback/retry, universal +collection, empirical transfer, backend equivalence or IFC/noninterference +proof. The accepted design and executable examples must state the bounded +guarantee and test zero prohibited calls for pre-effect refusals, distinct +execution/delivery/observation evidence, partial/unknown after-effect paths, +stale and failed handoff, incompatible clocks and weak timing, restart +reconciliation, and a successful mapped exchange. + +Use `.ground-control.yaml`, `.gc/plan-rules.md`, `tools/policy/requirement_order.yaml`, +`noxfile.py` and `.pre-commit-config.yaml` for workflow and verification. Set +`RAES_REQUIREMENT_UID=API-407` for this requirement's work, or `SEM-234` for +its semantic-owner work, when needed. Run only targeted local checks; +full, integration and fuzz suites remain CI-owned. Extend the #1014–#1016, +#1200, API-421/shared-time, crossing, API and operation-lifecycle witnesses +where their owning boundary changes; design-model tests and golden metadata +cannot replace executed adapter/bridge probes. No implementation or new tests +are part of this preflight. diff --git a/docs/explain/reference/mixed-participant-composition.md b/docs/explain/reference/mixed-participant-composition.md index 85c3ed6a6..735d685cb 100644 --- a/docs/explain/reference/mixed-participant-composition.md +++ b/docs/explain/reference/mixed-participant-composition.md @@ -80,7 +80,10 @@ Provider membership does not create a controller or disclosure permission. `RuntimeControlPlane` accepts an immutable `MixedRuntimeBinding` only when its plan entry, profile digest, trusted resolution context, component manifests, realization envelopes, runtime targets, run scope, and transition evaluators -match exactly. Activation commits the admitted initial phase into typed +match exactly. Executable mixed edges additionally bind a pinned bridge, exact +source and destination action subjects, an installed time service, and +independent destination and audience readback. Activation commits the admitted +initial phase into typed `mixed_composition_states` and append-only `mixed_composition_history` fields in `runtime-snapshot-v1`. A second activation is either an exact idempotent replay or a refusal; it cannot replace the incumbent composition. @@ -89,13 +92,27 @@ Participant action ingress still passes through the incumbent RUN-319/API-423 crossing and final-sink policy decision. Under the same mutation cut, the coordinator resolves one active participant allocation, action allocation, authenticated controller and action authority. If the providers differ, it -also requires the admitted directed edge and records its time mapping and -declared mapping loss. The coordinator atomically commits `decision` and -`attempt` facts before invoking the selected component. It then appends the -result plus delivery and observation facts, an explicit weakening fact when -mapping loss applies, or a failure fact when the provider refuses. An inactive, -ambiguous, unmapped, unauthorized, stale, or unsupported cut invokes no -component and discloses no backend result. +also requires an executable binding for the admitted directed edge. That +edge's subject, audience, policy cut, controller, disclosure authority, and +permitted final-sink decision must match the live crossing before any bridge +call. The binding preserves the governed compiled action address through the destination +provider's admitted action allocation, verifies the two declared clocks and +mapping against typed runtime readback, obtains a correlated order grant, and +invokes the selected provider once through the bridge. The coordinator +atomically commits `decision` and `attempt` before invocation. It appends a +backend result from correlated execution evidence. It appends `delivery` only +after destination receipt readback and `observation` only after participant and +audience readback. An explicit weakening fact carries the declared mapping +loss when the bridge reports it. A success boolean, mapping reference, or +timestamp cannot create a later stage. A missing or stale binding, incompatible +time readback, ambiguous mapping, unauthorized subject change, or failed +pre-effect commit invokes no component. Partial execution, unknown effects, +and unproved required delivery use the shared `INDETERMINATE` operation state +until explicit reconciliation; replay never repeats the bridge call. +Order checks include the microstep when mapped ticks are equal. A provider +result rejected by the incumbent backend gate cannot publish successful +execution, delivery, observation, or loss facts; a later readback failure +retains only the stages already confirmed under the same operation. Participant episode initialize, reset, restart, and terminate calls resolve the active participant allocation and authenticated controller in the same way. @@ -105,20 +122,45 @@ coordinator is never used as an unadmitted lifecycle fallback. Staged progression invokes only the evaluator bound to the admitted `evaluator_ref`, enforces its finite `progress_bound` and required evidence, -and commits a monotone phase revision plus handoff fact. Evaluator exceptions -become sanitized failure facts without changing phase membership. Snapshot -history-head checks and store revision CAS prevent stale concurrent commits. -The authoritative operation ledger also refuses progression while a mixed -effect is accepted, running, or indeterminate, so provider responsibility -cannot change around an outstanding effect. Restart recovery derives the exact -component from the durable pre-effect -attempt and never falls back to the logical target. +and requires an executable native handoff when the active component set +changes. That handoff obtains an admitted time grant and typed clock readback, +invokes the pinned transfer service, then reads back the native owner and time +state. Only a committed transfer with exact destination-owner readback commits +the next phase and `handoff` fact. Failed or stale transfer retains the old +phase; pending or unknown transfer is `INDETERMINATE` and blocks dependent +work. The store serializes run-scoped phase claims with mixed actions before +external calls, while snapshot history-head and revision CAS protect the +terminal commit. Restart recovery derives the exact component from the durable +pre-effect attempt and never falls back to the logical target. An interrupted +mixed edge cannot be promoted from a provider-only recovery observation: its +bridge, time, delivery, and audience stages remain unproved. An interrupted +native handoff likewise retains the old phase with an `INDETERMINATE` operation +until its owner and time cut are reconciled. A partial crossing history stays +quarantined during restart and cannot be administratively accepted as a valid +current snapshot. Generic current-snapshot acceptance cannot clear an interrupted +mixed edge or native handoff; their external stages require specific reconciliation. +Startup validates other crossing histories and the retained prefix before an +interrupted crossing. Time and bridge callbacks receive isolated snapshot or +time inputs, and a changed bridge snapshot is refused before the provider call. This is a single-control-plane reference realization. It does not claim backend-native federation, multi-controller consensus, leases, HLA ownership transfer, joint/fused action semantics, IFC/noninterference, equivalence, exactly-once external effects, or conformance of any production backend. +The executable examples in +[`test_issue_1355_mixed_mapping_time.py`](../../../implementations/python/tests/test_issue_1355_mixed_mapping_time.py) +drive the control plane with an installed bridge and time service. They cover +an evidenced mixed exchange, separated delivery and observation, missing +bindings, stale clock readback, unauthorized mapping changes, partial/unknown +outcomes and replay, and committed/failed/stale/pending staged handoffs. Run +the focused examples with `uv run --project implementations/python --frozen +pytest implementations/python/tests/test_issue_1355_mixed_mapping_time.py -q` +from the repository root. The stub receipts and native owner are test services; +they are not conformance evidence for a deployed apparatus. Linked inter-trial +identity remains covered by the admitted-trial tests and never becomes a +within-run fallback. + ## Four worked realizations | Case | Allocation and transition | Expected meaning and evidence boundary | @@ -207,7 +249,7 @@ fulfillment of the corresponding invariant family. | SEM-234(4), MCB-013–022 | Exact cut, policy/authority joins, existing SEM-230 projection; metadata, revocation and single-controller tests | No provider handshake, new RUN-310 protocol or noninterference proof | | SEM-234(5), MCB-027–034 | `advance` and `link_trials`; changed provider, immutable identity, stale/pending/commit and history tests | Synthetic result and trigger facts; no cleanup or derived-model realization | | SEM-234(6), MCB-035–037 | Cartesian axis cases and open-loop actuation refusal | Not description closure or a backend/product catalog | -| SEM-234(7), MCB-023–026, 038–041 | Directed partial-order closure, fresh cuts, explicit loss, refusal and commit tests plus `test_issue_1016_mixed_runtime_coordination.py` | Reference final-sink coordination is bounded to one control plane; not a clock synchronizer or distributed transaction | +| SEM-234(7–8), API-407, MCB-023–026, 038–041 | Directed partial-order closure, fresh cuts, explicit loss, refusal and commit tests plus `test_issue_1016_mixed_runtime_coordination.py` and `test_issue_1355_mixed_mapping_time.py` | Trusted installed bridge and time services are required; the stub witnesses are not deployed backend conformance or a physical clock guarantee | | MCB-042–045 / ASR-537 | Demonstration and separate-claim definitions; source/nonclaim policy checks | No executed apparatus demonstration, universal transfer, proof or backend conformance result | | SEM-230 | Existing `project_history`/crossing decisions plus `test_sem_230_information_flow_control.py` | Retains admission, output projection, release, transformation, hidden/visible labels, policy change and quantified claim boundary | | SCE-002 | `test_sce_002_trial_compiler.py` and immutable phase-plan tests | Incumbent composition/parameterization/randomization are reused; mixed compilation is not claimed | diff --git a/docs/governance/requirement-scopes/1355.json b/docs/governance/requirement-scopes/1355.json new file mode 100644 index 000000000..61af30ddd --- /dev/null +++ b/docs/governance/requirement-scopes/1355.json @@ -0,0 +1,160 @@ +{ + "schema_version": "requirement-scope/v1", + "issue_number": 1355, + "primary_requirement_uid": "SEM-234", + "requirement_uids": [ + "SEM-234", + "API-407" + ], + "bindings": { + "docs/decisions/adrs/adr-102-mixed-cross-backend-participant-control.md": [ + "SEM-234" + ], + "docs/decisions/adrs/adr-index.yaml": [ + "SEM-234" + ], + "docs/decisions/issue-1355-executable-mixed-mapping-time-preflight.md": [ + "SEM-234" + ], + "docs/explain/reference/mixed-participant-composition.md": [ + "SEM-234" + ], + "docs/governance/requirement-scopes/1355.json": [ + "SEM-234" + ], + "docs/requirements/API-407/requirement.md": [ + "API-407" + ], + "docs/requirements/SEM-234/requirement.md": [ + "SEM-234" + ], + "docs/research/formal-semantic-validation/index.md": [ + "SEM-234" + ], + "docs/research/formal-semantic-validation/execution-snapshot-v53.json": [ + "SEM-234" + ], + "docs/research/formal-semantic-validation/analysis-v53.json": [ + "SEM-234" + ], + "docs/research/formal-semantic-validation/bundles/retest-v53.json": [ + "SEM-234" + ], + "docs/research/specification-coverage/index.md": [ + "SEM-234" + ], + "docs/research/specification-coverage/execution-snapshot-v53.json": [ + "SEM-234" + ], + "docs/research/specification-coverage/analysis-v53.json": [ + "SEM-234" + ], + "docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1355-v53.json": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/control_plane_store.py": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/control_plane.py": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/control_plane_recovery.py": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/control_plane_resolution_records.py": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/control_plane_store_local_records.py": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/control_plane_store_memory.py": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/mixed_runtime.py": [ + "SEM-234", + "API-407" + ], + "implementations/python/packages/raes_runtime/mixed_runtime_dispatch.py": [ + "SEM-234", + "API-407" + ], + "implementations/python/packages/raes_runtime/mixed_runtime_edge.py": [ + "SEM-234", + "API-407" + ], + "implementations/python/packages/raes_runtime/mixed_runtime_edge_execution.py": [ + "SEM-234", + "API-407" + ], + "implementations/python/packages/raes_runtime/mixed_runtime_handoff.py": [ + "SEM-234", + "API-407" + ], + "implementations/python/packages/raes_runtime/mixed_runtime_handoff_execution.py": [ + "SEM-234", + "API-407" + ], + "implementations/python/packages/raes_runtime/mixed_runtime_phase.py": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/mixed_runtime_recovery.py": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/mixed_runtime_result.py": [ + "SEM-234", + "API-407" + ], + "implementations/python/packages/raes_runtime/participant_crossing_action.py": [ + "SEM-234" + ], + "implementations/python/packages/raes_runtime/participant_crossing_boundary.py": [ + "SEM-234" + ], + "implementations/python/tests/test_issue_1016_mixed_runtime_coordination.py": [ + "SEM-234" + ], + "implementations/python/tests/test_issue_1355_mixed_mapping_time.py": [ + "SEM-234", + "API-407" + ], + "implementations/python/tests/test_formal_semantic_validation.py": [ + "SEM-234" + ], + "implementations/python/tests/test_issue_989_versioned_evidence.py": [ + "SEM-234" + ], + "implementations/python/tests/test_specification_coverage.py": [ + "SEM-234" + ], + "specs/formal/participant-semantics/cross-backend-participant-control.md": [ + "SEM-234" + ], + "specs/formal/runtime-contracts/participant-backend-contracts.md": [ + "API-407" + ], + "tools/check_specification_coverage.py": [ + "SEM-234" + ], + "tools/formal_semantic_validation/_baseline.py": [ + "SEM-234" + ], + "tools/formal_semantic_validation/_loading.py": [ + "SEM-234" + ], + "tools/formal_semantic_validation/_release_revisions.py": [ + "SEM-234" + ], + "tools/formal_semantic_validation/_releases.py": [ + "SEM-234" + ], + "tools/formal_semantic_validation/_retest.py": [ + "SEM-234" + ], + "tools/policy/requirement_order.yaml": [ + "SEM-234" + ], + "tools/policy/historical_identity_records.json": [ + "SEM-234" + ] + } +} diff --git a/docs/requirements/API-407/requirement.md b/docs/requirements/API-407/requirement.md index 42b018857..a3a695f91 100644 --- a/docs/requirements/API-407/requirement.md +++ b/docs/requirements/API-407/requirement.md @@ -6,14 +6,14 @@ type: INTERFACE priority: SHOULD wave: 2 created_at: 2026-04-03T06:16:04.357369Z -updated_at: 2026-06-21T02:21:42.017233Z +updated_at: 2026-09-24T01:59:47Z --- # API-407 — Participant Feature Support And Constraint Declaration ## Statement -Backend manifests shall declare unsupported, constrained, or partially supported participant features without ambiguity, distinct from general realization-support and disclosure declarations that apply across concern domains. +Backend manifests shall declare unsupported, constrained, or partially supported participant features without ambiguity, distinct from general realization-support and disclosure declarations that apply across concern domains. For admitted mixed participant control, effective provider-local support and installed mapping, bridge, time-coordination, and readback services shall be checked in context; declaration or method presence alone does not establish executable support. Authorized weaker support shall retain its constraint, loss, disclosure, and evidence limits. ## Rationale @@ -70,3 +70,12 @@ Requirement inventory expansion. Participant-feature boundaries need to be expli - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_processor/trial_compiler/compiler.py` (Fail-closed composition admission through provider-local contexts) - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_processor/trial_compiler/realization_admission.py` (Provider-local contextual and apparatus admission orchestration) - TESTS → TEST `implementations/python/tests/test_issue_1015_mixed_staged_trial_admission.py` (Feature, envelope, mapping, context, and apparatus drift rejection coverage) +- IMPLEMENTS → GITHUB_ISSUE `1355` (Provider-local executable mixed-edge and timing support) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime.py` (Installed bridge and time-binding admission against the exact profile and context) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_edge.py` (Executable mapping, bridge, time, and readback support boundary) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_edge_execution.py` (Effective mapped bridge, time grant, and readback enforcement) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_dispatch.py` (Contextual refusal and distinct supported stage evidence) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_handoff.py` (Installed staged transfer and time-service support) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_handoff_execution.py` (Effective native transfer and time-service readback enforcement) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_result.py` (Evidence-bounded outcome settlement) +- TESTS → TEST `implementations/python/tests/test_issue_1355_mixed_mapping_time.py` (Missing support, stale time, mapped execution, and evidenced stage witnesses) diff --git a/docs/requirements/SEM-234/requirement.md b/docs/requirements/SEM-234/requirement.md index b2bc0ae3f..2c916b10d 100644 --- a/docs/requirements/SEM-234/requirement.md +++ b/docs/requirements/SEM-234/requirement.md @@ -6,19 +6,21 @@ type: FUNCTIONAL priority: MUST wave: 4 created_at: 2026-07-31T02:14:06.833733Z -updated_at: 2026-07-31T02:14:06.833733Z +updated_at: 2026-09-24T01:59:47Z --- # SEM-234 — Mixed Cross-Backend Participant-Control Composition ## Statement -RAES SHALL define a revisioned mixed cross-backend participant-control composition profile that: (1) supports both alternative realization of one authored scenario in simulation or emulation/operation and simultaneous composed realization across two or more admitted apparatus components; (2) allocates stable compiled participant, controlled-scope, action-family, observation-source, and crossing refs without adding backend choice to portable SDL meaning; (3) binds every composition edge to apparatus identities, authority, mapping, participant/audience policy, temporal coupling and governed order, mapping loss, failure behavior, and evidence; (4) keeps participant identity, acting controller, action admission, backend realization responsibility, HLA-style ownership, routing, and disclosure authority distinct; (5) represents linked inter-trial realization changes and only finite pre-admitted within-run membership/phase schedules without rewriting trial identity or history; (6) distinguishes open/closed control-loop posture, world assumption, and federation membership; and (7) rejects or explicitly weakens compositions with missing, stale, unsupported, contradictory, or unmapped authority, capability, policy, clock/order, or evidence. +RAES SHALL define a revisioned mixed cross-backend participant-control composition profile that: (1) supports both alternative realization of one authored scenario in simulation or emulation/operation and simultaneous composed realization across two or more admitted apparatus components; (2) allocates stable compiled participant, controlled-scope, action-family, observation-source, and crossing refs without adding backend choice to portable SDL meaning; (3) binds every composition edge to apparatus identities, authority, mapping, participant/audience policy, temporal coupling and governed order, mapping loss, failure behavior, and evidence; (4) keeps participant identity, acting controller, action admission, backend realization responsibility, HLA-style ownership, routing, and disclosure authority distinct; (5) represents linked inter-trial realization changes and only finite pre-admitted within-run membership/phase schedules without rewriting trial identity or history; (6) distinguishes open/closed control-loop posture, world assumption, and federation membership; (7) rejects or explicitly weakens compositions with missing, stale, unsupported, contradictory, or unmapped authority, capability, policy, clock/order, or evidence; and (8) requires an admitted mixed edge or staged handoff to execute its subject mapping, bridge or transfer, time coordination, and readback under the owning operation, with distinct correlated execution, delivery, observation, partial/unknown, and handoff facts. ## Rationale Existing RAES authorities support backend-neutral participant semantics, one selected realization envelope, a single acting controller, crossings, time, capability, and evidence, but do not define simultaneous mixed simulation/emulation composition or staged cross-runtime realization. HLA, co-simulation, cyber-range, LVC, and digital-twin precedents show that routing, ownership, time, topology, and empirical transfer need separate, evidenced treatment. +Executable realization must discharge the admitted edge and time obligations. A reference, timestamp, or backend success value cannot itself prove delivery, participant observation, or a native responsibility handoff. + ## Traceability - IMPLEMENTS → GITHUB_ISSUE `OpenRAE/rae#1016` (Coordinate mixed participant runtimes fail-closed) @@ -34,6 +36,8 @@ Existing RAES authorities support backend-neutral participant semantics, one sel - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane.py` (Single mixed-runtime mutation authority) - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_configuration.py` (Run-matched fail-closed mixed-runtime configuration) - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_recovery.py` (Exact component recovery routing without logical-target fallback) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_resolution_records.py` (Mixed-stage-safe administrative resolution classification) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_recovery.py` (Interrupted mixed edge and native handoff stage quarantine on restart) - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_store_history.py` (Composition history-head CAS support) - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_store_snapshots.py` (Durable composition state and history codec) - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime.py` (Exact admitted component binding and pre-effect provider decision) @@ -99,3 +103,16 @@ Existing RAES authorities support backend-neutral participant semantics, one sel - DOCUMENTS → DOCUMENTATION `docs/research/cross-backend-participant-control/composition-architecture.md` (Mixed cross-backend participant-control composition architecture) - TESTS → TEST `implementations/python/tests/test_issue_813_cross_backend_participant_control_design.py` (Issue 813 structural acceptance gate) - DOCUMENTS → GITHUB_ISSUE `OpenRAE/rae#813` (Design cross-backend participant control against simulation and cyber-range precedents) +- IMPLEMENTS → GITHUB_ISSUE `1355` (Executable mixed mapping, time, stage evidence, and handoff) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_edge.py` (Pinned executable edge, time grant, and independent stage-readback contracts) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_edge_execution.py` (Mapped bridge call, time grant, and correlated readback enforcement) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_handoff.py` (Exact native-owner transfer and readback contracts) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_handoff_execution.py` (Correlated native handoff execution and time-readback enforcement) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_result.py` (Separated action stages and shared operation settlement) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/mixed_runtime_phase.py` (Evidenced staged handoff and prior-phase retention) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/participant_crossing_boundary.py` (Mixed action outcome settlement under the owning crossing operation) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/participant_crossing_action.py` (Partial and unknown action states through the shared operation lifecycle) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_store.py` (Run-scoped phase/effect claim exclusion) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_store_memory.py` (Atomic in-memory mixed claim exclusion) +- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_store_local_records.py` (Atomic durable mixed claim exclusion) +- TESTS → TEST `implementations/python/tests/test_issue_1355_mixed_mapping_time.py` (Executed bridge, time, stage, uncertainty, and handoff witnesses) diff --git a/docs/research/formal-semantic-validation/analysis-v53.json b/docs/research/formal-semantic-validation/analysis-v53.json new file mode 100644 index 000000000..2a9cb84dc --- /dev/null +++ b/docs/research/formal-semantic-validation/analysis-v53.json @@ -0,0 +1,155 @@ +{ + "analysis_id": "issue-1355-analysis-v53", + "claim": { + "allowed_evidence": [ + "production parser and semantic-validator results", + "canonical compiled digests", + "participant contract regression tests", + "pinned protocol, corpus, and execution snapshot" + ], + "claim_id": "asr-530-formal-semantic-validation-retest", + "disallowed_evidence": [ + "schema success as semantic proof", + "workflow reachability as network or exploit reachability", + "FM labels as gate outcomes", + "attribution as counterfactual proof", + "formal prose or maintainer confidence alone" + ], + "evidence_artifacts": [ + "docs/research/formal-semantic-validation/protocol-v2.json", + "docs/research/formal-semantic-validation/corpus/manifest-v4.json", + "docs/research/formal-semantic-validation/execution-snapshot-v53.json", + "docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json", + "docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json", + "docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json", + "docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json" + ], + "falsification_protocol": "Replay every retained and new case through its production entrypoint, require complete digest and evidence joins, execute participant fixtures, and derive status from the recorded outcomes.", + "objective_fail_criteria": "A supported negative passes, a positive fails, an observation drifts, a required participant case is missing, or weaker evidence is promoted to solver, exploit-path, runtime-stability, or counterfactual assurance.", + "objective_pass_criteria": "Every claim class has positive and negative cases, all supported cases reproduce the frozen outcome, every participant obligation has passing positive and negative fixtures, and unsupported classes remain untested.", + "statement": "At the recorded source-state digest, the retained RAES controls have the bounded statuses recorded here; historical releases are integrity evidence, not current replay evidence.", + "threats_to_validity": [ + "The issue-specific corpus is intentionally small and does not enumerate every validator invariant.", + "The participant fixtures exercise reference production contracts and tests, not every independent backend realization.", + "The replay gate runs on one Python reference configuration and one pinned RAES revision.", + "Unsupported solver-level classes have protocol cases but no executable observations." + ] + }, + "claim_results": [ + { + "case_count": 2, + "claim_class_id": "schema-validity", + "evidence_status": "demonstrated", + "limitations": [ + "Bounded to the named source/model structural controls." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 0 + }, + { + "case_count": 4, + "claim_class_id": "semantic-consistency", + "evidence_status": "partial", + "limitations": [ + "Partial coverage of named static semantics and participant obligations, not universal consistency." + ], + "matching_case_count": 4, + "participant_obligation_count": 7, + "replayable_case_count": 4, + "unsupported_case_count": 0 + }, + { + "case_count": 2, + "claim_class_id": "graph-reachability", + "evidence_status": "partial", + "limitations": [ + "Partial workflow control-flow reachability only; not network, service, or exploit reachability." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 0 + }, + { + "case_count": 4, + "claim_class_id": "constraint-satisfiability", + "evidence_status": "demonstrated", + "limitations": [ + "Demonstrated only for raes-finite-domain-satisfiability-v1 and its pinned solver configuration." + ], + "matching_case_count": 4, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 2 + }, + { + "case_count": 4, + "claim_class_id": "exploit-path-validity", + "evidence_status": "demonstrated", + "limitations": [ + "Demonstrated only for the admitted snapshot, typed graph, query, semantics, and bounded search profile." + ], + "matching_case_count": 4, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 2 + }, + { + "case_count": 2, + "claim_class_id": "determinism-stability", + "evidence_status": "partial", + "limitations": [ + "Partial parse-to-compile repeatability only; runtime and backend determinism are untested." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 0 + }, + { + "case_count": 2, + "claim_class_id": "counterfactual-necessity", + "evidence_status": "untested", + "limitations": [ + "Untested because no governed intervention or ablation entrypoint ran." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 0, + "unsupported_case_count": 2 + } + ], + "corpus_revision": "4.0.0", + "evidence_status": "partial", + "execution_id": "issue-1355-execution-v53", + "generated_at": "2026-09-26", + "limitations": [ + "Satisfiability is limited to raes-finite-domain-satisfiability-v1 and its exact translation, theory, and Z3 configuration.", + "The subset-minimal unsatisfiable core is not a universal proof certificate.", + "Exploit-path results are limited to the admitted snapshot, normalized graph, query, transition semantics, and bounded search profile.", + "A valid path is not backend execution and an invalid path is not real-world non-exploitability.", + "The production exploit-path JSON loader permits duplicate keys; the research loader rejects them without claiming stronger production behavior.", + "Participant replay inherits the host environment and is not described as hermetic.", + "Counterfactual necessity remains untested.", + "Scoped observation demand is not a claim class in this preregistration and is not promoted to demonstrated by this retest.", + "EXP-732 provenance joins are verified by their dedicated regression suite; this retained corpus makes no universal run, apparatus, source, or augmentation assurance claim.", + "This retained corpus does not establish native backend attestation fidelity; materialization contract checks remain separate operational provenance, not experimental observations.", + "Capture admission and evidence-proof authority are verified by issue-1237 regression tests, not promoted to a new claim class by this retained corpus.", + "Evidence-requirement refinement lineage is outside this retained formal claim set; this retest refreshes integrated source provenance without promoting that feature to a formal claim.", + "Authoring-adapter transport behavior is outside this retained formal claim set.", + "Operational recovery observation and startup reconciliation are verified by their API-404 regression suite, not promoted to a new formal claim class by this retained corpus.", + "Single-owner store admission, immutable target/run scope, and provider shutdown ordering are verified by their API-404 CP-5 regression suite, not promoted to a formal claim by this retained corpus.", + "Mixed and staged trial admission is verified by its SEM-234/SCE-002/API-407 regression suite, not promoted to a new formal claim class by this retained corpus.", + "Offline control-plane maintenance, readiness, and bounded audit behavior are verified by issue #1186 runtime tests, not promoted to a formal claim by this retained corpus.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 profile declarations and capability admission are covered by dedicated runtime tests; the retained formal corpus does not execute control-plane profile composition.", + "Issue #1016 mixed-runtime coordination is covered by dedicated runtime tests; the retained formal corpus does not establish backend-native mixed realization, multi-controller coordination, IFC, or equivalence.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Issue #1355 mixed mapping, time coordination, handoff, and outcome execution is covered by dedicated runtime tests; this retained formal corpus does not execute mixed providers or establish live backend fidelity." + ], + "plain_language_outcome": "Retained controls replay against the merged backend-operation and denied-egress source. Prior claim limits and unsupported classes remain unchanged.", + "protocol_revision": "2.0.0" +} diff --git a/docs/research/formal-semantic-validation/bundles/retest-v53.json b/docs/research/formal-semantic-validation/bundles/retest-v53.json new file mode 100644 index 000000000..13ea1d46b --- /dev/null +++ b/docs/research/formal-semantic-validation/bundles/retest-v53.json @@ -0,0 +1,122 @@ +{ + "analysis_path": "docs/research/formal-semantic-validation/analysis-v53.json", + "analysis_sha256": "6bccf3a125915a8081238c3a37606dd07dda7e5497012b5d70bb83a39910acba", + "artifacts": [ + { + "artifact_id": "finite-domain-satisfiable-v2-input", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/satisfiable-control.sdl.yaml", + "sha256": "0ca9eaba9dc47171f7a042dc6753faa6c820c65ee966538f9d65fac5342202e8" + }, + { + "artifact_id": "finite-domain-satisfiable-v2-evidence", + "kind": "production-evidence", + "path": "docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json", + "sha256": "554202313d678046958b5c028e2de26ff03c74895cfac552677eed74e8153add" + }, + { + "artifact_id": "finite-domain-unsatisfiable-v2-input", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/unsatisfiable-control.sdl.yaml", + "sha256": "cfef56a1f56d5f0db9da195377fd75694bdd0f0b92932fdb8fafcbd3f7baf6c5" + }, + { + "artifact_id": "finite-domain-unsatisfiable-v2-evidence", + "kind": "production-evidence", + "path": "docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json", + "sha256": "c972725ef64822a75a60380afc11f08eac25b7fe9b091d39b058b3c9f7c8031d" + }, + { + "artifact_id": "typed-exploit-path-valid-v2-input", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/exploit-path-valid-v3.json", + "sha256": "0afe635a63db5b6e6380ac70982fd61d09790745d51a10d670321304121e7c39" + }, + { + "artifact_id": "typed-exploit-path-valid-v2-evidence", + "kind": "production-evidence", + "path": "docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json", + "sha256": "1b7f55d04db172da32658187c64a88c13b5f4d565267ce2be7cb86a9d04cb70c" + }, + { + "artifact_id": "typed-exploit-path-invalid-v2-input", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/exploit-path-invalid-v3.json", + "sha256": "0b2293d4a8983515ff05c516be6e6b418a4f3f09e055250a00bf15fda861aab3" + }, + { + "artifact_id": "typed-exploit-path-invalid-v2-evidence", + "kind": "production-evidence", + "path": "docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json", + "sha256": "244f895a64f14c10916ab0533ab462ce80a328021cd6a50c30a4aa59266d5533" + }, + { + "artifact_id": "schema-valid-control-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/schema-valid.sdl.yaml", + "sha256": "41a9adffdf9f5f2ccc2f887dcf7b15fba3b47c83a1af15f33db872c4a2449d67" + }, + { + "artifact_id": "schema-unknown-field-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/schema-invalid-unknown-field.sdl.yaml", + "sha256": "51cf62319a86c95a2517995939d1f370573051835e4b55bb6d5beaf049640481" + }, + { + "artifact_id": "semantic-resolved-objective-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/semantic-valid-participant-identity-v2.sdl.yaml", + "sha256": "75834bdc883e2003e1c473870bdf75700978955bb83095c6bd718ba6bd3908a6" + }, + { + "artifact_id": "semantic-dangling-assertion-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/semantic-invalid-dangling-ref-participant-identity-v2.sdl.yaml", + "sha256": "1d25bee5f556054e5f0a518df025e4c62e080e1964035e3c1a12e074d88d3a5d" + }, + { + "artifact_id": "semantic-ambiguous-reference-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/semantic-invalid-ambiguous-ref.sdl.yaml", + "sha256": "653cbd2fd62e220d49fb86f80133884207df5ae6752846345ae3085b93f6e4ed" + }, + { + "artifact_id": "semantic-feature-cycle-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/semantic-invalid-feature-cycle.sdl.yaml", + "sha256": "e1f66d95a9ad039687aec8cccbc8843b514072ff08e006c1b4ca6aa5cd8d4ed1" + }, + { + "artifact_id": "workflow-reachable-control-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/workflow-reachable.sdl.yaml", + "sha256": "54c40ceb98ad47247447d737973b2c55e8fb2045e209c7545c4fb20cf42dc3dc" + }, + { + "artifact_id": "workflow-unreachable-step-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/workflow-unreachable.sdl.yaml", + "sha256": "ef22ef2e260f1a7fd92d286f9b571716436b192ddfd54aea7bdfcfdda4ca52a2" + }, + { + "artifact_id": "compile-repeatability-control-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/determinism-a.sdl.yaml", + "sha256": "0bc40900d598c1af7a405d798ca19710405e53ced262d8733081abf12edf89fe" + }, + { + "artifact_id": "compile-non-vacuity-control-comparison-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/determinism-b.sdl.yaml", + "sha256": "d85338f89f20a45515b12da8640173c1a52e47eb17ca0f4f6b4f8f3306e863a1" + } + ], + "bundle_id": "raes-formal-semantic-validation", + "corpus_path": "docs/research/formal-semantic-validation/corpus/manifest-v4.json", + "corpus_sha256": "c57207af72406aa4f70882b9bbeb7cedcc79cf3854c878a95e3eb1fa59ea7a72", + "protocol_path": "docs/research/formal-semantic-validation/protocol-v2.json", + "protocol_sha256": "abf94093e344bf495dfb04e8b0c5985c0beaab8ebb17a75e15c8674fa81b1a7c", + "revision": "54.0.0", + "snapshot_path": "docs/research/formal-semantic-validation/execution-snapshot-v53.json", + "snapshot_sha256": "dcf379f52f0c8d8cdc702625cb93ae5bcb34496b9d16569edd3a57e4570288f1" +} diff --git a/docs/research/formal-semantic-validation/execution-snapshot-v53.json b/docs/research/formal-semantic-validation/execution-snapshot-v53.json new file mode 100644 index 000000000..61db7aea8 --- /dev/null +++ b/docs/research/formal-semantic-validation/execution-snapshot-v53.json @@ -0,0 +1,652 @@ +{ + "baseline": { + "execution_id": "issue-1360-execution-v52", + "release_path": "docs/research/formal-semantic-validation/bundles/retest-v52.json", + "release_revision": "53.0.0", + "release_sha256": "40db954fd4ea0b88ef2d56bed824afc286181782ec88a97c42b0ace7c1b28585" + }, + "captured_at": "2026-09-27T06:49:00.051312+00:00", + "commands": [ + { + "argv": [ + "implementations/python/.venv/bin/python", + "tools/check_formal_semantic_validation.py" + ], + "command_id": "bundle-replay", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/pytest", + "-q", + "implementations/python/tests/test_sem_208_participant_behavior.py::test_hidden_truth_disclosure_is_separate_from_observable_projection", + "implementations/python/tests/test_sem_208_participant_behavior.py::test_hidden_truth_cannot_be_observed_without_explicit_disclosure_rule", + "implementations/python/tests/test_sem_211_participant_action_semantics.py::test_action_contract_declares_sem_211_classes_and_compiles_them", + "implementations/python/tests/test_sem_211_participant_action_semantics.py::test_action_result_rejects_success_when_preconditions_are_unresolved", + "implementations/python/tests/test_run_308_concurrent_participant_execution.py::test_runtime_snapshot_publishes_joint_action_and_time_context_records", + "implementations/python/tests/test_run_308_concurrent_participant_execution.py::test_joint_action_record_contract_rejects_unordered_conflicting_writes", + "implementations/python/tests/test_participant_runtime_invariants.py::test_order_discipline_accepts_supported_order_claim_strengths", + "implementations/python/tests/test_participant_runtime_invariants.py::test_order_discipline_rejects_wall_clock_causality", + "implementations/python/tests/test_sem_212_participant_attribution_semantics.py::test_attribution_edge_round_trips_on_terminal_observation", + "implementations/python/tests/test_sem_212_participant_attribution_semantics.py::test_timestamp_adjacency_cannot_be_reported_as_strong_causality", + "implementations/python/tests/test_sem_215_participant_outcome_interpretation.py::test_outcome_interpretation_rule_parses_and_compiles_explicit_layers", + "implementations/python/tests/test_sem_215_participant_outcome_interpretation.py::test_local_action_success_does_not_imply_objective_success_without_rule_record", + "implementations/python/tests/test_realization_honesty_conformance.py::test_constructive_envelope_runs_positive_and_negative_honesty_probes", + "implementations/python/tests/test_realization_honesty_conformance.py::test_only_native_live_can_support_native_conformance" + ], + "command_id": "participant-fixtures", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/raes", + "processor", + "satisfiability", + "docs/research/formal-semantic-validation/corpus/satisfiable-control.sdl.yaml", + "--profile", + "raes-finite-domain-satisfiability-v1" + ], + "command_id": "finite-domain-satisfiable-v2", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/raes", + "processor", + "satisfiability", + "docs/research/formal-semantic-validation/corpus/unsatisfiable-control.sdl.yaml", + "--profile", + "raes-finite-domain-satisfiability-v1" + ], + "command_id": "finite-domain-unsatisfiable-v2", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/raes", + "processor", + "exploit-path", + "docs/research/formal-semantic-validation/corpus/exploit-path-valid-v3.json", + "--profile", + "raes-exploit-path-analysis-v1" + ], + "command_id": "typed-exploit-path-valid-v2", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/raes", + "processor", + "exploit-path", + "docs/research/formal-semantic-validation/corpus/exploit-path-invalid-v3.json", + "--profile", + "raes-exploit-path-analysis-v1" + ], + "command_id": "typed-exploit-path-invalid-v2", + "network": "disabled" + } + ], + "configuration_id": "raes-python-reference-offline-v41", + "corpus_revision": "4.0.0", + "deviations": [], + "execution_id": "issue-1355-execution-v53", + "execution_status": "complete", + "observations": [ + { + "actual_outcome": "accepted", + "analysis_profile": null, + "case_id": "schema-valid-control", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/schema-valid.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "A passing minimal source does not establish semantic correctness." + ], + "replayable": true, + "result_digest": "f7d364ef384df8a1526b489501835b635021c860793b5764f91d956710d2250c", + "source_digest": null + }, + { + "actual_outcome": "rejected", + "analysis_profile": null, + "case_id": "schema-unknown-field", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": "SDLParseError", + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/schema-invalid-unknown-field.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "The observation covers one unknown-field defect only." + ], + "replayable": true, + "result_digest": "f55d834b458f8e069e1c69061b4cc0a6d61e0e052bf90c670f2e6a5ad8b5bd98", + "source_digest": null + }, + { + "actual_outcome": "accepted", + "analysis_profile": null, + "case_id": "semantic-resolved-objective", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/semantic-valid-participant-identity-v2.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "This is a positive control for one objective-reference slice." + ], + "replayable": true, + "result_digest": "652288785dc09095955ed3649f6407d616fb7c4d4f4188df4ed513ccb7537e0b", + "source_digest": null + }, + { + "actual_outcome": "rejected", + "analysis_profile": null, + "case_id": "semantic-dangling-assertion", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": "SDLValidationError", + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/semantic-invalid-dangling-ref-participant-identity-v2.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "A single dangling reference does not prove complete semantic coverage." + ], + "replayable": true, + "result_digest": "0207cf616b56708ca9b8c4499d3301abe22dbe52162cf8d58d3bec429d9db024", + "source_digest": null + }, + { + "actual_outcome": "rejected", + "analysis_profile": null, + "case_id": "semantic-ambiguous-reference", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": "SDLValidationError", + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/semantic-invalid-ambiguous-ref.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "One namespace collision does not enumerate every ambiguity surface." + ], + "replayable": true, + "result_digest": "9da4a87797d228e0012ab6b30459f4892e41aa6f224a9840be035fee4a2eea73", + "source_digest": null + }, + { + "actual_outcome": "rejected", + "analysis_profile": null, + "case_id": "semantic-feature-cycle", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": "SDLValidationError", + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/semantic-invalid-feature-cycle.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "One static dependency cycle does not establish general constraint satisfiability." + ], + "replayable": true, + "result_digest": "d15dbcd99fb4f20b965d7031b07dd6534576302270399c3fa656d29e7de02b83", + "source_digest": null + }, + { + "actual_outcome": "accepted", + "analysis_profile": null, + "case_id": "workflow-reachable-control", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/workflow-reachable.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "The graph is workflow control flow only." + ], + "replayable": true, + "result_digest": "b1b49649b54bd59d4ef357b39cf9158da90f4eae560f8dd756acf97bd0827a06", + "source_digest": null + }, + { + "actual_outcome": "rejected", + "analysis_profile": null, + "case_id": "workflow-unreachable-step", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": "SDLValidationError", + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/workflow-unreachable.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "The result does not establish network, service, participant, or exploit reachability." + ], + "replayable": true, + "result_digest": "bb931d19346ef9193408ae6c85deb4079704378fc5f00dc5f47a2817cff21943", + "source_digest": null + }, + { + "actual_outcome": "unsupported", + "analysis_profile": null, + "case_id": "whole-scenario-satisfiable-request", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/decisions/issue-168-formal-semantic-validation-reachability-preflight.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "No governed whole-scenario constraint theory or solver exists." + ], + "replayable": false, + "result_digest": null, + "source_digest": null + }, + { + "actual_outcome": "unsupported", + "analysis_profile": null, + "case_id": "whole-scenario-unsatisfiable-request", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/decisions/issue-168-formal-semantic-validation-reachability-preflight.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Local checks cannot produce a whole-scenario unsat certificate." + ], + "replayable": false, + "result_digest": null, + "source_digest": null + }, + { + "actual_outcome": "unsupported", + "analysis_profile": null, + "case_id": "valid-exploit-path-request", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/decisions/issue-168-formal-semantic-validation-reachability-preflight.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "The issue-168 baseline had no canonical typed attack graph or path-query entrypoint." + ], + "replayable": false, + "result_digest": null, + "source_digest": null + }, + { + "actual_outcome": "unsupported", + "analysis_profile": null, + "case_id": "invalid-exploit-path-request", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/decisions/issue-168-formal-semantic-validation-reachability-preflight.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Vulnerability and topology declarations are not an invalid-path proof." + ], + "replayable": false, + "result_digest": null, + "source_digest": null + }, + { + "actual_outcome": "stable", + "analysis_profile": null, + "case_id": "compile-repeatability-control", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/determinism-a.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "The witness ends at compiled output." + ], + "replayable": true, + "result_digest": "11264a648a949917c0e84a2a1e5d116139a35e6cb941844735a422df95141d6c", + "source_digest": null + }, + { + "actual_outcome": "distinguishable", + "analysis_profile": null, + "case_id": "compile-non-vacuity-control", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/determinism-a.sdl.yaml", + "docs/research/formal-semantic-validation/corpus/determinism-b.sdl.yaml" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Distinct digests are a non-vacuity control, not semantic non-equivalence proof." + ], + "replayable": true, + "result_digest": "72c1ee8c7bbc1f970216fa232b3d4ae917bcb003bd823439bbac8a5db94214e2", + "source_digest": null + }, + { + "actual_outcome": "unsupported", + "analysis_profile": null, + "case_id": "necessity-witness-request", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/decisions/issue-168-formal-semantic-validation-reachability-preflight.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "No governed intervention or ablation protocol exists." + ], + "replayable": false, + "result_digest": null, + "source_digest": null + }, + { + "actual_outcome": "unsupported", + "analysis_profile": null, + "case_id": "non-necessity-control-request", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/decisions/issue-168-formal-semantic-validation-reachability-preflight.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Attribution and negative fixtures do not demonstrate non-necessity." + ], + "replayable": false, + "result_digest": null, + "source_digest": null + }, + { + "actual_outcome": "satisfiable", + "analysis_profile": "raes-finite-domain-satisfiability-v1", + "case_id": "finite-domain-satisfiable-v2", + "configuration_digest": "sha256:1204635e17e759e9ad3bd6be2ecb28c6de05c07ead6dfdd15936ed5d3d5b81b2", + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": "scenario-satisfiability-evidence/v1", + "evidence_artifact_path": "docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json", + "evidence_artifact_sha256": "554202313d678046958b5c028e2de26ff03c74895cfac552677eed74e8153add", + "evidence_digest": "sha256:23c2cae7d95d4cc83d77ca576e3911477b169ecc311c977cb45490345f633b5a", + "evidence_profile": "scenario-satisfiability-evidence/v1", + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/satisfiable-control.sdl.yaml", + "docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json", + "specs/formal/scenario-satisfiability/README.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Demonstrates only the pinned finite-domain theory, translation, solver profile, and source." + ], + "replayable": true, + "result_digest": "sha256:23c2cae7d95d4cc83d77ca576e3911477b169ecc311c977cb45490345f633b5a", + "source_digest": "sha256:0ca9eaba9dc47171f7a042dc6753faa6c820c65ee966538f9d65fac5342202e8" + }, + { + "actual_outcome": "unsatisfiable", + "analysis_profile": "raes-finite-domain-satisfiability-v1", + "case_id": "finite-domain-unsatisfiable-v2", + "configuration_digest": "sha256:1204635e17e759e9ad3bd6be2ecb28c6de05c07ead6dfdd15936ed5d3d5b81b2", + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": "scenario-satisfiability-evidence/v1", + "evidence_artifact_path": "docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json", + "evidence_artifact_sha256": "c972725ef64822a75a60380afc11f08eac25b7fe9b091d39b058b3c9f7c8031d", + "evidence_digest": "sha256:317b5cad00aa7f4f7868dca66127611ba19d40ffd86f35815502622814df54c1", + "evidence_profile": "scenario-satisfiability-evidence/v1", + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/unsatisfiable-control.sdl.yaml", + "docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json", + "specs/formal/scenario-satisfiability/README.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "The subset-minimal core is evidence for the pinned translation and solver, not a proof certificate for arbitrary SDL." + ], + "replayable": true, + "result_digest": "sha256:317b5cad00aa7f4f7868dca66127611ba19d40ffd86f35815502622814df54c1", + "source_digest": "sha256:cfef56a1f56d5f0db9da195377fd75694bdd0f0b92932fdb8fafcbd3f7baf6c5" + }, + { + "actual_outcome": "valid-path", + "analysis_profile": "raes-exploit-path-analysis-v1", + "case_id": "typed-exploit-path-valid-v2", + "configuration_digest": "sha256:7f8876d81feb77d3a3239be2fb8337de8885e2744f8786728ba23e4e6027bc0a", + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": "exploit-path-analysis-evidence/v1", + "evidence_artifact_path": "docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json", + "evidence_artifact_sha256": "1b7f55d04db172da32658187c64a88c13b5f4d565267ce2be7cb86a9d04cb70c", + "evidence_digest": "sha256:2d4d1a362751abd9544beb8af7f8c6331d04dac8f4abc315fb261f81fbaf4387", + "evidence_profile": "exploit-path-analysis-evidence/v1", + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/exploit-path-valid-v3.json", + "docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json", + "specs/formal/exploit-path-analysis/README.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "The witness is bounded to the admitted snapshot, normalized graph, query, semantics, and search profile; it does not establish backend execution." + ], + "replayable": true, + "result_digest": "sha256:2d4d1a362751abd9544beb8af7f8c6331d04dac8f4abc315fb261f81fbaf4387", + "source_digest": "sha256:0afe635a63db5b6e6380ac70982fd61d09790745d51a10d670321304121e7c39" + }, + { + "actual_outcome": "invalid-path", + "analysis_profile": "raes-exploit-path-analysis-v1", + "case_id": "typed-exploit-path-invalid-v2", + "configuration_digest": "sha256:7f8876d81feb77d3a3239be2fb8337de8885e2744f8786728ba23e4e6027bc0a", + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": "exploit-path-analysis-evidence/v1", + "evidence_artifact_path": "docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json", + "evidence_artifact_sha256": "244f895a64f14c10916ab0533ab462ce80a328021cd6a50c30a4aa59266d5533", + "evidence_digest": "sha256:1b416bb5a4d29d57c961b769cc9d3af5d9328624e3eebf104d57f39a94c5bb97", + "evidence_profile": "exploit-path-analysis-evidence/v1", + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/exploit-path-invalid-v3.json", + "docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json", + "specs/formal/exploit-path-analysis/README.md" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Structured rejection proves only that this bounded graph/query cannot reach its goal; it does not establish real-world non-exploitability." + ], + "replayable": true, + "result_digest": "sha256:1b416bb5a4d29d57c961b769cc9d3af5d9328624e3eebf104d57f39a94c5bb97", + "source_digest": "sha256:0b2293d4a8983515ff05c516be6e6b418a4f3f09e055250a00bf15fda861aab3" + } + ], + "participant_observations": [ + { + "evidence_refs": [ + "implementations/python/tests/test_sem_208_participant_behavior.py::test_hidden_truth_disclosure_is_separate_from_observable_projection", + "implementations/python/tests/test_sem_208_participant_behavior.py::test_hidden_truth_cannot_be_observed_without_explicit_disclosure_rule" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Covers the reference SDL/contract path, not every backend projection." + ], + "negative_outcome": "passed", + "obligation_id": "hidden-vs-visible-projection", + "positive_outcome": "passed" + }, + { + "evidence_refs": [ + "implementations/python/tests/test_sem_211_participant_action_semantics.py::test_action_contract_declares_sem_211_classes_and_compiles_them", + "implementations/python/tests/test_sem_211_participant_action_semantics.py::test_action_result_rejects_success_when_preconditions_are_unresolved" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Covers declared applicability and one unresolved-precondition failure." + ], + "negative_outcome": "passed", + "obligation_id": "fail-closed-action-applicability", + "positive_outcome": "passed" + }, + { + "evidence_refs": [ + "implementations/python/tests/test_run_308_concurrent_participant_execution.py::test_runtime_snapshot_publishes_joint_action_and_time_context_records", + "implementations/python/tests/test_run_308_concurrent_participant_execution.py::test_joint_action_record_contract_rejects_unordered_conflicting_writes" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Contract evidence does not prove every backend's live concurrency fidelity." + ], + "negative_outcome": "passed", + "obligation_id": "shared-state-effects", + "positive_outcome": "passed" + }, + { + "evidence_refs": [ + "implementations/python/tests/test_participant_runtime_invariants.py::test_order_discipline_accepts_supported_order_claim_strengths", + "implementations/python/tests/test_participant_runtime_invariants.py::test_order_discipline_rejects_wall_clock_causality" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Rejecting timestamp-only causality does not supply counterfactual proof." + ], + "negative_outcome": "passed", + "obligation_id": "ordering-before-causality", + "positive_outcome": "passed" + }, + { + "evidence_refs": [ + "implementations/python/tests/test_sem_212_participant_attribution_semantics.py::test_attribution_edge_round_trips_on_terminal_observation", + "implementations/python/tests/test_sem_212_participant_attribution_semantics.py::test_timestamp_adjacency_cannot_be_reported_as_strong_causality" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Attribution labels disclose basis; they do not demonstrate necessity." + ], + "negative_outcome": "passed", + "obligation_id": "evidence-labeled-attribution", + "positive_outcome": "passed" + }, + { + "evidence_refs": [ + "implementations/python/tests/test_sem_215_participant_outcome_interpretation.py::test_outcome_interpretation_rule_parses_and_compiles_explicit_layers", + "implementations/python/tests/test_sem_215_participant_outcome_interpretation.py::test_local_action_success_does_not_imply_objective_success_without_rule_record" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "The fixtures establish layer separation, not outcome validity in every realization." + ], + "negative_outcome": "passed", + "obligation_id": "participant-local-outcome-separation", + "positive_outcome": "passed" + }, + { + "evidence_refs": [ + "implementations/python/tests/test_realization_honesty_conformance.py::test_constructive_envelope_runs_positive_and_negative_honesty_probes", + "implementations/python/tests/test_realization_honesty_conformance.py::test_only_native_live_can_support_native_conformance" + ], + "execution_id": "issue-1355-execution-v53", + "limitations": [ + "Reference conformance evidence remains bounded to declared realization profiles." + ], + "negative_outcome": "passed", + "obligation_id": "realization-profile-honesty", + "positive_outcome": "passed" + } + ], + "protocol_revision": "2.0.0", + "raes_revision": "d9c4f3d6c35b70f1fc822eeae6781352b4d45c23", + "source_state": { + "base_revision": "d9c4f3d6c35b70f1fc822eeae6781352b4d45c23", + "checkout_state": "modified", + "implementation_digest": "139b3dc25bf1a07690c7f1c63b619c12647ae1eda1fe344e98524005a0d56158", + "profile": "python-reference-source/v2" + }, + "versions": { + "python": "3.12.3", + "raes": "5.0.0", + "z3_engine": "4.16.0", + "z3_solver": "4.16.0.0" + } +} diff --git a/docs/research/formal-semantic-validation/index.md b/docs/research/formal-semantic-validation/index.md index 7990e3b9f..dc9922941 100644 --- a/docs/research/formal-semantic-validation/index.md +++ b/docs/research/formal-semantic-validation/index.md @@ -336,7 +336,7 @@ outcomes and claim limits, recording the positive successor's changed result digest; the dangling-reference diagnostic remains identical. It establishes no autonomy threshold, authority grant, or realized attribution. -Current validation requires explicit release 53.0.0, rejects unsupported future +Current validation requires explicit release 54.0.0, rejects unsupported future or duplicate revisions, and never accepts an old/new output-digest pair as a substitute for replay. Historical releases (including the issue-826 supplement) undergo pin, shape, control, and internal-join checks without executing current @@ -494,3 +494,9 @@ Release 53.0.0 replays the retained controls on the source combining issue #1360 backend-operation contracts with issue #1358 denied-egress handling in [`execution-snapshot-v52.json`](execution-snapshot-v52.json) and [`analysis-v52.json`](analysis-v52.json). Earlier captures retain their source identities. + +Release 54.0.0 replays the retained formal controls against issue #1355's mixed +mapping, time, and handoff implementation in +[`execution-snapshot-v53.json`](execution-snapshot-v53.json) and +[`analysis-v53.json`](analysis-v53.json). Mixed runtime effects and recovery +remain covered by dedicated runtime tests, outside this formal corpus. diff --git a/docs/research/specification-coverage/analysis-v53.json b/docs/research/specification-coverage/analysis-v53.json new file mode 100644 index 000000000..fd59ee1f8 --- /dev/null +++ b/docs/research/specification-coverage/analysis-v53.json @@ -0,0 +1,104 @@ +{ + "analysis_id": "issue-1355-specification-coverage-v53", + "backend_leakage": [], + "claim": { + "allowed_evidence": [ + "pinned source metadata and bounded paraphrases", + "production parser, semantic, instantiation, admission, compiler, contract, and profile results", + "exact artifact digests and typed pointers", + "documented missing-concept and backend-specific dispositions" + ], + "claim_id": "raes-standardized-configurable-specification-coverage", + "disallowed_evidence": [ + "field-count or schema breadth alone", + "the existing scenario stress corpus as the representative request corpus", + "free-form metadata as typed coverage", + "backend-private interpretation", + "post-hoc removal or repair of falsifying concepts" + ], + "evidence_artifacts": [ + "docs/research/specification-coverage/protocol-v1.json", + "docs/research/specification-coverage/execution-snapshot-v53.json", + "docs/research/specification-coverage/analysis-v53.json" + ], + "falsification_protocol": "docs/research/specification-coverage/protocol-v1.json", + "objective_fail_criteria": "A load-bearing concept is missing or lossy, an applicable stage fails, or backend vocabulary is required in core SDL while the result claims success.", + "objective_pass_criteria": "Every load-bearing concept passes at every owning stage, backend-specific mechanics stay outside core SDL, and no requested concept is silently lost.", + "statement": "RAES provides a standardized configurable portable specification surface for the preregistered representative cyber-agent evaluation environment requirements without backend vocabulary in core SDL.", + "threats_to_validity": [ + "The representative corpus contains four source strata and sixteen atomic concepts rather than every cyber-range requirement.", + "The reference processor and repository fixtures are not independent backend implementations.", + "No live range, simulator federation, or participant execution was part of this offline specification-coverage test." + ] + }, + "classification_counts": { + "deliberately-backend-specific": 1, + "directly-expressible": 10, + "missing": 3, + "profile-or-manifest-constraint": 2 + }, + "evidence_status": "partial", + "execution_status": "complete", + "generated_at": "2026-09-26", + "limitations": [ + "This result demonstrates bounded specification coverage, not universal cyber-range coverage, usability, adoption, backend substitution, or behavioral equivalence.", + "The three missing concepts are evidence, not implementation tasks within this snapshot.", + "The retained protocol does not test recursive realization or plan-level profile semantics; this release only re-establishes its original bounded coverage result against the current implementation.", + "The retained protocol does not test evidence-requirement refinement lineage; the dedicated EXP-731 regression suite covers that production boundary.", + "Authoring-adapter transport behavior is outside this retained protocol.", + "Reviewed OCI mirror and pre-seed admission is covered by its own regression suites and the development artifact policy gate, not a new claim in this preregistered matrix.", + "Operational recovery observation and startup reconciliation are covered by their API-404 regression suite, not a new claim in this preregistered matrix.", + "Store ownership, immutable runtime scope, and provider shutdown ordering are covered by the API-404 CP-5 regression suite, not by this retained specification-coverage protocol.", + "Mixed/staged trial compilation and admission are covered by issue #1015 regression tests, not by this retained specification-coverage corpus; no live mixed-runtime result is claimed.", + "Issue #1186 control-plane recovery operations are covered by their runtime regression suite, not by this retained specification-coverage corpus.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 control-plane profile declarations are covered by their dedicated runtime suite, not promoted to new claims by the retained language corpus.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Participant-local outcome state is verified by the ACT-618 tests; this retained corpus makes no additional outcome-state claim.", + "Backend operation supervision contracts are covered by issue #1360 contract tests; this retained offline corpus establishes no live backend supervision or recovery guarantee.", + "This capture replays the merged issue #1360 and #1357 source; the protocol makes no live backend execution or supervision claim.", + "This capture replays the merged issue #1360 and #1358 source; the protocol makes no live backend execution or supervision claim.", + "This capture binds issue #1355 executable mixed mapping and time source to the retained offline protocol; dedicated runtime tests establish its behavior, not this coverage matrix." + ], + "load_bearing_results": { + "failed": 0, + "missing": 0, + "passed": 10, + "total": 10 + }, + "plain_language_outcome": "The retained specification matrix replays explicit participant affiliations, objective ownership, and assignment using abstract action contracts. Classification counts and untested concepts are unchanged; no execution authority or live backend behavior is inferred.", + "protocol_revision": "1.0.0", + "request_results": [ + { + "concept_count": 6, + "failed_stage_count": 0, + "missing_count": 0, + "request_id": "survey-representative-range", + "status": "demonstrated" + }, + { + "concept_count": 5, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "cyborg-participant-evaluation", + "status": "partial" + }, + { + "concept_count": 3, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "vsdl-configurable-infrastructure", + "status": "partial" + }, + { + "concept_count": 2, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "cyber-dem-federation", + "status": "partial" + } + ], + "snapshot_id": "issue-1355-specification-coverage-v53", + "snapshot_sha256": "9d3374e6d7c038e9d9439d6b803d97ca189207118cf4223745a13e9f8e676051" +} diff --git a/docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1355-v53.json b/docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1355-v53.json new file mode 100644 index 000000000..ed0ba9f30 --- /dev/null +++ b/docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1355-v53.json @@ -0,0 +1,10 @@ +{ + "analysis_path": "docs/research/specification-coverage/analysis-v53.json", + "analysis_sha256": "3b5b0b0faf6909793c6658e90f99ac3866347be1b4b9730772839fcea3da6c16", + "bundle_id": "raes-standardized-specification-coverage", + "protocol_path": "docs/research/specification-coverage/protocol-v1.json", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "revision": "53.0.0", + "snapshot_path": "docs/research/specification-coverage/execution-snapshot-v53.json", + "snapshot_sha256": "997e0d0cd09c17b1e661ba787c21cdcc0d8a7009fda68915c2343d651274a9bb" +} diff --git a/docs/research/specification-coverage/execution-snapshot-v53.json b/docs/research/specification-coverage/execution-snapshot-v53.json new file mode 100644 index 000000000..8d59d4dab --- /dev/null +++ b/docs/research/specification-coverage/execution-snapshot-v53.json @@ -0,0 +1,701 @@ +{ + "artifacts": [ + { + "artifact_id": "enterprise-participant-sdl", + "kind": "sdl", + "path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "sha256": "f7a8897beec243e188ee081975006fad32725f469f267db6e75a1e1cf5727032", + "validator": "raes parse, semantic, instantiation/admission, and compiler pipeline" + }, + { + "artifact_id": "port-range-sdl", + "kind": "sdl", + "path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "sha256": "0d5497ec946b863e6985284ec487dde7d7f6bf710a985be51401ac0e5e79dc4f", + "validator": "raes parse, semantic, instantiation/admission, and compiler pipeline" + }, + { + "artifact_id": "experiment-task-contract", + "kind": "experiment-task", + "path": "contracts/fixtures/experiment-core/experiment-task-v1/valid/reference.json", + "sha256": "f3edf713ac6af26bad609136851c6dd434bfb87ce919a2d8c4414c1035deeafc", + "validator": "raes_contracts.contracts.ExperimentTaskModel" + }, + { + "artifact_id": "apparatus-context-contract", + "kind": "experiment-apparatus-context", + "path": "contracts/fixtures/experiment-core/experiment-apparatus-context-v1/valid/reference.json", + "sha256": "e6fa559c5e961f0aab448d0f70dead24aa74fa8ba5f20e1b72f88e11473c9299", + "validator": "raes_contracts.contracts.ExperimentApparatusContextModel" + }, + { + "artifact_id": "backend-profile", + "kind": "backend-profile", + "path": "contracts/profiles/backend/orchestration-capable.json", + "sha256": "f70b8505a5c0055416db86c533e2e5bf08b11e5a514f076223b6d6c36215a092", + "validator": "raes_contracts.backend_profiles.BackendProfileModel" + }, + { + "artifact_id": "known-limitations", + "kind": "documentation", + "path": "docs/explain/sdl/limitations.md", + "sha256": "489eeab3ce682627682311581eb98af9abb9ff42a437145af266eefb71dc7fc4", + "validator": "documentation evidence only" + } + ], + "baseline": { + "release_revision": "1.1.0", + "release_sha256": "4020a1d56c7fe2831cec59ea64a12bbda9d38ccd94f93b916dd90f1a28f17fcb" + }, + "captured_at": "2026-09-27T06:49:00.051312+00:00", + "concept_results": [ + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "range-topology", + "rationale": "SDL nodes and infrastructure own host, network, link, and dependency meaning; the compiler emits canonical node deployment addresses.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed VM declaration.", + "outcome": "passed", + "pointer": "/nodes/shipping-portal", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Links and dependencies resolved.", + "outcome": "passed", + "pointer": "/infrastructure/shipping-portal", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Published instantiated shape admitted.", + "outcome": "passed", + "pointer": "/nodes/shipping-portal", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical deployment address retained.", + "outcome": "passed", + "pointer": "/node_deployments/provision.node.shipping-portal", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/nodes/shipping-portal" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "exercise-roles", + "rationale": "SDL entity roles own exercise responsibility without becoming control-plane identity or authorization.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed red role.", + "outcome": "passed", + "pointer": "/entities/enterprise-participant/role", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Entity references validated.", + "outcome": "passed", + "pointer": "/entities/enterprise-participant", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Role retained after instantiation.", + "outcome": "passed", + "pointer": "/entities/enterprise-participant/role", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Role retained in entity specification.", + "outcome": "passed", + "pointer": "/entity_specs/enterprise-participant/role", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/entities/enterprise-participant/role" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "evaluation-objectives", + "rationale": "SDL objectives own organization ownership, participant assignment, targets, windows, and assertion-based success; measures remain experiment contracts.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed objective declaration.", + "outcome": "passed", + "pointer": "/objectives/demonstrate-handoff", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Owner, participant assignment, targets, assertions, and workflow refs resolved.", + "outcome": "passed", + "pointer": "/objectives/demonstrate-handoff/success", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Objective retained in admitted artifact.", + "outcome": "passed", + "pointer": "/objectives/demonstrate-handoff", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical objective address retained.", + "outcome": "passed", + "pointer": "/objectives/evaluation.objective.demonstrate-handoff", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/objectives/demonstrate-handoff" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "control-workflows", + "rationale": "SDL workflows own the portable control graph and compile to canonical orchestration state contracts.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed control graph.", + "outcome": "passed", + "pointer": "/workflows/yard-recovery", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Step graph and objective refs validated.", + "outcome": "passed", + "pointer": "/workflows/yard-recovery/steps", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Workflow retained after instantiation.", + "outcome": "passed", + "pointer": "/workflows/yard-recovery", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical control graph retained.", + "outcome": "passed", + "pointer": "/workflows/orchestration.workflow.yard-recovery", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/workflows/yard-recovery" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "authored-evidence-expectations", + "rationale": "SDL evidence requirements own portable capture intent and remain distinct from evidence records and measures.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed capture obligation.", + "outcome": "passed", + "pointer": "/evidence_requirements/objective-truth-evidence", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Source refs and bindings validated.", + "outcome": "passed", + "pointer": "/evidence_requirements/objective-truth-evidence", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Evidence intent retained in admitted artifact.", + "outcome": "passed", + "pointer": "/evidence_requirements/objective-truth-evidence", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + } + ], + "typed_pointer": "/evidence_requirements/objective-truth-evidence" + }, + { + "backend_support": "profile-bound", + "backend_vocabulary_occurrences": [], + "classification": "profile-or-manifest-constraint", + "completeness_disposition": "implemented", + "concept_id": "apparatus-selection-constraints", + "rationale": "The experiment task contract binds processor/backend identities, manifest refs, and capabilities outside SDL.", + "stage_results": [ + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-task-v1/valid/reference.json", + "diagnostic_codes": [], + "note": "Closed ExperimentTaskModel validated.", + "outcome": "passed", + "pointer": "/apparatus_constraints/allowed_backend_refs/0", + "stage_id": "contract", + "validation_strength": "contract" + } + ], + "typed_pointer": "/apparatus_constraints/allowed_backend_refs/0" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "participant-agent", + "rationale": "SDL agents own participant entity, knowledge, actions, observation boundaries, and operating scope.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed participant declaration.", + "outcome": "passed", + "pointer": "/agents/participant-agent", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Participant refs and scope validated.", + "outcome": "passed", + "pointer": "/agents/participant-agent/observation_boundaries", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Participant retained in admitted artifact.", + "outcome": "passed", + "pointer": "/agents/participant-agent", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Compiled participant scope retained.", + "outcome": "passed", + "pointer": "/agent_specs/participant-agent", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/agents/participant-agent" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "participant-action-contract", + "rationale": "The action contract declares portable preconditions, effects, observations, evidence, and failure classes without a runner command.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed action contract.", + "outcome": "passed", + "pointer": "/action_contracts/probe-customer-portal-login", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Action refs and evidence bindings validated.", + "outcome": "passed", + "pointer": "/action_contracts/probe-customer-portal-login/effects", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Action retained in admitted artifact.", + "outcome": "passed", + "pointer": "/action_contracts/probe-customer-portal-login", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical action address retained.", + "outcome": "passed", + "pointer": "/action_contracts/participant.action-contract.probe-customer-portal-login", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/action_contracts/probe-customer-portal-login" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "participant-observation-boundary", + "rationale": "The observation boundary separately declares visible, hidden, and evidence-only information with transition rules.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed observation boundary.", + "outcome": "passed", + "pointer": "/observation_boundaries/participant-view", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Information refs and transitions validated.", + "outcome": "passed", + "pointer": "/observation_boundaries/participant-view/view_rules", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Boundary retained in admitted artifact.", + "outcome": "passed", + "pointer": "/observation_boundaries/participant-view", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical boundary address retained.", + "outcome": "passed", + "pointer": "/observation_boundaries/participant.observation-boundary.participant-view", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/observation_boundaries/participant-view" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "evaluation-measure", + "rationale": "ExperimentTaskModel owns metric construct, unit, direction, aggregation, and evidence requirements outside SDL objectives.", + "stage_results": [ + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-task-v1/valid/reference.json", + "diagnostic_codes": [], + "note": "Closed task contract validated.", + "outcome": "passed", + "pointer": "/evaluation_protocol/metric_definitions/foothold-achieved", + "stage_id": "contract", + "validation_strength": "contract" + } + ], + "typed_pointer": "/evaluation_protocol/metric_definitions/foothold-achieved" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "missing", + "completeness_disposition": "documented-gap", + "concept_id": "participant-tool-affordance", + "rationale": "This preregistered matrix has no tested carrier for participant tool affordances. The retained missing classification records missing coverage evidence, not the absence of current participant-behavior capabilities.", + "stage_results": [ + { + "artifact_path": "docs/explain/sdl/limitations.md", + "diagnostic_codes": [], + "note": "The preregistered carrier slot was not run; metadata does not substitute for a typed coverage test.", + "outcome": "not_run", + "pointer": null, + "stage_id": "authored", + "validation_strength": "not-applicable" + } + ], + "typed_pointer": null + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "resource-constrained-topology", + "rationale": "SDL node resources and infrastructure dependencies express portable resource intent without provider resource identifiers.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed CPU and memory declaration.", + "outcome": "passed", + "pointer": "/nodes/shipping-portal/resources", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Resource-bearing topology validated.", + "outcome": "passed", + "pointer": "/infrastructure/shipping-portal", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Constraints retained in admitted artifact.", + "outcome": "passed", + "pointer": "/nodes/shipping-portal/resources", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Deployment specification retains resource intent.", + "outcome": "passed", + "pointer": "/node_deployments/provision.node.shipping-portal", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/nodes/shipping-portal/resources" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "missing", + "completeness_disposition": "documented-gap", + "concept_id": "formal-constraint-satisfiability", + "rationale": "This coverage matrix did not exercise a solver-backed carrier. The separate formal-semantic-validation release demonstrates its bounded finite-domain profile; that result is not silently imported into this protocol's missing carrier slot.", + "stage_results": [ + { + "artifact_path": "docs/explain/sdl/limitations.md", + "diagnostic_codes": [], + "note": "No coverage-carrier execution was performed here; independent solver evidence does not change this preregistered denominator.", + "outcome": "not_run", + "pointer": null, + "stage_id": "semantic", + "validation_strength": "not-applicable" + } + ], + "typed_pointer": null + }, + { + "backend_support": "profile-bound", + "backend_vocabulary_occurrences": [ + { + "allowed": true, + "artifact_path": "source:vsdl-paper", + "pointer": "source sections 4-5", + "reason": "Legitimate VSDL realization vocabulary, not RAES core SDL structure.", + "term": "OpenStack/Terraform/Packer" + } + ], + "classification": "deliberately-backend-specific", + "completeness_disposition": "external", + "concept_id": "provider-specific-provisioning", + "rationale": "Provider image selection and provisioning engines are realization mechanics and therefore remain outside core SDL.", + "stage_results": [ + { + "artifact_path": "contracts/profiles/backend/orchestration-capable.json", + "diagnostic_codes": [], + "note": "The portable boundary requires backend contracts; it does not standardize a provider engine.", + "outcome": "not_applicable", + "pointer": "/required_contracts", + "stage_id": "realization-disclosure", + "validation_strength": "profile" + } + ], + "typed_pointer": null + }, + { + "backend_support": "profile-bound", + "backend_vocabulary_occurrences": [], + "classification": "profile-or-manifest-constraint", + "completeness_disposition": "implemented", + "concept_id": "apparatus-clock-context", + "rationale": "ExperimentApparatusContextModel records clock authority, time domain, and synchronization as apparatus facts outside scenario meaning.", + "stage_results": [ + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-apparatus-context-v1/valid/reference.json", + "diagnostic_codes": [], + "note": "Closed apparatus context contract validated.", + "outcome": "passed", + "pointer": "/clocks/0", + "stage_id": "contract", + "validation_strength": "contract" + } + ], + "typed_pointer": "/clocks/0" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "missing", + "completeness_disposition": "documented-gap", + "concept_id": "federated-object-event-exchange", + "rationale": "The federated cyber object/event exchange carrier was not exercised by this preregistered matrix. Runtime event internals are not treated as equivalent evidence.", + "stage_results": [ + { + "artifact_path": "docs/explain/sdl/limitations.md", + "diagnostic_codes": [], + "note": "The missing coverage-carrier test is recorded explicitly, without inferring an ecosystem-wide capability absence.", + "outcome": "not_run", + "pointer": null, + "stage_id": "contract", + "validation_strength": "not-applicable" + } + ], + "typed_pointer": null + } + ], + "deviations": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "baseline_sha256": "54ba1a60220e27a55da9cd2a407d7d3ab836fa54460d0b0c6cad87c2e744ddbb", + "rationale": "Migrate participant affiliations and explicit objective assignment, retaining organizational intent and portable action-contract declarations without granting execution authority.", + "retest_sha256": "f7a8897beec243e188ee081975006fad32725f469f267db6e75a1e1cf5727032" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "baseline_sha256": "a27c7a64e0c5c618fadaccafdf1a4e71600170a8b77b983190822b5141f00dec", + "rationale": "Migrate participant affiliations and explicit objective assignment, retaining organizational intent and portable action-contract declarations without granting execution authority.", + "retest_sha256": "0d5497ec946b863e6985284ec487dde7d7f6bf710a985be51401ac0e5e79dc4f" + }, + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-task-v1/valid/reference.json", + "baseline_sha256": "21952a752f4e8581a9fc3b872e4bc308150548170d38bcfc83dbbe35ff5e0b9f", + "rationale": "Replay the retained preregistered artifact against the current evidence-provenance validation implementation.", + "retest_sha256": "f3edf713ac6af26bad609136851c6dd434bfb87ce919a2d8c4414c1035deeafc" + }, + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-apparatus-context-v1/valid/reference.json", + "baseline_sha256": "9536d897a09cbc6920e667e4f8f9371e51307aa0b3b5ff3c7de682dd783420ab", + "rationale": "Replay the retained preregistered artifact against the current evidence-provenance validation implementation.", + "retest_sha256": "e6fa559c5e961f0aab448d0f70dead24aa74fa8ba5f20e1b72f88e11473c9299" + }, + { + "artifact_path": "docs/explain/sdl/limitations.md", + "baseline_sha256": "129cf17810aad4c51988bc872e28fe43ae95019a80053c42d800ff7e2b9cc93e", + "rationale": "Correct historical mandatory-profile guidance after issue #1207; retain the preregistered missing-concept classifications and coverage limits.", + "retest_sha256": "489eeab3ce682627682311581eb98af9abb9ff42a437145af266eefb71dc7fc4" + } + ], + "execution_status": "complete", + "implementation_surfaces": [ + { + "content_sha256": "9f7edff3ddc324cec333556ce8044c137f87c978a8c38f20f92971259625c43e", + "path": "implementations/python/packages/raes_contracts", + "surface_id": "contract-models" + }, + { + "content_sha256": "4999b8adf294f364a758bc9cf78816d5da9eae1c263ae678eabe4d0e2c82dec6", + "path": "implementations/python/packages/raes_processor", + "surface_id": "processor-pipeline" + }, + { + "content_sha256": "9ecd780448b054693503bab246120a1a2bb49a43016d0b9c27c5284ba609833f", + "path": "implementations/python/packages/raes", + "surface_id": "sdl-pipeline" + } + ], + "limitations": [ + "The execution validates the pinned reference implementation and published contracts, not an independent backend.", + "Repository-owned examples are exact execution artifacts but are not themselves the literature-derived request corpus; the protocol's requests and concepts are.", + "No live range, participant, simulator federation, or provider provisioning engine was executed.", + "Missing concepts remain frozen in this snapshot and require separately scoped product work before a later rerun.", + "This capture replays the retained protocol after EXP-732 run, apparatus, measurement-channel, and augmentation-producer provenance validation; it adds no independent backend or universal provenance assurance claim.", + "Materialization attestation is covered by its dedicated regression suite, not a new claim in this preregistered matrix.", + "This capture refreshes the corrected runtime limitations prose for issue #959; the protocol, coverage classifications and implementation source are unchanged.", + "This capture replays open-by-default augmentation scope integrated with the EXP-731 evidence refinements after composition type refinement; it does not evaluate native backend scope enforcement or broaden the preregistered coverage claims.", + "This capture replays the retained protocol after merging ACT-612 participant relationships with open-by-default augmentation scope; it adds no claim of realized participant relationships or native backend scope enforcement.", + "This capture replays issue #1299 partial listener descriptions on the integrated source state; endpoint completeness and backend admission remain outside this protocol's claims.", + "This capture also binds authoring-adapter semantic conformance to the integrated source; adapter transport behavior remains outside this protocol's claims.", + "Reviewed OCI mirror and pre-seed admission is covered by its own regression suites and the development artifact policy gate, not a new claim in this preregistered matrix.", + "This capture binds issue #1297 service-manager identity, native-name, and explicitly selected systemd-state contract changes to the integrated source. It exercises no live service manager and adds no backend-execution claim.", + "This capture replays the retained specification-coverage protocol after API-404 startup reconciliation added an operational recovery-observation contract. It does not evaluate crash recovery, classify provider effects, or broaden EXP-715 experiment-observation claims.", + "This capture binds API-404 single-owner store admission and immutable target/run scope to the integrated source. The retained offline protocol does not exercise process leases, SQLite lifecycle ordering, or crash recovery.", + "This capture binds issue #1015 deterministic mixed and staged trial admission to the integrated source. The retained offline language corpus does not execute mixed runtimes, phase transitions, backend handoff, or scheduler-driven realization.", + "This replay binds issue #1186 offline control-plane maintenance, readiness, and bounded audit code to the integrated source. The retained language corpus does not execute store recovery, HTTP health behavior, or audit redaction.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 control-plane profile declarations are covered by their dedicated runtime suite, not promoted to new claims by the retained language corpus.", + "Issue #1016 mixed-runtime coordination is covered by its dedicated runtime suite. The retained language corpus does not execute mixed providers or establish backend-native realization, multi-controller coordination, IFC, or equivalence.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Issue #1355 mixed mapping, time coordination, handoff, and outcome execution is covered by its dedicated runtime tests; this retained offline language corpus does not execute mixed providers or establish live backend fidelity." + ], + "protocol_revision": "1.0.0", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "raes_revision": "d9c4f3d6c35b70f1fc822eeae6781352b4d45c23", + "snapshot_id": "issue-1355-specification-coverage-v53", + "snapshot_revision": "53.0.0", + "source_state": { + "base_revision": "d9c4f3d6c35b70f1fc822eeae6781352b4d45c23", + "checkout_state": "modified", + "implementation_digest": "139b3dc25bf1a07690c7f1c63b619c12647ae1eda1fe344e98524005a0d56158", + "profile": "python-reference-source/v2" + } +} diff --git a/docs/research/specification-coverage/index.md b/docs/research/specification-coverage/index.md index 06740a7a3..a2933ce17 100644 --- a/docs/research/specification-coverage/index.md +++ b/docs/research/specification-coverage/index.md @@ -292,7 +292,7 @@ the port scenario. Historical captures and archived example bytes are retained. The matrix classifications and untested concepts are unchanged; no execution authority, successful action, or live backend fidelity is inferred. -Current validation requires release 52.0.0 and rejects duplicate or unsupported +Current validation requires release 53.0.0 and rejects duplicate or unsupported future revisions. It executes current artifacts, requires exact source and package hashes, and checks all passing stage pointers. `source_state` discloses the base Git commit, modified checkout state, and exact implementation digest; @@ -430,3 +430,9 @@ Release 52.0.0 replays the retained protocol on the source combining issue #1360 backend-operation contracts with issue #1358 denied-egress handling in [`execution-snapshot-v52.json`](execution-snapshot-v52.json) and [`analysis-v52.json`](analysis-v52.json). Earlier captures retain their source identities. + +Release 53.0.0 replays the retained offline protocol against issue #1355's +mixed mapping, time, and handoff implementation in +[`execution-snapshot-v53.json`](execution-snapshot-v53.json) and +[`analysis-v53.json`](analysis-v53.json). Mixed runtime effects and recovery +remain covered by dedicated runtime tests, outside this language corpus. diff --git a/implementations/python/packages/raes_runtime/control_plane.py b/implementations/python/packages/raes_runtime/control_plane.py index 5f1a4a25e..d30b1fe68 100644 --- a/implementations/python/packages/raes_runtime/control_plane.py +++ b/implementations/python/packages/raes_runtime/control_plane.py @@ -70,11 +70,11 @@ from .control_plane_submission import control_plane_plan_diagnostics from .control_plane_workflow_control import WorkflowControlMixin from .mixed_runtime import MixedRuntimeMixin +from .mixed_runtime_recovery import validate_restored_mixed_crossing_cut from .observation_execution import ObservationExecution from .observation_results import observation_execution_from_payload from .operational_apparatus import operational_apparatus_summary from .participant_control import ParticipantControlMixin -from .participant_crossing_mediation import validate_persisted_crossing_history from .participant_information_state_validation import require_participant_information_state_snapshot from .participant_retrieval import ParticipantRetrievalMixin from .registry import RuntimeTarget as _RuntimeTarget @@ -198,7 +198,7 @@ def _restore_persisted_state(self, config: ControlPlaneConfiguration) -> None: if self._snapshot.participant_crossing_history: if config.crossing_policy_resolver is None: raise ValueError("persisted participant crossing history requires a policy resolver") - validate_persisted_crossing_history(self._snapshot, config.crossing_policy_resolver) + validate_restored_mixed_crossing_cut(self, config.crossing_policy_resolver) @property def _snapshot(self) -> RuntimeSnapshot: diff --git a/implementations/python/packages/raes_runtime/control_plane_recovery.py b/implementations/python/packages/raes_runtime/control_plane_recovery.py index c4de9c682..8a3c99e76 100644 --- a/implementations/python/packages/raes_runtime/control_plane_recovery.py +++ b/implementations/python/packages/raes_runtime/control_plane_recovery.py @@ -5,7 +5,6 @@ from collections.abc import Mapping from copy import deepcopy from dataclasses import replace -from enum import Enum from uuid import uuid4 from raes_backend_protocols.recovery_observation import ( @@ -34,17 +33,13 @@ legacy_operation_request_commitment, operation_admission_context, ) +from .control_plane_resolution_records import IndeterminateResolutionDisposition, is_valid_resolution_child from .control_plane_store import ( ControlPlaneOperationRecord, NewClaimRejected, TerminalCommitMode, ) - - -class IndeterminateResolutionDisposition(str, Enum): - """Closed administrative acceptance of the currently stored state cut.""" - - ACCEPT_CURRENT_SNAPSHOT = "accept-current-snapshot" +from .mixed_runtime_recovery import require_resolvable_mixed_action_cut, requires_mixed_stage_reconciliation class RuntimeRecoveryMixin: @@ -174,6 +169,8 @@ def _observe_running_record( record: ControlPlaneOperationRecord, ) -> tuple[RecoveryEffectClassification, ApplyResult | None]: kind = record.status.context.operation_kind + if requires_mixed_stage_reconciliation(control_plane, record): + return RecoveryEffectClassification.INDETERMINATE, None if kind is OperationKind.COMPOSITION_PHASE: observation = (RecoveryEffectClassification.EFFECT_ABSENT, None) else: @@ -333,7 +330,7 @@ def unresolved_indeterminate_operation_ids_from_records( for record in records.values() if (parent_id := record.status.context.parent_operation_id) is not None and (parent := records.get(parent_id)) is not None - and _is_valid_resolution_child(parent, record) + and is_valid_resolution_child(parent, record) } return tuple( sorted( @@ -375,6 +372,7 @@ def resolve_indeterminate_operation( _authorize_resolution(control_plane, parent, context, identity) if parent.status.state is not OperationState.INDETERMINATE: raise ValueError("resolution parent must be indeterminate") + require_resolvable_mixed_action_cut(control_plane, parent) if not idempotency_key: raise ValueError("resolution requires an idempotency key") if idempotency_key == parent.idempotency_key: @@ -465,26 +463,6 @@ def _authorize_resolution( raise PermissionError("indeterminate resolution is forbidden") -def _is_valid_resolution_child( - parent: ControlPlaneOperationRecord, - child: ControlPlaneOperationRecord, -) -> bool: - context = child.status.context - return ( - parent.status.state is OperationState.INDETERMINATE - and child.status.state is OperationState.SUCCEEDED - and context.operation_kind is OperationKind.INDETERMINATE_RESOLUTION - and context.parent_operation_id == parent.receipt.operation_id - and context.target_scope == parent.status.context.target_scope - and context.run_scope == parent.status.context.run_scope - and "role:operator" in context.authorization_scope - and bool(child.idempotency_key) - and child.idempotency_key != parent.idempotency_key - and child.result_payload - == {"resolution_disposition": IndeterminateResolutionDisposition.ACCEPT_CURRENT_SNAPSHOT.value} - ) - - __all__ = ( "IndeterminateResolutionDisposition", "RuntimeRecoveryMixin", diff --git a/implementations/python/packages/raes_runtime/control_plane_resolution_records.py b/implementations/python/packages/raes_runtime/control_plane_resolution_records.py new file mode 100644 index 000000000..3c2fee5d1 --- /dev/null +++ b/implementations/python/packages/raes_runtime/control_plane_resolution_records.py @@ -0,0 +1,45 @@ +"""Durable classification of linked administrative resolution records.""" + +from __future__ import annotations + +from enum import Enum + +from raes_contracts.runtime_state import OperationKind, OperationState + +from .control_plane_store import ControlPlaneOperationRecord +from .mixed_runtime_recovery import has_mixed_resolution_cut + + +class IndeterminateResolutionDisposition(str, Enum): + """Closed administrative acceptance of the currently stored state cut.""" + + ACCEPT_CURRENT_SNAPSHOT = "accept-current-snapshot" + + +def is_valid_resolution_child( + parent: ControlPlaneOperationRecord, + child: ControlPlaneOperationRecord, +) -> bool: + """Recognize a child only when it can safely discharge its parent.""" + + context = child.status.context + same_scope = (context.target_scope, context.run_scope) == ( + parent.status.context.target_scope, + parent.status.context.run_scope, + ) + return ( + not has_mixed_resolution_cut(parent) + and parent.status.state is OperationState.INDETERMINATE + and child.status.state is OperationState.SUCCEEDED + and context.operation_kind is OperationKind.INDETERMINATE_RESOLUTION + and context.parent_operation_id == parent.receipt.operation_id + and same_scope + and "role:operator" in context.authorization_scope + and bool(child.idempotency_key) + and child.idempotency_key != parent.idempotency_key + and child.result_payload + == {"resolution_disposition": IndeterminateResolutionDisposition.ACCEPT_CURRENT_SNAPSHOT.value} + ) + + +__all__ = ("IndeterminateResolutionDisposition", "is_valid_resolution_child") diff --git a/implementations/python/packages/raes_runtime/control_plane_store.py b/implementations/python/packages/raes_runtime/control_plane_store.py index 89a176f3b..04008195b 100644 --- a/implementations/python/packages/raes_runtime/control_plane_store.py +++ b/implementations/python/packages/raes_runtime/control_plane_store.py @@ -4,6 +4,7 @@ from __future__ import annotations +from collections.abc import Iterable from dataclasses import dataclass, field from typing import Any, Literal, Protocol, runtime_checkable @@ -40,6 +41,43 @@ IdempotencyClaimIdentity = tuple[str, OperationKind, str] NewClaimBlock = Literal["current-state", "indeterminate", "stale-base-snapshot"] | None _MAX_IDEMPOTENCY_KEY_LENGTH = 256 +_MIXED_CLAIM_KINDS = frozenset( + {OperationKind.COMPOSITION_PHASE, OperationKind.PARTICIPANT_ACTION, OperationKind.PARTICIPANT_CROSSING} +) +_ACTIVE_CLAIM_STATES = frozenset({OperationState.ACCEPTED, OperationState.RUNNING, OperationState.INDETERMINATE}) + + +def mixed_claim_conflicts( + new: ControlPlaneOperationRecord, + existing_records: Iterable[ControlPlaneOperationRecord], +) -> bool: + """Serialize external mixed effects in one run at the store claim.""" + + context = new.status.context + if context.operation_kind not in _MIXED_CLAIM_KINDS: + return False + mixed_keys = { + key + for key in (*new.decision_history_heads, *new.result_history_heads) + if key.startswith("mixed_composition_history:") + } + if not mixed_keys: + return False + return any(_active_mixed_claim_overlaps(context, mixed_keys, existing) for existing in existing_records) + + +def _active_mixed_claim_overlaps( + context: OperationAdmissionContext, + mixed_keys: set[str], + existing: ControlPlaneOperationRecord, +) -> bool: + prior = existing.status.context + if (prior.target_scope, prior.run_scope) != (context.target_scope, context.run_scope): + return False + if prior.operation_kind not in _MIXED_CLAIM_KINDS or existing.status.state not in _ACTIVE_CLAIM_STATES: + return False + prior_keys = set(existing.decision_history_heads) | set(existing.result_history_heads) + return bool(mixed_keys.intersection(prior_keys)) @dataclass(frozen=True) diff --git a/implementations/python/packages/raes_runtime/control_plane_store_local_records.py b/implementations/python/packages/raes_runtime/control_plane_store_local_records.py index e66c6dcc2..03c02fdc0 100644 --- a/implementations/python/packages/raes_runtime/control_plane_store_local_records.py +++ b/implementations/python/packages/raes_runtime/control_plane_store_local_records.py @@ -12,6 +12,7 @@ _raise_new_claim_block, _require_operation_record_transition, _require_same_idempotency_replay, + mixed_claim_conflicts, require_idempotency_key, ) from .control_plane_store_local_codec import decode_payload as _decode_payload @@ -73,6 +74,8 @@ def claim_record( return existing if new_claim_blocked: _raise_new_claim_block(new_claim_blocked) + if mixed_claim_conflicts(record, self._load_records(connection).values()): + _raise_new_claim_block("current-state") existing = self._load_record(connection, record.receipt.operation_id) if _require_operation_record_transition(existing, record): self._upsert_record(connection, record) diff --git a/implementations/python/packages/raes_runtime/control_plane_store_memory.py b/implementations/python/packages/raes_runtime/control_plane_store_memory.py index bb4850881..03b46a75c 100644 --- a/implementations/python/packages/raes_runtime/control_plane_store_memory.py +++ b/implementations/python/packages/raes_runtime/control_plane_store_memory.py @@ -133,6 +133,8 @@ def claim_record( return existing if new_claim_blocked: _store._raise_new_claim_block(new_claim_blocked) + if _store.mixed_claim_conflicts(record, self._records.values()): + _store._raise_new_claim_block("current-state") self._save_record(record) return record diff --git a/implementations/python/packages/raes_runtime/mixed_runtime.py b/implementations/python/packages/raes_runtime/mixed_runtime.py index 19358ffef..24c33f72d 100644 --- a/implementations/python/packages/raes_runtime/mixed_runtime.py +++ b/implementations/python/packages/raes_runtime/mixed_runtime.py @@ -43,6 +43,8 @@ from .control_plane_operation_context import operation_admission_context from .control_plane_security import ControlPlaneIdentity from .control_plane_store import AuditEvent, ControlPlaneOperationRecord +from .mixed_runtime_edge import MixedEdgeExecutionBinding +from .mixed_runtime_handoff import MixedHandoffBinding from .registry import RuntimeTarget @@ -76,6 +78,8 @@ class MixedRuntimeBinding: context: MixedCompositionResolutionContext components: Mapping[str, MixedRuntimeComponent] transition_evaluators: Mapping[str, Callable[..., MixedPhaseTransitionEvaluation]] = field(default_factory=dict) + edge_bindings: Mapping[str, MixedEdgeExecutionBinding] = field(default_factory=dict) + handoff_bindings: Mapping[str, MixedHandoffBinding] = field(default_factory=dict) def __post_init__(self) -> None: plan = revalidate_admitted_trial_plan(self.plan) @@ -83,9 +87,79 @@ def __post_init__(self) -> None: validate_mixed_composition_context(self.profile, self.context, require_trial_admission=True) _require_bound_components(self.profile, self.components) _require_transition_evaluators(self.profile, self.transition_evaluators) + if set(self.edge_bindings) - set(self.profile.edges): + raise ValueError("mixed runtime edge bindings must name admitted edges") + if set(self.handoff_bindings) - set(self.profile.transitions): + raise ValueError("mixed runtime handoff bindings must name admitted transitions") + for transition_id, handoff in self.handoff_bindings.items(): + self._require_handoff_binding(transition_id, handoff) + for edge_id, installed in self.edge_bindings.items(): + self._require_edge_binding(edge_id, installed) object.__setattr__(self, "plan", plan) object.__setattr__(self, "components", MappingProxyType(dict(self.components))) object.__setattr__(self, "transition_evaluators", MappingProxyType(dict(self.transition_evaluators))) + object.__setattr__(self, "edge_bindings", MappingProxyType(dict(self.edge_bindings))) + object.__setattr__(self, "handoff_bindings", MappingProxyType(dict(self.handoff_bindings))) + + def _require_handoff_binding(self, transition_id: str, handoff: MixedHandoffBinding) -> None: + if not isinstance(handoff, MixedHandoffBinding): + raise TypeError("executable handoff must be a typed installed binding") + transition = self.profile.transitions[transition_id] + source = self.profile.phases[transition.source_phase_id] + target = self.profile.phases[transition.target_phase_id] + if {handoff.source_component_id, handoff.destination_component_id} - self.profile.components.keys(): + raise ValueError("executable handoff differs from admitted transition ownership") + ownership = ( + handoff.transition_id, + {handoff.source_component_id}, + {handoff.destination_component_id}, + handoff.source_owner_ref, + handoff.destination_owner_ref, + ) + admitted = ( + transition_id, + set(source.active_component_ids) - set(target.active_component_ids), + set(target.active_component_ids) - set(source.active_component_ids), + self.profile.components[handoff.source_component_id].native_ownership_ref, + self.profile.components[handoff.destination_component_id].native_ownership_ref, + ) + if ownership != admitted: + raise ValueError("executable handoff differs from admitted transition ownership") + time_model = self.context.time_models.get(handoff.time_model_ref) + if time_model is None: + raise ValueError("executable handoff time binding is unresolved") + if ( + self.context.time_model_digests.get(handoff.time_model_ref) != handoff.time_model_digest + or handoff.mapping_ref not in time_model.mappings + or handoff.source_clock_address not in time_model.clocks + or handoff.destination_clock_address not in time_model.clocks + ): + raise ValueError("executable handoff time binding is unresolved") + mapping = time_model.mappings[handoff.mapping_ref] + domains = (mapping.source_domain_address, mapping.target_domain_address) + clock_domains = ( + time_model.clocks[handoff.source_clock_address].time_domain_address, + time_model.clocks[handoff.destination_clock_address].time_domain_address, + ) + if domains != clock_domains: + raise ValueError("executable handoff clock mapping differs from admission") + + def _require_edge_binding(self, edge_id: str, installed: MixedEdgeExecutionBinding) -> None: + if not isinstance(installed, MixedEdgeExecutionBinding): + raise TypeError("executable edge binding must be a typed installed binding") + edge = self.profile.edges[edge_id] + if ( + installed.edge_id, + installed.bridge_ref, + installed.mapping_ref, + installed.mapping_loss_ref, + ) != ( + edge_id, + edge.routing_ref, + edge.time_binding.mapping_address, + edge.mapping_loss.limitation_ref, + ): + raise ValueError("executable edge binding differs from admitted edge") @property def entry(self) -> AdmittedTrialEntryModel: diff --git a/implementations/python/packages/raes_runtime/mixed_runtime_dispatch.py b/implementations/python/packages/raes_runtime/mixed_runtime_dispatch.py index 793d5f004..12a04688b 100644 --- a/implementations/python/packages/raes_runtime/mixed_runtime_dispatch.py +++ b/implementations/python/packages/raes_runtime/mixed_runtime_dispatch.py @@ -4,7 +4,6 @@ from collections.abc import Callable from dataclasses import dataclass -from typing import Literal from raes_contracts.contracts.mixed_composition import AllocationTargetKind, MixedCompositionAllocationModel from raes_contracts.contracts.mixed_runtime import ( @@ -12,16 +11,16 @@ MixedCompositionRuntimeStateModel, ) from raes_contracts.participant_binding import ParticipantActionAdmissionRequest -from raes_contracts.runtime_state import RuntimeSnapshot +from raes_contracts.runtime_state import ApplyResult, RuntimeSnapshot from .control_plane_security import ControlPlaneIdentity +from .mixed_runtime_edge import MixedEdgeExecutionCapture +from .mixed_runtime_edge_execution import _mapped_edge_method, _stage_readback_method from .mixed_runtime_state import append_runtime_events, runtime_state from .participant_crossing_mediation import PreparedParticipantCrossing +from .participant_flow_sink import ParticipantFlowSinkDecision from .registry import RuntimeTarget -_EventKind = Literal["result", "delivery", "observation", "weakening", "failure"] -_Disposition = Literal["committed", "succeeded", "failed"] - @dataclass(frozen=True) class PreparedMixedActionDispatch: @@ -32,6 +31,8 @@ class PreparedMixedActionDispatch: snapshot: RuntimeSnapshot expected_history_heads: dict[str, str | None] committed_history_heads: dict[str, str | None] + capture: MixedEdgeExecutionCapture | None = None + stage_readback: Callable[[ApplyResult], None] | None = None @dataclass(frozen=True) @@ -243,6 +244,7 @@ def prepare_mixed_action_dispatch( control_plane: object, request: ParticipantActionAdmissionRequest, crossing: PreparedParticipantCrossing, + sink_decision: ParticipantFlowSinkDecision | None, ) -> PreparedMixedActionDispatch | None: """Resolve and persist the exact provider decision before its effect call.""" @@ -254,11 +256,19 @@ def prepare_mixed_action_dispatch( allocation = _active_allocation(binding, state, "action-family", request.action_contract_address) _require_action_authority(participant, allocation, crossing, request, state) edge = _action_edge(binding, state, participant, allocation) - method = _action_method(binding, allocation) decision = crossing.decision if decision is None: raise ValueError("mixed action dispatch requires a committed crossing decision") + if edge is not None: + _require_edge_crossing_authority(edge, crossing, request, sink_decision) + method = _action_method(binding, allocation) operation_id = crossing.record.receipt.operation_id + capture = None + stage_readback = None + if edge is not None: + method, capture, stage_readback = _edge_action_dispatch( + binding, edge, request, allocation, method, operation_id + ) event_base = _runtime_event_fields( state, allocation_id=allocation.allocation_id, @@ -296,9 +306,75 @@ def prepare_mixed_action_dispatch( snapshot=snapshot, expected_history_heads=expected, committed_history_heads=committed, + capture=capture, + stage_readback=stage_readback, ) +def _edge_action_dispatch( + binding: object, + edge: object, + request: ParticipantActionAdmissionRequest, + allocation: MixedCompositionAllocationModel, + method: Callable[..., object], + operation_id: str, +) -> tuple[Callable[..., object], MixedEdgeExecutionCapture, Callable[[ApplyResult], None]]: + if edge.edge_id not in binding.edge_bindings: + raise ValueError("mixed action dispatch requires an executable edge binding") + installed = binding.edge_bindings[edge.edge_id] + if (installed.source_action_address, installed.destination_action_address) != ( + request.action_contract_address, + allocation.target_address, + ): + raise ValueError("mixed destination action differs from admitted policy and provider allocation") + capture = MixedEdgeExecutionCapture() + mapped = _mapped_edge_method(binding, edge, installed, method, operation_id, capture) + readback = _stage_readback_method(binding, edge, installed, request, operation_id, capture) + return mapped, capture, readback + + +def _require_edge_crossing_authority( + edge: object, + crossing: PreparedParticipantCrossing, + request: ParticipantActionAdmissionRequest, + sink_decision: ParticipantFlowSinkDecision | None, +) -> None: + """Join the admitted edge to the live crossing and final-sink cut.""" + + decision = crossing.decision + assert decision is not None + occurrence = decision.occurrence + expected_crossing = ( + crossing.governed_subject, + occurrence.subject, + crossing.intent.audience_scope_ref, + occurrence.audience_scope_ref, + occurrence.policy, + crossing.intent.controller_ref, + occurrence.controller_ref, + request.action_contract_address, + ) + admitted_crossing = ( + edge.crossing_subject, + edge.crossing_subject, + edge.audience_scope_ref, + edge.audience_scope_ref, + edge.policy, + edge.controller_ref, + edge.controller_ref, + crossing.intent.action_or_projection_ref, + ) + if ( + not isinstance(sink_decision, ParticipantFlowSinkDecision) + or not sink_decision.permitted + or not sink_decision.decision_id + or admitted_crossing != expected_crossing + or edge.authority_ref not in occurrence.authority_basis_refs + or edge.disclosure_authority_ref not in occurrence.authority_basis_refs + ): + raise ValueError("mixed edge differs from the authorized crossing or final-sink cut") + + def _require_action_authority( participant: MixedCompositionAllocationModel, allocation: MixedCompositionAllocationModel, @@ -352,59 +428,6 @@ def _action_method(binding: object, allocation: MixedCompositionAllocationModel) return method -def record_mixed_action_result( - control_plane: object, - snapshot: RuntimeSnapshot, - crossing: PreparedParticipantCrossing, - *, - success: bool, -) -> RuntimeSnapshot: - """Append the backend outcome without allowing it to rewrite the decision.""" - - binding = getattr(control_plane, "_mixed_runtime", None) - if binding is None: - return snapshot - state = runtime_state(binding, snapshot) - attempt = snapshot.mixed_composition_history[state.run_id][-1] - common = _runtime_event_fields( - state, - allocation_id=attempt.get("allocation_id"), - component_id=attempt.get("component_id"), - edge_id=attempt.get("edge_id"), - control_event_ref=attempt.get("control_event_ref"), - crossing_event_ref=attempt.get("crossing_event_ref"), - policy_decision_ref=attempt.get("policy_decision_ref"), - mapping_ref=attempt.get("mapping_ref"), - order_ref=str(attempt["order_ref"]), - mapping_loss_refs=list(attempt.get("mapping_loss_refs", [])), - evidence_refs=list(attempt.get("evidence_refs", [])), - ) - operation_id = crossing.record.receipt.operation_id - events: list[MixedCompositionRuntimeEventModel] = [] - - def append(kind: _EventKind, disposition: _Disposition) -> None: - predecessor = state.history_head if not events else events[-1].event_id - events.append( - MixedCompositionRuntimeEventModel( - event_id=f"composition:{operation_id}:{kind}", - event_kind=kind, - disposition=disposition, - predecessor_event_id=predecessor, - **common, - ) - ) - - append("result", "succeeded" if success else "failed") - if success: - append("delivery", "succeeded") - append("observation", "committed") - if common["mapping_loss_refs"]: - append("weakening", "committed") - else: - append("failure", "failed") - return append_runtime_events(binding, snapshot, state, events) - - def mixed_recovery_target(control_plane: object, operation_id: str) -> RuntimeTarget | None: """Recover the exact component from its durable pre-effect attempt fact.""" @@ -458,6 +481,5 @@ def _recovery_component( "mixed_policy_allocation", "prepare_mixed_action_dispatch", "prepare_mixed_lifecycle_dispatch", - "record_mixed_action_result", "record_mixed_lifecycle_result", ) diff --git a/implementations/python/packages/raes_runtime/mixed_runtime_edge.py b/implementations/python/packages/raes_runtime/mixed_runtime_edge.py new file mode 100644 index 000000000..5b3546e4c --- /dev/null +++ b/implementations/python/packages/raes_runtime/mixed_runtime_edge.py @@ -0,0 +1,142 @@ +"""Trusted executable bindings for admitted mixed-composition edges.""" + +from __future__ import annotations + +from collections.abc import Callable +from dataclasses import dataclass +from re import fullmatch +from typing import Literal + +from pydantic import Field, model_validator +from raes_contracts.addressing import require_compiled_address +from raes_contracts.contracts.base import ContractModel, NonEmptyString +from raes_contracts.contracts.time_model import TimeCoordinateModel + + +class MixedTimeCoordinationEvidence(ContractModel): + """Correlated service grant checked against live time-runtime readback.""" + + operation_id: NonEmptyString + mapping_ref: NonEmptyString + ordering_basis: NonEmptyString + order_ref: NonEmptyString + comparison: Literal["ordered", "incomparable"] + source_coordinate: TimeCoordinateModel + destination_coordinate: TimeCoordinateModel + mapping_evidence_refs: list[NonEmptyString] = Field(min_length=1, max_length=64) + timing_evidence_refs: list[NonEmptyString] = Field(min_length=1, max_length=64) + + +class MixedBridgeExecutionEvidence(ContractModel): + """Separate execution, destination delivery, and audience readback facts.""" + + operation_id: NonEmptyString + bridge_ref: NonEmptyString + bridge_version: NonEmptyString + bridge_digest: NonEmptyString + source_action_address: NonEmptyString + destination_action_address: NonEmptyString + execution_status: Literal["succeeded", "failed", "partial", "unknown"] + execution_evidence_refs: list[NonEmptyString] = Field(default_factory=list, max_length=64) + delivery_evidence_refs: list[NonEmptyString] = Field(default_factory=list, max_length=64) + observation_evidence_refs: list[NonEmptyString] = Field(default_factory=list, max_length=64) + mapping_loss_refs: list[NonEmptyString] = Field(default_factory=list, max_length=64) + cessation_evidence_refs: list[NonEmptyString] = Field(default_factory=list, max_length=64) + + @model_validator(mode="after") + def _stage_dependencies(self) -> MixedBridgeExecutionEvidence: + if self.delivery_evidence_refs and not self.execution_evidence_refs: + raise ValueError("delivery requires execution evidence") + if self.observation_evidence_refs and not self.delivery_evidence_refs: + raise ValueError("participant observation requires delivery evidence") + if self.execution_status == "succeeded" and not self.execution_evidence_refs: + raise ValueError("successful execution requires readback evidence") + if self.execution_status == "failed" and not self.cessation_evidence_refs: + raise ValueError("known failure requires cessation evidence") + return self + + +class MixedDeliveryReadback(ContractModel): + """Destination receipt observed independently of the bridge result.""" + + operation_id: NonEmptyString + destination_component_id: NonEmptyString + receipt_ref: NonEmptyString + evidence_refs: list[NonEmptyString] = Field(min_length=1, max_length=64) + + +class MixedObservationReadback(ContractModel): + """Participant/audience observation observed after authorized delivery.""" + + operation_id: NonEmptyString + participant_address: NonEmptyString + audience_ref: NonEmptyString + observation_ref: NonEmptyString + evidence_refs: list[NonEmptyString] = Field(min_length=1, max_length=64) + + +@dataclass +class MixedEdgeExecutionCapture: + """Transient outcome of one authorized bridge call, never a second ledger.""" + + provider_calls: int = 0 + provider_started: bool = False + method_completed: bool = False + stage_readback_failed: bool = False + time: MixedTimeCoordinationEvidence | None = None + time_confirmed: bool = False + bridge: MixedBridgeExecutionEvidence | None = None + delivery_confirmed: bool = False + observation_confirmed: bool = False + + +@dataclass(frozen=True) +class MixedEdgeExecutionBinding: + """Installed bridge, mapping and time service for one admitted edge.""" + + edge_id: str + bridge_ref: str + bridge_version: str + bridge_digest: str + source_action_address: str + destination_action_address: str + mapping_ref: str + mapping_loss_ref: str + time_runtime: object + map_action: Callable[..., object] + coordinate: Callable[..., object] + bridge: Callable[..., object] + delivery_readback: Callable[..., object] | None = None + observation_readback: Callable[..., object] | None = None + + def __post_init__(self) -> None: + if not all((self.edge_id, self.bridge_ref, self.bridge_version)): + raise ValueError("executable edge binding requires pinned bridge identity") + if fullmatch(r"sha256:[a-f0-9]{64}", self.bridge_digest) is None: + raise ValueError("executable edge binding requires a pinned bridge digest") + for address in (self.source_action_address, self.destination_action_address, self.mapping_ref): + require_compiled_address(address) + if not self.mapping_loss_ref: + raise ValueError("executable edge binding requires a declared mapping loss") + _require_edge_callbacks(self) + + +def _require_edge_callbacks(binding: MixedEdgeExecutionBinding) -> None: + if not all(callable(value) for value in (binding.map_action, binding.coordinate, binding.bridge)): + raise TypeError("executable edge binding requires mapping, coordination and bridge callables") + if not callable(getattr(binding.time_runtime, "state", None)): + raise TypeError("executable edge binding requires time-runtime readback") + for name in ("delivery_readback", "observation_readback"): + reader = getattr(binding, name) + if reader is not None and not callable(reader): + raise TypeError(f"executable edge {name} must be callable") + + +__all__ = ( + "MixedBridgeExecutionEvidence", + "MixedEdgeExecutionBinding", + "MixedEdgeExecutionCapture", + "MixedDeliveryReadback", + "MixedObservationReadback", + "MixedTimeCoordinationEvidence", +) diff --git a/implementations/python/packages/raes_runtime/mixed_runtime_edge_execution.py b/implementations/python/packages/raes_runtime/mixed_runtime_edge_execution.py new file mode 100644 index 000000000..ab33af00d --- /dev/null +++ b/implementations/python/packages/raes_runtime/mixed_runtime_edge_execution.py @@ -0,0 +1,287 @@ +"""Exact executable mapping, time grant, bridge call, and stage readback.""" + +from __future__ import annotations + +from collections.abc import Callable +from copy import deepcopy +from dataclasses import dataclass, replace +from fractions import Fraction +from functools import partial + +from raes_contracts.contracts.time_model import TimeRuntimeStateModel, validate_time_runtime_state +from raes_contracts.participant_binding import ParticipantActionAdmissionRequest +from raes_contracts.runtime_state import ApplyResult, RuntimeSnapshot + +from .mixed_runtime_edge import ( + MixedBridgeExecutionEvidence, + MixedDeliveryReadback, + MixedEdgeExecutionBinding, + MixedEdgeExecutionCapture, + MixedObservationReadback, + MixedTimeCoordinationEvidence, +) + +_UNSUPPORTED_EDGE_TIME = "executable edge time mapping or governed order is unsupported" + + +def _mapped_edge_method( + binding: object, + edge: object, + installed: MixedEdgeExecutionBinding, + provider_method: Callable[..., object], + operation_id: str, + capture: MixedEdgeExecutionCapture, +) -> Callable[..., object]: + """Execute one admitted edge after its decision and attempt are durable.""" + + declaration = binding.context.time_models[edge.time_binding.time_model_ref] + mapping = declaration.mappings[edge.time_binding.mapping_address] + source_clock = declaration.clocks[edge.time_binding.source_clock_address] + destination_clock = declaration.clocks[edge.time_binding.target_clock_address] + if ( + mapping.source_domain_address != source_clock.time_domain_address + or mapping.target_domain_address != destination_clock.time_domain_address + ): + raise ValueError("executable edge clock domains differ from admission") + + context = _MappedEdgeContext(installed, edge, declaration, mapping, provider_method, operation_id, capture) + return partial(_invoke_mapped_edge, context=context) + + +@dataclass(frozen=True) +class _MappedEdgeContext: + installed: MixedEdgeExecutionBinding + edge: object + declaration: object + mapping: object + provider_method: Callable[..., object] + operation_id: str + capture: MixedEdgeExecutionCapture + + +@dataclass +class _AuthorizedProviderCall: + request: ParticipantActionAdmissionRequest + authorized: ParticipantActionAdmissionRequest + expected: ParticipantActionAdmissionRequest + mapped: ParticipantActionAdmissionRequest + snapshot: RuntimeSnapshot + baseline_snapshot: RuntimeSnapshot + provider_method: Callable[..., object] + capture: MixedEdgeExecutionCapture + + def __call__(self, value: ParticipantActionAdmissionRequest, current: RuntimeSnapshot) -> object: + self.capture.provider_calls += 1 + if self.capture.provider_calls != 1: + raise ValueError("executable edge bridge invoked its provider more than once") + if value is not self.mapped or current is not self.snapshot: + raise ValueError("executable edge bridge changed the authorized invocation") + if (self.snapshot, self.request, self.mapped) != (self.baseline_snapshot, self.authorized, self.expected): + raise ValueError("executable edge bridge changed the authorized invocation") + self.capture.provider_started = True + return self.provider_method(value, current) + + +def _invoke_mapped_edge( + request: ParticipantActionAdmissionRequest, + snapshot: RuntimeSnapshot, + *, + context: _MappedEdgeContext, +) -> ApplyResult: + installed = context.installed + edge = context.edge + declaration = context.declaration + mapping = context.mapping + provider_method = context.provider_method + operation_id = context.operation_id + capture = context.capture + if request.action_contract_address != installed.source_action_address: + raise ValueError("executable edge source action differs from admitted subject") + baseline_snapshot = deepcopy(snapshot) + authorized = deepcopy(request) + expected = replace(deepcopy(authorized), action_contract_address=installed.destination_action_address) + mapped = installed.map_action(deepcopy(authorized)) + if not isinstance(mapped, ParticipantActionAdmissionRequest): + raise TypeError("executable edge mapping must return a typed action") + if (request, mapped) != (authorized, expected): + raise ValueError("executable edge mapping changed an unauthorized subject") + time_state = installed.time_runtime.state(deepcopy(snapshot)) + if not isinstance(time_state, TimeRuntimeStateModel): + raise TypeError("executable edge time readback must be typed") + validate_time_runtime_state(declaration, time_state) + if snapshot.time_model_state != time_state: + raise ValueError("executable edge time readback differs from the committed snapshot") + grant = MixedTimeCoordinationEvidence.model_validate( + installed.coordinate(operation_id, deepcopy(edge), deepcopy(time_state)) + ) + _require_time_grant(grant, operation_id, edge, mapping, time_state) + capture.time = grant + provider_call = _AuthorizedProviderCall( + request, authorized, expected, mapped, snapshot, baseline_snapshot, provider_method, capture + ) + bridged = installed.bridge(operation_id, mapped, snapshot, provider_call) + if not isinstance(bridged, tuple) or len(bridged) != 2 or capture.provider_calls != 1: + raise ValueError("executable edge bridge must return one correlated provider call") + result, report_payload = bridged + if not isinstance(result, ApplyResult): + raise TypeError("executable edge bridge returned an untyped provider result") + report = MixedBridgeExecutionEvidence.model_validate(report_payload) + _require_bridge_report(report, operation_id, installed, result) + capture.bridge = report + capture.method_completed = True + return result + + +def _stage_readback_method( + binding: object, + edge: object, + installed: MixedEdgeExecutionBinding, + request: ParticipantActionAdmissionRequest, + operation_id: str, + capture: MixedEdgeExecutionCapture, +) -> Callable[[ApplyResult], None]: + """Confirm external stages only after the backend result gate accepts the provider result.""" + + declaration = binding.context.time_models[edge.time_binding.time_model_ref] + + def confirm(result: ApplyResult) -> None: + report = capture.bridge + if not result.success or report is None: + return + readback = installed.time_runtime.state(deepcopy(result.snapshot)) + if not isinstance(readback, TimeRuntimeStateModel): + raise TypeError("executable edge post-effect time readback must be typed") + validate_time_runtime_state(declaration, readback) + if result.snapshot.time_model_state != readback: + raise ValueError("executable edge post-effect time readback differs from the result") + capture.time_confirmed = True + _require_stage_readbacks( + installed, + report, + edge, + request, + operation_id, + result.snapshot, + capture, + ) + + return confirm + + +def _require_stage_readbacks( + installed: MixedEdgeExecutionBinding, + report: MixedBridgeExecutionEvidence, + edge: object, + request: ParticipantActionAdmissionRequest, + operation_id: str, + snapshot: RuntimeSnapshot, + capture: MixedEdgeExecutionCapture, +) -> None: + if report.delivery_evidence_refs: + _require_delivery_readback(installed, report, edge, operation_id, snapshot) + capture.delivery_confirmed = True + if report.observation_evidence_refs: + _require_observation_readback(installed, report, edge, request, operation_id, snapshot) + capture.observation_confirmed = True + + +def _require_delivery_readback( + installed: MixedEdgeExecutionBinding, + report: MixedBridgeExecutionEvidence, + edge: object, + operation_id: str, + snapshot: RuntimeSnapshot, +) -> None: + if installed.delivery_readback is None: + raise ValueError("mixed delivery requires destination readback") + delivery = MixedDeliveryReadback.model_validate(installed.delivery_readback(operation_id, deepcopy(snapshot))) + if (delivery.operation_id, delivery.destination_component_id) != (operation_id, edge.target_component_id): + raise ValueError("mixed destination receipt differs from the admitted edge") + if not set(report.delivery_evidence_refs).issubset(delivery.evidence_refs): + raise ValueError("mixed destination receipt differs from the admitted edge") + + +def _require_observation_readback( + installed: MixedEdgeExecutionBinding, + report: MixedBridgeExecutionEvidence, + edge: object, + request: ParticipantActionAdmissionRequest, + operation_id: str, + snapshot: RuntimeSnapshot, +) -> None: + if installed.observation_readback is None: + raise ValueError("mixed observation requires participant readback") + observation = MixedObservationReadback.model_validate( + installed.observation_readback(operation_id, deepcopy(snapshot)) + ) + if (observation.operation_id, observation.participant_address, observation.audience_ref) != ( + operation_id, + request.participant_address, + edge.audience_scope_ref, + ): + raise ValueError("mixed participant observation differs from the authorized audience") + if not set(report.observation_evidence_refs).issubset(observation.evidence_refs): + raise ValueError("mixed participant observation differs from the authorized audience") + + +def _require_time_grant( + grant: MixedTimeCoordinationEvidence, + operation_id: str, + edge: object, + mapping: object, + state: TimeRuntimeStateModel, +) -> None: + source = state.clocks[edge.time_binding.source_clock_address].coordinate + destination = state.clocks[edge.time_binding.target_clock_address].coordinate + required = {item.evidence_ref for item in edge.evidence_bindings} + provided = set(grant.mapping_evidence_refs) | set(grant.timing_evidence_refs) + mapped_tick = Fraction(source.tick * mapping.scale.numerator, mapping.scale.denominator) + mapping.offset_ticks + granted_identity = (grant.operation_id, grant.mapping_ref, grant.ordering_basis, grant.comparison) + required_identity = (operation_id, edge.time_binding.mapping_address, edge.time_binding.ordering_basis, "ordered") + if granted_identity != required_identity or edge.time_binding.ordering_basis in { + "wall_clock_only", + "unknown", + "unsupported", + }: + raise ValueError(_UNSUPPORTED_EDGE_TIME) + if (grant.source_coordinate, grant.destination_coordinate, source.segment) != ( + source, + destination, + destination.segment, + ): + raise ValueError(_UNSUPPORTED_EDGE_TIME) + if (mapped_tick, source.microstep) > (destination.tick, destination.microstep) or not required.issubset(provided): + raise ValueError(_UNSUPPORTED_EDGE_TIME) + + +def _require_bridge_report( + report: MixedBridgeExecutionEvidence, + operation_id: str, + installed: MixedEdgeExecutionBinding, + result: ApplyResult, +) -> None: + report_identity = ( + report.operation_id, + report.bridge_ref, + report.bridge_version, + report.bridge_digest, + report.source_action_address, + report.destination_action_address, + ) + installed_identity = ( + operation_id, + installed.bridge_ref, + installed.bridge_version, + installed.bridge_digest, + installed.source_action_address, + installed.destination_action_address, + ) + if report_identity != installed_identity or set(report.mapping_loss_refs) != {installed.mapping_loss_ref}: + raise ValueError("executable edge report differs from the admitted bridge or provider result") + if (report.execution_status == "succeeded" and not result.success) or ( + report.execution_status == "failed" and result.success + ): + raise ValueError("executable edge report differs from the admitted bridge or provider result") + + +__all__ = ("_mapped_edge_method", "_stage_readback_method") diff --git a/implementations/python/packages/raes_runtime/mixed_runtime_handoff.py b/implementations/python/packages/raes_runtime/mixed_runtime_handoff.py new file mode 100644 index 000000000..eaa502a91 --- /dev/null +++ b/implementations/python/packages/raes_runtime/mixed_runtime_handoff.py @@ -0,0 +1,80 @@ +"""Trusted native responsibility transfer and readback for staged compositions.""" + +from __future__ import annotations + +from collections.abc import Callable +from dataclasses import dataclass +from typing import Literal + +from pydantic import Field +from raes_contracts.contracts.base import ContractModel, NonEmptyString + + +class MixedHandoffEvidence(ContractModel): + operation_id: NonEmptyString + transition_id: NonEmptyString + source_component_id: NonEmptyString + destination_component_id: NonEmptyString + predecessor_history_head: NonEmptyString + phase_revision: int = Field(ge=0) + status: Literal["committed", "failed", "pending", "stale", "unknown"] + order_ref: NonEmptyString + evidence_refs: list[NonEmptyString] = Field(default_factory=list, max_length=64) + + +class MixedHandoffReadback(ContractModel): + operation_id: NonEmptyString + owner_component_id: NonEmptyString + owner_ref: NonEmptyString + phase_revision: int = Field(ge=0) + evidence_refs: list[NonEmptyString] = Field(min_length=1, max_length=64) + + +@dataclass(frozen=True) +class MixedHandoffBinding: + """Installed transfer service for exactly one admitted phase transition.""" + + transition_id: str + source_component_id: str + destination_component_id: str + source_owner_ref: str + destination_owner_ref: str + time_model_ref: str + time_model_digest: str + source_clock_address: str + destination_clock_address: str + mapping_ref: str + ordering_basis: str + time_runtime: object + coordinate: Callable[..., object] + invoke: Callable[..., object] + readback: Callable[..., object] + + def __post_init__(self) -> None: + if not all( + ( + self.transition_id, + self.source_component_id, + self.destination_component_id, + self.source_owner_ref, + self.destination_owner_ref, + self.time_model_ref, + self.time_model_digest, + self.source_clock_address, + self.destination_clock_address, + self.mapping_ref, + self.ordering_basis, + ) + ): + raise ValueError("executable handoff requires exact admitted owner identities") + if self.source_component_id == self.destination_component_id: + raise ValueError("executable handoff requires distinct component owners") + if self.ordering_basis in {"wall_clock_only", "unknown", "unsupported"}: + raise ValueError("executable handoff requires governed order") + if not all(callable(value) for value in (self.coordinate, self.invoke, self.readback)): + raise TypeError("executable handoff requires time coordination, invocation and native readback") + if not callable(getattr(self.time_runtime, "state", None)): + raise TypeError("executable handoff requires time-runtime readback") + + +__all__ = ("MixedHandoffBinding", "MixedHandoffEvidence", "MixedHandoffReadback") diff --git a/implementations/python/packages/raes_runtime/mixed_runtime_handoff_execution.py b/implementations/python/packages/raes_runtime/mixed_runtime_handoff_execution.py new file mode 100644 index 000000000..9ea8982e7 --- /dev/null +++ b/implementations/python/packages/raes_runtime/mixed_runtime_handoff_execution.py @@ -0,0 +1,274 @@ +"""Executable native handoff and correlated time readback for mixed phases.""" + +from __future__ import annotations + +from copy import deepcopy +from dataclasses import dataclass +from fractions import Fraction + +from raes_contracts.contracts.mixed_composition import MixedCompositionTransitionModel +from raes_contracts.contracts.mixed_runtime import MixedCompositionRuntimeStateModel +from raes_contracts.contracts.time_model import TimeRuntimeStateModel, validate_time_runtime_state +from raes_contracts.runtime_state import OperationState, RuntimeSnapshot + +from .control_plane_mutation import external_control_plane_call +from .mixed_runtime import MixedRuntimeBinding +from .mixed_runtime_edge import MixedTimeCoordinationEvidence +from .mixed_runtime_handoff import MixedHandoffBinding, MixedHandoffEvidence, MixedHandoffReadback + +_UNSUPPORTED_HANDOFF_TIME = "handoff time coordination is unsupported" + + +@dataclass(frozen=True) +class _HandoffResolution: + state: OperationState + order_ref: str + evidence_refs: tuple[str, ...] = () + destination_component_id: str | None = None + + +@dataclass +class _HandoffProgress: + confirmed_refs: tuple[str, ...] + correlated: bool = False + evidence: MixedHandoffEvidence | None = None + readback: MixedHandoffReadback | None = None + + +@dataclass(frozen=True) +class _HandoffInvocation: + installed: MixedHandoffBinding + declaration: object + transition: MixedCompositionTransitionModel + state: MixedCompositionRuntimeStateModel + operation_id: str + baseline_snapshot: RuntimeSnapshot + time_state: TimeRuntimeStateModel + grant: MixedTimeCoordinationEvidence + + +def _perform_handoff( + control_plane: object, + binding: MixedRuntimeBinding, + transition: MixedCompositionTransitionModel, + state: MixedCompositionRuntimeStateModel, + operation_id: str, +) -> _HandoffResolution | None: + target = binding.profile.phases[transition.target_phase_id] + if set(state.active_component_ids) == set(target.active_component_ids): + return None + return _resolve_required_handoff(control_plane, binding, transition, state, operation_id) + + +def _resolve_required_handoff( + control_plane: object, + binding: MixedRuntimeBinding, + transition: MixedCompositionTransitionModel, + state: MixedCompositionRuntimeStateModel, + operation_id: str, +) -> _HandoffResolution: + installed = binding.handoff_bindings.get(transition.transition_id) + resolution = _HandoffResolution(OperationState.FAILED, "order:handoff-unbound") + if installed is not None: + declaration = binding.context.time_models[installed.time_model_ref] + baseline_snapshot = deepcopy(control_plane._snapshot) + try: + time_state, grant = _request_handoff_grant( + control_plane, installed, declaration, transition, operation_id, baseline_snapshot + ) + except Exception: + resolution = _HandoffResolution(OperationState.FAILED, "order:handoff-time-refused") + else: + progress = _HandoffProgress( + tuple(dict.fromkeys([*grant.mapping_evidence_refs, *grant.timing_evidence_refs])) + ) + try: + invocation = _HandoffInvocation( + installed, declaration, transition, state, operation_id, baseline_snapshot, time_state, grant + ) + _invoke_handoff_stage(control_plane, invocation, progress) + except Exception: + resolution = _HandoffResolution(OperationState.INDETERMINATE, grant.order_ref, progress.confirmed_refs) + else: + resolution = _handoff_stage_outcome(installed, state, operation_id, grant, progress) + return resolution + + +def _request_handoff_grant( + control_plane: object, + installed: MixedHandoffBinding, + declaration: object, + transition: MixedCompositionTransitionModel, + operation_id: str, + baseline_snapshot: RuntimeSnapshot, +) -> tuple[TimeRuntimeStateModel, MixedTimeCoordinationEvidence]: + with external_control_plane_call(control_plane): + time_state = installed.time_runtime.state(deepcopy(baseline_snapshot)) + if not isinstance(time_state, TimeRuntimeStateModel): + raise TypeError("handoff time readback must be typed") + validate_time_runtime_state(declaration, time_state) + if time_state != baseline_snapshot.time_model_state: + raise ValueError("handoff time readback differs from the committed snapshot") + grant = MixedTimeCoordinationEvidence.model_validate( + installed.coordinate(operation_id, deepcopy(transition), deepcopy(time_state)) + ) + _require_handoff_time_grant(installed, grant, operation_id, declaration, time_state, transition) + return time_state, grant + + +def _invoke_handoff_stage( + control_plane: object, + invocation: _HandoffInvocation, + progress: _HandoffProgress, +) -> None: + installed = invocation.installed + declaration = invocation.declaration + transition = invocation.transition + state = invocation.state + operation_id = invocation.operation_id + baseline_snapshot = invocation.baseline_snapshot + time_state = invocation.time_state + grant = invocation.grant + with external_control_plane_call(control_plane): + evidence = MixedHandoffEvidence.model_validate( + installed.invoke(operation_id, deepcopy(transition), deepcopy(state), deepcopy(baseline_snapshot)) + ) + required = {item.evidence_ref for item in transition.evidence_bindings} + progress.correlated = _handoff_evidence_correlated( + evidence, installed, transition, state, operation_id, grant, required + ) + progress.evidence = evidence + if progress.correlated: + progress.confirmed_refs = tuple(dict.fromkeys([*progress.confirmed_refs, *evidence.evidence_refs])) + readback = MixedHandoffReadback.model_validate(installed.readback(operation_id, deepcopy(baseline_snapshot))) + progress.readback = readback + if progress.correlated and readback.operation_id == operation_id: + progress.confirmed_refs = tuple(dict.fromkeys([*progress.confirmed_refs, *readback.evidence_refs])) + _validate_handoff_time_readback(installed, declaration, baseline_snapshot, time_state) + + +def _handoff_evidence_correlated( + evidence: MixedHandoffEvidence, + installed: MixedHandoffBinding, + transition: MixedCompositionTransitionModel, + state: MixedCompositionRuntimeStateModel, + operation_id: str, + grant: MixedTimeCoordinationEvidence, + required: set[str], +) -> bool: + observed = ( + evidence.operation_id, + evidence.transition_id, + evidence.source_component_id, + evidence.destination_component_id, + evidence.predecessor_history_head, + evidence.phase_revision, + evidence.order_ref, + ) + expected = ( + operation_id, + transition.transition_id, + installed.source_component_id, + installed.destination_component_id, + state.history_head, + state.phase_revision, + grant.order_ref, + ) + return observed == expected and required.issubset(evidence.evidence_refs) + + +def _validate_handoff_time_readback( + installed: MixedHandoffBinding, + declaration: object, + baseline_snapshot: RuntimeSnapshot, + time_state: TimeRuntimeStateModel, +) -> None: + final_time = installed.time_runtime.state(deepcopy(baseline_snapshot)) + if not isinstance(final_time, TimeRuntimeStateModel): + raise TypeError("handoff post-transfer time readback must be typed") + validate_time_runtime_state(declaration, final_time) + if final_time != baseline_snapshot.time_model_state: + raise ValueError("handoff post-transfer time readback differs from the committed snapshot") + for clock_address in (installed.source_clock_address, installed.destination_clock_address): + previous = time_state.clocks[clock_address].coordinate + current = final_time.clocks[clock_address].coordinate + if (current.segment, current.tick, current.microstep) < (previous.segment, previous.tick, previous.microstep): + raise ValueError("handoff time readback regressed") + + +def _handoff_stage_outcome( + installed: MixedHandoffBinding, + state: MixedCompositionRuntimeStateModel, + operation_id: str, + grant: MixedTimeCoordinationEvidence, + progress: _HandoffProgress, +) -> _HandoffResolution: + evidence = progress.evidence + readback = progress.readback + resolution = _HandoffResolution(OperationState.INDETERMINATE, grant.order_ref, progress.confirmed_refs) + if progress.correlated and evidence is not None and readback is not None and readback.operation_id == operation_id: + if evidence.status == "committed": + committed = (readback.owner_component_id, readback.owner_ref, readback.phase_revision) == ( + installed.destination_component_id, + installed.destination_owner_ref, + state.phase_revision + 1, + ) + resolution = _HandoffResolution( + OperationState.SUCCEEDED if committed else OperationState.INDETERMINATE, + evidence.order_ref, + progress.confirmed_refs, + installed.destination_component_id if committed else None, + ) + elif evidence.status in {"failed", "stale"}: + retained = (readback.owner_component_id, readback.owner_ref, readback.phase_revision) == ( + installed.source_component_id, + installed.source_owner_ref, + state.phase_revision, + ) + resolution = _HandoffResolution( + OperationState.FAILED if retained else OperationState.INDETERMINATE, + evidence.order_ref, + progress.confirmed_refs, + ) + else: + resolution = _HandoffResolution(OperationState.INDETERMINATE, evidence.order_ref, progress.confirmed_refs) + return resolution + + +def _require_handoff_time_grant( + installed: MixedHandoffBinding, + grant: MixedTimeCoordinationEvidence, + operation_id: str, + declaration: object, + state: TimeRuntimeStateModel, + transition: MixedCompositionTransitionModel, +) -> None: + source = state.clocks[installed.source_clock_address].coordinate + destination = state.clocks[installed.destination_clock_address].coordinate + mapping = declaration.mappings[installed.mapping_ref] + mapped_tick = Fraction(source.tick * mapping.scale.numerator, mapping.scale.denominator) + mapping.offset_ticks + required = {item.evidence_ref for item in transition.evidence_bindings} + granted = ( + grant.operation_id, + grant.mapping_ref, + grant.ordering_basis, + grant.comparison, + grant.source_coordinate, + grant.destination_coordinate, + source.segment, + ) + expected = ( + operation_id, + installed.mapping_ref, + installed.ordering_basis, + "ordered", + source, + destination, + destination.segment, + ) + if granted != expected: + raise ValueError(_UNSUPPORTED_HANDOFF_TIME) + if (mapped_tick, source.microstep) > (destination.tick, destination.microstep): + raise ValueError(_UNSUPPORTED_HANDOFF_TIME) + if not required.issubset(set(grant.mapping_evidence_refs) | set(grant.timing_evidence_refs)): + raise ValueError(_UNSUPPORTED_HANDOFF_TIME) diff --git a/implementations/python/packages/raes_runtime/mixed_runtime_phase.py b/implementations/python/packages/raes_runtime/mixed_runtime_phase.py index 61e2211eb..b99242b94 100644 --- a/implementations/python/packages/raes_runtime/mixed_runtime_phase.py +++ b/implementations/python/packages/raes_runtime/mixed_runtime_phase.py @@ -2,6 +2,7 @@ from __future__ import annotations +from copy import deepcopy from dataclasses import replace from uuid import uuid4 @@ -13,7 +14,13 @@ from raes_contracts.diagnostics import Diagnostic from raes_contracts.operation_lifecycle import OperationAdmissionContext from raes_contracts.planning import RuntimeDomain -from raes_contracts.runtime_state import OperationKind, OperationReceipt, OperationState, OperationStatus +from raes_contracts.runtime_state import ( + OperationKind, + OperationReceipt, + OperationState, + OperationStatus, + operation_terminal_diagnostics, +) from .control_plane_execution import _utc_now from .control_plane_mutation import external_control_plane_call @@ -21,6 +28,7 @@ from .control_plane_security import ControlPlaneIdentity from .control_plane_store import AuditEvent, ControlPlaneOperationRecord from .mixed_runtime import MixedPhaseTransitionEvaluation, MixedRuntimeBinding +from .mixed_runtime_handoff_execution import _HandoffResolution, _perform_handoff from .mixed_runtime_state import append_runtime_events, runtime_state _OUTSTANDING_STATES = {OperationState.ACCEPTED, OperationState.RUNNING, OperationState.INDETERMINATE} @@ -34,7 +42,8 @@ def _mixed_runtime_is_quiescent(control_plane: object, run_id: str, history_key: context = record.status.context if ( context.run_scope == run_scope - and context.operation_kind in {OperationKind.PARTICIPANT_ACTION, OperationKind.PARTICIPANT_CROSSING} + and context.operation_kind + in {OperationKind.PARTICIPANT_ACTION, OperationKind.PARTICIPANT_CROSSING, OperationKind.COMPOSITION_PHASE} and record.status.state in _OUTSTANDING_STATES and (history_key in record.decision_history_heads or history_key in record.result_history_heads) ): @@ -47,7 +56,7 @@ def _evaluate(control_plane: object, transition: object, state: object) -> Mixed evaluator = binding.transition_evaluators[transition.evaluator_ref] try: with external_control_plane_call(control_plane): - evaluation = evaluator(transition, state, control_plane._snapshot) + evaluation = evaluator(deepcopy(transition), deepcopy(state), deepcopy(control_plane._snapshot)) except Exception: evaluation = _failed_evaluation("order:evaluator-failed") if isinstance(evaluation, MixedPhaseTransitionEvaluation): @@ -162,29 +171,15 @@ def _phase_outcome( state: MixedCompositionRuntimeStateModel, evaluation: MixedPhaseTransitionEvaluation, operation_id: str, + handoff: _HandoffResolution | None, ) -> tuple[list[MixedCompositionRuntimeEventModel], OperationState, Diagnostic | None]: common = _phase_event_fields(state, transition, evaluation) - if not evaluation.permitted: - failure = MixedCompositionRuntimeEventModel( - event_id=f"composition:{operation_id}:failure", - event_kind="failure", - disposition="denied", - predecessor_event_id=state.history_head, - phase_id=state.phase_id, - phase_revision=state.phase_revision, - active_component_ids=state.active_component_ids, - active_allocation_ids=state.active_allocation_ids, - active_edge_ids=state.active_edge_ids, - **common, - ) - diagnostic = Diagnostic( - code="runtime.mixed-composition-transition-denied", - domain="runtime", - address=f"mixed-composition.{state.run_id}", - message="The admitted phase transition evaluator did not permit progression.", - ) - return [failure], OperationState.FAILED, diagnostic target = binding.profile.phases[transition.target_phase_id] + needs_handoff = set(state.active_component_ids) != set(target.active_component_ids) + if not evaluation.permitted or ( + needs_handoff and handoff is not None and handoff.state is not OperationState.SUCCEEDED + ): + return _denied_phase_outcome(state, evaluation, operation_id, handoff, common) phase = MixedCompositionRuntimeEventModel( event_id=f"composition:{operation_id}:phase", event_kind="phase-transition", @@ -197,14 +192,52 @@ def _phase_outcome( active_edge_ids=target.active_edge_ids, **common, ) - handoff = phase.model_copy( + if not needs_handoff: + return [phase], OperationState.SUCCEEDED, None + assert handoff is not None + event = phase.model_copy( update={ "event_id": f"composition:{operation_id}:handoff", "event_kind": "handoff", "predecessor_event_id": phase.event_id, + "component_id": handoff.destination_component_id, + "order_ref": handoff.order_ref, + "evidence_refs": list(handoff.evidence_refs), } ) - return [phase, handoff], OperationState.SUCCEEDED, None + return [phase, event], OperationState.SUCCEEDED, None + + +def _denied_phase_outcome( + state: MixedCompositionRuntimeStateModel, + evaluation: MixedPhaseTransitionEvaluation, + operation_id: str, + handoff: _HandoffResolution | None, + common: dict[str, object], +) -> tuple[list[MixedCompositionRuntimeEventModel], OperationState, Diagnostic]: + terminal_state = handoff.state if evaluation.permitted and handoff is not None else OperationState.FAILED + if evaluation.permitted and handoff is not None: + common["order_ref"] = handoff.order_ref + common["evidence_refs"] = list(dict.fromkeys([*evaluation.evidence_refs, *handoff.evidence_refs])) + failure = MixedCompositionRuntimeEventModel( + event_id=f"composition:{operation_id}:failure", + event_kind="failure", + disposition="indeterminate" if terminal_state is OperationState.INDETERMINATE else "denied", + predecessor_event_id=state.history_head, + phase_id=state.phase_id, + phase_revision=state.phase_revision, + active_component_ids=state.active_component_ids, + active_allocation_ids=state.active_allocation_ids, + active_edge_ids=state.active_edge_ids, + **common, + ) + diagnostic = Diagnostic( + code="runtime.mixed-composition-transition-denied", + domain="runtime", + address=f"mixed-composition.{state.run_id}", + message="The admitted phase transition or required executable handoff did not permit progression.", + ) + return [failure], terminal_state, diagnostic def advance_mixed_composition( @@ -233,7 +266,10 @@ def advance_mixed_composition( if claimed.receipt.operation_id != operation_id: return claimed.receipt evaluation = _evaluate(control_plane, transition, state) - events, terminal_state, diagnostic = _phase_outcome(binding, transition, state, evaluation, operation_id) + handoff = ( + _perform_handoff(control_plane, binding, transition, state, operation_id) if evaluation.permitted else None + ) + events, terminal_state, diagnostic = _phase_outcome(binding, transition, state, evaluation, operation_id, handoff) snapshot = append_runtime_events(binding, control_plane._snapshot, state, events) terminal = replace( running, @@ -241,7 +277,7 @@ def advance_mixed_composition( running.status, state=terminal_state, updated_at=_utc_now(), - diagnostics=[] if diagnostic is None else [diagnostic], + diagnostics=operation_terminal_diagnostics(terminal_state, [] if diagnostic is None else [diagnostic]), ), result_history_heads={history_key: events[-1].event_id}, ) @@ -249,10 +285,10 @@ def advance_mixed_composition( timestamp=terminal.status.updated_at, action="advance_mixed_composition", identity=context.actor_id, - allowed=evaluation.permitted, + allowed=terminal_state is OperationState.SUCCEEDED, target=context.target_scope, operation_id=operation_id, - reason="committed" if evaluation.permitted else "transition-denied", + reason="committed" if terminal_state is OperationState.SUCCEEDED else "transition-denied", ) control_plane._commit_participant_transition( expected_history_heads={history_key: state.history_head}, diff --git a/implementations/python/packages/raes_runtime/mixed_runtime_recovery.py b/implementations/python/packages/raes_runtime/mixed_runtime_recovery.py new file mode 100644 index 000000000..562cab37f --- /dev/null +++ b/implementations/python/packages/raes_runtime/mixed_runtime_recovery.py @@ -0,0 +1,126 @@ +"""Fail-closed startup classification for interrupted mixed external stages.""" + +from __future__ import annotations + +from raes_contracts.contracts.participant_crossing import ParticipantCrossingOccurrenceModel +from raes_contracts.runtime_state import OperationKind, OperationState, RuntimeSnapshot + +from .control_plane_store import ControlPlaneOperationRecord +from .mixed_runtime_dispatch import _recovery_attempt +from .participant_crossing_state_cut import canonical_crossing_digest, history_record_identity + + +def has_mixed_resolution_cut(record: ControlPlaneOperationRecord) -> bool: + """Identify a mixed effect from durable operation metadata alone.""" + + return record.status.context.operation_kind in { + OperationKind.COMPOSITION_PHASE, + OperationKind.PARTICIPANT_ACTION, + OperationKind.PARTICIPANT_CROSSING, + } and any(key.startswith("mixed_composition_history:") for key in record.decision_history_heads) + + +def requires_mixed_stage_reconciliation(control_plane: object, record: ControlPlaneOperationRecord) -> bool: + """A provider observation cannot prove a bridge or native transfer finished.""" + + kind = record.status.context.operation_kind + has_mixed_history = any(key.startswith("mixed_composition_history:") for key in record.decision_history_heads) + if not has_mixed_history or kind not in { + OperationKind.COMPOSITION_PHASE, + OperationKind.PARTICIPANT_ACTION, + OperationKind.PARTICIPANT_CROSSING, + }: + return False + if kind is OperationKind.COMPOSITION_PHASE: + # A claimed phase can have invoked its native owner before the terminal commit. + return True + binding = getattr(control_plane, "_mixed_runtime", None) + attempt = _recovery_attempt(control_plane, binding, record.receipt.operation_id) if binding is not None else None + # Missing provenance or an edge means provider-only recovery cannot prove + # the authorized time grant, bridge, delivery, and observation stages. + return attempt is None or attempt.edge_id is not None + + +def has_unresolved_mixed_action_cut(control_plane: object) -> bool: + """A partial crossing cut stays quarantined until its operation is resolved.""" + + return any( + record.status.state in {OperationState.RUNNING, OperationState.INDETERMINATE} + and record.status.context.operation_kind + in {OperationKind.PARTICIPANT_ACTION, OperationKind.PARTICIPANT_CROSSING} + and requires_mixed_stage_reconciliation(control_plane, record) + for record in control_plane._operations.values() + ) + + +def validate_restored_mixed_crossing_cut(control_plane: object, resolver: object) -> None: + """Validate every retained crossing outside an interrupted mixed suffix.""" + + from .participant_crossing_mediation import validate_persisted_crossing_history + + snapshot = control_plane._snapshot + if not has_unresolved_mixed_action_cut(control_plane): + validate_persisted_crossing_history(snapshot, resolver) + return + prefix_lengths = _interrupted_crossing_prefixes(control_plane, snapshot) + for history in snapshot.participant_crossing_history.values(): + for item in history: + ParticipantCrossingOccurrenceModel.model_validate(item) + retained = { + participant_address: list(history[: prefix_lengths.get(participant_address, len(history))]) + for participant_address, history in snapshot.participant_crossing_history.items() + } + projection: RuntimeSnapshot = snapshot.with_entries(dict(snapshot.entries), participant_crossing_history=retained) + validate_persisted_crossing_history(projection, resolver) + + +def _interrupted_crossing_prefixes(control_plane: object, snapshot: RuntimeSnapshot) -> dict[str, int]: + prefix_lengths: dict[str, int] = {} + for record in control_plane._operations.values(): + if not _is_interrupted_mixed_action(control_plane, record): + continue + crossing_heads = { + key.partition(":")[2]: head + for key, head in record.decision_history_heads.items() + if key.startswith("participant_crossing_history:") + } + if not crossing_heads: + raise ValueError("interrupted mixed action has no durable crossing cut") + for participant_address, head in crossing_heads.items(): + history = snapshot.participant_crossing_history.get(participant_address, []) + key = f"participant_crossing_history:{participant_address}" + cut = _crossing_prefix_length(history, head, record.result_history_heads.get(key)) + prefix_lengths[participant_address] = min(prefix_lengths.get(participant_address, len(history)), cut) + return prefix_lengths + + +def _is_interrupted_mixed_action(control_plane: object, record: ControlPlaneOperationRecord) -> bool: + return ( + record.status.state in {OperationState.RUNNING, OperationState.INDETERMINATE} + and record.status.context.operation_kind + in {OperationKind.PARTICIPANT_ACTION, OperationKind.PARTICIPANT_CROSSING} + and requires_mixed_stage_reconciliation(control_plane, record) + ) + + +def _crossing_prefix_length(history: list[dict[str, object]], head: str | None, result_head: str | None) -> int: + current_head = _crossing_head(history[-1]) if history else None + if current_head != result_head: + raise ValueError("interrupted mixed action crossing result head differs from the stored cut") + matches = ( + [index + 1 for index, item in enumerate(history) if _crossing_head(item) == head] if head is not None else [0] + ) + if len(matches) != 1: + raise ValueError("interrupted mixed action crossing predecessor is missing or ambiguous") + return matches[0] + + +def _crossing_head(item: dict[str, object]) -> str: + return history_record_identity(item) or canonical_crossing_digest(item) + + +def require_resolvable_mixed_action_cut(_control_plane: object, record: ControlPlaneOperationRecord) -> None: + """Generic acceptance cannot release unproved mixed external stages.""" + + if has_mixed_resolution_cut(record): + raise ValueError("mixed stage reconciliation is required before resolution") diff --git a/implementations/python/packages/raes_runtime/mixed_runtime_result.py b/implementations/python/packages/raes_runtime/mixed_runtime_result.py new file mode 100644 index 000000000..bdb716e09 --- /dev/null +++ b/implementations/python/packages/raes_runtime/mixed_runtime_result.py @@ -0,0 +1,196 @@ +"""Correlated mixed action stages and shared operation settlement.""" + +from __future__ import annotations + +from typing import Literal + +from raes_contracts.contracts.mixed_runtime import MixedCompositionRuntimeEventModel +from raes_contracts.runtime_state import ApplyResult, OperationState, RuntimeSnapshot + +from .mixed_runtime_dispatch import PreparedMixedActionDispatch, _runtime_event_fields +from .mixed_runtime_edge import MixedBridgeExecutionEvidence, MixedEdgeExecutionCapture +from .mixed_runtime_state import append_runtime_events, runtime_state +from .participant_crossing_mediation import PreparedParticipantCrossing + +_EventKind = Literal["result", "delivery", "observation", "weakening", "failure"] +_Disposition = Literal["committed", "succeeded", "failed", "indeterminate"] + + +def record_mixed_action_result( + control_plane: object, + snapshot: RuntimeSnapshot, + crossing: PreparedParticipantCrossing, + *, + success: bool, + capture: MixedEdgeExecutionCapture | None = None, +) -> RuntimeSnapshot: + """Append the backend outcome without allowing it to rewrite the decision.""" + + binding = getattr(control_plane, "_mixed_runtime", None) + if binding is None: + return snapshot + state = runtime_state(binding, snapshot) + attempt = snapshot.mixed_composition_history[state.run_id][-1] + common = _runtime_event_fields( + state, + allocation_id=attempt.get("allocation_id"), + component_id=attempt.get("component_id"), + edge_id=attempt.get("edge_id"), + control_event_ref=attempt.get("control_event_ref"), + crossing_event_ref=attempt.get("crossing_event_ref"), + policy_decision_ref=attempt.get("policy_decision_ref"), + mapping_ref=attempt.get("mapping_ref"), + order_ref=str(attempt["order_ref"]), + mapping_loss_refs=[], + evidence_refs=list(attempt.get("evidence_refs", [])), + ) + operation_id = crossing.record.receipt.operation_id + report = capture.bridge if capture is not None else None + rejected_result = capture is not None and capture.method_completed and not success + disposition = _result_disposition(capture, report, success, rejected_result) + _augment_result_evidence(common, capture, report, rejected_result) + events = [_result_event(operation_id, "result", disposition, state.history_head, common)] + _append_confirmed_stages(events, operation_id, common, capture, report, rejected_result) + if disposition == "failed": + events.append(_result_event(operation_id, "failure", "failed", events[-1].event_id, common)) + return append_runtime_events(binding, snapshot, state, events) + + +def _result_disposition( + capture: MixedEdgeExecutionCapture | None, + report: MixedBridgeExecutionEvidence | None, + success: bool, + rejected_result: bool, +) -> _Disposition: + if _unconfirmed_execution(capture, report, rejected_result): + disposition: _Disposition = "indeterminate" + elif report is not None and report.execution_status == "succeeded": + disposition = "succeeded" + else: + disposition = "succeeded" if success else "failed" + return disposition + + +def _unconfirmed_execution( + capture: MixedEdgeExecutionCapture | None, + report: MixedBridgeExecutionEvidence | None, + rejected_result: bool, +) -> bool: + if report is None: + unconfirmed = capture is not None and capture.provider_started + elif report.execution_status in {"partial", "unknown"}: + unconfirmed = True + elif report.execution_status == "succeeded": + unconfirmed = rejected_result or _unconfirmed_stages(capture) + else: + unconfirmed = False + return unconfirmed + + +def _unconfirmed_stages(capture: MixedEdgeExecutionCapture | None) -> bool: + return capture is not None and (capture.stage_readback_failed or not capture.time_confirmed) + + +def _augment_result_evidence( + common: dict[str, object], + capture: MixedEdgeExecutionCapture | None, + report: MixedBridgeExecutionEvidence | None, + rejected_result: bool, +) -> None: + if capture is None: + return + if report is not None and not rejected_result and capture.time_confirmed: + common["mapping_loss_refs"] = list(report.mapping_loss_refs) + if capture.time is not None and not rejected_result: + _append_time_evidence(common, capture, report) + if report is not None and report.execution_status == "failed" and capture.method_completed: + common["evidence_refs"] = list(dict.fromkeys([*common["evidence_refs"], *report.cessation_evidence_refs])) + + +def _append_time_evidence( + common: dict[str, object], + capture: MixedEdgeExecutionCapture, + report: MixedBridgeExecutionEvidence | None, +) -> None: + assert capture.time is not None + if capture.time_confirmed: + common["order_ref"] = capture.time.order_ref + common["evidence_refs"] = list( + dict.fromkeys( + [ + *common["evidence_refs"], + *capture.time.mapping_evidence_refs, + *capture.time.timing_evidence_refs, + *(report.execution_evidence_refs if report is not None else ()), + ] + ) + ) + + +def _result_event( + operation_id: str, + kind: _EventKind, + disposition: _Disposition, + predecessor: str, + common: dict[str, object], +) -> MixedCompositionRuntimeEventModel: + return MixedCompositionRuntimeEventModel( + event_id=f"composition:{operation_id}:{kind}", + event_kind=kind, + disposition=disposition, + predecessor_event_id=predecessor, + **common, + ) + + +def _append_confirmed_stages( + events: list[MixedCompositionRuntimeEventModel], + operation_id: str, + common: dict[str, object], + capture: MixedEdgeExecutionCapture | None, + report: MixedBridgeExecutionEvidence | None, + rejected_result: bool, +) -> None: + if rejected_result or report is None or capture is None: + return + if capture.delivery_confirmed: + common["evidence_refs"] = list(report.delivery_evidence_refs) + events.append(_result_event(operation_id, "delivery", "succeeded", events[-1].event_id, common)) + if capture.observation_confirmed: + common["evidence_refs"] = list(report.observation_evidence_refs) + events.append(_result_event(operation_id, "observation", "committed", events[-1].event_id, common)) + if capture.time_confirmed and report.mapping_loss_refs: + common["evidence_refs"] = list(capture.time.mapping_evidence_refs) if capture.time is not None else [] + events.append(_result_event(operation_id, "weakening", "committed", events[-1].event_id, common)) + + +def mixed_action_terminal_state( + dispatch: PreparedMixedActionDispatch | None, + result: ApplyResult, +) -> OperationState: + """Settle one mixed action from its correlated stages, not a success flag.""" + + if dispatch is None or dispatch.capture is None: + state = OperationState.SUCCEEDED if result.success else OperationState.FAILED + else: + state = _captured_action_terminal_state(dispatch.capture, result) + return state + + +def _captured_action_terminal_state(capture: MixedEdgeExecutionCapture, result: ApplyResult) -> OperationState: + report = capture.bridge + if report is None: + state = OperationState.INDETERMINATE if capture.provider_started else OperationState.FAILED + elif report.execution_status in {"partial", "unknown"}: + state = OperationState.INDETERMINATE + elif report.execution_status == "failed": + state = OperationState.FAILED + else: + confirmed = all( + (result.success, capture.time_confirmed, not capture.stage_readback_failed, capture.delivery_confirmed) + ) + state = OperationState.SUCCEEDED if confirmed else OperationState.INDETERMINATE + return state + + +__all__ = ("mixed_action_terminal_state", "record_mixed_action_result") diff --git a/implementations/python/packages/raes_runtime/participant_crossing_action.py b/implementations/python/packages/raes_runtime/participant_crossing_action.py index 026ecf2af..279384a23 100644 --- a/implementations/python/packages/raes_runtime/participant_crossing_action.py +++ b/implementations/python/packages/raes_runtime/participant_crossing_action.py @@ -26,8 +26,10 @@ class ActionIngressExecution: def action_operation_record( crossing: PreparedParticipantCrossing, result: object, + *, + terminal_state: OperationState | None = None, ) -> ControlPlaneOperationRecord: - state = OperationState.SUCCEEDED if result.success else OperationState.FAILED + state = terminal_state or (OperationState.SUCCEEDED if result.success else OperationState.FAILED) diagnostics = operation_terminal_diagnostics(state, list(result.diagnostics)) receipt = crossing.record.receipt status = OperationStatus( diff --git a/implementations/python/packages/raes_runtime/participant_crossing_boundary.py b/implementations/python/packages/raes_runtime/participant_crossing_boundary.py index e6590fab9..566abaa51 100644 --- a/implementations/python/packages/raes_runtime/participant_crossing_boundary.py +++ b/implementations/python/packages/raes_runtime/participant_crossing_boundary.py @@ -19,8 +19,8 @@ from .mixed_runtime_dispatch import ( PreparedMixedActionDispatch, prepare_mixed_action_dispatch, - record_mixed_action_result, ) +from .mixed_runtime_result import mixed_action_terminal_state, record_mixed_action_result from .participant_control_intents import ParticipantControlIntent, ParticipantControlIntentBase from .participant_control_mediation import ( bind_participant_control_request, @@ -302,7 +302,7 @@ def _prepare_action_effect( return _PreparedActionEffect( crossing=crossing, request=governed, - mixed_dispatch=prepare_mixed_action_dispatch(control_plane, governed, crossing), + mixed_dispatch=prepare_mixed_action_dispatch(control_plane, governed, crossing, sink_decision), sink_decision=sink_decision, ) @@ -354,7 +354,7 @@ def _apply_action_effect( ) -> ApplyResult: mixed = prepared.mixed_dispatch with control_plane._mutation_authority.external_call(): - return apply_authorized_participant_action( + result = apply_authorized_participant_action( method=mixed.method if mixed is not None else execution.method, request=prepared.request, snapshot=control_plane._snapshot, @@ -365,6 +365,13 @@ def _apply_action_effect( None, ), ) + if mixed is not None and mixed.stage_readback is not None and result.success: + try: + mixed.stage_readback(result) + except Exception: + assert mixed.capture is not None + mixed.capture.stage_readback_failed = True + return result def _commit_action_effect( @@ -385,14 +392,16 @@ def _commit_action_effect( next_snapshot, crossing, success=result.success, + capture=mixed_dispatch.capture if mixed_dispatch is not None else None, ) + terminal_state = mixed_action_terminal_state(mixed_dispatch, result) result_history_heads = _expected_history_heads(next_snapshot, request.participant_address) if mixed_dispatch is not None: result_history_heads[f"mixed_composition_history:{control_plane._mixed_runtime.entry.run_id}"] = ( next_snapshot.mixed_composition_states[control_plane._mixed_runtime.entry.run_id]["history_head"] ) record = replace( - action_operation_record(crossing, result), + action_operation_record(crossing, result, terminal_state=terminal_state), decision_history_heads=authorization_expected_heads, result_history_heads=result_history_heads, ) @@ -400,8 +409,8 @@ def _commit_action_effect( crossing.audit_event, crossing, action="admit_participant_action", - allowed=result.success, - reason="accepted" if result.success else "backend-admission-failed", + allowed=terminal_state is OperationState.SUCCEEDED, + reason="accepted" if terminal_state is OperationState.SUCCEEDED else "backend-admission-unresolved", ) if prepared.sink_decision is not None: audit = apply_flow_sink_details(audit, prepared.sink_decision) diff --git a/implementations/python/tests/test_formal_semantic_validation.py b/implementations/python/tests/test_formal_semantic_validation.py index d84008986..4ed35519d 100644 --- a/implementations/python/tests/test_formal_semantic_validation.py +++ b/implementations/python/tests/test_formal_semantic_validation.py @@ -132,6 +132,7 @@ def test_atomic_release_index_validates_every_historical_bundle() -> None: "51.0.0", "52.0.0", "53.0.0", + "54.0.0", ] assert all(validate_release_bundle(REPO_ROOT, release) == [] for release in releases) @@ -140,10 +141,10 @@ def test_atomic_release_index_validates_every_historical_bundle() -> None: def test_current_retest_bundle_is_coherent_and_clean() -> None: release, protocol, corpus, snapshot, analysis = copy_bundle(load_retest_bundle, REPO_ROOT) - assert release.manifest["revision"] == "53.0.0" + assert release.manifest["revision"] == "54.0.0" assert protocol["revision"] == "2.0.0" assert corpus["revision"] == "4.0.0" - assert snapshot["baseline"]["release_revision"] == "52.0.0" + assert snapshot["baseline"]["release_revision"] == "53.0.0" assert snapshot["deviations"] == [] assert validate_retest_bundle(REPO_ROOT, release, protocol, corpus, snapshot, analysis) == [] diff --git a/implementations/python/tests/test_issue_1016_mixed_runtime_coordination.py b/implementations/python/tests/test_issue_1016_mixed_runtime_coordination.py index 26f4f0eaa..cc62a26f1 100644 --- a/implementations/python/tests/test_issue_1016_mixed_runtime_coordination.py +++ b/implementations/python/tests/test_issue_1016_mixed_runtime_coordination.py @@ -3,13 +3,16 @@ from __future__ import annotations from concurrent.futures import ThreadPoolExecutor -from threading import Barrier, Event +from dataclasses import asdict +from threading import Event, Lock import pytest from participant_crossing_fixtures import ( ACTION, + AUDIENCE, CONTROLLER, PARTICIPANT, + StaticCrossingResolver, admission_request, behavior, evidence, @@ -29,6 +32,7 @@ from raes_runtime.control_plane import RuntimeControlPlane from raes_runtime.control_plane_store import ( InMemoryControlPlaneStore, + NewClaimRejected, _snapshot_from_payload, _snapshot_payload, ) @@ -38,9 +42,12 @@ MixedRuntimeComponent, ) from raes_runtime.mixed_runtime_dispatch import mixed_recovery_target +from raes_runtime.mixed_runtime_handoff import MixedHandoffBinding from raes_runtime.mixed_runtime_state import runtime_state +from raes_runtime.participant_crossing_state_cut import canonical_crossing_digest from raes_runtime.participant_result_contracts import participant_runtime_history_transition_diagnostics from raes_runtime.registry import RuntimeTarget +from raes_runtime.time_coordinator import ReferenceTimeRuntime from sem233_flow_sink_fixtures import permit_resolver from test_issue_1014_mixed_composition_contracts import _alternative_profile, _staged_profile from test_issue_1015_mixed_staged_trial_admission import _mixed_request @@ -222,6 +229,22 @@ def _runtime_mixed_profile(): for allocation_id in ("allocation.participant", "allocation.action"): fields["allocations"][allocation_id]["controller_ref"] = CONTROLLER fields["allocations"][allocation_id]["action_authority_ref"] = "authority:red-team" + request = admission_request() + fields["edges"]["edge.sim-to-emu"].update( + crossing_subject={ + "subject_kind": "participant-action-admission", + "contract_id": "participant-action-admission-v1", + "subject_ref": f"participant-action-admission:{PARTICIPANT}:episode-1:{request.action_instance_id}", + "subject_digest": canonical_crossing_digest(asdict(request)), + "participant_address": PARTICIPANT, + "episode_id": "episode-1", + }, + audience_scope_ref=AUDIENCE, + policy=StaticCrossingResolver().policy.model_dump(mode="python"), + controller_ref=CONTROLLER, + authority_ref="authority:red-team", + disclosure_authority_ref="authority:red-team", + ) return seal_mixed_composition_profile(**fields) @@ -283,6 +306,111 @@ def permit_transition(transition, _state, _snapshot): evaluator = transition_evaluator or permit_transition transition_evaluators = {transition.evaluator_ref: evaluator for transition in profile.transitions.values()} + handoff_bindings = {} + context = request.mixed_profile_contexts[profile.profile_id] + time_model_ref, declaration = next(iter(context.time_models.items())) + time_state = ReferenceTimeRuntime().initialize(declaration, RuntimeSnapshot()).snapshot.time_model_state + assert time_state is not None + + class FixtureTimeRuntime: + def state(self, _snapshot): + return time_state + + for transition in profile.transitions.values(): + source = profile.phases[transition.source_phase_id] + target = profile.phases[transition.target_phase_id] + departing = set(source.active_component_ids) - set(target.active_component_ids) + arriving = set(target.active_component_ids) - set(source.active_component_ids) + if len(departing) != 1 or len(arriving) != 1: + continue + source_id, destination_id = next(iter(departing)), next(iter(arriving)) + owner = {"component": source_id, "revision": 0} + owner_lock = Lock() + source_clock = next( + address for address, clock in declaration.clocks.items() if clock.authority_ref == source_id + ) + destination_clock = next( + address for address, clock in declaration.clocks.items() if clock.authority_ref == destination_id + ) + mapping_ref = next(iter(declaration.mappings)) + + def coordinate( + operation_id, + _transition, + state, + *, + _source=source_clock, + _destination=destination_clock, + _mapping=mapping_ref, + ): + return { + "operation_id": operation_id, + "mapping_ref": _mapping, + "ordering_basis": "partial_order", + "order_ref": f"order:native:{operation_id}", + "comparison": "ordered", + "source_coordinate": state.clocks[_source].coordinate.model_dump(mode="json"), + "destination_coordinate": state.clocks[_destination].coordinate.model_dump(mode="json"), + "mapping_evidence_refs": ["evidence:handoff-mapping"], + "timing_evidence_refs": ["evidence:phase-realization"], + } + + def invoke( + operation_id, + admitted, + state, + _snapshot, + *, + _owner=owner, + _lock=owner_lock, + _source=source_id, + _destination=destination_id, + ): + with _lock: + permitted = _owner["component"] == _source and _owner["revision"] == state.phase_revision + if permitted: + _owner.update(component=_destination, revision=state.phase_revision + 1) + return { + "operation_id": operation_id, + "transition_id": admitted.transition_id, + "source_component_id": _source, + "destination_component_id": _destination, + "predecessor_history_head": state.history_head, + "phase_revision": state.phase_revision, + "status": "committed" if permitted else "stale", + "order_ref": f"order:native:{operation_id}", + "evidence_refs": [item.evidence_ref for item in admitted.evidence_bindings], + } + + def readback(operation_id, _snapshot, *, _owner=owner, _lock=owner_lock): + with _lock: + component = _owner["component"] + revision = _owner["revision"] + return { + "operation_id": operation_id, + "owner_component_id": component, + "owner_ref": profile.components[component].native_ownership_ref, + "phase_revision": revision, + "evidence_refs": ["evidence:native-readback"], + } + + handoff_bindings[transition.transition_id] = MixedHandoffBinding( + transition_id=transition.transition_id, + source_component_id=source_id, + destination_component_id=destination_id, + source_owner_ref=profile.components[source_id].native_ownership_ref, + destination_owner_ref=profile.components[destination_id].native_ownership_ref, + time_model_ref=time_model_ref, + time_model_digest=context.time_model_digests[time_model_ref], + source_clock_address=source_clock, + destination_clock_address=destination_clock, + mapping_ref=mapping_ref, + ordering_basis="partial_order", + time_runtime=FixtureTimeRuntime(), + coordinate=coordinate, + invoke=invoke, + readback=readback, + ) return ( MixedRuntimeBinding( plan=compiled.plan, @@ -291,12 +419,19 @@ def permit_transition(transition, _state, _snapshot): context=request.mixed_profile_contexts[profile.profile_id], components=components, transition_evaluators=transition_evaluators, + handoff_bindings=handoff_bindings, ), entry.run_id, runtimes, ) +def _staged_time_snapshot(binding: MixedRuntimeBinding) -> RuntimeSnapshot: + empty = RuntimeSnapshot() + installed = next(iter(binding.handoff_bindings.values())) + return empty.with_entries({}, time_model_state=installed.time_runtime.state(empty)) + + def test_mixed_runtime_activation_commits_the_admitted_initial_phase() -> None: binding, run_id, _ = _admitted_binding() plane = RuntimeControlPlane( @@ -366,8 +501,6 @@ def test_action_dispatch_commits_exact_provider_cut_before_effect() -> None: "decision", "attempt", "result", - "delivery", - "observation", ] decision = next( event for event in plane.snapshot.mixed_composition_history[run_id] if event["event_kind"] == "decision" @@ -377,39 +510,6 @@ def test_action_dispatch_commits_exact_provider_cut_before_effect() -> None: assert decision["crossing_event_ref"] -def test_mixed_action_dispatch_resolves_the_admitted_edge_and_clock_mapping() -> None: - binding, run_id, runtimes = _admitted_binding(_runtime_mixed_profile) - plane = RuntimeControlPlane( - create_stub_target(with_participant_runtime=False), - mixed_runtime=binding, - crossing_policy_resolver=permit_resolver(), - run_scope=f"run:{run_id}", - ) - plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") - plane.initialize_participant_episode(PARTICIPANT, episode_id="episode-1", identity=identity()) - - receipt = plane.admit_participant_action( - behavior(), - admission_request(), - identity=identity(), - crossing_evidence=evidence(), - idempotency_key="mixed-edge-action", - ) - - assert runtimes["sim"].admission_count == 0 - assert runtimes["emu"].admission_count == 1 - decision = next( - event for event in plane.snapshot.mixed_composition_history[run_id] if event["event_kind"] == "decision" - ) - assert decision["edge_id"] == "edge.sim-to-emu" - assert decision["mapping_ref"] == "time.mappings.sim-to-emu" - assert decision["mapping_loss_refs"] == ["limitation:mapping"] - assert plane.snapshot.mixed_composition_history[run_id][-1]["event_kind"] == "weakening" - record = plane._store.load_records()[receipt.operation_id] - assert mixed_recovery_target(plane, record.receipt.operation_id) is binding.components["emu"].target - assert mixed_recovery_target(plane, "unknown-operation") is None - - def test_backend_rejection_appends_failure_without_delivery() -> None: binding, run_id, runtimes = _admitted_binding(_runtime_profile, failing_component="sim") plane = RuntimeControlPlane( @@ -550,6 +650,7 @@ def evaluate(transition, state, _snapshot): mixed_runtime=binding, crossing_policy_resolver=permit_resolver(), run_scope=f"run:{run_id}", + initial_snapshot=_staged_time_snapshot(binding), ) plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") plane.initialize_participant_episode(PARTICIPANT, episode_id="episode-1", identity=identity()) @@ -619,6 +720,7 @@ def evaluate(transition, state, _snapshot): mixed_runtime=binding, crossing_policy_resolver=permit_resolver(), run_scope=f"run:{run_id}", + initial_snapshot=_staged_time_snapshot(binding), ) first.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") first.initialize_participant_episode(PARTICIPANT, episode_id="episode-1", identity=identity()) @@ -673,6 +775,7 @@ def fail_with_sensitive_detail(*_args): mixed_runtime=binding, crossing_policy_resolver=permit_resolver(), run_scope=f"run:{run_id}", + initial_snapshot=_staged_time_snapshot(binding), ) plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") @@ -693,10 +796,12 @@ def fail_with_sensitive_detail(*_args): def test_concurrent_phase_progression_commits_one_cas_winner() -> None: - barrier = Barrier(2) + started = Event() + release = Event() def evaluate(transition, _state, _snapshot): - barrier.wait(timeout=5) + started.set() + assert release.wait(timeout=5) return MixedPhaseTransitionEvaluation( permitted=True, attempts=1, @@ -710,6 +815,7 @@ def evaluate(transition, _state, _snapshot): mixed_runtime=binding, crossing_policy_resolver=permit_resolver(), run_scope=f"run:{run_id}", + initial_snapshot=_staged_time_snapshot(binding), ) first.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") second = RuntimeControlPlane( @@ -720,20 +826,26 @@ def evaluate(transition, _state, _snapshot): store=first._store, ) - def advance(plane, key): + with ThreadPoolExecutor(max_workers=1) as pool: + future = pool.submit( + first.advance_mixed_composition, + "transition.sim-to-emu", + identity=identity(), + idempotency_key="advance-a", + ) + assert started.wait(timeout=5) try: - return plane.advance_mixed_composition( - "transition.sim-to-emu", - identity=identity(), - idempotency_key=key, - ) - except ValueError as exc: - return exc - - with ThreadPoolExecutor(max_workers=2) as pool: - outcomes = list(pool.map(advance, (first, second), ("advance-a", "advance-b"))) + actor = identity() + with pytest.raises(NewClaimRejected): + second.advance_mixed_composition( + "transition.sim-to-emu", + identity=actor, + idempotency_key="advance-b", + ) + finally: + release.set() + future.result(timeout=5) - assert sum(not isinstance(outcome, Exception) for outcome in outcomes) == 1 snapshot = first._store.load_snapshot() assert snapshot.mixed_composition_states[run_id]["phase_revision"] == 1 assert [event["event_kind"] for event in snapshot.mixed_composition_history[run_id]].count("phase-transition") == 1 diff --git a/implementations/python/tests/test_issue_1355_mixed_mapping_time.py b/implementations/python/tests/test_issue_1355_mixed_mapping_time.py new file mode 100644 index 000000000..62f965db7 --- /dev/null +++ b/implementations/python/tests/test_issue_1355_mixed_mapping_time.py @@ -0,0 +1,1206 @@ +"""Executable mixed-edge and stage-evidence regressions for issue #1355.""" + +from __future__ import annotations + +from dataclasses import replace + +import pytest +import raes_runtime.control_plane_recovery as recovery_module +from participant_crossing_fixtures import ACTION, PARTICIPANT, admission_request, behavior, evidence, identity +from raes_backend_protocols.recovery_observation import RecoveryEffectClassification +from raes_backend_stubs.stubs import create_stub_target +from raes_contracts.contracts import seal_mixed_composition_profile +from raes_contracts.contracts.time_model import ClockTransitionEventModel, RuntimeClockStateModel, TimeRuntimeStateModel +from raes_contracts.operation_lifecycle import OperationAdmissionContext +from raes_contracts.planning import RuntimeDomain +from raes_contracts.runtime_state import ( + ApplyResult, + OperationKind, + OperationReceipt, + OperationState, + OperationStatus, + RuntimeSnapshot, +) +from raes_runtime.control_plane import RuntimeControlPlane +from raes_runtime.control_plane_health import control_plane_readiness +from raes_runtime.control_plane_recovery import ( + IndeterminateResolutionDisposition, + unresolved_indeterminate_operation_ids_from_records, +) +from raes_runtime.control_plane_store import ControlPlaneOperationRecord, InMemoryControlPlaneStore, NewClaimRejected +from raes_runtime.control_plane_store_local import LocalControlPlaneStore +from raes_runtime.mixed_runtime_dispatch import mixed_recovery_target +from raes_runtime.mixed_runtime_edge import MixedEdgeExecutionBinding, MixedTimeCoordinationEvidence +from raes_runtime.mixed_runtime_edge_execution import _require_time_grant +from raes_runtime.mixed_runtime_handoff_execution import _require_handoff_time_grant +from raes_runtime.participant_crossing_mediation import validate_persisted_crossing_history +from raes_runtime.time_coordinator import ReferenceTimeRuntime +from sem233_flow_sink_fixtures import permit_resolver +from test_issue_1016_mixed_runtime_coordination import ( + _admitted_binding, + _runtime_mixed_profile, + _runtime_profile, + _runtime_staged_profile, + _staged_time_snapshot, +) + + +@pytest.mark.parametrize("store_kind", ["memory", "local"]) +def test_phase_and_action_claims_exclude_each_other_at_the_store(tmp_path, store_kind) -> None: + store = InMemoryControlPlaneStore() if store_kind == "memory" else LocalControlPlaneStore(tmp_path / "claims") + lease = store.admit_runtime(target_scope="target:1355", run_scope="run:run-1355") if store_kind == "local" else None + history_key = "mixed_composition_history:run-1355" + + def record(operation_id, kind): + context = OperationAdmissionContext( + actor_id="actor-1355", + authorization_scope=("participant-control",), + target_scope="target:1355", + run_scope="run:run-1355", + operation_kind=kind, + request_commitment="sha256:" + "a" * 64, + ) + receipt = OperationReceipt( + operation_id=operation_id, + domain=RuntimeDomain.PARTICIPANT, + submitted_at="2026-09-24T00:00:00Z", + accepted=True, + context=context, + ) + return ControlPlaneOperationRecord( + receipt=receipt, + status=OperationStatus( + operation_id=operation_id, + domain=receipt.domain, + state=OperationState.RUNNING, + submitted_at=receipt.submitted_at, + updated_at=receipt.submitted_at, + context=context, + ), + decision_history_heads={history_key: None}, + result_history_heads={history_key: None}, + ) + + phase = record("phase-1355", OperationKind.COMPOSITION_PHASE) + action = record("action-1355", OperationKind.PARTICIPANT_ACTION) + assert store.claim_record(phase) == phase + with pytest.raises(NewClaimRejected): + store.claim_record(action) + store.save_record(replace(phase, status=replace(phase.status, state=OperationState.SUCCEEDED))) + assert store.claim_record(action) == action + second_action = record("action-1355-b", OperationKind.PARTICIPANT_ACTION) + second_phase = record("phase-1355-b", OperationKind.COMPOSITION_PHASE) + with pytest.raises(NewClaimRejected): + store.claim_record(second_action) + with pytest.raises(NewClaimRejected): + store.claim_record(second_phase) + store.save_record(replace(action, status=replace(action.status, state=OperationState.SUCCEEDED))) + assert store.claim_record(record("action-1355-c", OperationKind.PARTICIPANT_ACTION)).receipt.operation_id == ( + "action-1355-c" + ) + if lease is not None: + lease.close() + + +def test_backend_success_does_not_invent_delivery_or_observation() -> None: + binding, run_id, runtimes = _admitted_binding(_runtime_profile) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + plane.initialize_participant_episode(PARTICIPANT, episode_id="episode-1", identity=identity()) + + receipt = plane.admit_participant_action( + behavior(), + admission_request(), + identity=identity(), + crossing_evidence=evidence(), + idempotency_key="unproven-delivery", + ) + + assert receipt.accepted + assert runtimes["sim"].admission_count == 1 + kinds = [event["event_kind"] for event in plane.snapshot.mixed_composition_history[run_id]] + assert kinds[-3:] == ["decision", "attempt", "result"] + assert "delivery" not in kinds + assert "observation" not in kinds + + +def test_unbound_mixed_edge_refuses_before_bridge_or_provider_call() -> None: + binding, run_id, runtimes = _admitted_binding(_runtime_mixed_profile) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + plane.initialize_participant_episode(PARTICIPANT, episode_id="episode-1", identity=identity()) + + action, admission, actor, crossing = behavior(), admission_request(), identity(), evidence() + with pytest.raises(ValueError, match="executable edge binding"): + plane.admit_participant_action( + action, + admission, + identity=actor, + crossing_evidence=crossing, + idempotency_key="unbound-edge", + ) + + assert all(runtime.admission_count == 0 for runtime in runtimes.values()) + + +def test_metadata_only_edge_binding_cannot_admit_mixed_execution() -> None: + original, _, _ = _admitted_binding(_runtime_mixed_profile) + + with pytest.raises(TypeError, match="executable edge binding"): + replace(original, edge_bindings={"edge.sim-to-emu": object()}) + + +def _executable_edge_plane( + *, + deliver: bool = True, + observe: bool = True, + execution_status: str = "succeeded", + fail_after_provider: bool = False, + change_terminal_requirement: bool = False, + stage_readback: bool = True, + stale_time_readback: bool = False, + stale_post_time_readback: bool = False, + destination_action_address: str = ACTION, + fail_stage: str | None = None, + profile_factory=_runtime_mixed_profile, +): + binding, run_id, runtimes = _admitted_binding(profile_factory) + edge = binding.profile.edges["edge.sim-to-emu"] + declaration = binding.context.time_models[edge.time_binding.time_model_ref] + time_runtime = ReferenceTimeRuntime() + initial_time = time_runtime.initialize(declaration, RuntimeSnapshot()).snapshot + if stale_time_readback or stale_post_time_readback: + original_readback = time_runtime.state + + def stale_readback(snapshot): + state = original_readback(snapshot) + if stale_time_readback or runtimes["emu"].admission_count > 0: + return state.model_copy(update={"declaration_digest": "sha256:" + "0" * 64}) + return state + + time_runtime.state = stale_readback + calls: list[str] = [] + + def map_action(request): + calls.append("map") + return replace( + request, + action_contract_address=destination_action_address, + requires_terminal_outcome=( + not request.requires_terminal_outcome + if change_terminal_requirement + else request.requires_terminal_outcome + ), + ) + + def coordinate(operation_id, admitted_edge, time_state): + calls.append("coordinate") + assert admitted_edge.edge_id == edge.edge_id + source = time_state.clocks[edge.time_binding.source_clock_address].coordinate + destination = time_state.clocks[edge.time_binding.target_clock_address].coordinate + return { + "operation_id": operation_id, + "mapping_ref": edge.time_binding.mapping_address, + "ordering_basis": edge.time_binding.ordering_basis, + "order_ref": f"order:bridge:{operation_id}", + "comparison": "ordered", + "source_coordinate": source.model_dump(mode="json"), + "destination_coordinate": destination.model_dump(mode="json"), + "mapping_evidence_refs": ["evidence:mapping-call"], + "timing_evidence_refs": ["evidence:time-grant", "evidence:edge-realization"], + } + + def bridge(operation_id, request, snapshot, provider_call): + calls.append("bridge") + result = provider_call(request, snapshot) + if fail_after_provider: + raise RuntimeError("private bridge outcome") + return result, { + "operation_id": operation_id, + "bridge_ref": edge.routing_ref, + "bridge_version": "1", + "bridge_digest": "sha256:" + "1" * 64, + "source_action_address": ACTION, + "destination_action_address": destination_action_address, + "execution_status": execution_status, + "execution_evidence_refs": ["evidence:backend-readback"], + "delivery_evidence_refs": ["evidence:destination-receipt"] if deliver else [], + "observation_evidence_refs": ["evidence:participant-readback"] if observe else [], + "mapping_loss_refs": [edge.mapping_loss.limitation_ref], + "cessation_evidence_refs": ["evidence:provider-cessation"] if execution_status == "failed" else [], + } + + def delivery_readback(operation_id, _snapshot): + calls.append("delivery-readback") + if fail_stage == "delivery": + raise RuntimeError("private destination readback failure") + return { + "operation_id": operation_id, + "destination_component_id": edge.target_component_id, + "receipt_ref": f"receipt:{operation_id}", + "evidence_refs": ["evidence:destination-receipt"], + } + + def observation_readback(operation_id, _snapshot): + calls.append("observation-readback") + if fail_stage == "observation": + raise RuntimeError("private participant readback failure") + return { + "operation_id": operation_id, + "participant_address": PARTICIPANT, + "audience_ref": edge.audience_scope_ref, + "observation_ref": f"observation:{operation_id}", + "evidence_refs": ["evidence:participant-readback"], + } + + executable = MixedEdgeExecutionBinding( + edge_id=edge.edge_id, + bridge_ref=edge.routing_ref, + bridge_version="1", + bridge_digest="sha256:" + "1" * 64, + source_action_address=ACTION, + destination_action_address=destination_action_address, + mapping_ref=edge.time_binding.mapping_address, + mapping_loss_ref=edge.mapping_loss.limitation_ref, + time_runtime=time_runtime, + map_action=map_action, + coordinate=coordinate, + bridge=bridge, + delivery_readback=delivery_readback if stage_readback else None, + observation_readback=observation_readback if stage_readback else None, + ) + binding = replace(binding, edge_bindings={edge.edge_id: executable}) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + store=InMemoryControlPlaneStore(snapshot=initial_time), + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + plane.initialize_participant_episode(PARTICIPANT, episode_id="episode-1", identity=identity()) + return plane, run_id, runtimes, calls, time_runtime + + +def test_mapped_edge_invokes_bridge_and_records_distinct_evidenced_stages() -> None: + plane, run_id, runtimes, calls, _ = _executable_edge_plane() + + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key="mapped" + ) + + assert receipt.accepted + assert calls == ["map", "coordinate", "bridge", "delivery-readback", "observation-readback"] + assert runtimes["sim"].admission_count == 0 + assert runtimes["emu"].admission_count == 1 + kinds = [event["event_kind"] for event in plane.snapshot.mixed_composition_history[run_id]] + assert kinds[-6:] == ["decision", "attempt", "result", "delivery", "observation", "weakening"] + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "succeeded" + assert mixed_recovery_target(plane, receipt.operation_id) is plane._mixed_runtime.components["emu"].target + + +def _reversed_microstep_state(state, source_address, destination_address): + clocks = dict(state.clocks) + for address, microstep in ((source_address, 2), (destination_address, 1)): + clock = clocks[address] + coordinate = clock.coordinate.model_copy(update={"microstep": microstep}) + event = ClockTransitionEventModel( + sequence=clock.sequence + 1, + kind="advance", + previous=clock.coordinate, + resulting=coordinate, + resulting_state=clock.state, + ) + clocks[address] = RuntimeClockStateModel.model_validate( + clock.model_copy( + update={ + "coordinate": coordinate, + "sequence": event.sequence, + "history": [*clock.history, event], + } + ).model_dump(mode="python") + ) + return TimeRuntimeStateModel.model_validate(state.model_copy(update={"clocks": clocks}).model_dump(mode="python")) + + +def test_edge_order_grant_rejects_reversed_microsteps() -> None: + binding, _, _ = _admitted_binding(_runtime_mixed_profile) + edge = binding.profile.edges["edge.sim-to-emu"] + declaration = binding.context.time_models[edge.time_binding.time_model_ref] + state = ReferenceTimeRuntime().initialize(declaration, RuntimeSnapshot()).snapshot.time_model_state + assert state is not None + state = _reversed_microstep_state( + state, edge.time_binding.source_clock_address, edge.time_binding.target_clock_address + ) + installed = _executable_edge_plane()[0]._mixed_runtime.edge_bindings[edge.edge_id] + grant = MixedTimeCoordinationEvidence.model_validate(installed.coordinate("operation:microsteps", edge, state)) + + with pytest.raises(ValueError, match="governed order is unsupported"): + _require_time_grant( + grant, + "operation:microsteps", + edge, + declaration.mappings[edge.time_binding.mapping_address], + state, + ) + + +def test_handoff_order_grant_rejects_reversed_microsteps() -> None: + binding, _, _ = _admitted_binding(_runtime_staged_profile) + transition = binding.profile.transitions["transition.sim-to-emu"] + installed = binding.handoff_bindings[transition.transition_id] + declaration = binding.context.time_models[installed.time_model_ref] + state = _staged_time_snapshot(binding).time_model_state + assert state is not None + state = _reversed_microstep_state(state, installed.source_clock_address, installed.destination_clock_address) + grant = MixedTimeCoordinationEvidence.model_validate( + installed.coordinate("operation:microsteps", transition, state) + ) + + with pytest.raises(ValueError, match="handoff time coordination is unsupported"): + _require_handoff_time_grant(installed, grant, "operation:microsteps", declaration, state, transition) + + +@pytest.mark.parametrize("stale_post_time_readback", [False, True]) +def test_rejected_backend_result_cannot_publish_successful_mixed_stages(stale_post_time_readback) -> None: + plane, run_id, runtimes, calls, _ = _executable_edge_plane(stale_post_time_readback=stale_post_time_readback) + runtime = runtimes["emu"] + original = runtime.admit_action + + def invalid_changed_address(request, snapshot): + result = original(request, snapshot) + return replace(result, changed_addresses=["participant.unadmitted-address"]) + + runtime.admit_action = invalid_changed_address + receipt = plane.admit_participant_action( + behavior(), + admission_request(), + identity=identity(), + crossing_evidence=evidence(), + idempotency_key="invalid-result", + ) + + assert runtime.admission_count == 1 + assert calls == ["map", "coordinate", "bridge"] + assert plane.get_operation(receipt.operation_id, identity=identity()).state is OperationState.INDETERMINATE + events = plane.snapshot.mixed_composition_history[run_id] + result = next(event for event in events if event["event_kind"] == "result") + assert result["disposition"] == "indeterminate" + assert "evidence:backend-readback" not in result["evidence_refs"] + assert not any(event["event_kind"] in {"delivery", "observation", "weakening"} for event in events) + + +def test_failed_bridge_retains_correlation_and_cessation_evidence() -> None: + plane, run_id, runtimes, _, _ = _executable_edge_plane(deliver=False, observe=False, execution_status="failed") + runtime = runtimes["emu"] + original = runtime.admit_action + + def provider_failure(request, snapshot): + original(request, snapshot) + return ApplyResult(success=False, snapshot=snapshot) + + runtime.admit_action = provider_failure + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key="failed" + ) + + assert runtime.admission_count == 1 + assert plane.get_operation(receipt.operation_id, identity=identity()).state is OperationState.FAILED + events = plane.snapshot.mixed_composition_history[run_id] + assert [event["event_kind"] for event in events[-2:]] == ["result", "failure"] + assert all("evidence:provider-cessation" in event["evidence_refs"] for event in events[-2:]) + + +@pytest.mark.parametrize( + ("field", "replacement"), + [ + ("audience_scope_ref", "audience:unrelated"), + ("crossing_subject.subject_ref", "participant-action-admission:unrelated"), + ("policy.policy_decision_ref", "decision:unrelated"), + ("disclosure_authority_ref", "authority:unrelated"), + ], +) +def test_edge_authority_must_match_the_authorized_crossing_before_effect(field, replacement) -> None: + def changed_edge_profile(): + profile = _runtime_mixed_profile() + fields = profile.model_dump(mode="python", exclude={"profile_digest"}) + edge = fields["edges"]["edge.sim-to-emu"] + if "." in field: + parent, child = field.split(".", 1) + edge[parent][child] = replacement + else: + edge[field] = replacement + return seal_mixed_composition_profile(**fields) + + plane, _, runtimes, calls, _ = _executable_edge_plane(profile_factory=changed_edge_profile) + action, admission, actor, crossing = behavior(), admission_request(), identity(), evidence() + with pytest.raises(ValueError, match="mixed edge differs from the authorized crossing"): + plane.admit_participant_action( + action, + admission, + identity=actor, + crossing_evidence=crossing, + idempotency_key="wrong-audience", + ) + + assert all(runtime.admission_count == 0 for runtime in runtimes.values()) + assert calls == [] + + +def test_partial_bridge_report_preserves_execution_evidence_without_delivery_claim() -> None: + plane, run_id, runtimes, _, _ = _executable_edge_plane(deliver=False, observe=False, execution_status="partial") + + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key="partial" + ) + + assert runtimes["emu"].admission_count == 1 + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "indeterminate" + events = plane.snapshot.mixed_composition_history[run_id] + execution = next(event for event in events if event["event_kind"] == "result") + assert execution["disposition"] == "indeterminate" + assert "evidence:backend-readback" in execution["evidence_refs"] + assert not any(event["event_kind"] in {"delivery", "observation"} for event in events) + + +def test_bridge_report_without_destination_readback_cannot_claim_delivery() -> None: + plane, run_id, runtimes, calls, _ = _executable_edge_plane(stage_readback=False) + + receipt = plane.admit_participant_action( + behavior(), + admission_request(), + identity=identity(), + crossing_evidence=evidence(), + idempotency_key="no-readback", + ) + + assert runtimes["emu"].admission_count == 1 + assert calls == ["map", "coordinate", "bridge"] + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "indeterminate" + assert not any( + event["event_kind"] in {"delivery", "observation"} for event in plane.snapshot.mixed_composition_history[run_id] + ) + + +@pytest.mark.parametrize("fail_stage", ["delivery", "observation"]) +def test_later_readback_failure_retains_known_execution_and_only_confirmed_stages(fail_stage) -> None: + plane, run_id, runtimes, _, _ = _executable_edge_plane(fail_stage=fail_stage) + + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key=fail_stage + ) + + assert runtimes["emu"].admission_count == 1 + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "indeterminate" + events = plane.snapshot.mixed_composition_history[run_id] + result = next(event for event in events if event["event_id"] == f"composition:{receipt.operation_id}:result") + assert result["disposition"] == "indeterminate" + assert "evidence:backend-readback" in result["evidence_refs"] + kinds = [event["event_kind"] for event in events] + assert ("delivery" in kinds) is (fail_stage == "observation") + assert "observation" not in kinds + assert "weakening" in kinds + assert ( + plane._mixed_runtime.profile.edges["edge.sim-to-emu"].mapping_loss.limitation_ref in result["mapping_loss_refs"] + ) + + +def test_stale_time_readback_refuses_before_bridge_or_provider() -> None: + plane, run_id, runtimes, calls, _ = _executable_edge_plane(stale_time_readback=True) + + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key="stale-time" + ) + + assert calls == ["map"] + assert all(runtime.admission_count == 0 for runtime in runtimes.values()) + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "failed" + assert "delivery" not in [event["event_kind"] for event in plane.snapshot.mixed_composition_history[run_id]] + events = plane.snapshot.mixed_composition_history[run_id] + assert events[-1]["event_kind"] == "failure" + assert events[-2]["event_kind"] == "result" + assert events[-2]["mapping_loss_refs"] == [] + assert events[-3]["mapping_loss_refs"] == [ + plane._mixed_runtime.profile.edges["edge.sim-to-emu"].mapping_loss.limitation_ref + ] + + +def test_post_execution_stale_time_keeps_backend_evidence_without_governed_order() -> None: + plane, run_id, runtimes, _, _ = _executable_edge_plane(stale_post_time_readback=True) + + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key="post-stale" + ) + + assert runtimes["emu"].admission_count == 1 + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "indeterminate" + result = next( + event + for event in plane.snapshot.mixed_composition_history[run_id] + if event["event_id"] == f"composition:{receipt.operation_id}:result" + ) + assert result["disposition"] == "indeterminate" + assert "evidence:backend-readback" in result["evidence_refs"] + assert not result["order_ref"].startswith("order:bridge:") + assert not any( + event["event_kind"] in {"delivery", "observation", "weakening"} + for event in plane.snapshot.mixed_composition_history[run_id] + ) + + +def test_timestamp_only_edge_cannot_claim_governed_order() -> None: + def timestamp_profile(): + source = _runtime_mixed_profile() + fields = source.model_dump(mode="python", exclude={"profile_digest"}) + fields["edges"]["edge.sim-to-emu"]["time_binding"]["ordering_basis"] = "wall_clock_only" + return seal_mixed_composition_profile(**fields) + + plane, run_id, runtimes, calls, _ = _executable_edge_plane(profile_factory=timestamp_profile) + + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key="weak-clock" + ) + + assert calls == ["map", "coordinate"] + assert all(runtime.admission_count == 0 for runtime in runtimes.values()) + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "failed" + assert "delivery" not in [event["event_kind"] for event in plane.snapshot.mixed_composition_history[run_id]] + + +def test_unknown_bridge_outcome_is_indeterminate_and_replay_never_reinvokes() -> None: + plane, run_id, runtimes, calls, _ = _executable_edge_plane(fail_after_provider=True) + action_behavior = behavior() + request = admission_request() + caller = identity() + crossing = evidence() + + receipt = plane.admit_participant_action( + action_behavior, + request, + identity=caller, + crossing_evidence=crossing, + idempotency_key="unknown-bridge", + ) + replay = plane.admit_participant_action( + action_behavior, + request, + identity=caller, + crossing_evidence=crossing, + idempotency_key="unknown-bridge", + ) + + assert replay.operation_id == receipt.operation_id + assert runtimes["emu"].admission_count == 1 + assert calls == ["map", "coordinate", "bridge"] + assert plane.get_operation(receipt.operation_id, identity=caller).state.value == "indeterminate" + assert plane.snapshot.mixed_composition_history[run_id][-1]["disposition"] == "indeterminate" + assert "private bridge outcome" not in repr(plane.get_operation(receipt.operation_id, identity=caller).diagnostics) + + +def test_mapping_cannot_expand_the_authorized_action_carrier() -> None: + plane, _, runtimes, calls, _ = _executable_edge_plane(change_terminal_requirement=True) + + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key="bad-map" + ) + + assert receipt.accepted + assert calls == ["map"] + assert all(runtime.admission_count == 0 for runtime in runtimes.values()) + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "failed" + + +@pytest.mark.parametrize("mutator", ["mapper", "bridge"]) +def test_mutable_action_carrier_cannot_escape_authorized_mapping(mutator) -> None: + plane, _, runtimes, _, _ = _executable_edge_plane() + binding = plane._mixed_runtime + assert binding is not None + edge = binding.edge_bindings["edge.sim-to-emu"] + original_map, original_bridge = edge.map_action, edge.bridge + + def mutating_map(request): + request.implementation_manifest.constraints["unauthorized"] = "injected" + return original_map(request) + + def mutating_bridge(operation_id, request, snapshot, provider_call): + request.implementation_manifest.constraints["unauthorized"] = "injected" + return original_bridge(operation_id, request, snapshot, provider_call) + + changed = replace( + edge, + map_action=mutating_map if mutator == "mapper" else original_map, + bridge=mutating_bridge if mutator == "bridge" else original_bridge, + ) + plane._mixed_runtime = replace(binding, edge_bindings={edge.edge_id: changed}) + request = admission_request() + receipt = plane.admit_participant_action( + behavior(), request, identity=identity(), crossing_evidence=evidence(), idempotency_key=f"mutating-{mutator}" + ) + + assert all(runtime.admission_count == 0 for runtime in runtimes.values()) + assert "unauthorized" not in request.implementation_manifest.constraints + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "failed" + + +def test_bridge_cannot_change_snapshot_before_the_provider_call() -> None: + plane, _, runtimes, _, _ = _executable_edge_plane() + binding = plane._mixed_runtime + assert binding is not None + installed = binding.edge_bindings["edge.sim-to-emu"] + + def mutating_bridge(operation_id, request, snapshot, provider_call): + snapshot.metadata["forged-by-bridge"] = True + return installed.bridge(operation_id, request, snapshot, provider_call) + + changed = replace(installed, bridge=mutating_bridge) + plane._mixed_runtime = replace(binding, edge_bindings={changed.edge_id: changed}) + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key="bad-cut" + ) + + assert runtimes["emu"].admission_count == 0 + assert plane.get_operation(receipt.operation_id, identity=identity()).state is OperationState.FAILED + assert "forged-by-bridge" not in plane.snapshot.metadata + + +@pytest.mark.parametrize("mutator", ["time-readback", "coordinate"]) +def test_time_callbacks_cannot_mutate_the_provider_snapshot(mutator) -> None: + plane, _, runtimes, _, time_runtime = _executable_edge_plane() + binding = plane._mixed_runtime + assert binding is not None + installed = binding.edge_bindings["edge.sim-to-emu"] + original_state = time_runtime.state + + def mutating_state(snapshot): + snapshot.metadata["forged-by-time"] = True + return original_state(snapshot) + + def mutating_coordinate(operation_id, edge, state): + grant = installed.coordinate(operation_id, edge, state) + state.clocks["clock.forged"] = next(iter(state.clocks.values())) + return grant + + changed = replace(installed, coordinate=mutating_coordinate if mutator == "coordinate" else installed.coordinate) + if mutator == "time-readback": + time_runtime.state = mutating_state + plane._mixed_runtime = replace(binding, edge_bindings={changed.edge_id: changed}) + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key=mutator + ) + + assert runtimes["emu"].admission_count == 1 + assert plane.get_operation(receipt.operation_id, identity=identity()).state is OperationState.SUCCEEDED + assert "forged-by-time" not in plane.snapshot.metadata + assert "clock.forged" not in plane.snapshot.time_model_state.clocks + + +def test_interrupted_mixed_edge_cannot_recover_from_provider_observation_alone(monkeypatch) -> None: + class Interrupted(BaseException): + pass + + plane, run_id, runtimes, _, _ = _executable_edge_plane() + binding = plane._mixed_runtime + assert binding is not None + edge = binding.edge_bindings["edge.sim-to-emu"] + + def interrupted_bridge(operation_id, request, snapshot, provider_call): + provider_call(request, snapshot) + raise Interrupted + + plane._mixed_runtime = replace(binding, edge_bindings={edge.edge_id: replace(edge, bridge=interrupted_bridge)}) + action, admission, actor, crossing = behavior(), admission_request(), identity(), evidence() + with pytest.raises(Interrupted): + plane.admit_participant_action( + action, + admission, + identity=actor, + crossing_evidence=crossing, + idempotency_key="crashed-edge", + ) + pending = next( + record for record in plane._store.load_records().values() if record.idempotency_key == "crashed-edge" + ) + assert pending.status.state is OperationState.RUNNING + assert runtimes["emu"].admission_count == 1 + + def provider_only_observation(control_plane, _record, _target): + return RecoveryEffectClassification.EFFECT_APPLIED, ApplyResult(success=True, snapshot=control_plane._snapshot) + + monkeypatch.setattr(recovery_module, "_observe_recovery_target", provider_only_observation) + + restarted = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=plane._mixed_runtime, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + store=plane._store, + ) + assert ( + restarted.get_operation(pending.receipt.operation_id, identity=identity()).state is OperationState.INDETERMINATE + ) + assert restarted.snapshot.mixed_composition_history[run_id][-1]["event_kind"] == "attempt" + assert control_plane_readiness(restarted).to_payload()["status"] == "unready" + actor = identity() + with pytest.raises(ValueError, match="mixed stage reconciliation is required"): + restarted.resolve_indeterminate_operation( + pending.receipt.operation_id, + disposition=IndeterminateResolutionDisposition.ACCEPT_CURRENT_SNAPSHOT, + idempotency_key="accept-partial-cut", + identity=actor, + ) + plane._store.load_snapshot().participant_crossing_history["participant.behavior.unrelated"] = [{}] + target = create_stub_target(with_participant_runtime=False) + resolver = permit_resolver() + with pytest.raises(ValueError): + RuntimeControlPlane( + target, + mixed_runtime=plane._mixed_runtime, + crossing_policy_resolver=resolver, + run_scope=f"run:{run_id}", + store=plane._store, + ) + + +def test_valid_mixed_crossing_cannot_clear_missing_stages_by_generic_resolution() -> None: + plane, run_id, _, _, _ = _executable_edge_plane(deliver=False, observe=False, execution_status="partial") + receipt = plane.admit_participant_action( + behavior(), admission_request(), identity=identity(), crossing_evidence=evidence(), idempotency_key="partial" + ) + assert plane.get_operation(receipt.operation_id, identity=identity()).state is OperationState.INDETERMINATE + assert plane.snapshot.participant_crossing_history[PARTICIPANT] + assert plane.snapshot.mixed_composition_history[run_id][-1]["event_kind"] == "weakening" + validate_persisted_crossing_history(plane.snapshot, plane._crossing_policy_resolver) + + actor = identity() + with pytest.raises(ValueError, match="mixed stage reconciliation is required"): + plane.resolve_indeterminate_operation( + receipt.operation_id, + disposition=IndeterminateResolutionDisposition.ACCEPT_CURRENT_SNAPSHOT, + idempotency_key="accept-partial", + identity=actor, + ) + assert control_plane_readiness(plane).to_payload()["status"] == "unready" + parent = plane._store.load_records()[receipt.operation_id] + child_context = parent.status.context.model_copy( + update={ + "operation_kind": OperationKind.INDETERMINATE_RESOLUTION, + "parent_operation_id": receipt.operation_id, + "authorization_scope": tuple(dict.fromkeys([*parent.status.context.authorization_scope, "role:operator"])), + } + ) + child = replace( + parent, + receipt=replace(parent.receipt, operation_id="historical-resolution", context=child_context), + status=replace( + parent.status, + operation_id="historical-resolution", + state=OperationState.SUCCEEDED, + context=child_context, + diagnostics=[], + ), + idempotency_key="historical-resolution", + result_payload={"resolution_disposition": IndeterminateResolutionDisposition.ACCEPT_CURRENT_SNAPSHOT.value}, + ) + assert receipt.operation_id in unresolved_indeterminate_operation_ids_from_records( + {receipt.operation_id: parent, "historical-resolution": child} + ) + history = plane._store.load_snapshot().participant_crossing_history[PARTICIPANT] + history.append({**history[-1], "event_id": "crossing-occurrence.decided.unrelated"}) + target = create_stub_target(with_participant_runtime=False) + resolver = permit_resolver() + with pytest.raises(ValueError, match="crossing result head differs"): + RuntimeControlPlane( + target, + mixed_runtime=plane._mixed_runtime, + crossing_policy_resolver=resolver, + run_scope=f"run:{run_id}", + store=plane._store, + ) + + +def test_handoff_refuses_time_readback_outside_the_stored_cut() -> None: + binding, run_id, _ = _admitted_binding(_runtime_staged_profile) + invoked: list[str] = [] + installed = binding.handoff_bindings["transition.sim-to-emu"] + + def coordinate(*_args): + invoked.append("coordinate") + return {} + + changed = replace(installed, coordinate=coordinate) + binding = replace(binding, handoff_bindings={changed.transition_id: changed}) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + + receipt = plane.advance_mixed_composition( + "transition.sim-to-emu", identity=identity(), idempotency_key="mismatched-time-cut" + ) + + assert invoked == [] + assert plane.get_operation(receipt.operation_id, identity=identity()).state is OperationState.FAILED + assert plane.snapshot.mixed_composition_states[run_id]["phase_id"] == "phase.sim" + + +@pytest.mark.parametrize("mutator", ["evaluator", "pre-time", "invoke", "readback", "post-time"]) +def test_native_handoff_callbacks_cannot_mutate_authoritative_snapshot(mutator) -> None: + binding, run_id, _ = _admitted_binding(_runtime_staged_profile) + initial_snapshot = _staged_time_snapshot(binding) + transition = binding.profile.transitions["transition.sim-to-emu"] + installed = binding.handoff_bindings[transition.transition_id] + evaluator = binding.transition_evaluators[transition.evaluator_ref] + + def changed_evaluator(admitted, state, snapshot): + snapshot.metadata["forged-by-handoff"] = mutator + return evaluator(admitted, state, snapshot) + + def changed_invoke(operation_id, admitted, state, snapshot): + snapshot.metadata["forged-by-handoff"] = mutator + return installed.invoke(operation_id, admitted, state, snapshot) + + def changed_readback(operation_id, snapshot): + snapshot.metadata["forged-by-handoff"] = mutator + return installed.readback(operation_id, snapshot) + + class ChangedTimeRuntime: + def __init__(self): + self.calls = 0 + + def state(self, snapshot): + self.calls += 1 + if (mutator == "pre-time" and self.calls == 1) or (mutator == "post-time" and self.calls == 2): + snapshot.metadata["forged-by-handoff"] = mutator + return installed.time_runtime.state(snapshot) + + if mutator == "evaluator": + binding = replace(binding, transition_evaluators={transition.evaluator_ref: changed_evaluator}) + else: + changed = replace( + installed, + invoke=changed_invoke if mutator == "invoke" else installed.invoke, + readback=changed_readback if mutator == "readback" else installed.readback, + time_runtime=ChangedTimeRuntime() if mutator in {"pre-time", "post-time"} else installed.time_runtime, + ) + binding = replace(binding, handoff_bindings={transition.transition_id: changed}) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + initial_snapshot=initial_snapshot, + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + + receipt = plane.advance_mixed_composition( + transition.transition_id, identity=identity(), idempotency_key=f"mutating-{mutator}" + ) + + assert plane.get_operation(receipt.operation_id, identity=identity()).state is OperationState.SUCCEEDED + assert "forged-by-handoff" not in plane.snapshot.metadata + assert "forged-by-handoff" not in plane._store.load_snapshot().metadata + + +def test_interrupted_native_handoff_retains_uncertain_owner_on_restart() -> None: + class Interrupted(BaseException): + pass + + binding, run_id, runtimes = _admitted_binding(_runtime_staged_profile) + installed = binding.handoff_bindings["transition.sim-to-emu"] + old_invoke = installed.invoke + + def interrupted_invoke(operation_id, transition, state, snapshot): + old_invoke(operation_id, transition, state, snapshot) + raise Interrupted + + changed = replace(installed, invoke=interrupted_invoke) + binding = replace(binding, handoff_bindings={changed.transition_id: changed}) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + initial_snapshot=_staged_time_snapshot(binding), + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + plane.initialize_participant_episode(PARTICIPANT, episode_id="episode-1", identity=identity()) + + actor = identity() + with pytest.raises(Interrupted): + plane.advance_mixed_composition("transition.sim-to-emu", identity=actor, idempotency_key="crashed-handoff") + pending = next( + record for record in plane._store.load_records().values() if record.idempotency_key == "crashed-handoff" + ) + assert pending.status.state is OperationState.RUNNING + + restarted = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + store=plane._store, + ) + assert ( + restarted.get_operation(pending.receipt.operation_id, identity=identity()).state is OperationState.INDETERMINATE + ) + assert restarted.snapshot.mixed_composition_states[run_id]["phase_id"] == "phase.sim" + assert control_plane_readiness(restarted).to_payload()["status"] == "unready" + actor = identity() + with pytest.raises(ValueError, match="mixed stage reconciliation is required"): + restarted.resolve_indeterminate_operation( + pending.receipt.operation_id, + disposition=IndeterminateResolutionDisposition.ACCEPT_CURRENT_SNAPSHOT, + idempotency_key="accept-handoff", + identity=actor, + ) + action, admission, actor, crossing = behavior(), admission_request(), identity(), evidence() + with pytest.raises(RuntimeError, match="indeterminate operation requires resolution"): + restarted.admit_participant_action( + action, + admission, + identity=actor, + crossing_evidence=crossing, + idempotency_key="old-owner", + ) + assert all(runtime.admission_count == 0 for runtime in runtimes.values()) + + +def test_native_handoff_retains_confirmed_transfer_evidence_when_readback_fails() -> None: + binding, run_id, _ = _admitted_binding(_runtime_staged_profile) + installed = binding.handoff_bindings["transition.sim-to-emu"] + + def invoke(operation_id, transition, state, snapshot): + report = installed.invoke(operation_id, transition, state, snapshot) + return {**report, "evidence_refs": [*report["evidence_refs"], "evidence:native-transfer"]} + + def failed_readback(_operation_id, _snapshot): + raise RuntimeError("owner readback unavailable") + + changed = replace(installed, invoke=invoke, readback=failed_readback) + binding = replace(binding, handoff_bindings={changed.transition_id: changed}) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + initial_snapshot=_staged_time_snapshot(binding), + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + + receipt = plane.advance_mixed_composition( + "transition.sim-to-emu", identity=identity(), idempotency_key="lost-owner-readback" + ) + + assert plane.get_operation(receipt.operation_id, identity=identity()).state is OperationState.INDETERMINATE + failure = plane.snapshot.mixed_composition_history[run_id][-1] + assert failure["event_kind"] == "failure" + assert {"evidence:handoff-mapping", "evidence:native-transfer"}.issubset(failure["evidence_refs"]) + + +def test_translated_action_outside_the_admitted_policy_cut_refuses_before_provider() -> None: + plane, _, runtimes, calls, _ = _executable_edge_plane( + destination_action_address="participant.action-contract.unadmitted" + ) + + action, admission, actor, crossing = behavior(), admission_request(), identity(), evidence() + with pytest.raises(ValueError, match="destination action differs from admitted policy"): + plane.admit_participant_action( + action, + admission, + identity=actor, + crossing_evidence=crossing, + idempotency_key="unadmitted-translation", + ) + + assert calls == [] + assert all(runtime.admission_count == 0 for runtime in runtimes.values()) + + +def test_staged_membership_change_needs_an_executable_handoff() -> None: + prepared, run_id, _ = _admitted_binding(_runtime_staged_profile) + binding = replace(prepared, handoff_bindings={}) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + initial_snapshot=_staged_time_snapshot(prepared), + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + + receipt = plane.advance_mixed_composition( + "transition.sim-to-emu", identity=identity(), idempotency_key="unbound-handoff" + ) + + assert plane.snapshot.mixed_composition_states[run_id]["phase_id"] == "phase.sim" + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "failed" + assert "handoff" not in [event["event_kind"] for event in plane.snapshot.mixed_composition_history[run_id]] + + +@pytest.mark.parametrize("readback_operation_matches", [True, False]) +def test_evidenced_staged_handoff_commits_after_native_readback(readback_operation_matches) -> None: + original, run_id, _ = _admitted_binding(_runtime_staged_profile) + calls: list[str] = [] + installed = original.handoff_bindings["transition.sim-to-emu"] + owner = {"component": "sim", "revision": 0} + + def coordinate(operation_id, transition, state): + calls.append("time-coordinate") + report = installed.coordinate(operation_id, transition, state) + return {**report, "order_ref": "order:native-transfer"} + + def invoke(operation_id, transition, state, _snapshot): + calls.append("invoke") + owner.update(component="emu", revision=1) + return { + "operation_id": operation_id, + "transition_id": transition.transition_id, + "source_component_id": "sim", + "destination_component_id": "emu", + "predecessor_history_head": state.history_head, + "phase_revision": state.phase_revision, + "status": "committed", + "order_ref": "order:native-transfer", + "evidence_refs": ["evidence:phase-realization", "evidence:native-transfer"], + } + + def readback(operation_id, _snapshot): + calls.append("readback") + return { + "operation_id": operation_id if readback_operation_matches else "unrelated-operation", + "owner_component_id": owner["component"], + "owner_ref": original.profile.components[owner["component"]].native_ownership_ref, + "phase_revision": owner["revision"], + "evidence_refs": ["evidence:native-owner-readback"], + } + + binding = replace( + original, + handoff_bindings={ + "transition.sim-to-emu": replace( + installed, + coordinate=coordinate, + invoke=invoke, + readback=readback, + ) + }, + ) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + initial_snapshot=_staged_time_snapshot(original), + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + + receipt = plane.advance_mixed_composition( + "transition.sim-to-emu", identity=identity(), idempotency_key="evidenced-handoff" + ) + + assert calls == ["time-coordinate", "invoke", "readback"] + if readback_operation_matches: + assert plane.snapshot.mixed_composition_states[run_id]["phase_id"] == "phase.emu" + assert plane.snapshot.mixed_composition_history[run_id][-1]["event_kind"] == "handoff" + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "succeeded" + else: + assert plane.snapshot.mixed_composition_states[run_id]["phase_id"] == "phase.sim" + assert plane.snapshot.mixed_composition_history[run_id][-1]["event_kind"] == "failure" + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == "indeterminate" + + +@pytest.mark.parametrize( + ("handoff_status", "terminal_state"), + [("pending", "indeterminate"), ("failed", "failed"), ("stale", "failed")], +) +def test_uncommitted_handoff_retains_prior_phase_and_classifies_outcome(handoff_status, terminal_state) -> None: + original, run_id, runtimes = _admitted_binding(_runtime_staged_profile) + installed = original.handoff_bindings["transition.sim-to-emu"] + + def uncommitted(operation_id, transition, state, _snapshot): + return { + "operation_id": operation_id, + "transition_id": transition.transition_id, + "source_component_id": "sim", + "destination_component_id": "emu", + "predecessor_history_head": state.history_head, + "phase_revision": state.phase_revision, + "status": handoff_status, + "order_ref": f"order:native:{operation_id}", + "evidence_refs": ["evidence:phase-realization"], + } + + def old_owner(operation_id, _snapshot): + return { + "operation_id": operation_id, + "owner_component_id": "sim", + "owner_ref": original.profile.components["sim"].native_ownership_ref, + "phase_revision": 0, + "evidence_refs": ["evidence:old-owner-readback"], + } + + binding = replace( + original, + handoff_bindings={ + "transition.sim-to-emu": replace( + installed, + invoke=uncommitted, + readback=old_owner, + ) + }, + ) + plane = RuntimeControlPlane( + create_stub_target(with_participant_runtime=False), + mixed_runtime=binding, + crossing_policy_resolver=permit_resolver(), + run_scope=f"run:{run_id}", + initial_snapshot=_staged_time_snapshot(original), + ) + plane.activate_mixed_composition(identity=identity(), idempotency_key="initial-phase") + plane.initialize_participant_episode(PARTICIPANT, episode_id="episode-1", identity=identity()) + + receipt = plane.advance_mixed_composition( + "transition.sim-to-emu", identity=identity(), idempotency_key="pending-handoff" + ) + + assert plane.get_operation(receipt.operation_id, identity=identity()).state.value == terminal_state + assert plane.snapshot.mixed_composition_states[run_id]["phase_id"] == "phase.sim" + failure = plane.snapshot.mixed_composition_history[run_id][-1] + assert failure["event_kind"] == "failure" + assert {"evidence:handoff-mapping", "evidence:phase-realization", "evidence:old-owner-readback"}.issubset( + failure["evidence_refs"] + ) + if terminal_state == "indeterminate": + action, admission, actor, crossing = behavior(), admission_request(), identity(), evidence() + with pytest.raises(RuntimeError, match="indeterminate operation requires resolution"): + plane.admit_participant_action( + action, + admission, + identity=actor, + crossing_evidence=crossing, + idempotency_key="after-pending", + ) + assert all(runtime.admission_count == 0 for runtime in runtimes.values()) + else: + retry = plane.admit_participant_action( + behavior(), + admission_request(), + identity=identity(), + crossing_evidence=evidence(), + idempotency_key="old-owner", + ) + assert plane.get_operation(retry.operation_id, identity=identity()).state.value == "succeeded" + assert runtimes["sim"].admission_count == 1 diff --git a/implementations/python/tests/test_issue_989_versioned_evidence.py b/implementations/python/tests/test_issue_989_versioned_evidence.py index 3a6f23105..d7cb91dca 100644 --- a/implementations/python/tests/test_issue_989_versioned_evidence.py +++ b/implementations/python/tests/test_issue_989_versioned_evidence.py @@ -230,7 +230,7 @@ def test_latest_current_release_is_versioned_and_strict(monkeypatch): from tools.formal_semantic_validation._releases import validate_retest_bundle release, protocol, corpus, snapshot, analysis = copy_bundle(load_retest_bundle, ROOT) - assert release.manifest["revision"] == "53.0.0" + assert release.manifest["revision"] == "54.0.0" original = _retest.replay_case def changed_result(root, case): @@ -283,7 +283,7 @@ def test_specification_current_capture_does_not_accept_old_artifact_digest(artif from tools.check_specification_coverage import load_bundle, validate_bundle manifest, protocol, snapshot, analysis = copy_bundle(load_bundle, ROOT) - assert manifest["revision"] == "52.0.0" + assert manifest["revision"] == "53.0.0" snapshot = deepcopy(snapshot) artifact = next(a for a in snapshot["artifacts"] if a["artifact_id"] == artifact_id) artifact["sha256"] = old_digest @@ -505,6 +505,7 @@ def test_no_capture_can_be_silently_dropped(monkeypatch, family, removed): "51.0.0", "52.0.0", "53.0.0", + "54.0.0", ] if family == "formal" else [ @@ -561,6 +562,7 @@ def test_no_capture_can_be_silently_dropped(monkeypatch, family, removed): "50.0.0", "51.0.0", "52.0.0", + "53.0.0", ] ) revisions.pop(-1 if removed == "current" else 0) diff --git a/implementations/python/tests/test_specification_coverage.py b/implementations/python/tests/test_specification_coverage.py index d150999d3..d79b41ffa 100644 --- a/implementations/python/tests/test_specification_coverage.py +++ b/implementations/python/tests/test_specification_coverage.py @@ -53,7 +53,7 @@ def test_immutable_bundle_index_preserves_concurrent_captures() -> None: bundles = copy_bundle(load_bundles, REPO_ROOT) assert {manifest["revision"] for manifest, *_rest in bundles} >= {"1.0.0", "1.1.0", "19.0.0"} manifest, *_rest = copy_bundle(load_bundle, REPO_ROOT) - assert manifest["revision"] == "52.0.0" + assert manifest["revision"] == "53.0.0" def test_historical_failures_name_the_revision_specific_documents() -> None: diff --git a/specs/formal/participant-semantics/cross-backend-participant-control.md b/specs/formal/participant-semantics/cross-backend-participant-control.md index 8bbdf0eed..264eb588f 100644 --- a/specs/formal/participant-semantics/cross-backend-participant-control.md +++ b/specs/formal/participant-semantics/cross-backend-participant-control.md @@ -740,9 +740,79 @@ authentication service, nested-profile resolver, coordinator or conformance engine. Its symbolic attempts/results are not realization evidence. MCB-001–045 are definitions; the matrix states the narrower clauses exercised -by executable witnesses. No portable schema, runtime enforcement, backend -realization, general model-checking result, proof or ASR-537 demonstration -is established. The profile keeps the edition-pinned prior-art dispositions +by executable witnesses. The #1013 semantic publication alone established no +portable schema or runtime enforcement. Subsequent #1014–#1016 and #1355 work +adds the published profile, trial admission, and bounded reference runtime +behavior described below; it does not establish a deployed backend +realization, general model-checking result, proof, or ASR-537 demonstration. +The profile keeps the edition-pinned prior-art dispositions from [the #813 source assessment](../../../docs/research/cross-backend-participant-control/prior-art-and-design-criteria.md). HLA ownership/time, co-simulation coupling and range transfer precedents remain design lineage, not wire or behavioral compatibility claims. + +## 17. Executable edge and handoff interpretation (#1355) + +For an admitted directed edge (e), the trusted runtime binding fixes an +installed bridge version and digest, source and destination action subjects, +the admitted loss, and a time service for the edge's named mapping. The mapper +must preserve the already authorized compiled action address and its provider +allocation; backend-native translation remains inside the pinned bridge. The +control plane retains the operation id and exact provider; the bridge cannot +select another provider or gain controller or disclosure authority. No binding, +capability, current policy, or evidence means refusal before a provider call. +The executable edge must join the exact governed crossing subject, audience, +policy cut, controller, action and disclosure authority, and permitted final +sink decision before bridge invocation. + +Let (A) be the durable decision/attempt, (X) the correlated provider result, +(D) a destination receipt from independent readback, and (O) an authorized +participant/audience readback. The executable ordering is: + +```text +invoke(e) only after committed A and an admitted, read-back time/order grant +record X only for the original operation and selected provider +record D only after X and a matching destination receipt +record O only after D and a matching participant/audience observation +``` + +The time grant cites the named source and destination clocks, mapping, +comparable order, and evidence; typed pre/post runtime readback must match the +admitted time model. A mapping declaration or pair of timestamps does not +provide the grant. The bounded implementation supports proved comparisons +within one segment. Incomparable or unsupported comparisons refuse; neither a +shared physical clock nor physical-OT timing is inferred. +At equal mapped ticks, source microstep must not exceed destination microstep. +Successful execution, delivery, observation, and weakening facts require the +incumbent backend result gate to accept the returned provider result. If a +later readback interrupts the call, already confirmed stages remain tied to +their original operation and the operation stays `INDETERMINATE`. + +For a staged transition that changes active components, the admitted evaluator +and an installed transfer service are separate. The service must obtain its +time grant, execute the exact native handoff under the operation id, and read +back the destination owner at the next phase revision. Only then may the new +phase and handoff fact commit. A failed or stale handoff with old-owner readback +retains the prior phase. Pending, contradictory, or unknown transfer is +`INDETERMINATE` and blocks dependent work. The store atomically excludes a +competing phase or mixed-effect claim for that run while the transfer is active. +Native ownership does not alter RUN-310 controller authority. + +The governed request and provider snapshot are fixed before a mapper runs; +mapping, time, and bridge callbacks cannot mutate either carrier and still +invoke the provider on an altered cut. Handoff +time readbacks join the committed snapshot before the grant and after the +transfer. On restart, an interrupted edge or native transfer has only its +durable pre-effect cut. Provider-only recovery cannot establish the bridge, +clock, delivery, audience, or native-owner stages. Such an operation remains +`INDETERMINATE` and blocks dependent work until those stages are reconciled. +Generic acceptance of the current snapshot cannot discharge an interrupted +mixed edge or native handoff, even when its crossing history is valid. A +stage-specific reconciliation must prove the missing external facts first. +Startup still validates typed crossing records and every unaffected history; +only the suffix of the interrupted crossing is withheld from contextual +validation while its operation is quarantined. + +Historical `sem-234/rev1` edge references and success values retain their old +reference-only meaning. They cannot be promoted to delivered, observed, or +governed-time facts by a new reader. The executable service binding is local to +the trusted runtime; no published profile schema changes in this amendment. diff --git a/specs/formal/runtime-contracts/participant-backend-contracts.md b/specs/formal/runtime-contracts/participant-backend-contracts.md index 78e04f218..039713150 100644 --- a/specs/formal/runtime-contracts/participant-backend-contracts.md +++ b/specs/formal/runtime-contracts/participant-backend-contracts.md @@ -156,6 +156,30 @@ Rules: evidence discipline without claiming runtime enforcement, which the RUN-319 final-sink boundary owns. +### Effective mixed support (issue #1355) + +For a mixed participant action or staged transfer, a manifest strength entry +is a declaration to be joined with the admitted provider-local feature and +time capabilities, exact profile edge or transition, current authority and +final-sink policy, and installed executable services. The bridge, mapper, +time coordinator, and destination or participant readback must execute their +named obligations under the owning operation. A support entry, service method, +mapping reference, timestamp, or backend success flag alone cannot establish +delivery, observation, governed order, or native handoff. Missing bindings or +contradictory pre-effect support refuse before an external effect; missing +post-effect readback leaves the operation indeterminate without claiming the +unconfirmed stage. + +The existing four support levels and separate constraint, limitation, +disclosure, and evidence references retain their meanings. A weaker admitted +mapping records its authorized loss and evidence only after correlated +execution; unknown or partial effects use the shared operation lifecycle, +not a new manifest support level. Shared time capabilities govern the named +clock mapping and comparison without requiring one physical clock or a +physical-OT timing guarantee. Installed bindings are trusted runtime inputs +against the sealed `sem-234/rev1` profile; this rule adds no manifest field, +support vocabulary term, or published carrier revision. + ### Adversarial-control apparatus and backend support (issue #1004) The following governed `participant-runtime-behavior-features` terms let a diff --git a/tools/check_specification_coverage.py b/tools/check_specification_coverage.py index 86799ea70..4749299ec 100644 --- a/tools/check_specification_coverage.py +++ b/tools/check_specification_coverage.py @@ -102,7 +102,7 @@ def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: max_bytes=_MAX_FILE_BYTES, ) current_path = current_release_path(records) - if dict(records)[current_path].get("revision") != "52.0.0" or {record.get("revision") for _, record in records} != { + if dict(records)[current_path].get("revision") != "53.0.0" or {record.get("revision") for _, record in records} != { "1.0.0", "1.1.0", "2.0.0", @@ -156,8 +156,9 @@ def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: "50.0.0", "51.0.0", "52.0.0", + "53.0.0", }: - raise ValueError("coverage evidence requires the explicit current 52.0.0 release and supported history") + raise ValueError("coverage evidence requires the explicit current 53.0.0 release and supported history") return records diff --git a/tools/formal_semantic_validation/_baseline.py b/tools/formal_semantic_validation/_baseline.py index dd252599e..6ea0a16dc 100644 --- a/tools/formal_semantic_validation/_baseline.py +++ b/tools/formal_semantic_validation/_baseline.py @@ -82,6 +82,7 @@ "50.0.0", "51.0.0", "52.0.0", + "53.0.0", } ) _V3_CORPUS_REVISIONS = frozenset( @@ -230,7 +231,18 @@ def _selected_baseline_manifest( if baseline_revision in _V2_REVISIONS else "docs/research/formal-semantic-validation/protocol-v1.json" ) - if baseline_revision in {"42.0.0", "45.0.0", "46.0.0", "47.0.0", "48.0.0", "49.0.0", "50.0.0", "51.0.0", "52.0.0"}: + if baseline_revision in { + "42.0.0", + "45.0.0", + "46.0.0", + "47.0.0", + "48.0.0", + "49.0.0", + "50.0.0", + "51.0.0", + "52.0.0", + "53.0.0", + }: expected_corpus_path = "docs/research/formal-semantic-validation/corpus/manifest-v4.json" elif baseline_revision in _V3_CORPUS_REVISIONS: expected_corpus_path = "docs/research/formal-semantic-validation/corpus/manifest-v3.json" diff --git a/tools/formal_semantic_validation/_loading.py b/tools/formal_semantic_validation/_loading.py index 112bad274..882f989b2 100644 --- a/tools/formal_semantic_validation/_loading.py +++ b/tools/formal_semantic_validation/_loading.py @@ -83,6 +83,7 @@ def load_release_bundles(repo_root: Path = REPO_ROOT) -> list[EvidenceRelease]: "51.0.0", "52.0.0", "53.0.0", + "54.0.0", }: raise ValueError("formal evidence requires every supported historical and current release") releases: list[EvidenceRelease] = [] @@ -129,6 +130,6 @@ def load_retest_bundle( if not releases: raise ValueError("the formal semantic-validation index selects no v2 retest release") release = max(releases, key=lambda item: revision_key(item.manifest.get("revision"))) - if release.manifest.get("revision") != "53.0.0" or release.protocol.get("revision") != "2.0.0": - raise ValueError("the current formal evidence release must be the explicit 53.0.0 retest") + if release.manifest.get("revision") != "54.0.0" or release.protocol.get("revision") != "2.0.0": + raise ValueError("the current formal evidence release must be the explicit 54.0.0 retest") return release, release.protocol, release.corpus, release.snapshot, release.analysis diff --git a/tools/formal_semantic_validation/_release_revisions.py b/tools/formal_semantic_validation/_release_revisions.py index ed9d002d8..60dd00488 100644 --- a/tools/formal_semantic_validation/_release_revisions.py +++ b/tools/formal_semantic_validation/_release_revisions.py @@ -52,8 +52,9 @@ "50.0.0", "51.0.0", "52.0.0", + "53.0.0", } ) -_SUPPORTED_RETEST_REVISIONS = _HISTORICAL_RETEST_REVISIONS | {"53.0.0"} +_SUPPORTED_RETEST_REVISIONS = _HISTORICAL_RETEST_REVISIONS | {"54.0.0"} _SOURCE_BOUND_RETEST_REVISIONS = _SUPPORTED_RETEST_REVISIONS - {"3.0.0"} diff --git a/tools/formal_semantic_validation/_releases.py b/tools/formal_semantic_validation/_releases.py index 6512c6614..8a5dd11fc 100644 --- a/tools/formal_semantic_validation/_releases.py +++ b/tools/formal_semantic_validation/_releases.py @@ -159,7 +159,7 @@ def validate_release_bundle(repo_root: Path, release: EvidenceRelease) -> list[P release.corpus, release.snapshot, release.analysis, - replay_current=manifest.get("revision") == "53.0.0", + replay_current=manifest.get("revision") == "54.0.0", ) ) else: @@ -270,6 +270,7 @@ def _expected_corpus_revision(release_revision: object) -> str: "51.0.0", "52.0.0", "53.0.0", + "54.0.0", }: expected_corpus_revision = "4.0.0" return expected_corpus_revision @@ -297,7 +298,7 @@ def validate_retest_bundle( return [ _failure( "formal-validation-current-replay-required", - "only releases 3.0.0 through 52.0.0 can use integrated historical validation", + "only releases 3.0.0 through 53.0.0 can use integrated historical validation", snapshot_path, ) ] @@ -423,6 +424,7 @@ def _current_retest_source_failures( "51.0.0": "50.0.0", "52.0.0": "51.0.0", "53.0.0": "52.0.0", + "54.0.0": "53.0.0", }[release_revision] if not isinstance(baseline, Mapping) or baseline.get("release_revision") != expected_baseline: failures.append( diff --git a/tools/formal_semantic_validation/_retest.py b/tools/formal_semantic_validation/_retest.py index d21b546ff..aa91752de 100644 --- a/tools/formal_semantic_validation/_retest.py +++ b/tools/formal_semantic_validation/_retest.py @@ -37,7 +37,7 @@ ) from tools.policy.common import PolicyFailure -_SOURCE_STATE_REVISIONS = frozenset(f"{revision}.0.0" for revision in range(4, 54)) +_SOURCE_STATE_REVISIONS = frozenset(f"{revision}.0.0" for revision in range(4, 55)) @dataclasses.dataclass(frozen=True) diff --git a/tools/policy/historical_identity_records.json b/tools/policy/historical_identity_records.json index edc74491d..aefadf385 100644 --- a/tools/policy/historical_identity_records.json +++ b/tools/policy/historical_identity_records.json @@ -495,7 +495,7 @@ "record_class": "historical-index", "rationale": "Indexes immutable pre-cutover ADR titles, paths, pins, and amendment summaries without making them current identity surfaces.", "occurrences": 4, - "content_sha256": "aaf64f1f6c3fc2fc7283bf846a59b2620c47361a3e617e8f9087b4bf4d40ea2d" + "content_sha256": "dddd15454fde8c67c1755e6b74e441bd748fb6088c8951b979b9688633a90a50" }, { "path": "docs/decisions/cage-2-replication-design.md", diff --git a/tools/policy/requirement_order.yaml b/tools/policy/requirement_order.yaml index 434f1f15f..c1bdd6438 100644 --- a/tools/policy/requirement_order.yaml +++ b/tools/policy/requirement_order.yaml @@ -834,22 +834,30 @@ ownership: # The #1016 preflight is documented here; runtime delivery remains # activation-gated. - specs/formal/participant-semantics/cross-backend-participant-control.md + - specs/formal/runtime-contracts/participant-backend-contracts.md - specs/formal/participant-semantics/README.md - specs/formal/assurance-fulfillment.yaml - docs/decisions/issue-1013-sem-234-mixed-participant-control-preflight.md - docs/decisions/issue-1014-mixed-composition-contracts-preflight.md - docs/decisions/issue-1015-mixed-staged-trial-admission-preflight.md - docs/decisions/issue-1016-mixed-runtime-coordination-preflight.md + - docs/decisions/issue-1355-executable-mixed-mapping-time-preflight.md + - docs/decisions/adrs/adr-102-mixed-cross-backend-participant-control.md + - docs/decisions/adrs/adr-index.yaml - docs/explain/reference/mixed-participant-composition.md - docs/explain/reference/scenario-variation-and-trial-realization.md - docs/governance/requirement-scopes/1014.json - docs/governance/requirement-scopes/1016.json + - docs/governance/requirement-scopes/1355.json - docs/research/formal-semantic-validation/bundles/retest-v31.json - docs/research/formal-semantic-validation/execution-snapshot-v31.json - docs/research/formal-semantic-validation/index.md - docs/research/formal-semantic-validation/analysis-v32.json - docs/research/formal-semantic-validation/bundles/retest-v32.json - docs/research/formal-semantic-validation/execution-snapshot-v32.json + - docs/research/formal-semantic-validation/analysis-v53.json + - docs/research/formal-semantic-validation/bundles/retest-v53.json + - docs/research/formal-semantic-validation/execution-snapshot-v53.json - docs/research/specification-coverage/analysis-v31.json - docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1183-v31.json - docs/research/specification-coverage/execution-snapshot-v31.json @@ -863,6 +871,9 @@ ownership: - docs/research/specification-coverage/analysis-v38.json - docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1016-v38.json - docs/research/specification-coverage/execution-snapshot-v38.json + - docs/research/specification-coverage/analysis-v53.json + - docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1355-v53.json + - docs/research/specification-coverage/execution-snapshot-v53.json - tools/check_json_artifacts.py - tools/check_specification_coverage.py - tools/formal_semantic_validation/_baseline.py @@ -904,19 +915,33 @@ ownership: - implementations/python/tests/test_issue_1014_mixed_composition_governance.py - implementations/python/tests/test_issue_1015_mixed_staged_trial_admission.py - implementations/python/tests/test_issue_1016_mixed_runtime_coordination.py + - implementations/python/tests/test_specification_coverage.py + - implementations/python/tests/test_formal_semantic_validation.py + - implementations/python/tests/test_issue_1355_mixed_mapping_time.py - implementations/python/packages/raes_runtime/__init__.py - implementations/python/packages/raes_runtime/backend_snapshot_contracts.py - implementations/python/packages/raes_runtime/control_plane.py - implementations/python/packages/raes_runtime/control_plane_configuration.py - implementations/python/packages/raes_runtime/control_plane_recovery.py + - implementations/python/packages/raes_runtime/control_plane_resolution_records.py - implementations/python/packages/raes_runtime/control_plane_store_history.py - implementations/python/packages/raes_runtime/control_plane_store_snapshots.py + - implementations/python/packages/raes_runtime/control_plane_store.py + - implementations/python/packages/raes_runtime/control_plane_store_local_records.py + - implementations/python/packages/raes_runtime/control_plane_store_memory.py - implementations/python/packages/raes_runtime/mixed_runtime.py - implementations/python/packages/raes_runtime/mixed_runtime_dispatch.py + - implementations/python/packages/raes_runtime/mixed_runtime_edge.py + - implementations/python/packages/raes_runtime/mixed_runtime_edge_execution.py + - implementations/python/packages/raes_runtime/mixed_runtime_handoff.py + - implementations/python/packages/raes_runtime/mixed_runtime_handoff_execution.py - implementations/python/packages/raes_runtime/mixed_runtime_phase.py + - implementations/python/packages/raes_runtime/mixed_runtime_recovery.py + - implementations/python/packages/raes_runtime/mixed_runtime_result.py - implementations/python/packages/raes_runtime/mixed_runtime_lifecycle.py - implementations/python/packages/raes_runtime/mixed_runtime_state.py - implementations/python/packages/raes_runtime/participant_action_validation.py + - implementations/python/packages/raes_runtime/participant_crossing_action.py - implementations/python/packages/raes_runtime/participant_control.py - implementations/python/packages/raes_runtime/participant_crossing_boundary.py - implementations/python/packages/raes_runtime/participant_crossing_policy.py @@ -958,6 +983,7 @@ ownership: - implementations/python/packages/raes_processor/trial_compiler/profiles.py - implementations/python/packages/raes_processor/trial_compiler/realization_admission.py - implementations/python/packages/raes_processor/trial_realization.py + - tools/policy/historical_identity_records.json - tools/policy/requirement_order.yaml - tools/verify_all.py # Supporting delivery-hook regression requested during #1013 review.