Double-entry accounting: aggregates, balance, and an invariant

Area: Rules, aggregates & recursion Teaches: quantitative modeling that was inexpressible declaratively before RFD 0029 — a rule head that carries a computed value, two aggregates compared (the double-entry invariant as a single check), exact Decimal money end to end, and banker’s rounding. Plus in-language test blocks that assert against the derived plane. Prerequisites: first-class relations (the postings join through relations); check constraints. Run: ox build examples/double_entry_v0 && ox run-scenario examples/double_entry_v0 — and ox test examples/double_entry_v0

Double-entry is the canonical small accounting model: every transaction posts a debit and a matching credit, and the books balance when, within every journal entry, total debits equal total credits. It is also the exact wall RFD 0029 broke through — a rule head could not carry a computed value, and two aggregates could not be compared, so neither a per-account balance nor the balancing invariant could be written.

What to read in ledger.ar

A head carries a computed value. The per-account balance is Σ debits − Σ credits, grouped by the outer-bound acct; both aggregates bind to a variable, then bal is a derived value:

pub derive accountBalance(acct, bal) :- acct: Account,
    debits  = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    credits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "C"),
    bal     = debits - credits;

The invariant compares two aggregates — a balanced entry derives nothing, an unbalanced one fires the check:

pub check EntryNotBalanced(e: Entry) :-
    e: Entry,
    debits  = sum(p.amount for p in Posting, inEntry(p, e), p.side == "D"),
    credits = sum(p.amount for p in Posting, inEntry(p, e), p.side == "C"),
    debits != credits
    => Diagnostic { severity: Severity::Error, code: "Ledger::E001", /* … */ };

Money is exact, with banker’s rounding. A Decimal stays a Decimal — never via f64 — and round_half_even ties to even (the money default, avoiding the upward bias of half-away-from-zero):

pub derive accountTax(acct, tax) :- acct: Account,
    debits = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D"),
    raw    = debits * 0.075,
    tax    = round_half_even(raw, 2);

Running it

ox run-scenario posts two balanced entries (Cash 100.50 / Revenue 100.50 and Cash 50.25 / Revenue 50.25), each leg pair committing atomically so the EntryNotBalanced Error guard is satisfied at every committed state:

scenario: applied 6 mutation(s) from examples/double_entry_v0/demo.toml

The interesting outputs are the derived values themselves, and the package asserts them directly with in-language test blocks. ox test runs each test "name" { … } against a fresh store and reports pass/fail:

PASS  a constructed account carries its name
PASS  postings carry exact decimal amounts and sides
PASS  an entry carries its memo and a second posting still reads back
PASS  accountBalance derives the posted amount per account
PASS  accountDebits derives the debit total per account
PASS  a balanced entry is derivable
PASS  an unbalanced entry is not derivable as balanced
PASS  an auto-discovered tests/ file runs its tests

8 passed, 0 failed, 0 errored, 0 inconclusive

The accountBalance test asserts accountBalance(cash) == 100.50 against the reasoner’s materialized extent — a deductive-plane assert, the point of testing a reasoning system. After the full demo harness the books read: accountBalance = {(cash, 150.75), (revenue, -150.75)}, and accountTax(cash) = round_half_even(11.30625, 2) = 11.31 (rounded to cents under round-half-even — here .30625 is past the half-cent, so it rounds up; the tie-to-even rule only changes the result on an exact x.xx5 boundary).

Honest caveats (what runs today)

• The ledger’s interesting predicates are pub derive, not pub query, so ox run-scenario --extent <name> (a concept extent lookup) does not enumerate them — the derived values are read through ox test asserts and the corpus pin instead.
• assert [not] derivable F(args) reads with world-honest three-valued semantics keyed on F’s world assumption. These concepts are closed-world (the package default), so absence is definite non-derivability — both derivable and not derivable are assertable here.
• The second tests/derived.ar file is auto-discovered by ox test but is not mod-wired into root.ar, so ox build never sees it (test-mode only).

This example is compiled and run in CI; a corpus test (oxc-runtime/tests/examples_corpus.rs) pins the exact decimal balances (150.75 / −150.75), the per-account totals, and the banker’s-rounded tax (11.31), so the aggregate semantics can’t drift from the language.