The UTxO Transition System¶
This is a work-in-progress of the Dijkstra-era UTxO transition system. Historically, this module captured the phase-1 structural checks specific to Dijkstra (nested transactions + guards). It now also contains a first pass at the batch semantics and the phase-2 (Plutus) execution model for validating a top-level transaction together with all of its subtransactions.
The primary guiding design principles are
- Spend-side safety. All spending inputs across the whole batch must come from a pre-batch UTxO snapshot (see point 6 of the Changes to Transaction Validity section of CIP-0118);
- Batch-scoped witnesses. Scripts and datums are collected once per batch and then shared for phase-2 evaluation; CIP-0118 explicitly states that reference scripts, and by implication reference-input-resolved UTxO entries, could be outputs of preceding transactions in the batch (see point 5 of the Changes to Transaction Validity section of CIP-0118);
- Batch-consistency. No two transactions in the batch may spend the
same input. This is enforced explicitly at the top level by a predicate
(called
NoOverlappingSpendInputsbelow) that is checked in theUTXOrule.
Functions and Types of the UTxO Transition System¶
The UTxO rules are parameterised by an environment UTxOEnv and an
evolving state UTxOState.
record DepositsChange : Type where field depositsChangeTop : ℤ depositsChangeSub : ℤ record UTxOEnv : Type where field slot : Slot pparams : PParams treasury : Treasury utxo₀ : UTxO depositsChange : DepositsChange allScripts : ℙ Script accountBalances : Rewards record SubUTxOEnv : Type where field slot : Slot pparams : PParams treasury : Treasury utxo₀ : UTxO isTopLevelValid : Bool allScripts : ℙ Script accountBalances : Rewards
The UTxOEnv carries
utxo₀: pre-batch snapshot of the UTxO;allScripts: batch-wide script pool containing all scripts available to the batch (witness scripts plus reference scripts resolved from allowed reference inputs and batch outputs);
The pre-batch UTxO snapshot utxo₀ is used to resolve all
spend-side lookups (inputs, collateral, and datum lookup for spent outputs).
The allScripts field of UTxOEnv capture
the batch-wide script pool. This pool is used to resolve all
script lookups during validation.
Scripts are treated as batch-wide witnesses; attaching a script to a transaction in the batch makes it available for phase-2 validation of any transaction in the batch, independent of which subtransaction originally supplied it.
If Γ denotes a particular UTxOEnv, then
we often access the allScripts field of Γ
via ScriptPoolOf Γ.
record UTxOState : Type where constructor ⟦_,_,_⟧ᵘ field utxo : UTxO fees : Fees donations : Donations
outs : Tx ℓ → UTxO outs tx = mapKeys (TxIdOf tx ,_) (TxOutsOf tx) balance : UTxO → Value balance utxo = ∑ˢ[ v ← valuesOfUTxO utxo ] v cbalance : UTxO → Coin cbalance utxo = coin (balance utxo) refScriptsSize : Tx ℓ → UTxO → ℕ refScriptsSize tx utxo = ∑ˡ[ x ← setToList (referenceScripts tx utxo) ] scriptSize x minfee : PParams → TopLevelTx → UTxO → Coin minfee pp txTop utxo = pp .a * (SizeOf txTop) + pp .b + txScriptFee (pp .prices) (totExUnits txTop) + scriptsCost pp (refScriptsSize txTop utxo)
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 → TopLevelTx → UTxO → Type collateralCheck pp txTop utxo = All (λ (addr , _) → isVKeyAddr addr) (range (utxo ∣ CollateralInputsOf txTop)) × isAdaOnly (balance (utxo ∣ CollateralInputsOf txTop)) × coin (balance (utxo ∣ CollateralInputsOf txTop)) * 100 ≥ (TxFeesOf txTop) * pp .collateralPercentage × (CollateralInputsOf txTop) ≢ ∅ module _ (depositsChange : DepositsChange) where open DepositsChange depositsChange depositRefundsSub : Coin depositRefundsSub = negPart depositsChangeSub newDepositsSub : Coin newDepositsSub = posPart depositsChangeSub newDepositsTop : Coin newDepositsTop = posPart depositsChangeTop depositRefundsTop : Coin depositRefundsTop = negPart depositsChangeTop consumedTx : Tx ℓ → UTxO → Value consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx) + MintedValueOf tx + inject (getCoin (WithdrawalsOf tx)) consumed : TopLevelTx → UTxO → Value consumed txTop utxo = consumedTx txTop utxo + inject depositRefundsTop consumedBatch : TopLevelTx → UTxO → Value consumedBatch txTop utxo = consumed txTop utxo + ∑ˡ[ stx ← SubTransactionsOf txTop ] (consumedTx stx utxo) + inject depositRefundsSub
Direct deposits can be made into account addresses.
In the preservation-of-value equation, direct deposits appear on the
produced side: getCoin (DirectDepositsOf tx) sums the ADA of all direct deposits in
the transaction and that amount is deposited into accounts.
producedTx : Tx ℓ → Value producedTx tx = balance (outs tx) + inject (DonationsOf tx) + inject (getCoin (DirectDepositsOf tx)) produced : TopLevelTx → Value produced txTop = producedTx txTop + inject (TxFeesOf txTop) + inject newDepositsTop producedBatch : TopLevelTx → Value producedBatch txTop = produced txTop + ∑ˡ[ stx ← SubTransactionsOf txTop ] (producedTx stx) + inject newDepositsSub
CIP-159 Notes¶
Preservation of Value¶
CIP-159 introduces two new fields to transactions: directDeposits and
balanceIntervals. Direct deposits represent value that flows from the transaction
into account addresses.
In the preservation-of-value equation, direct deposits appear on the
produced side: value leaves the UTxO and enters account balances. The
getCoin (DirectDepositsOf tx) term, appearing in the definition of
producedTx, sums the ADA of all direct deposits in
the transaction.
Phantom Asset Prevention¶
NoPhantomWithdrawals : Rewards → TopLevelTx → Type NoPhantomWithdrawals preBalances txTop = ∀[ (addr , amt) ∈ allWithdrawals txTop ˢ ] amt ≤ maybe id 0 (lookupᵐ? preBalances (RewardAddress.stake addr))
The Problem. CIP-159 identifies a "phantom asset" attack when nested transactions combine direct deposits and withdrawals to the same account within a single batch. If a sub-transaction deposits ADA into an account and a later sub-transaction withdraws it, Plutus scripts may be tricked into believing native assets were minted.
The Solution. Withdrawals across the entire batch are bounded by the
pre-batch account balances. The NoPhantomWithdrawals predicate
checks that the total withdrawal for each reward address (aggregated via
allWithdrawals) does not exceed the pre-batch balance of the
corresponding credential. This mirrors the spend-side safety principle where
spending inputs must come from the pre-batch UTxO snapshot (utxo₀).
The UTXOS Transition System¶
Phase-2 Validation¶
Phase-2 validation is the evaluation of all Plutus scripts needed by the top-level transaction and all its subtransactions in the shared, batch-scoped context.
The Script.Validation module is not UTxOEnv-context
aware, so in order to assemble the correct set of scripts and data
for each transaction, we must provide Script.Validation with
the following components:
- the pre-batch spend-side snapshot
UTxOOfΓ, - the script pool
ScriptPoolOfΓ,
Phase-2 scripts together with their context are collected by the function
allP2ScriptsWithContext:
allP2ScriptsWithContext : UTxOEnv → TopLevelTx → List (P2Script × List Data × ExUnits × CostModel) allP2ScriptsWithContext Γ txTop = p2ScriptsWithContext txTop ++ concatMap p2ScriptsWithContext (SubTransactionsOf txTop) where p2ScriptsWithContext : Tx ℓ → List (P2Script × List Data × ExUnits × CostModel) p2ScriptsWithContext t = collectP2ScriptsWithContext (PParamsOf Γ) txTop (UTxOOf Γ) -- (1) (ScriptPoolOf Γ) -- (2)
New in Dijkstra¶
In Dijkstra, the state-modifying logic, which before was part to
UTXOS (cf,. Conway specification), now belongs to the
UTXO rule.
The UTXOS rule validates the correspondence between evaluating
phase-2 scripts and the isValid flag in the top-level transaction.
Phase-2 validation occurs after (successful) phase-1 validation. In Dijkstra,
the evaluation of scripts, from the sub- and top-level transactions, is defered
to the UTXOS rule. This enforces that sub-transactions and
other aspects of the top-level transaction are phase-1 valid.
data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → ⊤ → TopLevelTx → ⊤ → Type where UTXOS : ∙ evalP2Scripts (allP2ScriptsWithContext Γ txTop) ≡ IsValidFlagOf txTop ──────────────────────────────── Γ ⊢ tt ⇀⦇ txTop ,UTXOS⦈ tt
The UTXO Transition System¶
The UTXO Transition System¶
The CIP states:
All inputs of all transactions in a single batch must be contained in the UTxO set before any of the batch transactions are applied. This ensures that operation of scripts is not disrupted, for example, by temporarily duplicating thread tokens, or falsifying access to assets via flash loans.
The SUBUTXO Rule¶
-
The set of spending inputs must be nonempty. This prevents replay attacks.
-
The set of spending and reference inputs must exist in the UTxO before applying the transaction (or partially applying any part of it).
-
The set of spending inputs must exist in the UTXO state, which has been updated by other sub-transactions in the batch. This prevents sub/top-level transactions from spending inputs twice. In other words, spending inputs across all top- and sub-level transactions are disjoint.
-
Direct deposit targets must be registered accounts (their credentials must appear in
dom accountBalances). -
Each balance interval assertion must hold against the pre-batch account balances; this is a Phase-1 validity condition.
data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where SUBUTXO : let UTxOOverhead = 160 maxBootstrapAddrSize = 64 in ∙ SpendInputsOf txSub ≢ ∅ -- (1) ∙ SpendInputsOf txSub ⊆ dom (UTxOOf Γ) -- (2) ∙ ReferenceInputsOf txSub ⊆ dom (UTxOOf Γ) -- (2) ∙ SpendInputsOf txSub ⊆ dom (UTxOOf s₀) -- (3) ∙ inInterval (SlotOf Γ) (ValidIntervalOf txSub) ∙ coin (MintedValueOf txSub) ≡ 0 ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txSub ∣ ] (inject ((UTxOOverhead + utxoEntrySize o) * coinsPerUTxOByte (PParamsOf Γ)) ≤ᵗ txOutToValue o) ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txSub ∣ ] (serializedSize (txOutToValue o) ≤ maxValSize (PParamsOf Γ)) ∙ ∀[ (a , _) ∈ range (TxOutsOf txSub) ] (Sum.All (const ⊤) (λ a → AttrSizeOf a ≤ maxBootstrapAddrSize) a) ∙ ∀[ (a , _) ∈ range (TxOutsOf txSub) ] (netId a ≡ NetworkId) ∙ ∀[ a ∈ dom (WithdrawalsOf txSub)] (NetworkIdOf a ≡ NetworkId) ∙ MaybeNetworkIdOf txSub ~ just NetworkId ∙ CurrentTreasuryOf txSub ~ just (TreasuryOf Γ) ∙ dom (DirectDepositsOf txSub) ⊆ dom (AccountBalancesOf Γ) ∙ dom (BalanceIntervalsOf txSub) ⊆ dom (AccountBalancesOf Γ) ∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txSub ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval) ──────────────────────────────── let s₁ = if IsTopLevelValidFlagOf Γ then $\begin{pmatrix} \,\htmlId{18285}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{18286}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{18293}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{18296}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#11706}{\htmlId{18298}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7676}{\htmlId{18312}{\htmlClass{Generalizable}{\text{txSub}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{18318}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{18319}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{18321}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7717}{\htmlId{18324}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7676}{\htmlId{18329}{\htmlClass{Generalizable}{\text{txSub}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{18337}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{18344}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{18349}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{18361}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{18364}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#650}{\htmlId{18366}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7676}{\htmlId{18378}{\htmlClass{Generalizable}{\text{txSub}}}}\, \end{pmatrix}$ else $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{18393}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{18400}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{18405}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{18412}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{18417}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{18429}{\htmlClass{Generalizable}{\text{s₀}}}}\, \end{pmatrix}$ in Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXO⦈ s₁
The UTXO Rule¶
-
The set of spending inputs must be nonempty. This prevents replay attacks.
-
The set of spending and reference inputs must exist in the UTxO before applying the transaction (or partially applying any part of it).
-
The set of spending inputs must exist in the UTXO state, which has been updated by other sub-transactions in the batch. This prevents sub/top-level transactions from spending inputs twice. In other words, spending inputs across all top- and sub-level transactions are disjoint.
-
In Legacy Mode: The top-level transaction must be self-balancing.
data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv × Bool → UTxOState → TopLevelTx → UTxOState → Type where UTXO : let UTxOOverhead = 160 maxBootstrapAddrSize = 64 in ∙ SpendInputsOf txTop ≢ ∅ ∙ SpendInputsOf txTop ⊆ dom (UTxOOf Γ) -- (2) ∙ ReferenceInputsOf txTop ⊆ dom (UTxOOf Γ) -- (2) ∙ SpendInputsOf txTop ⊆ dom (UTxOOf s₀) -- (3) ∙ inInterval (SlotOf Γ) (ValidIntervalOf txTop) ∙ minfee (PParamsOf Γ) txTop (UTxOOf Γ) ≤ TxFeesOf txTop ∙ coin (MintedValueOf txTop) ≡ 0 ∙ consumedBatch (DepositsChangeOf Γ) txTop (UTxOOf Γ) ≡ producedBatch (DepositsChangeOf Γ) txTop ∙ (legacyMode ≡ true → consumed (DepositsChangeOf Γ) txTop (UTxOOf Γ) ≡ produced (DepositsChangeOf Γ) txTop) -- (4) ∙ SizeOf txTop ≤ maxTxSize (PParamsOf Γ) ∙ ∑ˡ[ x ← setToList (allReferenceScripts txTop (UTxOOf Γ)) ] scriptSize x ≤ (PParamsOf Γ) .maxRefScriptSizePerTx ∙ ((RedeemersOf txTop ˢ ≢ ∅) ⊎ (List.Any (λ txSub → RedeemersOf txSub ˢ ≢ ∅) (SubTransactionsOf txTop)) → collateralCheck (PParamsOf Γ) txTop (UTxOOf Γ)) ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txTop ∣ ] (inject ((UTxOOverhead + utxoEntrySize o) * coinsPerUTxOByte (PParamsOf Γ)) ≤ᵗ txOutToValue o) ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txTop ∣ ] (serializedSize (txOutToValue o) ≤ maxValSize (PParamsOf Γ)) ∙ ∀[ (a , _) ∈ range (TxOutsOf txTop) ] (Sum.All (const ⊤) (λ a → AttrSizeOf a ≤ maxBootstrapAddrSize)) a ∙ ∀[ (a , _) ∈ range (TxOutsOf txTop) ] (netId a ≡ NetworkId) ∙ ∀[ a ∈ dom (WithdrawalsOf txTop)] NetworkIdOf a ≡ NetworkId ∙ MaybeNetworkIdOf txTop ~ just NetworkId ∙ CurrentTreasuryOf txTop ~ just (TreasuryOf Γ) ∙ dom (DirectDepositsOf txTop) ⊆ dom (AccountBalancesOf Γ) ∙ dom (BalanceIntervalsOf txTop) ⊆ dom (AccountBalancesOf Γ) ∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txTop ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval) ∙ Γ ⊢ _ ⇀⦇ txTop ,UTXOS⦈ _ ──────────────────────────────── let s₁ = if IsValidFlagOf txTop then $\begin{pmatrix} \,\htmlId{21270}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{21271}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{21278}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{21281}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#11706}{\htmlId{21283}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7648}{\htmlId{21297}{\htmlClass{Generalizable}{\text{txTop}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{21303}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{21304}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{21306}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7717}{\htmlId{21309}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7648}{\htmlId{21314}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{21322}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{21329}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{21332}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#10767}{\htmlId{21334}{\htmlClass{Field}{\text{TxFeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7648}{\htmlId{21343}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{21351}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{21363}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{21366}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#650}{\htmlId{21368}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7648}{\htmlId{21380}{\htmlClass{Generalizable}{\text{txTop}}}}\, \end{pmatrix}$ else $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{21395}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{21402}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{21405}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\htmlId{21407}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#10602}{\htmlId{21408}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7648}{\htmlId{21427}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{21432}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{21434}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{21438}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{21445}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{21448}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7854}{\htmlId{21450}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{21459}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{21460}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{21467}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{21470}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#10602}{\htmlId{21472}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7648}{\htmlId{21491}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{21496}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{21500}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7621}{\htmlId{21512}{\htmlClass{Generalizable}{\text{s₀}}}}\, \end{pmatrix}$ in (Γ , legacyMode) ⊢ s₀ ⇀⦇ txTop ,UTXO⦈ s₁