Ledger Model
Bitcoin validation is modeled as deterministic state transition over a proof-of-work header graph, available block data, and the active UTXO set. This section fixes the shared relations used by later sections.
State
A full-validation node’s protocol state is:
$$ S = (C,H,B,U,Q,\Pi) $$
| Symbol | Type | Meaning |
|---|---|---|
| $C$ | ActiveChain | Ordered sequence of connected blocks from genesis to the active tip. |
| $H$ | HeaderIndex | Known block-header graph keyed by block hash, including height, predecessor, target, timestamp, and accumulated work. |
| $B$ | BlockDataSet | Full block data known to the node, keyed by block hash. |
| $U$ | UTXOSet | Map from unspent outpoints to coin records at the active-chain tip. |
| $Q$ | Mempool | Locally accepted unconfirmed transactions. This is relay state, not consensus state. |
| $\Pi$ | PeerSet | Connected-peer state and negotiated network capabilities. |
Consensus validation reads $C,H,B,U$ and mutates only $C,H,B,U$. Mempool and peer transitions read consensus state but do not define block validity.
Coins
The UTXO set maps outpoints to coins:
$$ U[(txid,n)] = (value, scriptPubKey, height, coinbase). $$
| Coin field | Type | Meaning |
|---|---|---|
value | Amount | Output amount in satoshis. Consensus-valid values are in the money range. |
scriptPubKey | Script | Locking script committed by the creating transaction output. |
height | uint32 | Active-chain height of the creating transaction. |
coinbase | bool | True iff the creating transaction is the block coinbase. |
Rule context
Let $N$ be the selected network parameter set. For candidate height $h$, candidate block time $t$, and active chain $C$, define:
$$ R = \operatorname{Rules}(N,C,h,t). $$
$R$ is the set of consensus rules active for the candidate object. It includes network constants, buried activation heights, versionbits state, timestamp rules, and script flags. Later sections use $R$ rather than restating whether P2SH, BIP34, strict DER, locktime, sequence locks, SegWit, Taproot, Tapscript, or network-specific timewarp mitigations are active.
Validity classes
| Class | Meaning |
|---|---|
| $DecodeValid_T(b)$ | $E_T^-1(b)$ succeeds and consumes a canonical encoding of type $T$. |
| $FormValid(x)$ | Object $x$ is internally well-formed independent of chain state. |
| $ContextValid_R(x,C)$ | Object $x$ satisfies height, time, and active-rule predicates under $R$. |
| $StateValid_R(x,U)$ | Object $x$ is valid against the current spendable coin set. |
| $RelayValid_P(x,Q,U)$ | Object $x$ is accepted by local relay policy. This is not a consensus predicate. |
Transition relations
For a non-coinbase transaction, the transaction transition is:
$$ \operatorname{ApplyTx}(R,U,tx) = \begin{cases} U’, & \text{if } tx \text{ is valid against } U \text{ under } R,\ \bot, & \text{otherwise.} \end{cases} $$
For a block $B_h$ at height $h$, block connection is:
$$ \operatorname{ConnectBlock}(R,(C,U),B_h) = \begin{cases} (C’,U’), & \text{if every block and transaction predicate succeeds,}\ \bot, & \text{otherwise.} \end{cases} $$
Header acceptance, block-data acceptance, chain selection, and reorganization are the consensus transitions defined in Section Consensus. Mempool admission is the local transition defined in Section Mempool.
Invariants
Every accepted active-chain transition preserves:
| Invariant | Statement |
|---|---|
| Determinism | For fixed $N,C,U,B_h$, successful connection produces a unique $C’,U’$. |
| Outpoint uniqueness | At any active tip, each outpoint appears at most once in $U$. |
| No double spend | A connected transaction consumes each input outpoint at most once, and a connected block consumes each live outpoint at most once. |
| Conservation | A non-coinbase transaction cannot create value: $\sum outputs(tx) <= \sum spent(tx)$. |
| Issuance bound | For each connected block, $\sum outputs(coinbase) <= subsidy(h)+\sum fees(B_h)$. |
| Work selection | The active chain is selected from valid candidates by greatest accumulated work. |