{-# 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 (EraCrypto era)) 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 (EraCrypto era)) Coin
withdrawals <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(Map (RewardAccount (EraCrypto era)) 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 (EraCrypto era)) 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 (EraCrypto era)
p) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PoolCert (EraCrypto era)
p
  toSpecRep (ConwayTxCertGov ConwayGovCert (EraCrypto era)
c) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ConwayGovCert (EraCrypto era)
c
  toSpecRep (ConwayTxCertDeleg ConwayDelegCert (EraCrypto era)
x) = forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ConwayDelegCert (EraCrypto era)
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 (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
    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 (EraCrypto era)) Coin
deposits = forall era.
CertState era
-> Proposals era -> Map (DepositPurpose (EraCrypto era)) 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 (EraCrypto era)) 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 (EraCrypto era)) Coin
deposits = forall era.
CertState era
-> Proposals era -> Map (DepositPurpose (EraCrypto era)) 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 (EraCrypto era)) 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 (EraCrypto era)
AccountState
NonMyopic (EraCrypto era)
esAccountState :: forall era. EpochState era -> AccountState
esSnapshots :: forall era. EpochState era -> SnapShots (EraCrypto era)
esNonMyopic :: forall era. EpochState era -> NonMyopic (EraCrypto era)
esNonMyopic :: NonMyopic (EraCrypto era)
esSnapshots :: SnapShots (EraCrypto era)
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 (EraCrypto era)
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 (EraCrypto era))
-> 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 c) where
  type SpecRep (SnapShots c) = Agda.Snapshots

  toSpecRep :: SnapShots c -> SpecTransM ctx (SpecRep (SnapShots c))
toSpecRep (SnapShots {Coin
SnapShot c
PoolDistr c
$sel:ssStakeMark:SnapShots :: forall c. SnapShots c -> SnapShot c
$sel:ssStakeMarkPoolDistr:SnapShots :: forall c. SnapShots c -> PoolDistr c
$sel:ssStakeSet:SnapShots :: forall c. SnapShots c -> SnapShot c
$sel:ssStakeGo:SnapShots :: forall c. SnapShots c -> SnapShot c
$sel:ssFee:SnapShots :: forall c. SnapShots c -> Coin
ssFee :: Coin
ssStakeGo :: SnapShot c
ssStakeSet :: SnapShot c
ssStakeMarkPoolDistr :: PoolDistr c
ssStakeMark :: SnapShot c
..}) =
    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 c
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 c
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 c
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 c) where
  type SpecRep (SnapShot c) = Agda.Snapshot

  toSpecRep :: SnapShot c -> SpecTransM ctx (SpecRep (SnapShot c))
toSpecRep (SnapShot {Stake c
VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c)
VMap VB VB (KeyHash 'StakePool c) (PoolParams c)
$sel:ssStake:SnapShot :: forall c. SnapShot c -> Stake c
$sel:ssDelegations:SnapShot :: forall c.
SnapShot c
-> VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c)
$sel:ssPoolParams:SnapShot :: forall c.
SnapShot c -> VMap VB VB (KeyHash 'StakePool c) (PoolParams c)
ssPoolParams :: VMap VB VB (KeyHash 'StakePool c) (PoolParams c)
ssDelegations :: VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c)
ssStake :: Stake c
..}) =
    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 c
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 c) (KeyHash 'StakePool c)
ssDelegations)

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

  toSpecRep :: Stake c -> SpecTransM ctx (SpecRep (Stake c))
toSpecRep (Stake VMap VB VP (Credential 'Staking c) (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 c) (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 c) where
  type SpecRep (PulsingRewUpdate c) = Agda.HsRewardUpdate

  toSpecRep :: PulsingRewUpdate c -> SpecTransM ctx (SpecRep (PulsingRewUpdate c))
toSpecRep PulsingRewUpdate c
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 c) Coin
rwds
    where
      (RewardUpdate {RewardEvent c
DeltaCoin
NonMyopic c
deltaT :: forall c. RewardUpdate c -> DeltaCoin
deltaR :: forall c. RewardUpdate c -> DeltaCoin
rs :: forall c.
RewardUpdate c -> Map (Credential 'Staking c) (Set (Reward c))
deltaF :: forall c. RewardUpdate c -> DeltaCoin
nonMyopic :: forall c. RewardUpdate c -> NonMyopic c
nonMyopic :: NonMyopic c
rs :: RewardEvent c
deltaF :: DeltaCoin
deltaR :: DeltaCoin
deltaT :: DeltaCoin
..}, RewardEvent c
_) = forall a. ShelleyBase a -> a
runShelleyBase forall a b. (a -> b) -> a -> b
$ forall c.
PulsingRewUpdate c -> ShelleyBase (RewardUpdate c, RewardEvent c)
completeRupd PulsingRewUpdate c
x
      rwds :: Map (Credential 'Staking c) Coin
rwds = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Set.foldMap forall c. Reward c -> Coin
rewardAmount forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewardEvent c
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 (EraCrypto era))
PoolDistr (EraCrypto era)
BlocksMade (EraCrypto era)
EpochNo
EpochState era
StashedAVVMAddresses era
nesEL :: forall era. NewEpochState era -> EpochNo
nesBprev :: forall era. NewEpochState era -> BlocksMade (EraCrypto era)
nesBcur :: forall era. NewEpochState era -> BlocksMade (EraCrypto era)
nesEs :: forall era. NewEpochState era -> EpochState era
nesRu :: forall era.
NewEpochState era -> StrictMaybe (PulsingRewUpdate (EraCrypto era))
nesPd :: forall era. NewEpochState era -> PoolDistr (EraCrypto era)
stashedAVVMAddresses :: forall era. NewEpochState era -> StashedAVVMAddresses era
stashedAVVMAddresses :: StashedAVVMAddresses era
nesPd :: PoolDistr (EraCrypto era)
nesRu :: StrictMaybe (PulsingRewUpdate (EraCrypto era))
nesEs :: EpochState era
nesBcur :: BlocksMade (EraCrypto era)
nesBprev :: BlocksMade (EraCrypto era)
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 (EraCrypto era))
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
. String -> OpaqueErrorString
OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> Expr
toExpr