Choice-tape shrink engine: Conjecture-style generation recording, shrinking, and persistence

[matthiasgoergens]

This PR ports the core idea of Python Hypothesis's Conjecture engine to proptest: record every random decision made during generation as a tape of typed choices, and implement shrinking as edits to that tape followed by re-running generation, accepting an edit iff the test still fails and the re-recorded tape is shorter or simpler. I mentioned this work in #657; this is the substantive part.

Why

The ValueTree shrinker has structural limits that show up in practice:

• Floats frequently do not shrink at all. BinarySearch::reposition jumps straight to the low clamp on the first simplify(), and if that passes, complicate() walks back to the original value and the search ends. A property failing at v >= 1.7 over 0.0..10.0 typically reports something like 8.700790202766044 as its "minimal" example. The tape engine reports 2.0, via a port of Hypothesis's lexicographic float encoding that makes round numbers the simplest ones.
• prop_filter strands the shrinker at locally minimal values, because simplify() cannot step over rejected values (the code even relaxes the simplify/complicate contract to cope). The tape engine re-vets every proposal through the filter during replay, so a filtered even-integer property failing at v >= 100 shrinks to exactly 100 instead of stopping at, say, 122.
• Each ValueTree shrinks in isolation, so nothing can lower two related values together. Issue Proptest fails to find trivial failing example (but Hypothesis does) #500 is the canonical report: a paging bug guarded by total_count % count == 0 was near-impossible to find and, when found by hardcoding, would not shrink. With this PR the divisibility witness is generated reliably and shrinks to exactly (0, 1) (measured over 100 seeds: 100 found, 100 fully minimal). There is a regression test.

The engine also changes what failures persist as: a ct1 entry in the regression file is the serialized choice tape of the shrunken failure, so replaying it regenerates the exact minimal values, independent of RNG algorithm or rand version, and tolerant of strategy refactors. Seed entries continue to work.

Finally, generation itself now hunts edge cases the way Hypothesis does: integer draws occasionally take exact boundary values (this is what finds #500), wide ranges mostly produce values near the shrink target with a uniform tail, and float draws occasionally inject bounds, one-ulp-inside-bounds values, and NaN where permitted. any::<i64>() now actually generates i64::MIN; the README example that says abs(i64::MIN) will "virtually always" survive testing now has a test asserting the opposite. This distribution change immediately found a real bug in this repository: Arbitrary for Duration could panic on nanosecond carry overflow (#657).

How it works

• TestRng owns a TapeState. The rand 0.10 TryRng impl is the interception seam: every raw draw any strategy makes is recorded as an untyped choice, so existing and third-party strategies participate with zero code changes, and replay pins their values positionally.
• Migrated strategies (integer and float ranges, int ANY, the class-based float Any, char, collections, union picks, and proptest-state-machine's sequential strategy) record typed choices with constraints and shrink targets, which is where the quality comes from. Collections and state-machine sequences use a continuation-flag encoding with spans, so a generic deletion pass removes elements or transitions; state-machine preconditions are re-checked against the re-evolved state during replay.
• The shrinker runs passes to a fixpoint under the existing max_shrink_iters/max_shrink_time budgets: all-choices-to-target, span deletion with exponential batching, cross-value redistribution ([27, 23] becomes [0, 50] and then [50] for a sum-guarded failure), joint lowering of duplicated values (a == b && a >= 10 shrinks to (10, 10)), and per-choice minimization with exponential probing from the target.
• Everything is behind Config::shrink_engine / PROPTEST_SHRINK_ENGINE. The ValueTree engine remains fully supported, is used automatically under fork/timeout, and is one config line away for anyone who prefers it.

Compatibility and defaults

No API breaks: every existing Strategy/ValueTree implementation compiles and runs unchanged, and a small tape API on TestRunner (draw_bool, spans, forced flags) is available for out-of-crate strategy implementations. The full test suites of proptest and proptest-state-machine pass under both engines.

Two deliberate behavior changes, called out in the CHANGELOG: the tape engine is the default shrinker, and the numeric generation distributions changed as described above. I believe these defaults are the right ones (they are what make the engine find and report the bugs above), but I am happy to make either or both opt-in if you prefer; each is a one-line change, and the rest of the PR stands either way.

Reading guide

The commits build the engine in review-sized steps: design document, core engine, collections and unions, float and char typing, cross-value passes, tape persistence, biased generation, default flip, and the state-machine migration. design/choice-tape-shrinking.md in the repo root is the full design writeup, and proptest/examples/shrink-quality.rs runs both engines side by side over a dozen representative properties if you want to see the difference locally.

[matthiasgoergens]

Here is a concrete demo of what this engine does to the oldest complaint class against proptest's shrinking: shrinking through prop_flat_map, the monadic bind.

The problem, as reported by users. #181 asks for "alternative approaches to prop_flat_map due to shrinking behavior": matrices generated as (rows, cols).prop_flat_map(|(r, c)| vec(elem, r * c)) shrink their elements but rarely their dimensions. nalgebra's proptest support ships that caveat in its documentation to this day: "shrinking takes place by first shrinking the matrix elements before trying to shrink the dimensions of the matrix", so that "a large number of shrinking iterations are necessary to find a (nearly) minimal failing test case". The book's tutorial example for prop_flat_map, a vector plus a valid index into it, has the same shape.

Why binds are hard for ValueTree. A ValueTree shrinks the finished value, and a bind splits the value across two trees: the outer one (the dimensions) and an inner one built from its current value (the elements). Every outer shrink invalidates the inner tree's progress, so the search keeps restarting, and under the default iteration budget it often gives up with the outer value untouched. The workarounds discussed in #181 (custom ValueTree implementations, matrix-specific combinators) stay inside that paradigm. Hypothesis solved this class of problem at the engine level instead: shrink the recorded choices and replay generation, so the dependent structure regenerates consistently on every attempt. That is what this PR ports. One coordinated pass, taken from Hypothesis's minimize_individual_nodes, lowers a length choice while deleting one element span behind it, which is the edit neither side can make alone.

Measured. 100 fixed seeds per case, both engines from this branch, default config. "Fully minimal" counts runs that reached the ideal minimum stated with each case; "worst result" is that engine's furthest miss.

case	engine	fully minimal	avg test calls	worst result
matrix, issue #181: (1..=8, 1..=8) flat_map vec(0..1000, r*c), fail iff any elem >= 10 ideal minimum: (1, 1, [10])	ValueTree	95/100	405	(1, 8, [0, 0, 0, 0, 0, 6, 400, 703])
	tape	98/100	69	(2, 3, [0, 0, 0, 0, 0, 10])
book's vec-and-index: (1..=32) flat_map (vec(0..1000, len), 0..len), fail iff v[i] >= 10 ideal minimum: ([10], 0)	ValueTree	100/100	298
	tape	100/100	51
length-prefixed sum: (1..=64) flat_map vec(0..1000, len..=len), fail iff sum >= 100 ideal minimum: [100]	ValueTree	89/100	557	[0, 0, 0, 0, 0, 10, 393, 453]
	tape	100/100	109
chained binds: a in 10..1000, b in 10..=a, c in 10..=b, fail always ideal minimum: (10, 10, 10)	ValueTree	100/100	112
	tape	100/100	2

Two things stand out beyond the minimality counts. The tape gets there in a fraction of the test executions (4x to 56x fewer), which matters for expensive properties. And when either engine falls short of the global minimum, the failure modes differ in kind: ValueTree's non-minimal results carry leftover random values (400, 703, 453), while the tape's worst case is a correctly minimized value with surplus structure around it.

The chained binds row is the purest illustration: three dependent draws through two binds, and the tape's first shrink attempt (set every choice to its target) lands on (10, 10, 10) immediately, because replaying generation keeps the dependency a >= b >= c intact by construction.

Reproducible demo code (drop into proptest/examples/flat-map-demo.rs on this branch)

use std::cell::Cell;
use std::fmt::Debug;

use proptest::collection::vec;
use proptest::prelude::*;
use proptest::test_runner::{
    Config, RngAlgorithm, ShrinkEngine, TestError, TestRng, TestRunner,
};

fn run_case<S: Strategy>(
    engine: ShrinkEngine,
    strategy: &S,
    fail: &impl Fn(&S::Value) -> bool,
    seed_byte: u8,
) -> (Option<S::Value>, u64)
where
    S::Value: Debug,
{
    let calls = Cell::new(0u64);
    let seed = [seed_byte; 32];
    let mut runner = TestRunner::new_with_rng(
        Config {
            shrink_engine: engine,
            failure_persistence: None,
            ..Config::default()
        },
        TestRng::from_seed(RngAlgorithm::ChaCha, &seed),
    );
    let result = runner.run(strategy, |v| {
        calls.set(calls.get() + 1);
        if fail(&v) {
            Err(TestCaseError::fail("demo failure"))
        } else {
            Ok(())
        }
    });
    match result {
        Err(TestError::Fail(_, value)) => (Some(value), calls.get()),
        _ => (None, calls.get()),
    }
}

fn stats<S: Strategy>(
    name: &str,
    strategy: S,
    fail: impl Fn(&S::Value) -> bool,
    is_minimal: impl Fn(&S::Value) -> bool,
) where
    S::Value: Debug,
{
    println!("{} -- 100 seeds", name);
    for (label, engine) in [
        ("valuetree", ShrinkEngine::ValueTree),
        ("tape", ShrinkEngine::Tape),
    ] {
        let mut found = 0u32;
        let mut minimal = 0u32;
        let mut total_calls = 0u64;
        let mut worst: Option<String> = None;
        for seed_byte in 0..100u8 {
            let (value, calls) = run_case(engine, &strategy, &fail, seed_byte);
            total_calls += calls;
            if let Some(v) = value {
                found += 1;
                if is_minimal(&v) {
                    minimal += 1;
                } else {
                    let s = format!("{:?}", v);
                    if worst.as_ref().map_or(true, |w| s.len() > w.len()) {
                        worst = Some(s);
                    }
                }
            }
        }
        println!(
            "  {:<10} found {:>3}/100, fully minimal {:>3}/100, avg {:>4} test calls, worst: {}",
            label,
            found,
            minimal,
            total_calls / 100,
            worst.unwrap_or_else(|| "-".to_owned())
        );
    }
    println!();
}

fn main() {
    stats(
        "matrix (issue #181)",
        (1usize..=8, 1usize..=8).prop_flat_map(|(r, c)| {
            vec(0i32..1000, r * c).prop_map(move |data| (r, c, data))
        }),
        |(_, _, data)| data.iter().any(|&x| x >= 10),
        |(r, c, data)| *r == 1 && *c == 1 && *data == vec![10],
    );

    stats(
        "vec-and-index (book tutorial)",
        (1usize..=32)
            .prop_flat_map(|len| (vec(0i32..1000, len..=len), 0..len)),
        |(v, i)| v[*i] >= 10,
        |(v, i)| v.len() == 1 && v[0] == 10 && *i == 0,
    );

    stats(
        "length-prefixed sum",
        (1usize..=64).prop_flat_map(|len| vec(0i32..1000, len..=len)),
        |v| v.iter().sum::<i32>() >= 100,
        |v| *v == vec![100],
    );

    stats(
        "chained binds",
        (10i32..1000)
            .prop_flat_map(|a| (Just(a), 10..=a))
            .prop_flat_map(|(a, b)| (Just(a), Just(b), 10..=b)),
        |_| true,
        |t| *t == (10, 10, 10),
    );
}

The coordinated lower-and-delete pass and issue #181's matrix case in the shrink-quality example are the two most recent commits on the branch; there is a regression test asserting that the length-prefixed case shrinks to exactly [100].