{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Transaction

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

open import Ledger.Prelude
open TransactionStructure txs
open import Ledger.Dijkstra.Specification.Certs govStructure
open import Ledger.Dijkstra.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
    indexOfGuard          : Credential     → List Credential   → Maybe Ix

record AbstractFunctions : Type where
  field txScriptFee     : Prices → ExUnits → Fees
        serializedSize  : Value → MemoryEstimate
        indexOfImp      : indexOf
        runPLCScript    : CostModel → P2Script → ExUnits → List Data → Bool
        scriptSize      : Script → ℕ
        valContext      : TxInfo → ScriptPurpose → Data