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), exactDecimalmoney end to end, and banker’s rounding. Plus in-languagetestblocks 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— andox 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, notpub query, soox run-scenario --extent <name>(a concept extent lookup) does not enumerate them — the derived values are read throughox testasserts and the corpus pin instead. assert [not] derivable F(args)reads with world-honest three-valued semantics keyed onF’s world assumption. These concepts are closed-world (the package default), so absence is definite non-derivability — bothderivableandnot derivableare assertable here.- The second
tests/derived.arfile is auto-discovered byox testbut is notmod-wired intoroot.ar, soox buildnever 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.
Source
The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.
root.ar
//! Double-entry accounting — the quantitative-modeling wall, made a running
//! proof (RFD 0029).
//!
//! Before RFD 0029 this domain was *inexpressible declaratively*: a rule head
//! could not carry a computed value, and two aggregates could not be compared,
//! so neither the per-account balance `debits − credits` nor the ledger
//! invariant `sum(debits) == sum(credits)` could be written. This example is
//! the journey's exact wall — it exercises, end to end:
//!
//! * **body-level binding** `x = expr` (derived values) — RFD 0029 §2.1;
//! * **aggregates as bindable terms** with relation-atom sources and the
//! outer-variable grouping (per-account `sum`) — §2.2–§2.4;
//! * **comparing two aggregates** — the double-entry invariant — §2.3;
//! * **exact decimal arithmetic** end to end — money never via f64;
//! * **banker's rounding** (`round_half_even`) — §2.7;
//! * **decimal demo-harness arguments** — RFD 0029 R-B10.
//!
//! All concepts use the neutral `pub type` introducer (`std::core`'s
//! no-commitment baseline) — no ontological commitment lives in the language.
mod ledger;
mod tests;
ledger.ar
//! The ledger model.
//!
//! An `Account` holds postings. A journal `Entry` groups the postings of one
//! transaction. Each `Posting` records an exact `Decimal` `amount`, a `side`
//! (`"D"` debit / `"C"` credit), the `Account` it hits, and the `Entry` it
//! belongs to (carried as relations so the aggregates can join them).
//!
//! Double-entry's one invariant: within every entry, total debits equal total
//! credits. With RFD 0029 that is a single `check` comparing two aggregates.
pub type Account {
mut name: String,
}
pub type Entry {
mut memo: String,
}
pub type Posting {
mut amount: Decimal,
mut side: String,
}
/// `postedTo(p, a)` — posting `p` hits account `a`.
pub rel postedTo(mut posting: Posting, mut account: Account);
/// `inEntry(p, e)` — posting `p` belongs to journal entry `e`.
pub rel inEntry(mut posting: Posting, mut entry: Entry);
// ── Derived values ────────────────────────────────────────────────
//
// Per-account balance = Σ debits − Σ credits, grouped by account (the
// grouping is the outer bound variable `acct`, the standard Datalog reading).
// Both aggregates are BOUND to variables, then the balance is a derived value
// — exactly the head-carries-a-computed-value shape RFD 0029 R-B2 unblocks.
pub derive accountDebits(acct, total) :-
acct: Account,
total = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "D");
pub derive accountCredits(acct, total) :-
acct: Account,
total = sum(p.amount for p in Posting, postedTo(p, acct), p.side == "C");
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 double-entry invariant ────────────────────────────────────
//
// Within every entry, total debits == total credits. Two aggregates compared
// (RFD 0029 R-B3): a binding for each side, then `!=` flags the imbalance.
// A balanced entry derives nothing; an unbalanced one fires the check.
// ANCHOR: 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",
message: "journal entry is not balanced — total debits must equal total credits"
};
// ANCHOR_END: check
// A balanced entry: the positive twin of the check, so the corpus test can
// read the *balanced* set directly (a `check` populates no IDB).
pub derive balancedEntry(e) :-
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;
// ── Rounding ──────────────────────────────────────────────────────
//
// A 7.5%% sales-tax line on each account's debit total, rounded to cents with
// banker's rounding (the money default — round-half-even avoids the upward
// bias of half-away-from-zero). `round_half_even(x, 2)` is exact: a `Decimal`
// stays a `Decimal`, never via f64.
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);
// ── Seeding ───────────────────────────────────────────────────────
//
// One mutation per posting keeps the demo harness a flat script. Amounts
// arrive as decimal harness arguments (RFD 0029 R-B10).
// ANCHOR: mutate
pub mutate openAccount(a: Account, name: String) {
insert iof(a, Account);
update a: Account set { name = name };
}
// ANCHOR_END: mutate
pub mutate openEntry(e: Entry, memo: String) {
insert iof(e, Entry);
update e: Entry set { memo = memo };
}
/// Post a SINGLE leg. Useful for the negative case: posting one leg without
/// its matching opposite leaves the entry unbalanced, which the
/// `EntryNotBalanced` Error guard rejects (double-entry is enforced, not
/// merely reported). The balanced demo uses `postPair` instead.
pub mutate post1(p: Posting, account: Account, entry: Entry, amount: Decimal, side: String) {
insert iof(p, Posting);
update p: Posting set { amount = amount };
update p: Posting set { side = side };
insert postedTo(p, account);
insert inEntry(p, entry);
}
/// Post one balanced journal entry in a single atomic transaction: a debit
/// leg and a matching credit leg. Posting both legs together keeps the
/// `EntryNotBalanced` delta guard satisfied at every committed state — a
/// half-posted entry (debit without its credit) would gain a violation and
/// be rejected, so the two legs must commit together (double-entry IS atomic).
pub mutate postPair(
debit: Posting,
credit: Posting,
debitAccount: Account,
creditAccount: Account,
entry: Entry,
amount: Decimal
) {
insert iof(debit, Posting);
update debit: Posting set { amount = amount };
update debit: Posting set { side = "D" };
insert postedTo(debit, debitAccount);
insert inEntry(debit, entry);
insert iof(credit, Posting);
update credit: Posting set { amount = amount };
update credit: Posting set { side = "C" };
insert postedTo(credit, creditAccount);
insert inEntry(credit, entry);
}
tests/derived.ar
//! A second `tests/` file that is NOT `mod`-wired (no `mod derived;` in root).
//! `ox test` auto-discovers it; `ox build` never sees it (test-mode-only).
//!
//! A discovered top-level `tests/*.ar` references package items by their
//! package-absolute path (`pkg::`), since `super` from a plain `tests/` file
//! anchors at the `tests/` directory (no `ledger.ar` sibling there).
use pkg::ledger::{ Account };
test "an auto-discovered tests/ file runs its tests" {
let a = insert Account { name: "Auto" };
assert a.name == "Auto";
}
tests/mod.ar
//! In-language tests for the double-entry ledger (§16, the `test` atom).
//!
//! Each `test "name" { ... }` is a named imperative block run top-to-bottom
//! against a FRESH store by `ox test`. The body is the mutate-body statement
//! set (`let` / `insert` / mutation calls) plus the new `assert <bool-expr>;`
//! statement: true is a PASS, false a FAIL, an eval-error an ERROR, and
//! execution continues past a failed assert (unlike `require`, which aborts).
//!
//! An assert reads the DEDUCTIVE plane: a condition that names a derived
//! predicate / `pub query` (`accountBalance(cash)`) is evaluated against the
//! reasoner's materialized extent at the fixpoint of the current committed
//! state, after the body's writes (read-your-writes over committed+derived).
use super::ledger::{ Account, Entry, Posting };
// A constructed entity's scalar fields read back through field access — the
// simplest setup-then-assert flow (construct, then assert on `.field`).
test "a constructed account carries its name" {
let cash = insert Account { name: "Cash" };
assert cash.name == "Cash";
}
// Multiple asserts in one body; every one is recorded. Decimal amounts stay
// exact (never via f64), so the equality is precise.
test "postings carry exact decimal amounts and sides" {
let debit = insert Posting { amount: 100.50, side: "D" };
let credit = insert Posting { amount: 100.50, side: "C" };
assert debit.amount == 100.50;
assert credit.amount == 100.50;
assert debit.side == "D";
assert credit.side == "C";
}
// Setup interleaves with assertions: construct an entry, then assert on its
// field, then construct more — no separate fixture block needed.
test "an entry carries its memo and a second posting still reads back" {
let e = insert Entry { memo: "sale 1" };
assert e.memo == "sale 1";
let p = insert Posting { amount: 50.25, side: "D" };
assert p.amount == 50.25;
}
// The deductive-plane assert (the point of testing a reasoning system): after
// posting one balanced entry through the `postPair` mutation, the per-account
// balance derive `accountBalance(acct, bal)` is materialized and the keyed
// read `accountBalance(cash)` yields the computed value. The debit side nets
// +amount, the credit side -amount — exactly the §19 `x.method() == v` shape,
// evaluated against the reasoner's output, not a stored scalar.
test "accountBalance derives the posted amount per account" {
let cash = insert Account { name: "Cash" };
let rev = insert Account { name: "Revenue" };
let e = insert Entry { memo: "sale 1" };
postPair(cash, rev, cash, rev, e, 100.50);
assert accountBalance(cash) == 100.50;
assert accountBalance(rev) == - 100.50;
}
// A second derived aggregate read: the per-account debit total.
test "accountDebits derives the debit total per account" {
let cash = insert Account { name: "Cash" };
let rev = insert Account { name: "Revenue" };
let e = insert Entry { memo: "sale 1" };
postPair(cash, rev, cash, rev, e, 50.25);
assert accountDebits(cash) == 50.25;
assert accountCredits(rev) == 50.25;
}
// ── Derivability assertions (§17.14 / §7.9) ────────────────────────
//
// The membership / non-derivability half of the test atom's vocabulary.
// `assert [not] derivable F(args)` tests whether a matching row is in F's
// materialized extent, with world-honest three-valued semantics keyed on F's
// world assumption (§6.9). The ledger concepts are closed-world (the package
// default), so absence reads as definite non-derivability — both directions
// are assertable here.
// A balanced entry: posting a matching debit/credit pair makes
// `balancedEntry(e)` derivable (a value-less membership derive — the clean
// case the v1 value-read assert could not express). PRESENT ⇒ `derivable`
// passes.
test "a balanced entry is derivable" {
let cash = insert Account { name: "Cash" };
let rev = insert Account { name: "Revenue" };
let e = insert Entry { memo: "balanced sale" };
postPair(cash, rev, cash, rev, e, 100.00);
assert derivable balancedEntry(e);
}
// An entry with a single un-matched leg is NOT balanced, so `balancedEntry`
// does not derive it. Under the closed-world default, absence is definite
// non-derivability ⇒ `not derivable` passes (the non-derivability assertion
// the v1 assert could not make — a missing row errored).
test "an unbalanced entry is not derivable as balanced" {
let cash = insert Account { name: "Cash" };
let p = insert Posting { amount: 0.00, side: "D" };
let e = insert Entry { memo: "half-posted" };
post1(p, cash, e, 75.00, "D");
assert not derivable balancedEntry(e);
}