docs(spec): model the operator provisioning plane (S9) in Tamarin + prose

Stacked on #1657 (mini/community-provisioning). The operator plane
(POST /operator/communities) is the first runtime surface that can mint
tenancy, so it gets the same mechanized treatment as the rest of the
multi-tenant model:

Tamarin (docs/spec/MultiTenantAuth.spthy, new S9 section):
- Rules: Register_Operator / Compromise_Operator_Key, operator-signed
  provision + rotate requests (NIP-98 preimage includes the payload hash
  h(<host, owner>) — payload binding mandatory), relay provision +
  converge/rotate gated on the !OperatorKey allowlist, and the
  UniqueHostBinding restriction importing the append-only host map.
- Lemmas: provisioning_requires_operator_authorization (allowlist gate,
  no compromise disjunct — compromise doesn't extend the allowlist),
  provision_accepts_only_operator_signed_payload (payload binding),
  rotation_confined_to_host_community (S5/S6-style single witness), plus
  three exists-trace probes incl. the create-then-converge lifecycle.
- Full run: all 38 lemmas verified green (Tamarin 1.12.0 / Maude 3.5.1,
  ~141 s). Three commented mutations confirmed red:
  MUTATION_Provision_Unsigned_Body (the optional-payload-tag gap from the
  #1657 review; 8-step trace), MUTATION_Provision_Any_Client (8 steps),
  MUTATION_Rotate_Ignore_Host (12 steps).

TLA+ (docs/spec/MultiTenantRelay.tla, comment-only): stated assumption
P-HOST-APPEND — HostCommunity stays a constant-per-segment function
because the host map is append-only (ensure_configured_community's
ON CONFLICT upsert never re-points a bound host), so runtime
provisioning needs no TLC remodeling. SANY-checked.

Prose (docs/multi-tenant-relay.md): S9 section under Authorization
soundness, verification-status update (32 -> 38 lemmas, current run
figures), P-HOST-APPEND conformance row (incl. the require-payload-tag
and signer-checked-allowlist obligations), Mechanized Verification
bullet, machine-check-hygiene classification for the new lemmas, and a
stale spthy line-reference fix (:403/:413 -> :427/:437).

Co-authored-by: Tyler Longwell <tlongwell@block.xyz>
Signed-off-by: Tyler Longwell <tlongwell@block.xyz>

docs/multi-tenant-relay.md

@@ -571,13 +571,47 @@ load-bearing *backstop*.
   stops a B-stamped token authorizing over an A-host stops a B-host AUTH
   registering into A. Its in-relay counterpart is I5's open-community branch
   (`AuthenticateOpenCommunity`, mutation M10).
+- **S9 (Operator-plane provisioning confinement).** Runtime community
+  provisioning (`POST /operator/communities`) is the one admitted surface whose
+  *effect* spans tenants: it creates a community, binds its host, and
+  bootstraps or rotates that community's owner. Its authority is the
+  deployment-level `RELAY_OPERATOR_PUBKEYS` allowlist
+  (`crates/buzz-relay/src/api/operator.rs`), never a `relay_members` role —
+  deployment-root authority, documented as such on the endpoint. Three lemmas:
+  `provisioning_requires_operator_authorization` (every owner
+  bootstrap/rotation — the plane's only membership effect, emitted by both the
+  provision and the converge/rotate path — names an operator-registered key;
+  there is deliberately **no** compromise disjunct, because compromising an
+  operator's secret does not put a new key on the allowlist, so the claim
+  holds unconditionally); `provision_accepts_only_operator_signed_payload`
+  (the accepted `(host, owner)` pair is exactly a pair the named operator
+  signed — the NIP-98 payload hash over the JSON body is what forces this, so
+  a captured `Authorization` header can only *replay* the same pair, which is
+  the documented idempotent convergence, never *re-target* it); and
+  `rotation_confined_to_host_community` (an owner rotation lands only in the
+  community bound to the request's host — the request names a host, never a
+  community id, the same single-witness framing as S5/S6 via
+  `RotationResolved(owner, used_comm, host, host_comm)`). The payload-binding
+  lemma pins the PR #1657 review finding that `buzz-auth`'s NIP-98
+  verification treats the `payload` tag as *optional* if absent:
+  `MUTATION_Provision_Unsigned_Body` models exactly that gap (operator signs
+  without the payload hash; relay accepts body fields from the wire unbound)
+  and falsifies the lemma, so requiring the payload tag on this endpoint is a
+  conformance obligation, not a nicety. `Create_Community` remains the
+  trusted startup-seed path (`ensure_configured_community` at boot); the S9
+  theorems quantify over the provisioning action facts, so they constrain the
+  protocol path without pretending the config path is adversarial.
 
 Each Tamarin lemma is paired with an exists-trace sanity lemma (the honest
 protocol can run), the Tamarin analog of the mutation test.
 
-**Verification status.** S1–S8 are **machine-verified green** on
-Tamarin 1.12.0 / Maude 3.5.1 — the full selected run verifies all 32 lemmas in
-~12s with zero `analyzed` failures. S1/S2: `token_confinement`,
+**Verification status.** S1–S9 are **machine-verified green** on
+Tamarin 1.12.0 / Maude 3.5.1 — the full selected run verifies all 38 lemmas in
+~141s with zero `analyzed` failures. (The step counts and wall-clock figures
+below are from earlier, smaller revisions of the model; each addition enlarges
+the search space for the pre-existing lemmas — e.g.
+`other_community_key_compromise_does_not_authorize` closes at 486 steps in the
+current run versus 147 pre-S9 — but every lemma still closes.) S1/S2: `token_confinement`,
 `cross_community_use_attempts_are_not_authorized`, the two
 `minted_*_channels_match_stamp` lemmas, `token_stamp_matches_mint`,
 `cross_community_mint_yields_no_token_for_that_request`, and the
@@ -620,6 +654,23 @@ S8 (open-community AUTH confinement): `open_auth_registration_confined_to_host_c
 (5 steps) proving a legitimate open-community registration is producible, so the
 confinement lemma is non-vacuous; its in-relay counterpart is the M10 open-AUTH
 stamp mutation, confirmed red in TLA+ (a 2-state `Inv_AdmissionFence` violation).
+S9 (operator-plane provisioning): `provisioning_requires_operator_authorization`
+(6 steps), `provision_accepts_only_operator_signed_payload` (7 steps), and
+`rotation_confined_to_host_community` (2 steps — the S5/S6 single-witness
+framing, so a counterexample is one rule instance), with three exists-trace
+probes (`executable_provision`, 12 steps; `executable_rotate`, 10 steps; and
+`executable_rotate_after_provision`, 12 steps — the create-then-converge
+lifecycle end to end, proving a rotate on an already-bound host lands in the
+community the original provision bound). All three S9 mutations are confirmed
+red: `MUTATION_Provision_Unsigned_Body` (the payload tag omitted, so the signed
+NIP-98 event binds URL/method/freshness but not the JSON body — the PR #1657
+review finding) falsifies `provision_accepts_only_operator_signed_payload` with
+an 8-step trace; `MUTATION_Provision_Any_Client` (the `RELAY_OPERATOR_PUBKEYS`
+gate replaced by "any valid signature") falsifies
+`provisioning_requires_operator_authorization` with an 8-step trace; and
+`MUTATION_Rotate_Ignore_Host` (the rotation applied to a community other than
+the host's binding — the operator-plane confused deputy) falsifies
+`rotation_confined_to_host_community` with a 12-step trace.
 
 The S5 confinement lemma was deliberately framed to keep its mutation
 *cheaply* refutable. An earlier framing joined two action facts
@@ -700,6 +751,31 @@ Each axiom is *admitted* per deployment, not assumed universally:
   token under the deployment's routing/storage shape (and that the seen-set TTL
   covers the full ±60 s window). A failing test or an unmet gate rejects the
   deployment.
+- **P-HOST-APPEND (operator plane)** — the host→community map is **append-only**:
+  a host, once bound, is never re-pointed to a different community. Admitted by
+  `ensure_configured_community`'s upsert
+  (`crates/buzz-db/src/lib.rs`): `INSERT ... ON CONFLICT (lower(host)) DO UPDATE
+  SET host = EXCLUDED.host RETURNING id` — a second request for an
+  already-bound host returns the *same* community id and only refreshes the
+  host's stored casing; there is no code path (startup seeding or
+  `POST /operator/communities`) that changes an existing binding's community.
+  This is the assumption that lets the TLA+ model keep `HostCommunity` a
+  *constant* function per checked segment (runtime provisioning appends a new
+  host↦community pair, which is a fresh constant assignment for subsequent
+  behavior — never a mutation of an existing one), so every TLC result over the
+  fixed `HostA/HostB/HostBad` harness remains valid across provisioning events
+  without remodeling `HostCommunity` as a variable. Tamarin imports the same
+  assumption as the `UniqueHostBinding` restriction and discharges the operator
+  plane's authorization obligations as S9 (three lemmas + three confirmed-red
+  mutations). Two further conformance obligations ride on this surface: the
+  NIP-98 `payload` tag MUST be required (not merely verified-if-present) on
+  `POST /operator/communities`, since `MUTATION_Provision_Unsigned_Body` shows
+  an optional payload tag lets a captured `Authorization` header be raced with
+  a swapped JSON body on the one endpoint that mints tenancy; and
+  `RELAY_OPERATOR_PUBKEYS` must be checked against the *signer* of the NIP-98
+  event, never inferred from the body or connection. A migration lint asserting
+  no `UPDATE communities SET host` path (mirroring P-RESOLVE's
+  channel-immutability lint) admits the append-only axiom structurally.
 
 ## Prior Art
 
@@ -831,14 +907,16 @@ as label-flow non-interference is, to our knowledge, new for a Nostr relay.
   actors, and ids explodes the space; symmetry + bounded observations keep the
   core isolation surface exhaustively checkable.
 - **`docs/spec/MultiTenantAuth.spthy`** — the Tamarin authorization model. Run:
-  `tamarin-prover --prove docs/spec/MultiTenantAuth.spthy`. All 32 lemmas (S1–S8)
-  verify green (Tamarin 1.12.0 / Maude 3.5.1, ~12 s) — each safety lemma paired with
+  `tamarin-prover --prove docs/spec/MultiTenantAuth.spthy`. All 38 lemmas (S1–S9)
+  verify green (Tamarin 1.12.0 / Maude 3.5.1, ~141 s) — each safety lemma paired with
   a verified exists-trace sanity lemma, and the documented mutations
   (`MUTATION_Use_Token_Claimed_Community` for S1, the S3 bad-accept and S4
   splice-as-append mutations, `MUTATION_Use_Token_ChannelLess_Ignore_Host`
   for S5's host fence, `MUTATION_Use_Token_Ignore_Host` for S6's channel-bearing
-  host/channel-agreement fence, and `MUTATION_Admit_Ignore_Community` for S7's
-  NIP-43 admission confinement) confirmed red. The 32 lemmas include the
+  host/channel-agreement fence, `MUTATION_Admit_Ignore_Community` for S7's
+  NIP-43 admission confinement, and the three S9 operator-plane mutations —
+  `MUTATION_Provision_Unsigned_Body`, `MUTATION_Provision_Any_Client`,
+  `MUTATION_Rotate_Ignore_Host`) confirmed red. The 38 lemmas include the
   open-community AUTH pair added with the host-scoped-open-auth surfaces:
   `open_auth_registration_confined_to_host_community` (2 steps) proves an
   open-community auto-registration commits to the host-resolved community and never
@@ -849,12 +927,13 @@ as label-flow non-interference is, to our knowledge, new for a Nostr relay.
   full lemma list, the S5/S6 single-witness framing, and the corrected
   `other_community_key_compromise_does_not_authorize` vacuity fix.
 
-  **Machine-check hygiene.** S1–S8 lemmas close by two distinct shapes.
+  **Machine-check hygiene.** S1–S9 lemmas close by two distinct shapes.
   **Rule-shape closure** means the lemma's conclusion follows by unification on a
   single rule's action multiset: `token_confinement`,
   `audit_append_advances_same_community_head`,
   `channelless_use_confined_to_host_community` (the S5 single-witness fact),
-  `channelbearing_use_agrees_with_host` (the S6 single-witness fact), and
+  `channelbearing_use_agrees_with_host` (the S6 single-witness fact),
+  `rotation_confined_to_host_community` (the S9 single-witness fact), and
   the S2 supporting set
   (`minted_token_channels_match_stamp`, `minted_request_channels_match_stamp`,
   `token_stamp_matches_mint`). These are well-formedness guards on the model's
@@ -869,9 +948,13 @@ as label-flow non-interference is, to our knowledge, new for a Nostr relay.
   **Substantive closure** requires cross-rule reasoning over
   persistent-fact invariance (`cross_community_mint_yields_no_token_for_that_request`,
   `leaked_token_blast_radius_contained`,
-  `cross_community_use_attempts_are_not_authorized`), linear-fact lifecycle
+  `cross_community_use_attempts_are_not_authorized`,
+  `provisioning_requires_operator_authorization`), linear-fact lifecycle
   (`cross_community_audit_splice_attempt_is_not_append`), or signed-preimage
-  unification (`system_event_acceptance_requires_same_community_key_or_compromise`).
+  unification (`system_event_acceptance_requires_same_community_key_or_compromise`,
+  `provision_accepts_only_operator_signed_payload` — the S9 payload-binding
+  claim, which needs both the operator's signature over the payload hash and
+  the allowlist premise).
   Tamarin proves both kinds identically; the distinction is for reviewer hygiene,
   not a weakened theorem claim. This paragraph is prose-only to preserve the
   `.spthy` byte hash above.
@@ -999,7 +1082,7 @@ The model's obligations map to concrete code seams:
   red — so admit-into-A-then-act-in-B is a *caught* escape, not an invisible one.
   On the authorization side, NIP-43 member-list events are signed and accepted
   per-community in Tamarin (`Community_Signs_NIP43_MemberList` /
-  `Relay_Accepts_NIP43_MemberList`, `MultiTenantAuth.spthy:403`/`:413`), and
+  `Relay_Accepts_NIP43_MemberList`, `MultiTenantAuth.spthy:427`/`:437`), and
   `nip43_admission_confined_to_signing_community` proves B's signing key can
   never admit a pubkey into A (Theorem S7).
 

docs/spec/MultiTenantAuth.spthy

@@ -472,6 +472,264 @@ rule Relay_Accepts_NIP43_MemberList:
 // Expected mutation result: `nip43_admission_confined_to_signing_community`
 // goes red.
 
+// ============================================================================
+// S9: Deployment-operator community provisioning (POST /operator/communities)
+// ============================================================================
+//
+// PR #1657 adds a deployment-operator HTTP plane that can create a community
+// (and its host mapping) at runtime and bootstrap/rotate that community's
+// owner. This is intentionally the ONLY admitted surface whose effect spans
+// tenants: its authority is the deployment-level RELAY_OPERATOR_PUBKEYS
+// allowlist (`!OperatorKey`), never a `relay_members` role. `Create_Community`
+// above remains the CONFIG/STARTUP seeding path (ensure_configured_community
+// at boot — trusted by deployment, not by protocol); this section models the
+// runtime protocol path, so its theorems quantify over the provisioning
+// action facts, not over `CommunityCreated`.
+//
+// Wire shape: one NIP-98-signed POST whose signed preimage includes the
+// payload hash over the JSON body (host, owner). The payload binding is
+// load-bearing — see MUTATION_Provision_Unsigned_Body below, which models the
+// real "NIP-98 payload tag optional" gap (kalvin's review finding #1 on
+// PR #1657) and falsifies the S9 lemmas.
+//
+// Create-vs-rotate is decided by DB state, exactly like the endpoint: the
+// SAME signed request provisions when the host is unbound and converges
+// (owner bootstrap/rotation) when it is already bound. A replayed create can
+// therefore only re-assert the SAME (host, owner) it signed — benign
+// convergence, the documented idempotency — because the payload binds both.
+
+rule Register_Operator:
+  [ Fr(~sk_op) ]
+  --[
+      OperatorRegistered(pk(~sk_op))
+    ]->
+  [
+      !OperatorKey(pk(~sk_op)),
+      !OperatorSecret(pk(~sk_op), ~sk_op),
+      Out(pk(~sk_op))
+  ]
+
+rule Compromise_Operator_Key:
+  [ !OperatorSecret(op, sk) ]
+  --[
+      OperatorKeyCompromised(op)
+    ]->
+  [ Out(sk) ]
+
+// The operator signs a provision request for a fresh host. The signed
+// preimage commits to the payload hash h(<host, owner>) alongside URL,
+// method, and freshness — the NIP-98 payload-tag discipline made mandatory.
+// `OperatorAuthorizedProvision` is the single authorization witness both
+// relay rules (provision + rotate) are checked against: it names the exact
+// (host, owner) the operator signed.
+rule Operator_Sends_Provision_Request:
+  [ !OperatorSecret(op, sk), !ClientPublic(owner), Fr(~host), Fr(~url), Fr(~time) ]
+  --[
+      OperatorAuthorizedProvision(op, ~host, owner),
+      ProvisionRequested(op, ~host, owner)
+    ]->
+  [
+      Out(
+        < 'operator_provision',
+          op,
+          ~url,
+          'POST',
+          ~time,
+          ~host,
+          owner,
+          sign(< 'kind27235_operator', op, ~url, 'POST', ~time, h(< ~host, owner >) >, sk)
+        >
+      ),
+      Out(~host)
+  ]
+
+// The operator signs the same request shape for an ALREADY-BOUND host: the
+// endpoint converges (bootstrap_owner re-runs), which rotates the community
+// owner. Deployment-root authority, documented as such on the endpoint.
+rule Operator_Sends_Rotate_Request:
+  [ !OperatorSecret(op, sk), !HostCommunity(host, comm), !ClientPublic(owner),
+    Fr(~url), Fr(~time) ]
+  --[
+      OperatorAuthorizedProvision(op, host, owner),
+      RotateRequested(op, host, owner)
+    ]->
+  [
+      Out(
+        < 'operator_provision',
+          op,
+          ~url,
+          'POST',
+          ~time,
+          host,
+          owner,
+          sign(< 'kind27235_operator', op, ~url, 'POST', ~time, h(< host, owner >) >, sk)
+        >
+      )
+  ]
+
+// Provision path: the host has no existing binding, so the upsert inserts a
+// fresh community, binds the host, and bootstraps the owner. The signature is
+// verified against the payload hash recomputed over the RECEIVED body — an
+// adversary who swaps host/owner in transit fails verification (P-SIG).
+// The relay checks the sender against `!OperatorKey` — the model's
+// RELAY_OPERATOR_PUBKEYS allowlist. A registered client key is NOT sufficient
+// (see MUTATION_Provision_Any_Client).
+rule Relay_Provisions_Community:
+  [ In(< 'operator_provision', op, url, 'POST', time, host, owner, sig >),
+    !OperatorKey(op),
+    Fr(~comm), Fr(~sk_comm) ]
+  --[
+      Eq(verify(sig, < 'kind27235_operator', op, url, 'POST', time, h(< host, owner >) >, op), true),
+      CommunityProvisioned(~comm, host, op),
+      ProvisionAccepted(op, host, owner),
+      OwnerBootstrapped(owner, ~comm, host, op),
+      HostBound(host, ~comm)
+    ]->
+  [
+      !Community(~comm),
+      !CommunitySigningKey(~comm, ~sk_comm),
+      !HostCommunity(host, ~comm),
+      AuditHead(~comm, 'genesis'),
+      !Admitted(owner, ~comm)
+  ]
+
+// Converge/rotate path: the host is already bound, so the upsert is a no-op
+// on the community row and bootstrap_owner (re)runs for that SAME community.
+// The effect is confined to the host's bound community — the request names a
+// host, never a community id (see MUTATION_Rotate_Ignore_Host).
+rule Relay_Rotates_Owner:
+  [ In(< 'operator_provision', op, url, 'POST', time, host, owner, sig >),
+    !OperatorKey(op),
+    !HostCommunity(host, comm) ]
+  --[
+      Eq(verify(sig, < 'kind27235_operator', op, url, 'POST', time, h(< host, owner >) >, op), true),
+      OwnerRotated(owner, comm, host, op),
+      OwnerBootstrapped(owner, comm, host, op),
+      RotationResolved(owner, comm, host, comm)
+    ]->
+  [ !Admitted(owner, comm) ]
+
+// Idempotency / append-only host map, imported as a restriction: a host is
+// bound to at most one community, ever. Grounded in the implementation:
+// `ensure_configured_community` upserts `ON CONFLICT (lower(host)) DO UPDATE
+// SET host = EXCLUDED.host RETURNING id` — a second request for the same host
+// returns the SAME community id and never re-points the host. This is the
+// same append-only assumption the TLA+ model's header states for keeping
+// `HostCommunity` a constant-per-segment function; here it excludes traces
+// where a replayed provision would mint a second community for a bound host
+// (the real relay converges instead — the rotate rule above is that path).
+restriction UniqueHostBinding:
+  "All host c1 c2 #i #j.
+      HostBound(host, c1) @ i & HostBound(host, c2) @ j ==> #i = #j"
+
+// MUTATION_Provision_Unsigned_Body (DO NOT ENABLE in the real model): the
+// real-world gap this pins is kalvin's finding #1 on PR #1657 — NIP-98
+// verification treats the payload tag as OPTIONAL, so an operator client that
+// omits it produces a signature binding only URL/method/freshness, and anyone
+// who captures the Authorization header can race it with a swapped JSON body.
+// Modeled as the pair: the operator signs WITHOUT the payload hash, and the
+// relay accepts the body fields from the wire unbound.
+//
+// rule MUTATION_Operator_Signs_Without_Payload:
+//   [ !OperatorSecret(op, sk), !ClientPublic(owner), Fr(~host), Fr(~url), Fr(~time) ]
+//   --[
+//       OperatorAuthorizedProvision(op, ~host, owner),
+//       ProvisionRequested(op, ~host, owner)
+//     ]->
+//   [
+//       Out(< 'operator_provision_nopayload', op, ~url, 'POST', ~time, ~host, owner,
+//             sign(< 'kind27235_operator_nopayload', op, ~url, 'POST', ~time >, sk) >),
+//       Out(~host)
+//   ]
+//
+// rule MUTATION_Relay_Provisions_Unbound_Body:
+//   [ In(< 'operator_provision_nopayload', op, url, 'POST', time, host, owner, sig >),
+//     !OperatorKey(op),
+//     Fr(~comm), Fr(~sk_comm) ]
+//   --[
+//       Eq(verify(sig, < 'kind27235_operator_nopayload', op, url, 'POST', time >, op), true),
+//       CommunityProvisioned(~comm, host, op),
+//       ProvisionAccepted(op, host, owner),
+//       OwnerBootstrapped(owner, ~comm, host, op),
+//       HostBound(host, ~comm)
+//     ]->
+//   [
+//       !Community(~comm), !CommunitySigningKey(~comm, ~sk_comm),
+//       !HostCommunity(host, ~comm), AuditHead(~comm, 'genesis'),
+//       !Admitted(owner, ~comm)
+//     ]
+//
+// Expected mutation result: `provision_accepts_only_operator_signed_payload`
+// goes red — the adversary intercepts the unsigned-body message, substitutes
+// its own (host, owner), and the relay emits ProvisionAccepted for a pair the
+// operator never authorized. Confirmed: falsified with an 8-step trace on
+// Tamarin 1.12.0 / Maude 3.5.1 (see docs/multi-tenant-relay.md §Mechanized
+// Verification).
+
+// MUTATION_Provision_Any_Client (DO NOT ENABLE in the real model): the relay
+// authorizes provisioning from ANY registered client key instead of the
+// operator allowlist — the RELAY_OPERATOR_PUBKEYS gate replaced by "any valid
+// signature". Modeled by swapping the `!OperatorKey(op)` premise for
+// `!ClientPublic(op)` in Relay_Provisions_Community (clients can sign the
+// operator preimage with their own key; only the allowlist premise stops the
+// relay accepting it).
+//
+// rule MUTATION_Client_Signs_Provision:
+//   [ !ClientSecret(op, sk), !ClientPublic(owner), Fr(~host), Fr(~url), Fr(~time) ]
+//   --[ ClientSignedProvision(op, ~host, owner) ]->
+//   [
+//       Out(< 'operator_provision', op, ~url, 'POST', ~time, ~host, owner,
+//             sign(< 'kind27235_operator', op, ~url, 'POST', ~time, h(< ~host, owner >) >, sk) >),
+//       Out(~host)
+//   ]
+//
+// rule MUTATION_Relay_Provisions_For_Any_Client:
+//   [ In(< 'operator_provision', op, url, 'POST', time, host, owner, sig >),
+//     !ClientPublic(op),
+//     Fr(~comm), Fr(~sk_comm) ]
+//   --[
+//       Eq(verify(sig, < 'kind27235_operator', op, url, 'POST', time, h(< host, owner >) >, op), true),
+//       CommunityProvisioned(~comm, host, op),
+//       ProvisionAccepted(op, host, owner),
+//       OwnerBootstrapped(owner, ~comm, host, op),
+//       HostBound(host, ~comm)
+//     ]->
+//   [
+//       !Community(~comm), !CommunitySigningKey(~comm, ~sk_comm),
+//       !HostCommunity(host, ~comm), AuditHead(~comm, 'genesis'),
+//       !Admitted(owner, ~comm)
+//     ]
+//
+// Expected mutation result: `provisioning_requires_operator_authorization`
+// goes red — a mere registered client (never OperatorRegistered, never
+// compromised as an operator) mints a community. Confirmed: falsified with an
+// 8-step trace on Tamarin 1.12.0 / Maude 3.5.1.
+
+// MUTATION_Rotate_Ignore_Host (DO NOT ENABLE in the real model): the relay
+// applies the owner rotation to a community OTHER than the request host's
+// binding — the operator-plane confused deputy (effect escapes the named
+// host). The real rule's `!HostCommunity(host, comm)` premise pins the
+// effect; this mutation re-binds it to an arbitrary community.
+//
+// rule MUTATION_Relay_Rotates_Owner_Other_Community:
+//   [ In(< 'operator_provision', op, url, 'POST', time, host, owner, sig >),
+//     !OperatorKey(op),
+//     !HostCommunity(host, host_comm),
+//     !Community(other_comm) ]
+//   --[
+//       Eq(verify(sig, < 'kind27235_operator', op, url, 'POST', time, h(< host, owner >) >, op), true),
+//       Neq(host_comm, other_comm),
+//       OwnerRotated(owner, other_comm, host, op),
+//       OwnerBootstrapped(owner, other_comm, host, op),
+//       RotationResolved(owner, other_comm, host, host_comm)
+//     ]->
+//   [ !Admitted(owner, other_comm) ]
+//
+// Expected mutation result: `rotation_confined_to_host_community` goes red —
+// the single RotationResolved witness carries used_comm # host_comm in one
+// rule instance (same single-witness framing as S5/S6). Confirmed: falsified
+// with a 12-step trace on Tamarin 1.12.0 / Maude 3.5.1.
+
 // ============================================================================
 // Independent per-community audit chains
 // ============================================================================
@@ -684,6 +942,44 @@ lemma cross_community_audit_splice_attempt_is_not_append:
       CrossCommunityAuditSpliceAttempt(commA, commB, prevA, prevB, forged) @ i
     ==> not (Ex #j. AuditAppended(commA, prevB, forged) @ j)"
 
+// S9: every owner bootstrap/rotation — the operator plane's only effect,
+// emitted by BOTH the provision and the rotate rule — names an
+// operator-allowlisted key. Registration (`!OperatorKey`) is the
+// RELAY_OPERATOR_PUBKEYS gate; there is intentionally NO compromise
+// disjunct: compromising an operator's secret does not put a new key on the
+// allowlist, so the claim holds unconditionally. Enabling
+// MUTATION_Provision_Any_Client (relay accepts any registered client key)
+// falsifies this.
+lemma provisioning_requires_operator_authorization:
+  "All owner comm host op #i.
+      OwnerBootstrapped(owner, comm, host, op) @ i
+    ==> (Ex #j. OperatorRegistered(op) @ j & #j < #i)"
+
+// S9 payload binding: an accepted provision's (host, owner) pair is exactly a
+// pair the named operator signed — the payload hash h(<host, owner>) in the
+// NIP-98 preimage is what forces this. An adversary who captures the
+// Authorization material can replay it (benign convergence, same pair) but
+// cannot re-target it. The disjunct admits operator-key compromise, after
+// which the adversary can sign arbitrary pairs itself. Enabling
+// MUTATION_Provision_Unsigned_Body (payload tag omitted — kalvin's finding #1
+// on PR #1657) falsifies this.
+lemma provision_accepts_only_operator_signed_payload:
+  "All op host owner #i.
+      ProvisionAccepted(op, host, owner) @ i
+    ==> (Ex #j. OperatorAuthorizedProvision(op, host, owner) @ j & #j < #i)
+      | (Ex #k. OperatorKeyCompromised(op) @ k & #k < #i)"
+
+// S9 confinement: an owner rotation lands in exactly the community bound to
+// the request's host. Same single-witness framing as the S1-host lemmas: the
+// rotate rule emits one RotationResolved(owner, used_comm, host, host_comm)
+// fact carrying both the community actually mutated and the host's binding,
+// so a counterexample is one rule instance. Enabling
+// MUTATION_Rotate_Ignore_Host falsifies this fast.
+lemma rotation_confined_to_host_community:
+  "All owner used_comm host host_comm #i.
+      RotationResolved(owner, used_comm, host, host_comm) @ i
+    ==> used_comm = host_comm"
+
 // Reachability / anti-vacuity probes.
 lemma executable_token_leak:
   exists-trace
@@ -745,4 +1041,26 @@ lemma executable_open_auth_registration:
   exists-trace
   "Ex pk comm host #i. OpenCommunityAutoRegistered(pk, comm, host) @ i"
 
+// S9 anti-vacuity probes: the operator plane's provision and rotate paths are
+// both reachable, so the S9 safety lemmas are not vacuously true.
+lemma executable_provision:
+  exists-trace
+  "Ex op host owner #i #j.
+      OperatorAuthorizedProvision(op, host, owner) @ i
+    & ProvisionAccepted(op, host, owner) @ j
+    & #i < #j"
+
+lemma executable_rotate:
+  exists-trace
+  "Ex owner comm host op #i. OwnerRotated(owner, comm, host, op) @ i"
+
+// A rotate on an already-bound host lands in the community the ORIGINAL
+// provision bound — the create-then-converge lifecycle end to end.
+lemma executable_rotate_after_provision:
+  exists-trace
+  "Ex comm host op op2 owner2 #i #j.
+      CommunityProvisioned(comm, host, op) @ i
+    & OwnerRotated(owner2, comm, host, op2) @ j
+    & #i < #j"
+
 end

docs/spec/MultiTenantRelay.tla

@@ -133,6 +133,22 @@ InitialChannelOwners == [ch \in Channels |->
 \* NoCommunity sentinel (an unmapped/unknown host) -> the connection fails closed
 \* and no channel-less write may derive a community from it.  This is the upstream
 \* of ResolveTenant: ctx.community is *derived* from the host, never free-chosen.
+\*
+\* Stated assumption (P-HOST-APPEND): HostCommunity is a CONSTANT-per-segment
+\* function even though the operator plane (POST /operator/communities) can
+\* provision new communities at runtime.  The host map is append-only —
+\* ensure_configured_community's upsert (ON CONFLICT (lower(host)) DO UPDATE
+\* SET host = EXCLUDED.host RETURNING id) returns the SAME community id for an
+\* already-bound host and no code path re-points an existing binding — so a
+\* provisioning event only extends the function's domain with a fresh
+\* host |-> community pair.  Every behavior TLC checks over the fixed
+\* HostA/HostB/HostBad harness therefore remains valid across provisioning:
+\* new hosts are new constant assignments for subsequent behavior, never
+\* mutations of the bindings modeled here.  The authorization obligations of
+\* the operator plane itself (allowlist gate, payload binding, rotation
+\* confinement) live in the Tamarin model (MultiTenantAuth.spthy S9, with the
+\* append-only assumption imported as the UniqueHostBinding restriction); see
+\* docs/multi-tenant-relay.md SS-Conformance (P-HOST-APPEND).
 HostCommunity == [h \in Hosts |->
                     CASE h = HostA -> CommA
                       [] h = HostB -> CommB