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 NoOverlappingSpendInputs below) that is checked in the UTXO rule.

{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Abstract
open import Ledger.Dijkstra.Specification.Transaction

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

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

import Data.List.Relation.Unary.All as List
import Data.List.Relation.Unary.AllPairs as List
import Data.Sum.Relation.Unary.All as Sum


totExUnits : ∀{ℓ} → Tx ℓ → ExUnits
totExUnits tx = ∑[ (_ , eu) ← RedeemersOf tx ] eu

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

utxoEntrySize : TxOut → MemoryEstimate
utxoEntrySize (_ , v , _ , _) = utxoEntrySizeWithoutVal + size v

open PParams

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
    allData           : DataHash ⇀ Datum

record SubUTxOEnv : Type where
  field
    slot             : Slot
    pparams          : PParams
    treasury         : Treasury
    utxo₀            : UTxO
    isTopLevelValid  : Bool
    allScripts       : ℙ Script
    allData          : DataHash ⇀ Datum

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);
allData: datum-by-hash pool containing all data available to the batch.

The pre-batch UTxO snapshot utxo₀ is used to resolve all spend-side lookups (inputs, collateral, and datum lookup for spent outputs).

The allScripts and allData fields of UTxOEnv capture the batch-wide script pool and datum-by-hash pool respectively. These pools are used to resolve all script and datum lookups during phase-2 validation of subtransactions in the batch. Scripts and data are treated as batch-wide witnesses; attaching a script or datum 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 and allData fields of Γ via the ScriptPoolOf Γ and DataPoolOf Γ accessors, respectively.

record UTxOState : Type where
  constructor ⟦_,_,_⟧ᵘ
  field
    utxo       : UTxO
    fees       : Fees
    donations  : Donations

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

record HasIsTopLevelValidFlag {a} (A : Type a) : Type a where
  field IsTopLevelValidFlagOf : A → Bool
open HasIsTopLevelValidFlag ⦃...⦄ public

record HasDepositsChange {a} (A : Type a) : Type a where
  field DepositsChangeOf : A → DepositsChange
open HasDepositsChange ⦃...⦄ public

record HasScriptPool {a} (A : Type a) : Type a where
  field ScriptPoolOf : A → ℙ Script
open HasScriptPool ⦃...⦄ public

record HasDataPool {a} (A : Type a) : Type a where
  field DataPoolOf : A → DataHash ⇀ Datum
open HasDataPool ⦃...⦄ public

record HasSlot {a} (A : Type a) : Type a where
  field SlotOf : A → Slot
open HasSlot ⦃...⦄ public

instance
  HasSlot-UTxOEnv : HasSlot UTxOEnv
  HasSlot-UTxOEnv .SlotOf = UTxOEnv.slot

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

  HasTreasury-UTxOEnv : HasTreasury UTxOEnv
  HasTreasury-UTxOEnv .TreasuryOf = UTxOEnv.treasury

  HasUTxO-UTxOEnv : HasUTxO UTxOEnv
  HasUTxO-UTxOEnv .UTxOOf = UTxOEnv.utxo₀

  HasDepositsChange-UTxOEnv : HasDepositsChange UTxOEnv
  HasDepositsChange-UTxOEnv .DepositsChangeOf = UTxOEnv.depositsChange

  HasScriptPool-UTxOEnv : HasScriptPool UTxOEnv
  HasScriptPool-UTxOEnv .ScriptPoolOf = UTxOEnv.allScripts

  HasDataPool-UTxOEnv : HasDataPool UTxOEnv
  HasDataPool-UTxOEnv .DataPoolOf = UTxOEnv.allData

  HasSlot-SubUTxOEnv : HasSlot SubUTxOEnv
  HasSlot-SubUTxOEnv .SlotOf = SubUTxOEnv.slot

  HasPParams-SubUTxOEnv : HasPParams SubUTxOEnv
  HasPParams-SubUTxOEnv .PParamsOf = SubUTxOEnv.pparams

  HasTreasury-SubUTxOEnv : HasTreasury SubUTxOEnv
  HasTreasury-SubUTxOEnv .TreasuryOf = SubUTxOEnv.treasury

  HasUTxO-SubUTxOEnv : HasUTxO SubUTxOEnv
  HasUTxO-SubUTxOEnv .UTxOOf = SubUTxOEnv.utxo₀

  HasIsTopLevelValidFlag-SubUTxOEnv : HasIsTopLevelValidFlag SubUTxOEnv
  HasIsTopLevelValidFlag-SubUTxOEnv .IsTopLevelValidFlagOf = SubUTxOEnv.isTopLevelValid

  HasScriptPool-SubUTxOEnv : HasScriptPool SubUTxOEnv
  HasScriptPool-SubUTxOEnv .ScriptPoolOf = SubUTxOEnv.allScripts

  HasDataPool-SubUTxOEnv : HasDataPool SubUTxOEnv
  HasDataPool-SubUTxOEnv .DataPoolOf = SubUTxOEnv.allData

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

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

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

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

private
  variable
    ℓ          : TxLevel
    A          : Type
    Γ          : A
    legacyMode : Bool
    s₀         : UTxOState
    txTop      : TopLevelTx
    txSub      : SubLevelTx

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 : TopLevelTx → UTxO → ℕ
refScriptsSize txTop utxo =
 ∑ˡ[ x ← setToList (allReferenceScripts txTop 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)

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

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

coinPolicies : ℙ ScriptHash
coinPolicies = policies (inject 1)

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

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

  producedTx : Tx ℓ → Value
  producedTx tx = balance (outs tx) + inject (DonationsOf 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

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 datum-by-hash pool DataPoolOf Γ.
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)
                                    (DataPoolOf Γ)    -- (2)
                                    (ScriptPoolOf Γ)  -- (3)

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¶

unquoteDecl UTXOS-premises = genPremises UTXOS-premises (quote UTXOS)

The UTXO Transition System¶

The SUBUTXO Rule¶

data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where

  SUBUTXO :
    ∙ SpendInputsOf txSub ≢ ∅
    ∙ inInterval (SlotOf Γ) (ValidIntervalOf txSub)
    ∙ MaybeNetworkIdOf txSub ~ just NetworkId
      ────────────────────────────────
    let
       s₁ = if IsTopLevelValidFlagOf Γ
            then $\begin{pmatrix} \,\htmlId{14427}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5511}{\htmlId{14428}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{14435}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{14438}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#10727}{\htmlId{14440}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7768}{\htmlId{14454}{\htmlClass{Generalizable}{\text{txSub}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{14460}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{14461}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{14463}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7809}{\htmlId{14466}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7768}{\htmlId{14471}{\htmlClass{Generalizable}{\text{txSub}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{14479}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{14486}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{14491}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{14503}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{14506}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#650}{\htmlId{14508}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7768}{\htmlId{14520}{\htmlClass{Generalizable}{\text{txSub}}}}\, \end{pmatrix}$ else $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#5511}{\htmlId{14535}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{14542}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{14547}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{14554}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{14559}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{14571}{\htmlClass{Generalizable}{\text{s₀}}}}\, \end{pmatrix}$
    in
      Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXO⦈ s₁

unquoteDecl SUBUTXO-premises = genPremises SUBUTXO-premises (quote SUBUTXO)

The UTXO Rule¶

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.

This is achieved by the following precondition in the UTXO rule:

The set of spending and reference inputs must exist in the UTxO before applying the transaction (or partially applying any part of it).

In addition, the UTXO rule enforces:

No double spending: To prevent double spending across a batch of transactions, all spending input sets (top-level and subtransactions) must be pairwise disjoint. This is enforced by the NoOverlappingSpendInputs txTop precondition.
In Legacy Mode: The top-level transaction must be self-balancing.

UTXO-Premises : (UTxOEnv × Bool) → UTxOState → TopLevelTx → Type
UTXO-Premises (Γ , legacyMode) s₀ txTop =
    SpendInputsOf txTop ≢ ∅
    × inInterval (SlotOf Γ) (ValidIntervalOf txTop)
    × minfee (PParamsOf Γ) txTop (UTxOOf s₀) ≤ TxFeesOf txTop
    × consumedBatch (DepositsChangeOf Γ) txTop (UTxOOf Γ) ≡ producedBatch (DepositsChangeOf Γ) txTop
    × (legacyMode ≡ true → consumed (DepositsChangeOf Γ) txTop (UTxOOf Γ) ≡ produced (DepositsChangeOf Γ) txTop)  -- (3)
    × (SizeOf txTop ≤ maxTxSize (PParamsOf Γ))
    × (refScriptsSize txTop (UTxOOf Γ) ≤ (PParamsOf Γ) .maxRefScriptSizePerTx)
    × (allSpendInputs txTop ⊆ dom (UTxOOf Γ)) -- (1)
    × (allReferenceInputs txTop ⊆ dom (UTxOOf Γ)) -- (1)
    × NoOverlappingSpendInputs txTop -- (2)
    × (RedeemersOf txTop ˢ ≢ ∅ → collateralCheck (PParamsOf Γ) txTop (UTxOOf Γ))
    × (allMintedCoin txTop ≡ 0)
    × (∀[ (_ , o) ∈ ∣ TxOutsOf txTop ∣ ]
       (inject ((160 + utxoEntrySize o) * coinsPerUTxOByte (PParamsOf Γ)) ≤ᵗ txOutToValue o)
       × (serializedSize (txOutToValue o) ≤ maxValSize (PParamsOf Γ)))
    × (∀[ (a , _) ∈ range (TxOutsOf txTop) ]
       (Sum.All (const ⊤) (λ a → AttrSizeOf a ≤ 64)) a × (netId a ≡ NetworkId))
    × (∀[ a ∈ dom (WithdrawalsOf txTop)] NetworkIdOf a ≡ NetworkId)
    × (MaybeNetworkIdOf txTop ~ just NetworkId)
    × (CurrentTreasuryOf txTop  ~ just (TreasuryOf Γ))

data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv × Bool → UTxOState → TopLevelTx → UTxOState → Type where

  UTXO-valid :
    ∙ IsValidFlagOf txTop ≡ true
    ∙ Γ ⊢ _ ⇀⦇ txTop ,UTXOS⦈ _
    ∙ UTXO-Premises (Γ , legacyMode) s₀ txTop
      ────────────────────────────────
      (Γ , legacyMode)  ⊢ s₀ ⇀⦇ txTop ,UTXO⦈ $\begin{pmatrix} \,\htmlId{17372}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5511}{\htmlId{17373}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{17380}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{17383}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#10727}{\htmlId{17385}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7740}{\htmlId{17399}{\htmlClass{Generalizable}{\text{txTop}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{17405}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{17406}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{17408}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7809}{\htmlId{17411}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7740}{\htmlId{17416}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{17424}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{17431}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17434}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#9788}{\htmlId{17436}{\htmlClass{Field}{\text{TxFeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7740}{\htmlId{17445}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{17453}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{17465}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17468}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#650}{\htmlId{17470}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7740}{\htmlId{17482}{\htmlClass{Generalizable}{\text{txTop}}}}\, \end{pmatrix}$

  UTXO-invalid :
    ∙ IsValidFlagOf txTop ≡ false
    ∙ Γ ⊢ _ ⇀⦇ txTop ,UTXOS⦈ _
    ∙ UTXO-Premises (Γ , legacyMode) s₀ txTop
      ────────────────────────────────
      (Γ , legacyMode)  ⊢ s₀ ⇀⦇ txTop ,UTXO⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#5511}{\htmlId{17705}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{17712}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{17715}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\htmlId{17717}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#9623}{\htmlId{17718}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7740}{\htmlId{17737}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{17742}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{17744}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{17748}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{17755}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{17758}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7946}{\htmlId{17760}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{17769}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5511}{\htmlId{17770}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{17777}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{17780}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#9623}{\htmlId{17782}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7740}{\htmlId{17801}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{17806}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{17810}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7713}{\htmlId{17822}{\htmlClass{Generalizable}{\text{s₀}}}}\, \end{pmatrix}$

unquoteDecl UTXO-valid-premises = genPremises UTXO-valid-premises (quote UTXO-valid)
unquoteDecl UTXO-invalid-premises = genPremises UTXO-invalid-premises (quote UTXO-invalid)