Phase E (part 1): proptest property tests for spec §19 invariants - #11
Merged
Conversation
The two external reviews found bugs the existing test suite didn't catch. Per-subsystem unit + integration tests cover the happy paths; the bugs lived in cross-subsystem interactions (memtable × rollup × restart, dedupe × WAL × recovery, rollup × source/unit). Randomized property testing is the systematic answer. This PR adds tests/properties.rs with 7 properties, each running 32 random cases per CI run (224 total invariant checks): - raw_sum_equals_rollup_sum (§19.8) - duplicate_ingest_is_idempotent (§19.5) - compaction_preserves_sum (§19.9) - recovery_preserves_sum (§19.1) - recovery_preserves_sum_without_flush (§19.1, unflushed path) - rollup_tick_is_idempotent (§19.4) - conflict_when_same_id_different_payload (§19.6) Bug caught during writing: recovery_preserves_sum failed on a one-event input — restart was counting the event twice. Root cause: the harness's `force_flush` wrote segments and updated raw_segments but didn't rotate the WAL or advance last_sealed_wal_id. After restart, recovery replayed the still-active WAL into the memtable AND scanned the segment, so SUM doubled. Real production flusher does both; the harness now does too. (No production bug — just a regression-prone gap in the test harness that would have crept into more tests.) The harness mimics the production critical section synchronously, bypassing the channel/flusher worker for determinism. Each property spawns a fresh tempdir; cases=32 keeps CI quick. The shrunk failing case from the harness bug is committed in tests/properties.proptest-regressions so it re-runs on every CI run. Total tests: 66 (was 59; +7). Clean under RUSTFLAGS=-D warnings. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds randomized property tests for the spec §19 billing-safety invariants. Two external reviews caught real bugs the existing test suite missed — the bugs lived in cross-subsystem interactions, exactly the territory proptest covers. This is the first half of Phase E from the expanded roadmap; deterministic simulation testing (DST) is the larger follow-up.
Properties (7, 32 random cases each = 224 invariant checks per CI run)
raw_sum_equals_rollup_sumduplicate_ingest_is_idempotentcompaction_preserves_sumrecovery_preserves_sumrecovery_preserves_sum_without_flushrollup_tick_is_idempotentconflict_when_same_id_different_payloadBounded input space (
acc_a..acc_d, 3 meters, ts within one hour, quantity 1..1000) keeps each case quick — the full suite runs in <1s.Bug found while writing the tests
recovery_preserves_sumfailed on a one-event input: restart was double-counting. Root cause was in the harness, not production code — myforce_flushwrote segments + updatedraw_segmentsbut skipped the WAL rotation andlast_sealed_wal_idadvance. After "restart", recovery replayed the still-unsealed WAL into the memtable AND scanned the segment, doubling SUM. The fix mirrors what the production flusher does (rotate + bump watermark + delete sealed files). The shrunk case is committed totests/properties.proptest-regressionsso it re-runs on every CI run.No production bug, but a clear signal that the harness was about to grow more drift from production — better to catch it now.
Design notes
tokio::runtime::Builder::new_current_thread().build()+block_on— proptest isn't async-aware, so each case spins up its own runtime.tempfile::tempdir(); auto-cleaned on harness drop.Test plan
cargo build --all-targetsclean with-D warningscargo test --all-targets— 66 tests pass (was 59; +7 properties)Next in Phase E
Deterministic simulation testing — a state-machine driver that randomly interleaves
record/retry/flush/compact/rollup/crash-before-fsync/crash-after-fsync/corrupt-manifest/restart/queryover many steps and asserts every invariant. Much bigger than this PR; will land separately.🤖 Generated with Claude Code