P1: the books keep how they are kept

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

docs/architecture.md

@@ -104,6 +104,23 @@ every complete line before it changes anything: a torn tail is set aside
 only when the gate passes, so an older version never alters newer books.
 Rule: `docs/spec/rules.md` B-27.
 
+## How the books are kept, in the books (P1)
+
+Settings, conventions, decisions, open items and approvals are journaled
+(journal format 2, declared with `journal.format_set` before the first
+such line, so a P0 reader stops there with "update wanderbooks"). The
+engine keeps them beside the ledger (`ledger_core::settings::Settings`,
+`ledger_core::conventions::Conventions`, fields of `Ledger`), so the store,
+its replay and the viewer's `Snapshot` share one reading; `Ledger::
+differs_from` and `verify` compare them, and the projection has a table
+for each (schema v12). `ledger-config` is the codec between them and a
+`wanderbooks.toml` (`codec::import`, `codec::export`) and still reads the
+file for books that predate P1 (the "file" source, until
+`books.import_settings`). The server (`settings::Live`) takes the books'
+settings whenever their last `settings.set` changes (on every lock of the
+store) and then never reads a file; "today" is the company's time zone's,
+set per request. Rule: `docs/spec/rules.md` B-29.
+
 ## The MCP server's store lock (`ledger-mcp`, P0)
 
 One `Store` is shared by every session (`SharedStore`: a

docs/mcp-interface.md

@@ -23,45 +23,87 @@ layer.
 
 ## Company settings
 
-`ledger-mcp` reads the books dir's `wanderbooks.toml` (default: next to
-`--data-dir`; override with `--books-toml PATH`): `[company] name` heads
-every report, `[company] fiscal_year_start` ("MM-DD", default "01-01";
-the year's end is derived, never stored) defines fiscal-year-to-date for the
-CPA package and the balance sheet's net income line, `[[company.members]]`
-(`name`, `share` as "50%" or "0.5", `capital_account` code; shares must sum
-to 100%) drives the statement of members' equity, `[books]
-accounting_basis` ("accrual" or "cash", default accrual) labels report
-footers, and `[books] receipt_threshold` sets the receipt policy unless
-`config.json` sets `receipt_policy`. Members may name a
-`distribution_account`, and `files_jointly_with` (spouses filing one joint
-return; the CPA package's README notes their two K-1s go on one Form 1040,
-and k1-members.csv ends with a members' total, not a K-1, that ties to
-Schedule L); single-owner businesses may set `[books] close_into`
-(the equity account a close puts net income in; default Retained Earnings)
-and `close_sweep` (draw, distribution, or dividend accounts closed into it).
-The cash flow statement's account roles are `[books] cash_accounts` (what
-it reconciles to), `financing_accounts` (loans, and money the owners
-advanced, such as a "Due to owners" liability: ASC 230-10-45-14(b)), and
-`investing_accounts` (loans the company makes, investments it buys: ASC
-230-10-20); the tools and the viewer both read them, and a call may pass
-its own (docs/spec/rules.md B-14).
+The books keep their own settings (journal format 2, plan/served.md P1):
+each change is a `settings.set` line with who decided it and when, replayed
+into `ledger_core::settings::Settings` by the server and the viewer alike
+(rules.md B-29). Every key is in `ledger_core::settings::KEYS`, with what it
+takes and means: the company's facts (`company.name`, `.entity_type`,
+`.tax_classification`, `.tax_form`, `.fiscal_year_start` ("MM-01"; the
+year's end is derived, never stored), `.timezone` (what "today" means for
+the books), `.formation_state`, `.formed`, `.state_entity_number`, `.ein`
+(the one identity number a setting keeps, shown masked: "**-***5893"),
+`.irs_name_control`, `.duns`, `.address`, `.registered_agent`,
+`.partnership_representative`, `.cpa`, `.members` (name, share as "50%" or
+"0.5", capital account, optional distributions account and
+`files_jointly_with`; shares sum to exactly 1)); the books'
+(`books.accounting_basis`, `.cash_accounts`, `.financing_accounts` (loans,
+and money the owners advanced: ASC 230-10-45-14(b)), `.investing_accounts`
+(ASC 230-10-20), `.close_into` (single owner only), `.close_sweep`,
+`.asset_tag_prefix`); and policy (`policy.evidence.threshold` (receipts
+strictly above it; "0.00": every entry), `.required_accounts`,
+`.exempt_accounts`, `policy.parties` (off, suggest, require),
+`policy.approval_rules` (off, the default, or enforce)). A value is checked
+by its key and kept in one spelling (a time zone as the database spells it,
+an amount without leading zeros, a return as `schedule_c`, `1065`, `1120s`
+or `1120`); a change is all or nothing, and the settings after it must hold
+together (members and `close_into` never both, a classification that names
+one return, a fiscal year that doesn't move under a closed period). No
+setting holds nine digits that read as an SSN or EIN (bare, or printed
+3-2-4 or 2-7) except `company.ein` and `company.duns`.
 
-The server reloads `wanderbooks.toml` (and `config.json`'s receipt policy)
-whenever either changes, compared by content at the start of each request,
-so an edit takes effect on the next call with no restart. A broken edit
-keeps the last good settings in force and is reported until fixed; the
-data dir and base currency are fixed at startup (`ledger-mcp/src/settings.rs`).
+Books from before P1 hold no `settings.set` and still read the books dir's
+`wanderbooks.toml` (default: next to `--data-dir`; `--books-toml PATH`)
+and `config.json`'s `receipt_policy`, reloaded whenever either changes, as
+before. `books.import_settings` moves them in once; from then on no file
+is read, not even at start (a broken file beside the books can't stop the
+server). A vault key file is never a books setting: `--vault-key-file PATH`
+names it to the server and the viewer (it wins over a file's `[vault]
+key_file`).
 
-- `books.settings {}` → `{ books_toml, books_toml_exists, config_json_present,
-  reload_error, loads, company, fiscal_year_start, tax_form, basis,
-  receipt_rule, members, cash_accounts, financing_accounts,
-  investing_accounts, close_into, close_sweep, problems }`: the settings in
-  force and where they come from. `problems` lists settings that disagree
-  with the chart (a code not in it, or of the wrong kind), each saying what
-  to change; `books.digest` repeats them, with a failed reload, as
-  `settings_problems`. The agent edits the file when the human gives a
-  company fact, a refusal names a setting, or a problem is listed, then
-  checks `books.settings`.
+- `books.settings {}` → `{ source ("books" or "file"), timezone, today,
+  approval_rules, keys: [{ key, doc, identity, value, set_by, seq }],
+  books_toml, books_toml_exists, config_json_present, reload_error, loads,
+  company, fiscal_year_start, tax_form, basis, receipt_rule,
+  receipt_required_accounts, receipt_exempt_accounts, parties, members,
+  cash_accounts, financing_accounts, investing_accounts, close_into,
+  close_sweep, problems }`: the settings in force, every key the books know
+  with its value (null: unset, its default applies) and who set it, and
+  `problems`, settings that disagree with the chart, each saying what to
+  change (conventions naming an account no longer in the chart among
+  them); `books.digest` repeats them as `settings_problems`. Settings are
+  named by key for books that keep their own, as the file spells them for
+  books that still read one; for those, `keys` shows the file's values,
+  with no journal line.
+- `books.set_setting { changes: [{ key, value }], decided_by, decided_on?,
+  citation?, note? }` → `{ changed: [{ key, was, value }], problems }`: one
+  or more changes, together or not at all (`value` null clears a key back to
+  its default; a value already set changes nothing, idempotent;
+  destructive, since it can clear or switch off a setting). Refused while
+  the books still read a settings file (or `config.json`): import it first,
+  so no setting is lost.
+- `books.import_settings { toml_text, config_json_text?, confirmed?,
+  skip_unknown?, decided_by, decided_on?, citation?, note? }` → `{ status
+  ("preview" or "imported"), changes, notes, unknown, comments }`: exactly
+  the changes
+  that make the books' settings what the file (and `config.json`'s
+  `receipt_policy`, which wins as it does for the server) says. `notes` are
+  what isn't a books setting and where it goes (`[books] data_dir`, `[vault]
+  key_file`, `[viewer]`, `base_currency`); `unknown` are entries the books
+  don't know, not imported (confirm with `skip_unknown`); `comments` are
+  the file's comments, in order, which are not settings and are not
+  imported (record what matters in them as a decision, open item,
+  convention or a setting's note). The text must be
+  the file the server reads, whole (its import is compared with the
+  server's own reading of its files, key by key), and the server must read
+  every setting afterwards as it does now; the vault key must then come
+  from `--vault-key-file` (on the viewer too). A file never turns approval
+  rules on. Books that keep their own settings take no import that changes
+  them (an identical one is no change). Without `confirmed`, a preview that
+  records nothing. An identity value exported masked imports as
+  "unchanged".
+- `books.export_settings {}` → `{ toml_text }`: the settings as a settings
+  file, each with who decided it as a comment, the EIN masked; a copy, and
+  importing it back changes nothing (`ledger_config::codec`).
 
 The accounts invoices, bills, payroll, and closes post to are not settings:
 they are control roles in the journal (rules.md B-23).
@@ -75,6 +117,66 @@ they are control roles in the journal (rules.md B-23).
   another role, and moving a balance sheet role while its account holds a
   balance. Journaled as `role.assigned`.
 
+## Tools — how the books are kept
+
+Conventions, decisions, open items and approvals live in the books too
+(`ledger_core::conventions`, rules.md B-29), each with who decided it and
+when; `books.start` lists them, and the handbook's
+settings-and-conventions section says how to use them.
+
+- `books.start { focus? }` (read-only, at most 8 KB) → `{ book: { name,
+  timezone, today, fiscal_year, base_currency, basis }, head: { seq, hash },
+  state ("needs_onboarding" or "active"), settings_source, rules: {
+  evidence, parties, approval_rules }, settings_summary: [{ key, value,
+  set_by, seq }], conventions: [{ id, kind, title, summary }], open_items:
+  [{ id, title, due }], truncated, handbook_sections, next_steps: [{ tool,
+  args?, why }] }`. The connect text names it as the first call. Lists cut
+  to fit say so in `truncated` ("conventions: 4 more (books.conventions)").
+  `focus` adds steps: `onboarding` the onboarding step, `close` the
+  company's close steps, `audit` `books.verify`. Not built yet (P5):
+  `book.id`, `book.url`, `head.last_handoff`, the `agent` input, and
+  loading it up front under tool search. Also `books://start`.
+- `books.conventions { kind?, include_retired? }` → every convention with
+  its full text, structure, revision and source (`books://conventions`).
+  `books.set_convention { id, kind, title, body_md, structured?,
+  decided_by, ... }` sets or revises one (kinds: `posting_template`,
+  structured `{ description?, lines: [{ account, side, share }] }`, each
+  side's shares summing to 1, on accounts in the chart that take postings
+  or on slots (`"{expense}"`) each draft names;
+  `approval_rule`, structured `{ approver, accounts?, amount_over? }`; and
+  `policy`, `close_step`, `calendar`, `mapping`, `note`, in words). An id is
+  a slug, revised in place (same kind), never reused once retired:
+  `books.retire_convention { id, reason, decided_by, ... }` (destructive).
+- `books.draft_from_template { template_id, date, amount, accounts?,
+  description?, party?, no_party_reason? }` → `{ entry_id, description,
+  lines }`: a draft whose lines split the amount (at most a line's) by the
+  template's shares, each side summing to it exactly, odd cents by largest
+  remainder; `accounts` names each slot's account (`{"expense": "6300"}`),
+  every slot and nothing else. A refused draft journals nothing (a disk
+  failing midway could leave a partial draft, as for any draft built line
+  by line).
+- `books.record_decision { subject, decision_md, decided_by: [..],
+  decided_on, evidence_attachment?, supersedes?, citation? }` → `{ id }`;
+  `books.decisions { include_superseded? }`. A decision supersedes at most
+  one live decision; its evidence is a document still in the books.
+- `books.raise_item { title, detail_md?, due?, decided_by, ... }` → `{ id }`,
+  `books.resolve_item { id, resolution, decided_by, ... }`,
+  `books.open_items { include_resolved? }`.
+- `books.approve_entry { entry_id, approver, note?, approved_on? }`: the
+  approver approved the draft as it stands (its fingerprint: date,
+  description, every line and class; a line added or a class changed
+  afterwards voids it). Under `policy.approval_rules = enforce`,
+  `books.post_entry`'s preview lists `approvals_missing` and a confirmed
+  post is refused with `approval_required` until each covering rule's
+  approver approved (the store refuses it too), and a tool that posts at
+  once (an invoice, a bill, a payment, payroll, a remittance, a disposal)
+  is refused when a rule covers the entry it would post: draft it instead.
+  Reversals, closes, depreciation and amortization are exempt. A rule
+  names accounts that take postings; an account a rule names can't be
+  renumbered until the rule is revised, and `books.renumber_account` lists
+  the conventions that name the old code. Under `off` (the default) rules
+  block nothing.
+
 ## Transports
 
 - **stdio** (default): `ledger-mcp --data-dir PATH`. For Claude Code,
@@ -99,9 +201,10 @@ re-read first, so a client connecting after an edit is told the new rule).
 It is short on purpose: clients cut long instructions (one cut the old
 text at 4,096 characters), so it is at most **1,400 characters**, and its
 first paragraph, at most **512**, stands alone: the entry point
-(`books.handbook`), the rule that these tools are the only way to the books
-(never local files), decimal-string amounts, and the
-draft → lines → preview → confirmed post flow. The second paragraph adds
+(`books.start` first each session, and `books.handbook` for every
+procedure), the rule that these tools are the only way to the books (never
+local files), decimal-string amounts, and the draft → lines → preview →
+confirmed post flow. The second paragraph adds
 that every entry balances and uses real accounts from `books.chart`; the
 parties rule in force (`[books] parties`: under "require" every entry
 the agent posts names its party or a no-party reason, since closes,
@@ -115,9 +218,10 @@ the books); that `books.create_invoice`, `books.create_bill`,
 `books.receive_payment`, `books.pay_bill`, `books.run_payroll` and
 `books.remit_payroll_taxes` post at once without a receipt check; TINs
 only into the vault; show the numbers, and after posting check
-`books.digest` and offer it to the human; and the
-one local file the agent may edit, the settings file `books.settings`
-names (until settings move into the journal, P1). When a long rule (many
+`books.digest` and offer it to the human; and where settings live: in the
+books, changed only through the tools, or, for books that still read a
+settings file, that file, the one local file the agent may edit until
+`books.import_settings` moves it in. When a long rule (many
 accounts, a huge threshold, a long name) would push it past 1,400
 characters, it drops the tracing hint first (the handbook's
 tracing-figures section has it), then the reasons in parentheses, then the
@@ -164,8 +268,9 @@ Tool descriptions are at most 700 characters; eight longer ones are listed
 in `tool_descriptions_fit_700_characters`, to be shortened in P5.
 
 **Annotations.** Every tool has a `title` and a `readOnlyHint`; every tool
-that changes anything also has a `destructiveHint`, true for these 25:
-`books.post_entry`, `books.reverse_entry`, `books.unlink_receipt`,
+that changes anything also has a `destructiveHint`, true for these 28:
+`books.post_entry`, `books.reverse_entry`, `books.import_settings`,
+`books.set_setting`, `books.retire_convention`, `books.unlink_receipt`,
 `books.unlink_attachment`, `books.withdraw_attachment`,
 `books.correct_asset`, `books.dispose_asset`, `books.run_depreciation`,
 `books.run_schedules`, `books.run_recurring`, `books.renumber_account`,
@@ -174,10 +279,10 @@ that changes anything also has a `destructiveHint`, true for these 25:
 `books.set_tin` (both overwrite a vault record), `books.purge_tin`,
 `books.create_invoice`, `books.create_bill`, `books.receive_payment`,
 `books.pay_bill`, `books.run_payroll`, `books.remit_payroll_taxes`; and an
-`idempotentHint` on the five that a repeat with the same arguments leaves
+`idempotentHint` on the seven that a repeat with the same arguments leaves
 the journal and the vault as they were: `books.verify`,
-`books.run_depreciation`, `books.run_schedules`, `books.run_recurring` and
-`books.set_party_roles` (a setter such as `books.update_party`,
+`books.run_depreciation`, `books.run_schedules`, `books.run_recurring`,
+`books.set_party_roles`, `books.set_setting` and `books.import_settings` (a setter such as `books.update_party`,
 `books.set_fx_rate` or `books.set_tin` journals a line, and `books.set_tin`
 seals a new vault record, every time, so none carries it;
 `idempotent_tools_change_nothing_when_repeated` calls each candidate twice
@@ -923,6 +1028,7 @@ posting.
 Hand-rolled on `ServerHandler` (rmcp 3.x has no resource macros):
 `list_resources` advertises, `read_resource` renders.
 
+- `books://start`, `books://settings`, `books://conventions`
 - `books://chart`
 - `books://reports/trial-balance`, `books://reports/balance-sheet`,
   `books://reports/profit-and-loss`

docs/spec/rules.md

@@ -828,3 +828,78 @@ stops, and the books reopen after; the inputs that once panicked,
 pinned; every tool over every old book) and `server.rs`
 `periods_are_a_year_and_a_month`, `dates_are_four_digit_years_and_real_days`;
 `ledger-gui` `tests/old_books.rs`.
+
+## B-29 The books keep how they are kept
+
+**SOURCE:** DECISION (plan/served.md I-3, owner decisions of 2026-10-16:
+"the journal holds all books state"; light governance: decisions are
+recorded with who made them and when, not as paperwork); IRS Pub. 538 and
+the rules of B-1 to B-28 for what each setting means.
+
+A company's settings, its conventions (how it posts each kind of
+transaction, its policies and close steps), the decisions its owners made,
+what is open, and approvals of draft entries are facts about the books,
+kept in the journal like every other fact, each with who decided it and
+when (journal format 2: `settings.set`, `convention.set`,
+`convention.retired`, `decision.recorded`, `open_item.raised`,
+`open_item.resolved`, `entry.approved`). A settings file is only text to
+import from or export to; books that keep their own settings never read
+one.
+
+- A setting is one of the known keys, checked by its key and kept in one
+  spelling; a change is all or nothing, and the settings after it hold
+  together. Replay takes any value of the right shape (B-28).
+- No setting, convention id, convention, decision, open item or approval
+  holds a number that reads as a full TIN (nine digits standing alone,
+  bare or printed 3-2-4 or 2-7 with a dash or a space), except the
+  company's own EIN, shown masked everywhere but reports, packages and the
+  viewer, and a D-U-N-S number in its own key.
+- A record of how the books are kept changes no entry, draft, period or
+  account (proved for the model: `Step.record_changes_no_figure`; checked
+  on the engine after every record in `settings_replay_is_pure`). Settings
+  that say how the same entries are presented or later allocated (the
+  fiscal year, the cash flow roles, the members) present them by the
+  settings in force; the fiscal year can't move once a period is closed
+  under it (a changed tax year needs the IRS's consent, Form 1128).
+- Moving a settings file in reads every setting exactly as the server read
+  the file: the text must be the file the server reads, and books that
+  keep their own settings take no import that changes them.
+- A setting key or convention kind this version doesn't know is a newer
+  version's: the books are "newer", never "damaged" (B-27).
+- A posting template's lines split the amount exactly on each side, odd
+  cents by largest remainder (B-13's rule); a slot (`{expense}`) takes the
+  account each draft names.
+- Approval rules block anything only when the company enforces them
+  (`policy.approval_rules = enforce`; off by default). Then a draft a rule
+  covers posts only once its approver approved it as it stands (its
+  fingerprint: date, description, every line and class), and an operation
+  that would post such an entry at once (an invoice, a bill, a payment,
+  payroll, a remittance, a disposal) is refused: it is drafted instead.
+  Reversals, closes, depreciation and amortization follow from entries
+  already posted and are exempt. A rule names accounts that take postings,
+  and an account a rule names can't be renumbered until the rule is
+  revised.
+
+**Enforced:** `ledger_core::settings` (`check`, `Settings::check_changes`,
+`check_whole`, `shape`, `apply`), `ledger_core::conventions` (`check_new`,
+`check_decision`, `check_open_item`, `split`), `Ledger::check_settings`,
+`check_convention`, `approvals_missing`, `template_lines`; `ledger-store`
+`Store::change_settings`, `adopt_settings`, `set_convention`,
+`draft_from_template` (rehearsed whole), `record_decision`; the format gate
+(format 2 declared before the first such line); `ledger_config::codec`
+(`import`, `export`); `Store::post_entry` and `approval_gate`
+(`ApprovalRequired`, `ApprovalNeedsDraft`), `check_renumber_account`;
+`ledger-mcp` `books.import_settings` (the file the server reads, whole),
+`books.post_entry` (`approval_required`).
+**Checked:** `ledger-core` settings and conventions unit tests;
+`ledger-store` `tests/settings.rs` (`settings_replay_is_pure`, 256 cases
+per check, 2,000 by hand, with posts between records and every record
+checked to change no figure or entry; `approval_rules_off_by_default`,
+`approvals_cover_every_post`, `the_fiscal_year_stays_under_closed_periods`,
+`a_newer_key_or_kind_is_newer`;
+`books_written_under_p1_open_to_their_record`, fixture
+`old-books/p1_record`); `ledger-config` `tests/codec_props.rs`
+(`exports_round_trip`) and codec unit tests; `ledger-cli` `tests/init.rs`
+`the_toml_and_its_examples_import_and_round_trip`; `ledger-mcp`
+`tests/spec_kept.rs`; Lean `Step.record_changes_no_figure`,
+`Reachable.records`; fuzz `fuzz_settings_replay`.

docs/testing.md

@@ -279,6 +279,81 @@ since `asset_long_life` alone takes three minutes a run):
   ran past 9999 never trued up and could depreciate past its salvage
   (`spec_replayed_extremes.rs` `a_life_past_9999_trues_up_to_the_cent`).
 
+## P1: the books keep how they are kept (2026-10-17)
+
+| Law | Test |
+|---|---|
+| Replay is pure: after any sequence of settings, convention, decision, open-item, template and approval commands, valid or refused, the live store, the store reopened from its journal and the viewer's snapshot hold the same settings and conventions, and the store verifies (database row for row) | `ledger-store` `tests/settings.rs` `settings_replay_is_pure` (proptest, 512 cases per check; 2,000 by hand, release, passed) |
+| The first such change declares journal format 2, once; a change to what is set journals nothing; refused changes journal nothing | `the_first_change_declares_format_2`, `refused_changes_journal_nothing` |
+| Approval rules block nothing until enforced; then an entry a rule covers posts only once its approver approved it as it stands | `approval_rules_off_by_default`; `ledger-mcp` `spec_kept.rs` `approval_rules_through_the_server` |
+| A template drafts exactly, odd cents by largest remainder, its slots named by each draft, all or nothing | `templates_draft_exactly_or_not_at_all`, `template_slots_take_the_account_each_draft_names`, `templates_draft_through_the_server`, core `splits_are_exact` |
+| Books written under P1 open to the same record forever | `books_written_under_p1_open_to_their_record` (fixture `old-books/p1_record`, also in every old-books test of the store, the viewer and the server) |
+| A settings file imports exactly, reads as it did, and an export round-trips; a masked EIN never imports | `ledger-config` codec unit tests, `tests/codec_props.rs` `exports_round_trip` (512 cases), `ledger-cli` `the_toml_and_its_examples_import_and_round_trip` |
+| Moving settings in: set refused before, the preview records nothing, the file never read after (not even to start), an import that reads differently or loses the vault key refused, the EIN only ever masked | `spec_kept.rs` `a_settings_file_moves_into_the_books`, `an_import_that_reads_differently_is_refused`, `an_import_needs_the_vault_key_on_the_command_line` |
+| books.start fits in 8 KB and says what it cut | `start_fits_in_8_kb` |
+| Values are canonical; no full TIN but the company's EIN; settings hold together; replay takes shapes | core `settings::tests` |
+| Every new tool on the happy path, schema-checked; read-only tools change nothing; idempotent tools repeat as no-ops | `spec_mcp.rs` `inv1_*`, `read_only_tools_change_nothing`; `spec_vault.rs` `idempotent_tools_change_nothing_when_repeated` |
+| The connect text names books.start in its lead and where settings live, in budget, journaled or not | `instructions_budget`, `a_typical_company_gets_the_whole_connect_text` |
+| Fuzzed journals of the new events open in the writer and the viewer alike, verify, and read every way without a panic | `fuzz_settings_replay` (and `fuzz_store_replay` with the new types) |
+| A record changes no figure | Lean `Step.record_changes_no_figure`, `Reachable.records` |
+
+### P1 mutation testing (2026-10-17)
+
+Every mutant in the P1 diff (`--in-diff`), per crate, against that
+crate's tests and its nearest callers' (the recipes' settings:
+`STORE_CASES=64`, `MCP_CASES=16`, no shrinking). First run, then after
+targeted tests:
+
+| Crate | Mutants | First run: caught / timeouts / unviable / missed | Missed after |
+|---|---|---|---|
+| `ledger-core` (with `ledger-store`'s tests) | 486 | 318 / 5 / 41 / 122 | 1 (equivalent) |
+| `ledger-config` (with `ledger-cli`'s) | 72 | 44 / 0 / 2 / 26 | 0 |
+| `ledger-store` | 113 | 81 / 0 / 28 / 4 | 1 (equivalent) |
+| `ledger-mcp` | 260 | 156 / 0 / 96 / 8 | 0 |
+| `ledger-gui` | 25 | 7 / 12 / 3 / 3 | 0 |
+
+No survivor was a bug; each was a test gap, now closed by a test of
+the law it broke:
+
+- **Core.** `tests/settings_units.rs`: every settings accessor's exact
+  value, the company profile and its order, every party-policy
+  spelling, fiscal-year bounds off January, the TIN detector's joiner
+  limits, each text, share and month-day boundary, every tax
+  classification and the return it names, the one-quadrillion cap,
+  today in the company's time zone, and the display of members, lists
+  and the masked EIN. `tests/conventions_units.rs`: slot names (32 and
+  33 characters), summaries cut at 160 characters, template bounds (2
+  and 50 lines kept, 1 and 51 refused, a share out of (0, 1] named by
+  its line), the approval fingerprint against an independent FNV-1a of
+  the hashed text, approval rules at the limit and one cent over
+  (debits only), and which fields make a convention's revision.
+- **Store.** An empty import still moves the books in (once); a
+  posting template replay can't read is newer.
+- **Config.** The TOML comment scanner (a `#` in basic and literal
+  strings, an escaped quote), comments carried by an import, a masked
+  EIN matching, not matching and into empty books, an empty list
+  changing nothing, `differences` naming each field, the export's
+  provenance lines, `effective_receipt_policy` with and without
+  `config.json` (`tests/effective_policy.rs`).
+- **MCP.** `Live::journaled` reads no file, `sync` reloads once per
+  change; the books://start, settings and conventions resources; a
+  renumber names exactly the conventions that name the old code.
+- **Viewer.** The Company page's cards (`tests/kept.rs`): live
+  conventions and not retired ones, standing decisions and not
+  superseded ones, open items and not resolved ones, who decided each
+  and when, a late item saying so in words ("overdue since", added for
+  this: colour alone told only the sighted), and the empty-profile copy
+  of books that keep their settings. `--vault-key-file` wins over the
+  settings and an unknown argument exits 2 (`tests/vault_key_flag.rs`).
+  The first run's 12 timeouts were builds slowed by parallel work: the
+  rerun caught them all.
+
+Equivalent: `holds_printed_tin` mapping a full-width digit by `/`
+instead of `-` (every such digit becomes the digit 1: it asks only
+whether a character is a digit), and `approval_gate`'s fast path (`||`
+made `&&`: with rules off or none, the probe's `approvals_missing` is
+empty either way, so only the cost differs).
+
 ## Benchmarks (baseline 2026-10-13)
 
 No budget, by decision (Stephen, 2026-10-13: the books do little work

docs/verification.md

@@ -87,7 +87,9 @@ Each law, and what proves it. Kani harnesses are in
 ### 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.
+add an account, start a draft, post, reverse, open a period, close one,
+and record how the books are kept (a setting, convention, decision, open
+item or approval: one step, `record`, each record abstracted to a number).
 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**:
@@ -106,6 +108,18 @@ sequence of commands, of any length**:
     commands adds, removes, or changes an entry dated in it, and it stays
     closed.
     - Lean `Step.frozen`, `Steps.frozen`
+13a. **How the books are kept changes no entry**: in the model, a record
+    (a setting, convention, decision, open item or approval) leaves the
+    chart, every posted entry, every draft and every period exactly as they
+    were, and any number of them keeps a reachable state reachable. The
+    model's `record` step touches only the records by definition, so the
+    proof says the model is sound, not the engine; the engine's side is
+    checked by `settings_replay_is_pure`, which snapshots every figure and
+    entry around each record (rules.md B-29). Settings that change how the
+    same entries are presented (the fiscal year, cash flow roles, members)
+    are outside this law by design.
+    - Lean `Step.record_changes_no_figure`, `Reachable.records` (no
+      axioms at all) · property `settings_replay_is_pure`
 
 ### Closing