Program Logics for Ledgers

We give the denotational semantics of a ledger by mapping $L$ to a function of type $S\to \mathrm{𝑀𝑎𝑦𝑏𝑒}S$, executing all the transactions in the ledger starting from a given state with given account balances. The optional return type is used to model the case where a transaction fails due to insufficient funds: the result is $\mathrm{𝗃𝗎𝗌𝗍}$ a new state after successful execution or $\mathrm{𝗇𝗈𝗍𝗁𝗂𝗇𝗀}$ to signal an error.

This semantics for ledgers is straightforward to define by iterating its transactions:

The Kleisli arrow ($>=>$) composes partial functions by collapsing to $\mathrm{𝗇𝗈𝗍𝗁𝗂𝗇𝗀}$ when the first function fails. A transaction’s semantics ($d$) checks the validity of each transfer and fails if not enough funds are available, otherwise updates the state accordingly. We will write “$t$ is valid in $\sigma$” as a uniform way to express the validity of a transaction $t$ with respect to a given state $\sigma$, which will become more intricate when we consider blockchain ledgers in the next section.

We formulate and prove a simple compositionality result, stating that the appending of ledgers ($++$) is mapped to the composition of their denotations.

This result, however, gives us only limited modularity – we still need to break a ledger into sequential pieces that we consider individually. To handle large ledgers, however, we would like to reason about arbitrary ledger fragments; in particular, we may be interested in an arbitrary subset of the transactions that are related to a specific smart contract in the blockchain setting.

We also define an axiomatic semantics for $L$. To do so, we define inference rules for Hoare triples of the form $\{P\}l\{Q\}$, where $P$ and $Q$ are predicates on our state space $S$.

The base rule dictates that executing an empty ledger leaves the state unchanged, while the inductive step rule provides the weakest pre-condition by viewing the transaction as a predicate transformer [14].

Also note the necessary operation $\mathrm{\uparrow }$, lifting a predicate over $S$ to a predicate over $\mathrm{𝑀𝑎𝑦𝑏𝑒}S$. There are two canonical ways to achieve this lifting: the weak lifting that collapses to $\mathrm{𝗍𝗋𝗎𝖾}$ when a transaction fails, and the strong lifting that collapses to $\mathrm{𝖿𝖺𝗅𝗌𝖾}$ upon failure. Since we wish to observe failing transactions, we opt for the strong version, which we prove sound with respect to the denotational semantics:

We add the typical rule for weakening/strengthening pre-/post-conditions:

The soundness theorem also allows us to derive a sequencing rule as a corollary of the equivalent statement about ledgers in the denotational semantics:

Both of our denotational and axiomatic semantics rely on having the complete ledger at our disposal – we cannot yet use these semantics to reason about arbitrary subsets of transactions, independent of the others. To this end, we define a separating conjunction combining two predicates, $P$ and $Q$, on our state space $S$. Before we do so, however, we need to consider how to combine states $S$. In most program language semantics, this is done by splitting the memory state (i.e. the heap mapping variable addresses to their value) into two disjoint parts. The separating conjunction, $P\mathrm{\ast }Q$, is then defined as follows:

Here, $\sigma$ is the resulting heap of combining two smaller heaps $\sigma \mathrm{₁}$ and $\sigma \mathrm{₂}$ using the disjoint union operation ($\mathrm{\uplus }$).

When considering financial ledgers, however, we can do better. As each transaction preserves the overall funds, we do not require the maps to be disjoint; instead, we divide the funds from both maps into two distinct parts! To do so, we begin by defining the following operation of combining ledger states by pointwise addition of their funds:

Using this operation, we now define the separating conjunction of predicates as follows:

The frame rule, used to introduce the separating conjunction, now becomes:

Crucially, this version of the frame rule does not have the usual side conditions required to reason about imperative languages, namely, that the set of variables modified by $l$ must be disjoint from the free variables mentioned by $R$. Intuitively, this rule is valid since transactions preserve the total amount of funds in circulation: we split off some of these funds (leaving funds that satisfy $R$ left over), move these funds in accordance with $l$, and then recombine the result with the funds satisfying $R$.

To complete this semantics, however, we need to add a few basic rules that are currently missing. The rule for handling a single transaction is very simple indeed:

The precondition, $p\mathrm{₁}\mathrm{\mapsto }n$, states that participant $p\mathrm{₁}$ has a total of $n$ funds (and all other participants have none). After executing this transaction, $p\mathrm{₂}$ has received these $n$ funds (and all other participants, including $p\mathrm{₁}$, have none). By itself, this rule does not seem useful – but in combination with the frame rule above, it can be used to execute a single transaction in any larger state – leaving all other funds untouched. The final two rules describe the behaviour of an entire ledger:

The first rule states that the empty ledger leaves the empty state unchanged; the second describes how transactions from two non-empty ledgers are run sequentially.

Furthermore, we can define a (non-deterministic) interleaving operation on ledgers, $l\mathrm{₁}\mathrm{\parallel }l\mathrm{₂}$. One of the more promising observations we can make is that the familiar rule for concurrent separation logic also holds for the interleaving of two ledgers:

This provides a modular reasoning principle for ledgers: it allows us to focus on an arbitrary subset of the ledger’s transactions and reason about this subset in isolation. Whenever we interleave its transactions with the remainder of the ledger, any properties we have established still hold of the composite ledger. We refer the reader to Appendix A for example derivations.

In the previous section, a transaction could fail due to insufficient funds. Similarly in the UTxO setting, transactions are only valid under certain conditions. Given transaction $t$ and state $\sigma$, $t$ is valid in $\sigma$ iff all the following criteria are met:

• $\mathrm{■}$

  referenced outputs are unspent:

  $$\forall (i\mathrm{\in }t.\mathrm{𝗂𝗇𝗉𝗎𝗍𝗌}).i.\mathrm{𝗋𝖾𝖿}\mathrm{\in }\sigma$$

• $\mathrm{■}$

  there is no double spending:

  $$\forall (i,j\mathrm{\in }t.\mathrm{𝗂𝗇𝗉𝗎𝗍𝗌}).i\mathrm{\ne }j\to i.\mathrm{𝗋𝖾𝖿}\mathrm{\ne }j.\mathrm{𝗋𝖾𝖿}$$

• $\mathrm{■}$

  value is preserved:

  $$\sum _{i\mathrm{\in }t.\mathrm{𝗂𝗇𝗉𝗎𝗍𝗌}}\sigma (i.\mathrm{𝗋𝖾𝖿}).\mathrm{𝗏𝖺𝗅𝗎𝖾}=\sum _{o\mathrm{\in }t.\mathrm{𝗈𝗎𝗍𝗉𝗎𝗍𝗌}}o.\mathrm{𝗏𝖺𝗅𝗎𝖾}$$

• $\mathrm{■}$

  all inputs validate:

  $$\forall (i\mathrm{\in }t.\mathrm{𝗂𝗇𝗉𝗎𝗍𝗌}).\sigma (i.\mathrm{𝗋𝖾𝖿}).\mathrm{𝗏𝖺𝗅𝗂𝖽𝖺𝗍𝗈𝗋}(i.\mathrm{𝗋𝖾𝖽𝖾𝖾𝗆𝖾𝗋})=\mathrm{𝗍𝗋𝗎𝖾}$$

All other parts remain identical to the previous semantics, Hoare logic rules included, except the denotation of a single transaction: instead of updating account balances, it instead removes all previous UTxOs consumed by its inputs and then inserts new UTxOs for each output:

So far it has been straightforward to extend our results from the previous sections to UTxO-based blockchains: once we have the denotation of a single transaction, the semantics of a ledger is simply the composition of its constituent transactions. When we attempt to define a separation logic for the UTxO model, however, we encounter a new problem.

The UTxO model refers to existing outputs by name (i.e. the hash of the enclosing transaction), while the previous model for account-based ledger transferred funds directly by value. This allowed us to split and combine the finite maps, $\sigma \mathrm{₁}\mathrm{\oplus }\sigma \mathrm{₂}$, that associate each participant with their available funds. In the UTxO situation, however, funds are locked by a validator script and must be consumed as a whole: we cannot readily split and combine funds in the same way as we saw previously. Therefore, predicates such as $t_3^{\mathrm{♯}}\mathrm{\mapsto }v\mathrm{\ast }{t}_3^{\mathrm{♯}}\mathrm{\mapsto }{v}^{\prime }$ no longer make sense, since the third output of transaction $t$ can only be spent once. Thus our separating conjunction has to be restricted only to disjoint fragments of the state:

As a result, we have to extend the frame rule with a disjointness side-condition, familiar from the semantics of imperative programs that mutate memory:

The condition $l\mathrm{♯}R$ ensures all references in $l$ are disjoint from the support of $R$, i.e. the validity of the predicate does not depend on parts of the state that the ledger mutates:

Similarly, the parallel rule also needs to be restricted to only disjoint interleavings:

This is the point in our development where we have lost the stronger compositionality properties that the previous semantics enjoyed. To use the frame rule to reason about UTxO-based blockchains, this side condition requires checking disjointness (see Appendix B for examples) – where previously we were free to split off arbitrary funds from the account state.

To define a denotational semantics for AUTxO, we need to revise the validity conditions that check a transaction $t$ given a current ledger state $\sigma$, and redefine the state transition function, $d$. Validity of abstract transactions closely follows the criteria we set previously in Section 3.1, except that inputs now only contain a monetary value locked by a validator (i.e. they are no longer represented as unspent outputs attached to previous transactions), so we need only check that the current bag of unspent values contains at least the consumed amount, and there is no longer a requirement to check for duplicate references, since it is now perfectly sensible to have two inputs that carry the same value. Formally:

• $\mathrm{■}$

  there are sufficient funds in $\sigma$:

  $$t.\mathrm{𝗂𝗇𝗉𝗎𝗍𝗌}\subseteq \sigma$$

• $\mathrm{■}$

  all inputs validate:

  $$\forall (i\mathrm{\in }t.\mathrm{𝗂𝗇𝗉𝗎𝗍𝗌}).i.\mathrm{𝗋𝖾𝖿}.\mathrm{𝗏𝖺𝗅𝗂𝖽𝖺𝗍𝗈𝗋}(i.\mathrm{𝗋𝖾𝖽𝖾𝖾𝗆𝖾𝗋})=\mathrm{𝗍𝗋𝗎𝖾}$$

• $\mathrm{■}$

  value is preserved:

  $$\sum _{i\mathrm{\in }t.\mathrm{𝗂𝗇𝗉𝗎𝗍𝗌}}i.\mathrm{𝗋𝖾𝖿}.\mathrm{𝗏𝖺𝗅𝗎𝖾}=\sum _{o\mathrm{\in }t.\mathrm{𝗈𝗎𝗍𝗉𝗎𝗍𝗌}}o.\mathrm{𝗏𝖺𝗅𝗎𝖾}$$

Notice that value preservation has become significantly simpler to formulate in this more abstract model, since we no longer need to query the value of a referenced output from the current state $\sigma$: the reference is the value!

The denotational semantics of a single transaction removes previously unspent transaction outputs, replacing them with the outputs of the new transaction:

We derive the rest of the scaffolding to sequentially derive the denotation of a whole ledger exactly as before. The axiomatic semantics do not change in any way, except that they work on predicates over bags of outputs instead of maps from references to outputs.

We can finally regain modularity for our separation logic, thanks to transaction inputs in AUTxO referring to existing outputs by value. In particular, we can define separating conjunction:

Notice how we utilise the monoidal composition of two bags that may overlap, regardless of whether they are disjoint or not.

The resulting inference rules are identical to the ones presented previously for account-based ledgers in Section 2, where we now use the monoidal actions on bags of values instead of the pointwise sum on finite maps.

In particular, the par rule enables us to reason about separate parts of the ledger independently. We can now prove properties at the AUTxO level in a modular fashion (see Appendix C for an example), and have confidence that they also hold in an equivalent UTxO ledger with hash references and ordered outputs.

Note that the elements of each bag are pairs of a validator function and available funds. While previously in the account-based ledger model, we used the monoidal action on the monetary funds – adding their monetary value when splitting the state into smaller parts. In the UTxO model, however, we cannot split locked funds: if the same validator locks two values $v$ and $v^{\prime }$, we cannot deduce that it locks $v+v^{\prime }$ – a property that the simple account-based ledgers did support. We will discuss this limitation in more detail later (Section 7), but leave its resolution for future work.

The relation between AUTxO and UTxO is not yet satisfying, as we need some kind of full abstraction [24] result that lets us conduct compositional proofs at the abstract (𝔸) level which then translate to properties about an actual concrete (ℂ) ledger. One can informally see that all properties that do not observe the implementation details of the concrete model should be derivable from their abstract counterparts. To formalise this intuition, we first define the abstraction of a concrete state as viewing its range as a bag:

We can then build up abstraction functions for valid transactions ($ab{s}^T$) and ledgers ($ab{s}^L$), where we resolve the actual outputs that references consume. Most importantly, UTxO validity is transformed into AUTxO validity, making it possible to then relate their respective denotational semantics.

Finally, we can prove soundness of our abstract model with respect to the UTxO model, at least for properties that do not observe implementation details.

where both Hoare triples have been implicitly instantiated to the state $\sigma$ that is universally quantified at the outermost level.

This means it is sound to conduct modular proofs on the abstract level; the equivalent statement on concrete ledgers will also hold. Note that our abstract model is not complete, since we can only cover abstract state predicates of the form $P\mathrm{\circ }ab{s}^S$, thus we cannot hope to prove a full abstraction result. We feel that this will not be problematic in practice: these predicates mention implementation details that arguably should be kept abstract.