# AGENTS.md — wanderbooks

Operating manual for agents working in this repo. Read this first, then the
docs it points to. The short version: this is an engine-first, clean-room
rebuild of canonical double-entry bookkeeping, done the storytold way —
agents verify against oracles, track parity automatically, and never ship
what they haven't demonstrated.

## What this is

`wanderbooks` is a from-scratch implementation of double-entry bookkeeping
semantics, built to become a full bookkeeping application (engine now, UI
later). The reference points:

- **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
  (screenshot-in-the-loop, render oracles, automated parity floors). We adapt
  it to accounting: semantic oracles instead of pixel oracles.

## The non-negotiables

1. **Money is `Money`.** Exact `Decimal` plus a currency code. Binary floats
   (`f32`/`f64`) never appear in money paths — not for amounts, not for
   rates, not for "temporary" calculations. If you need a ratio, it is a
   `Decimal`.
2. **Every entry balances.** Debits equal credits exactly. No epsilon.
3. **Posted is forever.** Posted entries are immutable. Corrections are
   reversing entries linked by `reversal_of`. There is no edit, no delete.
4. **Reports are pure functions of a ledger.** If a report needs state that
   isn't in the ledger, the ledger model is wrong — fix the model.
5. **Clean room.** Build from public specs and observed behavior only:
   GnuCash documentation and file formats, the IFRS conceptual framework,
   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)

There is no UI yet, so "seeing what it's building" means **showing the
numbers**. The analog of storytold's screenshot-in-the-loop:

- A green `cargo test` is necessary but **not sufficient**. Every behavior
  change must be demonstrated through the public API with human-readable
  output: print the trial balance, the P&L, the balance sheet. Show the
  numbers moving the way accounting says they should.
- New behavior needs new tests in `crates/ledger-core/tests/invariants.rs`
  (or a new test file for a new crate). Tests encode accounting law, not
  implementation details: prefer "the accounting equation holds" over
  "this function returns that struct".
- **Golden files are sacred.** `tests/golden/*.json` hold hand-verified
  expected reports for canonical fixtures. If a change intentionally alters
  output, recompute the expected numbers *by hand from accounting principles*,
  update the golden, and explain the recomputation in the commit message.
  Never edit a golden to match output you haven't verified — that is how
  oracles die.
- 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:

0. **Specs come from authorities, not memory.** Every rule the engine
   enforces is in `docs/spec/rules.md` with its source: Pacioli for the
   mechanics of double entry, the IRS (vendored verbatim, public domain)
   for records, periods, 1099s, capitalization, partnerships, and payroll,
   FASB's Codification (cited, never copied) for GAAP. A rule no authority
   states is marked CONVENTION or DECISION, with who decided and when.
   Spec blocks in the code (```text GOAL/SOURCE/INVARIANTS/SCENARIOS)
   carry a `SOURCE:` line. Never write a spec from what the code happens
   to do, or from what you remember; find the document, or ask.

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
clone, with status. Rules:

- Every feature change updates `docs/parity.md` in the same commit.
- The **floor never decreases**: the count of `done` items is monotonic.
  CI will enforce this once the catalog is machine-readable (roadmap phase 3);
  until then, it is enforced by review — yours.
- Statuses are `done` (implemented + tested + golden-covered), `partial`,
  `todo`. No other statuses. `done` requires all three.

## Engine-first architecture

- All mutations are commands on `Ledger` (`create_entry`, `add_line`,
  `post_entry`, `reverse_entry`, `add_account`). Struct fields stay private;
  no other mutation path may exist.
- `ledger-core` depends only on `rust_decimal`, `thiserror`, `chrono`,
  `serde`, `serde_json`. New dependencies need justification in the commit
  message. No I/O, no networking, no time-source in the core.
- Future crates (`ledger-store`, `ledger-import`, `ledger-oracle`, `books-app`)
  depend inward toward the core, never the reverse. See `docs/architecture.md`.

## Working here

- `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.
- You have a very large context window. Use it: when working on semantics,
  load the whole `ledger-core` crate plus `docs/requirements.md` rather than
  guessing from snippets.
- If a requirement in `docs/requirements.md` conflicts with code, the
  requirement wins — then fix the code, and say so.

## Docs index

| Read this | When you need |
|---|---|
| `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 check correctness: golden files, property tests, fuzzing, cross-checks against other implementations (and who is right) |
| `docs/spec/` | The authorities every rule comes from (`rules.md`), with public-domain sources vendored verbatim |
| `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 |
| `docs/receipt-store.md` | Blob store + `ledger-store` SQLite persistence spec |
| `docs/glossary.md` | Debit/credit and friends, for agents new to accounting |
| `plan/STATUS.md` | Where the project stands right now |
| `plan/roadmap.md` | Phase plan: semantics → oracle harness → egui app → workflow parity |

## License

MIT OR Apache-2.0. New files carry no license headers; the license files at
the repo root cover the tree.