# Testing Matrix
Holt uses four validation layers. They are intentionally split by cost:
fast checks stay in PR CI, long durability campaigns run in nightly or
release-gate jobs.
## PR CI
Run on every push and pull request:
| Unit/integration | `cargo test --workspace --all-features --lib --tests --examples --locked` | API semantics, walker behavior, WAL replay, checkpoint recovery, view/range behavior, atomic batches |
| Doctests/examples | `cargo test --workspace --all-features --doc --locked`; example binaries | Public API examples stay buildable |
| Lint | `cargo fmt --all --check`; `cargo clippy --workspace --all-targets --all-features --locked -- -D warnings` | Formatting and warning-free code |
| Fuzz smoke | `cargo +nightly fuzz run atomic_model -- -runs=512` | Keeps the fuzz target building and exercises random API traces |
| Soak smoke | `tools/soak --mode normal` with a short run | Keeps the lifecycle harness buildable and catches obvious reopen regressions |
| Coverage | `cargo llvm-cov ...` | Prevents accidental coverage drops |
| Regression bench | `benches/ regression` | Catches large local performance regressions without comparator dependencies |
## Nightly Validation
`.github/workflows/nightly.yml` runs the expensive matrix on `main`.
| `fault-matrix` | Checkpoint write/delete/flush failpoints and WAL integration tests |
| `property-matrix` | Higher-count proptest oracle runs |
| `soak-normal` | Multi-thread lifecycle soak across async WAL, sync WAL, and constrained buffer-pool cases |
| `soak-crash` | Repeated `SIGKILL` with `wal_sync=true`; every acknowledged write must survive reopen |
| `fuzz-long` | Time-bounded libFuzzer campaign over the atomic/WAL/range/view model |
| `verified-model` | Manual Verus run for ART shape specs when a Verus binary is available |
## Fuzz Model
`fuzz/fuzz_targets/atomic_model.rs` compares Holt against a `BTreeMap`
oracle. The model covers:
- `put`, `delete`, `get`;
- `checkpoint` and `reopen` with `wal_sync=true`;
- `atomic` batches with create-only, compare-and-put, versioned delete,
version assertions, prefix-empty assertions, and rename;
- record range scans and prefix scans;
- delimiter rollup / `CommonPrefix` behavior;
- key-only scans through both owned iteration and borrowed visitor paths;
- scoped `View` snapshots and view-local key scans.
Long campaigns should preserve the minimized corpus under
`fuzz/corpus/atomic_model` only when the corpus entry represents a
useful new edge case.
## Soak Harness
`tools/soak` is the long-lifecycle validator.
Normal mode checks multi-threaded mixed operations, checkpoint, reopen,
and final oracle equality. Crash mode checks durability only for writes
that Holt acknowledged and the child recorded in the fsynced ack log.
Recommended release gate:
```sh
cargo run --manifest-path tools/soak/Cargo.toml --locked -- \
--mode normal --dir target/holt-soak-release --reset \
--duration-secs 21600 --keys 10000000 --ops 20000000 \
--threads 8 --buffer-pool 256 --wal-sync false
cargo run --manifest-path tools/soak/Cargo.toml --locked -- \
--mode crash --dir target/holt-soak-crash-release --reset \
--duration-secs 21600 --keys 100000 --ops 2000000 \
--buffer-pool 64 --wal-sync true \
--kill-min-ms 50 --kill-max-ms 5000
```
## Verified Model
`verified/` contains Verus specs for local ART invariants:
- Node4/16/48/256 capacity;
- grow/shrink capacity preservation;
- sorted child lookup and live-child guarantees;
- insert/remove arity preservation;
- prefix split branch shape;
- delimiter rollup bounds;
- virtual user-key terminator;
- leaf extent alignment.
Run it manually:
```sh
VERUS=/path/to/verus ./verified/verify.sh
```
The Verus model is not a proof of the entire Rust implementation. It
documents and checks the small structural invariants that the production
layout and walker code depend on.
## Known Gaps
These are not fully automated yet:
- disk-full / `ENOSPC`;
- permission changes and directory removal during operation;
- systematic manifest/blob bit-flip corruption injection;
- multi-process open contention;
- ThreadSanitizer or Loom-style concurrency model checking;
- long io_uring crash/soak on a real Linux NVMe host.