diff --git a/crates/ledger-core/src/error.rs b/crates/ledger-core/src/error.rs index e99bc13..b33d304 100644 --- a/crates/ledger-core/src/error.rs +++ b/crates/ledger-core/src/error.rs @@ -854,6 +854,12 @@ pub enum LedgerError { #[error("{0}")] InvalidVoid(String), + /// A draft's state or discard was refused: the message says why (a + /// note or reason that breaks the books' text rule, no reason given). + /// Plan P4, rules.md B-43. + #[error("{0}")] + InvalidDraft(String), + /// A void invoice can't be recorded as sent: it was never a document /// the customer should have received (plan P4b S5, B-38). #[error("invoice {0} is void: a void invoice was never sent")] diff --git a/crates/ledger-core/src/journal.rs b/crates/ledger-core/src/journal.rs index 4e26972..b6b2b30 100644 --- a/crates/ledger-core/src/journal.rs +++ b/crates/ledger-core/src/journal.rs @@ -23,6 +23,55 @@ pub enum EntryStatus { Posted, } +/// Where a draft entry stands (plan P4, `drafts_v2`): still being built, +/// or finished and waiting on the document that supports it (rules.md +/// B-43). Meaningful while the entry is a draft; a posted entry keeps +/// the state it had and nothing reads it. +#[derive(Clone, Debug, Default, PartialEq, Eq, Serialize, Deserialize)] +pub enum DraftState { + /// Lines are still being added. What every draft starts as. + #[default] + Building, + /// The lines are final and the entry waits for its receipt or other + /// evidence; `note` says what is awaited (empty: nothing said). + AwaitingEvidence { + /// What the draft waits on, in the words of whoever set the state. + note: String, + }, +} + +impl DraftState { + /// Its key as the journal, the tools and the viewer name it: + /// `building` or `awaiting_evidence`. + pub fn key(&self) -> &'static str { + match self { + DraftState::Building => "building", + DraftState::AwaitingEvidence { .. } => "awaiting_evidence", + } + } + + /// [`Self::key`] the other way, with the note an awaiting state + /// carries; `None` for a state this version doesn't know (a newer + /// version's). + pub fn parse(key: &str, note: &str) -> Option { + match key { + "building" => Some(DraftState::Building), + "awaiting_evidence" => Some(DraftState::AwaitingEvidence { + note: note.to_string(), + }), + _ => None, + } + } + + /// The note an awaiting state carries; empty for building. + pub fn note(&self) -> &str { + match self { + DraftState::Building => "", + DraftState::AwaitingEvidence { note } => note, + } + } +} + /// One debit or credit line of a journal entry. #[derive(Clone, Debug, Serialize, Deserialize, PartialEq)] pub struct JournalLine { @@ -59,6 +108,10 @@ pub struct JournalEntry { lines: Vec, status: EntryStatus, reversal_of: Option, + /// Where the draft stands (`entry.draft_state_set`); meaningful while + /// `status` is `Draft`. + #[serde(default)] + draft_state: DraftState, } impl JournalEntry { @@ -72,6 +125,7 @@ impl JournalEntry { lines: Vec::new(), status: EntryStatus::Draft, reversal_of: None, + draft_state: DraftState::Building, } } @@ -100,6 +154,12 @@ impl JournalEntry { self.status } + /// Where a draft stands (plan P4): building, or awaiting evidence. + /// Meaningful while the entry is a draft. + pub fn draft_state(&self) -> &DraftState { + &self.draft_state + } + /// If this entry reverses another, the reversed entry's id. pub fn reversal_of(&self) -> Option { self.reversal_of @@ -116,9 +176,17 @@ impl JournalEntry { self.lines[index].class_id = class_id; } + /// Set the draft's state. Only while drafted; only via + /// [`crate::Ledger::set_draft_state`]. + pub(crate) fn set_draft_state(&mut self, state: DraftState) { + self.draft_state = state; + } + /// Mark posted. Only via [`crate::Ledger`], after [`Self::validate`]. pub(crate) fn mark_posted(&mut self) { self.status = EntryStatus::Posted; + // A posted entry waits on nothing: its state is the canonical one. + self.draft_state = DraftState::Building; } /// Link this entry as the reversal of another. Only via [`crate::Ledger`]. diff --git a/crates/ledger-core/src/ledger.rs b/crates/ledger-core/src/ledger.rs index 8834994..c1ad4e5 100644 --- a/crates/ledger-core/src/ledger.rs +++ b/crates/ledger-core/src/ledger.rs @@ -355,6 +355,11 @@ pub struct Ledger { /// What each entry settles (`entry.settles`, plan P6): the one record /// a member-paid entry's "reimbursed" is derived from (IZ-18). entry_settles: std::collections::BTreeMap>, + /// The journal line that posted each posted entry (`entry.posted` or + /// `entry.reversed`, plan P4): what "posted since seq N" is read from, + /// backdated entries included. An entry the journal's own posting + /// line doesn't name (none today) has no place here. + posted_seq: std::collections::BTreeMap, } impl Ledger { @@ -411,6 +416,7 @@ impl Ledger { conventions: crate::conventions::Conventions::default(), annotations: std::collections::BTreeMap::new(), entry_settles: std::collections::BTreeMap::new(), + posted_seq: std::collections::BTreeMap::new(), } } @@ -826,6 +832,7 @@ impl Ledger { ("conventions", self.conventions == other.conventions), ("annotations", self.annotations == other.annotations), ("entry_settles", self.entry_settles == other.entry_settles), + ("posted_seq", self.posted_seq == other.posted_seq), ] .into_iter() .filter(|(_, same)| !same) @@ -1977,6 +1984,131 @@ impl Ledger { Ok(()) } + /// Set where a draft stands: still being built, or awaiting its + /// evidence (plan P4, rules.md B-43). A state is a note on the draft + /// and moves no figure; the draft's lines are what they were. + /// + /// ```text + /// GOAL: let a draft say it is finished and waiting on a document, + /// so it is neither lost nor mistaken for work in progress. + /// SOURCE: docs/spec/rules.md B-43 (DECISION D-47: a draft waits on + /// evidence; the evidence is checked when it posts); IRS + /// Pub. 583 "supporting documents". + /// INVARIANTS: + /// 1. Only a draft has a state: a posted entry is refused + /// (PostedEntryImmutable), an unknown one too (UnknownEntry). + /// 2. The note passes parties::check_text (no full TIN, no control + /// characters, at most 500 characters). + /// 3. No line, balance or report moves; a refusal changes nothing. + /// ``` + pub fn set_draft_state( + &mut self, + entry: EntryId, + state: crate::DraftState, + ) -> Result<(), LedgerError> { + if let crate::DraftState::AwaitingEvidence { note } = &state { + crate::parties::check_text("the note", note).map_err(LedgerError::InvalidDraft)?; + } + self.draft_mut(entry)?.set_draft_state(state); + Ok(()) + } + + /// [`Self::set_draft_state`] as journaled, for replay (rules.md + /// B-28): the state is restored on a draft that exists; a state + /// naming an entry since posted or discarded is refused like the + /// command, which journal order makes impossible. + #[doc(hidden)] + pub fn replay_set_draft_state( + &mut self, + entry: EntryId, + state: crate::DraftState, + ) -> Result<(), LedgerError> { + self.draft_mut(entry)?.set_draft_state(state); + Ok(()) + } + + /// Throw a draft away, with the reason (plan P4, rules.md B-43): the + /// only way out of an open draft that will never post, and so the way + /// a period it holds open can close. The draft was never in the books, + /// so no balance moves; the id is spent (ids are never reused); the + /// journal still holds its lines and why it went. + /// + /// ```text + /// GOAL: remove a draft that will not post, leaving the books and + /// every id as they were. + /// SOURCE: docs/spec/rules.md B-43; B-8 (a posted entry is never + /// removed: only a draft is); Lean Step.discard. + /// INVARIANTS: + /// 1. Only a draft is discarded: a posted entry is refused + /// (EntryAlreadyPosted), an unknown one too (UnknownEntry). + /// 2. The reason is not empty and passes parties::check_text. + /// 3. Posted entries, their order, every balance and every id + /// allocator are as they were; what was recorded about the draft + /// itself (its vendor, instrument, parties, settlements) goes + /// with it. + /// SCENARIOS: + /// 1. IF a period holds the draft open: after it, the period can + /// close (the Lean hypothesis hdrafts). + /// ``` + pub fn discard_draft(&mut self, entry: EntryId, reason: &str) -> Result<(), LedgerError> { + if reason.trim().is_empty() { + return Err(LedgerError::InvalidDraft( + "a discarded draft needs a reason".to_string(), + )); + } + crate::parties::check_text("the reason", reason).map_err(LedgerError::InvalidDraft)?; + self.replay_discard_draft(entry) + } + + /// [`Self::discard_draft`] as journaled, for replay: the draft goes. + #[doc(hidden)] + pub fn replay_discard_draft(&mut self, entry: EntryId) -> Result<(), LedgerError> { + let e = self + .entries + .get(&entry) + .ok_or(LedgerError::UnknownEntry(entry))?; + if e.status() != EntryStatus::Draft { + return Err(LedgerError::EntryAlreadyPosted(entry)); + } + self.entries.remove(&entry); + self.entry_vendors.remove(&entry); + self.entry_instruments.remove(&entry); + self.entry_parties.remove(&entry); + self.entry_no_party.remove(&entry); + self.entry_settles.remove(&entry); + Ok(()) + } + + /// The journal line (`seq`) that posted `entry`: `entry.posted` or + /// `entry.reversed`. `None` for a draft, an unknown entry, or books + /// read by a path that doesn't carry the sequence (plan P4). + pub fn posted_seq(&self, entry: EntryId) -> Option { + self.posted_seq.get(&entry).copied() + } + + /// Record the journal line that posted `entry` (the store, live and + /// on replay, after the posting line's own command). Idempotent for + /// the same line; a second, different line is ignored (the first + /// posting stands). + #[doc(hidden)] + pub fn note_posted_seq(&mut self, entry: EntryId, seq: u64) { + self.posted_seq.entry(entry).or_insert(seq); + } + + /// Draft entries in id order, with their state. + pub fn drafts(&self) -> Vec<&JournalEntry> { + let mut ids: Vec = self + .entries + .values() + .filter(|e| e.status() == EntryStatus::Draft) + .map(|e| e.id()) + .collect(); + ids.sort_unstable(); + ids.into_iter() + .filter_map(|i| self.entries.get(&i)) + .collect() + } + /// Look up an entry by id (draft or posted). pub fn get_entry(&self, entry: EntryId) -> Option<&JournalEntry> { self.entries.get(&entry) diff --git a/crates/ledger-core/src/lib.rs b/crates/ledger-core/src/lib.rs index 85ccbb9..6bea26e 100644 --- a/crates/ledger-core/src/lib.rs +++ b/crates/ledger-core/src/lib.rs @@ -76,7 +76,7 @@ pub use form1099::{ Vendor1099Line, Vendor1099Report, vendor_1099_report, }; pub use instruments::{Instrument, InstrumentId, InstrumentKind}; -pub use journal::{EntryId, EntryStatus, JournalEntry, JournalLine}; +pub use journal::{DraftState, EntryId, EntryStatus, JournalEntry, JournalLine}; pub use kernel::{EntryFlows, Flow}; pub use ledger::{ BAD_DEBTS, ControlAccount, GENERAL_EXPENSES, Ledger, PAYABLES, PAYMENT_PROCESSING_FEES, diff --git a/crates/ledger-core/tests/invariants.rs b/crates/ledger-core/tests/invariants.rs index 09a078e..76bead9 100644 --- a/crates/ledger-core/tests/invariants.rs +++ b/crates/ledger-core/tests/invariants.rs @@ -1609,3 +1609,75 @@ fn replayed_documents_and_payments_rebuild_the_records() { assert_eq!(b.status, DocumentStatus::Paid); assert_eq!(l.entry_vendor(last), Some(v)); } + +// --------------------------------------------------------------------------- +// Drafts: a state, and a way out (plan P4, rules.md B-43). +// --------------------------------------------------------------------------- + +/// Spec (rules.md B-43; Lean `Step.discard` and `hdrafts`): a period with +/// an open draft can't close; once the draft is discarded it can, and +/// nothing posted moved: balances, order and ids are as they were. +#[test] +fn discard_unblocks_close() { + let c = fixture_company(); + let mut ledger = c.ledger.clone(); + let jan = ledger.create_period("2026-01", date(1), date(31)).unwrap(); + let draft = ledger.create_entry(date(20), "Figma annual plan"); + ledger + .add_line(draft, c.rent, Side::Debit, usd(40)) + .unwrap(); + ledger + .add_line(draft, c.cash, Side::Credit, usd(40)) + .unwrap(); + // A state is a note on the draft: it moves nothing and doesn't unblock. + ledger + .set_draft_state( + draft, + ledger_core::DraftState::AwaitingEvidence { + note: "invoice due from Figma".into(), + }, + ) + .unwrap(); + assert_eq!( + ledger.get_entry(draft).unwrap().draft_state().key(), + "awaiting_evidence" + ); + assert_eq!( + ledger.close_period(jan).unwrap_err(), + LedgerError::DraftsInPeriod(jan) + ); + let tb_before = snapshot(&ledger).unwrap(); + let posted_before: Vec = ledger.posted_entries().map(|e| e.id()).collect(); + let next_before = ledger.next_entry_id(); + // A reason is required; a posted entry is never discarded. + assert!(matches!( + ledger.discard_draft(draft, " "), + Err(LedgerError::InvalidDraft(_)) + )); + assert_eq!( + ledger.discard_draft(posted_before[0], "oops").unwrap_err(), + LedgerError::EntryAlreadyPosted(posted_before[0]) + ); + ledger.discard_draft(draft, "never billed").unwrap(); + assert!(ledger.get_entry(draft).is_none()); + assert_eq!(snapshot(&ledger).unwrap(), tb_before); + assert_eq!( + ledger.posted_entries().map(|e| e.id()).collect::>(), + posted_before + ); + assert_eq!(ledger.next_entry_id(), next_before, "ids are never reused"); + assert!(ledger.close_period(jan).unwrap().is_some()); + // A state on a posted entry, or on none, is refused. + assert_eq!( + ledger + .set_draft_state(posted_before[0], ledger_core::DraftState::Building) + .unwrap_err(), + LedgerError::PostedEntryImmutable + ); + assert_eq!( + ledger + .set_draft_state(9999, ledger_core::DraftState::Building) + .unwrap_err(), + LedgerError::UnknownEntry(9999) + ); +} diff --git a/docs/verification.md b/docs/verification.md index 7fb091a..7f55c9b 100644 --- a/docs/verification.md +++ b/docs/verification.md @@ -608,6 +608,28 @@ credit, and the bounds are the existing date-sum's). books built from empty); the cash-basis refusal is a policy on the books' settings, not arithmetic, and is tested, not modelled. +### Drafts: a discard moves no figure (P4) + +A draft's state (`Ledger::set_draft_state`) is a note on the draft and +changes no line, so the model keeps nothing for it (like a record, it is +outside the books' figures). `Ledger::discard_draft` removes a draft: a +new command, so a new Lean step, and no kernel function. + +38. **A discard moves no figure and takes only its draft.** `Step.discard` + removes one entry from `drafts`; the posted log, the chart, the + periods and the records are the very same, so every balance, report + and closing read from them is the same. `Inv.draftsOpen` is kept + (the drafts left were drafts before), `Step.extends` and + `Step.frozen` hold with no new argument, and a period with exactly + one draft inside it can close once that draft is discarded + (`Step.discard_unblocks_close`, the `hdrafts` hypothesis of + `Step.close`). + - Lean `Step.discard`, `Step.discard_keeps_books`, + `Step.discard_drafts`, `Step.discard_unblocks_close` (in + `Audit.lean`) · tests `discard_unblocks_close` (the engine's side: + a period with an open draft can't close, discarded it can, and + every balance and id is as it was). + ## What the proofs found The engine already had 190+ tests, property tests, mutation testing, diff --git a/verify/lean/Audit.lean b/verify/lean/Audit.lean index fd35b7e..5430e2d 100644 --- a/verify/lean/Audit.lean +++ b/verify/lean/Audit.lean @@ -101,3 +101,6 @@ open Wanderbooks #print axioms Documents.Reachable.control_is_documents #print axioms Documents.Step.writeOff_unattached #print axioms Documents.writeOff_within_bounds +#print axioms Step.discard_keeps_books +#print axioms Step.discard_drafts +#print axioms Step.discard_unblocks_close diff --git a/verify/lean/Wanderbooks/Ledger.lean b/verify/lean/Wanderbooks/Ledger.lean index 965d7f9..7252f46 100644 --- a/verify/lean/Wanderbooks/Ledger.lean +++ b/verify/lean/Wanderbooks/Ledger.lean @@ -129,6 +129,11 @@ inductive Step : Ledger → Ledger → Prop = net (closings (nominalCodes L.chart) (allLines (through p.stop L.posted)))) (id : Nat) : Step L { L with posted := L.posted ++ closingFor L p ts id, periods := closeIn p L.periods } + /-- `discard_draft`: a draft removed, with the reason it went. The + drafts shrink; the posted log, the chart, the periods and the records + are as they were, so no balance moves. -/ + | discard (L : Ledger) (e : Entry) (hd : e ∈ L.drafts) : + Step L { L with drafts := L.drafts.filter (· ≠ e) } /-- `apply_settings`, `apply_convention`, `apply_decision`, `apply_open_item`, `apply_approval` and their retirements and resolutions, and the 1099 records `set_vendor_1099`, @@ -242,6 +247,10 @@ theorem Step.inv {L L' : Ledger} (s : Step L L') (h : Inv L) : Inv L' := by rcases closedOn_closeIn L p d.date hcl with hcl | ⟨-, hc⟩ · exact h.draftsOpen d hd hcl · simp [hdrafts d hd] at hc + | discard e hd => + refine ⟨h.distinct, h.accepted, h.known, ?_⟩ + intro d hd' + exact h.draftsOpen d ((List.mem_filter.1 hd').1) | record r => exact ⟨h.distinct, h.accepted, h.known, h.draftsOpen⟩ /-- **The invariant holds in every reachable state.** -/ @@ -310,6 +319,7 @@ theorem Step.extends {L L' : Ledger} (s : Step L L') : ∃ t, L'.posted = L.post | reverse e _ r => exact ⟨[r], rfl⟩ | openPeriod => exact ⟨[], by simp⟩ | close p _ _ _ _ _ ts _ _ id => exact ⟨closingFor L p ts id, rfl⟩ + | discard => exact ⟨[], by simp⟩ | record => exact ⟨[], by simp⟩ /-- Any number of steps. -/ @@ -328,6 +338,39 @@ theorem Steps.extends {L L' : Ledger} (s : Steps L L') : ∃ t, L'.posted = L.po obtain ⟨u, hu⟩ := s.extends exact ⟨t ++ u, by rw [hu, ht, List.append_assoc]⟩ +/-! ## A discarded draft takes nothing with it -/ + +/-- **A discard moves no figure**: the posted log, the chart and the +periods are the very same, so every balance, report and closing read from +them is the same too. -/ +theorem Step.discard_keeps_books (L : Ledger) (e : Entry) : + ({ L with drafts := L.drafts.filter (· ≠ e) } : Ledger).posted = L.posted + ∧ ({ L with drafts := L.drafts.filter (· ≠ e) } : Ledger).chart = L.chart + ∧ ({ L with drafts := L.drafts.filter (· ≠ e) } : Ledger).periods = L.periods := + ⟨rfl, rfl, rfl⟩ + +/-- **A discard removes the draft and only it**: afterwards `e` is no +draft, and every draft left was a draft before. -/ +theorem Step.discard_drafts (L : Ledger) (e : Entry) : + e ∉ L.drafts.filter (· ≠ e) ∧ ∀ d ∈ L.drafts.filter (· ≠ e), d ∈ L.drafts := by + refine ⟨?_, fun d hd => (List.mem_filter.1 hd).1⟩ + intro h + simpa using (List.mem_filter.1 h).2 + +/-- **Discarding unblocks a close**: if every draft left after a discard +is outside the period `p`, then the draft discarded was the only one in it +(the `hdrafts` hypothesis of `Step.close` holds once the drafts in `p` +are discarded). -/ +theorem Step.discard_unblocks_close (L : Ledger) (p : Period) (e : Entry) + (hin : ∀ d ∈ L.drafts, p.contains d.date = true → d = e) : + ∀ d ∈ L.drafts.filter (· ≠ e), p.contains d.date = false := by + intro d hd + obtain ⟨h1, h2⟩ := List.mem_filter.1 hd + have hne : d ≠ e := by simpa using h2 + cases hc : p.contains d.date with + | false => rfl + | true => exact absurd (hin d h1 hc) hne + /-! ## Closed periods are frozen -/ /-- Entries dated in a period. -/