feat(bookspec): GnuCash as the second engine, its differences settled (P13 step 5)

bookspec-gnucash implements the Engine trait over the oracle container
(oracle/gnucash/books.py) and claims the rules whose examples ask only
for balances. It passes BS-entry-3, BS-ledger-3, BS-statement-1 and
BS-statement-2 and differs from three examples, each adjudicated from the
sources and pinned by tests: GnuCash accepts an unbalanced entry and
parks the difference in an Imbalance account (BS-entry-1 refuses it); it
reads a credit of minus 100 as a debit (BS-entry-2 is a convention that
removes the ambiguity); it rounds 10.005 to 10.01 silently (BS-ledger-1
is the owner's choice not to). The example stands in each case: GnuCash
is a cross-check, not the authority.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HS8WZziDnyxunC23MUxrLp

Cargo.lock

@@ -34,6 +34,16 @@ dependencies = [
  "toml",
 ]
 
+[[package]]
+name = "bookspec-gnucash"
+version = "0.1.0"
+dependencies = [
+ "bookspec-checker",
+ "bookspec-runner",
+ "rust_decimal",
+ "serde_json",
+]
+
 [[package]]
 name = "bookspec-runner"
 version = "0.1.0"

Cargo.toml

@@ -3,7 +3,7 @@
 # repository (P13 step 6, D-34).
 [workspace]
 resolver = "2"
-members = ["checker", "runner"]
+members = ["checker", "runner", "gnucash"]
 
 [workspace.package]
 edition = "2024"

README.md

@@ -421,6 +421,16 @@ the 1st, among others) and `untagged_control_line` (a hand line on a
 receivables or payables control account, which only a document may post
 to: rules.md B-38's control guard).
 
+The refusals of the ledger's own laws (BS-entry, BS-ledger, BS-period)
+are spelled `unbalanced` (debits differ from credits), `too_few_lines`,
+`negative_amount` and `zero_amount` (BS-entry-2), `finer_than_minor_unit`
+(an amount finer than the currency's smallest unit, BS-ledger-1),
+`parent_type_mismatch` (a child account of another type than its parent,
+BS-ledger-2), `already_reversed` (BS-ledger-6) and `period_closed` (an
+entry dated inside a closed period, BS-period-2). A refused entry may
+carry the amount the books refuse (zero or negative, in the amount's
+exact decimal spelling); an accepted one carries a positive amount.
+
 `cash_flow` (rules.md B-14): the statement of cash flows for `[from, to]`.
 
 | key | the value |
@@ -453,6 +463,68 @@ event taken or refused as it says, on the books' own store. Each query is
 then checked by the crate that answers it (the table above), so the shape
 never rots either.
 
+## The specification, the laws, the checks (P13 steps 4 and 5)
+
+- `spec/` is the specification text: `00-model.md` (definitions, the
+  model, the five laws, how an example is checked) and one file per area
+  (`entry.md`, `ledger.md`, ... `format.md`), each rule a section with its
+  status, its MUST/MUST NOT/MAY statement, its sources (a vendored source
+  with a verbatim pin, or an exact external reference), its symbolic form,
+  its examples by id and its applicability. `spec/rules-index.md` is the
+  table from `docs/spec/rules.md`'s B-1 to B-45. The checker's
+  `tests/spec.rs` fails the build when a rule lacks its section, a
+  statement lacks MUST/SHOULD/MAY, a pin is not verbatim in its vendored
+  source, a rule's examples differ from the catalogue's, or the edition
+  passes 60 pages.
+- `lean/` is the five laws as Lean theorems (`Bookspec.law_*`), ported
+  from `verify/lean`; `lake build` in that directory builds them and
+  `lake env lean Audit.lean` prints their axioms, which the checker's
+  `tests/lean.rs` requires to be only `propext`, `Quot.sound` and
+  `Classical.choice`.
+- The checker derives expected figures itself (`checker/src/derive.rs`):
+  an engine-free reference model with exact decimals replays an example's
+  entries, reversals, close, bills and invoices and computes its
+  `trial_balance`, `balances`, `profit_and_loss` and `entry` figures from
+  the rules' symbolic forms, and checks that each refusal the example
+  expects is justified by its rule. An example whose figure disagrees
+  fails `checker/tests/derive.rs`, before any engine is consulted. What
+  the model does not cover is reported as skipped, never passed.
+- `gnucash/` is the second engine: GnuCash 5.10 in the oracle container
+  (`just oracle` builds it), driven through `oracle/gnucash/books.py`.
+  `cargo test -p bookspec-gnucash -- --ignored` runs it (it needs
+  Docker). It claims the rules whose examples ask only for balances and
+  passes `BS-entry-3`, `BS-ledger-3`, `BS-statement-1` and
+  `BS-statement-2`.
+
+### GnuCash, the second engine: where it differs
+
+GnuCash is a cross-check, never the authority (`docs/oracle.md`, "Who is
+right"). It differs from three examples, each settled from the sources
+and pinned by `gnucash/tests/gnucash.rs`:
+
+- **`entry-an-unbalanced-entry-is-refused`.** GnuCash accepts debits of
+  100.00 against credits of 90.00 and parks the ten dollars in an
+  `Imbalance-USD` account of its own making; the accounts it lists no
+  longer net to zero. BS-entry-1 (Pacioli ch. 36; IRS Pub. 583: "the
+  total debits must equal the total credits") says such an entry is
+  refused. The example stands; GnuCash records a difference, flagged for
+  the user to repair, instead of refusing it.
+- **`entry-a-line-amount-is-positive`.** GnuCash takes a credit of
+  minus 100.00 as a debit of 100.00, both lines debits, and parks 200.00
+  in the Imbalance account. BS-entry-2 is a CONVENTION (no authority
+  forbids a negative amount); the example stands as the convention the
+  specification chose, and GnuCash's reading is the very ambiguity the
+  convention removes.
+- **`ledger-a-fraction-of-a-cent-is-refused`.** GnuCash rounds 10.005 to
+  10.01 silently. BS-ledger-1 is a CHOICE (the owner, 2026-10-13, found
+  by the first GnuCash cross-check): the books never round silently. An
+  engine's pick is its own; GnuCash's is the other option, recorded.
+
+The example `ledger-a-mistake-is-reversed-never-erased` and the others
+that need an engine's own reversal link or entry query are not claimed by
+the GnuCash adapter: GnuCash has no reversal link, so it cannot answer
+`already_reversed`.
+
 ## Licence and sources
 
 The examples state rules in their own words with the paragraph cited

gnucash/Cargo.toml

@@ -0,0 +1,18 @@
+[package]
+name = "bookspec-gnucash"
+version = "0.1.0"
+edition.workspace = true
+license.workspace = true
+repository.workspace = true
+description = "A second engine for bookspec: GnuCash, driven through the oracle container's files."
+
+[dependencies]
+bookspec-checker = { path = "../checker" }
+serde_json = "1"
+rust_decimal = "1"
+
+[dev-dependencies]
+bookspec-runner = { path = "../runner" }
+
+[lints]
+workspace = true

gnucash/src/lib.rs

@@ -0,0 +1,250 @@
+//! GnuCash as a second bookspec engine (`plan/served.md` P13 step 5).
+//!
+//! The adapter keeps an example's chart and entries as the oracle's JSON
+//! books (`oracle/gnucash/books.py`: accounts, entries, as-of days) and
+//! asks GnuCash 5.10, in its pinned container, for each balance. GnuCash
+//! is a cross-check, never the authority (`docs/oracle.md`, "Who is
+//! right"): where it differs from an example, the difference is
+//! adjudicated from the sources and recorded, not conformed to.
+//!
+//! Only what GnuCash itself answers is claimed: the balance queries
+//! (`trial_balance`, `balances`), by the rules whose examples ask nothing
+//! else. GnuCash never refuses an entry (it books the difference to an
+//! `Imbalance` account), so a refused event is *accepted* here, as it
+//! would be by a GnuCash user, and the runner reports the difference.
+
+use std::collections::BTreeMap;
+use std::io::Write;
+use std::process::{Command, Stdio};
+use std::str::FromStr;
+
+use bookspec_checker::{
+    Area, ChangeSpec, Claims, Engine, Event, Query, Refusal, RuleId, Setup, fallback_refusal,
+};
+use rust_decimal::Decimal;
+use serde_json::{Value, json};
+
+/// The oracle container (`just oracle` builds it from `oracle/gnucash`).
+pub const IMAGE: &str = "wanderbooks-gnucash-oracle";
+
+/// The rules this adapter claims: those whose examples ask only for
+/// balances, which GnuCash answers itself.
+pub fn claimed() -> Vec<RuleId> {
+    vec![
+        RuleId::new(Area::Entry, 1),
+        RuleId::new(Area::Entry, 2),
+        RuleId::new(Area::Entry, 3),
+        RuleId::new(Area::Ledger, 1),
+        RuleId::new(Area::Ledger, 3),
+        RuleId::new(Area::Statement, 1),
+        RuleId::new(Area::Statement, 2),
+    ]
+}
+
+/// One account of the book handed to GnuCash.
+struct Account {
+    code: String,
+    kind: &'static str,
+    normal_debit: bool,
+}
+
+/// GnuCash, as bookspec's `Engine`.
+#[derive(Default)]
+pub struct GnuCash {
+    accounts: Vec<Account>,
+    entries: Vec<Value>,
+    /// Each event's entry, by event number (1-based), for reversals.
+    event_entries: BTreeMap<usize, usize>,
+    events: usize,
+}
+
+impl GnuCash {
+    /// An empty engine.
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    fn id(&self, code: &str) -> Option<usize> {
+        self.accounts
+            .iter()
+            .position(|a| a.code == code)
+            .map(|i| i + 1)
+    }
+
+    fn book(&self, as_of: &str) -> Value {
+        let accounts: Vec<Value> = self
+            .accounts
+            .iter()
+            .enumerate()
+            .map(|(i, a)| json!({"id": i + 1, "code": a.code, "name": a.code, "type": a.kind}))
+            .collect();
+        json!({"accounts": accounts, "entries": self.entries, "as_of": [as_of]})
+    }
+
+    /// GnuCash's own balance of every account as of a day: debits
+    /// positive, exact decimal strings, by account code.
+    fn balances(&self, as_of: &str) -> Result<BTreeMap<String, Decimal>, Refusal> {
+        let mut child = Command::new("docker")
+            .args(["run", "--rm", "-i", IMAGE])
+            .stdin(Stdio::piped())
+            .stdout(Stdio::piped())
+            .stderr(Stdio::null())
+            .spawn()
+            .map_err(|e| unavailable(format!("docker: {e}")))?;
+        let books = json!([self.book(as_of)]);
+        child
+            .stdin
+            .take()
+            .unwrap()
+            .write_all(books.to_string().as_bytes())
+            .map_err(|e| unavailable(format!("docker stdin: {e}")))?;
+        let out = child
+            .wait_with_output()
+            .map_err(|e| unavailable(format!("docker: {e}")))?;
+        if !out.status.success() {
+            return Err(unavailable(
+                "the GnuCash oracle failed; build it with `just oracle`".into(),
+            ));
+        }
+        let results: Value = serde_json::from_slice(&out.stdout)
+            .map_err(|e| unavailable(format!("oracle output: {e}")))?;
+        let at = &results[0]["balances"][as_of];
+        let mut map = BTreeMap::new();
+        for (i, a) in self.accounts.iter().enumerate() {
+            let v = at[(i + 1).to_string()]
+                .as_str()
+                .ok_or_else(|| unavailable(format!("no balance for {}", a.code)))?;
+            map.insert(
+                a.code.clone(),
+                Decimal::from_str(v).map_err(|e| unavailable(e.to_string()))?,
+            );
+        }
+        Ok(map)
+    }
+}
+
+fn unavailable(why: String) -> Refusal {
+    fallback_refusal(
+        RuleId::new(Area::Ledger, 1),
+        format!("the GnuCash oracle: {why}"),
+    )
+}
+
+fn not_supported(what: &str) -> Refusal {
+    fallback_refusal(
+        RuleId::new(Area::Ledger, 1),
+        format!("the GnuCash adapter does not take {what}"),
+    )
+}
+
+impl Engine for GnuCash {
+    fn load(&mut self, setup: &Setup) -> Result<(), Refusal> {
+        for a in &setup.accounts {
+            let (kind, normal_debit) = match a.kind.as_str() {
+                "asset" => ("Asset", true),
+                "liability" => ("Liability", false),
+                "equity" => ("Equity", false),
+                "revenue" => ("Revenue", false),
+                "expense" => ("Expense", true),
+                other => return Err(not_supported(&format!("account type {other}"))),
+            };
+            self.accounts.push(Account {
+                code: a.code.clone(),
+                kind,
+                normal_debit,
+            });
+        }
+        if setup.currency != "USD" {
+            return Err(not_supported("a currency other than USD"));
+        }
+        Ok(())
+    }
+
+    fn apply(&mut self, event: &Event) -> Result<(), Refusal> {
+        self.events += 1;
+        let n = self.events;
+        let date = event
+            .date
+            .clone()
+            .ok_or_else(|| not_supported("an undated event"))?;
+        let description = event.description.clone().unwrap_or_default();
+        if !event.lines.is_empty() {
+            let mut lines = Vec::new();
+            for l in &event.lines {
+                let account = self
+                    .id(&l.account)
+                    .ok_or_else(|| not_supported("an unknown account"))?;
+                lines.push(json!({"account": account, "side": l.side, "amount": l.amount}));
+            }
+            self.entries
+                .push(json!({"date": date, "description": description, "lines": lines}));
+            self.event_entries.insert(n, self.entries.len() - 1);
+            return Ok(());
+        }
+        if let Some(of) = event.reverses {
+            // GnuCash has no reversal link; a user reverses by writing the
+            // opposite transaction, which is what is done here.
+            let idx = *self
+                .event_entries
+                .get(&of)
+                .ok_or_else(|| not_supported("a reversal of an event that posted nothing"))?;
+            let original = self.entries[idx].clone();
+            let flipped: Vec<Value> = original["lines"]
+                .as_array()
+                .unwrap()
+                .iter()
+                .map(|l| {
+                    let side = if l["side"] == "debit" {
+                        "credit"
+                    } else {
+                        "debit"
+                    };
+                    json!({"account": l["account"], "side": side, "amount": l["amount"]})
+                })
+                .collect();
+            self.entries
+                .push(json!({"date": date, "description": description, "lines": flipped}));
+            self.event_entries.insert(n, self.entries.len() - 1);
+            return Ok(());
+        }
+        Err(not_supported("this kind of event"))
+    }
+
+    fn query(&self, q: &Query) -> Result<Value, Refusal> {
+        let as_of = q
+            .as_of
+            .clone()
+            .ok_or_else(|| not_supported("a query without as_of"))?;
+        match q.name.as_str() {
+            "trial_balance" | "balances" => {
+                let balances = self.balances(&as_of)?;
+                let mut out = serde_json::Map::new();
+                for a in &self.accounts {
+                    let b = balances[&a.code];
+                    let mut shown = if q.name == "balances" && !a.normal_debit {
+                        -b
+                    } else {
+                        b
+                    };
+                    if shown.is_zero() {
+                        shown = Decimal::ZERO;
+                    }
+                    if shown.scale() < 2 {
+                        shown.rescale(2);
+                    }
+                    out.insert(a.code.clone(), Value::String(shown.to_string()));
+                }
+                Ok(Value::Object(out))
+            }
+            other => Err(not_supported(&format!("the {other} query"))),
+        }
+    }
+
+    fn claims(&self) -> Claims {
+        Claims::new(claimed())
+    }
+
+    fn change(&mut self, _change: &ChangeSpec) -> Result<(), Refusal> {
+        Err(not_supported("a change"))
+    }
+}

gnucash/tests/gnucash.rs

@@ -0,0 +1,137 @@
+//! GnuCash, run through bookspec's examples (`just oracle` builds the
+//! container). Needs Docker, so the test is ignored by default:
+//! `cargo test -p bookspec-gnucash -- --ignored --nocapture`.
+
+use std::path::{Path, PathBuf};
+
+use bookspec_checker::{Example, rules};
+use bookspec_gnucash::{GnuCash, claimed};
+
+fn examples() -> Vec<Example> {
+    let dir = Path::new(env!("CARGO_MANIFEST_DIR")).join("../examples");
+    let mut files: Vec<PathBuf> = std::fs::read_dir(dir)
+        .unwrap()
+        .map(|e| e.unwrap().path())
+        .filter(|p| p.extension().is_some_and(|x| x == "toml"))
+        .collect();
+    files.sort();
+    files
+        .iter()
+        .map(|f| Example::from_toml(&std::fs::read_to_string(f).unwrap()).unwrap())
+        .collect()
+}
+
+/// The differences GnuCash shows, each settled from the sources
+/// (`bookspec/README.md`, "GnuCash, the second engine"). A new difference,
+/// or one that goes away, fails this test until it is adjudicated again.
+const ADJUDICATED: [(&str, &str); 3] = [
+    (
+        "entry-an-unbalanced-entry-is-refused",
+        "event 2: accepted, expected refused: unbalanced",
+    ),
+    (
+        "entry-a-line-amount-is-positive",
+        "event 1: accepted, expected refused: negative_amount",
+    ),
+    (
+        "ledger-a-fraction-of-a-cent-is-refused",
+        "event 1: accepted, expected refused: finer_than_minor_unit",
+    ),
+];
+
+fn run_claimed() -> bookspec_runner::Report {
+    let claimed = claimed();
+    let mut wanted = std::collections::BTreeSet::new();
+    for r in rules().iter().filter(|r| claimed.contains(&r.id)) {
+        wanted.extend(r.examples.iter().copied());
+    }
+    let examples: Vec<Example> = examples()
+        .into_iter()
+        .filter(|e| wanted.contains(e.id.as_str()))
+        .collect();
+    bookspec_runner::run(&examples, rules(), |_| GnuCash::new())
+}
+
+#[test]
+#[ignore = "needs Docker and the GnuCash image: `just oracle`"]
+fn gnucash_differs_only_where_it_was_adjudicated() {
+    let report = run_claimed();
+    let found: Vec<(&str, &str)> = report
+        .examples
+        .iter()
+        .filter_map(|e| e.failure.as_deref().map(|f| (e.id.as_str(), f)))
+        .collect();
+    let mut want: Vec<(&str, &str)> = ADJUDICATED.to_vec();
+    want.sort();
+    let mut got = found.clone();
+    got.sort();
+    assert_eq!(got, want, "GnuCash's differences changed: adjudicate again");
+    // The rules that every example passes are passed.
+    for rule in [
+        "BS-entry-3",
+        "BS-ledger-3",
+        "BS-statement-1",
+        "BS-statement-2",
+    ] {
+        let id = bookspec_checker::RuleId::parse(rule).unwrap();
+        assert_eq!(report.rules[&id], bookspec_runner::Outcome::Pass, "{rule}");
+    }
+}
+
+/// The evidence the adjudications rest on, from GnuCash's own answers:
+/// what it did with the entry it accepted.
+#[test]
+#[ignore = "needs Docker and the GnuCash image: `just oracle`"]
+fn what_gnucash_did_with_the_entries_the_specification_refuses() {
+    use bookspec_checker::Engine;
+    use std::str::FromStr;
+    let by_id = |id: &str| examples().into_iter().find(|e| e.id == id).unwrap();
+    let net = |id: &str, event: usize| -> rust_decimal::Decimal {
+        let ex = by_id(id);
+        let mut g = GnuCash::new();
+        g.load(&ex.setup).unwrap();
+        for e in ex.events.iter().take(event) {
+            g.apply(e).expect("GnuCash accepts it");
+        }
+        let q = ex
+            .expect
+            .iter()
+            .find(|x| x.query == "trial_balance")
+            .unwrap()
+            .query();
+        let answer = g.query(&q).unwrap();
+        answer
+            .as_object()
+            .unwrap()
+            .values()
+            .map(|v| rust_decimal::Decimal::from_str(v.as_str().unwrap()).unwrap())
+            .sum()
+    };
+    // Debits 100.00 against credits 90.00: the accounts GnuCash lists no
+    // longer net to zero; ten dollars sit where GnuCash parked them, in an
+    // Imbalance account of its own making.
+    assert_eq!(
+        net("entry-an-unbalanced-entry-is-refused", 2).to_string(),
+        "10.00"
+    );
+    // A credit of minus 100.00 is booked as a debit of 100.00: both lines
+    // are debits, and 200.00 sits in the Imbalance account.
+    assert_eq!(
+        net("entry-a-line-amount-is-positive", 1).to_string(),
+        "200.00"
+    );
+    // 10.005 on each side is rounded to the cent, silently: GnuCash's USD
+    // balance reads 10.01 (the choice rules.md B-3 records the owner took
+    // the other way, after the first cross-check found it).
+    let ex = by_id("ledger-a-fraction-of-a-cent-is-refused");
+    let mut g = GnuCash::new();
+    g.load(&ex.setup).unwrap();
+    g.apply(&ex.events[0]).unwrap();
+    let q = ex
+        .expect
+        .iter()
+        .find(|x| x.query == "trial_balance")
+        .unwrap()
+        .query();
+    assert_eq!(g.query(&q).unwrap()["1000"], "10.01");
+}