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.)
Functions supporting UTxO rules¶
totExUnits : Tx → ExUnits totExUnits tx = ∑[ (_ , eu) ← tx .wits .txrdmrs ] eu
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
field utxo : UTxO fees : Fees deposits : Deposits donations : Donations
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 thescriptsCost
function defined in the Fees module.
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)
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.
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 (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)
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)
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)
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¶
data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type where Scripts-Yes : let pp = Γ .pparams
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
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}$
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
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'
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.