Property-Based, Model-Based, Snapshot, and Golden Testing

The failure arrives as operation 117 of a generated ledger history:

seed=0x5eed
credit(31), debit(8), debit(39), credit(7), ... 113 more commands
model balance=23; system balance=62

That report is reproducible but not yet explanatory. Removing the first half still fails. Removing the second quarter still fails. Replacing amounts with smaller values preserves the mismatch. After reduction, the counterexample is:

credit(1), debit(1), debit(1)

The first two commands return the account to zero. The third should be rejected without mutation, but a stale “last successful delta” is applied twice. A hand-picked test could have found this sequence; the important difference is the search system that discovered it, the shrinker that made it legible, and the reference model that knew the result was wrong.

Tests over large behavior spaces require three separate designs: a generator defines which cases can be explored, an oracle defines what correctness means, and a reducer turns a failure into evidence a human can act on. Property, model, differential, metamorphic, snapshot, and golden techniques supply different oracles. They complement exact examples; they do not replace them.

State the property before choosing a generator

A property quantifies a contract over a set of inputs or histories. “The parser does not panic” is useful but weak. “For every valid sequence of u16 values, decoding its encoding returns the original sequence” specifies a stronger relationship:

decode(encode(values)) = Ok(values)

Other durable property shapes include:

• Invariant: accepted ledger histories never produce a negative logical balance.
• Round trip: parsing a canonical serialization reconstructs the same semantic value.
• Idempotence: canonicalizing canonical output changes nothing.
• Conservation: moving value between two accounts preserves total value when fees are zero.
• Monotonicity: acknowledging more contiguous messages never decreases the committed offset.
• Equivalence: an optimized implementation produces the same result as a simple reference.
• Metamorphic relation: splitting input into chunks and concatenating encoded chunks equals encoding the whole input when boundaries carry no semantics.

Write the quantifier and preconditions. A round-trip property over arbitrary byte strings is wrong if the format has invalid encodings. Decide whether the generator produces valid semantic values and encodes them, arbitrary wire bytes including invalid cases, or a controlled mixture. Each answers a different question.

Do not let the library’s convenient generator determine the contract. Uniform random integers rarely resemble boundary-heavy production data. Build distributions around empty, singleton, maximum-length, duplicate, sorted, reverse-sorted, near-capacity, overflow-adjacent, malformed, and version-transition cases. Weighting is search policy, not a semantic guarantee; exact regression tests should retain cases too important to leave to sampling.

Make seeds replayable, not ceremonial

The lab uses a small deterministic generator to avoid third-party dependencies:

pub fn generated_commands(mut seed: u64, count: usize) -> Vec<Command> {
    let mut commands = Vec::with_capacity(count);
    for _ in 0..count {
        seed = seed.wrapping_mul(6_364_136_223_846_793_005).wrapping_add(1);
        let amount = ((seed >> 32) as u16 % 40) + 1;
        commands.push(if seed & 1 == 0 {
            Command::Credit(amount)
        } else {
            Command::Debit(amount)
        });
    }
    commands
}

This is an instructional fixture, not a recommendation for statistical quality or cryptography. Production property frameworks provide richer strategies, compositional shrinking, failure persistence, and runner configuration. Whatever the tool, record seed, framework version, case count, generator parameters, feature set, target, and operation index. A seed without the generator version may not reconstruct the same stream after an upgrade.

Randomizing a seed on every presubmit run increases exploration but can create a failure that disappears locally. Print the chosen seed before execution and include it in test artifacts. Keep a fixed deterministic corpus for fast gates, add rotating seeds in broader jobs, and promote every meaningful minimized failure to a stable regression. Never use production entropy, wall clock, hash-map iteration order, or scheduler timing as an undocumented generator.

Shrinking is part of diagnostic design

A shrinker searches for a simpler input that still falsifies the property. “Simpler” must reflect the domain. For an integer, it may mean toward zero and boundaries. For bytes, shorter length and simpler byte values. For a command history, delete ranges, delete individual operations, shrink amounts, simplify keys, then reduce concurrency structure.

The lab exposes the smallest structural step:

pub fn shrink_sequence(commands: &[Command]) -> Vec<Vec<Command>> {
    (0..commands.len())
        .map(|index| {
            let mut shorter = commands.to_vec();
            shorter.remove(index);
            shorter
        })
        .collect()
}

A real reducer repeats candidates until no simpler failing case remains. It must preserve generator validity where the property requires valid input. Blindly deleting a Begin operation from a protocol history may create an invalid sequence that fails for an irrelevant reason. State-aware shrinking can remove a transaction as a unit, repair identifiers, or replay candidate commands through the model before presenting them.

Shrinking consumes time. Bound attempts and report whether the result is minimal, locally minimal under known transforms, or merely smaller. Retain the original seed and input as well as the minimized case; a shrinker can have defects, and the full case may contain a second failure hidden by the first.

Use a state machine when correctness depends on history

Input properties suit pure functions. Stateful systems need histories. Model-based testing defines:

1. an abstract state small enough to trust;
2. commands allowed from each state;
3. expected return values and state transitions;
4. the concrete system adapter;
5. observations compared after each step.

For Ledger, the model is a u32 balance. Credit uses checked addition; debit uses checked subtraction. A command is accepted exactly when the arithmetic yields Some(next). After each accepted command, model and system balances must match. After rejection, the system must retain the prior state.

The reference must be independent enough to catch the production defect. Copying the same helper, arithmetic shortcut, parser, or generated table into both sides creates correlated error. Prefer a slower, clearer representation: a map instead of a custom index, sequential execution instead of a parallel algorithm, arbitrary-precision arithmetic instead of fixed-width arithmetic when range comparison is intended, or an obviously direct specification.

Model boundaries matter. A model that ignores persistence cannot verify crash recovery. One that treats time as a monotonically increasing integer cannot find wall-clock rollback defects. State the abstraction and residual risks. Increase fidelity only when the extra state addresses a named contract; an equally complex “reference implementation” may merely double the maintenance burden.

Command generation should be state-aware. Generate CloseAccount only for an open account if testing valid workflows, and deliberately generate invalid closes in a separate rejection property. Track command preconditions, postconditions, and observation points. Compare after every operation rather than only at the end, because compensating defects can converge on the same final state.

Differential tests compare independent implementations

Differential testing runs the same input through two systems and compares normalized results. The peer can be a reference parser, an old release, a different language implementation, a database engine, or two algorithm variants. It is powerful for parsers and serializers because accepted/rejected status, consumed length, semantic value, and re-encoded bytes can all be compared.

Agreement is not truth. Two implementations may share a specification misunderstanding, dependency, or undefined corner. Versions may intentionally differ. Define the comparison domain and normalization:

• Are noncanonical but valid encodings accepted by both?
• Are error categories compared, or unstable message strings?
• Does map order carry meaning?
• Are floating-point NaNs, signed zero, Unicode normalization, or timestamps equivalent under the contract?
• Is the old implementation authoritative or merely another witness?

For wireview, compare the zero-copy parser with a simple allocating decoder built from explicit byte reads. Generate valid frames from semantic values, malformed frames by controlled mutation, and truncated prefixes. Compare acceptance, decoded fields, and consumed length. If one parser accepts a frame the other rejects, retain the bytes before deciding which is wrong.

Differential testing across releases also detects compatibility drift, but do not freeze defects accidentally. Triage each difference against the format specification and migration policy. A reviewed divergence list is safer than a blanket “outputs must always match.”

Use metamorphic relations when no reference answer is cheap

Some systems have outputs that are expensive or impossible to calculate independently, yet transformations imply relationships between runs. Metamorphic testing checks those relations.

The lab’s byte encoder has a concatenation relation:

encode(left) ++ encode(right) = encode(left ++ right)

because each u16 is encoded independently at a fixed width. This property would be false for a format with a leading total-length field, cross-record compression, or checksum. The relation comes from the contract, not from a generic testing recipe.

Other examples:

• reordering independent requests preserves the multiset of outcomes;
• adding an unused symbol to a module does not change a serialized protocol descriptor;
• parsing after canonical formatting preserves the syntax tree;
• partitioning a sum and combining partial sums matches the whole, within an explicit numeric policy;
• retrying an idempotent operation with the same key produces one effect.

Metamorphic tests can expose defects without a complete expected output, but a weak relation can be satisfied by a broken implementation. A parser that always returns an empty document may satisfy some formatting relations. Combine multiple independent properties and exact anchor cases.

Separate snapshots from golden contracts

Both snapshots and golden files compare current output with stored expected data, but teams often use the words differently. A snapshot is usually captured through a framework with update/review tooling and may be fine-grained or inline. A golden file is commonly an explicit external artifact treated as a reviewed compatibility or rendering reference. The filename does not create rigor; ownership and review do.

The lab canonicalizes a report and compares it with tests/fixtures/report.golden:

assert_eq!(
    canonical_report(&ledger),
    include_str!("fixtures/report.golden")
);

The canonicalizer sorts fields by a defined order and emits stable line endings. It does not erase semantic differences. Good canonicalization removes irrelevant nondeterminism—temporary directories, generated IDs, unordered-map iteration, controlled timestamps—while retaining everything a caller cares about. Bad canonicalization replaces every number or path and makes distinct failures look equal.

Use snapshots where the output is easier to review as a whole than to assert field by field: diagnostics, structured plans, syntax trees, rendered fragments, or protocol fixtures. Use targeted assertions for small semantic contracts. A hundred-line snapshot that changes because one flag flipped can hide an unrelated deletion; split artifacts along review boundaries.

Binary golden files need companion tooling: a textual dump, schema-aware diff, image comparison with justified tolerances, or decoder that makes changes inspectable. Never approve an opaque byte replacement merely because regeneration succeeded. Keep generators deterministic, store provenance when necessary, and ensure update commands are separate from verification commands.

Make snapshot review a change-control gate

An update workflow should be deliberately asymmetric:

1. the ordinary test command detects drift and never repairs it;
2. a named update command writes candidate artifacts;
3. review shows semantic diffs and the input that caused each output;
4. the reviewer classifies the change as intended behavior, intentional format evolution, test correction, or defect;
5. compatibility-sensitive changes receive the same migration and version review as code.

Bulk “accept all” is dangerous when a refactor touches many snapshots. Partition updates, limit generated churn, and require an explanation for high-impact goldens. Store small stable artifacts in the repository when review value exceeds size. Large corpora may live in versioned artifact storage with hashes and retention ownership, but the test must fail clearly when data is unavailable rather than silently skip.

Snapshot brittleness has three common causes. First, the artifact includes irrelevant volatile fields. Canonicalize them narrowly. Second, the assertion boundary is too broad. Split by semantic ownership. Third, the output itself has no stable contract. Replace the snapshot with targeted properties or accept that the test will track implementation rather than behavior.

Do not confuse low churn with value. A stale snapshot can pass forever while no one runs the path that produces it. Verify fixture reachability, generator inputs, and update tooling in clean environments.

The techniques now form one evidence loop rather than a catalog. Use the figure to trace a generated value or history through independent observations, then follow a mismatch backward through replay and shrinking until it becomes an exact regression or a reviewed artifact.

Apply the techniques to parsers and serializers

A robust wireview campaign can combine distinct evidence:

• exact examples for header versions, empty payloads, maximum lengths, and known malformed frames;
• generated semantic frames satisfying schema constraints;
• decode(encode(value)) = value for canonical semantic values;
• encode(decode(bytes)) = canonical(bytes) for valid noncanonical inputs, if the format permits them;
• a simple allocating reference decoder compared with the zero-copy parser;
• metamorphic truncation: every proper prefix either reports incomplete input or a specific structural error, never reads beyond bounds;
• mutation properties for checksums, length fields, and reserved bits;
• golden bytes for protocol compatibility vectors shared with other languages.

Keep ownership and aliasing in view. A zero-copy result borrows the input, so generated buffers must live through observations. The test should compare semantic fields without turning the production parser into an owned parser merely for convenience. Unsafe internals still need layered dynamic assurance; properties exercise contracts but do not prove absence of undefined behavior.

Serialization properties need explicit canonical rules. Map ordering, float representation, Unicode normalization, omitted defaults, and version fields can make semantic equality differ from byte equality. Decide which one the protocol promises. If bytes are signed or hashed, canonical byte equality is a security contract, not formatting preference.

Model a concurrent queue without pretending to control every schedule

For a bounded multi-producer queue, begin with sequential abstract commands:

Offer(value) -> Accepted | Full | Closed
Poll         -> Item(value) | Empty | Closed
Close        -> NewlyClosed | AlreadyClosed

The model tracks capacity, FIFO contents, and closed state. Generate valid and invalid operations, compare return categories after every step, and assert invariants: length never exceeds capacity; accepted items are returned once; no offer succeeds after closure; FIFO order holds within the contract’s scope.

This sequential model does not prove linearizability under concurrent schedules. A concurrent extension records invocation and response intervals, generates small thread programs, and asks whether the observed history has a legal sequential ordering consistent with real-time constraints. Shrinking must reduce operations and threads while preserving the failing interleaving evidence. Seeds alone may not replay an OS schedule; deterministic schedule exploration requires a controlled scheduler or model checker.

Do not add sleeps to “encourage” races. They increase duration and nondeterminism without defining the schedule. Exact stress tests can be useful operational evidence, but label their probabilistic limits and retain any captured trace the harness can replay.

Define two campaigns before writing code

For wireview, specify:

• semantic and raw-byte generators, including size limits and invalid-input ratio;
• at least four properties, with preconditions and exact equality notions;
• a simple independent oracle or differential peer;
• structural and value shrink operations;
• deterministic seed/corpus retention;
• which minimized cases become exact tests and which protocol vectors become goldens.

For the bounded concurrent queue, specify:

• abstract state and command result categories;
• capacity, value, thread, and history generators;
• sequential invariants and the additional concurrent correctness criterion;
• how schedules are controlled or recorded;
• operation/thread shrink order;
• a presubmit budget and a deeper scheduled budget;
• what a failure artifact must contain to be replayable.

Reject answers that say only “use property testing” or “take a snapshot.” The engineering work is choosing the input domain, oracle, reduction order, determinism boundary, and regression destination.

Review behavior-space evidence

Before approving a generated or artifact-based suite, ask:

• Is the property written independently of the implementation?
• Does the generator cover boundaries and invalid classes rather than merely convenient random values?
• Are preconditions explicit, and can shrinking preserve them?
• Does every failure record enough versioned state to replay?
• Is the reference model simpler and independent, with abstraction limits documented?
• Could two differential peers share the same defect?
• Does each metamorphic relation follow from the actual contract?
• Does canonicalization remove only irrelevant variability?
• Can reviewers understand snapshot/golden changes without regenerating trust?
• Are minimized failures promoted to deterministic regression tests at the lowest layer that observes the whole contract?
• Are concurrency claims limited to schedules actually explored?

The search loop earns confidence only when it produces durable evidence. Generate broadly, compare against a meaningful oracle, shrink with domain knowledge, replay deterministically, and then place the regression at the correct architectural boundary. Fuzzers, interpreters, sanitizers, and schedule explorers can extend this loop; none repairs a missing oracle.

Sources and version notes

The executable fixture intentionally implements deterministic generation and shrinking with the standard library so its mechanics remain visible. Mature Rust projects usually use maintained ecosystem tools for strategy composition, persistence, snapshots, and model checking; pin their versions and verify current behavior before adopting them. The core distinctions in this chapter do not depend on one framework.

• The Rust Reference: testing attributes
• The Cargo Book: test targets and integration tests
• The rustdoc book: documentation tests and compile_fail
• The Rustonomicon: testing unsafe code with dynamic tools