fix(core): due-today is Current; odd cents split by largest remainder

Max-testing pass, step 2: two spec decisions the owner confirmed
(2026-10-13), each test-first.

Aging (arap::aging_bucket): a document due today was "1-30 days past
due"; it is Current, since past due starts the day after (QuickBooks'
convention). Spec in the doc comment. Boundary examples at every edge
(due today, 1, 30, 31, 60, 61, 90, 91 days) fail on the old code. A
property: the balance lands in exactly one bucket, and time only ages
it.

Member splits (periods::allocate): the last member absorbed every odd
cent, so the same partner always got or lost it. Now largest remainder:
each share rounded toward zero to the cent, leftover cents to the
largest remainders, ties to the earlier member, a loss the negation of
the gain. The core is a new kernel function, kernel::apportion,
allocation-free so Kani proves it (n <= 3): apportion_is_exact (it
succeeds exactly when the shortfall is under a unit per part; then the
parts sum to the whole, each gains 0 or 1 unit, one may take the
sub-unit fraction) and apportion_is_fair (never a unit to a part while
a larger remainder goes without). Kani found an off-by-one in the first
version: a shortfall of n units plus a fraction was accepted. Native
regression apportion_refuses_a_shortfall_of_a_unit_per_part_or_more.
Properties at Decimal (2,000 cases, up to 5 members): conservation,
within a cent of each exact share, fairness, sign symmetry; they fail on
the old rule. Bridge: apportion agrees on i64 and Decimal.

Contract: closes journaled before this change replay exactly. New
member closes journal "rounding": "largest_remainder"; journal lines
without it replay as CloseTo::MembersLastAbsorbs, the old rule
(periods::allocate_last_absorbs, pinned by
closes_journaled_under_the_old_rule_replay_with_it). The members'
equity statement isn't journaled and uses the new rule.

Open gap: Lean proof of apportion's sum law for any n (needs a
permutation lemma on the ranking); Kani covers n <= 3, properties n <= 5.
The Lean closing theorems already hold for any split summing to the
net.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GWVo7x3UHw5kwCUaWxiejX
This commit is contained in:
swaitsandClaude Opus 5.5 committed 2026-10-13 12:10:55 -06:00
1 parent 847dd4388d
commit e0b6d6988f
11 files changed
+502 -36

No files matched your search

+73 -2
View File
@@ -194,7 +194,26 @@ impl AgingRow {
}
}
/// Bucket a past-due balance by days overdue.
/// Put an open balance in its aging bucket.
///
/// ```text
/// GOAL: say how overdue a balance is, as of a date.
/// INVARIANTS:
/// 1. MUST put the whole balance in exactly one bucket; the others are
/// zero.
/// 2. NEVER moves a balance to a younger bucket as `as_of` advances.
/// SCENARIOS:
/// 1. IF `as_of` is on or before the due date:
/// - SHOULD be Current
/// - NEVER past due
/// BECAUSE a document due today is not yet overdue (QuickBooks'
/// convention; owner, 2026-10-13).
/// 2. IF it is 1 to 30 days past due: SHOULD be 1-30.
/// 3. IF 31 to 60: SHOULD be 31-60.
/// 4. IF 61 to 90: SHOULD be 61-90.
/// 5. IF more than 90: SHOULD be 90+.
/// BECAUSE these are the standard 30-day aging buckets.
/// ```
pub fn aging_bucket(due_date: NaiveDate, as_of: NaiveDate, balance: Decimal) -> AgingRow {
let mut row = AgingRow {
name: String::new(),
@@ -204,7 +223,7 @@ pub fn aging_bucket(due_date: NaiveDate, as_of: NaiveDate, balance: Decimal) ->
days_90: Decimal::ZERO,
days_90_plus: Decimal::ZERO,
};
if due_date > as_of {
if due_date >= as_of {
row.current = balance;
} else {
let days = (as_of - due_date).num_days();
@@ -348,6 +367,58 @@ mod tests {
assert!(matches!(err, Err(LedgerError::Overpayment(_, _))));
}
#[test]
fn aging_boundaries() {
// Spec scenarios 1-5, at every edge.
let due = NaiveDate::from_ymd_opt(2026, 3, 31).unwrap();
let b = Decimal::from(7);
let bucket = |days: i64| {
let r = aging_bucket(due, due + chrono::Duration::days(days), b);
[r.current, r.days_30, r.days_60, r.days_90, r.days_90_plus]
.iter()
.position(|x| !x.is_zero())
.unwrap()
};
for (days, want) in [
(-10, 0),
(0, 0),
(1, 1),
(30, 1),
(31, 2),
(60, 2),
(61, 3),
(90, 3),
(91, 4),
(4000, 4),
] {
assert_eq!(bucket(days), want, "{days} days past due");
}
}
proptest::proptest! {
/// Invariants 1 and 2: one bucket holds the whole balance, and
/// time only ever ages it.
#[test]
fn aging_is_exclusive_and_only_ages(
due_off in 0i64..2000, a in 0i64..2000, step in 0i64..400, cents in 1i64..10_000_000,
) {
let base = NaiveDate::from_ymd_opt(2024, 1, 1).unwrap();
let due = base + chrono::Duration::days(due_off);
let b = Decimal::new(cents, 2);
let idx = |as_of: NaiveDate| {
let r = aging_bucket(due, as_of, b);
let cells = [r.current, r.days_30, r.days_60, r.days_90, r.days_90_plus];
let held: Vec<usize> = (0..5).filter(|&i| !cells[i].is_zero()).collect();
proptest::prop_assert_eq!(held.len(), 1);
proptest::prop_assert_eq!(cells[held[0]], b);
Ok(held[0])
};
let early = base + chrono::Duration::days(a);
let later = early + chrono::Duration::days(step);
proptest::prop_assert!(idx(early)? <= idx(later)?);
}
}
#[test]
fn ar_aging_buckets_correctly() {
let mut l = arap_ledger();