Component

A state machine in one output

The chain stores only a commitment to the state, and every spend must prove the old state against that commitment, apply one rule, and commit to the new state. The state itself never goes on-chain, so one output can carry the balances of many owners, or any other state that can be hashed into a root and changed by a rule a script can check.

The figure runs one spend through the covenant. The rule in this example is an exit: B leaves with its 3. The list under the caption tracks the three checks the covenant makes.

The pattern

A covenant is a script that restricts what the spending transaction may contain, not only who may sign it. Bitcoin script keeps no variables between transactions, so the only place a covenant can keep state is in the output it guards. LayerTree keeps the state in the output's key. The key is derived from the root of the tree, then tweaked by the set of scripts the output may be spent with, in the usual taproot way. The starting point of the derivation is a point whose private key nobody knows, so the output can never be spent by a signature alone; every spend must run one of the scripts.

Each script then makes the same three checks:

1. The input commits to the old root. The witness supplies the old state and a proof. The script folds the proof into a root, derives the output key from it, and compares that key with the key of the output being spent.
2. The rule holds. The script checks whatever the transition requires: a signature from the leaf's owner, a signature from the operator, a block height, a signed voucher.
3. The output commits to the new root. The script folds the new state up the same proof, derives the output key for the new root, and requires the transaction to create an output with that key and the new total.

Those three checks are the whole covenant. Every page on this site is an instance of it with a different rule and a different node replaced.

Why every node carries a sum

A plain Merkle tree commits to which leaves exist. A Merkle-sum tree also commits to how much they add up to: every node holds a hash and an amount, and a node's amount is the sum of its children's. The hash covers both children's amounts, so a proof of one leaf also fixes the sum of every sibling on its path. The script recomputes the sums on the way up, and the root's sum must equal the amount of the output being spent.

That turns "the operator cannot steal" into a property of the arithmetic. The script recomputes the root twice, before and after the change, and the difference between the two totals is exactly the value that may leave the output. Section 10.2 of the specification states the consequence: for any set of leaves whose proofs verify against an output, their amounts add up to at most the output's amount. Every provable leaf can be paid.

Why this scales ownership

On Bitcoin, each owner normally needs an output of their own, and outputs are what every node must store. Here one output holds the balances of up to 2^D owners, where D is the tree's depth, fixed when the tree is created. Each owner holds a proof of their own leaf. A spend touches one leaf and costs one proof, so the size of every transition depends on the depth, not on how many owners the tree has: at depth 16 the tree has 65,536 slots and an exit is about 1,020 vB whether one slot is full or all of them are.

Beyond balances

Nothing in the three checks is specific to money. Any state that can be hashed into a root, and any change a script can check given a proof, fits the same shape. A few examples follow; LayerTree builds none of them, and they are here to show the reach of the pattern.

• A counter that may only increase. Each leaf already carries one: its seq field rises by one with every voucher redeemed against it, which is how a used voucher can never verify again.
• A registry that maps keys to values. LayerTree's sparse profile places each leaf at a position derived from its owner's key, so a proof that the slot at that position is empty proves the key is not registered.
• An auction. The state is the current best bid; the rule accepts a replacement only if it is higher, and pays the previous bidder back in the same transaction.

The limits

• Cost grows with depth. Script has no loops, so the fold is written out once per level. In the FULL tier each level costs 88 bytes of script and 41 bytes of witness, about 32 vB. A deeper tree holds more owners and costs more to leave.
• The script sees only what it is shown. It must be given every node it checks. A rule about many leaves needs all of them in the witness: the cohort sweep publishes every slot of the subtree it removes. And a member who loses their proof cannot exit until they rebuild it, which they can do from the witnesses of past transitions on the chain (spec 9.7).
• Transitions are sequential. Every transition spends the same output, so each must wait for the one before it. The overview covers what that means for throughput.
• The opcodes are proposals. Deriving a key from a root and reading the spending transaction need opcodes Bitcoin does not have today. The tiers page lists the four sets the scripts have been built against.

What is proved

The rules are mechanised in Lean 4 in formal/, with no external libraries and no unproved steps. The headline theorems, by name:

• fold_sound: if a node and a path fold to a tree's root, the tree holds that node at that position, assuming the hash has no collisions. This is check 1.
• witness_root_binds and output_binds: the output key determines both the root and the script set, so checks 1 and 3 pin the state on both sides of the transaction.
• Steps.sum: every sequence of steps conserves the total, unconditionally.
• ExitK.no_inflation: no exit creates value.
• payable: whoever holds a leaf and its path can always build an accepted exit paying the leaf's amount, without anyone's cooperation.

payable assumes the committed root is the root of an actual tree, an invariant that creation and grafting must establish off-chain; the join page explains why. Lean covers the rules, not the bytecode. The scripts are checked by execution: a simulator runs every compiled script against reference trees, with failing cases for every rule, and a Go implementation regenerates the same scripts byte for byte.