From fb3b4ab476ad6daf74cc97482ea323f7a1c5f45c Mon Sep 17 00:00:00 2001 From: Stephen Waits Date: Tue, 13 Oct 2026 18:58:21 -0600 Subject: [PATCH] closes: a run of members closes splits cumulatively Each close into members' capital rounded on its own, ties to the earlier member, so twelve monthly 50/50 closes of odd-cent income could leave one member several cents ahead of half the year (docs/testing.md #12, found with the members' equity fix). - CloseTo::Members now splits cumulatively over a run (closes back to back with the same members and shares): each close gives a member allocate(run total so far) - allocate(run total before). Periods record their close order and a cumulative close's members and net (Period::close_seq, member_close) so the next close continues the run and replay recomputes it exactly. A close to anything else, or other shares, ends the run. - Journaled "rounding": "cumulative". The per-close rule is kept as CloseTo::MembersPerClose for closes journaled "largest_remainder"; older closes still replay with the last member absorbing it. - Lean: runPart_telescopes (a member's total from a run is their allocation of the run's total) and closePart_total (each close hands out exactly its net), audited to the standard axioms. - Tests: hand-computed three one-cent months (per close A 0.03 / B 0; cumulative A 0.02 / B 0.01), a run ending, a property that each member stays within a cent of their share (fails on the per-close rule), and a store contract that each rule journals and replays as itself. Wanderland's books have no closes yet, so all of theirs use the new rule. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX --- crates/ledger-core/src/ledger.rs | 64 ++++++++- crates/ledger-core/src/lib.rs | 4 +- crates/ledger-core/src/periods.rs | 26 +++- crates/ledger-core/tests/statements.rs | 174 +++++++++++++++++++++++++ crates/ledger-store/src/store.rs | 21 ++- crates/ledger-store/tests/store.rs | 66 ++++++++++ docs/spec/rules.md | 16 ++- docs/testing.md | 2 +- docs/verification.md | 7 + verify/lean/Audit.lean | 2 + verify/lean/Wanderbooks/Closing.lean | 50 +++++++ 11 files changed, 416 insertions(+), 16 deletions(-) diff --git a/crates/ledger-core/src/ledger.rs b/crates/ledger-core/src/ledger.rs index 44f240b..08f9421 100644 --- a/crates/ledger-core/src/ledger.rs +++ b/crates/ledger-core/src/ledger.rs @@ -1294,6 +1294,8 @@ impl Ledger { end, status: PeriodStatus::Open, closing_entry: None, + close_seq: None, + member_close: None, }, ); Ok(id) @@ -1417,13 +1419,23 @@ impl Ledger { sweep(*a, *into, self); } } - periods::CloseTo::Members(members) | periods::CloseTo::MembersLastAbsorbs(members) => { + periods::CloseTo::Members(members) + | periods::CloseTo::MembersPerClose(members) + | periods::CloseTo::MembersLastAbsorbs(members) => { let shares: Vec = members.iter().map(|m| m.share).collect(); let parts = match to { periods::CloseTo::MembersLastAbsorbs(_) => { periods::allocate_last_absorbs(net, &shares) } - _ => periods::allocate(net, &shares), + periods::CloseTo::MembersPerClose(_) => periods::allocate(net, &shares), + _ => { + // Cumulative: what the run gives each member with + // this close, less what it gave them before. + let before = self.member_close_run(&member_key(members)); + let after = periods::allocate(before + net, &shares); + let prior = periods::allocate(before, &shares); + after.iter().zip(&prior).map(|(a, p)| a - p).collect() + } }; for (m, part) in members.iter().zip(parts) { equity.push((m.capital, part)); @@ -1462,12 +1474,46 @@ impl Ledger { Some(entry) }; + let close_seq = self + .periods + .values() + .filter(|p| p.status == PeriodStatus::Closed) + .count() as u64 + + 1; let p = self.periods.get_mut(&id).expect("period exists"); p.status = PeriodStatus::Closed; p.closing_entry = closing_entry; + p.close_seq = Some(close_seq); + p.member_close = match to { + periods::CloseTo::Members(members) => Some(periods::MemberCloseRecord { + members: member_key(members), + net, + }), + _ => None, + }; Ok(closing_entry) } + /// The net closed by the run of cumulative members closes, with exactly + /// these members and shares, that ends with the latest close: zero if + /// the latest close was anything else (or there is none). + fn member_close_run(&self, members: &[(AccountId, Decimal)]) -> Decimal { + let mut closed: Vec<&periods::Period> = self + .periods + .values() + .filter(|p| p.status == PeriodStatus::Closed) + .collect(); + closed.sort_by_key(|p| std::cmp::Reverse(p.close_seq)); + let mut total = Decimal::ZERO; + for p in closed { + match &p.member_close { + Some(r) if r.members == members => total += r.net, + _ => break, + } + } + total + } + /// Revenue and expense balances as of `end` as closing lines (code /// order), and the net income they carry (revenue debits minus expense /// credits). @@ -1519,7 +1565,9 @@ impl Ledger { accounts.push(*into); accounts.extend(sweep); } - periods::CloseTo::Members(members) | periods::CloseTo::MembersLastAbsorbs(members) => { + periods::CloseTo::Members(members) + | periods::CloseTo::MembersPerClose(members) + | periods::CloseTo::MembersLastAbsorbs(members) => { let total: Decimal = members.iter().map(|m| m.share).sum(); if members.is_empty() || total != Decimal::ONE @@ -1623,7 +1671,9 @@ impl Ledger { let sweeps: Vec = match to { periods::CloseTo::RetainedEarnings { sweep } | periods::CloseTo::Account { sweep, .. } => sweep.clone(), - periods::CloseTo::Members(members) | periods::CloseTo::MembersLastAbsorbs(members) => { + periods::CloseTo::Members(members) + | periods::CloseTo::MembersPerClose(members) + | periods::CloseTo::MembersLastAbsorbs(members) => { members.iter().filter_map(|m| m.distributions).collect() } }; @@ -2770,3 +2820,9 @@ fn check_minor_units(amount: Money) -> Result<(), LedgerError> { _ => Ok(()), } } + +/// A members close's (capital account, share) list, in order: what a run +/// of cumulative closes must share. +fn member_key(members: &[periods::MemberClose]) -> Vec<(AccountId, Decimal)> { + members.iter().map(|m| (m.capital, m.share)).collect() +} diff --git a/crates/ledger-core/src/lib.rs b/crates/ledger-core/src/lib.rs index 0274334..0ecb04e 100644 --- a/crates/ledger-core/src/lib.rs +++ b/crates/ledger-core/src/lib.rs @@ -57,7 +57,9 @@ pub use ledger::{ pub use money::{Currency, Money}; pub use payouts::{Payout, PayoutAdjustment, PayoutLine, PayoutTotals, payout_plan}; pub use payroll::{PayrollLine, PayrollRun, PayrollRunId}; -pub use periods::{CloseTo, MemberClose, Period, PeriodId, PeriodStatus, RETAINED_EARNINGS_CODE}; +pub use periods::{ + CloseTo, MemberClose, MemberCloseRecord, Period, PeriodId, PeriodStatus, RETAINED_EARNINGS_CODE, +}; pub use reports::{ BalanceSheet, BalanceSheetStatement, CashFlowLine, CashFlowParams, CashFlowStatement, ClassProfitAndLoss, GeneralLedger, LedgerAccount, LedgerPosting, MemberCapital, diff --git a/crates/ledger-core/src/periods.rs b/crates/ledger-core/src/periods.rs index 7863e07..5cae621 100644 --- a/crates/ledger-core/src/periods.rs +++ b/crates/ledger-core/src/periods.rs @@ -51,8 +51,15 @@ pub enum CloseTo { /// Members' capital accounts by share (shares sum to 1): the /// partnership convention, where each member's capital account carries /// their allocated earnings and absorbs their distributions. Odd cents - /// go by largest remainder ([`allocate`]). + /// go by largest remainder ([`allocate`]), cumulatively: a run of + /// member closes with the same members and shares gives each member, + /// in total, their share of the run's total to the cent, so rounding + /// never piles up close after close (rules.md B-13; since 2026-10-13). Members(Vec), + /// [`CloseTo::Members`] rounding each close on its own (largest + /// remainder), the rule for closes journaled on 2026-10-13 before the + /// cumulative one. Only replay of those journals produces it. + MembersPerClose(Vec), /// [`CloseTo::Members`] under the rounding closes used before /// 2026-10-13 ([`allocate_last_absorbs`]). Only replay of those journals /// produces it; new closes use `Members`. @@ -134,6 +141,23 @@ pub struct Period { pub status: PeriodStatus, /// The closing entry's id, once closed. pub closing_entry: Option, + /// The order it closed in among all closes (1 for the first), once + /// closed. + #[serde(default)] + pub close_seq: Option, + /// What a cumulative members close allocated, once closed that way. + #[serde(default)] + pub member_close: Option, +} + +/// A cumulative members close ([`CloseTo::Members`]): who shared, and the +/// net it closed. The next close with the same members continues the run. +#[derive(Clone, Debug, Serialize, Deserialize, PartialEq)] +pub struct MemberCloseRecord { + /// (capital account, share), in the order given. + pub members: Vec<(crate::AccountId, rust_decimal::Decimal)>, + /// The net income this close allocated (negative for a loss). + pub net: rust_decimal::Decimal, } impl Period { diff --git a/crates/ledger-core/tests/statements.rs b/crates/ledger-core/tests/statements.rs index b58b208..ab7a0a0 100644 --- a/crates/ledger-core/tests/statements.rs +++ b/crates/ledger-core/tests/statements.rs @@ -1522,3 +1522,177 @@ mod chaining { } } } + +mod cumulative_closes { + use super::*; + use ledger_core::{CloseTo, MemberClose}; + + /// Three months of one-cent income, 50/50, each month closed into the + /// members' capital. + fn three_cent_months(to: impl Fn(&[AccountId; 2]) -> CloseTo) -> (Ledger, [AccountId; 2]) { + let mut l = Ledger::new(Currency::USD); + let mut add = |code: &str, t| l.add_account(code, code, t, None, false).unwrap(); + let cash = add("1000", AccountType::Asset); + let caps = [ + add("3000", AccountType::Equity), + add("3001", AccountType::Equity), + ]; + let rev = add("4000", AccountType::Revenue); + for m in 1..=3 { + let e = l.create_entry(d(m, 10), "a cent"); + l.add_line( + e, + cash, + Side::Debit, + Money::new(cents("0.01"), Currency::USD), + ) + .unwrap(); + l.add_line( + e, + rev, + Side::Credit, + Money::new(cents("0.01"), Currency::USD), + ) + .unwrap(); + l.post_entry(e).unwrap(); + let end = d(m + 1, 1).pred_opt().unwrap(); + let p = l + .create_period(&format!("2026-{m:02}"), d(m, 1), end) + .unwrap(); + l.close_period_to(p, &to(&caps)).unwrap(); + } + (l, caps) + } + + fn half(caps: &[AccountId; 2]) -> Vec { + caps.iter() + .map(|&capital| MemberClose { + capital, + share: cents("0.5"), + distributions: None, + }) + .collect() + } + + /// Oracle: rules.md B-13 (cumulative closes; docs/testing.md #12), + /// hand-computed. Closing each cent on its own gives the earlier member + /// every tie: A 0.03, B 0.00 after three months. Cumulatively: after + /// month 1 the run's 0.01 splits A 0.01 / B 0; after month 2, 0.02 + /// splits 0.01 / 0.01, so month 2 gives B the cent; after month 3, 0.03 + /// splits 0.02 / 0.01, so month 3 gives A the cent. A 0.02, B 0.01. + #[test] + fn a_run_of_closes_never_piles_up_rounding() { + let (l, caps) = three_cent_months(|c| CloseTo::MembersPerClose(half(c))); + let bal = |l: &Ledger, a| l.account_balance(a).unwrap(); + assert_eq!( + (bal(&l, caps[0]), bal(&l, caps[1])), + (cents("0.03"), cents("0.00")), + "per close: the earlier member takes every tie" + ); + let (l, caps) = three_cent_months(|c| CloseTo::Members(half(c))); + assert_eq!( + (bal(&l, caps[0]), bal(&l, caps[1])), + (cents("0.02"), cents("0.01")), + "cumulative: within a cent of half of 0.03 each" + ); + } + + proptest::proptest! { + /// Oracle: rules.md B-13, cumulative closes. For any run of monthly + /// profits and losses closed into three members at 33.33% / + /// 33.33% / 33.34%, each member's total from the run is within one + /// cent of their exact share of everything closed. + #[test] + fn each_member_stays_within_a_cent_of_their_share( + nets in proptest::collection::vec(-500_000i64..500_000, 1..12), + ) { + let mut l = Ledger::new(Currency::USD); + let mut add = |code: &str, t| l.add_account(code, code, t, None, false).unwrap(); + let cash = add("1000", AccountType::Asset); + let caps = [ + add("3000", AccountType::Equity), + add("3001", AccountType::Equity), + add("3002", AccountType::Equity), + ]; + let rev = add("4000", AccountType::Revenue); + let exp = add("6000", AccountType::Expense); + let shares = [cents("0.3333"), cents("0.3333"), cents("0.3334")]; + let to = CloseTo::Members( + caps.iter() + .zip(shares) + .map(|(&capital, share)| MemberClose { capital, share, distributions: None }) + .collect(), + ); + for (i, n) in nets.iter().enumerate() { + let m = i as u32 + 1; + if *n != 0 { + let amount = Money::new(Decimal::new(n.abs(), 2), Currency::USD); + let (dr, cr) = if *n > 0 { (cash, rev) } else { (exp, cash) }; + let e = l.create_entry(d(m, 10), "month"); + l.add_line(e, dr, Side::Debit, amount).unwrap(); + l.add_line(e, cr, Side::Credit, amount).unwrap(); + l.post_entry(e).unwrap(); + } + let end = if m == 12 { d(12, 31) } else { d(m + 1, 1).pred_opt().unwrap() }; + let p = l.create_period(&format!("2026-{m:02}"), d(m, 1), end).unwrap(); + l.close_period_to(p, &to).unwrap(); + } + let total = Decimal::new(nets.iter().sum::(), 2); + for (cap, share) in caps.iter().zip(shares) { + let got = l.account_balance(*cap).unwrap(); + proptest::prop_assert!((got - total * share).abs() < cents("0.01"), "{got} vs {}", total * share); + } + } + } + + /// A run is closes with the same members and shares, back to back: a + /// close to anything else (or with other shares) ends it, and the next + /// members close starts afresh. + #[test] + fn a_different_close_ends_the_run() { + let mut l = Ledger::new(Currency::USD); + let mut add = |code: &str, t| l.add_account(code, code, t, None, false).unwrap(); + let cash = add("1000", AccountType::Asset); + let caps = [ + add("3000", AccountType::Equity), + add("3001", AccountType::Equity), + ]; + let rev = add("4000", AccountType::Revenue); + let cent = |l: &mut Ledger, m| { + let e = l.create_entry(d(m, 10), "a cent"); + l.add_line( + e, + cash, + Side::Debit, + Money::new(cents("0.01"), Currency::USD), + ) + .unwrap(); + l.add_line( + e, + rev, + Side::Credit, + Money::new(cents("0.01"), Currency::USD), + ) + .unwrap(); + l.post_entry(e).unwrap(); + }; + let close = |l: &mut Ledger, m: u32, to: &CloseTo| { + let end = d(m + 1, 1).pred_opt().unwrap(); + let p = l + .create_period(&format!("2026-{m:02}"), d(m, 1), end) + .unwrap(); + l.close_period_to(p, to).unwrap(); + }; + // Month 1 to members (A gets the cent), month 2 to retained + // earnings (ends the run), month 3 to members again: a new run, so + // A gets that cent too. + cent(&mut l, 1); + close(&mut l, 1, &CloseTo::Members(half(&caps))); + cent(&mut l, 2); + close(&mut l, 2, &CloseTo::RetainedEarnings { sweep: vec![] }); + cent(&mut l, 3); + close(&mut l, 3, &CloseTo::Members(half(&caps))); + assert_eq!(l.account_balance(caps[0]).unwrap(), cents("0.02")); + assert_eq!(l.account_balance(caps[1]).unwrap(), cents("0")); + } +} diff --git a/crates/ledger-store/src/store.rs b/crates/ledger-store/src/store.rs index d4a7ac9..01e4eb2 100644 --- a/crates/ledger-store/src/store.rs +++ b/crates/ledger-store/src/store.rs @@ -1099,7 +1099,9 @@ impl Store { CloseTo::RetainedEarnings { sweep } if sweep.is_empty() => json!("retained_earnings"), CloseTo::RetainedEarnings { sweep } => json!({"retained_earnings": {"sweep": sweep}}), CloseTo::Account { into, sweep } => json!({"account": {"into": into, "sweep": sweep}}), - CloseTo::Members(members) | CloseTo::MembersLastAbsorbs(members) => { + CloseTo::Members(members) + | CloseTo::MembersPerClose(members) + | CloseTo::MembersLastAbsorbs(members) => { let mut v = json!({ "members": members .iter() @@ -1110,10 +1112,13 @@ impl Store { })) .collect::>(), }); - // Closes journaled before 2026-10-13 carry no rounding and - // replay with the last member absorbing it. - if matches!(to, CloseTo::Members(_)) { - v["rounding"] = json!("largest_remainder"); + // The rounding rule, so replay closes the same way. Closes + // journaled before 2026-10-13 carry none (the last member + // absorbed it). + match to { + CloseTo::Members(_) => v["rounding"] = json!("cumulative"), + CloseTo::MembersPerClose(_) => v["rounding"] = json!("largest_remainder"), + _ => {} } v } @@ -3487,10 +3492,12 @@ fn close_to_from_journal(v: Option<&Value>) -> Result { }) .collect::>()?; // The rounding rule the close was made under: absent before - // 2026-10-13, when the last member absorbed it. + // 2026-10-13, when the last member absorbed it; "largest_remainder" + // per close, then "cumulative" over a run of closes. match v.get("rounding").and_then(|r| r.as_str()) { None => Ok(CloseTo::MembersLastAbsorbs(members)), - Some("largest_remainder") => Ok(CloseTo::Members(members)), + Some("largest_remainder") => Ok(CloseTo::MembersPerClose(members)), + Some("cumulative") => Ok(CloseTo::Members(members)), Some(_) => Err(corrupt("unknown rounding")), } } diff --git a/crates/ledger-store/tests/store.rs b/crates/ledger-store/tests/store.rs index fb6c680..e2e02a3 100644 --- a/crates/ledger-store/tests/store.rs +++ b/crates/ledger-store/tests/store.rs @@ -1698,3 +1698,69 @@ fn scrapping_an_asset_for_nothing_disposes_it() { fn store_add(store: &mut Store, code: &str, t: AccountType) -> ledger_core::AccountId { store.add_account(code, code, t, None, false).unwrap() } + +/// Contract (rules.md B-13): each members close journals its rounding rule +/// and replays under it: "cumulative" for new closes, "largest_remainder" +/// for the per-close rule of earlier on 2026-10-13. Three one-cent months, +/// 50/50: cumulative ends A 0.02 / B 0.01, per close A 0.03 / B 0.00. +#[test] +fn members_closes_replay_under_the_rule_they_were_journaled_with() { + for (cumulative, rule, a, b) in [ + (true, "\"rounding\":\"cumulative\"", "0.02", "0.01"), + (false, "\"rounding\":\"largest_remainder\"", "0.03", "0.00"), + ] { + let dir = test_dir(&format!("close-rule-{cumulative}")); + let mut store = Store::create(&dir, Currency::USD).unwrap(); + let cash = store + .add_account("1000", "Cash", AccountType::Asset, None, false) + .unwrap(); + let caps = [ + store + .add_account("3000", "A", AccountType::Equity, None, false) + .unwrap(), + store + .add_account("3001", "B", AccountType::Equity, None, false) + .unwrap(), + ]; + let rev = store + .add_account("4000", "Sales", AccountType::Revenue, None, false) + .unwrap(); + let members: Vec = caps + .iter() + .map(|&capital| ledger_core::MemberClose { + capital, + share: Decimal::new(5, 1), + distributions: None, + }) + .collect(); + let to = if cumulative { + ledger_core::CloseTo::Members(members) + } else { + ledger_core::CloseTo::MembersPerClose(members) + }; + let cent = Money::new(Decimal::new(1, 2), Currency::USD); + for m in 1..=3u32 { + let day = |d| NaiveDate::from_ymd_opt(2026, m, d).unwrap(); + let e = store.create_entry(day(10), "a cent").unwrap(); + store.add_line(e, cash, Side::Debit, cent).unwrap(); + store.add_line(e, rev, Side::Credit, cent).unwrap(); + store.post_entry(e).unwrap(); + let end = NaiveDate::from_ymd_opt(2026, m + 1, 1) + .unwrap() + .pred_opt() + .unwrap(); + let p = store + .create_period(&format!("2026-{m:02}"), day(1), end) + .unwrap(); + store.close_period_to(p, &to).unwrap(); + } + let journal = std::fs::read_to_string(dir.join(ledger_store::JOURNAL_FILE)).unwrap(); + assert_eq!(journal.matches(rule).count(), 3, "{rule}"); + drop(store); + let store = Store::open(&dir).unwrap(); + store.verify().unwrap(); + let bal = |id| store.ledger().account_balance(id).unwrap(); + assert_eq!(bal(caps[0]), a.parse::().unwrap(), "{rule}"); + assert_eq!(bal(caps[1]), b.parse::().unwrap(), "{rule}"); + } +} diff --git a/docs/spec/rules.md b/docs/spec/rules.md index 7bc3f09..291ef75 100644 --- a/docs/spec/rules.md +++ b/docs/spec/rules.md @@ -217,6 +217,14 @@ closed period). - **No authority** says how to round a share to the cent. Largest remainder, ties to the earlier member: DECISION (Stephen, 2026-10-13). Closes made before then replay with the last member absorbing it. +- Rounding never piles up: a run of members closes (same members and + shares, back to back) splits cumulatively, each close giving a member + their allocation of the run's total so far less their allocation before + it, so each member's total from the run is within a cent of their exact + share (follows from the running capital account below; found + 2026-10-13: closing each month on its own gave every tied cent to the + earlier member). Journaled as `"rounding": "cumulative"`; closes + journaled `"largest_remainder"` replay one at a time. - A capital account is one running balance: Form 1065 Schedule K-1 instructions, Item L: "The partnership must report your beginning capital account and ending capital account for the year", "based on the @@ -229,8 +237,12 @@ closed period). **Enforced:** `CloseTo::Members`, `periods::allocate`, `kernel::apportion`, `members_equity`. **Checked:** Kani -`apportion_is_exact`, `apportion_is_fair`; properties `prop_split_*`, -`each_members_capital_chains_across_statements`; +`apportion_is_exact`, `apportion_is_fair`; Lean `runPart_telescopes`, +`closePart_total`; properties `prop_split_*`, +`each_members_capital_chains_across_statements`, +`each_member_stays_within_a_cent_of_their_share`; +`a_run_of_closes_never_piles_up_rounding`, +`members_closes_replay_under_the_rule_they_were_journaled_with`; `closes_journaled_under_the_old_rule_replay_with_it`. ## B-14 Statements: P&L for a period; cash flow by the indirect method diff --git a/docs/testing.md b/docs/testing.md index 994ca64..e0a2c13 100644 --- a/docs/testing.md +++ b/docs/testing.md @@ -79,7 +79,7 @@ accounting question), CHANGE (a source says otherwise; work pending). | 9 | An asset's life ends at purchase + life months, that day not held; day-count proration | CONVENTION | Exactly N months of service; day proration and the mid-month convention are both accepted book policies (ASC 360-10-35-4 not read: login) | | 10 | A payroll entry has one line per account total | CONFIRMED | The per-employee detail the IRS requires ("Amounts and dates of all wage ... payments", Employment Tax Recordkeeping) is kept in the run; a summary entry is standard | | 11 | A period with exactly the dates of an existing one is allowed | DESIGN | Nothing governs duplicate periods; harmless (the second close locks only). Refusing exact duplicates is an option | -| 12 | Each close into members' capital rounds on its own (ties to the earlier member) | CHANGE (pending) | Found 2026-10-13 with #7: twelve monthly 50/50 closes can leave one member several cents ahead of half the year's income. Closes should split cumulatively too (year-to-date allocation minus what earlier closes gave); a new journaled rounding rule, older closes replaying as booked | +| 12 | Each close into members' capital rounds on its own (ties to the earlier member) | CHANGED 2026-10-13 | Twelve monthly 50/50 closes could leave one member several cents ahead. A run of members closes now splits cumulatively (rules.md B-13; Lean `runPart_telescopes`; property `each_member_stays_within_a_cent_of_their_share` fails on the per-close rule); journaled `"cumulative"`, older closes replay as booked | Questions are settled from the sources, not by any one company's CPA (wanderbooks is general software). Where the standards leave a real diff --git a/docs/verification.md b/docs/verification.md index 257db4f..cd64530 100644 --- a/docs/verification.md +++ b/docs/verification.md @@ -124,6 +124,13 @@ sequence of commands, of any length**: other shares were rounded, and only the last share changes. - Kani `plug_last_sums_exactly` · Lean `plugLast_total`, `plugLast_keeps` +17. **A run of member closes telescopes**: each member's total from a run + of cumulative closes is their allocation of everything the run closed + (so its rounding is one allocation's, never a sum of them), and each + close hands out exactly its net, for any allocation whose parts sum to + the whole (rules.md B-13). + - Lean `runPart_telescopes`, `closePart_total` · property + `each_member_stays_within_a_cent_of_their_share` ## What the proofs found diff --git a/verify/lean/Audit.lean b/verify/lean/Audit.lean index 8983c4e..d4f9c1a 100644 --- a/verify/lean/Audit.lean +++ b/verify/lean/Audit.lean @@ -19,6 +19,8 @@ open Wanderbooks #print axioms net_closings_is_net_income #print axioms plugLast_total #print axioms plugLast_keeps +#print axioms runPart_telescopes +#print axioms closePart_total #print axioms Reachable.inv #print axioms Reachable.books_net_zero #print axioms Reachable.trial_balance diff --git a/verify/lean/Wanderbooks/Closing.lean b/verify/lean/Wanderbooks/Closing.lean index dade993..a6bda74 100644 --- a/verify/lean/Wanderbooks/Closing.lean +++ b/verify/lean/Wanderbooks/Closing.lean @@ -317,4 +317,54 @@ theorem plugLast_keeps (whole : Int) (ps : List Int) : rw [show plugLast whole (p :: q :: rest) = p :: plugLast (whole - p) (q :: rest) from rfl, List.dropLast_cons_of_ne_nil hne, ih, List.dropLast_cons_cons] +/-! ## Cumulative member closes + +A run of members closes (`CloseTo::Members`, rules.md B-13) gives each +member, at each close, their allocation of the run's total so far minus +their allocation of the total before it. `alloc` is any allocation of an +amount to members (member `i` gets `alloc x i`), such as +`periods::allocate`. -/ + +/-- What one close gives member `i`: `before` is the run's total before +it, `net` what it closes. -/ +def closePart (alloc : Int → Nat → Int) (before net : Int) (i : Nat) : Int := + alloc (before + net) i - alloc before i + +/-- What a run of closes with these nets, starting after `before`, gives +member `i` in all. -/ +def runPart (alloc : Int → Nat → Int) : Int → List Int → Nat → Int + | _, [], _ => 0 + | before, net :: rest, i => closePart alloc before net i + runPart alloc (before + net) rest i + +/-- **A run telescopes**: member `i`'s total from a run is their allocation +of everything the run closed, less their allocation of where it started. +From an empty start (`alloc 0 = 0`), it is exactly their allocation of +the run's total, so its rounding is one allocation's rounding, never a +sum of them. -/ +theorem runPart_telescopes (alloc : Int → Nat → Int) (before : Int) (nets : List Int) (i : Nat) : + runPart alloc before nets i = alloc (before + nets.sum) i - alloc before i := by + induction nets generalizing before with + | nil => simp [runPart] + | cons n rest ih => + simp only [runPart, closePart, ih, List.sum_cons] + rw [show before + n + rest.sum = before + (n + rest.sum) by omega] + omega + +/-- A sum of differences is the difference of the sums. -/ +theorem sum_map_sub (f g : Nat → Int) (ms : List Nat) : + (ms.map (fun i => f i - g i)).sum = (ms.map f).sum - (ms.map g).sum := by + induction ms with + | nil => simp + | cons m ms ih => simp only [List.map_cons, List.sum_cons, ih]; omega + +/-- **Each close hands out exactly its net** when every allocation sums +to its amount (`periods::allocate` does: `kernel::apportion`). -/ +theorem closePart_total (alloc : Int → Nat → Int) (members : List Nat) + (sums : ∀ x, (members.map (alloc x)).sum = x) (before net : Int) : + (members.map (closePart alloc before net)).sum = net := by + have h := sum_map_sub (alloc (before + net)) (alloc before) members + unfold closePart + rw [h, sums, sums] + omega + end Wanderbooks