Prototypes FolioP32 · Bookkeeping

The proof

A property test runs two laptops and the server from a seed. Each step is one random operation: a laptop posts an entry, sends an invoice, registers a bill, corrects or reverses an entry, imports a bank file, matches a bank line, closes a quarter, tries to save an entry that does not balance, loses its network or syncs, and some syncs are lost on the way. After every step the invariants are checked on the server and on both laptops. At the end both laptops come online and must hold the server’s entries exactly. This page runs the same code as the test in node; a seed gives the same run every time.

Starting. The first run begins when the page has loaded.

The invariants

InvariantCheckedResult

The operations

OperationTimes

The last seed, step by step

    How Folio is built
    1. The books are a log of events that is only ever appended to: an entry, an invoice, a bill, a reversal, a bank file, a match and a close. Each laptop keeps the log in IndexedDB and works out the entries, the reports and the VAT return from it, so it opens and posts with no network. A service worker keeps the app itself.
    2. An event’s id is the laptop and its own sequence number, such as Anna:12. The laptop sends the events it made with the number of events it already has from the server, and gets back what was taken, what was refused and why, and every event after its number. The server stores an id once, so an event sent again after a lost answer counts once.
    3. The server keeps the one order of events. A laptop shows the server’s events in that order, then its own waiting ones. After a sync both laptops have the same log, so the same voucher and invoice numbers, the same trial balance and the same VAT return.
    4. To correct an entry, Folio posts the entry that reverses it and the corrected one, as one event. Two laptops can therefore never overwrite each other: two entries made offline both arrive, and a second reversal of the same entry is refused with the name of who reversed it first.
    5. Every check is the same code on the laptop and on the server (books.mjs): an entry must balance in whole øre, a VAT line must be 25 % of its line, an invoice or a bill is never paid more than is open, a bank line is matched once, and a closed quarter takes no entry. When two laptops match one bank line offline, the server takes the first to arrive and tells the other.
    6. A bank file is read as Danske Bank, Nordea and most Danish banks export it: semicolons, Danish dates and amounts, Windows-1252 or UTF-8. A line’s id comes from its date, amount, text and balance, so two overlapping files or the same file on two laptops give one set of lines. The matcher scores each open invoice, bill, payroll and VAT settlement by the amount, a number or a name in the text, and the date against the due date, and shows the reasons. A person confirms.
    7. The VAT return has the boxes of the Danish form. Each box is worked out from the VAT lines, and checked against the base lines and against the accounts. Closing a quarter posts the settlement to account 6950 and locks the quarter.
    8. The proof: a property test with its own seeded random generator runs thousands of random operations on two laptops, with offline periods and syncs in random order, and checks after every step that every entry balances, the trial balance sums to zero, the VAT return equals the VAT postings, a locked quarter never changes, nothing counts twice and every change is kept or refused with a reason, and at the end that both laptops hold the server’s entries. Four flawed versions show that the test finds each kind of mistake.