From ad649be3d5620fcf22e477555175269b74233425 Mon Sep 17 00:00:00 2001 From: Stephen Waits Date: Tue, 27 Oct 2026 13:46:43 -0600 Subject: [PATCH] docs: S5 step 4 landed; attention predicates in the test record (P4b S5) The As-built block records step 4 built after U0b, its two items and their tests; docs/testing.md names them and what P12 must mutate (the number exemption, the open/partial check, sends.is_empty(), the two day comparisons with their checked date arithmetic, the last-send max); docs/parity.md says sent tracking also feeds Needs attention. --- docs/parity.md | 6 +++++- docs/testing.md | 25 +++++++++++++++++++------ plan/served.md | 3 ++- 3 files changed, 26 insertions(+), 8 deletions(-) diff --git a/docs/parity.md b/docs/parity.md index 50450f8..562cad0 100644 --- a/docs/parity.md +++ b/docs/parity.md @@ -115,4 +115,8 @@ reference, for an owner or a delegate such as an agent. The record is `invoice.sent`, under `documents_v2` (D-52), and it moves no figure, so the A/R and A/P rows' figures are unchanged. The floor never decreases: the row is `done`, tested by `sends_replay_and_project`, -`a_send_changes_no_figure` and `mark_sent_records_who_and_how`. +`a_send_changes_no_figure` and `mark_sent_records_who_and_how`. Sent +tracking also feeds Needs attention: an issued invoice nobody marked sent +(past `invoicing.unsent_days`) and an overdue invoice not reminded within +`invoicing.reminder_days` are one list in the viewer and in `books.start`, +each offering `books.mark_sent` (step 4; U0b's one engine). diff --git a/docs/testing.md b/docs/testing.md index 53f302d..4b53918 100644 --- a/docs/testing.md +++ b/docs/testing.md @@ -3069,7 +3069,7 @@ one line and no entry, replay restores it and the projection keeps it in before and after), `mark_sent_on_void_refused` (`DocumentVoid`, nothing journaled; a send dated before the void is taken). - **`ledger-store` `tests/arap_props.rs`:** `status_is_a_function_of_journal_and_date` - gains `Op::Sent` (random sends on invoices, skipped on bills): every + gains `Op::MarkSent` (random sends on invoices, skipped on bills): every figure, the control check and both agings still agree across live, replay and snapshot. - **`ledger-store` `tests/format.rs`:** `an_older_version_stops_at_invoice_sent` @@ -3087,6 +3087,17 @@ one line and no entry, replay restores it and the projection keeps it in total). - **`ledger-mcp/src/handbook.rs`:** the new `invoices-and-bills` section renders, and its id is unique (the existing handbook tests). +- **Step 4, Attention (R-F):** `ledger-gui/tests/invoices.rs`: + `an_unsent_invoice_is_listed_until_a_send_clears_it` (an issued invoice + past `invoicing.unsent_days` is one to-do opening the invoice; the + overview draws it, `attention-unsent-invoice.png`; a send clears it), + `a_legacy_invoice_with_no_number_is_never_listed_as_unsent` (exempt), + `an_overdue_invoice_with_an_old_send_is_asked_to_remind` (due Mar 1, + last sent Feb 20: 14 days overdue, target the invoice, prompt names + `books.mark_sent`). `ledger-cli/tests/attention_parity.rs`: + `an_unsent_invoice_is_on_both_lists` (the viewer's list and `books.start` + both carry the item, and the step is `books.mark_sent` on `invoice:1`). + `the_viewer_and_books_start_see_the_same_attention` stays green. **For P12 (mutation targets):** `Ledger::mark_sent`'s refusals (unknown invoice, a send dated before it, `DocumentVoid`, empty `to`, and each of @@ -3096,8 +3107,10 @@ its `other:` prefix; `SendKind::parse`'s two arms; `sent_via`'s arms and its empty fallback; `send_kind`'s error arm; the handler's `kind` default (`original` when `sends` is empty, `reminder` after), its `to` fallback (bill-to, then party, then refused) and its `by` fallback; `invoice_id`'s -`invoice:` strip; `last_sent`'s `max`; and the replay reader's -`newer_content` arms for an unknown channel or kind. The two attention -predicates ("invoice never sent", "overdue invoice not reminded") and -their day comparisons are deferred with the unit's step 4 until U0b -lands, and are named here when they do. +`invoice:` strip; `last_sent`'s `max`; the replay reader's +`newer_content` arms for an unknown channel or kind; and the two attention +predicates in `ledger-package::attention`: `invoice.number.is_some()` +(the legacy exemption), `Open | Partial`, `sends.is_empty()`, the +`checked_add_days` `unsent_days` comparison (`>`), `overdue_days > 0`, the +`sends.max()` last send, and the `reminder_days` comparison (`>`), plus +each item's target (`Target::Invoice`) and `books.mark_sent` step args. diff --git a/plan/served.md b/plan/served.md index 3169370..aeb1507 100644 --- a/plan/served.md +++ b/plan/served.md @@ -1339,8 +1339,9 @@ Each unit follows the 8.0.4 template. "A-n" is an owner answer numbered in 8.3.1 5. **Files:** owns the `Sent` types and `Ledger::mark_sent`, the `invoice.sent` arms, `books.mark_sent`; touches the 8.0.3 files. 6. **Tests and proofs:** named above; no kernel change, no Lean change (a send moves no money). 8.0.6 items 1-4, 6. 7. **Done when:** (1) the tests pass; (2) a send on a fixture book changes no report and no `DocState` (`a_send_changes_no_figure`); (3) an older version stops at the `invoice.sent` line with `NewerJournal` (the `tests/format.rs` arm); (4) `just check` green; (5) attention parity holds. -8. **As built** (2026-10-27, branch `S5`): Build steps 1-3 and 5 are done; **step 4 (the two attention items) is deferred until U0b lands** (8.0.5 R-F: no attention item before it), as the EM directed. Departures: +8. **As built** (2026-10-27, branch `S5`): Build steps 1-5 are done. ~~step 4 (the two attention items) is deferred until U0b lands~~ → built after U0b landed (`cc4f104f`), on main `ed637f0e` (D-55). Departures: - ~~no Lean change (a send moves no money)~~ → AGENTS.md's formal-methods bar (I-13) wins: `Ledger::mark_sent` is a new `Ledger` command, so `verify/lean/Wanderbooks/Documents.lean` gains `sends` on `Books`, `Step.markSent` and `Step.markSent_changes_no_figure` (no axioms), listed in `Audit.lean` and in `docs/verification.md` rule 34. + - Step 4: `ledger-package::attention` gains `Target::Invoice` and two items, `invoice_never_sent` (an issued invoice still Open or Partial, no send, past `invoicing.unsent_days`; a legacy invoice with no number is exempt) and `invoice_not_reminded` (overdue, last send older than `invoicing.reminder_days`); both are Todo, open the invoice, and offer `books.mark_sent` with the invoice. The viewer maps the target (one line in its Target→Route table; it owns no item) and draws them; `books.start` turns them into next steps from the one function. Tests: `an_unsent_invoice_is_listed_until_a_send_clears_it` (`attention-unsent-invoice.png`), `a_legacy_invoice_with_no_number_is_never_listed_as_unsent`, `an_overdue_invoice_with_an_old_send_is_asked_to_remind`, `an_unsent_invoice_is_on_both_lists`; `the_viewer_and_books_start_see_the_same_attention` stays green. - The MCP parameter for the recipients is `recipients`, not `to`: `no_tool_takes_a_path` refuses a parameter named `to` (a whole-word path-name rule, I-2). The journal event and the result keep the plan's `to`. - `Ledger::mark_sent` also passes `note` through `parties::check_text`, beside `to` and `reference`: a note must not carry a full TIN (I-7). - `LedgerError::DocumentVoid` (the plan's name) and `LedgerError::InvalidSend` (the text refusals) are new variants.