{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert () where

import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.CertState
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.EpochBoundary
import Cardano.Ledger.Shelley.LedgerState
import qualified Data.Foldable as Set
import Data.Functor.Identity (Identity)
import Data.Map.Strict (Map)
import qualified Data.VMap as VMap
import Lens.Micro
import qualified Lib as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool ()
import Test.Cardano.Ledger.Constrained.Conway.Utxo (depositsMap)
import Test.Cardano.Ledger.Conway.TreeDiff
import Test.Cardano.Ledger.Shelley.Utils (runShelleyBase)

instance
  ( SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , Inject ctx (VotingProcedures era)
  , Inject ctx (Map RewardAccount Coin)
  ) =>
  SpecTranslate ctx (CertEnv era)
  where
  type SpecRep (CertEnv era) = Agda.CertEnv
  toSpecRep :: CertEnv era -> SpecTransM ctx (SpecRep (CertEnv era))
toSpecRep CertEnv {Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
PParams era
StrictMaybe (Committee era)
EpochNo
cePParams :: forall era. CertEnv era -> PParams era
ceCurrentEpoch :: forall era. CertEnv era -> EpochNo
ceCurrentCommittee :: forall era. CertEnv era -> StrictMaybe (Committee era)
ceCommitteeProposals :: forall era.
CertEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCurrentCommittee :: StrictMaybe (Committee era)
ceCurrentEpoch :: EpochNo
cePParams :: PParams era
..} = do
    VotingProcedures era
votes <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(VotingProcedures era)
    Map RewardAccount Coin
withdrawals <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(Map RewardAccount Coin)
    Integer -> PParams -> [GovVote] -> HSMap RwdAddr Integer -> CertEnv
Agda.MkCertEnv
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
ceCurrentEpoch
      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 PParams era
cePParams
      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 VotingProcedures era
votes
      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 RewardAccount Coin
withdrawals

instance SpecTranslate ctx (CertState era) where
  type SpecRep (CertState era) = Agda.CertState
  toSpecRep :: CertState era -> SpecTransM ctx (SpecRep (CertState era))
toSpecRep CertState {DState era
PState era
VState era
certVState :: forall era. CertState era -> VState era
certPState :: forall era. CertState era -> PState era
certDState :: forall era. CertState era -> DState era
certDState :: DState era
certPState :: PState era
certVState :: VState era
..} =
    DState -> PState -> GState -> CertState
Agda.MkCertState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DState era
certDState
      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 PState era
certPState
      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 VState era
certVState

instance Era era => SpecTranslate ctx (ConwayTxCert era) where
  type SpecRep (ConwayTxCert era) = Agda.DCert

  toSpecRep :: ConwayTxCert era -> SpecTransM ctx (SpecRep (ConwayTxCert era))
toSpecRep (ConwayTxCertPool PoolCert
p) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PoolCert
p
  toSpecRep (ConwayTxCertGov ConwayGovCert
c) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ConwayGovCert
c
  toSpecRep (ConwayTxCertDeleg ConwayDelegCert
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ConwayDelegCert
x

instance
  ( SpecTranslate ctx (TxOut era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  , GovState era ~ ConwayGovState era
  , Inject ctx (CertState 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
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
utxosDonation :: forall era. UTxOState era -> Coin
utxosDonation :: Coin
utxosStakeDistr :: IncrementalStake
utxosGovState :: GovState era
utxosFees :: Coin
utxosDeposited :: Coin
utxosUtxo :: UTxO era
..} = do
    CertState era
certState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(CertState era)
    let
      props :: Proposals era
props = GovState era
utxosGovState forall s a. s -> Getting a s a -> a
^. forall era. Lens' (ConwayGovState era) (Proposals era)
cgsProposalsL
      deposits :: Map DepositPurpose Coin
deposits = forall era.
CertState era -> Proposals era -> Map DepositPurpose Coin
depositsMap CertState era
certState Proposals era
props
    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 Coin
deposits
      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

instance
  ( ConwayEraGov era
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , SpecRep (TxOut era) ~ Agda.TxOut
  , GovState era ~ ConwayGovState era
  , SpecTranslate (CertState era) (TxOut era)
  ) =>
  SpecTranslate ctx (LedgerState era)
  where
  type SpecRep (LedgerState era) = Agda.LState

  toSpecRep :: LedgerState era -> SpecTransM ctx (SpecRep (LedgerState era))
toSpecRep (LedgerState {CertState era
UTxOState era
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsCertState :: forall era. LedgerState era -> CertState era
lsCertState :: CertState era
lsUTxOState :: UTxOState era
..}) = do
    let
      props :: Proposals era
props = forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
lsUTxOState forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraGov era =>
Lens' (GovState era) (Proposals era)
proposalsGovStateL
      deposits :: Map DepositPurpose Coin
deposits = forall era.
CertState era -> Proposals era -> Map DepositPurpose Coin
depositsMap CertState era
lsCertState Proposals era
props
    UTxOState
-> [((Integer, Integer), GovActionState)] -> CertState -> LState
Agda.MkLState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx CertState era
lsCertState (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UTxOState era
lsUTxOState)
      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 Proposals era
props
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx Map DepositPurpose Coin
deposits (forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CertState era
lsCertState)

instance
  ( EraPParams era
  , ConwayEraGov era
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , Inject ctx [GovActionState era]
  , ToExpr (PParamsHKD StrictMaybe era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  , GovState era ~ ConwayGovState era
  , SpecTranslate (CertState era) (TxOut era)
  ) =>
  SpecTranslate ctx (EpochState era)
  where
  type SpecRep (EpochState era) = Agda.EpochState

  toSpecRep :: EpochState era -> SpecTransM ctx (SpecRep (EpochState era))
toSpecRep (EpochState {esLState :: forall era. EpochState era -> LedgerState era
esLState = esLState :: LedgerState era
esLState@LedgerState {UTxOState era
lsUTxOState :: UTxOState era
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsUTxOState}, SnapShots
AccountState
NonMyopic
esAccountState :: forall era. EpochState era -> AccountState
esSnapshots :: forall era. EpochState era -> SnapShots
esNonMyopic :: forall era. EpochState era -> NonMyopic
esNonMyopic :: NonMyopic
esSnapshots :: SnapShots
esAccountState :: AccountState
..}) =
    Acnt
-> Snapshots -> LState -> EnactState -> RatifyState -> EpochState
Agda.MkEpochState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep AccountState
esAccountState
      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 SnapShots
esSnapshots
      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 LedgerState era
esLState
      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 EnactState era
enactState
      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 RatifyState era
ratifyState
    where
      enactState :: EnactState era
enactState = forall era. ConwayEraGov era => GovState era -> EnactState era
mkEnactState forall a b. (a -> b) -> a -> b
$ forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
lsUTxOState
      ratifyState :: RatifyState era
ratifyState = forall era.
EnactState era
-> Seq (GovActionState era)
-> Set GovActionId
-> Bool
-> RatifyState era
RatifyState EnactState era
enactState forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty Bool
False

instance SpecTranslate ctx SnapShots where
  type SpecRep SnapShots = Agda.Snapshots

  toSpecRep :: SnapShots -> SpecTransM ctx (SpecRep SnapShots)
toSpecRep (SnapShots {Coin
SnapShot
PoolDistr
$sel:ssStakeMark:SnapShots :: SnapShots -> SnapShot
$sel:ssStakeMarkPoolDistr:SnapShots :: SnapShots -> PoolDistr
$sel:ssStakeSet:SnapShots :: SnapShots -> SnapShot
$sel:ssStakeGo:SnapShots :: SnapShots -> SnapShot
$sel:ssFee:SnapShots :: SnapShots -> Coin
ssFee :: Coin
ssStakeGo :: SnapShot
ssStakeSet :: SnapShot
ssStakeMarkPoolDistr :: PoolDistr
ssStakeMark :: SnapShot
..}) =
    Snapshot -> Snapshot -> Snapshot -> Integer -> Snapshots
Agda.MkSnapshots
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SnapShot
ssStakeMark
      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 SnapShot
ssStakeSet
      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 SnapShot
ssStakeGo
      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
ssFee

instance SpecTranslate ctx SnapShot where
  type SpecRep SnapShot = Agda.Snapshot

  toSpecRep :: SnapShot -> SpecTransM ctx (SpecRep SnapShot)
toSpecRep (SnapShot {Stake
VMap VB VB (KeyHash 'StakePool) PoolParams
VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
$sel:ssStake:SnapShot :: SnapShot -> Stake
$sel:ssDelegations:SnapShot :: SnapShot -> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
$sel:ssPoolParams:SnapShot :: SnapShot -> VMap VB VB (KeyHash 'StakePool) PoolParams
ssPoolParams :: VMap VB VB (KeyHash 'StakePool) PoolParams
ssDelegations :: VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
ssStake :: Stake
..}) =
    HSMap Credential Integer -> HSMap Credential Integer -> Snapshot
Agda.MkSnapshot
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Stake
ssStake
      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 (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
ssDelegations)

instance SpecTranslate ctx Stake where
  type SpecRep Stake = Agda.HSMap Agda.Credential Agda.Coin

  toSpecRep :: Stake -> SpecTransM ctx (SpecRep Stake)
toSpecRep (Stake VMap VB VP (Credential 'Staking) (CompactForm Coin)
stake) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep forall a b. (a -> b) -> a -> b
$ forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap VMap VB VP (Credential 'Staking) (CompactForm Coin)
stake

instance SpecTranslate ctx AccountState where
  type SpecRep AccountState = Agda.Acnt

  toSpecRep :: AccountState -> SpecTransM ctx (SpecRep AccountState)
toSpecRep (AccountState {Coin
asTreasury :: AccountState -> Coin
asReserves :: AccountState -> Coin
asReserves :: Coin
asTreasury :: Coin
..}) =
    Integer -> Integer -> Acnt
Agda.MkAcnt
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
asTreasury
      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
asReserves

instance SpecTranslate ctx DeltaCoin where
  type SpecRep DeltaCoin = Integer

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

instance SpecTranslate ctx PulsingRewUpdate where
  type SpecRep PulsingRewUpdate = Agda.HsRewardUpdate

  toSpecRep :: PulsingRewUpdate -> SpecTransM ctx (SpecRep PulsingRewUpdate)
toSpecRep PulsingRewUpdate
x =
    Integer
-> Integer -> Integer -> HSMap Credential Integer -> HsRewardUpdate
Agda.MkRewardUpdate
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DeltaCoin
deltaT
      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 DeltaCoin
deltaR
      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 DeltaCoin
deltaF
      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 (Credential 'Staking) Coin
rwds
    where
      (RewardUpdate {RewardEvent
DeltaCoin
NonMyopic
deltaT :: RewardUpdate -> DeltaCoin
deltaR :: RewardUpdate -> DeltaCoin
rs :: RewardUpdate -> RewardEvent
deltaF :: RewardUpdate -> DeltaCoin
nonMyopic :: RewardUpdate -> NonMyopic
nonMyopic :: NonMyopic
rs :: RewardEvent
deltaF :: DeltaCoin
deltaR :: DeltaCoin
deltaT :: DeltaCoin
..}, RewardEvent
_) = forall a. ShelleyBase a -> a
runShelleyBase forall a b. (a -> b) -> a -> b
$ PulsingRewUpdate -> ShelleyBase (RewardUpdate, RewardEvent)
completeRupd PulsingRewUpdate
x
      rwds :: Map (Credential 'Staking) Coin
rwds = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Set.foldMap Reward -> Coin
rewardAmount forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewardEvent
rs

instance
  ( EraPParams era
  , ConwayEraGov era
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , Inject ctx [GovActionState era]
  , ToExpr (PParamsHKD StrictMaybe era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  , GovState era ~ ConwayGovState era
  , SpecTranslate (CertState era) (TxOut era)
  ) =>
  SpecTranslate ctx (NewEpochState era)
  where
  type SpecRep (NewEpochState era) = Agda.NewEpochState

  toSpecRep :: NewEpochState era -> SpecTransM ctx (SpecRep (NewEpochState era))
toSpecRep (NewEpochState {StrictMaybe PulsingRewUpdate
PoolDistr
BlocksMade
EpochNo
EpochState era
StashedAVVMAddresses era
nesEL :: forall era. NewEpochState era -> EpochNo
nesBprev :: forall era. NewEpochState era -> BlocksMade
nesBcur :: forall era. NewEpochState era -> BlocksMade
nesEs :: forall era. NewEpochState era -> EpochState era
nesRu :: forall era. NewEpochState era -> StrictMaybe PulsingRewUpdate
nesPd :: forall era. NewEpochState era -> PoolDistr
stashedAVVMAddresses :: forall era. NewEpochState era -> StashedAVVMAddresses era
stashedAVVMAddresses :: StashedAVVMAddresses era
nesPd :: PoolDistr
nesRu :: StrictMaybe PulsingRewUpdate
nesEs :: EpochState era
nesBcur :: BlocksMade
nesBprev :: BlocksMade
nesEL :: EpochNo
..}) =
    Integer -> EpochState -> Maybe HsRewardUpdate -> NewEpochState
Agda.MkNewEpochState
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
nesEL
      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 EpochState era
nesEs
      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 PulsingRewUpdate
nesRu

instance SpecTranslate ctx (ConwayNewEpochPredFailure era) where
  type SpecRep (ConwayNewEpochPredFailure era) = OpaqueErrorString
  toSpecRep :: ConwayNewEpochPredFailure era
-> SpecTransM ctx (SpecRep (ConwayNewEpochPredFailure era))
toSpecRep = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString