UTxO¶

This section is part of the Ledger.Conway.Utxo module of the formal ledger specification, where we define types and functions needed for the UTxO transition system.

Accounting¶

{-# OPTIONS --safe #-}

open import Algebra              using (CommutativeMonoid)
open import Data.Nat.Properties  using (+-0-monoid)
import Data.Maybe as M
import Data.Sum.Relation.Unary.All as Sum

import Data.Integer as ℤ
import Data.Rational as ℚ


open import Ledger.Prelude
open import Ledger.Conway.Abstract
open import Ledger.Conway.Transaction

module Ledger.Conway.Utxo
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Conway.Script.Validation txs abs
open import Ledger.Conway.Fees txs using (scriptsCost)
open import Ledger.Conway.Certs govStructure

instance
  _ = +-0-monoid

Functions supporting UTxO rules¶

totExUnits : Tx → ExUnits
totExUnits tx = ∑[ (_ , eu) ← tx .wits .txrdmrs ] eu
  where open Tx; open TxWitnesses

-- utxoEntrySizeWithoutVal = 27 words (8 bytes)
utxoEntrySizeWithoutVal : MemoryEstimate
utxoEntrySizeWithoutVal = 8

utxoEntrySize : TxOutʰ → MemoryEstimate
utxoEntrySize o = utxoEntrySizeWithoutVal + size (getValueʰ o)


open PParams

define functions needed for the UTxO transition system.

Conway specifics

define types and functions needed for the UTxO transition system.

Figure 'UTxO-transition-system-types' defines the types needed for the UTxO transition system. The UTxO transition system is given in Figure 'UTXO-inference-rules'.

The function \(\fun{outs}\) creates the unspent outputs generated by a transaction. It maps the transaction id and output index to the output.
The \(\fun{balance}\) function calculates sum total of all the coin in a given UTxO.

The deposits have been reworked since the original Shelley design. We now track the amount of every deposit individually. This fixes an issue in the original design: An increase in deposit amounts would allow an attacker to make lots of deposits before that change and refund them after the change. The additional funds necessary would have been provided by the treasury. Since changes to protocol parameters were (and still are) known publicly and guaranteed before they are enacted, this comes at zero risk for an attacker. This means the deposit amounts could realistically never be increased. This issue is gone with the new design. See also .

Similar to ScriptPurpose, DepositPurpose carries the information what the deposit is being made for. The deposits are stored in the deposits field of UTxOState (the type Deposits is defined in Figure 'Deposit-types'). updateDeposits is responsible for updating this map, which is split into updateCertDeposits and updateProposalDeposits, responsible for certificates and proposals respectively. Both of these functions iterate over the relevant fields of the transaction body and insert or remove deposits depending on the information seen. Note that some deposits can only be refunded at the epoch boundary and are not removed by these functions.

There are two equivalent ways to introduce this tracking of the deposits. One option would be to populate the deposits field of UTxOState with the correct keys and values that can be extracted from the state of the previous era at the transition into the Conway era. Alternatively, we can effectively treat the old handling of deposits as an erratum in the Shelley specification, which we fix by implementing the new deposits logic in older eras and then replaying the chain. (The handling of deposits in the Shelley era is discussed in .)

UTxO transition system types¶

UTxO environment

record UTxOEnv : Type where
  field
    slot      : Slot
    pparams   : PParams
    treasury  : Coin

instance
  HasPParams-UTxOEnv : HasPParams UTxOEnv
  HasPParams-UTxOEnv .PParamsOf = UTxOEnv.pparams

  HasgovActionDeposit-UTxOEnv : HasgovActionDeposit UTxOEnv
  HasgovActionDeposit-UTxOEnv .govActionDepositOf = govActionDepositOf ∘ PParamsOf

UTxO states

record UTxOState : Type where

  constructor ⟦_,_,_,_⟧ᵘ

  field
    utxo       : UTxO
    fees       : Coin
    deposits   : Deposits
    donations  : Coin

record HasUTxOState {a} (A : Type a) : Type a where
  field UTxOStateOf : A → UTxOState
open HasUTxOState ⦃...⦄ public

instance
  HasDeposits-UTxOState : HasDeposits UTxOState
  HasDeposits-UTxOState .DepositsOf = UTxOState.deposits

  HasUTxO-UTxOState : HasUTxO UTxOState
  HasUTxO-UTxOState .UTxOOf = UTxOState.utxo

  unquoteDecl HasCast-UTxOEnv HasCast-UTxOState = derive-HasCast
    ( (quote UTxOEnv   , HasCast-UTxOEnv  ) ∷
    [ (quote UTxOState , HasCast-UTxOState) ])

UTxO transitions

data

  _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type

Functions used in UTxO rules¶

module _ (let open Tx; open TxBody; open TxWitnesses) where opaque

  outs : TxBody → UTxO
  outs tx = mapKeys (tx .txid ,_) (tx .txouts)

  balance : UTxO → Value
  balance utxo = ∑[ x ← mapValues txOutHash utxo ] getValueʰ x

  cbalance : UTxO → Coin
  cbalance utxo = coin (balance utxo)


  refScriptsSize : UTxO → Tx → ℕ
  refScriptsSize utxo tx = sum (map scriptSize (setToList (refScripts tx utxo)))

  minfee : PParams → UTxO → Tx → Coin
  minfee pp utxo tx  = pp .a * tx .txsize + pp .b
                     + txscriptfee (pp .prices) (totExUnits tx)
                     + scriptsCost pp (refScriptsSize utxo tx)

instance
  HasCoin-UTxO : HasCoin UTxO
  HasCoin-UTxO .getCoin = cbalance

certDeposit : DCert → PParams → Deposits
certDeposit (delegate c _ _ v) _   = ❴ CredentialDeposit c , v ❵
certDeposit (reg c _)          pp  = ❴ CredentialDeposit c , pp .keyDeposit ❵
certDeposit (regpool kh _)     pp  = ❴ PoolDeposit kh , pp .poolDeposit ❵
certDeposit (regdrep c v _)    _   = ❴ DRepDeposit c , v ❵
certDeposit _                  _   = ∅

certRefund : DCert → ℙ DepositPurpose
certRefund (dereg c _)      = ❴ CredentialDeposit c ❵
certRefund (deregdrep c _)  = ❴ DRepDeposit c ❵
certRefund _                = ∅

data ValidCertDeposits (pp : PParams) (deps : Deposits) : List DCert → Set

  where
  []         : ValidCertDeposits pp deps []
  delegate   : ∀ {c del kh v certs}
             → ValidCertDeposits pp (deps ∪⁺ ❴ CredentialDeposit c , v ❵) certs
             → ValidCertDeposits pp deps (delegate c del kh v ∷ certs)
  regpool    : ∀ {kh p certs}
             → ValidCertDeposits pp (deps ∪⁺ ❴ PoolDeposit kh , pp .poolDeposit ❵) certs
             → ValidCertDeposits pp deps (regpool kh p ∷ certs)
  regdrep    : ∀ {c v a certs}
             → ValidCertDeposits pp (deps ∪⁺ ❴ DRepDeposit c , v ❵) certs
             → ValidCertDeposits pp deps (regdrep c v a ∷ certs)
  reg        : ∀ {c v certs}
             → ValidCertDeposits pp (deps ∪⁺ ❴ CredentialDeposit c , pp .keyDeposit ❵) certs
             → ValidCertDeposits pp deps (reg c v ∷ certs)
  dereg      : ∀ {c md d certs}
             → (CredentialDeposit c , d) ∈ deps
             → md ≡ nothing ⊎ md ≡ just d
             → ValidCertDeposits pp (deps ∣ ❴ CredentialDeposit c ❵ ᶜ) certs
             → ValidCertDeposits pp deps (dereg c md ∷ certs)
  deregdrep  : ∀ {c d certs}
             → (DRepDeposit c , d) ∈ deps
             → ValidCertDeposits pp (deps ∣ ❴ DRepDeposit c ❵ ᶜ) certs
             → ValidCertDeposits pp deps (deregdrep c d ∷ certs)
  ccreghot   : ∀ {c v certs}
             → ValidCertDeposits pp deps certs
             → ValidCertDeposits pp deps (ccreghot c v ∷ certs)
  retirepool : ∀ {kh e certs}
             → ValidCertDeposits pp deps certs
             → ValidCertDeposits pp deps (retirepool kh e  ∷ certs)

private
  validCertDeposits? : ∀ {pp} deps certs → Dec (ValidCertDeposits pp deps certs)
  validCertDeposits? deps [] = yes []
  validCertDeposits? deps (delegate _ _ _ _ ∷ certs) =
    mapDec delegate (λ where (delegate p) → p) (validCertDeposits? _ _)
  validCertDeposits? deps (regpool _ _ ∷ certs) =
    mapDec regpool (λ where (regpool p) → p) (validCertDeposits? _ _)
  validCertDeposits? deps (regdrep _ _ _ ∷ certs) =
    mapDec regdrep (λ where (regdrep p) → p) (validCertDeposits? _ _)
  validCertDeposits? deps (retirepool _ _ ∷ certs) =
    mapDec retirepool (λ where (retirepool p) → p) (validCertDeposits? _ _)
  validCertDeposits? deps (ccreghot _ _ ∷ certs) =
    mapDec ccreghot (λ where (ccreghot p) → p) (validCertDeposits? _ _)
  validCertDeposits? deps (reg _ _ ∷ certs) =
    mapDec reg (λ where (reg p) → p) (validCertDeposits? _ _)
  validCertDeposits? deps (dereg c nothing ∷ certs) with ¿ CredentialDeposit c ∈ dom deps ¿ 
  ... | yes p = mapDec (dereg (proj₂ (Equivalence.from dom∈ p)) (inj₁ refl)) (λ { (dereg _ _ p) → p }) (validCertDeposits? _ _)
  ... | no ¬p = no λ { (dereg x _ _) → ¬p (Equivalence.to dom∈ (_ , x)) }
  validCertDeposits? deps (dereg c (just d) ∷ certs) with ¿ (CredentialDeposit c , d) ∈ deps ¿ 
  ... | yes p = mapDec (dereg p (inj₂ refl)) (λ { (dereg _ _ p) → p }) (validCertDeposits? _ _)
  ... | no ¬p = no λ { (dereg x (inj₂ refl) _) → ¬p x }
  validCertDeposits? deps (deregdrep c d ∷ certs) with ¿ (DRepDeposit c , d) ∈ deps ¿
  ... | yes p = mapDec (deregdrep p)  (λ where (deregdrep _ v) → v) (validCertDeposits? _ _)
  ... | no ¬p = no (λ where (deregdrep p _) → ¬p p)

instance
  Dec-ValidCertDeposits : ∀ {pp deps certs} → ValidCertDeposits pp deps certs ⁇
  Dec-ValidCertDeposits = ⁇ (validCertDeposits? _ _)

Functions used in UTxO rules, continued¶

updateCertDeposits  : PParams → List DCert → Deposits → Deposits
updateCertDeposits pp [] deposits = deposits

updateCertDeposits pp (reg c v ∷ certs) deposits
  = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (reg c v) pp)

updateCertDeposits pp (delegate c vd khs v ∷ certs) deposits
  = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (delegate c vd khs v) pp)
updateCertDeposits pp (regpool kh p ∷ certs) deposits
  = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (regpool kh p) pp)
updateCertDeposits pp (regdrep c v a ∷ certs) deposits
  = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (regdrep c v a) pp)
updateCertDeposits pp (dereg c v ∷ certs) deposits
  = updateCertDeposits pp certs (deposits ∣ certRefund (dereg c v)ᶜ)
updateCertDeposits pp (deregdrep c v ∷ certs) deposits
  = updateCertDeposits pp certs (deposits ∣ certRefund (deregdrep c v)ᶜ)
updateCertDeposits pp (_ ∷ certs) deposits
  = updateCertDeposits pp certs deposits

updateProposalDeposits : List GovProposal → TxId → Coin → Deposits → Deposits
updateProposalDeposits []        _     _      deposits  = deposits
updateProposalDeposits (_ ∷ ps)  txid  gaDep  deposits  =
  updateProposalDeposits ps txid gaDep deposits
  ∪⁺ ❴ GovActionDeposit (txid , length ps) , gaDep ❵

updateDeposits : PParams → TxBody → Deposits → Deposits
updateDeposits pp txb = updateCertDeposits pp txcerts
                        ∘ updateProposalDeposits txprop txid (pp .govActionDeposit)

  where open TxBody txb

proposalDepositsΔ : List GovProposal → PParams → TxBody → Deposits
proposalDepositsΔ props pp txb = updateProposalDeposits props txid (pp .govActionDeposit) ∅
  where open TxBody txb


depositsChange : PParams → TxBody → Deposits → ℤ
depositsChange pp txb deposits =
  getCoin (updateDeposits pp txb deposits) - getCoin deposits

Functions used in UTxO rules, continued¶

data inInterval (slot : Slot) : (Maybe Slot × Maybe Slot) → Type where
  both   : ∀ {l r}  → l ≤ slot × slot ≤ r  →  inInterval slot (just l   , just r)
  lower  : ∀ {l}    → l ≤ slot             →  inInterval slot (just l   , nothing)
  upper  : ∀ {r}    → slot ≤ r             →  inInterval slot (nothing  , just r)
  none   :                                    inInterval slot (nothing  , nothing)

-- Note: inInterval has to be a type definition for inference to work
instance
  Dec-inInterval : inInterval ⁇²
  Dec-inInterval {slot} {just x  , just y } .dec with x ≤? slot | slot ≤? y
  ... | no ¬p₁ | _      = no λ where (both (h₁ , h₂)) → ¬p₁ h₁
  ... | yes p₁ | no ¬p₂ = no λ where (both (h₁ , h₂)) → ¬p₂ h₂
  ... | yes p₁ | yes p₂ = yes (both (p₁ , p₂))
  Dec-inInterval {slot} {just x  , nothing} .dec with x ≤? slot
  ... | no ¬p = no  (λ where (lower h) → ¬p h)
  ... | yes p = yes (lower p)
  Dec-inInterval {slot} {nothing , just x } .dec with slot ≤? x
  ... | no ¬p = no  (λ where (upper h) → ¬p h)
  ... | yes p = yes (upper p)
  Dec-inInterval {slot} {nothing , nothing} .dec = yes none

  HasCoin-UTxOState : HasCoin UTxOState
  HasCoin-UTxOState .getCoin s = getCoin (UTxOState.utxo s)
                               + (UTxOState.fees s)
                               + getCoin (UTxOState.deposits s)
                               + UTxOState.donations s

coinPolicies : ℙ ScriptHash
coinPolicies = policies (inject 1)

isAdaOnly : Value → Type
isAdaOnly v = policies v ≡ᵉ coinPolicies

collateralCheck : PParams → Tx → UTxO → Type
collateralCheck pp tx utxo =
  All (λ (addr , _) → isVKeyAddr addr) (range (utxo ∣ collateral))
  × isAdaOnly balance′
  × coin balance′ * 100 ≥ txfee * pp .collateralPercentage
  × collateral ≢ ∅
  where
    open Tx tx; open TxBody body
    balance′ = balance (utxo ∣ collateral)

Functions used in UTxO rules, continued¶

module _ (let open UTxOState; open TxBody) where

  depositRefunds : PParams → UTxOState → TxBody → Coin
  depositRefunds pp st txb = negPart (depositsChange pp txb (st .deposits))

  newDeposits : PParams → UTxOState → TxBody → Coin
  newDeposits pp st txb = posPart (depositsChange pp txb (st .deposits))

  consumed : PParams → UTxOState → TxBody → Value
  consumed pp st txb
    =  balance (st .utxo ∣ txb .txins)
    +  txb .mint
    +  inject (depositRefunds pp st txb)
    +  inject (getCoin (txb .txwdrls))

  produced : PParams → UTxOState → TxBody → Value
  produced pp st txb = balance (outs txb)
                     + inject (txb .txfee)
                     + inject (newDeposits pp st txb)
                     + inject (txb .txdonation)

As seen in Figure 'Functions-used-in-UTxO-rules,-continued', we redefine depositRefunds and newDeposits via depositsChange, which computes the difference between the total deposits before and after their application. This simplifies their definitions and some correctness proofs. We then add the absolute value of depositsChange to consumed or produced depending on its sign. This is done via negPart and posPart, which satisfy the key property that their difference is the identity function.

Figure 'Functions-used-in-UTxO-rules' defines the function minfee. In Conway, minfee includes the cost for reference scripts. This is calculated using scriptsCost (see 'fig:scriptsCost' (unresolved reference)).

Figure 'Functions-used-in-UTxO-rules' also shows the signature of ValidCertDeposits. Inhabitants of this type are constructed in one of eight ways, corresponding to seven certificate types plus one for an empty list of certificates. Suffice it to say that ValidCertDeposits is used to check the validity of the deposits in a transaction so that the function updateCertDeposits can correctly register and deregister deposits in the UTxO state based on the certificates in the transaction.

UTXOS rule¶

open PParams

private variable
  Γ : UTxOEnv
  s s' : UTxOState
  tx : Tx
  utxo : UTxO
  fees donations : Coin
  deposits : Deposits

open UTxOEnv

data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type where

  Scripts-Yes :
    let  pp         = Γ .pparams

         open Tx tx renaming (body to txb); open TxBody txb

         p2Scripts  = collectP2ScriptsWithContext pp tx utxo
      in
        ∙ ValidCertDeposits pp deposits txcerts
        ∙ evalP2Scripts p2Scripts ≡ isValid
        ∙ isValid ≡ true
          ────────────────────────────────
          Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#16704}{\htmlId{17262}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#16718}{\htmlId{17269}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#16742}{\htmlId{17276}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#16723}{\htmlId{17287}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} (\,\href{Ledger.Conway.Utxo.html#16704}{\htmlId{17316}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{17321}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Transaction.html#4623}{\htmlId{17323}{\htmlClass{Function}{\text{txins}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{17329}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,) \,\href{Axiom.Set.Map.html#6320}{\htmlId{17332}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, (\,\href{Ledger.Conway.Utxo.html#5640}{\htmlId{17336}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Conway.Utxo.html#16975}{\htmlId{17341}{\htmlClass{Function}{\text{txb}}}}\,) \\ \,\href{Ledger.Conway.Utxo.html#16718}{\htmlId{17348}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17353}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Transaction.html#4717}{\htmlId{17355}{\htmlClass{Function}{\text{txfee}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#11625}{\htmlId{17363}{\htmlClass{Function}{\text{updateDeposits}}}}\, \,\href{Ledger.Conway.Utxo.html#16893}{\htmlId{17378}{\htmlClass{Bound}{\text{pp}}}}\, \,\href{Ledger.Conway.Utxo.html#16975}{\htmlId{17381}{\htmlClass{Function}{\text{txb}}}}\, \,\href{Ledger.Conway.Utxo.html#16742}{\htmlId{17385}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#16723}{\htmlId{17396}{\htmlClass{Generalizable}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17406}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Transaction.html#4959}{\htmlId{17408}{\htmlClass{Function}{\text{txdonation}}}}\, \end{pmatrix}$
  Scripts-No :
    let  pp         = Γ .pparams

         open Tx tx renaming (body to txb); open TxBody txb

         p2Scripts  = collectP2ScriptsWithContext pp tx utxo
      in
        ∙ evalP2Scripts p2Scripts ≡ isValid
        ∙ isValid ≡ false
          ────────────────────────────────
          Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#16704}{\htmlId{17767}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#16718}{\htmlId{17774}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#16742}{\htmlId{17781}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#16723}{\htmlId{17792}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Utxo.html#16704}{\htmlId{17820}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{17825}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Transaction.html#5158}{\htmlId{17827}{\htmlClass{Function}{\text{collateral}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{17838}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#16718}{\htmlId{17842}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17847}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Utxo.html#5800}{\htmlId{17849}{\htmlClass{Function}{\text{cbalance}}}}\, (\,\href{Ledger.Conway.Utxo.html#16704}{\htmlId{17859}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{17864}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Transaction.html#5158}{\htmlId{17866}{\htmlClass{Function}{\text{collateral}}}}\,) \\ \,\href{Ledger.Conway.Utxo.html#16742}{\htmlId{17880}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Utxo.html#16723}{\htmlId{17891}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$

unquoteDecl Scripts-Yes-premises = genPremises Scripts-Yes-premises (quote Scripts-Yes)
unquoteDecl Scripts-No-premises  = genPremises Scripts-No-premises  (quote Scripts-No)

data _⊢_⇀⦇_,UTXO⦈_ where

UTXO inference rules¶

  UTXO-inductive :
    let pp        = Γ .pparams
        slot      = Γ .slot
        treasury  = Γ .treasury
        utxo      = s .UTxOState.utxo

        open Tx tx renaming (body to txb); open TxBody txb
        open TxWitnesses wits

        txoutsʰ   = mapValues txOutHash txouts
        overhead  = 160
    in
    ∙ txins ≢ ∅                              ∙ txins ∪ refInputs ⊆ dom utxo
    ∙ txins ∩ refInputs ≡ ∅                  ∙ inInterval slot txvldt
    ∙ minfee pp utxo tx ≤ txfee              ∙ (txrdmrs ˢ ≢ ∅ → collateralCheck pp tx utxo)
    ∙ consumed pp s txb ≡ produced pp s txb  ∙ coin mint ≡ 0
    ∙ txsize ≤ maxTxSize pp
    ∙ refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx
    ∙ ∀[ (_ , txout) ∈ ∣ txoutsʰ ∣ ]
        inject ((overhead + utxoEntrySize txout) * coinsPerUTxOByte pp) ≤ᵗ getValueʰ txout
    ∙ ∀[ (_ , txout) ∈ ∣ txoutsʰ ∣ ]
        serSize (getValueʰ txout) ≤ maxValSize pp
    ∙ ∀[ (a , _) ∈ range txoutsʰ ]
        Sum.All (const ⊤) (λ a → a .BootstrapAddr.attrsSize ≤ 64) a
    ∙ ∀[ (a , _) ∈ range txoutsʰ ]  netId a         ≡ NetworkId
    ∙ ∀[ a ∈ dom txwdrls ]          NetworkIdOf a ≡ NetworkId
    ∙ txNetworkId  ~ just NetworkId
    ∙ curTreasury  ~ just treasury
    ∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'
      ────────────────────────────────
      Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'

pattern UTXO-inductive⋯ tx Γ s x y z w k l m c v j n o p q r t u h
  = UTXO-inductive {Γ = Γ} {s = s} {tx = tx} (x , y , z , w , k , l , m , c , v , j , n , o , p , q , r , t , u , h)
unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO-inductive)

Figure 'UTXO-inference-rules' ties all the pieces of the UTXO rule together. The symbol ≡? is explained in 'sec:notation' (unresolved reference).