{-# OPTIONS --safe #-}
module Ledger.Dijkstra.Specification.Transaction where

import Data.Maybe.Base as M

open import Ledger.Prelude renaming (filterᵐ to filter)

open import Ledger.Core.Specification.Crypto
open import Ledger.Core.Specification.Epoch
open import Ledger.Dijkstra.Specification.Gov.Base

import Ledger.Core.Specification.Address renaming (RewardAddress to RewardAddress)
import Ledger.Dijkstra.Specification.Certs
import Ledger.Dijkstra.Specification.Gov.Actions
import Ledger.Dijkstra.Specification.PParams
import Ledger.Dijkstra.Specification.Script
import Ledger.Dijkstra.Specification.TokenAlgebra.Base

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

open import Tactic.Derive.DecEq
open import Relation.Nullary.Decidable using (⌊_⌋)


data TxLevel : Type where
  TxLevelTop TxLevelSub : TxLevel


InTopLevel : TxLevel → Type → Type
InTopLevel TxLevelTop X = X
InTopLevel TxLevelSub _ = ⊤

InSubLevel : TxLevel → Type → Type
InSubLevel TxLevelSub X = X
InSubLevel TxLevelTop _ = ⊤


unquoteDecl DecEq-TxLevel = derive-DecEq ((quote TxLevel , DecEq-TxLevel) ∷ [])

private
  variable
    txLevel : TxLevel

data Tag : TxLevel → Type where
  Spend Mint Cert Reward Vote Propose Guard : Tag txLevel
  SubGuard : Tag TxLevelSub

unquoteDecl DecEq-Tag = derive-DecEq ((quote Tag , DecEq-Tag) ∷ [])


record TransactionStructure : Type₁ where
  field
    Ix TxId AuxiliaryData  : Type
    adHashingScheme        : isHashableSet AuxiliaryData
    globalConstants        : GlobalConstants
    crypto                 : CryptoStructure
    epochStructure         : EpochStructure


    ⦃ DecEq-Ix   ⦄ : DecEq Ix
    ⦃ DecEq-TxId ⦄ : DecEq TxId
  open isHashableSet adHashingScheme renaming (THash to ADHash) public
  open GlobalConstants globalConstants public
  open CryptoStructure crypto public
  open Ledger.Dijkstra.Specification.TokenAlgebra.Base ScriptHash public
  open Ledger.Core.Specification.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public
  open EpochStructure epochStructure public
  open Ledger.Dijkstra.Specification.Script crypto epochStructure public
  field


    scriptStructure        : ScriptStructure


  open ScriptStructure scriptStructure public
  open Ledger.Dijkstra.Specification.PParams crypto epochStructure scriptStructure public
  field


    govParams              : GovParams
    tokenAlgebra           : TokenAlgebra
    txidBytes              : TxId → Ser


  open GovParams govParams public
  open TokenAlgebra tokenAlgebra public


  govStructure : GovStructure
  govStructure = record
    -- TODO: figure out what to do with the hash
    { TxId = TxId; DocHash = ADHash
    ; cryptoStructure = crypto
    ; epochStructure = epochStructure
    ; scriptStructure = scriptStructure
    ; govParams = govParams
    ; globalConstants = globalConstants
    }


  module GovernanceActions = Ledger.Dijkstra.Specification.Gov.Actions govStructure
  open GovernanceActions hiding (Vote; yes; no; abstain) public

  open import Ledger.Dijkstra.Specification.Certs govStructure


  TxIn : Type
  TxIn = TxId × Ix

  TxOut : Type
  TxOut = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe Script

  UTxO : Type
  UTxO = TxIn ⇀ TxOut

  RedeemerPtr : TxLevel → Type
  RedeemerPtr txLevel  = Tag txLevel × Ix

  ProposedPPUpdates : Type
  ProposedPPUpdates = KeyHash ⇀ PParamsUpdate

  Update : Type
  Update = ProposedPPUpdates × Epoch

  record HasUTxO {a} (A : Type a) : Type a where
    field UTxOOf : A → UTxO
  open HasUTxO ⦃...⦄ public


  mutual
    record Tx (txLevel : TxLevel) : Type where
      inductive
      field
        txBody       : TxBody txLevel
        txWitnesses  : TxWitnesses txLevel
        txSize       : ℕ
        isValid      : InTopLevel txLevel Bool
        txAuxData    : Maybe AuxiliaryData

    record TxBody (txLevel : TxLevel) : Type where
      inductive
      field
        txIns                : ℙ TxIn
        referenceInputs      : ℙ TxIn
        collateralInputs     : InTopLevel txLevel (ℙ TxIn)
        txOuts               : Ix ⇀ TxOut
        txId                 : TxId
        txCerts              : List DCert
        txFee                : InTopLevel txLevel Fees
        txWithdrawals        : Withdrawals
        txVldt               : Maybe Slot × Maybe Slot
        txADhash             : Maybe ADHash
        txDonation           : Donations
        txGovVotes           : List GovVote
        txGovProposals       : List GovProposal
        txNetworkId          : Maybe Network
        currentTreasury      : Maybe Coin
        mint                 : Value
        scriptIntegrityHash  : Maybe ScriptHash

        -- New in Dijkstra --
        txSubTransactions         : InTopLevel txLevel (List (Tx TxLevelSub))
        txGuards                  : ℙ Credential
        txRequiredTopLevelGuards  : InSubLevel txLevel (ℙ (Credential × Maybe Datum))
        ---------------------

      requiredSignerHashes : ℙ KeyHash
      requiredSignerHashes = mapPartial isKeyHashObj txGuards


    record TxWitnesses (txLevel : TxLevel) : Type where
      inductive
      field
        vKeySigs     : VKey ⇀ Sig
        scripts      : ℙ Script
        txData       : ℙ Datum
        txRedeemers  : RedeemerPtr txLevel ⇀ Redeemer × ExUnits

      scriptsP1 : ℙ P1Script
      scriptsP1 = mapPartial isInj₁ scripts


  TopLevelTx : Type
  TopLevelTx = Tx TxLevelTop

  SubLevelTx : Type
  SubLevelTx = Tx TxLevelSub


  AnyLevelTx : Type
  AnyLevelTx = TopLevelTx ⊎ SubLevelTx


  -- Level-Dependent Type Classes --
  record HasTxBody {txLevel} {a} (A : Type a) : Type a where
    field TxBodyOf : A → TxBody txLevel
  open HasTxBody  ⦃...⦄ public

  record HasTxWitnesses {txLevel} {a} (A : Type a) : Type a where
    field TxWitnessesOf : A → TxWitnesses txLevel
  open HasTxWitnesses ⦃...⦄ public

  record HasRedeemers {txLevel} {a} (A : Type a) : Type a where
    field RedeemersOf : A → RedeemerPtr txLevel ⇀ Redeemer × ExUnits
  open HasRedeemers ⦃...⦄ public

  -- (top-level only) --
  record HasCollateralInputs {txLevel} {a} (A : Type a) : Type a where
    field CollateralInputsOf : A → InTopLevel txLevel (ℙ TxIn)
  open HasCollateralInputs ⦃...⦄ public

  record HasTxFees {txLevel} {a} (A : Type a) : Type a where
    field TxFeesOf : A → InTopLevel txLevel Fees
  open HasTxFees ⦃...⦄ public

  record HasSubTransactions {txLevel} {a} (A : Type a) : Type a where
    field SubTransactionsOf : A → InTopLevel txLevel (List (Tx TxLevelSub))
  open HasSubTransactions ⦃...⦄ public

  -- (sub-level only) --
  record HasTopLevelGuards {txLevel} {a} (A : Type a) : Type a where
    field TopLevelGuardsOf : A → InSubLevel txLevel (ℙ (Credential × Maybe Datum))
  open HasTopLevelGuards ⦃...⦄ public


  -- Level-Independent Type Classes --
  record HasTxId {a} (A : Type a) : Type a where
    field TxIdOf : A → TxId
  open HasTxId ⦃...⦄ public

  record HasSize {a} (A : Type a) : Type a where
    field SizeOf : A → ℕ
  open HasSize ⦃...⦄ public

  record HasValidInterval {a} (A : Type a) : Type a where
    field ValidIntervalOf : A → Maybe Slot × Maybe Slot
  open HasValidInterval ⦃...⦄ public

  record HasSpendInputs {a} (A : Type a) : Type a where
    field SpendInputsOf : A → ℙ TxIn
  open HasSpendInputs ⦃...⦄ public

  record HasReferenceInputs {a} (A : Type a) : Type a where
    field ReferenceInputsOf : A → ℙ TxIn
  open HasReferenceInputs ⦃...⦄ public

  record HasMintedValue {a} (A : Type a) : Type a where
    field MintedValueOf : A → Value
  open HasMintedValue ⦃...⦄ public

  record HasFees? {a} (A : Type a) : Type a where
    field FeesOf? : A → Maybe Fees
  open HasFees? ⦃...⦄ public

  record HasDCerts {a} (A : Type a) : Type a where
    field DCertsOf : A → List DCert
  open HasDCerts ⦃...⦄ public

  record HasData {a} (A : Type a) : Type a where
    field DataOf : A → ℙ Datum
  open HasData ⦃...⦄ public

  record HasListOfGovProposals {a} (A : Type a) : Type a where
    field ListOfGovProposalsOf : A → List GovProposal
  open HasListOfGovProposals ⦃...⦄ public

  record HasListOfGovVotes {a} (A : Type a) : Type a where
    field ListOfGovVotesOf : A → List GovVote
  open HasListOfGovVotes ⦃...⦄ public

  record HasGuards {a} (A : Type a) : Type a where
    field GuardsOf : A → ℙ Credential
  open HasGuards ⦃...⦄ public

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

  record HasTxOuts {a} (A : Type a) : Type a where
    field TxOutsOf : A → Ix ⇀ TxOut
  open HasTxOuts ⦃...⦄ public

  record HasRequiredSingerHashes {a} (A : Type a) : Type a where
    field RequiredSignerHashesOf : A → ℙ KeyHash
  open HasRequiredSingerHashes ⦃...⦄ public

  record HasCurrentTreasury {a} (A : Type a) : Type a where
    field CurrentTreasuryOf : A → Maybe Coin
  open HasCurrentTreasury ⦃...⦄ public

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

  instance
    HasTxBody-Tx : HasTxBody (Tx txLevel)
    HasTxBody-Tx .TxBodyOf = Tx.txBody

    HasSize-Tx : HasSize (Tx txLevel)
    HasSize-Tx .SizeOf = Tx.txSize

    HasTxWitnesses-Tx : HasTxWitnesses (Tx txLevel)
    HasTxWitnesses-Tx .TxWitnessesOf = Tx.txWitnesses

    HasIsValidFlag-Tx : HasIsValidFlag TopLevelTx
    HasIsValidFlag-Tx .IsValidFlagOf = Tx.isValid

    HasRedeemers-TxWitnesses : HasRedeemers (TxWitnesses txLevel)
    HasRedeemers-TxWitnesses .RedeemersOf = TxWitnesses.txRedeemers
    HasRedeemers-Tx : HasRedeemers (Tx txLevel)
    HasRedeemers-Tx .RedeemersOf = RedeemersOf ∘ TxWitnessesOf

    HasCollateralInputs-TopLevelTx : HasCollateralInputs TopLevelTx
    HasCollateralInputs-TopLevelTx .CollateralInputsOf = TxBody.collateralInputs ∘ TxBodyOf

    HasTxFees-TopLevelTx : HasTxFees TopLevelTx
    HasTxFees-TopLevelTx .TxFeesOf = TxBody.txFee ∘ TxBodyOf

    HasSubTransactions-TopLevelTx : HasSubTransactions TopLevelTx
    HasSubTransactions-TopLevelTx .SubTransactionsOf = TxBody.txSubTransactions ∘ TxBodyOf

    HasTopLevelGuards-SubLevelTx : HasTopLevelGuards SubLevelTx
    HasTopLevelGuards-SubLevelTx .TopLevelGuardsOf = TxBody.txRequiredTopLevelGuards ∘ TxBodyOf

    HasDCerts-TxBody : HasDCerts (TxBody txLevel)
    HasDCerts-TxBody .DCertsOf = TxBody.txCerts
    HasDCerts-Tx : HasDCerts (Tx txLevel)
    HasDCerts-Tx .DCertsOf = DCertsOf ∘ TxBodyOf

    HasWithdrawals-TxBody : HasWithdrawals (TxBody txLevel)
    HasWithdrawals-TxBody .WithdrawalsOf = TxBody.txWithdrawals
    HasWithdrawals-Tx : HasWithdrawals (Tx txLevel)
    HasWithdrawals-Tx .WithdrawalsOf = WithdrawalsOf ∘ TxBodyOf

    HasValidInterval-TxBody : HasValidInterval (TxBody txLevel)
    HasValidInterval-TxBody .ValidIntervalOf = TxBody.txVldt
    HasValidInterval-Tx : HasValidInterval (Tx txLevel)
    HasValidInterval-Tx .ValidIntervalOf = ValidIntervalOf ∘ TxBodyOf

    HasSpendInputs-TxBody : HasSpendInputs (TxBody txLevel)
    HasSpendInputs-TxBody .SpendInputsOf = TxBody.txIns
    HasSpendInputs-Tx : HasSpendInputs (Tx txLevel)
    HasSpendInputs-Tx .SpendInputsOf = SpendInputsOf ∘ TxBodyOf

    HasReferenceInputs-TxBody : HasReferenceInputs (TxBody txLevel)
    HasReferenceInputs-TxBody .ReferenceInputsOf = TxBody.referenceInputs
    HasReferenceInputs-Tx : HasReferenceInputs (Tx txLevel)
    HasReferenceInputs-Tx .ReferenceInputsOf = ReferenceInputsOf ∘ TxBodyOf

    HasMintedValue-TxBody : HasMintedValue (TxBody txLevel)
    HasMintedValue-TxBody .MintedValueOf = TxBody.mint
    HasMintedValue-Tx : HasMintedValue (Tx txLevel)
    HasMintedValue-Tx .MintedValueOf = MintedValueOf ∘ TxBodyOf

    HasListOfGovVotes-TxBody : HasListOfGovVotes (TxBody txLevel)
    HasListOfGovVotes-TxBody .ListOfGovVotesOf = TxBody.txGovVotes
    HasListOfGovVotes-Tx : HasListOfGovVotes (Tx txLevel)
    HasListOfGovVotes-Tx .ListOfGovVotesOf = ListOfGovVotesOf ∘ TxBodyOf

    HasListOfGovProposals-TxBody : HasListOfGovProposals (TxBody txLevel)
    HasListOfGovProposals-TxBody .ListOfGovProposalsOf = TxBody.txGovProposals
    HasListOfGovProposals-Tx : HasListOfGovProposals (Tx txLevel)
    HasListOfGovProposals-Tx .ListOfGovProposalsOf = ListOfGovProposalsOf ∘ TxBodyOf

    HasMaybeNetworkId-TxBody : HasMaybeNetworkId (TxBody txLevel)
    HasMaybeNetworkId-TxBody .MaybeNetworkIdOf = TxBody.txNetworkId
    HasMaybeNetworkId-Tx : HasMaybeNetworkId (Tx txLevel)
    HasMaybeNetworkId-Tx .MaybeNetworkIdOf = MaybeNetworkIdOf ∘ TxBodyOf

    HasFees?-TxBody : {ℓ : TxLevel} → HasFees? (TxBody ℓ)
    HasFees?-TxBody {TxLevelTop} .FeesOf? tbTop = just (TxBody.txFee tbTop)
    HasFees?-TxBody {TxLevelSub} .FeesOf? tbSub = nothing
    HasFees?-Tx : HasFees? (Tx txLevel)
    HasFees?-Tx .FeesOf? = FeesOf? ∘ TxBodyOf

    HasTxId-TxBody : HasTxId (TxBody txLevel)
    HasTxId-TxBody .TxIdOf = TxBody.txId
    HasTxId-Tx : HasTxId (Tx txLevel)
    HasTxId-Tx .TxIdOf = TxIdOf ∘ TxBodyOf

    HasDonations-TxBody : HasDonations (TxBody txLevel)
    HasDonations-TxBody .DonationsOf = TxBody.txDonation
    HasDonations-Tx : HasDonations (Tx txLevel)
    HasDonations-Tx .DonationsOf = DonationsOf ∘ TxBodyOf

    HasCoin-TxOut : HasCoin TxOut
    HasCoin-TxOut .getCoin = coin ∘ proj₁ ∘ proj₂

    HasData-TxWitnesses : HasData (TxWitnesses txLevel)
    HasData-TxWitnesses .DataOf = TxWitnesses.txData
    HasData-Tx : HasData (Tx txLevel)
    HasData-Tx .DataOf = DataOf ∘ TxWitnessesOf

    HasGuards-TxBody : HasGuards (TxBody txLevel)
    HasGuards-TxBody .GuardsOf = TxBody.txGuards
    HasGuards-Tx : HasGuards (Tx txLevel)
    HasGuards-Tx .GuardsOf = GuardsOf ∘ TxBodyOf

    HasScripts-TxWitnesses : HasScripts (TxWitnesses txLevel)
    HasScripts-TxWitnesses .ScriptsOf = TxWitnesses.scripts
    HasScripts-Tx : HasScripts (Tx txLevel)
    HasScripts-Tx .ScriptsOf = ScriptsOf ∘ TxWitnessesOf

    HasTxOuts-TxBody : HasTxOuts (TxBody txLevel)
    HasTxOuts-TxBody .TxOutsOf = TxBody.txOuts
    HasTxOuts-Tx : HasTxOuts (Tx txLevel)
    HasTxOuts-Tx .TxOutsOf = TxOutsOf ∘ TxBodyOf

    HasRequiredSingerHashes-TxBody : HasRequiredSingerHashes (TxBody txLevel)
    HasRequiredSingerHashes-TxBody .RequiredSignerHashesOf = TxBody.requiredSignerHashes
    HasRequiredSingerHashes-Tx : HasRequiredSingerHashes (Tx txLevel)
    HasRequiredSingerHashes-Tx .RequiredSignerHashesOf = RequiredSignerHashesOf ∘ TxBodyOf

    HasCurrentTreasury-TxBody : HasCurrentTreasury (TxBody txLevel)
    HasCurrentTreasury-TxBody .CurrentTreasuryOf = TxBody.currentTreasury
    HasCurrentTreasury-Tx : HasCurrentTreasury (Tx txLevel)
    HasCurrentTreasury-Tx .CurrentTreasuryOf = CurrentTreasuryOf ∘ TxBodyOf


  -- Helpers --
  --| extract scripts from TxOuts
  txOutToScript : TxOut → Maybe Script
  txOutToScript (_ , _ , _ , s) = s
  --| extract datum from TxOuts
  txOutToDatum : TxOut → Maybe Datum
  txOutToDatum (_ , _ , d , _) = d >>= isInj₁
  --| extract value from TxOuts
  txOutToValue : TxOut → Value
  txOutToValue (_ , v , _ , _) = v
  --| extract set of values from a UTxO
  valuesOfUTxO : UTxO → ℙ Value
  valuesOfUTxO = mapˢ txOutToValue ∘ range

  --| Spending inputs
  allSpendInputs : TopLevelTx → ℙ TxIn
  allSpendInputs txTop = foldl  (λ acc txSub → acc ∪ SpendInputsOf txSub)
                                (SpendInputsOf txTop)
                                (SubTransactionsOf txTop)
  allSpendInputsList : TopLevelTx → List (ℙ TxIn)
  allSpendInputsList t = SpendInputsOf t ∷ map SpendInputsOf (SubTransactionsOf t)

  --| Reference inputs
  allReferenceInputs : TopLevelTx → ℙ TxIn
  allReferenceInputs txTop = foldl  (λ acc txSub → acc ∪ ReferenceInputsOf txSub)
                                    (ReferenceInputsOf txTop)
                                    (SubTransactionsOf txTop)

  --| OUTPUTS -------------------------------------------------------------------
  --|
  --| Sets of TxOuts can come from the range of...
  --|
  --| ...a UTxO
  _ : UTxO → ℙ TxOut
  _ = range
  --|
  --| ...the txOuts field of a transaction
  _ : Tx txLevel → ℙ TxOut
  _ = range ∘ TxOutsOf

  --| TxOuts from .a UTxO restricted to spending inputs of a Tx
  spendTxOuts : Tx txLevel → UTxO → ℙ TxOut
  spendTxOuts tx utxo = range (utxo ∣ SpendInputsOf tx)

  --| TxOuts from .a UTxO restricted to reference inputs of a Tx
  referencedTxOuts : Tx txLevel → UTxO → ℙ TxOut
  referencedTxOuts tx utxo = range (utxo ∣ ReferenceInputsOf tx)

  --| Set of scripts from outputs of a UTxO
  scriptsOfUTxO : UTxO → ℙ Script
  scriptsOfUTxO = mapPartial txOutToScript ∘ range

  --| Set of scripts from outputs of a Tx
  scriptsOfTx : Tx txLevel → ℙ Script
  scriptsOfTx = mapPartial txOutToScript ∘ range ∘ TxOutsOf

  --| Set of scripts from the spending inputs of a Tx
  spendScripts : Tx txLevel → UTxO → ℙ Script
  spendScripts = mapPartial txOutToScript ∘₂ spendTxOuts

  --| Set of scripts from reference inputs
  referenceScripts : Tx txLevel → UTxO → ℙ Script
  referenceScripts = mapPartial txOutToScript ∘₂ referencedTxOuts

  --| Set of scripts from reference inputs in a batch
  allReferenceScripts : TopLevelTx → UTxO → ℙ Script
  allReferenceScripts tx utxo =
    foldl (λ acc t → acc ∪ referenceScripts t utxo)
          (referenceScripts tx utxo) (SubTransactionsOf tx)

  --| Set of scripts from a transactions's witness field
  witnessScripts : Tx txLevel → ℙ Script
  witnessScripts = ScriptsOf

  --| Set of all scripts from a transaction
  getTxScripts : Tx txLevel → UTxO → ℙ Script
  getTxScripts tx utxo =  scriptsOfTx tx
                          ∪ spendScripts tx utxo
                          ∪ referenceScripts tx utxo
                          ∪ witnessScripts tx

  --| Set of scripts from a batch
  getAllScripts : TopLevelTx → UTxO →  ℙ Script
  getAllScripts txTop utxo = foldl  (λ acc txSub → acc ∪ getTxScripts txSub utxo)
                                    (getTxScripts txTop utxo)
                                    (SubTransactionsOf txTop)

  --| Set of datum from a transaction
  dataOfTx : Tx txLevel → ℙ Datum
  dataOfTx = mapPartial txOutToDatum ∘ range ∘ TxOutsOf

  --| Set of data from a UTxO
  txOutDataOfUTxO : UTxO → ℙ Datum
  txOutDataOfUTxO = mapPartial txOutToDatum ∘ range

  --| Set of data from spendTxOuts
  spendData : Tx txLevel → UTxO → ℙ Datum
  spendData = mapPartial txOutToDatum ∘₂ spendTxOuts

  --| Set of data from referencedTxOuts
  referenceData : Tx txLevel → UTxO → ℙ Datum
  referenceData = mapPartial txOutToDatum ∘₂ referencedTxOuts

  --| Set of data from a transaction's witness field
  witnessData : Tx txLevel → ℙ Datum
  witnessData = DataOf

  --| Set of data from a transaction
  getTxData : Tx txLevel → UTxO → ℙ Datum
  getTxData tx utxo =  dataOfTx tx
                       ∪ spendData tx utxo
                       ∪ referenceData tx utxo
                       ∪ witnessData tx

  --| Set of data from a batch
  getAllData : TopLevelTx → UTxO → ℙ Datum
  getAllData txTop utxo = foldl  (λ acc txSub → acc ∪ getTxData txSub utxo)
                                 (getTxData txTop utxo)
                                 (SubTransactionsOf txTop)

  NoOverlappingSpendInputs : TopLevelTx → Type
  NoOverlappingSpendInputs topTx =
    List.AllPairs disjoint (SpendInputsOf topTx ∷ map SpendInputsOf (SubTransactionsOf topTx))

  -- Total Ada minted across the entire batch (top-level tx + all sub-txs).
  allMintedCoin : TopLevelTx → Coin
  allMintedCoin txTop = foldl (λ acc txSub → acc + coin (MintedValueOf txSub))
                              (coin (MintedValueOf txTop))
                              (SubTransactionsOf txTop)
  -- To maintain total Ada supply invariant, this must satisfy `allMintedCoin ≡ 0`;
  -- this is a generalization of Conway's `coin mint ≡ 0`.

  lookupScriptHash : ScriptHash → Tx txLevel → UTxO → Maybe Script
  lookupScriptHash sh tx utxo = lookupHash sh (getTxScripts tx utxo)


  TaggedTopLevelGuard : Type
  TaggedTopLevelGuard = TxId × Credential × Maybe Datum
                     -- (subTxId, guard credential, optional datum argument)

  GroupedTopLevelGuards : Type
  GroupedTopLevelGuards = List (Credential × List (TxId × Maybe Datum))

  groupTopLevelGuards : List TaggedTopLevelGuard → GroupedTopLevelGuards
  groupTopLevelGuards = foldr insertGuard []
    where
    -- Insert one tagged guard into an existing group:
    --   + if the credential already has a group, cons (subTxId, datum?) onto its list
    --   + otherwise create a new group for that credential.
    insertGuard : TaggedTopLevelGuard → GroupedTopLevelGuards → GroupedTopLevelGuards
    insertGuard (tid , cred , md) [] = (cred , (tid , md) ∷ []) ∷ []
    insertGuard (tid , cred , md) ((c , xs) ∷ rest) with c ≟ cred
    ... | yes _ = (c , (tid , md) ∷ xs) ∷ rest
    ... | no  _ = (c , xs) ∷ insertGuard (tid , cred , md) rest

  subTxTaggedGuards : SubLevelTx → ℙ TaggedTopLevelGuard
  subTxTaggedGuards subtx =
    mapˢ (λ (cred , md) → (TxIdOf subtx , cred , md)) (TopLevelGuardsOf subtx)

  -- Turn a subTx body's `txRequiredTopLevelGuards` into a set of guard credentials.
  subTxGuardCredentials : SubLevelTx → ℙ Credential
  subTxGuardCredentials = (mapˢ proj₁) ∘ TopLevelGuardsOf

  -- Phase-1 condition (CIP-0118):
  -- every credential required by a subTx body must appear in the top-level txGuards set.
  requiredGuardsInTopLevel : TopLevelTx → List SubLevelTx → Type
  requiredGuardsInTopLevel topTx subTxs = requiredCreds ⊆ GuardsOf topTx
    where
    -- union a list of sets
    concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B
    concatMapˡ f as = proj₁ $ unions (fromList (map f as))
    -- maybe move this to agda-sets or src-lib-exts

    requiredCreds : ℙ Credential
    requiredCreds = concatMapˡ subTxGuardCredentials subTxs