Multi-tenant relay: spec + mechanized formal proof (S1–S8)

[tlongwell-block]

Multi-tenant relay: spec + mechanized formal proof

Spec and formal proof for moving Buzz to multi-tenant — one shared Postgres, N stateless relay processes, M communities — with machine-checked guarantees that no community can observe or act on another. This is the safety floor for going multi-tenant (Path B: community as a first-class concept, every scoped row carries a community_id). It is not the implementation and deliberately does not prove liveness/performance — that's the perf rig, later. House-style matches git-on-object-storage.md and the NIP-AB spec.

What's here

• docs/multi-tenant-relay.md (1113 lines) — the prose spec: DB setup, relay/community semantics, isolation invariants (S1–S8), conformance criteria, operational gates, and the named carve-outs.
• docs/multi-tenant-conformance.md (74 lines) — source-vs-model conformance checklist: the behaviors a single-community deployment must keep exhibiting unchanged.
• docs/spec/MultiTenantRelay.tla + .cfg — TLA+ model of cross-community isolation (S1/S2), with documented mutation blocks confirmed red.
• docs/spec/MultiTenantAuth.spthy — Tamarin model of auth/key/audit/admission (S1–S8) under a Dolev-Yao adversary.
• Community semantics threaded into the root docs: ARCHITECTURE.md, NOSTR.md, README.md, and the VISION*.md set — so the prose narrative matches the proven model.

Proof status — all machine-verified (reproduced independently on two toolchains)

• S1/S2 (TLA+ cross-community isolation): green. TLC 472,530,528 states generated / 16,226,016 distinct / 0 errors / depth 13 (8 workers, ~5m).
• S1–S8 (Tamarin auth/key/audit/admission/open-community confinement): green — 32 lemmas verified (Tamarin 1.12.0 / Maude 3.5.1).
• Non-vacuity guarded. Exists-trace witness lemmas + confirmed-red mutations (M1–M13) prove the safety lemmas assert real content, not vacuous truth.

Isolation as non-interference, not a row filter

The model proves label-flow non-interference: every state element (row, membership, projection cell, in-flight query, emitted error, audit entry) carries the community it came from, and no high-labeled value flows into a low-labeled observation. The load-bearing fence is the confused-deputy defense — the client-supplied h tag is adversary-controlled; tenancy commits on the server-resolved community_id, never the claimed one. An unmapped host fails closed (NoCommunity), recording/accepting nothing.

New surfaces proven in this revision

The model was extended past the original S1–S4 isolation/auth core to cover the host-resolved, channel-less paths the clients actually use:

• S5 (channel-less host confinement) — a profile/DM/feed/list read with no #h resolves community from the connection host and stays fenced to it.
• S7 (NIP-43 admission confinement) — a community's member-list never admits across communities.
• S8 (open-community AUTH confinement) — when a community carries no allowlist, first-AUTH auto-registration is confined to the host community.
  Each arrived with reachability probes + confirmed-red mutations (M10–M13) so the new invariant conjuncts bite rather than pass vacuously.

Confirmed-red mutations (what makes the green run mean something)

• M1 — ReadScoped answers from an unscoped/global id lookup → caught.
• M3 — WriteDuplicate conflicts on id only (drops community_id from the uniqueness key) → Safety violated at depth 3.
• M8 — the universal host/channel agreement fence dropped on the insert path (2-state trace Init → WriteInsert) and the duplicate/existence-oracle path (3-state trace) → Inv_HostBindingFence violated.
• M10–M13 — the new channel-less / open-community surfaces: dropping each host-resolution fence (raw-error leak → Safety at depth 2; unscoped channel-less read → depth 4; global admission guard IsAdmitted(c,a) → GloballyAdmitted(a)) → caught.

Metric convention: older mutations are reported as TLC search depths; the M8 fences are reported as counterexample trace lengths. Labeled explicitly in-model rather than silently normalized.

Notable — the proof caught its own author's bug

Review found a genuine vacuity bug: other_community_key_compromise_does_not_authorize bound Neq(commA, commB) to the same timepoint as CommunityKeyCompromised(commB), but no rule emits Neq there — the premise was unsatisfiable and the lemma verified vacuously (an exists-trace probe of the old premise returns "no trace found"). Fixed with a decoupled #k witness + an anti-vacuity guard (executable_other_key_compromise_plus_system_accept), making the 126-step proof genuinely non-vacuous.

Honest carve-outs (named, not hidden)

• Physical timing side-channels (buffer cache, autovacuum) — we do not claim timing non-interference.
• A leaked token is contained to its own community; blast radius isn't zero and the model says so explicitly.

Named future work (not in this PR)

Deeper O.AUTH/O.AUDIT pass · P-RESOLVE re-tenanting discipline · C1 timing carve-out pressure-test · chart-side HA closure for NIP-98 replay (Redis-backed nip98_seen seen-set vs. documenting replicaCount=1).

Verification provenance

The reviewed local tree IS the PR tree — verified mechanically, not asserted. Both gates re-run on the exact pushed tree; two independent reviewers (Max, Mari) signed off on the PR head after fetching it, confirming byte-for-byte match to the reviewed tree, trailers present, and both gates green from PR head. Branch is current with main (merged at b6bbff29); spec/model bytes unchanged across the merge so the gate results carry forward.