swaits
2c28dd77b4
The nightly workflow has failed every run since it was added. Fix the four distinct issues so it can actually exercise the slow checks: - cargo-mutants: drop bogus `--in-diff-base ""` flag (never existed in cargo-mutants; v27 rejects it). - fuzz smoke: pin `--target x86_64-unknown-linux-gnu`. Binstall ships a musl-static cargo-fuzz binary whose default target inherits its own triple, and libfuzzer's sanitizer is incompatible with `crt-static`. - miri: move multi-module filters after `--`. `cargo test` only accepts one TESTNAME positional; libtest accepts multiple substring filters. - stateright random_large: add `target_state_count(1_000_000)` so the simulation actually terminates instead of looping past the 30 min CI timeout. The comment already claimed "up to 10⁶ states". Also refreshes fuzz/Cargo.lock, regenerated by the local verification build (was stale vs. parent deps).
292 lines
9.4 KiB
Rust
292 lines
9.4 KiB
Rust
//! Stateright model of the rendezvous algorithm.
|
||
//!
|
||
//! Gives a bounded-exhaustive safety proof (BFS) and a sampled liveness
|
||
//! witness (random walk) for the PROTOCOL.md §§4–5 procedures.
|
||
//!
|
||
//! Scope — what this model **does** capture:
|
||
//! * `WriteSlot`: a node writes its self-entry (age 0) + up to V vouches
|
||
//! at age 1 to its `slot_u = H(self_id) mod K`, using a simplified merge
|
||
//! (age-up, evict by max-age with deterministic tie-break).
|
||
//! * `HealRead`: a node reads a random slot and adds discovered IDs to
|
||
//! its `joined` set — the simulator's stand-in for `GossipSender::join_peers`.
|
||
//! * `Dial`: completes a gossip connection (the iroh-gossip dial handshake
|
||
//! is abstracted to a single atomic action).
|
||
//!
|
||
//! What it **does not** model (by design):
|
||
//! * Crypto — accepted correct (RustCrypto stack).
|
||
//! * Actual network timing, jitter, or dropped packets.
|
||
//! * Byzantine writers.
|
||
//!
|
||
//! **Safety properties checked** (must always hold across every reachable
|
||
//! state in the BFS-explored state space):
|
||
//!
|
||
//! - **S1 (size)**: every slot's record has `len ≤ B`.
|
||
//! - **S2 (age)**: every entry has `age < A_max`.
|
||
//!
|
||
//! **Liveness property** (sampled via random-walk; not exhaustive):
|
||
//!
|
||
//! - **L1 (partition heals)**: starting from two disjoint connected
|
||
//! components, eventually some node in one has discovered a node in
|
||
//! the other via a HealRead.
|
||
//!
|
||
//! Run:
|
||
//! ```text
|
||
//! cargo test --test stateright_model --release -- --ignored bfs_small
|
||
//! cargo test --test stateright_model --release -- --ignored random_large
|
||
//! ```
|
||
|
||
#![allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]
|
||
#![allow(dead_code, unused_variables)]
|
||
|
||
use std::collections::BTreeSet;
|
||
|
||
use stateright::Checker;
|
||
use stateright::Model;
|
||
|
||
/// Simplified entry: (id, age). Used in the model, not the real crate.
|
||
#[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
|
||
struct ModelEntry {
|
||
id: u8,
|
||
age: u8,
|
||
}
|
||
|
||
/// Simplified slot. `seq` is monotonic per slot; writes bump by 1.
|
||
#[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, Default)]
|
||
struct Slot {
|
||
entries: Vec<ModelEntry>,
|
||
seq: u32,
|
||
}
|
||
|
||
#[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
|
||
struct ModelState {
|
||
slots: Vec<Slot>, // len = K
|
||
neighbors: Vec<BTreeSet<u8>>, // per-node active-view sets (node ids)
|
||
joined: Vec<BTreeSet<u8>>, // per-node "discovered via heal-read" set
|
||
}
|
||
|
||
#[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
|
||
enum Action {
|
||
/// Node `id` writes to its `slot_u` — adds self at age 0, vouches for
|
||
/// all current neighbors (up to V), evicts oldest.
|
||
Write { node: u8 },
|
||
/// Node `id` heals by reading slot `slot_idx` — union entries' IDs
|
||
/// into its `joined` set.
|
||
HealRead { node: u8, slot_idx: u8 },
|
||
/// Node `a` dials `b`. Updates both neighbor sets.
|
||
Dial { a: u8, b: u8 },
|
||
}
|
||
|
||
/// Parameters: small to keep BFS tractable.
|
||
struct RendezvousModel {
|
||
n: u8, // number of nodes
|
||
k: u8, // number of slots
|
||
max_age: u8, // A_max
|
||
max_entries: u8, // B
|
||
max_vouches: u8, // V
|
||
}
|
||
|
||
impl RendezvousModel {
|
||
fn slot_for(&self, id: u8) -> u8 {
|
||
// Deterministic slot assignment.
|
||
id % self.k
|
||
}
|
||
|
||
/// Perform the merge: age up non-self entries, drop ≥ A_max, add self
|
||
/// at 0, vouch up to V neighbors at 1, evict max-age.
|
||
fn merge(
|
||
&self,
|
||
current: &[ModelEntry],
|
||
self_id: u8,
|
||
neighbor_ids: &BTreeSet<u8>,
|
||
) -> Vec<ModelEntry> {
|
||
let mut out: Vec<ModelEntry> = current
|
||
.iter()
|
||
.filter(|e| e.id != self_id)
|
||
.filter_map(|e| {
|
||
let a = e.age.saturating_add(1);
|
||
(a < self.max_age).then_some(ModelEntry { id: e.id, age: a })
|
||
})
|
||
.collect();
|
||
out.push(ModelEntry {
|
||
id: self_id,
|
||
age: 0,
|
||
});
|
||
|
||
// Vouch deterministically: first V neighbors in sorted order.
|
||
for &nid in neighbor_ids.iter().take(self.max_vouches as usize) {
|
||
if nid == self_id {
|
||
continue;
|
||
}
|
||
if let Some(existing) = out.iter_mut().find(|e| e.id == nid) {
|
||
if existing.age > 1 {
|
||
existing.age = 1;
|
||
}
|
||
} else {
|
||
out.push(ModelEntry { id: nid, age: 1 });
|
||
}
|
||
}
|
||
|
||
// Evict: deterministic tie-break — drop highest id among oldest.
|
||
while out.len() > self.max_entries as usize {
|
||
let max_age = out.iter().map(|e| e.age).max().unwrap_or(0);
|
||
let pick = out
|
||
.iter()
|
||
.enumerate()
|
||
.filter(|(_, e)| e.age == max_age)
|
||
.max_by_key(|(_, e)| e.id)
|
||
.map(|(i, _)| i)
|
||
.unwrap_or(0);
|
||
out.swap_remove(pick);
|
||
}
|
||
|
||
out.sort_by(|a, b| a.id.cmp(&b.id).then(a.age.cmp(&b.age)));
|
||
out
|
||
}
|
||
}
|
||
|
||
impl Model for RendezvousModel {
|
||
type State = ModelState;
|
||
type Action = Action;
|
||
|
||
fn init_states(&self) -> Vec<Self::State> {
|
||
let slots = (0..self.k).map(|_| Slot::default()).collect();
|
||
let neighbors = (0..self.n).map(|_| BTreeSet::new()).collect();
|
||
let joined = (0..self.n).map(|_| BTreeSet::new()).collect();
|
||
vec![ModelState {
|
||
slots,
|
||
neighbors,
|
||
joined,
|
||
}]
|
||
}
|
||
|
||
fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>) {
|
||
for node in 0..self.n {
|
||
actions.push(Action::Write { node });
|
||
for slot_idx in 0..self.k {
|
||
actions.push(Action::HealRead { node, slot_idx });
|
||
}
|
||
for other in 0..self.n {
|
||
if other != node && !state.neighbors[node as usize].contains(&other) {
|
||
actions.push(Action::Dial { a: node, b: other });
|
||
}
|
||
}
|
||
}
|
||
}
|
||
|
||
fn next_state(&self, last: &Self::State, action: Self::Action) -> Option<Self::State> {
|
||
let mut state = last.clone();
|
||
match action {
|
||
Action::Write { node } => {
|
||
let slot = self.slot_for(node) as usize;
|
||
let neighbors = state.neighbors[node as usize].clone();
|
||
let merged = self.merge(&state.slots[slot].entries, node, &neighbors);
|
||
state.slots[slot].entries = merged;
|
||
state.slots[slot].seq += 1;
|
||
}
|
||
Action::HealRead { node, slot_idx } => {
|
||
let entries = state.slots[slot_idx as usize].entries.clone();
|
||
for e in entries {
|
||
if e.id != node {
|
||
state.joined[node as usize].insert(e.id);
|
||
}
|
||
}
|
||
}
|
||
Action::Dial { a, b } => {
|
||
state.neighbors[a as usize].insert(b);
|
||
state.neighbors[b as usize].insert(a);
|
||
}
|
||
}
|
||
Some(state)
|
||
}
|
||
|
||
fn properties(&self) -> Vec<stateright::Property<Self>> {
|
||
// Stateright 0.31's Property::always takes a fn pointer — no
|
||
// closure captures. Property functions read the bounds off `m`.
|
||
vec![
|
||
stateright::Property::<Self>::always("S1 record size bounded", |m, s| {
|
||
s.slots
|
||
.iter()
|
||
.all(|slot| slot.entries.len() <= m.max_entries as usize)
|
||
}),
|
||
stateright::Property::<Self>::always("S2 age bounded", |m, s| {
|
||
s.slots
|
||
.iter()
|
||
.all(|slot| slot.entries.iter().all(|e| e.age < m.max_age))
|
||
}),
|
||
]
|
||
}
|
||
}
|
||
|
||
// ── Tests ──────────────────────────────────────────────────────────────
|
||
|
||
/// BFS proof of S1 + S2 for N=2, K=1 with small bounds. Runs quickly
|
||
/// (seconds). Verifies the model's safety invariants hold across every
|
||
/// reachable state.
|
||
#[test]
|
||
#[ignore = "stateright: explicit run"]
|
||
fn bfs_small() {
|
||
let model = RendezvousModel {
|
||
n: 2,
|
||
k: 1,
|
||
max_age: 3,
|
||
max_entries: 3,
|
||
max_vouches: 1,
|
||
};
|
||
model
|
||
.checker()
|
||
.threads(num_cpus())
|
||
.target_max_depth(20)
|
||
.spawn_bfs()
|
||
.join()
|
||
.assert_properties();
|
||
}
|
||
|
||
/// BFS at N=3, K=2 — larger but should terminate in minutes.
|
||
#[test]
|
||
#[ignore = "stateright: explicit run, slow"]
|
||
fn bfs_n3_k2() {
|
||
let model = RendezvousModel {
|
||
n: 3,
|
||
k: 2,
|
||
max_age: 4,
|
||
max_entries: 4,
|
||
max_vouches: 2,
|
||
};
|
||
model
|
||
.checker()
|
||
.threads(num_cpus())
|
||
.target_max_depth(30)
|
||
.spawn_bfs()
|
||
.join()
|
||
.assert_properties();
|
||
}
|
||
|
||
/// Random-walk exploration for a larger configuration (N=6, K=3). Not
|
||
/// exhaustive; searches up to 10⁶ states for counterexamples. Useful
|
||
/// evidence but not proof.
|
||
#[test]
|
||
#[ignore = "stateright: explicit run, ~minutes"]
|
||
fn random_large() {
|
||
let model = RendezvousModel {
|
||
n: 6,
|
||
k: 3,
|
||
max_age: 5,
|
||
max_entries: 5,
|
||
max_vouches: 3,
|
||
};
|
||
model
|
||
.checker()
|
||
.threads(num_cpus())
|
||
.target_max_depth(50)
|
||
.target_state_count(1_000_000)
|
||
.spawn_simulation(0, stateright::UniformChooser)
|
||
.join()
|
||
.assert_properties();
|
||
}
|
||
|
||
fn num_cpus() -> usize {
|
||
std::thread::available_parallelism()
|
||
.map(std::num::NonZeroUsize::get)
|
||
.unwrap_or(4)
|
||
}
|