swaits/wanderbooks
1
0 Fork 0
Code Issues Pull Requests Actions 10 Packages Projects Releases Wiki Activity

feat(core): prove the accounting laws (Kani + Lean); fix three engine gaps

Browse Source 
The money arithmetic every invariant rests on now lives in one kernel,
ledger-core/src/kernel.rs: signing a line, totals, net, per-account
movements, reversal, normal balances, trial-balance columns, closing
lines, and the rounding plug for member splits. It is generic over a
checked `Amount` trait. The engine runs it on Decimal (validate,
movements, reverse_entry, account_balance, close_period_to, allocate,
trial_balance): there is one copy of the arithmetic, and it is the one
under proof.

Three layers, docs/verification.md maps every law to its proofs:

- Kani (src/proofs.rs): 17 harnesses prove the kernel at i64 for every
  input up to 4 lines over 3 accounts. An entry is accepted exactly
  when it is two or more positive, in-range lines whose debits equal
  credits; accepted entries net to zero; grouping by account loses
  nothing; a reversal mirrors and cancels its original; trial-balance
  columns balance iff the books net to zero; closing lines zero their
  accounts and a close balances however the net is split; the plug
  makes parts sum to the whole. No panics, no overflow. kani::cover!
  shows the proofs are not vacuous.
- Lean 4 (verify/lean): 24 headline theorems for books of any size. The
  ledger is a state machine (add account, draft, post, reverse, open,
  close), and in every reachable state the books net to zero, the trial
  balance balances (as of any date), and the accounting equation holds.
  Posting only appends ("posted is forever"), closed periods are
  frozen, a close zeroes revenue and expenses and credits exactly the net
  income, and period statements add up. Audit.lean shows standard axioms
  only, no sorry.
- Bridge (tests/kernel_bridge.rs): the Decimal and i64 kernels agree.

What the proofs found (each one missed by every test, fuzzer, and
mutant):

- The engine accepted negative line amounts; only MCP refused them. Now
  NegativeAmountLine: direction is the side's job.
- Summing lines near Decimal::MAX panicked. Lines are now capped at one
  quadrillion and ten decimal places (AmountOutOfRange), which keeps
  every realistic sum exact, and the kernel's sums are checked.
- FX conversion (foreign_amount * fx_rate) could panic the same way; it
  is now a checked multiply.
- Kani itself: 0.68 mis-models symbolic-length copy_from_slice
  (model-checking/kani#4904) and reported a reversal that doesn't net to
  zero. The counterexample, replayed natively, passes, and a 15-line
  standalone crate reproduces the bug. Harnesses avoid bulk copies, and
  a should_panic canary will flag the upstream fix.

`just prove` runs it all (Kani memory- and time-capped, fails on an
unsatisfiable cover or a non-standard Lean axiom). AGENTS.md now makes
formal coverage part of every core change.

Also, docs: GnuCash is *an* oracle, never *the* oracle (the owner). The
spec is accounting principles, proved. Golden files are recomputed from
principles. External implementations (GnuCash, the old Sheet, QBO/Xero)
are cross-checks whose disagreements get adjudicated, never obeyed.
docs/oracle.md gains "Who is right"; AGENTS, README, architecture,
roadmap, parity, and STATUS are reworded to match.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX
This commit is contained in:
swaitsandClaude Opus 5.5 committed 2026-10-13 11:12:13 -06:00
1 parent dd0b0fa69a
commit 2d36fb05a4
31 files changed
+2682 -131
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

crates/ledger-core/src/ledger.rs
+35 -63
View File
@@ -13,7 +13,7 @@ use crate::{
Account, AccountId, AccountType, AgingRow, Asset, AssetId, AssetStatus, Bill, BillId,
ChartOfAccounts, Class, ClassId, Currency, Customer, CustomerId, DocumentLine, DocumentStatus,
EntryId, EntryStatus, Invoice, InvoiceId, JournalEntry, JournalLine, LedgerError, Money,
NewAsset, Period, PeriodId, PeriodStatus, Side, Vendor, VendorId, arap, assets,
NewAsset, Period, PeriodId, PeriodStatus, Side, Vendor, VendorId, arap, assets, kernel,
payroll::{
PayrollAccounts, PayrollLine, PayrollRun, PayrollRunId, payroll_entry_plan,
payroll_remit_plan, validate_payroll_lines,
@@ -556,7 +556,9 @@ impl Ledger {
found: foreign_currency.code().to_string(),
});
}
let base_amount = foreign_amount * fx_rate;
let base_amount = foreign_amount
.checked_mul(fx_rate)
.ok_or(LedgerError::AmountOutOfRange)?;
if base_amount <= Decimal::ZERO {
return Err(LedgerError::InvalidFxRate(fx_rate));
}
@@ -622,11 +624,7 @@ impl Ledger {
}
let id = self.create_entry(date, description);
for (idx, line) in original.lines().iter().enumerate() {
let flipped = match line.side {
Side::Debit => Side::Credit,
Side::Credit => Side::Debit,
};
self.add_line(id, line.account, flipped, line.amount)?;
self.add_line(id, line.account, kernel::flip(line.side), line.amount)?;
// The reversal offsets the original line for line: carry the
// class so divisional P&L nets correctly.
if line.class_id.is_some() {
@@ -896,23 +894,15 @@ impl Ledger {
} else {
let entry = self.create_entry(period.end, &format!("Close period {}", period.name));
let post = |this: &mut Self, account, credit: Decimal| -> Result<(), LedgerError> {
if credit.is_zero() {
return Ok(());
match kernel::credit_line(credit) {
Some((side, amount)) => {
this.add_line(entry, account, side, Money::new(amount, this.base_currency))
}
None => Ok(()),
}
let (side, amount) = if credit > Decimal::ZERO {
(Side::Credit, credit)
} else {
(Side::Debit, -credit)
};
this.add_line(entry, account, side, Money::new(amount, this.base_currency))
};
for (account, side, amount) in closings {
let credit = if side == Side::Credit {
amount
} else {
-amount
};
post(self, account, credit)?;
self.add_line(entry, account, side, Money::new(amount, self.base_currency))?;
}
for (account, share) in equity {
post(self, account, share)?;
@@ -947,24 +937,15 @@ impl Ledger {
) {
continue;
}
let movement = self.movement_through(account.id, end);
if movement.is_zero() {
continue;
}
// To zero the account: post the opposite of its net movement.
closings.push(if movement > Decimal::ZERO {
(account.id, Side::Credit, movement)
} else {
(account.id, Side::Debit, -movement)
});
if let Some((side, amount)) =
kernel::closing_line(self.movement_through(account.id, end))
{
closings.push((account.id, side, amount));
}
}
let net = closings
.iter()
.map(|(_, side, amount)| match side {
Side::Debit => *amount,
Side::Credit => -*amount,
})
.sum();
let net = kernel::net(closings.iter().map(|&(_, side, amount)| (side, amount)))
.expect("posted lines are in range, so their sums are");
(closings, net)
}
@@ -1025,16 +1006,20 @@ impl Ledger {
/// Debits minus credits on an account across posted entries dated on or
/// before `end`.
fn movement_through(&self, account: AccountId, end: NaiveDate) -> Decimal {
let mut total = Decimal::ZERO;
for entry in self.posted_entries().filter(|e| e.date() <= end) {
for line in entry.lines().iter().filter(|l| l.account == account) {
match line.side {
Side::Debit => total += line.amount.amount,
Side::Credit => total -= line.amount.amount,
}
}
}
total
self.net_of(account, |e| e.date() <= end)
}
/// Debits minus credits on an account across the posted entries
/// `include` accepts.
fn net_of(&self, account: AccountId, include: impl Fn(&JournalEntry) -> bool) -> Decimal {
kernel::net(
self.posted_entries()
.filter(|e| include(e))
.flat_map(|e| e.lines())
.filter(|l| l.account == account)
.map(|l| (l.side, l.amount.amount)),
)
.expect("posted lines are in range, so their sums are")
}
/// [`Self::preview_close_period_to`] closing into Retained Earnings.
@@ -1712,18 +1697,7 @@ impl Ledger {
/// Signed net movement of an account across all posted entries:
/// debits minus credits. Positive means net debit movement.
pub fn account_movement(&self, account: AccountId) -> Decimal {
let mut total = Decimal::ZERO;
for entry in self.posted_entries() {
for line in entry.lines() {
if line.account == account {
match line.side {
Side::Debit => total += line.amount.amount,
Side::Credit => total -= line.amount.amount,
}
}
}
}
total
self.net_of(account, |_| true)
}
/// Balance expressed in the account's normal side: positive means a
@@ -1734,10 +1708,8 @@ impl Ledger {
.get(account)
.ok_or(LedgerError::UnknownAccount(account))?;
let movement = self.account_movement(account.id);
let balance = match account.account_type.normal_side() {
Side::Debit => movement,
Side::Credit => -movement,
};
let balance = kernel::normal_balance(account.account_type, movement)
.expect("Decimal negation is exact");
// Never leak negative zero into reports: it is a representation
// artifact of negating an exact zero, and money must never print "-0".
Ok(if balance.is_zero() {