mirror of
https://github.com/block/buzz.git
synced 2026-11-04 00:12:02 +00:00
4720dc54c2
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>
36 lines
1.6 KiB
TOML
36 lines
1.6 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 }
|
|
|
|
# Independence rule still holds for dev-deps: proptest is a test-only
|
|
# generator harness, not a production crate, and the property tests call
|
|
# only the crate's public `check_trace` API — never the production reducer
|
|
# and never `transitions::check_step` as a parallel oracle.
|
|
[dev-dependencies]
|
|
proptest = { workspace = true }
|