diff --git a/Cargo.lock b/Cargo.lock index e65cb9cbe..09108807c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -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" diff --git a/Cargo.toml b/Cargo.toml index 40220f842..03cba4ee7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -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 } diff --git a/crates/buzz-conformance/Cargo.toml b/crates/buzz-conformance/Cargo.toml index 0d2d1b5d2..2d5f9a1f5 100644 --- a/crates/buzz-conformance/Cargo.toml +++ b/crates/buzz-conformance/Cargo.toml @@ -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 } diff --git a/crates/buzz-conformance/tests/proptest_checker.rs b/crates/buzz-conformance/tests/proptest_checker.rs new file mode 100644 index 000000000..3d2b81ef6 --- /dev/null +++ b/crates/buzz-conformance/tests/proptest_checker.rs @@ -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 { + (0..POOL).prop_map(community) +} + +fn arb_channel() -> impl Strategy { + (0..POOL).prop_map(channel) +} + +fn arb_opaque() -> impl Strategy { + (0u32..16).prop_map(|i| OpaqueId(format!("m{i}"))) +} + +fn arb_verdict() -> impl Strategy { + prop_oneof![Just(Verdict::Allow), Just(Verdict::Deny)] +} + +fn arb_reason() -> impl Strategy { + 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 { + 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, resolved: CommunityLabel) -> Vec { + 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)> { + 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::(), + 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 = 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::(), + ) { + 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 = (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" + ); + } +}