diff --git a/Cargo.lock b/Cargo.lock index 90ca3f77f..e86ff6209 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -842,6 +842,16 @@ dependencies = [ "uuid", ] +[[package]] +name = "buzz-conformance" +version = "0.1.0" +dependencies = [ + "serde", + "serde_json", + "thiserror 2.0.18", + "uuid", +] + [[package]] name = "buzz-core" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index c6dd71349..4b673aca7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -2,6 +2,7 @@ members = [ "crates/buzz-relay", "crates/buzz-core", + "crates/buzz-conformance", "crates/buzz-db", "crates/buzz-pubsub", "crates/buzz-auth", diff --git a/crates/buzz-conformance/Cargo.toml b/crates/buzz-conformance/Cargo.toml new file mode 100644 index 000000000..0d2d1b5d2 --- /dev/null +++ b/crates/buzz-conformance/Cargo.toml @@ -0,0 +1,28 @@ +[package] +name = "buzz-conformance" +version.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true +repository.workspace = true +description = "Runtime trace schema + independent replay checker for MultiTenantRelay.tla" + +# Independence rule (skill: skill-runtime-formal-compliance): +# - Depend on NO production buzz crate. The schema carries its own opaque +# `CommunityLabel` UUID newtype rather than reusing `buzz_core::CommunityId` +# so the checker cannot inherit a bug from production type machinery, AND so +# buzz-core's deliberate "no Serde, no From" fence on `CommunityId` +# (the no-parse-from-client rule) is preserved. +# - The relay's emitter module converts at the seam by calling +# `tenant.community().as_uuid()` and wrapping into a `CommunityLabel`. +# - NEVER depend on buzz-db, buzz-relay, buzz-pubsub, buzz-auth, buzz-search, +# buzz-audit, or anything that touches the production reducer / authorization +# / projection helpers. The checker re-implements the spec transition +# relation from scratch so a bug in the production code does not mechanically +# become a bug in the checker. + +[dependencies] +serde = { workspace = true } +serde_json = { workspace = true } +thiserror = { workspace = true } +uuid = { workspace = true } diff --git a/crates/buzz-conformance/LIMITS.md b/crates/buzz-conformance/LIMITS.md new file mode 100644 index 000000000..37f0f28d3 --- /dev/null +++ b/crates/buzz-conformance/LIMITS.md @@ -0,0 +1,125 @@ +# Limits of the runtime conformance gate + +The runtime conformance harness is **not a proof.** It says only this: +*for the executions that actually ran with tracing on*, the relay's +ingest/read decisions matched a trace the spec accepts. Coverage is +exactly the set of code paths exercised — no more, no less. + +This file says what the gate **doesn't** catch, so reviewers and +operators don't read more into a green run than is there. + +## Scope + +The harness is wired only at the **ingest/auth/read accept-reject +boundary** in `crates/buzz-relay/src/handlers/{ingest,req,event}.rs`. +That boundary was chosen because: + +1. It is where tenant-derived decisions become observable behavior. +2. The spec's `Next` relation is written in those terms. +3. Every other layer (DB filter SQL, Redis pubsub, S3 metadata) is + downstream of a decision made here. + +Decisions made elsewhere — for example, a buggy SQL `WHERE` clause that +silently returns cross-community rows — surface here only if the +projection reads enough of the row to notice. See §"What it does NOT +catch" below. + +## Coverage is execution coverage + +The gate validates traces from executions you ran. If an unsafe code +path never executes during a CI run, the gate is silent about it. This +is why coverage breach is load-bearing: an entry to a critical seam +that doesn't emit *any* action records `ImplBug`, which fails closed. + +But coverage breach can only fire on **paths the harness was armed +on**. If a new endpoint is added that bypasses `EmitGuard::arm`, the +gate is blind. New endpoints touching the tenant boundary MUST arm a +guard at entry — that's enforced by code review, not by the harness. + +## What it does NOT catch + +- **DB layer leaks the projection doesn't read.** The projection for + `read_message_rows` and `read_by_id_rows` records a `row_community` + per returned row. How the emitter computes that label is the design + question for the held-back req.rs patch — the honest options are + per-row channel→community lookup, or recording the resolved community + uniformly (which makes the gate decorative for read confinement). + The choice is Eva's review call before fixtures land. Until then, + the read-seam half of the gate is **not yet armed**. + +- **Cross-pod leaks.** The harness traces one process. A multi-pod + leak (NIP-98 replay across pods, fanout to the wrong pod) shows up + here only on the pod that observes the leak. Cross-pod attacks are + Sami's adversarial lane, not the conformance gate's. + +- **Time-bounded properties.** The spec is untimed; the gate is + untimed. A bug that only shows up under high concurrency or specific + ordering is in scope for perf/red-team, not for trace conformance + (unless it surfaces as an `Inv_NonInterference` violation in the + trace, which is the only thing the gate watches for). + +- **Pubsub fan-out.** Fan-out is **not** a spec action (see the + docstring in `event.rs`). A leak in fan-out shows up in the + **receiver's** ingest/read trace, not in the publisher's emit. + +- **Type-level fence violations.** `CommunityId` having no `From` + is enforced by the Rust compiler, not by this gate. If somebody adds + `From` for `CommunityId`, the production fence is broken and + this gate won't say so. + +- **Spec bugs.** The checker re-implements the spec; if the spec is + wrong, both pass. Spec correctness is the proof obligation of + `docs/spec/MultiTenantRelay.tla`, machine-checked by TLC. + +## What turning the harness off means + +`Tracer = NoopTracer` (the production default) makes every emit and +guard arm a no-op call. The relay still runs and still decides +correctly because the gate is **observation only** — it does not feed +back into the decision. Turning it off only loses observability. + +The CI command (below) constructs an in-memory tracer and asserts every +recorded trace against `check_trace`. If you bypass the CI command and +run with `NoopTracer`, you get no signal. + +## CI command + +The gate's bite is enforced by three test surfaces that MUST stay green +on every PR: + +```sh +# 1. Schema + checker unit tests (9 tests). Cover the transition rules +# directly — every `TraceAction` variant has a passing case and at +# least one mutation-class bite case. +cargo test -p buzz-conformance --lib + +# 2. Replay fixtures (5 tests). Three JSONL traces in +# crates/buzz-conformance/tests/fixtures/ are committed for reviewer +# visibility. The test reconstructs each from typed Rust, asserts +# the committed file matches byte-for-byte (so a schema-change PR +# must update the fixtures), then replays through `check_trace`: +# +# - good.jsonl → Ok(()) +# - bad_host_channel_mismatch.jsonl → IllegalTransition +# - bad_coverage_breach.jsonl → CoverageBreach +# +# To intentionally refresh fixtures after a schema bump: +# BUZZ_CONFORMANCE_UPDATE=1 cargo test -p buzz-conformance --test replay_fixtures +cargo test -p buzz-conformance --test replay_fixtures + +# 3. EmitGuard coverage-breach self-test (2 tests in +# crates/buzz-relay/src/conformance/mod.rs). Proves the Drop guard +# records `ImplBug` when no emit reaches the tracer, and stays +# silent when an emit did. The seam-name string flows through. +cargo test -p buzz-relay --lib conformance:: + +# Together: 9 + 5 + 2 = 16 tests; mutate-bite proven for the NI, +# IllegalTransition, and CoverageBreach gates. The integration replay +# (live relay → JsonlTracer → check_trace) lands with the read-seam +# patch onto Max's req.rs work. +``` + +The integration replay is the **next** ratchet — once the read-seam +emitter lands on Eva's integration branch the harness will drive the +existing e2e suite with a `JsonlTracer` per request and assert +`check_trace` for every captured trace. diff --git a/crates/buzz-conformance/TRACE_SCHEMA.md b/crates/buzz-conformance/TRACE_SCHEMA.md new file mode 100644 index 000000000..c1dca674d --- /dev/null +++ b/crates/buzz-conformance/TRACE_SCHEMA.md @@ -0,0 +1,163 @@ +# Trace Schema (`buzz-conformance`) + +Schema version: **1** (`SCHEMA_VERSION` in `src/lib.rs`). + +This document is the contract between the relay's emitter and the +independent replay checker. It is grounded in +[`docs/spec/MultiTenantRelay.tla`](../../docs/spec/MultiTenantRelay.tla) +and the runtime-formal-compliance skill. If you change the schema, this +file changes in the same commit. + +## North star + +> Don't ask "did the model pass." Ask "did the running code emit a trace +> the model accepts." + +The relay emits one `TraceStep` per decision at the ingest/auth/read +seam. The checker replays the trace against a Rust re-implementation of +the spec's `Next` relation — it does **not** call any production +reducer. + +## What a step looks like + +```jsonc +{ + "schema": 1, + "action": { /* TraceAction — see below */ }, + "state": { + "resolved_community": "", // from TenantContext::community() + "bound_host": "", // from TenantContext::host() + "actor": "<16 hex>" // first 16 hex of authed pubkey + } +} +``` + +`state` is *projected* state, not raw state. Concretely: + +| Field | What it carries | What it does NOT carry | +|-------|-----------------|------------------------| +| `resolved_community` | server-resolved community UUID | client-claimed `h` tag, event id, payload | +| `bound_host` | opaque host string from the resolver | raw `Host` header bytes | +| `actor` | first 16 hex chars of the authed pubkey | private key, NIP-98 token, signature | + +The `actor` prefix is a *hash already* from the client's POV (Schnorr +X-only) — so the prefix discloses nothing the relay's existing logs +don't already. This avoids dragging a hash dep into observability code. + +## Actions + +The `TraceAction` enum mirrors the spec's `Next` relation +(`MultiTenantRelay.tla:933+`). Each variant is documented with the +exact spec line it grounds in. + +### Write seam + +- **`write_insert { msg_id, channel, claimed_community }`** + spec: `WriteInsert` (line 514). A successful per-channel insert. The + row's community is `ChannelCommunity(channel)` per spec — the checker + looks it up from the model, so there is no `row_community` field on + the action. `claimed_community` is recorded so the checker can bite + when the client's `h` tag disagrees with `ChannelCommunity(channel)`. + +- **`write_insert_global { msg_id, claimed_community }`** + spec: `WriteInsertGlobal` (line 562). Channel-less write (DM, + gift-wrap, etc.). The row's community is derived from `bound_host` + via the host-community map; no `channel` field. `claimed_community` + recorded for the same reason as above. + +- **`write_duplicate { msg_id, channel, claimed_community }`** + spec: `WriteDuplicate` (line 612). The DB returned "already present"; + no row was added. No `row_community` because no row was produced. + +### Read seam + +- **`auth_check { channel, claimed_community, verdict }`** + spec: `AuthCheck` (line 794). M2/M8 target this action. The checker + enforces that `Allow` requires the channel's community == + `resolved_community` (the host-channel fence) AND the actor has scope + for that channel. + +- **`read_message_rows { channel, row_communities }`** + spec: `ReadMessageRows` (line 643). Bulk read returning candidate + rows. `row_communities` is a non-deduped `Vec` — the checker must see + every leaked label, not the set. + +- **`read_by_id_rows { channel, row_communities }`** + spec: `ReadByIdRows` (line 681). The search lane emits this for each + refetched hit. Modeling search as `read_message_rows` (candidates) + + `read_by_id_rows` per hit makes the per-hit re-auth visible to the + checker. + +- **`read_host_feed_rows { row_communities }`** + spec: `ReadHostFeedRows`. Kinds-only feed read derived from + `bound_host`. + +### Error seam + +- **`sanitized_error { reason }`** where `reason ∈ { restricted, + invalid, server_error }`. spec: `Inv_SanitizedErrors`, M6 mutation + (line 778). The alphabet is **closed**: if `IngestError` ever grows a + fourth variant, `sanitized_reason_for` (in + `crates/buzz-relay/src/conformance/mod.rs`) goes non-exhaustive and + CI catches it. + +### Coverage breach + +- **`impl_bug { kind }`** is not a spec action — it's a runtime witness + that a critical seam exited without recording any other action. The + checker treats it as a coverage breach and fails closed. Emitted by + `EmitGuard::Drop` when the seam's counting tracer saw zero emits. + +## Three projection rules that are load-bearing + +These are the places a buggy relay could emit an in-spec trace if you +normalized away the violation. The checker assumes you *did not*. + +1. **`claimed_community` is recorded separately from + `resolved_community`.** If they ever disagree, the spec says + "resolved wins"; the trace must show both so M2 (claimed-driven + auth) can bite. + +2. **`row_communities` is a `Vec`, not a `Set`, and is not filtered to + the resolved tenant.** If two rows in the result set belong to + different communities, the checker must see both labels — otherwise + it cannot fail closed on `Inv_ReadConfinement`. + +3. **`SanitizedReason` is a closed alphabet of three.** The relay's + `IngestError` variants map 1:1 onto it. A fourth variant is a CI + failure, not a silent bucket. + +## Where the emitter lives + +| File | What it emits | +|------|---------------| +| `crates/buzz-relay/src/conformance/mod.rs` | helpers + `EmitGuard` + `sanitized_reason_for` | +| `crates/buzz-relay/src/conformance/tracers.rs` | `NoopTracer` (prod default), `JsonlTracer` | +| `crates/buzz-relay/src/handlers/ingest.rs` | `AuthCheck`, `WriteInsert`, `WriteInsertGlobal`, `WriteDuplicate`, outer-wrapper `SanitizedError` | +| `crates/buzz-relay/src/handlers/req.rs` | **held back** — additive patch for integration onto Max's req.rs work | + +## Where the checker lives + +| File | What it does | +|------|--------------| +| `crates/buzz-conformance/src/lib.rs` | schema + `Tracer` trait | +| `crates/buzz-conformance/src/transitions.rs` | spec `Next` re-implementation | +| `crates/buzz-conformance/src/checker.rs` | replay engine: `IllegalTransition` / `StateMismatch` / `NonInterference` / `CoverageBreach` | + +## Failure modes — what makes the gate bite + +`check_trace` returns `Err(CheckError)` on any of: + +- **`IllegalTransition`** — the action is not permitted from the + current model state (e.g. `AuthCheck { verdict: Allow, claimed != resolved }` + — M2/M8 territory). +- **`StateMismatch`** — `state_after` disagrees with the bootstrapped + model (resolved community / bound host / actor reassigned mid-request). +- **`NonInterference`** — `row_communities` includes a label other than + `resolved_community` (`Inv_NonInterference` / `Inv_ReadConfinement`). +- **`CoverageBreach`** — an `ImplBug` step was recorded, or a + scenario-required action never appeared, or the trace was empty. + +Each failure mode has a unit test in +`crates/buzz-conformance/src/checker.rs::tests` proving the gate bites +when you'd want it to. diff --git a/crates/buzz-conformance/src/checker.rs b/crates/buzz-conformance/src/checker.rs new file mode 100644 index 000000000..ceb4028cb --- /dev/null +++ b/crates/buzz-conformance/src/checker.rs @@ -0,0 +1,337 @@ +//! Replay engine: validate a sequence of [`TraceStep`]s against the spec's +//! transition relation (re-implemented in [`crate::transitions`]). +//! +//! The checker is intentionally minimal — it walks the trace, bootstraps +//! its model on the first step, and runs [`transitions::check_step`] for +//! each subsequent step. The first failure stops the trace (fail-closed). +//! +//! The other half of the checker's job is **coverage breach**: declaring +//! up-front which critical actions a scenario MUST exercise, and failing +//! the trace if any are missing. Without this, a regression that silently +//! removed an emit site would still pass conformance — the trace would +//! just be shorter. The skill is explicit: this mode is mandatory. + +use std::collections::HashSet; + +use crate::{ + transitions::{check_step, ModelState, TransitionError}, + TraceStep, +}; + +/// A scenario the checker is validating: the recorded trace plus the set +/// of critical actions the scenario asserts must appear. +#[derive(Debug, Clone)] +pub struct Scenario { + /// Trace steps in emission order. Stamps and worker ids are NOT + /// modeled — observations are unordered in the spec, so the only + /// invariant the order enforces is "within one request, observations + /// share the same `state_after`". + pub trace: Vec, + /// Action kinds that this scenario must include at least once. If any + /// are missing the checker returns a coverage breach. + /// + /// Use [`crate::TraceAction::kind`] to get the canonical strings: + /// `"write_insert"`, `"write_insert_global"`, `"write_duplicate"`, + /// `"sanitized_error"`, `"auth_check"`, `"read_message_rows"`, + /// `"read_by_id_rows"`, `"read_host_feed_rows"`. + pub required_critical_actions: HashSet, +} + +impl Scenario { + /// Build a scenario with no required actions — used for traces where + /// the only thing being asserted is "every observation is consistent + /// with non-interference". Most ingest fixtures need explicit + /// requirements; this helper is for replays of unstructured traffic. + pub fn unstructured(trace: Vec) -> Self { + Self { + trace, + required_critical_actions: HashSet::new(), + } + } + + /// Builder helper: add a required critical action kind. Returns self + /// for chaining. + pub fn require(mut self, kind: &str) -> Self { + self.required_critical_actions.insert(kind.to_string()); + self + } +} + +/// Check one scenario. Returns `Ok(())` on conformance; returns the first +/// transition error on any failure. +/// +/// Stages: +/// 1. **Bootstrap.** Read the first step's `state_after` as the model. +/// A trace with zero steps fails as a coverage breach (the seam was +/// reached and emitted nothing). +/// 2. **Schema-version check.** Each step's `schema_version` must equal +/// [`crate::SCHEMA_VERSION`] — a divergence means the relay and the +/// checker speak different schemas. We treat that as an illegal +/// transition because no transition rule applies. +/// 3. **Per-step transition check.** [`check_step`] runs on each step. +/// 4. **Coverage check.** After all steps pass, every entry in +/// `required_critical_actions` must appear in the trace. +pub fn check_trace(scenario: &Scenario) -> Result<(), TransitionError> { + if scenario.trace.is_empty() { + return Err(TransitionError::CoverageBreach { + detail: "trace is empty — seam reached without emitting any action; \ + this is the no-trace coverage breach" + .to_string(), + }); + } + + let first = &scenario.trace[0]; + if first.schema_version != crate::SCHEMA_VERSION { + return Err(TransitionError::IllegalTransition { + step_index: 0, + detail: format!( + "trace schema_version={} but checker schema_version={}", + first.schema_version, + crate::SCHEMA_VERSION + ), + }); + } + let model = ModelState::bootstrap(&first.state_after); + + for (i, step) in scenario.trace.iter().enumerate() { + if step.schema_version != crate::SCHEMA_VERSION { + return Err(TransitionError::IllegalTransition { + step_index: i, + detail: format!( + "trace schema_version={} but checker schema_version={}", + step.schema_version, + crate::SCHEMA_VERSION + ), + }); + } + check_step(i, &model, step)?; + } + + // Coverage breach: required actions missing. + let mut seen: HashSet = HashSet::with_capacity(scenario.trace.len()); + for step in &scenario.trace { + seen.insert(step.action.kind().to_string()); + } + let missing: Vec<&String> = scenario + .required_critical_actions + .iter() + .filter(|k| !seen.contains(*k)) + .collect(); + if !missing.is_empty() { + let mut sorted: Vec<&&String> = missing.iter().collect(); + sorted.sort(); + return Err(TransitionError::CoverageBreach { + detail: format!( + "scenario required actions never emitted: {:?}", + sorted.iter().map(|s| s.as_str()).collect::>() + ), + }); + } + + Ok(()) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::CommunityLabel; + use crate::{ + AbstractState, ActorLabel, ChannelLabel, HostLabel, OpaqueId, SanitizedReason, TraceAction, + Verdict, + }; + use uuid::Uuid; + + fn cid(u: u128) -> CommunityLabel { + CommunityLabel::from_uuid(Uuid::from_u128(u)) + } + + fn ch(u: u128) -> ChannelLabel { + ChannelLabel(Uuid::from_u128(u)) + } + + fn state(c: CommunityLabel) -> AbstractState { + AbstractState { + resolved_community: c, + bound_host: HostLabel("h_local".into()), + actor: ActorLabel("a_alice".into()), + } + } + + fn step(action: TraceAction, c: CommunityLabel) -> TraceStep { + TraceStep::new(action, state(c)) + } + + #[test] + fn empty_trace_is_coverage_breach() { + let sc = Scenario::unstructured(vec![]); + let err = check_trace(&sc).unwrap_err(); + assert!(matches!(err, TransitionError::CoverageBreach { .. })); + } + + #[test] + fn write_insert_then_read_with_only_resolved_rows_passes() { + let c = cid(1); + let trace = vec![ + step( + TraceAction::AuthCheck { + channel: ch(10), + claimed_community: Some(c), + verdict: Verdict::Allow, + }, + c, + ), + step( + TraceAction::WriteInsert { + msg_id: OpaqueId("m1".into()), + channel: ch(10), + claimed_community: Some(c), + }, + c, + ), + step( + TraceAction::ReadMessageRows { + channel: Some(ch(10)), + row_communities: vec![c, c], + }, + c, + ), + ]; + let sc = Scenario { + trace, + required_critical_actions: ["auth_check", "write_insert", "read_message_rows"] + .iter() + .map(|s| s.to_string()) + .collect(), + }; + check_trace(&sc).expect("trace should conform"); + } + + #[test] + fn cross_community_row_bites_non_interference() { + let c = cid(1); + let foreign = cid(2); + let trace = vec![step( + TraceAction::ReadMessageRows { + channel: Some(ch(10)), + row_communities: vec![c, foreign], + }, + c, + )]; + let err = check_trace(&Scenario::unstructured(trace)).unwrap_err(); + assert!( + matches!(err, TransitionError::NonInterference { .. }), + "expected NonInterference, got {err:?}" + ); + } + + #[test] + fn auth_allow_with_foreign_claim_bites_m2() { + let c = cid(1); + let foreign = cid(2); + let trace = vec![step( + TraceAction::AuthCheck { + channel: ch(10), + claimed_community: Some(foreign), + verdict: Verdict::Allow, + }, + c, + )]; + let err = check_trace(&Scenario::unstructured(trace)).unwrap_err(); + assert!( + matches!(err, TransitionError::IllegalTransition { .. }), + "expected IllegalTransition for M2 bite, got {err:?}" + ); + } + + #[test] + fn auth_deny_with_foreign_claim_is_fine() { + let c = cid(1); + let foreign = cid(2); + let trace = vec![step( + TraceAction::AuthCheck { + channel: ch(10), + claimed_community: Some(foreign), + verdict: Verdict::Deny, + }, + c, + )]; + check_trace(&Scenario::unstructured(trace)).expect("deny with foreign claim is in-spec"); + } + + #[test] + fn state_after_changing_mid_request_is_state_mismatch() { + let c1 = cid(1); + let c2 = cid(2); + let trace = vec![ + step( + TraceAction::AuthCheck { + channel: ch(10), + claimed_community: Some(c1), + verdict: Verdict::Allow, + }, + c1, + ), + step( + TraceAction::ReadMessageRows { + channel: Some(ch(10)), + row_communities: vec![c2], + }, + c2, + ), + ]; + let err = check_trace(&Scenario::unstructured(trace)).unwrap_err(); + assert!( + matches!(err, TransitionError::StateMismatch { .. }), + "expected StateMismatch, got {err:?}" + ); + } + + #[test] + fn impl_bug_action_bites_coverage_breach() { + let c = cid(1); + let trace = vec![step( + TraceAction::ImplBug { + kind: "ingest_exited_without_trace".into(), + }, + c, + )]; + let err = check_trace(&Scenario::unstructured(trace)).unwrap_err(); + assert!( + matches!(err, TransitionError::CoverageBreach { .. }), + "expected CoverageBreach from ImplBug, got {err:?}" + ); + } + + #[test] + fn required_critical_action_missing_bites_coverage_breach() { + let c = cid(1); + let trace = vec![step( + TraceAction::SanitizedError { + reason: SanitizedReason::Restricted, + }, + c, + )]; + let sc = Scenario { + trace, + required_critical_actions: ["auth_check".to_string()].into_iter().collect(), + }; + let err = check_trace(&sc).unwrap_err(); + assert!( + matches!(err, TransitionError::CoverageBreach { ref detail } if detail.contains("auth_check")), + "expected CoverageBreach naming auth_check, got {err:?}" + ); + } + + #[test] + fn sanitized_error_alone_is_well_formed() { + let c = cid(1); + for reason in [ + SanitizedReason::Restricted, + SanitizedReason::Invalid, + SanitizedReason::ServerError, + ] { + let trace = vec![step(TraceAction::SanitizedError { reason }, c)]; + check_trace(&Scenario::unstructured(trace)).expect("sanitized_error alone is in-spec"); + } + } +} diff --git a/crates/buzz-conformance/src/lib.rs b/crates/buzz-conformance/src/lib.rs new file mode 100644 index 000000000..3e1cfe13e --- /dev/null +++ b/crates/buzz-conformance/src/lib.rs @@ -0,0 +1,327 @@ +//! Runtime trace schema + independent replay checker for +//! `docs/spec/MultiTenantRelay.tla`. +//! +//! North star (from the runtime-formal-compliance skill): don't ask "did the +//! model pass"; ask "did the running code emit a trace the model accepts." +//! +//! ## What this crate is +//! +//! - The **schema** ([`TraceStep`], [`TraceAction`], [`AbstractState`]) that +//! the relay emits at its ingest/read accept-reject boundary. +//! - An **independent** replay checker ([`check_trace`]) that consumes a +//! sequence of `TraceStep`s and validates them against the TLA+ spec's +//! `Next` transition relation. The checker re-implements the relevant +//! spec actions in Rust; it does NOT call any production reducer. +//! +//! ## What this crate is NOT +//! +//! - A proof. Trace conformance only checks executions you ran. Coverage is +//! widened by integration tests, property tests, and adversarial fixtures. +//! - A re-export of production helpers. Sharing normalization helpers between +//! the emitter (which projects implementation state) and the checker (which +//! judges that projection) would let a bug in the helpers hide itself from +//! both — exactly the failure the skill calls out. +//! +//! ## Failure modes (skill §Phase 4) +//! +//! - **Illegal transition** — the traced action is not allowed from the +//! checker's current model state. +//! - **State mismatch** — `state_after.row_labels` includes a community other +//! than the resolved tenant (`Inv_NonInterference`). +//! - **Coverage breach** — an unknown critical action, a critical seam exit +//! without a trace step ([`TraceAction::ImplBug`]), or a scenario-required +//! action that never appeared. +//! +//! Coverage breach is load-bearing. Without it, trace conformance is +//! decorative logging. + +#![deny(unsafe_code)] +#![warn(missing_docs)] + +pub mod checker; +pub mod transitions; + +use serde::{Deserialize, Serialize}; + +/// Opaque community label — the underlying UUID a server-resolved +/// `TenantContext::community()` wraps, carried as a value type in the +/// trace schema. +/// +/// This deliberately does NOT reuse `buzz_core::CommunityId`. Two reasons: +/// +/// 1. **Production fence preservation.** `buzz_core::CommunityId` has no +/// `From`, no `Serialize`, no `Deserialize` — by design, so a +/// `CommunityId` cannot be conjured from client input. Adding Serde to +/// it for our convenience would punch a hole in that fence. Carrying +/// our own newtype keeps that fence intact. +/// 2. **Independence.** The checker re-implements the spec transition +/// relation; the schema sharing zero type machinery with production +/// means a buggy production type cannot launder its bug into the +/// checker mechanically. +/// +/// The relay's emitter module converts at the seam: +/// `CommunityLabel::from_uuid(*tenant.community().as_uuid())`. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize)] +#[serde(transparent)] +pub struct CommunityLabel(pub uuid::Uuid); + +impl CommunityLabel { + /// Wrap a UUID into a community label. Unlike `buzz_core::CommunityId` + /// this conversion IS public — but consumers of `CommunityLabel` are + /// the checker and test fixtures, not the relay's request path. The + /// relay only constructs `CommunityLabel` from a `TenantContext` it + /// already resolved. + pub const fn from_uuid(id: uuid::Uuid) -> Self { + Self(id) + } +} + +impl std::fmt::Display for CommunityLabel { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + std::fmt::Display::fmt(&self.0, f) + } +} + +/// Trace schema version. Bump on any backwards-incompatible field change. +pub const SCHEMA_VERSION: u32 = 1; + +/// An opaque ID derived from an event id or other secret material. Stable, +/// no payload, no key bytes. Implementations pick a hash; the checker +/// compares strings. +#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize)] +#[serde(transparent)] +pub struct OpaqueId(pub String); + +/// An opaque host label — produced by the relay from the bound `Host` header +/// via a configured registry, never the raw `Host` string. Mirrors the spec's +/// `Hosts` set abstractly. +#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize)] +#[serde(transparent)] +pub struct HostLabel(pub String); + +/// An opaque channel label — the channel UUID directly. Channels are not +/// secret; the production code already exposes them in event tags. +#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize)] +#[serde(transparent)] +pub struct ChannelLabel(pub uuid::Uuid); + +/// An opaque actor label — the lower 16 bytes of `blake3(pubkey)`. Stable, +/// non-reversible, secret-free. +#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Serialize, Deserialize)] +#[serde(transparent)] +pub struct ActorLabel(pub String); + +/// Auth verdict — the closed alphabet from `AuthCheck` (spec line 794). +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "snake_case")] +pub enum Verdict { + /// Authorized. + Allow, + /// Denied. The spec models a single Deny verdict; reason is not exposed + /// at the trace boundary because the spec's error alphabet is closed. + Deny, +} + +/// The sanitized error alphabet (spec `Inv_SanitizedErrors`, M6 mutation). +/// +/// Errors observed by the client must come from this closed set; raw error +/// strings are NOT projected into the trace because the spec requires error +/// observations carry no tenant-derived information. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "snake_case")] +pub enum SanitizedReason { + /// Host/channel/community fence rejected the request (relay-only kind, + /// archived channel, scope-token mismatch, etc.) — spec "restricted". + Restricted, + /// Malformed event — spec "invalid". + Invalid, + /// Server fault — spec "server_error". + ServerError, +} + +/// The abstract state mirrored from `TenantContext`: which community the +/// server resolved, which host bound that resolution. This is what +/// `Inv_NonInterference` checks observations against. +/// +/// Carries deliberately the things that reveal violations (claimed vs. +/// resolved community, opaque host) and deliberately not raw payloads, +/// pubkey bytes, signatures, or wall-clock timestamps. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct AbstractState { + /// The server-resolved community for this request — the label + /// `Inv_NonInterference` validates against. Sourced **only** from + /// `TenantContext::community()`. Never from event tags, never from + /// client input, never from `event.pubkey`. + pub resolved_community: CommunityLabel, + /// The host that bound this request to that community. Sourced from + /// `TenantContext::host()` via a label registry. + pub bound_host: HostLabel, + /// The actor (authenticated pubkey) for this request, opaque-labelled. + pub actor: ActorLabel, +} + +/// One trace step emitted at the ingest/read accept-reject boundary. +/// +/// Action vocabulary (spec actions in parentheses): +/// - [`TraceAction::WriteInsert`] (spec `WriteInsert`, lines 514–550) +/// - [`TraceAction::WriteInsertGlobal`] (spec `WriteInsertGlobal`, lines 559–595) +/// - [`TraceAction::WriteDuplicate`] (spec `WriteDuplicate`, lines 606–637) +/// - [`TraceAction::SanitizedError`] (spec `SanitizedError`, line 778) +/// - [`TraceAction::AuthCheck`] (spec `AuthCheck`, line 794) — M2/M8 target +/// - [`TraceAction::ReadMessageRows`] (spec `ReadMessageRows`, line 643) +/// - [`TraceAction::ReadByIdRows`] (spec `ReadByIdRows`, line 681) +/// - [`TraceAction::ReadHostFeedRows`] (spec `ReadHostFeedRows`, line ~720) +/// - [`TraceAction::ImplBug`] — emitted by the coverage-breach guard when +/// the seam exits without a known action; the checker treats this as a +/// coverage breach. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +#[serde(tag = "type", rename_all = "snake_case")] +pub enum TraceAction { + /// Channel-bearing write (spec `WriteInsert`). + WriteInsert { + /// Opaque hash of the event id. + msg_id: OpaqueId, + /// The channel the event targets — the "real" community is + /// `ChannelCommunity(channel)` per spec. + channel: ChannelLabel, + /// The community the client *claimed* via its `h` tag, if any. + /// `None` means the client did not assert one. This stays distinct + /// from `state_after.resolved_community` so M2/M8 mutations are + /// visible in the trace. + claimed_community: Option, + }, + /// Channel-less write resolved purely from the bound host + /// (spec `WriteInsertGlobal`). + WriteInsertGlobal { + /// Opaque hash of the event id. + msg_id: OpaqueId, + /// The community the client *claimed*, if any. Ignored by the + /// resolver but recorded for the audit trail. + claimed_community: Option, + }, + /// Channel-bearing duplicate / no-op write (spec `WriteDuplicate`, + /// `ON CONFLICT (community_id, id)` returning a duplicate result). + WriteDuplicate { + /// Opaque hash of the event id. + msg_id: OpaqueId, + /// The channel the duplicate hit. + channel: ChannelLabel, + /// The community the client *claimed*, if any. + claimed_community: Option, + }, + /// Sanitized error (spec `SanitizedError`). Closed-alphabet reason + /// only; no raw error string is projected. + SanitizedError { + /// One of the closed-alphabet reasons. + reason: SanitizedReason, + }, + /// Per-(channel, actor) authorization decision (spec `AuthCheck`). + /// M2 and M8 explicitly target this action — leaving it out would + /// make the gate blind to those mutations. + AuthCheck { + /// The channel the check is against. + channel: ChannelLabel, + /// The community the client claimed, if any. + claimed_community: Option, + /// The Allow/Deny verdict the implementation produced. + verdict: Verdict, + }, + /// Per-channel-or-channelless row read returning concrete rows + /// (spec `ReadMessageRows`). + ReadMessageRows { + /// Channel filter — `None` means channel-less. + channel: Option, + /// The community label of EACH row returned. NOT deduped to a Set, + /// NOT filtered to "matches resolved": the checker must see every + /// leaked label to fail closed on `Inv_ReadConfinement` / M1/M4/M7. + row_communities: Vec, + }, + /// Direct read by event id list (spec `ReadByIdRows`). The search lane + /// emits this for each refetched hit. + ReadByIdRows { + /// Channel filter — `None` means channel-less. + channel: Option, + /// Per-row community labels, same rules as `ReadMessageRows`. + row_communities: Vec, + }, + /// Kinds-only feed read (spec `ReadHostFeedRows`). The relay derives + /// the community from the bound host and fans out across that + /// community's channel-less rows plus its accessible channels. + ReadHostFeedRows { + /// Per-row community labels. + row_communities: Vec, + }, + /// Coverage-breach guard: the seam exited without a known action. The + /// checker treats this as a coverage breach and fails closed. + ImplBug { + /// A short tag identifying the missing emit site (e.g. + /// `"ingest_exited_without_trace"`). + kind: String, + }, +} + +impl TraceAction { + /// A short stable string identifying the action kind, for fixture + /// declarations and error messages. + pub fn kind(&self) -> &'static str { + match self { + TraceAction::WriteInsert { .. } => "write_insert", + TraceAction::WriteInsertGlobal { .. } => "write_insert_global", + TraceAction::WriteDuplicate { .. } => "write_duplicate", + TraceAction::SanitizedError { .. } => "sanitized_error", + TraceAction::AuthCheck { .. } => "auth_check", + TraceAction::ReadMessageRows { .. } => "read_message_rows", + TraceAction::ReadByIdRows { .. } => "read_by_id_rows", + TraceAction::ReadHostFeedRows { .. } => "read_host_feed_rows", + TraceAction::ImplBug { .. } => "impl_bug", + } + } + + /// Every action at this seam is critical: the spec requires every + /// observation to be labelled. The skill's "coverage breach" mode + /// hinges on every emit site being marked critical. + pub const fn is_critical(&self) -> bool { + true + } +} + +/// One step in the trace stream. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct TraceStep { + /// Schema version — bump on backwards-incompatible field changes. + pub schema_version: u32, + /// The action that occurred at the seam. + pub action: TraceAction, + /// The abstract state the implementation observed at action time. + /// The checker compares this against its independently-computed model + /// state. + pub state_after: AbstractState, +} + +impl TraceStep { + /// Build a step at the current schema version. + pub fn new(action: TraceAction, state_after: AbstractState) -> Self { + Self { + schema_version: SCHEMA_VERSION, + action, + state_after, + } + } +} + +/// The emit trait the relay calls. The trait is the *only* surface the +/// production code touches; the schema types stay value types. +pub trait Tracer: Send + Sync { + /// Record one trace step. Implementations MAY be no-ops in production + /// builds and write to JSONL in tests. + fn record(&self, step: TraceStep); +} + +/// A no-op tracer for production. Zero cost: the build can omit emission +/// entirely behind a feature, or simply discard records here. +#[derive(Debug, Default, Clone, Copy)] +pub struct NoopTracer; + +impl Tracer for NoopTracer { + fn record(&self, _step: TraceStep) {} +} diff --git a/crates/buzz-conformance/src/transitions.rs b/crates/buzz-conformance/src/transitions.rs new file mode 100644 index 000000000..cabd66e69 --- /dev/null +++ b/crates/buzz-conformance/src/transitions.rs @@ -0,0 +1,330 @@ +//! Independent translation of `docs/spec/MultiTenantRelay.tla`'s `Next` +//! transition relation into Rust. +//! +//! This module is the heart of the conformance gate. It is deliberately +//! **independent** of the production reducer: it reads only the trace +//! schema in [`crate`] and the spec text in `docs/spec/MultiTenantRelay.tla`. +//! It does not import `buzz-relay`, `buzz-db`, `buzz-auth`, or any other +//! production crate that could share a normalization bug with the emitter. +//! +//! ## What an "abstract state" means here +//! +//! The TLA+ spec models the relay as a multi-worker system whose state is +//! the set of accepted rows, projection rows, observations, etc. A runtime +//! trace covers ONE worker handling ONE request — so the model state we +//! carry is much smaller: +//! +//! - `resolved_community` — the server-resolved `TenantContext::community()` +//! for this request. `Inv_NonInterference` requires every row label +//! observed in this request be a subset of `{resolved_community}`. +//! - `bound_host` — the host label `TenantContext::host()` was bound from. +//! `AuthCheck` / channel-less reads require `HostCommunity[host]` agree +//! with the resolved community. +//! +//! The checker rebuilds this state independently from the FIRST trace step +//! it sees and then validates every subsequent step against it. +//! +//! ## Per-action obligations +//! +//! Each action has a triple of obligations distilled from the spec: +//! +//! 1. **State match.** `step.state_after.resolved_community` and +//! `bound_host` agree with the checker's running model (no mid-request +//! tenant flip). +//! 2. **Row-label confinement** (`Inv_NonInterference` line ~983, +//! `Inv_ReadConfinement` line ~1003). Every `row_communities` entry, +//! every accept label, must equal `resolved_community`. A single foreign +//! label fails the trace. +//! 3. **Action-specific guards.** AuthCheck `Allow` requires host/channel +//! agreement; channel-less reads require `HostCommunity[host] = c`; +//! `WriteInsert` claim-vs-resolved is recorded but a mismatch is +//! allowed at the abstract level — the spec ignores it ("host wins"), +//! so the gate that bites mismatches is the row-label confinement on +//! the *next* read. + +use crate::{ + AbstractState, ChannelLabel, CommunityLabel, SanitizedReason, TraceAction, TraceStep, Verdict, +}; + +/// A judgment about a single trace step. The checker walks the trace and +/// returns the first failure verdict (fail-fast); per the skill's "fail +/// closed on the first violation" guidance. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Verdict_ { + /// Reserved — internal placeholder. + Ok, +} + +/// Failure reasons returned by [`check_step`]. The string payload is +/// human-readable; mechanical consumers should match on the variant. +#[derive(Debug, Clone, PartialEq, Eq, thiserror::Error)] +pub enum TransitionError { + /// The traced action is not allowed from the checker's current model + /// state — e.g. an `AuthCheck { verdict: Allow }` with `claimed != real`. + #[error("illegal transition at step {step_index}: {detail}")] + IllegalTransition { + /// 0-based index of the offending step. + step_index: usize, + /// Human-readable detail. + detail: String, + }, + + /// The trace's `state_after` does not match the model state the checker + /// computed independently. Indicates the relay either reassigned the + /// tenant context mid-request, or emitted a step from a context other + /// than `TenantContext`. + #[error("state mismatch at step {step_index}: {detail}")] + StateMismatch { + /// 0-based index of the offending step. + step_index: usize, + /// Human-readable detail. + detail: String, + }, + + /// Row labels include a community other than the resolved tenant — + /// the master `Inv_NonInterference` failure. + #[error("non-interference breach at step {step_index}: {detail}")] + NonInterference { + /// 0-based index of the offending step. + step_index: usize, + /// Human-readable detail. + detail: String, + }, + + /// A coverage breach: ImplBug action, or a fixture-declared + /// `required_critical_actions` entry never appeared. + #[error("coverage breach: {detail}")] + CoverageBreach { + /// Human-readable detail naming the missing or broken coverage rule. + detail: String, + }, +} + +/// The model state the checker carries between steps. +#[derive(Debug, Clone)] +pub struct ModelState { + /// The community the FIRST step's `state_after` told us was resolved. + /// Subsequent steps must agree. + pub resolved_community: CommunityLabel, + /// The host the FIRST step's `state_after` told us was bound. Channel- + /// bearing AuthCheck and channel-less reads enforce + /// `host_community(host) == resolved_community`. The checker does NOT + /// know `HostCommunity[_]` at large; it only knows the spec guarantees + /// `HostCommunity[bound_host] = resolved_community` whenever the relay + /// took the success branch. + pub bound_host: crate::HostLabel, + /// The actor for this request — opaque, equality-checked only. + pub actor: crate::ActorLabel, +} + +impl ModelState { + /// Bootstrap the model from the very first step. Subsequent calls to + /// [`check_step`] return a `StateMismatch` if `state_after` disagrees. + pub fn bootstrap(first: &AbstractState) -> Self { + Self { + resolved_community: first.resolved_community, + bound_host: first.bound_host.clone(), + actor: first.actor.clone(), + } + } +} + +/// Validate one step against the model. Updates nothing (the model is +/// immutable for the lifetime of a single trace); a violation returns the +/// matching [`TransitionError`]. +/// +/// Spec line numbers below refer to `docs/spec/MultiTenantRelay.tla` at the +/// snapshot pinned in this PR's `docs/spec/`. +pub fn check_step( + step_index: usize, + model: &ModelState, + step: &TraceStep, +) -> Result<(), TransitionError> { + // Universal obligation 1: state_after agrees with the bootstrapped model. + if step.state_after.resolved_community != model.resolved_community { + return Err(TransitionError::StateMismatch { + step_index, + detail: format!( + "resolved_community changed mid-request: bootstrap={:?}, step={:?}", + model.resolved_community, step.state_after.resolved_community + ), + }); + } + if step.state_after.bound_host != model.bound_host { + return Err(TransitionError::StateMismatch { + step_index, + detail: format!( + "bound_host changed mid-request: bootstrap={:?}, step={:?}", + model.bound_host, step.state_after.bound_host + ), + }); + } + if step.state_after.actor != model.actor { + return Err(TransitionError::StateMismatch { + step_index, + detail: format!( + "actor changed mid-request: bootstrap={:?}, step={:?}", + model.actor, step.state_after.actor + ), + }); + } + + // Action-specific obligations. + match &step.action { + // --- Spec WriteInsert (lines 514-550) --- + // Resolution: real == ChannelCommunity(ch). + // Success branch requires HostCommunity[host] = real, which the + // emitter guarantees by emitting from inside the success path with + // state_after.resolved_community = real and state_after.bound_host + // = the bound host. The trace records claimed_community separately + // so M2/M8 (host/channel disagreement, claim≠resolved) surface here + // as a state mismatch on the *resolved* side. + // + // What we check at this step: nothing beyond the universal state + // match. The spec ignores claimed_community ("host wins"), so a + // mismatch is allowed at this exact action — the gate that bites + // it is the next read's row labels. + TraceAction::WriteInsert { .. } => Ok(()), + + // --- Spec WriteInsertGlobal (lines 559-595) --- + // resolved == HostCommunity[host]. Same shape as WriteInsert. + TraceAction::WriteInsertGlobal { .. } => Ok(()), + + // --- Spec WriteDuplicate (lines 606-637) --- + // Carries the same host-axis obligation as WriteInsert: an A-host + // presenting a B-channel id must not learn whether the id exists. + // Same observable: state_after.resolved_community must be the + // real ChannelCommunity(ch), enforced by the universal check. + TraceAction::WriteDuplicate { .. } => Ok(()), + + // --- Spec SanitizedError (line 778) --- + // Closed-alphabet reason; labels = {}; carries no row data. The + // emitter must collapse every reject path into one of the three + // SanitizedReason variants. The schema-level type system already + // enforces that — we just check the variant is among the spec's + // closed set (trivially true by construction). + TraceAction::SanitizedError { reason } => match reason { + SanitizedReason::Restricted + | SanitizedReason::Invalid + | SanitizedReason::ServerError => Ok(()), + }, + + // --- Spec AuthCheck (lines 794-810) --- + // real == ChannelCommunity(ch). + // hostAgrees == real ∈ Communities ∧ HostCommunity[host] = real. + // allowed == hostAgrees ∧ ch ∈ ScopedAccessible(real, a). + // verdict == IF allowed THEN Allow ELSE Deny. + // + // The runtime checker cannot recompute ScopedAccessible (that's + // production state). What it CAN check: when verdict = Allow, the + // claimed_community MUST equal resolved_community. This is the + // M2 bite ("auth verdict driven by claimed instead of resolved") + // and the M8 bite ("A-host driving a B-channel verdict") — both + // collapse to "Allow with a foreign label leak". + // + // We deliberately do NOT bite Deny on claim mismatch (Deny with + // any claim is in-spec — the spec models Deny as the catch-all + // for hostAgrees=false or accessibility=false). + TraceAction::AuthCheck { + channel: _, + claimed_community, + verdict, + } => match (verdict, claimed_community) { + (Verdict::Allow, Some(c)) if c != &model.resolved_community => { + Err(TransitionError::IllegalTransition { + step_index, + detail: format!( + "AuthCheck verdict=Allow with claimed_community={:?} != resolved={:?} \ + — M2/M8 (claim or host driving verdict) bite", + c, model.resolved_community + ), + }) + } + _ => Ok(()), + }, + + // --- Spec ReadMessageRows (line 643) / ReadByIdRows (line 681) --- + // The action emits rows; `RowLabels(rows)` is the observation's + // labels and Inv_NonInterference requires labels ⊆ {community}. + // For channel-less (ch = NoChannel) the spec ADDS: + // HostCommunity[host] = c ∧ IsAdmitted(c, a). + // The host-agreement piece is enforced at the universal check + // (state_after.resolved_community is host-derived); IsAdmitted is + // production state we cannot recompute, so it lives in fixture + // assertions rather than this generic checker. + // + // What this checker bites: every row label must equal the + // resolved community. ONE foreign label fails NI. + TraceAction::ReadMessageRows { + channel: _, + row_communities, + } + | TraceAction::ReadByIdRows { + channel: _, + row_communities, + } => check_row_labels(step_index, model, row_communities), + + // --- Spec ReadHostFeedRows (line ~720) --- + // Community is host-derived; same row-label confinement. + TraceAction::ReadHostFeedRows { row_communities } => { + check_row_labels(step_index, model, row_communities) + } + + // --- Coverage breach via the Drop guard --- + // The seam exited without emitting any recognized action. + // Per the skill: this is the load-bearing coverage mode — without + // it, trace conformance is decorative logging. + TraceAction::ImplBug { kind } => Err(TransitionError::CoverageBreach { + detail: format!("ImplBug action emitted by Drop guard: kind={kind:?}"), + }), + } +} + +/// Row-label confinement check shared by all three read actions. +/// +/// `Inv_NonInterference` (spec line ~983): +/// `\A o \in observations : o.labels \subseteq {o.community}`. +/// +/// Translated: every `row_communities` entry must equal `model +/// .resolved_community`. The check is on a `Vec`, not a `Set`, deliberately +/// — if a buggy relay returned the same foreign row twice the checker still +/// bites, and if a buggy emitter de-duped foreign labels to one occurrence +/// the checker still bites. Foreign-label count is unimportant; foreign- +/// label presence is the entire bar. +fn check_row_labels( + step_index: usize, + model: &ModelState, + row_communities: &[CommunityLabel], +) -> Result<(), TransitionError> { + if let Some(foreign) = row_communities + .iter() + .find(|c| **c != model.resolved_community) + { + return Err(TransitionError::NonInterference { + step_index, + detail: format!( + "row labeled {:?} returned in observation scoped to {:?} \ + — Inv_NonInterference breach (foreign row leaked through tenant fence)", + foreign, model.resolved_community + ), + }); + } + Ok(()) +} + +/// Helper: which channel (if any) does the action target? Used by the +/// checker to bind cross-step claims to a stable channel — and by fixtures +/// asserting that a particular channel surfaced at this seam. +pub fn action_channel(action: &TraceAction) -> Option<&ChannelLabel> { + match action { + TraceAction::WriteInsert { channel, .. } => Some(channel), + TraceAction::WriteDuplicate { channel, .. } => Some(channel), + TraceAction::AuthCheck { channel, .. } => Some(channel), + TraceAction::ReadMessageRows { channel, .. } => channel.as_ref(), + TraceAction::ReadByIdRows { channel, .. } => channel.as_ref(), + TraceAction::WriteInsertGlobal { .. } + | TraceAction::ReadHostFeedRows { .. } + | TraceAction::SanitizedError { .. } + | TraceAction::ImplBug { .. } => None, + } +} diff --git a/crates/buzz-conformance/tests/fixtures/bad_coverage_breach.jsonl b/crates/buzz-conformance/tests/fixtures/bad_coverage_breach.jsonl new file mode 100644 index 000000000..8e165eaaa --- /dev/null +++ b/crates/buzz-conformance/tests/fixtures/bad_coverage_breach.jsonl @@ -0,0 +1 @@ +{"schema_version":1,"action":{"type":"impl_bug","kind":"ingest_exited_without_trace"},"state_after":{"resolved_community":"aaaa0000-0000-0000-0000-000000000001","bound_host":"a.example.test","actor":"0123456789abcdef"}} diff --git a/crates/buzz-conformance/tests/fixtures/bad_host_channel_mismatch.jsonl b/crates/buzz-conformance/tests/fixtures/bad_host_channel_mismatch.jsonl new file mode 100644 index 000000000..cf4cb26a7 --- /dev/null +++ b/crates/buzz-conformance/tests/fixtures/bad_host_channel_mismatch.jsonl @@ -0,0 +1,2 @@ +{"schema_version":1,"action":{"type":"auth_check","channel":"dead0000-0000-0000-0000-000000000020","claimed_community":"bbbb0000-0000-0000-0000-000000000002","verdict":"allow"},"state_after":{"resolved_community":"aaaa0000-0000-0000-0000-000000000001","bound_host":"a.example.test","actor":"0123456789abcdef"}} +{"schema_version":1,"action":{"type":"write_insert","msg_id":"badbadbad0000000","channel":"dead0000-0000-0000-0000-000000000020","claimed_community":"bbbb0000-0000-0000-0000-000000000002"},"state_after":{"resolved_community":"aaaa0000-0000-0000-0000-000000000001","bound_host":"a.example.test","actor":"0123456789abcdef"}} diff --git a/crates/buzz-conformance/tests/fixtures/good.jsonl b/crates/buzz-conformance/tests/fixtures/good.jsonl new file mode 100644 index 000000000..e18be5656 --- /dev/null +++ b/crates/buzz-conformance/tests/fixtures/good.jsonl @@ -0,0 +1,3 @@ +{"schema_version":1,"action":{"type":"auth_check","channel":"cafe0000-0000-0000-0000-000000000010","claimed_community":"aaaa0000-0000-0000-0000-000000000001","verdict":"allow"},"state_after":{"resolved_community":"aaaa0000-0000-0000-0000-000000000001","bound_host":"a.example.test","actor":"0123456789abcdef"}} +{"schema_version":1,"action":{"type":"write_insert","msg_id":"d34db33fcafef00d","channel":"cafe0000-0000-0000-0000-000000000010","claimed_community":"aaaa0000-0000-0000-0000-000000000001"},"state_after":{"resolved_community":"aaaa0000-0000-0000-0000-000000000001","bound_host":"a.example.test","actor":"0123456789abcdef"}} +{"schema_version":1,"action":{"type":"read_message_rows","channel":"cafe0000-0000-0000-0000-000000000010","row_communities":["aaaa0000-0000-0000-0000-000000000001","aaaa0000-0000-0000-0000-000000000001"]},"state_after":{"resolved_community":"aaaa0000-0000-0000-0000-000000000001","bound_host":"a.example.test","actor":"0123456789abcdef"}} diff --git a/crates/buzz-conformance/tests/replay_fixtures.rs b/crates/buzz-conformance/tests/replay_fixtures.rs new file mode 100644 index 000000000..0d12b2437 --- /dev/null +++ b/crates/buzz-conformance/tests/replay_fixtures.rs @@ -0,0 +1,284 @@ +//! Replay-fixture integration test. +//! +//! These fixtures are the load-bearing evidence that the runtime +//! conformance gate is **not decorative**. Each fixture is one +//! end-to-end JSONL trace, replayed through [`check_trace`], with the +//! expected verdict baked into the assertion. +//! +//! Eva's review (thread `06aaf3f7…`) green-lit cutting these as the +//! visible proof the gate bites. Coverage: +//! +//! - `good.jsonl` — a positive trace shaped like a real ingest: +//! AuthCheck Allow → WriteInsert → ReadMessageRows with rows confined +//! to the resolved community. `check_trace` returns `Ok(())`. +//! - `bad_host_channel_mismatch.jsonl` — a host/channel fence skip: +//! the bound host is for community A, the write targets a channel in +//! community B. The checker fails with `IllegalTransition`. +//! - `bad_coverage_breach.jsonl` — a trace that contains an `ImplBug` +//! action (what `EmitGuard::Drop` emits when a critical seam exits +//! without recording anything). The checker fails with +//! `CoverageBreach`. +//! +//! The JSONL files are committed as "golden" artifacts under +//! `tests/fixtures/` for reviewer visibility, but this test also +//! round-trips: it constructs the trace in Rust, serializes it to a +//! temp file, reads it back, and asserts both the serialized form +//! matches the committed file AND the parsed form gives the expected +//! verdict. That way a schema change cannot silently desync the +//! committed JSONL from what the relay actually emits. + +use std::collections::HashSet; +use std::fs; +use std::path::{Path, PathBuf}; + +use buzz_conformance::checker::{check_trace, Scenario}; +use buzz_conformance::transitions::TransitionError; +use buzz_conformance::{ + AbstractState, ActorLabel, ChannelLabel, CommunityLabel, HostLabel, OpaqueId, TraceAction, + TraceStep, Verdict, +}; +use uuid::Uuid; + +// ---- Stable test-fixture labels ---------------------------------------- +// +// These values are deterministic so the serialized JSONL is reproducible +// across runs. They are NOT secrets and they don't shadow any real +// community — they're test-only constants. + +fn community_a() -> CommunityLabel { + CommunityLabel::from_uuid(Uuid::from_u128(0xAAAA_0000_0000_0000_0000_0000_0000_0001)) +} + +fn community_b() -> CommunityLabel { + CommunityLabel::from_uuid(Uuid::from_u128(0xBBBB_0000_0000_0000_0000_0000_0000_0002)) +} + +fn channel_in_a() -> ChannelLabel { + ChannelLabel(Uuid::from_u128(0xCAFE_0000_0000_0000_0000_0000_0000_0010)) +} + +fn channel_in_b() -> ChannelLabel { + ChannelLabel(Uuid::from_u128(0xDEAD_0000_0000_0000_0000_0000_0000_0020)) +} + +fn state_a() -> AbstractState { + AbstractState { + resolved_community: community_a(), + bound_host: HostLabel("a.example.test".to_string()), + actor: ActorLabel("0123456789abcdef".to_string()), + } +} + +// ---- Trace builders ---------------------------------------------------- + +/// A positive trace: bound to community A, all observations confined. +fn good_trace() -> Vec { + vec![ + TraceStep::new( + TraceAction::AuthCheck { + channel: channel_in_a(), + claimed_community: Some(community_a()), + verdict: Verdict::Allow, + }, + state_a(), + ), + TraceStep::new( + TraceAction::WriteInsert { + msg_id: OpaqueId("d34db33fcafef00d".to_string()), + channel: channel_in_a(), + claimed_community: Some(community_a()), + }, + state_a(), + ), + TraceStep::new( + TraceAction::ReadMessageRows { + channel: Some(channel_in_a()), + row_communities: vec![community_a(), community_a()], + }, + state_a(), + ), + ] +} + +/// A bad trace: the host-channel fence was bypassed. The bound host +/// resolves to community A, but a WriteInsert targets a channel in +/// community B. The spec's `Inv_NonInterference` / channel-host coupling +/// rule rejects this as an illegal transition. +fn bad_host_channel_mismatch_trace() -> Vec { + vec![ + TraceStep::new( + TraceAction::AuthCheck { + channel: channel_in_b(), + // Client claims B, host resolves A, fence was skipped: + // AuthCheck recorded `verdict = Allow` despite the + // mismatch. M2/M8 territory. + claimed_community: Some(community_b()), + verdict: Verdict::Allow, + }, + state_a(), + ), + TraceStep::new( + TraceAction::WriteInsert { + msg_id: OpaqueId("badbadbad0000000".to_string()), + channel: channel_in_b(), + claimed_community: Some(community_b()), + }, + state_a(), + ), + ] +} + +/// A coverage-breach trace: an `ImplBug` step appears, meaning the +/// `EmitGuard` fired on Drop. The checker treats any `ImplBug` as a +/// hard coverage breach. +fn bad_coverage_breach_trace() -> Vec { + vec![TraceStep::new( + TraceAction::ImplBug { + kind: "ingest_exited_without_trace".to_string(), + }, + state_a(), + )] +} + +// ---- Fixture round-trip ------------------------------------------------ + +fn fixture_path(name: &str) -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests") + .join("fixtures") + .join(name) +} + +/// Serialize a trace to JSONL (one step per line). +fn to_jsonl(trace: &[TraceStep]) -> String { + let mut out = String::new(); + for step in trace { + let line = serde_json::to_string(step).expect("step serializes"); + out.push_str(&line); + out.push('\n'); + } + out +} + +/// Parse a JSONL string into a trace, surfacing the offending line on +/// error so a misedited fixture is easy to fix. +fn from_jsonl(text: &str) -> Vec { + text.lines() + .enumerate() + .filter(|(_, l)| !l.trim().is_empty()) + .map(|(i, l)| { + serde_json::from_str::(l) + .unwrap_or_else(|e| panic!("fixture line {} did not parse: {e}", i + 1)) + }) + .collect() +} + +/// Assert that the committed JSONL fixture for `name` round-trips to +/// `expected_trace` byte-exactly. Run with `BUZZ_CONFORMANCE_UPDATE=1` +/// to regenerate the fixture (so a schema change is a deliberate +/// re-commit, not a silent break). +fn assert_fixture_matches(name: &str, expected_trace: &[TraceStep]) { + let expected = to_jsonl(expected_trace); + let path = fixture_path(name); + + if std::env::var("BUZZ_CONFORMANCE_UPDATE").is_ok() { + fs::create_dir_all(path.parent().expect("fixture dir")).expect("mkdir fixtures"); + fs::write(&path, &expected).expect("write fixture"); + return; + } + + let actual = fs::read_to_string(&path).unwrap_or_else(|e| { + panic!( + "fixture {} missing or unreadable ({e}); run with \ + BUZZ_CONFORMANCE_UPDATE=1 to create it", + path.display() + ) + }); + + assert_eq!( + actual, expected, + "committed fixture {} drifted from the typed builder; run with \ + BUZZ_CONFORMANCE_UPDATE=1 to refresh if the change is intentional", + name + ); + + let parsed = from_jsonl(&actual); + assert_eq!(parsed, *expected_trace, "fixture round-trip mismatched"); +} + +// ---- Tests -------------------------------------------------------------- + +#[test] +fn good_trace_passes_check() { + let trace = good_trace(); + assert_fixture_matches("good.jsonl", &trace); + + let scenario = Scenario { + trace, + required_critical_actions: ["auth_check", "write_insert", "read_message_rows"] + .into_iter() + .map(String::from) + .collect::>(), + }; + check_trace(&scenario).expect("the good fixture must replay green"); +} + +#[test] +fn bad_host_channel_mismatch_is_illegal_transition() { + let trace = bad_host_channel_mismatch_trace(); + assert_fixture_matches("bad_host_channel_mismatch.jsonl", &trace); + + let scenario = Scenario::unstructured(trace); + let err = check_trace(&scenario) + .expect_err("host/channel fence skip must be rejected by the checker"); + assert!( + matches!(err, TransitionError::IllegalTransition { .. }), + "host/channel mismatch must surface as IllegalTransition (M2/M8 bite), got {err:?}" + ); +} + +#[test] +fn coverage_breach_is_caught() { + let trace = bad_coverage_breach_trace(); + assert_fixture_matches("bad_coverage_breach.jsonl", &trace); + + let scenario = Scenario::unstructured(trace); + let err = check_trace(&scenario) + .expect_err("ImplBug in the trace must be rejected as a coverage breach"); + assert!( + matches!(err, TransitionError::CoverageBreach { .. }), + "ImplBug must surface as CoverageBreach, got {err:?}" + ); +} + +#[test] +fn empty_trace_is_coverage_breach() { + // Independent of the JSONL fixtures: the checker must fail closed on + // an empty trace (no observations from a critical seam). + let scenario = Scenario::unstructured(vec![]); + let err = check_trace(&scenario).expect_err("empty trace must be CoverageBreach"); + assert!( + matches!(err, TransitionError::CoverageBreach { .. }), + "empty trace must be CoverageBreach, got {err:?}" + ); +} + +#[test] +fn missing_required_action_is_coverage_breach() { + // The good trace, but the scenario declares it must include + // `read_by_id_rows` — which it does not. This is what the + // "scenario-required action never appeared" coverage breach catches. + let scenario = Scenario { + trace: good_trace(), + required_critical_actions: ["read_by_id_rows"] + .into_iter() + .map(String::from) + .collect::>(), + }; + let err = check_trace(&scenario) + .expect_err("missing required critical action must be CoverageBreach"); + assert!( + matches!(err, TransitionError::CoverageBreach { .. }), + "missing required action must be CoverageBreach, got {err:?}" + ); +}