Money Conservation

Check that every unit a payer authorizes ends in exactly one place, in the kernel's hold ledger and in a funded escrow.

On this page

Money leaks out of an accounting system in two ways. A reservation that is never closed keeps capacity from everyone after it, and a reservation closed into the wrong bucket lets spend escape its ceiling or releases money an unknown outcome still owes. Both are conservation failures. Chio states conservation as two identities and checks each one independently: the kernel's budget law, which every hold obeys from reservation to its one terminal state, and the funding identity $P + R + L + F = D$ , which every escrowed deposit obeys from funding to payment or refund.

Both identities are stated over amounts that appear in signed records. The kernel writes a hold's reservation and its terminal disposition into the receipt, and the escrow emits each funding, payment, and refund as an event, so an auditor rebuilds both ledgers from exported evidence and checks the sums without trusting either system's arithmetic.

Budget conservationChoose a step.

\begin{aligned} R &= \htmlClass{role-seal}{C} + \mathit{Rel} + \htmlClass{role-grant}{\mathit{Ret}} + \htmlClass{cor-parent}{O} \\ 2.40 &= \htmlClass{role-seal}{0.21} + 1.39 + \htmlClass{role-grant}{0.80} + \htmlClass{cor-parent}{0.00} \end{aligned}

A refusal before dispatch reverses the hold

A third USD 0.80 hold is reserved and a guard refuses the call before dispatch. The hold is reversed in full, so the released amount grows by USD 0.80 and nothing is committed. The ledger in TLA+ and Apalache.

The holds on one grant, stepped through reserve, reconcile, a lost reply, and a reversal, with the partition drawn against everything reserved so far. Amounts are illustrative; per-hold identity, invocation slots, and child shares are left out.

Every hold ends in exactly one terminal state

For each admission $a$ , the reserved amount $R(a)$ is partitioned at every reachable state. $C$ is committed spend, realized at reconciliation. $\mathit{Rel}$ is released: reversed before dispatch, or returned after a known outcome. $\mathit{Ret}$ is retained because the outcome after dispatch is unknown, and $O$ is exposure still awaiting a disposition. A delegated child's share $s_c$ is admitted only while its siblings' shares stay within the parent's:

\begin{aligned} R(a) &= C(a) + \mathit{Rel}(a) + \mathit{Ret}(a) + O(a), \qquad O(a) \ge 0 \\[4pt] \textstyle\sum_{c \,\in\, \mathrm{children}(p)} s_c &\le s_p \end{aligned}

Two rules sit beside the sum. A hold is never both reversed and settled, and a finalized hold accepts no further reservation or disposition. Reconciling an exposure of USD 0.80 to a realized USD 0.21 commits the 0.21 and releases the 0.59 under one terminal disposition, reconciled. The kernel's transitions are the law's alphabet:

Law term	Store journal event	When the kernel records it
reserve	`AuthorizeExposure`	At admission, before dispatch
commit	`ReconcileSpend`	A known reply with its reported cost
release	`ReverseExposure`, `ReleaseExposure`	A refusal before dispatch, or no spend
retain	none; the exposure stays outstanding	A reply lost after dispatch

The empty cell is deliberate. Reversing a hold whose outcome is unknown would reopen spending capacity while the tool may have acted, so the store leaves the exposure outstanding and the signed receipt carries post_dispatch_outcome_unknown with the hold id. The store's outstanding amount and the receipt's retained projection are two views of one amount, never added together.

Four independent checks hold the same law

The law is written once, beside the store's journal vocabulary, and four methods that fail in different ways check it:

Interleavings. Apalache checks ReservationConservation at every reachable state of a counted ledger, with ChildSplitsBounded on active child shares.
Amounts. Lean proves ledger_conservation and ledger_terminal_unique over the pure transition function ledger_apply; a Kani harness checks dense sequences and u64 boundary states, and a Creusot contract proves the same algebra.
The running kernel. Debug builds replay every monetary journal event, check each recorded after-state and the final usage row, and stop on a hold marked terminal with no matching disposition.
The store. A stateful property test drives the real store through 10,000 mixed sequences of authorize, reverse, release, and reconcile, checking the journal, the usage row, and the terminal history after every operation.

The theorems cover the transition model. That the production store follows the model is checked at run time by the replay and the property test, and the law is stated for one node's atomic store; a replicated cluster budget carries its own exposure bound.

Read more in the theorem inventory, under theorem.budget.reservation_conservation.

Escrowed money obeys P + R + L + F = D

A funding source is one deposit in one settlement domain and asset. $D$ is what was deposited, $P$ what has been paid to beneficiaries, $R$ what has been refunded to the funder, $L$ the most the remaining claims could still take, and $F$ what is free to allocate:

P + R + L + F = D, \qquad P,\, R,\, L,\, F \ge 0

Funding conservationChoose a step.

\begin{aligned} D &= \htmlClass{role-seal}{P} + \htmlClass{cor-relation}{R} + \htmlClass{cor-parent}{L} + \htmlClass{role-call}{F} \\ 300 &= \htmlClass{role-seal}{200} + \htmlClass{cor-relation}{60} + \htmlClass{cor-parent}{0} + \htmlClass{role-call}{40} \end{aligned}

A timed-out allocation refunds its lock

The child task misses its deadline, so its 60 locked units return to the payer. The identity holds: 200 paid, 60 refunded, 0 locked, and 40 free make the 300 deposited. Work Claim Escrow.

One deposit split into a provider allocation and a child allocation, stepped through locking, acceptance, payment, and a timed-out refund. Units are illustrative; fees, deadlines, and the chain transactions behind each move are left out.

Locking an allocation moves units from $F$ to $L$ , and payment or refund moves that allocation's lock once, to $P$ or $R$ . $L$ counts the full ceiling of every claim still eligible, verifier and dispute fees included, so recorded backing never exceeds received funds. A new deposit opens a new entry, and money refunded and deposited again counts once in each.

Acceptance confines a claim to payable or paid, and a transition on another allocation cannot touch it, so a parent's refund never revokes a child's earned payment. A child is funded from its own deposit; expected parent revenue never backs it. Payments along a supply chain are separate transfers from separate sources, so an auditor never sums them against the root buyer's budget.

Read more in Work Claim Escrow and Work Agreements and Funding.

A reader checks both identities from exported evidence

Each financial receipt carries its hold's lineage. The reconciled model call from the figure reads:

rcpt-01a8…5d17 · metadatajson

"budget_authority": {
  "guarantee_level": "single_node_atomic",
  "authority_profile": "authoritative_hold_event",
  "metering_profile": "max_cost_preauthorize_then_reconcile_actual",
  "hold_id": "budget-hold:req-01a8…4b10:cap-01a8…31f2:0",
  "authorize": { "exposure_units": 80, "committed_cost_units_after": 80 },
  "terminal": {
    "disposition": "reconciled",
    "exposure_units": 80,
    "realized_spend_units": 21,
    "committed_cost_units_after": 21
  }
}

Group receipts by hold_id. The authorize event gives $R$ , a reconciled terminal splits it into realized_spend_units committed and the rest released, a reversed or released terminal releases all of it, and a hold with no terminal is retained when its receipt marks the outcome unknown. The verifier runs that fold for every hold, and the same arithmetic over the escrow's funding, payment, and refund events in a work export:

audit.tsaudit.pysrc/main.rs · in mainTerminal

const evidence = await project.history.export("audit/");
console.log(await evidence.verify({ ledger: true }));

Output

receipts   9 signed decisions from your kernel
holds      3 on cap-01a8…31f2, each with one terminal disposition or a retained outcome
budget     reserved 2.40 = committed 0.21 + released 1.39 + retained 0.80 + outstanding 0.00
retained   rcpt-01a8…c311: outcome unknown, hold kept until resolved
funding    1 deposit: paid 200 + refunded 60 + locked 0 + free 40 = deposited 300
verified   offline, against your kernel key 4f1c…a2e9

evidence = project.history.export("audit/")
print(evidence.verify(ledger=True))

Output

receipts   9 signed decisions from your kernel
holds      3 on cap-01a8…31f2, each with one terminal disposition or a retained outcome
budget     reserved 2.40 = committed 0.21 + released 1.39 + retained 0.80 + outstanding 0.00
retained   rcpt-01a8…c311: outcome unknown, hold kept until resolved
funding    1 deposit: paid 200 + refunded 60 + locked 0 + free 40 = deposited 300
verified   offline, against your kernel key 4f1c…a2e9

let evidence = project.history().export("audit/")?;
println!("{}", evidence.verify_ledger()?);

Output

receipts   9 signed decisions from your kernel
holds      3 on cap-01a8…31f2, each with one terminal disposition or a retained outcome
budget     reserved 2.40 = committed 0.21 + released 1.39 + retained 0.80 + outstanding 0.00
retained   rcpt-01a8…c311: outcome unknown, hold kept until resolved
funding    1 deposit: paid 200 + refunded 60 + locked 0 + free 40 = deposited 300
verified   offline, against your kernel key 4f1c…a2e9

chio evidence export --output audit
chio evidence verify --input audit --ledger

Output

receipts   9 signed decisions from your kernel
holds      3 on cap-01a8…31f2, each with one terminal disposition or a retained outcome
budget     reserved 2.40 = committed 0.21 + released 1.39 + retained 0.80 + outstanding 0.00
retained   rcpt-01a8…c311: outcome unknown, hold kept until resolved
funding    1 deposit: paid 200 + refunded 60 + locked 0 + free 40 = deposited 300
verified   offline, against your kernel key 4f1c…a2e9

You should see both identities balance, with the retained hold named by its receipt. A package whose holds do not partition, or whose funding sums disagree, fails verification and names the hold or allocation that broke it.

Next: read the proofs behind the law

TLA+ and ApalacheSee the counted ledger and the invariants checked at every state.Work Claim EscrowFollow a funded claim from deposit to payment or refund.Guarantees and BoundariesPlace conservation among every economic claim by boundary class.

PreviousFiscal Charters NextComptroller Console