fix(runtime): declare the missing multi-owner and exactly-once nonclaims

docs/explain/sdl/runtime-architecture.md

@@ -625,9 +625,9 @@ make no named profile claim.
 
 | Profile | Guarantee identifiers | Nonclaim identifiers |
 | --- | --- | --- |
-| P0 | in-process-safety, actor-scoped-idempotency, target-run-isolation, revision-cas, atomic-audit | durability, restart-recovery, multi-owner, high-availability, multitenancy |
+| P0 | in-process-safety, actor-scoped-idempotency, target-run-isolation, revision-cas, atomic-audit | durability, restart-recovery, multi-owner, high-availability, exactly-once-effects, multitenancy |
 | P1 | in-process-safety, actor-scoped-idempotency, target-run-isolation, revision-cas, atomic-audit, durable-state, retained-idempotency, lease-admission, startup-reconciliation | multi-owner, high-availability, exactly-once-effects, multitenancy |
-| P2 | in-process-safety, actor-scoped-idempotency, target-run-isolation, revision-cas, atomic-audit, durable-state, retained-idempotency, lease-admission, startup-reconciliation, authenticated-transport, actor-bound-disclosure, owner-serialized-mutation, revision-carrying-reads | multi-worker, tls-proxy-deployment, high-availability, exactly-once-effects, multitenancy |
+| P2 | in-process-safety, actor-scoped-idempotency, target-run-isolation, revision-cas, atomic-audit, durable-state, retained-idempotency, lease-admission, startup-reconciliation, authenticated-transport, actor-bound-disclosure, owner-serialized-mutation, revision-carrying-reads | multi-owner, multi-worker, tls-proxy-deployment, high-availability, exactly-once-effects, multitenancy |
 | P3 | none | future-coordination |
 
 P0 uses an in-memory store for one target and one run, with an actor supplied

docs/public/guides/control-plane.md

@@ -116,6 +116,49 @@ client-supplied identity headers and sets verified ones.
 - Never turn a snapshot, operation record, history, receipt, or error into a
   participant view by filtering it.
 
+## Bound request bodies
+
+The adapter checks the size of every HTTP request before it routes,
+authenticates, or parses it. The check covers every method and path: the
+public probes, the API description routes, and paths that match no route.
+`ControlPlaneSecurityConfig.max_request_bytes` sets the limit. The default is
+1,000,000 bytes.
+
+- **Declared length.** A request gets `400` with `invalid content-length` when
+  it has more than one `Content-Length` header or a value that is not plain
+  digits. A declared length above the limit gets `413` before the adapter reads
+  any of the body.
+- **Counted bytes.** The adapter counts the body bytes that the ASGI server
+  delivers, whatever the header says. When a chunk would take the total past
+  the limit, the adapter returns `413` with `request too large`. It does not
+  keep that chunk or read the rest of the body.
+- **Buffering.** The adapter holds an accepted body in memory, up to the limit.
+  Then it passes the whole body to the route as one message. A route never sees
+  part of a body. The adapter does not stream a body to a route.
+- **Disconnects.** If the server reports a disconnect before the adapter has
+  read the last chunk of the body, the adapter drops what it has read. No route
+  runs, and no response is sent. This can happen even after the client has sent
+  the whole body. Once the adapter has read the last chunk, the route runs even
+  if the client then leaves. Send each mutation with an `Idempotency-Key`
+  header, and reuse it when you retry.
+- **Rejections.** Every `400` or `413` from this check has the same body for its
+  status and carries `Cache-Control: no-store`. No route runs. The adapter
+  audits the rejection as an `anonymous` `http-request-rejected` event. When
+  that audit write fails or its queue is full, the response stays the same. The
+  log gets a fixed message with no error details.
+
+Your ASGI server and proxy own the rest of this boundary:
+
+- Set a proxy body limit no larger than `max_request_bytes`.
+- Limit header size, request time, idle time, and open connections. The adapter
+  sets no time limit on a slow body, and each open request can buffer up to
+  `max_request_bytes`.
+- The server parses HTTP framing, such as chunked bodies and requests that send
+  both `Content-Length` and `Transfer-Encoding`. The adapter sees only the
+  body bytes that the server passes on.
+- After a rejection, the adapter stops reading the body. The server decides
+  whether to read and discard the rest or to close the connection.
+
 ## Deploy the adapter
 
 - Serve P2 on an administration or service network. Participants must not
@@ -133,6 +176,15 @@ client-supplied identity headers and sets verified ones.
   not let `403` or `404` reveal whether another participant exists.
 - Keep the store directory private. Treat store backups as privileged.
 
+The adapter is one process that owns one store. It provides no high
+availability and no operation by several owners or workers. RAES does not
+guarantee that a backend effect happens exactly once, and it never replays one.
+After a crash, an operation whose effect cannot be established becomes
+`INDETERMINATE` and keeps that state. To resolve it, an operator calls
+`POST /operations/{operation_id}/resolution`. That call records a separate,
+linked operation and leaves the original unchanged. TLS and proxy correctness
+belong to your deployment.
+
 ## Add a route to the adapter
 
 Register the route inside `create_control_plane_app()`, before the adapter

docs/requirements/API-404/requirement.md

@@ -269,6 +269,9 @@ identifies those implementation gaps and the retained canonical requirements.
 - TESTS → TEST `implementations/python/tests/test_runtime_control_plane_api.py` (HTTP/JSON control-plane API tests — auth, idempotency, durability, audit)
 - TESTS → TEST `implementations/python/tests/test_issue_1182_operation_lifecycle_contract.py` (Closed transition matrix, malformed carriers, immutability, denial, semantic idempotency, and schema governance)
 - TESTS → TEST `implementations/python/tests/test_issue_1093_request_rejection_offload.py` (Non-blocking, saturation-bounded, fail-closed request rejection audit tests)
+- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_api_guards.py` (No dispatch or response for a request abandoned before its body completes)
+- DOCUMENTS → DOCUMENTATION `docs/public/guides/control-plane.md` (Bounded routes, size limit, counting point, buffering, disconnects, and server/proxy duties)
+- TESTS → TEST `implementations/python/tests/test_issue_1091_request_limit_boundary.py` (Body-shape and absent or misleading Content-Length matrix, abandoned-request non-dispatch, intact accepted-body delivery, stable uncacheable 413 before any endpoint, and audit failure without admission or disclosure)
 - DOCUMENTS → GITHUB_ISSUE `1092` (Make the local control plane crash-consistent and explicitly single-process)
 - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_mutation.py` (Operation-family-neutral logical mutation authority and guarded extension callback boundary)
 - IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_runtime/control_plane_execution.py` (Write-ahead RUNNING claims, guarded backend validation and execution, and terminal commit routing)

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

@@ -0,0 +1,163 @@
+{
+  "analysis_id": "issue-1091-analysis-v70",
+  "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-v70.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-1091-execution-v70",
+  "generated_at": "2026-10-09T08:31:45.066266+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.",
+    "Issue #1091 request-boundary admission, including requests abandoned before their body completes, is verified by its dedicated request-boundary suite and adds no new formal-semantic claim to this retained corpus."
+  ],
+  "plain_language_outcome": "The retained formal cases reproduce their prior outcomes after issue #1091 stopped dispatching control-plane HTTP requests that are abandoned before their body completes. The bounded claims and unsupported classes are unchanged.",
+  "protocol_revision": "2.0.0"
+}