Skip to content

UTxO

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

The UTxO transition system is built up from a number of smaller parts defined in this section, culminating in the UTXO rule given in the final subsection below (UTXO Inference Rule).

Accounting

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 Corduan22.)

{-# 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.Specification.Abstract
open import Ledger.Conway.Specification.Transaction

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

open import Ledger.Conway.Specification.Script.Validation txs abs
open import Ledger.Conway.Specification.Fees txs using (scriptsCost)
open import Ledger.Conway.Specification.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

UTxO transition system types

As its name indicates, DepositPurpose specifies the purpose of a deposit. Deposits are stored in the deposits field of the UTxOState type defined in this section. (The DepositPurpose and Deposits types are defined in the Deposit Types section of the Certs module.)

UTxO environment

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

UTxO states

record UTxOState : Type where
  constructor ⟦_,_,_,_⟧ᵘ
  field
    utxo       : UTxO
    fees       : Fees
    deposits   : Deposits
    donations  : Donations
record HasUTxOState {a} (A : Type a) : Type a where
  field UTxOStateOf : A  UTxOState
open HasUTxOState ⦃...⦄ public

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

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

  HasFee-UTxOState : HasFees UTxOState
  HasFee-UTxOState .FeesOf = UTxOState.fees

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

  HasDonations-UTxOState : HasDonations UTxOState
  HasDonations-UTxOState .DonationsOf = UTxOState.donations

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

UTxO transitions

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

(The main constructor of this type, UTXO-inductive, is defined in the UTXO Inference Rule subsection below.)

Functions used in the UTxO rules

Here we define, among other things,

  • the outs function, which creates the unspent outputs generated by a transaction; it maps the transaction id and output index to the output;

  • the balance function, which calculates sum total of all the coin in a given UTxO;

  • the minfee function, which includes the cost for reference scripts, calculated using the scriptsCost function defined in the Fees module.

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 _                = 

The type ValidCertDeposits has the following signature:

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

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.

  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? _ _)

The updateDeposits function is responsible for updating this map; it is split into updateCertDeposits and updateProposalDeposits, which are responsible for certificates and proposals, respectively. 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 Corduan22 and CVG19.)

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 txGovProposals 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

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  collateralInputs))
  × isAdaOnly balance′
  × coin balance′ * 100  txFee * pp .collateralPercentage
  × collateralInputs  
  where
    open Tx tx; open TxBody body
    balance′ = balance (utxo  collateralInputs)
module _ (let open UTxOState; open TxBody) where

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.

  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 .txWithdrawals))

  produced : PParams  UTxOState  TxBody  Value
  produced pp st txb = balance (outs txb)
                     + inject (txb .txFee)
                     + inject (newDeposits pp st txb)
                     + inject (txb .txDonation)

The UTXOS rule

open PParams
private variable
  Γ : UTxOEnv
  s s' : UTxOState
  tx : Tx
  utxo : UTxO
  fees : Fees
  donations : Donations
  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.Specification.Utxo.html#16556}{\htmlId{17120}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16570}{\htmlId{17127}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16608}{\htmlId{17134}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16584}{\htmlId{17145}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\htmlId{17173}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#16556}{\htmlId{17174}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{17179}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#4850}{\htmlId{17181}{\htmlClass{Function}{\text{txIns}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{17187}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{17188}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{17190}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\htmlId{17193}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#4920}{\htmlId{17194}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#16836}{\htmlId{17199}{\htmlClass{Function}{\text{txb}}}}\,\,\htmlId{17202}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16570}{\htmlId{17206}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17211}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#5072}{\htmlId{17213}{\htmlClass{Function}{\text{txFee}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#12475}{\htmlId{17221}{\htmlClass{Function}{\text{updateDeposits}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#16757}{\htmlId{17236}{\htmlClass{Bound}{\text{pp}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#16836}{\htmlId{17239}{\htmlClass{Function}{\text{txb}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#16608}{\htmlId{17243}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16584}{\htmlId{17254}{\htmlClass{Generalizable}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17264}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#5242}{\htmlId{17266}{\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.Specification.Utxo.html#16556}{\htmlId{17617}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16570}{\htmlId{17624}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16608}{\htmlId{17631}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16584}{\htmlId{17642}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#16556}{\htmlId{17670}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{17675}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#4922}{\htmlId{17677}{\htmlClass{Function}{\text{collateralInputs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{17694}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16570}{\htmlId{17698}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17703}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#5080}{\htmlId{17705}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{17714}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#16556}{\htmlId{17715}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#10678}{\htmlId{17720}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#4922}{\htmlId{17722}{\htmlClass{Function}{\text{collateralInputs}}}}\,\,\htmlId{17738}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16608}{\htmlId{17742}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16584}{\htmlId{17753}{\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)

UTXO Inference Rule

This section ties all the pieces of the UTXO rule together.

(The symbol ≡? is explained in Section Notation.)

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

  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 txWithdrawals ]    NetworkIdOf a   NetworkId
     txNetworkId  ~ just NetworkId
     currentTreasury  ~ 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)

References

[Corduan22] Jared Corduan. Track individual deposits. 2022.

[CVG19] Jared Corduan and Polina Vinogradova and Matthias Güdemann. A Formal Specification of the Cardano Ledger. 2019.