From 0a0c53dfd35d852dc13b0f3ae05f33c89c1681f4 Mon Sep 17 00:00:00 2001 From: x7k2m967z <272240395+x7k2m967z@users.noreply.github.com> Date: Fri, 23 Oct 2026 13:15:33 +0200 Subject: [PATCH] docs: clarify verification scope and evidence --- README.md | 15 ++++++++------- docs/VERIFICATION.md | 13 +++++++++---- 2 files changed, 17 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 0dc06fb..98022c4 100644 --- a/README.md +++ b/README.md @@ -13,10 +13,9 @@ This is not an execution engine and connects to no broker. It is the correctness core such an engine would sit on. A companion C++20 project, [execution-journal](https://github.com/ddehanne/execution-journal), -carries the same contract into live-execution engineering — durable -journaling with an fsync dispatch-eligibility barrier, broker -reconciliation, real-process fault injection, IBKR TWS API adapter -exercised against a live paper gateway. +explores related execution-integrity mechanisms in C++20, including +durable journaling, dispatch eligibility, reconciliation and fault +injection. Its verification scope is documented separately. ## Design laws @@ -67,7 +66,7 @@ its torn-tail repair is deliberately not exposed by this CLI. | Level | Tool | Claim | Reproduce | |---|---|---|---| -| 1 | `cargo test` | 32 example tests | `cargo test --workspace` | +| 1 | `cargo test` | 33 example tests | `cargo test --workspace` | | 2 | proptest | 3 properties on arbitrary journals | same | | 3 | Miri | zero UB on all exercised paths | `cargo +nightly miri test -p ledger-core --lib` | | 4 | libFuzzer+ASAN | 17.4M runs, 0 crashes on `parse_journal_bytes` | `cargo +nightly fuzz run fuzz_target_1 -- -max_total_time=120` | @@ -75,8 +74,10 @@ its torn-tail repair is deliberately not exposed by this CLI. Kani proofs: money arithmetic total & exact over **all** `i64` pairs (`i128` oracle); sequence successor law over **all** `u64`; transition -table over the **full** state×event product — never panics, -no-mutation-on-error. +table across all nine modeled states and six event variants, with +bounded symbolic quantities. The harness checks transition behavior +within those bounds; it is not a proof over unrestricted quantities +or of mutation behavior outside the pure transition interface. Details: [`docs/VERIFICATION.md`](docs/VERIFICATION.md). diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index 664d87c..f35feed 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -1,7 +1,7 @@ # Verification Evidence ## Level 1 — Example tests -32 unit/integration tests across the workspace (see crates' test files). +33 unit/integration tests across the workspace (see crates' test files). ## Level 2 — Property tests (proptest) 3 properties on arbitrary event journals (256 cases each per run): @@ -20,10 +20,15 @@ Contract: arbitrary bytes never panic (Ok with recovery, or typed error). Result: 17,461,635 runs in 121s, zero crashes, zero leaks. ## Level 5 — Bounded model checking (Kani v0.67 / CBMC) -Three proofs in `ledger-core/src/kani_proofs.rs` — symbolic, exhaustive +Three proofs in `crates/ledger-core/src/kani_proofs.rs` — symbolic, exhaustive within stated domains: - P1 `checked_add` total & exact over ALL i64 pairs (checked vs i128) - P2 sequence successor law characterized over ALL u64 -- P3 transition table: full state×event product — never panics, - no-mutation-on-error proven exhaustively (INV-17) +- P3 transition table: all nine modeled states and six event variants, + with symbolic quantities restricted by harness assumptions. + The harness checks its assertions exhaustively within these bounds; + it does not establish unrestricted quantity coverage. Because the + transition interface borrows the input immutably, its equality check + on error is not an independent proof of mutation safety throughout + the authoritative reducer (INV-17). Result: `Complete - 3 successfully verified harnesses, 0 failures.`