{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
  committeeCredentialToStrictMaybe,
  SpecTranslate (..),
  SpecTranslationError,
  ConwayExecEnactEnv (..),
  DepositPurpose (..),
) where

import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..))
import Cardano.Crypto.Hash (Hash)
import Cardano.Crypto.Util (bytesToNatural)
import Cardano.Ledger.Address (Addr (..), BootstrapAddress (..), RewardAccount (..))
import Cardano.Ledger.Allegra.Scripts (
  Timelock,
  pattern RequireTimeExpire,
  pattern RequireTimeStart,
 )
import Cardano.Ledger.Alonzo (AlonzoTxAuxData, MaryValue)
import Cardano.Ledger.Alonzo.PParams (OrdExUnits (OrdExUnits))
import Cardano.Ledger.Alonzo.Scripts (AlonzoPlutusPurpose (..))
import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..), IsValid (..))
import Cardano.Ledger.Alonzo.TxAuxData (AuxiliaryDataHash)
import Cardano.Ledger.Alonzo.TxWits (AlonzoTxWits (..), Redeemers (..), TxDats (..))
import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..))
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Binary (DecShareCBOR (..), Interns, Sized (..))
import Cardano.Ledger.CertState (CommitteeAuthorization (..), CommitteeState (..))
import Cardano.Ledger.Coin (Coin (..), CompactForm)
import Cardano.Ledger.Compactible (Compactible)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.PParams (ConwayPParams (..), THKD (..))
import Cardano.Ledger.Conway.Rules (
  ConwayCertPredFailure,
  ConwayGovPredFailure,
  ConwayUtxoPredFailure,
  EnactSignal (..),
  maxRefScriptSizePerBlock,
  maxRefScriptSizePerTx,
 )
import Cardano.Ledger.Conway.Scripts (AlonzoScript (..), ConwayPlutusPurpose (..))
import Cardano.Ledger.Conway.Tx (refScriptCostMultiplier, refScriptCostStride)
import Cardano.Ledger.Conway.TxBody (ConwayTxBody)
import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
import Cardano.Ledger.Credential (Credential (..), StakeReference (..))
import Cardano.Ledger.Crypto (Crypto (..))
import Cardano.Ledger.DRep (DRep (..), DRepState (..))
import Cardano.Ledger.HKD (HKD)
import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..), VKey (..))
import Cardano.Ledger.Keys.WitVKey (WitVKey (..))
import Cardano.Ledger.Plutus (CostModels, ExUnits (..), Prices)
import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData)
import Cardano.Ledger.PoolDistr (IndividualPoolStake (..), PoolDistr (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.SafeHash (SafeHash, extractHash)
import Cardano.Ledger.Shelley.LedgerState
import Cardano.Ledger.Shelley.Rules (Identity, UtxoEnv (..))
import Cardano.Ledger.Shelley.Scripts (
  pattern RequireAllOf,
  pattern RequireAnyOf,
  pattern RequireMOf,
  pattern RequireSignature,
 )
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
import Cardano.Ledger.UMap (fromCompact)
import Cardano.Ledger.UTxO (UTxO (..))
import Cardano.Ledger.Val (Val (..))
import Constrained (HasSimpleRep, HasSpec)
import Control.DeepSeq (NFData)
import Control.Monad.Except (MonadError (..))
import Control.State.Transition.Extended (STS (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Bitraversable (bimapM)
import Data.Data (Typeable)
import Data.Default.Class (Default (..))
import Data.Foldable (Foldable (..))
import Data.List (sortOn)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.OMap.Strict (OMap)
import qualified Data.OMap.Strict as OMap
import Data.OSet.Strict (OSet)
import Data.Sequence (Seq)
import Data.Sequence.Strict (StrictSeq)
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Traversable (forM)
import Data.Void (Void, absurd)
import Data.Word (Word16, Word32, Word64)
import qualified GHC.Exts as Exts
import GHC.Generics (Generic)
import Lens.Micro
import Lens.Micro.Extras (view)
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance (
  OpaqueErrorString (..),
  SpecTransM,
  SpecTranslate (..),
  SpecTranslationError,
  askCtx,
  hashToInteger,
  withCtx,
 )
import Test.Cardano.Ledger.Constrained.Conway (DepositPurpose (..), IsConwayUniv)
import Test.Cardano.Ledger.Constrained.Conway.Epoch
import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..), showExpr)

instance SpecTranslate ctx Void where
  type SpecRep Void = Void

  toSpecRep :: Void -> SpecTransM ctx (SpecRep Void)
toSpecRep = forall a. Void -> a
absurd

instance SpecTranslate ctx a => SpecTranslate ctx [a] where
  type SpecRep [a] = [SpecRep a]

  toSpecRep :: [a] -> SpecTransM ctx (SpecRep [a])
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep

instance SpecTranslate ctx TxIx where
  type SpecRep TxIx = Integer

  toSpecRep :: TxIx -> SpecTransM ctx (SpecRep TxIx)
toSpecRep (TxIx Word64
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger Word64
x

instance SpecTranslate ctx (TxIn era) where
  type SpecRep (TxIn era) = Agda.TxIn

  toSpecRep :: TxIn era -> SpecTransM ctx (SpecRep (TxIn era))
toSpecRep (TxIn TxId era
txId TxIx
txIx) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxId era
txId, TxIx
txIx)

instance SpecTranslate ctx (StakeReference era) where
  type SpecRep (StakeReference era) = Agda.Credential

  toSpecRep :: StakeReference era -> SpecTransM ctx (SpecRep (StakeReference era))
toSpecRep (StakeRefBase StakeCredential era
c) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeCredential era
c
  toSpecRep (StakeRefPtr Ptr
_) = forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot translate StakeRefPtr"
  toSpecRep StakeReference era
StakeRefNull = forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot translate StakeRefNull"

instance SpecTranslate ctx (BootstrapAddress era) where
  type SpecRep (BootstrapAddress era) = Agda.BootstrapAddr

  toSpecRep :: BootstrapAddress era
-> SpecTransM ctx (SpecRep (BootstrapAddress era))
toSpecRep BootstrapAddress era
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot translate bootstrap addresses"

instance SpecTranslate ctx (Addr era) where
  type SpecRep (Addr era) = Agda.Addr

  toSpecRep :: Addr era -> SpecTransM ctx (SpecRep (Addr era))
toSpecRep (Addr Network
nw PaymentCredential era
pc StakeReference era
sr) =
    forall a b. a -> Either a b
Left
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (() -> Credential -> Credential -> BaseAddr
Agda.BaseAddr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
nw forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PaymentCredential era
pc forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StakeReference era
sr)
  toSpecRep (AddrBootstrap BootstrapAddress era
ba) = forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep BootstrapAddress era
ba

instance SpecTranslate ctx (Hash a b) where
  type SpecRep (Hash a b) = Integer

  toSpecRep :: Hash a b -> SpecTransM ctx (SpecRep (Hash a b))
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Hash a b -> Integer
hashToInteger

instance SpecTranslate ctx (SafeHash c EraIndependentData) where
  type SpecRep (SafeHash c EraIndependentData) = Agda.DataHash

  toSpecRep :: SafeHash c EraIndependentData
-> SpecTransM ctx (SpecRep (SafeHash c EraIndependentData))
toSpecRep SafeHash c EraIndependentData
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance SpecTranslate ctx (SafeHash c EraIndependentTxBody) where
  type SpecRep (SafeHash c EraIndependentTxBody) = Integer

  toSpecRep :: SafeHash c EraIndependentTxBody
-> SpecTransM ctx (SpecRep (SafeHash c EraIndependentTxBody))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c i. SafeHash c i -> Hash (HASH c) i
extractHash

instance SpecTranslate ctx (SafeHash c EraIndependentScriptIntegrity) where
  type SpecRep (SafeHash c EraIndependentScriptIntegrity) = Integer

  toSpecRep :: SafeHash c EraIndependentScriptIntegrity
-> SpecTransM
     ctx (SpecRep (SafeHash c EraIndependentScriptIntegrity))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c i. SafeHash c i -> Hash (HASH c) i
extractHash

instance SpecTranslate ctx (SafeHash c AnchorData) where
  type SpecRep (SafeHash c AnchorData) = Agda.DataHash

  toSpecRep :: SafeHash c AnchorData
-> SpecTransM ctx (SpecRep (SafeHash c AnchorData))
toSpecRep SafeHash c AnchorData
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance
  ( SpecRep (DataHash (EraCrypto era)) ~ Agda.DataHash
  , Era era
  ) =>
  SpecTranslate ctx (BinaryData era)
  where
  type SpecRep (BinaryData era) = Agda.DataHash

  toSpecRep :: BinaryData era -> SpecTransM ctx (SpecRep (BinaryData era))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Era era => BinaryData era -> DataHash (EraCrypto era)
hashBinaryData

instance Era era => SpecTranslate ctx (Datum era) where
  type SpecRep (Datum era) = Maybe (Either Agda.Datum Agda.DataHash)

  toSpecRep :: Datum era -> SpecTransM ctx (SpecRep (Datum era))
toSpecRep Datum era
NoDatum = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
  toSpecRep (Datum BinaryData era
d) = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep BinaryData era
d
  toSpecRep (DatumHash DataHash (EraCrypto era)
h) = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DataHash (EraCrypto era)
h

instance
  ( AlonzoEraScript era
  , NativeScript era ~ Timelock era
  , Script era ~ AlonzoScript era
  ) =>
  SpecTranslate ctx (Timelock era)
  where
  type SpecRep (Timelock era) = Agda.HashedTimelock

  toSpecRep :: Timelock era -> SpecTransM ctx (SpecRep (Timelock era))
toSpecRep Timelock era
tl =
    Timelock -> Integer -> HashedTimelock
Agda.HashedTimelock
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {era} {ctx}.
AllegraEraScript era =>
NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep Timelock era
tl
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era.
EraScript era =>
Script era -> ScriptHash (EraCrypto era)
hashScript @era forall a b. (a -> b) -> a -> b
$ forall era. Timelock era -> AlonzoScript era
TimelockScript Timelock era
tl)
    where
      timelockToSpecRep :: NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep NativeScript era
x =
        case NativeScript era
x of
          RequireSignature KeyHash 'Witness (EraCrypto era)
kh ->
            Integer -> Timelock
Agda.RequireSig forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash 'Witness (EraCrypto era)
kh
          RequireAllOf StrictSeq (NativeScript era)
ss -> do
            StrictSeq Timelock
tls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Timelock] -> Timelock
Agda.RequireAllOf forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
          RequireAnyOf StrictSeq (NativeScript era)
ss -> do
            StrictSeq Timelock
tls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Timelock] -> Timelock
Agda.RequireAnyOf forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
          RequireMOf Int
m StrictSeq (NativeScript era)
ss -> do
            StrictSeq Timelock
tls <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse NativeScript era -> SpecTransM ctx Timelock
timelockToSpecRep StrictSeq (NativeScript era)
ss
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> [Timelock] -> Timelock
Agda.RequireMOf (forall a. Integral a => a -> Integer
toInteger Int
m) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq Timelock
tls
          RequireTimeExpire SlotNo
slot -> Integer -> Timelock
Agda.RequireTimeExpire forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
slot
          RequireTimeStart SlotNo
slot -> Integer -> Timelock
Agda.RequireTimeStart forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SlotNo
slot

instance
  ( AlonzoEraScript era
  , NativeScript era ~ Timelock era
  , Script era ~ AlonzoScript era
  ) =>
  SpecTranslate ctx (PlutusScript era)
  where
  type SpecRep (PlutusScript era) = Agda.ScriptHash

  toSpecRep :: PlutusScript era -> SpecTransM ctx (SpecRep (PlutusScript era))
toSpecRep PlutusScript era
ps = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraScript era =>
Script era -> ScriptHash (EraCrypto era)
hashScript forall a b. (a -> b) -> a -> b
$ forall era. PlutusScript era -> AlonzoScript era
PlutusScript @era PlutusScript era
ps

instance
  ( AlonzoEraScript era
  , Script era ~ AlonzoScript era
  , NativeScript era ~ Timelock era
  ) =>
  SpecTranslate ctx (AlonzoScript era)
  where
  type SpecRep (AlonzoScript era) = Agda.Script

  toSpecRep :: AlonzoScript era -> SpecTransM ctx (SpecRep (AlonzoScript era))
toSpecRep (TimelockScript Timelock era
s) = forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Timelock era
s
  toSpecRep (PlutusScript PlutusScript era
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right ()

instance
  ( EraTxOut era
  , SpecRep (Value era) ~ Agda.Coin
  , Script era ~ AlonzoScript era
  , SpecTranslate ctx (Value era)
  , SpecTranslate ctx (Script era)
  ) =>
  SpecTranslate ctx (BabbageTxOut era)
  where
  type SpecRep (BabbageTxOut era) = Agda.TxOut

  toSpecRep :: BabbageTxOut era -> SpecTransM ctx (SpecRep (BabbageTxOut era))
toSpecRep (BabbageTxOut Addr (EraCrypto era)
addr Value era
val Datum era
datum StrictMaybe (Script era)
script) = do
    Either BaseAddr BootstrapAddr
addr' <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Addr (EraCrypto era)
addr
    Integer
val' <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Value era
val
    Maybe (Either () ())
datum' <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Datum era
datum
    Maybe (Either HashedTimelock ())
script' <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe (Script era)
script
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either BaseAddr BootstrapAddr
addr', (Integer
val', (Maybe (Either () ())
datum', Maybe (Either HashedTimelock ())
script')))

instance SpecTranslate ctx Integer where
  type SpecRep Integer = Integer

  toSpecRep :: Integer -> SpecTransM ctx (SpecRep Integer)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure

deriving instance SpecTranslate ctx Coin

instance
  ( SpecTranslate ctx (TxOut era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  ) =>
  SpecTranslate ctx (UTxO era)
  where
  type SpecRep (UTxO era) = SpecRep (Map (TxIn (EraCrypto era)) (TxOut era))
  toSpecRep :: UTxO era -> SpecTransM ctx (SpecRep (UTxO era))
toSpecRep (UTxO Map (TxIn (EraCrypto era)) (TxOut era)
m) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (TxIn (EraCrypto era)) (TxOut era)
m

instance
  ( SpecTranslate ctx (TxOut era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  , GovState era ~ ConwayGovState era
  ) =>
  SpecTranslate ctx (UTxOState era)
  where
  type SpecRep (UTxOState era) = Agda.UTxOState

  toSpecRep :: UTxOState era -> SpecTransM ctx (SpecRep (UTxOState era))
toSpecRep UTxOState {GovState era
Coin
UTxO era
IncrementalStake (EraCrypto era)
utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosDeposited :: forall era. UTxOState era -> Coin
utxosFees :: forall era. UTxOState era -> Coin
utxosGovState :: forall era. UTxOState era -> GovState era
utxosStakeDistr :: forall era. UTxOState era -> IncrementalStake (EraCrypto era)
utxosDonation :: forall era. UTxOState era -> Coin
utxosDonation :: Coin
utxosStakeDistr :: IncrementalStake (EraCrypto era)
utxosGovState :: GovState era
utxosFees :: Coin
utxosDeposited :: Coin
utxosUtxo :: UTxO era
..} = do
    let
      gasDeposits :: Map (DepositPurpose (EraCrypto era)) Coin
gasDeposits =
        forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall c. GovActionId c -> DepositPurpose c
GovActionDeposit forall era. GovActionState era -> Coin
gasDeposit) forall a b. (a -> b) -> a -> b
$
          forall k v. Ord k => OMap k v -> [(k, v)]
OMap.assocList (GovState era
utxosGovState forall s a. s -> Getting a s a -> a
^. forall era. Lens' (ConwayGovState era) (Proposals era)
cgsProposalsL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
Lens'
  (Proposals era)
  (OMap (GovActionId (EraCrypto era)) (GovActionState era))
pPropsL)
    HSMap (Integer, Integer) TxOut
-> Integer -> HSMap DepositPurpose Integer -> Integer -> UTxOState
Agda.MkUTxOState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UTxO era
utxosUtxo
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
utxosFees
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (DepositPurpose (EraCrypto era)) Coin
gasDeposits
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
utxosDonation

deriving instance SpecTranslate ctx SlotNo

deriving instance SpecTranslate ctx EpochNo

deriving instance SpecTranslate ctx EpochInterval

instance SpecTranslate ctx ProtVer where
  type SpecRep ProtVer = (Integer, Integer)

  toSpecRep :: ProtVer -> SpecTransM ctx (SpecRep ProtVer)
toSpecRep (ProtVer Version
ver Natural
minor) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall i. Integral i => Version -> i
getVersion Version
ver, forall a. Integral a => a -> Integer
toInteger Natural
minor)

instance SpecTranslate ctx CostModels where
  type SpecRep CostModels = ()

  toSpecRep :: CostModels -> SpecTransM ctx (SpecRep CostModels)
toSpecRep CostModels
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance SpecTranslate ctx Prices where
  type SpecRep Prices = ()

  toSpecRep :: Prices -> SpecTransM ctx (SpecRep Prices)
toSpecRep Prices
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance SpecTranslate ctx ExUnits where
  type SpecRep ExUnits = Agda.ExUnits

  toSpecRep :: ExUnits -> SpecTransM ctx (SpecRep ExUnits)
toSpecRep (ExUnits Natural
a Natural
b) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Integral a => a -> Integer
toInteger Natural
a, forall a. Integral a => a -> Integer
toInteger Natural
b)

deriving instance SpecTranslate ctx OrdExUnits

deriving instance SpecTranslate ctx CoinPerByte

instance
  SpecTranslate ctx (HKD f a) =>
  SpecTranslate ctx (THKD r f a)
  where
  type SpecRep (THKD r f a) = SpecRep (HKD f a)

  toSpecRep :: THKD r f a -> SpecTransM ctx (SpecRep (THKD r f a))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD

instance SpecTranslate ctx DRepVotingThresholds where
  type SpecRep DRepVotingThresholds = Agda.DrepThresholds

  toSpecRep :: DRepVotingThresholds
-> SpecTransM ctx (SpecRep DRepVotingThresholds)
toSpecRep DRepVotingThresholds {UnitInterval
dvtMotionNoConfidence :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNormal :: DRepVotingThresholds -> UnitInterval
dvtCommitteeNoConfidence :: DRepVotingThresholds -> UnitInterval
dvtUpdateToConstitution :: DRepVotingThresholds -> UnitInterval
dvtHardForkInitiation :: DRepVotingThresholds -> UnitInterval
dvtPPNetworkGroup :: DRepVotingThresholds -> UnitInterval
dvtPPEconomicGroup :: DRepVotingThresholds -> UnitInterval
dvtPPTechnicalGroup :: DRepVotingThresholds -> UnitInterval
dvtPPGovGroup :: DRepVotingThresholds -> UnitInterval
dvtTreasuryWithdrawal :: DRepVotingThresholds -> UnitInterval
dvtTreasuryWithdrawal :: UnitInterval
dvtPPGovGroup :: UnitInterval
dvtPPTechnicalGroup :: UnitInterval
dvtPPEconomicGroup :: UnitInterval
dvtPPNetworkGroup :: UnitInterval
dvtHardForkInitiation :: UnitInterval
dvtUpdateToConstitution :: UnitInterval
dvtCommitteeNoConfidence :: UnitInterval
dvtCommitteeNormal :: UnitInterval
dvtMotionNoConfidence :: UnitInterval
..} =
    Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> Rational
-> DrepThresholds
Agda.MkDrepThresholds
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtMotionNoConfidence
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtCommitteeNormal
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtCommitteeNoConfidence
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtUpdateToConstitution
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtHardForkInitiation
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPNetworkGroup
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPEconomicGroup
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPTechnicalGroup
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtPPGovGroup
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
dvtTreasuryWithdrawal

instance SpecTranslate ctx PoolVotingThresholds where
  type SpecRep PoolVotingThresholds = Agda.PoolThresholds

  toSpecRep :: PoolVotingThresholds
-> SpecTransM ctx (SpecRep PoolVotingThresholds)
toSpecRep PoolVotingThresholds {UnitInterval
pvtMotionNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNormal :: PoolVotingThresholds -> UnitInterval
pvtCommitteeNoConfidence :: PoolVotingThresholds -> UnitInterval
pvtHardForkInitiation :: PoolVotingThresholds -> UnitInterval
pvtPPSecurityGroup :: PoolVotingThresholds -> UnitInterval
pvtPPSecurityGroup :: UnitInterval
pvtHardForkInitiation :: UnitInterval
pvtCommitteeNoConfidence :: UnitInterval
pvtCommitteeNormal :: UnitInterval
pvtMotionNoConfidence :: UnitInterval
..} =
    Rational
-> Rational -> Rational -> Rational -> Rational -> PoolThresholds
Agda.MkPoolThresholds
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtMotionNoConfidence
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtCommitteeNormal
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtCommitteeNoConfidence
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtHardForkInitiation
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
pvtPPSecurityGroup

instance SpecTranslate ctx (ConwayPParams Identity era) where
  type SpecRep (ConwayPParams Identity era) = Agda.PParams

  toSpecRep :: ConwayPParams Identity era
-> SpecTransM ctx (SpecRep (ConwayPParams Identity era))
toSpecRep ConwayPParams {THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
HKDNoUpdate Identity ProtVer
cppMinFeeA :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMinFeeB :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f Coin
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Coin
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
cppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
cppDRepActivity :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppDRepDeposit :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
cppGovActionDeposit :: THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
cppGovActionLifetime :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppCommitteeMaxTermLength :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
cppDRepVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
cppPoolVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
cppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
cppCollateralPercentage :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBlockExUnits :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
cppMaxTxExUnits :: THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
cppPrices :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
cppCostModels :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
cppCoinsPerUTxOByte :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppMinPoolCost :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppProtocolVersion :: HKDNoUpdate Identity ProtVer
cppTau :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppRho :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity UnitInterval
cppA0 :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
cppNOpt :: THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppEMax :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
cppPoolDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppKeyDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
cppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMinFeeB :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeA :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
..} = do
    Integer
ppA <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeA
    Integer
ppB <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity Coin
cppMinFeeB
    Rational
ppA0 <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  NonNegativeInterval
cppA0
    Rational
ppMinFeeRefScriptCoinsPerByte <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  Identity
  NonNegativeInterval
cppMinFeeRefScriptCostPerByte
    Integer
ppCollateralPercentage <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppCollateralPercentage
    let
      ppMaxBlockSize :: Integer
ppMaxBlockSize = forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxBBSize
      ppMaxTxSize :: Integer
ppMaxTxSize = forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxTxSize
      ppMaxHeaderSize :: Integer
ppMaxHeaderSize = forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word16
cppMaxBHSize
    Integer
ppKeyDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppKeyDeposit
    Integer
ppPoolDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Coin
cppPoolDeposit
    Integer
ppEmax <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  Identity
  EpochInterval
cppEMax
    Integer
ppNopt <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity Word16
cppNOpt)
    let
      -- We don't really care about `ppPv` in conformance testing, because
      -- the actual protocol version is stored elsewhere starting from Conway
      -- and this is just here for backwards compatibility
      ppPv :: (Integer, Integer)
ppPv = (Integer
0, Integer
0)
      ppMinUTxOValue :: Integer
ppMinUTxOValue = Integer
0 -- minUTxOValue has been deprecated and is not supported in Conway
    Integer
ppCoinsPerUTxOByte <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) Identity CoinPerByte
cppCoinsPerUTxOByte
    ()
ppCostmdls <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) Identity CostModels
cppCostModels
    ()
ppPrices <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) Identity Prices
cppPrices
    let
      ppMaxRefScriptSizePerTx :: Integer
ppMaxRefScriptSizePerTx = forall a. Integral a => a -> Integer
toInteger Int
maxRefScriptSizePerTx
      ppMaxRefScriptSizePerBlock :: Integer
ppMaxRefScriptSizePerBlock = forall a. Integral a => a -> Integer
toInteger Int
maxRefScriptSizePerBlock
      ppRefScriptCostStride :: Integer
ppRefScriptCostStride = forall a. Integral a => a -> Integer
toInteger Int
refScriptCostStride
      ppRefScriptCostMultiplier :: Rational
ppRefScriptCostMultiplier = Rational
refScriptCostMultiplier
    (Integer, Integer)
ppMaxTxExUnits <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity OrdExUnits
cppMaxTxExUnits
    (Integer, Integer)
ppMaxBlockExUnits <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity OrdExUnits
cppMaxBlockExUnits
    let
      ppMaxValSize :: Integer
ppMaxValSize = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) Identity Word32
cppMaxValSize
      ppMaxCollateralInputs :: Integer
ppMaxCollateralInputs = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) Identity Word16
cppMaxCollateralInputs
    PoolThresholds
ppPoolThresholds <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  PoolVotingThresholds
cppPoolVotingThresholds
    DrepThresholds
ppDrepThresholds <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  Identity
  DRepVotingThresholds
cppDRepVotingThresholds
    let
      ppCcMinSize :: Integer
ppCcMinSize = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Word16
cppCommitteeMinSize
      ppCcMaxTermLength :: Integer
ppCcMaxTermLength = forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInterval -> Word32
unEpochInterval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppCommitteeMaxTermLength
    Integer
ppGovActionLifetime <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppGovActionLifetime
    Integer
ppGovActionDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'SecurityGroup) Identity Coin
cppGovActionDeposit
    Integer
ppDrepDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity Coin
cppDRepDeposit
    Integer
ppDrepActivity <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) Identity EpochInterval
cppDRepActivity

    forall (f :: * -> *) a. Applicative f => a -> f a
pure Agda.MkPParams {Integer
Rational
()
(Integer, Integer)
DrepThresholds
PoolThresholds
ppMaxBlockSize :: Integer
ppMaxTxSize :: Integer
ppMaxHeaderSize :: Integer
ppMaxTxExUnits :: (Integer, Integer)
ppMaxBlockExUnits :: (Integer, Integer)
ppMaxValSize :: Integer
ppMaxCollateralInputs :: Integer
ppPv :: (Integer, Integer)
ppA :: Integer
ppB :: Integer
ppKeyDeposit :: Integer
ppPoolDeposit :: Integer
ppCoinsPerUTxOByte :: Integer
ppPrices :: ()
ppMinFeeRefScriptCoinsPerByte :: Rational
ppMaxRefScriptSizePerTx :: Integer
ppMaxRefScriptSizePerBlock :: Integer
ppRefScriptCostStride :: Integer
ppRefScriptCostMultiplier :: Rational
ppMinUTxOValue :: Integer
ppEmax :: Integer
ppNopt :: Integer
ppA0 :: Rational
ppCollateralPercentage :: Integer
ppCostmdls :: ()
ppPoolThresholds :: PoolThresholds
ppDrepThresholds :: DrepThresholds
ppCcMinSize :: Integer
ppCcMaxTermLength :: Integer
ppGovActionLifetime :: Integer
ppGovActionDeposit :: Integer
ppDrepDeposit :: Integer
ppDrepActivity :: Integer
ppDrepActivity :: Integer
ppDrepDeposit :: Integer
ppGovActionDeposit :: Integer
ppGovActionLifetime :: Integer
ppCcMaxTermLength :: Integer
ppCcMinSize :: Integer
ppDrepThresholds :: DrepThresholds
ppPoolThresholds :: PoolThresholds
ppMaxCollateralInputs :: Integer
ppMaxValSize :: Integer
ppMaxBlockExUnits :: (Integer, Integer)
ppMaxTxExUnits :: (Integer, Integer)
ppRefScriptCostMultiplier :: Rational
ppRefScriptCostStride :: Integer
ppMaxRefScriptSizePerBlock :: Integer
ppMaxRefScriptSizePerTx :: Integer
ppPrices :: ()
ppCostmdls :: ()
ppCoinsPerUTxOByte :: Integer
ppMinUTxOValue :: Integer
ppPv :: (Integer, Integer)
ppNopt :: Integer
ppEmax :: Integer
ppPoolDeposit :: Integer
ppKeyDeposit :: Integer
ppMaxHeaderSize :: Integer
ppMaxTxSize :: Integer
ppMaxBlockSize :: Integer
ppCollateralPercentage :: Integer
ppMinFeeRefScriptCoinsPerByte :: Rational
ppA0 :: Rational
ppB :: Integer
ppA :: Integer
..}

instance
  SpecTranslate ctx (PParamsHKD Identity era) =>
  SpecTranslate ctx (PParams era)
  where
  type SpecRep (PParams era) = SpecRep (PParamsHKD Identity era)

  toSpecRep :: PParams era -> SpecTransM ctx (SpecRep (PParams era))
toSpecRep (PParams PParamsHKD Identity era
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsHKD Identity era
x

instance
  ( SpecRep (PParams era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD Identity era)
  ) =>
  SpecTranslate ctx (UtxoEnv era)
  where
  type SpecRep (UtxoEnv era) = Agda.UTxOEnv

  toSpecRep :: UtxoEnv era -> SpecTransM ctx (SpecRep (UtxoEnv era))
toSpecRep UtxoEnv era
x =
    Integer -> PParams -> Integer -> UTxOEnv
Agda.MkUTxOEnv
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. UtxoEnv era -> SlotNo
ueSlot UtxoEnv era
x)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. UtxoEnv era -> PParams era
uePParams UtxoEnv era
x)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Integer -> Coin
Coin Integer
10_000_000) -- TODO: Fix generating types

instance SpecTranslate ctx a => SpecTranslate ctx (Set a) where
  type SpecRep (Set a) = Agda.HSSet (SpecRep a)

  toSpecRep :: Set a -> SpecTransM ctx (SpecRep (Set a))
toSpecRep = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [a] -> HSSet a
Agda.MkHSSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList

instance SpecTranslate ctx a => SpecTranslate ctx (StrictSeq a) where
  type SpecRep (StrictSeq a) = [SpecRep a]

  toSpecRep :: StrictSeq a -> SpecTransM ctx (SpecRep (StrictSeq a))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance SpecTranslate ctx a => SpecTranslate ctx (Seq a) where
  type SpecRep (Seq a) = [SpecRep a]

  toSpecRep :: Seq a -> SpecTransM ctx (SpecRep (Seq a))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance SpecTranslate ctx a => SpecTranslate ctx (Sized a) where
  type SpecRep (Sized a) = SpecRep a

  toSpecRep :: Sized a -> SpecTransM ctx (SpecRep (Sized a))
toSpecRep (Sized a
x Int64
_) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x

instance SpecTranslate ctx ValidityInterval where
  type SpecRep ValidityInterval = (Maybe Integer, Maybe Integer)

  toSpecRep :: ValidityInterval -> SpecTransM ctx (SpecRep ValidityInterval)
toSpecRep (ValidityInterval StrictMaybe SlotNo
lo StrictMaybe SlotNo
hi) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (StrictMaybe SlotNo
lo, StrictMaybe SlotNo
hi)

instance SpecTranslate ctx (KeyHash r c) where
  type SpecRep (KeyHash r c) = Integer

  toSpecRep :: KeyHash r c -> SpecTransM ctx (SpecRep (KeyHash r c))
toSpecRep (KeyHash Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
h) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Hash (ADDRHASH c) (VerKeyDSIGN (DSIGN c))
h

instance Crypto c => SpecTranslate ctx (VKey k c) where
  type SpecRep (VKey k c) = Integer

  toSpecRep :: VKey k c -> SpecTransM ctx (SpecRep (VKey k c))
toSpecRep (VKey VerKeyDSIGN (DSIGN c)
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Natural
bytesToNatural forall a b. (a -> b) -> a -> b
$ forall v. DSIGNAlgorithm v => VerKeyDSIGN v -> ByteString
rawSerialiseVerKeyDSIGN VerKeyDSIGN (DSIGN c)
x

instance DSIGNAlgorithm v => SpecTranslate ctx (SignedDSIGN v a) where
  type SpecRep (SignedDSIGN v a) = Integer

  toSpecRep :: SignedDSIGN v a -> SpecTransM ctx (SpecRep (SignedDSIGN v a))
toSpecRep (SignedDSIGN SigDSIGN v
x) =
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Natural
bytesToNatural forall a b. (a -> b) -> a -> b
$ forall v. DSIGNAlgorithm v => SigDSIGN v -> ByteString
rawSerialiseSigDSIGN SigDSIGN v
x

instance (Crypto c, Typeable k) => SpecTranslate ctx (WitVKey k c) where
  type SpecRep (WitVKey k c) = (Integer, Integer)

  toSpecRep :: WitVKey k c -> SpecTransM ctx (SpecRep (WitVKey k c))
toSpecRep (WitVKey VKey k c
vk SignedDSIGN (DSIGN c) (Hash (HASH c) EraIndependentTxBody)
sk) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VKey k c
vk, SignedDSIGN (DSIGN c) (Hash (HASH c) EraIndependentTxBody)
sk)

instance Era era => SpecTranslate ctx (TxDats era) where
  type SpecRep (TxDats era) = Agda.HSMap Agda.DataHash Agda.Datum

  toSpecRep :: TxDats era -> SpecTransM ctx (SpecRep (TxDats era))
toSpecRep (TxDats Map (DataHash (EraCrypto era)) (Data era)
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (DataHash (EraCrypto era)) (Data era)
x

instance
  ( SpecTranslate ctx k
  , SpecTranslate ctx v
  ) =>
  SpecTranslate ctx (Map k v)
  where
  type SpecRep (Map k v) = Agda.HSMap (SpecRep k) (SpecRep v)

  toSpecRep :: Map k v -> SpecTransM ctx (SpecRep (Map k v))
toSpecRep = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toList

instance SpecTranslate ctx Word64 where
  type SpecRep Word64 = Integer

  toSpecRep :: Word64 -> SpecTransM ctx (SpecRep Word64)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance SpecTranslate ctx Word32 where
  type SpecRep Word32 = Integer

  toSpecRep :: Word32 -> SpecTransM ctx (SpecRep Word32)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance SpecTranslate ctx (AlonzoPlutusPurpose AsIx era) where
  type SpecRep (AlonzoPlutusPurpose AsIx era) = Agda.RdmrPtr

  toSpecRep :: AlonzoPlutusPurpose AsIx era
-> SpecTransM ctx (SpecRep (AlonzoPlutusPurpose AsIx era))
toSpecRep = \case
    AlonzoSpending (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoMinting (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoCertifying (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, forall a. Integral a => a -> Integer
toInteger Word32
i)
    AlonzoRewarding (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, forall a. Integral a => a -> Integer
toInteger Word32
i)

instance SpecTranslate ctx (ConwayPlutusPurpose AsIx era) where
  type SpecRep (ConwayPlutusPurpose AsIx era) = Agda.RdmrPtr

  toSpecRep :: ConwayPlutusPurpose AsIx era
-> SpecTransM ctx (SpecRep (ConwayPlutusPurpose AsIx era))
toSpecRep = \case
    ConwaySpending (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Spend, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayMinting (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Mint, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayCertifying (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Cert, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayRewarding (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Rewrd, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayVoting (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Vote, forall a. Integral a => a -> Integer
toInteger Word32
i)
    ConwayProposing (AsIx Word32
i) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tag
Agda.Propose, forall a. Integral a => a -> Integer
toInteger Word32
i)

instance
  ( SpecTranslate ctx a
  , SpecTranslate ctx b
  ) =>
  SpecTranslate ctx (a, b)
  where
  type SpecRep (a, b) = (SpecRep a, SpecRep b)

  toSpecRep :: (a, b) -> SpecTransM ctx (SpecRep (a, b))
toSpecRep (a
x, b
y) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep b
y

instance SpecTranslate ctx (Data era) where
  type SpecRep (Data era) = ()

  toSpecRep :: Data era -> SpecTransM ctx (SpecRep (Data era))
toSpecRep Data era
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance
  ( AlonzoEraScript era
  , SpecTranslate ctx (PlutusPurpose AsIx era)
  ) =>
  SpecTranslate ctx (Redeemers era)
  where
  type
    SpecRep (Redeemers era) =
      Agda.HSMap (SpecRep (PlutusPurpose AsIx era)) (Agda.Redeemer, Agda.ExUnits)

  toSpecRep :: Redeemers era -> SpecTransM ctx (SpecRep (Redeemers era))
toSpecRep (Redeemers Map (PlutusPurpose AsIx era) (Data era, ExUnits)
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (PlutusPurpose AsIx era) (Data era, ExUnits)
x

instance
  ( AlonzoEraScript era
  , SpecTranslate ctx (PlutusPurpose AsIx era)
  , SpecRep (PlutusPurpose AsIx era) ~ Agda.RdmrPtr
  , Script era ~ AlonzoScript era
  , NativeScript era ~ Timelock era
  ) =>
  SpecTranslate ctx (AlonzoTxWits era)
  where
  type SpecRep (AlonzoTxWits era) = Agda.TxWitnesses

  toSpecRep :: AlonzoTxWits era -> SpecTransM ctx (SpecRep (AlonzoTxWits era))
toSpecRep AlonzoTxWits era
x =
    HSMap Integer Integer
-> HSSet (Either HashedTimelock ())
-> HSMap () ()
-> HSMap RdmrPtr ((), (Integer, Integer))
-> TxWitnesses
Agda.MkTxWitnesses
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep [WitVKey 'Witness (EraCrypto era)]
txWitsMap)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [a] -> HSSet a
Agda.MkHSSet (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Map (ScriptHash (EraCrypto era)) (Script era)
txscripts AlonzoTxWits era
x))
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. AlonzoEraScript era => AlonzoTxWits era -> TxDats era
txdats AlonzoTxWits era
x)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Redeemers era
txrdmrs AlonzoTxWits era
x)
    where
      txWitsMap :: [WitVKey 'Witness (EraCrypto era)]
txWitsMap = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (forall era.
AlonzoEraScript era =>
AlonzoTxWits era -> Set (WitVKey 'Witness (EraCrypto era))
txwitsVKey AlonzoTxWits era
x)

instance SpecTranslate ctx a => SpecTranslate ctx (StrictMaybe a) where
  type SpecRep (StrictMaybe a) = Maybe (SpecRep a)

  toSpecRep :: StrictMaybe a -> SpecTransM ctx (SpecRep (StrictMaybe a))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe

instance SpecTranslate ctx a => SpecTranslate ctx (Maybe a) where
  type SpecRep (Maybe a) = Maybe (SpecRep a)

  toSpecRep :: Maybe a -> SpecTransM ctx (SpecRep (Maybe a))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep

instance SpecTranslate ctx (AlonzoTxAuxData era) where
  type SpecRep (AlonzoTxAuxData era) = Agda.AuxiliaryData

  toSpecRep :: AlonzoTxAuxData era
-> SpecTransM ctx (SpecRep (AlonzoTxAuxData era))
toSpecRep AlonzoTxAuxData era
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance SpecTranslate ctx (ScriptHash c) where
  type SpecRep (ScriptHash c) = Integer

  toSpecRep :: ScriptHash c -> SpecTransM ctx (SpecRep (ScriptHash c))
toSpecRep (ScriptHash Hash (ADDRHASH c) EraIndependentScript
h) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Hash (ADDRHASH c) EraIndependentScript
h

instance SpecTranslate ctx (Credential k c) where
  type SpecRep (Credential k c) = Agda.Credential

  toSpecRep :: Credential k c -> SpecTransM ctx (SpecRep (Credential k c))
toSpecRep (KeyHashObj KeyHash k c
h) = Integer -> Credential
Agda.KeyHashObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash k c
h
  toSpecRep (ScriptHashObj ScriptHash c
h) = Integer -> Credential
Agda.ScriptObj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ScriptHash c
h

instance SpecTranslate ctx Network where
  type SpecRep Network = ()

  toSpecRep :: Network -> SpecTransM ctx (SpecRep Network)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const ()

instance SpecTranslate ctx (RewardAccount c) where
  type SpecRep (RewardAccount c) = Agda.RwdAddr

  toSpecRep :: RewardAccount c -> SpecTransM ctx (SpecRep (RewardAccount c))
toSpecRep (RewardAccount Network
n Credential 'Staking c
c) = () -> Credential -> RwdAddr
Agda.RwdAddr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Network
n forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'Staking c
c

instance SpecTranslate ctx (PoolParams era) where
  type SpecRep (PoolParams era) = Agda.PoolParams

  toSpecRep :: PoolParams era -> SpecTransM ctx (SpecRep (PoolParams era))
toSpecRep PoolParams {Set (KeyHash 'Staking era)
Hash era (VerKeyVRF era)
StrictMaybe PoolMetadata
Coin
RewardAccount era
StrictSeq StakePoolRelay
UnitInterval
KeyHash 'StakePool era
ppId :: forall c. PoolParams c -> KeyHash 'StakePool c
ppVrf :: forall c. PoolParams c -> Hash c (VerKeyVRF c)
ppPledge :: forall c. PoolParams c -> Coin
ppCost :: forall c. PoolParams c -> Coin
ppMargin :: forall c. PoolParams c -> UnitInterval
ppRewardAccount :: forall c. PoolParams c -> RewardAccount c
ppOwners :: forall c. PoolParams c -> Set (KeyHash 'Staking c)
ppRelays :: forall c. PoolParams c -> StrictSeq StakePoolRelay
ppMetadata :: forall c. PoolParams c -> StrictMaybe PoolMetadata
ppMetadata :: StrictMaybe PoolMetadata
ppRelays :: StrictSeq StakePoolRelay
ppOwners :: Set (KeyHash 'Staking era)
ppRewardAccount :: RewardAccount era
ppMargin :: UnitInterval
ppCost :: Coin
ppPledge :: Coin
ppVrf :: Hash era (VerKeyVRF era)
ppId :: KeyHash 'StakePool era
..} = Credential -> PoolParams
Agda.PoolParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj KeyHash 'StakePool era
ppId)

instance SpecTranslate ctx (DRep c) where
  type SpecRep (DRep c) = Agda.VDeleg

  toSpecRep :: DRep c -> SpecTransM ctx (SpecRep (DRep c))
toSpecRep (DRepCredential Credential 'DRepRole c
c) = GovRole -> Credential -> VDeleg
Agda.CredVoter GovRole
Agda.DRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole c
c
  toSpecRep DRep c
DRepAlwaysAbstain = forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.AbstainRep
  toSpecRep DRep c
DRepAlwaysNoConfidence = forall (f :: * -> *) a. Applicative f => a -> f a
pure VDeleg
Agda.NoConfidenceRep

instance SpecTranslate ctx Url where
  type SpecRep Url = T.Text
  toSpecRep :: Url -> SpecTransM ctx (SpecRep Url)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Url -> Text
urlToText

instance SpecTranslate ctx (Anchor c) where
  type SpecRep (Anchor c) = Agda.Anchor
  toSpecRep :: Anchor c -> SpecTransM ctx (SpecRep (Anchor c))
toSpecRep (Anchor Url
url SafeHash c AnchorData
_) = Text -> () -> Anchor
Agda.Anchor forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Url
url forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance SpecTranslate ctx (TxId era) where
  type SpecRep (TxId era) = Agda.TxId

  toSpecRep :: TxId era -> SpecTransM ctx (SpecRep (TxId era))
toSpecRep (TxId SafeHash era EraIndependentTxBody
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash era EraIndependentTxBody
x

instance SpecTranslate ctx (Withdrawals era) where
  type SpecRep (Withdrawals era) = Agda.Wdrl

  toSpecRep :: Withdrawals era -> SpecTransM ctx (SpecRep (Withdrawals era))
toSpecRep (Withdrawals Map (RewardAcnt era) Coin
w) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (RewardAcnt era) Coin
w

instance SpecTranslate ctx (AuxiliaryDataHash c) where
  type SpecRep (AuxiliaryDataHash c) = ()

  toSpecRep :: AuxiliaryDataHash c
-> SpecTransM ctx (SpecRep (AuxiliaryDataHash c))
toSpecRep AuxiliaryDataHash c
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance
  ( ConwayEraTxBody era
  , TxBody era ~ ConwayTxBody era
  , SpecRep (TxOut era) ~ Agda.TxOut
  , SpecRep (ConwayTxCert era) ~ Agda.DCert
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , TxCert era ~ ConwayTxCert era
  , Share (TxOut era) ~ Interns (Credential 'Staking (EraCrypto era))
  , Inject ctx Integer
  , Inject ctx (TxId (EraCrypto era))
  , SpecTranslate ctx (TxOut era)
  , SpecTranslate ctx (ConwayTxCert era)
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  ) =>
  SpecTranslate ctx (ConwayTxBody era)
  where
  type SpecRep (ConwayTxBody era) = Agda.TxBody

  toSpecRep :: ConwayTxBody era -> SpecTransM ctx (SpecRep (ConwayTxBody era))
toSpecRep ConwayTxBody era
txb = do
    Integer
sizeTx <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx
    TxId (EraCrypto era)
txId <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(TxId (EraCrypto era))
    HSSet (Integer, Integer)
-> HSSet (Integer, Integer)
-> HSMap Integer TxOut
-> Integer
-> Integer
-> (Maybe Integer, Maybe Integer)
-> [DCert]
-> HSMap RwdAddr Integer
-> [GovVote]
-> [GovProposal]
-> Integer
-> Maybe (HSMap Integer PParamsUpdate, Integer)
-> Maybe ()
-> Maybe ()
-> Maybe Integer
-> Integer
-> Integer
-> HSSet (Integer, Integer)
-> HSSet Integer
-> Maybe Integer
-> TxBody
Agda.MkTxBody
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
inputsTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
referenceInputsTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0 ..] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxOut era))
outputsTxBodyL))
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
AllegraEraTxBody era =>
Lens' (TxBody era) ValidityInterval
vldtTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Withdrawals (EraCrypto era))
withdrawalsTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraTxBody era =>
Lens' (TxBody era) (VotingProcedures era)
votingProceduresTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraTxBody era =>
Lens' (TxBody era) (OSet (ProposalProcedure era))
proposalProceduresTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. ConwayEraTxBody era => Lens' (TxBody era) Coin
treasuryDonationTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing -- TODO implement this properly
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens'
  (TxBody era) (StrictMaybe (AuxiliaryDataHash (EraCrypto era)))
auxDataHashTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (StrictMaybe Network)
networkIdTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraTxBody era =>
Lens' (TxBody era) (StrictMaybe Coin)
currentTreasuryValueTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
sizeTx
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep TxId (EraCrypto era)
txId
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
collateralInputsTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (Set (KeyHash 'Witness (EraCrypto era)))
reqSignerHashesTxBodyL)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (ConwayTxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
AlonzoEraTxBody era =>
Lens'
  (TxBody era) (StrictMaybe (ScriptIntegrityHash (EraCrypto era)))
scriptIntegrityHashTxBodyL)

data ConwayTxBodyTransContext c = ConwayTxBodyTransContext
  { forall c. ConwayTxBodyTransContext c -> Integer
ctbtcSizeTx :: !Integer
  , forall c. ConwayTxBodyTransContext c -> TxId c
ctbtcTxId :: !(TxId c)
  }

instance Inject (ConwayTxBodyTransContext c) Integer where
  inject :: ConwayTxBodyTransContext c -> Integer
inject = forall c. ConwayTxBodyTransContext c -> Integer
ctbtcSizeTx

instance Inject (ConwayTxBodyTransContext c) (TxId c) where
  inject :: ConwayTxBodyTransContext c -> TxId c
inject = forall c. ConwayTxBodyTransContext c -> TxId c
ctbtcTxId

instance SpecTranslate ctx IsValid where
  type SpecRep IsValid = Bool

  toSpecRep :: IsValid -> SpecTransM ctx (SpecRep IsValid)
toSpecRep (IsValid Bool
b) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
b

instance
  ( SpecTranslate ctx (TxWits era)
  , SpecTranslate ctx (TxAuxData era)
  , SpecTranslate (ConwayTxBodyTransContext (EraCrypto era)) (TxBody era)
  , SpecRep (TxWits era) ~ Agda.TxWitnesses
  , SpecRep (TxAuxData era) ~ Agda.AuxiliaryData
  , SpecRep (TxBody era) ~ Agda.TxBody
  , Tx era ~ AlonzoTx era
  , EraTx era
  , BabbageEraTxBody era
  ) =>
  SpecTranslate ctx (AlonzoTx era)
  where
  type SpecRep (AlonzoTx era) = Agda.Tx

  toSpecRep :: AlonzoTx era -> SpecTransM ctx (SpecRep (AlonzoTx era))
toSpecRep AlonzoTx era
tx =
    TxBody -> TxWitnesses -> Bool -> Maybe () -> Tx
Agda.MkTx
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx
        (forall c. Integer -> TxId c -> ConwayTxBodyTransContext c
ConwayTxBodyTransContext @(EraCrypto era) (AlonzoTx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => SimpleGetter (Tx era) Integer
sizeTxF) (forall era. EraTx era => Tx era -> TxId (EraCrypto era)
txIdTx AlonzoTx era
tx))
        (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. AlonzoTx era -> TxBody era
body AlonzoTx era
tx))
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. AlonzoTx era -> TxWits era
wits AlonzoTx era
tx)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. AlonzoTx era -> IsValid
isValid AlonzoTx era
tx)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. AlonzoTx era -> StrictMaybe (TxAuxData era)
auxiliaryData AlonzoTx era
tx)

instance
  ( ToExpr (Value era)
  , ToExpr (TxOut era)
  , ToExpr (PredicateFailure (EraRule "UTXOS" era))
  ) =>
  SpecTranslate ctx (ConwayUtxoPredFailure era)
  where
  type SpecRep (ConwayUtxoPredFailure era) = OpaqueErrorString

  toSpecRep :: ConwayUtxoPredFailure era
-> SpecTransM ctx (SpecRep (ConwayUtxoPredFailure era))
toSpecRep ConwayUtxoPredFailure era
e = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> OpaqueErrorString
OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. ToExpr a => a -> Expr
toExpr ConwayUtxoPredFailure era
e

instance
  ( EraPParams era
  , ToExpr (PParamsHKD StrictMaybe era)
  ) =>
  SpecTranslate ctx (ConwayGovPredFailure era)
  where
  type SpecRep (ConwayGovPredFailure era) = OpaqueErrorString

  toSpecRep :: ConwayGovPredFailure era
-> SpecTransM ctx (SpecRep (ConwayGovPredFailure era))
toSpecRep ConwayGovPredFailure era
e = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> OpaqueErrorString
OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. ToExpr a => a -> Expr
toExpr ConwayGovPredFailure era
e

instance SpecTranslate ctx (GovPurposeId r c) where
  type SpecRep (GovPurposeId r c) = (Agda.TxId, Integer)

  toSpecRep :: GovPurposeId r c -> SpecTransM ctx (SpecRep (GovPurposeId r c))
toSpecRep (GovPurposeId GovActionId (EraCrypto c)
gaId) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId (EraCrypto c)
gaId

instance SpecTranslate ctx UnitInterval where
  type SpecRep UnitInterval = Agda.Rational

  toSpecRep :: UnitInterval -> SpecTransM ctx (SpecRep UnitInterval)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. BoundedRational r => r -> Rational
unboundRational

instance SpecTranslate ctx (Committee era) where
  type SpecRep (Committee era) = (Agda.HSMap Agda.Credential Agda.Epoch, Agda.Rational)

  toSpecRep :: Committee era -> SpecTransM ctx (SpecRep (Committee era))
toSpecRep (Committee Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
members UnitInterval
threshold) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
members, UnitInterval
threshold)

instance SpecTranslate ctx (Constitution era) where
  type SpecRep (Constitution era) = (Agda.DataHash, Maybe Agda.ScriptHash)

  toSpecRep :: Constitution era -> SpecTransM ctx (SpecRep (Constitution era))
toSpecRep (Constitution (Anchor Url
_ SafeHash (EraCrypto era) AnchorData
h) StrictMaybe (ScriptHash (EraCrypto era))
policy) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (SafeHash (EraCrypto era) AnchorData
h, StrictMaybe (ScriptHash (EraCrypto era))
policy)

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  ) =>
  SpecTranslate ctx (EnactState era)
  where
  type SpecRep (EnactState era) = Agda.EnactState

  toSpecRep :: EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
toSpecRep EnactState {Map (Credential 'Staking (EraCrypto era)) Coin
PParams era
StrictMaybe (Committee era)
Coin
Constitution era
GovRelation StrictMaybe era
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe era
ensWithdrawals :: forall era.
EnactState era -> Map (Credential 'Staking (EraCrypto era)) Coin
ensTreasury :: forall era. EnactState era -> Coin
ensPrevPParams :: forall era. EnactState era -> PParams era
ensCurPParams :: forall era. EnactState era -> PParams era
ensConstitution :: forall era. EnactState era -> Constitution era
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
ensPrevGovActionIds :: GovRelation StrictMaybe era
ensWithdrawals :: Map (Credential 'Staking (EraCrypto era)) Coin
ensTreasury :: Coin
ensPrevPParams :: PParams era
ensCurPParams :: PParams era
ensConstitution :: Constitution era
ensCommittee :: StrictMaybe (Committee era)
..} =
    (Maybe (HSMap Credential Integer, Rational), (Integer, Integer))
-> (((), Maybe Integer), (Integer, Integer))
-> ((Integer, Integer), (Integer, Integer))
-> (PParams, (Integer, Integer))
-> HSMap RwdAddr Integer
-> EnactState
Agda.MkEnactState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
 Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected StrictMaybe (Committee era)
ensCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
grCommittee
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
 Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected Constitution era
ensConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grConstitution
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
 Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected (PParams era
ensCurPParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL) StrictMaybe (GovPurposeId 'HardForkPurpose era)
grHardFork
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {a} {a} {b} {ctx} {a}.
(SpecRep a ~ (a, b), SpecTranslate ctx a, SpecTranslate ctx a,
 Num a, Num b) =>
a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected PParams era
ensCurPParams StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
grPParamUpdate
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {a} {ctx}.
(SpecRep a ~ Credential, SpecTranslate ctx a) =>
Map a Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
transWithdrawals Map (Credential 'Staking (EraCrypto era)) Coin
ensWithdrawals
    where
      GovRelation {StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
StrictMaybe (GovPurposeId 'HardForkPurpose era)
StrictMaybe (GovPurposeId 'CommitteePurpose era)
StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grConstitution :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'ConstitutionPurpose era)
grCommittee :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'CommitteePurpose era)
grHardFork :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'HardForkPurpose era)
grPParamUpdate :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'PParamUpdatePurpose era)
grPParamUpdate :: StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
grHardFork :: StrictMaybe (GovPurposeId 'HardForkPurpose era)
grConstitution :: StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
grCommittee :: StrictMaybe (GovPurposeId 'CommitteePurpose era)
..} = GovRelation StrictMaybe era
ensPrevGovActionIds
      transWithdrawals :: Map a Coin -> SpecTransM ctx (HSMap RwdAddr Integer)
transWithdrawals Map a Coin
ws = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
Map.toList Map a Coin
ws) forall a b. (a -> b) -> a -> b
$
        \(a
cred, Coin Integer
amount) -> do
          Credential
agdaCred <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
cred
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Credential -> RwdAddr
Agda.RwdAddr () Credential
agdaCred, Integer
amount)
      transHashProtected :: a -> StrictMaybe a -> SpecTransM ctx (SpecRep a, (a, b))
transHashProtected a
x StrictMaybe a
h = do
        SpecRep a
committee <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
x
        (a, b)
agdaLastId <- case StrictMaybe a
h of
          SJust a
lastId -> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
lastId
          StrictMaybe a
SNothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
0, b
0)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecRep a
committee, (a, b)
agdaLastId)

instance SpecTranslate ctx (Voter era) where
  type SpecRep (Voter era) = Agda.Voter

  toSpecRep :: Voter era -> SpecTransM ctx (SpecRep (Voter era))
toSpecRep (CommitteeVoter Credential 'HotCommitteeRole era
c) = (GovRole
Agda.CC,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'HotCommitteeRole era
c
  toSpecRep (DRepVoter Credential 'DRepRole era
c) = (GovRole
Agda.DRep,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole era
c
  toSpecRep (StakePoolVoter KeyHash 'StakePool era
kh) = (GovRole
Agda.SPO,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj KeyHash 'StakePool era
kh)

instance SpecTranslate ctx Vote where
  type SpecRep Vote = Agda.Vote

  toSpecRep :: Vote -> SpecTransM ctx (SpecRep Vote)
toSpecRep Vote
VoteYes = forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.Yes
  toSpecRep Vote
VoteNo = forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.No
  toSpecRep Vote
Abstain = forall (f :: * -> *) a. Applicative f => a -> f a
pure Vote
Agda.Abstain

instance SpecTranslate ctx (VotingProcedures era) where
  type SpecRep (VotingProcedures era) = [Agda.GovVote]

  toSpecRep :: VotingProcedures era
-> SpecTransM ctx (SpecRep (VotingProcedures era))
toSpecRep = forall era c.
(Voter (EraCrypto era)
 -> GovActionId (EraCrypto era) -> VotingProcedure era -> c -> c)
-> c -> VotingProcedures era -> c
foldrVotingProcedures Voter (EraCrypto era)
-> GovActionId (EraCrypto era)
-> VotingProcedure era
-> SpecTransM ctx [GovVote]
-> SpecTransM ctx [GovVote]
go (forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
    where
      go ::
        Voter (EraCrypto era) ->
        GovActionId (EraCrypto era) ->
        VotingProcedure era ->
        SpecTransM ctx [Agda.GovVote] ->
        SpecTransM ctx [Agda.GovVote]
      go :: Voter (EraCrypto era)
-> GovActionId (EraCrypto era)
-> VotingProcedure era
-> SpecTransM ctx [GovVote]
-> SpecTransM ctx [GovVote]
go Voter (EraCrypto era)
voter GovActionId (EraCrypto era)
gaId VotingProcedure era
votingProcedure SpecTransM ctx [GovVote]
m =
        (:)
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( (Integer, Integer)
-> (GovRole, Credential) -> Vote -> Maybe Anchor -> GovVote
Agda.GovVote
                  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId (EraCrypto era)
gaId
                  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Voter (EraCrypto era)
voter
                  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. VotingProcedure era -> Vote
vProcVote VotingProcedure era
votingProcedure)
                  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era.
VotingProcedure era -> StrictMaybe (Anchor (EraCrypto era))
vProcAnchor VotingProcedure era
votingProcedure)
              )
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx [GovVote]
m

instance SpecTranslate ctx Word16 where
  type SpecRep Word16 = Integer

  toSpecRep :: Word16 -> SpecTransM ctx (SpecRep Word16)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance SpecTranslate ctx NonNegativeInterval where
  type SpecRep NonNegativeInterval = Agda.Rational

  toSpecRep :: NonNegativeInterval -> SpecTransM ctx (SpecRep NonNegativeInterval)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. BoundedRational r => r -> Rational
unboundRational

instance SpecTranslate ctx (ConwayPParams StrictMaybe era) where
  type SpecRep (ConwayPParams StrictMaybe era) = Agda.PParamsUpdate

  toSpecRep :: ConwayPParams StrictMaybe era
-> SpecTransM ctx (SpecRep (ConwayPParams StrictMaybe era))
toSpecRep (ConwayPParams {THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  DRepVotingThresholds
THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  CostModels
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  NonNegativeInterval
THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  EpochInterval
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
HKDNoUpdate StrictMaybe ProtVer
cppMinFeeRefScriptCostPerByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
cppDRepActivity :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppDRepDeposit :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
cppGovActionDeposit :: THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
cppGovActionLifetime :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppCommitteeMaxTermLength :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppCommitteeMinSize :: THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
cppDRepVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  DRepVotingThresholds
cppPoolVotingThresholds :: THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
cppMaxCollateralInputs :: THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCollateralPercentage :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppMaxValSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxBlockExUnits :: THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
cppMaxTxExUnits :: THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
cppPrices :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
cppCostModels :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  CostModels
cppCoinsPerUTxOByte :: THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
cppMinPoolCost :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppProtocolVersion :: HKDNoUpdate StrictMaybe ProtVer
cppTau :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
cppRho :: THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup)
  StrictMaybe
  UnitInterval
cppA0 :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  NonNegativeInterval
cppNOpt :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppEMax :: THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  EpochInterval
cppPoolDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppKeyDeposit :: THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppMaxBHSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
cppMaxTxSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxBBSize :: THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMinFeeB :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeA :: THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeA :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMinFeeB :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f Coin
cppMaxBBSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxTxSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppMaxBHSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word16
cppKeyDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppPoolDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppEMax :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f EpochInterval
cppNOpt :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppA0 :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f NonNegativeInterval
cppRho :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppTau :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f UnitInterval
cppProtocolVersion :: forall (f :: * -> *) era.
ConwayPParams f era -> HKDNoUpdate f ProtVer
cppMinPoolCost :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Coin
cppCoinsPerUTxOByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'SecurityGroup) f CoinPerByte
cppCostModels :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f CostModels
cppPrices :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) f Prices
cppMaxTxExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f OrdExUnits
cppMaxBlockExUnits :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f OrdExUnits
cppMaxValSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'SecurityGroup) f Word32
cppCollateralPercentage :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) f Word16
cppMaxCollateralInputs :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) f Word16
cppPoolVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f PoolVotingThresholds
cppDRepVotingThresholds :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'GovGroup 'NoStakePoolGroup) f DRepVotingThresholds
cppCommitteeMinSize :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Word16
cppCommitteeMaxTermLength :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionLifetime :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppGovActionDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'SecurityGroup) f Coin
cppDRepDeposit :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f Coin
cppDRepActivity :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) f EpochInterval
cppMinFeeRefScriptCostPerByte :: forall (f :: * -> *) era.
ConwayPParams f era
-> THKD
     ('PPGroups 'EconomicGroup 'SecurityGroup) f NonNegativeInterval
..}) = do
    Maybe Integer
ppuA <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeA
    Maybe Integer
ppuB <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe Coin
cppMinFeeB
    Maybe Rational
ppuA0 <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  NonNegativeInterval
cppA0
    Maybe Rational
ppuMinFeeRefScriptCoinsPerByte <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup)
  StrictMaybe
  NonNegativeInterval
cppMinFeeRefScriptCostPerByte
    Maybe Integer
ppuCollateralPercentage <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCollateralPercentage
    let
      ppuMaxBlockSize :: Maybe Integer
ppuMaxBlockSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxBBSize
      ppuMaxTxSize :: Maybe Integer
ppuMaxTxSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxTxSize
      ppuMaxHeaderSize :: Maybe Integer
ppuMaxHeaderSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word16
cppMaxBHSize
    Maybe Integer
ppuKeyDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppKeyDeposit
    Maybe Integer
ppuPoolDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Coin
cppPoolDeposit
    Maybe Integer
ppuEmax <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  EpochInterval
cppEMax
    Maybe Integer
ppuNopt <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup) StrictMaybe Word16
cppNOpt)
    let
      ppuPv :: Maybe a
ppuPv = forall a. Maybe a
Nothing
      ppuMinUTxOValue :: Maybe a
ppuMinUTxOValue = forall a. Maybe a
Nothing -- minUTxOValue has been deprecated and is not supported in Conway
    Maybe Integer
ppuCoinsPerUTxOByte <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'SecurityGroup) StrictMaybe CoinPerByte
cppCoinsPerUTxOByte
    Maybe ()
ppuCostmdls <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'TechnicalGroup 'NoStakePoolGroup)
  StrictMaybe
  CostModels
cppCostModels
    Maybe ()
ppuPrices <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'EconomicGroup 'NoStakePoolGroup) StrictMaybe Prices
cppPrices
    let
      ppuMaxRefScriptSizePerTx :: Maybe a
ppuMaxRefScriptSizePerTx = forall a. Maybe a
Nothing
      ppuMaxRefScriptSizePerBlock :: Maybe a
ppuMaxRefScriptSizePerBlock = forall a. Maybe a
Nothing
      ppuRefScriptCostStride :: Maybe a
ppuRefScriptCostStride = forall a. Maybe a
Nothing
      ppuRefScriptCostMultiplier :: Maybe a
ppuRefScriptCostMultiplier = forall a. Maybe a
Nothing
    Maybe (Integer, Integer)
ppuMaxTxExUnits <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe OrdExUnits
cppMaxTxExUnits
    Maybe (Integer, Integer)
ppuMaxBlockExUnits <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe OrdExUnits
cppMaxBlockExUnits
    let
      ppuMaxValSize :: Maybe Integer
ppuMaxValSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'SecurityGroup) StrictMaybe Word32
cppMaxValSize
      ppuMaxCollateralInputs :: Maybe Integer
ppuMaxCollateralInputs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD forall a b. (a -> b) -> a -> b
$ THKD ('PPGroups 'NetworkGroup 'NoStakePoolGroup) StrictMaybe Word16
cppMaxCollateralInputs
    Maybe PoolThresholds
ppuPoolThresholds <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  PoolVotingThresholds
cppPoolVotingThresholds
    Maybe DrepThresholds
ppuDrepThresholds <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup)
  StrictMaybe
  DRepVotingThresholds
cppDRepVotingThresholds
    let
      ppuCcMinSize :: Maybe Integer
ppuCcMinSize = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Word16
cppCommitteeMinSize
      ppuCcMaxTermLength :: Maybe Integer
ppuCcMaxTermLength =
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochInterval -> Word32
unEpochInterval) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall a b. (a -> b) -> a -> b
$ forall (t :: PPGroups) (f :: * -> *) a. THKD t f a -> HKD f a
unTHKD THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppCommitteeMaxTermLength
    Maybe Integer
ppuGovActionLifetime <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppGovActionLifetime
    Maybe Integer
ppuGovActionDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'SecurityGroup) StrictMaybe Coin
cppGovActionDeposit
    Maybe Integer
ppuDrepDeposit <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe Coin
cppDRepDeposit
    Maybe Integer
ppuDrepActivity <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep THKD
  ('PPGroups 'GovGroup 'NoStakePoolGroup) StrictMaybe EpochInterval
cppDRepActivity

    forall (f :: * -> *) a. Applicative f => a -> f a
pure Agda.MkPParamsUpdate {Maybe Integer
Maybe Rational
Maybe ()
Maybe (Integer, Integer)
Maybe DrepThresholds
Maybe PoolThresholds
forall a. Maybe a
ppuMaxBlockSize :: Maybe Integer
ppuMaxTxSize :: Maybe Integer
ppuMaxHeaderSize :: Maybe Integer
ppuMaxValSize :: Maybe Integer
ppuMaxCollateralInputs :: Maybe Integer
ppuMaxTxExUnits :: Maybe (Integer, Integer)
ppuMaxBlockExUnits :: Maybe (Integer, Integer)
ppuPv :: Maybe (Integer, Integer)
ppuA :: Maybe Integer
ppuB :: Maybe Integer
ppuKeyDeposit :: Maybe Integer
ppuPoolDeposit :: Maybe Integer
ppuCoinsPerUTxOByte :: Maybe Integer
ppuPrices :: Maybe ()
ppuMinFeeRefScriptCoinsPerByte :: Maybe Rational
ppuMaxRefScriptSizePerTx :: Maybe Integer
ppuMaxRefScriptSizePerBlock :: Maybe Integer
ppuRefScriptCostStride :: Maybe Integer
ppuRefScriptCostMultiplier :: Maybe Rational
ppuMinUTxOValue :: Maybe Integer
ppuA0 :: Maybe Rational
ppuEmax :: Maybe Integer
ppuNopt :: Maybe Integer
ppuCollateralPercentage :: Maybe Integer
ppuCostmdls :: Maybe ()
ppuDrepThresholds :: Maybe DrepThresholds
ppuPoolThresholds :: Maybe PoolThresholds
ppuGovActionLifetime :: Maybe Integer
ppuGovActionDeposit :: Maybe Integer
ppuDrepDeposit :: Maybe Integer
ppuDrepActivity :: Maybe Integer
ppuCcMinSize :: Maybe Integer
ppuCcMaxTermLength :: Maybe Integer
ppuDrepActivity :: Maybe Integer
ppuDrepDeposit :: Maybe Integer
ppuGovActionDeposit :: Maybe Integer
ppuGovActionLifetime :: Maybe Integer
ppuCcMaxTermLength :: Maybe Integer
ppuCcMinSize :: Maybe Integer
ppuDrepThresholds :: Maybe DrepThresholds
ppuPoolThresholds :: Maybe PoolThresholds
ppuMaxCollateralInputs :: Maybe Integer
ppuMaxValSize :: Maybe Integer
ppuMaxBlockExUnits :: Maybe (Integer, Integer)
ppuMaxTxExUnits :: Maybe (Integer, Integer)
ppuRefScriptCostMultiplier :: forall a. Maybe a
ppuRefScriptCostStride :: forall a. Maybe a
ppuMaxRefScriptSizePerBlock :: forall a. Maybe a
ppuMaxRefScriptSizePerTx :: forall a. Maybe a
ppuPrices :: Maybe ()
ppuCostmdls :: Maybe ()
ppuCoinsPerUTxOByte :: Maybe Integer
ppuMinUTxOValue :: forall a. Maybe a
ppuPv :: forall a. Maybe a
ppuNopt :: Maybe Integer
ppuEmax :: Maybe Integer
ppuPoolDeposit :: Maybe Integer
ppuKeyDeposit :: Maybe Integer
ppuMaxHeaderSize :: Maybe Integer
ppuMaxTxSize :: Maybe Integer
ppuMaxBlockSize :: Maybe Integer
ppuCollateralPercentage :: Maybe Integer
ppuMinFeeRefScriptCoinsPerByte :: Maybe Rational
ppuA0 :: Maybe Rational
ppuB :: Maybe Integer
ppuA :: Maybe Integer
..}

instance
  SpecTranslate ctx (PParamsHKD StrictMaybe era) =>
  SpecTranslate ctx (PParamsUpdate era)
  where
  type SpecRep (PParamsUpdate era) = SpecRep (PParamsHKD StrictMaybe era)

  toSpecRep :: PParamsUpdate era -> SpecTransM ctx (SpecRep (PParamsUpdate era))
toSpecRep (PParamsUpdate PParamsHKD StrictMaybe era
ppu) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsHKD StrictMaybe era
ppu

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (GovAction era)
  where
  type SpecRep (GovAction era) = Agda.GovAction

  toSpecRep :: GovAction era -> SpecTransM ctx (SpecRep (GovAction era))
toSpecRep (ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
_ PParamsUpdate era
ppu StrictMaybe (ScriptHash (EraCrypto era))
_) = PParamsUpdate -> GovAction
Agda.ChangePParams forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParamsUpdate era
ppu
  toSpecRep (HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
_ ProtVer
pv) = (Integer, Integer) -> GovAction
Agda.TriggerHF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ProtVer
pv
  toSpecRep (TreasuryWithdrawals Map (RewardAccount (EraCrypto era)) Coin
withdrawals StrictMaybe (ScriptHash (EraCrypto era))
_) =
    HSMap RwdAddr Integer -> GovAction
Agda.TreasuryWdrl
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (RewardAccount (EraCrypto era)) Coin
withdrawals
  toSpecRep (NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure GovAction
Agda.NoConfidence
  toSpecRep (UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
_ Set (Credential 'ColdCommitteeRole (EraCrypto era))
remove Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
add UnitInterval
threshold) =
    HSMap Credential Integer
-> HSSet Credential -> Rational -> GovAction
Agda.UpdateCommittee
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
add
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (Credential 'ColdCommitteeRole (EraCrypto era))
remove
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UnitInterval
threshold
  toSpecRep (NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
_ (Constitution (Anchor Url
_ SafeHash (EraCrypto era) AnchorData
h) StrictMaybe (ScriptHash (EraCrypto era))
policy)) =
    () -> Maybe Integer -> GovAction
Agda.NewConstitution
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SafeHash (EraCrypto era) AnchorData
h
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe (ScriptHash (EraCrypto era))
policy
  toSpecRep GovAction era
InfoAction = forall (f :: * -> *) a. Applicative f => a -> f a
pure GovAction
Agda.Info

instance SpecTranslate ctx a => SpecTranslate ctx (OSet a) where
  type SpecRep (OSet a) = [SpecRep a]

  toSpecRep :: OSet a -> SpecTransM ctx (SpecRep (OSet a))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance
  ( SpecTranslate ctx k
  , SpecTranslate ctx v
  , Ord k
  ) =>
  SpecTranslate ctx (OMap k v)
  where
  type SpecRep (OMap k v) = [(SpecRep k, SpecRep v)]

  toSpecRep :: OMap k v -> SpecTransM ctx (SpecRep (OMap k v))
toSpecRep = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => OMap k v -> [(k, v)]
OMap.assocList

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (ProposalProcedure era)
  where
  type SpecRep (ProposalProcedure era) = Agda.GovProposal

  toSpecRep :: ProposalProcedure era
-> SpecTransM ctx (SpecRep (ProposalProcedure era))
toSpecRep ProposalProcedure {Coin
RewardAccount (EraCrypto era)
Anchor (EraCrypto era)
GovAction era
pProcAnchor :: forall era. ProposalProcedure era -> Anchor (EraCrypto era)
pProcGovAction :: forall era. ProposalProcedure era -> GovAction era
pProcReturnAddr :: forall era. ProposalProcedure era -> RewardAccount (EraCrypto era)
pProcDeposit :: forall era. ProposalProcedure era -> Coin
pProcAnchor :: Anchor (EraCrypto era)
pProcGovAction :: GovAction era
pProcReturnAddr :: RewardAccount (EraCrypto era)
pProcDeposit :: Coin
..} =
    GovAction
-> (Integer, Integer)
-> Maybe Integer
-> Integer
-> RwdAddr
-> Anchor
-> GovProposal
Agda.MkGovProposal
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
pProcGovAction
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall c era.
Crypto c =>
StrictMaybe (GovActionId c) -> GovAction era -> GovActionId c
nullifyIfNotNeeded StrictMaybe (GovActionId (EraCrypto era))
prevActionId GovAction era
pProcGovAction)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe (ScriptHash (EraCrypto era))
policy
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
pProcDeposit
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep RewardAccount (EraCrypto era)
pProcReturnAddr
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Anchor (EraCrypto era)
pProcAnchor
    where
      prevActionId :: StrictMaybe (GovActionId (EraCrypto era))
prevActionId = forall era.
GovAction era -> StrictMaybe (GovActionId (EraCrypto era))
prevGovActionId GovAction era
pProcGovAction
      policy :: StrictMaybe (ScriptHash (EraCrypto era))
policy =
        case GovAction era
pProcGovAction of
          TreasuryWithdrawals Map (RewardAccount (EraCrypto era)) Coin
_ StrictMaybe (ScriptHash (EraCrypto era))
sh -> StrictMaybe (ScriptHash (EraCrypto era))
sh
          ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
_ PParamsUpdate era
_ StrictMaybe (ScriptHash (EraCrypto era))
sh -> StrictMaybe (ScriptHash (EraCrypto era))
sh
          GovAction era
_ -> forall a. StrictMaybe a
SNothing

prevGovActionId :: GovAction era -> StrictMaybe (GovActionId (EraCrypto era))
prevGovActionId :: forall era.
GovAction era -> StrictMaybe (GovActionId (EraCrypto era))
prevGovActionId GovAction era
action =
  case GovAction era
action of
    ParameterChange StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x PParamsUpdate era
_ StrictMaybe (ScriptHash (EraCrypto era))
_ -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId (EraCrypto era)
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'PParamUpdatePurpose era)
x
    HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose era)
x ProtVer
_ -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId (EraCrypto era)
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'HardForkPurpose era)
x
    UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose era)
x Set (Credential 'ColdCommitteeRole (EraCrypto era))
_ Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo
_ UnitInterval
_ -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId (EraCrypto era)
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose era)
x
    NoConfidence StrictMaybe (GovPurposeId 'CommitteePurpose era)
x -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId (EraCrypto era)
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'CommitteePurpose era)
x
    NewConstitution StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
x Constitution era
_ -> forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId (EraCrypto era)
unGovPurposeId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictMaybe (GovPurposeId 'ConstitutionPurpose era)
x
    GovAction era
_ -> forall a. StrictMaybe a
SNothing

nullGovActionId :: Crypto c => GovActionId c
nullGovActionId :: forall c. Crypto c => GovActionId c
nullGovActionId = forall c. TxId c -> GovActionIx -> GovActionId c
GovActionId (forall c. SafeHash c EraIndependentTxBody -> TxId c
TxId forall a. Default a => a
def) (Word16 -> GovActionIx
GovActionIx Word16
0)

nullifyIfNotNeeded :: Crypto c => StrictMaybe (GovActionId c) -> GovAction era -> GovActionId c
nullifyIfNotNeeded :: forall c era.
Crypto c =>
StrictMaybe (GovActionId c) -> GovAction era -> GovActionId c
nullifyIfNotNeeded StrictMaybe (GovActionId c)
SNothing = forall a b. a -> b -> a
const forall c. Crypto c => GovActionId c
nullGovActionId
nullifyIfNotNeeded (SJust GovActionId c
gaId) = \case
  TreasuryWithdrawals {} -> forall c. Crypto c => GovActionId c
nullGovActionId
  GovAction era
InfoAction -> forall c. Crypto c => GovActionId c
nullGovActionId
  GovAction era
_ -> GovActionId c
gaId

unionsHSMaps :: [Agda.HSMap k v] -> Agda.HSMap k v
unionsHSMaps :: forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps [] = forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap []
unionsHSMaps ((Agda.MkHSMap [(k, v)]
x) : [HSMap k v]
xs) =
  let Agda.MkHSMap [(k, v)]
xs' = forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps [HSMap k v]
xs
   in forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall a b. (a -> b) -> a -> b
$ [(k, v)]
x forall a. Semigroup a => a -> a -> a
<> [(k, v)]
xs'

mapHSMapKey :: (k -> l) -> Agda.HSMap k v -> Agda.HSMap l v
mapHSMapKey :: forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey k -> l
f (Agda.MkHSMap [(k, v)]
l) = forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first k -> l
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(k, v)]
l

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (GovActionState era)
  where
  type SpecRep (GovActionState era) = Agda.GovActionState

  toSpecRep :: GovActionState era -> SpecTransM ctx (SpecRep (GovActionState era))
toSpecRep gas :: GovActionState era
gas@GovActionState {Map (Credential 'HotCommitteeRole (EraCrypto era)) Vote
Map (Credential 'DRepRole (EraCrypto era)) Vote
Map (KeyHash 'StakePool (EraCrypto era)) Vote
ProposalProcedure era
GovActionId (EraCrypto era)
EpochNo
gasExpiresAfter :: forall era. GovActionState era -> EpochNo
gasProposedIn :: forall era. GovActionState era -> EpochNo
gasProposalProcedure :: forall era. GovActionState era -> ProposalProcedure era
gasStakePoolVotes :: forall era.
GovActionState era -> Map (KeyHash 'StakePool (EraCrypto era)) Vote
gasDRepVotes :: forall era.
GovActionState era
-> Map (Credential 'DRepRole (EraCrypto era)) Vote
gasCommitteeVotes :: forall era.
GovActionState era
-> Map (Credential 'HotCommitteeRole (EraCrypto era)) Vote
gasId :: forall era. GovActionState era -> GovActionId (EraCrypto era)
gasExpiresAfter :: EpochNo
gasProposedIn :: EpochNo
gasProposalProcedure :: ProposalProcedure era
gasStakePoolVotes :: Map (KeyHash 'StakePool (EraCrypto era)) Vote
gasDRepVotes :: Map (Credential 'DRepRole (EraCrypto era)) Vote
gasCommitteeVotes :: Map (Credential 'HotCommitteeRole (EraCrypto era)) Vote
gasId :: GovActionId (EraCrypto era)
..} = do
    HSMap (GovRole, Credential) Vote
-> RwdAddr
-> Integer
-> GovAction
-> (Integer, Integer)
-> GovActionState
Agda.MkGovActionState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx (HSMap (GovRole, Credential) Vote)
agdaVoteMap
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall era. GovActionState era -> RewardAccount (EraCrypto era)
gasReturnAddr GovActionState era
gas)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
gasExpiresAfter
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
action
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (forall c era.
Crypto c =>
StrictMaybe (GovActionId c) -> GovAction era -> GovActionId c
nullifyIfNotNeeded (forall era.
GovAction era -> StrictMaybe (GovActionId (EraCrypto era))
prevGovActionId GovAction era
action) GovAction era
action)
    where
      action :: GovAction era
action = forall era. GovActionState era -> GovAction era
gasAction GovActionState era
gas
      agdaVoteMap :: SpecTransM ctx (Agda.HSMap (Agda.GovRole, Agda.Credential) Agda.Vote)
      agdaVoteMap :: SpecTransM ctx (HSMap (GovRole, Credential) Vote)
agdaVoteMap = do
        HSMap Credential Vote
drepVotes <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'DRepRole (EraCrypto era)) Vote
gasDRepVotes
        HSMap Credential Vote
ccVotes <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'HotCommitteeRole (EraCrypto era)) Vote
gasCommitteeVotes
        HSMap Integer Vote
spoVotes <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool (EraCrypto era)) Vote
gasStakePoolVotes
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
          forall k v. [HSMap k v] -> HSMap k v
unionsHSMaps
            [ forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (GovRole
Agda.DRep,) HSMap Credential Vote
drepVotes
            , forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (GovRole
Agda.CC,) HSMap Credential Vote
ccVotes
            , forall k l v. (k -> l) -> HSMap k v -> HSMap l v
mapHSMapKey (\Integer
h -> (GovRole
Agda.SPO, Integer -> Credential
Agda.KeyHashObj Integer
h)) HSMap Integer Vote
spoVotes
            ]

instance SpecTranslate ctx GovActionIx where
  type SpecRep GovActionIx = Integer

  toSpecRep :: GovActionIx -> SpecTransM ctx (SpecRep GovActionIx)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionIx -> Word16
unGovActionIx

instance SpecTranslate ctx (GovActionId c) where
  type SpecRep (GovActionId c) = Agda.GovActionID

  toSpecRep :: GovActionId c -> SpecTransM ctx (SpecRep (GovActionId c))
toSpecRep (GovActionId TxId c
txId GovActionIx
gaIx) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (TxId c
txId, GovActionIx
gaIx)

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (Proposals era)
  where
  type SpecRep (Proposals era) = Agda.GovState

  -- TODO get rid of `prioritySort` once we've changed the implementation so
  -- that the proposals are always sorted
  toSpecRep :: Proposals era -> SpecTransM ctx (SpecRep (Proposals era))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap (GovActionId (EraCrypto era)) (GovActionState era)
-> OMap (GovActionId (EraCrypto era)) (GovActionState era)
prioritySort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era.
Lens'
  (Proposals era)
  (OMap (GovActionId (EraCrypto era)) (GovActionState era))
pPropsL
    where
      prioritySort ::
        OMap (GovActionId (EraCrypto era)) (GovActionState era) ->
        OMap (GovActionId (EraCrypto era)) (GovActionState era)
      prioritySort :: OMap (GovActionId (EraCrypto era)) (GovActionState era)
-> OMap (GovActionId (EraCrypto era)) (GovActionState era)
prioritySort = forall l. IsList l => [Item l] -> l
Exts.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (forall era. GovAction era -> Int
actionPriority forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. GovActionState era -> GovAction era
gasAction) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
Exts.toList

instance Crypto c => SpecTranslate ctx (MaryValue c) where
  type SpecRep (MaryValue c) = Agda.Coin

  toSpecRep :: MaryValue c -> SpecTransM ctx (SpecRep (MaryValue c))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Val t => t -> Coin
coin

instance
  ( ToExpr (PredicateFailure (EraRule "DELEG" era))
  , ToExpr (PredicateFailure (EraRule "GOVCERT" era))
  , ToExpr (PredicateFailure (EraRule "POOL" era))
  ) =>
  SpecTranslate ctx (ConwayCertPredFailure era)
  where
  type SpecRep (ConwayCertPredFailure era) = OpaqueErrorString

  toSpecRep :: ConwayCertPredFailure era
-> SpecTransM ctx (SpecRep (ConwayCertPredFailure era))
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> OpaqueErrorString
OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> [Char]
showExpr

instance (SpecTranslate ctx a, Compactible a) => SpecTranslate ctx (CompactForm a) where
  type SpecRep (CompactForm a) = SpecRep a

  toSpecRep :: CompactForm a -> SpecTransM ctx (SpecRep (CompactForm a))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Compactible a => CompactForm a -> a
fromCompact

instance SpecTranslate ctx (CommitteeAuthorization c) where
  type
    SpecRep (CommitteeAuthorization c) =
      SpecRep (Maybe (Credential 'HotCommitteeRole c))

  toSpecRep :: CommitteeAuthorization c
-> SpecTransM ctx (SpecRep (CommitteeAuthorization c))
toSpecRep (CommitteeHotCredential Credential 'HotCommitteeRole c
c) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Credential 'HotCommitteeRole c
c
  toSpecRep (CommitteeMemberResigned StrictMaybe (Anchor c)
_) =
    forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$
      forall a. Maybe a
Nothing @(Credential 'HotCommitteeRole c)

instance SpecTranslate ctx (CommitteeState era) where
  type
    SpecRep (CommitteeState era) =
      SpecRep
        ( Map
            (Credential 'ColdCommitteeRole (EraCrypto era))
            (CommitteeAuthorization (EraCrypto era))
        )

  toSpecRep :: CommitteeState era -> SpecTransM ctx (SpecRep (CommitteeState era))
toSpecRep = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
CommitteeState era
-> Map
     (Credential 'ColdCommitteeRole (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era))
csCommitteeCreds

instance SpecTranslate ctx (IndividualPoolStake c) where
  type SpecRep (IndividualPoolStake c) = SpecRep Coin

  toSpecRep :: IndividualPoolStake c
-> SpecTransM ctx (SpecRep (IndividualPoolStake c))
toSpecRep (IndividualPoolStake Rational
_ CompactForm Coin
c Hash c (VerKeyVRF c)
_) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CompactForm Coin
c

instance SpecTranslate ctx (PoolDistr c) where
  type SpecRep (PoolDistr c) = Agda.HSMap Agda.VDeleg Agda.Coin

  toSpecRep :: PoolDistr c -> SpecTransM ctx (SpecRep (PoolDistr c))
toSpecRep (PoolDistr Map (KeyHash 'StakePool c) (IndividualPoolStake c)
ps CompactForm Coin
_) = do
    Agda.MkHSMap [(Integer, Integer)]
l <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (KeyHash 'StakePool c) (IndividualPoolStake c)
ps
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (GovRole -> Credential -> VDeleg
Agda.CredVoter GovRole
Agda.SPO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Credential
Agda.KeyHashObj) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Integer, Integer)]
l

instance
  Inject ctx Coin =>
  SpecTranslate ctx (RatifyEnv era)
  where
  type SpecRep (RatifyEnv era) = Agda.RatifyEnv

  toSpecRep :: RatifyEnv era -> SpecTransM ctx (SpecRep (RatifyEnv era))
toSpecRep RatifyEnv {Map (DRep (EraCrypto era)) (CompactForm Coin)
Map
  (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
Map (Credential 'Staking (EraCrypto era)) (DRep (EraCrypto era))
Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
CommitteeState era
PoolDistr (EraCrypto era)
EpochNo
reStakeDistr :: forall era.
RatifyEnv era
-> Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr (EraCrypto era)
reDRepDistr :: forall era.
RatifyEnv era -> Map (DRep (EraCrypto era)) (CompactForm Coin)
reDRepState :: forall era.
RatifyEnv era
-> Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reDelegatees :: forall era.
RatifyEnv era
-> Map (Credential 'Staking (EraCrypto era)) (DRep (EraCrypto era))
rePoolParams :: forall era.
RatifyEnv era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
rePoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
reDelegatees :: Map (Credential 'Staking (EraCrypto era)) (DRep (EraCrypto era))
reCommitteeState :: CommitteeState era
reCurrentEpoch :: EpochNo
reDRepState :: Map
  (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
reDRepDistr :: Map (DRep (EraCrypto era)) (CompactForm Coin)
reStakePoolDistr :: PoolDistr (EraCrypto era)
reStakeDistr :: Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
..} = do
    let
      stakeDistrs :: SpecTransM ctx StakeDistrs
stakeDistrs = do
        Agda.MkHSMap [(VDeleg, Integer)]
stakeDistrsMap <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PoolDistr (EraCrypto era)
reStakePoolDistr
        [(VDeleg, Integer)]
drepDistrsMap <- forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map (DRep (EraCrypto era)) (CompactForm Coin)
reDRepDistr
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. HSMap VDeleg Integer -> StakeDistrs
Agda.StakeDistrs forall a b. (a -> b) -> a -> b
$ forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(VDeleg, Integer)]
stakeDistrsMap forall a. Semigroup a => a -> a -> a
<> [(VDeleg, Integer)]
drepDistrsMap)
      dreps :: SpecTransM
  ctx (SpecRep (Map (Credential 'DRepRole (EraCrypto era)) EpochNo))
dreps = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall c. DRepState c -> EpochNo
drepExpiry Map
  (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
reDRepState
    Coin
treasury <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @Coin
    StakeDistrs
-> Integer
-> HSMap Credential Integer
-> HSMap Credential (Maybe Credential)
-> Integer
-> RatifyEnv
Agda.MkRatifyEnv
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM ctx StakeDistrs
stakeDistrs
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
reCurrentEpoch
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM
  ctx (SpecRep (Map (Credential 'DRepRole (EraCrypto era)) EpochNo))
dreps
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CommitteeState era
reCommitteeState
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
treasury

instance SpecTranslate ctx Bool where
  type SpecRep Bool = Bool

  toSpecRep :: Bool -> SpecTransM ctx (SpecRep Bool)
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance
  ( EraPParams era
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD Identity era)
  , Inject ctx [GovActionState era]
  , ToExpr (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  ) =>
  SpecTranslate ctx (RatifyState era)
  where
  type SpecRep (RatifyState era) = Agda.RatifyState

  toSpecRep :: RatifyState era -> SpecTransM ctx (SpecRep (RatifyState era))
toSpecRep RatifyState {Bool
Set (GovActionId (EraCrypto era))
EnactState era
Seq (GovActionState era)
rsDelayed :: forall era. RatifyState era -> Bool
rsExpired :: forall era. RatifyState era -> Set (GovActionId (EraCrypto era))
rsEnacted :: forall era. RatifyState era -> Seq (GovActionState era)
rsEnactState :: forall era. RatifyState era -> EnactState era
rsDelayed :: Bool
rsExpired :: Set (GovActionId (EraCrypto era))
rsEnacted :: Seq (GovActionState era)
rsEnactState :: EnactState era
..} = do
    Map (GovActionId (EraCrypto era)) (GovActionState era)
govActionMap <-
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Map (GovActionId (EraCrypto era)) (GovActionState era)
acc GovActionState era
gas -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (forall era. GovActionState era -> GovActionId (EraCrypto era)
gasId GovActionState era
gas) GovActionState era
gas Map (GovActionId (EraCrypto era)) (GovActionState era)
acc) forall a. Monoid a => a
mempty
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @[GovActionState era]
    let
      lookupGAS :: GovActionId (EraCrypto era)
-> SpecTransM
     ctx (Set (GovActionId (EraCrypto era), GovActionState era))
-> SpecTransM
     ctx (Set (GovActionId (EraCrypto era), GovActionState era))
lookupGAS GovActionId (EraCrypto era)
gaId SpecTransM
  ctx (Set (GovActionId (EraCrypto era), GovActionState era))
m = do
        case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup GovActionId (EraCrypto era)
gaId Map (GovActionId (EraCrypto era)) (GovActionState era)
govActionMap of
          Just GovActionState era
x -> forall a. Ord a => a -> Set a -> Set a
Set.insert (GovActionId (EraCrypto era)
gaId, GovActionState era
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecTransM
  ctx (Set (GovActionId (EraCrypto era), GovActionState era))
m
          Maybe (GovActionState era)
Nothing ->
            forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
              Text
"gaId: "
                forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (forall a. ToExpr a => a -> [Char]
showExpr GovActionId (EraCrypto era)
gaId)
                forall a. Semigroup a => a -> a -> a
<> Text
"\n\ngovActionMap: "
                forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (forall a. ToExpr a => a -> [Char]
showExpr Map (GovActionId (EraCrypto era)) (GovActionState era)
govActionMap)
                forall a. Semigroup a => a -> a -> a
<> Text
"\n\nGovActionId is not contained in the govActionMap"
    Set (GovActionId (EraCrypto era), GovActionState era)
removed <-
      forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr'
        GovActionId (EraCrypto era)
-> SpecTransM
     ctx (Set (GovActionId (EraCrypto era), GovActionState era))
-> SpecTransM
     ctx (Set (GovActionId (EraCrypto era), GovActionState era))
lookupGAS
        (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty)
        (Set (GovActionId (EraCrypto era))
rsExpired forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList (forall era. GovActionState era -> GovActionId (EraCrypto era)
gasId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq (GovActionState era)
rsEnacted))
    EnactState
-> HSSet ((Integer, Integer), GovActionState)
-> Bool
-> RatifyState
Agda.MkRatifyState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState era
rsEnactState
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (GovActionId (EraCrypto era), GovActionState era)
removed
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Bool
rsDelayed

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (RatifySignal era)
  where
  type
    SpecRep (RatifySignal era) =
      SpecRep [(GovActionId (EraCrypto era), GovActionState era)]

  toSpecRep :: RatifySignal era -> SpecTransM ctx (SpecRep (RatifySignal era))
toSpecRep (RatifySignal StrictSeq (GovActionState era)
x) =
    forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$
      (\gas :: GovActionState era
gas@GovActionState {GovActionId (EraCrypto era)
gasId :: GovActionId (EraCrypto era)
gasId :: forall era. GovActionState era -> GovActionId (EraCrypto era)
gasId} -> (GovActionId (EraCrypto era)
gasId, GovActionState era
gas)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictSeq (GovActionState era)
x

instance
  ( EraPParams era
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  ) =>
  SpecTranslate ctx (EnactSignal era)
  where
  type SpecRep (EnactSignal era) = SpecRep (GovAction era)

  toSpecRep :: EnactSignal era -> SpecTransM ctx (SpecRep (EnactSignal era))
toSpecRep (EnactSignal GovActionId (EraCrypto era)
_ GovAction era
ga) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovAction era
ga

instance ToExpr (EpochExecEnv era)
instance Era era => NFData (EpochExecEnv era)

instance HasSimpleRep (EpochExecEnv era)
instance (IsConwayUniv fn, Era era) => HasSpec fn (EpochExecEnv era)

instance SpecTranslate ctx (EpochExecEnv era) where
  type SpecRep (EpochExecEnv era) = ()

  toSpecRep :: EpochExecEnv era -> SpecTransM ctx (SpecRep (EpochExecEnv era))
toSpecRep EpochExecEnv era
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | This type is used as the Env only in the Agda Spec
data ConwayExecEnactEnv era = ConwayExecEnactEnv
  { forall era. ConwayExecEnactEnv era -> GovActionId (EraCrypto era)
ceeeGid :: !(GovActionId (EraCrypto era))
  , forall era. ConwayExecEnactEnv era -> Coin
ceeeTreasury :: !Coin
  , forall era. ConwayExecEnactEnv era -> EpochNo
ceeeEpoch :: !EpochNo
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
forall era x.
ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
$cto :: forall era x.
Rep (ConwayExecEnactEnv era) x -> ConwayExecEnactEnv era
$cfrom :: forall era x.
ConwayExecEnactEnv era -> Rep (ConwayExecEnactEnv era) x
Generic, ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
$c/= :: forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
== :: ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
$c== :: forall era.
ConwayExecEnactEnv era -> ConwayExecEnactEnv era -> Bool
Eq, Int -> ConwayExecEnactEnv era -> ShowS
forall era. Int -> ConwayExecEnactEnv era -> ShowS
forall era. [ConwayExecEnactEnv era] -> ShowS
forall era. ConwayExecEnactEnv era -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [ConwayExecEnactEnv era] -> ShowS
$cshowList :: forall era. [ConwayExecEnactEnv era] -> ShowS
show :: ConwayExecEnactEnv era -> [Char]
$cshow :: forall era. ConwayExecEnactEnv era -> [Char]
showsPrec :: Int -> ConwayExecEnactEnv era -> ShowS
$cshowsPrec :: forall era. Int -> ConwayExecEnactEnv era -> ShowS
Show)

-- | Here we inject the Agda Spec Env into the STS rule Environment, which is ().
instance Inject (ConwayExecEnactEnv era) () where
  inject :: ConwayExecEnactEnv era -> ()
inject ConwayExecEnactEnv era
_ = ()

instance ToExpr (ConwayExecEnactEnv era)
instance Era era => NFData (ConwayExecEnactEnv era)

instance HasSimpleRep (ConwayExecEnactEnv era)
instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayExecEnactEnv era)

instance SpecTranslate ctx (ConwayExecEnactEnv era) where
  type SpecRep (ConwayExecEnactEnv era) = Agda.EnactEnv

  toSpecRep :: ConwayExecEnactEnv era
-> SpecTransM ctx (SpecRep (ConwayExecEnactEnv era))
toSpecRep ConwayExecEnactEnv {Coin
GovActionId (EraCrypto era)
EpochNo
ceeeEpoch :: EpochNo
ceeeTreasury :: Coin
ceeeGid :: GovActionId (EraCrypto era)
ceeeEpoch :: forall era. ConwayExecEnactEnv era -> EpochNo
ceeeTreasury :: forall era. ConwayExecEnactEnv era -> Coin
ceeeGid :: forall era. ConwayExecEnactEnv era -> GovActionId (EraCrypto era)
..} =
    (Integer, Integer) -> Integer -> Integer -> EnactEnv
Agda.MkEnactEnv
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId (EraCrypto era)
ceeeGid
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
ceeeTreasury
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
ceeeEpoch

committeeCredentialToStrictMaybe ::
  CommitteeAuthorization c ->
  StrictMaybe (Credential 'HotCommitteeRole c)
committeeCredentialToStrictMaybe :: forall c.
CommitteeAuthorization c
-> StrictMaybe (Credential 'HotCommitteeRole c)
committeeCredentialToStrictMaybe (CommitteeHotCredential Credential 'HotCommitteeRole c
c) = forall a. a -> StrictMaybe a
SJust Credential 'HotCommitteeRole c
c
committeeCredentialToStrictMaybe (CommitteeMemberResigned StrictMaybe (Anchor c)
_) = forall a. StrictMaybe a
SNothing

instance HasSimpleRep (DepositPurpose c)
instance (IsConwayUniv fn, Crypto c) => HasSpec fn (DepositPurpose c)

instance SpecTranslate ctx (DepositPurpose c) where
  type SpecRep (DepositPurpose c) = Agda.DepositPurpose
  toSpecRep :: DepositPurpose c -> SpecTransM ctx (SpecRep (DepositPurpose c))
toSpecRep (CredentialDeposit Credential 'Staking c
cred) =
    Credential -> DepositPurpose
Agda.CredentialDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'Staking c
cred
  toSpecRep (PoolDeposit KeyHash 'StakePool c
kh) =
    Integer -> DepositPurpose
Agda.PoolDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep KeyHash 'StakePool c
kh
  toSpecRep (DRepDeposit Credential 'DRepRole c
cred) =
    Credential -> DepositPurpose
Agda.DRepDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential 'DRepRole c
cred
  toSpecRep (GovActionDeposit GovActionId c
gid) =
    (Integer, Integer) -> DepositPurpose
Agda.GovActionDeposit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep GovActionId c
gid