From 4706004f4769e3515066cd6975003c3ea02c2421 Mon Sep 17 00:00:00 2001 From: "K. Isom" Date: Sat, 17 Oct 2026 21:42:16 -0700 Subject: [PATCH] test(sim): property tests for convergence, order independence, monotonicity --- tines-sim/src/world.rs | 14 ++- tines-sim/tests/props.rs | 257 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 270 insertions(+), 1 deletion(-) create mode 100644 tines-sim/tests/props.rs diff --git a/tines-sim/src/world.rs b/tines-sim/src/world.rs index c459e45..b80b364 100644 --- a/tines-sim/src/world.rs +++ b/tines-sim/src/world.rs @@ -10,7 +10,7 @@ use rand::{rngs::StdRng, SeedableRng}; use std::cell::RefCell; use std::collections::VecDeque; use std::rc::Rc; -use tines_core::transport::Event; +use tines_core::transport::{Event, FrameBuf}; /// World configuration for a `SimWorld`. #[derive(Clone, Debug)] @@ -105,6 +105,18 @@ impl SimWorld { pub fn frames_dropped(&self) -> u64 { self.frames_dropped } + + /// Inject a raw inbound `Frame` into `node`'s mailbox without going through + /// the transport's reachability, MTU, or loss checks. + /// + /// A test seam: it lets tests feed arbitrary or malformed byte strings + /// straight to a node's exchange, which is where the "never panic on + /// untrusted wire input" guarantee lives. The frame is not validated here — + /// a malformed frame is dropped by the receiving node's + /// [`Exchange`](tines_core::Exchange) rather than stored. + pub fn inject_frame(&mut self, node: usize, peer: usize, bytes: FrameBuf) { + self.inboxes[node].push_back(Event::Frame(peer, bytes)); + } } // --------------------------------------------------------------------------- diff --git a/tines-sim/tests/props.rs b/tines-sim/tests/props.rs new file mode 100644 index 0000000..0bebf42 --- /dev/null +++ b/tines-sim/tests/props.rs @@ -0,0 +1,257 @@ +//! Property tests for the tines simulator. +//! +//! These are not deterministic scenarios (see `convergence.rs`) but *properties* +//! that must hold over randomly generated scenarios: +//! +//! * [`connected_components_converge`] — every connected component of the +//! contact graph ends each run fully gossiped. +//! * [`store_is_independent_of_contact_order`] — reordering the contacts of a +//! fully-connected 3-node graph does not change the resulting store. +//! * [`union_is_monotone`] — a node's id set never shrinks as the simulation +//! advances (no trimming). +//! * [`garbage_frames_never_panic`] — malformed wire frames are dropped, never +//! panic the node. + +use proptest::prelude::*; +use tines_core::{FrameBuf, Store}; +use tines_sim::{Contact, ContactTrace, Sim, WorldConfig}; + +/// A fixed set of short observation topics the tests reuse so the generated +/// observations round-trip cleanly through the core (`MAX_TOPIC` is 64 bytes). +const TOPICS: [&[u8]; 8] = [ + b"temp", + b"humid", + b"door", + b"motion", + b"light", + b"batt", + b"press", + b"power", +]; + +/// A single contact window over `nodes` nodes. `start` is bounded well below the +/// duration floor so every contact in a scenario overlaps in a long common +/// window, keeping every union-find component *temporally connected* (a +/// component that is structurally connected but temporally disconnected can +/// never converge — a correct negative, not a protocol bug — so the scenario is +/// constrained to temporally-connected inputs). +/// +/// The unordered pair `a != b` uses the `b_prime` slot shifted past `a`. +fn contact(nodes: usize) -> impl Strategy { + ( + 0u64..5_000u64, + 30_000u64..=40_000u64, + 0usize..nodes, + 0usize..nodes.saturating_sub(1), + ) + .prop_map(|(start, duration, a, b_prime)| { + let mut b = b_prime; + if b >= a { + b += 1; + } + Contact { + start_ms: start, + end_ms: start + duration, + a, + b, + } + }) +} + +/// A single observation: a topic drawn from [`TOPICS`] and a random 1..=64 byte +/// payload. +fn observation() -> impl Strategy, Vec)> { +( + 0u32..8u32, + proptest::collection::vec(any::(), 1..=64usize), +) +.prop_map(|(topic_idx, payload)| (TOPICS[topic_idx as usize].to_vec(), payload)) +} + +/// A generated scenario: a node count, a contact trace over those nodes, and a +/// flat list of `(node, topic, payload)` observations to apply at `t = 0`. +type Scenario = (usize, ContactTrace, Vec<(usize, Vec, Vec)>); + +/// The [`scenario`] strategy, built on top of [`contact`] and [`observation`]. +/// +/// `prop_flat_map` fixes `nodes` first so the same node count drives both the +/// trace and the per-node observation lists. +fn scenario() -> impl Strategy { + (2..=6usize).prop_flat_map(|nodes| { + let trace = proptest::collection::vec(contact(nodes), 1..=12usize); + let obs = proptest::collection::vec(observation(), nodes..=nodes); + (trace, obs).prop_map(move |(contacts, per_node)| { + let trace = ContactTrace { contacts }; + let mut list = Vec::new(); + for (node, (topic, payload)) in per_node.into_iter().enumerate() { + list.push((node, topic, payload)); + } + (nodes, trace, list) + }) + }) +} + +/// A 3-node observation list, reused by the order-independence test. +fn observations_3nodes() -> impl Strategy, Vec)>> { + proptest::collection::vec(observation(), 3..=3) + .prop_map(|per_node| per_node.into_iter().enumerate().map(|(n, o)| (n, o.0, o.1)).collect()) +} + +/// Maps a `u64` seed to one of the six permutations of three slots. +fn permute3(perm: u64) -> [usize; 3] { + let bases = [ + [0usize, 1, 2], + [0, 2, 1], + [1, 0, 2], + [1, 2, 0], + [2, 0, 1], + [2, 1, 0], + ]; + bases[(perm % 6) as usize] +} + +proptest! { + #![proptest_config(ProptestConfig { cases: 64, .. ProptestConfig::default() })] + + /// Every connected component of the contact graph must be fully gossiped by + /// the end of the trace. Tested at `loss = 0`: the spec's convergence is + /// best-effort per contact and eventual over contacts, so guaranteed full + /// convergence under loss within a finite window is NOT a spec property + /// (a lost summary delays re-diff until the next summary round). Lossy + /// eventual-convergence is covered deterministically by + /// `convergence.rs::lossy_link_still_converges_given_time`. + #[test] + fn connected_components_converge(scenario in scenario()) { + let (nodes, trace, obs) = scenario; + let end = trace.end(); + let cfg = WorldConfig { + nodes, + mtu: 512, + loss: 0.0, + dup: 0.05, + seed: 1, + }; + let mut sim = Sim::new(cfg, trace); + for (node, topic, payload) in &obs { + sim.observe(*node, topic, payload); + } + sim.run_until(end + 1); + for component in sim.components() { + prop_assert!( + sim.converged(&component), + "component {:?} over {} nodes did not converge", + component, + nodes, + ); + } + } + + /// Reordering the contacts of a fully-connected 3-node graph does not + /// change the per-node store, so long as loss is absent. + #[test] + fn store_is_independent_of_contact_order( + obs in observations_3nodes(), + perm in any::(), + ) { + // Three time slots, each a 5000 ms window. + let slots = [(0u64, 5000u64), (6000, 11000), (12000, 17000)]; + // The three node pairs that make contact. + let pairs = [(0usize, 1usize), (1usize, 2usize), (0usize, 2usize)]; + + let build = |order: [usize; 3]| { + let mut trace = ContactTrace::default(); + for (i, &(start, end)) in slots.iter().enumerate() { + let (a, b) = pairs[order[i]]; + trace.contacts.push(Contact { start_ms: start, end_ms: end, a, b }); + } + trace + }; + + let cfg = WorldConfig { nodes: 3, mtu: 512, loss: 0.0, dup: 0.0, seed: 1 }; + let order = permute3(perm); + + let mut a = Sim::new(cfg.clone(), build([0, 1, 2])); + for (node, topic, payload) in &obs { + a.observe(*node, topic, payload); + } + a.run_until(17000); + + let mut b = Sim::new(cfg.clone(), build(order)); + for (node, topic, payload) in &obs { + b.observe(*node, topic, payload); + } + b.run_until(17000); + + for i in 0..3 { + prop_assert_eq!(a.id_set(i), b.id_set(i), "node {} id sets differ", i); + } + } + + /// A node's id set is monotonically non-decreasing: nothing is ever + /// trimmed from the store during a normal run. + #[test] + fn union_is_monotone(scenario in scenario()) { + use std::collections::BTreeSet; + + let (nodes, trace, obs) = scenario; + let end = trace.end(); + let cfg = WorldConfig { + nodes, + mtu: 512, + loss: 0.0, + dup: 0.0, + seed: 1, + }; + let mut sim = Sim::new(cfg, trace); + for (node, topic, payload) in &obs { + sim.observe(*node, topic, payload); + } + + let mut prev: Vec> = (0..nodes).map(|i| sim.id_set(i)).collect(); + let mut elapsed = 0u64; + while elapsed < end { + // Advance one sample period (1000 ms) at the 10 ms step resolution. + for _ in 0..100 { + sim.step(); + } + elapsed += 1000; + let prev_t = elapsed - 1000; + let now: Vec> = (0..nodes).map(|i| sim.id_set(i)).collect(); + for i in 0..nodes { + prop_assert!( + prev[i].is_subset(&now[i]), + "node {} lost an observation between t={} and t={}", + i, + prev_t, + elapsed, + ); + } + prev = now; + } + } + + /// Malformed wire frames are dropped by the exchange and never panic the + /// node; the store stays empty. + #[test] + fn garbage_frames_never_panic( + bytes in proptest::collection::vec(any::(), 0..1500), + ) { + let cfg = WorldConfig { + nodes: 1, + mtu: 512, + loss: 0.0, + dup: 0.0, + seed: 1, + }; + let mut sim = Sim::new(cfg, ContactTrace::default()); + let mut node = sim.nodes.pop().expect("one node"); + + // `bytes` is at most 1499 bytes, which fits the MAX_FRAME buffer. + let buf = FrameBuf::from_slice(&bytes).expect("payload fits in a MAX_FRAME buffer"); + sim.world.borrow_mut().inject_frame(0, 1, buf); + + let stored = node.poll(0); + prop_assert_eq!(stored, 0, "a garbage frame must not be stored"); + prop_assert_eq!(node.store().len(), 0, "store must be unchanged by a garbage frame"); + } +}