From 44cbc1c7cef6a05f109357befdedc87acb6d9ca8 Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Fri, 25 Sep 2026 17:59:23 +0200 Subject: [PATCH 01/10] fix: admit participant delivery temporal subjects --- docs/public/participant-control.md | 5 +++- .../raes_contracts/contracts/time_model.py | 23 ++++++++++++++++++- ...est_dsl_142_participant_inject_delivery.py | 11 +++++++++ 3 files changed, 37 insertions(+), 2 deletions(-) diff --git a/docs/public/participant-control.md b/docs/public/participant-control.md index d78ccdf0b..bd894b884 100644 --- a/docs/public/participant-control.md +++ b/docs/public/participant-control.md @@ -120,7 +120,10 @@ observation boundary. Reuse the action, control, or inject carrier. - Use `participant_inject_deliveries` when an existing orchestration inject is addressed to a participant. Retain its inject identity. Retain its event/script/story identity. Bind an observation boundary. Name each needed - delivery, order, evidence, or control reference. + delivery, order, evidence, or control reference. A temporal constraint bound + to the delivery compiles to that delivery's `participant.*` address; it + constrains the authored occurrence and does not prove dispatch, delivery, or + observation. - Do not infer a participant addressee from an environment inject. Do not put policy text, hidden answers, credentials, or raw evidence in a participant carrier. diff --git a/implementations/python/packages/raes_contracts/contracts/time_model.py b/implementations/python/packages/raes_contracts/contracts/time_model.py index 5b3fcb19b..32b4054a5 100644 --- a/implementations/python/packages/raes_contracts/contracts/time_model.py +++ b/implementations/python/packages/raes_contracts/contracts/time_model.py @@ -268,7 +268,8 @@ def _validate_constraint_references(self) -> None: if constraint.clock_address not in self.clocks: raise ValueError(f"temporal constraint {constraint.address!r} references an unknown clock") if any( - not subject.startswith("sdl.") and subject not in known_subjects + not _is_declared_resource_subject(subject) + and subject not in known_subjects for subject in constraint.subject_addresses ): raise ValueError(f"temporal constraint {constraint.address!r} references an unknown subject") @@ -278,6 +279,26 @@ def canonical_digest(self) -> str: return "sha256:" + hashlib.sha256(payload).hexdigest() +def _is_declared_resource_subject(address: str) -> bool: + """Admit compiler-owned resource addresses as temporal subjects. + + Most authored resources compile under ``sdl``. Participant-directed inject + deliveries are the one current exception: the participant compiler owns + their canonical address because the delivery is a participant relation to + an orchestration occurrence. Keep that exception exact so an arbitrary + participant address cannot bypass the time-model reference check. + """ + + parts = address.split(".") + return address.startswith("sdl.") or ( + len(parts) == 5 + and all(parts) + and parts[0] == "participant" + and parts[1] == "behavior-specification" + and parts[3] == "inject-delivery" + ) + + class ClockTransitionEventModel(ContractModel): sequence: StrictInt = Field(ge=0) kind: ClockTransitionKind diff --git a/implementations/python/tests/test_dsl_142_participant_inject_delivery.py b/implementations/python/tests/test_dsl_142_participant_inject_delivery.py index db286cb86..a59a66638 100644 --- a/implementations/python/tests/test_dsl_142_participant_inject_delivery.py +++ b/implementations/python/tests/test_dsl_142_participant_inject_delivery.py @@ -13,6 +13,7 @@ from raes.instantiate import instantiate_scenario from raes.parser import parse_sdl, parse_sdl_file from raes_contracts.contracts import schema_bundle +from raes_processor.compiler.time_model import time_model_contract_model from raes_processor.compiler import compile_runtime_model REPO_ROOT = Path(__file__).resolve().parents[3] @@ -165,6 +166,16 @@ def test_participant_inject_delivery_parses_and_compiles_typed_metadata() -> Non assert INJECT_ADDRESS in compiled.refresh_dependencies +def test_participant_inject_delivery_is_a_valid_temporal_subject() -> None: + model = compile_runtime_model(parse_sdl(_scenario_yaml())) + + declaration = time_model_contract_model(model.time_model) + + assert declaration is not None + constraint = declaration.temporal_constraints["time.constraint.briefing-window"] + assert constraint.subject_addresses == [BINDING_ADDRESS] + + def test_compiler_preserves_inject_identity_without_copying_hidden_content() -> None: model = compile_runtime_model(parse_sdl(_scenario_yaml())) compiled = model.participant_inject_deliveries[BINDING_ADDRESS] From a3009f155da0c832a970ae58c52ff2372fabf3bf Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Fri, 25 Sep 2026 18:06:39 +0200 Subject: [PATCH 02/10] fix: keep time subject validation modular --- .../packages/raes_contracts/addressing.py | 14 +++++++++++ .../raes_contracts/contracts/time_model.py | 25 ++----------------- 2 files changed, 16 insertions(+), 23 deletions(-) diff --git a/implementations/python/packages/raes_contracts/addressing.py b/implementations/python/packages/raes_contracts/addressing.py index 7bc8d833b..b56f936c0 100644 --- a/implementations/python/packages/raes_contracts/addressing.py +++ b/implementations/python/packages/raes_contracts/addressing.py @@ -51,10 +51,24 @@ def render_compiled_address(*parts: str) -> str: return require_compiled_address(address) +def is_compiler_owned_temporal_subject_address(address: str) -> bool: + """Return whether a temporal subject is owned by an SDL compiler.""" + + parts = address.split(".") + return address.startswith("sdl.") or ( + len(parts) == 5 + and all(parts) + and parts[0] == "participant" + and parts[1] == "behavior-specification" + and parts[3] == "inject-delivery" + ) + + __all__ = [ "COMPILED_ADDRESS_JSON_SCHEMA", "COMPILED_ADDRESS_MAX_LENGTH", "CompiledAddress", + "is_compiler_owned_temporal_subject_address", "render_compiled_address", "require_compiled_address", ] diff --git a/implementations/python/packages/raes_contracts/contracts/time_model.py b/implementations/python/packages/raes_contracts/contracts/time_model.py index 32b4054a5..122a6f789 100644 --- a/implementations/python/packages/raes_contracts/contracts/time_model.py +++ b/implementations/python/packages/raes_contracts/contracts/time_model.py @@ -8,7 +8,7 @@ from pydantic import Field, StrictInt, model_validator -from ..addressing import CompiledAddress +from ..addressing import CompiledAddress, is_compiler_owned_temporal_subject_address from ..versions import ( REALIZED_TIME_MODEL_SCHEMA_VERSION, TIME_MODEL_SCHEMA_VERSION, @@ -268,8 +268,7 @@ def _validate_constraint_references(self) -> None: if constraint.clock_address not in self.clocks: raise ValueError(f"temporal constraint {constraint.address!r} references an unknown clock") if any( - not _is_declared_resource_subject(subject) - and subject not in known_subjects + not is_compiler_owned_temporal_subject_address(subject) and subject not in known_subjects for subject in constraint.subject_addresses ): raise ValueError(f"temporal constraint {constraint.address!r} references an unknown subject") @@ -279,26 +278,6 @@ def canonical_digest(self) -> str: return "sha256:" + hashlib.sha256(payload).hexdigest() -def _is_declared_resource_subject(address: str) -> bool: - """Admit compiler-owned resource addresses as temporal subjects. - - Most authored resources compile under ``sdl``. Participant-directed inject - deliveries are the one current exception: the participant compiler owns - their canonical address because the delivery is a participant relation to - an orchestration occurrence. Keep that exception exact so an arbitrary - participant address cannot bypass the time-model reference check. - """ - - parts = address.split(".") - return address.startswith("sdl.") or ( - len(parts) == 5 - and all(parts) - and parts[0] == "participant" - and parts[1] == "behavior-specification" - and parts[3] == "inject-delivery" - ) - - class ClockTransitionEventModel(ContractModel): sequence: StrictInt = Field(ge=0) kind: ClockTransitionKind From f1e08c48ed298456969bed1ce9a22bd992192ebb Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Fri, 25 Sep 2026 18:11:09 +0200 Subject: [PATCH 03/10] fix: normalize participant delivery test imports --- .../python/tests/test_dsl_142_participant_inject_delivery.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/implementations/python/tests/test_dsl_142_participant_inject_delivery.py b/implementations/python/tests/test_dsl_142_participant_inject_delivery.py index a59a66638..9f5920c87 100644 --- a/implementations/python/tests/test_dsl_142_participant_inject_delivery.py +++ b/implementations/python/tests/test_dsl_142_participant_inject_delivery.py @@ -13,8 +13,8 @@ from raes.instantiate import instantiate_scenario from raes.parser import parse_sdl, parse_sdl_file from raes_contracts.contracts import schema_bundle -from raes_processor.compiler.time_model import time_model_contract_model from raes_processor.compiler import compile_runtime_model +from raes_processor.compiler.time_model import time_model_contract_model REPO_ROOT = Path(__file__).resolve().parents[3] BINDING_REF = "behavior_specifications.red-briefing.participant_inject_deliveries.briefing" From 2824074e386f6acf13b35e8c1472b05367bb7453 Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Fri, 25 Sep 2026 18:26:04 +0200 Subject: [PATCH 04/10] test: refresh source-bound participant evidence --- docs/requirements/ASR-530/requirement.md | 2 + .../analysis-v48.json | 157 ++++ .../bundles/retest-v48.json | 122 +++ .../execution-snapshot-v48.json | 652 ++++++++++++++++ .../formal-semantic-validation/index.md | 6 + .../specification-coverage/analysis-v48.json | 103 +++ ...specification-coverage-issue-1389-v48.json | 10 + .../execution-snapshot-v48.json | 701 ++++++++++++++++++ docs/research/specification-coverage/index.md | 7 +- .../tests/test_formal_semantic_validation.py | 3 +- .../test_issue_989_versioned_evidence.py | 6 +- .../tests/test_specification_coverage.py | 2 +- tools/check_specification_coverage.py | 5 +- tools/formal_semantic_validation/_loading.py | 3 +- .../_release_revisions.py | 3 +- tools/formal_semantic_validation/_releases.py | 7 +- tools/formal_semantic_validation/_retest.py | 2 +- 17 files changed, 1778 insertions(+), 13 deletions(-) create mode 100644 docs/research/formal-semantic-validation/analysis-v48.json create mode 100644 docs/research/formal-semantic-validation/bundles/retest-v48.json create mode 100644 docs/research/formal-semantic-validation/execution-snapshot-v48.json create mode 100644 docs/research/specification-coverage/analysis-v48.json create mode 100644 docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1389-v48.json create mode 100644 docs/research/specification-coverage/execution-snapshot-v48.json diff --git a/docs/requirements/ASR-530/requirement.md b/docs/requirements/ASR-530/requirement.md index 1e8678869..f6497912b 100644 --- a/docs/requirements/ASR-530/requirement.md +++ b/docs/requirements/ASR-530/requirement.md @@ -21,6 +21,8 @@ Agent-assisted development can produce internally coherent code and documentatio ## Traceability +- IMPLEMENTS → PROOF `docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1389-v48.json` (Current source-bound coverage replay after participant inject temporal-subject admission) +- IMPLEMENTS → PROOF `docs/research/formal-semantic-validation/bundles/retest-v48.json` (Current source-bound formal replay after participant inject temporal-subject admission) - IMPLEMENTS → PROOF `docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1358-v45.json` (Prior source-bound coverage replay with retained classifications) - IMPLEMENTS → PROOF `docs/research/formal-semantic-validation/bundles/retest-v45.json` (Prior source-bound formal replay with retained bounded claims) - IMPLEMENTS → PROOF `docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1358-v46.json` (Current source-bound coverage replay with retained classifications) diff --git a/docs/research/formal-semantic-validation/analysis-v48.json b/docs/research/formal-semantic-validation/analysis-v48.json new file mode 100644 index 000000000..c53786e3a --- /dev/null +++ b/docs/research/formal-semantic-validation/analysis-v48.json @@ -0,0 +1,157 @@ +{ + "analysis_id": "issue-1389-analysis-v48", + "claim": { + "allowed_evidence": [ + "production parser and semantic-validator results", + "canonical compiled digests", + "participant contract regression tests", + "pinned protocol, corpus, and execution snapshot" + ], + "claim_id": "asr-530-formal-semantic-validation-retest", + "disallowed_evidence": [ + "schema success as semantic proof", + "workflow reachability as network or exploit reachability", + "FM labels as gate outcomes", + "attribution as counterfactual proof", + "formal prose or maintainer confidence alone" + ], + "evidence_artifacts": [ + "docs/research/formal-semantic-validation/protocol-v2.json", + "docs/research/formal-semantic-validation/corpus/manifest-v4.json", + "docs/research/formal-semantic-validation/execution-snapshot-v48.json", + "docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json", + "docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json", + "docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json", + "docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json" + ], + "falsification_protocol": "Replay every retained and new case through its production entrypoint, require complete digest and evidence joins, execute participant fixtures, and derive status from the recorded outcomes.", + "objective_fail_criteria": "A supported negative passes, a positive fails, an observation drifts, a required participant case is missing, or weaker evidence is promoted to solver, exploit-path, runtime-stability, or counterfactual assurance.", + "objective_pass_criteria": "Every claim class has positive and negative cases, all supported cases reproduce the frozen outcome, every participant obligation has passing positive and negative fixtures, and unsupported classes remain untested.", + "statement": "At the recorded source-state digest, the retained RAES controls have the bounded statuses recorded here; historical releases are integrity evidence, not current replay evidence.", + "threats_to_validity": [ + "The issue-specific corpus is intentionally small and does not enumerate every validator invariant.", + "The participant fixtures exercise reference production contracts and tests, not every independent backend realization.", + "The replay gate runs on one Python reference configuration and one pinned RAES revision.", + "Unsupported solver-level classes have protocol cases but no executable observations." + ] + }, + "claim_results": [ + { + "case_count": 2, + "claim_class_id": "schema-validity", + "evidence_status": "demonstrated", + "limitations": [ + "Bounded to the named source/model structural controls." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 0 + }, + { + "case_count": 4, + "claim_class_id": "semantic-consistency", + "evidence_status": "partial", + "limitations": [ + "Partial coverage of named static semantics and participant obligations, not universal consistency." + ], + "matching_case_count": 4, + "participant_obligation_count": 7, + "replayable_case_count": 4, + "unsupported_case_count": 0 + }, + { + "case_count": 2, + "claim_class_id": "graph-reachability", + "evidence_status": "partial", + "limitations": [ + "Partial workflow control-flow reachability only; not network, service, or exploit reachability." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 0 + }, + { + "case_count": 4, + "claim_class_id": "constraint-satisfiability", + "evidence_status": "demonstrated", + "limitations": [ + "Demonstrated only for raes-finite-domain-satisfiability-v1 and its pinned solver configuration." + ], + "matching_case_count": 4, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 2 + }, + { + "case_count": 4, + "claim_class_id": "exploit-path-validity", + "evidence_status": "demonstrated", + "limitations": [ + "Demonstrated only for the admitted snapshot, typed graph, query, semantics, and bounded search profile." + ], + "matching_case_count": 4, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 2 + }, + { + "case_count": 2, + "claim_class_id": "determinism-stability", + "evidence_status": "partial", + "limitations": [ + "Partial parse-to-compile repeatability only; runtime and backend determinism are untested." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 0 + }, + { + "case_count": 2, + "claim_class_id": "counterfactual-necessity", + "evidence_status": "untested", + "limitations": [ + "Untested because no governed intervention or ablation entrypoint ran." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 0, + "unsupported_case_count": 2 + } + ], + "corpus_revision": "4.0.0", + "evidence_status": "partial", + "execution_id": "issue-1389-execution-v48", + "generated_at": "2026-09-25", + "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 #1358 final-egress denial is covered by runtime tests; this formal semantic corpus makes no new egress claim.", + "Merged governed v2 decision admission is covered by dedicated runtime tests; this retained formal corpus makes no additional crossing-authority claim.", + "Issue #1389 temporal-subject admission is verified by dedicated compiler tests and adds no new formal-semantic claim to this retained corpus." + ], + "plain_language_outcome": "The retained formal cases reproduce their prior outcomes against source that admits exact participant inject delivery temporal subjects. The bounded claims and unsupported classes are unchanged.", + "protocol_revision": "2.0.0" +} diff --git a/docs/research/formal-semantic-validation/bundles/retest-v48.json b/docs/research/formal-semantic-validation/bundles/retest-v48.json new file mode 100644 index 000000000..0ec0427fc --- /dev/null +++ b/docs/research/formal-semantic-validation/bundles/retest-v48.json @@ -0,0 +1,122 @@ +{ + "analysis_path": "docs/research/formal-semantic-validation/analysis-v48.json", + "analysis_sha256": "f83b60db82d9a0cc0ee53ef0aa8734ff888bac8960f3260eabe2f559d6eb1bc4", + "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": "49.0.0", + "snapshot_path": "docs/research/formal-semantic-validation/execution-snapshot-v48.json", + "snapshot_sha256": "c3d80699936be2f14920f9ad9d525075d75a847a76ee590a1647157f2a9f2e15" +} diff --git a/docs/research/formal-semantic-validation/execution-snapshot-v48.json b/docs/research/formal-semantic-validation/execution-snapshot-v48.json new file mode 100644 index 000000000..8ca4196e1 --- /dev/null +++ b/docs/research/formal-semantic-validation/execution-snapshot-v48.json @@ -0,0 +1,652 @@ +{ + "baseline": { + "execution_id": "issue-1338-execution-v41", + "release_path": "docs/research/formal-semantic-validation/bundles/retest-v41.json", + "release_revision": "42.0.0", + "release_sha256": "7a0b838003e4006df8196e26b6cbde304a1a21cd212cc3d28b1da8f17e00d3a2" + }, + "captured_at": "2026-09-25T16:20:39.809061+00:00", + "commands": [ + { + "argv": [ + "implementations/python/.venv/bin/python", + "tools/check_formal_semantic_validation.py" + ], + "command_id": "bundle-replay", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/pytest", + "-q", + "implementations/python/tests/test_sem_208_participant_behavior.py::test_hidden_truth_disclosure_is_separate_from_observable_projection", + "implementations/python/tests/test_sem_208_participant_behavior.py::test_hidden_truth_cannot_be_observed_without_explicit_disclosure_rule", + "implementations/python/tests/test_sem_211_participant_action_semantics.py::test_action_contract_declares_sem_211_classes_and_compiles_them", + "implementations/python/tests/test_sem_211_participant_action_semantics.py::test_action_result_rejects_success_when_preconditions_are_unresolved", + "implementations/python/tests/test_run_308_concurrent_participant_execution.py::test_runtime_snapshot_publishes_joint_action_and_time_context_records", + "implementations/python/tests/test_run_308_concurrent_participant_execution.py::test_joint_action_record_contract_rejects_unordered_conflicting_writes", + "implementations/python/tests/test_participant_runtime_invariants.py::test_order_discipline_accepts_supported_order_claim_strengths", + "implementations/python/tests/test_participant_runtime_invariants.py::test_order_discipline_rejects_wall_clock_causality", + "implementations/python/tests/test_sem_212_participant_attribution_semantics.py::test_attribution_edge_round_trips_on_terminal_observation", + "implementations/python/tests/test_sem_212_participant_attribution_semantics.py::test_timestamp_adjacency_cannot_be_reported_as_strong_causality", + "implementations/python/tests/test_sem_215_participant_outcome_interpretation.py::test_outcome_interpretation_rule_parses_and_compiles_explicit_layers", + "implementations/python/tests/test_sem_215_participant_outcome_interpretation.py::test_local_action_success_does_not_imply_objective_success_without_rule_record", + "implementations/python/tests/test_realization_honesty_conformance.py::test_constructive_envelope_runs_positive_and_negative_honesty_probes", + "implementations/python/tests/test_realization_honesty_conformance.py::test_only_native_live_can_support_native_conformance" + ], + "command_id": "participant-fixtures", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/raes", + "processor", + "satisfiability", + "docs/research/formal-semantic-validation/corpus/satisfiable-control.sdl.yaml", + "--profile", + "raes-finite-domain-satisfiability-v1" + ], + "command_id": "finite-domain-satisfiable-v2", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/raes", + "processor", + "satisfiability", + "docs/research/formal-semantic-validation/corpus/unsatisfiable-control.sdl.yaml", + "--profile", + "raes-finite-domain-satisfiability-v1" + ], + "command_id": "finite-domain-unsatisfiable-v2", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/raes", + "processor", + "exploit-path", + "docs/research/formal-semantic-validation/corpus/exploit-path-valid-v3.json", + "--profile", + "raes-exploit-path-analysis-v1" + ], + "command_id": "typed-exploit-path-valid-v2", + "network": "disabled" + }, + { + "argv": [ + "implementations/python/.venv/bin/raes", + "processor", + "exploit-path", + "docs/research/formal-semantic-validation/corpus/exploit-path-invalid-v3.json", + "--profile", + "raes-exploit-path-analysis-v1" + ], + "command_id": "typed-exploit-path-invalid-v2", + "network": "disabled" + } + ], + "configuration_id": "raes-python-reference-offline-v41", + "corpus_revision": "4.0.0", + "deviations": [], + "execution_id": "issue-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "limitations": [ + "The witness ends at compiled output." + ], + "replayable": true, + "result_digest": "11264a648a949917c0e84a2a1e5d116139a35e6cb941844735a422df95141d6c", + "source_digest": null + }, + { + "actual_outcome": "distinguishable", + "analysis_profile": null, + "case_id": "compile-non-vacuity-control", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/determinism-a.sdl.yaml", + "docs/research/formal-semantic-validation/corpus/determinism-b.sdl.yaml" + ], + "execution_id": "issue-1389-execution-v48", + "limitations": [ + "Distinct digests are a non-vacuity control, not semantic non-equivalence proof." + ], + "replayable": true, + "result_digest": "72c1ee8c7bbc1f970216fa232b3d4ae917bcb003bd823439bbac8a5db94214e2", + "source_digest": null + }, + { + "actual_outcome": "unsupported", + "analysis_profile": null, + "case_id": "necessity-witness-request", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/decisions/issue-168-formal-semantic-validation-reachability-preflight.md" + ], + "execution_id": "issue-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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-1389-execution-v48", + "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": "5a9d74bab4531060adf5fc9fd4585310f176e381", + "source_state": { + "base_revision": "5a9d74bab4531060adf5fc9fd4585310f176e381", + "checkout_state": "modified", + "implementation_digest": "adadb0f9e7bd2d9983b0c0e6903b637778227b77f45e9bdf1d230a748f702d26", + "profile": "python-reference-source/v2" + }, + "versions": { + "python": "3.14.4", + "raes": "5.0.0", + "z3_engine": "4.16.0", + "z3_solver": "4.16.0.0" + } +} diff --git a/docs/research/formal-semantic-validation/index.md b/docs/research/formal-semantic-validation/index.md index d0b39cfbd..3e79ac037 100644 --- a/docs/research/formal-semantic-validation/index.md +++ b/docs/research/formal-semantic-validation/index.md @@ -466,3 +466,9 @@ in [`execution-snapshot-v47.json`](execution-snapshot-v47.json) and [`analysis-v47.json`](analysis-v47.json). It retains the issue #1338 baseline, bounded claims, and unsupported classes. Final egress denial and governed admission are verified by dedicated runtime regressions. + +Release 49.0.0 is recorded in +[`execution-snapshot-v48.json`](execution-snapshot-v48.json) and +[`analysis-v48.json`](analysis-v48.json). It replays the retained formal cases +after issue #1389 admitted the exact participant inject delivery address as a +temporal subject. Outcomes and bounded claim limits remain unchanged. diff --git a/docs/research/specification-coverage/analysis-v48.json b/docs/research/specification-coverage/analysis-v48.json new file mode 100644 index 000000000..2043430c8 --- /dev/null +++ b/docs/research/specification-coverage/analysis-v48.json @@ -0,0 +1,103 @@ +{ + "analysis_id": "raes-standardized-specification-coverage-issue-1389-v48", + "backend_leakage": [], + "claim": { + "allowed_evidence": [ + "pinned source metadata and bounded paraphrases", + "production parser, semantic, instantiation, admission, compiler, contract, and profile results", + "exact artifact digests and typed pointers", + "documented missing-concept and backend-specific dispositions" + ], + "claim_id": "raes-standardized-configurable-specification-coverage", + "disallowed_evidence": [ + "field-count or schema breadth alone", + "the existing scenario stress corpus as the representative request corpus", + "free-form metadata as typed coverage", + "backend-private interpretation", + "post-hoc removal or repair of falsifying concepts" + ], + "evidence_artifacts": [ + "docs/research/specification-coverage/protocol-v1.json", + "docs/research/specification-coverage/execution-snapshot-v48.json", + "docs/research/specification-coverage/analysis-v48.json" + ], + "falsification_protocol": "docs/research/specification-coverage/protocol-v1.json", + "objective_fail_criteria": "A load-bearing concept is missing or lossy, an applicable stage fails, or backend vocabulary is required in core SDL while the result claims success.", + "objective_pass_criteria": "Every load-bearing concept passes at every owning stage, backend-specific mechanics stay outside core SDL, and no requested concept is silently lost.", + "statement": "RAES provides a standardized configurable portable specification surface for the preregistered representative cyber-agent evaluation environment requirements without backend vocabulary in core SDL.", + "threats_to_validity": [ + "The representative corpus contains four source strata and sixteen atomic concepts rather than every cyber-range requirement.", + "The reference processor and repository fixtures are not independent backend implementations.", + "No live range, simulator federation, or participant execution was part of this offline specification-coverage test." + ] + }, + "classification_counts": { + "deliberately-backend-specific": 1, + "directly-expressible": 10, + "missing": 3, + "profile-or-manifest-constraint": 2 + }, + "evidence_status": "partial", + "execution_status": "complete", + "generated_at": "2026-09-25", + "limitations": [ + "This result demonstrates bounded specification coverage, not universal cyber-range coverage, usability, adoption, backend substitution, or behavioral equivalence.", + "The three missing concepts are evidence, not implementation tasks within this snapshot.", + "The retained protocol does not test recursive realization or plan-level profile semantics; this release only re-establishes its original bounded coverage result against the current implementation.", + "The retained protocol does not test evidence-requirement refinement lineage; the dedicated EXP-731 regression suite covers that production boundary.", + "Authoring-adapter transport behavior is outside this retained protocol.", + "Reviewed OCI mirror and pre-seed admission is covered by its own regression suites and the development artifact policy gate, not a new claim in this preregistered matrix.", + "Operational recovery observation and startup reconciliation are covered by their API-404 regression suite, not a new claim in this preregistered matrix.", + "Store ownership, immutable runtime scope, and provider shutdown ordering are covered by the API-404 CP-5 regression suite, not by this retained specification-coverage protocol.", + "Mixed/staged trial compilation and admission are covered by issue #1015 regression tests, not by this retained specification-coverage corpus; no live mixed-runtime result is claimed.", + "Issue #1186 control-plane recovery operations are covered by their runtime regression suite, not by this retained specification-coverage corpus.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 control-plane profile declarations are covered by their dedicated runtime suite, not promoted to new claims by the retained language corpus.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Participant-local outcome state is verified by the ACT-618 tests; this retained corpus makes no additional outcome-state claim.", + "Issue #1358 final-egress denial remains covered by dedicated runtime tests, not by this retained SDL matrix.", + "The merged issue #1357 governed admission change is covered by dedicated v2 decision-surface tests; this retained SDL matrix makes no additional crossing-authority 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." + ], + "load_bearing_results": { + "failed": 0, + "missing": 0, + "passed": 10, + "total": 10 + }, + "plain_language_outcome": "The retained specification matrix replays unchanged classifications and claim limits against source that admits exact participant inject delivery temporal subjects. Dedicated compiler tests, rather than this corpus, verify that delivery-timing behavior.", + "protocol_revision": "1.0.0", + "request_results": [ + { + "concept_count": 6, + "failed_stage_count": 0, + "missing_count": 0, + "request_id": "survey-representative-range", + "status": "demonstrated" + }, + { + "concept_count": 5, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "cyborg-participant-evaluation", + "status": "partial" + }, + { + "concept_count": 3, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "vsdl-configurable-infrastructure", + "status": "partial" + }, + { + "concept_count": 2, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "cyber-dem-federation", + "status": "partial" + } + ], + "snapshot_id": "raes-standardized-specification-coverage-issue-1389-v48", + "snapshot_sha256": "1d9651ebaa7176137e6daa8731e21250045e6f95a797c3dd1162c4bd307a7340" +} diff --git a/docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1389-v48.json b/docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1389-v48.json new file mode 100644 index 000000000..77304fe31 --- /dev/null +++ b/docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1389-v48.json @@ -0,0 +1,10 @@ +{ + "analysis_path": "docs/research/specification-coverage/analysis-v48.json", + "analysis_sha256": "ea26c6a55df971e13c73c7f3a7b5f44215d8dda33927a06fe4d4ccf0e84809db", + "bundle_id": "raes-standardized-specification-coverage", + "protocol_path": "docs/research/specification-coverage/protocol-v1.json", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "revision": "48.0.0", + "snapshot_path": "docs/research/specification-coverage/execution-snapshot-v48.json", + "snapshot_sha256": "1c434602c115ff1c9bcb47ac84aab04e7b2ff69dceeaffc9ee194f5c8fcd58f2" +} diff --git a/docs/research/specification-coverage/execution-snapshot-v48.json b/docs/research/specification-coverage/execution-snapshot-v48.json new file mode 100644 index 000000000..e33ecc3c5 --- /dev/null +++ b/docs/research/specification-coverage/execution-snapshot-v48.json @@ -0,0 +1,701 @@ +{ + "artifacts": [ + { + "artifact_id": "enterprise-participant-sdl", + "kind": "sdl", + "path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "sha256": "f7a8897beec243e188ee081975006fad32725f469f267db6e75a1e1cf5727032", + "validator": "raes parse, semantic, instantiation/admission, and compiler pipeline" + }, + { + "artifact_id": "port-range-sdl", + "kind": "sdl", + "path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "sha256": "0d5497ec946b863e6985284ec487dde7d7f6bf710a985be51401ac0e5e79dc4f", + "validator": "raes parse, semantic, instantiation/admission, and compiler pipeline" + }, + { + "artifact_id": "experiment-task-contract", + "kind": "experiment-task", + "path": "contracts/fixtures/experiment-core/experiment-task-v1/valid/reference.json", + "sha256": "f3edf713ac6af26bad609136851c6dd434bfb87ce919a2d8c4414c1035deeafc", + "validator": "raes_contracts.contracts.ExperimentTaskModel" + }, + { + "artifact_id": "apparatus-context-contract", + "kind": "experiment-apparatus-context", + "path": "contracts/fixtures/experiment-core/experiment-apparatus-context-v1/valid/reference.json", + "sha256": "e6fa559c5e961f0aab448d0f70dead24aa74fa8ba5f20e1b72f88e11473c9299", + "validator": "raes_contracts.contracts.ExperimentApparatusContextModel" + }, + { + "artifact_id": "backend-profile", + "kind": "backend-profile", + "path": "contracts/profiles/backend/orchestration-capable.json", + "sha256": "f70b8505a5c0055416db86c533e2e5bf08b11e5a514f076223b6d6c36215a092", + "validator": "raes_contracts.backend_profiles.BackendProfileModel" + }, + { + "artifact_id": "known-limitations", + "kind": "documentation", + "path": "docs/explain/sdl/limitations.md", + "sha256": "489eeab3ce682627682311581eb98af9abb9ff42a437145af266eefb71dc7fc4", + "validator": "documentation evidence only" + } + ], + "baseline": { + "release_revision": "1.1.0", + "release_sha256": "4020a1d56c7fe2831cec59ea64a12bbda9d38ccd94f93b916dd90f1a28f17fcb" + }, + "captured_at": "2026-09-25T16:20:39.809061+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": "2f905cf6a357d94c45b994c2e93c700c59168b54bff7a8855f322444d9b65794", + "path": "implementations/python/packages/raes_contracts", + "surface_id": "contract-models" + }, + { + "content_sha256": "4999b8adf294f364a758bc9cf78816d5da9eae1c263ae678eabe4d0e2c82dec6", + "path": "implementations/python/packages/raes_processor", + "surface_id": "processor-pipeline" + }, + { + "content_sha256": "9ecd780448b054693503bab246120a1a2bb49a43016d0b9c27c5284ba609833f", + "path": "implementations/python/packages/raes", + "surface_id": "sdl-pipeline" + } + ], + "limitations": [ + "The execution validates the pinned reference implementation and published contracts, not an independent backend.", + "Repository-owned examples are exact execution artifacts but are not themselves the literature-derived request corpus; the protocol's requests and concepts are.", + "No live range, participant, simulator federation, or provider provisioning engine was executed.", + "Missing concepts remain frozen in this snapshot and require separately scoped product work before a later rerun.", + "This capture replays the retained protocol after EXP-732 run, apparatus, measurement-channel, and augmentation-producer provenance validation; it adds no independent backend or universal provenance assurance claim.", + "Materialization attestation is covered by its dedicated regression suite, not a new claim in this preregistered matrix.", + "This capture refreshes the corrected runtime limitations prose for issue #959; the protocol, coverage classifications and implementation source are unchanged.", + "This capture replays open-by-default augmentation scope integrated with the EXP-731 evidence refinements after composition type refinement; it does not evaluate native backend scope enforcement or broaden the preregistered coverage claims.", + "This capture replays the retained protocol after merging ACT-612 participant relationships with open-by-default augmentation scope; it adds no claim of realized participant relationships or native backend scope enforcement.", + "This capture replays issue #1299 partial listener descriptions on the integrated source state; endpoint completeness and backend admission remain outside this protocol's claims.", + "This capture also binds authoring-adapter semantic conformance to the integrated source; adapter transport behavior remains outside this protocol's claims.", + "Reviewed OCI mirror and pre-seed admission is covered by its own regression suites and the development artifact policy gate, not a new claim in this preregistered matrix.", + "This capture binds issue #1297 service-manager identity, native-name, and explicitly selected systemd-state contract changes to the integrated source. It exercises no live service manager and adds no backend-execution claim.", + "This capture replays the retained specification-coverage protocol after API-404 startup reconciliation added an operational recovery-observation contract. It does not evaluate crash recovery, classify provider effects, or broaden EXP-715 experiment-observation claims.", + "This capture binds API-404 single-owner store admission and immutable target/run scope to the integrated source. The retained offline protocol does not exercise process leases, SQLite lifecycle ordering, or crash recovery.", + "This capture binds issue #1015 deterministic mixed and staged trial admission to the integrated source. The retained offline language corpus does not execute mixed runtimes, phase transitions, backend handoff, or scheduler-driven realization.", + "This replay binds issue #1186 offline control-plane maintenance, readiness, and bounded audit code to the integrated source. The retained language corpus does not execute store recovery, HTTP health behavior, or audit redaction.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 control-plane profile declarations are covered by their dedicated runtime suite, not promoted to new claims by the retained language corpus.", + "Issue #1016 mixed-runtime coordination is covered by its dedicated runtime suite. The retained language corpus does not execute mixed providers or establish backend-native realization, multi-controller coordination, IFC, or equivalence.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Issue #1358 final-egress denial is verified by dedicated runtime regressions; this retained SDL corpus adds no egress assurance claim." + ], + "protocol_revision": "1.0.0", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "raes_revision": "5a9d74bab4531060adf5fc9fd4585310f176e381", + "snapshot_id": "raes-standardized-specification-coverage-issue-1389-v48", + "snapshot_revision": "47.0.0", + "source_state": { + "base_revision": "5a9d74bab4531060adf5fc9fd4585310f176e381", + "checkout_state": "modified", + "implementation_digest": "adadb0f9e7bd2d9983b0c0e6903b637778227b77f45e9bdf1d230a748f702d26", + "profile": "python-reference-source/v2" + } +} diff --git a/docs/research/specification-coverage/index.md b/docs/research/specification-coverage/index.md index 9419f36d6..2b41e07ca 100644 --- a/docs/research/specification-coverage/index.md +++ b/docs/research/specification-coverage/index.md @@ -292,7 +292,7 @@ the port scenario. Historical captures and archived example bytes are retained. The matrix classifications and untested concepts are unchanged; no execution authority, successful action, or live backend fidelity is inferred. -Current validation requires release 47.0.0 and rejects duplicate or unsupported +Current validation requires release 48.0.0 and rejects duplicate or unsupported future revisions. It executes current artifacts, requires exact source and package hashes, and checks all passing stage pointers. `source_state` discloses the base Git commit, modified checkout state, and exact implementation digest; @@ -402,3 +402,8 @@ Current release 47.0.0 replays the same controls against the merged source in [`analysis-v47.json`](analysis-v47.json). Classifications and claim limits remain unchanged; egress denial and governed admission are verified by their dedicated runtime tests. + +Current release 48.0.0 replays the retained matrix after issue #1389 admitted +the exact participant inject delivery address as a temporal subject. The +classifications and claim limits remain unchanged; participant delivery timing +is verified by its dedicated compiler tests. diff --git a/implementations/python/tests/test_formal_semantic_validation.py b/implementations/python/tests/test_formal_semantic_validation.py index 3ca9d141b..204560ef3 100644 --- a/implementations/python/tests/test_formal_semantic_validation.py +++ b/implementations/python/tests/test_formal_semantic_validation.py @@ -127,6 +127,7 @@ def test_atomic_release_index_validates_every_historical_bundle() -> None: "46.0.0", "47.0.0", "48.0.0", + "49.0.0", ] assert all(validate_release_bundle(REPO_ROOT, release) == [] for release in releases) @@ -135,7 +136,7 @@ def test_atomic_release_index_validates_every_historical_bundle() -> None: def test_current_retest_bundle_is_coherent_and_clean() -> None: release, protocol, corpus, snapshot, analysis = copy_bundle(load_retest_bundle, REPO_ROOT) - assert release.manifest["revision"] == "48.0.0" + assert release.manifest["revision"] == "49.0.0" assert protocol["revision"] == "2.0.0" assert corpus["revision"] == "4.0.0" assert snapshot["baseline"]["release_revision"] == "42.0.0" diff --git a/implementations/python/tests/test_issue_989_versioned_evidence.py b/implementations/python/tests/test_issue_989_versioned_evidence.py index 0c16c1442..3cedf5ddb 100644 --- a/implementations/python/tests/test_issue_989_versioned_evidence.py +++ b/implementations/python/tests/test_issue_989_versioned_evidence.py @@ -230,7 +230,7 @@ def test_latest_current_release_is_versioned_and_strict(monkeypatch): from tools.formal_semantic_validation._releases import validate_retest_bundle release, protocol, corpus, snapshot, analysis = copy_bundle(load_retest_bundle, ROOT) - assert release.manifest["revision"] == "48.0.0" + assert release.manifest["revision"] == "49.0.0" original = _retest.replay_case def changed_result(root, case): @@ -283,7 +283,7 @@ def test_specification_current_capture_does_not_accept_old_artifact_digest(artif from tools.check_specification_coverage import load_bundle, validate_bundle manifest, protocol, snapshot, analysis = copy_bundle(load_bundle, ROOT) - assert manifest["revision"] == "47.0.0" + assert manifest["revision"] == "48.0.0" snapshot = deepcopy(snapshot) artifact = next(a for a in snapshot["artifacts"] if a["artifact_id"] == artifact_id) artifact["sha256"] = old_digest @@ -500,6 +500,7 @@ def test_no_capture_can_be_silently_dropped(monkeypatch, family, removed): "46.0.0", "47.0.0", "48.0.0", + "49.0.0", ] if family == "formal" else [ @@ -551,6 +552,7 @@ def test_no_capture_can_be_silently_dropped(monkeypatch, family, removed): "45.0.0", "46.0.0", "47.0.0", + "48.0.0", ] ) revisions.pop(-1 if removed == "current" else 0) diff --git a/implementations/python/tests/test_specification_coverage.py b/implementations/python/tests/test_specification_coverage.py index 3c3f3bdf5..284e7baa3 100644 --- a/implementations/python/tests/test_specification_coverage.py +++ b/implementations/python/tests/test_specification_coverage.py @@ -53,7 +53,7 @@ def test_immutable_bundle_index_preserves_concurrent_captures() -> None: bundles = copy_bundle(load_bundles, REPO_ROOT) assert {manifest["revision"] for manifest, *_rest in bundles} >= {"1.0.0", "1.1.0", "19.0.0"} manifest, *_rest = copy_bundle(load_bundle, REPO_ROOT) - assert manifest["revision"] == "47.0.0" + assert manifest["revision"] == "48.0.0" def test_historical_failures_name_the_revision_specific_documents() -> None: diff --git a/tools/check_specification_coverage.py b/tools/check_specification_coverage.py index 1b71a6988..106f64840 100644 --- a/tools/check_specification_coverage.py +++ b/tools/check_specification_coverage.py @@ -102,7 +102,7 @@ def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: max_bytes=_MAX_FILE_BYTES, ) current_path = current_release_path(records) - if dict(records)[current_path].get("revision") != "47.0.0" or {record.get("revision") for _, record in records} != { + if dict(records)[current_path].get("revision") != "48.0.0" or {record.get("revision") for _, record in records} != { "1.0.0", "1.1.0", "2.0.0", @@ -151,8 +151,9 @@ def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: "45.0.0", "46.0.0", "47.0.0", + "48.0.0", }: - raise ValueError("coverage evidence requires the explicit current 47.0.0 release and supported history") + raise ValueError("coverage evidence requires the explicit current 48.0.0 release and supported history") return records diff --git a/tools/formal_semantic_validation/_loading.py b/tools/formal_semantic_validation/_loading.py index 3d0f12001..68f2f4ffa 100644 --- a/tools/formal_semantic_validation/_loading.py +++ b/tools/formal_semantic_validation/_loading.py @@ -78,6 +78,7 @@ def load_release_bundles(repo_root: Path = REPO_ROOT) -> list[EvidenceRelease]: "46.0.0", "47.0.0", "48.0.0", + "49.0.0", }: raise ValueError("formal evidence requires every supported historical and current release") releases: list[EvidenceRelease] = [] @@ -124,6 +125,6 @@ def load_retest_bundle( if not releases: raise ValueError("the formal semantic-validation index selects no v2 retest release") release = max(releases, key=lambda item: revision_key(item.manifest.get("revision"))) - if release.manifest.get("revision") != "48.0.0" or release.protocol.get("revision") != "2.0.0": + if release.manifest.get("revision") != "49.0.0" or release.protocol.get("revision") != "2.0.0": raise ValueError("the current formal evidence release must be the explicit 48.0.0 retest") return release, release.protocol, release.corpus, release.snapshot, release.analysis diff --git a/tools/formal_semantic_validation/_release_revisions.py b/tools/formal_semantic_validation/_release_revisions.py index 819789278..542a48d01 100644 --- a/tools/formal_semantic_validation/_release_revisions.py +++ b/tools/formal_semantic_validation/_release_revisions.py @@ -47,8 +47,9 @@ "45.0.0", "46.0.0", "47.0.0", + "48.0.0", } ) -_SUPPORTED_RETEST_REVISIONS = _HISTORICAL_RETEST_REVISIONS | {"48.0.0"} +_SUPPORTED_RETEST_REVISIONS = _HISTORICAL_RETEST_REVISIONS | {"49.0.0"} _SOURCE_BOUND_RETEST_REVISIONS = _SUPPORTED_RETEST_REVISIONS - {"3.0.0"} diff --git a/tools/formal_semantic_validation/_releases.py b/tools/formal_semantic_validation/_releases.py index 39269ed01..0dcf7ce5b 100644 --- a/tools/formal_semantic_validation/_releases.py +++ b/tools/formal_semantic_validation/_releases.py @@ -159,7 +159,7 @@ def validate_release_bundle(repo_root: Path, release: EvidenceRelease) -> list[P release.corpus, release.snapshot, release.analysis, - replay_current=manifest.get("revision") == "48.0.0", + replay_current=manifest.get("revision") == "49.0.0", ) ) else: @@ -244,7 +244,7 @@ def validate_retest_bundle( return [ _failure( "formal-validation-current-replay-required", - "only releases 3.0.0 through 47.0.0 can use integrated historical validation", + "only releases 3.0.0 through 48.0.0 can use integrated historical validation", snapshot_path, ) ] @@ -292,7 +292,7 @@ def validate_retest_bundle( } else "2.0.0" ) - if release_revision in {"42.0.0", "45.0.0", "46.0.0", "47.0.0", "48.0.0"}: + if release_revision in {"42.0.0", "45.0.0", "46.0.0", "47.0.0", "48.0.0", "49.0.0"}: expected_corpus_revision = "4.0.0" if protocol.get("revision") != "2.0.0" or corpus.get("revision") != expected_corpus_revision: failures.append( @@ -402,6 +402,7 @@ def _current_retest_source_failures( "46.0.0": "45.0.0", "47.0.0": "42.0.0", "48.0.0": "42.0.0", + "49.0.0": "42.0.0", }[release_revision] if not isinstance(baseline, Mapping) or baseline.get("release_revision") != expected_baseline: failures.append( diff --git a/tools/formal_semantic_validation/_retest.py b/tools/formal_semantic_validation/_retest.py index 066df45d3..f55edde99 100644 --- a/tools/formal_semantic_validation/_retest.py +++ b/tools/formal_semantic_validation/_retest.py @@ -37,7 +37,7 @@ ) from tools.policy.common import PolicyFailure -_SOURCE_STATE_REVISIONS = frozenset(f"{revision}.0.0" for revision in range(4, 49)) +_SOURCE_STATE_REVISIONS = frozenset(f"{revision}.0.0" for revision in range(4, 50)) @dataclasses.dataclass(frozen=True) From 9185ce04c55e76569a6152493c53381fdd2a2c9e Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Sun, 27 Sep 2026 02:21:37 +0200 Subject: [PATCH 05/10] style: apply repository tooling format --- tools/check_specification_coverage.py | 41 ++----- tools/formal_semantic_validation/_baseline.py | 104 ++++-------------- tools/formal_semantic_validation/_loading.py | 37 ++----- tools/formal_semantic_validation/_releases.py | 70 +++--------- tools/formal_semantic_validation/_retest.py | 63 +++-------- 5 files changed, 72 insertions(+), 243 deletions(-) diff --git a/tools/check_specification_coverage.py b/tools/check_specification_coverage.py index 653b9d65d..4749299ec 100644 --- a/tools/check_specification_coverage.py +++ b/tools/check_specification_coverage.py @@ -88,14 +88,9 @@ def load_bundle( def load_bundles( repo_root: Path = REPO_ROOT, -) -> list[ - tuple[dict[str, object], dict[str, object], dict[str, object], dict[str, object]] -]: +) -> list[tuple[dict[str, object], dict[str, object], dict[str, object], dict[str, object]]]: records = _load_bundle_index(repo_root) - return [ - _load_bundle_record(repo_root, manifest_path, manifest) - for manifest_path, manifest in records - ] + return [_load_bundle_record(repo_root, manifest_path, manifest) for manifest_path, manifest in records] def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: @@ -107,9 +102,7 @@ def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: max_bytes=_MAX_FILE_BYTES, ) current_path = current_release_path(records) - if dict(records)[current_path].get("revision") != "53.0.0" or { - record.get("revision") for _, record in records - } != { + if dict(records)[current_path].get("revision") != "53.0.0" or {record.get("revision") for _, record in records} != { "1.0.0", "1.1.0", "2.0.0", @@ -165,9 +158,7 @@ def _load_bundle_index(repo_root: Path) -> list[tuple[str, dict[str, object]]]: "52.0.0", "53.0.0", }: - raise ValueError( - "coverage evidence requires the explicit current 53.0.0 release and supported history" - ) + raise ValueError("coverage evidence requires the explicit current 53.0.0 release and supported history") return records @@ -185,22 +176,14 @@ def _load_bundle_record( for label in ("protocol", "snapshot", "analysis"): path_value = manifest[f"{label}_path"] sha_value = manifest[f"{label}_sha256"] - resolved = ( - safe_repo_path(repo_root, path_value) - if isinstance(path_value, str) - else None - ) + resolved = safe_repo_path(repo_root, path_value) if isinstance(path_value, str) else None if resolved is None or not resolved.is_file(): - raise ValueError( - f"{manifest_path!r} contains unsafe or missing {label}_path" - ) + raise ValueError(f"{manifest_path!r} contains unsafe or missing {label}_path") if not isinstance(sha_value, str) or not _SHA256_RE.fullmatch(sha_value): raise ValueError(f"{manifest_path!r} contains invalid {label}_sha256") if _sha256(resolved) != sha_value: raise ValueError(f"{manifest_path!r} contains stale {label}_sha256") - loaded.append( - load_bounded_json_object(repo_root, path_value, max_bytes=_MAX_FILE_BYTES) - ) + loaded.append(load_bounded_json_object(repo_root, path_value, max_bytes=_MAX_FILE_BYTES)) return manifest, loaded[0], loaded[1], loaded[2] @@ -213,16 +196,10 @@ def evaluate(repo_root: Path = REPO_ROOT) -> list[PolicyFailure]: for manifest_path, manifest in records ] except (OSError, ValueError) as exc: - return [ - _failure("specification-coverage-bundle-invalid", str(exc), MANIFEST_PATH) - ] + return [_failure("specification-coverage-bundle-invalid", str(exc), MANIFEST_PATH)] failures: list[PolicyFailure] = [] for manifest_path, (manifest, protocol, snapshot, analysis) in bundles: - validator = ( - validate_bundle - if manifest_path == current_path - else validate_historical_bundle - ) + validator = validate_bundle if manifest_path == current_path else validate_historical_bundle failures.extend(validator(repo_root, manifest, protocol, snapshot, analysis)) return failures diff --git a/tools/formal_semantic_validation/_baseline.py b/tools/formal_semantic_validation/_baseline.py index 76a87f355..6ea0a16dc 100644 --- a/tools/formal_semantic_validation/_baseline.py +++ b/tools/formal_semantic_validation/_baseline.py @@ -24,18 +24,10 @@ ) from tools.policy.common import PolicyFailure, load_bounded_json_object, safe_repo_path -_ARCHIVE_PINS_PATH = ( - "docs/research/formal-semantic-validation/historical-artifacts/pins-v1.json" -) -_ARCHIVE_PINS_SHA256 = ( - "bcb61fa1f0bce5411eb4d3f9583b51df47798ac955d85b6dd3eadf50c14599f2" -) -_ADDITIONAL_ARCHIVE_PINS_PATH = ( - "docs/research/formal-semantic-validation/historical-artifacts/pins-v2.json" -) -_ADDITIONAL_ARCHIVE_PINS_SHA256 = ( - "04b4a1cdfa8c76ccbc536e87365e9343bec4fb8dcde712c15a6535c6e927352a" -) +_ARCHIVE_PINS_PATH = "docs/research/formal-semantic-validation/historical-artifacts/pins-v1.json" +_ARCHIVE_PINS_SHA256 = "bcb61fa1f0bce5411eb4d3f9583b51df47798ac955d85b6dd3eadf50c14599f2" +_ADDITIONAL_ARCHIVE_PINS_PATH = "docs/research/formal-semantic-validation/historical-artifacts/pins-v2.json" +_ADDITIONAL_ARCHIVE_PINS_SHA256 = "04b4a1cdfa8c76ccbc536e87365e9343bec4fb8dcde712c15a6535c6e927352a" _DRIFT_COMPARISON_KEYS = ("actual_outcome", "diagnostic_kind", "result_digest") _V2_REVISIONS = frozenset( @@ -127,16 +119,9 @@ ) -def _pinned_document( - repo_root: Path, relative: str, digest: str -) -> Mapping[str, object] | None: +def _pinned_document(repo_root: Path, relative: str, digest: str) -> Mapping[str, object] | None: path = safe_repo_path(repo_root, relative) - if ( - path is None - or not path.is_file() - or path.stat().st_size > _MAX_FILE_BYTES - or _sha256_file(path) != digest - ): + if path is None or not path.is_file() or path.stat().st_size > _MAX_FILE_BYTES or _sha256_file(path) != digest: return None try: return load_bounded_json_object(repo_root, relative, max_bytes=_MAX_FILE_BYTES) @@ -159,9 +144,7 @@ def _archive_allowed(repo_root: Path, relative: str, digest: str) -> bool: return False -def _baseline_document( - repo_root: Path, path_value: object, digest: object -) -> Mapping[str, object] | None: +def _baseline_document(repo_root: Path, path_value: object, digest: object) -> Mapping[str, object] | None: """Read the exact captured bytes, including a preserved historical copy.""" if ( not isinstance(path_value, str) @@ -172,9 +155,7 @@ def _baseline_document( return None candidates = [path_value] if _archive_allowed(repo_root, path_value, digest): - candidates.append( - f"docs/research/formal-semantic-validation/historical-artifacts/{digest}.json" - ) + candidates.append(f"docs/research/formal-semantic-validation/historical-artifacts/{digest}.json") document = None for candidate in candidates: document = _pinned_document(repo_root, candidate, digest) @@ -243,9 +224,7 @@ def _selected_baseline_manifest( ) return None indexed = indexed_records.get(baseline_path) - baseline_manifest = _baseline_document( - repo_root, baseline_path, baseline.get("release_sha256") - ) + baseline_manifest = _baseline_document(repo_root, baseline_path, baseline.get("release_sha256")) baseline_revision = baseline.get("release_revision") expected_protocol_path = ( "docs/research/formal-semantic-validation/protocol-v2.json" @@ -264,21 +243,13 @@ def _selected_baseline_manifest( "52.0.0", "53.0.0", }: - expected_corpus_path = ( - "docs/research/formal-semantic-validation/corpus/manifest-v4.json" - ) + expected_corpus_path = "docs/research/formal-semantic-validation/corpus/manifest-v4.json" elif baseline_revision in _V3_CORPUS_REVISIONS: - expected_corpus_path = ( - "docs/research/formal-semantic-validation/corpus/manifest-v3.json" - ) + expected_corpus_path = "docs/research/formal-semantic-validation/corpus/manifest-v3.json" elif baseline_revision in _V2_REVISIONS: - expected_corpus_path = ( - "docs/research/formal-semantic-validation/corpus/manifest-v2.json" - ) + expected_corpus_path = "docs/research/formal-semantic-validation/corpus/manifest-v2.json" else: - expected_corpus_path = ( - "docs/research/formal-semantic-validation/corpus/manifest-v1.json" - ) + expected_corpus_path = "docs/research/formal-semantic-validation/corpus/manifest-v1.json" if ( not isinstance(baseline_manifest, Mapping) or not isinstance(indexed, Mapping) @@ -311,9 +282,7 @@ def _loaded_baseline_snapshot( ) -> Mapping[str, object] | None: baseline_snapshot_path = baseline_manifest.get("snapshot_path") baseline_snapshot_digest = baseline_manifest.get("snapshot_sha256") - baseline_snapshot = _baseline_document( - repo_root, baseline_snapshot_path, baseline_snapshot_digest - ) + baseline_snapshot = _baseline_document(repo_root, baseline_snapshot_path, baseline_snapshot_digest) if baseline_snapshot is None: failures.append( _failure( @@ -341,11 +310,7 @@ def _resolved_baseline_snapshot( path: str, ) -> Mapping[str, object] | None: baseline = _validated_baseline_pin(snapshot, failures, path) - manifest = ( - _selected_baseline_manifest(repo_root, baseline, failures, path) - if baseline is not None - else None - ) + manifest = _selected_baseline_manifest(repo_root, baseline, failures, path) if baseline is not None else None if manifest is None: return None return _loaded_baseline_snapshot(repo_root, manifest, baseline, failures, path) @@ -357,10 +322,7 @@ def _drift_join( historical_cases: Mapping[object, Mapping[str, object]], failures: list[PolicyFailure], path: str, -) -> ( - tuple[dict[str, Mapping[str, object]], dict[str, Mapping[str, object]], set[str]] - | None -): +) -> tuple[dict[str, Mapping[str, object]], dict[str, Mapping[str, object]], set[str]] | None: baseline_observations = baseline_snapshot.get("observations") retest_observations = snapshot.get("observations") baseline_ids, baseline_unique = _stable_ids(baseline_observations, "case_id") @@ -382,16 +344,8 @@ def _drift_join( ) ) return None - baseline_by_id = { - str(item.get("case_id")): item - for item in baseline_observations - if isinstance(item, Mapping) - } - retest_by_id = { - str(item.get("case_id")): item - for item in retest_observations - if isinstance(item, Mapping) - } + baseline_by_id = {str(item.get("case_id")): item for item in baseline_observations if isinstance(item, Mapping)} + retest_by_id = {str(item.get("case_id")): item for item in retest_observations if isinstance(item, Mapping)} return baseline_by_id, retest_by_id, retained_ids @@ -406,9 +360,7 @@ def _deviation_entry_failures( """Check one retained case's drift disposition; return whether it changed.""" changed_fields = [ - key - for key in _DRIFT_COMPARISON_KEYS - if baseline_observation.get(key) != retest_observation.get(key) + key for key in _DRIFT_COMPARISON_KEYS if baseline_observation.get(key) != retest_observation.get(key) ] if not changed_fields: return False @@ -422,12 +374,8 @@ def _deviation_entry_failures( path=path, ): return True - expected_baseline = { - key: baseline_observation.get(key) for key in _DRIFT_COMPARISON_KEYS - } - expected_retest = { - key: retest_observation.get(key) for key in _DRIFT_COMPARISON_KEYS - } + expected_baseline = {key: baseline_observation.get(key) for key in _DRIFT_COMPARISON_KEYS} + expected_retest = {key: retest_observation.get(key) for key in _DRIFT_COMPARISON_KEYS} if ( deviation.get("changed_fields") != changed_fields or deviation.get("baseline") != expected_baseline @@ -465,11 +413,7 @@ def _deviation_failures( ) ) deviations = [] - deviations_by_id = { - str(item.get("case_id")): item - for item in deviations - if isinstance(item, Mapping) - } + deviations_by_id = {str(item.get("case_id")): item for item in deviations if isinstance(item, Mapping)} expected_deviation_ids: set[str] = set() for case_id in sorted(retained_ids): if _deviation_entry_failures( @@ -507,6 +451,4 @@ def _validate_baseline_drift( if join is None: return baseline_by_id, retest_by_id, retained_ids = join - _deviation_failures( - snapshot, retained_ids, baseline_by_id, retest_by_id, failures, path - ) + _deviation_failures(snapshot, retained_ids, baseline_by_id, retest_by_id, failures, path) diff --git a/tools/formal_semantic_validation/_loading.py b/tools/formal_semantic_validation/_loading.py index 2e148f300..882f989b2 100644 --- a/tools/formal_semantic_validation/_loading.py +++ b/tools/formal_semantic_validation/_loading.py @@ -85,29 +85,17 @@ def load_release_bundles(repo_root: Path = REPO_ROOT) -> list[EvidenceRelease]: "53.0.0", "54.0.0", }: - raise ValueError( - "formal evidence requires every supported historical and current release" - ) + raise ValueError("formal evidence requires every supported historical and current release") releases: list[EvidenceRelease] = [] for manifest_path, manifest in records: revision_key(manifest.get("revision")) loaded: list[dict[str, object]] = [] for label in ("protocol", "corpus", "snapshot", "analysis"): path_value = manifest.get(f"{label}_path") - path = ( - safe_repo_path(repo_root, path_value) - if isinstance(path_value, str) - else None - ) + path = safe_repo_path(repo_root, path_value) if isinstance(path_value, str) else None if path is None or not path.is_file(): - raise ValueError( - f"{manifest_path!r} contains unsafe or missing {label}_path" - ) - loaded.append( - load_bounded_json_object( - repo_root, path_value, max_bytes=_MAX_FILE_BYTES - ) - ) + raise ValueError(f"{manifest_path!r} contains unsafe or missing {label}_path") + loaded.append(load_bounded_json_object(repo_root, path_value, max_bytes=_MAX_FILE_BYTES)) releases.append( EvidenceRelease( manifest_path=manifest_path, @@ -140,17 +128,8 @@ def load_retest_bundle( releases = load_release_bundles(repo_root) if not releases: - raise ValueError( - "the formal semantic-validation index selects no v2 retest release" - ) - release = max( - releases, key=lambda item: revision_key(item.manifest.get("revision")) - ) - if ( - release.manifest.get("revision") != "54.0.0" - or release.protocol.get("revision") != "2.0.0" - ): - raise ValueError( - "the current formal evidence release must be the explicit 54.0.0 retest" - ) + raise ValueError("the formal semantic-validation index selects no v2 retest release") + release = max(releases, key=lambda item: revision_key(item.manifest.get("revision"))) + if release.manifest.get("revision") != "54.0.0" or release.protocol.get("revision") != "2.0.0": + raise ValueError("the current formal evidence release must be the explicit 54.0.0 retest") return release, release.protocol, release.corpus, release.snapshot, release.analysis diff --git a/tools/formal_semantic_validation/_releases.py b/tools/formal_semantic_validation/_releases.py index eba47fcc2..8a5dd11fc 100644 --- a/tools/formal_semantic_validation/_releases.py +++ b/tools/formal_semantic_validation/_releases.py @@ -44,9 +44,7 @@ def _stale_pin(repo_root: Path, path_value: object, digest_value: object) -> bool: - resolved = ( - safe_repo_path(repo_root, path_value) if isinstance(path_value, str) else None - ) + resolved = safe_repo_path(repo_root, path_value) if isinstance(path_value, str) else None return ( resolved is None or not resolved.is_file() @@ -63,9 +61,7 @@ def _release_document_pin_failures( path: str, ) -> None: for label in ("protocol", "corpus", "snapshot", "analysis"): - if _stale_pin( - repo_root, manifest.get(f"{label}_path"), manifest.get(f"{label}_sha256") - ): + if _stale_pin(repo_root, manifest.get(f"{label}_path"), manifest.get(f"{label}_sha256")): failures.append( _failure( "formal-validation-release-digest", @@ -125,9 +121,7 @@ def _pinned_release_artifacts( return list(artifacts) -def validate_release_bundle( - repo_root: Path, release: EvidenceRelease -) -> list[PolicyFailure]: +def validate_release_bundle(repo_root: Path, release: EvidenceRelease) -> list[PolicyFailure]: """Validate one atomic release record, all digest pins, and its evidence.""" failures: list[PolicyFailure] = [] @@ -190,9 +184,7 @@ def validate_release_bundle( replay_cases=False, ) ) - artifact_by_kind = { - item.get("kind"): item for item in artifacts if isinstance(item, Mapping) - } + artifact_by_kind = {item.get("kind"): item for item in artifacts if isinstance(item, Mapping)} sat_snapshot_pin = artifact_by_kind.get("satisfiability-snapshot") sat_analysis_pin = artifact_by_kind.get("satisfiability-analysis") if sat_snapshot_pin is not None or sat_analysis_pin is not None: @@ -206,12 +198,8 @@ def validate_release_bundle( ) else: legacy_manifest["revision"] = "2.0.0" - legacy_manifest["satisfiability_snapshot_path"] = sat_snapshot_pin.get( - "path" - ) - legacy_manifest["satisfiability_analysis_path"] = sat_analysis_pin.get( - "path" - ) + legacy_manifest["satisfiability_snapshot_path"] = sat_snapshot_pin.get("path") + legacy_manifest["satisfiability_analysis_path"] = sat_analysis_pin.get("path") snapshot = load_bounded_json_object( repo_root, str(sat_snapshot_pin.get("path")), @@ -323,10 +311,7 @@ def validate_retest_bundle( ) ) expected_corpus_revision = _expected_corpus_revision(release_revision) - if ( - protocol.get("revision") != "2.0.0" - or corpus.get("revision") != expected_corpus_revision - ): + if protocol.get("revision") != "2.0.0" or corpus.get("revision") != expected_corpus_revision: failures.append( _failure( "formal-validation-retest-revision", @@ -347,9 +332,7 @@ def validate_retest_bundle( ) _validate_protocol(repo_root, protocol, failures, protocol_path) cases_by_id = _validate_corpus(repo_root, protocol, corpus, failures, corpus_path) - historical_cases = _retained_historical_cases( - repo_root, cases_by_id, failures, corpus_path, corpus.get("revision") - ) + historical_cases = _retained_historical_cases(repo_root, cases_by_id, failures, corpus_path, corpus.get("revision")) _validate_retest_snapshot( _RetestScope( repo_root=repo_root, @@ -363,17 +346,9 @@ def validate_retest_bundle( failures, snapshot_path, ) - baseline_cases = ( - cases_by_id - if release_revision in _SOURCE_BOUND_RETEST_REVISIONS - else historical_cases - ) - _validate_baseline_drift( - repo_root, snapshot, baseline_cases, failures, snapshot_path - ) - _validate_analysis( - repo_root, protocol, corpus, snapshot, analysis, failures, analysis_path - ) + baseline_cases = cases_by_id if release_revision in _SOURCE_BOUND_RETEST_REVISIONS else historical_cases + _validate_baseline_drift(repo_root, snapshot, baseline_cases, failures, snapshot_path) + _validate_analysis(repo_root, protocol, corpus, snapshot, analysis, failures, analysis_path) return failures @@ -386,15 +361,9 @@ def _current_retest_source_failures( release_revision: str, replay_current: bool, ) -> None: - failures.extend( - source_state_failures( - repo_root, snapshot.get("source_state"), path, current=replay_current - ) - ) + failures.extend(source_state_failures(repo_root, snapshot.get("source_state"), path, current=replay_current)) state = snapshot.get("source_state") - if not isinstance(state, Mapping) or state.get("base_revision") != snapshot.get( - "raes_revision" - ): + if not isinstance(state, Mapping) or state.get("base_revision") != snapshot.get("raes_revision"): failures.append( _failure( "research-evidence-source-state", @@ -457,10 +426,7 @@ def _current_retest_source_failures( "53.0.0": "52.0.0", "54.0.0": "53.0.0", }[release_revision] - if ( - not isinstance(baseline, Mapping) - or baseline.get("release_revision") != expected_baseline - ): + if not isinstance(baseline, Mapping) or baseline.get("release_revision") != expected_baseline: failures.append( _failure( "formal-validation-baseline-selection", @@ -493,18 +459,14 @@ def _retained_historical_cases( ) historical_corpus = {} historical_cases = { - item.get("case_id"): item - for item in historical_corpus.get("cases", []) - if isinstance(item, Mapping) + item.get("case_id"): item for item in historical_corpus.get("cases", []) if isinstance(item, Mapping) } retained_cases_match = all( cases_by_id.get(str(case_id)) == { **case, "fixture_path": ( - PARTICIPANT_IDENTITY_FIXTURE_SUCCESSORS.get( - case.get("fixture_path"), case.get("fixture_path") - ) + PARTICIPANT_IDENTITY_FIXTURE_SUCCESSORS.get(case.get("fixture_path"), case.get("fixture_path")) if corpus_revision == "4.0.0" else case.get("fixture_path") ), diff --git a/tools/formal_semantic_validation/_retest.py b/tools/formal_semantic_validation/_retest.py index 3ce42222d..aa91752de 100644 --- a/tools/formal_semantic_validation/_retest.py +++ b/tools/formal_semantic_validation/_retest.py @@ -66,11 +66,7 @@ def _validate_retest_snapshot( if not _closed_object( snapshot, _SNAPSHOT_V2_KEYS - | ( - {"source_state"} - if release.manifest.get("revision") in _SOURCE_STATE_REVISIONS - else set() - ), + | ({"source_state"} if release.manifest.get("revision") in _SOURCE_STATE_REVISIONS else set()), rule_id="formal-validation-snapshot-shape", label="retest snapshot", failures=failures, @@ -78,28 +74,18 @@ def _validate_retest_snapshot( ): return _validate_retest_header(protocol, corpus, snapshot, failures, path) - command_ids, commands_by_id = _validate_retest_commands( - protocol, snapshot, failures, path - ) + command_ids, commands_by_id = _validate_retest_commands(protocol, snapshot, failures, path) - release_artifacts = [ - item - for item in release.manifest.get("artifacts", []) - if isinstance(item, Mapping) - ] + release_artifacts = [item for item in release.manifest.get("artifacts", []) if isinstance(item, Mapping)] release_artifacts_by_path = { - item.get("path"): item - for item in release_artifacts - if isinstance(item.get("path"), str) + item.get("path"): item for item in release_artifacts if isinstance(item.get("path"), str) } expected_release_paths = _retest_observation_failures( scope, (release_artifacts_by_path, commands_by_id), failures, path ) if release.manifest.get("revision") in _SOURCE_STATE_REVISIONS: expected_release_paths.update(_retained_fixture_paths(cases_by_id)) - _validate_release_selection( - scope, command_ids, expected_release_paths, failures, path - ) + _validate_release_selection(scope, command_ids, expected_release_paths, failures, path) _validate_retest_participant_observations(protocol, snapshot, failures, path) @@ -126,8 +112,7 @@ def _validate_release_selection( selected_release_paths = { str(item.get("path")) for item in scope.release.manifest.get("artifacts", []) - if isinstance(item, Mapping) - and item.get("kind") in {"corpus-input", "production-evidence"} + if isinstance(item, Mapping) and item.get("kind") in {"corpus-input", "production-evidence"} } if selected_release_paths != expected_paths: failures.append( @@ -208,9 +193,7 @@ def _validate_retest_commands( return command_ids, commands_by_id -def _validate_retest_command( - command: object, failures: list[PolicyFailure], path: str -) -> None: +def _validate_retest_command(command: object, failures: list[PolicyFailure], path: str) -> None: if not _closed_object( command, _COMMAND_KEYS, @@ -242,10 +225,7 @@ def _validate_retest_participant_command( "-q", *_participant_test_refs(protocol), ] - if ( - not isinstance(participant_command, Mapping) - or participant_command.get("argv") != expected_argv - ): + if not isinstance(participant_command, Mapping) or participant_command.get("argv") != expected_argv: failures.append( _failure( "formal-validation-participant-command", @@ -286,15 +266,11 @@ def _validate_retest_observation( ) ) else: - _validate_retest_observation_metadata( - scope.snapshot, case, observation, failures, path - ) + _validate_retest_observation_metadata(scope.snapshot, case, observation, failures, path) if case.get("replay_mode") in PRODUCTION_EVIDENCE_REPLAY_MODES: release_artifacts_by_path, commands_by_id = replay_context _validate_production_evidence_observation( - _ProductionObservationContext( - scope.repo_root, release_artifacts_by_path, scope.replay_current - ), + _ProductionObservationContext(scope.repo_root, release_artifacts_by_path, scope.replay_current), case, observation, commands_by_id.get(case_id), @@ -329,9 +305,9 @@ def _validate_retest_observation_metadata( path: str, ) -> None: case_id = observation.get("case_id") - if observation.get("execution_id") != snapshot.get( - "execution_id" - ) or observation.get("configuration_id") != snapshot.get("configuration_id"): + if observation.get("execution_id") != snapshot.get("execution_id") or observation.get( + "configuration_id" + ) != snapshot.get("configuration_id"): failures.append( _failure( "formal-validation-observation-join", @@ -348,9 +324,7 @@ def _validate_retest_observation_metadata( path, ) ) - if not _string_list(observation.get("evidence_refs")) or not _string_list( - observation.get("limitations") - ): + if not _string_list(observation.get("evidence_refs")) or not _string_list(observation.get("limitations")): failures.append( _failure( "formal-validation-observation-evidence", @@ -421,17 +395,12 @@ def _validate_retained_retest_observation( ) -def _historical_observation_matches( - case: Mapping[str, object], observation: Mapping[str, object] -) -> bool: +def _historical_observation_matches(case: Mapping[str, object], observation: Mapping[str, object]) -> bool: digest = observation.get("result_digest") diagnostic_kind = observation.get("diagnostic_kind") return ( observation.get("actual_outcome") == case.get("expected_outcome") - and ( - digest is None - or (isinstance(digest, str) and bool(_SHA256_RE.fullmatch(digest))) - ) + and (digest is None or (isinstance(digest, str) and bool(_SHA256_RE.fullmatch(digest)))) and (diagnostic_kind is None or isinstance(diagnostic_kind, str)) ) From 0ac86b9c4e789d9f852998d11046b9a94a8fb28c Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Sun, 27 Sep 2026 06:57:11 +0200 Subject: [PATCH 06/10] fix: use autarchy Sonar credential --- .github/workflows/ci.yml | 2 +- implementations/python/tests/test_release_workflows.py | 2 +- tools/tooling_artifact_policy_actions.py | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4a1cb0b5e..bf67ae63f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -43,7 +43,7 @@ jobs: # token below is never exposed to fork or Dependabot contexts. sonar-enabled: true secrets: - sonar_token: ${{ secrets.SONAR_TOKEN }} + sonar_token: ${{ secrets.AUTARCHY_SONAR_TOKEN }} # The repository's dev/main branch protections require the historical `verify` # and `sonar` check contexts. The reusable call is atomic to this caller, so it diff --git a/implementations/python/tests/test_release_workflows.py b/implementations/python/tests/test_release_workflows.py index 4d3624ae3..ca59072b1 100644 --- a/implementations/python/tests/test_release_workflows.py +++ b/implementations/python/tests/test_release_workflows.py @@ -439,7 +439,7 @@ def test_ci_uses_the_same_canonical_verifier_for_github_sha() -> None: assert "github.event.pull_request.base.sha" in canonical["with"]["base-rev"] assert canonical["with"]["requirement-branch"] == "${{ github.head_ref || github.ref_name }}" assert canonical["with"]["sonar-enabled"] is True - assert canonical["secrets"]["sonar_token"] == "${{ secrets.SONAR_TOKEN }}" + assert canonical["secrets"]["sonar_token"] == "${{ secrets.AUTARCHY_SONAR_TOKEN }}" # noqa: S105 # dev/main branch protection requires the `verify` and `sonar` contexts. Both # are now decoupled joins over the reusable graph's outcomes (#935). diff --git a/tools/tooling_artifact_policy_actions.py b/tools/tooling_artifact_policy_actions.py index b74cfe186..eb8c9f125 100644 --- a/tools/tooling_artifact_policy_actions.py +++ b/tools/tooling_artifact_policy_actions.py @@ -49,8 +49,8 @@ def _sonar_boundary(path: str, name: str, job: Mapping[str, Any], workflows: Map and name == "canonical" and guarded and job.get("uses") == "./" + _CANONICAL - and job.get("secrets") == {"sonar_token": "${{ secrets.SONAR_TOKEN }}"} - and _secret_expressions(job) == {"${{ secrets.SONAR_TOKEN }}"} + and job.get("secrets") == {"sonar_token": "${{ secrets.AUTARCHY_SONAR_TOKEN }}"} + and _secret_expressions(job) == {"${{ secrets.AUTARCHY_SONAR_TOKEN }}"} ) From 27ff564eb35aa65657738da995431b744030dba3 Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Sun, 27 Sep 2026 07:18:38 +0200 Subject: [PATCH 07/10] fix: restore refreshed Sonar credential --- .github/workflows/ci.yml | 2 +- implementations/python/tests/test_release_workflows.py | 2 +- tools/tooling_artifact_policy_actions.py | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bf67ae63f..4a1cb0b5e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -43,7 +43,7 @@ jobs: # token below is never exposed to fork or Dependabot contexts. sonar-enabled: true secrets: - sonar_token: ${{ secrets.AUTARCHY_SONAR_TOKEN }} + sonar_token: ${{ secrets.SONAR_TOKEN }} # The repository's dev/main branch protections require the historical `verify` # and `sonar` check contexts. The reusable call is atomic to this caller, so it diff --git a/implementations/python/tests/test_release_workflows.py b/implementations/python/tests/test_release_workflows.py index ca59072b1..960a8fe46 100644 --- a/implementations/python/tests/test_release_workflows.py +++ b/implementations/python/tests/test_release_workflows.py @@ -439,7 +439,7 @@ def test_ci_uses_the_same_canonical_verifier_for_github_sha() -> None: assert "github.event.pull_request.base.sha" in canonical["with"]["base-rev"] assert canonical["with"]["requirement-branch"] == "${{ github.head_ref || github.ref_name }}" assert canonical["with"]["sonar-enabled"] is True - assert canonical["secrets"]["sonar_token"] == "${{ secrets.AUTARCHY_SONAR_TOKEN }}" # noqa: S105 + assert canonical["secrets"]["sonar_token"] == "${{ secrets.SONAR_TOKEN }}" # noqa: S105 # dev/main branch protection requires the `verify` and `sonar` contexts. Both # are now decoupled joins over the reusable graph's outcomes (#935). diff --git a/tools/tooling_artifact_policy_actions.py b/tools/tooling_artifact_policy_actions.py index eb8c9f125..b74cfe186 100644 --- a/tools/tooling_artifact_policy_actions.py +++ b/tools/tooling_artifact_policy_actions.py @@ -49,8 +49,8 @@ def _sonar_boundary(path: str, name: str, job: Mapping[str, Any], workflows: Map and name == "canonical" and guarded and job.get("uses") == "./" + _CANONICAL - and job.get("secrets") == {"sonar_token": "${{ secrets.AUTARCHY_SONAR_TOKEN }}"} - and _secret_expressions(job) == {"${{ secrets.AUTARCHY_SONAR_TOKEN }}"} + and job.get("secrets") == {"sonar_token": "${{ secrets.SONAR_TOKEN }}"} + and _secret_expressions(job) == {"${{ secrets.SONAR_TOKEN }}"} ) From 8427757825adfb8a2d6db10f23cc3085b62b92dd Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Sun, 27 Sep 2026 08:57:31 +0200 Subject: [PATCH 08/10] refactor: centralize formal evidence revisions --- tools/formal_semantic_validation/_baseline.py | 57 +---------------- tools/formal_semantic_validation/_loading.py | 61 +------------------ 2 files changed, 5 insertions(+), 113 deletions(-) diff --git a/tools/formal_semantic_validation/_baseline.py b/tools/formal_semantic_validation/_baseline.py index 6ea0a16dc..560463bed 100644 --- a/tools/formal_semantic_validation/_baseline.py +++ b/tools/formal_semantic_validation/_baseline.py @@ -6,6 +6,7 @@ from pathlib import Path from tools.evidence_bundle_index import load_index_records +from tools.formal_semantic_validation._release_revisions import _HISTORICAL_RETEST_REVISIONS from tools.formal_semantic_validation._shape import ( _closed_object, _failure, @@ -30,61 +31,7 @@ _ADDITIONAL_ARCHIVE_PINS_SHA256 = "04b4a1cdfa8c76ccbc536e87365e9343bec4fb8dcde712c15a6535c6e927352a" _DRIFT_COMPARISON_KEYS = ("actual_outcome", "diagnostic_kind", "result_digest") -_V2_REVISIONS = frozenset( - { - "3.0.0", - "4.0.0", - "5.0.0", - "6.0.0", - "7.0.0", - "8.0.0", - "9.0.0", - "10.0.0", - "11.0.0", - "12.0.0", - "13.0.0", - "14.0.0", - "15.0.0", - "16.0.0", - "17.0.0", - "18.0.0", - "19.0.0", - "20.0.0", - "21.0.0", - "22.0.0", - "23.0.0", - "24.0.0", - "25.0.0", - "26.0.0", - "27.0.0", - "28.0.0", - "29.0.0", - "30.0.0", - "31.0.0", - "32.0.0", - "33.0.0", - "34.0.0", - "35.0.0", - "36.0.0", - "37.0.0", - "38.0.0", - "39.0.0", - "40.0.0", - "41.0.0", - "42.0.0", - "43.0.0", - "44.0.0", - "45.0.0", - "46.0.0", - "47.0.0", - "48.0.0", - "49.0.0", - "50.0.0", - "51.0.0", - "52.0.0", - "53.0.0", - } -) +_V2_REVISIONS = _HISTORICAL_RETEST_REVISIONS _V3_CORPUS_REVISIONS = frozenset( { "16.0.0", diff --git a/tools/formal_semantic_validation/_loading.py b/tools/formal_semantic_validation/_loading.py index 882f989b2..36002d218 100644 --- a/tools/formal_semantic_validation/_loading.py +++ b/tools/formal_semantic_validation/_loading.py @@ -5,6 +5,7 @@ from pathlib import Path from tools.evidence_bundle_index import load_index_records, revision_key +from tools.formal_semantic_validation._release_revisions import _SUPPORTED_RETEST_REVISIONS from tools.formal_semantic_validation._types import ( _MAX_FILE_BYTES, MANIFEST_PATH, @@ -27,64 +28,8 @@ def load_release_bundles(repo_root: Path = REPO_ROOT) -> list[EvidenceRelease]: max_bytes=_MAX_FILE_BYTES, ) current_release_path(records) - if {record.get("revision") for _, record in records} != { - "1.0.0", - "1.1.0", - "1.2.0", - "2.0.0", - "3.0.0", - "4.0.0", - "5.0.0", - "6.0.0", - "7.0.0", - "8.0.0", - "9.0.0", - "10.0.0", - "11.0.0", - "12.0.0", - "13.0.0", - "14.0.0", - "15.0.0", - "16.0.0", - "17.0.0", - "18.0.0", - "19.0.0", - "20.0.0", - "21.0.0", - "22.0.0", - "23.0.0", - "24.0.0", - "25.0.0", - "26.0.0", - "27.0.0", - "28.0.0", - "29.0.0", - "30.0.0", - "31.0.0", - "32.0.0", - "33.0.0", - "34.0.0", - "35.0.0", - "36.0.0", - "37.0.0", - "38.0.0", - "39.0.0", - "40.0.0", - "41.0.0", - "42.0.0", - "43.0.0", - "44.0.0", - "45.0.0", - "46.0.0", - "47.0.0", - "48.0.0", - "49.0.0", - "50.0.0", - "51.0.0", - "52.0.0", - "53.0.0", - "54.0.0", - }: + supported_revisions = _SUPPORTED_RETEST_REVISIONS | {"1.0.0", "1.1.0", "1.2.0", "2.0.0"} + if {record.get("revision") for _, record in records} != supported_revisions: raise ValueError("formal evidence requires every supported historical and current release") releases: list[EvidenceRelease] = [] for manifest_path, manifest in records: From 687311011fa931ce36f9193920c06da2f1dc589a Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Sun, 27 Sep 2026 09:22:07 +0200 Subject: [PATCH 09/10] refactor: separate current historical revision --- tools/formal_semantic_validation/_release_revisions.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tools/formal_semantic_validation/_release_revisions.py b/tools/formal_semantic_validation/_release_revisions.py index 60dd00488..f9c58d269 100644 --- a/tools/formal_semantic_validation/_release_revisions.py +++ b/tools/formal_semantic_validation/_release_revisions.py @@ -52,9 +52,8 @@ "50.0.0", "51.0.0", "52.0.0", - "53.0.0", } -) +) | {"53.0.0"} _SUPPORTED_RETEST_REVISIONS = _HISTORICAL_RETEST_REVISIONS | {"54.0.0"} _SOURCE_BOUND_RETEST_REVISIONS = _SUPPORTED_RETEST_REVISIONS - {"3.0.0"} From 44cabc82481a1cc81453908cdc2c767f9a5c311e Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Sun, 27 Sep 2026 09:55:37 +0200 Subject: [PATCH 10/10] Fix Python test import ordering --- .../python/tests/test_formal_semantic_validation.py | 3 +-- .../python/tests/test_issue_989_versioned_evidence.py | 8 -------- .../python/tests/test_specification_coverage.py | 3 +-- 3 files changed, 2 insertions(+), 12 deletions(-) diff --git a/implementations/python/tests/test_formal_semantic_validation.py b/implementations/python/tests/test_formal_semantic_validation.py index ac77b92d9..812bf74be 100644 --- a/implementations/python/tests/test_formal_semantic_validation.py +++ b/implementations/python/tests/test_formal_semantic_validation.py @@ -8,9 +8,8 @@ from types import SimpleNamespace import pytest -from evidence_test_fixtures import copy_bundle - import tools.check_formal_semantic_validation as formal_validation +from evidence_test_fixtures import copy_bundle from tools.check_formal_semantic_validation import ( REQUIRED_CLAIM_CLASS_IDS, REQUIRED_PARTICIPANT_OBLIGATION_IDS, diff --git a/implementations/python/tests/test_issue_989_versioned_evidence.py b/implementations/python/tests/test_issue_989_versioned_evidence.py index b8801df94..707f08176 100644 --- a/implementations/python/tests/test_issue_989_versioned_evidence.py +++ b/implementations/python/tests/test_issue_989_versioned_evidence.py @@ -16,7 +16,6 @@ def test_historical_evidence_rejects_malformed_shapes_even_with_rebound_digest(c import json from raes_contracts.canonical import canonical_json_digest - from tools.formal_semantic_validation._production import _historical_production_replay payload = json.loads((ROOT / f"docs/research/formal-semantic-validation/evidence/{case_name}-v3.json").read_text()) @@ -98,7 +97,6 @@ def test_historical_computed_joins_reject_rebound_evidence(family, field): import json from raes_contracts.canonical import canonical_json_digest - from tools.formal_semantic_validation._production import _historical_production_replay payload = json.loads((ROOT / f"docs/research/formal-semantic-validation/evidence/{family}-v3.json").read_text()) @@ -124,7 +122,6 @@ def test_historical_integrity_checks_reject_shape_valid_substitutions(version, m import json from raes_contracts.canonical import canonical_json_digest - from tools.formal_semantic_validation._production import _historical_production_replay satisfiability = mutation in {"source", "authored"} @@ -162,7 +159,6 @@ def test_current_compile_replay_hashes_complete_capture_dimension(): from raes import instantiate_scenario, parse_sdl_file from raes_processor.compiler import compile_runtime_model - from tools.formal_semantic_validation._loading import load_retest_bundle from tools.formal_semantic_validation._replay import _compiled_case_digest, _migration_policy_for_case from tools.formal_semantic_validation._shape import _digest @@ -212,7 +208,6 @@ def test_old_output_digest_pairs_do_not_substitute_for_replay(): def test_historical_integrated_release_does_not_execute_current_code(monkeypatch, revision): from raes_contracts.exploit_path import ExploitPathAnalysisEvidenceModel from raes_contracts.satisfiability import ScenarioSatisfiabilityEvidenceModel - from tools.formal_semantic_validation import _production, _releases, _retest from tools.formal_semantic_validation._loading import load_release_bundles @@ -265,7 +260,6 @@ def test_current_release_requires_truthful_implementation_provenance(): @pytest.mark.integration def test_current_production_evidence_replay_failure_is_not_hidden(monkeypatch): from raes_processor import satisfiability - from tools.formal_semantic_validation._loading import load_retest_bundle from tools.formal_semantic_validation._releases import validate_retest_bundle @@ -378,7 +372,6 @@ def test_source_state_malformed_values_fail_closed(state): def test_historical_supplement_never_runs_current_analyzer(monkeypatch): from raes_processor import satisfiability - from tools.formal_semantic_validation._loading import load_release_bundles from tools.formal_semantic_validation._releases import validate_release_bundle @@ -643,7 +636,6 @@ def test_classification_retirement_has_a_recorded_adr_001_amendment(): import hashlib import yaml - from tools.check_adr_immutability import amendment_refs, canonical_content path = ROOT / "docs/decisions/adrs/adr-001-scenario-description-language.md" diff --git a/implementations/python/tests/test_specification_coverage.py b/implementations/python/tests/test_specification_coverage.py index c3d72a98c..cb3d4c9fc 100644 --- a/implementations/python/tests/test_specification_coverage.py +++ b/implementations/python/tests/test_specification_coverage.py @@ -6,9 +6,8 @@ from pathlib import Path import pytest -from evidence_test_fixtures import copy_bundle - import tools.check_specification_coverage as coverage_gate +from evidence_test_fixtures import copy_bundle from tools.check_specification_coverage import ( EXPECTED_CLASSIFICATIONS, EXPECTED_STRATA,