From 39c499163aebc6a6eefc352b14b2dfb55013bb92 Mon Sep 17 00:00:00 2001 From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com> Date: Fri, 9 Oct 2026 03:47:59 -0700 Subject: [PATCH 1/4] fix(runtime): order workflow compensation by completion instant, not timestamp text Producers format step completion times with isoformat(), which drops the fraction on a whole second, so a later completion stamped ...:01.001000Z sorted before an earlier one stamped ...:01Z and compensation ran in completion order. Sort completed steps by the parsed instant. --- .../raes_runtime/control_plane_workflows.py | 4 +- .../test_issue_1462_compensation_order.py | 117 ++++++++++++++++++ 2 files changed, 120 insertions(+), 1 deletion(-) create mode 100644 implementations/python/tests/test_issue_1462_compensation_order.py diff --git a/implementations/python/packages/raes_runtime/control_plane_workflows.py b/implementations/python/packages/raes_runtime/control_plane_workflows.py index 78b6cbbe4..e1f2764b7 100644 --- a/implementations/python/packages/raes_runtime/control_plane_workflows.py +++ b/implementations/python/packages/raes_runtime/control_plane_workflows.py @@ -49,7 +49,9 @@ def maybe_apply_compensation( assert contract is not None completed_events = _completed_compensable_events(history, contract) if completed_events: - ordered = sorted(completed_events, key=lambda event: event.timestamp, reverse=True) + # Order by instant: producers format with isoformat(), which drops the fraction on a whole second, so + # the text of a later completion can sort before an earlier one. + ordered = sorted(completed_events, key=lambda event: parse_timestamp(event.timestamp), reverse=True) updated_history = list(history) _append_compensation_history(updated_history, ordered, contract, result, submitted_at) payload = _compensated_workflow_payload(result, submitted_at) diff --git a/implementations/python/tests/test_issue_1462_compensation_order.py b/implementations/python/tests/test_issue_1462_compensation_order.py new file mode 100644 index 000000000..bc7c56d8e --- /dev/null +++ b/implementations/python/tests/test_issue_1462_compensation_order.py @@ -0,0 +1,117 @@ +"""Issue #1462: compensation runs in reverse completion order for the timestamps producers emit.""" + +from __future__ import annotations + +from datetime import datetime, timedelta + +from raes import parse_sdl +from raes_backend_stubs.stubs import create_stub_target +from raes_processor.compiler import compile_runtime_model +from raes_processor.planner import plan +from raes_runtime.control_plane import RuntimeControlPlane + +_WORKFLOW = "orchestration.workflow.response" +_SCENARIO = """ +name: workflow +nodes: + vm: + type: compute + resources: {ram: 1 gib, cpu: 1} + conditions: {health: ops} + roles: {ops: operator} +conditions: + health: {command: /bin/true, interval: 15} +propositions: + health: + description: The governed VM has declared runtime state. + subjects: [nodes.vm] + basis: declared_state + predicate: {kind: presence, property: runtime, semantic_ref: urn:raes:declared-property:runtime, operator: exists} +assertions: + health: {proposition: health, role: postcondition, polarity: positive} +entities: + blue: {role: blue} +objectives: + validate: + owner: blue + success: {assertions: [health]} + verify: + owner: blue + success: {assertions: [health]} +workflows: + rollback-a: + start: finish + steps: + finish: {type: end} + rollback-b: + start: finish + steps: + finish: {type: end} + response: + start: a + compensation: + mode: automatic + on: [cancelled] + steps: + a: {type: objective, objective: validate, compensate_with: rollback-a, on_success: b, on_failure: finish} + b: {type: objective, objective: verify, compensate_with: rollback-b, on_success: finish, on_failure: finish} + finish: {type: end} +""" + + +def _producer_timestamp(instant: datetime) -> str: + # The RAES runtime (control_plane_execution._utc_now) and the LilRAE workflow engine both format instants with + # isoformat(), which drops the fraction when the microsecond is zero. + return instant.isoformat().replace("+00:00", "Z") + + +def _step_completed(step_name: str, timestamp: str) -> dict[str, object]: + return { + "event_type": "step_completed", + "timestamp": timestamp, + "step_name": step_name, + "branch_name": None, + "join_step": None, + "outcome": "succeeded", + "details": {}, + } + + +def test_cancellation_compensates_the_later_step_first_across_a_whole_second() -> None: + target = create_stub_target() + execution_plan = plan(compile_runtime_model(parse_sdl(_SCENARIO)), target.manifest) + control_plane = RuntimeControlPlane(target) + control_plane.register_planner_produced_plan(execution_plan) + assert control_plane.submit_provisioning(execution_plan.provisioning).accepted + assert control_plane.submit_evaluation(execution_plan.evaluation).accepted + assert control_plane.submit_orchestration(execution_plan.orchestration).accepted + snapshot = control_plane.snapshot + result = dict(snapshot.orchestration_results[_WORKFLOW]) + started = datetime.fromisoformat(result["started_at"].replace("Z", "+00:00")) + a_completed = (started + timedelta(seconds=1)).replace(microsecond=0) + b_completed = a_completed + timedelta(milliseconds=1) + completed = {"lifecycle": "completed", "outcome": "succeeded", "attempts": 1} + result["steps"] = {**result["steps"], "a": completed, "b": completed} + seeded = snapshot.with_entries( + dict(snapshot.entries), + orchestration_results={**snapshot.orchestration_results, _WORKFLOW: result}, + orchestration_history={ + **snapshot.orchestration_history, + _WORKFLOW: [ + *snapshot.orchestration_history[_WORKFLOW], + _step_completed("a", _producer_timestamp(a_completed)), + _step_completed("b", _producer_timestamp(b_completed)), + ], + }, + ) + control_plane._store.save_snapshot(seeded, expected_revision=control_plane._store.load_snapshot_state().revision) + + receipt = control_plane.cancel_workflow(_WORKFLOW, reason="operator requested stop") + + history = control_plane.snapshot.orchestration_history[_WORKFLOW] + control_plane.close() + assert receipt.accepted, receipt.diagnostics + assert [event["step_name"] for event in history if event["event_type"] == "compensation_registered"] == [ + "b", + "a", + ] From 03417e5fe2aa0f4417a3f940eb5f1493dbb3308c Mon Sep 17 00:00:00 2001 From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com> Date: Fri, 9 Oct 2026 05:44:36 -0700 Subject: [PATCH 2/4] fix(runtime): read offset-less completion timestamps as UTC when ordering compensation The compensation sort used the strict parse_timestamp, which raises on a timestamp without an offset. The workflow history contract checks admit such a value and read it as UTC, so cancelling or timing out a workflow with an admitted offset-less completion raised instead of compensating. Sort with the parser those checks use (diagnostics._parse_timestamp). The regression test now seeds every instant in the past, so the history stays monotonic after the cancellation or timeout. It covers both compensation triggers and three admitted timestamp forms. --- .../raes_runtime/control_plane_workflows.py | 9 +- .../test_issue_1462_compensation_order.py | 98 +++++++++++++------ 2 files changed, 73 insertions(+), 34 deletions(-) diff --git a/implementations/python/packages/raes_runtime/control_plane_workflows.py b/implementations/python/packages/raes_runtime/control_plane_workflows.py index e1f2764b7..0543adf99 100644 --- a/implementations/python/packages/raes_runtime/control_plane_workflows.py +++ b/implementations/python/packages/raes_runtime/control_plane_workflows.py @@ -13,6 +13,8 @@ WorkflowHistoryEventType, ) +from .diagnostics import _parse_timestamp + _EXPLICIT_OFFSET_TIMESTAMP_ERROR = "timestamp must be an ISO-8601 value with an explicit UTC offset" @@ -49,9 +51,10 @@ def maybe_apply_compensation( assert contract is not None completed_events = _completed_compensable_events(history, contract) if completed_events: - # Order by instant: producers format with isoformat(), which drops the fraction on a whole second, so - # the text of a later completion can sort before an earlier one. - ordered = sorted(completed_events, key=lambda event: parse_timestamp(event.timestamp), reverse=True) + # Order by instant, parsed the way the history contract checks parse it (an offset-less value is UTC). + # Producers format with isoformat(), which drops the fraction on a whole second, so the text of a later + # completion can sort before an earlier one. + ordered = sorted(completed_events, key=lambda event: _parse_timestamp(event.timestamp), reverse=True) updated_history = list(history) _append_compensation_history(updated_history, ordered, contract, result, submitted_at) payload = _compensated_workflow_payload(result, submitted_at) diff --git a/implementations/python/tests/test_issue_1462_compensation_order.py b/implementations/python/tests/test_issue_1462_compensation_order.py index bc7c56d8e..d0afa431b 100644 --- a/implementations/python/tests/test_issue_1462_compensation_order.py +++ b/implementations/python/tests/test_issue_1462_compensation_order.py @@ -1,16 +1,21 @@ -"""Issue #1462: compensation runs in reverse completion order for the timestamps producers emit.""" +"""Issue #1462: compensation runs in reverse completion order for every timestamp form the history contract admits.""" from __future__ import annotations -from datetime import datetime, timedelta +from collections.abc import Callable +import pytest from raes import parse_sdl from raes_backend_stubs.stubs import create_stub_target +from raes_contracts.runtime_state import OperationReceipt from raes_processor.compiler import compile_runtime_model from raes_processor.planner import plan from raes_runtime.control_plane import RuntimeControlPlane +from raes_runtime.result_contracts import workflow_result_contract_diagnostics _WORKFLOW = "orchestration.workflow.response" +# Every seeded instant lies in the past, so the cancellation or timeout the runtime stamps now follows them. +_STARTED_AT = "2000-01-01T00:00:00.500000Z" _SCENARIO = """ name: workflow nodes: @@ -49,9 +54,10 @@ finish: {type: end} response: start: a + timeout: 1 compensation: mode: automatic - on: [cancelled] + on: [cancelled, timed_out] steps: a: {type: objective, objective: validate, compensate_with: rollback-a, on_success: b, on_failure: finish} b: {type: objective, objective: verify, compensate_with: rollback-b, on_success: finish, on_failure: finish} @@ -59,10 +65,12 @@ """ -def _producer_timestamp(instant: datetime) -> str: - # The RAES runtime (control_plane_execution._utc_now) and the LilRAE workflow engine both format instants with - # isoformat(), which drops the fraction when the microsecond is zero. - return instant.isoformat().replace("+00:00", "Z") +def _cancel(control_plane: RuntimeControlPlane) -> OperationReceipt: + return control_plane.cancel_workflow(_WORKFLOW, reason="operator requested stop") + + +def _reconcile_timeouts(control_plane: RuntimeControlPlane) -> OperationReceipt: + return control_plane.reconcile_workflow_timeouts() def _step_completed(step_name: str, timestamp: str) -> dict[str, object]: @@ -77,41 +85,69 @@ def _step_completed(step_name: str, timestamp: str) -> dict[str, object]: } -def test_cancellation_compensates_the_later_step_first_across_a_whole_second() -> None: - target = create_stub_target() - execution_plan = plan(compile_runtime_model(parse_sdl(_SCENARIO)), target.manifest) - control_plane = RuntimeControlPlane(target) - control_plane.register_planner_produced_plan(execution_plan) - assert control_plane.submit_provisioning(execution_plan.provisioning).accepted - assert control_plane.submit_evaluation(execution_plan.evaluation).accepted - assert control_plane.submit_orchestration(execution_plan.orchestration).accepted +def _seed_completed_steps(control_plane: RuntimeControlPlane, a_completed: str, b_completed: str) -> None: snapshot = control_plane.snapshot - result = dict(snapshot.orchestration_results[_WORKFLOW]) - started = datetime.fromisoformat(result["started_at"].replace("Z", "+00:00")) - a_completed = (started + timedelta(seconds=1)).replace(microsecond=0) - b_completed = a_completed + timedelta(milliseconds=1) completed = {"lifecycle": "completed", "outcome": "succeeded", "attempts": 1} + result = { + **snapshot.orchestration_results[_WORKFLOW], + "started_at": _STARTED_AT, + "updated_at": _STARTED_AT, + } result["steps"] = {**result["steps"], "a": completed, "b": completed} + history = [{**event, "timestamp": _STARTED_AT} for event in snapshot.orchestration_history[_WORKFLOW]] seeded = snapshot.with_entries( dict(snapshot.entries), orchestration_results={**snapshot.orchestration_results, _WORKFLOW: result}, orchestration_history={ **snapshot.orchestration_history, - _WORKFLOW: [ - *snapshot.orchestration_history[_WORKFLOW], - _step_completed("a", _producer_timestamp(a_completed)), - _step_completed("b", _producer_timestamp(b_completed)), - ], + _WORKFLOW: [*history, _step_completed("a", a_completed), _step_completed("b", b_completed)], }, ) + assert workflow_result_contract_diagnostics(seeded) == [] control_plane._store.save_snapshot(seeded, expected_revision=control_plane._store.load_snapshot_state().revision) - receipt = control_plane.cancel_workflow(_WORKFLOW, reason="operator requested stop") - history = control_plane.snapshot.orchestration_history[_WORKFLOW] - control_plane.close() +@pytest.mark.parametrize( + ("trigger", "status"), + [(_cancel, "cancelled"), (_reconcile_timeouts, "timed_out")], + ids=["cancelled", "timed_out"], +) +@pytest.mark.parametrize( + ("a_completed", "b_completed"), + [ + # LilRAE's workflow engine stamps each event 1 ms after the previous one with isoformat(), which drops the + # fraction on a whole second, so the later completion sorts first as text. + ("2000-01-01T00:00:01Z", "2000-01-01T00:00:01.001000Z"), + # The history contract checks read an offset-less value as UTC. + ("2000-01-01T00:00:01", "2000-01-01T00:00:01.001000"), + # With an explicit non-UTC offset, the earlier completion sorts last as text. + ("2000-01-01T02:00:01+02:00", "2000-01-01T00:00:01.001000Z"), + ], + ids=["isoformat-whole-second", "offset-less", "explicit-offset"], +) +def test_compensation_registers_the_later_step_first( + trigger: Callable[[RuntimeControlPlane], OperationReceipt], + status: str, + a_completed: str, + b_completed: str, +) -> None: + target = create_stub_target() + execution_plan = plan(compile_runtime_model(parse_sdl(_SCENARIO)), target.manifest) + control_plane = RuntimeControlPlane(target) + try: + control_plane.register_planner_produced_plan(execution_plan) + assert control_plane.submit_provisioning(execution_plan.provisioning).accepted + assert control_plane.submit_evaluation(execution_plan.evaluation).accepted + assert control_plane.submit_orchestration(execution_plan.orchestration).accepted + _seed_completed_steps(control_plane, a_completed, b_completed) + + receipt = trigger(control_plane) + snapshot = control_plane.snapshot + finally: + control_plane.close() + assert receipt.accepted, receipt.diagnostics - assert [event["step_name"] for event in history if event["event_type"] == "compensation_registered"] == [ - "b", - "a", - ] + assert snapshot.orchestration_results[_WORKFLOW]["workflow_status"] == status + history = snapshot.orchestration_history[_WORKFLOW] + assert [event["step_name"] for event in history if event["event_type"] == "compensation_registered"] == ["b", "a"] + assert workflow_result_contract_diagnostics(snapshot) == [] From 105dfbc0d841ef779aa4a32656d5c5c20c2fb9a3 Mon Sep 17 00:00:00 2001 From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com> Date: Sat, 10 Oct 2026 06:23:53 -0700 Subject: [PATCH 3/4] fix(runtime): compensate equal-instant completions in reverse history order sorted(..., reverse=True) is stable, so completions with equal instants kept their history order and were compensated in the order they ran. The workflow history contract checks reject only decreasing timestamps, so in an admitted history the history order of equal instants is their completion order. Sort ascending and reverse the list in place, so that equal instants are also compensated in reverse completion order. The reversal is an explicit list.reverse() call. SonarCloud reported sorted(...)[::-1] as python:S7511 ("Remove this redundant subscript reversal"). The reversal is not redundant, and sorted(..., reverse=True) is not equivalent here: it keeps equal keys in their original order. The regression test gains an identical-instant pair and a pair that writes one instant two ways (+00:00, then Z). It now asserts the order of compensation_workflow_started events, the execution order that specs/formal/workflows/compensation.md requires. --- .../raes_runtime/control_plane_workflows.py | 7 +++++-- .../tests/test_issue_1462_compensation_order.py | 17 +++++++++++++---- 2 files changed, 18 insertions(+), 6 deletions(-) diff --git a/implementations/python/packages/raes_runtime/control_plane_workflows.py b/implementations/python/packages/raes_runtime/control_plane_workflows.py index 0543adf99..940bff7e7 100644 --- a/implementations/python/packages/raes_runtime/control_plane_workflows.py +++ b/implementations/python/packages/raes_runtime/control_plane_workflows.py @@ -53,8 +53,11 @@ def maybe_apply_compensation( if completed_events: # Order by instant, parsed the way the history contract checks parse it (an offset-less value is UTC). # Producers format with isoformat(), which drops the fraction on a whole second, so the text of a later - # completion can sort before an earlier one. - ordered = sorted(completed_events, key=lambda event: _parse_timestamp(event.timestamp), reverse=True) + # completion can sort before an earlier one. Admitted histories have non-decreasing timestamps, so for equal + # instants the history order is the completion order. The stable ascending sort, reversed, compensates those + # steps in reverse history order; reverse=True would keep them in history order. + ordered = sorted(completed_events, key=lambda event: _parse_timestamp(event.timestamp)) + ordered.reverse() updated_history = list(history) _append_compensation_history(updated_history, ordered, contract, result, submitted_at) payload = _compensated_workflow_payload(result, submitted_at) diff --git a/implementations/python/tests/test_issue_1462_compensation_order.py b/implementations/python/tests/test_issue_1462_compensation_order.py index d0afa431b..b940c08f3 100644 --- a/implementations/python/tests/test_issue_1462_compensation_order.py +++ b/implementations/python/tests/test_issue_1462_compensation_order.py @@ -1,4 +1,8 @@ -"""Issue #1462: compensation runs in reverse completion order for every timestamp form the history contract admits.""" +"""Issue #1462: compensation runs in reverse completion order. + +Covered completion timestamp pairs: a whole second written without its fraction, offset-less, a non-UTC offset, one +instant written twice the same way, and one instant written two ways. +""" from __future__ import annotations @@ -122,10 +126,14 @@ def _seed_completed_steps(control_plane: RuntimeControlPlane, a_completed: str, ("2000-01-01T00:00:01", "2000-01-01T00:00:01.001000"), # With an explicit non-UTC offset, the earlier completion sorts last as text. ("2000-01-01T02:00:01+02:00", "2000-01-01T00:00:01.001000Z"), + # The history contract checks reject only decreasing timestamps, so for equal instants the history order is + # the completion order: b, recorded after a, ran after it. + ("2000-01-01T00:00:01Z", "2000-01-01T00:00:01Z"), + ("2000-01-01T00:00:01+00:00", "2000-01-01T00:00:01Z"), ], - ids=["isoformat-whole-second", "offset-less", "explicit-offset"], + ids=["isoformat-whole-second", "offset-less", "explicit-offset", "identical-instant", "same-instant-two-forms"], ) -def test_compensation_registers_the_later_step_first( +def test_compensation_runs_the_later_step_first( trigger: Callable[[RuntimeControlPlane], OperationReceipt], status: str, a_completed: str, @@ -149,5 +157,6 @@ def test_compensation_registers_the_later_step_first( assert receipt.accepted, receipt.diagnostics assert snapshot.orchestration_results[_WORKFLOW]["workflow_status"] == status history = snapshot.orchestration_history[_WORKFLOW] - assert [event["step_name"] for event in history if event["event_type"] == "compensation_registered"] == ["b", "a"] + started = [event["step_name"] for event in history if event["event_type"] == "compensation_workflow_started"] + assert started == ["b", "a"] assert workflow_result_contract_diagnostics(snapshot) == [] From 421ed21e98e749c54d3adb53057bacfcb78e166b Mon Sep 17 00:00:00 2001 From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com> Date: Tue, 13 Oct 2026 11:36:52 +0000 Subject: [PATCH 4/4] test: record research captures for issue #1462 Records content-addressed specification-coverage and formal-semantic-validation captures for this branch's source with python -m tools.research_capture record, from dev's newest captures as templates. --- ...3292d6be864fb04d8b534178dc8e130c7c73a.json | 4 + .../analysis.json | 171 +++++ .../manifest.json | 122 +++ .../snapshot.json | 652 ++++++++++++++++ ...e4e8a90ac287bf891bf44fbefc5ec91d123ae.json | 4 + .../analysis.json | 118 +++ .../manifest.json | 10 + .../snapshot.json | 708 ++++++++++++++++++ 8 files changed, 1789 insertions(+) create mode 100644 docs/research/formal-semantic-validation/capture-records/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a.json create mode 100644 docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/analysis.json create mode 100644 docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/manifest.json create mode 100644 docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/snapshot.json create mode 100644 docs/research/specification-coverage/capture-records/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae.json create mode 100644 docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/analysis.json create mode 100644 docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/manifest.json create mode 100644 docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/snapshot.json diff --git a/docs/research/formal-semantic-validation/capture-records/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a.json b/docs/research/formal-semantic-validation/capture-records/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a.json new file mode 100644 index 000000000..93530c92c --- /dev/null +++ b/docs/research/formal-semantic-validation/capture-records/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a.json @@ -0,0 +1,4 @@ +{ + "capture_path": "docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/manifest.json", + "capture_sha256": "36aee775f771e87471b682e4d4eb6a7c378c78ccd4db0e9bf28fc405e633030f" +} diff --git a/docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/analysis.json b/docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/analysis.json new file mode 100644 index 000000000..afd866aea --- /dev/null +++ b/docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/analysis.json @@ -0,0 +1,171 @@ +{ + "analysis_id": "issue-1462-formal-analysis-c942f79a9e01", + "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", + "@snapshot", + "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-1462-formal-c942f79a9e01", + "generated_at": "2026-10-13T11:36:35.817106+00:00", + "limitations": [ + "Satisfiability is limited to raes-finite-domain-satisfiability-v1 and its exact translation, theory, and Z3 configuration.", + "The subset-minimal unsatisfiable core is not a universal proof certificate.", + "Exploit-path results are limited to the admitted snapshot, normalized graph, query, transition semantics, and bounded search profile.", + "A valid path is not backend execution and an invalid path is not real-world non-exploitability.", + "The production exploit-path JSON loader permits duplicate keys; the research loader rejects them without claiming stronger production behavior.", + "Participant replay inherits the host environment and is not described as hermetic.", + "Counterfactual necessity remains untested.", + "Scoped observation demand is not a claim class in this preregistration and is not promoted to demonstrated by this retest.", + "EXP-732 provenance joins are verified by their dedicated regression suite; this retained corpus makes no universal run, apparatus, source, or augmentation assurance claim.", + "This retained corpus does not establish native backend attestation fidelity; materialization contract checks remain separate operational provenance, not experimental observations.", + "Capture admission and evidence-proof authority are verified by issue-1237 regression tests, not promoted to a new claim class by this retained corpus.", + "Evidence-requirement refinement lineage is outside this retained formal claim set; this retest refreshes integrated source provenance without promoting that feature to a formal claim.", + "Authoring-adapter transport behavior is outside this retained formal claim set.", + "Operational recovery observation and startup reconciliation are verified by their API-404 regression suite, not promoted to a new formal claim class by this retained corpus.", + "Single-owner store admission, immutable target/run scope, and provider shutdown ordering are verified by their API-404 CP-5 regression suite, not promoted to a formal claim by this retained corpus.", + "Mixed and staged trial admission is verified by its SEM-234/SCE-002/API-407 regression suite, not promoted to a new formal claim class by this retained corpus.", + "Offline control-plane maintenance, readiness, and bounded audit behavior are verified by issue #1186 runtime tests, not promoted to a formal claim by this retained corpus.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 profile declarations and capability admission are covered by dedicated runtime tests; the retained formal corpus does not execute control-plane profile composition.", + "Issue #1016 mixed-runtime coordination is covered by dedicated runtime tests; the retained formal corpus does not establish backend-native mixed realization, multi-controller coordination, IFC, or equivalence.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Issue #1389 temporal-subject admission is verified by dedicated compiler tests and adds no new formal-semantic claim to this retained corpus.", + "Issue #971 model construction is verified by its own tests; this retained corpus establishes no participant-crossing equivalence or runtime-realization claim.", + "Issue #1359 control-plane route authority, participant-view scoping, and no-store HTTP boundary are verified by their dedicated HTTP-boundary suite and add no new formal-semantic claim to this retained corpus.", + "Issue #1401 required-evidence media-type coherence is verified by its dedicated suite and adds no new formal-semantic claim to this retained corpus.", + "Issue #1361 execution and recovery requirements are verified by dedicated policy, composition, and admission tests; this retained corpus establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 maintainability repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 resource type-hint repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The combined issue #1361 execution-policy and hatchling update preserves retained outcomes and bounded claims; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1418 runtime-fact export manifest split changes no contract, schema or behavior and adds no new formal-semantic claim.", + "The issue #1423 inject trigger request and occurrence contracts are new draft carriers that no SDL construct, compiler or runtime path reads, and they add no new formal-semantic claim.", + "The issue #1366 inject readback, correlation and backend declaration contracts are new draft carriers; the shared backend allowlist also lets SDL participant behavior specifications cite inject-occurrence-v1 and inject-occurrence-outcome-v1 as evidence_contract_refs, which the compiler copies through uninterpreted, and no runtime path or shipped backend reads or declares them; they add no new formal-semantic claim.", + "This synchronization preserves the original inject baseline chain in the pre-sync archive, retains frozen production and participant evidence, and binds the combined contract source. CI independently verifies current evidence replay; no new runtime adoption is claimed.", + "This second synchronization binds behavior-authoring source from issue #297, retains frozen production and participant evidence, and pins the preserved first-sync release 75 as its baseline. CI independently verifies replay; no new runtime adoption is claimed.", + "Issue #1091 request-boundary admission is verified by its dedicated tests; this retained corpus does not execute the served HTTP adapter or broaden its bounded claims.", + "This combined-source capture replays the supported retained corpus and the 18 declared participant test cases. The inject contract repair has 126 passing request, occurrence and readback tests; no runtime inject execution or broader formal claim is established. CI independently verifies replay.", + "Issue #1425's updated branch derives reference and libvirt specs from published plan operations. This retained corpus makes no new realization, HTTP relay, or backend-honesty claim.", + "Issue #1462 makes workflow compensation order completed steps by their parsed completion instant, compensating equal instants in reverse history order; this retained corpus makes no new claim." + ], + "plain_language_outcome": "The retained formal cases reproduce their outcomes after issue #1462 began ordering workflow compensation by parsed completion instant instead of timestamp text. Bounded claims and unsupported classes are unchanged.", + "protocol_revision": "2.0.0" +} diff --git a/docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/manifest.json b/docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/manifest.json new file mode 100644 index 000000000..3fa2dcac5 --- /dev/null +++ b/docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/manifest.json @@ -0,0 +1,122 @@ +{ + "analysis_path": "docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/analysis.json", + "analysis_sha256": "75dec5268482fa03f3ff7f07ed6b1e1c164a0560c1d7f9feaf4d50116db98b8b", + "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": "capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a", + "snapshot_path": "docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/snapshot.json", + "snapshot_sha256": "dcfd32a28f2f09ba352fc06b93e307219147c94851b78508caf69827f05718d1" +} diff --git a/docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/snapshot.json b/docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/snapshot.json new file mode 100644 index 000000000..1c7591e8b --- /dev/null +++ b/docs/research/formal-semantic-validation/captures/capture-bae7b3aac8ecc4f37b4bb524e1a3292d6be864fb04d8b534178dc8e130c7c73a/snapshot.json @@ -0,0 +1,652 @@ +{ + "baseline": { + "execution_id": "issue-1425-combined-formal-51496af2b628", + "release_path": "docs/research/formal-semantic-validation/captures/capture-2df4b6bd919dca53c37e0aef9766e5ff1333a235cf4a8f0050b47a74121088a2/manifest.json", + "release_revision": "capture-2df4b6bd919dca53c37e0aef9766e5ff1333a235cf4a8f0050b47a74121088a2", + "release_sha256": "c271782cf5baa098d7a55954b4989fcdab9c073df76a39bd7c5ac1296363a61a" + }, + "captured_at": "2026-10-13T11:36:35.817106+00:00", + "commands": [ + { + "argv": [ + "implementations/python/.venv/bin/python", + "-" + ], + "command_id": "retained-case-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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "limitations": [ + "The witness ends at compiled output." + ], + "replayable": true, + "result_digest": "d7c098c5d063b8d1b0747e8df5daa90061456065cdda0bbedfa10918442f5daa", + "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-1462-formal-c942f79a9e01", + "limitations": [ + "Distinct digests are a non-vacuity control, not semantic non-equivalence proof." + ], + "replayable": true, + "result_digest": "a2fcebba3341592b133af813e8bb8e5f47270418bc58bfd471a89bfbc8ba46da", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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-1462-formal-c942f79a9e01", + "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": "105dfbc0d841ef779aa4a32656d5c5c20c2fb9a3", + "source_state": { + "base_revision": "105dfbc0d841ef779aa4a32656d5c5c20c2fb9a3", + "checkout_state": "clean", + "implementation_digest": "c942f79a9e0155607e185ca306a312df57f70cf8be29d183e730882f08080b44", + "profile": "python-reference-source/v2" + }, + "versions": { + "python": "3.12.3", + "raes": "5.0.0", + "z3_engine": "4.16.0", + "z3_solver": "4.16.0.0" + } +} diff --git a/docs/research/specification-coverage/capture-records/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae.json b/docs/research/specification-coverage/capture-records/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae.json new file mode 100644 index 000000000..d19782486 --- /dev/null +++ b/docs/research/specification-coverage/capture-records/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae.json @@ -0,0 +1,4 @@ +{ + "capture_path": "docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/manifest.json", + "capture_sha256": "8b7c43eda26180c75c9ddd4c5e444b91364d0c9c4401626efea8befd90be74ff" +} diff --git a/docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/analysis.json b/docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/analysis.json new file mode 100644 index 000000000..d0613c6f4 --- /dev/null +++ b/docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/analysis.json @@ -0,0 +1,118 @@ +{ + "analysis_id": "issue-1462-specification-analysis-c942f79a9e01", + "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", + "@snapshot" + ], + "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-10-13T11:36:35.817106+00:00", + "limitations": [ + "This result demonstrates bounded specification coverage, not universal cyber-range coverage, usability, adoption, backend substitution, or behavioral equivalence.", + "The three missing concepts are evidence, not implementation tasks within this snapshot.", + "The retained protocol does not test recursive realization or plan-level profile semantics; this release only re-establishes its original bounded coverage result against the current implementation.", + "The retained protocol does not test evidence-requirement refinement lineage; the dedicated EXP-731 regression suite covers that production boundary.", + "Authoring-adapter transport behavior is outside this retained protocol.", + "Reviewed OCI mirror and pre-seed admission is covered by its own regression suites and the development artifact policy gate, not a new claim in this preregistered matrix.", + "Operational recovery observation and startup reconciliation are covered by their API-404 regression suite, not a new claim in this preregistered matrix.", + "Store ownership, immutable runtime scope, and provider shutdown ordering are covered by the API-404 CP-5 regression suite, not by this retained specification-coverage protocol.", + "Mixed/staged trial compilation and admission are covered by issue #1015 regression tests, not by this retained specification-coverage corpus; no live mixed-runtime result is claimed.", + "Issue #1186 control-plane recovery operations are covered by their runtime regression suite, not by this retained specification-coverage corpus.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 control-plane profile declarations are covered by their dedicated runtime suite, not promoted to new claims by the retained language corpus.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Participant-local outcome state is verified by the ACT-618 tests; this retained corpus makes no additional outcome-state claim.", + "Backend operation supervision contracts are covered by issue #1360 contract tests; this retained offline corpus establishes no live backend supervision or recovery guarantee.", + "This capture replays the merged issue #1360 and #1357 source; the protocol makes no live backend execution or supervision claim.", + "This capture replays the merged issue #1360 and #1358 source; the protocol makes no live backend execution or supervision claim.", + "Issue #1389 participant inject delivery temporal-subject admission is covered by dedicated compiler tests; this retained matrix makes no new timing or execution claim.", + "Issue #971 adds offline crossing model construction; this retained protocol establishes no crossing equivalence or runtime-realization claim.", + "Issue #1359 control-plane route authority, participant-view scoping, and no-store HTTP boundary are covered by their dedicated HTTP-boundary suite; this retained matrix makes no new exposure or execution claim.", + "Issue #1401 required-evidence media-type coherence is verified by its dedicated suite; this retained matrix makes no new admission or capture claim.", + "Issue #1361 execution and recovery requirements are verified by dedicated policy, composition, and admission tests; this retained corpus establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 maintainability repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 resource type-hint repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The combined issue #1361 execution-policy and hatchling update preserves retained outcomes and bounded claims; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1418 runtime-fact export manifest split changes no contract, schema or behavior; this retained matrix makes no new admission or coverage claim.", + "The issue #1423 inject trigger request and occurrence contracts are new draft carriers that no SDL construct, compiler or runtime path reads; this retained matrix makes no new admission or coverage claim.", + "The issue #1366 inject readback, correlation and backend declaration contracts are new draft carriers; the shared backend allowlist also lets SDL participant behavior specifications cite inject-occurrence-v1 and inject-occurrence-outcome-v1 as evidence_contract_refs, which the compiler copies through uninterpreted, and no runtime path or shipped backend reads or declares them; this retained matrix makes no new admission or coverage claim.", + "This synchronization preserves the original inject and mixed-backend captures, binds their combined source, and adds no runtime or backend-adoption claim.", + "This second synchronization adds behavior-authoring source from issue #297; prior inject and behavior-authoring captures remain preserved. No additional runtime adoption is claimed.", + "Issue #1091 request-boundary admission is verified by its dedicated tests; this retained corpus does not execute the served HTTP adapter or broaden its bounded claims.", + "Issue #1425's updated branch derives reference and libvirt specs from published plan operations. This retained corpus makes no new realization, HTTP relay, or backend-honesty claim.", + "Issue #1462 makes workflow compensation order completed steps by their parsed completion instant, compensating equal instants in reverse history order; this retained corpus makes no new claim." + ], + "load_bearing_results": { + "failed": 0, + "missing": 0, + "passed": 10, + "total": 10 + }, + "plain_language_outcome": "The retained specification matrix reproduces its classifications after issue #1462 began ordering workflow compensation by parsed completion instant instead of timestamp text. Bounded claims and untested concepts are unchanged.", + "protocol_revision": "1.0.0", + "request_results": [ + { + "concept_count": 6, + "failed_stage_count": 0, + "missing_count": 0, + "request_id": "survey-representative-range", + "status": "demonstrated" + }, + { + "concept_count": 5, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "cyborg-participant-evaluation", + "status": "partial" + }, + { + "concept_count": 3, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "vsdl-configurable-infrastructure", + "status": "partial" + }, + { + "concept_count": 2, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "cyber-dem-federation", + "status": "partial" + } + ], + "snapshot_id": "issue-1462-specification-c942f79a9e01", + "snapshot_sha256": "be36ee260cdaea739cf0b7d76e9ce4dbe9d22f002c695d621c27aefe93fdf3d5" +} diff --git a/docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/manifest.json b/docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/manifest.json new file mode 100644 index 000000000..e4e465ba0 --- /dev/null +++ b/docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/manifest.json @@ -0,0 +1,10 @@ +{ + "analysis_path": "docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/analysis.json", + "analysis_sha256": "ae5d340f90f3ff228e61c67339280dae0e676f663bcf84e90abd2d7ed635026f", + "bundle_id": "raes-standardized-specification-coverage", + "protocol_path": "docs/research/specification-coverage/protocol-v1.json", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "revision": "capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae", + "snapshot_path": "docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/snapshot.json", + "snapshot_sha256": "ccd2d834da1222989c5b28a4e6d641de72b0928e5ce6b5d56dba564d38de130a" +} diff --git a/docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/snapshot.json b/docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/snapshot.json new file mode 100644 index 000000000..067c51525 --- /dev/null +++ b/docs/research/specification-coverage/captures/capture-5f61582ecbf7ea0cbc5c378dbefe4e8a90ac287bf891bf44fbefc5ec91d123ae/snapshot.json @@ -0,0 +1,708 @@ +{ + "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-10-13T11:36:35.817106+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": "53443a7c713e5573980e51c86e1b86310c8fc0cab87263f392362f3b5cdf3f12", + "path": "implementations/python/packages/raes_contracts", + "surface_id": "contract-models" + }, + { + "content_sha256": "e947f59695e907f5af899a6bc4bde60e629620aa7c4a69a41e074ba335758c7a", + "path": "implementations/python/packages/raes_processor", + "surface_id": "processor-pipeline" + }, + { + "content_sha256": "fd19fc83b0306d5d0ff4495d97a8cc9f7c9d45300fc640cb0d246e1c6c2cdbe2", + "path": "implementations/python/packages/raes", + "surface_id": "sdl-pipeline" + } + ], + "limitations": [ + "The execution validates the pinned reference implementation and published contracts, not an independent backend.", + "Repository-owned examples are exact execution artifacts but are not themselves the literature-derived request corpus; the protocol's requests and concepts are.", + "No live range, participant, simulator federation, or provider provisioning engine was executed.", + "Missing concepts remain frozen in this snapshot and require separately scoped product work before a later rerun.", + "This capture replays the retained protocol after EXP-732 run, apparatus, measurement-channel, and augmentation-producer provenance validation; it adds no independent backend or universal provenance assurance claim.", + "Materialization attestation is covered by its dedicated regression suite, not a new claim in this preregistered matrix.", + "This capture refreshes the corrected runtime limitations prose for issue #959; the protocol, coverage classifications and implementation source are unchanged.", + "This capture replays open-by-default augmentation scope integrated with the EXP-731 evidence refinements after composition type refinement; it does not evaluate native backend scope enforcement or broaden the preregistered coverage claims.", + "This capture replays the retained protocol after merging ACT-612 participant relationships with open-by-default augmentation scope; it adds no claim of realized participant relationships or native backend scope enforcement.", + "This capture replays issue #1299 partial listener descriptions on the integrated source state; endpoint completeness and backend admission remain outside this protocol's claims.", + "This capture also binds authoring-adapter semantic conformance to the integrated source; adapter transport behavior remains outside this protocol's claims.", + "Reviewed OCI mirror and pre-seed admission is covered by its own regression suites and the development artifact policy gate, not a new claim in this preregistered matrix.", + "This capture binds issue #1297 service-manager identity, native-name, and explicitly selected systemd-state contract changes to the integrated source. It exercises no live service manager and adds no backend-execution claim.", + "This capture replays the retained specification-coverage protocol after API-404 startup reconciliation added an operational recovery-observation contract. It does not evaluate crash recovery, classify provider effects, or broaden EXP-715 experiment-observation claims.", + "This capture binds API-404 single-owner store admission and immutable target/run scope to the integrated source. The retained offline protocol does not exercise process leases, SQLite lifecycle ordering, or crash recovery.", + "This capture binds issue #1015 deterministic mixed and staged trial admission to the integrated source. The retained offline language corpus does not execute mixed runtimes, phase transitions, backend handoff, or scheduler-driven realization.", + "This replay binds issue #1186 offline control-plane maintenance, readiness, and bounded audit code to the integrated source. The retained language corpus does not execute store recovery, HTTP health behavior, or audit redaction.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 control-plane profile declarations are covered by their dedicated runtime suite, not promoted to new claims by the retained language corpus.", + "Issue #1016 mixed-runtime coordination is covered by its dedicated runtime suite. The retained language corpus does not execute mixed providers or establish backend-native realization, multi-controller coordination, IFC, or equivalence.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Issue #1361 execution and recovery requirements are verified by dedicated policy, composition, and admission tests; this retained corpus establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 maintainability repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 resource type-hint repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The combined issue #1361 execution-policy and hatchling update preserves retained outcomes and bounded claims; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "Issue #1091 request-boundary admission is verified by its dedicated tests; this retained corpus does not execute the served HTTP adapter or broaden its bounded claims.", + "This combined-source capture re-executes the named SDL, contract and profile artifacts and their passing typed pointers. The inject placement discriminator repair adds no specification coverage claim; runtime dispatch and live backend effects remain outside this corpus. CI independently verifies replay.", + "Issue #1425's updated branch derives reference and libvirt specs from published plan operations. This retained corpus makes no new realization, HTTP relay, or backend-honesty claim.", + "Issue #1462 makes workflow compensation order completed steps by their parsed completion instant, compensating equal instants in reverse history order; this retained corpus makes no new claim." + ], + "protocol_revision": "1.0.0", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "raes_revision": "105dfbc0d841ef779aa4a32656d5c5c20c2fb9a3", + "snapshot_id": "issue-1462-specification-c942f79a9e01", + "snapshot_revision": "branch-capture", + "source_state": { + "base_revision": "105dfbc0d841ef779aa4a32656d5c5c20c2fb9a3", + "checkout_state": "clean", + "implementation_digest": "c942f79a9e0155607e185ca306a312df57f70cf8be29d183e730882f08080b44", + "profile": "python-reference-source/v2" + } +}