mirror of
https://github.com/block/buzz.git
synced 2026-10-31 06:21:34 +00:00
e1b090e48e
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>
29 lines
1.3 KiB
TOML
29 lines
1.3 KiB
TOML
[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 }
|