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>
