Value conservation

A value transaction cannot create tokens. For every token it touches, the transaction proof shows that what comes in equals what goes out, and the chain supplies the public terms of that equation itself instead of trusting the sender's numbers.

The equationCopy Anchor Link

For each token, the circuit enforces one equation between what the transaction brings in and what it sends out. The chart below shows its two sides.

flowchart LR
in1["Input notes"] --> eq{{"Equal, per token"}}
in2["Deposits"] --> eq
eq --> out1["Output notes"]
eq --> out2["Fees on outputs"]
eq --> out3["Withdrawals"]
eq --> out4["Fees on withdrawals"]
eq --> out5["Relayer tip"]

The left side is the total of two things: the amounts of the input notes of that token, and the amounts deposited in that token. The right side is the total of five: the amounts of the output notes of that token, the protocol fee on each of those output notes, the amounts withdrawn in that token, the protocol fee on each of those withdrawals, and the relayer tip if it is paid in that token. Each term is counted only where its token matches the token being checked, so notes and lanes of other tokens drop out of the equation.

Dummy notes and idle lanes contribute zero, since a dummy's amount is 0 by definition and an idle lane's amount, token and counterparty must all be 0. The protocol fee is charged on what is received, output by output and withdrawal by withdrawal, and becomes the treasury's fee notes; the relayer tip is credited to the relayer's accrual account and collected later. See the fee model.

The circuit checks the equation once for every token that appears anywhere in the transaction: the token of each input note, output note, deposit lane and withdrawal lane, and the relayer tip's token. Checking the tip's token matters. A transaction that spent token A and paid its tip in token B would balance for token A alone; because token B is checked as well, a tip in a token the transaction brought in none of must be zero. The Lean model proves that this extra check is necessary. A transaction touches at most three distinct tokens, so the equations are few, but they are checked over the full list of candidates.

Who supplies each termCopy Anchor Link

The private terms, the note amounts and the fees, are known only to the prover and are fixed by the proof. The public terms come from the chain:

• Deposits enter the proof's public input as the amount the pool token account actually received, measured by the program from its balance before and after the transfer.
• Withdrawals enter as the amounts in the payload, and the program pays exactly those amounts out of the pool token accounts, after checking each account can cover them.
• The relayer tip enters as the payload's tip, which the program credits to the tip accrual for that relayer and token.
• Token identities of the lanes enter as the mint addresses of the accounts the program checked, split into two 128-bit halves.

For SOL the account in both cases is the pool's lamport account: the program measures its lamports on the way in, and pays out of what it holds above its reserve.

A prover who lies about any public term makes a proof for a different public input, and it fails to verify. See pool token accounts and tokens.

Why the range checks matterCopy Anchor Link

The equation is checked in the BN254 scalar field, where arithmetic wraps around at a 254-bit prime. On its own, a field equation says little about token amounts: a "fee" equal to minus a thousand, which is a huge field element, would let an output of a thousand balance an input of zero. The Lean model contains exactly this counterexample, and shows the equation holds for it.

The range checks rule it out. Every note amount, deposit, withdrawal and tip is checked to fit in 64 bits, and every protocol fee in 65 bits. With at most 11 terms on either side, neither side can reach the field's size, so the field equation is also an equation between ordinary whole numbers. An amount is a count of the token's base units, up to 2⁶⁴ − 1.

What the Lean proofs establishCopy Anchor Link

The TransactionCircuit Lean library models the circuit's conservation constraints and proves three theorems about any transaction that satisfies them, for every token the transaction checks:

1. No minting. The total of the output notes is at most the total of the input notes plus deposits.
2. No unfunded withdrawal. The total withdrawn is at most the total of the input notes plus deposits.
3. Fees are funded. The protocol fees plus the relayer tip are at most the total of the input notes plus deposits.

Each theorem assumes the amounts are within the bounds above; the library then shows those bounds are enough for the production shape of three inputs, three outputs, two deposit lanes and two withdrawal lanes. It also records which circuit check imposes each bound.

Under which assumptionsCopy Anchor Link

• The model is hand-written. The Lean definitions are a transcription of the Circom constraints, not generated from them. That they match is stated as an axiom whose content is simply "true", which records the assumption without proving it.
• The field's order is prime is taken as an axiom rather than proved. The three theorems use no cryptographic assumption: no property of Poseidon, BLS or Groth16 enters them.
• The lane token halves are not range-checked in the circuit. The library identifies the two 128-bit halves of each deposit and withdrawal token address as the one pair of values the circuit reassembles without bounding. They are sound because the program, not the prover, supplies them from real 32-byte addresses; that argument crosses from the circuit to the program and is stated in Lean as a premise, not proved about the program.
• The Groth16 proof must be sound. The theorems are about transactions that satisfy the constraints. A forged proof under a compromised proving key satisfies nothing.

Conservation is one transaction at a time. That no note is spent twice is a separate guarantee, kept by nullifiers and the staging buffer, and it is what turns per-transaction conservation into a pool that stays funded. The formal verification page covers the rest of the library.

RelatedCopy Anchor Link