mirror of
https://github.com/block/buzz.git
synced 2026-08-18 06:50:31 +02:00
feat(conformance): runtime trace schema + independent replay checker
Adds `crates/buzz-conformance/` — the substrate for runtime formal-spec
conformance. It is the **independent oracle** for the multi-tenant relay:
given a trace of seam events recorded by the relay at runtime, the
checker asserts they obey `docs/spec/MultiTenantRelay.tla`. Production
binaries pay zero cost (the relay defaults to `NoopTracer`); test/staging
runs against `JsonlTracer` and the checker re-runs every captured trace.
Crate contents:
- `src/lib.rs` — schema: `TraceStep`, `TraceAction` (8 spec actions +
`ImplBug` for coverage-breach), `AbstractState` (resolved_community,
bound_host, actor), the `Tracer` trait, `NoopTracer` for prod.
- `src/transitions.rs` — re-implementation of the spec's `Next` relation
in Rust, used by the checker. Owned by this crate, not pulled from the
relay — that's what makes the oracle independent.
- `src/checker.rs` — replay engine: `check_trace` returns
`Err(IllegalTransition | StateMismatch | NonInterference | CoverageBreach)`
on any departure from the spec. 9 unit tests covering each failure mode
plus the M2/M8 (`claimed != resolved`) and NI/ReadConfinement bites.
- `tests/replay_fixtures.rs` + `tests/fixtures/*.jsonl` — five tests that
reconstruct three on-disk JSONL fixtures from typed Rust, assert the
committed file matches byte-for-byte (any schema change requires
`BUZZ_CONFORMANCE_UPDATE=1` to refresh), then replay each through
`check_trace`:
- `good.jsonl` → `Ok(())`
- `bad_host_channel_mismatch.jsonl` → `IllegalTransition`
- `bad_coverage_breach.jsonl` → `CoverageBreach`
- `TRACE_SCHEMA.md` — grounds every action in its `MultiTenantRelay.tla`
line and calls out the three load-bearing projection rules.
- `LIMITS.md` — honestly describes what a green run does/doesn't prove,
and the CI command listing the test surfaces.
Production-fence discipline: deps are exactly `serde / serde_json /
thiserror / uuid`. Zero `buzz-*` production crates. `CommunityLabel(Uuid)`
is a newtype in this crate, NOT `buzz_core::CommunityId` — the checker
physically cannot inherit a production bug because it shares no code
with the relay.
Verify discipline:
- `cargo test -p buzz-conformance --lib` → 9/9
- `cargo test -p buzz-conformance --test replay_fixtures` → 5/5
- Mutate→red→restore proven three times (in earlier session): row-label
corruption → `NonInterference` fires; trace `claimed = resolved` →
`IllegalTransition` vanishes; counter threshold loosened →
`ImplBug` doesn't fire.
This commit lands the substrate only. The relay-side glue
(`crates/buzz-relay/src/conformance/{mod,tracers}.rs`, `AppState.tracer`,
`EmitGuard`) and the ingest-seam emitter follow on the next branch
(`quinn/conformance-relay-glue`). The req.rs read-seam emitters land
after.
Co-authored-by: Tyler Longwell <tlongwell@block.xyz>
Signed-off-by: Tyler Longwell <tlongwell@block.xyz>
This commit is contained in:
npub1jmc9dt2lyvzu3h0kxlwxt5zg4fxp9476awyxw6gwxn72g6cw7exqs64whm
co-authored by
Tyler Longwell
Tyler Longwell
parent
7f191ccb1e
commit
caae4cdbb8
Generated
+10
@@ -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"
|
||||
|
||||
@@ -2,6 +2,7 @@
|
||||
members = [
|
||||
"crates/buzz-relay",
|
||||
"crates/buzz-core",
|
||||
"crates/buzz-conformance",
|
||||
"crates/buzz-db",
|
||||
"crates/buzz-pubsub",
|
||||
"crates/buzz-auth",
|
||||
|
||||
@@ -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<Uuid>" 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 }
|
||||
@@ -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<Uuid>`
|
||||
is enforced by the Rust compiler, not by this gate. If somebody adds
|
||||
`From<Uuid>` 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.
|
||||
@@ -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": "<uuid>", // from TenantContext::community()
|
||||
"bound_host": "<host str>", // 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.
|
||||
@@ -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<TraceStep>,
|
||||
/// 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<String>,
|
||||
}
|
||||
|
||||
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<TraceStep>) -> 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<String> = 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::<Vec<_>>()
|
||||
),
|
||||
});
|
||||
}
|
||||
|
||||
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");
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -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<Uuid>`, 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<CommunityLabel>,
|
||||
},
|
||||
/// 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<CommunityLabel>,
|
||||
},
|
||||
/// 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<CommunityLabel>,
|
||||
},
|
||||
/// 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<CommunityLabel>,
|
||||
/// 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<ChannelLabel>,
|
||||
/// 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<CommunityLabel>,
|
||||
},
|
||||
/// 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<ChannelLabel>,
|
||||
/// Per-row community labels, same rules as `ReadMessageRows`.
|
||||
row_communities: Vec<CommunityLabel>,
|
||||
},
|
||||
/// 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<CommunityLabel>,
|
||||
},
|
||||
/// 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) {}
|
||||
}
|
||||
@@ -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,
|
||||
}
|
||||
}
|
||||
@@ -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"}}
|
||||
@@ -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"}}
|
||||
@@ -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"}}
|
||||
@@ -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<TraceStep> {
|
||||
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<TraceStep> {
|
||||
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<TraceStep> {
|
||||
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<TraceStep> {
|
||||
text.lines()
|
||||
.enumerate()
|
||||
.filter(|(_, l)| !l.trim().is_empty())
|
||||
.map(|(i, l)| {
|
||||
serde_json::from_str::<TraceStep>(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::<HashSet<_>>(),
|
||||
};
|
||||
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::<HashSet<_>>(),
|
||||
};
|
||||
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:?}"
|
||||
);
|
||||
}
|
||||
Reference in New Issue
Block a user