Add proptest-generated action sequences exercising the conformance
checker beyond the hand-built fixtures, closing the skill's
"property/fuzz-generated action sequences where feasible" gap
(skill-runtime-formal-compliance). Test-only: no production or checker
behavior change.
The tests assert spec-derived invariants about check_trace's verdict —
NOT a parallel oracle re-deriving the verdict (which would just clone
check_step and test the code against itself). Six properties, each
honoring check_trace's fail-fast contract by constructing traces where
the targeted violation is the first/only one:
- non-interference soundness: any read (ReadMessageRows / ReadByIdRows /
ReadHostFeedRows) carrying a foreign row label is rejected
- non-interference completeness: a fully clean trace is accepted
- AuthCheck Allow + foreign claim bites IllegalTransition; Deny is in-spec
- ImplBug bites CoverageBreach
- a mid-trace state flip bites StateMismatch
- check_trace is deterministic and never panics
proptest is added as a dev-dependency only; the property tests touch
only the crate's public check_trace API and depend on no production
crate, preserving the checker's independence rule.
128 cases, trace length 1..=12. The new tests run in the existing
just test-unit gate (now 22 buzz-conformance tests, was 15) at
negligible cost.
Co-authored-by: Max <d8473ee32b973aa31a21a65adddcc4b69cc2a8a4dee8121ecd51926e0cddbc02@sprout-oss.stage.blox.sqprod.co>
Co-authored-by: Tyler Longwell <tlongwell@block.xyz>
Signed-off-by: Tyler Longwell <tlongwell@block.xyz>
The Typesense search backend was replaced by Postgres FTS in this rewrite,
but two vestiges remained in live code:
- `Config.typesense_url` / `Config.typesense_key` were still parsed from
`TYPESENSE_URL` / `TYPESENSE_API_KEY` and stored on the struct, yet read
nowhere outside config.rs. Removed the fields, env parsing, and struct init.
- Several doc/inline comments still described the search path as hitting
Typesense (req.rs NIP-50 handler, bridge.rs post-filter rationale). The
behavior is unchanged but the engine is Postgres FTS; corrected the naming
so the comments match the code.
Kept genuinely historical references intact (event.rs note that the old
index_event worker is gone; query.rs/schema provenance of the legacy
__global__ sentinel and the FTS migration).
cargo check -p buzz-relay green.
Co-authored-by: Tyler Longwell <tlongwell@block.xyz>
Signed-off-by: Tyler Longwell <tlongwell@block.xyz>
Add `crates/buzz-relay/src/conformance/` module:
- `Tracer` re-export, `NoopTracer` (production), `JsonlTracer` (test/CI).
- `EmitGuard::arm(tracer, state, kind) → (guard, counting_tracer)`:
RAII coverage breach. The guard wraps the original tracer in a
counting layer; production callers transparently use that wrapper.
If no emit reaches the wrapper before the guard drops, the guard
emits a synthetic `ImplBug` step on the underlying tracer — the
checker treats that as CoverageBreach. The wrapper design means
production paths never need to "disarm" or pass anything around;
a future new exit that forgets to emit will be caught
automatically.
- `state_for_request(tenant, actor)`: builds AbstractState. Pulls
community + host directly from server-resolved TenantContext.
- `claimed_community_from_event`: reads the event's h tag for the
trace's `claimed_community` field — recorded SEPARATELY from
`resolved_community` so M2 (claim≠resolved) and M8 (host/channel
disagreement) bite at the checker.
- `sanitized_reason_for(&IngestError) → SanitizedReason`: 1:1 map
of IngestError variants (Rejected/AuthFailed/Internal) onto the
closed SanitizedReason alphabet (Invalid/Restricted/ServerError).
Adding a fourth IngestError variant breaks this match — CI catches
it before it ships.
Emitter wiring in `crates/buzz-relay/src/handlers/ingest.rs`:
- `ingest_event` is now a thin wrapper: arms EmitGuard, calls
`ingest_event_inner`, and on Err maps to SanitizedError. All 36
early-Err returns and 6 Ok returns in the inner fn are covered
by this single outer mapping.
- At `check_channel_membership` call site (line 1401): emits
`AuthCheck { channel, claimed_community, verdict }` with
Allow on Ok, Deny on Err. The verdict basis is `tenant.community()`
server-resolved — confirmed at ingest.rs:424's `is_member_cached`
call signature (not event-derived).
- At each `dispatch_persistent_event` call site (lines 1908, 2014):
emits `WriteInsert` (channel + was_inserted=true), `WriteDuplicate`
(channel + was_inserted=false), or `WriteInsertGlobal` (no channel).
This is the entire write side of the ingest seam.
`crates/buzz-relay/src/handlers/event.rs` `dispatch_persistent_event`:
- No emit added. Documented why inline: the spec has no separate
fan-out action — acceptance is recorded at ingest's WriteInsert;
fan-out surfaces as ReadMessageRows on the subscriber side (the
read seam in req.rs, lands in the held-back additive diff).
AppState carries `tracer: Arc<dyn buzz_conformance::Tracer>`,
defaulting to NoopTracer (zero cost). Test contexts overwrite this
field with a JsonlTracer after construction.
Verify:
- cargo check -p buzz-relay green
- cargo test -p buzz-relay --lib: 378/378 (no regressions)
- cargo test -p buzz-conformance: 9/9 (checker still bites all four
failure modes)
Co-authored-by: Tyler Longwell <tlongwell@block.xyz>
Signed-off-by: Tyler Longwell <tlongwell@block.xyz>
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>
