Automated GUMBOX Property-Based Testing of Thread Components

This chapter describes automated GUMBOX property-based testing — the third and most automated of HAMR’s component testing styles. In this style, the PropTest framework is used to generate random input test vectors from HAMR-generated value strategies, and the same contract-based harnesses introduced in the Manual GUMBOX Testing chapter judge every vector against the executable (GUMBOX) form of the component’s GUMBO contracts. It continues with the same running examples: the Simple Isolette from the HAMR tutorials repository, in its data-port (P-DP) and event-data-port (P-EDP) variants, centered on the Thermostat thread.

We assume you have read the GUMBO Component Contracts chapter (the contracts being tested), the GUMBOX translation chapter (the executable oracles), and — as the immediate prerequisite — the Manual GUMBOX Testing chapter, whose harness family (testInitializeCB/testComputeCB/testComputeCBwGSV), HarnessResult outcomes, and #[serial] discipline this chapter uses without re-introduction. The base infrastructure chapter, Manual Unit Testing, remains the reference for the test folder layout, running tests, and coverage.

The PropTest libraries which we use have many features which we do not explain here. The goal in this chapter is to explain the basic ways in which HAMR uses PropTest. “Power users” will want to continue on with the extensive documentation provided by PropTest.

This chapter completes HAMR’s three-style testing series — plain manual, manual GUMBOX, and property-based GUMBOX — all driven by the single GUMBO specification.

Why Property-Based Tests?

A GUMBO compute contract is, read as a whole, a property: for every admissible input vector and pre-state, the dispatch’s outputs satisfy the postcondition oracle. Manual GUMBOX tests sample that universal claim at specific developer-chosen points; Verus proves it outright. Property-based testing occupies the wide middle ground: it samples the claim at hundreds of random points per run, mechanically reaching input combinations no engineer thought to write down.

What that buys, concretely:

• Breadth at zero specification cost. One macro invocation yields (by default) one hundred contract-checked dispatches with fresh random vectors on every run. The oracles, the harnesses, and the value generators are all HAMR-generated from the model — the developer writes configuration, not test logic.
• The inputs you didn’t think of. Hand-chosen vectors cluster around the scenarios their authors imagined. Random generation is indifferent to imagination — it lands on odd combinations of pre-state, message presence, and boundary-adjacent values, which is precisely where interacting-clause bugs hide.
• Works from day one. The initial tests.rs skeleton that HAMR generates already contains ready-to-run macro invocations wired to the default strategies — property-based testing is available the moment code generation completes, before any manual test has been written.
• A dynamic approximation of verification. The property being sampled is the same ∀-statement the Verus contracts state (i.e., “for all component input port values and state variable values that satisfy the pre-condition, the post-condition holds.”). A property-based campaign is a cheap, evidence-producing rehearsal for verification — and after verification, a continuing audit of what the proof takes on trust (below).

What it does not replace: the chosen, requirement-linked, citable scenarios of manual GUMBOX tests, and manual tests’ role in validating the specification itself. The styles are complements; the Manual GUMBOX Testing chapter develops that comparison from the other side.

Where the Support Is Generated

Property-based testing adds two generated ingredients to the testing infrastructure already in the component crate:

• src/test/util/generators.rs — one value strategy per model data type (plus Option helpers), in default and customizable forms (below);
• the three PropTest macros — testInitializeCB_macro!, testComputeCB_macro!, testComputeCBwGSV_macro! — exported from src/test/util/cb_apis.rs alongside the harnesses they drive.

Both files are fully auto-generated and regenerated with the model. The macro invocations — which strategies to use, how many cases to run — live in the developer-edited tests.rs, conventionally in a mod GUMBOX_tests module beside the manual test modules; HAMR seeds that module in the initial skeleton with default-strategy invocations for every entry point. For the DP thermostat see generators.rs and the GUMBOX_tests module of tests.rs; the EDP example has files of the same names.

The PropTest Macros

Each macro expands to a complete PropTest-driven test function around one harness. The DP testComputeCBwGSV_macro! (generated code, verbatim) shows the shape:

#[macro_export]
macro_rules!
testComputeCBwGSV_macro {
  (
    $test_name: ident,
    config: $config:expr,
    In_lastCmd: $In_lastCmd_strat:expr,
    api_current_temp: $api_current_temp_strat:expr,
    api_desired_temp: $api_desired_temp_strat:expr
  ) => {
    proptest!{
      #![proptest_config($config)]
      #[test]
      #[serial]
      fn $test_name(
        (In_lastCmd, api_current_temp, api_desired_temp)
            in ($In_lastCmd_strat, $api_current_temp_strat, $api_desired_temp_strat)
      ) {
        match $crate::test::util::cb_apis::testComputeCBwGSV(In_lastCmd, api_current_temp, api_desired_temp) {
          $crate::test::util::cb_apis::HarnessResult::RejectedPrecondition => {
            return Err(proptest::test_runner::TestCaseError::reject(
              "Precondition failed: invalid input combination",
            ))
          }
          $crate::test::util::cb_apis::HarnessResult::FailedPostcondition(e) => {
            return Err(e)
          }
          $crate::test::util::cb_apis::HarnessResult::Passed => { }
        }
      }
    }
  };
}

Reading the expansion:

• The caller supplies a test name, a ProptestConfig, and one strategy per harness parameter — here the pre-state In_lastCmd and the two input ports. (The macro’s parameter list mirrors the harness’s; the EDP variant accordingly takes five strategies: In_currentSetPoints, In_lastCmd, api_desired_temp, api_temp_changed, api_current_temp.)
• PropTest draws a tuple from the strategies and calls the same harness a manual test calls; the three HarnessResult outcomes map onto PropTest’s vocabulary:
  • RejectedPrecondition → TestCaseError::reject(...) — the vector is discarded as inapplicable and PropTest draws another, counting it against the rejection budget (next section);
  • FailedPostcondition(e) → Err(e) — a genuine test failure: the implementation violated the contract on this vector;
  • Passed → the case succeeds and the next vector is drawn.
• #[serial] is baked into the expansion, so the generated test respects the same serialization discipline as every other component test.

testComputeCB_macro! is identical minus the pre-state strategies (each drawn vector runs against the freshly initialized component), and testInitializeCB_macro! takes only a config — initialization has no inputs, so its “property” is simply that the initialize contract holds, checked cases times.

Configuring a Run

The skeleton GUMBOX_tests module defines three constants whose generated comments state the configuration model (DP tests.rs, verbatim):

  // number of valid (i.e., non-rejected) test cases that must be executed for the compute method.
  const numValidComputeTestCases: u32 = 100;

  // how many total test cases (valid + rejected) that may be attempted.
  //   0 means all inputs must satisfy the precondition (if present),
  //   5 means at most 5 rejected inputs are allowed per valid test case
  const computeRejectRatio: u32 = 5;

  const verbosity: u32 = 2;

which feed the ProptestConfig in every invocation:

    config: ProptestConfig {
      cases: numValidComputeTestCases,
      max_global_rejects: numValidComputeTestCases * computeRejectRatio,
      verbose: verbosity,
      ..ProptestConfig::default()
    }

• cases — how many valid (non-rejected) vectors the run must execute. Every one of them is a full contract-checked dispatch.
• max_global_rejects — the rejection budget: the total number of RejectedPrecondition outcomes tolerated across the run. With the defaults, up to 500 rejects may be spent finding 100 valid vectors. If the budget is exhausted first, the test fails — but with a “too many global rejects” diagnosis, which means your strategies are generating mostly inadmissible vectors, not that the component violated its contract. Tightening the strategies (next sections) is the remedy.
• verbose — PropTest’s logging level (2 traces each case; lower it once a suite is stable).

The Generated Value Strategies

generators.rs provides a strategy — a PropTest value generator — for each model data type, in two forms following a uniform naming convention:

The generated code composes cleanly because each _default is defined in terms of its _cust. For the Isolette’s data types (verbatim):

pub fn Isolette_Data_Model_On_Off_strategy_cust(
  Onn_bias: u32,
  Off_bias: u32) -> impl Strategy<Value = Isolette_Data_Model::On_Off>
{
  prop_oneof![
    Onn_bias => Just(Isolette_Data_Model::On_Off::Onn),
    Off_bias => Just(Isolette_Data_Model::On_Off::Off)
  ]
}

pub fn Isolette_Data_Model_Temp_strategy_default() -> impl Strategy<Value = Isolette_Data_Model::Temp>
{
  Isolette_Data_Model_Temp_strategy_cust(
    any::<i32>()
  )
}

pub fn Isolette_Data_Model_Temp_strategy_cust<degrees_i32_strategy: Strategy<Value = i32>> (degrees_strategy: degrees_i32_strategy) -> impl Strategy<Value = Isolette_Data_Model::Temp>
{
  (degrees_strategy).prop_map(|(degrees)| {
    Isolette_Data_Model::Temp { degrees }
  })
}

pub fn Isolette_Data_Model_Set_Points_strategy_cust
  <lower_Isolette_Data_Model_Temp_strategy: Strategy<Value = Isolette_Data_Model::Temp>, 
   upper_Isolette_Data_Model_Temp_strategy: Strategy<Value = Isolette_Data_Model::Temp>> (
  lower_strategy: lower_Isolette_Data_Model_Temp_strategy,
  upper_strategy: upper_Isolette_Data_Model_Temp_strategy) -> impl Strategy<Value = Isolette_Data_Model::Set_Points>
{
  (lower_strategy, upper_strategy).prop_map(|(lower, upper)| {
    Isolette_Data_Model::Set_Points { lower, upper }
  })
}

Read the pattern by type kind: an enum strategy takes one weight per variant (so _cust(0, 1) excludes Onn entirely, _cust(5, 1) biases toward it); a struct strategy takes one sub-strategy per field (so Temp_strategy_cust(94..=105) draws degrees from a range instead of all of i32 — Rust ranges are themselves PropTest strategies); and nesting composes (a custom Set_Points takes two custom Temp strategies). For event data ports, the Option helpers control message presence:

pub fn option_strategy_bias
  <T: Clone + std::fmt::Debug, 
   S:  Strategy<Value = T>> (
  bias: u32,
  base: S) -> impl Strategy<Value = Option<T>>
{
  prop_oneof![
    bias => base.prop_map(Some),
    1 => Just(None),
  ]
}

option_strategy_bias(3, s) yields a message three-quarters of the time; option_strategy_default(s) is the 1:1 case; and PropTest’s own Just(None) / s.prop_map(Some) give the two extremes. Presence ratios are a genuinely EDP-specific testing dimension — how often each port has traffic shapes which contract clauses get exercised (below).

The Rejection Problem, and Custom Ranges (DP)

The defaults are deliberately naive: Temp_strategy_default() draws degrees from all of i32. Now recall the thermostat’s precondition oracle (GUMBOX translation): the integration assume ASSM_CT_Range admits only temperatures in [95, 104] — ten values out of 2³², so a uniformly random vector is admissible with probability effectively zero. A default-strategy compute campaign burns its entire rejection budget without ever finding 100 valid vectors and fails with “too many global rejects.”

This is why the DP solution’s GUMBOX_tests module keeps the default-strategy compute invocations commented out (preserved as a teaching artifact) and runs a custom-range campaign instead (verbatim):

  testComputeCBwGSV_macro! {
    prop_testComputeCBwGSV_REQ2thru4, // test name
    config: ProptestConfig { // proptest configuration, built by overriding fields from default config
      cases: numValidComputeTestCases,
      max_global_rejects: numValidComputeTestCases * computeRejectRatio,
      verbose: verbosity,
      ..ProptestConfig::default()
    },
    // Replace the default strategies with strategies for custom ranges
    In_lastCmd: generators::Isolette_Data_Model_On_Off_strategy_default(),
    api_current_temp: generators::Isolette_Data_Model_Temp_strategy_cust(94..=105),
    api_desired_temp: generators::Isolette_Data_Model_Set_Points_strategy_cust(
      generators::Isolette_Data_Model_Temp_strategy_cust(94..=103),
      generators::Isolette_Data_Model_Temp_strategy_cust(97..=105)
    )
  }

Two design choices are worth noticing:

• The ranges deliberately overshoot the envelope. api_current_temp draws from [94, 105] while the contract admits [95, 104]; the set-point fields draw from overlapping-but-independent ranges, so lower > upper (violating ASSM_LDT_LE_UDT) is still occasionally generated. Some vectors are therefore still rejected — by design. Sampling just outside the envelope means the precondition oracle itself gets exercised at its boundary, and the rejection budget (5 rejects per valid case) absorbs the cost comfortably. Strategies need to be tight enough to stay within budget, not perfectly tight.
• Enum strategy stays default. On_Off has two admissible values; nothing to constrain. Customization effort goes where the admissibility gap is.

The general recipe: read the component’s precondition oracle (compute_CEP_Pre), and shape each parameter’s strategy so that a healthy majority of drawn vectors satisfy it — using _cust ranges for numeric fields and variant weights for enums.

Correlated Strategies and Targeted Campaigns (the EDP variant)

The EDP thermostat pushes strategy design two steps further. Its GUMBOX_tests module opens with the plan (verbatim comment):

Automated property-based GUMBOX tests: PropTest generates random input vectors from the strategies below; the GUMBOX oracles check the GUMBO contract on every vector. Vectors that violate the preconditions (integration assumes, INV_CSP) are rejected — the custom strategies below are constrained so that rejections are rare by construction.

Step one: correlated generation for cross-field constraints. The generated Set_Points_strategy_cust takes independent strategies for lower and upper — so no choice of ranges can guarantee lower <= upper, and with the EDP variant needing well-formed set points in two places (the INV_CSP compute assume on the latched pre-state, and the ASSM_LDT_LE_UDT integration assume on arriving messages), independent generation would reject constantly. The suite defines a hand-written correlated strategy instead (verbatim, with its explanatory comment):

  // Correlated strategy for WELL-FORMED set points (lower <= upper): the
  // generated Set_Points_strategy_cust takes independent strategies for the
  // two fields and so cannot enforce the cross-field constraint -- generating
  // (lower, delta) pairs instead makes precondition rejections impossible.
  fn well_formed_set_points_strategy() -> impl Strategy<Value = Set_Points> {
    (95i32..=104i32, 0i32..=9i32).prop_map(|(lo, d)| Set_Points {
      lower: Temp { degrees: lo },
      upper: Temp { degrees: if lo + d > 104 { 104 } else { lo + d } },
    })
  }

  // Sensed temperatures within the ASSM_CT_Range integration assume [95, 104]
  fn sensed_temp_strategy() -> impl Strategy<Value = Temp> {
    generators::Isolette_Data_Model_Temp_strategy_cust(95i32..=104i32)
  }

Drawing (lower, delta) and computing upper = lower + delta makes ill-formed set points impossible rather than merely rare — the constraint holds by construction. This is the standard move whenever a precondition relates multiple fields: generate the degrees of freedom, derive the constrained value. (Custom strategies are ordinary PropTest code; HAMR’s generated strategies are the building blocks, not a ceiling.)

Step two: multiple campaigns, each aimed at a behavior regime. Rather than one macro invocation, the EDP suite runs four. The broad one randomizes everything — latched pre-state, both message ports (with a 3:1 presence bias on set-point messages), and the sensed temperature:

  testComputeCBwGSV_macro! {
    prop_testComputeCBwGSV_macro, // test name
    config: ProptestConfig {
      cases: numValidComputeTestCases,
      max_global_rejects: numValidComputeTestCases * computeRejectRatio,
      verbose: verbosity,
      ..ProptestConfig::default()
    },
    // strategies for generating each component input
    In_currentSetPoints: well_formed_set_points_strategy(),
    In_lastCmd: generators::Isolette_Data_Model_On_Off_strategy_default(),
    api_desired_temp: generators::option_strategy_bias(3, well_formed_set_points_strategy()),
    api_temp_changed: generators::option_strategy_default(sensed_temp_strategy()),
    api_current_temp: sensed_temp_strategy()
  }

and two focused variants pin some parameters with Just(...) to concentrate the randomness where it matters. The boundary-biased campaign fixes the latched range and draws the temperature only from the five values straddling its thresholds:

  testComputeCBwGSV_macro! {
    prop_testComputeCBwGSV_boundary_biased, // test name
    config: ProptestConfig {
      cases: numValidComputeTestCases,
      max_global_rejects: numValidComputeTestCases * computeRejectRatio,
      verbose: verbosity,
      ..ProptestConfig::default()
    },
    In_currentSetPoints: Just(Set_Points { lower: Temp { degrees: 98 }, upper: Temp { degrees: 101 } }),
    In_lastCmd: generators::Isolette_Data_Model_On_Off_strategy_default(),
    api_desired_temp: Just(None::<Set_Points>),
    api_temp_changed: generators::option_strategy_bias(3, sensed_temp_strategy()),
    api_current_temp: prop_oneof![
      Just(Temp { degrees: 97 }),   // just below lower
      Just(Temp { degrees: 98 }),   // at lower
      Just(Temp { degrees: 100 }),  // in range
      Just(Temp { degrees: 101 }),  // at upper
      Just(Temp { degrees: 102 })   // just above upper
    ]
  }

and the no-event-biased campaign sets both event ports to Just(None), so all one hundred cases exercise the frame-condition clauses (noTriggerNoChange, noSendNoChange) that a broad campaign hits only when the random draw happens to produce a quiet dispatch:

    In_currentSetPoints: well_formed_set_points_strategy(),
    In_lastCmd: generators::Isolette_Data_Model_On_Off_strategy_default(),
    api_desired_temp: Just(None::<Set_Points>),
    api_temp_changed: Just(None::<Temp>),
    api_current_temp: sensed_temp_strategy()

The principle generalizes: one broad campaign for the input space at large, plus a focused campaign per behavior regime — each regime identified by reading the contract’s cases and guards (GUMBOX EDP semantics) and asking which clauses a uniform draw would rarely make non-vacuous.

Interpreting Results and Failures

A passing run of a compute campaign certifies: cases admissible random vectors were dispatched, and every one satisfied the entire postcondition oracle — the same per-vector meaning as a manual GUMBOX Passed (Manual GUMBOX Testing chapter), multiplied by volume and refreshed with new vectors on every run.

When a case fails (FailedPostcondition), PropTest does two useful things beyond reporting: it shrinks the failing vector — repeatedly simplifying it while the failure persists, converging toward a minimal failing case that is far easier to read than the original random draw — and it persists the failure (by default in a proptest-regressions/ file next to the test source) so subsequent runs replay the exact failing case first, before generating new ones. See the PropTest book for the mechanics. The recommended follow-up in the HAMR workflow: freeze the shrunk vector as a manual GUMBOX regression test (it is already in exactly the harness’s parameter shape), and if the reason for the violation is unclear, probe the individual clause oracles with the vector’s values to localize which clause failed and why (Interrogating a Contract).

The third outcome — a run aborting with too many global rejects — is a strategy problem, not a component problem: your generators are producing mostly inadmissible vectors. Tighten ranges, add correlation, or raise the rejection budget, in that order of preference (a bigger budget spends time; better strategies spend it on real dispatches).

Running the Campaigns, and Coverage

Property-based tests are ordinary cargo tests, so everything in the manual chapters applies (running tests); the useful specifics:

• Just the property-based suite: the shared prop_ prefix and the module name make filtering easy — make test args=prop or cargo test GUMBOX_tests from the crate directory.
• One campaign: cargo test prop_testComputeCBwGSV_boundary_biased.
• All crates: top-level make test from hamr/microkit/.
• Output: cargo test -- --nocapture streams per-case logging (with verbose: 2, PropTest traces every case — expect a lot of it at hundreds of cases per campaign).
• Runtime: each campaign is cases full dispatches, and each vector passes through initialization plus the complete oracle; keep cases proportionate as component counts grow, and remember #[serial] means campaigns run one at a time.

Coverage closes a loop opened in the Manual Unit Testing chapter. Its Gap 2 analysis showed a thin manual suite leaving the consequent lines of compute_case_REQ_THERM_2/_3 in *_GUMBOX.rs with zero hits — those requirements were only ever checked vacuously — and observed that this “is precisely the signal that the auto-generated propTest macros are designed to fix: by sweeping inputs across the full range of each generator, they drive the antecedent of every case to true at least once, lighting up the consequent.” Run make coverage args=prop (or the full suite) and confirm exactly that: with well-shaped strategies, every case oracle’s consequent shows hits, meaning every requirement clause was genuinely — not vacuously — exercised.

Relation to Verus Verification

Property-based GUMBOX testing and Verus verification address the same universal statement — every admissible dispatch satisfies the contract — one by sampling, one by proof. That makes them natural partners at both ends of the verification workflow:

• Before proving: a property-based campaign is the highest-volume, lowest-effort bug filter available. Implementation errors that would surface as Verus proof failures surface first as shrunk, concrete counterexamples — cheaper to diagnose and already in test-vector form. Clearing the campaigns before running make verus reserves proof effort for what testing cannot find.
• After proving: a verified component must pass every admissible vector any campaign can generate (the proof covers them all). A FailedPostcondition on verified code therefore points at the trusted base — external_body helpers, the test-mode environment — rather than the proved logic. Leaving the campaigns in the suite makes every CI run a continuing randomized audit of exactly the parts the proof takes on trust.

And when a campaign fails while a proof attempt is also failing, the shrunk vector is a ready-made concrete explanation of the abstract proof failure — the workflow developed in Explaining Verus Failures.

The Testing Series, Complete

This chapter closes HAMR’s component-testing series. The three styles, in one view:

All three run against the same generated infrastructure, and the two GUMBOX styles consume the same specification that drives Verus verification — one set of GUMBO contracts, authored once at the model level (GUMBO Component Contracts), translated once into executable and logical form.

For hands-on practice, Part 2 of the tutorial series Adding GUMBO Thread Component Contracts to an Existing System includes the property-based campaigns shown here — see Part 2 or follow the Recommended Reading Order.