diff --git a/AGENTS.md b/AGENTS.md index d5a3f98..39236d7 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -12,9 +12,13 @@ what they haven't demonstrated. semantics, built to become a full bookkeeping application (engine now, UI later). The reference points: -- **Semantic oracle:** GnuCash. It is open source with open file formats - (XML/SQLite), which makes it both the spec and the reference implementation - we diff against. See `docs/oracle.md`. +- **Spec:** accounting principles, written down as proofs + (`docs/verification.md`). That is the only authority. +- **Cross-check oracles:** GnuCash (open source, open file formats), the + old Google Sheet, QBO/Xero exports. Useful to diff against, *never* + trusted to be right: a disagreement is adjudicated from principles, and + nothing may rest on another program's behavior alone. See + `docs/oracle.md`, "Who is right". - **Workflow reference:** QuickBooks Online and Xero — for *what the UI must do*, never for code. We observe behavior; we write our own implementation. - **Method reference:** storytold/ArtCraft's app-cloning pipeline @@ -37,6 +41,10 @@ later). The reference points: IRS publications for tax-adjacent logic later. GnuCash itself is GPL — read its docs, never copy its code. This repo is MIT OR Apache-2.0. Never disassemble or copy from proprietary software. +6. **Accounting laws are proved, not just tested.** Arithmetic that money + flows through lives in `kernel.rs` and carries Kani proofs; the laws + it serves carry Lean proofs. `just prove` stays green. See + "Formal methods" below. ## Verification protocol (read this twice) @@ -60,6 +68,58 @@ numbers**. The analog of storytold's screenshot-in-the-loop: - The randomized invariant test (`random_balanced_journals_preserve_invariants`) is the always-on property oracle. Extend it when you add invariants. +## Formal methods: the bar (read this three times) + +Tests check the cases someone thought of; proofs check all of them. The +first formal pass on this engine (2026-10, `docs/verification.md`) paid +for itself several times over, on code that already had 190+ tests, +property tests, mutation testing, and 11.5M fuzz executions: + +- **Negative line amounts were accepted by the engine.** Only the MCP + layer refused them. Any other caller could post them. +- **A large enough amount crashed the engine** (a `Decimal` overflow + panic while summing lines) instead of returning an error. +- **Currency conversion could crash** the same way. +- **The verifier itself had a soundness bug.** Kani 0.68 mis-models + `copy_from_slice` of symbolic length (model-checking/kani#4904): it + reported a reversal that doesn't net to zero. We didn't wave it away. + Replaying the counterexample natively, then shrinking it to a 15-line + crate, proved it was the tool, not the books. Now a canary harness + watches for the fix, and covers prove no proof is vacuous. +- **Writing the spec simplified the code.** `credit_line` and + `closing_line` turned out to be the same function. Lean also proved + that no draft can exist in a closed period, the invariant that lets + the store journal a post before applying it. + +So the bar, for every agent, every change: + +1. **Money arithmetic goes in `kernel.rs`, generic over `Amount`.** If + you write a sum, a sign flip, a split, or a rounding plug anywhere + else, move it into the kernel. The engine calls the kernel. It never + gets a second copy. +2. **Every kernel function gets a Kani harness** in `src/proofs.rs`, on + fixed arrays (no symbolic-length `Vec` growth, no `copy_from_slice`), + with a `kani::cover!` showing the interesting case is reached. +3. **Every new law gets a Lean theorem** in `verify/lean`. Laws about + the books over time are theorems about `Reachable` states. A new + `Ledger` command is a new `Step` constructor, with its preservation + proof. No `sorry`, ever; `Audit.lean` lists every headline theorem. +4. **Every kernel instantiation gets a bridge property** in + `tests/kernel_bridge.rs`, so what Kani proved on `i64` holds on + `Decimal`. +5. **A failing proof is a finding, not an obstacle.** Get the + counterexample, replay it natively, and decide on evidence: bug in + our code, bug in the spec, or bug in the tool. Never weaken an + assertion, raise a bound, or delete a harness to make red go green + without writing down why in `docs/verification.md`. +6. **More, not less.** When you touch an area the proofs don't cover + yet (A/R and A/P documents, payroll, depreciation, FX, persistence), + leave it with more formal coverage than you found it. Proptest, + mutation testing, fuzzing, Kani, and Lean all stack. Use all of them. + +`just check` and `just prove` both pass before every commit that touches +`ledger-core`. + ## Parity tracking `docs/parity.md` is the parity catalog: every semantic feature we intend to @@ -85,8 +145,11 @@ clone, with status. Rules: ## Working here -- Rust stable, edition 2024. `cargo test` must pass; `cargo clippy` should be - clean; `cargo fmt` before committing. +- `mise install` sets up every tool (pinned in `mise.toml`): Rust, + just, Kani, Lean, cargo-mutants, cargo-fuzz. If a recipe needs a tool, + it goes in `mise.toml`; nothing gets installed by hand. +- Rust stable, edition 2024. `just check` must pass: fmt, clippy with zero + warnings, every test. `just prove` must pass for core changes. - Conventional commits: `feat:`, `fix:`, `docs:`, `test:`, `refactor:`. One logical change per commit. The commit message explains the *accounting* reasoning, not just the code. @@ -102,7 +165,8 @@ clone, with status. Rules: |---|---| | `docs/requirements.md` | What the engine must do (R-1…), what is future work | | `docs/architecture.md` | Crate layout, command pattern, dependency rules | -| `docs/oracle.md` | How we prove correctness: golden files, property tests, GnuCash diffing | +| `docs/oracle.md` | How we check correctness: golden files, property tests, fuzzing, cross-checks against other implementations (and who is right) | +| `docs/verification.md` | The formal proofs: every accounting law, its Kani harness and Lean theorem, what they found | | `docs/parity.md` | Feature catalog and the non-regression floor | | `docs/capability-parity.md` | Parity vs the GSheet+GDrive system + the cutover rule | | `docs/mcp-interface.md` | The MCP tool surface: the primary interface spec | diff --git a/Cargo.toml b/Cargo.toml index a2eb360..ea55516 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,3 +9,5 @@ repository = "https://git.swaits.com/swaits/wanderbooks" [workspace.lints.rust] missing_docs = "warn" +# `cargo kani` sets cfg(kani) for the proof harnesses. +unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] } diff --git a/README.md b/README.md index 524073a..0b9b8a3 100644 --- a/README.md +++ b/README.md @@ -36,12 +36,23 @@ through MCP. Self-hosted, no rent. This is the storytold way applied to accounting: agents verify against oracles, never ship what they haven't demonstrated. -- 70 workspace tests: invariant tests encoding accounting law, golden-file +- 190+ workspace tests: invariant tests encoding accounting law, golden-file report snapshots, property tests (proptest), end-to-end MCP stdio tests. +- **Formal proofs of the accounting laws** (`just prove`, + `docs/verification.md`). Kani model-checks the engine's arithmetic + kernel exhaustively within bounds. Lean 4 proves that, after any + sequence of commands, the trial balance balances, the accounting + equation holds, posted entries are forever, closed periods stay + frozen, and a close moves exactly the net income to equity. The first + pass found three engine bugs that every test, fuzzer, and mutant had + missed: negative amounts accepted, and two crashes on oversized + amounts. It also caught a soundness bug in the model checker itself. - Mutation testing via cargo-mutants; fuzzing via cargo-fuzz (11.5M+ executions, zero crashes). -- GnuCash is the behavioral oracle (never a code source — clean room, - MIT OR Apache-2.0). +- GnuCash is *a* behavioral cross-check, never the authority and never + a code source (clean room, MIT OR Apache-2.0). Accounting principles, + proved, are the spec. Where any other program disagrees, we work out + from principles who is right. ## Status @@ -71,6 +82,16 @@ Already installed: `wanderbooks new ~/Books/Acme` (add `--codex` to keep the books with Codex instead of Claude Code). In a books dir, `just` lists the shortcuts (`just gui`, `just agent`, `just backup`). +## Developing + +Every tool the recipes use (Rust, just, Kani, Lean, cargo-mutants, +cargo-fuzz, Node for deploys) is pinned in `mise.toml`: + +```sh +mise install +just # lists the recipes: check, build, prove, demo, ... +``` + ## Layout ``` diff --git a/crates/ledger-core/src/error.rs b/crates/ledger-core/src/error.rs index d035021..2b9d803 100644 --- a/crates/ledger-core/src/error.rs +++ b/crates/ledger-core/src/error.rs @@ -26,6 +26,15 @@ pub enum LedgerError { #[error("journal line has a zero amount")] ZeroAmountLine, + /// Line amounts are positive; the side says which way the money moves. + #[error("journal line has a negative amount; use the other side instead")] + NegativeAmountLine, + + /// A line larger than one quadrillion, or with more than ten decimal + /// places, is a mistake, and one that could overflow exact arithmetic. + #[error("journal line amount is out of range (at most 1000000000000000, ten decimal places)")] + AmountOutOfRange, + /// The referenced account does not exist in the chart of accounts. #[error("unknown account id {0}")] UnknownAccount(u64), diff --git a/crates/ledger-core/src/journal.rs b/crates/ledger-core/src/journal.rs index 19ec9e0..957bdd3 100644 --- a/crates/ledger-core/src/journal.rs +++ b/crates/ledger-core/src/journal.rs @@ -4,6 +4,7 @@ //! total credits. Entries are born as drafts, validated, then posted. Posting //! is one-way; a posted entry can only be corrected by a reversing entry. +use crate::kernel::{self, LineError}; use crate::{AccountId, ChartOfAccounts, ClassId, Currency, LedgerError, Money, Side}; use chrono::NaiveDate; use rust_decimal::Decimal; @@ -126,14 +127,11 @@ impl JournalEntry { } /// Validate the entry against the chart of accounts. This is the heart of - /// R-1: at least two lines, no zero amounts, no placeholder or unknown - /// accounts, one currency throughout, and debits exactly equal to credits. + /// R-1: at least two lines, every amount positive and within line range, + /// no placeholder or unknown accounts, one currency throughout, and + /// debits exactly equal to credits. The arithmetic is + /// [`kernel::check_lines`]. pub fn validate(&self, chart: &ChartOfAccounts) -> Result<(), LedgerError> { - if self.lines.len() < 2 { - return Err(LedgerError::TooFewLines); - } - let mut debits = Decimal::ZERO; - let mut credits = Decimal::ZERO; let mut currency: Option = None; for line in &self.lines { let account = chart @@ -142,9 +140,6 @@ impl JournalEntry { if account.placeholder { return Err(LedgerError::PlaceholderAccount(account.code.clone())); } - if line.amount.is_zero() { - return Err(LedgerError::ZeroAmountLine); - } match currency { None => currency = Some(line.amount.currency), Some(c) if c != line.amount.currency => { @@ -161,28 +156,33 @@ impl JournalEntry { found: line.amount.currency.code().to_string(), }); } - match line.side { - Side::Debit => debits += line.amount.amount, - Side::Credit => credits += line.amount.amount, + } + let sides: Vec<(Side, Decimal)> = self + .lines + .iter() + .map(|l| (l.side, l.amount.amount)) + .collect(); + kernel::check_lines(&sides).map_err(|e| match e { + LineError::TooFewLines => LedgerError::TooFewLines, + LineError::ZeroAmount => LedgerError::ZeroAmountLine, + LineError::NegativeAmount => LedgerError::NegativeAmountLine, + LineError::OutOfRange => LedgerError::AmountOutOfRange, + LineError::Unbalanced { debits, credits } => { + LedgerError::UnbalancedEntry { debits, credits } } - } - if debits != credits { - return Err(LedgerError::UnbalancedEntry { debits, credits }); - } - Ok(()) + }) } /// Net movement per account within this entry: debits minus credits. /// Sums to zero across accounts for any valid entry. pub fn movements(&self) -> HashMap { - let mut out = HashMap::new(); - for line in &self.lines { - let delta = match line.side { - Side::Debit => line.amount.amount, - Side::Credit => -line.amount.amount, - }; - *out.entry(line.account).or_insert(Decimal::ZERO) += delta; - } - out + kernel::movements( + self.lines + .iter() + .map(|l| (l.account, l.side, l.amount.amount)), + ) + .expect("posted lines are in range, so their sums are") + .into_iter() + .collect() } } diff --git a/crates/ledger-core/src/kernel.rs b/crates/ledger-core/src/kernel.rs new file mode 100644 index 0000000..759bdb7 --- /dev/null +++ b/crates/ledger-core/src/kernel.rs @@ -0,0 +1,292 @@ +//! The accounting kernel: the arithmetic every bookkeeping invariant rests +//! on, in one place. +//! +//! Each function here is small, pure, and generic over [`Amount`]. The +//! engine runs it on [`Decimal`]; the Kani harnesses in `proofs.rs` run the +//! very same code on machine integers and prove it correct for every input +//! within their bounds; and the Lean model in `verify/lean` proves the +//! laws it implements hold for books of any size. See +//! `docs/verification.md` for which proof covers which law. +//! +//! The laws, in the order they appear: +//! +//! * a line's signed amount is `+amount` for a debit, `-amount` for a credit; +//! * an entry is acceptable when it has two or more lines, every amount is +//! positive and in range, and its debits equal its credits exactly; +//! * an acceptable entry nets to zero, account by account summed; +//! * a reversal flips every side, so it is acceptable exactly when the +//! original is, and the two together net every account to zero; +//! * an account's balance is its movement read on its normal side, so the +//! balances satisfy the accounting equation whenever movements net to +//! zero; +//! * a trial balance puts each movement in exactly one column, so its +//! columns differ by the net of all movements; +//! * a closing line zeroes the account it closes; +//! * an allocation's parts sum to the whole, to the last unit. + +use crate::{AccountType, Side}; +use rust_decimal::Decimal; + +/// What the kernel needs of a money amount: exact, ordered, and checked +/// arithmetic that reports overflow instead of rounding or wrapping. +pub trait Amount: Copy + Ord { + /// Zero. + const ZERO: Self; + /// `self + rhs`, or `None` when it cannot be represented exactly. + fn checked_add(self, rhs: Self) -> Option; + /// `-self`, or `None` when it cannot be represented. + fn checked_neg(self) -> Option; + /// True when the amount is small and precise enough for a journal line + /// (see [`MAX_LINE_AMOUNT`] and [`MAX_LINE_SCALE`] for [`Decimal`]). + fn in_line_range(self) -> bool; + + /// `self - rhs`, or `None` when it cannot be represented exactly. + fn checked_sub(self, rhs: Self) -> Option { + self.checked_add(rhs.checked_neg()?) + } +} + +/// The largest amount one journal line may carry: one quadrillion units of +/// the base currency. Far beyond any real transaction, and far enough +/// below [`Decimal::MAX`] that no realistic sum of lines can overflow. +pub const MAX_LINE_AMOUNT: Decimal = Decimal::from_parts(0xA4C6_8000, 0x0003_8D7E, 0, false, 0); + +/// The most decimal places a journal line may carry. Cents need two; +/// foreign-currency lines (amount times rate) need more; ten keeps every +/// sum of lines exact as long as the total stays under 7.9 quintillion. +pub const MAX_LINE_SCALE: u32 = 10; + +impl Amount for Decimal { + const ZERO: Self = Decimal::ZERO; + fn checked_add(self, rhs: Self) -> Option { + Decimal::checked_add(self, rhs) + } + fn checked_neg(self) -> Option { + Some(-self) + } + fn in_line_range(self) -> bool { + self.abs() <= MAX_LINE_AMOUNT && self.normalize().scale() <= MAX_LINE_SCALE + } +} + +impl Amount for i64 { + const ZERO: Self = 0; + fn checked_add(self, rhs: Self) -> Option { + i64::checked_add(self, rhs) + } + fn checked_neg(self) -> Option { + i64::checked_neg(self) + } + fn in_line_range(self) -> bool { + // Scaled down with the same headroom as Decimal's range: lines + // this size can be summed many times over without overflow. + self.unsigned_abs() <= (1 << 40) + } +} + +/// Why the kernel rejected an entry's lines. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum LineError { + /// Fewer than two lines. + TooFewLines, + /// A line with a zero amount. + ZeroAmount, + /// A line with a negative amount: direction is the side's job. + NegativeAmount, + /// A line too large or too precise for a journal line. + OutOfRange, + /// Debits and credits differ. + Unbalanced { + /// Sum of debit lines. + debits: T, + /// Sum of credit lines. + credits: T, + }, +} + +/// The other side. +pub fn flip(side: Side) -> Side { + match side { + Side::Debit => Side::Credit, + Side::Credit => Side::Debit, + } +} + +/// A line's signed amount: positive for a debit, negative for a credit. +pub fn signed(side: Side, amount: T) -> Option { + match side { + Side::Debit => Some(amount), + Side::Credit => amount.checked_neg(), + } +} + +/// Total debits and total credits of some lines. +pub fn totals(lines: impl IntoIterator) -> Option<(T, T)> { + let mut debits = T::ZERO; + let mut credits = T::ZERO; + for (side, amount) in lines { + match side { + Side::Debit => debits = debits.checked_add(amount)?, + Side::Credit => credits = credits.checked_add(amount)?, + } + } + Some((debits, credits)) +} + +/// The net of some lines: debits minus credits. +pub fn net(lines: impl IntoIterator) -> Option { + let mut total = T::ZERO; + for (side, amount) in lines { + total = total.checked_add(signed(side, amount)?)?; + } + Some(total) +} + +/// Check an entry's lines: two or more, every amount positive and within +/// line range, debits equal to credits. Accounts and currencies are the +/// caller's to check; this is the arithmetic. +pub fn check_lines(lines: &[(Side, T)]) -> Result<(), LineError> { + if lines.len() < 2 { + return Err(LineError::TooFewLines); + } + for &(_, amount) in lines { + if amount == T::ZERO { + return Err(LineError::ZeroAmount); + } + if amount < T::ZERO { + return Err(LineError::NegativeAmount); + } + if !amount.in_line_range() { + return Err(LineError::OutOfRange); + } + } + let (debits, credits) = totals(lines.iter().copied()).ok_or(LineError::OutOfRange)?; + if debits != credits { + return Err(LineError::Unbalanced { debits, credits }); + } + Ok(()) +} + +/// Net movement per account (debits minus credits), in order of first +/// appearance. +pub fn movements( + lines: impl IntoIterator, +) -> Option> { + let lines: Vec<_> = lines.into_iter().collect(); + let Some(&(first, _, _)) = lines.first() else { + return Some(Vec::new()); + }; + // At most one account per line. + let mut out = vec![(first, T::ZERO); lines.len()]; + let n = movements_into(&lines, &mut out)?; + out.truncate(n); + Some(out) +} + +/// [`movements`] into a caller's buffer, without allocating: returns how +/// many accounts it wrote, or `None` on overflow or if `out` is too small. +pub fn movements_into( + lines: &[(K, Side, T)], + out: &mut [(K, T)], +) -> Option { + let mut n = 0; + for &(account, side, amount) in lines { + let delta = signed(side, amount)?; + match out[..n].iter_mut().find(|(k, _)| *k == account) { + Some((_, total)) => *total = total.checked_add(delta)?, + None => { + *out.get_mut(n)? = (account, delta); + n += 1; + } + } + } + Some(n) +} + +/// The lines of a reversing entry: every side flipped, accounts and +/// amounts unchanged. +pub fn reversal(lines: &[(K, Side, T)]) -> Vec<(K, Side, T)> { + lines.iter().map(|&line| reverse_line(line)).collect() +} + +/// One line of a reversing entry: the side flipped, account and amount +/// unchanged. +pub fn reverse_line((account, side, amount): (K, Side, T)) -> (K, Side, T) { + (account, flip(side), amount) +} + +/// An account's balance read on its normal side: positive is a normal +/// balance, negative a contra balance. +pub fn normal_balance(account_type: AccountType, movement: T) -> Option { + match account_type.normal_side() { + Side::Debit => Some(movement), + Side::Credit => movement.checked_neg(), + } +} + +/// A movement in trial-balance columns: `(debit, credit)`, one of them +/// zero, both non-negative. +pub fn columns(movement: T) -> Option<(T, T)> { + if movement > T::ZERO { + Some((movement, T::ZERO)) + } else { + Some((T::ZERO, movement.checked_neg()?)) + } +} + +/// The line that zeroes an account with this movement: the opposite side, +/// for the same amount. `None` for a zero movement (nothing to close). +pub fn closing_line(movement: T) -> Option<(Side, T)> { + if movement > T::ZERO { + Some((Side::Credit, movement)) + } else if movement < T::ZERO { + Some((Side::Debit, movement.checked_neg()?)) + } else { + None + } +} + +/// The line that credits `credit` to an account (a negative credit is a +/// debit). `None` for zero. This is [`closing_line`]: crediting `c` and +/// zeroing a movement of `c` are the same line. +pub fn credit_line(credit: T) -> Option<(Side, T)> { + closing_line(credit) +} + +/// Make rounded parts sum to the whole: the last part becomes `whole` +/// minus the others, absorbing every unit of rounding. Returns `None` on +/// overflow, leaving `parts` unchanged. +pub fn plug_last(whole: T, parts: &mut [T]) -> Option<()> { + let Some((last, rest)) = parts.split_last_mut() else { + return Some(()); + }; + let mut others = T::ZERO; + for &p in rest.iter() { + others = others.checked_add(p)?; + } + *last = whole.checked_sub(others)?; + Some(()) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn max_line_amount_is_one_quadrillion() { + assert_eq!(MAX_LINE_AMOUNT, Decimal::from(1_000_000_000_000_000u64)); + assert!(MAX_LINE_AMOUNT.in_line_range()); + assert!(!(MAX_LINE_AMOUNT + Decimal::ONE).in_line_range()); + assert!("0.0000000001".parse::().unwrap().in_line_range()); + assert!(!"0.00000000001".parse::().unwrap().in_line_range()); + // Trailing zeros are not precision. + assert!("1.000000000000".parse::().unwrap().in_line_range()); + } + + #[test] + fn credit_line_sides() { + assert_eq!(credit_line(5i64), Some((Side::Credit, 5))); + assert_eq!(credit_line(-5i64), Some((Side::Debit, 5))); + assert_eq!(credit_line(0i64), None); + } +} diff --git a/crates/ledger-core/src/ledger.rs b/crates/ledger-core/src/ledger.rs index 568e5c9..0b81dee 100644 --- a/crates/ledger-core/src/ledger.rs +++ b/crates/ledger-core/src/ledger.rs @@ -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() { diff --git a/crates/ledger-core/src/lib.rs b/crates/ledger-core/src/lib.rs index 92c2907..9754fb1 100644 --- a/crates/ledger-core/src/lib.rs +++ b/crates/ledger-core/src/lib.rs @@ -24,11 +24,14 @@ pub mod classes; pub mod error; pub mod form1099; pub mod journal; +pub mod kernel; pub mod ledger; pub mod money; pub mod payouts; pub mod payroll; pub mod periods; +#[cfg(kani)] +mod proofs; pub mod reports; pub mod schedules; pub mod tax; diff --git a/crates/ledger-core/src/periods.rs b/crates/ledger-core/src/periods.rs index e081d5c..6f54ed4 100644 --- a/crates/ledger-core/src/periods.rs +++ b/crates/ledger-core/src/periods.rs @@ -77,9 +77,7 @@ pub fn allocate( .iter() .map(|s| (amount * s).round_dp_with_strategy(2, MidpointAwayFromZero)) .collect(); - if let Some((last, rest)) = parts.split_last_mut() { - *last = amount - rest.iter().copied().sum::(); - } + crate::kernel::plug_last(amount, &mut parts).expect("allocated amounts are in range"); parts } diff --git a/crates/ledger-core/src/proofs.rs b/crates/ledger-core/src/proofs.rs new file mode 100644 index 0000000..2d0311f --- /dev/null +++ b/crates/ledger-core/src/proofs.rs @@ -0,0 +1,485 @@ +//! Kani proof harnesses for the accounting kernel. +//! +//! `cargo kani -p ledger-core` (or `just prove`) model-checks each +//! harness: CBMC explores *every* input within the stated bounds, not a +//! sample, and fails if any one of them breaks an assertion, panics, or +//! overflows. The code under proof is the engine's own [`crate::kernel`], +//! instantiated at `i64` (exact integer money, in the smallest unit); the +//! engine runs the same functions on `Decimal`, and the `kernel_bridge` +//! property test checks the two instantiations agree. +//! +//! Bounds: entries of up to [`N`] lines over up to [`K`] accounts, and +//! amounts up to 2^40 in magnitude. The Lean model in `verify/lean` +//! proves the same laws for any number of lines and accounts. + +use crate::kernel::{self, Amount, LineError}; +use crate::{AccountType, Side}; + +/// Most lines per entry the harnesses explore. +const N: usize = 4; +/// Accounts the harnesses' lines draw from. +const K: u8 = 3; + +fn any_side() -> Side { + if kani::any() { + Side::Debit + } else { + Side::Credit + } +} + +fn any_type() -> AccountType { + // An assumption, not `% 5`: modulo is costly for the SAT solver. + let t: u8 = kani::any(); + kani::assume(t < 5); + match t { + 0 => AccountType::Asset, + 1 => AccountType::Liability, + 2 => AccountType::Equity, + 3 => AccountType::Revenue, + _ => AccountType::Expense, + } +} + +/// Any amount a journal line could carry, sign included. +fn any_amount() -> i64 { + let a: i64 = kani::any(); + kani::assume(a.in_line_range()); + a +} + +/// Any count up to `N`. Harnesses fill fixed arrays and take a prefix of +/// this length: fixed arrays keep the model free of allocation (which is +/// also why they call `movements_into` rather than `movements`). +fn any_len() -> usize { + let n: usize = kani::any(); + kani::assume(n <= N); + n +} + +/// `N` lines, any sides, any in-range amounts (use a prefix). +fn any_lines() -> [(Side, i64); N] { + core::array::from_fn(|_| (any_side(), any_amount())) +} + +/// `N` lines over `K` accounts (use a prefix). +fn any_account_lines() -> [(u8, Side, i64); N] { + core::array::from_fn(|_| { + let k: u8 = kani::any(); + kani::assume(k < K); + (k, any_side(), any_amount()) + }) +} + +/// The mathematical signed amount. Amounts are at most 2^40 and no +/// harness sums more than eight, so `i64` holds every spec sum exactly +/// (and Kani would flag it if not). +fn wide(side: Side, amount: i64) -> i64 { + match side { + Side::Debit => amount, + Side::Credit => -(amount), + } +} + +fn wide_net(lines: &[(Side, i64)]) -> i64 { + lines.iter().map(|&(s, a)| wide(s, a)).sum() +} + +/// The sides and amounts of some account lines, into a fixed array. +fn sides(lines: &[(u8, Side, i64)]) -> [(Side, i64); N] { + let mut out = [(Side::Debit, 0); N]; + for (o, &(_, s, a)) in out.iter_mut().zip(lines) { + *o = (s, a); + } + out +} + +// --------------------------------------------------------------------------- +// Lines and entries +// --------------------------------------------------------------------------- + +/// Flipping a side negates its signed amount, and flipping twice is the +/// identity. +#[kani::proof] +fn flip_negates() { + let side = any_side(); + let a = any_amount(); + assert_eq!(kernel::flip(kernel::flip(side)), side); + assert_ne!(kernel::flip(side), side); + assert_eq!(kernel::signed(kernel::flip(side), a), Some(-wide(side, a))); +} + +/// In-range lines never overflow the kernel's sums: `totals` and `net` +/// always succeed, and agree with the mathematical sums. (`movements` +/// is covered by its own harnesses.) +#[kani::proof] +#[kani::unwind(6)] +fn sums_are_exact() { + let all = any_account_lines(); + let lines = &all[..any_len()]; + let all_sides = sides(lines); + let s = &all_sides[..lines.len()]; + let (debits, credits) = kernel::totals(s.iter().copied()).expect("no overflow"); + let net = kernel::net(s.iter().copied()).expect("no overflow"); + assert_eq!(net, wide_net(s)); + assert_eq!(debits - credits, wide_net(s)); +} + +/// The kernel accepts an entry exactly when it has two or more lines, +/// every amount is positive and in range, and debits equal credits. +#[kani::proof] +#[kani::unwind(6)] +fn check_lines_is_exact() { + let all = any_lines(); + let lines = &all[..any_len()]; + let positive = lines.iter().all(|&(_, a)| a > 0); + let debits: i64 = lines + .iter() + .filter(|l| l.0 == Side::Debit) + .map(|l| l.1) + .sum(); + let credits: i64 = lines + .iter() + .filter(|l| l.0 == Side::Credit) + .map(|l| l.1) + .sum(); + let spec = lines.len() >= 2 && positive && debits == credits; + let got = kernel::check_lines(lines); + assert_eq!(got.is_ok(), spec); + if let Err(LineError::Unbalanced { + debits: d, + credits: c, + }) = got + { + assert_eq!((d, c), (debits, credits)); + } +} + +/// An out-of-range amount is always rejected. +#[kani::proof] +fn out_of_range_is_rejected() { + let big: i64 = kani::any(); + kani::assume(big > 0 && !big.in_line_range()); + let side = any_side(); + let lines = [(side, big), (kernel::flip(side), big)]; + assert_eq!(kernel::check_lines(&lines), Err(LineError::OutOfRange)); +} + +/// An accepted entry nets to zero. +#[kani::proof] +#[kani::unwind(6)] +fn accepted_entry_nets_to_zero() { + let all = any_lines(); + let lines = &all[..any_len()]; + if kernel::check_lines(lines).is_ok() { + assert_eq!(kernel::net(lines.iter().copied()), Some(0)); + kani::cover!(lines.len() == N, "an accepted four-line entry"); + } +} + +/// Movements group lines by account without losing or inventing money: +/// any account appears at most once, and its movement is the net of its +/// own lines (zero if it has none). +#[kani::proof] +#[kani::unwind(6)] +fn movements_are_per_account() { + let all = any_account_lines(); + let lines = &all[..any_len()]; + let mut out = [(0u8, 0i64); N]; + let n = kernel::movements_into(lines, &mut out).expect("no overflow, room for all"); + let moves = &out[..n]; + let k: u8 = kani::any(); + kani::assume(k < K); + let mut own = 0i64; + let mut has = false; + for &(a, s, x) in lines { + if a == k { + own += wide(s, x); + has = true; + } + } + let mut found = 0; + let mut movement = 0i64; + for &(a, m) in moves { + if a == k { + found += 1; + movement = m; + } + } + assert_eq!(found, usize::from(has)); + assert_eq!(movement, own); + kani::cover!(n == 3, "three distinct accounts"); +} + +/// The movements sum to the lines' net: zero for an accepted entry. +#[kani::proof] +#[kani::unwind(6)] +fn movements_sum_to_the_net() { + let all = any_account_lines(); + let lines = &all[..any_len()]; + let mut out = [(0u8, 0i64); N]; + let n = kernel::movements_into(lines, &mut out).expect("no overflow, room for all"); + let total: i64 = out[..n].iter().map(|&(_, m)| m).sum(); + let all_sides = sides(lines); + let s = &all_sides[..lines.len()]; + assert_eq!(total, wide_net(s)); + if kernel::check_lines(s).is_ok() { + assert_eq!(total, 0); + kani::cover!( + n >= 2 && lines.len() == N, + "an accepted entry over several accounts" + ); + } +} + +/// A reversal flips every side and keeps every account and amount, so it +/// is accepted exactly when the original is. (`kernel::reversal` is +/// `reverse_line` mapped over the lines; proving it line by line keeps +/// the model free of allocation.) +#[kani::proof] +#[kani::unwind(6)] +fn reversal_mirrors() { + let all = any_account_lines(); + let lines = &all[..any_len()]; + let mut rev = [(0u8, Side::Debit, 0i64); N]; + for i in 0..lines.len() { + rev[i] = kernel::reverse_line(lines[i]); + assert_eq!((rev[i].0, rev[i].2), (lines[i].0, lines[i].2)); + assert_eq!(rev[i].1, kernel::flip(lines[i].1)); + } + let n = lines.len(); + assert_eq!( + kernel::check_lines(&sides(&rev[..n])[..n]).is_ok(), + kernel::check_lines(&sides(lines)[..n]).is_ok() + ); + kani::cover!( + n == N && kernel::check_lines(&sides(lines)[..n]).is_ok(), + "an accepted four-line entry, reversed" + ); +} + +/// An entry and its reversal together net every account to zero. +#[kani::proof] +#[kani::unwind(10)] +fn reversal_cancels() { + let all = any_account_lines(); + let n = any_len(); + let lines = &all[..n]; + // Element by element, never `copy_from_slice`: Kani 0.68 mis-models a + // bulk copy of symbolic length (see `kani_symbolic_copy_canary`). + let mut both = [(0u8, Side::Debit, 0i64); 2 * N]; + for i in 0..n { + let (k, s, a) = lines[i]; + both[i] = lines[i]; + both[n + i] = kernel::reverse_line((k, s, a)); + } + let mut out = [(0u8, 0i64); 2 * N]; + let m = kernel::movements_into(&both[..2 * n], &mut out).expect("no overflow"); + for &(_, total) in &out[..m] { + assert_eq!(total, 0); + } + // Not vacuous: an account with several lines on both sides is reached. + kani::cover!(n == N && m == 1, "four lines on one account, reversed"); +} + +// --------------------------------------------------------------------------- +// Balances and statements +// --------------------------------------------------------------------------- + +/// A normal balance is the movement for assets and expenses, and its +/// negation for liabilities, equity, and revenue. This is the fact the +/// accounting equation rests on: the Lean theorem `accounting_equation` +/// proves it gives Assets = Liabilities + Equity + (Revenue − Expenses) +/// for any number of accounts whose movements net to zero. +#[kani::proof] +fn normal_balance_is_signed() { + let t = any_type(); + let m = any_amount(); + let b = kernel::normal_balance(t, m).expect("in range"); + match t { + AccountType::Asset | AccountType::Expense => assert_eq!(b, m), + AccountType::Liability | AccountType::Equity | AccountType::Revenue => { + assert_eq!(b, -m) + } + } +} + +/// The accounting equation end to end on the code, for up to three +/// accounts: whenever movements net to zero, +/// Assets = Liabilities + Equity + (Revenue − Expenses). (Regrouping a +/// sum of signed 64-bit values is hard for a SAT solver, so the bound is +/// small here; `normal_balance_is_signed` and the Lean proof cover the +/// rest.) +#[kani::proof] +#[kani::unwind(4)] +fn accounting_equation() { + const EQ: usize = 3; + let all: [(AccountType, i64); EQ] = core::array::from_fn(|_| (any_type(), any_amount())); + let n: usize = kani::any(); + kani::assume(n <= EQ); + let accounts = &all[..n]; + let (mut net, mut a, mut l, mut e, mut r, mut x) = (0i64, 0i64, 0i64, 0i64, 0i64, 0i64); + for &(t, m) in accounts { + net += m; + let b = kernel::normal_balance(t, m).expect("in range"); + match t { + AccountType::Asset => a += b, + AccountType::Liability => l += b, + AccountType::Equity => e += b, + AccountType::Revenue => r += b, + AccountType::Expense => x += b, + } + } + assert_eq!(a - (l + e + (r - x)), net); + if net == 0 { + assert_eq!(a, l + e + (r - x)); + kani::cover!(n == EQ, "a balanced three-account chart"); + } +} + +/// A normal-side line raises an account's balance by its amount; an +/// opposite-side line lowers it. +#[kani::proof] +fn normal_side_increases() { + let t = any_type(); + let a = any_amount(); + let side = any_side(); + let movement = kernel::signed(side, a).expect("in range"); + let bal = kernel::normal_balance(t, movement).expect("in range"); + if side == t.normal_side() { + assert_eq!(bal, a); + } else { + assert_eq!(bal, -a); + } +} + +/// A trial balance puts each movement in exactly one non-negative column, +/// so its columns balance exactly when movements net to zero. +#[kani::proof] +#[kani::unwind(6)] +fn trial_balance_columns() { + let all: [i64; N] = core::array::from_fn(|_| any_amount()); + let moves = &all[..any_len()]; + let (mut debits, mut credits) = (0i64, 0i64); + for &m in moves { + let (d, c) = kernel::columns(m).expect("in range"); + assert!(d >= 0 && c >= 0); + assert!(d == 0 || c == 0); + assert_eq!(d - c, m); + debits += d; + credits += c; + } + let net: i64 = moves.iter().map(|&m| m).sum(); + assert_eq!(debits - credits, net); + assert_eq!(debits == credits, net == 0); +} + +// --------------------------------------------------------------------------- +// Closing +// --------------------------------------------------------------------------- + +/// A closing line zeroes its account: opposite side, same amount, nothing +/// for a zero balance. +#[kani::proof] +fn closing_line_zeroes() { + let m = any_amount(); + match kernel::closing_line(m) { + None => assert_eq!(m, 0), + Some((side, amount)) => { + assert!(amount > 0); + assert_eq!(m + wide(side, amount), 0); + } + } +} + +/// `credit_line` credits exactly what it is asked to. +#[kani::proof] +fn credit_line_credits() { + let c = any_amount(); + match kernel::credit_line(c) { + None => assert_eq!(c, 0), + Some((side, amount)) => { + assert!(amount > 0); + assert_eq!(wide(side, amount), -c); + } + } +} + +/// A period close balances and zeroes every revenue and expense account: +/// one closing line per nonzero nominal account, plus the net credited to +/// equity (whole, or split among members): the entry's lines net to +/// zero, and each nominal account ends at zero. +#[kani::proof] +#[kani::unwind(6)] +fn closing_entry_balances() { + const NOMINAL: usize = 3; + let nominal: [i64; NOMINAL] = core::array::from_fn(|_| any_amount()); + // Each nominal account's closing line zeroes it. + let mut entry = [(Side::Debit, 0i64); NOMINAL + 2]; + let mut len = 0; + for &m in &nominal { + if let Some((side, amount)) = kernel::closing_line(m) { + assert_eq!(m + wide(side, amount), 0); + entry[len] = (side, amount); + len += 1; + } else { + assert_eq!(m, 0); + } + } + let net = kernel::net(entry[..len].iter().copied()).expect("no overflow"); + // Split the net between two members, the first share rounded any way. + let mut parts = [any_amount(), 0]; + kernel::plug_last(net, &mut parts).expect("no overflow"); + for p in parts { + if let Some(line) = kernel::credit_line(p) { + entry[len] = line; + len += 1; + } + } + assert_eq!(wide_net(&entry[..len]), 0); + kani::cover!(len == NOMINAL + 2, "three accounts closed to two members"); +} + +/// An allocation's parts sum to the whole exactly, whatever the rounding +/// of the others, and only the last part changes. +#[kani::proof] +#[kani::unwind(6)] +fn plug_last_sums_exactly() { + let whole = any_amount(); + let n = any_len(); + let mut all: [i64; N] = core::array::from_fn(|_| any_amount()); + let before = all; + let parts = &mut all[..n]; + kernel::plug_last(whole, parts).expect("no overflow"); + if n > 0 { + let sum: i64 = parts.iter().map(|&p| p).sum(); + assert_eq!(sum, whole); + for i in 0..n - 1 { + assert_eq!(parts[i], before[i]); + } + } +} + +// --------------------------------------------------------------------------- +// The checker itself +// --------------------------------------------------------------------------- + +/// A canary for a known Kani bug: Kani 0.68 (CBMC 6.11) mis-models a bulk +/// copy whose length is symbolic, so this correct copy "fails" +/// (model-checking/kani#4904, closed as a duplicate, unfixed in 0.68). The +/// bug is unsound in both directions, so no harness above copies a slice +/// of symbolic length. This harness is expected to fail; when a Kani +/// upgrade fixes the bug it will start passing, `should_panic` will then +/// report it, and this canary and the comment in `reversal_cancels` can go. +#[kani::proof] +#[kani::unwind(10)] +#[kani::should_panic] +fn kani_symbolic_copy_canary() { + let src: [i64; N] = kani::any(); + let n = any_len(); + let mut dst = [0i64; 2 * N]; + dst[..n].copy_from_slice(&src[..n]); + for i in 0..n { + assert_eq!(dst[i], src[i]); + } +} diff --git a/crates/ledger-core/src/reports.rs b/crates/ledger-core/src/reports.rs index dcc4f4d..79742b6 100644 --- a/crates/ledger-core/src/reports.rs +++ b/crates/ledger-core/src/reports.rs @@ -59,10 +59,8 @@ fn trial_balance_where(ledger: &Ledger, include: &dyn Fn(&JournalEntry) -> bool) let mut movements: BTreeMap = BTreeMap::new(); for entry in ledger.posted_entries().filter(|e| include(e)) { for line in entry.lines() { - let signed = match line.side { - crate::Side::Debit => line.amount.amount, - crate::Side::Credit => -line.amount.amount, - }; + let signed = crate::kernel::signed(line.side, line.amount.amount) + .expect("Decimal negation is exact"); *movements.entry(line.account).or_default() += signed; } } @@ -80,11 +78,7 @@ fn trial_balance_where(ledger: &Ledger, include: &dyn Fn(&JournalEntry) -> bool) if movement.is_zero() { continue; } - let (debit, credit) = if movement > Decimal::ZERO { - (movement, Decimal::ZERO) - } else { - (Decimal::ZERO, -movement) - }; + let (debit, credit) = crate::kernel::columns(movement).expect("Decimal negation is exact"); total_debits += debit; total_credits += credit; lines.push(TrialBalanceLine { diff --git a/crates/ledger-core/tests/invariants.rs b/crates/ledger-core/tests/invariants.rs index 6450ca5..1d89ac5 100644 --- a/crates/ledger-core/tests/invariants.rs +++ b/crates/ledger-core/tests/invariants.rs @@ -181,6 +181,65 @@ fn zero_amount_line_is_rejected() { ); } +#[test] +fn negative_amount_line_is_rejected() { + let c = fixture_company(); + let mut ledger = c.ledger; + let id = ledger.create_entry(date(21), "Negative line"); + let minus = Money::new(Decimal::from(-100), Currency::USD); + ledger.add_line(id, c.cash, Side::Debit, minus).unwrap(); + ledger.add_line(id, c.equity, Side::Credit, minus).unwrap(); + assert_eq!( + ledger.post_entry(id).unwrap_err(), + LedgerError::NegativeAmountLine + ); +} + +#[test] +fn out_of_range_amount_is_rejected() { + let c = fixture_company(); + let mut ledger = c.ledger; + // Big enough to overflow a sum: an error, never a panic. + let id = ledger.create_entry(date(21), "Too big"); + let big = Money::new(Decimal::MAX, Currency::USD); + ledger.add_line(id, c.cash, Side::Debit, big).unwrap(); + ledger.add_line(id, c.cash, Side::Debit, big).unwrap(); + ledger.add_line(id, c.equity, Side::Credit, big).unwrap(); + assert_eq!( + ledger.post_entry(id).unwrap_err(), + LedgerError::AmountOutOfRange + ); + // Too precise. + let id = ledger.create_entry(date(21), "Too precise"); + let tiny = Money::new("0.00000000001".parse().unwrap(), Currency::USD); + ledger.add_line(id, c.cash, Side::Debit, tiny).unwrap(); + ledger.add_line(id, c.equity, Side::Credit, tiny).unwrap(); + assert_eq!( + ledger.post_entry(id).unwrap_err(), + LedgerError::AmountOutOfRange + ); +} + +#[test] +fn fx_overflow_is_an_error() { + let c = fixture_company(); + let mut ledger = c.ledger; + let id = ledger.create_entry(date(21), "Huge FX"); + assert_eq!( + ledger + .add_line_fx( + id, + c.cash, + Side::Debit, + Currency::EUR, + Decimal::MAX, + Decimal::from(2) + ) + .unwrap_err(), + LedgerError::AmountOutOfRange + ); +} + #[test] fn unknown_account_is_rejected() { let c = fixture_company(); diff --git a/crates/ledger-core/tests/kernel_bridge.rs b/crates/ledger-core/tests/kernel_bridge.rs new file mode 100644 index 0000000..8ae4e72 --- /dev/null +++ b/crates/ledger-core/tests/kernel_bridge.rs @@ -0,0 +1,154 @@ +//! The bridge between the proofs and the engine. +//! +//! The Kani harnesses (`src/proofs.rs`) prove the accounting kernel on +//! `i64` money in the smallest unit; the engine runs the same kernel on +//! `Decimal`. These properties check the two instantiations agree, value +//! for value, on cents: whatever Kani proved of the `i64` kernel holds of +//! the `Decimal` one for the same amounts. + +use ledger_core::kernel::{self, Amount, LineError}; +use ledger_core::{AccountType, Side}; +use proptest::prelude::*; +use rust_decimal::Decimal; + +/// Cents within both instantiations' line range. +const MAX_CENTS: i64 = 1 << 40; + +fn dec(cents: i64) -> Decimal { + Decimal::new(cents, 2) +} + +fn arb_side() -> impl Strategy { + prop_oneof![Just(Side::Debit), Just(Side::Credit)] +} + +fn arb_type() -> impl Strategy { + prop_oneof![ + Just(AccountType::Asset), + Just(AccountType::Liability), + Just(AccountType::Equity), + Just(AccountType::Revenue), + Just(AccountType::Expense), + ] +} + +fn arb_cents() -> impl Strategy { + prop_oneof![ + -MAX_CENTS..=MAX_CENTS, + // Small amounts collide, so balanced entries and zeros show up. + -3i64..=3, + ] +} + +/// Lines over four accounts. Balanced entries are rare at random, so half +/// the time the last line plugs the difference. +fn arb_lines() -> impl Strategy> { + ( + prop::collection::vec((0u8..4, arb_side(), arb_cents()), 0..7), + any::(), + ) + .prop_map(|(mut lines, plug)| { + if plug && !lines.is_empty() { + let net: i64 = lines[..lines.len() - 1] + .iter() + .map(|&(_, s, a)| if s == Side::Debit { a } else { -a }) + .sum(); + let last = lines.len() - 1; + if net.abs() > MAX_CENTS { + // Out of both ranges, where the two differ by design. + return lines; + } + lines[last].1 = if net > 0 { Side::Credit } else { Side::Debit }; + lines[last].2 = net.abs(); + } + lines + }) +} + +fn to_dec(lines: &[(u8, Side, i64)]) -> Vec<(u8, Side, Decimal)> { + lines.iter().map(|&(k, s, a)| (k, s, dec(a))).collect() +} + +fn sides(lines: &[(u8, Side, T)]) -> Vec<(Side, T)> { + lines.iter().map(|&(_, s, a)| (s, a)).collect() +} + +fn map_err(e: LineError) -> LineError { + match e { + LineError::TooFewLines => LineError::TooFewLines, + LineError::ZeroAmount => LineError::ZeroAmount, + LineError::NegativeAmount => LineError::NegativeAmount, + LineError::OutOfRange => LineError::OutOfRange, + LineError::Unbalanced { debits, credits } => LineError::Unbalanced { + debits: dec(debits), + credits: dec(credits), + }, + } +} + +proptest! { + #![proptest_config(ProptestConfig::with_cases(2000))] + + #[test] + fn check_lines_agrees(lines in arb_lines()) { + let i = kernel::check_lines(&sides(&lines)).map_err(map_err); + let d = kernel::check_lines(&sides(&to_dec(&lines))); + prop_assert_eq!(i, d); + } + + #[test] + fn sums_agree(lines in arb_lines()) { + let (i, d) = (sides(&lines), sides(&to_dec(&lines))); + let ti = kernel::totals(i.iter().copied()).unwrap(); + let td = kernel::totals(d.iter().copied()).unwrap(); + prop_assert_eq!((dec(ti.0), dec(ti.1)), td); + prop_assert_eq!( + kernel::net(i.iter().copied()).map(dec), + kernel::net(d.iter().copied()) + ); + let mi: Vec<_> = kernel::movements(lines.iter().copied()) + .unwrap() + .into_iter() + .map(|(k, m)| (k, dec(m))) + .collect(); + prop_assert_eq!(Some(mi), kernel::movements(to_dec(&lines))); + } + + #[test] + fn reversal_agrees(lines in arb_lines()) { + let ri: Vec<_> = kernel::reversal(&lines) + .into_iter() + .map(|(k, s, a)| (k, s, dec(a))) + .collect(); + prop_assert_eq!(ri, kernel::reversal(&to_dec(&lines))); + } + + #[test] + fn balances_agree(t in arb_type(), m in arb_cents()) { + prop_assert_eq!(kernel::normal_balance(t, m).map(dec), kernel::normal_balance(t, dec(m))); + let ci = kernel::columns(m).unwrap(); + prop_assert_eq!(Some((dec(ci.0), dec(ci.1))), kernel::columns(dec(m))); + prop_assert_eq!( + kernel::closing_line(m).map(|(s, a)| (s, dec(a))), + kernel::closing_line(dec(m)) + ); + prop_assert_eq!( + kernel::credit_line(m).map(|(s, a)| (s, dec(a))), + kernel::credit_line(dec(m)) + ); + } + + #[test] + fn plug_last_agrees(whole in arb_cents(), parts in prop::collection::vec(arb_cents(), 0..5)) { + let mut pi = parts.clone(); + let mut pd: Vec = parts.iter().copied().map(dec).collect(); + kernel::plug_last(whole, &mut pi).unwrap(); + kernel::plug_last(dec(whole), &mut pd).unwrap(); + prop_assert_eq!(pi.into_iter().map(dec).collect::>(), pd); + } + + #[test] + fn line_range_agrees(cents in arb_cents()) { + prop_assert_eq!(cents.in_line_range(), dec(cents).in_line_range()); + } +} diff --git a/docs/architecture.md b/docs/architecture.md index 9eb064e..e585495 100644 --- a/docs/architecture.md +++ b/docs/architecture.md @@ -57,7 +57,7 @@ The core is a pure domain library and stays that way. | `ledger-store` | Journal (hash-chained JSONL) + SQLite projection, blob store | `ledger-core` | | `ledger-import` | QuickBooks CSV read-only import (bank transactions, chart of accounts) | `ledger-core` | | `ledger-export` | Format renderers: CSV, XLSX, IIF journal entries (QuickBooks Desktop) | `ledger-core` | -| `ledger-oracle` | Diff harness: our engine vs GnuCash on fixture books | `ledger-core`, `ledger-import` | +| `ledger-oracle` | Cross-check harness: our engine vs other implementations (GnuCash first) on fixture books; diffs are adjudicated, not obeyed | `ledger-core`, `ledger-import` | Dependency direction is always inward toward `ledger-core`. Nothing in the core may depend on a future crate. UI concerns (formatting, locale, widgets) diff --git a/docs/oracle.md b/docs/oracle.md index 9f9f4e6..adfb415 100644 --- a/docs/oracle.md +++ b/docs/oracle.md @@ -9,15 +9,33 @@ our oracle is *semantic*, not visual. 1. **Fixture books.** A canonical set of journal entries exercising a feature (the January 2026 fixture company in `tests/invariants.rs` is the first). -2. **Two engines.** The same fixtures go through our engine and through - **GnuCash** — the open-source, double-entry reference implementation with - open file formats. GnuCash is both the spec and the oracle. +2. **More than one engine.** The same fixtures go through our engine and + through independent implementations: **GnuCash** (open source, open file + formats), the old Google Sheet, and later QBO/Xero exports. These are + *cross-checks*, not authorities (see "Who is right" below). 3. **Exact diff.** `reports::snapshot()` renders trial balance, P&L, and balance sheet as canonical JSON. The outputs must be **identical** — decimal strings, no floats, no locale, no epsilon. Where storytold allows 2/255 of perceptual slop, we allow zero: accounting has no "close enough". -## The three oracle layers (today → future) +## Who is right + +No other program is the spec. GnuCash, the Sheet, QuickBooks: each is +*an* oracle, and each can be wrong. The order of authority: + +1. **Accounting principles, stated as proofs.** The laws in + `docs/verification.md`, proved in Lean and model-checked by Kani. They + do not depend on any other implementation's behavior. +2. **Golden files recomputed by hand** from those principles (Layer 1). +3. **External oracles** (GnuCash, the Sheet, QBO/Xero exports). A + disagreement with one is a *finding*: work out from principles which + side is wrong and write the reasoning down. Never change our output just + to match theirs. If theirs is wrong, add a test that pins our correct + behavior, and note their bug in `docs/parity.md`. + +Nothing in this repo may rest on an external oracle's behavior alone. + +## The oracle layers (today → future) **Layer 1 — Golden files (live now).** `tests/golden/*.json` hold hand-verified expected reports for canonical fixtures. The golden test fails @@ -53,16 +71,28 @@ always balances exactly), `fuzz_op_sequence` (arbitrary op sequences via `arbitrary`; the trial balance always balances). 11.5M execs, zero crashes as of 2026-10-10. Corpora persist in `fuzz/corpus/` for regression. -**Layer 5 — GnuCash diff harness (roadmap phase 3).** A `ledger-oracle` crate -will run fixture books through our engine and through GnuCash headless, then -diff `snapshot()` output automatically — `cargo xtask oracle`. This is the -direct analog of storytold's `cargo xtask corpus` / `oracle_diff`. Note the -distinction: GnuCash is the *behavioral* oracle, not a file-format target +**Layer 4½ — Formal proofs (live now).** The accounting arithmetic lives +in one generic kernel (`kernel.rs`). Kani model-checks it exhaustively +within bounds, Lean 4 proves the laws for books of any size (trial +balance, accounting equation, reversals, posted-is-forever, frozen closed +periods, closing to net income), and a property test bridges the two. +`just prove`; see `docs/verification.md`. Its first pass found three +engine bugs that Layers 1–4 had all missed. + +**Layer 5 — Cross-implementation diff harness (roadmap phase 3).** A +`ledger-oracle` crate will run fixture books through our engine and through +other implementations (GnuCash headless first), then diff `snapshot()` +output automatically: `cargo xtask oracle`. This is the direct analog of +storytold's `cargo xtask corpus` / `oracle_diff`, with one difference: a +diff does not mean we are wrong. Each one is adjudicated from principles +(see "Who is right"). Note also: GnuCash is *a* behavioral cross-check, not +a file-format target (Stephen: "for file format import/export I could not give a single shit about GnuCash XML — QBO is all that matters"). The harness feeds fixtures to GnuCash via whatever it imports reliably (QIF/OFX) or its Python bindings; -the exact mechanism is decided at implementation time. Until the harness -exists, Layers 1 and 2 are the oracle, and they are not optional. +the exact mechanism is decided at implementation time. The proofs and +Layers 1–4 are the foundation and are not optional. The harness adds +evidence. It never overrides them. ## What the oracle does NOT cover (yet) diff --git a/docs/parity.md b/docs/parity.md index fe8ed9c..2f6f2bd 100644 --- a/docs/parity.md +++ b/docs/parity.md @@ -10,7 +10,7 @@ No other statuses. **Floor: 10 done** (2026-10-10; fixed-asset register added). -| Area | GnuCash reference | Status | Notes | +| Area | GnuCash counterpart (a cross-check, not the spec) | Status | Notes | |---|---|---|---| | Chart of accounts (5 types, codes, hierarchy) | Accounts tab | done | `account.rs`; placeholder support in | | Double-entry validation (balanced, ≥2 lines) | Journal validation | done | `journal.rs::validate` | @@ -44,7 +44,7 @@ No other statuses. | Payout gross-up (deposit → revenue, fees, adjustments) | Bank deposit with fee lines; Xero/QBO Stripe & Shopify integrations | partial | hand-verified fixture incl. classes and a negative payout; no statement parsers yet | | 1099 vendor tracking + year-end worksheet | Vendors → Track payments for 1099; 1099 report | partial | hand-verified fixture (bill payments, card exclusion, reversal, year boundary); no golden file yet | | Prepaid expense + deferred revenue amortization | Amortization schedules (Xero/QBO add-ons) | partial | hand-verified fixture, to the cent; no golden file yet | -| Automated GnuCash diff harness | — (our `xtask oracle`) | todo | roadmap phase 3 | +| Automated cross-implementation diff harness (GnuCash first) | — (our `xtask oracle`) | todo | roadmap phase 3 | Workflow/UI parity (QuickBooks/Xero reference) gets its own catalog when the egui phase starts; semantics come first. diff --git a/docs/verification.md b/docs/verification.md new file mode 100644 index 0000000..257db4f --- /dev/null +++ b/docs/verification.md @@ -0,0 +1,222 @@ +# Formal verification: the accounting laws, proved + +Tests check the examples someone thought of. Proofs check every case. +wanderbooks proves the fundamental laws of double-entry bookkeeping three +ways, each covering what the others can't: + +| Layer | Tool | What it proves | Scope | +|---|---|---|---| +| **Code** | [Kani](https://model-checking.github.io/kani/) (bounded model checking) | The engine's own Rust kernel is correct and never panics or overflows | Every input within the bounds: up to 4 lines, 3 accounts, amounts to 2^40 | +| **Laws** | [Lean 4](https://lean-lang.org) (machine-checked proof) | The laws hold for books of any size, after any sequence of commands | Unbounded: any number of entries, accounts, periods, steps | +| **Bridge** | proptest | The kernel on `Decimal` (what the engine runs) agrees with the kernel on `i64` (what Kani proves) | 2,000 random cases per property | + +Run all of it with `just prove` (after `mise install`; see the end). + +## The kernel + +Every invariant rests on a little arithmetic: signing a line, summing +sides, grouping by account, flipping for a reversal, reading a balance on +its normal side, splitting a movement into trial-balance columns, closing +an account, plugging the last share of an allocation. That arithmetic +lives in one place, `crates/ledger-core/src/kernel.rs`. Its functions +are small, pure, and generic over an `Amount` trait with *checked* +operations. The engine calls them on `Decimal`: `JournalEntry::validate`, +`movements`, `reverse_entry`, `account_balance`, `account_movement`, +period closing, `periods::allocate`, and the trial balance. There is no +second copy of the arithmetic for proofs to drift from. + +Kani compiles the same functions at `i64` (exact integer money in the +smallest unit) and explores every input in the bounds. (Grouping by +account is proved through `movements_into`, the allocation-free core +that `movements` wraps: symbolic heap growth is beyond what the model +checker explores in reasonable time.) The Lean model in +`verify/lean` restates each function over `Int` and proves the laws with +no bounds at all. + +## The laws + +Each law, and what proves it. Kani harnesses are in +`crates/ledger-core/src/proofs.rs`; Lean theorems are in +`verify/lean/Wanderbooks/`. + +### Entries + +1. **An entry is accepted exactly when** it has two or more lines, every + amount is positive and in range, and debits equal credits, to the unit. + - Kani `check_lines_is_exact` (both directions: no bad entry gets in, + no good one is refused), `out_of_range_is_rejected` + - Lean `Accepted` +2. **An accepted entry nets to zero.** + - Kani `accepted_entry_nets_to_zero` · Lean `Accepted.net_zero` +3. **Grouping by account loses and invents nothing**: each account's + movement is the net of its own lines, and the movements sum to the + entry's net. + - Kani `movements_are_per_account`, `movements_sum_to_the_net` · + Lean `sum_movements` +4. **Sums are exact and never overflow** for in-range lines. + - Kani `sums_are_exact` (every harness also fails on any panic or + arithmetic overflow) + +### Reversals + +5. **A reversal is accepted exactly when the original is**, and **the two + together net every account to zero**. + - Kani `reversal_mirrors`, `reversal_cancels`, `flip_negates` + - Lean `accepted_reversal_iff`, `movement_with_reversal` + +### Balances and statements + +6. **Normal sides**: a line on an account's normal side raises its + balance by the amount; the other side lowers it. + - Kani `normal_side_increases` · Lean `balance_after_line` +7. **The trial balance balances**, and it balances *only* if the books + net to zero: it is a complete check of the arithmetic. + - Kani `trial_balance_columns` · Lean `trial_balance_iff`, + `Reachable.trial_balance`, `Reachable.trial_balance_through` (as of + any date) +8. **The accounting equation**: Assets = Liabilities + Equity + (Revenue − + Expenses), always and as of any date. + - Kani `normal_balance_is_signed` (the fact it rests on, every type + and amount) and `accounting_equation` (end to end, up to three + accounts: regrouping signed 64-bit sums is hard for a SAT solver) · + Lean `accounting_equation`, `Reachable.accounting_equation`, + `Reachable.accounting_equation_through` (any number of accounts) +9. **Period statements add up**: a year's P&L is the sum of its months'. + - Lean `statements_add_up` + +### The books over time + +The Lean model (`Ledger.lean`) describes the engine as a state machine: +add an account, start a draft, post, reverse, open a period, close one. +Each step carries the checks the engine makes before it mutates. These +theorems hold in **every state reachable from empty books, by any +sequence of commands, of any length**: + +10. **The invariant holds**: chart codes are unique, every posted entry is + acceptable and on known accounts, and no draft is dated in a closed + period. (That last one is why the store can journal a post before + applying it: a post can never then fail on a closed period.) + - Lean `Step.inv`, `Reachable.inv` +11. **The books always net to zero.** · Lean `Reachable.books_net_zero` +12. **Posted is forever**: posting only appends. After any sequence of + commands the old log is a prefix of the new one. Nothing is edited, + reordered, or removed. + - Lean `Step.extends`, `Steps.extends` +13. **Closed periods are frozen**: once a period is closed, no sequence of + commands adds, removes, or changes an entry dated in it, and it stays + closed. + - Lean `Step.frozen`, `Steps.frozen` + +### Closing + +14. **A closing line zeroes its account**, and **a closing entry balances + and zeroes every revenue and expense account** through the period's + last day, whether the net goes to one account or is split among + members. + - Kani `closing_line_zeroes`, `credit_line_credits`, + `closing_entry_balances` + - Lean `closingEntry_net`, `closingEntry_zeroes`, + `closingEntry_accepted`, `close_zeroes` +15. **A close credits equity with exactly the net income**: revenue minus + expenses through the period's last day. + - Lean `net_closings_is_net_income`, `close_credits_net_income` +16. **An allocation's parts sum to the whole, to the unit**, however the + other shares were rounded, and only the last share changes. + - Kani `plug_last_sums_exactly` · Lean `plugLast_total`, + `plugLast_keeps` + +## What the proofs found + +The engine already had 190+ tests, property tests, mutation testing, +and 11.5M fuzz executions with zero crashes. Writing the laws down +precisely still turned up three gaps in it, now closed: + +- **Negative line amounts were accepted.** Only the MCP layer refused + them. The engine now rejects them (`NegativeAmountLine`): direction is + the side's job. +- **A huge amount could crash the engine.** Summing lines near + `Decimal::MAX` panicked instead of returning an error. Lines are now + limited to one quadrillion and ten decimal places + (`AmountOutOfRange`), and the kernel's sums are checked. +- **Foreign-currency conversion could crash** the same way + (`foreign_amount * fx_rate`). It is now a checked multiply. + +And three things besides bugs: + +- **A soundness bug in the verifier.** Kani reported a reversal that + doesn't net to zero. Tracing it took a native replay of the + counterexample (it passed) and a 15-line repro crate: Kani 0.68 + mis-models symbolic-length slice copies. See "Trusting the checker" + below. Taking every red result seriously is the method. +- **Simpler code.** `credit_line` and `closing_line` are the same + function. The model made that obvious, and the code now says so. +- **A load-bearing invariant, made explicit.** No draft can exist in a + closed period (`Inv.draftsOpen`). That is why the store can journal a + post before applying it: the closed-period check can never fail after + the journal write. It was true by accident of the checks' design. Now + it is a theorem, and breaking it breaks the build. + +Each of these shipped past every test we had. That is the case for +formal methods here: tests sample, proofs exhaust. `AGENTS.md` makes +growing this coverage part of every change. + +## Trusting the checker + +A model checker is a program too. While building these proofs, Kani +reported that an entry plus its reversal could leave an account nonzero. +That was not a bookkeeping bug. Kani's own counterexample passes when +replayed natively. We narrowed it to a 15-line crate with no wanderbooks +code: Kani 0.68 (CBMC 6.11) mis-models `copy_from_slice` whenever the +length is symbolic. It is the known bug model-checking/kani#4904, closed +as a duplicate and unfixed in 0.68. It is unsound in both directions: it +can also prove false claims. So: + +- **No harness copies a slice of symbolic length.** They write element by + element (`reversal_cancels` says why), and the kernel functions under + proof contain no bulk copies. +- **A canary watches for the fix.** `kani_symbolic_copy_canary` runs the + faulty copy and is marked `should_panic`. When a Kani upgrade fixes the + bug, the canary starts failing, and the workaround can go. +- **The proofs are not vacuous.** `kani::cover!` statements make Kani + show that the interesting cases are reachable: an accepted four-line + entry, a reversal on one account with several lines, three distinct + accounts, a balanced three-account chart, a close to two members. `just prove` fails if any cover is unsatisfiable. + +## What is and isn't proved + +Be precise about the claims: + +- **Kani is bounded.** It proves the kernel for every input up to 4 lines + over 3 accounts and amounts to 2^40 units (the accounting equation end + to end: up to 3 accounts). Lean proves the laws for any + size, but of a *model*. The model is a direct restatement of the kernel, + and the bridge property test ties the `Decimal` instantiation to the + `i64` one Kani checked. +- **`Decimal` itself is trusted.** `rust_decimal` is exact for these + sizes: 96-bit integers scaled by a power of ten. With lines capped at + one quadrillion and ten decimal places, every sum is exact while the + total of all amounts stays below 7.9 × 10^18. Kani can't explore + `Decimal` arithmetic directly: a single symbolic add runs for more than + ten minutes. +- **The state machine is a model of `Ledger`'s checks**, not a proof + about `ledger.rs` line by line. Its correspondence to the code is + checked by review and by the end-to-end property tests in + `tests/properties.rs` (trial balance, balance sheet, reversals, + immutability) and the golden files. +- **Out of scope:** currency (the ledger is single-currency, enforced + structurally), A/R and A/P documents, payroll, depreciation schedules + (those have their own property tests), and persistence (the journal + store's hash chain is tested in `ledger-store`). + +## Running it + +```sh +mise install # once: Kani, Lean, and the rest, pinned in mise.toml +just prove +``` + +`just prove` runs every Kani harness, builds the Lean proofs (seconds), +and fails if any headline theorem depends on anything beyond Lean's +standard axioms (`propext`, `Quot.sound`, `Classical.choice`). In +particular, `sorryAx` fails it. Kani downloads its pinned nightly and +CBMC into `~/.kani` on first use. diff --git a/justfile b/justfile index f76a0f2..cf40163 100644 --- a/justfile +++ b/justfile @@ -15,6 +15,30 @@ check: cargo clippy --workspace --all-targets -- -D warnings cargo test --workspace +# Formal proofs: Kani on the accounting kernel, Lean for books of any size (docs/verification.md) +prove: + #!/usr/bin/env bash + set -euo pipefail + # Capped: a harness that blows up should fail, not eat the machine. + log=$(mktemp) + (ulimit -v 12000000; cd crates/ledger-core && + timeout 1800 cargo kani -j "$(nproc)" --output-format terse | tee "$log") + # A cover that can't be satisfied means a proof is vacuous. + if grep -E "\*\* [0-9]+ of [0-9]+ cover properties satisfied" "$log" | + awk '{ if ($2 != $4) bad = 1 } END { exit !bad }'; then + echo "Kani: an unsatisfiable cover; some proof is vacuous" >&2 + exit 1 + fi + rm -f "$log" + cd verify/lean + lake build + audit=$(lake env lean Audit.lean) + if grep -v -E "depends on axioms: \[(propext|Quot.sound|Classical.choice)(, (propext|Quot.sound|Classical.choice))*\]$|does not depend on any axioms" <<<"$audit"; then + echo "Lean audit: a theorem rests on something beyond the standard axioms" >&2 + exit 1 + fi + echo "Lean: $(wc -l <<<"$audit") headline theorems, standard axioms only" + # Build the release binaries (CLI, MCP server, GUI) build: cargo build --release -p ledger-cli -p ledger-mcp -p ledger-gui diff --git a/plan/STATUS.md b/plan/STATUS.md index 4e9454a..4f657b5 100644 --- a/plan/STATUS.md +++ b/plan/STATUS.md @@ -58,6 +58,15 @@ public. Parity is 12 of 12 against the spreadsheet workflow. design, parity catalog (floor: 10 done), glossary, mcp-interface (incl. the 5 asset tools), receipt-store (journal design), capability-parity (10 of 12 rows covered). Plan: this file + roadmap. +- **Formal verification** (2026-10-13, `docs/verification.md`): the + money arithmetic moved into one generic kernel (`kernel.rs`) that the + engine calls. 18 Kani harnesses prove it exhaustively within bounds, + with covers against vacuity and a canary for a Kani soundness bug. 24 + Lean 4 theorems prove the accounting laws for books of any size, after + any sequence of commands. A property test bridges `i64` and `Decimal`. + `just prove`. Found and fixed: negative line amounts accepted by the + engine, an overflow crash on huge amounts, and an overflow crash in FX + conversion. **In progress:** nothing — the next arcs are queued below, unstarted. @@ -76,11 +85,18 @@ interface is MCP, not a cloned GUI. The first storage + MCP slice is done 4. **Capability parity** (`docs/capability-parity.md`): 11 of 12 rows covered; full CPA export (xlsx/iif) remains. Then the month-long parallel run against the GSheet; cutover per the cutover rule. -5. Then: oracle harness (GnuCash diff), read-only GUI on the event log, +5. Then: oracle harness (cross-check diffs, GnuCash first), read-only GUI on the event log, workflow parity. ## Decisions log +- 2026-10-13: Formal methods are part of the bar (Stephen: "This shit is + fucking GOLD"). Money arithmetic lives in `kernel.rs` with Kani + harnesses; accounting laws get Lean theorems; `just prove` stays green. + The engine now rejects negative and out-of-range line amounts (max one + quadrillion, ten decimal places). Every dev tool is pinned in + `mise.toml`. See AGENTS.md "Formal methods". + - 2026-10-10: Single currency per ledger for day one (R-5). Multi-currency is designed-for, not built. - 2026-10-10: `Money` arithmetic is checked and returns `Result`; no @@ -96,8 +112,9 @@ interface is MCP, not a cloned GUI. The first storage + MCP slice is done a parallel-run cutover rule. GUI drops to read-only, event-log-driven, phase 4. - 2026-10-10: Import/export targets QuickBooks formats (CSV, IIF, XLSX) — - "could not give a single shit about GnuCash XML." GnuCash stays the - *behavioral* oracle only. Receipt enforcement is server-side policy in the + "could not give a single shit about GnuCash XML." GnuCash stays a + *behavioral* cross-check only. (2026-10-13, Stephen: it is "an" oracle, + not "the" oracle; never trust it to be correct.) Receipt enforcement is server-side policy in the MCP layer (threshold + per-account overrides, typed `receipt_required` error, checklist in every preview); the engine stays policy-free. - 2026-10-10: Storage durability (Stephen). SQLite is the query engine, not diff --git a/plan/roadmap.md b/plan/roadmap.md index f0e4845..32265e8 100644 --- a/plan/roadmap.md +++ b/plan/roadmap.md @@ -24,8 +24,10 @@ The primary interface is MCP, not a cloned GUI (Stephen's call, 2026-10-10). ## Phase 3 — Oracle harness (next) -- `ledger-oracle`: fixture books through our engine and GnuCash headless, - automatic `snapshot()` diffing. +- `ledger-oracle`: fixture books through our engine and other + implementations (GnuCash headless first), automatic `snapshot()` + diffing. Each diff is adjudicated from principles; no other program is + the authority. - Parity catalog becomes machine-readable; CI enforces the non-regression floor. - Done when: a fixture book produces byte-identical snapshots from both @@ -82,7 +84,8 @@ The primary interface is MCP, not a cloned GUI (Stephen's call, 2026-10-10). - Multi-currency with FX translation. - Period close. - The goal: a self-hosted bookkeeping system with a tested claim to - semantic parity with GnuCash and capability parity with the old + proved accounting semantics (cross-checked against GnuCash and others) + and capability parity with the old GSheet+GDrive workflow — no SaaS subscription required. ## Explicitly not on the roadmap diff --git a/verify/lean/.gitignore b/verify/lean/.gitignore new file mode 100644 index 0000000..01f8cdb --- /dev/null +++ b/verify/lean/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/verify/lean/Audit.lean b/verify/lean/Audit.lean new file mode 100644 index 0000000..8983c4e --- /dev/null +++ b/verify/lean/Audit.lean @@ -0,0 +1,32 @@ +import Wanderbooks + +/-! `just prove` runs this file: each headline theorem's axioms are printed, +and must be only Lean's standard three (`propext`, `Quot.sound`, +`Classical.choice`) or fewer. No `sorryAx`, nothing assumed. -/ + +open Wanderbooks + +#print axioms Accepted.net_zero +#print axioms sum_movements +#print axioms movement_with_reversal +#print axioms accepted_reversal_iff +#print axioms accounting_equation +#print axioms balance_after_line +#print axioms trial_balance_iff +#print axioms closingEntry_net +#print axioms closingEntry_zeroes +#print axioms closingEntry_accepted +#print axioms net_closings_is_net_income +#print axioms plugLast_total +#print axioms plugLast_keeps +#print axioms Reachable.inv +#print axioms Reachable.books_net_zero +#print axioms Reachable.trial_balance +#print axioms Reachable.trial_balance_through +#print axioms Reachable.accounting_equation +#print axioms Reachable.accounting_equation_through +#print axioms Steps.extends +#print axioms Steps.frozen +#print axioms close_zeroes +#print axioms close_credits_net_income +#print axioms statements_add_up diff --git a/verify/lean/Wanderbooks.lean b/verify/lean/Wanderbooks.lean new file mode 100644 index 0000000..0b2a78b --- /dev/null +++ b/verify/lean/Wanderbooks.lean @@ -0,0 +1,5 @@ +import Wanderbooks.Basic +import Wanderbooks.Entry +import Wanderbooks.Statements +import Wanderbooks.Closing +import Wanderbooks.Ledger diff --git a/verify/lean/Wanderbooks/Basic.lean b/verify/lean/Wanderbooks/Basic.lean new file mode 100644 index 0000000..a5cad23 --- /dev/null +++ b/verify/lean/Wanderbooks/Basic.lean @@ -0,0 +1,165 @@ +/-! +# Lines, sides, and nets + +The vocabulary of double entry. Money is `Int`: an exact count of the +smallest unit the books use. Any finite set of exact decimals (what the +engine stores) scales to integers without loss, and every law here is a +law of addition, so `Int` is a faithful model. + +Mirrors `crates/ledger-core/src/kernel.rs` (`flip`, `signed`, `net`, +`totals`) and `account.rs` (`Side`, `AccountType`, `normal_side`). +-/ + +namespace Wanderbooks + +/-- Debit or credit. -/ +inductive Side where + | debit + | credit + deriving DecidableEq, Repr + +/-- The other side (`kernel::flip`). -/ +def Side.flip : Side → Side + | .debit => .credit + | .credit => .debit + +@[simp] theorem Side.flip_flip (s : Side) : s.flip.flip = s := by + cases s <;> rfl + +theorem Side.flip_ne (s : Side) : s.flip ≠ s := by + cases s <;> simp [Side.flip] + +/-- The five account types. -/ +inductive AccountType where + | asset + | liability + | equity + | revenue + | expense + deriving DecidableEq, Repr + +/-- The side that increases an account (`AccountType::normal_side`). -/ +def AccountType.normal : AccountType → Side + | .asset | .expense => .debit + | .liability | .equity | .revenue => .credit + +/-- A line's signed amount: `+a` for a debit, `-a` for a credit +(`kernel::signed`). -/ +def signed : Side → Int → Int + | .debit, a => a + | .credit, a => -a + +@[simp] theorem signed_debit (a : Int) : signed .debit a = a := rfl +@[simp] theorem signed_credit (a : Int) : signed .credit a = -a := rfl + +theorem signed_flip (s : Side) (a : Int) : signed s.flip a = -signed s a := by + cases s <;> simp [Side.flip] + +/-- One journal line. -/ +structure Line where + account : Nat + side : Side + amount : Int + deriving DecidableEq, Repr + +/-- A line's signed amount. -/ +def Line.signed (l : Line) : Int := Wanderbooks.signed l.side l.amount + +/-- The net of some lines: debits minus credits (`kernel::net`). -/ +def net : List Line → Int + | [] => 0 + | l :: ls => l.signed + net ls + +/-- Total debits. -/ +def debits : List Line → Int + | [] => 0 + | l :: ls => (if l.side = .debit then l.amount else 0) + debits ls + +/-- Total credits. -/ +def credits : List Line → Int + | [] => 0 + | l :: ls => (if l.side = .credit then l.amount else 0) + credits ls + +@[simp] theorem net_nil : net [] = 0 := rfl +@[simp] theorem net_cons (l : Line) (ls : List Line) : net (l :: ls) = l.signed + net ls := rfl + +theorem net_append (xs ys : List Line) : net (xs ++ ys) = net xs + net ys := by + induction xs with + | nil => simp + | cons x xs ih => simp only [List.cons_append, net_cons, ih]; omega + +/-- The net is debits minus credits. -/ +theorem net_eq_debits_sub_credits (ls : List Line) : net ls = debits ls - credits ls := by + induction ls with + | nil => rfl + | cons l ls ih => + obtain ⟨a, s, m⟩ := l + cases s <;> simp [net, debits, credits, Line.signed, signed, ih] <;> omega + +/-- A sum over a list of account codes. -/ +def sumOver (f : Nat → Int) : List Nat → Int + | [] => 0 + | a :: as => f a + sumOver f as + +@[simp] theorem sumOver_nil (f : Nat → Int) : sumOver f [] = 0 := rfl +@[simp] theorem sumOver_cons (f : Nat → Int) (a : Nat) (as : List Nat) : + sumOver f (a :: as) = f a + sumOver f as := rfl + +theorem sumOver_add (f g : Nat → Int) (as : List Nat) : + sumOver (fun a => f a + g a) as = sumOver f as + sumOver g as := by + induction as with + | nil => rfl + | cons a as ih => simp only [sumOver_cons, ih]; omega + +theorem sumOver_neg (f : Nat → Int) (as : List Nat) : + sumOver (fun a => -f a) as = -sumOver f as := by + induction as with + | nil => rfl + | cons a as ih => simp only [sumOver_cons, ih]; omega + +theorem sumOver_zero (as : List Nat) : sumOver (fun _ => 0) as = 0 := by + induction as with + | nil => rfl + | cons a as ih => simp [ih] + +theorem sumOver_congr (f g : Nat → Int) (as : List Nat) (h : ∀ a ∈ as, f a = g a) : + sumOver f as = sumOver g as := by + induction as with + | nil => rfl + | cons a as ih => + simp only [sumOver_cons] + rw [h a (by simp), ih (fun b hb => h b (by simp [hb]))] + +/-- No code repeats (a chart's codes are unique). -/ +def Distinct : List Nat → Prop + | [] => True + | a :: as => a ∉ as ∧ Distinct as + +/-- Summing an indicator over codes that do not include `k` gives zero. -/ +theorem sumOver_indicator_absent (k : Nat) (x : Int) (as : List Nat) (h : k ∉ as) : + sumOver (fun a => if k = a then x else 0) as = 0 := by + induction as with + | nil => rfl + | cons a as ih => + have hka : k ≠ a := fun e => h (e ▸ List.mem_cons_self ..) + have hk : k ∉ as := fun hm => h (List.mem_cons_of_mem _ hm) + simp [hka, ih hk] + +/-- Summing an indicator over distinct codes that include `k` picks out +exactly one term. -/ +theorem sumOver_indicator (k : Nat) (x : Int) (as : List Nat) (hd : Distinct as) + (hk : k ∈ as) : sumOver (fun a => if k = a then x else 0) as = x := by + induction as with + | nil => simp at hk + | cons a as ih => + obtain ⟨ha, hd⟩ := hd + by_cases e : k = a + · subst e + simp [sumOver_indicator_absent k x as ha] + · have : k ∈ as := by + cases hk with + | head => exact absurd rfl e + | tail _ h => exact h + simp [e, ih hd this] + +end Wanderbooks diff --git a/verify/lean/Wanderbooks/Closing.lean b/verify/lean/Wanderbooks/Closing.lean new file mode 100644 index 0000000..dade993 --- /dev/null +++ b/verify/lean/Wanderbooks/Closing.lean @@ -0,0 +1,320 @@ +import Wanderbooks.Statements + +/-! +# Closing a period, and splitting the net + +Mirrors `kernel::closing_line`, `kernel::credit_line`, `kernel::plug_last`, +`periods::allocate`, and `Ledger::close_period_to` (income closing, net to +one equity account or split among members). +-/ + +namespace Wanderbooks + +/-- The line that zeroes an account with movement `m`: the opposite side, +same amount; nothing for zero (`kernel::closing_line`). It is also the +line that credits `m` to an account (`kernel::credit_line`). -/ +def closingLine (a : Nat) (m : Int) : List Line := + if 0 < m then [⟨a, .credit, m⟩] else if m < 0 then [⟨a, .debit, -m⟩] else [] + +theorem net_closingLine (a : Nat) (m : Int) : net (closingLine a m) = -m := by + unfold closingLine + split + · simp [Line.signed] + · split <;> simp [Line.signed] <;> omega + +theorem movement_closingLine (b a : Nat) (m : Int) : + movement b (closingLine a m) = if b = a then -m else 0 := by + by_cases e : b = a + · subst e + rcases (by omega : 0 < m ∨ m < 0 ∨ m = 0) with h | h | h + · simp [closingLine, h, Line.signed] + · have : ¬ 0 < m := by omega + simp [closingLine, h, this, Line.signed] + · simp [closingLine, h] + · have e' : ¬ a = b := fun x => e x.symm + unfold closingLine + split <;> (try split) <;> simp [e'] + +theorem closingLine_pos (a : Nat) (m : Int) : ∀ l ∈ closingLine a m, 0 < l.amount := by + unfold closingLine + split + · simp; omega + · split + · simp; omega + · simp + +theorem closingLine_account (a : Nat) (m : Int) : ∀ l ∈ closingLine a m, l.account = a := by + unfold closingLine + split + · simp + · split <;> simp + +theorem closingLine_eq_nil (a : Nat) (m : Int) : closingLine a m = [] ↔ m = 0 := by + unfold closingLine + split + · simp; omega + · split + · simp; omega + · simp; omega + +/-- The closing lines for some accounts: one per account with a nonzero +movement. -/ +def closings (as : List Nat) (ls : List Line) : List Line := + match as with + | [] => [] + | a :: as => closingLine a (movement a ls) ++ closings as ls + +theorem net_closings (as : List Nat) (ls : List Line) : + net (closings as ls) = -sumOver (fun a => movement a ls) as := by + induction as with + | nil => rfl + | cons a as ih => simp only [closings, net_append, net_closingLine, ih, sumOver_cons]; omega + +theorem movement_closings (b : Nat) (as : List Nat) (ls : List Line) (hd : Distinct as) : + movement b (closings as ls) = if b ∈ as then -movement b ls else 0 := by + induction as with + | nil => simp [closings] + | cons a as ih => + obtain ⟨ha, hd⟩ := hd + simp only [closings, movement_append, movement_closingLine, ih hd] + by_cases e : b = a + · subst e; simp [ha] + · simp [e] + +theorem closings_pos (as : List Nat) (ls : List Line) : ∀ l ∈ closings as ls, 0 < l.amount := by + induction as with + | nil => simp [closings] + | cons a as ih => + intro l hl + simp only [closings, List.mem_append] at hl + cases hl with + | inl h => exact closingLine_pos _ _ l h + | inr h => exact ih l h + +theorem closings_account (as : List Nat) (ls : List Line) : ∀ l ∈ closings as ls, l.account ∈ as := by + induction as with + | nil => simp [closings] + | cons a as ih => + intro l hl + simp only [closings, List.mem_append] at hl + cases hl with + | inl h => rw [closingLine_account _ _ l h]; simp + | inr h => exact List.mem_cons_of_mem _ (ih l h) + +/-- Nothing to close means every closed account was already at zero. -/ +theorem closings_eq_nil (as : List Nat) (ls : List Line) (h : closings as ls = []) : + ∀ a ∈ as, movement a ls = 0 := by + induction as with + | nil => simp + | cons a as ih => + simp only [closings, List.append_eq_nil_iff] at h + intro b hb + cases hb with + | head => exact (closingLine_eq_nil _ _).1 h.1 + | tail _ hb => exact ih h.2 b hb + +/-! ## The net to equity -/ + +/-- The sum of some amounts. -/ +def total : List Int → Int + | [] => 0 + | x :: xs => x + total xs + +/-- Lines crediting each target its part (`kernel::credit_line` per +member). -/ +def equityLines : List (Nat × Int) → List Line + | [] => [] + | (t, c) :: ts => closingLine t c ++ equityLines ts + +theorem net_equityLines (ts : List (Nat × Int)) : + net (equityLines ts) = -total (ts.map Prod.snd) := by + induction ts with + | nil => rfl + | cons x ts ih => + obtain ⟨t, c⟩ := x + simp only [equityLines, net_append, net_closingLine, ih, List.map_cons, total]; omega + +theorem movement_equityLines_absent (b : Nat) (ts : List (Nat × Int)) + (h : ∀ x ∈ ts, x.1 ≠ b) : movement b (equityLines ts) = 0 := by + induction ts with + | nil => rfl + | cons x ts ih => + obtain ⟨t, c⟩ := x + have ht : b ≠ t := fun e => h (t, c) (by simp) e.symm + simp only [equityLines, movement_append, movement_closingLine, ht, ite_false, + ih (fun y hy => h y (List.mem_cons_of_mem _ hy))] + rfl + +theorem equityLines_pos (ts : List (Nat × Int)) : ∀ l ∈ equityLines ts, 0 < l.amount := by + induction ts with + | nil => simp [equityLines] + | cons x ts ih => + obtain ⟨t, c⟩ := x + intro l hl + simp only [equityLines, List.mem_append] at hl + cases hl with + | inl h => exact closingLine_pos _ _ l h + | inr h => exact ih l h + +theorem equityLines_account (ts : List (Nat × Int)) : + ∀ l ∈ equityLines ts, ∃ x ∈ ts, l.account = x.1 := by + induction ts with + | nil => simp [equityLines] + | cons x ts ih => + obtain ⟨t, c⟩ := x + intro l hl + simp only [equityLines, List.mem_append] at hl + cases hl with + | inl h => exact ⟨(t, c), by simp, closingLine_account _ _ l h⟩ + | inr h => + obtain ⟨y, hy, e⟩ := ih l h + exact ⟨y, List.mem_cons_of_mem _ hy, e⟩ + +theorem equityLines_eq_nil (ts : List (Nat × Int)) (h : equityLines ts = []) : + total (ts.map Prod.snd) = 0 := by + induction ts with + | nil => rfl + | cons x ts ih => + obtain ⟨t, c⟩ := x + simp only [equityLines, List.append_eq_nil_iff] at h + simp only [List.map_cons, total, (closingLine_eq_nil _ _).1 h.1, ih h.2]; rfl + +/-- The closing entry: zero the closed accounts, credit the net to the +targets. -/ +def closingEntry (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) : List Line := + closings as ls ++ equityLines ts + +/-- **A closing entry balances** when the targets' parts sum to the net +of the closing lines (the net income), however that net was split. -/ +theorem closingEntry_net (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) + (hsum : total (ts.map Prod.snd) = net (closings as ls)) : + net (closingEntry as ts ls) = 0 := by + rw [closingEntry, net_append, net_equityLines, hsum]; omega + +/-- **A closing entry zeroes every account it closes.** -/ +theorem closingEntry_zeroes (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) + (hd : Distinct as) (b : Nat) (hb : b ∈ as) (ht : ∀ x ∈ ts, x.1 ≠ b) : + movement b (ls ++ closingEntry as ts ls) = 0 := by + rw [movement_append, closingEntry, movement_append, movement_closings b as ls hd, + movement_equityLines_absent b ts ht] + simp only [hb, ite_true]; omega + +/-- **A non-empty closing entry is acceptable**: two or more lines, every +amount positive, debits equal to credits. -/ +theorem closingEntry_accepted (as : List Nat) (ts : List (Nat × Int)) (ls : List Line) + (hsum : total (ts.map Prod.snd) = net (closings as ls)) (hne : closings as ls ≠ []) : + Accepted (closingEntry as ts ls) := by + refine ⟨?_, ?_, ?_⟩ + · rw [closingEntry, List.length_append] + match hc : closings as ls with + | [] => exact absurd hc hne + | [l] => + have hl : 0 < l.amount := closings_pos as ls l (by rw [hc]; simp) + have hnet : net (closings as ls) ≠ 0 := by + rw [hc]; obtain ⟨a, s, m⟩ := l + cases s <;> simp [Line.signed] at hl ⊢ <;> omega + have : equityLines ts ≠ [] := fun h => hnet (hsum ▸ equityLines_eq_nil ts h) + have : 1 ≤ (equityLines ts).length := by + cases h : equityLines ts with + | nil => exact absurd h this + | cons _ _ => simp + simp; omega + | _ :: _ :: _ => simp; omega + · intro l hl + simp only [closingEntry, List.mem_append] at hl + cases hl with + | inl h => exact closings_pos as ls l h + | inr h => exact equityLines_pos ts l h + · have := closingEntry_net as ts ls hsum + rw [net_eq_debits_sub_credits] at this; omega + +/-! ## Net income -/ + +/-- The chart's revenue and expense codes: what a close zeroes. -/ +def nominalCodes : Chart → List Nat + | [] => [] + | (a, t) :: c => if t = .revenue ∨ t = .expense then a :: nominalCodes c else nominalCodes c + +theorem nominalCodes_sub (c : Chart) : ∀ a ∈ nominalCodes c, a ∈ codes c := by + induction c with + | nil => simp [nominalCodes] + | cons x c ih => + obtain ⟨a, t⟩ := x + intro b hb + simp only [nominalCodes] at hb + split at hb + · cases hb with + | head => simp + | tail _ h => exact List.mem_cons_of_mem _ (ih b h) + · exact List.mem_cons_of_mem _ (ih b hb) + +theorem nominalCodes_distinct (c : Chart) (hd : Distinct (codes c)) : Distinct (nominalCodes c) := by + induction c with + | nil => trivial + | cons x c ih => + obtain ⟨a, t⟩ := x + obtain ⟨ha, hd⟩ := hd + simp only [nominalCodes] + split + · exact ⟨fun h => ha (nominalCodes_sub c a h), ih hd⟩ + · exact ih hd + +/-- **The net a close credits to equity is the period's net income**: +revenue balances minus expense balances. -/ +theorem net_closings_is_net_income (c : Chart) (ls : List Line) : + net (closings (nominalCodes c) ls) = typeTotal .revenue ls c - typeTotal .expense ls c := by + rw [net_closings] + induction c with + | nil => rfl + | cons x c ih => + obtain ⟨a, t⟩ := x + cases t <;> simp [nominalCodes, typeTotal, balance, AccountType.normal, signed] at ih ⊢ <;> omega + +/-! ## Splitting among members -/ + +/-- Make rounded parts sum to the whole: the last becomes the whole minus +the others (`kernel::plug_last`). -/ +def plugLast (whole : Int) : List Int → List Int + | [] => [] + | [_] => [whole] + | p :: q :: rest => p :: plugLast (whole - p) (q :: rest) + +/-- **An allocation's parts sum to the whole, exactly**, however the +other parts were rounded. -/ +theorem plugLast_total (whole : Int) (ps : List Int) (h : ps ≠ []) : + total (plugLast whole ps) = whole := by + induction ps generalizing whole with + | nil => exact absurd rfl h + | cons p rest ih => + match rest, ih with + | [], _ => show total [whole] = whole; simp [total] + | q :: rest, ih => + simp only [plugLast, total] + have := ih (whole - p) (by simp) + omega + +theorem plugLast_length (whole : Int) (ps : List Int) : (plugLast whole ps).length = ps.length := by + induction ps generalizing whole with + | nil => rfl + | cons p rest ih => + match rest, ih with + | [], _ => rfl + | q :: rest, ih => simp only [plugLast, List.length_cons]; rw [ih]; rfl + +/-- Only the last part changes. -/ +theorem plugLast_keeps (whole : Int) (ps : List Int) : + (plugLast whole ps).dropLast = ps.dropLast := by + induction ps generalizing whole with + | nil => rfl + | cons p rest ih => + match rest, ih with + | [], _ => rfl + | q :: rest, ih => + have hne : plugLast (whole - p) (q :: rest) ≠ [] := by + intro h + have := plugLast_length (whole - p) (q :: rest) + rw [h] at this; simp at this + rw [show plugLast whole (p :: q :: rest) = p :: plugLast (whole - p) (q :: rest) from rfl, + List.dropLast_cons_of_ne_nil hne, ih, List.dropLast_cons_cons] + +end Wanderbooks diff --git a/verify/lean/Wanderbooks/Entry.lean b/verify/lean/Wanderbooks/Entry.lean new file mode 100644 index 0000000..443056e --- /dev/null +++ b/verify/lean/Wanderbooks/Entry.lean @@ -0,0 +1,117 @@ +import Wanderbooks.Basic + +/-! +# Entries: acceptance, movements, reversals + +Mirrors `kernel::check_lines`, `kernel::movements`, `kernel::reversal`, +and `JournalEntry::validate`. +-/ + +namespace Wanderbooks + +/-- What the engine accepts (the arithmetic of `JournalEntry::validate`, +i.e. `kernel::check_lines`): two or more lines, every amount positive, +debits equal to credits. (Range, account, and currency checks are not +arithmetic laws and are left out of the model.) -/ +def Accepted (ls : List Line) : Prop := + 2 ≤ ls.length ∧ (∀ l ∈ ls, 0 < l.amount) ∧ debits ls = credits ls + +/-- **Every accepted entry nets to zero.** -/ +theorem Accepted.net_zero {ls : List Line} (h : Accepted ls) : net ls = 0 := by + rw [net_eq_debits_sub_credits]; have := h.2.2; omega + +/-- Net movement of account `a` over some lines. -/ +def movement (a : Nat) : List Line → Int + | [] => 0 + | l :: ls => (if l.account = a then l.signed else 0) + movement a ls + +@[simp] theorem movement_nil (a : Nat) : movement a [] = 0 := rfl +@[simp] theorem movement_cons (a : Nat) (l : Line) (ls : List Line) : + movement a (l :: ls) = (if l.account = a then l.signed else 0) + movement a ls := rfl + +theorem movement_append (a : Nat) (xs ys : List Line) : + movement a (xs ++ ys) = movement a xs + movement a ys := by + induction xs with + | nil => simp + | cons x xs ih => simp only [List.cons_append, movement_cons, ih]; omega + +/-- **Movements partition the net.** Summed over a chart's distinct codes +that cover every line's account, the per-account movements add up to the +net of the lines: grouping by account loses and invents nothing. -/ +theorem sum_movements (as : List Nat) (hd : Distinct as) : + ∀ ls : List Line, (∀ l ∈ ls, l.account ∈ as) → + sumOver (fun a => movement a ls) as = net ls := by + intro ls + induction ls with + | nil => intro _; simpa using sumOver_zero as + | cons l ls ih => + intro hcov + simp only [movement_cons, net_cons] + rw [sumOver_add, ih (fun m hm => hcov m (List.mem_cons_of_mem _ hm)), + sumOver_indicator l.account l.signed as hd (hcov l (List.mem_cons_self ..))] + +/-- So the movements of an accepted entry sum to zero. -/ +theorem Accepted.movements_sum_zero {ls : List Line} (h : Accepted ls) (as : List Nat) + (hd : Distinct as) (hcov : ∀ l ∈ ls, l.account ∈ as) : + sumOver (fun a => movement a ls) as = 0 := by + rw [sum_movements as hd ls hcov, h.net_zero] + +/-! ## Reversals -/ + +/-- A line with its side flipped. -/ +def Line.reverse (l : Line) : Line := { l with side := l.side.flip } + +/-- A reversing entry's lines (`kernel::reversal`). -/ +def reversal (ls : List Line) : List Line := ls.map Line.reverse + +theorem Line.reverse_signed (l : Line) : l.reverse.signed = -l.signed := by + simp [Line.reverse, Line.signed, signed_flip] + +theorem net_reversal (ls : List Line) : net (reversal ls) = -net ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [reversal, List.map_cons] at ih ⊢ + simp only [net_cons, ih, Line.reverse_signed]; omega + +theorem movement_reversal (a : Nat) (ls : List Line) : + movement a (reversal ls) = -movement a ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [reversal, List.map_cons] at ih ⊢ + simp only [movement_cons, ih, Line.reverse_signed] + by_cases h : l.account = a <;> simp [Line.reverse, h] <;> omega + +/-- **An entry and its reversal net every account to zero.** -/ +theorem movement_with_reversal (a : Nat) (ls : List Line) : + movement a (ls ++ reversal ls) = 0 := by + rw [movement_append, movement_reversal]; omega + +theorem debits_reversal (ls : List Line) : debits (reversal ls) = credits ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [reversal, List.map_cons] at ih ⊢ + obtain ⟨a, s, m⟩ := l + cases s <;> simp [debits, credits, Line.reverse, Side.flip, ih] + +theorem credits_reversal (ls : List Line) : credits (reversal ls) = debits ls := by + induction ls with + | nil => rfl + | cons l ls ih => + simp only [reversal, List.map_cons] at ih ⊢ + obtain ⟨a, s, m⟩ := l + cases s <;> simp [debits, credits, Line.reverse, Side.flip, ih] + +/-- **A reversal is accepted exactly when the original is.** -/ +theorem accepted_reversal_iff (ls : List Line) : Accepted (reversal ls) ↔ Accepted ls := by + unfold Accepted + rw [debits_reversal, credits_reversal] + have hlen : (reversal ls).length = ls.length := List.length_map .. + have hpos : (∀ l ∈ reversal ls, 0 < l.amount) ↔ (∀ l ∈ ls, 0 < l.amount) := by + simp [reversal, Line.reverse] + rw [hlen, hpos] + constructor <;> rintro ⟨a, b, c⟩ <;> exact ⟨a, b, c.symm⟩ + +end Wanderbooks diff --git a/verify/lean/Wanderbooks/Ledger.lean b/verify/lean/Wanderbooks/Ledger.lean new file mode 100644 index 0000000..a0d52ad --- /dev/null +++ b/verify/lean/Wanderbooks/Ledger.lean @@ -0,0 +1,446 @@ +import Wanderbooks.Closing + +/-! +# The ledger as a state machine + +The engine's command surface (`Ledger`), modelled as the steps it allows: +add an account, start a draft, post, reverse, open a period, close one. +Each step carries the checks the engine makes before it mutates. The +theorems below hold in *every* state reachable from empty books, by any +sequence of commands, of any length. + +Mirrors `Ledger::add_account`, `try_create_entry`, `post_entry`, +`reverse_entry`, `create_period`, and `close_period_to`. +-/ + +namespace Wanderbooks + +/-- A journal entry: its id, its date (a day number), its lines. -/ +structure Entry where + id : Nat + date : Nat + lines : List Line + deriving DecidableEq + +/-- Every line of some entries, in order. -/ +def allLines : List Entry → List Line + | [] => [] + | e :: es => e.lines ++ allLines es + +theorem allLines_append (xs ys : List Entry) : allLines (xs ++ ys) = allLines xs ++ allLines ys := by + induction xs with + | nil => rfl + | cons x xs ih => simp [allLines, ih] + +theorem mem_allLines {l : Line} {es : List Entry} : l ∈ allLines es ↔ ∃ e ∈ es, l ∈ e.lines := by + induction es with + | nil => simp [allLines] + | cons e es ih => simp [allLines, ih] + +/-- **Any collection of balanced entries nets to zero**: all of them, those +dated through some day, those in some period, any filter at all. -/ +theorem net_allLines (es : List Entry) (h : ∀ e ∈ es, net e.lines = 0) : net (allLines es) = 0 := by + induction es with + | nil => rfl + | cons e es ih => + simp only [allLines, net_append, h e (by simp), ih (fun x hx => h x (by simp [hx]))] + rfl + +/-- An accounting period: inclusive day range, open or closed. -/ +structure Period where + id : Nat + start : Nat + stop : Nat + closed : Bool + deriving DecidableEq + +/-- Whether a day falls in a period. -/ +def Period.contains (p : Period) (d : Nat) : Bool := decide (p.start ≤ d ∧ d ≤ p.stop) + +/-- The books: chart, posted entries in posting order, drafts, periods. -/ +structure Ledger where + chart : Chart + posted : List Entry + drafts : List Entry + periods : List Period + +/-- Empty books. -/ +def Ledger.empty : Ledger := ⟨[], [], [], []⟩ + +/-- Whether a closed period contains a day. -/ +def Ledger.closedOn (L : Ledger) (d : Nat) : Prop := + ∃ p ∈ L.periods, p.closed = true ∧ p.contains d = true + +/-- Entries dated on or before a day. -/ +def through (d : Nat) (es : List Entry) : List Entry := es.filter (fun e => decide (e.date ≤ d)) + +/-- Mark one period closed. -/ +def closeIn (p : Period) (ps : List Period) : List Period := + ps.map (fun q => if q = p then { q with closed := true } else q) + +/-- The closing entry for period `p` crediting targets `ts`, if there is +anything to close. -/ +def closingFor (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) : List Entry := + if closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) = [] then [] + else [⟨id, p.stop, closingEntry (nominalCodes L.chart) ts (allLines (through p.stop L.posted))⟩] + +/-- What the engine allows. -/ +inductive Step : Ledger → Ledger → Prop + /-- `add_account`: codes are unique. -/ + | addAccount (L : Ledger) (a : Nat) (t : AccountType) (h : a ∉ codes L.chart) : + Step L { L with chart := (a, t) :: L.chart } + /-- `try_create_entry` (and lines added to it): not in a closed period. -/ + | draft (L : Ledger) (e : Entry) (h : ¬ L.closedOn e.date) : + Step L { L with drafts := e :: L.drafts } + /-- `post_entry`: a draft, acceptable, on known accounts, not in a closed + period. Appends to the log. -/ + | post (L : Ledger) (e : Entry) (hd : e ∈ L.drafts) (ha : Accepted e.lines) + (hk : ∀ l ∈ e.lines, l.account ∈ codes L.chart) (hc : ¬ L.closedOn e.date) : + Step L { L with posted := L.posted ++ [e], drafts := L.drafts.filter (· ≠ e) } + /-- `reverse_entry`: a posted entry's lines, sides flipped, posted on a + day not in a closed period. -/ + | reverse (L : Ledger) (e : Entry) (he : e ∈ L.posted) (r : Entry) + (hr : r.lines = reversal e.lines) (hc : ¬ L.closedOn r.date) : + Step L { L with posted := L.posted ++ [r] } + /-- `create_period`: periods open. -/ + | openPeriod (L : Ledger) (p : Period) (h : p.closed = false) : + Step L { L with periods := p :: L.periods } + /-- `close_period_to`: an open period with no drafts in it, whose last day + is in no other closed period, with no later period closed, crediting the + net income to equity targets (not themselves revenue or expense) in + parts that sum to it. -/ + | close (L : Ledger) (p : Period) (hp : p ∈ L.periods) (hopen : p.closed = false) + (hdrafts : ∀ d ∈ L.drafts, p.contains d.date = false) + (hother : ∀ q ∈ L.periods, q.closed = true → q.contains p.stop = false) + (hlater : ∀ q ∈ L.periods, q.closed = true → q.stop ≤ p.stop) + (ts : List (Nat × Int)) + (hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart) + (hsum : total (ts.map Prod.snd) + = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted)))) + (id : Nat) : + Step L { L with posted := L.posted ++ closingFor L p ts id, periods := closeIn p L.periods } + +/-- States reachable from empty books. -/ +inductive Reachable : Ledger → Prop + | empty : Reachable Ledger.empty + | step {L L' : Ledger} : Reachable L → Step L L' → Reachable L' + +/-- What holds in every reachable state. -/ +structure Inv (L : Ledger) : Prop where + distinct : Distinct (codes L.chart) + accepted : ∀ e ∈ L.posted, Accepted e.lines + known : ∀ e ∈ L.posted, ∀ l ∈ e.lines, l.account ∈ codes L.chart + draftsOpen : ∀ d ∈ L.drafts, ¬ L.closedOn d.date + +theorem closedOn_closeIn (L : Ledger) (p : Period) (d : Nat) : + ({ L with periods := closeIn p L.periods } : Ledger).closedOn d → + L.closedOn d ∨ (p ∈ L.periods ∧ p.contains d = true) := by + rintro ⟨q, hq, hc, hd⟩ + simp only [closeIn, List.mem_map] at hq + obtain ⟨q', hq', rfl⟩ := hq + by_cases e : q' = p + · subst e; right; simp at hd; exact ⟨hq', by simpa [Period.contains] using hd⟩ + · left; simp [e] at hc hd; exact ⟨q', hq', hc, hd⟩ + +theorem closingFor_lines (L : Ledger) (p : Period) (ts : List (Nat × Int)) (id : Nat) : + ∀ e ∈ closingFor L p ts id, + e.date = p.stop ∧ e.lines = closingEntry (nominalCodes L.chart) ts + (allLines (through p.stop L.posted)) + ∧ closings (nominalCodes L.chart) (allLines (through p.stop L.posted)) ≠ [] := by + intro e he + unfold closingFor at he + split at he + · simp at he + · simp at he; subst he; exact ⟨rfl, rfl, by assumption⟩ + +/-- **Every step preserves the invariant.** -/ +theorem Step.inv {L L' : Ledger} (s : Step L L') (h : Inv L) : Inv L' := by + cases s with + | addAccount a t ha => + exact ⟨⟨ha, h.distinct⟩, h.accepted, + fun e he l hl => List.mem_cons_of_mem _ (h.known e he l hl), h.draftsOpen⟩ + | draft e hc => + refine ⟨h.distinct, h.accepted, h.known, ?_⟩ + intro d hd + cases hd with + | head => exact hc + | tail _ hd => exact h.draftsOpen d hd + | post e hd ha hk hc => + refine ⟨h.distinct, ?_, ?_, ?_⟩ + · intro x hx + simp only [List.mem_append, List.mem_singleton] at hx + rcases hx with hx | rfl + · exact h.accepted x hx + · exact ha + · intro x hx + simp only [List.mem_append, List.mem_singleton] at hx + rcases hx with hx | rfl + · exact h.known x hx + · exact hk + · intro d hd + exact h.draftsOpen d ((List.mem_filter.1 hd).1) + | reverse e he r hr hc => + refine ⟨h.distinct, ?_, ?_, h.draftsOpen⟩ + · intro x hx + simp only [List.mem_append, List.mem_singleton] at hx + rcases hx with hx | rfl + · exact h.accepted x hx + · rw [hr, accepted_reversal_iff]; exact h.accepted e he + · intro x hx + simp only [List.mem_append, List.mem_singleton] at hx + rcases hx with hx | rfl + · exact h.known x hx + · intro l hl + rw [hr] at hl + simp only [reversal, List.mem_map] at hl + obtain ⟨l', hl', rfl⟩ := hl + exact h.known e he l' hl' + | openPeriod p hp => + refine ⟨h.distinct, h.accepted, h.known, ?_⟩ + rintro d hd ⟨q, hq, hc, hdq⟩ + cases hq with + | head => simp [hp] at hc + | tail _ hq => exact h.draftsOpen d hd ⟨q, hq, hc, hdq⟩ + | close p hp hopen hdrafts hother hlater ts hts hsum id => + refine ⟨h.distinct, ?_, ?_, ?_⟩ + · intro x hx + simp only [List.mem_append] at hx + rcases hx with hx | hx + · exact h.accepted x hx + · obtain ⟨-, hl, hne⟩ := closingFor_lines L p ts id x hx + rw [hl]; exact closingEntry_accepted _ _ _ hsum hne + · intro x hx + simp only [List.mem_append] at hx + rcases hx with hx | hx + · exact h.known x hx + · obtain ⟨-, hl, -⟩ := closingFor_lines L p ts id x hx + intro l hl' + rw [hl] at hl' + simp only [closingEntry, List.mem_append] at hl' + rcases hl' with hl' | hl' + · exact nominalCodes_sub _ _ (closings_account _ _ l hl') + · obtain ⟨y, hy, e⟩ := equityLines_account ts l hl' + rw [e]; exact (hts y hy).1 + · intro d hd hcl + rcases closedOn_closeIn L p d.date hcl with hcl | ⟨-, hc⟩ + · exact h.draftsOpen d hd hcl + · simp [hdrafts d hd] at hc + +/-- **The invariant holds in every reachable state.** -/ +theorem Reachable.inv {L : Ledger} (r : Reachable L) : Inv L := by + induction r with + | empty => exact ⟨trivial, by simp [Ledger.empty], by simp [Ledger.empty], by simp [Ledger.empty]⟩ + | step _ s ih => exact s.inv ih + +/-! ## The books always balance -/ + +/-- **The books net to zero**: in every reachable state, the posted lines' +debits equal their credits. -/ +theorem Reachable.books_net_zero {L : Ledger} (r : Reachable L) : net (allLines L.posted) = 0 := + net_allLines _ (fun e he => (r.inv.accepted e he).net_zero) + +/-- The same through any day: the books as of any date balance too. -/ +theorem Reachable.net_zero_through {L : Ledger} (r : Reachable L) (d : Nat) : + net (allLines (through d L.posted)) = 0 := + net_allLines _ (fun e he => (r.inv.accepted e ((List.mem_filter.1 he).1)).net_zero) + +theorem Reachable.covers {L : Ledger} (r : Reachable L) (es : List Entry) + (hs : ∀ e ∈ es, e ∈ L.posted) : ∀ l ∈ allLines es, l.account ∈ codes L.chart := by + intro l hl + obtain ⟨e, he, hl⟩ := mem_allLines.1 hl + exact r.inv.known e (hs e he) l hl + +/-- **The trial balance balances**, in every reachable state. -/ +theorem Reachable.trial_balance {L : Ledger} (r : Reachable L) : + tbDebits (allLines L.posted) (codes L.chart) = tbCredits (allLines L.posted) (codes L.chart) := + trial_balance_balances _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero + +/-- **The trial balance as of any date balances.** -/ +theorem Reachable.trial_balance_through {L : Ledger} (r : Reachable L) (d : Nat) : + tbDebits (allLines (through d L.posted)) (codes L.chart) + = tbCredits (allLines (through d L.posted)) (codes L.chart) := + trial_balance_balances _ _ r.inv.distinct + (r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d) + +/-- **The accounting equation holds**, in every reachable state: +Assets = Liabilities + Equity + (Revenue - Expenses). -/ +theorem Reachable.accounting_equation {L : Ledger} (r : Reachable L) : + let ls := allLines L.posted + typeTotal .asset ls L.chart + = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart + + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) := + Wanderbooks.accounting_equation _ _ r.inv.distinct (r.covers _ (fun _ h => h)) r.books_net_zero + +/-- **The balance sheet as of any date balances.** -/ +theorem Reachable.accounting_equation_through {L : Ledger} (r : Reachable L) (d : Nat) : + let ls := allLines (through d L.posted) + typeTotal .asset ls L.chart + = typeTotal .liability ls L.chart + typeTotal .equity ls L.chart + + (typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart) := + Wanderbooks.accounting_equation _ _ r.inv.distinct + (r.covers _ (fun _ h => (List.mem_filter.1 h).1)) (r.net_zero_through d) + +/-! ## Posted is forever -/ + +/-- **Posting only appends.** No step edits, reorders, or removes a posted +entry. -/ +theorem Step.extends {L L' : Ledger} (s : Step L L') : ∃ t, L'.posted = L.posted ++ t := by + cases s with + | addAccount => exact ⟨[], by simp⟩ + | draft => exact ⟨[], by simp⟩ + | post e => exact ⟨[e], rfl⟩ + | reverse e _ r => exact ⟨[r], rfl⟩ + | openPeriod => exact ⟨[], by simp⟩ + | close p _ _ _ _ _ ts _ _ id => exact ⟨closingFor L p ts id, rfl⟩ + +/-- Any number of steps. -/ +inductive Steps : Ledger → Ledger → Prop + | refl (L : Ledger) : Steps L L + | tail {L M N : Ledger} : Steps L M → Step M N → Steps L N + +/-- **Posted is forever**: after any sequence of commands, the old log is +a prefix of the new one. Every posted entry keeps its place and its +lines. -/ +theorem Steps.extends {L L' : Ledger} (s : Steps L L') : ∃ t, L'.posted = L.posted ++ t := by + induction s with + | refl => exact ⟨[], by simp⟩ + | tail _ s ih => + obtain ⟨t, ht⟩ := ih + obtain ⟨u, hu⟩ := s.extends + exact ⟨t ++ u, by rw [hu, ht, List.append_assoc]⟩ + +/-! ## Closed periods are frozen -/ + +/-- Entries dated in a period. -/ +def within (p : Period) (es : List Entry) : List Entry := es.filter (fun e => p.contains e.date) + +theorem within_append (p : Period) (xs ys : List Entry) : + within p (xs ++ ys) = within p xs ++ within p ys := List.filter_append .. + +/-- A closed period stays closed. -/ +theorem Step.keeps_closed {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods) + (hc : q.closed = true) : q ∈ L'.periods := by + cases s with + | openPeriod p _ => exact List.mem_cons_of_mem _ hq + | close p _ hopen => + have : q ≠ p := fun e => by subst e; simp [hopen] at hc + exact List.mem_map.2 ⟨q, hq, by simp [this]⟩ + | _ => exact hq + +/-- **A step never changes what a closed period contains.** -/ +theorem Step.frozen {L L' : Ledger} (s : Step L L') (q : Period) (hq : q ∈ L.periods) + (hc : q.closed = true) : within q L'.posted = within q L.posted := by + have nothing : ∀ e : Entry, ¬ L.closedOn e.date → within q [e] = [] := by + intro e he + simp only [within, List.filter_cons, List.filter_nil] + split + · exact absurd ⟨q, hq, hc, by assumption⟩ he + · rfl + cases s with + | post e _ _ _ hcl => rw [within_append, nothing e hcl, List.append_nil] + | reverse e _ r _ hcl => rw [within_append, nothing r hcl, List.append_nil] + | close p hp hopen hdrafts hother hlater ts hts hsum id => + rw [within_append] + have : within q (closingFor L p ts id) = [] := by + unfold closingFor + split + · rfl + · simp only [within, List.filter_cons, List.filter_nil] + rw [hother q hq hc]; rfl + rw [this, List.append_nil] + | _ => rfl + +/-- **Closed periods are frozen**: once a period is closed, no sequence of +commands adds, removes, or changes an entry dated in it. -/ +theorem Steps.frozen {L L' : Ledger} (s : Steps L L') (q : Period) (hq : q ∈ L.periods) + (hc : q.closed = true) : within q L'.posted = within q L.posted ∧ q ∈ L'.periods := by + induction s with + | refl => exact ⟨rfl, hq⟩ + | tail _ s ih => + obtain ⟨h1, h2⟩ := ih + exact ⟨(s.frozen q h2 hc).trans h1, s.keeps_closed q h2 hc⟩ + +/-! ## Closing -/ + +/-- **After a close, every revenue and expense account is zero through the +period's last day.** (The trial balance still balances: the close is a +step, and `Reachable.trial_balance` covers every step.) -/ +theorem close_zeroes {L : Ledger} (r : Reachable L) (p : Period) + (ts : List (Nat × Int)) (hts : ∀ x ∈ ts, x.1 ∈ codes L.chart ∧ x.1 ∉ nominalCodes L.chart) + (id : Nat) (a : Nat) (ha : a ∈ nominalCodes L.chart) : + movement a (allLines (through p.stop (L.posted ++ closingFor L p ts id))) = 0 := by + have hd := nominalCodes_distinct _ r.inv.distinct + have hta : ∀ x ∈ ts, x.1 ≠ a := fun x hx e => (hts x hx).2 (e ▸ ha) + rw [through, List.filter_append, ← through, allLines_append] + unfold closingFor + split + · rename_i hnil + simp only [List.filter_nil, allLines, List.append_nil] + exact closings_eq_nil _ _ hnil a ha + · simp only [List.filter_cons, Nat.le_refl, decide_true, ite_true, List.filter_nil, allLines, + List.append_nil] + exact closingEntry_zeroes _ ts _ hd a ha hta + +/-- **A close credits equity with exactly the period's net income**: +revenue minus expenses through its last day, split among the targets. -/ +theorem close_credits_net_income (L : Ledger) (p : Period) (ts : List (Nat × Int)) + (hsum : total (ts.map Prod.snd) + = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted)))) : + let ls := allLines (through p.stop L.posted) + total (ts.map Prod.snd) = typeTotal .revenue ls L.chart - typeTotal .expense ls L.chart := by + intro ls + rw [hsum, net_closings_is_net_income] + +/-! ## Period statements add up -/ + +/-- Entries dated after day `b`, through day `c`. -/ +def between (b c : Nat) (es : List Entry) : List Entry := + es.filter (fun e => decide (b < e.date ∧ e.date ≤ c)) + +theorem movement_split (a b c : Nat) (h : b ≤ c) (es : List Entry) : + movement a (allLines (through c es)) + = movement a (allLines (through b es)) + movement a (allLines (between b c es)) := by + induction es with + | nil => rfl + | cons e es ih => + simp only [through, between] at ih ⊢ + by_cases h1 : e.date ≤ b + · have h2 : e.date ≤ c := by omega + have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega + rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_pos (by simpa using h1), + List.filter_cons_of_neg (by simpa using h3)] + simp only [allLines, movement_append, ih]; omega + · by_cases h2 : e.date ≤ c + · have h3 : b < e.date ∧ e.date ≤ c := by omega + rw [List.filter_cons_of_pos (by simpa using h2), List.filter_cons_of_neg (by simpa using h1), + List.filter_cons_of_pos (by simpa using h3)] + simp only [allLines, movement_append, ih]; omega + · have h3 : ¬ (b < e.date ∧ e.date ≤ c) := by omega + rw [List.filter_cons_of_neg (by simpa using h2), List.filter_cons_of_neg (by simpa using h1), + List.filter_cons_of_neg (by simpa using h3)] + exact ih + +theorem typeTotal_split (t : AccountType) (x y z : List Line) + (h : ∀ a, movement a x = movement a y + movement a z) (c : Chart) : + typeTotal t x c = typeTotal t y c + typeTotal t z c := by + induction c with + | nil => rfl + | cons p c ih => + obtain ⟨a, t'⟩ := p + simp only [typeTotal, h a, ih] + split + · cases t' <;> simp [balance, AccountType.normal, signed] <;> omega + · omega + +/-- **Period statements add up**: every account type's total (so revenue, +expenses, and net income) through day `c` is its total through day `b` +plus its total for the days after `b` through `c`. A year's P&L is the sum +of its months'. -/ +theorem statements_add_up (t : AccountType) (b c : Nat) (h : b ≤ c) (es : List Entry) + (chart : Chart) : + typeTotal t (allLines (through c es)) chart + = typeTotal t (allLines (through b es)) chart + + typeTotal t (allLines (between b c es)) chart := + typeTotal_split t _ _ _ (fun a => movement_split a b c h es) chart + +end Wanderbooks diff --git a/verify/lean/Wanderbooks/Statements.lean b/verify/lean/Wanderbooks/Statements.lean new file mode 100644 index 0000000..bd50e4c --- /dev/null +++ b/verify/lean/Wanderbooks/Statements.lean @@ -0,0 +1,104 @@ +import Wanderbooks.Entry + +/-! +# Balances and statements + +Mirrors `kernel::normal_balance`, `kernel::columns`, +`Ledger::account_balance`, and `reports::trial_balance`. +-/ + +namespace Wanderbooks + +/-- A chart of accounts: each account's code and type. -/ +abbrev Chart := List (Nat × AccountType) + +/-- The chart's codes. -/ +def codes (c : Chart) : List Nat := c.map Prod.fst + +@[simp] theorem codes_nil : codes [] = [] := rfl +@[simp] theorem codes_cons (a : Nat) (t : AccountType) (c : Chart) : + codes ((a, t) :: c) = a :: codes c := rfl + +/-- An account's balance on its normal side (`kernel::normal_balance`). -/ +def balance (t : AccountType) (m : Int) : Int := signed t.normal m + +/-- **A normal-side line raises a balance by its amount; an opposite-side +line lowers it.** -/ +theorem balance_after_line (t : AccountType) (m : Int) (s : Side) (a : Int) : + balance t (m + signed s a) = balance t m + (if s = t.normal then a else -a) := by + cases t <;> cases s <;> simp [balance, AccountType.normal, signed] <;> omega + +/-- The total balance of every account of type `t`. -/ +def typeTotal (t : AccountType) (ls : List Line) : Chart → Int + | [] => 0 + | (a, t') :: rest => (if t' = t then balance t' (movement a ls) else 0) + typeTotal t ls rest + +/-- The accounting equation's two sides differ by the net movement of the +chart's accounts. -/ +theorem equation_gap (ls : List Line) (c : Chart) : + typeTotal .asset ls c + typeTotal .expense ls c + - typeTotal .liability ls c - typeTotal .equity ls c - typeTotal .revenue ls c + = sumOver (fun a => movement a ls) (codes c) := by + induction c with + | nil => rfl + | cons x c ih => + obtain ⟨a, t⟩ := x + cases t <;> simp [typeTotal, balance, AccountType.normal, signed] <;> omega + +/-- **The accounting equation.** For lines that net to zero, over a chart +with distinct codes covering every line's account: +Assets = Liabilities + Equity + (Revenue - Expenses). -/ +theorem accounting_equation (ls : List Line) (c : Chart) (hd : Distinct (codes c)) + (hcov : ∀ l ∈ ls, l.account ∈ codes c) (hnet : net ls = 0) : + typeTotal .asset ls c + = typeTotal .liability ls c + typeTotal .equity ls c + + (typeTotal .revenue ls c - typeTotal .expense ls c) := by + have := equation_gap ls c + rw [sum_movements _ hd ls hcov, hnet] at this + omega + +/-! ## Trial balance -/ + +/-- The debit column for a movement (`kernel::columns`). -/ +def colDebit (m : Int) : Int := if 0 < m then m else 0 +/-- The credit column for a movement (`kernel::columns`). -/ +def colCredit (m : Int) : Int := if 0 < m then 0 else -m + +theorem columns_spec (m : Int) : + 0 ≤ colDebit m ∧ 0 ≤ colCredit m ∧ (colDebit m = 0 ∨ colCredit m = 0) + ∧ colDebit m - colCredit m = m := by + unfold colDebit colCredit; split <;> omega + +/-- The trial balance's debit column total. -/ +def tbDebits (ls : List Line) (as : List Nat) : Int := sumOver (fun a => colDebit (movement a ls)) as +/-- The trial balance's credit column total. -/ +def tbCredits (ls : List Line) (as : List Nat) : Int := + sumOver (fun a => colCredit (movement a ls)) as + +theorem tb_gap (ls : List Line) (as : List Nat) : + tbDebits ls as - tbCredits ls as = sumOver (fun a => movement a ls) as := by + induction as with + | nil => rfl + | cons a as ih => + simp only [tbDebits, tbCredits, sumOver_cons] at ih ⊢ + have := (columns_spec (movement a ls)).2.2.2 + omega + +/-- **The trial balance balances** for lines that net to zero. -/ +theorem trial_balance_balances (ls : List Line) (as : List Nat) (hd : Distinct as) + (hcov : ∀ l ∈ ls, l.account ∈ as) (hnet : net ls = 0) : + tbDebits ls as = tbCredits ls as := by + have := tb_gap ls as + rw [sum_movements as hd ls hcov, hnet] at this + omega + +/-- And conversely: a balanced trial balance means the lines net to zero. +The trial balance is a complete check of the books' arithmetic. -/ +theorem trial_balance_iff (ls : List Line) (as : List Nat) (hd : Distinct as) + (hcov : ∀ l ∈ ls, l.account ∈ as) : + tbDebits ls as = tbCredits ls as ↔ net ls = 0 := by + have := tb_gap ls as + rw [sum_movements as hd ls hcov] at this + omega + +end Wanderbooks diff --git a/verify/lean/lake-manifest.json b/verify/lean/lake-manifest.json new file mode 100644 index 0000000..8b04555 --- /dev/null +++ b/verify/lean/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "wanderbooks", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/verify/lean/lakefile.toml b/verify/lean/lakefile.toml new file mode 100644 index 0000000..d89b232 --- /dev/null +++ b/verify/lean/lakefile.toml @@ -0,0 +1,5 @@ +name = "wanderbooks" +defaultTargets = ["Wanderbooks"] + +[[lean_lib]] +name = "Wanderbooks" diff --git a/verify/lean/lean-toolchain b/verify/lean/lean-toolchain new file mode 100644 index 0000000..ba8ebf2 --- /dev/null +++ b/verify/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.1