mirror of
https://github.com/block/buzz.git
synced 2026-08-18 06:50:31 +02:00
pr-1321
3
Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
|
4720dc54c2 |
test(buzz-conformance): property/fuzz traces for the replay checker
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> |
||
|
npub1jmc9dt2lyvzu3h0kxlwxt5zg4fxp9476awyxw6gwxn72g6cw7exqs64whmandTyler Longwell
|
36485ade2b |
feat(relay): emit read-row trace steps with (B) projection
Land the read-seam emitter for the runtime conformance gate. Two
emit sites, one buzz-db helper, one negative fixture.
## buzz-db: `communities_of_channels` helper
`Buzz::communities_of_channels(&[Uuid]) -> HashMap<Uuid, CommunityId>`
— batched per-channel community lookup. Used by the relay emitters to
project each row's true community label independently of the fetch
query's WHERE clause. That independence is what makes the
`Inv_NonInterference` / `Inv_ReadConfinement` bite non-vacuous: a
mutation dropping `community_id = $X` from `query_events` would
still let this helper return the row's true label and the checker
would catch the mismatch.
Channels missing from the result map are intentionally NOT mapped to
a default — callers MUST treat "channel-id not in map" as a coverage
breach, never as "use the resolved community."
## buzz-relay: projection + record helpers
`crate::conformance` gains four new items:
- `project_row_community` — single-row helper encoding the (B)
strategy: channel-less → resolved (honest, not tautological);
channel-scoped → lookup or `None` (caller fails closed).
- `RowCommunityProjection` enum — Ok(Vec<CommunityLabel>) OR
MissingLookup discriminated outcome.
- `record_read_message_rows` — non-search lane: emits
`ReadMessageRows` on Ok projection, `ImplBug { kind:
"row_community_lookup_missing" }` on MissingLookup.
- `record_read_by_id_rows` — search lane companion, same shape but
emits `ReadByIdRows`. `filter_channel` is `None` for the search
lane (search at the abstract level isn't bound to a single channel;
per-row `channel_id` carries channel identity honestly).
## req.rs wire-up: two emit sites
- Site 1 (`req.rs` non-search loop, after `query_events`): collect
distinct channel ids from the result set → `communities_of_channels`
→ `record_read_message_rows`. Production cost: one extra DB query
per request (NoopTracer short-circuits in non-conformance builds).
- Site 2 (`req.rs` search loop, after `get_events_by_ids`): same
pattern → `record_read_by_id_rows`. `handle_search_req` gains a
threaded-through `trace_state: Option<&AbstractState>` parameter.
DB-helper errors on either site fall back to an empty lookup map.
This intentionally triggers `MissingLookup` → `ImplBug` for any
channel-scoped row in the result set, surfacing the helper failure
as a coverage breach (fail-closed) rather than a silent resolved-
label substitution.
## Negative fixture: foreign-row leak
New `bad_foreign_row_leak.jsonl` + matching test. The fixture is a
`ReadMessageRows` whose row_communities contains community B while
the state is bound to community A. This is the proof artifact Eva
requested for the (B)-projection guard-rail: if the row had been
mis-projected as channel-less (defaulting to resolved A), the subset
check would have passed vacuously. By recording the row's TRUE
community independently, `Inv_NonInterference` surfaces it
immediately as `NonInterference`.
## Unit tests (conformance::tests)
Five new tests pinning every behavior:
- `project_row_communities_channelless_uses_resolved` (positive)
- `project_row_communities_channel_scoped_uses_lookup_label` (the
non-tautological correctness — lookup label, NOT resolved)
- `project_row_communities_channel_scoped_missing_is_breach` (the
guard-rail bite)
- `record_read_message_rows_missing_lookup_emits_impl_bug`
- `record_read_by_id_rows_ok_emits_read_by_id_rows`
## Mutate → red → restore (three independent bites)
1. Make `project_row_community` fall back to resolved on missing-
lookup (the tempting wrong-fix): `project_row_communities_channel_
scoped_missing_is_breach` + `record_read_message_rows_missing_
lookup_emits_impl_bug` go red with explicit messages
("missing lookup must be a breach, got Ok([...])", "expected
ImplBug coverage breach, got ReadMessageRows {...}"). Restored.
2. Make every channel-scoped row project to resolved (the
tautological projection): 4 of 9 unit tests go red — the lookup-
label, missing-breach, and record-helper tests all bite. Restored.
3. Edit the negative fixture to use community_a instead of
community_b: `foreign_row_leak_is_non_interference` reds ("foreign
row community label must be rejected by Inv_NonInterference"). The
fixture is load-bearing, not decorative. Restored.
## Test surfaces
- `cargo test -p buzz-relay --lib` → **394/0** (was 387 baseline).
- `cargo test -p buzz-conformance --lib` → 9/0.
- `cargo test -p buzz-conformance --test replay_fixtures` → **6/0**
(was 5; +foreign_row_leak).
- `cargo test -p buzz-db --lib` → 75/0 (helper compiles; DB-driven
integration coverage lives in `--include-ignored` lane on PG).
- `cargo clippy -p buzz-relay -p buzz-db -p buzz-conformance
--all-targets -- -D warnings` clean.
- `cargo fmt --all -- --check` clean.
Co-authored-by: Tyler Longwell <tlongwell@block.xyz>
Signed-off-by: Tyler Longwell <tlongwell@block.xyz>
|
||
|
npub1jmc9dt2lyvzu3h0kxlwxt5zg4fxp9476awyxw6gwxn72g6cw7exqs64whmandTyler Longwell
|
e1b090e48e |
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>
|