diff --git a/docs/architecture.md b/docs/architecture.md index a80d7ff..747485a 100644 --- a/docs/architecture.md +++ b/docs/architecture.md @@ -80,3 +80,39 @@ 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`. + +## The journal format gate (`ledger-store`, P0) + +Every journal line passes a gate after its parse, seq and chain checks +(`ledger_store::format`): a type this version knows, or a +`journal.format_set` this version reads. A line it can't read stops the +read whole (the writer never opens, the viewer applies none of the new +lines): never skipped, never half-read. A line with a key beside the +envelope's (`seq`, `ts`, `type`, `payload`, `prev`, frozen across formats) +is refused the same way, never read with the key dropped. The refusal is +`NewerJournal`, not `JournalCorrupt`: verified ("line N is intact; this +version can't check the lines after it") when the next line's `prev`, +read leniently whatever format frames that line, matches the refused +line's hash (the SHA-256 of its canonical JSON, every key included); +corruption when a `prev` it can read doesn't match; "newer or damaged" +when there is no next line or no `prev` it can read. The writer +(`Store::open`) and the viewer (`Snapshot`) read the journal the same way +(bytes split on newlines) and share the same gate and settling +(`format::gate`, `format::settle`), so they always give the same answer +for the same journal (fuzzed by `fuzz_store_replay`). The writer checks +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. + +## The MCP server's store lock (`ledger-mcp`, P0) + +One `Store` is shared by every session (`SharedStore`: a +`tokio::sync::Mutex` and a `stopped` flag). Tool bodies run on tokio's +blocking threads (`run_blocking`), never on the async workers, and take the +lock with `blocking_lock`; the guard is `!Send`, so no tool can hold it +across an `.await`. The store journals a command before it changes memory, +so a panic between the two would leave memory behind the journal; and a +tokio mutex never poisons. So the server fails closed: a panic in a +request (its task, or while it holds the guard) sets `stopped`, and every +later request, on every session, is refused until a restart, which +re-verifies the journal. diff --git a/docs/mcp-interface.md b/docs/mcp-interface.md index 8985a51..2f58f3c 100644 --- a/docs/mcp-interface.md +++ b/docs/mcp-interface.md @@ -52,7 +52,7 @@ 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.settings {}` → `{ books_toml, books_toml_exists, config_json, +- `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 @@ -92,14 +92,127 @@ they are control roles in the journal (rules.md B-23). ## Server instructions -The MCP `initialize` response carries an `instructions` string: the agent -operating contract (below) in condensed form. The model reads it at the start -of every session, before any tool call. Tool descriptions repeat the relevant -fragment at the point of use (`post_entry`'s description states the -preview-before-post rule; `attach_receipt`'s states the receipt rule). Prose -guidance is therefore delivered twice — once at session start, once at the -tool — but it is guidance, not enforcement. Enforcement is the receipt policy -below. +The MCP `initialize` response carries an `instructions` string, the +**connect text** (`ledger-mcp/src/handbook.rs`), composed in `get_info` +from the settings in force when the client connects (the settings are +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 +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, +depreciation and amortization post with none; under "suggest" name it +where there is one; under "off" nothing); corrections by reversal; the receipt rule in force +(`ReceiptPolicy::rule`: the exact threshold in the books' base currency, +never rounded, the accounts that always need a receipt and those exempt, +and that reversals need none); the exemptions (depreciation and +amortization, whose schedules are the evidence, and closes, derived from +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 +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 +tracing hint for good and lists fewer account codes (at last only how many +there are; `books.settings` lists every one, uncut, in +`receipt_required_accounts` and `receipt_exempt_accounts`), then words +that only help; never the rule itself. A company with no name yet (the +settings' default) is "a new company". The company name in it is one line of plain text (control characters and +line breaks become spaces, Unicode format characters such as bidi +overrides and zero-width spaces are dropped), cut to 56 characters. +`instructions_budget` (the longest rule, every parties setting) and +`the_company_name_is_one_plain_line` check it. + +The long guidance is the **handbook**, compiled in from +`ledger-mcp/handbook/*.md`, with the receipt rule in force rendered in: + +- `books.handbook { section? }` (read-only) → `{ read_first, sections: + [{ id, title, uri, chars }], section: { id, title, text } | null }`. + Without `section`, the index (`read_first` says to read `contract` + first); with a section id, that section's Markdown; with `"all"`, the + whole handbook in reading order. The input schema lists the ids: + contract, entries, drafts-and-reversals, evidence-and-receipts, + attachments, files-in-out, reconciliation, fixed-assets, + prepaid-and-recurring, revenue-and-payouts, parties-and-tins, 1099, + cpa-handoff, settings-and-conventions, viewer, rules-that-change, + control-roles, tracing-figures. +- The same as resources: `books://handbook` (the index, JSON) and + `books://handbook/{section}` (Markdown, `text/markdown`), one listed per + section. + +No text the agent is given (tool JSON with its schemas, resources, connect +text, handbook, and every refusal fixed in code: each error variant's +template in the crates under the server, scanned from source, built error +texts, and the server's refusal constants) names a helper command, a home +path, the data dir or its flag, the import-root flag, a file of the books +(`.jsonl`, the database, `vault.key`, `.gitignore`), git, GitHub, a pull +request, a repo doc (`docs/`, `.md`), or tells the agent to read the +books' files; no tool title or description, connect text or handbook +section names `wanderbooks.toml` (the input and output schemas name it by +design, for `books.settings`' `books_toml`) (`tool_text_lint`). A rule set by law that the books +don't know for a year names its official source (the statute or +publication, with its address) and says to tell the human. +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`, +`books.unlink_attachment`, `books.withdraw_attachment`, +`books.correct_asset`, `books.dispose_asset`, `books.run_depreciation`, +`books.run_schedules`, `books.run_recurring`, `books.renumber_account`, +`books.assign_role`, `books.close_period`, `books.reconcile`, +`books.void_statement`, `books.void_reconciliation`, `books.set_w9`, +`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 +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.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 +to check). Every tool's +`openWorldHint` is false: the books are a closed world, and no tool +reaches beyond them. `books.export_cpa_package` writes a file, so it is +not read-only. No tool carries `requiresUserInteraction` (owner decision +2026-10-16: no added prompts). `annotations_complete` pins all of this. +The read-only hint is true in behaviour: `spec_mcp` checks, on every call, +that a read-only tool leaves the journal, the contents of every file under +the data dir (the database by every row of every table; SQLite's -wal and +-shm files, which move pages and hold read marks on their own, aside), +the vault and the settings file as they were +(`read_only_tools_change_nothing`). + +**Failing closed.** Tool bodies run on blocking threads, one at a time on +the store. If a request panics (an internal error), the journal may hold a +line the memory doesn't, so the server stops taking requests: every later +call, on every session sharing the store, is refused with "the books +server stopped taking requests after an internal error, to protect the +books: ask the human to restart the books server", never the panic's own +text. A restart re-verifies the journal +(`a_request_that_panics_stops_the_server`). So a panic an input can reach +would be a denial of service, and none can be: the dates a tool takes +are four-digit years and real days, its amounts at most a journal +line's, and a recurring run bounded; books an earlier version wrote past +those bounds still open (replay accepts what that version accepted), so +every figure the server derives from them (a draft's total, a schedule's +plan, aging, a party's totals, the asset register) is computed or +refused ("too large to compute exactly", or a date outside the calendar +the books keep), never a panic (rules.md B-28). `tests/hostile_args.rs` +drives every tool with generated hostile arguments and every resource +with generated URIs, checks after each call that the server still +serves, restarts it after them to check the books reopen, and drives +every tool over every book in ledger-store's `tests/fixtures/old-books`. ## Tool design principles @@ -119,6 +232,7 @@ below. ## Tools — books +- `books.handbook { section? }`: the guide (see "Server instructions"). - `books.chart` → `{ accounts: [{ id, code, name, type, parent, placeholder, balance }] }`. Balances included: one call answers "what do we have." - `books.draft_entry { date: "2026-10-10", description: "...", vendor?, @@ -147,7 +261,10 @@ below. its `vendor`, `party_id`, and `party` (the party's label, when it names exactly one) tags, `parties` / `parties_error` as in the `post_entry` preview, and `no_party_reason` when it is marked as having no - counterparty. + counterparty. `total` (its debits) is null, with `total_error` saying + why, for a draft an earlier version journaled whose lines exact + arithmetic can't sum; a draft line on an account the chart doesn't have + (older books hold such drafts) shows an empty code and "(no account N)". - `books.search_entries { account?, date_from?, date_to?, text?, limit?, offset? }` → entries with lines, newest first. `limit` caps at 100. - `books.trial_balance { as_of? }` → `as_of`, lines, totals, `balanced` @@ -240,9 +357,13 @@ through the policy. - `books.create_schedule { kind: "prepaid_expense" | "deferred_revenue", description, total, start, months, balance_account, pl_account }` → - `{ schedule_id, ..., total, remaining, months: [{ date, amount, posted }] }`. - Prepaid needs an asset and an expense account; deferred revenue a - liability and a revenue account. + `{ schedule_id, ..., total, remaining, months: [{ date, amount, posted }], + plan_error }`. Prepaid needs an asset and an expense account; deferred + revenue a liability and a revenue account. `plan_error` is null, except + for a schedule an earlier version accepted whose months run past the + last date the books can compute: then it says why, `remaining` is null + and `months` empty, and `books.run_schedules` refuses until it is dealt + with. - `books.list_schedules {}` → `{ schedules: [...] }`, same shape. - `books.run_schedules { through?, confirmed? }` → `{ status: "preview" | "posted", postings: [{ schedule_id, date, description, amount, @@ -533,15 +654,46 @@ and the CPA package carries them. `books.set_tin`); a TIN with a new last four clears the old TIN facts first (`party.tin_set` null), so the two never disagree. The form (PDF, PNG, JPEG; 25 MB at most) goes to the vault only, never the attachment - store. Facts given later without a TIN keep the vault record when their + store. `w9_file_path` is read exactly as `books.import_local_file` reads + a path (the import roots, the sealed places, no links followed out of + them), and its type is judged by the file the path really leads to. + Facts given later without a TIN keep the vault record when their last four agree with the vault's TIN, and are refused when they don't (pass the new TIN, or purge). Clearing the facts (`clear: true`) is refused while the vault holds the party's TIN or form: purge first. - `books.get_w9 { party, save_to }` → `{ party_id, path, file_name, size_bytes, note }`. Writes the party's form from the vault to `save_to`: a new file (an existing one is refused), in a folder that exists, - outside the books dir, mode 0600. Returns the path, never the contents. - Journals nothing. + outside the books dir and outside the import roots, mode 0600. Returns + the path, never the contents. Journals nothing. The same holds for + `books.vendor_1099`'s `save_csv_to` with `include_tins` and + `books.export_cpa_package`'s `save_to` with TINs: a file with full TINs + never lands where it could be filed back in. Nor does one go in from + elsewhere: the server keeps, beside the vault, the SHA-256 of every file + it read or wrote with full TINs (the W-9 `books.set_w9` reads, recorded + once the call has passed every check, just before the vault keeps it, + so a refused call marks no file; each of these outputs; each file inside a CPA package + that holds a TIN), shared by every session and kept across restarts, + and every filing tool (`books.import_local_file`, `books.attach_receipt`, + `books.file_document`) refuses those exact files and any text file + (CSV, TSV, text, JSON, IIF, XML, HTML, Markdown, by type, name or UTF-8 + or UTF-16 decoding, UTF-16 with a byte-order mark or NUL-interleaved + without one) holding a full TIN, storing nothing. A text file + holds one when it has a TIN the vault holds, anywhere, as nine digits, + 3-2-4 joined by hyphens, spaces or dots, or 2-7 joined by a hyphen or a + space (compared on the server; a vault that can't be opened leaves the + next test alone), or a stand-alone number printed as an SSN or EIN is + (123-45-6789, 12-3456789; no digit, and no hyphen or dot followed by a + digit, beside it). Bank exports pass: routing and account numbers, + long references and dates next to amounts are not TINs (rules.md B-26). + No probing: a text with more than two TIN-shaped numbers ending in the + last four of a TIN the books know is refused before the vault is + opened, in the same words whether or not one is that TIN, so the vault + is compared against at most two candidates a filing (rules.md B-26). + An altered copy of a binary file (a W-9 PDF re-saved or re-scanned), + and a TIN the vault doesn't hold written another way, are not + detected: P2 and P7 take the path tools and full TINs out of the + agent's reach. - `books.purge_tin { party, reason, confirmed? }` → `{ status: "preview" | "purged", party_id, name, tin_in_vault, w9_file_in_vault, tin_last4?, journaled, note }`. Without `confirmed`, a preview that changes nothing. @@ -630,9 +782,11 @@ posting. (account codes that always require receipts, e.g. meals and travel) and `receipt_exempt_accounts` (e.g. automated bank fees). Human-edited and versioned with the deployment. -- **Preview.** Every `post_entry` / `reverse_entry` preview includes the - receipt checklist (`attached: [...]`, `required_but_missing: bool`), so the - human sees it before confirming. +- **Preview.** Every `post_entry` preview includes the receipt checklist + (`receipts: [...]`, `receipt_required: bool`, `receipt_missing: bool`, + `split_detected: [...]`), so the human sees it before confirming. A + `reverse_entry` preview carries none: a reversal needs no receipt (the + original carries the evidence). - **Hard error.** Confirming a posting that violates the policy fails with a structured, machine-readable error (JSON in the tool-error string): `{ "code": "receipt_required", "message": "…", "entry_id": 5, @@ -728,9 +882,41 @@ posting. - `books.import_chart_csv { csv_text }` → creates accounts from `code,name,type,parent_code` CSV. All-or-nothing. - `books.import_local_file { path, category: "receipt" | "document", ... }` - → imports a file from the server's filesystem. The Drive backfill path: - the agent downloads from Google Drive via the CLI to a temp path, then - calls this. Keeps Drive credentials out of the server. + → files a file from the server's own disk, read only from the **import + roots**: each `--import-root DIR` given to `ledger-mcp` (repeatable), or + by default the downloads folder only (`$XDG_DOWNLOAD_DIR`, else + `~/Downloads`). No root may be `/`, the home folder or a folder holding + it, a folder holding the books dir, the data dir (where a symlinked one + really is), the vault or a vault key, or a folder inside the books dir, + the data dir or the vault (every file there would be refused): a named + root like that stops + the server at startup, saying why; a default one is dropped. The default + is used only when it is a real folder that isn't the home folder (an + `XDG_DOWNLOAD_DIR` of `$HOME/` falls back to `~/Downloads`, and to no + root when that doesn't exist; an import then says the server has no + import folder). The path must be absolute, with no `.` or `..` name, + and where it leads (every link followed) a regular file strictly inside + a root, with one hard link. Refusals never name a path and never probe: + a path that is missing, a dangling link, outside the roots, or with a + `.` or `..` name (refused before anything is looked up: `a/b/..` + resolves only when `b` is a folder) gets one refusal, "no + such file in the server's import folders (by default your downloads + folder): save it there first". Inside a root, the books' sealed places + (the data dir, the vault, the key file in force and the default one, + where each leads, `~/.config/wanderbooks`, and the key files' folders + unless that folder is the home folder, a root, or holds one) are refused + as "belongs to the books or the TIN vault"; anything else in the books + dir is refused with "save a copy of it in the server's import folders + first". The file is opened by a walk from `/`, one name at a time, each + folder with `openat(O_DIRECTORY | O_NOFOLLOW)` and the file with + `O_NOFOLLOW | O_NONBLOCK`, so a folder on the path swapped for a link + after the check fails the open and a pipe can't hang the server; no step + may land on a protected place by device and inode (one renamed into a + root), and the file opened must be the checked one (device, inode, one + link). It is filed under the name and type of the file the path leads + to. Files holding full TINs are refused as above + (`ledger-mcp/src/local_files.rs`, `tin_files.rs`). Deleted in P2 + (uploads replace it). ## Resources (read-only) @@ -740,7 +926,10 @@ Hand-rolled on `ServerHandler` (rmcp 3.x has no resource macros): - `books://chart` - `books://reports/trial-balance`, `books://reports/balance-sheet`, `books://reports/profit-and-loss` -- `books://digest?since=2026-10-01` +- `books://digest?since=2026-10-01`; bare (or with an empty `since=`), + this month so far +- `books://handbook` (the index) and `books://handbook/{section}` (one per + section, Markdown) - `books://receipts/{id}` — receipt metadata + base64 bytes Resources exist so read-only clients (dashboards, the future read-only GUI, @@ -756,7 +945,7 @@ in the server's tool descriptions, so the model reads it at use time): in prose. 3. **Attach receipts at record time.** A material entry without its source document is an incomplete entry. File first, link later if the entry - isn't ready. Postings at or above the receipt policy threshold *cannot* + isn't ready. Postings strictly above the receipt policy threshold *cannot* post without one — the server refuses with `receipt_required`. 4. **When unsure of categorization, draft and ask.** A draft is cheap; a wrong posting is a reversal. Never guess-post. diff --git a/docs/parity.md b/docs/parity.md index 2f6f2bd..9e2c7fe 100644 --- a/docs/parity.md +++ b/docs/parity.md @@ -49,6 +49,19 @@ No other statuses. Workflow/UI parity (QuickBooks/Xero reference) gets its own catalog when the egui phase starts; semantics come first. +### P0 guard rails (2026-10-16) + +P0 (`plan/served.md`) changed no feature in the catalog above, so no +status moved and the floor stands. It hardened what exists: an older +version refuses books from a newer one as newer, not corrupt (rules.md +B-27); the MCP server fails closed after an internal error, and no input +reaches one (dates are four-digit years, amounts at most a line's, B-28); +local files +are read only from the import roots, never the books, the vault or its +key; no file with a full TIN is filed into the books (B-26); the agent is +told the rules in force in a short connect text and a handbook, and no +agent text points at the books' files, git or the repo. + ## Capability parity (AI-first phase) Semantic parity (above) is about *correctness*: the engine computes the diff --git a/docs/spec/rules.md b/docs/spec/rules.md index 76c0674..1d654b2 100644 --- a/docs/spec/rules.md +++ b/docs/spec/rules.md @@ -589,19 +589,55 @@ filed back in as a receipt and read out again), and the package comes back only as its path. No file holding a full TIN is filed into the books (DECISION, P0 review round 2, 2026-10-16): the server keeps, beside the vault, the SHA-256 of every file it read or wrote with full TINs (the W-9 -`books.set_w9` reads, recorded as it is read; each `books.get_w9` copy; +`books.set_w9` reads, recorded once the call has passed every check, just +before the vault keeps it, so a refused call marks no file; each +`books.get_w9` copy; a 1099 worksheet with TINs; a CPA package with TINs and each file in it that holds one), shared by every session and every later server for the books, and every way a file enters the books (`books.import_local_file`, `books.attach_receipt`, `books.file_document`) refuses those exact files, and refuses any text file (by its type or name, or because it decodes as -UTF-8 or UTF-16) in which `has_full_tin` finds a TIN. What this can't -catch: a changed copy of a binary file (a W-9 PDF re-saved or re-scanned), -or a TIN in an image; `plan/served.md` P2 and P7 take the path tools and -full TINs out of the agent's reach. The text scan reads nine digits with -separators as a TIN, so a statement's text with a date run into an -amount, or a long reference number, is refused too; such a file is filed -as a PDF. A locked vault or a missing TIN never fails +UTF-8 or UTF-16, with a byte-order mark or, NUL-interleaved, without one) +holding (a) a TIN the vault holds for a party of the +books, anywhere in the text, as nine digits in a row, as 3-2-4 digits +joined by hyphens, spaces or dots, or as 2-7 digits joined by a hyphen +or a space (compared on the server against the decrypted vault, never +returned or logged; a vault that can't be opened leaves (b) alone), or +(b) a number printed as an SSN or EIN is, standing alone: 3-2-4 digits +joined by hyphens (123-45-6789) or 2-7 joined by a hyphen (12-3456789), +with no digit, and no hyphen or dot followed by a digit, on either side. +Full-width digits and Unicode hyphens and spaces count as their ASCII +kin (`tin_files.rs`). The text check is narrow on purpose (DECISION, +Stephen, 2026-10-16): bank exports are filed for reconciliation, and +their routing numbers, long references and dates next to amounts are +not TINs; the broad `has_full_tin` reading stays on what the server says +(refusals and results). Because (a) compares against the vault, its +answer would tell an agent whether a text it chose holds a vault TIN; +the tools show each TIN's last four, so an agent filing texts full of +nine-digit numbers ending in those four could find the TIN in about 17 +filings. So (a) answers for at most two candidates a filing (DECISION, +P0 review, 2026-10-16): before the vault is opened, a text holding more +than two distinct TIN-shaped numbers (in any rendering (a) reads; one +number written several ways counts once) that end in the last four of a +TIN the books know (each party's TIN facts and W-9 facts, read from the +books; once the vault is opened, its own records' last fours too) is +refused with words of its own ("more than two numbers shaped like a +TIN"), the same byte for byte whether or not one of them is a vault TIN +and whether or not the vault is open; only a text with no more than two +is compared against the vault. With the last four known, a TIN is one of +100,000 numbers, so finding one this way takes on the order of 50,000 +filings, each one refused and seen. What this can't catch: a changed +copy of a binary file (a W-9 PDF re-saved or re-scanned), a TIN in an +image, or a TIN the vault doesn't hold written other than (b); +`plan/served.md` P2 and P7 take the path tools and full TINs out of the +agent's reach. A known limit, open until then: (a) still answers for two +candidates a filing, so an agent that makes those 50,000 refused filings +can find a TIN; P2's access log records every call, refusals included, +and P7's human-only TIN channel takes full TINs, and with them this +check, off the agent's path. A bank export holding three numbers that +happen to end in a known last four is refused the same way (filed as a +PDF instead). +A locked vault or a missing TIN never fails the package: it says which TINs are missing. `books.purge_tin` deletes a party's vault records and journals that it did. @@ -614,15 +650,18 @@ records, records_held, purge_records); `ledger-mcp` `books.set_w9`, `books.set_tin`, `books.get_w9`, `books.purge_tin`, `books.vendor_1099`, `books.export_cpa_package` (open_vault refuses a key file in the books dir; outside_books for files with a TIN; vault_tin checks the vault -against the books); `ledger-mcp` `tin_files` (the registry and the text -scan, on every filing tool). +against the books); `ledger-mcp` `tin_files` (the registry, the text +scan and its probe bound, on every filing tool; `known_tin_last4` gives +the books' last fours). **Checked:** `ledger-core` `tests/spec_parties.rs`; `ledger-store` `tests/parties.rs`; `ledger-vault` `tests/vault.rs`; `ledger-mcp` `tests/spec_parties.rs`, `tests/spec_vault.rs` (every response, the log, and every file in the books dir outside `vault/` scanned for the TINs in any formatting), `tests/tin_files.rs` -(`a_tin_bearing_file_is_refused_from_every_session_and_after_a_restart`), -and the unit tests in `tin_files.rs`. +(`a_tin_bearing_file_is_refused_from_every_session_and_after_a_restart`, +`text_with_a_vault_tin_or_a_printed_one_is_refused_and_a_bank_export_is_not`, +`text_probing_for_a_tin_is_refused_alike_by_every_filing_tool`), and the +unit tests in `tin_files.rs`. ## B-27 The journal format gate: newer is not corrupt @@ -689,3 +728,103 @@ lines before it pass, so an older version never alters newer books. `ledger-gui` `tests/newer_journal.rs`; `ledger-mcp` `tests/startup.rs`; the `fuzz_store_replay` target (the writer and the viewer agree on newer versus bad). + +## B-28 What new commands take: four-digit years, amounts a line can carry + +**Status:** CONVENTION (ISO 8601's basic calendar dates have four-digit +years, as do the spreadsheet and PDF formats the books export to); +DECISION (P0 review round 3, 2026-10-16, finding S1: the server stops +for every session when a request panics, so no input may reach one); +DECISION (P0 review round 4, 2026-10-17: posted is forever, so the +bounds are the commands', never replay's) + +**New commands.** Every date a command takes or derives is in +0001-01-01 through 9999-12-31 (`ledger_core::calendar`): a date given +to a tool is exactly YYYY-MM-DD, a real day in that range (no sign, no +space, no fifth year digit); a period is a month of it; a new schedule's +last month, a new asset's last day of depreciation, a new recurring +entry's start and end, a new period, a new invoice's or bill's date and +due date, a disposal's date stay in it. Every amount a command takes, +not only a posted line's, is at most a journal line's +(1,000,000,000,000,000, `kernel::MAX_LINE_AMOUNT`): a draft line (by +size; its precision is checked when it posts), a document line, a +payout's lines and deposit, every payroll figure, a statement's +balances, a party's share, a contributor's basis, disposal proceeds, a +recurring template's lines. One run of the recurring entries creates at +most 1,000 drafts (`MAX_RECURRING_RUN`); a later date is run in steps. + +**Replay accepts every line an earlier version accepted.** The bounds +above came after books were written, and posted is forever (B-8): a +journal an earlier wanderbooks wrote opens, in the writer and the +viewer alike, and replays to the same figures, forever. Replay applies +each check exactly as the version before the bound did: a journaled date +is any date chrono reads as `%Y-%m-%d` (chrono's own range, about +262,000 years either way, written "+10000-01-01" past 9999); a draft +line, a recurring template, a party's share, a contributor's basis, a +document line, a payment, a payroll run and disposal proceeds carry no +upper bound beyond what their own rules always said (positive, cents, +balanced, and so on); a schedule's months are 1 to 600 and an asset's +life ends on a date chrono holds. The checks split in two: the +command's (`Ledger::add_line`, `register_asset`, `TaxBasis::check`, +`shares::check_shares`, ...) and replay's (`replay_add_line`, +`replay_register_asset`, `TaxBasis::check_journaled`, +`shares::check_shares_journaled`, ...), and every bound has its pair of +tests: the command refuses past it; replay of an old line past it is +accepted. + +**Derived figures refuse, never panic.** Because replay accepts what +the commands now refuse, every figure the books derive is computed with +checked arithmetic: a sum or product exact arithmetic can't hold is +refused with "too large to compute exactly" (`TooLargeToCompute`), and +a date past chrono's last day with `DateOutOfRange`, at the point of +computation (a draft's debits, a document's total and balance, aging, +net pay, a payroll plan, an entry's money flow and its shares' +resolution, the fixed asset register, an amortization plan), never +wrapped, rounded early or panicked on, and the server stays up. Date +walks reach chrono's last day without stepping past it (an asset's +depreciation in December 262142, an interval ending at +`NaiveDate::MAX`). A replayed line whose own figures overflow (a +recurring template whose debits Decimal can't sum: no version could +write it, and the last one panicked replaying it) is refused as the +books open, never a panic. + +**Enforced:** `ledger_core::calendar`; `Ledger::try_create_entry`, +`add_line`, `add_line_fx`, `validate_new_asset`, `dispose_asset`, +`schedules::validate_schedule`, `validate_recurring`, +`periods::validate_period_range`, `arap::validate_lines`, +`validate_due_date`, `payroll::check_payroll_ranges`, `payout_plan`, +`shares::check_shares`, `TaxBasis::check`, `reconciliation_report`; for +replay, `replay_add_line`, `replay_add_line_fx`, +`replay_register_asset`, `replay_correct_asset`, +`replay_dispose_asset`, `replay_set_asset_tax_basis`, +`replay_set_entry_parties`, `replay_register_recurring`, +`replay_register_schedule` (`validate_schedule_shape`), +`replay_create_period` (`validate_period_order`), `replay_invoice`, +`replay_bill`, `replay_invoice_payment`, `replay_bill_payment`, +`replay_payroll_run`, `validate_new_asset_journaled`, +`validate_recurring_journaled`, `check_shares_journaled`, +`TaxBasis::check_journaled`; derived: `Invoice::total`/`balance`, +`Bill::total`/`balance`, `AgingRow::total`, `ar_aging`, `ap_aging`, +`PayrollLine::net_pay`, `payroll_entry_plan`, `parties::entry_flow`, +`shares::share_target`, `shares::resolve`, `fixed_asset_register`, +`schedules::amortization_plan`, `month_end`, `depreciation_schedule`, +`analysis::intervals`, `form1099::vendor_part`, `k1::share_property`, +`ReceiptPolicy::entry_debits`; `ledger-store` `parse_date` (replay: +chrono's range), `parse_period`, `last_day_of_month`, +`record_statement`, `dispose_preview`, `run_recurring`; `ledger-mcp` +`parse_date`, `parse_period_mcp`, `last_day_of_month`. +**Checked:** `ledger-core` `tests/spec_bounds.rs` (each bound and its +replay pair), `calendar.rs`, the unit tests of `amortization_plan`, +`intervals`, `vendor_part` and `share_property`, `assets.rs` +`registration_rejects_date_overflow`, `invariants.rs` +`out_of_range_amount_is_rejected`; `ledger-store` `tests/store.rs` +`books_an_earlier_version_wrote_open_to_its_figures` (every book in +`tests/fixtures/old-books`, written by main 188c90ea, opens in the writer +and the viewer and replays to exactly the figures main computed) and +`every_figure_over_old_books_is_computed_or_refused`, `tests/bounds.rs`; +`ledger-mcp` `tests/hostile_args.rs` (every tool with generated hostile +arguments and every resource with generated URIs: the server never +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`. diff --git a/docs/testing.md b/docs/testing.md index 82ddf98..b84d695 100644 --- a/docs/testing.md +++ b/docs/testing.md @@ -14,7 +14,7 @@ promise. |---|---|---|---|---|---| | Spec-derived examples | written specs with sources (1) | `tests/spec_*.rs`, `invariants.rs`, `statements.rs`, `assets.rs`, ...; the store's `tests/spec_store.rs` (written blind, from its specs only) | `just check` | seconds | every change | | Regressions | the bug, named (1) | beside the code they cover, `*_regression`/named for the defect | `just check` | seconds | every change | -| Compatibility contracts | journals written under older rules must open (1) | `ledger-store/tests/store.rs` (`books_written_under_older_rules_still_open`) | `just check` | <1s | every change | +| Compatibility contracts | journals written under older rules must open, and replay to the figures their version computed (1) | `ledger-store/tests/store.rs` (`books_written_under_older_rules_still_open`; `books_an_earlier_version_wrote_open_to_its_figures` over `tests/fixtures/old-books`: books main 188c90ea wrote, with main's own figures in `expected.json`, in the writer and the viewer; `every_figure_over_old_books_is_computed_or_refused`); `ledger-mcp/tests/hostile_args.rs` `old_books_answer_every_tool`; `ledger-gui/tests/old_books.rs` | `just check` | ~30s | every change | | Properties | laws over all inputs (2) | `properties.rs`, `spec_*.rs`, `kernel_bridge.rs` | `just check` | seconds | every change | | Metamorphic | scaling, reversal, ordering invariance (2) | `spec_reports.rs` | `just check` | seconds | every change | | Refusal law (store) | a refused command never reaches the journal, an accepted one always does; the live ledger equals its journal's replay in every part, and the books reopen to it (2, 3) | `store.rs` `refused_commands_never_reach_the_journal` | `just check` (`STORE_CASES=5000` deeper) | ~20s | every change | @@ -49,6 +49,236 @@ Layer 1). The van depreciation golden was replaced on 2026-10-13 by a hand computation (`van_schedule_is_the_hand_computed_one`) after every row was checked against it. +## P0 guard rails (2026-10-16) + +Laws added with P0 (`plan/served.md`) and its review, each with the test +that would fail if it broke: + +| Law | Test | +|---|---| +| Books from a newer wanderbooks are "newer", never "corrupt", from the writer, the viewer and the server; damage stays corruption (rules.md B-27) | `ledger-store` `tests/format.rs` (`old_reader_gets_newer_journal`, `damaged_journals_are_still_corrupt`); `ledger-gui` `tests/newer_journal.rs`; `ledger-mcp` `tests/startup.rs` | +| A line the gate refuses is called newer only once the next line's `prev` checks its hash; a last line is "newer or damaged" | `a_damaged_line_that_looks_newer_is_corrupt_when_the_next_line_checks_it`, `an_unreadable_last_line_is_reported_as_newer_or_damaged`, `a_newer_line_the_next_line_chains_onto_is_newer_and_intact` (the message vouches for that line only) | +| The envelope and its hash are frozen across formats: a next line in a newer format (a float, a string seq, keys of its own) settles by its `prev` alone, never as corrupt; a key beside the envelope is newer, never dropped, and still checked through; a refused line followed by an unreadable one is "newer or damaged" | `format.rs` `a_newer_format_frames_its_lines_its_own_way`, `an_unknown_envelope_key_is_newer_and_checked_through`, `a_refused_line_followed_by_a_garbled_line_is_unverified` | +| The writer and the viewer read bytes alike: a line that isn't UTF-8 is corrupt to both; an older version never repairs (truncates) newer books | `a_line_that_is_not_utf8_is_corrupt_for_the_viewer_and_the_writer`, `an_old_reader_never_repairs_newer_books` | +| A newer format is newer whatever its features look like; a blank line is damage to the viewer as to the writer | `format.rs` `a_newer_format_is_newer_whatever_its_features_look_like`; `a_blank_line_is_corrupt_for_the_viewer_and_the_writer` | +| A request that panics stops the server: every later request, on every session, is refused | `server.rs` `a_request_that_panics_stops_the_server` | +| No input reaches a panic (each would stop the server for every session): every tool with arguments generated from its schema and made hostile (wrong types, u64::MAX, decimals of 30+ digits or absurd exponents, dates like 0000-00-00, 99999-12-31, +262142-12-31, 2026-02-30, periods like 999999-01, control and format characters, long strings), every resource URI generated; the inputs that once panicked, pinned; after each property the server restarts and the books reopen (a call a command accepts but replay refuses would brick them); every tool and resource over every old book (rules.md B-28) | `ledger-mcp` `tests/hostile_args.rs` `hostile_tool_arguments_never_stop_the_server` (with a floor: most calls reach a tool, some succeed), `hostile_resource_uris_never_stop_the_server`, `inputs_that_once_panicked_are_refused_or_answered`, `old_books_answer_every_tool`; `MCP_CASES` and `OLD_BOOKS_CASES` (default 3 per tool per book) set the cases | +| Dates are in 0001-01-01 through 9999-12-31 and amounts at most a line's, for every new command; replay accepts every line an earlier version accepted (each bound has its pair: the command refuses past it, the replayed old line is accepted); a figure derived past exact arithmetic or chrono's calendar is refused, never a panic; a recurring run makes at most 1,000 drafts (rules.md B-28) | `ledger-core` `tests/spec_bounds.rs`, `calendar.rs` tests, `plans_at_the_edges_are_computed_or_refused`, `intervals_reach_chronos_last_day`, `a_vendor_part_is_scaled_exactly_or_refused`, the `share_property` cases; `ledger-store` `tests/bounds.rs`, `tests/store.rs` (the old-books tests); `server.rs` `periods_are_a_year_and_a_month`, `dates_are_four_digit_years_and_real_days` | +| Opening the books changes nothing until every complete line passes in memory (chain, gate, first line, replay); the viewer applies the writer's first-line rule (rules.md B-27) | `format.rs` `a_bad_complete_line_before_a_torn_tail_leaves_the_journal_as_it_was`, `the_first_line_is_store_created_for_the_viewer_and_the_writer`; `fuzz_store_replay` (the first line varies) | +| A path with a `.` or `..` name is refused as missing before anything is looked up; a root inside the books, the data dir or the vault is refused at startup (dropped as the default) | `local_files.rs` `a_dot_or_dotdot_name_never_tells_whether_folders_outside_exist`, `a_root_holding_the_books_or_the_home_folder_is_refused`; `startup.rs` `an_import_root_holding_the_books_or_the_home_folder_is_refused`, `a_default_download_dir_holding_the_books_is_dropped_not_fatal` | +| UTF-16 text without a byte-order mark is scanned like any text; a refused `books.set_w9` marks no file; a refused resource read never echoes a TIN | `tin_files.rs` (tests) `utf16_text_without_a_byte_order_mark_is_scanned_either_way_round`, `a_refused_set_w9_never_marks_its_file`, unit test `only_nul_interleaved_bytes_read_as_utf16_without_a_mark`; `spec_vault.rs` `resource_refusals_never_echo_a_tin` | +| idempotentHint only where a repeat with the same arguments leaves the journal and the vault as they were; every tool's hints pinned in one table | `spec_vault.rs` `idempotent_tools_change_nothing_when_repeated`; `annotations_complete` | +| books.settings lists every receipt-required and exempt account, uncut; a fresh company is "a new company"; the lint catches `just` however it ends and where the books are | `mcp_stdio.rs` `every_receipt_account_left_out_of_the_connect_text_is_in_books_settings`; `handbook.rs` `a_fresh_company_is_a_new_company`; `tool_text_lint_catches_helpers_and_locations` | +| A local file is read only from inside an import root, never a sealed place (data dir, vault, keys, the key folders that don't hold a root), never through a swap after the check (a component walk with `O_NOFOLLOW`, no step onto a protected inode); a missing, dangling or outside path gets one refusal | `local_files.rs` `import_local_file_refuses_key_and_journal`, the property `import_allowed_iff_regular_file_inside_a_root_outside_the_books`, `refusals_never_tell_what_is_there`, `a_file_swapped_after_the_check_is_never_read`, `a_folder_swapped_after_the_check_is_never_walked_through` (the reviewer's race, without `/proc`), `resolved_follows_every_link_a_dangling_one_too`, `sealing_a_key_never_seals_a_whole_root`; through the tools, `mcp_stdio.rs` `import_local_file_and_set_w9_refuse_the_key_vault_and_journal_inside_a_root` | +| No import root is `/`, the home folder or holds it, or holds the books, data dir, vault or a key; the default is a real downloads folder or none | `local_files.rs` `the_default_root_is_never_the_home_folder_or_the_filesystem`, `a_root_holding_the_books_or_the_home_folder_is_refused`; `startup.rs` `an_import_root_holding_the_books_or_the_home_folder_is_refused`, `a_download_dir_of_home_never_opens_the_home_folder` | +| A file with full TINs is never written into an import root, and never filed into the books: every file the server read or wrote with TINs (from any session, after a restart, out of a CPA package), by every filing tool | `mcp_stdio.rs` `tin_bearing_files_never_land_where_they_could_be_filed_back_in`; `tin_files.rs` (tests) `a_tin_bearing_file_is_refused_from_every_session_and_after_a_restart`; unit test `a_recorded_tin_file_is_refused_by_every_reader_of_the_registry` | +| Text filed into the books is refused when it holds a TIN the vault keeps (nine digits, 3-2-4 by hyphen, space or dot, 2-7 by hyphen or space, anywhere) or a stand-alone printed SSN or EIN (123-45-6789, 12-3456789), and only then: a bank export (routing numbers, long references, a date next to an amount) and a longer number holding an SSN shape go in; a locked vault leaves the printed shapes (rules.md B-26) | `tin_files.rs` (tests) `text_with_a_vault_tin_or_a_printed_one_is_refused_and_a_bank_export_is_not`; unit tests `text_holding_a_vault_tin_is_refused_in_every_rendering`, `a_printed_ssn_or_ein_is_refused`, `a_longer_number_holding_a_tin_shape_passes`, `an_ordinary_bank_export_passes`, `binary_bytes_are_not_scanned` | +| Filing is no TIN oracle: text with more than two TIN-shaped numbers ending in a known TIN's last four (the books' TIN and W-9 facts, then the vault's own) is refused before the vault is opened, byte for byte alike whether one is the vault's TIN or none is, the vault open or locked, by every filing tool; one or two such numbers are compared against the vault, one number written many ways counts once, and other last fours never count (rules.md B-26) | `tin_files.rs` (tests) `text_probing_for_a_tin_is_refused_alike_by_every_filing_tool`; unit tests `text_probing_for_a_tin_is_refused_alike_whether_or_not_it_holds_it` (the vault never opened for a probe), `one_or_two_candidates_are_compared_against_the_vault` | +| The connect text fits its budgets, its lead stands alone, it states the receipt rule enforced (exact threshold in the base currency, required and exempt accounts, reversals) and the parties rule in force, and the company name can't break it (control and format characters) | `handbook.rs` `instructions_budget`, `a_typical_company_gets_the_whole_connect_text`, `the_company_name_is_one_plain_line`; `receipt_policy.rs` `the_rule_told_is_the_rule_enforced`, `a_long_or_odd_account_list_stays_short_and_plain`; a new session is told the settings in force: `a_new_session_is_told_the_settings_in_force` | +| No text the agent is given (whole tool JSON, resources, connect text, handbook, every error template and refusal) points at files, git, GitHub, repo docs, flags or helper commands; descriptions fit 700 characters (listed exceptions, P5) | `tool_text_lint`, `tool_descriptions_fit_700_characters`; `ledger-core` `an_unknown_year_threshold_is_never_guessed` | +| Every tool is annotated (openWorldHint false on all), and the read-only hint is true in behaviour (journal, every data-dir file's contents, the database's rows, the vault and the settings unchanged) | `annotations_complete`; `spec_mcp.rs` `read_only_tools_change_nothing` (checked on every call in `Mcp::tool`) | +| A bare (or empty-`since`) digest covers this month so far, on any day of it, as the server counts it (the stdio test reads the server's own month, and starts over if it turns) | `a_bare_digest_covers_this_month_so_far`; `mcp_stdio.rs` `digest_resource_bare_reads` | +| The handbook: every section, "all" in order, the schema names every id | `handbook_sections_render_the_rule_in_force`, `the_whole_handbook_is_every_section_in_order`, `mcp_stdio.rs` `handbook_tool_and_resources_over_stdio` | + +## P0 mutation testing (2026-10-16) + +Every mutant cargo-mutants makes in the final P0 diff (`jj diff -r +'main..@'`, `--in-diff`), per crate, against that crate's tests (the +recipes' settings: `STORE_CASES=64`, `MCP_CASES=16`, no shrinking; the +viewer against its lib tests and `newer_journal`). Final run: + +| Crate | Mutants | Caught | Timeouts | Unviable | Missed | +|---|---|---|---|---|---| +| `ledger-mcp` | 296 | 208 | 3 | 71 | 14 (equivalent, below) | +| `ledger-store` | 73 | 58 | 0 | 12 | 3 (equivalent, below) | +| `ledger-config` | 35 | 35 | 0 | 0 | 0 | +| `ledger-gui` | 9 | 6 | 0 | 3 | 0 | +| `ledger-core` | 1 | 1 | 0 | 0 | 0 | + +(`ledger-cli`'s change makes no mutant.) After the filing scan's probe +bound (rules.md B-26), `tin_files.rs` alone was run again against the +whole P0 diff: 74 mutants, 74 caught, among them every mutant of the +bound (`probes` made true or false, `>` made `>=`, `==` or `<`, the +last four's `%` made `/` or `+`, here and for the vault's own last +fours) and of the shared `tin_shaped` scan. The three MCP timeouts are +`resolved` without its hop limit (`< 40` made true, the count made to +go down or stay 0): a link loop then never ends, so the tests can't +pass. The first run missed 36 in the MCP server, 5 in the store, 4 in +config and 1 in the viewer. Each was killed by a test of the law it +broke, removed by simpler code, or is equivalent: + +- **Killed (MCP).** A section's title is its heading + (`a_title_is_the_heading_text`; over stdio the handbook tool titles a + section by its heading and "all" as the whole handbook, + `handbook_tool_and_resources_over_stdio`). A refused default import + root is dropped, never fatal (`ImportRoots::explicit`: + `a_default_download_dir_holding_the_books_is_dropped_not_fatal`). A + `.jpg` or `.jpeg` W-9 is taken (`every_w9_file_type_is_taken`). The + waker wakes: a request pending until another thread wakes it completes + (`a_request_that_waits_is_woken_and_completes`). The walk opens each + folder with `O_DIRECTORY | O_NOFOLLOW`: a folder swapped for a link to + an unprotected folder outside the roots, or for a pipe, is never walked + through and never blocks + (`a_folder_swapped_for_a_link_or_a_pipe_is_never_walked_through`). A + read failure names its kind, never the path + (`cant_read_names_the_failure_not_the_path`). `resolved` follows 40 + links, as the kernel does, and no more + (`resolved_follows_forty_links_and_no_more`). A file is saved only to + a new file in a folder that exists, and a missing folder or a taken + file is refused as such, never as a failed write + (`a_package_goes_only_to_a_new_file_in_a_folder_that_exists`, + `the_w9_file_goes_to_the_vault_never_the_documents`). The CPA package + marks only its own TIN files: a statement it carries still goes in + afterwards (`a_tin_bearing_file_is_refused_from_every_session_and_after_a_restart`). + An unreadable TIN-file registry refuses every file + (`an_unreadable_registry_refuses_every_file`). Text that isn't UTF-8 + is scanned when its type is `text/*`, a JSON type (`/json`, `+json`) + or its name says text (`encodings` in the `tin_files.rs` unit tests). +- **Killed (store).** `read_journal_and_format` returns every line and + the format in force (`read_journal_and_format_gives_every_line_and_the_format`). + The newline that ends a line is no part of it, so the viewer's words + about a damaged line are the writer's, opening and following + (`the_viewer_and_the_writer_say_the_same_of_a_damaged_line`; it kills + `snapshot.rs` `raw.len() - 1` → `/ 1`). +- **Killed (config).** The short rule (no codes listed) counts each kind + of account, whichever kinds there are, and says nothing of accounts + when there are none (`the_short_rule_counts_each_kind_of_account`); a + code of exactly 12 characters is kept whole + (`a_long_or_odd_account_list_stays_short_and_plain`). +- **Killed (viewer).** The journal page tells a `journal.format_set` + line (`a_format_this_version_reads_opens_and_the_journal_page_tells_it`). +- **Simpler code (MCP).** `inspect` compared `canonicalize` with + `resolved`; only a race between those two calls could make them differ, + and the file read was the checked one either way. It now places an + existing path by `canonicalize` itself. `read_checked` refused by the + file's size before reading, so its read limit (`limit + 1`) was only + reached by a file growing during the read; the read's limit is now the + one check (the 25 MiB upload test kills `+ 1` → `* 1`). `openat` failed + on `fd < 0`, now on `fd == -1`, as openat(2) specifies. +- **Equivalent (MCP, all 14 missed).** `^` for `|` in the open flags + (six: the walk's first step, each folder's two, the file's two, and + `openat`'s `O_CLOEXEC`): `O_RDONLY` is 0 and `O_DIRECTORY`, `O_NOFOLLOW`, + `O_NONBLOCK`, `O_CLOEXEC` are distinct bits, so `a ^ b` is `a | b`. + `&` for `|` in the first step's `O_RDONLY | O_DIRECTORY`: it opens `/` + read-only either way, and `/` is always a folder. The off-Unix stubs + (`Protected::inodes`, five mutants; `open_walk`; `hard_linked`) are + not compiled on Linux, so their mutants change nothing here. +- **Equivalent (store, all 3 missed).** `Snapshot::journal_format` and + `Store::journal_format` returning the default: this version reads + format 1 with no features only (`SUPPORTED_JOURNAL_FORMAT` 1, + `KNOWN_FEATURES` empty), and that is the default, so no journal it + opens has another format in force; the first format 2 or feature makes + them killable. `Store::open` setting aside a torn tail when + `complete <= raw.len()`: `repair_torn_tail` re-reads the journal under + the writer lock and does nothing when it ends in a newline. + +### Round 3 (2026-10-17) + +`cargo mutants --in-diff` on this round's changes (the diff from the +round-2 stack to round 3), per crate, output under +`~/.cache/wanderbooks/mutants/p0-r3-` (`MCP_CASES=16`, +`STORE_CASES=64`, `PROPTEST_MAX_SHRINK_ITERS=0`): + +| Crate | Mutants | Caught | Missed, then killed | Equivalent | Timeouts | Unviable | +|---|---|---|---|---|---|---| +| `ledger-core` (tests of core and store) | 63 | 53 | 3 | 1 | 0 | 6 | +| `ledger-store` | 40 | 34 | 0 | 0 | 2 | 4 | +| `ledger-mcp` | 85 | 63 | 5 | 1 | 0 | 16 | +| `ledger-config` (a doc comment only) | 0 | | | | | | + +- **Killed (core).** `replay_add_line_fx`'s size check (`>` to `==` or + `>=`) and `validate_recurring`'s (`>` to `>=`): a line, base or + foreign, added or replayed, and a template line may be exactly the line + limit (`spec_bounds.rs` `the_bound_is_the_line_limit_itself`). +- **Timeouts (store, counted as caught).** `run_recurring`'s cap (`>` to + `==` or `<`): without it, a monthly entry run through 9999-12-31 writes + some 95,000 drafts, which is what the cap is for + (`bounds.rs` `a_recurring_run_has_an_end`). +- **Killed (MCP).** `text_of`'s byte-order-mark arms: text with a mark and + no NUL byte at all (full-width digits, CJK) is still read as UTF-16 + (`utf16_with_a_mark_is_read_whatever_it_holds`); its NUL-stripped + reading (`!=` to `==`): NULs scattered in text hide no TIN + (`nuls_scattered_in_text_hide_no_tin`); `nul_interleaved`'s eighth + (`*` to `+`): half NUL on one side and three of sixteen on the other is + not UTF-16; `redact_value`'s array arm: a TIN inside an array of an + error's data is masked (`redact_error_masks_every_tin_in_the_message_and_data`). +- **Equivalent.** `k1::share_property` returning early on + `whole <= 0 && total <= 0` instead of `||`: `whole` is + `min(pool, total)` with both sums of non-negative amounts, so the two + differ only when `whole` is 0 and `total` positive, where the + computation goes on to split 0 into zeros, the early answer. + `redact_value`'s guard `has_full_tin(t)` replaced by `true`: + `redact_full_tins` returns its input unchanged when it finds no run, + exactly when `has_full_tin` is false, so the guard only saves a copy. + +### Round 4 (2026-10-17) + +`cargo mutants --in-diff` on this round's changes (replay restored to +main's rules, derived figures checked, the old-books contracts), per +crate, output under `~/.cache/wanderbooks/mutants/p0-r4-` +(`MCP_CASES=16`, `OLD_BOOKS_CASES=1`, `STORE_CASES=64`, +`PROPTEST_MAX_SHRINK_ITERS=0`; the GUI's old-books test over the edge +books only, `OLD_BOOKS_ONLY=x_draft_max_lines,x_schedule_chrono_end,...`, +since `asset_long_life` alone takes three minutes a run): + +| Crate | Mutants | Caught | Missed, then killed | Equivalent | Timeouts | Unviable | +|---|---|---|---|---|---|---| +| `ledger-core` (tests of core and store) | 176 | 153 | 6 | 3 | 0 | 14 | +| `ledger-store` | 12 | 11 | 0 | 0 | 0 | 1 | +| `ledger-mcp` | 81 | 13 | 5 | 1 | 0 | 62 | +| `ledger-config` | 7 | 7 | 0 | 0 | 0 | 0 | +| `ledger-gui` | 221 | 47 | 137 | 11 | 7 | 19 | + +- **Killed (core).** `name_payroll_parties` (replaced by `Ok(())`, and + `==` to `!=` in merging one employee's lines): a payroll entry names + its employees, each with their net pay, live and on replay + (`spec_parties.rs` `a_payroll_entry_names_the_employees_it_paid`); + `entry_flow`'s `across_left -= take` (`+=`, `/=`): across is used up + in order (`entry_flow_takes_across_in_order_until_used_up`); + `share_target`'s debit filter (`==` to `!=`): an unbalanced draft + moving no money splits over its debits + (`a_share_target_without_money_is_the_debits`); `resolve`'s capital + debit sign: members' derived shares net their capital lines + (`derived_member_shares_net_their_capital_lines`). These were in code + this round touched only to make it checked; the core and store tests + never reached them (the MCP tests did). +- **Killed (MCP).** `lines_settled` (whole and in parts): an empty, an + unbalanced and a Decimal-overflowing draft are not settled, a + balanced draft and a posted entry are (`server.rs` + `settled_lines_are_posted_or_balanced_drafts`). +- **Killed (GUI).** The pages' display of what can't be computed and + of the edges was barely asserted: new tests in `tests/edges.rs` and + beside the pages (`test_support.rs` renders a page headless and reads + its painted text and shapes) cover the runway and "coming up" on the + cash page, the balance chart's labels and hover, an entry's totals + (balanced, out of balance, too large to total), a party's span and + monthly chart at chrono's edges, a split entry's part, the register's + reconciliation colours, the company page's cards, the report range, + prior period and column limit, and the transaction row. The rerun + (`p0-r4-gui-rerun`) left only the equivalents. +- **Equivalent (GUI, 11).** `party_span`'s `<` to `<=` (twice): they + differ only at year 0, which chrono holds, so the fallback is never + taken. The asset notice's `>` to `>=`: with nothing unposted both + amounts are 0 and nothing is pushed. `occurrences_from`'s five + arithmetic mutants: each leaves `k0` a lower bound on the first + occurrence on or after `from`, so only the walk's length changes. The + cash forecast's `>` to `>=`: a zero amount added to inflow instead of + subtracted from outflow. The company page's `total.is_zero()` guard: + a schedule's total is always positive. Its recurring total's `==` to + `!=`: a template always balances, so its credits sum to its debits. +- **Equivalent.** `entry_flow`'s filters `v > 0` to `>= 0` and `v < 0` + to `<= 0`: they only add zeros to a sum. `split_first`'s + `weights.is_empty() || total.is_zero()` to `&&`: every weight is + positive (a percent above 0, a member's share checked above 0), so a + non-empty list never sums to zero. `lines_settled`'s side filter + `l.side == s` to `!=`: it swaps which sum is called debits, and the + comparison and the overflow refusal are symmetric. +- **A real defect found while writing these tests:** the depreciation + true-up named its final month with chrono's `%Y`, which signs a year + past 9999 ("+10004-03"), while the lines don't, so an asset whose life + 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`). + ## Benchmarks (baseline 2026-10-13) No budget, by decision (Stephen, 2026-10-13: the books do little work diff --git a/docs/verification.md b/docs/verification.md index cd64530..742dc6b 100644 --- a/docs/verification.md +++ b/docs/verification.md @@ -215,6 +215,20 @@ Be precise about the claims: (those have their own property tests), and persistence (the journal store's hash chain is tested in `ledger-store`). +### P0 guard rails (2026-10-16) + +P0 (`plan/served.md`) added no kernel arithmetic and no new law about +balances, so it added no Kani harness and no Lean theorem; nothing here +was weakened. What it added is checked by tests and properties (listed in +`docs/testing.md`, "P0 guard rails"): the journal format gate (newer is +never called corrupt, damage always is; the envelope and its hash are +frozen across formats, rules.md B-27), the server failing closed after a +panic, the import roots' lockdown (a property over generated paths, and a +component walk that refuses a folder swapped for a link), files with full +TINs kept out of the books (B-26), and the agent text lint. Out of scope +for proof today: the format gate and the walk are I/O, and the model in +`verify/lean` stops at the ledger. + ## Running it ```sh