From d74ee1e9620f45b1d21b7c74b54cfb72a35741dc Mon Sep 17 00:00:00 2001 From: Stephen Waits Date: Tue, 27 Oct 2026 12:45:01 -0600 Subject: [PATCH] docs(plan): P4b S7 as built (P4b S7) The unit's As-built block: where the build departed from its text, and why (the bad_debts role, the least-owed bound over the date-sum, the evidence rule, the handbook section it had to create, the bookspec schema's write_off event, and where the tests live). The Build text is untouched; the EM moves the status row. --- plan/served.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/plan/served.md b/plan/served.md index 65948c9..8a15c12 100644 --- a/plan/served.md +++ b/plan/served.md @@ -1375,7 +1375,15 @@ Each unit follows the 8.0.4 template. "A-n" is an owner answer numbered in 8.3.1 5. **Files:** owns `Ledger::write_off`, the event's arms, `books.write_off_invoice`, `Step.writeOff`; touches the 8.0.3 files. 6. **Tests and proofs:** named above; Lean `writeOff_within_bounds`; no kernel change. 7. **Done when:** (1) the tests pass; (2) `just prove` green with the new theorem in `Audit.lean`; (3) 8.0.6 in the PR; (4) the handbook says when to void, write off or reverse; (5) `just check` green. -8. **As built:** none yet. +8. **As built** (2026-10-27, `d5af44b9`, `62f2fb05`, `4e71cf63`, `0f1c7786`, `b731d7ed`, `03227786`, `e801908a`, `f31dd264`, `22cdfcf3`, `176baa52`): departures only, the Build text above untouched. + - The `bad_debts` role had no engine constant (8.3.4's table names it, but only S7 needed it): `ledger_core::BAD_DEBTS` (6990 Bad Debt Expense, an Expense control role) is added and joined to `control_accounts()`, so `books.roles` and `books.assign_role` see it. + - The amount bound is the least the invoice owes on any day from the write-off's on (`least_owed_from`, the helper `payment_room` now shares), not only its outstanding on the day: a write-off dated before a payment that later settles it would otherwise take the document below nothing at that later day (B-38 INVARIANT 2). The refusal says what is owed and, when a later payment lowers it, what can be written off. + - The evidence given as `existing_attachment_id` must be an attachment not yet on an entry: one already filed against another entry would be one receipt counted twice (the refusal `link_receipt` gives, B-38's own invariant 5). An upload's bytes are put in the content-addressed store before the first journal line, as the issued invoice's PDF is (S4.3). + - The handbook section `invoices-and-bills` did not exist yet (S4.5 owns it and has not landed), so this unit created it with step 4 and the two recovery procedures; S4.5 adds steps 1-3 and 5 around them, in its own reading position. + - bookspec had no way to state a write-off: the example schema gained the dated `write_off = { invoice, amount?, reason }` event (the invoice named by its event, as `reverses` names one), and a `refused` `lines` entry, which the adapter rehearses on a clone so a refusal journals nothing; `older` and `refused` never combine. The loader's refusal vocabulary gained `untagged_control_line` (B-38), as the unit says. `bad-debt-direct-write-off` states B-41 (its bookspec status moves from "allocated" to CHOICE); `arap-hand-control-posting-refused` states B-38's control guard and its legacy-line replay. + - The store tests went into `tests/arap_standing.rs` (where R-A puts the feature-wait test) and the over-the-wire tests opened `crates/ledger-cli/tests/documents.rs` (its allocated file); `arap_props.rs` gained `Op::WriteOff`. + - `docs/verification.md`'s "out of scope" list no longer says A/R and A/P documents are unproved: S1's `Documents` model exists, and S7 adds the write-off step to it. + - There is no `books.adopt_control_line`, no `books.assign_role { move_balance }` and no `Movement::Recovery` (D-49, 8.4), as the unit says. **Deferred from S7 (D-49, recorded in 8.4):** `books.adopt_control_line` and `books.assign_role { move_balance }`. 8.3.14 item 4 already gives two remedies for a legacy hand line on 1200 or 2000 that need no code: reverse it and re-enter it as a document while its period is open; or leave it, record a decision, and let the CPA README footnote it (the identity's `unattached` term exists for exactly this). Build the tools only if `books.control_check` on the owner's books lists a line neither remedy can take; then the EM writes a unit for them with a Lean `Step.adopt` and a per-account `owed_on` identity (8.4 has the notes).