`just mutants-store` (64 random cases per mutant, temp books on a RAM disk in CI) runs beside the core's weekly; fuzz_store_replay joins the weekly fuzz matrix. docs/testing.md lists the spec-blind store suite, the refusal property's converse law, and the replay fuzz oracles. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX
This commit is contained in:
1 parent
4d8d5daf37
commit
db00b74e82
4 files changed
+16
-5
No files matched your search
@@ -22,7 +22,7 @@ jobs:
|
||||
strategy:
|
||||
fail-fast: false
|
||||
matrix:
|
||||
target: [fuzz_journal_line, fuzz_entry_validate, fuzz_op_sequence, fuzz_core_serde, fuzz_store_open]
|
||||
target: [fuzz_journal_line, fuzz_entry_validate, fuzz_op_sequence, fuzz_core_serde, fuzz_store_open, fuzz_store_replay]
|
||||
steps:
|
||||
- uses: actions/checkout@v4
|
||||
- uses: jdx/mise-action@v2
|
||||
@@ -33,8 +33,11 @@ jobs:
|
||||
- uses: actions/checkout@v4
|
||||
- uses: jdx/mise-action@v2
|
||||
- run: just mutants
|
||||
- run: TMPDIR=/dev/shm just mutants-store
|
||||
- if: always()
|
||||
uses: actions/upload-artifact@v4
|
||||
with:
|
||||
name: mutants
|
||||
path: mutants.out
|
||||
path: |
|
||||
mutants.out
|
||||
mutants-store/mutants.out
|
||||
@@ -3,3 +3,5 @@
|
||||
.DS_Store
|
||||
site/dist/
|
||||
.netlify/
|
||||
/mutants.out*/
|
||||
/mutants-store/
|
||||
+3
-3
@@ -10,19 +10,19 @@ the store's journal safety; the other crates come next (gap list).
|
||||
|
||||
| Layer | Oracle (rank) | Where | Command | Runtime | Gates |
|
||||
|---|---|---|---|---|---|
|
||||
| Spec-derived examples | written specs with sources (1) | `tests/spec_*.rs`, `invariants.rs`, `statements.rs`, `assets.rs`, ... | `just check` | seconds | every change |
|
||||
| Spec-derived examples | written specs with sources (1) | `tests/spec_*.rs`, `invariants.rs`, `statements.rs`, `assets.rs`, ...; the store's `tests/spec_store.rs` (written blind, from its specs only) | `just check` | seconds | every change |
|
||||
| Regressions | the bug, named (1) | beside the code they cover, `*_regression`/named for the defect | `just check` | seconds | every change |
|
||||
| Compatibility contracts | journals written under older rules must open (1) | `ledger-store/tests/store.rs` (`books_written_under_older_rules_still_open`) | `just check` | <1s | every change |
|
||||
| Properties | laws over all inputs (2) | `properties.rs`, `spec_*.rs`, `kernel_bridge.rs` | `just check` | seconds | every change |
|
||||
| Metamorphic | scaling, reversal, ordering invariance (2) | `spec_reports.rs` | `just check` | seconds | every change |
|
||||
| Refusal law (store) | a refused command never reaches the journal; the books reopen to the same reports (2, 3) | `store.rs` `refused_commands_never_reach_the_journal` | `just check` (`STORE_CASES=5000` deeper) | ~20s | every change |
|
||||
| Refusal law (store) | a refused command never reaches the journal, an accepted one always does; the live ledger equals its journal's replay in every part, and the books reopen to it (2, 3) | `store.rs` `refused_commands_never_reach_the_journal` | `just check` (`STORE_CASES=5000` deeper) | ~20s | every change |
|
||||
| Fault injection (store) | a full disk or a cut-off append leaves whole, openable books (1) | `ledger-store/tests/faults.rs`, `store.rs` (`power_loss_at_any_byte_of_the_last_append_is_recovered`) | `just check` | ~5s | every change |
|
||||
| Concurrency (store) | a viewer reading while the books are written sees only whole books, never a false "differs" (2) | `ledger-store/tests/concurrency.rs` | `just check` | <1s | every change |
|
||||
| Model-based stateful | the Lean state machine, transcribed (3) | `tests/model.rs` | `just check` | ~3s | every change |
|
||||
| Differential: Decimal vs i64 | the kernel at two types (3) | `kernel_bridge.rs` | `just check` | <1s | every change |
|
||||
| Differential: GnuCash | another implementation, adjudicated (3) | `tests/oracle_gnucash.rs`, `oracle/gnucash/` | `just oracle` | ~2 min | weekly |
|
||||
| Formal proofs | Kani (bounded) and Lean (unbounded) | `src/proofs.rs`, `verify/lean/` | `just prove` | ~3 min | weekly |
|
||||
| Fuzzing | crash, hang, broken books (4) | `fuzz/fuzz_targets/`, corpora in `fuzz/corpus/` | `just fuzz <target> <secs>` | 10 min each | weekly |
|
||||
| Fuzzing | crash, hang, broken books (4); for `fuzz_store_replay` (validly chained journals with fuzz-chosen events): books that open must verify, and the viewer must accept exactly what the writer does | `fuzz/fuzz_targets/`, corpora in `fuzz/corpus/` | `just fuzz <target> <secs>` | 10 min each | weekly |
|
||||
| Miri | undefined behavior in our use of dependencies (4) | the core's unit, bridge, invariant tests | `just miri` | ~2 min | on demand |
|
||||
| Golden | `tests/golden/fixture_company.json` (5) | `invariants.rs` | `just check` | <1s | every change |
|
||||
| Benchmarks | a baseline (6) | `ledger-core/benches/books.rs`, `ledger-store/benches/store.rs` | `just bench` | ~2 min | none (no budget, by decision) |
|
||||
|
||||
@@ -66,6 +66,12 @@ mutants:
|
||||
# the whole workspace would rebuild the viewer for every mutant.
|
||||
cargo mutants -p ledger-core --exclude crates/ledger-core/src/proofs.rs --test-package ledger-core --test-package ledger-store -j 4 --timeout 120
|
||||
|
||||
# Mutation testing of the store. Fewer random cases per mutant (each needs
|
||||
# a run that catches it, not the deep sweep); temp books on a RAM disk if
|
||||
# TMPDIR is one, since every journal append is synced.
|
||||
mutants-store:
|
||||
STORE_CASES=64 cargo mutants -p ledger-store --test-package ledger-store -j 3 --timeout 300 -o mutants-store
|
||||
|
||||
# Benchmarks of the core's hot paths (no budget gates them yet)
|
||||
bench:
|
||||
cargo bench -p ledger-core --bench books
|
||||
|
||||
Reference in new issue
Block a user