{-# 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


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


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


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)


data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → ⊤ → TopLevelTx → ⊤ → Type where

  UTXOS :

    ∙ evalP2Scripts (allP2ScriptsWithContext Γ txTop) ≡ IsValidFlagOf txTop
      ────────────────────────────────
      Γ ⊢ tt ⇀⦇ txTop ,UTXOS⦈ tt


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


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{9730}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#3518}{\htmlId{9731}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{9738}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9741}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#7269}{\htmlId{9743}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4794}{\htmlId{9757}{\htmlClass{Generalizable}{\text{txSub}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9763}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{9764}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9766}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4820}{\htmlId{9769}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4794}{\htmlId{9774}{\htmlClass{Generalizable}{\text{txSub}}}}\, \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{9782}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{9789}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{9794}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{9806}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9809}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#554}{\htmlId{9811}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4794}{\htmlId{9823}{\htmlClass{Generalizable}{\text{txSub}}}}\, \end{pmatrix}$ else $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#3518}{\htmlId{9838}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{9845}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{9850}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{9857}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{9862}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{9874}{\htmlClass{Generalizable}{\text{s₀}}}}\, \end{pmatrix}$
    in
      Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXO⦈ s₁


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


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{11665}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#3518}{\htmlId{11666}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{11673}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11676}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#7269}{\htmlId{11678}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4766}{\htmlId{11692}{\htmlClass{Generalizable}{\text{txTop}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11698}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{11699}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11701}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4820}{\htmlId{11704}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4766}{\htmlId{11709}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{11717}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{11724}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11727}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#6330}{\htmlId{11729}{\htmlClass{Field}{\text{TxFeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4766}{\htmlId{11738}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{11746}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{11758}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11761}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#554}{\htmlId{11763}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4766}{\htmlId{11775}{\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#3518}{\htmlId{11998}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{12005}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{12008}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\htmlId{12010}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#6165}{\htmlId{12011}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4766}{\htmlId{12030}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{12035}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{12037}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{12041}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{12048}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12051}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4957}{\htmlId{12053}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{12062}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#3518}{\htmlId{12063}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{12070}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{12073}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#6165}{\htmlId{12075}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4766}{\htmlId{12094}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{12099}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{12103}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4739}{\htmlId{12115}{\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)