External/buzz
1
0
Fork 0
mirror of https://github.com/block/buzz.git synced 2026-08-18 06:50:31 +02:00
Code Issues Packages Projects Releases Wiki Activity

test(buzz-conformance): property/fuzz traces for the replay checker

Browse Source 
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>
This commit is contained in:
npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d
2026-06-28 09:28:40 -04:00
co-authored by Max Tyler Longwell
parent 1b2d8fa85e
commit 4720dc54c2
4 changed files with 489 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
Cargo.lock
Generated
+48 -1
View File
@@ -555,6 +555,21 @@ dependencies = [
"unicode-normalization",
]
[[package]]
name = "bit-set"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "08807e080ed7f9d5433fa9b275196cfc35414f66a0c79d864dc51a0d825231a3"
dependencies = [
"bit-vec",
]
[[package]]
name = "bit-vec"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5e764a1d40d510daf35e07be9eb06e75770908c27d411ee6c92109c9840eaaf7"
[[package]]
name = "bitcoin-io"
version = "0.1.4"
@@ -846,6 +861,7 @@ dependencies = [
name = "buzz-conformance"
version = "0.1.0"
dependencies = [
"proptest",
"serde",
"serde_json",
"thiserror 2.0.18",
@@ -3458,7 +3474,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "525e9ff3e1a4be2fbea1fdf0e98686a6d98b4d8f937e1bf7402245af1909e8c3"
dependencies = [
"byteorder-lite",
"quick-error",
"quick-error 2.0.1",
]
[[package]]
@@ -5922,12 +5938,16 @@ version = "1.11.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4b45fcc2344c680f5025fe57779faef368840d0bd1f42f216291f0dc4ace4744"
dependencies = [
"bit-set",
"bit-vec",
"bitflags",
"num-traits",
"rand 0.9.4",
"rand_chacha 0.9.0",
"rand_xorshift",
"regex-syntax",
"rusty-fork",
"tempfile",
"unarray",
]
@@ -6067,6 +6087,12 @@ dependencies = [
"winapi",
]
[[package]]
name = "quick-error"
version = "1.2.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0"
[[package]]
name = "quick-error"
version = "2.0.1"
@@ -6754,6 +6780,18 @@ version = "1.0.22"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d"
[[package]]
name = "rusty-fork"
version = "0.3.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cc6bf79ff24e648f6da1f8d1f011e9cac26491b619e6b9280f2b47f1774e6ee2"
dependencies = [
"fnv",
"quick-error 1.2.3",
"tempfile",
"wait-timeout",
]
[[package]]
name = "rxml"
version = "0.11.1"
@@ -8643,6 +8681,15 @@ version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
[[package]]
name = "wait-timeout"
version = "0.2.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "09ac3b126d3914f9849036f826e054cbabdc8519970b8998ddaf3b5bd3c65f11"
dependencies = [
"libc",
]
[[package]]
name = "walkdir"
version = "2.5.0"
Cargo.toml
+3
View File
@@ -102,6 +102,9 @@ futures-util = "0.3"
tokio-tungstenite = { version = "0.29", features = ["rustls-tls-webpki-roots"] }
url = "2"
# Property-based testing (dev-only)
proptest = "1"
# MCP SDK (used by buzz-dev-mcp and buzz-agent)
rmcp = { version = "1.1.0", features = ["server", "transport-io", "macros"] }
schemars = { version = "1", default-features = false }
crates/buzz-conformance/Cargo.toml
+7
View File
@@ -26,3 +26,10 @@ 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 }
crates/buzz-conformance/tests/proptest_checker.rs
+431
View File
@@ -0,0 +1,431 @@
//! Property/fuzz-generated conformance traces.
//!
//! These tests widen the checker's exercised input space beyond the hand-
//! built fixtures in `tests/fixtures/`. The skill (skill-runtime-formal-
//! compliance) calls for "property/fuzz-generated action sequences where
//! feasible"; this is that lane.
//!
//! ## Design: invariant properties, NOT a parallel oracle
//!
//! `transitions::check_step` is small and direct. A "reference oracle" that
//! re-derived the verdict would just be a copy of the checker — testing the
//! code against itself, proving nothing. So these tests do NOT re-implement
//! the verdict. They assert **spec-derived facts** about `check_trace`'s
//! result, read off the *shape of the generated trace*:
//!
//! - any read carrying a foreign row label MUST be rejected (NonInterference)
//! - a fully clean trace MUST be accepted
//! - AuthCheck Allow + foreign claim MUST bite (IllegalTransition)
//! - ImplBug MUST bite (CoverageBreach)
//! - a mid-trace state flip MUST bite (StateMismatch)
//! - the checker never panics and is deterministic
//!
//! The only checker surface these tests touch is the public
//! [`buzz_conformance::checker::check_trace`]. They never call
//! `transitions::check_step`, and they never depend on a production crate.
//!
//! ## Fail-fast discipline
//!
//! `check_trace` returns the FIRST error it finds. So every property that
//! asserts a *specific* error variant must construct traces in which the
//! targeted violation is the first/only one — otherwise an earlier
//! `StateMismatch` / `IllegalTransition` / `CoverageBreach` would mask the
//! variant under test. Each generator below is built to honor that.
use buzz_conformance::checker::{check_trace, Scenario};
use buzz_conformance::transitions::TransitionError;
use buzz_conformance::{
AbstractState, ActorLabel, ChannelLabel, CommunityLabel, HostLabel, OpaqueId, SanitizedReason,
TraceAction, TraceStep, Verdict,
};
use proptest::prelude::*;
use uuid::Uuid;
// --- Small fixed pools -----------------------------------------------------
//
// Pools are intentionally tiny (3 each) so that "foreign vs resolved"
// collisions happen with meaningful frequency. With a 3-community pool a
// randomly chosen row label is foreign ~2/3 of the time, so P1 actually
// stresses the leak path instead of almost always generating clean traces.
const POOL: u128 = 3;
fn community(i: u128) -> CommunityLabel {
CommunityLabel::from_uuid(Uuid::from_u128(
0x0c00_0000_0000_0000_0000_0000_0000_0000 + i,
))
}
fn channel(i: u128) -> ChannelLabel {
ChannelLabel(Uuid::from_u128(
0x0ca0_0000_0000_0000_0000_0000_0000_0000 + i,
))
}
fn host(i: u128) -> HostLabel {
HostLabel(format!("h_{i}"))
}
fn actor(i: u128) -> ActorLabel {
ActorLabel(format!("a_{i}"))
}
fn arb_community() -> impl Strategy<Value = CommunityLabel> {
(0..POOL).prop_map(community)
}
fn arb_channel() -> impl Strategy<Value = ChannelLabel> {
(0..POOL).prop_map(channel)
}
fn arb_opaque() -> impl Strategy<Value = OpaqueId> {
(0u32..16).prop_map(|i| OpaqueId(format!("m{i}")))
}
fn arb_verdict() -> impl Strategy<Value = Verdict> {
prop_oneof![Just(Verdict::Allow), Just(Verdict::Deny)]
}
fn arb_reason() -> impl Strategy<Value = SanitizedReason> {
prop_oneof![
Just(SanitizedReason::Restricted),
Just(SanitizedReason::Invalid),
Just(SanitizedReason::ServerError),
]
}
/// The bootstrapped state for a request resolved to `resolved`. Host/actor
/// are fixed so that, when we reuse this state for every step, the only way
/// a `StateMismatch` can arise is if a property deliberately flips a field.
fn state_for(resolved: CommunityLabel) -> AbstractState {
AbstractState {
resolved_community: resolved,
bound_host: host(0),
actor: actor(0),
}
}
// --- Action generators -----------------------------------------------------
/// A "clean" action: one whose presence in a trace bootstrapped to
/// `resolved` introduces NO violation on its own. Read labels are all
/// `resolved`; AuthCheck either Denies (any claim) or Allows with a claim
/// equal to `resolved` (or no claim). No ImplBug. This is the alphabet P2
/// draws from, and the benign filler P1/P3/P4/P5 use for prefixes.
fn arb_clean_action(resolved: CommunityLabel) -> impl Strategy<Value = TraceAction> {
let res = resolved;
prop_oneof![
(arb_opaque(), arb_channel(), prop::option::of(Just(res))).prop_map(
|(msg_id, channel, claimed_community)| TraceAction::WriteInsert {
msg_id,
channel,
claimed_community,
}
),
(arb_opaque(), prop::option::of(Just(res))).prop_map(|(msg_id, claimed_community)| {
TraceAction::WriteInsertGlobal {
msg_id,
claimed_community,
}
}),
(arb_opaque(), arb_channel(), prop::option::of(Just(res))).prop_map(
|(msg_id, channel, claimed_community)| TraceAction::WriteDuplicate {
msg_id,
channel,
claimed_community,
}
),
arb_reason().prop_map(|reason| TraceAction::SanitizedError { reason }),
// AuthCheck that cannot bite M2/M8: either Deny (any claim is in-spec)
// or Allow with a claim that is None or equal to resolved.
(
arb_channel(),
arb_verdict(),
prop_oneof![Just(None), Just(Some(res))],
)
.prop_map(|(channel, verdict, claimed_community)| {
// For Deny, the claim is unconstrained; for Allow it is
// None-or-resolved by construction above, so it never bites.
TraceAction::AuthCheck {
channel,
claimed_community,
verdict,
}
}),
// Reads whose every row label equals resolved.
(arb_channel(), 0usize..4).prop_map(move |(channel, n)| TraceAction::ReadMessageRows {
channel: Some(channel),
row_communities: vec![res; n],
}),
(0usize..4).prop_map(move |n| TraceAction::ReadByIdRows {
channel: None,
row_communities: vec![res; n],
}),
(0usize..4).prop_map(move |n| TraceAction::ReadHostFeedRows {
row_communities: vec![res; n],
}),
]
}
/// Wrap actions into steps that all share the bootstrapped state, so the
/// only violations possible are action-level (no incidental StateMismatch).
fn steps_with_state(actions: Vec<TraceAction>, resolved: CommunityLabel) -> Vec<TraceStep> {
let st = state_for(resolved);
actions
.into_iter()
.map(|a| TraceStep::new(a, st.clone()))
.collect()
}
/// A clean trace: 1..=12 clean actions over one resolved community, all
/// sharing the bootstrap state. By construction this contains no foreign
/// label, no Allow+foreign claim, no ImplBug, no state flip, no schema
/// mismatch.
fn arb_clean_trace() -> impl Strategy<Value = (CommunityLabel, Vec<TraceStep>)> {
arb_community().prop_flat_map(|resolved| {
prop::collection::vec(arb_clean_action(resolved), 1..=12)
.prop_map(move |actions| (resolved, steps_with_state(actions, resolved)))
})
}
proptest! {
#![proptest_config(ProptestConfig::with_cases(128))]
/// P2 — completeness / no false reject.
/// A fully clean, non-empty, current-schema, consistent-state trace with
/// no coverage obligations MUST be accepted. `Scenario::unstructured`
/// declares no required actions, so coverage breach cannot fire.
#[test]
fn clean_trace_is_accepted((_resolved, trace) in arb_clean_trace()) {
let sc = Scenario::unstructured(trace);
prop_assert!(
check_trace(&sc).is_ok(),
"clean trace was rejected: {:?}",
check_trace(&sc)
);
}
/// P1 — non-interference soundness / no false accept of a leak.
/// A clean prefix followed by a single read whose row set contains a
/// foreign label MUST be rejected with NonInterference. The foreign read
/// is the only possible violation, so fail-fast surfaces exactly it.
#[test]
fn foreign_row_label_is_rejected(
resolved in arb_community(),
foreign_idx in 0u128..POOL,
prefix in prop::collection::vec(arb_community().prop_map(|_| ()), 0..6),
clean_before in any::<bool>(),
which_read in 0u8..3,
) {
// Pick a foreign community distinct from resolved.
let foreign = {
let mut f = community(foreign_idx);
if f == resolved {
f = community((foreign_idx + 1) % POOL);
}
f
};
// If POOL were 1 this could still collide; guard explicitly.
prop_assume!(foreign != resolved);
let mut actions: Vec<TraceAction> = Vec::new();
// Optional benign clean prefix (reads of resolved-only rows) to prove
// the violation still bites after valid steps.
if clean_before {
for _ in &prefix {
actions.push(TraceAction::ReadMessageRows {
channel: Some(channel(0)),
row_communities: vec![resolved],
});
}
}
// The single violating read carries one foreign label. NI confinement
// is enforced on ALL THREE read surfaces (they share `check_row_labels`),
// so the property must bite regardless of which read leaked.
let leaked = vec![resolved, foreign];
let violating = match which_read {
0 => TraceAction::ReadMessageRows {
channel: Some(channel(0)),
row_communities: leaked,
},
1 => TraceAction::ReadByIdRows {
channel: None,
row_communities: leaked,
},
_ => TraceAction::ReadHostFeedRows {
row_communities: leaked,
},
};
actions.push(violating);
let trace = steps_with_state(actions, resolved);
let err = check_trace(&Scenario::unstructured(trace)).unwrap_err();
prop_assert!(
matches!(err, TransitionError::NonInterference { .. }),
"expected NonInterference, got {err:?}"
);
}
/// P3a — AuthCheck Allow + foreign claim always bites IllegalTransition.
/// One-step trace so the M2/M8 bite is the only candidate.
#[test]
fn auth_allow_foreign_claim_bites(
resolved in arb_community(),
foreign_idx in 0u128..POOL,
chan in arb_channel(),
) {
let foreign = {
let mut f = community(foreign_idx);
if f == resolved {
f = community((foreign_idx + 1) % POOL);
}
f
};
prop_assume!(foreign != resolved);
let trace = steps_with_state(
vec![TraceAction::AuthCheck {
channel: chan,
claimed_community: Some(foreign),
verdict: Verdict::Allow,
}],
resolved,
);
let err = check_trace(&Scenario::unstructured(trace)).unwrap_err();
prop_assert!(
matches!(err, TransitionError::IllegalTransition { .. }),
"expected IllegalTransition for Allow+foreign claim, got {err:?}"
);
}
/// P3b — AuthCheck Deny with any claim is in-spec (never bites on the
/// claim axis). One-step clean-otherwise trace MUST be accepted.
#[test]
fn auth_deny_any_claim_is_ok(
resolved in arb_community(),
claim_idx in 0u128..POOL,
chan in arb_channel(),
has_claim in any::<bool>(),
) {
let claimed = if has_claim { Some(community(claim_idx)) } else { None };
let trace = steps_with_state(
vec![TraceAction::AuthCheck {
channel: chan,
claimed_community: claimed,
verdict: Verdict::Deny,
}],
resolved,
);
prop_assert!(
check_trace(&Scenario::unstructured(trace)).is_ok(),
"Deny with any claim should be in-spec"
);
}
/// P4 — ImplBug always bites CoverageBreach. Clean prefix then ImplBug;
/// since the prefix is clean, the ImplBug is the first/only violation.
#[test]
fn impl_bug_bites_coverage_breach(
resolved in arb_community(),
prefix_len in 0usize..4,
kind in "[a-z_]{1,16}",
) {
let mut actions: Vec<TraceAction> = (0..prefix_len)
.map(|_| TraceAction::ReadMessageRows {
channel: Some(channel(0)),
row_communities: vec![resolved],
})
.collect();
actions.push(TraceAction::ImplBug { kind });
let trace = steps_with_state(actions, resolved);
let err = check_trace(&Scenario::unstructured(trace)).unwrap_err();
prop_assert!(
matches!(err, TransitionError::CoverageBreach { .. }),
"expected CoverageBreach from ImplBug, got {err:?}"
);
}
/// P5 — a mid-trace state flip bites StateMismatch. One clean bootstrap
/// step, then a benign action whose `state_after` flips exactly one of
/// resolved_community / bound_host / actor. State is checked before any
/// action-specific logic, so this is the only possible violation.
#[test]
fn state_flip_bites_state_mismatch(
resolved in arb_community(),
other_idx in 0u128..POOL,
which in 0u8..3,
) {
let boot = state_for(resolved);
// A benign first step.
let step0 = TraceStep::new(
TraceAction::ReadMessageRows {
channel: Some(channel(0)),
row_communities: vec![resolved],
},
boot.clone(),
);
// Flip exactly one field for step 1.
let mut flipped = boot.clone();
match which {
0 => {
let mut other = community(other_idx);
if other == resolved {
other = community((other_idx + 1) % POOL);
}
prop_assume!(other != resolved);
flipped.resolved_community = other;
}
1 => flipped.bound_host = host(9),
_ => flipped.actor = actor(9),
}
let step1 = TraceStep::new(
TraceAction::ReadMessageRows {
channel: Some(channel(0)),
// Use the FLIPPED resolved so the read itself is clean
// relative to its own state_after; the bite must come from
// the state divergence, not row labels.
row_communities: vec![flipped.resolved_community],
},
flipped,
);
let err = check_trace(&Scenario::unstructured(vec![step0, step1])).unwrap_err();
prop_assert!(
matches!(err, TransitionError::StateMismatch { .. }),
"expected StateMismatch from a mid-trace field flip, got {err:?}"
);
}
/// P6 — determinism and no-panic. Running `check_trace` twice on the same
/// scenario yields the same result, and neither call panics. Draws from
/// the clean alphabet plus occasional violations so the input space is
/// broad; we assert nothing about the verdict, only its stability.
#[test]
fn check_trace_is_deterministic_and_total(
resolved in arb_community(),
actions in prop::collection::vec(
prop_oneof![
arb_clean_action(community(0)),
// a few intentionally-violating shapes to widen coverage
Just(TraceAction::ImplBug { kind: "fuzz".into() }),
arb_community().prop_map(|c| TraceAction::ReadMessageRows {
channel: None,
row_communities: vec![c],
}),
],
1..=12,
),
) {
let trace = steps_with_state(actions, resolved);
let sc = Scenario::unstructured(trace);
let r1 = check_trace(&sc);
let r2 = check_trace(&sc);
prop_assert_eq!(
format!("{r1:?}"),
format!("{r2:?}"),
"check_trace was non-deterministic"
);
}
}