Mini-Ledger: batch admission without locks

A demo of yichus admit: given a batch of transfers, declared balance rules, and the real handler, the checker computes which subset can commit together in one write, and explains every operation it turns away.

This is a demo of Yichus, a research checker for programs written in Bosatsu (a small, total, functional language from a separate project that this checker builds on). The problem it demonstrates: TigerBeetle, a financial-transactions database, admits a whole batch of transfers in one write because its schema and invariants are fixed in advance. Doing the same for user-declared invariants needs three things. Value-indexed footprints: whether two transfers conflict or commute depends on which account ids their inputs name, not just on which table they touch. An escrow declaration: balances move by signed deltas and invariants are interval bounds. That is the escrow-transaction method (O'Neil, 1986), which reserves each update's worst case against the bound so admission needs only interval arithmetic, never the exact balance. And a query mode on an existing checker: Yichus's interleaving checker (see the interleaving-checker demo) asks whether the declared properties hold under every interleaving; yichus admit runs the same order-enumeration engine as a search for a subset of this batch and a witness ordering (one concrete execution order, exhibited as evidence) under which every property holds. A Yichus/Spec::EscrowSpec declares all three; the sources are below.

The results on this page are not screenshots: on every deploy, the site build reruns yichus admit against the sources shown and writes the JSON this page renders (the runs are rows in the deploy manifest, executed by the deploy workflow). The domain is a minimal ledger with four accounts starting at A 200, B 60, C 40, D 150. Every balance must stay ≥ 0, and account D is a credit account capped at 200. There is one operation, transfer(source, target, amount), written as an ordinary guarded handler.

Reading the sources: Bosatsu's layout is Python-like; struct declares a record type, match/case pattern-match, <- binds a result inside an IO block, and exposes names the packages whose types appear in a package's exported values.

loading…

loading…

loading…

1. Escrow admission of the sample batch

The batch is the eight transfers below. For each operation the solver evaluates the spec's key and amount functions against the concrete input, so it knows which account ids the operation touches. That set of ids is its value-indexed footprint. Operations that touch the same key conflict; operations whose keys are all distinct commute. Per account, the solver keeps an escrow interval [initial − Σdebits, initial + Σcredits] over the admitted set and admits greedily in arrival order: an operation is admitted only if every declared bound holds at the worst case of every ordering of the admitted set. That order-independence is what removes the locks: no execution order of the admitted set can break a bound, so the whole set commits in one round. A deferred operation gets a why-trace: which bound, which key, and which admitted operations consumed the headroom.

loading…

yichus admit ledger.bosatsu ledger.spec.bosatsu ledger_handlers.bosatsu \
  --batch batch-sample.json --result admission.json
# exit 0 — replay verified

To run this locally: clone github.com/snoble/yichus (needs git, a JVM 17+, and sbt), then run sbt assembly, which writes yichus.jar under target/. Set alias yichus="java -jar $(pwd)/target/scala-*/yichus.jar" and run the command above from demos/admission/.

2. Write-round counts: escrow batch vs serial locking

The two numbers below are computed from the admission result above. They are round counts, not a timing benchmark; no performance measurement is claimed on this page. Serial per-operation locking pays one write round per operation. Escrow admission pays one round for the whole admitted set, because the interval arithmetic already proved every ordering of it safe. A deferred operation still carries its explanation and waits for the next batch.

3. A non-monotone invariant forces bounded witness search

Add one non-monotone policy: account D's balance must stay even. It is a legal, total predicate, but it is not an interval bound and cannot be classified as a signed delta, so interval arithmetic cannot admit through it. The declaration (KeyProperty("d-stays-even", ["D"], is_even)) moves every operation touching D off the escrow fast path into witness search over its conflict component, the group of operations linked by shared evaluated keys. Distinct keys still commute, so the search space is one component at a time, never the whole batch. But when a component grows past the search bound (8 operations), the solver reports inconclusive: search bound exhausted rather than admitting anything it did not check. The trade: with monotone (signed-delta, interval-bounded) structure, admission is interval arithmetic at any batch size; without it, admission is a per-component search that can hit its bound.

yichus admit ledger.bosatsu ledger_parity.spec.bosatsu ledger_handlers.bosatsu \
  --batch batch-sample.json --result admission.json

loading…

4. Run the solver in your browser

The same solver, compiled to JavaScript (the deploy build links the browser bundle from the same sources as the CLI), runs entirely in your browser: spec evaluation, escrow arithmetic, witness search, and replay through the compiled handlers. Things to try:

• Contention: raise the hot-account slider. More transfers hit account D, its escrow band shrinks faster, and deferrals accumulate with "headroom consumed by" traces.
• The non-monotone policy: switch on the parity checkbox and D's operations leave the fast path (search). To see the bound itself, set batch size 24, hot-account share 100%, policy on. D's conflict component then exceeds 8 operations and the verdicts read inconclusive: search bound exhausted.
• Break the handler: edit the handler below and re-run. Make it credit add(amount, amount) instead of amount, or drop the debit. Replay verification executes the witness through your edited handler and reports model drift, located at the first diverging operation and key. One thing that does not break it: deleting the guard alone changes nothing, because admission already proved every admitted operation safe. That is why no lock is needed.

Run admission in your browser

How it works

The EscrowSpec declares: the state cell (accounts), its real initial value, a view projecting each account's balance, Delta rows classifying transfer as a signed delta per key (Dec on the source, Inc on the target, key and amount as pure functions of the input), interval Bounds (the domain's own limit functions, the same compiled code the handler's guard calls), and optional non-monotone KeyProperty declarations. The admission solver and the interleaving checker share the order-enumeration engine and evaluate every declared function with the compiler's own evaluator, so the spec never has to be translated into a separate modelling language.

Soundness rules, the same discipline as the interleaving checker's: an operation that writes the cell with no Delta classification poisons every verdict on the cell (inconclusive: unclassified write); a declared operation with no implementing write stays inconclusive; beyond the search bound, inconclusive: search bound exhausted. And because the deltas and bounds are declarations about the handler rather than facts extracted from it, every batch is replay-verified: the witness ordering executes through the actual compiled handlers, and any divergence makes the batch inconclusive: model drift with the divergence located, and the CLI exits nonzero. The comparison is per step: after each operation of the witness, the cell, projected through the spec's own view, is compared per key against what the declared deltas predict. Replay is what ties the interval arithmetic to the real program. Without it, a handler that does something other than its declared deltas would make every verdict meaningless.

Read more: the design note (the algorithm, the soundness rules, and the adaptation notes behind this demo) · sources on GitHub · raw artifacts (each admission JSON is exactly what --result writes): escrow, with the parity policy, the batch.