fix(runtime): refuse backend snapshot entries whose runtime domain is an untyped string

docs/research/formal-semantic-validation/capture-records/capture-86296e4c4d531cfa6a72a8710e5dd8db25e3066f87ed9f6ba71bd1c40c1cc454.json

@@ -0,0 +1,4 @@
+{
+  "capture_path": "docs/research/formal-semantic-validation/captures/capture-86296e4c4d531cfa6a72a8710e5dd8db25e3066f87ed9f6ba71bd1c40c1cc454/manifest.json",
+  "capture_sha256": "5a4c03a176a33d23d13216f3fec16ee7cd94087043fc1e2ef61bbc0956971d27"
+}

docs/research/formal-semantic-validation/captures/capture-86296e4c4d531cfa6a72a8710e5dd8db25e3066f87ed9f6ba71bd1c40c1cc454/analysis.json

@@ -0,0 +1,170 @@
+{
+  "analysis_id": "issue-1434-typed-runtime-domain-formal-analysis-719a546cff12",
+  "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-1434-typed-runtime-domain-formal-719a546cff12",
+  "generated_at": "2026-10-14T02:44:08.894969+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 #1395 adds a separate bounded two-operation crossing model profile. This retained corpus does not establish participant-crossing equivalence or runtime realization; those assurances remain separate."
+  ],
+  "plain_language_outcome": "The retained formal cases and participant tests replay against the issue #1434 source, which refuses backend snapshot entries whose runtime domain is an untyped string, with their classifications unchanged.",
+  "protocol_revision": "2.0.0"
+}

docs/research/formal-semantic-validation/captures/capture-86296e4c4d531cfa6a72a8710e5dd8db25e3066f87ed9f6ba71bd1c40c1cc454/manifest.json

@@ -0,0 +1,122 @@
+{
+  "analysis_path": "docs/research/formal-semantic-validation/captures/capture-86296e4c4d531cfa6a72a8710e5dd8db25e3066f87ed9f6ba71bd1c40c1cc454/analysis.json",
+  "analysis_sha256": "caaeff0887bbb03badd06b7e54cd2fde6962e1fe390f542588c4855221e538d7",
+  "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-86296e4c4d531cfa6a72a8710e5dd8db25e3066f87ed9f6ba71bd1c40c1cc454",
+  "snapshot_path": "docs/research/formal-semantic-validation/captures/capture-86296e4c4d531cfa6a72a8710e5dd8db25e3066f87ed9f6ba71bd1c40c1cc454/snapshot.json",
+  "snapshot_sha256": "6965c91b203e06162c0dd71f1a81a1a032ac9a82cd3f6a97aa9f67035939d4e4"
+}