{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Conway.Specification.Transaction

module Ledger.Conway.Specification.Abstract (txs : TransactionStructure) where

open TransactionStructure txs
open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Script.ScriptPurpose txs


record indexOf : Type where
  field
    indexOfDCert          : DCert          → List DCert        → Maybe Ix
    indexOfRewardAddress  : RewardAddress  → Withdrawals       → Maybe Ix
    indexOfTxIn           : TxIn           → ℙ TxIn            → Maybe Ix
    indexOfPolicyId       : ScriptHash     → ℙ ScriptHash      → Maybe Ix
    indexOfVote           : GovVoter       → List GovVoter     → Maybe Ix
    indexOfProposal       : GovProposal    → List GovProposal  → Maybe Ix

ValidityInterval = Maybe Slot × Maybe Slot


record AbstractFunctions : Type₁ where
  field UTCTime      : Type
        ⦃ DecEq-UTCTime ⦄ : DecEq UTCTime
        txscriptfee  : Prices → ExUnits → Coin
        serSize      : Value → MemoryEstimate
        indexOfImp   : indexOf
        runPLCScript : CostModel → P2Script → ExUnits → List Data → Bool
        scriptSize   : Script → ℕ
        valContext   : TxInfo → ScriptPurpose → Data
        getLanguageView : PParams → Language → LangDepView
        epochInfoSlotToUTCTime : Slot → Maybe UTCTime

        -- Translates a ValidityInterval, which is expressed in slots, to a
        -- POSIXTimeRange, expressed in terms of POSIXTime.
        transVITime : ValidityInterval → POSIXTimeRange