swaitsandClaude Opus 5.5
3609bf065e
The money arithmetic every invariant rests on now lives in one kernel,
ledger-core/src/kernel.rs: signing a line, totals, net, per-account
movements, reversal, normal balances, trial-balance columns, closing
lines, and the rounding plug for member splits. It is generic over a
checked `Amount` trait. The engine runs it on Decimal (validate,
movements, reverse_entry, account_balance, close_period_to, allocate,
trial_balance): there is one copy of the arithmetic, and it is the one
under proof.
Three layers, docs/verification.md maps every law to its proofs:
- Kani (src/proofs.rs): 17 harnesses prove the kernel at i64 for every
input up to 4 lines over 3 accounts. An entry is accepted exactly
when it is two or more positive, in-range lines whose debits equal
credits; accepted entries net to zero; grouping by account loses
nothing; a reversal mirrors and cancels its original; trial-balance
columns balance iff the books net to zero; closing lines zero their
accounts and a close balances however the net is split; the plug
makes parts sum to the whole. No panics, no overflow. kani::cover!
shows the proofs are not vacuous.
- Lean 4 (verify/lean): 24 headline theorems for books of any size. The
ledger is a state machine (add account, draft, post, reverse, open,
close), and in every reachable state the books net to zero, the trial
balance balances (as of any date), and the accounting equation holds.
Posting only appends ("posted is forever"), closed periods are
frozen, a close zeroes revenue and expenses and credits exactly the net
income, and period statements add up. Audit.lean shows standard axioms
only, no sorry.
- Bridge (tests/kernel_bridge.rs): the Decimal and i64 kernels agree.
What the proofs found (each one missed by every test, fuzzer, and
mutant):
- The engine accepted negative line amounts; only MCP refused them. Now
NegativeAmountLine: direction is the side's job.
- Summing lines near Decimal::MAX panicked. Lines are now capped at one
quadrillion and ten decimal places (AmountOutOfRange), which keeps
every realistic sum exact, and the kernel's sums are checked.
- FX conversion (foreign_amount * fx_rate) could panic the same way; it
is now a checked multiply.
- Kani itself: 0.68 mis-models symbolic-length copy_from_slice
(model-checking/kani#4904) and reported a reversal that doesn't net to
zero. The counterexample, replayed natively, passes, and a 15-line
standalone crate reproduces the bug. Harnesses avoid bulk copies, and
a should_panic canary will flag the upstream fix.
`just prove` runs it all (Kani memory- and time-capped, fails on an
unsatisfiable cover or a non-standard Lean axiom). AGENTS.md now makes
formal coverage part of every core change.
Also, docs: GnuCash is *an* oracle, never *the* oracle (Stephen). The
spec is accounting principles, proved. Golden files are recomputed from
principles. External implementations (GnuCash, the old Sheet, QBO/Xero)
are cross-checks whose disagreements get adjudicated, never obeyed.
docs/oracle.md gains "Who is right"; AGENTS, README, architecture,
roadmap, parity, and STATUS are reworded to match.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX
3.7 KiB
Architecture
The one big idea: engine-first, everything is a command
ledger-core owns all accounting knowledge. Every state change is a method
on Ledger:
add_account— extend the chart of accountscreate_entry/add_line— build a draft journal entrypost_entry— validate and apply (one-way)reverse_entry— correct via reversal (one-way)
Each command validates before it applies, and each failure is a typed
LedgerError variant. There is no other mutation path: struct fields are
private, and constructors are pub(crate) where it matters. This is what
makes the ledger auditable and what will make the future oracle harness
trustworthy — the harness only needs to drive the command surface.
Reports (trial_balance, balance_sheet, profit_and_loss, snapshot)
are free functions: pure, total, and deterministic. Same ledger in, same
report out, every time, on every platform. That determinism is the entire
basis of docs/oracle.md.
Current crate layout
crates/ledger-core/
src/
lib.rs # crate docs, re-exports, design rules
money.rs # Currency + Money (Decimal, checked arithmetic)
account.rs # AccountType, Side, Account, ChartOfAccounts
journal.rs # JournalLine, JournalEntry, validate()
ledger.rs # Ledger: the command surface, append-only log
reports.rs # trial_balance, profit_and_loss, balance_sheet, snapshot
tests/
invariants.rs # accounting-law tests + randomized property test
golden/ # hand-verified expected report snapshots
Dependency rules
ledger-core may depend only on:
rust_decimal— exact decimal arithmeticthiserror— the error typechrono— dates (NaiveDate; no wall-clock reads in the core)serde/serde_json— the oracle interchange format
New dependencies need justification in the commit message. In particular: no I/O, no networking, no async runtime, no logging framework in the core. The core is a pure domain library and stays that way.
Future crates (do not create until the roadmap says so)
| Crate | Purpose | Depends on |
|---|---|---|
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 |
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)
never leak into the core; the core speaks Decimal and ISO codes.
Why Rust
Exact decimal semantics, exhaustive pattern matching on the five account types, and a type system that makes invalid states (mutable posted entries, float money) unrepresentable. The storytold pipeline this project is modeled on is Rust + egui for the same reasons; when the UI crate arrives it will be one codebase compiling to native and WASM.
The GUI (ledger-gui)
Read-only by construction: it opens a ledger_store::Snapshot (journal
verified and replayed into its own Ledger, projected into a private
in-memory SQLite, blobs read through the verifying store) and never writes
to the data directory. A loader thread watches the directory and applies
appended journal lines; the UI renders an immutable view model rebuilt per
change. Statements and series come from ledger-core (reports,
analysis); the GUI only arranges them. See plan/gui.md.