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
4.8 KiB
4.8 KiB
Parity catalog
Every semantic feature we intend to clone, with its status. Updated in the
same commit as the feature. The floor never decreases: the count of
done items is monotonic across commits.
Statuses: done = implemented + invariant-tested + golden-covered.
partial = implemented but missing tests or goldens. todo = not started.
No other statuses.
Floor: 10 done (2026-10-10; fixed-asset register added).
| 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 |
| Exact decimal money, no floats | — (we go further) | done | money.rs; Currency ISO codes |
| Posted-entry immutability | Read-only posted txns | done | reversal via reverse_entry |
| Trial balance | Reports → Trial Balance | done | golden-covered |
| Balance sheet (A = L + E) | Reports → Balance Sheet | done | current earnings folded in pre-close; golden-covered |
| Profit & loss | Reports → Income Statement | done | golden-covered |
| P&L for a date range, line per account (closing entries excluded) | Reports → Income Statement (custom dates) | partial | hand-verified fixture + property tests; no golden file yet |
| Balance sheet as of a date, line per account | Reports → Balance Sheet (as of) | partial | hand-verified fixture + property tests; no golden file yet |
| General ledger by account (running balance, split) | Reports → General Ledger | partial | hand-verified fixture, ties to trial balance; no golden file yet |
| Trial balance as of a date | Reports → Trial Balance (as of) | partial | hand-verified fixture; no golden file yet |
| Statement of changes in members' equity | Reports → Statement of Changes in Equity | partial | hand-verified two-member fixture incl. rounding and a close; no golden file yet |
| Tax line mapping + tax summary | Accounts → Tax line mapping; Tax reports | partial | hand-verified fixture (50% meals, nondeductible, contra income); no golden file yet |
| Reversing entries | Reverse transaction | done | linked via reversal_of |
| Canonical report snapshots (JSON) | — (our oracle format) | done | reports::snapshot |
| Fixed-asset register + straight-line depreciation | Fixed Asset register | done | assets.rs; golden-covered schedule; idempotent runs; disposal with gain/loss |
| Cash flow statement (indirect) | Reports → Cash Flow | done | R-FUTURE-3 |
| Foreign-currency lines (base + foreign stored) | Multi-currency accts | done | R-FUTURE-1 |
| Period close (closing entry to Retained Earnings) | Close books | done | R-FUTURE-2 |
| Bank reconciliation (cleared flags + report) | Reconcile | done | — |
| QuickBooks CSV import (bank txns, chart of accounts) | Banking → Upload | done | R-FUTURE-4 |
| QuickBooks IIF + XLSX export | Export / reports | done | R-FUTURE-4 |
| A/R invoices + payments + aging | Business → Invoices | done | R-FUTURE-5 |
| A/P bills + payments + aging | Business → Bills | done | R-FUTURE-5 |
| Payroll runs (accounting only, no tax tables) + tax remittance | Payroll | done | — |
| Tracking classes (divisional P&L) | Class tracking | done | — |
| CPA handoff package (TB + GL xlsx, P&L + BS pdf, zip) | Reports → export | done | — |
| Budgets | Budgets | todo | R-FUTURE-6 (declined as bloat) |
| Scheduled transactions (recurring entries → drafts) | Scheduled txns / Recurring transactions | partial | hand-verified fixture incl. month-end dates; drafts only, by design |
| 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 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.
Capability parity (AI-first phase)
Semantic parity (above) is about correctness: the engine computes the
right numbers. Capability parity is about usefulness: can the new system
do everything the GSheet+GDrive system does today? Tracked separately in
docs/capability-parity.md, with its own cutover rule (parallel run +
Stephen's approval). The two catalogs converge: when both are green, the
sheet retires.