viewer: no false "database differs" while the books are being written
check / check (push) Canceled after 0s
check / check (push) Canceled after 0s
New concurrency test: one thread writes entries, drafts and receipts as
fast as it can while a Snapshot (the viewer) refreshes in a loop. At
every refresh the snapshot's books must balance, never go backward, and
never see the writer's database as differing from the journal; at the
end it must equal the writer in full. It failed 30 runs in 50:
check_disk read the applied position and the tables in separate
statements, so a write landing between them made a consistent database
look like it "differs", which the viewer shows as a problem in Needs
attention.
- check_disk reads in one read transaction (one consistent view).
- A database that has applied lines the viewer hasn't read yet is now
DiskCheck::Ahead ("viewer catching up"), not Behind.
- Without the transaction the test fails 14 runs in 20; with it, 50/50.
Also: members' equity spec 3b states the exact bound (a member's period
income is within two cents of their share, one cent of rounding at each
end; the running balance chains exactly), and the spec-blind property
checks that bound. docs/testing.md gains the concurrency layer and item
12: each close into members' capital still rounds on its own (pending).
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
37824e55d3
commit
f4381f170c
6 files changed
+165
-10
No files matched your search
@@ -832,8 +832,10 @@ pub struct MembersEquityStatement {
|
||||
/// 1065 Schedule K-1 instructions, Item L, "beginning capital account
|
||||
/// and ending capital account ... based on the partnership's books").
|
||||
/// 3b. A member's income is the roll-forward's remainder: their share of
|
||||
/// the period's income within a rounding cent; the members' incomes
|
||||
/// MUST sum to the period's net income.
|
||||
/// the period's income, off by less than two cents (under one cent of
|
||||
/// rounding at each end of the cumulative split); the members'
|
||||
/// incomes MUST sum to the period's net income. (Earnings a close has
|
||||
/// already moved into capital were rounded by that close, B-13.)
|
||||
/// 4. NEVER hide an unexplained change: it goes in "other".
|
||||
/// 5. An entry dated `start` is period activity, not beginning capital.
|
||||
/// SCENARIOS:
|
||||
|
||||
@@ -2394,10 +2394,12 @@ proptest! {
|
||||
prop_assert_eq!(st.total.beginning, balance_sheet_as_of(&b.l, prev(day(a))).unwrap().total_equity);
|
||||
}
|
||||
|
||||
/// Oracle: ME INVARIANT 3 — the period's income (closing entries
|
||||
/// excluded: the model) is split by share to the cent by largest
|
||||
/// remainder: parts sum to it and each is within one cent of its exact
|
||||
/// share, and the larger exact remainder never gets less rounding.
|
||||
/// Oracle: ME INVARIANTS 3-3b — the members' incomes sum to the period's
|
||||
/// income (closing entries excluded: the model), and each is within
|
||||
/// less than two cents of its exact share: under one cent of rounding
|
||||
/// at each end of the cumulative split (docs/testing.md #7: a member's
|
||||
/// running balance, what Form 1065 K-1 Item L reports, chains exactly;
|
||||
/// see `each_members_capital_chains_across_statements`).
|
||||
#[test]
|
||||
fn prop_me_period_income_split_by_share(gens in arb_books(), (a, _m, e) in three_days(), pct in 1i64..100, month in opt_month()) {
|
||||
let mut b = build(&gens);
|
||||
@@ -2409,7 +2411,7 @@ proptest! {
|
||||
prop_assert_eq!(st.total.net_income, ni);
|
||||
let cent = c(1);
|
||||
for (col, share) in st.members.iter().zip([share_a, Decimal::ONE - share_a]) {
|
||||
prop_assert!((col.net_income - ni * share).abs() < cent, "{:?} share {}", col, share);
|
||||
prop_assert!((col.net_income - ni * share).abs() < cent + cent, "{:?} share {}", col, share);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@@ -700,6 +700,7 @@ fn checks(b: &Books) -> Vec<(bool, String, String)> {
|
||||
out.push(match &b.integrity.disk {
|
||||
DiskCheck::Matches => (true, "Database matches journal".to_string(), "The server's SQLite database matches a fresh projection of the journal, every table, row for row.".to_string()),
|
||||
DiskCheck::Behind { applied, journal } => (true, "Database catching up".to_string(), format!("The database has applied {applied} of {journal} journal events; the server applies the rest right after writing them.")),
|
||||
DiskCheck::Ahead { .. } => (true, "Viewer catching up".to_string(), "The server has written journal events this view hasn't read yet; it reads them on its next refresh.".to_string()),
|
||||
DiskCheck::Missing => (true, "Read-only copy".to_string(), "No server database here: a copy of the books (a CPA's, say), or the server hasn't run yet. The journal and every file are verified either way.".to_string()),
|
||||
DiskCheck::Differs(why) => (false, "Database differs".to_string(), format!("{why}. The server rebuilds it from the journal (books.verify, or on its next start).")),
|
||||
DiskCheck::Unreadable(why) => (false, "Database unreadable".to_string(), why.clone()),
|
||||
|
||||
@@ -40,6 +40,14 @@ pub enum DiskCheck {
|
||||
/// Journal lines there are.
|
||||
journal: u64,
|
||||
},
|
||||
/// The database has applied journal lines this snapshot hasn't read
|
||||
/// yet (normal while the writer is busy; the next refresh catches up).
|
||||
Ahead {
|
||||
/// Journal lines the database has applied.
|
||||
applied: u64,
|
||||
/// Journal lines this snapshot has read.
|
||||
journal: u64,
|
||||
},
|
||||
/// No database file (the writer rebuilds it on start).
|
||||
Missing,
|
||||
/// The database differs from the journal: what differs.
|
||||
@@ -192,19 +200,29 @@ impl Snapshot {
|
||||
|
||||
/// Compare the writer's SQLite database (opened read-only) with this
|
||||
/// snapshot's own projection of the journal, every table, row for row.
|
||||
///
|
||||
/// The applied position and the tables are read in one read
|
||||
/// transaction, so a write landing between the two reads can't make
|
||||
/// them disagree (the writer is often busy while a viewer checks: found
|
||||
/// by the concurrency test, 2026-10-13, as a false "differs").
|
||||
pub fn check_disk(&self) -> DiskCheck {
|
||||
use rusqlite::OpenFlags;
|
||||
let path = self.data_dir.join(DB_FILE);
|
||||
if !path.exists() {
|
||||
return DiskCheck::Missing;
|
||||
}
|
||||
let conn = match Connection::open_with_flags(
|
||||
let mut conn = match Connection::open_with_flags(
|
||||
&path,
|
||||
OpenFlags::SQLITE_OPEN_READ_ONLY | OpenFlags::SQLITE_OPEN_NO_MUTEX,
|
||||
) {
|
||||
Ok(c) => c,
|
||||
Err(e) => return DiskCheck::Unreadable(e.to_string()),
|
||||
};
|
||||
// One consistent view of the database for every read below.
|
||||
let conn = match conn.transaction() {
|
||||
Ok(t) => t,
|
||||
Err(e) => return DiskCheck::Unreadable(e.to_string()),
|
||||
};
|
||||
let applied: u64 = match conn.query_row(
|
||||
"SELECT value FROM meta WHERE key='last_applied_seq'",
|
||||
[],
|
||||
@@ -214,9 +232,12 @@ impl Snapshot {
|
||||
Err(e) => return DiskCheck::Unreadable(e.to_string()),
|
||||
};
|
||||
let journal = self.journal_seq();
|
||||
if applied != journal {
|
||||
if applied < journal {
|
||||
return DiskCheck::Behind { applied, journal };
|
||||
}
|
||||
if applied > journal {
|
||||
return DiskCheck::Ahead { applied, journal };
|
||||
}
|
||||
let (disk, ours) = match (projection_rows(&conn), projection_rows(&self.conn)) {
|
||||
(Ok(d), Ok(o)) => (d, o),
|
||||
(Err(e), _) | (_, Err(e)) => return DiskCheck::Unreadable(e.to_string()),
|
||||
|
||||
@@ -0,0 +1,127 @@
|
||||
//! Concurrency (rank 2): the viewer reads while the agent writes.
|
||||
//!
|
||||
//! The viewer ([`Snapshot`]) follows the live journal of a [`Store`] that
|
||||
//! another thread (in production, another process) is writing as fast as
|
||||
//! it can. Its own spec (snapshot.rs): a line still being appended is left
|
||||
//! for the next refresh, never treated as corruption; it never writes.
|
||||
//!
|
||||
//! Oracle, at every refresh: the snapshot's books are whole (the trial
|
||||
//! balance balances, every posted entry is valid), they never go backward,
|
||||
//! and the writer's database is never seen to differ from the journal
|
||||
//! (behind is fine: the writer applies right after journaling). At the end
|
||||
//! the snapshot equals the writer, every part of the ledger, attachments
|
||||
//! included.
|
||||
|
||||
use chrono::NaiveDate;
|
||||
use ledger_core::{AccountType, Currency, Money, Side};
|
||||
use ledger_store::{DiskCheck, Snapshot, Store};
|
||||
use rust_decimal::Decimal;
|
||||
use std::sync::atomic::{AtomicBool, Ordering};
|
||||
use std::sync::{Arc, Barrier};
|
||||
|
||||
fn test_dir(name: &str) -> std::path::PathBuf {
|
||||
let dir = std::env::temp_dir().join(format!("wanderbooks-conc-{name}-{}", std::process::id()));
|
||||
let _ = std::fs::remove_dir_all(&dir);
|
||||
std::fs::create_dir_all(&dir).unwrap();
|
||||
dir
|
||||
}
|
||||
|
||||
const ENTRIES: u32 = 400;
|
||||
|
||||
#[test]
|
||||
fn a_viewer_reading_while_the_books_are_written_sees_only_whole_books() {
|
||||
let dir = test_dir("viewer");
|
||||
let mut store = Store::create(&dir, Currency::USD).unwrap();
|
||||
let cash = store
|
||||
.add_account("1000", "Cash", AccountType::Asset, None, false)
|
||||
.unwrap();
|
||||
let sales = store
|
||||
.add_account("4000", "Sales", AccountType::Revenue, None, false)
|
||||
.unwrap();
|
||||
let mut snapshot = Snapshot::load(&dir).unwrap();
|
||||
|
||||
let done = Arc::new(AtomicBool::new(false));
|
||||
let start = Arc::new(Barrier::new(2));
|
||||
let writer = {
|
||||
let (done, start) = (done.clone(), start.clone());
|
||||
std::thread::spawn(move || {
|
||||
start.wait();
|
||||
for n in 0..ENTRIES {
|
||||
let day = NaiveDate::from_ymd_opt(2026, 1, 1).unwrap()
|
||||
+ chrono::Days::new(u64::from(n % 365));
|
||||
let e = store.create_entry(day, &format!("sale {n}")).unwrap();
|
||||
let m = Money::new(Decimal::new(i64::from(n) * 100 + 1, 2), Currency::USD);
|
||||
store.add_line(e, cash, Side::Debit, m).unwrap();
|
||||
store.add_line(e, sales, Side::Credit, m).unwrap();
|
||||
if n % 3 == 0 {
|
||||
// Leave every third a draft for a while: drafts are
|
||||
// journaled too, and must read back whole.
|
||||
continue;
|
||||
}
|
||||
if n % 10 == 1 {
|
||||
store
|
||||
.attach_receipt(
|
||||
Some(e),
|
||||
&format!("r{n}.pdf"),
|
||||
"application/pdf",
|
||||
format!("receipt {n}").as_bytes(),
|
||||
None,
|
||||
)
|
||||
.unwrap();
|
||||
}
|
||||
store.post_entry(e).unwrap();
|
||||
}
|
||||
done.store(true, Ordering::SeqCst);
|
||||
store
|
||||
})
|
||||
};
|
||||
|
||||
start.wait();
|
||||
let (mut last_seq, mut last_posted, mut refreshes) = (0u64, 0usize, 0u64);
|
||||
loop {
|
||||
let finished = done.load(Ordering::SeqCst);
|
||||
snapshot.refresh().unwrap();
|
||||
refreshes += 1;
|
||||
let l = snapshot.ledger();
|
||||
let tb = ledger_core::reports::trial_balance(l);
|
||||
assert_eq!(tb.total_debits, tb.total_credits, "refresh {refreshes}");
|
||||
for e in l.posted_entries() {
|
||||
assert!(
|
||||
e.validate(l.chart()).is_ok(),
|
||||
"entry {} at refresh {refreshes}",
|
||||
e.id()
|
||||
);
|
||||
}
|
||||
let posted = l.posted_entries().count();
|
||||
assert!(
|
||||
snapshot.journal_seq() >= last_seq,
|
||||
"the journal went backward"
|
||||
);
|
||||
assert!(posted >= last_posted, "posted entries went backward");
|
||||
(last_seq, last_posted) = (snapshot.journal_seq(), posted);
|
||||
match snapshot.check_disk() {
|
||||
DiskCheck::Matches | DiskCheck::Behind { .. } | DiskCheck::Ahead { .. } => {}
|
||||
other => panic!("refresh {refreshes}: the database {other:?}"),
|
||||
}
|
||||
if finished {
|
||||
break;
|
||||
}
|
||||
}
|
||||
let store = writer.join().unwrap();
|
||||
snapshot.refresh().unwrap();
|
||||
let parts = store.ledger().differs_from(snapshot.ledger());
|
||||
assert!(
|
||||
parts.is_empty(),
|
||||
"the viewer differs from the writer in {parts:?}"
|
||||
);
|
||||
assert_eq!(
|
||||
snapshot.attachments(None).unwrap().len(),
|
||||
store.list_attachments(None).unwrap().len()
|
||||
);
|
||||
assert_eq!(snapshot.check_disk(), DiskCheck::Matches);
|
||||
assert!(refreshes > 1, "the reader never overlapped the writer");
|
||||
if std::env::var("CONC_STATS").is_ok() {
|
||||
eprintln!("REFRESHES {refreshes}");
|
||||
}
|
||||
let _ = std::fs::remove_dir_all(&dir);
|
||||
}
|
||||
+3
-1
@@ -17,6 +17,7 @@ the store's journal safety; the other crates come next (gap list).
|
||||
| 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 |
|
||||
| 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 |
|
||||
@@ -78,6 +79,7 @@ accounting question), CHANGE (a source says otherwise; work pending).
|
||||
| 9 | An asset's life ends at purchase + life months, that day not held; day-count proration | CONVENTION | Exactly N months of service; day proration and the mid-month convention are both accepted book policies (ASC 360-10-35-4 not read: login) |
|
||||
| 10 | A payroll entry has one line per account total | CONFIRMED | The per-employee detail the IRS requires ("Amounts and dates of all wage ... payments", Employment Tax Recordkeeping) is kept in the run; a summary entry is standard |
|
||||
| 11 | A period with exactly the dates of an existing one is allowed | DESIGN | Nothing governs duplicate periods; harmless (the second close locks only). Refusing exact duplicates is an option |
|
||||
| 12 | Each close into members' capital rounds on its own (ties to the earlier member) | CHANGE (pending) | Found 2026-10-13 with #7: twelve monthly 50/50 closes can leave one member several cents ahead of half the year's income. Closes should split cumulatively too (year-to-date allocation minus what earlier closes gave); a new journaled rounding rule, older closes replaying as booked |
|
||||
|
||||
Questions are settled from the sources, not by any one company's CPA
|
||||
(wanderbooks is general software). Where the standards leave a real
|
||||
@@ -93,7 +95,7 @@ B-14) are the first.
|
||||
| Integration | SKIP for the core (no collaborators) | the core gains one; covered at the store and MCP layers |
|
||||
| End-to-end | SKIP for the core (a library) | MCP stdio tests cover the journeys |
|
||||
| Security properties | SKIP for the core (no roles, no secrets) | the first permission concept, or a secret-bearing field |
|
||||
| Concurrency stress | SKIP for the core (no shared state) | the first `Arc`, atomic, or lock in the core; the GUI and MCP server have threads (next) |
|
||||
| Concurrency stress | SKIP for the core (no shared state); DONE for the store's writer + viewer (found the false "differs") | the first `Arc`, atomic, or lock in the core; the MCP server's HTTP transport shares one store across sessions (next) |
|
||||
| Lean: apportion's sum law for any n | OPEN | Kani covers n <= 3, properties n <= 5; needs a permutation lemma |
|
||||
| ASC paragraphs not yet read | OPEN | ASC 360-10-35-4, 340-10, 230-10-45-10, 606-10-55-37B, 210: needs a FASB basic-view login |
|
||||
| GnuCash's own close | OPEN | the oracle books closes as ordinary entries; comparing GnuCash's Close Book needs its Scheme API |
|
||||
|
||||
Reference in new issue
Block a user