bookspec is a specification first: every rule normative and sourced,
every rule demonstrated by concrete examples, and any accounting engine
checked against them through one interface (D-34). This moves the
examples' schema out of the test that happened to parse them and makes
the interface explicit.
- `bookspec/checker` (its own workspace, inside this repository until
the harness is stable): `Example`, `Setup`, `Event`, `Expect`, `Query`,
`Refusal` and the TOML parser, every structure `deny_unknown_fields`,
with `Example::from_toml` checking the cross-field shape (closed lists,
exact decimal amounts, dates, one event kind, `reverses` counting from
1, the shares summing to 1, commands accepted or refused and not both).
- `Engine` (`load`, `apply`, `query`, `claims`) and `Refusal { rule,
reason }`; the refusal's rule is the bookspec identifier, so a refusal
names the rule it belongs to. `Claims` also carries the option an
engine picks for a CHOICE rule.
- `bookspec/runner` drives any `Engine` through the examples and reports
per rule: pass, fail, not claimed. It compares the answer itself; an
engine is never asked whether it agrees with itself.
- `crates/ledger-core/tests/bookspec.rs` is the wanderbooks adapter over
`Store`: the loader parses through the checker, its own checks are
unchanged, and the new `the_runner_reports_every_claimed_rule_green`
runs all 56 examples through the trait. The IIF appendix is answered
through `ledger_package::export_iif`, the code its own test checks.
- `just check` runs the bookspec workspace's fmt, clippy, rustdoc and
tests too, so an example cannot rot (D-34, Z-17).
The plan's trait has four methods and no path for an example's
`[[changes]]` (a rename, the policy, an asset correction), which post no
entry: `change` is the fifth, required so an engine cannot skip those
examples silently. This is reported to the EM as the one departure.
One money rule holds here too: an answer's figures are exact decimal
strings, never JSON numbers, so no engine can round a cent through a
float.
The final month takes what the months before leave, spread over its days;
a disposed asset stops on its disposal day. A skipped month is caught up
in the month the run is made; a reversed run un-posts its month. New
schedules spread by day; equal-months schedules must start on the 1st.
Amounts round to the currency's own minor unit. Kani and Lean proofs; an
exhaustive search over runs, reversals and disposals.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01T3gXMVt7XJPi6ens1or9Dj
Members' shares of earnings are split cumulatively by largest remainder in
the closes, the members' equity statement, the K-1 worksheet and the
viewer, so a member's capital on a given day never moves by a cent when its
month is later closed. Old closes replay as they were; the first P3 close
carries any true-up. Feature members_cumulative. Kani and Lean proofs of
the bounded drift; bookspec examples.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01T3gXMVt7XJPi6ens1or9Dj
Settings, conventions (posting templates, approval rules, policies,
close steps, calendar, mappings, notes), decisions, open items and
entry approvals are journal events (journal format 2). Books that keep
their settings never read wanderbooks.toml or config.json; the server
and the viewer take the vault key from --vault-key-file instead.
books.import_settings moves a settings file in once, exactly as the
server reads it. Approval rules, when enforced, gate every posting
path. Replay refuses what it can't read as newer, never as corrupt.
Lean: a record changes no figure. Mutation on the whole diff: every
survivor killed by a test but two equivalent (docs/testing.md). The
Company page says a late open item is overdue in words, not colour
alone.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01T3gXMVt7XJPi6ens1or9Dj
Max-testing pass, ranks 4-6 and step 9 for ledger-core.
Fuzzing (rank 4): fuzz_op_sequence now drives balanced pairs, foreign
lines, periods, closes, and amounts from raw decimal bits, and asserts
the books stay valid (TB balances, posted entries validate, no draft in
a closed period); new fuzz_core_serde (every persisted core type
round-trips) and fuzz_store_open (a corrupt journal is an error, never a
panic); hangs count (-timeout=10). 54M executions; one crash:
- fuzz_journal_line: a number too big for an integer parsed as a float,
and its canonical form (which the hash chain covers) re-canonicalized
differently. The journal never holds floats (R-2), so the reader now
refuses them (JournalLine::parse, used by every journal reader);
regression a_journal_line_with_a_float_is_refused. Checked first: the
real books' journal has none. Rerun: 13.2M executions, clean.
Seeds in fuzz/seeds/ (synthetic, minimal); the grown corpora stay out of
git. `just fuzz <target> <seconds>`.
Miri (rank 4): the core's unit, bridge, and invariant tests under Miri
(our code has no unsafe; rust_decimal and chrono do): no undefined
behavior. `just miri`. A pinned nightly (nightly-2026-10-01, with miri)
is now in mise.toml.
Benchmarks (rank 6): criterion (new dev-dependency: the playbook's Rust
benchmark tool; none existed) in benches/books.rs; baselines in
docs/testing.md. The store's per-command rehearsal clone costs ~1 ms at
10k entries. No budget yet, so nothing gates on them. `just bench`.
CI: .github/workflows/check.yml runs `just check` on every push;
scheduled.yml runs proofs, the GnuCash oracle, fuzzing, and mutation
weekly. Tools come from mise.toml.
docs/testing.md: every layer, its oracle rank, command, runtime, and
gate; benchmark baselines; the ASSUMED invariants for the owner to reject;
the gap list with triggers. docs/oracle.md's fuzzing paragraph had
claimed persistent corpora that didn't exist; corrected.
Also: ledger-import now inherits the workspace lints (nightly cargo
warned).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX