op-reth: model-based test of the proofs engine state machine

[einar-oplabs]

A randomized, model-based test of the proofs engine (rust/op-reth/crates/trie/src/engine): random interleavings of commits, reorgs, reverts, sync targets, flushes, failed saves, stale notifications and crashes, driven over reth's persistence model, with the store and the engine held to a reference model after every step. The engine's bugs are interleaving bugs (ethereum-optimism/protocol-team#464, #477, #478), and the deterministic cases of #23441 and #23449 only cover the interleavings someone thought of.

What the test does

New integration target rust/op-reth/crates/trie/tests/engine_model.rs (its own target so that it and the live target do not share a time budget):

• Reference model (tests/engine_model/model.rs): the canonical chain as the consensus layer holds it (hash, parent, state root per block), the proof window, a lower bound on what the store has persisted, the fork points whose hash the engine holds for certain, and the engine's possible states as a small set of (tip, sync target) candidates. Saves and the sync loop run in the background, so the model predicts a set of outcomes per step and the harness narrows it with the tip it observes once the engine settles. It knows nothing of the engine's internals.
• Simulated reth: the existing SimulatedReth from tests/live/simulated_reth.rs (a real BlockchainProvider driven by reth's threshold rule), extended with revert_to, crash_and_restart (loses everything above reth's persisted tip and reopens from the database) and a persisted accessor. Faults: a store wrapper whose next write transaction fails (tests/engine_model/faults.rs, for a failed save), and a block reported as replaced through a stale ChainCommitted delivered after reth reorged it away (the execute path then finds no parent state).
• Actions (tests/engine_model/actions.rs), chosen per step with proptest: Commit{n}, Reorg{depth, length}, Revert{depth}, SyncTo{n} (reth commits n blocks the engine only learns of through a sync target), Flush, FailNextSave, StaleCommit{depth, length}, BogusReorg (a one-block reorg on a parent no block has, at a fork point the engine knows), and Crash(Same) (drop the engine without flushing, reopen the store, spawn a fresh engine, sync_to(best), then reth rebuilds the lost blocks from the same chain and the harness delivers them as live notifications, with no WAL replay). Crash(Different) exists but only the tracked-bug run enables it.
• Invariants after every step (tests/engine_model/invariants.rs): the engine settles on a tip the model predicts within 30 s; the store's earliest and latest blocks are on the canonical chain; the latest is at or below the engine's tip and at or above what the store had persisted; the window holds at most its configured size; the stored state at the window's ends and at the last fork point serves proofs that hash to the canonical state root there (window and views read in one MDBX read transaction, so a concurrent save cannot prune a height from under the check); every valid delivery is taken (a ParentHashMismatch is accepted only where the model says the engine's tip at that height is another block, which a stale notification can cause); a reorg or revert at or below the window's earliest block is refused with UnwindBeyondEarliest naming an earliest block the window held around the call, and ends the case since reth moved on without the store; a reorg whose first block does not build on the stored fork block is refused with the stored hash; at the end of a case, after settling, fewer blocks than the persistence threshold stay buffered. Every engine call runs on its own thread with a 30 s bound, so a stalled or panicked engine fails the case instead of hanging it (op-reth: liveness test of the proofs engine under a slow store #23392).
• Shrinking: proptest shrinks the action sequence and the configuration; actions are interpreted against the current state (depths clamp to what reth holds in memory), so every sequence is valid. A failure prints the minimal sequence plus the harness transcript of each step (engine tip, store window, reth head), and the first failing case is printed as found, before shrinking, so a run that nextest cuts short still shows it. A tip the model allows on no path fails at once instead of waiting out the settle bound. ENGINE_MODEL_TRANSCRIPT=1 prints the transcript of passing cases too.
• Model unit tests (model.rs, rstest): the delivery rules (at or below the tip, next block, parent state missing, beyond the next block, mid-sync, refusals on a stale tip), reorg and revert skip-or-unwind, settling, and the restart bounds.

Matrix

Sampled per case: reth persistence threshold {7, 50} x state masking {0; 30 only with threshold 50, since reth rejects masking + buffer target >= threshold} x memory-block-buffer target {5} x engine (persistence, backpressure) thresholds {(1, 2), (5, 10)} x proofs path by verification interval {0 (index), 1 (execute), 4 (mixed)} x proof window {1000 (never pruned), 4 (pruned on every save)}. Store: MdbxProofsStorage in a tempdir. Masking is a parameter of the persistence model only: on develop reth has no partial persistence, so it only decides which persisted blocks stay in memory (see #23441).

Default 24 cases, up to 24 steps each; PROPTEST_CASES=<n> raises it (the config goes through contextualize_config, so the other PROPTEST_* variables apply too). rust/.config/nextest.toml gives the engine_model binary a 1 m slow period and a 5 m limit, since the whole proptest is one test and a failing case shrinks for up to a minute on top of the run.

Seams

• EngineHandle::tip() under cfg(any(test, feature = "test-utils")), next to flush(): the model has to wait for the sync loop to settle without side effects, and the only other way to read the tip (probing with a block above it) raises the sync target when the engine is behind.
• tests/live/chain.rs: the chain and store helpers of tests/live.rs, moved so that both integration targets share them (tests/live.rs keeps its scenario runner and tests).
• SimulatedReth::{persisted, revert_to, crash_and_restart}, and reorg_block, reorg_block_without_data and UNRELATED_PARENT moved there from reorg_revert_edges.rs so both targets share them; BlockView::read_from(provider, ...) and ProofTarget::accounts(...).

Left for later, from the rust-code-reviewer pass: a shared DiskSnapshot in store_view.rs (reorg_revert_edges.rs has one), one store wrapper with hooks instead of StoreWithSaveFaults, StoreWithWriteGate and StoreWithReadHook, and Scenario::assert_tip reading engine.tip() instead of probing.

Local verification

cd rust
cargo test -p reth-optimism-trie --test engine_model
# test result: ok. 17 passed; 0 failed; 3 ignored; finished in 14.01s  (the proptest at 24 cases plus the model's unit cases)

PROPTEST_CASES=120 cargo test -p reth-optimism-trie --test engine_model
# test result: ok. 17 passed; 0 failed; 3 ignored; finished in 62.54s
# (an earlier 200-case run before the review pass: 99.01s)

cargo nextest run -p reth-optimism-trie --test engine_model
# Summary [  21.027s] 17 tests run: 17 passed, 3 skipped

cargo test -p reth-optimism-trie --test live
# test result: ok. 129 passed; 0 failed; 16 ignored; finished in 53.75s

cargo test -p reth-optimism-trie
# unittests 249 passed in 25.78s; engine_model 12.92s; tests/lib 0.16s; live 54.89s; doctests 0.26s: about 94 s in all (run before the review pass)

cargo clippy -p reth-optimism-trie --all-targets --all-features -- -D warnings   # clean
cargo +nightly-2026-08-22 fmt --all -- --check                                   # clean

Tracked bugs reproduced (ignored, naming the issue)

ethereum-optimism/protocol-team#464 (store ahead of reth after an unclean shutdown). engine_and_store_follow_the_model_through_crashes_rebuilding_a_different_chain is the random run with Crash(Different) enabled; it shrinks to the two-step sequence that store_follows_reth_through_a_crash_rebuilding_a_different_chain replays deterministically:

minimal failing input: config = Config { cadence: (persistence 1, backpressure 2), persistence: threshold 7, verification_interval: 0, window: 1000 },
actions = [Commit { count: 1 }, Crash(Different)]

Error: the store's latest block 1:0x1e41e789dfc0bb9a57adb1b27b9a31fce50bb89feacc13f39c0f3295ee19f307 is not on the canonical chain, whose block 1 is 0x4f527f04ca93da271b1fd73d0e552863b36888b1b9852b5ab312ad8f72a2a20b
--- steps ---
step 0: Commit { count: 1 }
  engine tip 1, store blocks 0..=0, reth head 1
step 1: Crash(Different)
  crash: reth loses blocks 1..=1 and rebuilds them (Different)
  restart: the store serves through block 1, reth's head is 0

The harness restarts the ExEx the way it starts today (fresh engine, sync_to(best), live notifications). #23358 adds a startup reconcile to the ExEx; the PR that un-skips these cases has to add the same step to Harness::crash.

ethereum-optimism/protocol-team#478 (FinishedHeight acknowledges heights not yet persisted). sync_loop_completes_while_reth_prunes_bodies_through_the_acknowledged_tip runs [SyncTo { count: 40 }, Commit { count: 1 }] with reth pruning bodies through the acknowledged tip (Config::body_pruning):

Error: the engine did not settle within 30s: its tip is NumHash { number: 0, hash: 0x37f157e831e926dc33d479b5c3a6fabefdeeffd9e1735075959b45878a66602b }, the model expects one of [NumHash { number: 40, hash: 0x178862dcc49ec13002cb60187c4a81b188b0cd36ac274a5a943cd02323b04ecc }], the store holds blocks 0..=0
--- steps ---
step 0: SyncTo { count: 40 }
  reth pruned bodies through block 32

The pruner model is SimulatedReth::prune_bodies_through from #23449, called with the notification tip the ExEx acknowledges.

Findings from the random runs

• The first runs failed on a harness race, not an engine bug: reading the window and the block views in separate read transactions let a save that pruned the window land in between. BlockView::read_from reads them from one transaction now.
• A stale ChainCommitted whose parent the sync loop has already replaced makes the engine return ParentHashMismatch (its tip at that height is the replacing block). That is the engine's contract and the model predicts it; for the ExEx it is fatal (handle_notification returns the error). The window is narrow (the loop has to cross the reorg point while the ExEx processes the stale notification) and no issue tracks it yet; it is not reproduced deterministically here.

Stacked on #23449, #23445, #23442, #23441, #23437, #23434, #23429, #23428, #23421 and #23418.

Closes #23381

🤖 Generated with Claude Code

CI follow-up: the window invariant holds on both reth pins

engine_and_store_follow_the_model held the store to latest - earliest <= window, which only develop's pruner satisfies; the pruner of the reth 2.6 bump with #23358 prunes no further than reth's persisted head, so the store legitimately keeps more under a short window while reth's persistence lags (the store holds blocks 0..=5, more than its window of 4). The model now records reth's persisted head at each block's commit and requires the earliest block to lie in max(0, min(latest - window, persisted_at_commit(latest))) ..= max(0, highest_head - window), which holds under either pruner (on develop the lower end is weaker than the old latest - window, the price of being pin-agnostic). The commit explains why this was chosen over keeping reth persisted through latest - window at every save: that is not equivalent, since it caps reth's in-memory chain at the window and keeps the cap from ever binding. The two Crash(Different) cases stay ignored (#464; they need #23358's startup reconcile in the harness). Verified with cargo test -p reth-optimism-trie --test engine_model: 23 passed, 3 ignored on develop; on the bump evaluation tree engine_and_store_follow_the_model and the model's unit tests pass (its un-ignored Crash(Different) cases fail there for the #464 reason, unchanged).