Files
wanderbooks/crates/ledger-core/src/kernel.rs
T
swaitsandClaude Opus 5.5 321b94562a
check / check (push) Canceled after 0s
Projects: classes as entities, and the sidebar fits short windows
A project is a class with facts (description, status, kind, party,
dates, links, notes) in one project.set event behind the format
feature projects. Four tools (books.add_project, update_project,
projects, project); documents and decisions link to projects; B-37:
on-spec costs are expensed as incurred, repayment is revenue, and the
unrecovered cost is never below zero (Kani). Viewer: a Projects list
and a project page with its figures, by month and by account. The
sidebar measures its footer instead of reserving a fixed 172 px.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01T3gXMVt7XJPi6ens1or9Dj
2026-10-22 03:50:52 -06:00

2041 lines
80 KiB
Rust
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
//! The accounting kernel: the arithmetic every bookkeeping invariant rests
//! on, in one place.
//!
//! Each function here is small, pure, and generic over [`Amount`]. The
//! engine runs it on [`Decimal`]; the Kani harnesses in `proofs.rs` run the
//! very same code on machine integers and prove it correct for every input
//! within their bounds; and the Lean model in `verify/lean` proves the
//! laws it implements hold for books of any size. See
//! `docs/verification.md` for which proof covers which law.
//!
//! The laws, in the order they appear (each traced to its authority in
//! `docs/spec/rules.md`):
//!
//! * a line's signed amount is `+amount` for a debit, `-amount` for a credit
//! (B-2);
//! * an entry is acceptable when it has two or more lines, every amount is
//! positive and in range, and its debits equal its credits exactly (B-1,
//! B-2, B-21);
//! * an acceptable entry nets to zero, account by account summed (B-1);
//! * a reversal flips every side, so it is acceptable exactly when the
//! original is, and the two together net every account to zero (B-9);
//! * an account's balance is its movement read on its normal side, so the
//! balances satisfy the accounting equation whenever movements net to
//! zero (B-5, B-7);
//! * a trial balance puts each movement in exactly one column, so its
//! columns differ by the net of all movements (B-6);
//! * a closing line zeroes the account it closes (B-11);
//! * a payment to a vendor splits, line by line, into what counts toward
//! its 1099, what a card or payment network paid, and what is unknown,
//! and money moved between the company's own sources nets out (B-19);
//! * an allocation's parts sum to the whole, to the last unit, by largest
//! remainder (B-13);
//! * a cumulative allocation hands out exactly the new amount, and leaves
//! each running total one allocation of everything allocated, so it never
//! drifts a unit from its exact share (B-13);
//! * an entry's cash is applied to the sections of the statement of cash
//! flows moving against it, in a fixed order, each up to its own
//! movement: the parts sum to the entry's cash, what no cash settled sums
//! to zero, and a reversal's parts are the original's negated (B-14);
//! * what a member or lender paid or received for the company, with no
//! cash account moving, is split among the kinds it settled, netting to
//! zero, and mirrored by a reversal (B-14 rule 11);
//! * a party's part of an entry is signed as a line on the party's own
//! account would be, a reversal's is its original's negated, and what of
//! it counts as money or as property never exceeds it (B-35);
//! * a span prorated by days (depreciation, B-15; daily schedules, B-16)
//! splits into parts that sum to its total, each but the last its days
//! times the monthly rate within one unit, the last the remainder;
//! * a catch-up run brings the books to the schedule without ever carrying
//! more than it says at a month end already posted (B-15), and a
//! disposal trues what the books carry up or down to the schedule;
//! * an asset's basis figures follow from its basis rule and facts: the
//! §723 basis is the contributor's adjusted basis, the depreciable basis
//! the cost, that basis, or the lesser of it and fair market value, and
//! the §704(c) built-in gain is fair market value less the §723 basis
//! (B-25).
use crate::assets::BasisRule;
use crate::{AccountType, Side};
use rust_decimal::Decimal;
/// What the kernel needs of a money amount: exact, ordered, and checked
/// arithmetic that reports overflow instead of rounding or wrapping.
pub trait Amount: Copy + Ord {
/// Zero.
const ZERO: Self;
/// `self + rhs`, or `None` when it cannot be represented exactly.
fn checked_add(self, rhs: Self) -> Option<Self>;
/// `-self`, or `None` when it cannot be represented.
fn checked_neg(self) -> Option<Self>;
/// True when the amount is small and precise enough for a journal line
/// (see [`MAX_LINE_AMOUNT`] and [`MAX_LINE_SCALE`] for [`Decimal`]).
fn in_line_range(self) -> bool;
/// `self - rhs`, or `None` when it cannot be represented exactly.
fn checked_sub(self, rhs: Self) -> Option<Self> {
self.checked_add(rhs.checked_neg()?)
}
}
/// The largest amount one journal line may carry: one quadrillion units of
/// the base currency. Far beyond any real transaction, and far enough
/// below [`Decimal::MAX`] that no realistic sum of lines can overflow.
pub const MAX_LINE_AMOUNT: Decimal = Decimal::from_parts(0xA4C6_8000, 0x0003_8D7E, 0, false, 0);
/// The most decimal places a journal line may carry. Cents need two;
/// foreign-currency lines (amount times rate) need more; ten keeps every
/// sum of lines exact as long as the total stays under 7.9 quintillion.
pub const MAX_LINE_SCALE: u32 = 10;
impl Amount for Decimal {
const ZERO: Self = Decimal::ZERO;
fn checked_add(self, rhs: Self) -> Option<Self> {
Decimal::checked_add(self, rhs)
}
fn checked_neg(self) -> Option<Self> {
Some(-self)
}
fn in_line_range(self) -> bool {
self.abs() <= MAX_LINE_AMOUNT && self.normalize().scale() <= MAX_LINE_SCALE
}
}
impl Amount for i64 {
const ZERO: Self = 0;
fn checked_add(self, rhs: Self) -> Option<Self> {
i64::checked_add(self, rhs)
}
fn checked_neg(self) -> Option<Self> {
i64::checked_neg(self)
}
fn in_line_range(self) -> bool {
// Scaled down with the same headroom as Decimal's range: lines
// this size can be summed many times over without overflow.
self.unsigned_abs() <= (1 << 40)
}
}
/// Why the kernel rejected an entry's lines.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum LineError<T> {
/// Fewer than two lines.
TooFewLines,
/// A line with a zero amount.
ZeroAmount,
/// A line with a negative amount: direction is the side's job.
NegativeAmount,
/// A line too large or too precise for a journal line.
OutOfRange,
/// Debits and credits differ.
Unbalanced {
/// Sum of debit lines.
debits: T,
/// Sum of credit lines.
credits: T,
},
}
/// The other side.
pub fn flip(side: Side) -> Side {
match side {
Side::Debit => Side::Credit,
Side::Credit => Side::Debit,
}
}
/// A line's signed amount: positive for a debit, negative for a credit.
pub fn signed<T: Amount>(side: Side, amount: T) -> Option<T> {
match side {
Side::Debit => Some(amount),
Side::Credit => amount.checked_neg(),
}
}
/// Total debits and total credits of some lines.
pub fn totals<T: Amount>(lines: impl IntoIterator<Item = (Side, T)>) -> Option<(T, T)> {
let mut debits = T::ZERO;
let mut credits = T::ZERO;
for (side, amount) in lines {
match side {
Side::Debit => debits = debits.checked_add(amount)?,
Side::Credit => credits = credits.checked_add(amount)?,
}
}
Some((debits, credits))
}
/// The net of some lines: debits minus credits.
pub fn net<T: Amount>(lines: impl IntoIterator<Item = (Side, T)>) -> Option<T> {
let mut total = T::ZERO;
for (side, amount) in lines {
total = total.checked_add(signed(side, amount)?)?;
}
Some(total)
}
/// Check an entry's lines: two or more, every amount positive and within
/// line range, debits equal to credits. Accounts and currencies are the
/// caller's to check; this is the arithmetic.
pub fn check_lines<T: Amount>(lines: &[(Side, T)]) -> Result<(), LineError<T>> {
if lines.len() < 2 {
return Err(LineError::TooFewLines);
}
for &(_, amount) in lines {
if amount == T::ZERO {
return Err(LineError::ZeroAmount);
}
if amount < T::ZERO {
return Err(LineError::NegativeAmount);
}
if !amount.in_line_range() {
return Err(LineError::OutOfRange);
}
}
let (debits, credits) = totals(lines.iter().copied()).ok_or(LineError::OutOfRange)?;
if debits != credits {
return Err(LineError::Unbalanced { debits, credits });
}
Ok(())
}
/// Net movement per account (debits minus credits), in order of first
/// appearance.
pub fn movements<K: Copy + Eq, T: Amount>(
lines: impl IntoIterator<Item = (K, Side, T)>,
) -> Option<Vec<(K, T)>> {
let lines: Vec<_> = lines.into_iter().collect();
let Some(&(first, _, _)) = lines.first() else {
return Some(Vec::new());
};
// At most one account per line.
let mut out = vec![(first, T::ZERO); lines.len()];
let n = movements_into(&lines, &mut out)?;
out.truncate(n);
Some(out)
}
/// [`movements`] into a caller's buffer, without allocating: returns how
/// many accounts it wrote, or `None` on overflow or if `out` is too small.
pub fn movements_into<K: Copy + Eq, T: Amount>(
lines: &[(K, Side, T)],
out: &mut [(K, T)],
) -> Option<usize> {
let mut n = 0;
for &(account, side, amount) in lines {
let delta = signed(side, amount)?;
match out[..n].iter_mut().find(|(k, _)| *k == account) {
Some((_, total)) => *total = total.checked_add(delta)?,
None => {
*out.get_mut(n)? = (account, delta);
n += 1;
}
}
}
Some(n)
}
/// The lines of a reversing entry: every side flipped, accounts and
/// amounts unchanged.
pub fn reversal<K: Copy, T: Amount>(lines: &[(K, Side, T)]) -> Vec<(K, Side, T)> {
lines.iter().map(|&line| reverse_line(line)).collect()
}
/// One line of a reversing entry: the side flipped, account and amount
/// unchanged.
pub fn reverse_line<K, T: Amount>((account, side, amount): (K, Side, T)) -> (K, Side, T) {
(account, flip(side), amount)
}
/// An account's balance read on its normal side: positive is a normal
/// balance, negative a contra balance.
pub fn normal_balance<T: Amount>(account_type: AccountType, movement: T) -> Option<T> {
match account_type.normal_side() {
Side::Debit => Some(movement),
Side::Credit => movement.checked_neg(),
}
}
/// A movement in trial-balance columns: `(debit, credit)`, one of them
/// zero, both non-negative.
pub fn columns<T: Amount>(movement: T) -> Option<(T, T)> {
if movement > T::ZERO {
Some((movement, T::ZERO))
} else if movement == T::ZERO {
// Never a negative zero: money never prints "-0".
Some((T::ZERO, T::ZERO))
} else {
Some((T::ZERO, movement.checked_neg()?))
}
}
/// The line that zeroes an account with this movement: the opposite side,
/// for the same amount. `None` for a zero movement (nothing to close).
pub fn closing_line<T: Amount>(movement: T) -> Option<(Side, T)> {
if movement > T::ZERO {
Some((Side::Credit, movement))
} else if movement < T::ZERO {
Some((Side::Debit, movement.checked_neg()?))
} else {
None
}
}
/// The line that credits `credit` to an account (a negative credit is a
/// debit). `None` for zero. This is [`closing_line`]: crediting `c` and
/// zeroing a movement of `c` are the same line.
pub fn credit_line<T: Amount>(credit: T) -> Option<(Side, T)> {
closing_line(credit)
}
// ---------------------------------------------------------------------------
// 1099 payments: where each payment line goes (rules.md B-19)
// ---------------------------------------------------------------------------
/// A line's role in a payment to a vendor, from its account.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum PayRole {
/// One of the books' cash accounts: bank, cash on hand.
Cash,
/// One of the books' financing liabilities (what members or lenders
/// paid on the company's behalf), or an account a member's card or
/// cash, or a payment platform, pays through: how a payment through
/// it was made, only the entry's method says.
Financing,
/// The account of a company card (a business card's liability).
CardAccount,
/// None of these (an expense, payables, prepaid): not a payment line.
Other,
}
/// What an entry's payment-method tag says about one of its lines.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Tag {
/// The entry has no payment method recorded.
None,
/// The method pays through this line's account and is a card or a
/// payment network.
ThisCard,
/// The method pays through this line's account and is neither (the
/// company's bank, a member's own cash or check).
ThisOther,
/// The method pays through another account: it doesn't describe this
/// line.
Elsewhere,
}
/// Where a payment line's amount goes on the 1099 worksheet.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Bucket {
/// Counts toward the payee's 1099.
Counts,
/// Paid by card or payment network: Form 1099-K's, never 1099-NEC or
/// 1099-MISC's.
Card,
/// Can't be classified until the payment method is recorded.
Undetermined,
}
impl Bucket {
/// Every bucket, in [`split_payment`]'s order.
pub const ALL: [Bucket; 3] = [Bucket::Counts, Bucket::Card, Bucket::Undetermined];
/// Its place in [`split_payment`]'s array.
pub const fn index(self) -> usize {
match self {
Bucket::Counts => 0,
Bucket::Card => 1,
Bucket::Undetermined => 2,
}
}
}
/// The bucket a payment line goes in, from its role and the entry's tag.
///
/// ```text
/// GOAL: every payment line to a vendor counts toward its 1099, is a card
/// or payment-network payment (Form 1099-K), or is unknown; never
/// guessed.
/// SOURCE: docs/spec/rules.md B-19 (Treas. Reg. §1.6041-1(a)(1)(iv): a
/// transaction reportable under §6050W is not reported under
/// §6041; §1.6041-1(e)(1): a member writing a check at the
/// company's direction doesn't make the member the payor;
/// sources/irs-1099-payment-method.md); DECISION D-40 (owner,
/// 2026-10-20: a bank payment with no method recorded counts).
/// INVARIANTS (first match wins):
/// 1. The tag names this line's account: Card for a card or network,
/// else Counts.
/// 2. Otherwise the role decides: Cash counts (presumed check, ACH or
/// transfer, D-40); Financing is Undetermined (a member's card or
/// their check, unknown until tagged); CardAccount is Card; Other is
/// no payment line (None).
/// ```
pub fn payment_bucket(role: PayRole, tag: Tag) -> Option<Bucket> {
match (tag, role) {
(Tag::ThisCard, _) => Some(Bucket::Card),
(Tag::ThisOther, _) => Some(Bucket::Counts),
(Tag::None | Tag::Elsewhere, PayRole::Cash) => Some(Bucket::Counts),
(Tag::None | Tag::Elsewhere, PayRole::Financing) => Some(Bucket::Undetermined),
(Tag::None | Tag::Elsewhere, PayRole::CardAccount) => Some(Bucket::Card),
(Tag::None | Tag::Elsewhere, PayRole::Other) => None,
}
}
/// What an entry paid, per bucket: credits minus debits of the lines in
/// each (a line in no bucket is not a payment line). `None` on overflow.
pub fn split_payment<T: Amount>(lines: &[(Option<Bucket>, Side, T)]) -> Option<[T; 3]> {
let mut out = [T::ZERO; 3];
for &(bucket, side, amount) in lines {
if let Some(b) = bucket {
let i = b.index();
out[i] = match side {
Side::Credit => out[i].checked_add(amount)?,
Side::Debit => out[i].checked_sub(amount)?,
};
}
}
Some(out)
}
/// Net one entry's buckets ([`split_payment`]): money moved between the
/// company's own payment sources pays no one.
///
/// ```text
/// GOAL: a card bill paid from the bank, a member reimbursed, or a loan
/// paid down never counts toward a vendor's 1099.
/// SOURCE: docs/spec/rules.md B-19 (26 U.S.C. §6041(a): payments made to
/// the payee; P3 review R1, 2026-10-20).
/// INVARIANTS:
/// 1. The buckets' sum P is kept exactly.
/// 2. No bucket ends opposite in sign to P.
/// 3. Buckets all of one sign (zeros aside) come back unchanged.
/// SCENARIOS:
/// 1. IF the signs differ and P = 0 (Dr 2050 / Cr 1000, the card bill):
/// SHOULD be [0, 0, 0].
/// 2. IF the signs differ and exactly one bucket has P's sign: SHOULD
/// give it P and the others 0.
/// 3. IF two buckets have P's sign: SHOULD put P in Undetermined
/// BECAUSE which source the other side offsets is unknown (split
/// the entry).
/// ```
pub fn net_buckets<T: Amount>(b: [T; 3]) -> Option<[T; 3]> {
let positive = b.iter().any(|&x| x > T::ZERO);
let negative = b.iter().any(|&x| x < T::ZERO);
if !(positive && negative) {
return Some(b);
}
let p = b[0].checked_add(b[1])?.checked_add(b[2])?;
let mut out = [T::ZERO; 3];
if p == T::ZERO {
return Some(out);
}
let mut taker = Bucket::Undetermined.index();
let mut takers = 0;
for (i, &x) in b.iter().enumerate() {
if x != T::ZERO && (x > T::ZERO) == (p > T::ZERO) {
taker = i;
takers += 1;
}
}
if takers != 1 {
taker = Bucket::Undetermined.index();
}
out[taker] = p;
Some(out)
}
/// Make rounded parts sum to the whole: the last part becomes `whole`
/// minus the others, absorbing every unit of rounding. Returns `None` on
/// overflow, leaving `parts` unchanged.
pub fn plug_last<T: Amount>(whole: T, parts: &mut [T]) -> Option<()> {
let Some((last, rest)) = parts.split_last_mut() else {
return Some(());
};
let mut others = T::ZERO;
for &p in rest.iter() {
others = others.checked_add(p)?;
}
*last = whole.checked_sub(others)?;
Some(())
}
/// Largest-remainder apportionment: make rounded-down `parts` sum to
/// `whole`, handing out the shortfall one `unit` at a time, largest
/// `remainders` first (ties to the earlier part). Any final fraction of a
/// unit (when `whole` isn't a whole number of units) goes to the first
/// part in that order.
///
/// ```text
/// GOAL: split a whole into parts, each a whole number of units where
/// possible, summing to the whole exactly, without favoring anyone.
/// SOURCE: docs/spec/rules.md B-13 (shares: 26 U.S.C. §704(a); cent
/// rounding: DECISION, owner 2026-10-13), B-21 (exact totals).
/// INVARIANTS:
/// 1. MUST make the parts sum to `whole` exactly.
/// 2. MUST change each part by zero or one unit (the first in order
/// may also take the sub-unit fraction).
/// 3. NEVER gives a unit to a part while a part with a strictly larger
/// remainder goes without.
/// SCENARIOS:
/// 1. IF the shortfall is negative, or `n` units or more (the parts
/// weren't rounded down from shares of `whole`):
/// - SHOULD return None, leaving `parts` unchanged
/// BECAUSE apportioning only corrects rounding.
/// 2. IF $100.00 splits three equal ways:
/// - SHOULD be 33.34, 33.33, 33.33
/// - NEVER the same partner absorbing every odd cent by position
/// BECAUSE the cent goes to the largest remainder, ties to the first
/// (owner, 2026-10-13).
/// ```
///
/// Allocation-free and O(n^2): it ranks each part by counting the parts
/// ahead of it, so the model checker can prove it outright.
pub fn apportion<T: Amount>(whole: T, parts: &mut [T], remainders: &[T], unit: T) -> Option<()> {
if parts.len() != remainders.len() || unit <= T::ZERO {
return None;
}
if parts.is_empty() {
// Nothing to give the whole to.
return (whole == T::ZERO).then_some(());
}
let mut shortfall = whole;
for &p in parts.iter() {
shortfall = shortfall.checked_sub(p)?;
}
if shortfall < T::ZERO {
return None;
}
// Whole units short, by subtraction: no division in `Amount`. A
// shortfall of a unit per part or more isn't rounding; refuse it.
let mut units = 0;
while shortfall >= unit {
shortfall = shortfall.checked_sub(unit)?;
units += 1;
if units == parts.len() {
return None;
}
}
// A part's rank: the parts ahead of it (larger remainder, or equal and
// earlier).
let rank = |i: usize| {
(0..remainders.len())
.filter(|&j| remainders[j] > remainders[i] || (remainders[j] == remainders[i] && j < i))
.count()
};
for (i, part) in parts.iter_mut().enumerate() {
let r = rank(i);
let mut add = T::ZERO;
if r < units {
add = unit;
}
if r == 0 {
add = add.checked_add(shortfall)?;
}
*part = part.checked_add(add)?;
}
Some(())
}
/// Cumulative apportionment: what one close gives each part when the
/// running `total` is apportioned afresh ([`apportion`]) and what earlier
/// closes gave each part (`given`) is taken back. `parts` and
/// `remainders` are the rounded-down shares of `total` and what rounding
/// took from each, as for [`apportion`].
///
/// ```text
/// GOAL: members' running totals that never drift a unit from their
/// exact shares, whatever earlier closes did.
/// SOURCE: docs/spec/rules.md B-13 (shares: 26 U.S.C. §704(a); capital
/// accounts carry the allocations: Treas. Reg.
/// §1.704-1(b)(2)(iv)(b); cent rounding: DECISION, owner
/// 2026-10-13; counted from the first close: D-10, 2026-10-16).
/// INVARIANTS:
/// 1. MUST make the parts sum to `total − Σ given` exactly.
/// 2. MUST leave given[i] + parts[i] equal to what `apportion(total, …)`
/// gives part i: a running total is one apportionment, so it carries
/// one apportionment's rounding, never a sum of them.
/// 3. On None, `parts` MUST be unchanged.
/// SCENARIOS:
/// 1. IF the lengths differ, the unit isn't positive, `total`, the
/// unit, a part or a `given` is out of line range, or apportion
/// refuses: SHOULD return None, leaving `parts` unchanged
/// BECAUSE in range, the subtraction can't overflow, so a refusal is
/// known before anything changes.
/// 2. IF 0.03 was closed as A 0.03 / B 0 and the running total is now
/// 0.04 (50/50, floors 0.02 / 0.02): SHOULD give A −0.01, B +0.02
/// BECAUSE 0.04 apportions 0.02 each.
/// ```
///
/// Allocation-free, with no bulk copy (docs/verification.md, "Trusting
/// the checker"), so the model checker can prove it outright.
pub fn apportion_cumulative<T: Amount>(
total: T,
parts: &mut [T],
remainders: &[T],
unit: T,
given: &[T],
) -> Option<()> {
if parts.len() != given.len() || !total.in_line_range() || !unit.in_line_range() {
return None;
}
if parts.iter().chain(given).any(|a| !a.in_line_range()) {
return None;
}
apportion(total, parts, remainders, unit)?;
// Each part is now under three line ranges and each `given` within
// one: the subtraction can't fail (Kani apportion_cumulative_is_exact).
for (part, &g) in parts.iter_mut().zip(given) {
*part = part.checked_sub(g)?;
}
Some(())
}
/// Where a line falls on the statement of cash flows (rules.md B-14 rule
/// 2): a cash account, or one of the three sections.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum Flow {
/// A cash account: what the statement explains the change in.
Cash,
/// Operating activities.
Operating,
/// Investing activities.
Investing,
/// Financing activities.
Financing,
}
impl Flow {
/// The three sections, in the order cash is applied to them (rules.md
/// B-14 rule 3): operating, investing, financing.
pub const SECTIONS: [Flow; 3] = [Flow::Operating, Flow::Investing, Flow::Financing];
}
/// One entry's effect on the statement of cash flows.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct EntryFlows<T> {
/// Net movement of the entry's cash lines, debit-positive: + is cash
/// in.
pub cash: T,
/// Cash per section, `[operating, investing, financing]`, + is in.
/// Sums to `cash`.
pub flows: [T; 3],
/// What no cash settled, per section, debit-positive: the section's
/// movement plus its cash. Sums to zero.
pub noncash: [T; 3],
}
/// The cash one section takes from what is left of an entry's cash
/// (`remaining`), given the section's net movement (debit-positive): only
/// a section moving against the cash takes any, and never more than its
/// own movement. Cash in (`remaining > 0`) settles credits (`movement <
/// 0`); cash out settles debits.
pub fn take<T: Amount>(remaining: T, movement: T) -> Option<T> {
let against = movement.checked_neg()?;
Some(if remaining > T::ZERO && movement < T::ZERO {
remaining.min(against)
} else if remaining < T::ZERO && movement > T::ZERO {
remaining.max(against)
} else {
T::ZERO
})
}
/// Apply `cash` to `movements` in order, each taking [`take`] of what is
/// left: `applied[k]` is the cash of part `k`. `None` when something is
/// left over (the movements against the cash are smaller than it), the
/// slices differ in length, or on overflow.
///
/// ```text
/// GOAL: split an entry's cash among the parts it settled, without
/// inventing or losing any.
/// SOURCE: rules.md B-14 rule 3 (ASC 230-10-50-5: only the cash portion
/// of a part-cash transaction is a cash flow; the order is a
/// CONVENTION, the ASC is silent).
/// INVARIANTS:
/// 1. On success the parts sum to `cash` exactly.
/// 2. Each part has the sign of `cash` (or is zero) and is no larger
/// than its own movement, which runs against the cash.
/// 3. Applying `-cash` to the negated movements gives the negated parts
/// (a reversal mirrors its original).
/// SCENARIOS:
/// 1. IF the movements against the cash sum to at least the cash:
/// - SHOULD succeed (a balanced entry always does)
/// 2. IF they don't: SHOULD return None, never a part out of thin air.
/// ```
pub fn apply_cash<T: Amount>(cash: T, movements: &[T], applied: &mut [T]) -> Option<()> {
if movements.len() != applied.len() {
return None;
}
let mut remaining = cash;
for (out, &movement) in applied.iter_mut().zip(movements) {
let part = take(remaining, movement)?;
*out = part;
remaining = remaining.checked_sub(part)?;
}
(remaining == T::ZERO).then_some(())
}
/// An entry's cash flows (rules.md B-14 rule 3): the net movement of its
/// cash lines, applied to the sections moving against it in the order
/// operating, investing, financing, each up to its own movement; what is
/// left of a section's movement is the part no cash settled. `None` when
/// the lines don't net to zero (never for a posted entry) or on overflow.
/// It is [`entry_movements`] then [`flows_of`], so each is proved on its
/// own (docs/verification.md, law 10).
pub fn entry_flows<T: Amount>(lines: &[(Flow, Side, T)]) -> Option<EntryFlows<T>> {
let (cash, moved) = entry_movements(lines)?;
flows_of(cash, moved)
}
/// An entry's net movement on its cash lines and on each section's,
/// `(cash, [operating, investing, financing])`, debit-positive. `None`
/// on overflow.
pub fn entry_movements<T: Amount>(lines: &[(Flow, Side, T)]) -> Option<(T, [T; 3])> {
let mut cash = T::ZERO;
let mut moved = [T::ZERO; 3];
for &(flow, side, amount) in lines {
let delta = signed(side, amount)?;
let slot = match flow {
Flow::Cash => &mut cash,
Flow::Operating => &mut moved[0],
Flow::Investing => &mut moved[1],
Flow::Financing => &mut moved[2],
};
*slot = slot.checked_add(delta)?;
}
Some((cash, moved))
}
/// The cash flows of an entry whose cash lines moved `cash` and whose
/// sections moved `moved` ([`entry_flows`]). `None` when they don't net
/// to zero, or on overflow.
pub fn flows_of<T: Amount>(cash: T, moved: [T; 3]) -> Option<EntryFlows<T>> {
// Balanced lines only: every part below rests on it.
let mut total = cash;
for &m in &moved {
total = total.checked_add(m)?;
}
if total != T::ZERO {
return None;
}
let mut flows = [T::ZERO; 3];
apply_cash(cash, &moved, &mut flows)?;
let mut noncash = [T::ZERO; 3];
for ((n, m), f) in noncash.iter_mut().zip(moved).zip(flows) {
*n = m.checked_add(f)?;
}
Some(EntryFlows {
cash,
flows,
noncash,
})
}
/// The credits and the debits among some movements (debit-positive):
/// `(Σ max(-m, 0), Σ max(m, 0))`.
fn credits_and_debits<T: Amount>(movements: &[T]) -> Option<(T, T)> {
let (mut credits, mut debits) = (T::ZERO, T::ZERO);
for &m in movements {
if m < T::ZERO {
credits = credits.checked_sub(m)?;
} else {
debits = debits.checked_add(m)?;
}
}
Some((credits, debits))
}
/// Which way money a member or a lender handled for the company went
/// (rules.md B-14 rule 11, D-42).
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub enum OnBehalf {
/// Paid for the company: sources credited (borrowed, contributed)
/// against uses debited (spent).
Paid,
/// Received for the company: sources debited (repaid, distributed)
/// against uses credited (collected).
Received,
}
impl OnBehalf {
/// The other way: what an entry's reversal does.
pub fn mirror(self) -> Self {
match self {
OnBehalf::Paid => OnBehalf::Received,
OnBehalf::Received => OnBehalf::Paid,
}
}
}
/// What a member or a lender paid, or received, for the company with no
/// cash account moving: a constructive receipt and disbursement (rules.md
/// B-14 rule 11, D-42). `sources` are what is left unsettled of the
/// entry's kinds that can pay or receive for the company (a financing
/// liability, a member's equity), `uses` of the kinds they can pay or
/// receive for, each debit-positive. [`OnBehalf::Paid`]: `amount =
/// min(source credits, use debits)`, cash in to the sources' credits and
/// out of the uses' debits (borrowed or contributed, then spent);
/// [`OnBehalf::Received`]: `amount = min(source debits, use credits)`,
/// cash in to the uses' credits and out of the sources' debits (collected,
/// then repaid or distributed). `from[i]` is source `i`'s cash (+ in) and
/// `to[j]` use `j`'s, each applied in order by [`apply_cash`]. `None` when
/// the slices differ in length, or on overflow.
///
/// ```text
/// GOAL: show money a member or lender handled for the company as the
/// company's own, borrowed (or contributed) and spent, without
/// inventing or losing a cent.
/// SOURCE: rules.md B-14 rule 11 (D-42; ASC 230 is silent, PwC Viewpoint
/// FSP 6.9.3.1, Deloitte DART Roadmap 7.2, BDO Blueprint 3.4).
/// INVARIANTS:
/// 1. The parts net to zero: Σ from + Σ to = 0, so the entry's cash
/// flows still sum to its cash.
/// 2. Each part settles its own movement, toward zero and never past it
/// (zero, or the opposite sign and no larger).
/// 3. The other way, minus the sources and minus the uses give minus
/// the parts (a reversal mirrors its original).
/// 4. As much is settled as can be: afterwards, paid, no source credit
/// is left beside a use debit; received, no source debit beside a use
/// credit.
/// ```
pub fn constructive<T: Amount>(
way: OnBehalf,
sources: &[T],
uses: &[T],
from: &mut [T],
to: &mut [T],
) -> Option<()> {
let (source_credits, source_debits) = credits_and_debits(sources)?;
let (use_credits, use_debits) = credits_and_debits(uses)?;
// The cash the sources take (+ in): what was paid, or minus what was
// received; the uses take the opposite.
let cash = match way {
OnBehalf::Paid => source_credits.min(use_debits),
OnBehalf::Received => source_debits.min(use_credits).checked_neg()?,
};
apply_cash(cash, sources, from)?;
apply_cash(cash.checked_neg()?, uses, to)
}
/// How much of an entry is an exchange inside investing and financing
/// that no cash settled (rules.md B-14 rule 7, ASC 230-10-50-4: debt
/// converted to equity, one asset traded for another). `debits` and
/// `credits` are the net debits and net credits of the entry's investing
/// and financing balance-sheet accounts (each account netted first; both
/// non-negative); `inflow` and `outflow` are the cash those two sections
/// took in and paid out (both non-negative; constructive cash included,
/// rule 11). Cash in settles credits and cash out settles debits; what's
/// left of the smaller side was exchanged:
/// `max(0, min(debits - outflow, credits - inflow))`.
pub fn exchanged<T: Amount>(debits: T, credits: T, inflow: T, outflow: T) -> Option<T> {
let d = debits.checked_sub(outflow)?;
let c = credits.checked_sub(inflow)?;
Some(d.min(c).max(T::ZERO))
}
/// Which way an entry moved value with its parties (rules.md B-35).
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub enum Direction {
/// The company paid the party, or gave it value: a line on the
/// party's own account would be a debit.
Paid,
/// The company received from the party: a line on its own account
/// would be a credit.
Received,
/// Neither: nothing moved with the party yet (a bill, an invoice, a
/// fee charged on its own card, a distribution still owed), or the
/// entry moved nothing with anyone (a close, a reclassification).
/// Counted in no total.
Neither,
}
impl Direction {
/// The other way: paid and received swap; neither stays neither.
pub fn flip(self) -> Self {
match self {
Direction::Paid => Direction::Received,
Direction::Received => Direction::Paid,
Direction::Neither => Direction::Neither,
}
}
/// The direction of a signed amount: paid above zero, received below,
/// neither at zero.
pub fn of<T: Amount>(amount: T) -> Self {
if amount > T::ZERO {
Direction::Paid
} else if amount < T::ZERO {
Direction::Received
} else {
Direction::Neither
}
}
/// Its wire name: `paid`, `received`, or `neither`.
pub fn key(self) -> &'static str {
match self {
Direction::Paid => "paid",
Direction::Received => "received",
Direction::Neither => "neither",
}
}
}
/// What an entry's parties split, and what of it counts in their totals
/// (rules.md B-35).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct PartyTarget<T> {
/// The whole, signed as a line on the parties' own account would be
/// (debit-positive): positive, the company paid or gave; negative, it
/// received.
pub amount: T,
/// Which way value moved.
pub direction: Direction,
/// The part of `amount` that moved as money (of a member's
/// contribution, what the K-1 worksheet counts as cash; of a
/// distribution, the money it paid): counted on both bases.
pub cash: T,
/// The part of `amount` that moved as property: counted on basis
/// "all" only.
pub in_kind: T,
}
/// The magnitude of `a`, or `None` past the type's range.
fn magnitude<T: Amount>(a: T) -> Option<T> {
if a < T::ZERO {
a.checked_neg()
} else {
Some(a)
}
}
/// The magnitude `m` with the sign of `like`, never a negative zero (a
/// zero `m` is the plain zero, whatever sign arithmetic left on it).
fn with_sign<T: Amount>(like: T, m: T) -> Option<T> {
if m == T::ZERO {
Some(T::ZERO)
} else if like < T::ZERO {
m.checked_neg()
} else {
Some(m)
}
}
/// The smaller of `a` and `b`.
fn least<T: Amount>(a: T, b: T) -> T {
if a < b { a } else { b }
}
/// What an entry's parties split and what of it counts (rules.md B-35
/// item 3, every case but a close and a reversal, which the caller
/// handles: a close is its parties' own-account movement with direction
/// neither, a reversal is [`reverse_target`] of its original's).
///
/// ```text
/// GOAL: one signed whole for an entry's parties, debit-positive as a line
/// on their own account, with its direction and what of it moved as
/// money or as property, so a property contribution and its
/// reversal never read alike, and a promise is never counted as if
/// it were paid.
/// SOURCE: rules.md B-35 (B-2 signs; DECISION, owner, 2026-10-20: a
/// member's entry counts what moved their capital, money is cash,
/// cards, the members' financing and loans, and a liability credit
/// never counts as paying that liability's own creditor; Helvering
/// v. Price: a promise to pay is not payment).
/// INPUTS (each signed debit-positive over the entry's lines):
/// capital: Some((e, property)) when every party named is a member: e
/// the movement of equity other than retained earnings; property what
/// property accounts took in (their debits, when e < 0) or gave up
/// (their credits, when e > 0).
/// net: the money paid (+) or received (−) (parties::entry_flow, a
/// named party's own liabilities not counted as money).
/// own: the movement of the parties' own accounts (payables,
/// receivables, liabilities owed to a party named).
/// debits: the entry's total debits.
/// INVARIANTS:
/// 1. capital with e < 0 (a contribution): amount = e; |in_kind| =
/// min(|e|, property⁺); cash the rest (what the K-1 worksheet counts
/// as cash: money, or what the member paid for the company).
/// 2. capital with e > 0 (a distribution): amount = e; cash = min(e,
/// net⁺), the money it paid; in_kind = min(e − cash, property⁺), the
/// property it gave; the rest (credited to a liability that isn't
/// money for the entry: a distribution declared, still owed) counts
/// as nothing until it is paid.
/// 3. In 1 and 2, direction is the sign of e, or neither when nothing
/// counts.
/// 4. Else net ≠ 0: amount = cash = net, in_kind = 0, direction its
/// sign.
/// 5. Else amount = own when it isn't zero, else debits; neither.
/// 6. cash and in_kind each have amount's sign or are zero (never a
/// negative zero), |cash| + |in_kind| ≤ |amount|, and direction is
/// neither exactly when both are zero.
/// 7. Odd, but for the debits fallback and a member's entry whose cash
/// isn't exactly its money (an expense booked straight to capital, a
/// debt converted, a distribution still owed): negating e, net and
/// own (property comes from the other side of the lines, so it keeps
/// its size) gives reverse_target of the result.
/// ```
///
/// `None` past the type's range.
pub fn party_target<T: Amount>(
capital: Option<(T, T)>,
net: T,
own: T,
debits: T,
) -> Option<PartyTarget<T>> {
if let Some((e, property)) = capital
&& e != T::ZERO
{
let whole = magnitude(e)?;
let property = if property > T::ZERO {
property
} else {
T::ZERO
};
let (cash, in_kind) = if e < T::ZERO {
let in_kind = least(property, whole);
(whole.checked_sub(in_kind)?, in_kind)
} else {
let paid = if net > T::ZERO {
least(net, whole)
} else {
T::ZERO
};
(paid, least(property, whole.checked_sub(paid)?))
};
let counted = cash.checked_add(in_kind)?;
return Some(PartyTarget {
amount: e,
direction: if counted == T::ZERO {
Direction::Neither
} else {
Direction::of(e)
},
cash: with_sign(e, cash)?,
in_kind: with_sign(e, in_kind)?,
});
}
if net != T::ZERO {
return Some(PartyTarget {
amount: net,
direction: Direction::of(net),
cash: net,
in_kind: T::ZERO,
});
}
Some(PartyTarget {
amount: if own != T::ZERO { own } else { debits },
direction: Direction::Neither,
cash: T::ZERO,
in_kind: T::ZERO,
})
}
/// A reversal's target from its original's (rules.md B-35 item 3; B-9: a
/// correction is the opposite entry): every amount negated (never to a
/// negative zero), paid and received swapped. An involution. `None` past
/// the type's range.
pub fn reverse_target<T: Amount>(t: PartyTarget<T>) -> Option<PartyTarget<T>> {
let neg = |a: T| {
if a == T::ZERO {
Some(T::ZERO)
} else {
a.checked_neg()
}
};
Some(PartyTarget {
amount: neg(t.amount)?,
direction: t.direction.flip(),
cash: neg(t.cash)?,
in_kind: neg(t.in_kind)?,
})
}
// ---------------------------------------------------------------------------
// Proration by days
// ---------------------------------------------------------------------------
/// Exact integer arithmetic the proration by days needs: money as a whole
/// number of its smallest step (`i128` in the engine; `i64` and, for the
/// harnesses whose properties relate a product to a quotient, `i32` under
/// Kani). Kept apart from [`Amount`]: proration multiplies and divides,
/// which no journal line ever does.
pub trait Units: Copy + Ord {
/// Zero.
const ZERO: Self;
/// One.
const ONE: Self;
/// `n`, exactly, or `None` when it doesn't fit.
fn from_u32(n: u32) -> Option<Self>;
/// `self + rhs`, or `None` on overflow.
fn checked_add(self, rhs: Self) -> Option<Self>;
/// `self - rhs`, or `None` on overflow.
fn checked_sub(self, rhs: Self) -> Option<Self>;
/// `self * rhs`, or `None` on overflow.
fn checked_mul(self, rhs: Self) -> Option<Self>;
/// `(self / rhs, self % rhs)` for `self >= 0` and `rhs > 0`; `None`
/// otherwise.
fn checked_div_rem(self, rhs: Self) -> Option<(Self, Self)>;
}
impl Units for i32 {
const ZERO: Self = 0;
const ONE: Self = 1;
fn from_u32(n: u32) -> Option<Self> {
i32::try_from(n).ok()
}
fn checked_add(self, rhs: Self) -> Option<Self> {
i32::checked_add(self, rhs)
}
fn checked_sub(self, rhs: Self) -> Option<Self> {
i32::checked_sub(self, rhs)
}
fn checked_mul(self, rhs: Self) -> Option<Self> {
i32::checked_mul(self, rhs)
}
fn checked_div_rem(self, rhs: Self) -> Option<(Self, Self)> {
if self < 0 || rhs <= 0 {
return None;
}
Some((self / rhs, self % rhs))
}
}
impl Units for i64 {
const ZERO: Self = 0;
const ONE: Self = 1;
fn from_u32(n: u32) -> Option<Self> {
Some(i64::from(n))
}
fn checked_add(self, rhs: Self) -> Option<Self> {
i64::checked_add(self, rhs)
}
fn checked_sub(self, rhs: Self) -> Option<Self> {
i64::checked_sub(self, rhs)
}
fn checked_mul(self, rhs: Self) -> Option<Self> {
i64::checked_mul(self, rhs)
}
fn checked_div_rem(self, rhs: Self) -> Option<(Self, Self)> {
if self < 0 || rhs <= 0 {
return None;
}
Some((self / rhs, self % rhs))
}
}
impl Units for i128 {
const ZERO: Self = 0;
const ONE: Self = 1;
fn from_u32(n: u32) -> Option<Self> {
Some(i128::from(n))
}
fn checked_add(self, rhs: Self) -> Option<Self> {
i128::checked_add(self, rhs)
}
fn checked_sub(self, rhs: Self) -> Option<Self> {
i128::checked_sub(self, rhs)
}
fn checked_mul(self, rhs: Self) -> Option<Self> {
i128::checked_mul(self, rhs)
}
fn checked_div_rem(self, rhs: Self) -> Option<(Self, Self)> {
if self < 0 || rhs <= 0 {
return None;
}
Some((self / rhs, self % rhs))
}
}
/// lcm(28, 29, 30, 31): every month's length divides it, so a day of any
/// month is a whole number of `MONTH_L`ths of a month, and proration needs
/// no fractions.
pub const MONTH_L: u32 = 377_580;
/// One calendar month's share of a span of days: `days` of the month's
/// `month_days`.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct MonthPart {
/// Days of the span in the month, 1 to `month_days`.
pub days: u32,
/// Days in the month, 28 to 31.
pub month_days: u32,
}
impl MonthPart {
/// Whether it is a share a calendar month can have: 28 to 31 days in
/// the month, 1 to all of them in the span.
pub fn is_valid(self) -> bool {
(28..=31).contains(&self.month_days) && (1..=self.month_days).contains(&self.days)
}
}
/// A part's weight in `MONTH_L`ths of a month: `days × (MONTH_L /
/// month_days)`, exactly. `None` for a part no month has.
pub fn part_weight<T: Units>(p: MonthPart) -> Option<T> {
if !p.is_valid() {
return None;
}
T::from_u32(p.days)?.checked_mul(T::from_u32(MONTH_L / p.month_days)?)
}
/// `num / den` rounded half away from zero to a multiple of `unit` (`num`
/// not negative; `den` and `unit` positive).
fn round_to_unit<T: Units>(num: T, den: T, unit: T) -> Option<T> {
let step = den.checked_mul(unit)?;
let (q, r) = num.checked_div_rem(step)?;
// Up when the remainder is half a step or more: compared as r >=
// step - r, so nothing is doubled and nothing can overflow.
let q = if r >= step.checked_sub(r)? {
q.checked_add(T::ONE)?
} else {
q
};
q.checked_mul(unit)
}
/// The exact cumulative charge of `total` (in units) spread over `months`
/// months by day, through `k` days of `part`, after earlier parts weighing
/// `before` `MONTH_L`ths; `last` marks the span's last part. Rounded half
/// away from zero (half up: nothing here is negative) to a multiple of
/// `unit`, or `total` itself when that rounds above it (a total that isn't
/// a whole number of units); and the last part's last day is `total`.
///
/// ```text
/// GOAL: how much of a total a span of days has used up by a given day,
/// each day of a month bearing the same share, the whole total
/// reached on the span's last day and never before.
/// SOURCE: docs/spec/rules.md B-15 (straight line, partial months by days;
/// ASC 360-10-35-4: "systematic and rational", as equitably as
/// possible to the periods served), B-16 (daily schedules, D-11),
/// B-21 (exact totals).
/// INVARIANTS (W = months × MONTH_L, m = part.month_days, d = part.days):
/// 1. Not the last part: round(total × (before + k × MONTH_L / m) / W):
/// the monthly rate total/months times the days held over the days
/// in each month.
/// 2. The last part: round(total × (before × d + (W − before) × k) /
/// (W × d)): what the earlier parts leave of the total, C = total ×
/// before / W, plus the remainder R = total − C spread evenly over
/// its d days. It is never "plugged": through an earlier day of the
/// last month it is prorated by days.
/// 3. It is non-decreasing in (part, k), never above total, continuous
/// at part boundaries ((i, days_i) equals (i + 1, 0)), and exactly
/// total at (last, d).
/// SCENARIOS:
/// 1. IF total is negative, months is 0, unit isn't positive, the part
/// is no month's (see MonthPart::is_valid), k > d, before is negative
/// or above W, a part but the last is charged through a day past W
/// (before + k × MONTH_L / m > W; prorate_by_days charges every part
/// but the last through its last day, so it refuses a part ending past
/// W), or any product overflows:
/// - SHOULD return None
/// - NEVER panic
/// BECAUSE a figure the books can't compute is refused (rules.md
/// B-28), and symbolic parts are not a calendar.
/// 2. IF 12,000.00 over 12 months from Jan 1, through Dec 15 (the last
/// part, 31 days, before = 11 months):
/// - SHOULD be 11,000.00 + 1,000.00 × 15/31 = 11,483.87
/// - NEVER 12,000.00 (the old plug)
/// BECAUSE the final month is charged by its days like any other.
/// ```
pub fn prorated_through<T: Units>(
total: T,
months: u32,
before: T,
part: MonthPart,
k: u32,
last: bool,
unit: T,
) -> Option<T> {
if total < T::ZERO
|| months == 0
|| unit <= T::ZERO
|| !part.is_valid()
|| k > part.days
|| before < T::ZERO
{
return None;
}
let whole = T::from_u32(months)?.checked_mul(T::from_u32(MONTH_L)?)?;
if before > whole {
return None;
}
let charged = if last {
if k == part.days {
// Exactly the total, even one that isn't a whole number of
// units (an asset an earlier version took in tenths of a cent).
return Some(total);
}
let d = T::from_u32(part.days)?;
let left = whole.checked_sub(before)?;
let elapsed = before
.checked_mul(d)?
.checked_add(left.checked_mul(T::from_u32(k)?)?)?;
round_to_unit(total.checked_mul(elapsed)?, whole.checked_mul(d)?, unit)?
} else {
let rate = T::from_u32(MONTH_L / part.month_days)?;
let elapsed = before.checked_add(T::from_u32(k)?.checked_mul(rate)?)?;
if elapsed > whole {
return None;
}
round_to_unit(total.checked_mul(elapsed)?, whole, unit)?
};
// A total that isn't a whole number of units can round above itself
// on the day before the last; the cap keeps every part non-negative.
Some(charged.min(total))
}
/// Split `total` (in units) over a span of `months` months cut into
/// calendar-month `parts`: `out[i]` is the cumulative charge through the
/// end of part `i` ([`prorated_through`]) less the one before it, and the
/// last part is `total` less all the others. `out` must be as long as
/// `parts`; on `None` its contents mean nothing.
///
/// ```text
/// GOAL: one month's posting of a span spread by day (depreciation,
/// daily prepaid and deferred-revenue schedules).
/// SOURCE: docs/spec/rules.md B-15, B-16 (D-11), B-21; plan/served.md P3
/// defect 9 (one shared prorate_by_days, Kani: parts sum to the
/// total, each is days × rate within one unit, the last absorbs
/// the remainder).
/// INVARIANTS:
/// 1. The parts sum to total exactly.
/// 2. Every part is >= 0.
/// 3. Each part but the last is within one unit of total × days_i /
/// (months × month_days_i).
/// 4. The last part is total − Σ others.
/// SCENARIOS:
/// 1. IF there are no parts, out isn't as long as parts, or prorated_
/// through refuses a part (the weights of all but the last above W,
/// among others): SHOULD return None, never panic.
/// 2. IF 1,200.00 over 12 months from Mar 15 (parts 17/31, eleven full
/// months, then 14 days):
/// - SHOULD be 54.84, eleven × 100.00, then 45.16
/// BECAUSE each day bears the same share, and the last part takes
/// what the others leave.
/// ```
///
/// Allocation-free and O(n): a loop over fixed slices, so the model
/// checker can prove it outright.
pub fn prorate_by_days<T: Units>(
total: T,
months: u32,
parts: &[MonthPart],
unit: T,
out: &mut [T],
) -> Option<()> {
if out.len() != parts.len() {
return None;
}
let (&last, rest) = parts.split_last()?;
let mut before = T::ZERO;
let mut charged = T::ZERO;
for (o, &p) in out.iter_mut().zip(rest) {
let through = prorated_through(total, months, before, p, p.days, false, unit)?;
*o = through.checked_sub(charged)?;
charged = through;
before = before.checked_add(part_weight(p)?)?;
}
// The last part is checked too (its weight before it within the span),
// and its whole is the total, so it takes the remainder.
let through = prorated_through(total, months, before, last, last.days, true, unit)?;
*out.last_mut()? = through.checked_sub(charged)?;
Some(())
}
// ---------------------------------------------------------------------------
// Catching up and truing up
// ---------------------------------------------------------------------------
/// What a run catches up: the largest amount, at least zero, that can be
/// added to what the books carry at every month end from the run's on
/// without carrying more than the schedule says there:
/// `max(0, min_i(scheduled[i] − posted[i]))`, where `scheduled[i]` and
/// `posted[i]` are cumulative at successive month ends starting with the
/// run's own. `None` when the slices differ in length or are empty, or on
/// overflow.
///
/// ```text
/// GOAL: a skipped month is caught up in the month the run is made, and a
/// run never overtakes the schedule at a month end already posted.
/// SOURCE: plan/served.md P3 "Settled in design" (2026-10-20): a month of
/// depreciation skipped is caught up in the month the run is made
/// (an immaterial miss; a material one is restated, ASC 250);
/// docs/spec/rules.md B-15.
/// INVARIANTS:
/// 1. The result is >= 0.
/// 2. Whenever every posted[i] <= scheduled[i], posted[i] + result <=
/// scheduled[i] for every i: the run never carries the books past the
/// schedule at any month end it reaches.
/// 3. The result is 0 or some scheduled[i] − posted[i]: with one month
/// (no run after this one), it is everything the schedule says is due
/// through it.
/// ```
pub fn catch_up<T: Amount>(scheduled: &[T], posted: &[T]) -> Option<T> {
if scheduled.len() != posted.len() {
return None;
}
let mut least: Option<T> = None;
for (&s, &p) in scheduled.iter().zip(posted) {
let gap = s.checked_sub(p)?;
least = Some(match least {
Some(l) if l <= gap => l,
_ => gap,
});
}
let least = least?;
Some(if least > T::ZERO { least } else { T::ZERO })
}
/// [`catch_up`] of every suffix at once: `out[i]` is `catch_up(&scheduled[i..],
/// &posted[i..])`, what a run at each month end posts. One pass from the
/// end, O(n), so a viewer can say of every month of a long life whether
/// anything is due for it. `None` when the slices differ in length, or on
/// overflow.
pub fn catch_ups<T: Amount>(scheduled: &[T], posted: &[T], out: &mut [T]) -> Option<()> {
if scheduled.len() != posted.len() || out.len() != scheduled.len() {
return None;
}
let mut least: Option<T> = None;
for ((&s, &p), o) in scheduled.iter().zip(posted).zip(out.iter_mut()).rev() {
let gap = s.checked_sub(p)?;
let l = match least {
Some(l) if l <= gap => l,
_ => gap,
};
least = Some(l);
*o = if l > T::ZERO { l } else { T::ZERO };
}
Some(())
}
/// Bring what the books carry (`posted`) to `target`: `(post, take_back)`,
/// both >= 0, one of them zero, with `posted + post − take_back = target`.
/// This is [`columns`] of `target − posted`: raising the books by `post`
/// and lowering them by `take_back` are a debit and a credit of the gap.
///
/// ```text
/// GOAL: a disposal clears exactly what the schedule says was used up
/// through its day, whatever the runs posted.
/// SOURCE: docs/spec/rules.md B-15 (a disposed asset depreciates through
/// its disposal day); Ledger::dispose_asset INVARIANT 1 (gain =
/// proceeds − book value at the disposal date).
/// ```
pub fn true_up<T: Amount>(target: T, posted: T) -> Option<(T, T)> {
columns(target.checked_sub(posted)?)
}
/// An asset's three basis figures ([`basis_figures`]).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct BasisFigures<T> {
/// The partnership's basis in contributed property, IRC §723: the
/// contributor's adjusted basis. `None` for a purchase.
pub tax_basis_723: Option<T>,
/// The basis tax depreciation starts from.
pub depreciable_basis: T,
/// Fair market value less the §723 basis at contribution, IRC §704(c):
/// positive a built-in gain, negative a built-in loss. `None` for a
/// purchase (not property contributed).
pub built_in_gain_704c: Option<T>,
}
/// An asset's basis figures from its rule and facts: `cost` the book cost
/// (a purchase's basis), `adjusted` the contributing member's adjusted
/// basis and `fmv` the fair market value at contribution (both ignored for
/// a purchase).
///
/// ```text
/// GOAL: the three tax figures of an asset, each named for what it is,
/// from one function the register, the tools and the viewer share.
/// SOURCE: docs/spec/rules.md B-25: IRC §1012(a) (cost); IRC §723 (the
/// contributor's adjusted basis carries over); Treas. Reg.
/// §1.168(i)-4(b)(1) (property converted from personal use: "the
/// lesser of its fair market value or its adjusted depreciable
/// basis"; DECISION D-41, owner 2026-10-20); Treas. Reg.
/// §1.704-3(a)(3)(ii) (built-in gain: "the excess of the
/// property's book value over the contributing partner's adjusted
/// tax basis upon contribution", book value being fair market
/// value at contribution, §1.704-3(a)(3)(i)).
/// INVARIANTS:
/// 1. Purchase: depreciable = cost; no §723 basis, no built-in gain.
/// 2. Contribution: tax_basis_723 = adjusted; built_in_gain_704c =
/// fmv − adjusted, negative exactly when adjusted > fmv (a built-in
/// loss, IRC §704(c)(1)(C)).
/// 3. Carryover723: depreciable = adjusted.
/// 4. PersonalUseConversion: depreciable = min(fmv, adjusted), at most
/// each of them and equal to one.
/// 5. NEVER wraps: None when a figure can't be represented.
/// ```
pub fn basis_figures<T: Amount>(
rule: BasisRule,
cost: T,
adjusted: T,
fmv: T,
) -> Option<BasisFigures<T>> {
Some(match rule {
BasisRule::Purchase => BasisFigures {
tax_basis_723: None,
depreciable_basis: cost,
built_in_gain_704c: None,
},
BasisRule::Carryover723 => BasisFigures {
tax_basis_723: Some(adjusted),
depreciable_basis: adjusted,
built_in_gain_704c: Some(fmv.checked_sub(adjusted)?),
},
BasisRule::PersonalUseConversion => BasisFigures {
tax_basis_723: Some(adjusted),
depreciable_basis: if fmv < adjusted { fmv } else { adjusted },
built_in_gain_704c: Some(fmv.checked_sub(adjusted)?),
},
})
}
/// A project's unrecovered cost from its tagged revenue and expenses to
/// date: what it would take to be repaid in full (rules.md B-37 item 4).
///
/// ```text
/// GOAL: the "if repaid" figure of work done on spec, from one function
/// the tools, the viewer and bookspec share.
/// SOURCE: docs/spec/rules.md B-37 item 4 (ASC 450-30-25-1: a hoped-for
/// payment is a gain contingency, never recorded before it is
/// received; so this is a figure, never a receivable).
/// INVARIANTS:
/// 1. Never below zero.
/// 2. expenses - revenue when expenses >= revenue; zero otherwise.
/// 3. Never above max(expenses, 0) when revenue >= 0 (expenses can be
/// negative: a reimbursement credited to the expense above its cost).
/// 4. NEVER wraps: None when the difference can't be represented.
/// ```
pub fn unrecovered_cost<T: Amount>(revenue: T, expenses: T) -> Option<T> {
let gap = expenses.checked_sub(revenue)?;
Some(if gap > T::ZERO { gap } else { T::ZERO })
}
#[cfg(test)]
mod tests {
use super::*;
/// rules.md B-14 rule 3, by hand. Equipment 1,000 for 300 cash and a
/// 700 note: investing takes the 300, the note's 700 and the rest of
/// the equipment's are the noncash part.
#[test]
fn part_cash_part_noncash_takes_only_the_cash() {
use Flow::*;
let f = entry_flows(&[
(Investing, Side::Debit, 1000i64),
(Cash, Side::Credit, 300),
(Financing, Side::Credit, 700),
])
.unwrap();
assert_eq!(f.cash, -300);
assert_eq!(f.flows, [0, -300, 0]);
assert_eq!(f.noncash, [0, 700, -700]);
// A fee withheld from a loan: Dr cash 9,900, Dr fee 100 / Cr loan
// 10,000. Operating moves with the cash (a debit), so takes none.
let f = entry_flows(&[
(Cash, Side::Debit, 9900i64),
(Operating, Side::Debit, 100),
(Financing, Side::Credit, 10000),
])
.unwrap();
assert_eq!(f.flows, [0, 0, 9900]);
assert_eq!(f.noncash, [100, 0, -100]);
}
/// Lines that don't net to zero are refused (review item 12): no part
/// is made up for them.
#[test]
fn unbalanced_lines_have_no_flows() {
use Flow::*;
assert_eq!(
entry_flows(&[(Operating, Side::Debit, 5i64), (Investing, Side::Debit, 5)]),
None
);
assert_eq!(
entry_flows(&[(Cash, Side::Debit, 5i64), (Investing, Side::Credit, 4)]),
None
);
// Too little against the cash: nothing is invented.
let mut out = [0i64; 2];
assert_eq!(apply_cash(10, &[-3, 4], &mut out), None);
assert_eq!(apply_cash(10, &[-3], &mut out), None);
}
/// The exchange measure (rules.md B-14 rule 7) on the review's
/// hand-checked cases.
#[test]
fn exchanged_matches_the_hand_checked_cases() {
// Debt to equity, 500.
assert_eq!(exchanged(500i64, 500, 0, 0), Some(500));
// Part-cash purchase with the seller's note: D 1,000, C 700, cash
// out 300.
assert_eq!(exchanged(1000i64, 700, 0, 300), Some(700));
// Note received for equipment: D 700, C 1,000, cash in 300.
assert_eq!(exchanged(700i64, 1000, 300, 0), Some(700));
// Trade-in with 1,500 boot: D 2,000, C 1,000, cash out 1,500.
assert_eq!(exchanged(2000i64, 1000, 0, 1500), Some(500));
// A cash sale: nothing debited, cash in 500.
assert_eq!(exchanged(0i64, 1000, 500, 0), Some(0));
// A cash purchase: cash out covers every debit.
assert_eq!(exchanged(1000i64, 0, 0, 1000), Some(0));
// Equipment a lender paid for (rule 11): 1,000 borrowed in, 1,000
// spent out, nothing exchanged.
assert_eq!(exchanged(1000i64, 1000, 1000, 1000), Some(0));
}
/// rules.md B-14 rule 11 (D-42), by hand.
#[test]
fn constructive_pays_and_receives_for_the_company() {
use OnBehalf::{Paid, Received};
// A member pays a 59 expense (Dr expense / Cr due to members): the
// source's 59 credit pays the use's 59 debit.
let (mut from, mut to) = ([0i64; 1], [0i64; 1]);
constructive(Paid, &[-59], &[59], &mut from, &mut to).unwrap();
assert_eq!((from, to), ([59], [-59]));
// Its reversal, the other way, mirrors it.
constructive(Received, &[59], &[-59], &mut from, &mut to).unwrap();
assert_eq!((from, to), ([-59], [59]));
// The reversal's shape read as a payment settles nothing.
constructive(Paid, &[59], &[-59], &mut from, &mut to).unwrap();
assert_eq!((from, to), ([0], [0]));
// A 100 credit from the source against 60 of uses (the other 40
// against something else): only 60 is paid; uses take in order.
let (mut from, mut to) = ([0i64; 2], [0i64; 2]);
constructive(Paid, &[-100, 0], &[25, 35], &mut from, &mut to).unwrap();
assert_eq!((from, to), ([60, 0], [-25, -35]));
// Two sources, one use smaller than both: the first source pays
// first.
constructive(Paid, &[-30, -30], &[40, 0], &mut from, &mut to).unwrap();
assert_eq!((from, to), ([30, 10], [-40, 0]));
// Each way settles only its own side.
constructive(Paid, &[-50, 20], &[50, -20], &mut from, &mut to).unwrap();
assert_eq!((from, to), ([50, 0], [-50, 0]));
constructive(Received, &[-50, 20], &[50, -20], &mut from, &mut to).unwrap();
assert_eq!((from, to), ([0, -20], [0, 20]));
// Nothing against: nothing moves.
constructive(Paid, &[-50, 0], &[-10, 0], &mut from, &mut to).unwrap();
assert_eq!((from, to), ([0, 0], [0, 0]));
// Mismatched lengths are refused.
let one = [-1i64];
assert_eq!(
constructive(Paid, &one, &[1], &mut [0i64; 2], &mut [0]),
None
);
assert_eq!(
constructive(Paid, &one, &[1], &mut [0i64], &mut [0; 2]),
None
);
assert_eq!(Paid.mirror(), Received);
assert_eq!(Received.mirror(), Paid);
}
fn part(days: u32, month_days: u32) -> MonthPart {
MonthPart { days, month_days }
}
/// Every month length divides MONTH_L, and it is the least such.
#[test]
fn month_l_is_the_lcm_of_month_lengths() {
for m in 28..=31 {
assert_eq!(MONTH_L % m, 0, "{m}");
}
for smaller in 1..MONTH_L {
assert!((28..=31).any(|m| smaller % m != 0), "{smaller}");
}
assert_eq!(part_weight::<i64>(part(31, 31)), Some(i64::from(MONTH_L)));
assert_eq!(part_weight::<i64>(part(1, 28)), Some(13_485));
assert_eq!(part_weight::<i64>(part(0, 30)), None);
assert_eq!(part_weight::<i64>(part(32, 31)), None);
assert_eq!(part_weight::<i64>(part(27, 27)), None);
}
/// Spec scenario 2 of prorated_through, and the brief's 1,200.00 from
/// March 15 (prorate_by_days scenario 2), in cents.
#[test]
fn the_final_month_is_prorated_and_a_mid_month_span_splits_by_day() {
let l = i128::from(MONTH_L);
let dec15 = prorated_through(1_200_000i128, 12, 11 * l, part(31, 31), 15, true, 1);
assert_eq!(dec15, Some(1_148_387));
assert_eq!(
prorated_through(1_200_000i128, 12, 11 * l, part(31, 31), 31, true, 1),
Some(1_200_000)
);
let mut parts = vec![part(17, 31)];
parts.extend([30, 31, 30, 31, 31, 30, 31, 30, 31, 31, 28].map(|m| part(m, m)));
parts.push(part(14, 31));
let mut out = vec![0i128; parts.len()];
prorate_by_days(120_000i128, 12, &parts, 1, &mut out).unwrap();
let mut want = vec![5_484i128];
want.extend([10_000; 11]);
want.push(4_516);
assert_eq!(out, want);
}
/// Half a unit rounds away from zero (up, for the non-negative amounts
/// here): 0.01 over 2 months from the 1st gives 0.005 after one month.
#[test]
fn half_a_unit_rounds_up() {
let mut out = [0i64; 2];
prorate_by_days(1, 2, &[part(31, 31), part(28, 28)], 1, &mut out).unwrap();
assert_eq!(out, [1, 0]);
// Just under half a unit stays down: 0.01 over 3 months.
let mut out = [0i64; 3];
prorate_by_days(
1,
3,
&[part(31, 31), part(28, 28), part(31, 31)],
1,
&mut out,
)
.unwrap();
assert_eq!(out, [0, 1, 0]);
}
/// R4(a): a total that isn't a whole number of units (100.006 in
/// thousandths, rounded to cents) never makes the last part negative.
#[test]
fn a_total_finer_than_its_unit_never_gives_a_negative_part() {
let l = i64::from(MONTH_L);
let mut out = [0i64; 2];
prorate_by_days(100_006, 2, &[part(31, 31), part(28, 28)], 10, &mut out).unwrap();
assert_eq!(out, [50_000, 50_006]);
// 30 of 31 days of a one-month span: 100.006 × 30/31 = 96.780
// exactly, already whole cents.
assert_eq!(
prorated_through(100_006i64, 1, 0, part(31, 31), 30, true, 10),
Some(96_780)
);
// One day short of a 4,000-month span: 100.006 less 0.0008 is
// 100.0052, which rounds to 100.01, past the total: capped there,
// so the day left gets 0, never -0.004.
let w = 4_000 * l;
assert_eq!(
prorated_through(100_006i64, 4_000, w - l, part(30, 31), 30, false, 10),
Some(100_006)
);
}
/// Spec scenario 1 of prorated_through (R4(b), R4(c)): malformed input
/// is refused, never a panic.
#[test]
fn malformed_proration_is_refused() {
let l = i64::from(MONTH_L);
let p = part(10, 30);
assert_eq!(prorated_through(-1i64, 1, 0, p, 1, false, 1), None);
assert_eq!(prorated_through(1i64, 0, 0, p, 1, false, 1), None);
assert_eq!(prorated_through(1i64, 1, 0, p, 1, false, 0), None);
assert_eq!(prorated_through(1i64, 1, 0, p, 11, false, 1), None);
assert_eq!(prorated_through(1i64, 1, -1, p, 1, false, 1), None);
assert_eq!(prorated_through(1i64, 1, l + 1, p, 1, true, 1), None);
assert_eq!(prorated_through(1i64, 1, 0, part(0, 30), 0, false, 1), None);
assert_eq!(
prorated_through(1i64, 1, 0, part(31, 30), 1, false, 1),
None
);
// A part but the last that ends past the span.
assert_eq!(prorated_through(1i64, 1, l, part(1, 31), 1, false, 1), None);
let mut out = [0i64; 3];
assert_eq!(
prorate_by_days(
100,
1,
&[part(31, 31), part(31, 31), part(5, 30)],
1,
&mut out
),
None
);
assert_eq!(prorate_by_days(100i64, 1, &[], 1, &mut []), None);
assert_eq!(
prorate_by_days(100i64, 1, &[part(31, 31)], 1, &mut []),
None
);
assert_eq!(
prorated_through(i64::MAX, 600, 0, part(31, 31), 31, false, 1),
None
);
}
/// prorated_through over every span of 1 to 3 months starting on any
/// day of a common year and a leap year, walked day by day, for a
/// spread of totals and both units: it never falls (within a month and
/// across a month's end: the charge through a month's last day is the
/// next month's through none of its days), never exceeds the total, and
/// is the total on the last day. Exhaustive over those spans; the
/// relation between two divisions is too costly for Kani's solver
/// (docs/verification.md), and Lean proves the law for the model.
/// Not under Miri, which looks for undefined behavior: this is safe
/// integer arithmetic the other kernel tests already take through it,
/// and walked exhaustively under the interpreter it held `just miri`
/// for over ten minutes.
#[test]
#[cfg_attr(
miri,
ignore = "exhaustive arithmetic: the other kernel tests cover it under Miri"
)]
fn the_charge_never_falls_and_is_continuous_over_real_calendars() {
use chrono::NaiveDate;
let mut start = NaiveDate::from_ymd_opt(2027, 1, 1).unwrap();
let stop = NaiveDate::from_ymd_opt(2029, 1, 1).unwrap();
let mut spans = 0;
while start < stop {
for months in 1..=3u32 {
let end = start
.checked_add_months(chrono::Months::new(months))
.unwrap();
let parts: Vec<_> = crate::calendar::month_parts(start, end).collect();
for total in [0i64, 1, 3, 7, 10, 999, 100_005, 65_536] {
for unit in [1i64, 10] {
let mut before = 0i64;
let mut last_charge = 0i64;
for p in &parts {
for k in 0..=p.part.days {
let c = prorated_through(
total, months, before, p.part, k, p.last, unit,
)
.unwrap();
assert!(
c >= last_charge && c <= total,
"{start} + {months}: {c} after {last_charge}"
);
last_charge = c;
}
before += part_weight::<i64>(p.part).unwrap();
}
assert_eq!(last_charge, total, "{start} + {months}");
}
}
spans += 1;
}
start = start.succ_opt().unwrap();
}
assert_eq!(spans, 731 * 3);
}
/// catch_up: everything due through the run's month when no run comes
/// after it; never past a later month end already posted.
#[test]
fn a_catch_up_never_overtakes_a_posted_month_end() {
// Jan run, Feb skipped, a Feb run with nothing after it: Feb's.
assert_eq!(catch_up(&[200i64], &[100]), Some(100));
// March already caught February up: a Feb run posts nothing.
assert_eq!(catch_up(&[200i64, 300], &[100, 300]), Some(0));
// A run carried past the schedule (an old tie cent): nothing.
assert_eq!(catch_up(&[200i64], &[201]), Some(0));
// January reversed after March ran: January posts it back.
assert_eq!(catch_up(&[100i64, 200, 300], &[0, 100, 200]), Some(100));
assert_eq!(catch_up::<i64>(&[], &[]), None);
assert_eq!(catch_up(&[1i64], &[1, 2]), None);
}
/// catch_ups is catch_up of every suffix: positive and distinct ones
/// (a catch_ups that wrote zeros would fail), and a month carried past
/// the schedule (zero from it back).
#[test]
fn catch_ups_is_every_suffixs_catch_up() {
let (s, p) = ([100i64, 200, 300, 400], [0i64, 100, 150, 250]);
let mut out = [0i64; 4];
catch_ups(&s, &p, &mut out).unwrap();
for i in 0..4 {
assert_eq!(Some(out[i]), catch_up(&s[i..], &p[i..]), "{i}");
}
assert_eq!(out, [100, 100, 150, 150]);
let (s, p) = ([100i64, 200, 300, 400], [0i64, 300, 200, 400]);
catch_ups(&s, &p, &mut out).unwrap();
for i in 0..4 {
assert_eq!(Some(out[i]), catch_up(&s[i..], &p[i..]), "{i}");
}
assert_eq!(out, [0, 0, 0, 0]);
let mut none: [i64; 0] = [];
assert_eq!(catch_ups::<i64>(&[], &[], &mut none), Some(()));
assert_eq!(catch_ups(&s, &p, &mut [0i64; 3]), None);
}
/// true_up is the gap's columns.
#[test]
fn a_true_up_reaches_the_target() {
assert_eq!(true_up(5_500i64, 5_000), Some((500, 0)));
assert_eq!(true_up(5_500i64, 6_000), Some((0, 500)));
assert_eq!(true_up(5_500i64, 5_500), Some((0, 0)));
}
/// basis_figures INVARIANTS 1-4, by hand: a 1,440.00 laptop the member
/// holds at 1,688.40 (personal use): §723 1,688.40, depreciable
/// 1,440.00, built-in loss 248.40; as business property, depreciable
/// 1,688.40; a purchase at 900.00: depreciable 900.00 and nothing else.
#[test]
fn basis_figures_by_rule() {
let (fmv, adj) = (144_000i64, 168_840i64);
let p = basis_figures(BasisRule::PersonalUseConversion, fmv, adj, fmv).unwrap();
assert_eq!(
p,
BasisFigures {
tax_basis_723: Some(adj),
depreciable_basis: fmv,
built_in_gain_704c: Some(-24_840),
}
);
let c = basis_figures(BasisRule::Carryover723, fmv, adj, fmv).unwrap();
assert_eq!(c.depreciable_basis, adj);
assert_eq!(c.built_in_gain_704c, Some(-24_840));
// Value above basis: depreciable is the basis, a built-in gain.
let g = basis_figures(BasisRule::PersonalUseConversion, 1000, 400, 1000).unwrap();
assert_eq!(
(g.depreciable_basis, g.built_in_gain_704c),
(400, Some(600))
);
let b = basis_figures(BasisRule::Purchase, 90_000i64, 7, 8).unwrap();
assert_eq!(
b,
BasisFigures {
tax_basis_723: None,
depreciable_basis: 90_000,
built_in_gain_704c: None,
}
);
assert_eq!(
basis_figures(BasisRule::Carryover723, 0, i64::MAX, i64::MIN),
None
);
}
#[test]
fn max_line_amount_is_one_quadrillion() {
assert_eq!(MAX_LINE_AMOUNT, Decimal::from(1_000_000_000_000_000u64));
assert!(MAX_LINE_AMOUNT.in_line_range());
assert!(!(MAX_LINE_AMOUNT + Decimal::ONE).in_line_range());
assert!("0.0000000001".parse::<Decimal>().unwrap().in_line_range());
assert!(!"0.00000000001".parse::<Decimal>().unwrap().in_line_range());
// Trailing zeros are not precision.
assert!("1.000000000000".parse::<Decimal>().unwrap().in_line_range());
}
/// Regression (Kani `apportion_is_exact`, 2026-10-13): a shortfall of
/// two units and a bit, with one part, was accepted and handed almost
/// two units to that part. Spec scenario 1: more than one unit short
/// per part is refused.
#[test]
fn apportion_refuses_a_shortfall_of_a_unit_per_part_or_more() {
let mut parts = [0i64];
assert_eq!(apportion(1805, &mut parts, &[0], 903), None);
assert_eq!(parts, [0]);
let mut parts = [0i64, 0];
assert_eq!(apportion(1806, &mut parts, &[0, 0], 903), None);
// Just under: accepted.
let mut parts = [0i64, 0];
assert_eq!(apportion(1805, &mut parts, &[1, 0], 903), Some(()));
assert_eq!(parts, [1805, 0]);
}
/// The i64 model's line range: up to 2^40 either way, inclusive.
#[test]
fn i64_line_range_is_two_to_the_fortieth() {
assert!((1i64 << 40).in_line_range());
assert!((-(1i64 << 40)).in_line_range());
assert!(!((1i64 << 40) + 1).in_line_range());
assert!(!i64::MIN.in_line_range());
}
/// B-9: a reversal flips every side and keeps accounts and amounts, so
/// with the original it nets every account to zero.
#[test]
fn a_reversal_flips_every_line_and_nets_to_zero() {
let lines = [
(1u8, Side::Debit, 70i64),
(2, Side::Credit, 50),
(3, Side::Credit, 20),
];
let rev = reversal(&lines);
assert_eq!(rev.len(), lines.len());
for (o, r) in lines.iter().zip(&rev) {
assert_eq!((r.0, r.1, r.2), (o.0, flip(o.1), o.2));
}
let both = movements(lines.iter().chain(&rev).copied()).unwrap();
assert_eq!(both, vec![(1, 0), (2, 0), (3, 0)]);
}
/// Spec scenario 1's preconditions: parts and remainders pair up, and
/// the unit is positive; otherwise nothing is apportioned.
#[test]
fn apportion_refuses_mismatched_inputs_or_a_nonpositive_unit() {
let mut parts = [0i64, 0];
assert_eq!(apportion(0, &mut parts, &[0], 1), None);
assert_eq!(parts, [0, 0]);
let mut none: [i64; 0] = [];
assert_eq!(apportion(0, &mut none, &[], 0), None);
assert_eq!(apportion(0, &mut none, &[], -1), None);
}
/// apportion_cumulative scenario 1: mismatched lengths, a bad unit, an
/// input out of line range, or a shortfall apportion refuses: None,
/// and the parts untouched.
#[test]
fn apportion_cumulative_refuses_mismatched_or_out_of_range_inputs() {
let big = (1i64 << 40) + 1;
for (total, parts, rems, unit, given) in [
(4i64, [2i64, 2], [0i64, 0], 1i64, &[0i64][..]),
(4, [2, 2], [0, 0], 0, &[0, 0][..]),
(4, [2, 2], [0, 0], big, &[0, 0][..]),
(big, [2, 2], [0, 0], 1, &[0, 0][..]),
(4, [big, 2], [0, 0], 1, &[0, 0][..]),
(4, [2, 2], [0, 0], 1, &[big, 0][..]),
// Three units short of two parts: not rounding.
(7, [2, 2], [0, 0], 1, &[0, 0][..]),
] {
let mut p = parts;
assert_eq!(
apportion_cumulative(total, &mut p, &rems, unit, given),
None,
"{total} {parts:?} {unit} {given:?}"
);
assert_eq!(p, parts);
}
// Remainders that don't pair with the parts: apportion's refusal.
let mut p = [2i64, 2];
assert_eq!(apportion_cumulative(4, &mut p, &[0], 1, &[0, 0]), None);
assert_eq!(p, [2, 2]);
}
/// apportion_cumulative scenario 2 (cents, i64): three cents closed
/// one at a time gave A all three; the fourth cent's close apportions
/// the running 4 cents (2 / 2) and takes back what A and B had.
#[test]
fn apportion_cumulative_trues_up_a_legacy_split() {
let mut parts = [2i64, 2];
apportion_cumulative(4, &mut parts, &[0, 0], 1, &[3, 0]).unwrap();
assert_eq!(parts, [-1, 2]);
// A running total of 5: floors 2 / 2 with equal remainders, so the
// tied unit goes to the first (3 / 2), less what each had (3 / 1).
let mut parts = [2i64, 2];
apportion_cumulative(5, &mut parts, &[5, 5], 1, &[3, 1]).unwrap();
assert_eq!(parts, [0, 1]);
}
/// With no parts, only a zero whole is fully apportioned.
#[test]
fn apportion_to_no_parts_accepts_only_zero() {
let mut none: [i64; 0] = [];
assert_eq!(apportion(0, &mut none, &[], 1), Some(()));
assert_eq!(apportion(5, &mut none, &[], 1), None);
}
/// A zero movement's columns are both a plain zero, never "-0" (found
/// by mutation triage, 2026-10-13: it returned a negative-zero credit).
#[test]
fn a_zero_movement_has_no_negative_zero_column() {
let (d, c) = columns(Decimal::ZERO).unwrap();
assert_eq!(
(d.to_string(), c.to_string()),
("0".to_string(), "0".to_string())
);
}
#[test]
fn credit_line_sides() {
assert_eq!(credit_line(5i64), Some((Side::Credit, 5)));
assert_eq!(credit_line(-5i64), Some((Side::Debit, 5)));
assert_eq!(credit_line(0i64), None);
}
}