From 4dbccc6fdd1e4e68a45184d521a15909ff9123db Mon Sep 17 00:00:00 2001 From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com> Date: Tue, 13 Oct 2026 03:47:31 +0000 Subject: [PATCH 1/2] fix(sdl): report lock, trust-policy and import-provenance failures as sdl diagnostics --- docs/explain/sdl/parser.md | 5 +- .../packages/raes/_composition_provenance.py | 56 ++- .../packages/raes/_model_diagnostics.py | 44 +- .../packages/raes/composition/_expand.py | 25 +- .../packages/raes/composition/_provenance.py | 8 +- .../packages/raes/module_registry/__init__.py | 3 +- .../raes/module_registry/_lock_records.py | 54 +++ .../packages/raes/module_registry/models.py | 38 +- .../raes/module_registry/resolution.py | 144 +++---- .../python/packages/raes_cli/sdl.py | 19 +- ..._issue_1580_import_boundary_diagnostics.py | 391 ++++++++++++++++++ 11 files changed, 667 insertions(+), 120 deletions(-) create mode 100644 implementations/python/packages/raes/module_registry/_lock_records.py create mode 100644 implementations/python/tests/test_issue_1580_import_boundary_diagnostics.py diff --git a/docs/explain/sdl/parser.md b/docs/explain/sdl/parser.md index 1f50985af..b150ca412 100644 --- a/docs/explain/sdl/parser.md +++ b/docs/explain/sdl/parser.md @@ -228,7 +228,10 @@ invalid, including when migration acceptance is enabled. Imported-unit typed-model failures use the same bounded `sdl.model.invalid` diagnostics as root declarations, with the imported source file and field pointer. Malformed import version constraints also raise `SDLParseError` with a -field diagnostic. Authored behavior refs using the reserved `__private` segment +field diagnostic, through `parse_sdl_file()` and `resolve_lock_records()` alike. +An invalid or cyclic `raes.lock.json` record, an unreadable or invalid +`raes.lock.json` or `raes-trust.yaml`, and an import that names a directory also +raise `SDLParseError`, naming the file or import without rendering its values. Authored behavior refs using the reserved `__private` segment fail before composition; generated private refs remain valid in expanded SDL. See [behavior composition](../../decisions/issue-297-behavior-authoring.md) for reference scope, compatibility, and the authoring/runtime boundary. diff --git a/implementations/python/packages/raes/_composition_provenance.py b/implementations/python/packages/raes/_composition_provenance.py index 82014f115..47fef55b5 100644 --- a/implementations/python/packages/raes/_composition_provenance.py +++ b/implementations/python/packages/raes/_composition_provenance.py @@ -3,14 +3,19 @@ from __future__ import annotations from collections.abc import Mapping +from pathlib import Path + +from pydantic import ValidationError from ._errors import SDLParseError +from ._model_diagnostics import _field_problems from ._module_symbols import HASHMAP_SECTIONS from .instantiate import _BoundScenarioResult from .module_registry import ResolvedModule from .phase_contracts import ( CapabilityConstraint, ExplicitnessProvenanceRecord, + ParameterBinding, ParameterDerivation, ResolvedImportProvenance, ) @@ -36,21 +41,44 @@ def resolved_import_record( *, requested: ImportDecl, bindings: _BoundScenarioResult, + path: Path, ) -> ResolvedImportProvenance: - return ResolvedImportProvenance( - namespace=(requested.namespace,), - requested_source=requested.normalized_source, - requested_version=requested.version, - requested_digest=_normalized_digest(requested.digest), - module_id=resolved.module_descriptor.id, - module_version=resolved.module_descriptor.version, - resolved_source=resolved.resolved_source, - manifest_digest=_normalized_digest(resolved.manifest_digest), - content_digest=_normalized_digest(resolved.content_digest), - export_hash=_normalized_digest(resolved.export_hash), - signer_id=resolved.signer_id, - bindings=bindings.bindings, - ) + return _provenance_record(resolved, requested=requested, bindings=bindings.bindings, path=path) + + +def _provenance_record( + resolved: ResolvedModule, + *, + requested: ImportDecl, + path: Path, + bindings: tuple[ParameterBinding, ...] = (), +) -> ResolvedImportProvenance: + """Build one resolved-import record, failing as an SDL error when its bounds reject a value. + + ``path`` is the document that declares ``requested``; the error names it. + """ + + try: + return ResolvedImportProvenance( + namespace=(requested.namespace,), + requested_source=requested.normalized_source, + requested_version=requested.version, + requested_digest=_normalized_digest(requested.digest), + module_id=resolved.module_descriptor.id, + module_version=resolved.module_descriptor.version, + resolved_source=resolved.resolved_source, + manifest_digest=_normalized_digest(resolved.manifest_digest), + content_digest=_normalized_digest(resolved.content_digest), + export_hash=_normalized_digest(resolved.export_hash), + signer_id=resolved.signer_id, + bindings=bindings, + ) + except ValidationError as exc: + raise SDLParseError( + f"Import '{requested.normalized_source}' cannot be recorded as resolved import provenance: " + + _field_problems(exc), + path=path, + ) from exc def prefixed_constraint( diff --git a/implementations/python/packages/raes/_model_diagnostics.py b/implementations/python/packages/raes/_model_diagnostics.py index 2ea5c1b35..72e1f3c8b 100644 --- a/implementations/python/packages/raes/_model_diagnostics.py +++ b/implementations/python/packages/raes/_model_diagnostics.py @@ -8,9 +8,10 @@ from __future__ import annotations +from collections.abc import Mapping from pathlib import Path -from pydantic import ValidationError +from pydantic import TypeAdapter, ValidationError from ._classification_guard import CLASSIFICATION_MIGRATION_CODE from ._errors import ( @@ -19,6 +20,9 @@ SDLSourcePosition, SDLSourceRange, ) +from ._module_declarations import ImportDecl + +_IMPORT_DECLARATIONS: TypeAdapter[list[ImportDecl]] = TypeAdapter(list[ImportDecl]) def _dedupe_source_diagnostics( @@ -77,15 +81,30 @@ def _bounded_model_message(message: str) -> str: return escaped[: _MODEL_DIAGNOSTIC_MESSAGE_MAX_LENGTH - 3] + "..." +def _field_problems(error: ValidationError, *, field_names: Mapping[str, str] | None = None) -> str: + """Render each failure as ``field: message`` with bounded prose and no input values.""" + + names = field_names or {} + problems: list[str] = [] + for item in error.errors(): + location = [str(part) for part in item.get("loc", ())] + if location: + location[0] = names.get(location[0], location[0]) + message = _bounded_model_message(str(item.get("msg", ""))) + problems.append(f"{'.'.join(location)}: {message}" if location else message) + return "; ".join(problems) + + def _model_parse_error( error: ValidationError, *, path: Path | None, source_ranges: dict[str, SDLSourceRange], + location_prefix: tuple[str, ...] = (), ) -> SDLParseError: diagnostics: list[SDLParseDiagnostic] = [] for item in error.errors(): - pointer = _pointer_from_location(tuple(item.get("loc", ()))) + pointer = _pointer_from_location((*location_prefix, *item.get("loc", ()))) raw_message = str(item.get("msg", "")) is_identifier = "portable SDL identifier" in raw_message or "qualified SDL identifier" in raw_message message = _bounded_model_message(raw_message) @@ -110,3 +129,24 @@ def _model_parse_error( path=path, diagnostics=diagnostics, ) + + +def _import_declarations( + data: Mapping[str, object], + *, + path: Path | None, + source_ranges: dict[str, SDLSourceRange], +) -> list[ImportDecl]: + """Validate a document's ``imports`` as its typed field, failing with field diagnostics. + + Pointers and source ranges match what full-document validation reports for + the same ``imports`` value, so callers that consume only the declarations + agree with :func:`raes.parser.parse_sdl` (ADR-053 validation order, step 3). + """ + + if "imports" not in data: + return [] + try: + return _IMPORT_DECLARATIONS.validate_python(data["imports"]) + except ValidationError as exc: + raise _model_parse_error(exc, path=path, source_ranges=source_ranges, location_prefix=("imports",)) from exc diff --git a/implementations/python/packages/raes/composition/_expand.py b/implementations/python/packages/raes/composition/_expand.py index 79136e66d..1a4ae8841 100644 --- a/implementations/python/packages/raes/composition/_expand.py +++ b/implementations/python/packages/raes/composition/_expand.py @@ -15,7 +15,7 @@ from .._composition_budget import CompositionBudget, CompositionTraversal from .._errors import SDLInstantiationError, SDLParseDiagnostic, SDLParseError, SDLSourceRange -from .._model_diagnostics import _model_parse_error +from .._model_diagnostics import _import_declarations, _model_parse_error from .._module_symbols import FORWARDING_AGENTS_SECTION from .._module_symbols import HASHMAP_SECTIONS as _HASHMAP_SECTIONS from .._module_symbols import ( @@ -37,7 +37,7 @@ load_trust_policy, resolve_import, ) -from ..parser import _load_normalized_data +from ..parser import _load_normalized_data, _reject_removed_scoring_sections from ..phase_contracts import ( CapabilityConstraint, ExpansionProvenance, @@ -173,12 +173,6 @@ def _merge_sections( return merged -def _import_decl(value: object) -> ImportDecl: - if isinstance(value, ImportDecl): - return value - return ImportDecl.model_validate(value) - - @dataclass(frozen=True) class _ImportContext: """Invariant per-document context threaded through each import expansion.""" @@ -234,7 +228,7 @@ def _expansion_context(options: _ExpansionPrivateOptions) -> _ExpansionContext: def _expand_one_import( - raw_import: object, + import_decl: ImportDecl, merged: dict[str, Any], context: _ImportContext, ) -> tuple[ @@ -249,7 +243,6 @@ def _expand_one_import( """Resolve, expand, namespace, and merge a single import; return provenance additions.""" context.budget.add_import(path=context.path) - import_decl = _import_decl(raw_import) if "__private." in import_decl.namespace: raise SDLParseError( "Import namespaces may not contain the reserved '__private' segment", @@ -284,6 +277,7 @@ def _expand_one_import( source_diagnostics=context.source_diagnostics, source_ranges=source_ranges, ) + _reject_removed_scoring_sections(imported_raw, path=import_path) try: Scenario.model_validate(imported_raw) except ValidationError as exc: @@ -334,7 +328,10 @@ def _expand_one_import( context.budget.check_namespaces(namespaced_payload, path=import_path) merged = _merge_sections(merged, namespaced_payload, path=import_path) - return (merged, *_import_provenance_additions(resolved_import, import_decl, bound, inner_provenance, symbols)) + additions = _import_provenance_additions( + resolved_import, import_decl, bound, inner_provenance, symbols, path=context.path + ) + return (merged, *additions) def expand_sdl_modules( @@ -413,9 +410,11 @@ def expand_sdl_modules( semantic_revision=data.get("semantic_revision"), ) - for raw_import in merged.get("imports", []): + # ADR-053 steps 1, 3 and 4: the policy files are loaded, then every declaration + # is validated as the typed field before the first import resolves. + for import_decl in _import_declarations(merged, path=path, source_ranges={}): merged, import_add, capability_add, derivation_add, explicitness_add, realization_add, constraint_add = ( - _expand_one_import(raw_import, merged, context) + _expand_one_import(import_decl, merged, context) ) import_records.extend(import_add) capability_constraints.extend(capability_add) diff --git a/implementations/python/packages/raes/composition/_provenance.py b/implementations/python/packages/raes/composition/_provenance.py index 15966e66f..aa09b489d 100644 --- a/implementations/python/packages/raes/composition/_provenance.py +++ b/implementations/python/packages/raes/composition/_provenance.py @@ -2,6 +2,8 @@ from __future__ import annotations +from pathlib import Path + from .._composition_provenance import ( prefixed_constraint as _prefixed_constraint, ) @@ -41,6 +43,8 @@ def import_provenance_additions( bound: _BoundScenarioResult, inner_provenance: ExpansionProvenance, symbols: dict[str, dict[str, str] | set[str]], + *, + path: Path, ) -> tuple[ list[ResolvedImportProvenance], list[CapabilityConstraint], @@ -49,11 +53,11 @@ def import_provenance_additions( list[RealizationDesignationRecord], list[RealizationConstraintRecord], ]: - """Build the namespaced provenance additions contributed by one import.""" + """Build the namespaced provenance additions contributed by one import declared in ``path``.""" namespace = import_decl.namespace import_records: list[ResolvedImportProvenance] = [ - _resolved_import_record(resolved_import, requested=import_decl, bindings=bound) + _resolved_import_record(resolved_import, requested=import_decl, bindings=bound, path=path) ] import_records.extend(_prefixed_import_record(record, namespace) for record in inner_provenance.imports) capability_constraints = [ diff --git a/implementations/python/packages/raes/module_registry/__init__.py b/implementations/python/packages/raes/module_registry/__init__.py index 0bfd92f24..d147f6325 100644 --- a/implementations/python/packages/raes/module_registry/__init__.py +++ b/implementations/python/packages/raes/module_registry/__init__.py @@ -85,6 +85,7 @@ _same_file_identity, _write_version_pointer, ) +from ._lock_records import resolve_lock_records from ._verified_sources import _cache_source_result, _VerifiedSourceBundle from .models import ( Lockfile, @@ -97,7 +98,7 @@ write_lockfile, ) from .publishing import publish_module_to_oci_layout -from .resolution import resolve_import, resolve_lock_records +from .resolution import resolve_import from .signing import _signable_payload, _verify_signatures _OCI_LIMITS = _OCIResourceLimits() diff --git a/implementations/python/packages/raes/module_registry/_lock_records.py b/implementations/python/packages/raes/module_registry/_lock_records.py new file mode 100644 index 000000000..fa1882c64 --- /dev/null +++ b/implementations/python/packages/raes/module_registry/_lock_records.py @@ -0,0 +1,54 @@ +"""Lockfile record resolution for an SDL root's import declarations.""" + +from __future__ import annotations + +from pathlib import Path + +from .._errors import SDLSourceRange +from .._model_diagnostics import _import_declarations +from .models import Lockfile, LockRecord, TrustPolicy, load_trust_policy +from .resolution import resolve_import + + +def resolve_lock_records( + root_path: Path, + *, + trust_policy: TrustPolicy | None = None, +) -> Lockfile: + """Resolve the root's imports into lock records. + + The declarations and the provenance each record implies are checked as + ``parse_sdl_file`` checks them, so a root it rejects for either reason + never yields a lockfile. + """ + + from .._composition_provenance import _provenance_record + from ..parser import _load_normalized_data, read_sdl_source + + trust_policy = trust_policy or load_trust_policy(root_path.parent) + source_ranges: dict[str, SDLSourceRange] = {} + root_data = _load_normalized_data(read_sdl_source(root_path).text, path=root_path, source_ranges=source_ranges) + imports = _import_declarations(root_data, path=root_path, source_ranges=source_ranges) + records: list[LockRecord] = [] + for import_decl in imports: + resolved = resolve_import( + import_decl, + base_dir=root_path.parent, + trust_policy=trust_policy, + ) + _provenance_record(resolved, requested=import_decl, path=root_path) + records.append( + LockRecord( + source=import_decl.normalized_source, + namespace=import_decl.namespace, + requested_version=import_decl.version or "*", + resolved_source=resolved.resolved_source, + module_id=resolved.module_descriptor.id, + module_version=resolved.module_descriptor.version, + manifest_digest=resolved.manifest_digest, + content_digest=resolved.content_digest, + export_hash=resolved.export_hash, + signer_id=resolved.signer_id, + ) + ) + return Lockfile(imports=records) diff --git a/implementations/python/packages/raes/module_registry/models.py b/implementations/python/packages/raes/module_registry/models.py index 0bf4ca489..ebfbbd961 100644 --- a/implementations/python/packages/raes/module_registry/models.py +++ b/implementations/python/packages/raes/module_registry/models.py @@ -8,10 +8,11 @@ from typing import TYPE_CHECKING import yaml -from pydantic import Field +from pydantic import Field, ValidationError from .._base import SDLModel from .._errors import SDLParseError +from .._model_diagnostics import _model_parse_error from ..scenario import ImportDecl, ModuleDescriptor, Scenario from ._constants import ( LOCKFILE_NAME, @@ -78,19 +79,48 @@ def _scenario_module_descriptor(scenario: Scenario, *, source_id: str) -> Module ) +def _read_policy_file(path: Path) -> str: + """Read a lockfile or trust policy, failing closed without OS error text.""" + + try: + return path.read_text(encoding="utf-8") + except (OSError, UnicodeDecodeError) as exc: + raise SDLParseError(f"{path.name} could not be read as a UTF-8 file", path=path) from exc + + +def _policy_model_error(error: ValidationError, *, path: Path) -> SDLParseError: + """Render a policy-file model failure through the bounded SDL envelope, naming the file.""" + + rendered = _model_parse_error(error, path=path, source_ranges={}) + return SDLParseError(f"{path.name}: {rendered.details}", path=path, diagnostics=rendered.diagnostics) + + def load_trust_policy(base_dir: Path) -> TrustPolicy: path = base_dir / TRUST_POLICY_NAME if not path.exists(): return TrustPolicy() - payload = yaml.safe_load(path.read_text(encoding="utf-8")) or {} - return TrustPolicy.model_validate(payload) + text = _read_policy_file(path) + try: + payload = yaml.safe_load(text) or {} + except yaml.YAMLError as exc: + mark = getattr(exc, "problem_mark", None) + where = f" at line {mark.line + 1}, column {mark.column + 1}" if mark is not None else "" + raise SDLParseError(f"{path.name} is not valid YAML{where}", path=path) from exc + try: + return TrustPolicy.model_validate(payload) + except ValidationError as exc: + raise _policy_model_error(exc, path=path) from exc def load_lockfile(base_dir: Path) -> Lockfile | None: path = base_dir / LOCKFILE_NAME if not path.exists(): return None - return Lockfile.model_validate_json(path.read_text(encoding="utf-8")) + text = _read_policy_file(path) + try: + return Lockfile.model_validate_json(text) + except ValidationError as exc: + raise _policy_model_error(exc, path=path) from exc def write_lockfile(base_dir: Path, lockfile: Lockfile) -> Path: diff --git a/implementations/python/packages/raes/module_registry/resolution.py b/implementations/python/packages/raes/module_registry/resolution.py index dda7507a3..f044f1d4f 100644 --- a/implementations/python/packages/raes/module_registry/resolution.py +++ b/implementations/python/packages/raes/module_registry/resolution.py @@ -4,27 +4,23 @@ from dataclasses import dataclass from pathlib import Path -from typing import Any, TypedDict, Unpack +from typing import TYPE_CHECKING, Any, TypedDict, Unpack from urllib.parse import quote from packaging.version import InvalidVersion, Version from pydantic import ValidationError from .._errors import SDLParseDiagnostic, SDLParseError, SDLSourceRange -from .._model_diagnostics import _model_parse_error +from .._model_diagnostics import _field_problems, _model_parse_error from .._source_profile import DEFAULT_SOURCE_PARSE_OPTIONS, SDLSourceParseOptions from ..scenario import ImportDecl, ModuleDescriptor, Scenario from ._constants import LOCKFILE_NAME, OCI_BUNDLE_MEDIA_TYPE, OCI_LAYOUT_MEDIA_TYPE from ._digests import _SHA256_PREFIX, _descriptor_digest, _normalize_exact_or_range, _satisfies_version from ._verified_sources import _local_resolved_source, _VerifiedSourceBundle -from .models import ( - Lockfile, - LockRecord, - ResolvedModule, - TrustPolicy, - _scenario_module_descriptor, - load_trust_policy, -) +from .models import Lockfile, LockRecord, ResolvedModule, TrustPolicy, _scenario_module_descriptor + +if TYPE_CHECKING: + from ..parser import SDLSourceDocument # The private digest/signature seams (``_sha256_digest``, ``_json_request``, # ``_bytes_request``, ``_extract_bundle_to_cache``, ``_verify_signatures``, @@ -34,6 +30,9 @@ # production calls use, exactly as the pre-split single-file module did. +_LOCKED_PREFIX = "locked:" + + @dataclass(frozen=True) class _ResolutionContext: """Invariant options shared by locked, local, and OCI resolution.""" @@ -161,7 +160,7 @@ def resolve_import( def _resolve_import_with_context(import_decl: ImportDecl, context: _ResolutionContext) -> ResolvedModule: source = import_decl.normalized_source - if source.startswith("locked:"): + if source.startswith(_LOCKED_PREFIX): return _resolve_locked_import(import_decl, source, context=context) if source.startswith("local:"): return _resolve_local_import(import_decl, source, context=context) @@ -183,28 +182,63 @@ def _resolve_locked_import( *, context: _ResolutionContext, ) -> ResolvedModule: - locked_ref = source.removeprefix("locked:") lockfile = context.lockfile if lockfile is None: raise SDLParseError(f"Locked import '{source}' requires {LOCKFILE_NAME}") - record = next( - ( - candidate - for candidate in lockfile.imports - if candidate.resolved_source == locked_ref or candidate.source == locked_ref - ), - None, - ) - if record is None: - raise SDLParseError(f"Locked import '{source}' is not present in {LOCKFILE_NAME}") - delegated = ImportDecl( - source=record.source, - namespace=import_decl.namespace or record.namespace, - version=record.requested_version, - parameters=dict(import_decl.parameters), - digest=import_decl.digest or record.content_digest, - ) - return _resolve_import_with_context(delegated, context) + # Follow the record chain iteratively: each hop delegates exactly as one + # recursive call did, and a revisited ref is an import cycle (ADR-053 step 6). + seen: set[str] = set() + while source.startswith(_LOCKED_PREFIX): + locked_ref = source.removeprefix(_LOCKED_PREFIX) + if locked_ref in seen: + raise SDLParseError(f"Locked import '{source}' forms a cycle in {LOCKFILE_NAME}") + seen.add(locked_ref) + record = next( + (item for item in lockfile.imports if item.resolved_source == locked_ref or item.source == locked_ref), + None, + ) + if record is None: + raise SDLParseError(f"Locked import '{source}' is not present in {LOCKFILE_NAME}") + import_decl = _delegated_import(import_decl, record, source=source) + source = import_decl.normalized_source + return _resolve_import_with_context(import_decl, context) + + +_LOCK_RECORD_FIELDS = {"version": "requested_version", "digest": "content_digest"} + + +def _delegated_import(import_decl: ImportDecl, record: LockRecord, *, source: str) -> ImportDecl: + try: + return ImportDecl( + source=record.source, + namespace=import_decl.namespace or record.namespace, + version=record.requested_version, + parameters=dict(import_decl.parameters), + digest=import_decl.digest or record.content_digest, + ) + except ValidationError as exc: + problems = _field_problems(exc, field_names=_LOCK_RECORD_FIELDS) + raise SDLParseError( + f"Locked import '{source}' uses an invalid {LOCKFILE_NAME} record for source '{record.source}': {problems}" + ) from exc + + +def _local_import_source(relative: str, context: _ResolutionContext) -> tuple[Path, SDLSourceDocument]: + from ..parser import read_sdl_source + + if context.verified_sources is not None: + return context.verified_sources.resolve_local(base_dir=context.base_dir, relative=relative) + import_path = (context.base_dir / relative).resolve() + if not import_path.is_relative_to(context.base_dir.resolve()): + raise SDLParseError(f"Local import path escapes base directory: {relative!r}") + if not import_path.exists(): + raise SDLParseError(f"Imported SDL file not found: {relative}") + if not import_path.is_file(): + raise SDLParseError(f"Imported SDL source is not a regular file: {relative}") + try: + return import_path, read_sdl_source(import_path, limits=context.source_options.limits) + except OSError as exc: + raise SDLParseError(f"Imported SDL file could not be read: {relative}") from exc def _resolve_local_import( @@ -213,22 +247,11 @@ def _resolve_local_import( *, context: _ResolutionContext, ) -> ResolvedModule: - from ..parser import _load_normalized_data, read_sdl_source + from ..parser import _load_normalized_data, _reject_removed_scoring_sections from . import _sha256_digest relative = source.removeprefix("local:") - if context.verified_sources is None: - import_path = (context.base_dir / relative).resolve() - if not import_path.is_relative_to(context.base_dir.resolve()): - raise SDLParseError(f"Local import path escapes base directory: {relative!r}") - if not import_path.exists(): - raise SDLParseError(f"Imported SDL file not found: {relative}") - imported_source = read_sdl_source(import_path, limits=context.source_options.limits) - else: - import_path, imported_source = context.verified_sources.resolve_local( - base_dir=context.base_dir, - relative=relative, - ) + import_path, imported_source = _local_import_source(relative, context) source_ranges: dict[str, SDLSourceRange] = {} imported_raw = _load_normalized_data( imported_source.text, @@ -237,6 +260,7 @@ def _resolve_local_import( source_diagnostics=context.source_diagnostics, source_ranges=source_ranges, ) + _reject_removed_scoring_sections(imported_raw, path=import_path) try: imported_scenario = Scenario.model_validate(imported_raw) except ValidationError as exc: @@ -456,37 +480,3 @@ def _resolve_oci_import( signer_id=signer_id, verified_sources=verified_sources, ) - - -def resolve_lock_records( - root_path: Path, - *, - trust_policy: TrustPolicy | None = None, -) -> Lockfile: - from ..parser import _load_normalized_data, read_sdl_source - - trust_policy = trust_policy or load_trust_policy(root_path.parent) - root_data = _load_normalized_data(read_sdl_source(root_path).text, path=root_path) - imports = [ImportDecl.model_validate(item) for item in root_data.get("imports", [])] - records: list[LockRecord] = [] - for import_decl in imports: - resolved = resolve_import( - import_decl, - base_dir=root_path.parent, - trust_policy=trust_policy, - ) - records.append( - LockRecord( - source=import_decl.normalized_source, - namespace=import_decl.namespace, - requested_version=import_decl.version or "*", - resolved_source=resolved.resolved_source, - module_id=resolved.module_descriptor.id, - module_version=resolved.module_descriptor.version, - manifest_digest=resolved.manifest_digest, - content_digest=resolved.content_digest, - export_hash=resolved.export_hash, - signer_id=resolved.signer_id, - ) - ) - return Lockfile(imports=records) diff --git a/implementations/python/packages/raes_cli/sdl.py b/implementations/python/packages/raes_cli/sdl.py index a4d0b1ee9..4ff479b88 100644 --- a/implementations/python/packages/raes_cli/sdl.py +++ b/implementations/python/packages/raes_cli/sdl.py @@ -64,13 +64,20 @@ def resolve( ), ) -> None: """Resolve SDL imports and write/update the lockfile.""" - resolved = resolve_lock_records(path) + try: + resolved = resolve_lock_records(path) + except SDLParseError as exc: + # The failure can sit in the trust policy or an imported unit, so keep the file it names. + raise typer.BadParameter(str(exc)) from exc output_path = lockfile or (path.parent / LOCKFILE_NAME) - output_path.parent.mkdir(parents=True, exist_ok=True) - output_path.write_text( - json.dumps(resolved.model_dump(mode="python"), indent=2, sort_keys=True) + "\n", - encoding="utf-8", - ) + try: + output_path.parent.mkdir(parents=True, exist_ok=True) + output_path.write_text( + json.dumps(resolved.model_dump(mode="python"), indent=2, sort_keys=True) + "\n", + encoding="utf-8", + ) + except OSError as exc: + raise typer.BadParameter(f"Lockfile could not be written: {output_path}") from exc typer.echo(str(output_path)) diff --git a/implementations/python/tests/test_issue_1580_import_boundary_diagnostics.py b/implementations/python/tests/test_issue_1580_import_boundary_diagnostics.py new file mode 100644 index 000000000..56a89c6e2 --- /dev/null +++ b/implementations/python/tests/test_issue_1580_import_boundary_diagnostics.py @@ -0,0 +1,391 @@ +"""Issue #1580: module import resolution fails as SDL diagnostics, never as raw exceptions. + +Invalid root import declarations, lock records, lockfiles, trust policies, +directory imports, removed scoring sections in imported units and provenance +bounds reach ``parse_sdl_file``, ``resolve_lock_records``, ``expand_sdl_modules`` +and ``raes sdl resolve`` through one ``SDLParseError`` envelope. Expected +diagnostics come from ``parse_sdl_file`` on the same root where possible. +""" + +from __future__ import annotations + +import dataclasses +import hashlib +import json +import re +import textwrap +from collections.abc import Callable +from pathlib import Path + +import pytest +import raes.composition._expand as composition_expand +import raes.parser as sdl_parser +from raes._errors import SDLParseError +from raes.composition import expand_sdl_modules +from raes.module_registry import LOCKFILE_NAME, LOCKFILE_SCHEMA_VERSION, TRUST_POLICY_NAME, resolve_lock_records +from raes.parser import SDLSourceDocument, parse_sdl, parse_sdl_file +from raes.scenario import ExpandedScenario +from raes_cli.main import app +from typer.testing import CliRunner + +MODULE = """\ +name: shared +version: 1.2.3 +module: + id: acme/shared + version: 1.2.3 + exports: + nodes: [vm] +nodes: + vm: + type: compute + os: linux + resources: {ram: 1 gib, cpu: 1} +""" +SHARED = "- source: local:shared.yaml\n namespace: shared\n" +SENTINEL = "SENTINEL-7d1f" +REMOVED_SCORING = "metrics: {}\n" +LONG_RANGE = ",".join([">=1.0", *(f"!=0.{index}" for index in range(48))]) + + +def _scenario(directory: Path, imports: str | None, files: dict[str, str | bytes | None] | None = None) -> Path: + """Write ``shared.yaml``, a root importing ``imports`` and extra files (``None`` makes a directory).""" + + (directory / "shared.yaml").write_text(MODULE, encoding="utf-8") + for name, content in (files or {}).items(): + target = directory / name + if content is None: + target.mkdir() + elif isinstance(content, bytes): + target.write_bytes(content) + else: + target.write_text(content, encoding="utf-8") + body = "imports: {}\n" if imports is None else "imports:\n" + textwrap.indent(imports, " ") + root = directory / "root.yaml" + root.write_text(f"name: root\n{body}", encoding="utf-8") + return root + + +def _raised(call: Callable[[], object]) -> SDLParseError: + with pytest.raises(SDLParseError) as caught: + call() + return caught.value + + +def _diagnostics(error: SDLParseError) -> list[tuple[object, ...]]: + return [(item.code, item.pointer, item.primary_range.as_dict(), item.message) for item in error.diagnostics] + + +def _adr_073_message() -> str: + return _raised(lambda: parse_sdl(f"name: root\n{REMOVED_SCORING}")).details + + +def _lock_record(**overrides: str) -> dict[str, str]: + record = { + "source": "local:shared.yaml", + "namespace": "shared", + "requested_version": "*", + "resolved_source": "shared.yaml", + "module_id": "acme/shared", + "module_version": "1.2.3", + "manifest_digest": "", + "content_digest": "", + "export_hash": "", + } + return record | overrides + + +def _lockfile(*records: dict[str, str]) -> str: + return json.dumps({"imports": list(records)}) + + +@pytest.mark.parametrize( + "imports", + [ + pytest.param(f"{SHARED} version: 1.0\n", id="number-version"), + pytest.param("- source: local:shared.yaml\n", id="no-namespace"), + pytest.param("- namespace: shared\n", id="no-source"), + pytest.param(f"{SHARED} path: shared.yaml\n", id="source-and-path"), + pytest.param("- source: local:shared.yaml\n namespace: Not An Id\n", id="bad-namespace"), + pytest.param(f"{SHARED} colour: red\n", id="unknown-field"), + pytest.param(f"{SHARED} parameters: [a]\n", id="parameters-list"), + pytest.param(f"{SHARED} version: '>=banana'\n", id="malformed-range"), + pytest.param(None, id="imports-mapping"), + ], +) +def test_resolve_reports_invalid_declarations_like_parse(tmp_path: Path, imports: str | None) -> None: + root = _scenario(tmp_path, imports) + + parsed = _raised(lambda: parse_sdl_file(root)) + resolved = _raised(lambda: resolve_lock_records(root)) + + assert parsed.diagnostics + assert all(item.pointer.startswith("/imports") for item in parsed.diagnostics) + assert _diagnostics(resolved) == _diagnostics(parsed) + assert resolved.path == parsed.path == root + + +def test_direct_expansion_reports_an_invalid_declaration_as_a_field_diagnostic(tmp_path: Path) -> None: + root = _scenario(tmp_path, SHARED) + data = {"name": "root", "imports": [{"source": "local:shared.yaml", "namespace": "shared", "version": 1.0}]} + + error = _raised(lambda: expand_sdl_modules(data, path=root)) + + assert [(item.code, item.pointer, item.primary_range.start.line) for item in error.diagnostics] == [ + ("sdl.model.invalid", "/imports/0/version", 1) + ] + assert error.path == root + + +@pytest.mark.parametrize( + ("record", "expected"), + [ + pytest.param( + _lock_record(requested_version=">=banana"), + "for source 'local:shared.yaml': requested_version: import version must be", + id="bad-requested-version", + ), + pytest.param( + _lock_record(source=""), + "for source '': Import requires either 'source' or deprecated 'path'", + id="blank-source", + ), + ], +) +def test_invalid_lock_record_names_the_lockfile_record_and_field( + tmp_path: Path, record: dict[str, str], expected: str +) -> None: + lockfile = _lockfile(record) + root = _scenario(tmp_path, "- source: locked:shared.yaml\n namespace: shared\n", {LOCKFILE_NAME: lockfile}) + + error = _raised(lambda: parse_sdl_file(root)) + + assert error.details.startswith(f"Locked import 'locked:shared.yaml' uses an invalid {LOCKFILE_NAME} record ") + assert expected in error.details + + +@pytest.mark.parametrize( + "records", + [ + pytest.param([_lock_record(source="locked:x", resolved_source="x")], id="self-cycle"), + pytest.param( + [ + _lock_record(source="locked:b", resolved_source="x"), + _lock_record(source="locked:x", resolved_source="b"), + ], + id="two-record-cycle", + ), + ], +) +def test_locked_import_cycles_are_typed_errors(tmp_path: Path, records: list[dict[str, str]]) -> None: + root = _scenario(tmp_path, "- source: locked:x\n namespace: shared\n", {LOCKFILE_NAME: _lockfile(*records)}) + + error = _raised(lambda: parse_sdl_file(root)) + + assert error.details.endswith(f"forms a cycle in {LOCKFILE_NAME}") + + +def test_acyclic_locked_chain_resolves_like_its_local_target(tmp_path: Path) -> None: + (tmp_path / "direct").mkdir() + (tmp_path / "chain").mkdir() + chain = _lockfile(_lock_record(source="locked:b", resolved_source="a"), _lock_record(resolved_source="b")) + direct_root = _scenario(tmp_path / "direct", SHARED) + locked_root = _scenario(tmp_path / "chain", "- source: locked:a\n namespace: shared\n", {LOCKFILE_NAME: chain}) + + direct = parse_sdl_file(direct_root) + locked = parse_sdl_file(locked_root) + + assert isinstance(locked, ExpandedScenario) + assert isinstance(direct, ExpandedScenario) + expected = direct.expansion_provenance.imports[0].model_dump(mode="python") | {"requested_source": "locked:a"} + assert locked.expansion_provenance.imports[0].model_dump(mode="python") == expected + + +POLICY_FILES = [ + pytest.param(LOCKFILE_NAME, '{"imports": [' + SENTINEL, id="lockfile-bad-json"), + pytest.param(LOCKFILE_NAME, json.dumps({"imports": SENTINEL}), id="lockfile-bad-shape"), + pytest.param(LOCKFILE_NAME, b"\xff" + SENTINEL.encode(), id="lockfile-not-utf8"), + pytest.param(LOCKFILE_NAME, None, id="lockfile-directory"), + pytest.param(TRUST_POLICY_NAME, f"registries: {SENTINEL}\n", id="trust-bad-shape"), + pytest.param(TRUST_POLICY_NAME, f"registries: [{SENTINEL}\n", id="trust-bad-yaml"), + pytest.param(TRUST_POLICY_NAME, f"registries: {SENTINEL}\x07\n", id="trust-control-character"), + pytest.param(TRUST_POLICY_NAME, b"\xff" + SENTINEL.encode(), id="trust-not-utf8"), + pytest.param(TRUST_POLICY_NAME, None, id="trust-directory"), +] + + +def _entry_points(name: str) -> list[Callable[[Path], object]]: + # resolve_lock_records never reads the lockfile, so only the trust policy reaches it. + return [parse_sdl_file] if name == LOCKFILE_NAME else [parse_sdl_file, resolve_lock_records] + + +@pytest.mark.parametrize(("name", "content"), POLICY_FILES) +def test_invalid_policy_files_are_typed_errors_naming_the_file( + tmp_path: Path, name: str, content: str | bytes | None +) -> None: + root = _scenario(tmp_path, SHARED, {name: content}) + + for entry in _entry_points(name): + error = _raised(lambda entry=entry: entry(root)) + + assert error.path == tmp_path / name + assert error.details.startswith(name) + rendered = [str(error), *(item.message for item in error.diagnostics)] + assert not any(SENTINEL in text for text in rendered) + + +@pytest.mark.parametrize( + ("imports", "module_version"), + [ + pytest.param(f"{SHARED} version: ''\n", "1.2.3", id="blank-import-version"), + pytest.param(f"{SHARED} version: '{LONG_RANGE}'\n", "1.2.3", id="long-import-range"), + pytest.param(SHARED, "''", id="blank-module-version"), + pytest.param(SHARED, f"'{'9' * 257}'", id="long-module-version"), + ], +) +def test_unrecordable_provenance_fails_alike_through_parse_and_resolve( + tmp_path: Path, imports: str, module_version: str +) -> None: + assert len(LONG_RANGE) > 256 + root = _scenario(tmp_path, imports) + (tmp_path / "shared.yaml").write_text(MODULE.replace(" version: 1.2.3", f" version: {module_version}")) + + parsed = _raised(lambda: parse_sdl_file(root)) + resolved = _raised(lambda: resolve_lock_records(root)) + + assert parsed.details.startswith("Import 'local:shared.yaml' cannot be recorded as resolved import provenance: ") + assert (resolved.details, resolved.path) == (parsed.details, parsed.path) + assert parsed.path == root + + +@pytest.mark.parametrize("entry", [parse_sdl_file, resolve_lock_records]) +def test_directory_import_is_a_typed_error_naming_the_import(tmp_path: Path, entry: Callable[[Path], object]) -> None: + root = _scenario(tmp_path, "- source: local:unit\n namespace: shared\n", {"unit": None}) + + error = _raised(lambda: entry(root)) + + assert error.details == "Imported SDL source is not a regular file: unit" + + +@pytest.mark.parametrize("entry", [parse_sdl_file, resolve_lock_records]) +def test_unreadable_import_is_a_typed_error_naming_the_import( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch, entry: Callable[[Path], object] +) -> None: + root = _scenario(tmp_path, SHARED) + real_read = sdl_parser.read_sdl_source + + def denied(path: Path, **kwargs: object) -> SDLSourceDocument: + if path.name == "shared.yaml": + raise PermissionError(f"{SENTINEL}: permission denied") + return real_read(path, **kwargs) + + monkeypatch.setattr(sdl_parser, "read_sdl_source", denied) + error = _raised(lambda: entry(root)) + + assert error.details == "Imported SDL file could not be read: shared.yaml" + + +def test_imported_unit_with_removed_scoring_gets_the_root_migration_message(tmp_path: Path) -> None: + root = _scenario(tmp_path, SHARED) + (tmp_path / "shared.yaml").write_text(MODULE + REMOVED_SCORING, encoding="utf-8") + + error = _raised(lambda: parse_sdl_file(root)) + + assert error.details == _adr_073_message() + assert error.path == tmp_path / "shared.yaml" + + +def test_unvalidated_resolver_unit_with_removed_scoring_gets_the_migration_message( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + # OCI resolution returns the unit's verified bytes without typed validation; + # expansion is then the first place that reads the unit's sections. + root = _scenario(tmp_path, SHARED) + real_resolve_import = composition_expand.resolve_import + text = MODULE + REMOVED_SCORING + + def unvalidated(*args: object, **kwargs: object) -> object: + resolved = real_resolve_import(*args, **kwargs) + document = SDLSourceDocument(raw_bytes=text.encode("utf-8"), text=text) + return dataclasses.replace(resolved, source_document=document) + + monkeypatch.setattr(composition_expand, "resolve_import", unvalidated) + error = _raised(lambda: parse_sdl_file(root)) + + assert error.details == _adr_073_message() + + +def _compact(text: str) -> str: + return "".join(text.split()) + + +def _cli_output(arguments: list[str]) -> tuple[int, str]: + """Return the exit code and the output without styling, panel borders or whitespace. + + Rich wraps and folds the error panel at the terminal width, so long paths + can break anywhere; callers compare whitespace-free fragments. + """ + + result = CliRunner().invoke(app, arguments) + return result.exit_code, _compact(re.sub(r"\x1b\[[0-9;]*m", "", result.output).replace("│", " ")) + + +@pytest.mark.parametrize( + ("imports", "files", "expected"), + [ + pytest.param(f"{SHARED} version: 1.0\n", {}, ["root.yaml", "/imports/0/version"], id="declaration"), + pytest.param(SHARED, {TRUST_POLICY_NAME: "registries: [1]\n"}, [TRUST_POLICY_NAME, "/registries"], id="trust"), + pytest.param( + f"{SHARED} version: ''\n", + {}, + ["root.yaml: Import 'local:shared.yaml' cannot be recorded as resolved import provenance"], + id="provenance", + ), + pytest.param( + "- source: local:mod.yaml\n namespace: shared\n", + {"mod.yaml": MODULE + REMOVED_SCORING}, + ["mod.yaml", "removed from the language by ADR-073"], + id="imported-unit", + ), + pytest.param( + SHARED, {LOCKFILE_NAME: None}, ["Lockfile could not be written", LOCKFILE_NAME], id="lockfile-directory" + ), + ], +) +def test_raes_sdl_resolve_reports_each_failure_without_a_traceback( + tmp_path: Path, monkeypatch: pytest.MonkeyPatch, imports: str, files: dict[str, str], expected: list[str] +) -> None: + _scenario(tmp_path, imports, files) + monkeypatch.chdir(tmp_path) + + exit_code, output = _cli_output(["sdl", "resolve", "root.yaml"]) + + assert exit_code != 0 + assert "Traceback" not in output + assert all(_compact(fragment) in output for fragment in expected), output + assert "input_value" not in output + assert not (tmp_path / LOCKFILE_NAME).is_file() + + +def test_valid_root_keeps_a_byte_identical_lockfile_and_parse_result(tmp_path: Path) -> None: + root = _scenario(tmp_path, SHARED) + content_digest = "sha256:" + hashlib.sha256(MODULE.encode("utf-8")).hexdigest() + export_hash = hashlib.sha256(b'{"nodes":["vm"]}').hexdigest() + record = _lock_record(content_digest=content_digest, export_hash=export_hash) | {"signer_id": ""} + lockfile = {"imports": [record], "schema_version": LOCKFILE_SCHEMA_VERSION} + expected = json.dumps(lockfile, indent=2, sort_keys=True) + "\n" + + exit_code, output = _cli_output(["sdl", "resolve", str(root)]) + scenario = parse_sdl_file(root) + (tmp_path / "plain.yaml").write_text("name: plain\n", encoding="utf-8") + assert resolve_lock_records(tmp_path / "plain.yaml").imports == [] + + assert exit_code == 0, output + assert (tmp_path / LOCKFILE_NAME).read_text(encoding="utf-8") == expected + assert isinstance(scenario, ExpandedScenario) + provenance = scenario.expansion_provenance.imports[0] + assert (provenance.requested_source, provenance.module_version, provenance.content_digest) == ( + "local:shared.yaml", + "1.2.3", + content_digest, + ) From a7a4ca9063c15a0ed4fd8130800615157525ab5f Mon Sep 17 00:00:00 2001 From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com> Date: Tue, 13 Oct 2026 05:44:50 +0000 Subject: [PATCH 2/2] chore(research): record research captures for issue #1580 --- ...6357bf41d90b8e922dccc987471cc54da1b48.json | 4 + .../analysis.json | 171 +++++ .../manifest.json | 122 +++ .../snapshot.json | 652 ++++++++++++++++ ...033526eb339f0f87ad8ce60f5f9dd31b414cf.json | 4 + .../analysis.json | 118 +++ .../manifest.json | 10 + .../snapshot.json | 708 ++++++++++++++++++ 8 files changed, 1789 insertions(+) create mode 100644 docs/research/formal-semantic-validation/capture-records/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48.json create mode 100644 docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/analysis.json create mode 100644 docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/manifest.json create mode 100644 docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/snapshot.json create mode 100644 docs/research/specification-coverage/capture-records/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf.json create mode 100644 docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/analysis.json create mode 100644 docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/manifest.json create mode 100644 docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/snapshot.json diff --git a/docs/research/formal-semantic-validation/capture-records/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48.json b/docs/research/formal-semantic-validation/capture-records/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48.json new file mode 100644 index 000000000..b0789eec6 --- /dev/null +++ b/docs/research/formal-semantic-validation/capture-records/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48.json @@ -0,0 +1,4 @@ +{ + "capture_path": "docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/manifest.json", + "capture_sha256": "c70ba15a14a4231bc55158e8a494e5653d0aaf0f4fc5869f631727456daccd7a" +} diff --git a/docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/analysis.json b/docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/analysis.json new file mode 100644 index 000000000..9162a4d92 --- /dev/null +++ b/docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/analysis.json @@ -0,0 +1,171 @@ +{ + "analysis_id": "issue-1580-formal-analysis-f7b42a16eff6", + "claim": { + "allowed_evidence": [ + "production parser and semantic-validator results", + "canonical compiled digests", + "participant contract regression tests", + "pinned protocol, corpus, and execution snapshot" + ], + "claim_id": "asr-530-formal-semantic-validation-retest", + "disallowed_evidence": [ + "schema success as semantic proof", + "workflow reachability as network or exploit reachability", + "FM labels as gate outcomes", + "attribution as counterfactual proof", + "formal prose or maintainer confidence alone" + ], + "evidence_artifacts": [ + "docs/research/formal-semantic-validation/protocol-v2.json", + "docs/research/formal-semantic-validation/corpus/manifest-v4.json", + "@snapshot", + "docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json", + "docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json", + "docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json", + "docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json" + ], + "falsification_protocol": "Replay every retained and new case through its production entrypoint, require complete digest and evidence joins, execute participant fixtures, and derive status from the recorded outcomes.", + "objective_fail_criteria": "A supported negative passes, a positive fails, an observation drifts, a required participant case is missing, or weaker evidence is promoted to solver, exploit-path, runtime-stability, or counterfactual assurance.", + "objective_pass_criteria": "Every claim class has positive and negative cases, all supported cases reproduce the frozen outcome, every participant obligation has passing positive and negative fixtures, and unsupported classes remain untested.", + "statement": "At the recorded source-state digest, the retained RAES controls have the bounded statuses recorded here; historical releases are integrity evidence, not current replay evidence.", + "threats_to_validity": [ + "The issue-specific corpus is intentionally small and does not enumerate every validator invariant.", + "The participant fixtures exercise reference production contracts and tests, not every independent backend realization.", + "The replay gate runs on one Python reference configuration and one pinned RAES revision.", + "Unsupported solver-level classes have protocol cases but no executable observations." + ] + }, + "claim_results": [ + { + "case_count": 2, + "claim_class_id": "schema-validity", + "evidence_status": "demonstrated", + "limitations": [ + "Bounded to the named source/model structural controls." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 0 + }, + { + "case_count": 4, + "claim_class_id": "semantic-consistency", + "evidence_status": "partial", + "limitations": [ + "Partial coverage of named static semantics and participant obligations, not universal consistency." + ], + "matching_case_count": 4, + "participant_obligation_count": 7, + "replayable_case_count": 4, + "unsupported_case_count": 0 + }, + { + "case_count": 2, + "claim_class_id": "graph-reachability", + "evidence_status": "partial", + "limitations": [ + "Partial workflow control-flow reachability only; not network, service, or exploit reachability." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 0 + }, + { + "case_count": 4, + "claim_class_id": "constraint-satisfiability", + "evidence_status": "demonstrated", + "limitations": [ + "Demonstrated only for raes-finite-domain-satisfiability-v1 and its pinned solver configuration." + ], + "matching_case_count": 4, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 2 + }, + { + "case_count": 4, + "claim_class_id": "exploit-path-validity", + "evidence_status": "demonstrated", + "limitations": [ + "Demonstrated only for the admitted snapshot, typed graph, query, semantics, and bounded search profile." + ], + "matching_case_count": 4, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 2 + }, + { + "case_count": 2, + "claim_class_id": "determinism-stability", + "evidence_status": "partial", + "limitations": [ + "Partial parse-to-compile repeatability only; runtime and backend determinism are untested." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 2, + "unsupported_case_count": 0 + }, + { + "case_count": 2, + "claim_class_id": "counterfactual-necessity", + "evidence_status": "untested", + "limitations": [ + "Untested because no governed intervention or ablation entrypoint ran." + ], + "matching_case_count": 2, + "participant_obligation_count": 0, + "replayable_case_count": 0, + "unsupported_case_count": 2 + } + ], + "corpus_revision": "4.0.0", + "evidence_status": "partial", + "execution_id": "issue-1580-formal-f7b42a16eff6", + "generated_at": "2026-10-13T05:44:37.947232+00:00", + "limitations": [ + "Satisfiability is limited to raes-finite-domain-satisfiability-v1 and its exact translation, theory, and Z3 configuration.", + "The subset-minimal unsatisfiable core is not a universal proof certificate.", + "Exploit-path results are limited to the admitted snapshot, normalized graph, query, transition semantics, and bounded search profile.", + "A valid path is not backend execution and an invalid path is not real-world non-exploitability.", + "The production exploit-path JSON loader permits duplicate keys; the research loader rejects them without claiming stronger production behavior.", + "Participant replay inherits the host environment and is not described as hermetic.", + "Counterfactual necessity remains untested.", + "Scoped observation demand is not a claim class in this preregistration and is not promoted to demonstrated by this retest.", + "EXP-732 provenance joins are verified by their dedicated regression suite; this retained corpus makes no universal run, apparatus, source, or augmentation assurance claim.", + "This retained corpus does not establish native backend attestation fidelity; materialization contract checks remain separate operational provenance, not experimental observations.", + "Capture admission and evidence-proof authority are verified by issue-1237 regression tests, not promoted to a new claim class by this retained corpus.", + "Evidence-requirement refinement lineage is outside this retained formal claim set; this retest refreshes integrated source provenance without promoting that feature to a formal claim.", + "Authoring-adapter transport behavior is outside this retained formal claim set.", + "Operational recovery observation and startup reconciliation are verified by their API-404 regression suite, not promoted to a new formal claim class by this retained corpus.", + "Single-owner store admission, immutable target/run scope, and provider shutdown ordering are verified by their API-404 CP-5 regression suite, not promoted to a formal claim by this retained corpus.", + "Mixed and staged trial admission is verified by its SEM-234/SCE-002/API-407 regression suite, not promoted to a new formal claim class by this retained corpus.", + "Offline control-plane maintenance, readiness, and bounded audit behavior are verified by issue #1186 runtime tests, not promoted to a formal claim by this retained corpus.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 profile declarations and capability admission are covered by dedicated runtime tests; the retained formal corpus does not execute control-plane profile composition.", + "Issue #1016 mixed-runtime coordination is covered by dedicated runtime tests; the retained formal corpus does not establish backend-native mixed realization, multi-controller coordination, IFC, or equivalence.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Issue #1389 temporal-subject admission is verified by dedicated compiler tests and adds no new formal-semantic claim to this retained corpus.", + "Issue #971 model construction is verified by its own tests; this retained corpus establishes no participant-crossing equivalence or runtime-realization claim.", + "Issue #1359 control-plane route authority, participant-view scoping, and no-store HTTP boundary are verified by their dedicated HTTP-boundary suite and add no new formal-semantic claim to this retained corpus.", + "Issue #1401 required-evidence media-type coherence is verified by its dedicated suite and adds no new formal-semantic claim to this retained corpus.", + "Issue #1361 execution and recovery requirements are verified by dedicated policy, composition, and admission tests; this retained corpus establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 maintainability repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 resource type-hint repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The combined issue #1361 execution-policy and hatchling update preserves retained outcomes and bounded claims; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1418 runtime-fact export manifest split changes no contract, schema or behavior and adds no new formal-semantic claim.", + "The issue #1423 inject trigger request and occurrence contracts are new draft carriers that no SDL construct, compiler or runtime path reads, and they add no new formal-semantic claim.", + "The issue #1366 inject readback, correlation and backend declaration contracts are new draft carriers; the shared backend allowlist also lets SDL participant behavior specifications cite inject-occurrence-v1 and inject-occurrence-outcome-v1 as evidence_contract_refs, which the compiler copies through uninterpreted, and no runtime path or shipped backend reads or declares them; they add no new formal-semantic claim.", + "This synchronization preserves the original inject baseline chain in the pre-sync archive, retains frozen production and participant evidence, and binds the combined contract source. CI independently verifies current evidence replay; no new runtime adoption is claimed.", + "This second synchronization binds behavior-authoring source from issue #297, retains frozen production and participant evidence, and pins the preserved first-sync release 75 as its baseline. CI independently verifies replay; no new runtime adoption is claimed.", + "Issue #1091 request-boundary admission is verified by its dedicated tests; this retained corpus does not execute the served HTTP adapter or broaden its bounded claims.", + "This combined-source capture replays the supported retained corpus and the 18 declared participant test cases. The inject contract repair has 126 passing request, occurrence and readback tests; no runtime inject execution or broader formal claim is established. CI independently verifies replay.", + "Issue #1425's updated branch derives reference and libvirt specs from published plan operations. This retained corpus makes no new realization, HTTP relay, or backend-honesty claim.", + "Issue #1580 module-import error-boundary diagnostics are covered by their dedicated parser, resolver and CLI suite; this retained matrix makes no new composition, trust or execution claim." + ], + "plain_language_outcome": "The retained formal controls reproduce their prior outcomes after issue #1580 changed how module import resolution reports invalid declarations, lock records, policy files and import provenance. Bounded claim limits are unchanged.", + "protocol_revision": "2.0.0" +} diff --git a/docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/manifest.json b/docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/manifest.json new file mode 100644 index 000000000..ab900caee --- /dev/null +++ b/docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/manifest.json @@ -0,0 +1,122 @@ +{ + "analysis_path": "docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/analysis.json", + "analysis_sha256": "09d9d1d62a3786e3f8dd3e1d3b013504213257be55474e04bea1da90dff7174c", + "artifacts": [ + { + "artifact_id": "finite-domain-satisfiable-v2-input", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/satisfiable-control.sdl.yaml", + "sha256": "0ca9eaba9dc47171f7a042dc6753faa6c820c65ee966538f9d65fac5342202e8" + }, + { + "artifact_id": "finite-domain-satisfiable-v2-evidence", + "kind": "production-evidence", + "path": "docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json", + "sha256": "554202313d678046958b5c028e2de26ff03c74895cfac552677eed74e8153add" + }, + { + "artifact_id": "finite-domain-unsatisfiable-v2-input", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/unsatisfiable-control.sdl.yaml", + "sha256": "cfef56a1f56d5f0db9da195377fd75694bdd0f0b92932fdb8fafcbd3f7baf6c5" + }, + { + "artifact_id": "finite-domain-unsatisfiable-v2-evidence", + "kind": "production-evidence", + "path": "docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json", + "sha256": "c972725ef64822a75a60380afc11f08eac25b7fe9b091d39b058b3c9f7c8031d" + }, + { + "artifact_id": "typed-exploit-path-valid-v2-input", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/exploit-path-valid-v3.json", + "sha256": "0afe635a63db5b6e6380ac70982fd61d09790745d51a10d670321304121e7c39" + }, + { + "artifact_id": "typed-exploit-path-valid-v2-evidence", + "kind": "production-evidence", + "path": "docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json", + "sha256": "1b7f55d04db172da32658187c64a88c13b5f4d565267ce2be7cb86a9d04cb70c" + }, + { + "artifact_id": "typed-exploit-path-invalid-v2-input", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/exploit-path-invalid-v3.json", + "sha256": "0b2293d4a8983515ff05c516be6e6b418a4f3f09e055250a00bf15fda861aab3" + }, + { + "artifact_id": "typed-exploit-path-invalid-v2-evidence", + "kind": "production-evidence", + "path": "docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json", + "sha256": "244f895a64f14c10916ab0533ab462ce80a328021cd6a50c30a4aa59266d5533" + }, + { + "artifact_id": "schema-valid-control-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/schema-valid.sdl.yaml", + "sha256": "41a9adffdf9f5f2ccc2f887dcf7b15fba3b47c83a1af15f33db872c4a2449d67" + }, + { + "artifact_id": "schema-unknown-field-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/schema-invalid-unknown-field.sdl.yaml", + "sha256": "51cf62319a86c95a2517995939d1f370573051835e4b55bb6d5beaf049640481" + }, + { + "artifact_id": "semantic-resolved-objective-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/semantic-valid-participant-identity-v2.sdl.yaml", + "sha256": "75834bdc883e2003e1c473870bdf75700978955bb83095c6bd718ba6bd3908a6" + }, + { + "artifact_id": "semantic-dangling-assertion-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/semantic-invalid-dangling-ref-participant-identity-v2.sdl.yaml", + "sha256": "1d25bee5f556054e5f0a518df025e4c62e080e1964035e3c1a12e074d88d3a5d" + }, + { + "artifact_id": "semantic-ambiguous-reference-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/semantic-invalid-ambiguous-ref.sdl.yaml", + "sha256": "653cbd2fd62e220d49fb86f80133884207df5ae6752846345ae3085b93f6e4ed" + }, + { + "artifact_id": "semantic-feature-cycle-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/semantic-invalid-feature-cycle.sdl.yaml", + "sha256": "e1f66d95a9ad039687aec8cccbc8843b514072ff08e006c1b4ca6aa5cd8d4ed1" + }, + { + "artifact_id": "workflow-reachable-control-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/workflow-reachable.sdl.yaml", + "sha256": "54c40ceb98ad47247447d737973b2c55e8fb2045e209c7545c4fb20cf42dc3dc" + }, + { + "artifact_id": "workflow-unreachable-step-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/workflow-unreachable.sdl.yaml", + "sha256": "ef22ef2e260f1a7fd92d286f9b571716436b192ddfd54aea7bdfcfdda4ca52a2" + }, + { + "artifact_id": "compile-repeatability-control-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/determinism-a.sdl.yaml", + "sha256": "0bc40900d598c1af7a405d798ca19710405e53ced262d8733081abf12edf89fe" + }, + { + "artifact_id": "compile-non-vacuity-control-comparison-fixture", + "kind": "corpus-input", + "path": "docs/research/formal-semantic-validation/corpus/determinism-b.sdl.yaml", + "sha256": "d85338f89f20a45515b12da8640173c1a52e47eb17ca0f4f6b4f8f3306e863a1" + } + ], + "bundle_id": "raes-formal-semantic-validation", + "corpus_path": "docs/research/formal-semantic-validation/corpus/manifest-v4.json", + "corpus_sha256": "c57207af72406aa4f70882b9bbeb7cedcc79cf3854c878a95e3eb1fa59ea7a72", + "protocol_path": "docs/research/formal-semantic-validation/protocol-v2.json", + "protocol_sha256": "abf94093e344bf495dfb04e8b0c5985c0beaab8ebb17a75e15c8674fa81b1a7c", + "revision": "capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48", + "snapshot_path": "docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/snapshot.json", + "snapshot_sha256": "0ea3d52888f4cab4674953ca2497e64e8e2b58d44c3c48d0eb91fb4162340a32" +} diff --git a/docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/snapshot.json b/docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/snapshot.json new file mode 100644 index 000000000..0288ea27e --- /dev/null +++ b/docs/research/formal-semantic-validation/captures/capture-526d5758842365111e8db88fd6c6357bf41d90b8e922dccc987471cc54da1b48/snapshot.json @@ -0,0 +1,652 @@ +{ + "baseline": { + "execution_id": "issue-1425-combined-formal-51496af2b628", + "release_path": "docs/research/formal-semantic-validation/captures/capture-2df4b6bd919dca53c37e0aef9766e5ff1333a235cf4a8f0050b47a74121088a2/manifest.json", + "release_revision": "capture-2df4b6bd919dca53c37e0aef9766e5ff1333a235cf4a8f0050b47a74121088a2", + "release_sha256": "c271782cf5baa098d7a55954b4989fcdab9c073df76a39bd7c5ac1296363a61a" + }, + "captured_at": "2026-10-13T05:44:37.947232+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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "limitations": [ + "The witness ends at compiled output." + ], + "replayable": true, + "result_digest": "d7c098c5d063b8d1b0747e8df5daa90061456065cdda0bbedfa10918442f5daa", + "source_digest": null + }, + { + "actual_outcome": "distinguishable", + "analysis_profile": null, + "case_id": "compile-non-vacuity-control", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/research/formal-semantic-validation/corpus/determinism-a.sdl.yaml", + "docs/research/formal-semantic-validation/corpus/determinism-b.sdl.yaml" + ], + "execution_id": "issue-1580-formal-f7b42a16eff6", + "limitations": [ + "Distinct digests are a non-vacuity control, not semantic non-equivalence proof." + ], + "replayable": true, + "result_digest": "a2fcebba3341592b133af813e8bb8e5f47270418bc58bfd471a89bfbc8ba46da", + "source_digest": null + }, + { + "actual_outcome": "unsupported", + "analysis_profile": null, + "case_id": "necessity-witness-request", + "configuration_digest": null, + "configuration_id": "raes-python-reference-offline-v41", + "diagnostic_kind": null, + "evidence_artifact_path": null, + "evidence_artifact_sha256": null, + "evidence_digest": null, + "evidence_profile": null, + "evidence_refs": [ + "docs/decisions/issue-168-formal-semantic-validation-reachability-preflight.md" + ], + "execution_id": "issue-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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-1580-formal-f7b42a16eff6", + "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": "4dbccc6fdd1e4e68a45184d521a15909ff9123db", + "source_state": { + "base_revision": "4dbccc6fdd1e4e68a45184d521a15909ff9123db", + "checkout_state": "clean", + "implementation_digest": "f7b42a16eff6ab3d606d82f4b45332ffba7c136579a41e897e9ff388e9e16e8a", + "profile": "python-reference-source/v2" + }, + "versions": { + "python": "3.12.3", + "raes": "5.0.0", + "z3_engine": "4.16.0", + "z3_solver": "4.16.0.0" + } +} diff --git a/docs/research/specification-coverage/capture-records/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf.json b/docs/research/specification-coverage/capture-records/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf.json new file mode 100644 index 000000000..c39310f60 --- /dev/null +++ b/docs/research/specification-coverage/capture-records/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf.json @@ -0,0 +1,4 @@ +{ + "capture_path": "docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/manifest.json", + "capture_sha256": "1b3f40095d53bd530b90da312f17baeee53735d16e7c36634c600b74d322c159" +} diff --git a/docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/analysis.json b/docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/analysis.json new file mode 100644 index 000000000..7f40bbce2 --- /dev/null +++ b/docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/analysis.json @@ -0,0 +1,118 @@ +{ + "analysis_id": "issue-1580-specification-analysis-f7b42a16eff6", + "backend_leakage": [], + "claim": { + "allowed_evidence": [ + "pinned source metadata and bounded paraphrases", + "production parser, semantic, instantiation, admission, compiler, contract, and profile results", + "exact artifact digests and typed pointers", + "documented missing-concept and backend-specific dispositions" + ], + "claim_id": "raes-standardized-configurable-specification-coverage", + "disallowed_evidence": [ + "field-count or schema breadth alone", + "the existing scenario stress corpus as the representative request corpus", + "free-form metadata as typed coverage", + "backend-private interpretation", + "post-hoc removal or repair of falsifying concepts" + ], + "evidence_artifacts": [ + "docs/research/specification-coverage/protocol-v1.json", + "@snapshot" + ], + "falsification_protocol": "docs/research/specification-coverage/protocol-v1.json", + "objective_fail_criteria": "A load-bearing concept is missing or lossy, an applicable stage fails, or backend vocabulary is required in core SDL while the result claims success.", + "objective_pass_criteria": "Every load-bearing concept passes at every owning stage, backend-specific mechanics stay outside core SDL, and no requested concept is silently lost.", + "statement": "RAES provides a standardized configurable portable specification surface for the preregistered representative cyber-agent evaluation environment requirements without backend vocabulary in core SDL.", + "threats_to_validity": [ + "The representative corpus contains four source strata and sixteen atomic concepts rather than every cyber-range requirement.", + "The reference processor and repository fixtures are not independent backend implementations.", + "No live range, simulator federation, or participant execution was part of this offline specification-coverage test." + ] + }, + "classification_counts": { + "deliberately-backend-specific": 1, + "directly-expressible": 10, + "missing": 3, + "profile-or-manifest-constraint": 2 + }, + "evidence_status": "partial", + "execution_status": "complete", + "generated_at": "2026-10-13T05:44:37.947232+00:00", + "limitations": [ + "This result demonstrates bounded specification coverage, not universal cyber-range coverage, usability, adoption, backend substitution, or behavioral equivalence.", + "The three missing concepts are evidence, not implementation tasks within this snapshot.", + "The retained protocol does not test recursive realization or plan-level profile semantics; this release only re-establishes its original bounded coverage result against the current implementation.", + "The retained protocol does not test evidence-requirement refinement lineage; the dedicated EXP-731 regression suite covers that production boundary.", + "Authoring-adapter transport behavior is outside this retained protocol.", + "Reviewed OCI mirror and pre-seed admission is covered by its own regression suites and the development artifact policy gate, not a new claim in this preregistered matrix.", + "Operational recovery observation and startup reconciliation are covered by their API-404 regression suite, not a new claim in this preregistered matrix.", + "Store ownership, immutable runtime scope, and provider shutdown ordering are covered by the API-404 CP-5 regression suite, not by this retained specification-coverage protocol.", + "Mixed/staged trial compilation and admission are covered by issue #1015 regression tests, not by this retained specification-coverage corpus; no live mixed-runtime result is claimed.", + "Issue #1186 control-plane recovery operations are covered by their runtime regression suite, not by this retained specification-coverage corpus.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 control-plane profile declarations are covered by their dedicated runtime suite, not promoted to new claims by the retained language corpus.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Participant-local outcome state is verified by the ACT-618 tests; this retained corpus makes no additional outcome-state claim.", + "Backend operation supervision contracts are covered by issue #1360 contract tests; this retained offline corpus establishes no live backend supervision or recovery guarantee.", + "This capture replays the merged issue #1360 and #1357 source; the protocol makes no live backend execution or supervision claim.", + "This capture replays the merged issue #1360 and #1358 source; the protocol makes no live backend execution or supervision claim.", + "Issue #1389 participant inject delivery temporal-subject admission is covered by dedicated compiler tests; this retained matrix makes no new timing or execution claim.", + "Issue #971 adds offline crossing model construction; this retained protocol establishes no crossing equivalence or runtime-realization claim.", + "Issue #1359 control-plane route authority, participant-view scoping, and no-store HTTP boundary are covered by their dedicated HTTP-boundary suite; this retained matrix makes no new exposure or execution claim.", + "Issue #1401 required-evidence media-type coherence is verified by its dedicated suite; this retained matrix makes no new admission or capture claim.", + "Issue #1361 execution and recovery requirements are verified by dedicated policy, composition, and admission tests; this retained corpus establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 maintainability repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 resource type-hint repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The combined issue #1361 execution-policy and hatchling update preserves retained outcomes and bounded claims; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1418 runtime-fact export manifest split changes no contract, schema or behavior; this retained matrix makes no new admission or coverage claim.", + "The issue #1423 inject trigger request and occurrence contracts are new draft carriers that no SDL construct, compiler or runtime path reads; this retained matrix makes no new admission or coverage claim.", + "The issue #1366 inject readback, correlation and backend declaration contracts are new draft carriers; the shared backend allowlist also lets SDL participant behavior specifications cite inject-occurrence-v1 and inject-occurrence-outcome-v1 as evidence_contract_refs, which the compiler copies through uninterpreted, and no runtime path or shipped backend reads or declares them; this retained matrix makes no new admission or coverage claim.", + "This synchronization preserves the original inject and mixed-backend captures, binds their combined source, and adds no runtime or backend-adoption claim.", + "This second synchronization adds behavior-authoring source from issue #297; prior inject and behavior-authoring captures remain preserved. No additional runtime adoption is claimed.", + "Issue #1091 request-boundary admission is verified by its dedicated tests; this retained corpus does not execute the served HTTP adapter or broaden its bounded claims.", + "Issue #1425's updated branch derives reference and libvirt specs from published plan operations. This retained corpus makes no new realization, HTTP relay, or backend-honesty claim.", + "Issue #1580 module-import error-boundary diagnostics are covered by their dedicated parser, resolver and CLI suite; this retained matrix makes no new composition, trust or execution claim." + ], + "load_bearing_results": { + "failed": 0, + "missing": 0, + "passed": 10, + "total": 10 + }, + "plain_language_outcome": "The retained specification-coverage matrix reproduces its prior outcomes after issue #1580 began reporting invalid import declarations, lock records, lockfiles, trust policies, directory imports and unrecordable import provenance as bounded SDL parse diagnostics instead of raw exceptions. Bounded claim limits are unchanged.", + "protocol_revision": "1.0.0", + "request_results": [ + { + "concept_count": 6, + "failed_stage_count": 0, + "missing_count": 0, + "request_id": "survey-representative-range", + "status": "demonstrated" + }, + { + "concept_count": 5, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "cyborg-participant-evaluation", + "status": "partial" + }, + { + "concept_count": 3, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "vsdl-configurable-infrastructure", + "status": "partial" + }, + { + "concept_count": 2, + "failed_stage_count": 1, + "missing_count": 1, + "request_id": "cyber-dem-federation", + "status": "partial" + } + ], + "snapshot_id": "issue-1580-specification-f7b42a16eff6", + "snapshot_sha256": "9275987d4188623ce08c72c2f9f70df63f769f412c73063162ee34c1e096d4fe" +} diff --git a/docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/manifest.json b/docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/manifest.json new file mode 100644 index 000000000..261eb23ff --- /dev/null +++ b/docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/manifest.json @@ -0,0 +1,10 @@ +{ + "analysis_path": "docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/analysis.json", + "analysis_sha256": "5d44d4e30a2bc6c48be7bbcd05d2e54851324d4b4b242aa8a9841295e2bcc00d", + "bundle_id": "raes-standardized-specification-coverage", + "protocol_path": "docs/research/specification-coverage/protocol-v1.json", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "revision": "capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf", + "snapshot_path": "docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/snapshot.json", + "snapshot_sha256": "07e483cf8ba1cfb297df3f7fae9778de9493bedc620ad474406b8a64b2129af9" +} diff --git a/docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/snapshot.json b/docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/snapshot.json new file mode 100644 index 000000000..4a56d3ba5 --- /dev/null +++ b/docs/research/specification-coverage/captures/capture-19de059e1fb6a5202726532d444033526eb339f0f87ad8ce60f5f9dd31b414cf/snapshot.json @@ -0,0 +1,708 @@ +{ + "artifacts": [ + { + "artifact_id": "enterprise-participant-sdl", + "kind": "sdl", + "path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "sha256": "f7a8897beec243e188ee081975006fad32725f469f267db6e75a1e1cf5727032", + "validator": "raes parse, semantic, instantiation/admission, and compiler pipeline" + }, + { + "artifact_id": "port-range-sdl", + "kind": "sdl", + "path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "sha256": "0d5497ec946b863e6985284ec487dde7d7f6bf710a985be51401ac0e5e79dc4f", + "validator": "raes parse, semantic, instantiation/admission, and compiler pipeline" + }, + { + "artifact_id": "experiment-task-contract", + "kind": "experiment-task", + "path": "contracts/fixtures/experiment-core/experiment-task-v1/valid/reference.json", + "sha256": "f3edf713ac6af26bad609136851c6dd434bfb87ce919a2d8c4414c1035deeafc", + "validator": "raes_contracts.contracts.ExperimentTaskModel" + }, + { + "artifact_id": "apparatus-context-contract", + "kind": "experiment-apparatus-context", + "path": "contracts/fixtures/experiment-core/experiment-apparatus-context-v1/valid/reference.json", + "sha256": "e6fa559c5e961f0aab448d0f70dead24aa74fa8ba5f20e1b72f88e11473c9299", + "validator": "raes_contracts.contracts.ExperimentApparatusContextModel" + }, + { + "artifact_id": "backend-profile", + "kind": "backend-profile", + "path": "contracts/profiles/backend/orchestration-capable.json", + "sha256": "f70b8505a5c0055416db86c533e2e5bf08b11e5a514f076223b6d6c36215a092", + "validator": "raes_contracts.backend_profiles.BackendProfileModel" + }, + { + "artifact_id": "known-limitations", + "kind": "documentation", + "path": "docs/explain/sdl/limitations.md", + "sha256": "489eeab3ce682627682311581eb98af9abb9ff42a437145af266eefb71dc7fc4", + "validator": "documentation evidence only" + } + ], + "baseline": { + "release_revision": "1.1.0", + "release_sha256": "4020a1d56c7fe2831cec59ea64a12bbda9d38ccd94f93b916dd90f1a28f17fcb" + }, + "captured_at": "2026-10-13T05:44:37.947232+00:00", + "concept_results": [ + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "range-topology", + "rationale": "SDL nodes and infrastructure own host, network, link, and dependency meaning; the compiler emits canonical node deployment addresses.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed VM declaration.", + "outcome": "passed", + "pointer": "/nodes/shipping-portal", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Links and dependencies resolved.", + "outcome": "passed", + "pointer": "/infrastructure/shipping-portal", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Published instantiated shape admitted.", + "outcome": "passed", + "pointer": "/nodes/shipping-portal", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical deployment address retained.", + "outcome": "passed", + "pointer": "/node_deployments/provision.node.shipping-portal", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/nodes/shipping-portal" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "exercise-roles", + "rationale": "SDL entity roles own exercise responsibility without becoming control-plane identity or authorization.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed red role.", + "outcome": "passed", + "pointer": "/entities/enterprise-participant/role", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Entity references validated.", + "outcome": "passed", + "pointer": "/entities/enterprise-participant", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Role retained after instantiation.", + "outcome": "passed", + "pointer": "/entities/enterprise-participant/role", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Role retained in entity specification.", + "outcome": "passed", + "pointer": "/entity_specs/enterprise-participant/role", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/entities/enterprise-participant/role" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "evaluation-objectives", + "rationale": "SDL objectives own organization ownership, participant assignment, targets, windows, and assertion-based success; measures remain experiment contracts.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed objective declaration.", + "outcome": "passed", + "pointer": "/objectives/demonstrate-handoff", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Owner, participant assignment, targets, assertions, and workflow refs resolved.", + "outcome": "passed", + "pointer": "/objectives/demonstrate-handoff/success", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Objective retained in admitted artifact.", + "outcome": "passed", + "pointer": "/objectives/demonstrate-handoff", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical objective address retained.", + "outcome": "passed", + "pointer": "/objectives/evaluation.objective.demonstrate-handoff", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/objectives/demonstrate-handoff" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "control-workflows", + "rationale": "SDL workflows own the portable control graph and compile to canonical orchestration state contracts.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed control graph.", + "outcome": "passed", + "pointer": "/workflows/yard-recovery", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Step graph and objective refs validated.", + "outcome": "passed", + "pointer": "/workflows/yard-recovery/steps", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Workflow retained after instantiation.", + "outcome": "passed", + "pointer": "/workflows/yard-recovery", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical control graph retained.", + "outcome": "passed", + "pointer": "/workflows/orchestration.workflow.yard-recovery", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/workflows/yard-recovery" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "authored-evidence-expectations", + "rationale": "SDL evidence requirements own portable capture intent and remain distinct from evidence records and measures.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed capture obligation.", + "outcome": "passed", + "pointer": "/evidence_requirements/objective-truth-evidence", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Source refs and bindings validated.", + "outcome": "passed", + "pointer": "/evidence_requirements/objective-truth-evidence", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Evidence intent retained in admitted artifact.", + "outcome": "passed", + "pointer": "/evidence_requirements/objective-truth-evidence", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + } + ], + "typed_pointer": "/evidence_requirements/objective-truth-evidence" + }, + { + "backend_support": "profile-bound", + "backend_vocabulary_occurrences": [], + "classification": "profile-or-manifest-constraint", + "completeness_disposition": "implemented", + "concept_id": "apparatus-selection-constraints", + "rationale": "The experiment task contract binds processor/backend identities, manifest refs, and capabilities outside SDL.", + "stage_results": [ + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-task-v1/valid/reference.json", + "diagnostic_codes": [], + "note": "Closed ExperimentTaskModel validated.", + "outcome": "passed", + "pointer": "/apparatus_constraints/allowed_backend_refs/0", + "stage_id": "contract", + "validation_strength": "contract" + } + ], + "typed_pointer": "/apparatus_constraints/allowed_backend_refs/0" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "participant-agent", + "rationale": "SDL agents own participant entity, knowledge, actions, observation boundaries, and operating scope.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed participant declaration.", + "outcome": "passed", + "pointer": "/agents/participant-agent", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Participant refs and scope validated.", + "outcome": "passed", + "pointer": "/agents/participant-agent/observation_boundaries", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Participant retained in admitted artifact.", + "outcome": "passed", + "pointer": "/agents/participant-agent", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Compiled participant scope retained.", + "outcome": "passed", + "pointer": "/agent_specs/participant-agent", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/agents/participant-agent" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "participant-action-contract", + "rationale": "The action contract declares portable preconditions, effects, observations, evidence, and failure classes without a runner command.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed action contract.", + "outcome": "passed", + "pointer": "/action_contracts/probe-customer-portal-login", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Action refs and evidence bindings validated.", + "outcome": "passed", + "pointer": "/action_contracts/probe-customer-portal-login/effects", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Action retained in admitted artifact.", + "outcome": "passed", + "pointer": "/action_contracts/probe-customer-portal-login", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical action address retained.", + "outcome": "passed", + "pointer": "/action_contracts/participant.action-contract.probe-customer-portal-login", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/action_contracts/probe-customer-portal-login" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "participant-observation-boundary", + "rationale": "The observation boundary separately declares visible, hidden, and evidence-only information with transition rules.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed observation boundary.", + "outcome": "passed", + "pointer": "/observation_boundaries/participant-view", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Information refs and transitions validated.", + "outcome": "passed", + "pointer": "/observation_boundaries/participant-view/view_rules", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Boundary retained in admitted artifact.", + "outcome": "passed", + "pointer": "/observation_boundaries/participant-view", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "diagnostic_codes": [], + "note": "Canonical boundary address retained.", + "outcome": "passed", + "pointer": "/observation_boundaries/participant.observation-boundary.participant-view", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/observation_boundaries/participant-view" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "evaluation-measure", + "rationale": "ExperimentTaskModel owns metric construct, unit, direction, aggregation, and evidence requirements outside SDL objectives.", + "stage_results": [ + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-task-v1/valid/reference.json", + "diagnostic_codes": [], + "note": "Closed task contract validated.", + "outcome": "passed", + "pointer": "/evaluation_protocol/metric_definitions/foothold-achieved", + "stage_id": "contract", + "validation_strength": "contract" + } + ], + "typed_pointer": "/evaluation_protocol/metric_definitions/foothold-achieved" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "missing", + "completeness_disposition": "documented-gap", + "concept_id": "participant-tool-affordance", + "rationale": "This preregistered matrix has no tested carrier for participant tool affordances. The retained missing classification records missing coverage evidence, not the absence of current participant-behavior capabilities.", + "stage_results": [ + { + "artifact_path": "docs/explain/sdl/limitations.md", + "diagnostic_codes": [], + "note": "The preregistered carrier slot was not run; metadata does not substitute for a typed coverage test.", + "outcome": "not_run", + "pointer": null, + "stage_id": "authored", + "validation_strength": "not-applicable" + } + ], + "typed_pointer": null + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "directly-expressible", + "completeness_disposition": "implemented", + "concept_id": "resource-constrained-topology", + "rationale": "SDL node resources and infrastructure dependencies express portable resource intent without provider resource identifiers.", + "stage_results": [ + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Typed CPU and memory declaration.", + "outcome": "passed", + "pointer": "/nodes/shipping-portal/resources", + "stage_id": "authored", + "validation_strength": "structural" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Resource-bearing topology validated.", + "outcome": "passed", + "pointer": "/infrastructure/shipping-portal", + "stage_id": "semantic", + "validation_strength": "semantic" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Constraints retained in admitted artifact.", + "outcome": "passed", + "pointer": "/nodes/shipping-portal/resources", + "stage_id": "instantiated", + "validation_strength": "phase-admitted" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "diagnostic_codes": [], + "note": "Deployment specification retains resource intent.", + "outcome": "passed", + "pointer": "/node_deployments/provision.node.shipping-portal", + "stage_id": "compiled", + "validation_strength": "compiled" + } + ], + "typed_pointer": "/nodes/shipping-portal/resources" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "missing", + "completeness_disposition": "documented-gap", + "concept_id": "formal-constraint-satisfiability", + "rationale": "This coverage matrix did not exercise a solver-backed carrier. The separate formal-semantic-validation release demonstrates its bounded finite-domain profile; that result is not silently imported into this protocol's missing carrier slot.", + "stage_results": [ + { + "artifact_path": "docs/explain/sdl/limitations.md", + "diagnostic_codes": [], + "note": "No coverage-carrier execution was performed here; independent solver evidence does not change this preregistered denominator.", + "outcome": "not_run", + "pointer": null, + "stage_id": "semantic", + "validation_strength": "not-applicable" + } + ], + "typed_pointer": null + }, + { + "backend_support": "profile-bound", + "backend_vocabulary_occurrences": [ + { + "allowed": true, + "artifact_path": "source:vsdl-paper", + "pointer": "source sections 4-5", + "reason": "Legitimate VSDL realization vocabulary, not RAES core SDL structure.", + "term": "OpenStack/Terraform/Packer" + } + ], + "classification": "deliberately-backend-specific", + "completeness_disposition": "external", + "concept_id": "provider-specific-provisioning", + "rationale": "Provider image selection and provisioning engines are realization mechanics and therefore remain outside core SDL.", + "stage_results": [ + { + "artifact_path": "contracts/profiles/backend/orchestration-capable.json", + "diagnostic_codes": [], + "note": "The portable boundary requires backend contracts; it does not standardize a provider engine.", + "outcome": "not_applicable", + "pointer": "/required_contracts", + "stage_id": "realization-disclosure", + "validation_strength": "profile" + } + ], + "typed_pointer": null + }, + { + "backend_support": "profile-bound", + "backend_vocabulary_occurrences": [], + "classification": "profile-or-manifest-constraint", + "completeness_disposition": "implemented", + "concept_id": "apparatus-clock-context", + "rationale": "ExperimentApparatusContextModel records clock authority, time domain, and synchronization as apparatus facts outside scenario meaning.", + "stage_results": [ + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-apparatus-context-v1/valid/reference.json", + "diagnostic_codes": [], + "note": "Closed apparatus context contract validated.", + "outcome": "passed", + "pointer": "/clocks/0", + "stage_id": "contract", + "validation_strength": "contract" + } + ], + "typed_pointer": "/clocks/0" + }, + { + "backend_support": "not-evaluated", + "backend_vocabulary_occurrences": [], + "classification": "missing", + "completeness_disposition": "documented-gap", + "concept_id": "federated-object-event-exchange", + "rationale": "The federated cyber object/event exchange carrier was not exercised by this preregistered matrix. Runtime event internals are not treated as equivalent evidence.", + "stage_results": [ + { + "artifact_path": "docs/explain/sdl/limitations.md", + "diagnostic_codes": [], + "note": "The missing coverage-carrier test is recorded explicitly, without inferring an ecosystem-wide capability absence.", + "outcome": "not_run", + "pointer": null, + "stage_id": "contract", + "validation_strength": "not-applicable" + } + ], + "typed_pointer": null + } + ], + "deviations": [ + { + "artifact_path": "examples/scenarios/enterprise-participant-evidence-loop.sdl.yaml", + "baseline_sha256": "54ba1a60220e27a55da9cd2a407d7d3ab836fa54460d0b0c6cad87c2e744ddbb", + "rationale": "Migrate participant affiliations and explicit objective assignment, retaining organizational intent and portable action-contract declarations without granting execution authority.", + "retest_sha256": "f7a8897beec243e188ee081975006fad32725f469f267db6e75a1e1cf5727032" + }, + { + "artifact_path": "examples/scenarios/port-authority-surge-response.sdl.yaml", + "baseline_sha256": "a27c7a64e0c5c618fadaccafdf1a4e71600170a8b77b983190822b5141f00dec", + "rationale": "Migrate participant affiliations and explicit objective assignment, retaining organizational intent and portable action-contract declarations without granting execution authority.", + "retest_sha256": "0d5497ec946b863e6985284ec487dde7d7f6bf710a985be51401ac0e5e79dc4f" + }, + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-task-v1/valid/reference.json", + "baseline_sha256": "21952a752f4e8581a9fc3b872e4bc308150548170d38bcfc83dbbe35ff5e0b9f", + "rationale": "Replay the retained preregistered artifact against the current evidence-provenance validation implementation.", + "retest_sha256": "f3edf713ac6af26bad609136851c6dd434bfb87ce919a2d8c4414c1035deeafc" + }, + { + "artifact_path": "contracts/fixtures/experiment-core/experiment-apparatus-context-v1/valid/reference.json", + "baseline_sha256": "9536d897a09cbc6920e667e4f8f9371e51307aa0b3b5ff3c7de682dd783420ab", + "rationale": "Replay the retained preregistered artifact against the current evidence-provenance validation implementation.", + "retest_sha256": "e6fa559c5e961f0aab448d0f70dead24aa74fa8ba5f20e1b72f88e11473c9299" + }, + { + "artifact_path": "docs/explain/sdl/limitations.md", + "baseline_sha256": "129cf17810aad4c51988bc872e28fe43ae95019a80053c42d800ff7e2b9cc93e", + "rationale": "Correct historical mandatory-profile guidance after issue #1207; retain the preregistered missing-concept classifications and coverage limits.", + "retest_sha256": "489eeab3ce682627682311581eb98af9abb9ff42a437145af266eefb71dc7fc4" + } + ], + "execution_status": "complete", + "implementation_surfaces": [ + { + "content_sha256": "53443a7c713e5573980e51c86e1b86310c8fc0cab87263f392362f3b5cdf3f12", + "path": "implementations/python/packages/raes_contracts", + "surface_id": "contract-models" + }, + { + "content_sha256": "e947f59695e907f5af899a6bc4bde60e629620aa7c4a69a41e074ba335758c7a", + "path": "implementations/python/packages/raes_processor", + "surface_id": "processor-pipeline" + }, + { + "content_sha256": "25dcd76213e576a5a47c33f69c1a522c9e67b7cb42d12c684c11041688ebb201", + "path": "implementations/python/packages/raes", + "surface_id": "sdl-pipeline" + } + ], + "limitations": [ + "The execution validates the pinned reference implementation and published contracts, not an independent backend.", + "Repository-owned examples are exact execution artifacts but are not themselves the literature-derived request corpus; the protocol's requests and concepts are.", + "No live range, participant, simulator federation, or provider provisioning engine was executed.", + "Missing concepts remain frozen in this snapshot and require separately scoped product work before a later rerun.", + "This capture replays the retained protocol after EXP-732 run, apparatus, measurement-channel, and augmentation-producer provenance validation; it adds no independent backend or universal provenance assurance claim.", + "Materialization attestation is covered by its dedicated regression suite, not a new claim in this preregistered matrix.", + "This capture refreshes the corrected runtime limitations prose for issue #959; the protocol, coverage classifications and implementation source are unchanged.", + "This capture replays open-by-default augmentation scope integrated with the EXP-731 evidence refinements after composition type refinement; it does not evaluate native backend scope enforcement or broaden the preregistered coverage claims.", + "This capture replays the retained protocol after merging ACT-612 participant relationships with open-by-default augmentation scope; it adds no claim of realized participant relationships or native backend scope enforcement.", + "This capture replays issue #1299 partial listener descriptions on the integrated source state; endpoint completeness and backend admission remain outside this protocol's claims.", + "This capture also binds authoring-adapter semantic conformance to the integrated source; adapter transport behavior remains outside this protocol's claims.", + "Reviewed OCI mirror and pre-seed admission is covered by its own regression suites and the development artifact policy gate, not a new claim in this preregistered matrix.", + "This capture binds issue #1297 service-manager identity, native-name, and explicitly selected systemd-state contract changes to the integrated source. It exercises no live service manager and adds no backend-execution claim.", + "This capture replays the retained specification-coverage protocol after API-404 startup reconciliation added an operational recovery-observation contract. It does not evaluate crash recovery, classify provider effects, or broaden EXP-715 experiment-observation claims.", + "This capture binds API-404 single-owner store admission and immutable target/run scope to the integrated source. The retained offline protocol does not exercise process leases, SQLite lifecycle ordering, or crash recovery.", + "This capture binds issue #1015 deterministic mixed and staged trial admission to the integrated source. The retained offline language corpus does not execute mixed runtimes, phase transitions, backend handoff, or scheduler-driven realization.", + "This replay binds issue #1186 offline control-plane maintenance, readiness, and bounded audit code to the integrated source. The retained language corpus does not execute store recovery, HTTP health behavior, or audit redaction.", + "Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.", + "Issue #1189 control-plane profile declarations are covered by their dedicated runtime suite, not promoted to new claims by the retained language corpus.", + "Issue #1016 mixed-runtime coordination is covered by its dedicated runtime suite. The retained language corpus does not execute mixed providers or establish backend-native realization, multi-controller coordination, IFC, or equivalence.", + "Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.", + "Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.", + "Issue #1361 execution and recovery requirements are verified by dedicated policy, composition, and admission tests; this retained corpus establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 maintainability repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The issue #1361 resource type-hint repair preserves policy semantics and retained corpus outcomes; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "The combined issue #1361 execution-policy and hatchling update preserves retained outcomes and bounded claims; it establishes no live recovery, continuation, or trial-allocation guarantee.", + "Issue #1091 request-boundary admission is verified by its dedicated tests; this retained corpus does not execute the served HTTP adapter or broaden its bounded claims.", + "This combined-source capture re-executes the named SDL, contract and profile artifacts and their passing typed pointers. The inject placement discriminator repair adds no specification coverage claim; runtime dispatch and live backend effects remain outside this corpus. CI independently verifies replay.", + "Issue #1425's updated branch derives reference and libvirt specs from published plan operations. This retained corpus makes no new realization, HTTP relay, or backend-honesty claim.", + "Issue #1580 module-import error-boundary diagnostics are covered by their dedicated parser, resolver and CLI suite; this retained matrix makes no new composition, trust or execution claim." + ], + "protocol_revision": "1.0.0", + "protocol_sha256": "e97a19e643e94c9e589dca823a63c6ce49d3329fe2a3cb888ab630838ed93125", + "raes_revision": "4dbccc6fdd1e4e68a45184d521a15909ff9123db", + "snapshot_id": "issue-1580-specification-f7b42a16eff6", + "snapshot_revision": "branch-capture", + "source_state": { + "base_revision": "4dbccc6fdd1e4e68a45184d521a15909ff9123db", + "checkout_state": "clean", + "implementation_digest": "f7b42a16eff6ab3d606d82f4b45332ffba7c136579a41e897e9ff388e9e16e8a", + "profile": "python-reference-source/v2" + } +}