Model-Based Stateful Testing with proptest-state-machine

This post is part of the Model-Based Stateful Testing with madhouse-rs series.

Imagine trying to test a distributed system with dozens of operations:

• miners submitting blocks
• nodes joining and leaving
• transactions flooding the mempool
• network partitions
• and more.

Traditional unit tests can’t capture the chaotic, interleaved nature of these scenarios.

Model-based testing offers a solution: define all possible operations, let the framework generate random sequences, and check that your system behaves correctly. But… how you structure those operations determines whether your test harness scales from 5 commands to 500.

proptest-state-machine sits firmly on the operations-open, data-closed side of the expression problem. You define a central Transition enum that lists every possible operation.

The Enum Approach

Let’s explore this with a simple counter example first – while the real-world blockchain scenarios would be more complex to demonstrate initially, the core design patterns are identical. We’ll see the blockchain applications later in the series.

use proptest_state_machine::*;
use proptest::prelude::*;

// The model state.
#[derive(Clone, Debug)]
struct CounterModel {
    value: i32,
    max_value: i32,
}

// The real system under test.
struct Counter {
    value: i32,
    max_value: i32,
}

// All possible operations in one enum.
#[derive(Clone, Debug)]
enum CounterTransition {
    Inc,
    Dec,
    Reset,
}

impl StateMachine for CounterModel {
    type State = CounterModel;
    type Sut = Counter;
    type Transition = CounterTransition;

    fn init_state() -> BoxedStrategy<Self::State> {
        Just(CounterModel { value: 0, max_value: 100 }).boxed()
    }

    fn init_sut(state: &Self::State) -> BoxedStrategy<Self::Sut> {
        Just(Counter {
            value: state.value,
            max_value: state.max_value
        }).boxed()
    }

    fn transitions(_state: &Self::State) -> BoxedStrategy<Self::Transition> {
        prop_oneof![
            Just(CounterTransition::Inc),
            Just(CounterTransition::Dec),
            Just(CounterTransition::Reset),
        ].boxed()
    }

    fn apply(
        mut state: Self::State,
        sut: &mut Self::Sut,
        transition: Self::Transition,
    ) -> Self::State {
        match transition {
            CounterTransition::Inc => {
                if state.value < state.max_value {
                    state.value += 1;
                    sut.value += 1;
                }
            }
            CounterTransition::Dec => {
                state.value -= 1;
                sut.value -= 1;
            }
            CounterTransition::Reset => {
                state.value = 0;
                sut.value = 0;
            }
        }
        state
    }

    fn postconditions(state: &Self::State, sut: &Self::Sut) {
        assert_eq!(state.value, sut.value);
        assert_eq!(state.max_value, sut.max_value);
        assert!(state.value <= state.max_value);
    }
}

The Scalability Problem

This approach starts simple, but every new operation requires:

1. Adding a variant to the central CounterTransition enum.
2. Updating the apply function with a new match arm.
3. Updating the transitions function to include the new operation.

With 10 operations, this is manageable. With 100+ operations – like testing a blockchain node – it becomes unwieldy. The apply function grows into a monolithic match statement. Every developer adding a test command must touch this central file.

Real-World Complexity

Consider testing the Stacks blockchain, where operations include:

enum StacksTransition {
    MineBitcoinBlock,
    MineStacksBlock(BlockData),
    SubmitTransaction(Transaction),
    ConnectPeer(PeerInfo),
    DisconnectPeer(PeerId),
    NetworkPartition(Vec<NodeId>),
    RestoreNetwork,
    RestartNode(NodeId),
    // ... 50+ more operations.
}

The apply function becomes hundreds of lines. Adding new test scenarios requires editing this central bottleneck. Worse, the logic for each command is scattered – generation in transitions, preconditions mixed into apply, and postconditions in a separate function.

This scaling limitation becomes apparent in complex scenarios like reproducing a Stacks mainnet bug. While that specific attempt used hand-written tests, the enum-based approach would face the same bottleneck – dozens of blockchain operations in a central enum and apply function, making it difficult to generate the chaotic scenarios needed to reveal subtle consensus issues.

Next: Scaling Model-Based Stateful Testing with madhouse-rs