fix: admit participant delivery temporal subjects

docs/public/participant-control.md

@@ -120,7 +120,10 @@ observation boundary. Reuse the action, control, or inject carrier.
 - Use `participant_inject_deliveries` when an existing orchestration inject is
   addressed to a participant. Retain its inject identity. Retain its
   event/script/story identity. Bind an observation boundary. Name each needed
-  delivery, order, evidence, or control reference.
+  delivery, order, evidence, or control reference. A temporal constraint bound
+  to the delivery compiles to that delivery's `participant.*` address; it
+  constrains the authored occurrence and does not prove dispatch, delivery, or
+  observation.
 - Do not infer a participant addressee from an environment inject. Do not put
   policy text, hidden answers, credentials, or raw evidence in a participant
   carrier.

docs/requirements/ASR-530/requirement.md

@@ -21,6 +21,8 @@ Agent-assisted development can produce internally coherent code and documentatio
 
 ## Traceability
 
+- IMPLEMENTS → PROOF `docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1389-v53.json` (Current source-bound coverage replay after participant inject temporal-subject admission)
+- IMPLEMENTS → PROOF `docs/research/formal-semantic-validation/bundles/retest-v53.json` (Current source-bound formal replay after participant inject temporal-subject admission)
 - IMPLEMENTS → PROOF `docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1358-v45.json` (Prior source-bound coverage replay with retained classifications)
 - IMPLEMENTS → PROOF `docs/research/formal-semantic-validation/bundles/retest-v45.json` (Prior source-bound formal replay with retained bounded claims)
 - IMPLEMENTS → PROOF `docs/research/specification-coverage/bundles/raes-standardized-specification-coverage-issue-1358-v46.json` (Current source-bound coverage replay with retained classifications)

docs/research/formal-semantic-validation/analysis-v53.json

@@ -0,0 +1,155 @@
+{
+  "analysis_id": "issue-1389-analysis-v53",
+  "claim": {
+    "allowed_evidence": [
+      "production parser and semantic-validator results",
+      "canonical compiled digests",
+      "participant contract regression tests",
+      "pinned protocol, corpus, and execution snapshot"
+    ],
+    "claim_id": "asr-530-formal-semantic-validation-retest",
+    "disallowed_evidence": [
+      "schema success as semantic proof",
+      "workflow reachability as network or exploit reachability",
+      "FM labels as gate outcomes",
+      "attribution as counterfactual proof",
+      "formal prose or maintainer confidence alone"
+    ],
+    "evidence_artifacts": [
+      "docs/research/formal-semantic-validation/protocol-v2.json",
+      "docs/research/formal-semantic-validation/corpus/manifest-v4.json",
+      "docs/research/formal-semantic-validation/execution-snapshot-v53.json",
+      "docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json",
+      "docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json",
+      "docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json",
+      "docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json"
+    ],
+    "falsification_protocol": "Replay every retained and new case through its production entrypoint, require complete digest and evidence joins, execute participant fixtures, and derive status from the recorded outcomes.",
+    "objective_fail_criteria": "A supported negative passes, a positive fails, an observation drifts, a required participant case is missing, or weaker evidence is promoted to solver, exploit-path, runtime-stability, or counterfactual assurance.",
+    "objective_pass_criteria": "Every claim class has positive and negative cases, all supported cases reproduce the frozen outcome, every participant obligation has passing positive and negative fixtures, and unsupported classes remain untested.",
+    "statement": "At the recorded source-state digest, the retained RAES controls have the bounded statuses recorded here; historical releases are integrity evidence, not current replay evidence.",
+    "threats_to_validity": [
+      "The issue-specific corpus is intentionally small and does not enumerate every validator invariant.",
+      "The participant fixtures exercise reference production contracts and tests, not every independent backend realization.",
+      "The replay gate runs on one Python reference configuration and one pinned RAES revision.",
+      "Unsupported solver-level classes have protocol cases but no executable observations."
+    ]
+  },
+  "claim_results": [
+    {
+      "case_count": 2,
+      "claim_class_id": "schema-validity",
+      "evidence_status": "demonstrated",
+      "limitations": [
+        "Bounded to the named source/model structural controls."
+      ],
+      "matching_case_count": 2,
+      "participant_obligation_count": 0,
+      "replayable_case_count": 2,
+      "unsupported_case_count": 0
+    },
+    {
+      "case_count": 4,
+      "claim_class_id": "semantic-consistency",
+      "evidence_status": "partial",
+      "limitations": [
+        "Partial coverage of named static semantics and participant obligations, not universal consistency."
+      ],
+      "matching_case_count": 4,
+      "participant_obligation_count": 7,
+      "replayable_case_count": 4,
+      "unsupported_case_count": 0
+    },
+    {
+      "case_count": 2,
+      "claim_class_id": "graph-reachability",
+      "evidence_status": "partial",
+      "limitations": [
+        "Partial workflow control-flow reachability only; not network, service, or exploit reachability."
+      ],
+      "matching_case_count": 2,
+      "participant_obligation_count": 0,
+      "replayable_case_count": 2,
+      "unsupported_case_count": 0
+    },
+    {
+      "case_count": 4,
+      "claim_class_id": "constraint-satisfiability",
+      "evidence_status": "demonstrated",
+      "limitations": [
+        "Demonstrated only for raes-finite-domain-satisfiability-v1 and its pinned solver configuration."
+      ],
+      "matching_case_count": 4,
+      "participant_obligation_count": 0,
+      "replayable_case_count": 2,
+      "unsupported_case_count": 2
+    },
+    {
+      "case_count": 4,
+      "claim_class_id": "exploit-path-validity",
+      "evidence_status": "demonstrated",
+      "limitations": [
+        "Demonstrated only for the admitted snapshot, typed graph, query, semantics, and bounded search profile."
+      ],
+      "matching_case_count": 4,
+      "participant_obligation_count": 0,
+      "replayable_case_count": 2,
+      "unsupported_case_count": 2
+    },
+    {
+      "case_count": 2,
+      "claim_class_id": "determinism-stability",
+      "evidence_status": "partial",
+      "limitations": [
+        "Partial parse-to-compile repeatability only; runtime and backend determinism are untested."
+      ],
+      "matching_case_count": 2,
+      "participant_obligation_count": 0,
+      "replayable_case_count": 2,
+      "unsupported_case_count": 0
+    },
+    {
+      "case_count": 2,
+      "claim_class_id": "counterfactual-necessity",
+      "evidence_status": "untested",
+      "limitations": [
+        "Untested because no governed intervention or ablation entrypoint ran."
+      ],
+      "matching_case_count": 2,
+      "participant_obligation_count": 0,
+      "replayable_case_count": 0,
+      "unsupported_case_count": 2
+    }
+  ],
+  "corpus_revision": "4.0.0",
+  "evidence_status": "partial",
+  "execution_id": "issue-1389-execution-v53",
+  "generated_at": "2026-09-26",
+  "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."
+  ],
+  "plain_language_outcome": "The retained formal cases reproduce their prior outcomes against source that admits exact participant inject delivery temporal subjects. The bounded claims and unsupported classes are unchanged.",
+  "protocol_revision": "2.0.0"
+}

docs/research/formal-semantic-validation/bundles/retest-v53.json

@@ -0,0 +1,122 @@
+{
+  "analysis_path": "docs/research/formal-semantic-validation/analysis-v53.json",
+  "analysis_sha256": "8dd885f774cec9b1a71d1feb8295194eed1b022d5677aff0fbb31c8457a53357",
+  "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": "54.0.0",
+  "snapshot_path": "docs/research/formal-semantic-validation/execution-snapshot-v53.json",
+  "snapshot_sha256": "ae7b70b213f4027e732ee4cb2d5e15b3bf9fdab03cab4dc9d7ff6e08c7a8130c"
+}