Compare commits
2
Commits
bea2ee2dc2
...
3609bf065e
| Author | SHA1 | Date | |
|---|---|---|---|
  swaitsandClaude Opus 5.5
|
3609bf065e | ||
|
swaitsandClaude Opus 5.5
|
d5c4e38b18 |
No files matched your search
@@ -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 |
|
||||
|
||||
@@ -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)"] }
|
||||
@@ -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
|
||||
|
||||
```
|
||||
|
||||
@@ -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),
|
||||
|
||||
@@ -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<Currency> = 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<AccountId, Decimal> {
|
||||
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()
|
||||
}
|
||||
}
|
||||
@@ -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>;
|
||||
/// `-self`, or `None` when it cannot be represented.
|
||||
fn checked_neg(self) -> Option<Self>;
|
||||
/// 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> {
|
||||
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<Self> {
|
||||
Decimal::checked_add(self, rhs)
|
||||
}
|
||||
fn checked_neg(self) -> Option<Self> {
|
||||
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<Self> {
|
||||
i64::checked_add(self, rhs)
|
||||
}
|
||||
fn checked_neg(self) -> Option<Self> {
|
||||
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<T> {
|
||||
/// 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<T: Amount>(side: Side, amount: T) -> Option<T> {
|
||||
match side {
|
||||
Side::Debit => Some(amount),
|
||||
Side::Credit => amount.checked_neg(),
|
||||
}
|
||||
}
|
||||
|
||||
/// Total debits and total credits of some lines.
|
||||
pub fn totals<T: Amount>(lines: impl IntoIterator<Item = (Side, T)>) -> 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<T: Amount>(lines: impl IntoIterator<Item = (Side, T)>) -> Option<T> {
|
||||
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<T: Amount>(lines: &[(Side, T)]) -> Result<(), LineError<T>> {
|
||||
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<K: Copy + Eq, T: Amount>(
|
||||
lines: impl IntoIterator<Item = (K, Side, T)>,
|
||||
) -> Option<Vec<(K, T)>> {
|
||||
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<K: Copy + Eq, T: Amount>(
|
||||
lines: &[(K, Side, T)],
|
||||
out: &mut [(K, T)],
|
||||
) -> Option<usize> {
|
||||
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<K: Copy, T: Amount>(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<K, T: Amount>((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<T: Amount>(account_type: AccountType, movement: T) -> Option<T> {
|
||||
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<T: Amount>(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<T: Amount>(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<T: Amount>(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<T: Amount>(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::<Decimal>().unwrap().in_line_range());
|
||||
assert!(!"0.00000000001".parse::<Decimal>().unwrap().in_line_range());
|
||||
// Trailing zeros are not precision.
|
||||
assert!("1.000000000000".parse::<Decimal>().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);
|
||||
}
|
||||
}
|
||||
@@ -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() {
|
||||
|
||||
@@ -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;
|
||||
|
||||
@@ -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::<rust_decimal::Decimal>();
|
||||
}
|
||||
crate::kernel::plug_last(amount, &mut parts).expect("allocated amounts are in range");
|
||||
parts
|
||||
}
|
||||
|
||||
|
||||
@@ -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]);
|
||||
}
|
||||
}
|
||||
@@ -59,10 +59,8 @@ fn trial_balance_where(ledger: &Ledger, include: &dyn Fn(&JournalEntry) -> bool)
|
||||
let mut movements: BTreeMap<crate::AccountId, Decimal> = 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 {
|
||||
|
||||
@@ -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();
|
||||
|
||||
@@ -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<Value = Side> {
|
||||
prop_oneof![Just(Side::Debit), Just(Side::Credit)]
|
||||
}
|
||||
|
||||
fn arb_type() -> impl Strategy<Value = AccountType> {
|
||||
prop_oneof![
|
||||
Just(AccountType::Asset),
|
||||
Just(AccountType::Liability),
|
||||
Just(AccountType::Equity),
|
||||
Just(AccountType::Revenue),
|
||||
Just(AccountType::Expense),
|
||||
]
|
||||
}
|
||||
|
||||
fn arb_cents() -> impl Strategy<Value = i64> {
|
||||
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<Value = Vec<(u8, Side, i64)>> {
|
||||
(
|
||||
prop::collection::vec((0u8..4, arb_side(), arb_cents()), 0..7),
|
||||
any::<bool>(),
|
||||
)
|
||||
.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<T: Copy>(lines: &[(u8, Side, T)]) -> Vec<(Side, T)> {
|
||||
lines.iter().map(|&(_, s, a)| (s, a)).collect()
|
||||
}
|
||||
|
||||
fn map_err(e: LineError<i64>) -> LineError<Decimal> {
|
||||
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<Decimal> = 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::<Vec<_>>(), pd);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn line_range_agrees(cents in arb_cents()) {
|
||||
prop_assert_eq!(cents.in_line_range(), dec(cents).in_line_range());
|
||||
}
|
||||
}
|
||||
@@ -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)
|
||||
|
||||
+41
-11
@@ -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)
|
||||
|
||||
|
||||
+2
-2
@@ -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.
|
||||
|
||||
@@ -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.
|
||||
@@ -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
|
||||
|
||||
@@ -0,0 +1,18 @@
|
||||
# Everything needed to build, test, prove, and ship wanderbooks.
|
||||
# `mise install` in this directory, then `just` lists the recipes.
|
||||
|
||||
[tools]
|
||||
# Workspace toolchain (clippy and rustfmt for `just check`).
|
||||
rust = { version = "1.99", components = "clippy,rustfmt" }
|
||||
just = "1"
|
||||
# `just deploy` runs the Netlify CLI through npx.
|
||||
node = "26"
|
||||
# `just prove`: Kani model-checks the accounting kernel. Kani fetches its
|
||||
# own pinned nightly and CBMC under ~/.kani on first run.
|
||||
"cargo:kani-verifier" = "0.68.0"
|
||||
# `just prove`: Lean proves the accounting laws (verify/lean). Matches
|
||||
# verify/lean/lean-toolchain.
|
||||
"github:leanprover/lean4" = "4.34.1"
|
||||
# Mutation testing and fuzzing (docs/oracle.md).
|
||||
"cargo:cargo-mutants" = "latest"
|
||||
"cargo:cargo-fuzz" = "latest"
|
||||
+20
-3
@@ -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
|
||||
|
||||
+6
-3
@@ -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
|
||||
|
||||
@@ -0,0 +1 @@
|
||||
.lake/
|
||||
@@ -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
|
||||
@@ -0,0 +1,5 @@
|
||||
import Wanderbooks.Basic
|
||||
import Wanderbooks.Entry
|
||||
import Wanderbooks.Statements
|
||||
import Wanderbooks.Closing
|
||||
import Wanderbooks.Ledger
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -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
|
||||
@@ -0,0 +1,6 @@
|
||||
{"version": "1.3.0",
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages": [],
|
||||
"name": "wanderbooks",
|
||||
"lakeDir": ".lake",
|
||||
"fixedToolchain": false}
|
||||
@@ -0,0 +1,5 @@
|
||||
name = "wanderbooks"
|
||||
defaultTargets = ["Wanderbooks"]
|
||||
|
||||
[[lean_lib]]
|
||||
name = "Wanderbooks"
|
||||
@@ -0,0 +1 @@
|
||||
leanprover/lean4:v4.34.1
|
||||
Reference in new issue
Block a user