UTxO¶

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 using (scriptsCost)
open import Ledger.Conway.Specification.Certs govStructure

instance
  _ = +-0-monoid

Functions supporting UTxO rules¶

This section defines types and functions needed for the UTxO transition system.

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 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
  -- pool deposits are not added a second time if they are already present
  -- (reregistrations or duplicate certificates).
  = 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 Transition 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#16569}{\htmlId{17133}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16583}{\htmlId{17140}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16621}{\htmlId{17147}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16597}{\htmlId{17158}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\htmlId{17186}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#16569}{\htmlId{17187}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{17192}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#4816}{\htmlId{17194}{\htmlClass{Function}{\text{txIns}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{17200}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{17201}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{17203}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\htmlId{17206}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#4858}{\htmlId{17207}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#16849}{\htmlId{17212}{\htmlClass{Function}{\text{txb}}}}\,\,\htmlId{17215}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16583}{\htmlId{17219}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17224}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#5038}{\htmlId{17226}{\htmlClass{Function}{\text{txFee}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#12538}{\htmlId{17234}{\htmlClass{Function}{\text{updateDeposits}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#16770}{\htmlId{17249}{\htmlClass{Bound}{\text{pp}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#16849}{\htmlId{17252}{\htmlClass{Function}{\text{txb}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#16621}{\htmlId{17256}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16597}{\htmlId{17267}{\htmlClass{Generalizable}{\text{donations}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17277}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#5208}{\htmlId{17279}{\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#16569}{\htmlId{17630}{\htmlClass{Generalizable}{\text{utxo}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16583}{\htmlId{17637}{\htmlClass{Generalizable}{\text{fees}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16621}{\htmlId{17644}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16597}{\htmlId{17655}{\htmlClass{Generalizable}{\text{donations}}}}\, \end{pmatrix}$ ⇀⦇ tx ,UTXOS⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Utxo.html#16569}{\htmlId{17683}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{17688}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#4888}{\htmlId{17690}{\htmlClass{Function}{\text{collateralInputs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{17707}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16583}{\htmlId{17711}{\htmlClass{Generalizable}{\text{fees}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17716}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Utxo.html#5018}{\htmlId{17718}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{17727}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Utxo.html#16569}{\htmlId{17728}{\htmlClass{Generalizable}{\text{utxo}}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{17733}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Conway.Specification.Transaction.html#4888}{\htmlId{17735}{\htmlClass{Function}{\text{collateralInputs}}}}\,\,\htmlId{17751}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16621}{\htmlId{17755}{\htmlClass{Generalizable}{\text{deposits}}}}\, \\ \,\href{Ledger.Conway.Specification.Utxo.html#16597}{\htmlId{17766}{\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)

The UTXO Transition System¶

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

One of the checks is ensuring that the validity interval bounds are translatable to UTCTime. This is necessary to ensure that transVITime can build a POSIXTimeRange from it. We only check for translatability of the upper bound because the lower bound is in the past and therefore guaranteed to be translatable.

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 ∪ collateralInputs ⊆ dom utxo
    ∙ inInterval slot txVldt
    ∙ minfee pp utxo tx ≤ txFee
    ∙ (txrdmrs ˢ ≢ ∅ → collateralCheck pp tx utxo)
    ∙ consumed pp s txb ≡ produced pp s txb
    ∙ coin mint ≡ 0
    ∙ (∅ᵐ ≢ᵐ txrdmrs × nothing ≢ proj₂ txVldt →
         map epochInfoSlotToUTCTime (proj₂ txVldt) ≢ nothing
      )
    ∙ 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 w k l m c d v j n o p q r t u h
  = UTXO-inductive {Γ = Γ} {s = s} {tx = tx} (x , y , w , k , l , m , c , d , 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.