From 3b7208b15f8dc29db8ad6d3b15bde792d79220b7 Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Thu, 24 Sep 2026 03:25:26 +0200 Subject: [PATCH 1/6] Fix governed context forwarding in v2 admission --- ...ue-1357-v2-governed-admission-preflight.md | 81 +++++++++++ ...rticipant-decision-surface-v2-migration.md | 5 +- ...participant_decision_surface_control_v2.py | 38 +++-- ...participant_decision_surface_v2_runtime.py | 133 +++++++++++++++++- 4 files changed, 244 insertions(+), 13 deletions(-) create mode 100644 docs/decisions/issue-1357-v2-governed-admission-preflight.md diff --git a/docs/decisions/issue-1357-v2-governed-admission-preflight.md b/docs/decisions/issue-1357-v2-governed-admission-preflight.md new file mode 100644 index 000000000..a7a6676b5 --- /dev/null +++ b/docs/decisions/issue-1357-v2-governed-admission-preflight.md @@ -0,0 +1,81 @@ +# Issue #1357 — v2 governed admission preflight + +Scope: the public Python `admit_participant_decision_surface_selection_v2()` +entry point. The GitHub issue is the contract. This note records boundaries for +implementation; it does not change runtime behavior or ADR-095 semantics. + +## Architecture decision + +The v2 selection binder owns agreement with the delivered surface; ordinary +participant-action admission owns caller and ingress-crossing authority. Keep +that sequence. Forward the caller's original identity and crossing evidence +through the v2 entry point to `admit_participant_action()` together with the +bound request and existing retry context. The v1 selection entry point and +`ParticipantSubmissionOptions` already provide the submission-context pattern. +The v2 path currently forwards only `idempotency_key` and +`request_fingerprint`, so a configured governed ingress cannot receive the +identity and evidence that ordinary admission requires. Keep one canonical +submission-options vocabulary and shape check; do not create a v2 authority DTO. + +`ParticipantActionAdmissionRequest` is the backend-neutral action request, not +the caller's authenticated identity or crossing evidence. The v2 selection is +a participant choice bound to a surface id, decision epoch, view digest and +delivery ref; it grants no new authority. The surface's derivation cut and +delivery cut are distinct from the fresh ingress crossing cut. Preserve their +participant/episode, action, audience, policy and occurrence identities through +the existing validators. Neither a selected action nor a delivery record may +synthesize caller authority, required evidence or a crossing occurrence. + +## Cross-cutting boundaries + +| Layer | Existing owner and required behavior | +| --- | --- | +| Published shape and proposal | `contracts/schemas/control-plane/participant-decision-surface-v2.json`, `raes_contracts.contracts.participant_decision_surface_v2`, `raes_contracts.participant_binding_v2` and `ParticipantActionAdmissionRequest` own surface/selection fields, agreement, apparatus resolution and governed argument-shape validation. Use their typed carriers and existing checks; no duplicate schema or parser. | +| Exact-cut and disclosure | `validate_participant_decision_surface_v2_anchor()` re-resolves the derivation anchor; `validate_participant_decision_surface_v2_delivery()` re-resolves authoritative delivery. ADR-095 and SEM-226 keep projection, disclosure, delivery, participant observation, selection and admission distinct. Never put assurance-only refs or crossing evidence in the participant-facing view. | +| Submission and authentication | `ParticipantSubmissionOptions.from_fields()` owns optional submission shape. `ControlPlaneIdentity` and `_require_crossing_identity()` own authenticated principal, target, role and exact participant/controller binding. A governed ingress requires the original typed identity; `operation_actor_scope(None)` denotes a trusted embedded process and must not replace a served caller. | +| Crossing and policy | `ParticipantCrossingEvidence` supplies caller-owned evidence metadata; `action_crossing_intent()`, `prepare_participant_crossing()`, `participant_crossing_policy`, `participant_flow_sink` and API-424 control mediation derive and validate the live occurrence, policy, evidence, capability, audience and final-sink decisions. Evidence refs are claims to check against trusted resolver context, not proof by presence. Unknown, stale, mismatched or unauthorized context fails closed. | +| State and effect | `RuntimeMutationAuthority`, `control_plane_mutation()`, `external_control_plane_call()`, `expected_participant_history_heads()`, the operation record and atomic store commit own serialized state cuts, re-entry fencing, replay and durable crossing/action history. Preserve the existing pre-mutation check and recheck under the mutation permit; do not dispatch a backend action before the governed decision and claim. | +| Failure and observation | `_participant_binding_diagnostic()`, `_reject_diagnostics()`, `OperationReceipt`, `operation_admission_context()` and crossing denial audit own the current rejection forms. Bind early rejections to the supplied actor where available, and keep audit details and returned diagnostics bounded and value-free. Do not wrap ordinary `PermissionError`/`ValueError` into a new exception hierarchy or expose raw evidence/policy payloads. | + +The public v2 method is a Python control-plane API; the current HTTP adapter +does not expose this admission method. Thus no new HTTP request body, auth +dependency, error envelope, configuration or environment binding is in scope. +If an HTTP route is later introduced, it must use `ControlPlaneSecurityConfig` +and the existing API authentication and response machinery, with typed identity +coming from the auth dependency rather than the request body. This change +needs no credential lookup, secret value, subprocess argument or environment +variable. Do not pass identity or evidence through `argv`, logging, diagnostic +text or participant-visible serialization. Existing operation commitments and +audit records remain the persistence surface; no new journal or cache. + +## Verification boundary and anti-patterns + +The targeted v2 runtime test should show a valid delivered selection reaches +governed ordinary admission with the correct authenticated actor and crossing +occurrence, then reject absent identity/evidence, stale surface or crossing +cut, wrong participant/episode/action/audience/controller, and unauthorized +role/target/subject. Check that rejection leaves action/behavior history and +backend effects absent, except for the incumbent denial audit or crossing +record where that boundary intentionally records one. Reuse the existing +`participant_crossing_fixtures.py` resolver, identity and evidence fixtures +alongside `test_sem_220_participant_decision_surface_v2_runtime.py`; preserve +the mutation/concurrency and replay tests for the same path. Run only targeted +local checks under `.ground-control.yaml`, `.gc/plan-rules.md` and `noxfile.py`; +broad suites belong to CI. The published schema is governed by +`contracts/schema-publication-manifest.json` and +`tools/check_generated_schemas.py`; this forwarding change does not call for a +schema edit or a second contract artifact. + +Do not copy RUN-319 crossing validation into the v2 binder, infer a controller +from the chosen action, use the decision epoch as policy order, treat the +delivery ref as ingress evidence, turn a rejected crossing into success, or +relax an existing validator to fit a forwarded value. The next submission +context variation belongs in the shared `ParticipantSubmissionOptions` seam +and then passes through both selection entry points and ordinary admission; +it should not require another v2-only options parser. + +Non-goals: changing the v2 wire schema, ADR-095, v1 historical meaning, +participant projection or delivery rules, policy semantics, backend execution, +HTTP routing, secret/config handling, or store formats. A separate mixed-runtime +support change must resolve the current v2 target guard against the ordinary +action path's mixed-runtime guard before claiming mixed admission support. diff --git a/docs/explain/reference/participant-decision-surface-v2-migration.md b/docs/explain/reference/participant-decision-surface-v2-migration.md index 391c992cf..d6930ea6a 100644 --- a/docs/explain/reference/participant-decision-surface-v2-migration.md +++ b/docs/explain/reference/participant-decision-surface-v2-migration.md @@ -40,7 +40,10 @@ For each participant choice: 9. Accept a selection only when it binds surface id, decision epoch, canonical participant-view digest, and delivery ref. 10. At admission, re-resolve the derivation anchor, delivery record, apparatus, - and existing participant-action constraints before writing behavior. + and existing participant-action constraints before writing behavior. Pass + the authenticated caller identity and, for governed ingress, the caller's + crossing evidence to the v2 admission method. The selection and delivery + record do not supply either authority or ingress evidence. The reference entry points are: diff --git a/implementations/python/packages/raes_runtime/participant_decision_surface_control_v2.py b/implementations/python/packages/raes_runtime/participant_decision_surface_control_v2.py index 6e44ffafa..d02d1d407 100644 --- a/implementations/python/packages/raes_runtime/participant_decision_surface_control_v2.py +++ b/implementations/python/packages/raes_runtime/participant_decision_surface_control_v2.py @@ -26,6 +26,7 @@ _participant_binding_address, _participant_binding_diagnostic, ) +from .participant_submission_options import ParticipantSubmissionOptions def _bind_participant_decision_surface_v2( @@ -68,18 +69,23 @@ def admit_participant_decision_surface_selection_v2( selection: ParticipantDecisionSurfaceSelectionV2Model, admission_request: ParticipantActionAdmissionRequest, resolvers: ParticipantDecisionSurfaceBindingResolversV2, - idempotency_key: str = "", - request_fingerprint: str = "", + **submission_options: object, ) -> OperationReceipt: """Re-resolve v2 state and delivery before ordinary action admission.""" + options = ParticipantSubmissionOptions.from_fields(submission_options) receipt: OperationReceipt if self._target.participant_runtime is None: receipt = self._reject_submission( domain=RuntimeDomain.PARTICIPANT, message=_NO_PARTICIPANT_RUNTIME_MESSAGE, - idempotency_key=idempotency_key, - request_fingerprint=request_fingerprint, + idempotency_key=options.idempotency_key, + request_fingerprint=options.request_fingerprint, + identity=options.identity, + request={ + "operation": "participant-decision-surface-selection-v2", + "participant_address": getattr(participant_behavior, "address", "unknown"), + }, ) else: request, diagnostic = _bind_participant_decision_surface_v2( @@ -94,8 +100,13 @@ def admit_participant_decision_surface_selection_v2( receipt = self._reject_diagnostics( domain=RuntimeDomain.PARTICIPANT, diagnostics=[diagnostic], - idempotency_key=idempotency_key, - request_fingerprint=request_fingerprint, + idempotency_key=options.idempotency_key, + request_fingerprint=options.request_fingerprint, + identity=options.identity, + request={ + "operation": "participant-decision-surface-selection-v2", + "participant_address": getattr(participant_behavior, "address", "unknown"), + }, ) else: with control_plane_mutation(self, OperationKind.PARTICIPANT_ACTION): @@ -111,16 +122,23 @@ def admit_participant_decision_surface_selection_v2( receipt = self._reject_diagnostics( domain=RuntimeDomain.PARTICIPANT, diagnostics=[diagnostic], - idempotency_key=idempotency_key, - request_fingerprint=request_fingerprint, + idempotency_key=options.idempotency_key, + request_fingerprint=options.request_fingerprint, + identity=options.identity, + request={ + "operation": "participant-decision-surface-selection-v2", + "participant_address": getattr(participant_behavior, "address", "unknown"), + }, ) else: assert request is not None receipt = self.admit_participant_action( participant_behavior, request, - idempotency_key=idempotency_key, - request_fingerprint=request_fingerprint, + idempotency_key=options.idempotency_key, + request_fingerprint=options.request_fingerprint, + identity=options.identity, + crossing_evidence=options.crossing_evidence, ) return receipt diff --git a/implementations/python/tests/test_sem_220_participant_decision_surface_v2_runtime.py b/implementations/python/tests/test_sem_220_participant_decision_surface_v2_runtime.py index b76e552ca..15796ad60 100644 --- a/implementations/python/tests/test_sem_220_participant_decision_surface_v2_runtime.py +++ b/implementations/python/tests/test_sem_220_participant_decision_surface_v2_runtime.py @@ -5,6 +5,7 @@ from dataclasses import replace import pytest +from participant_crossing_fixtures import StaticCrossingResolver, evidence, identity, policy_capable_target from raes_backend_stubs.stubs import create_stub_target from raes_contracts.contracts import ( ParticipantDecisionSurfaceDeliveryV2Model, @@ -26,6 +27,7 @@ resolve_participant_episode_readiness_anchor_v2, ) from raes_runtime.control_plane import RuntimeControlPlane +from raes_runtime.control_plane_security import ControlPlaneRole from test_sem_220_participant_decision_surface import ( BEHAVIOR, BOUNDARY, @@ -222,8 +224,8 @@ def _delivery(surface) -> ParticipantDecisionSurfaceDeliveryV2Model: ) -def _initial_surface(): - control = RuntimeControlPlane(create_stub_target()) +def _initial_surface(control: RuntimeControlPlane | None = None): + control = control or RuntimeControlPlane(create_stub_target()) control.initialize_participant_episode(PARTICIPANT, episode_id=EPISODE) snapshot = control.get_snapshot().snapshot anchor = resolve_participant_episode_readiness_anchor_v2( @@ -259,6 +261,133 @@ def _selection_for(delivered) -> ParticipantDecisionSurfaceSelectionV2Model: ) +def _governed_selection_case(): + resolver = StaticCrossingResolver() + control, projected, implementation_selection = _initial_surface( + RuntimeControlPlane( + policy_capable_target(), + crossing_policy_resolver=resolver, + enforce_final_sink_flow_control=False, + ) + ) + delivery = _delivery(projected) + delivered = deliver_participant_decision_surface_v2( + projected, delivery_ref=delivery.delivery_ref, resolver=lambda **_: delivery + ) + return control, delivered, implementation_selection, delivery + + +def _admit_governed_selection(control, delivered, implementation_selection, delivery, *, selection=None, **context): + return control.admit_participant_decision_surface_selection_v2( + replace(_compiled_participant_behavior(), authority_anchor_addresses=("authority:red-team",)), + surface=delivered, + selection=selection or _selection_for(delivered), + admission_request=replace(_admission_request(), implementation_selection=implementation_selection), + resolvers=ParticipantDecisionSurfaceBindingResolversV2( + argument_shape=_resolved_selection, + apparatus=lambda **_: implementation_selection, + delivery=lambda **_: delivery, + ), + **context, + ) + + +def test_v2_selection_forwards_authenticated_context_to_governed_admission() -> None: + control, delivered, implementation_selection, delivery = _governed_selection_case() + receipt = _admit_governed_selection( + control, + delivered, + implementation_selection, + delivery, + identity=identity(participant_address=PARTICIPANT), + crossing_evidence=evidence(), + ) + + assert receipt.accepted is True + crossing = control.get_snapshot().snapshot.participant_crossing_history[PARTICIPANT][0] + assert crossing["participant_address"] == PARTICIPANT + assert crossing["episode_id"] == EPISODE + assert crossing["occurrence"]["interaction_kind"] == "candidate-selection" + assert crossing["occurrence"]["action_or_projection_ref"] == SCAN + assert len(control.get_snapshot().snapshot.participant_behavior_history[PARTICIPANT]) == 3 + + +@pytest.mark.parametrize("missing", ("identity", "crossing_evidence")) +def test_v2_governed_admission_requires_caller_context(missing: str) -> None: + control, delivered, implementation_selection, delivery = _governed_selection_case() + context = { + "identity": identity(participant_address=PARTICIPANT), + "crossing_evidence": evidence(), + } + context.pop(missing) + + with pytest.raises((PermissionError, ValueError)): + _admit_governed_selection(control, delivered, implementation_selection, delivery, **context) + + assert control.get_snapshot().snapshot.participant_behavior_history.get(PARTICIPANT, []) == [] + + +@pytest.mark.parametrize("unauthorized", ("wrong_target", "wrong_role", "wrong_participant")) +def test_v2_governed_admission_rejects_unauthorized_caller(unauthorized: str) -> None: + control, delivered, implementation_selection, delivery = _governed_selection_case() + caller = identity(participant_address=PARTICIPANT) + if unauthorized == "wrong_target": + caller = replace(caller, target_name="another-target") + elif unauthorized == "wrong_role": + caller = replace(caller, roles=frozenset({ControlPlaneRole.AUDITOR})) + else: + caller = identity(participant_address="participant.behavior.other") + + with pytest.raises(PermissionError): + _admit_governed_selection( + control, + delivered, + implementation_selection, + delivery, + identity=caller, + crossing_evidence=evidence(), + ) + + assert control.get_snapshot().snapshot.participant_behavior_history.get(PARTICIPANT, []) == [] + + +def test_v2_governed_admission_rejects_a_stale_episode_cut() -> None: + control, delivered, implementation_selection, delivery = _governed_selection_case() + control.reset_participant_episode(PARTICIPANT, episode_id=f"{EPISODE}-reset") + + receipt = _admit_governed_selection( + control, + delivered, + implementation_selection, + delivery, + identity=identity(participant_address=PARTICIPANT), + crossing_evidence=evidence(), + ) + + assert receipt.accepted is False + assert control.get_snapshot().snapshot.participant_behavior_history.get(PARTICIPANT, []) == [] + + +def test_v2_governed_admission_rejects_mismatched_selected_action() -> None: + control, delivered, implementation_selection, delivery = _governed_selection_case() + selection = _selection_for(delivered).model_copy( + update={"action_contract_address": "participant.action-contract.other"} + ) + + receipt = _admit_governed_selection( + control, + delivered, + implementation_selection, + delivery, + selection=selection, + identity=identity(participant_address=PARTICIPANT), + crossing_evidence=evidence(), + ) + + assert receipt.accepted is False + assert control.get_snapshot().snapshot.participant_behavior_history.get(PARTICIPANT, []) == [] + + def test_initial_epoch_projects_delivers_and_admits_only_the_exact_view() -> None: control, projected, implementation_selection = _initial_surface() delivery = _delivery(projected) From 97e4ecc673dfad849a7730b447dd813d5ed0a669 Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Thu, 24 Sep 2026 03:35:20 +0200 Subject: [PATCH 2/6] Refresh specification coverage evidence for current source --- .../specification-coverage/analysis-v45.json | 101 +++ ...specification-coverage-issue-1357-v45.json | 10 + .../execution-snapshot-v45.json | 701 ++++++++++++++++++ docs/research/specification-coverage/index.md | 11 +- .../tests/test_specification_coverage.py | 2 +- tools/check_specification_coverage.py | 42 +- 6 files changed, 855 insertions(+), 12 deletions(-) create mode 100644 docs/research/specification-coverage/analysis-v45.json create mode 100644 docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1357-v45.json create mode 100644 docs/research/specification-coverage/execution-snapshot-v45.json diff --git a/docs/research/specification-coverage/analysis-v45.json b/docs/research/specification-coverage/analysis-v45.json new file mode 100644 index 000000000..ec18c294c --- /dev/null +++ b/docs/research/specification-coverage/analysis-v45.json @@ -0,0 +1,101 @@ +{ + "analysis_id": "raes-standardized-specification-coverage-issue-1357-v45", + "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-v45.json", + "docs/research/specification-coverage/analysis-v45.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-24", + "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.", + "Issue #1357 governed v2 admission is covered by dedicated runtime and crossing tests, not promoted to a new claim by the retained offline specification corpus." + ], + "load_bearing_results": { + "failed": 0, + "missing": 0, + "passed": 10, + "total": 10 + }, + "plain_language_outcome": "The retained specification matrix still demonstrates the same bounded SDL coverage on the current implementation. Governed v2 action admission is tested separately; no runtime authorization or live backend claim is derived from this offline corpus.", + "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": "raes-standardized-specification-coverage-issue-1357-v45", + "snapshot_sha256": "ab68c6e8c36ceea3dd1e6ec7a31c521bc06e740c82d6f198b144cad998fdfebd" +} diff --git a/docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1357-v45.json b/docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1357-v45.json new file mode 100644 index 000000000..66ab04577 --- /dev/null +++ b/docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1357-v45.json @@ -0,0 +1,10 @@ +{ + "analysis_path": "docs/research/specification-coverage/analysis-v45.json", + "analysis_sha256": "6cd6c830ac5286d27d0c7cb2872e6de27bd5abad68fe3d67d4e38ed433e4f12d", + "bundle_id": "raes-standardized-specification-coverage", + "protocol_path": "docs/research/specification-coverage/protocol-v1.json", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "revision": "45.0.0", + "snapshot_path": "docs/research/specification-coverage/execution-snapshot-v45.json", + "snapshot_sha256": "ef01b1182eff55e4f12317611c5415caefac1b666fefd9de83ea5b05c4874c72" +} diff --git a/docs/research/specification-coverage/execution-snapshot-v45.json b/docs/research/specification-coverage/execution-snapshot-v45.json new file mode 100644 index 000000000..14aac2568 --- /dev/null +++ b/docs/research/specification-coverage/execution-snapshot-v45.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-24T01:33:03.875794+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": "945267796770238855d21a75e9da35f74791edbe1b0b72d544cdb94a12f01b12", + "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.", + "This replay binds issue #1357 governed v2 decision admission and the integrated source state. The retained offline specification corpus does not exercise participant crossing authorization or assert new runtime behavior." + ], + "protocol_revision": "1.0.0", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "raes_revision": "3b7208b15f8dc29db8ad6d3b15bde792d79220b7", + "snapshot_id": "raes-standardized-specification-coverage-issue-1357-v45", + "snapshot_revision": "45.0.0", + "source_state": { + "base_revision": "3b7208b15f8dc29db8ad6d3b15bde792d79220b7", + "checkout_state": "modified", + "implementation_digest": "a6c52cd21e5a4847632b60abdaf57cb6046687474a41cdcd7457748851232294", + "profile": "python-reference-source/v2" + } +} diff --git a/docs/research/specification-coverage/index.md b/docs/research/specification-coverage/index.md index 04ee1b312..838c11a7a 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 44.0.0 and rejects duplicate or unsupported +Current validation requires release 45.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; @@ -376,10 +376,17 @@ refactoring in [`execution-snapshot-v43.json`](execution-snapshot-v43.json) and [`analysis-v43.json`](analysis-v43.json). Fresh replay retains the same bounded outcomes and claim limits; it does not add a new semantic claim. -Current release 44.0.0 records the merged participant identity and local +Release 44.0.0 records the merged participant identity and local outcome implementation in [`execution-snapshot-v44.json`](execution-snapshot-v44.json) and [`analysis-v44.json`](analysis-v44.json). The two pre-merge issue #218 captures retain their observations and source identities in v42 and v43; only their release numbers, paths, and corresponding digest joins were reconciled with the independently published issue #1338 capture. The combined capture uses the issue #1338 baseline and preserves the same bounded claim limits. + +Current release 45.0.0 replays the retained protocol against the source state +containing issue #1357's governed v2 decision admission. Its +[`execution snapshot`](execution-snapshot-v45.json) and +[`analysis`](analysis-v45.json) retain the same classifications and bounded +claim limits. Participant crossing authorization is exercised by dedicated +runtime tests, outside this offline specification corpus. diff --git a/implementations/python/tests/test_specification_coverage.py b/implementations/python/tests/test_specification_coverage.py index 3b774fbd5..8406035dd 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"] == "44.0.0" + assert manifest["revision"] == "45.0.0" def test_historical_failures_name_the_revision_specific_documents() -> None: diff --git a/tools/check_specification_coverage.py b/tools/check_specification_coverage.py index d584d2ed4..21fe2161b 100644 --- a/tools/check_specification_coverage.py +++ b/tools/check_specification_coverage.py @@ -88,9 +88,14 @@ def load_bundle( def load_bundles( repo_root: Path = REPO_ROOT, -) -> list[tuple[dict[str, object], dict[str, object], dict[str, object], dict[str, object]]]: +) -> list[ + tuple[dict[str, object], dict[str, object], dict[str, object], dict[str, object]] +]: records = _load_bundle_index(repo_root) - return [_load_bundle_record(repo_root, manifest_path, manifest) for manifest_path, manifest in records] + return [ + _load_bundle_record(repo_root, manifest_path, manifest) + for manifest_path, manifest in records + ] def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: @@ -102,7 +107,9 @@ 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") != "44.0.0" or {record.get("revision") for _, record in records} != { + if dict(records)[current_path].get("revision") != "45.0.0" or { + record.get("revision") for _, record in records + } != { "1.0.0", "1.1.0", "2.0.0", @@ -148,8 +155,11 @@ def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: "42.0.0", "43.0.0", "44.0.0", + "45.0.0", }: - raise ValueError("coverage evidence requires the explicit current 44.0.0 release and supported history") + raise ValueError( + "coverage evidence requires the explicit current 45.0.0 release and supported history" + ) return records @@ -167,14 +177,22 @@ def _load_bundle_record( for label in ("protocol", "snapshot", "analysis"): path_value = manifest[f"{label}_path"] sha_value = manifest[f"{label}_sha256"] - resolved = safe_repo_path(repo_root, path_value) if isinstance(path_value, str) else None + resolved = ( + safe_repo_path(repo_root, path_value) + if isinstance(path_value, str) + else None + ) if resolved is None or not resolved.is_file(): - raise ValueError(f"{manifest_path!r} contains unsafe or missing {label}_path") + raise ValueError( + f"{manifest_path!r} contains unsafe or missing {label}_path" + ) if not isinstance(sha_value, str) or not _SHA256_RE.fullmatch(sha_value): raise ValueError(f"{manifest_path!r} contains invalid {label}_sha256") if _sha256(resolved) != sha_value: raise ValueError(f"{manifest_path!r} contains stale {label}_sha256") - loaded.append(load_bounded_json_object(repo_root, path_value, max_bytes=_MAX_FILE_BYTES)) + loaded.append( + load_bounded_json_object(repo_root, path_value, max_bytes=_MAX_FILE_BYTES) + ) return manifest, loaded[0], loaded[1], loaded[2] @@ -187,10 +205,16 @@ def evaluate(repo_root: Path = REPO_ROOT) -> list[PolicyFailure]: for manifest_path, manifest in records ] except (OSError, ValueError) as exc: - return [_failure("specification-coverage-bundle-invalid", str(exc), MANIFEST_PATH)] + return [ + _failure("specification-coverage-bundle-invalid", str(exc), MANIFEST_PATH) + ] failures: list[PolicyFailure] = [] for manifest_path, (manifest, protocol, snapshot, analysis) in bundles: - validator = validate_bundle if manifest_path == current_path else validate_historical_bundle + validator = ( + validate_bundle + if manifest_path == current_path + else validate_historical_bundle + ) failures.extend(validator(repo_root, manifest, protocol, snapshot, analysis)) return failures From 764accface02435a33d4c48c76c506ab8ffded07 Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Thu, 24 Sep 2026 03:37:57 +0200 Subject: [PATCH 3/6] Format specification coverage release check --- tools/check_specification_coverage.py | 41 ++++++--------------------- 1 file changed, 9 insertions(+), 32 deletions(-) diff --git a/tools/check_specification_coverage.py b/tools/check_specification_coverage.py index 21fe2161b..10ba95c52 100644 --- a/tools/check_specification_coverage.py +++ b/tools/check_specification_coverage.py @@ -88,14 +88,9 @@ def load_bundle( def load_bundles( repo_root: Path = REPO_ROOT, -) -> list[ - tuple[dict[str, object], dict[str, object], dict[str, object], dict[str, object]] -]: +) -> list[tuple[dict[str, object], dict[str, object], dict[str, object], dict[str, object]]]: records = _load_bundle_index(repo_root) - return [ - _load_bundle_record(repo_root, manifest_path, manifest) - for manifest_path, manifest in records - ] + return [_load_bundle_record(repo_root, manifest_path, manifest) for manifest_path, manifest in records] def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: @@ -107,9 +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") != "45.0.0" or { - record.get("revision") for _, record in records - } != { + if dict(records)[current_path].get("revision") != "45.0.0" or {record.get("revision") for _, record in records} != { "1.0.0", "1.1.0", "2.0.0", @@ -157,9 +150,7 @@ def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: "44.0.0", "45.0.0", }: - raise ValueError( - "coverage evidence requires the explicit current 45.0.0 release and supported history" - ) + raise ValueError("coverage evidence requires the explicit current 45.0.0 release and supported history") return records @@ -177,22 +168,14 @@ def _load_bundle_record( for label in ("protocol", "snapshot", "analysis"): path_value = manifest[f"{label}_path"] sha_value = manifest[f"{label}_sha256"] - resolved = ( - safe_repo_path(repo_root, path_value) - if isinstance(path_value, str) - else None - ) + resolved = safe_repo_path(repo_root, path_value) if isinstance(path_value, str) else None if resolved is None or not resolved.is_file(): - raise ValueError( - f"{manifest_path!r} contains unsafe or missing {label}_path" - ) + raise ValueError(f"{manifest_path!r} contains unsafe or missing {label}_path") if not isinstance(sha_value, str) or not _SHA256_RE.fullmatch(sha_value): raise ValueError(f"{manifest_path!r} contains invalid {label}_sha256") if _sha256(resolved) != sha_value: raise ValueError(f"{manifest_path!r} contains stale {label}_sha256") - loaded.append( - load_bounded_json_object(repo_root, path_value, max_bytes=_MAX_FILE_BYTES) - ) + loaded.append(load_bounded_json_object(repo_root, path_value, max_bytes=_MAX_FILE_BYTES)) return manifest, loaded[0], loaded[1], loaded[2] @@ -205,16 +188,10 @@ def evaluate(repo_root: Path = REPO_ROOT) -> list[PolicyFailure]: for manifest_path, manifest in records ] except (OSError, ValueError) as exc: - return [ - _failure("specification-coverage-bundle-invalid", str(exc), MANIFEST_PATH) - ] + return [_failure("specification-coverage-bundle-invalid", str(exc), MANIFEST_PATH)] failures: list[PolicyFailure] = [] for manifest_path, (manifest, protocol, snapshot, analysis) in bundles: - validator = ( - validate_bundle - if manifest_path == current_path - else validate_historical_bundle - ) + validator = validate_bundle if manifest_path == current_path else validate_historical_bundle failures.extend(validator(repo_root, manifest, protocol, snapshot, analysis)) return failures From 3409a5ab3abdf515877e0950cd278b9a6302380f Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Thu, 24 Sep 2026 03:46:25 +0200 Subject: [PATCH 4/6] Refresh formal semantic evidence for current source --- .../analysis-v45.json | 155 +++++ .../bundles/retest-v45.json | 122 ++++ .../execution-snapshot-v45.json | 652 ++++++++++++++++++ .../formal-semantic-validation/index.md | 11 +- .../tests/test_formal_semantic_validation.py | 5 +- tools/formal_semantic_validation/_baseline.py | 3 +- tools/formal_semantic_validation/_loading.py | 5 +- .../_release_revisions.py | 3 +- tools/formal_semantic_validation/_releases.py | 7 +- tools/formal_semantic_validation/_retest.py | 2 +- 10 files changed, 953 insertions(+), 12 deletions(-) create mode 100644 docs/research/formal-semantic-validation/analysis-v45.json create mode 100644 docs/research/formal-semantic-validation/bundles/retest-v45.json create mode 100644 docs/research/formal-semantic-validation/execution-snapshot-v45.json diff --git a/docs/research/formal-semantic-validation/analysis-v45.json b/docs/research/formal-semantic-validation/analysis-v45.json new file mode 100644 index 000000000..c574a244f --- /dev/null +++ b/docs/research/formal-semantic-validation/analysis-v45.json @@ -0,0 +1,155 @@ +{ + "analysis_id": "issue-1357-analysis-v45", + "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-v45.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-1357-execution-v45", + "generated_at": "2026-09-24", + "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.", + "This source replay includes issue #1357 governed v2 admission, which is tested by its dedicated runtime suite; this retained formal corpus makes no additional crossing-authorization claim." + ], + "plain_language_outcome": "The retained formal semantic-validation corpus replays its existing obligations on the current implementation. Governed v2 decision admission is tested separately; this release adds no new authorization claim.", + "protocol_revision": "2.0.0" +} diff --git a/docs/research/formal-semantic-validation/bundles/retest-v45.json b/docs/research/formal-semantic-validation/bundles/retest-v45.json new file mode 100644 index 000000000..54fd1b350 --- /dev/null +++ b/docs/research/formal-semantic-validation/bundles/retest-v45.json @@ -0,0 +1,122 @@ +{ + "analysis_path": "docs/research/formal-semantic-validation/analysis-v45.json", + "analysis_sha256": "c2066d6fd9fed2f4de9297a8a7c984d38fa7f7e2a832f7e0b742b4269946d25a", + "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": "46.0.0", + "snapshot_path": "docs/research/formal-semantic-validation/execution-snapshot-v45.json", + "snapshot_sha256": "667aaca87402497964fc5a2286f0017fab51ce8d431f54281765db173c5d0478" +} diff --git a/docs/research/formal-semantic-validation/execution-snapshot-v45.json b/docs/research/formal-semantic-validation/execution-snapshot-v45.json new file mode 100644 index 000000000..650e1ced4 --- /dev/null +++ b/docs/research/formal-semantic-validation/execution-snapshot-v45.json @@ -0,0 +1,652 @@ +{ + "baseline": { + "execution_id": "issue-218-execution-v44", + "release_path": "docs/research/formal-semantic-validation/bundles/retest-v44.json", + "release_revision": "45.0.0", + "release_sha256": "64e562329eef767b3d75b5a0457aa0a36dd36da2d8eacec6880aa4dfdf1b9c3b" + }, + "captured_at": "2026-09-24T01:44:28.097138+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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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-1357-execution-v45", + "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": "764accface02435a33d4c48c76c506ab8ffded07", + "source_state": { + "base_revision": "764accface02435a33d4c48c76c506ab8ffded07", + "checkout_state": "modified", + "implementation_digest": "a6c52cd21e5a4847632b60abdaf57cb6046687474a41cdcd7457748851232294", + "profile": "python-reference-source/v2" + }, + "versions": { + "python": "3.11.15", + "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 a2fbe8266..da3f6c58e 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 45.0.0, rejects unsupported future +Current validation requires explicit release 46.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 @@ -440,10 +440,17 @@ refactoring in [`execution-snapshot-v43.json`](execution-snapshot-v43.json) and [`analysis-v43.json`](analysis-v43.json). Fresh replay retains the same bounded outcomes and claim limits; it does not add a new semantic claim. -Current release 45.0.0 records the merged participant identity and local +Release 45.0.0 records the merged participant identity and local outcome implementation in [`execution-snapshot-v44.json`](execution-snapshot-v44.json) and [`analysis-v44.json`](analysis-v44.json). The two pre-merge issue #218 captures retain their observations and source identities in v42 and v43; only their release numbers, paths, and corresponding digest joins were reconciled with the independently published issue #1338 capture. The combined capture uses the issue #1338 baseline and preserves the same bounded claim limits. + +Current release 46.0.0 replays the retained controls against the source state +containing issue #1357's governed v2 decision admission. Its +[`execution snapshot`](execution-snapshot-v45.json) and +[`analysis`](analysis-v45.json) retain the previous claim limits. Crossing +authorization is exercised by dedicated runtime tests, outside this formal +corpus. diff --git a/implementations/python/tests/test_formal_semantic_validation.py b/implementations/python/tests/test_formal_semantic_validation.py index a026dec57..864544cb6 100644 --- a/implementations/python/tests/test_formal_semantic_validation.py +++ b/implementations/python/tests/test_formal_semantic_validation.py @@ -124,6 +124,7 @@ def test_atomic_release_index_validates_every_historical_bundle() -> None: "43.0.0", "44.0.0", "45.0.0", + "46.0.0", ] assert all(validate_release_bundle(REPO_ROOT, release) == [] for release in releases) @@ -132,10 +133,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"] == "45.0.0" + assert release.manifest["revision"] == "46.0.0" assert protocol["revision"] == "2.0.0" assert corpus["revision"] == "4.0.0" - assert snapshot["baseline"]["release_revision"] == "42.0.0" + assert snapshot["baseline"]["release_revision"] == "45.0.0" assert snapshot["deviations"] == [] assert validate_retest_bundle(REPO_ROOT, release, protocol, corpus, snapshot, analysis) == [] diff --git a/tools/formal_semantic_validation/_baseline.py b/tools/formal_semantic_validation/_baseline.py index 22ecd31ed..35c22fa96 100644 --- a/tools/formal_semantic_validation/_baseline.py +++ b/tools/formal_semantic_validation/_baseline.py @@ -74,6 +74,7 @@ "42.0.0", "43.0.0", "44.0.0", + "45.0.0", } ) _V3_CORPUS_REVISIONS = frozenset( @@ -222,7 +223,7 @@ def _selected_baseline_manifest( if baseline_revision in _V2_REVISIONS else "docs/research/formal-semantic-validation/protocol-v1.json" ) - if baseline_revision == "42.0.0": + if baseline_revision in {"42.0.0", "45.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 c05945aac..873dcff8e 100644 --- a/tools/formal_semantic_validation/_loading.py +++ b/tools/formal_semantic_validation/_loading.py @@ -75,6 +75,7 @@ def load_release_bundles(repo_root: Path = REPO_ROOT) -> list[EvidenceRelease]: "43.0.0", "44.0.0", "45.0.0", + "46.0.0", }: raise ValueError("formal evidence requires every supported historical and current release") releases: list[EvidenceRelease] = [] @@ -121,6 +122,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") != "45.0.0" or release.protocol.get("revision") != "2.0.0": - raise ValueError("the current formal evidence release must be the explicit 45.0.0 retest") + if release.manifest.get("revision") != "46.0.0" or release.protocol.get("revision") != "2.0.0": + raise ValueError("the current formal evidence release must be the explicit 46.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 2710eff1b..851561e53 100644 --- a/tools/formal_semantic_validation/_release_revisions.py +++ b/tools/formal_semantic_validation/_release_revisions.py @@ -44,8 +44,9 @@ "42.0.0", "43.0.0", "44.0.0", + "45.0.0", } ) -_SUPPORTED_RETEST_REVISIONS = _HISTORICAL_RETEST_REVISIONS | {"45.0.0"} +_SUPPORTED_RETEST_REVISIONS = _HISTORICAL_RETEST_REVISIONS | {"46.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 4a45b2446..46fd67a0d 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") == "45.0.0", + replay_current=manifest.get("revision") == "46.0.0", ) ) else: @@ -244,7 +244,7 @@ def validate_retest_bundle( return [ _failure( "formal-validation-current-replay-required", - "only releases 3.0.0 through 44.0.0 can use integrated historical validation", + "only releases 3.0.0 through 45.0.0 can use integrated historical validation", snapshot_path, ) ] @@ -292,7 +292,7 @@ def validate_retest_bundle( } else "2.0.0" ) - if release_revision in {"42.0.0", "45.0.0"}: + if release_revision in {"42.0.0", "45.0.0", "46.0.0"}: expected_corpus_revision = "4.0.0" if protocol.get("revision") != "2.0.0" or corpus.get("revision") != expected_corpus_revision: failures.append( @@ -399,6 +399,7 @@ def _current_retest_source_failures( "43.0.0": "41.0.0", "44.0.0": "43.0.0", "45.0.0": "42.0.0", + "46.0.0": "45.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 cc8d62700..b8d81d0b4 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, 46)) +_SOURCE_STATE_REVISIONS = frozenset(f"{revision}.0.0" for revision in range(4, 47)) @dataclasses.dataclass(frozen=True) From 6dc9d034fa1f1ef5682917926ff7b9455ac479ec Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Thu, 24 Sep 2026 03:53:17 +0200 Subject: [PATCH 5/6] Align evidence release tests with current revisions --- .../python/tests/test_issue_989_versioned_evidence.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/implementations/python/tests/test_issue_989_versioned_evidence.py b/implementations/python/tests/test_issue_989_versioned_evidence.py index e74645b01..35199486c 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"] == "45.0.0" + assert release.manifest["revision"] == "46.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"] == "44.0.0" + assert manifest["revision"] == "45.0.0" snapshot = deepcopy(snapshot) artifact = next(a for a in snapshot["artifacts"] if a["artifact_id"] == artifact_id) artifact["sha256"] = old_digest @@ -497,6 +497,7 @@ def test_no_capture_can_be_silently_dropped(monkeypatch, family, removed): "43.0.0", "44.0.0", "45.0.0", + "46.0.0", ] if family == "formal" else [ @@ -545,6 +546,7 @@ def test_no_capture_can_be_silently_dropped(monkeypatch, family, removed): "42.0.0", "43.0.0", "44.0.0", + "45.0.0", ] ) revisions.pop(-1 if removed == "current" else 0) From 817c9661701a4d78c45faddee973f43f2d647bdd Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Thu, 24 Sep 2026 04:17:32 +0200 Subject: [PATCH 6/6] Clarify unauthorized admission exception test --- .../test_sem_220_participant_decision_surface_v2_runtime.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/implementations/python/tests/test_sem_220_participant_decision_surface_v2_runtime.py b/implementations/python/tests/test_sem_220_participant_decision_surface_v2_runtime.py index 15796ad60..acce7ee16 100644 --- a/implementations/python/tests/test_sem_220_participant_decision_surface_v2_runtime.py +++ b/implementations/python/tests/test_sem_220_participant_decision_surface_v2_runtime.py @@ -338,6 +338,7 @@ def test_v2_governed_admission_rejects_unauthorized_caller(unauthorized: str) -> else: caller = identity(participant_address="participant.behavior.other") + crossing_evidence = evidence() with pytest.raises(PermissionError): _admit_governed_selection( control, @@ -345,7 +346,7 @@ def test_v2_governed_admission_rejects_unauthorized_caller(unauthorized: str) -> implementation_selection, delivery, identity=caller, - crossing_evidence=evidence(), + crossing_evidence=crossing_evidence, ) assert control.get_snapshot().snapshot.participant_behavior_history.get(PARTICIPANT, []) == []