{-# 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.Coin
import Cardano.Ledger.Compactible (Compactible (..))
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Shelley.LedgerState
import qualified Data.Foldable as Set
import Data.Functor.Identity (Identity)
import Data.Map.Strict (Map, keysSet)
import qualified Data.Map.Strict as Map
import qualified Data.OMap.Strict as OMap
import qualified Data.VMap as VMap
import Lens.Micro
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (bimapMHSMap, unionsHSMap)
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.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) (GovActionState era)
StrictMaybe (Committee era)
PParams era
EpochNo
cePParams :: PParams era
ceCurrentEpoch :: EpochNo
ceCurrentCommittee :: StrictMaybe (Committee era)
ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
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) (GovActionState 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)
    let ccColdCreds :: Set (Credential 'ColdCommitteeRole)
ccColdCreds = (Committee era -> Set (Credential 'ColdCommitteeRole))
-> StrictMaybe (Committee era)
-> Set (Credential 'ColdCommitteeRole)
forall m a. Monoid m => (a -> m) -> StrictMaybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Map (Credential 'ColdCommitteeRole) EpochNo
-> Set (Credential 'ColdCommitteeRole)
forall k a. Map k a -> Set k
keysSet (Map (Credential 'ColdCommitteeRole) EpochNo
 -> Set (Credential 'ColdCommitteeRole))
-> (Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo)
-> Committee era
-> Set (Credential 'ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo
forall era.
Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo
committeeMembers) StrictMaybe (Committee era)
ceCurrentCommittee
    Integer
-> PParams
-> [GovVote]
-> HSMap RwdAddr Integer
-> HSSet Credential
-> CertEnv
Agda.MkCertEnv
      (Integer
 -> PParams
 -> [GovVote]
 -> HSMap RwdAddr Integer
 -> HSSet Credential
 -> CertEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (PParams
      -> [GovVote]
      -> HSMap RwdAddr Integer
      -> HSSet Credential
      -> CertEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
ceCurrentEpoch
      SpecTransM
  ctx
  (PParams
   -> [GovVote]
   -> HSMap RwdAddr Integer
   -> HSSet Credential
   -> CertEnv)
-> SpecTransM ctx PParams
-> SpecTransM
     ctx
     ([GovVote] -> HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PParams era -> SpecTransM ctx (SpecRep (PParams era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParams era
cePParams
      SpecTransM
  ctx
  ([GovVote] -> HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
-> SpecTransM ctx [GovVote]
-> SpecTransM
     ctx (HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VotingProcedures era
-> SpecTransM ctx (SpecRep (VotingProcedures era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep VotingProcedures era
votes
      SpecTransM
  ctx (HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
-> SpecTransM ctx (HSMap RwdAddr Integer)
-> SpecTransM ctx (HSSet Credential -> CertEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map RewardAccount Coin
-> SpecTransM ctx (SpecRep (Map RewardAccount Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map RewardAccount Coin
withdrawals
      SpecTransM ctx (HSSet Credential -> CertEnv)
-> SpecTransM ctx (HSSet Credential) -> SpecTransM ctx CertEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (Credential 'ColdCommitteeRole)
-> SpecTransM ctx (SpecRep (Set (Credential 'ColdCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (Credential 'ColdCommitteeRole)
ccColdCreds

instance ConwayEraAccounts era => SpecTranslate ctx (ConwayCertState era) where
  type SpecRep (ConwayCertState era) = Agda.CertState
  toSpecRep :: ConwayCertState era
-> SpecTransM ctx (SpecRep (ConwayCertState era))
toSpecRep ConwayCertState {PState era
DState era
VState era
conwayCertVState :: VState era
conwayCertPState :: PState era
conwayCertDState :: DState era
conwayCertVState :: forall era. ConwayCertState era -> VState era
conwayCertPState :: forall era. ConwayCertState era -> PState era
conwayCertDState :: forall era. ConwayCertState era -> DState era
..} =
    DState -> PState -> GState -> CertState
Agda.MkCertState
      (DState -> PState -> GState -> CertState)
-> SpecTransM ctx DState
-> SpecTransM ctx (PState -> GState -> CertState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DState era -> SpecTransM ctx (SpecRep (DState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DState era
conwayCertDState
      SpecTransM ctx (PState -> GState -> CertState)
-> SpecTransM ctx PState -> SpecTransM ctx (GState -> CertState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PState era -> SpecTransM ctx (SpecRep (PState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PState era
conwayCertPState
      SpecTransM ctx (GState -> CertState)
-> SpecTransM ctx GState -> SpecTransM ctx CertState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VState era -> SpecTransM ctx (SpecRep (VState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep VState era
conwayCertVState

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) = PoolCert -> SpecTransM ctx (SpecRep PoolCert)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PoolCert
p
  toSpecRep (ConwayTxCertGov ConwayGovCert
c) = ConwayGovCert -> SpecTransM ctx (SpecRep ConwayGovCert)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ConwayGovCert
c
  toSpecRep (ConwayTxCertDeleg ConwayDelegCert
x) = ConwayDelegCert -> SpecTransM ctx (SpecRep ConwayDelegCert)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ConwayDelegCert
x

depositsMap ::
  ConwayEraCertState era =>
  CertState era -> Proposals era -> SpecTransM ctx (Agda.HSMap Agda.DepositPurpose Integer)
depositsMap :: forall era ctx.
ConwayEraCertState era =>
CertState era
-> Proposals era -> SpecTransM ctx (HSMap DepositPurpose Integer)
depositsMap CertState era
certState Proposals era
props =
  [HSMap DepositPurpose Integer] -> HSMap DepositPurpose Integer
forall k v. Ord k => [HSMap k v] -> HSMap k v
unionsHSMap
    ([HSMap DepositPurpose Integer] -> HSMap DepositPurpose Integer)
-> SpecTransM ctx [HSMap DepositPurpose Integer]
-> SpecTransM ctx (HSMap DepositPurpose Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecTransM ctx (HSMap DepositPurpose Integer)]
-> SpecTransM ctx [HSMap DepositPurpose Integer]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
      [ (Credential 'Staking -> SpecTransM ctx DepositPurpose)
-> (AccountState era -> SpecTransM ctx Integer)
-> HSMap (Credential 'Staking) (AccountState era)
-> SpecTransM ctx (HSMap DepositPurpose Integer)
forall (m :: * -> *) k k' v v'.
Applicative m =>
(k -> m k') -> (v -> m v') -> HSMap k v -> m (HSMap k' v')
bimapMHSMap
          ((Credential -> DepositPurpose)
-> SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Credential -> DepositPurpose
Agda.CredentialDeposit (SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose)
-> (Credential 'Staking -> SpecTransM ctx Credential)
-> Credential 'Staking
-> SpecTransM ctx DepositPurpose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Credential 'Staking -> SpecTransM ctx Credential
Credential 'Staking
-> SpecTransM ctx (SpecRep (Credential 'Staking))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep)
          (Coin -> SpecTransM ctx Integer
Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Coin -> SpecTransM ctx Integer)
-> (AccountState era -> Coin)
-> AccountState era
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (AccountState era -> CompactForm Coin)
-> AccountState era
-> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
-> AccountState era -> CompactForm Coin
forall a s. Getting a s a -> s -> a
view Getting (CompactForm Coin) (AccountState era) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState era) (CompactForm Coin)
depositAccountStateL)
          ([(Credential 'Staking, AccountState era)]
-> HSMap (Credential 'Staking) (AccountState era)
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(Credential 'Staking, AccountState era)]
 -> HSMap (Credential 'Staking) (AccountState era))
-> (Map (Credential 'Staking) (AccountState era)
    -> [(Credential 'Staking, AccountState era)])
-> Map (Credential 'Staking) (AccountState era)
-> HSMap (Credential 'Staking) (AccountState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Credential 'Staking) (AccountState era)
-> [(Credential 'Staking, AccountState era)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (Credential 'Staking) (AccountState era)
 -> HSMap (Credential 'Staking) (AccountState era))
-> Map (Credential 'Staking) (AccountState era)
-> HSMap (Credential 'Staking) (AccountState era)
forall a b. (a -> b) -> a -> b
$ CertState era
certState CertState era
-> Getting
     (Map (Credential 'Staking) (AccountState era))
     (CertState era)
     (Map (Credential 'Staking) (AccountState era))
-> Map (Credential 'Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (DState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (DState era))
-> CertState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era
  -> Const
       (Map (Credential 'Staking) (AccountState era)) (DState era))
 -> CertState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (CertState era))
-> ((Map (Credential 'Staking) (AccountState era)
     -> Const
          (Map (Credential 'Staking) (AccountState era))
          (Map (Credential 'Staking) (AccountState era)))
    -> DState era
    -> Const
         (Map (Credential 'Staking) (AccountState era)) (DState era))
-> Getting
     (Map (Credential 'Staking) (AccountState era))
     (CertState era)
     (Map (Credential 'Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((Accounts era
  -> Const
       (Map (Credential 'Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential 'Staking) (AccountState era)) (DState era))
-> ((Map (Credential 'Staking) (AccountState era)
     -> Const
          (Map (Credential 'Staking) (AccountState era))
          (Map (Credential 'Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential 'Staking) (AccountState era)) (Accounts era))
-> (Map (Credential 'Staking) (AccountState era)
    -> Const
         (Map (Credential 'Staking) (AccountState era))
         (Map (Credential 'Staking) (AccountState era)))
-> DState era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'Staking) (AccountState era)
 -> Const
      (Map (Credential 'Staking) (AccountState era))
      (Map (Credential 'Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential 'Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential 'Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential 'Staking) (AccountState era))
accountsMapL)
      , (KeyHash 'StakePool -> SpecTransM ctx DepositPurpose)
-> (Coin -> SpecTransM ctx Integer)
-> HSMap (KeyHash 'StakePool) Coin
-> SpecTransM ctx (HSMap DepositPurpose Integer)
forall (m :: * -> *) k k' v v'.
Applicative m =>
(k -> m k') -> (v -> m v') -> HSMap k v -> m (HSMap k' v')
bimapMHSMap
          ((Integer -> DepositPurpose)
-> SpecTransM ctx Integer -> SpecTransM ctx DepositPurpose
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> DepositPurpose
Agda.PoolDeposit (SpecTransM ctx Integer -> SpecTransM ctx DepositPurpose)
-> (KeyHash 'StakePool -> SpecTransM ctx Integer)
-> KeyHash 'StakePool
-> SpecTransM ctx DepositPurpose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KeyHash 'StakePool -> SpecTransM ctx Integer
KeyHash 'StakePool -> SpecTransM ctx (SpecRep (KeyHash 'StakePool))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep)
          Coin -> SpecTransM ctx Integer
Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep
          ([(KeyHash 'StakePool, Coin)] -> HSMap (KeyHash 'StakePool) Coin
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(KeyHash 'StakePool, Coin)] -> HSMap (KeyHash 'StakePool) Coin)
-> (Map (KeyHash 'StakePool) Coin -> [(KeyHash 'StakePool, Coin)])
-> Map (KeyHash 'StakePool) Coin
-> HSMap (KeyHash 'StakePool) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (KeyHash 'StakePool) Coin -> [(KeyHash 'StakePool, Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (KeyHash 'StakePool) Coin -> HSMap (KeyHash 'StakePool) Coin)
-> Map (KeyHash 'StakePool) Coin -> HSMap (KeyHash 'StakePool) Coin
forall a b. (a -> b) -> a -> b
$ CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (StakePoolState -> CompactForm Coin) -> StakePoolState -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StakePoolState -> CompactForm Coin
spsDeposit (StakePoolState -> Coin)
-> Map (KeyHash 'StakePool) StakePoolState
-> Map (KeyHash 'StakePool) Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CertState era
certState CertState era
-> Getting
     (Map (KeyHash 'StakePool) StakePoolState)
     (CertState era)
     (Map (KeyHash 'StakePool) StakePoolState)
-> Map (KeyHash 'StakePool) StakePoolState
forall s a. s -> Getting a s a -> a
^. (PState era
 -> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era
  -> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era))
-> ((Map (KeyHash 'StakePool) StakePoolState
     -> Const
          (Map (KeyHash 'StakePool) StakePoolState)
          (Map (KeyHash 'StakePool) StakePoolState))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era))
-> Getting
     (Map (KeyHash 'StakePool) StakePoolState)
     (CertState era)
     (Map (KeyHash 'StakePool) StakePoolState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) StakePoolState
 -> Const
      (Map (KeyHash 'StakePool) StakePoolState)
      (Map (KeyHash 'StakePool) StakePoolState))
-> PState era
-> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) StakePoolState
 -> f (Map (KeyHash 'StakePool) StakePoolState))
-> PState era -> f (PState era)
psStakePoolsL)
      , (Credential 'DRepRole -> SpecTransM ctx DepositPurpose)
-> (DRepState -> SpecTransM ctx Integer)
-> HSMap (Credential 'DRepRole) DRepState
-> SpecTransM ctx (HSMap DepositPurpose Integer)
forall (m :: * -> *) k k' v v'.
Applicative m =>
(k -> m k') -> (v -> m v') -> HSMap k v -> m (HSMap k' v')
bimapMHSMap
          ((Credential -> DepositPurpose)
-> SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Credential -> DepositPurpose
Agda.DRepDeposit (SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose)
-> (Credential 'DRepRole -> SpecTransM ctx Credential)
-> Credential 'DRepRole
-> SpecTransM ctx DepositPurpose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Credential 'DRepRole -> SpecTransM ctx Credential
Credential 'DRepRole
-> SpecTransM ctx (SpecRep (Credential 'DRepRole))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep)
          (CompactForm Coin -> SpecTransM ctx Integer
CompactForm Coin -> SpecTransM ctx (SpecRep (CompactForm Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (CompactForm Coin -> SpecTransM ctx Integer)
-> (DRepState -> CompactForm Coin)
-> DRepState
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DRepState -> CompactForm Coin
drepDeposit)
          ([(Credential 'DRepRole, DRepState)]
-> HSMap (Credential 'DRepRole) DRepState
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(Credential 'DRepRole, DRepState)]
 -> HSMap (Credential 'DRepRole) DRepState)
-> (Map (Credential 'DRepRole) DRepState
    -> [(Credential 'DRepRole, DRepState)])
-> Map (Credential 'DRepRole) DRepState
-> HSMap (Credential 'DRepRole) DRepState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Credential 'DRepRole) DRepState
-> [(Credential 'DRepRole, DRepState)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (Credential 'DRepRole) DRepState
 -> HSMap (Credential 'DRepRole) DRepState)
-> Map (Credential 'DRepRole) DRepState
-> HSMap (Credential 'DRepRole) DRepState
forall a b. (a -> b) -> a -> b
$ CertState era
certState CertState era
-> Getting
     (Map (Credential 'DRepRole) DRepState)
     (CertState era)
     (Map (Credential 'DRepRole) DRepState)
-> Map (Credential 'DRepRole) DRepState
forall s a. s -> Getting a s a -> a
^. (VState era
 -> Const (Map (Credential 'DRepRole) DRepState) (VState era))
-> CertState era
-> Const (Map (Credential 'DRepRole) DRepState) (CertState era)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState era) (VState era)
certVStateL ((VState era
  -> Const (Map (Credential 'DRepRole) DRepState) (VState era))
 -> CertState era
 -> Const (Map (Credential 'DRepRole) DRepState) (CertState era))
-> ((Map (Credential 'DRepRole) DRepState
     -> Const
          (Map (Credential 'DRepRole) DRepState)
          (Map (Credential 'DRepRole) DRepState))
    -> VState era
    -> Const (Map (Credential 'DRepRole) DRepState) (VState era))
-> Getting
     (Map (Credential 'DRepRole) DRepState)
     (CertState era)
     (Map (Credential 'DRepRole) DRepState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'DRepRole) DRepState
 -> Const
      (Map (Credential 'DRepRole) DRepState)
      (Map (Credential 'DRepRole) DRepState))
-> VState era
-> Const (Map (Credential 'DRepRole) DRepState) (VState era)
forall era (f :: * -> *).
Functor f =>
(Map (Credential 'DRepRole) DRepState
 -> f (Map (Credential 'DRepRole) DRepState))
-> VState era -> f (VState era)
vsDRepsL)
      , (GovActionId -> SpecTransM ctx DepositPurpose)
-> (GovActionState era -> SpecTransM ctx Integer)
-> HSMap GovActionId (GovActionState era)
-> SpecTransM ctx (HSMap DepositPurpose Integer)
forall (m :: * -> *) k k' v v'.
Applicative m =>
(k -> m k') -> (v -> m v') -> HSMap k v -> m (HSMap k' v')
bimapMHSMap
          (((Integer, Integer) -> DepositPurpose)
-> SpecTransM ctx (Integer, Integer)
-> SpecTransM ctx DepositPurpose
forall a b. (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer, Integer) -> DepositPurpose
Agda.GovActionDeposit (SpecTransM ctx (Integer, Integer)
 -> SpecTransM ctx DepositPurpose)
-> (GovActionId -> SpecTransM ctx (Integer, Integer))
-> GovActionId
-> SpecTransM ctx DepositPurpose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionId -> SpecTransM ctx (Integer, Integer)
GovActionId -> SpecTransM ctx (SpecRep GovActionId)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep)
          (Coin -> SpecTransM ctx Integer
Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Coin -> SpecTransM ctx Integer)
-> (GovActionState era -> Coin)
-> GovActionState era
-> SpecTransM ctx Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionState era -> Coin
forall era. GovActionState era -> Coin
gasDeposit)
          ([(GovActionId, GovActionState era)]
-> HSMap GovActionId (GovActionState era)
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(GovActionId, GovActionState era)]
 -> HSMap GovActionId (GovActionState era))
-> (OMap GovActionId (GovActionState era)
    -> [(GovActionId, GovActionState era)])
-> OMap GovActionId (GovActionState era)
-> HSMap GovActionId (GovActionState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState era)
-> [(GovActionId, GovActionState era)]
forall k v. Ord k => OMap k v -> [(k, v)]
OMap.assocList (OMap GovActionId (GovActionState era)
 -> HSMap GovActionId (GovActionState era))
-> OMap GovActionId (GovActionState era)
-> HSMap GovActionId (GovActionState era)
forall a b. (a -> b) -> a -> b
$ Proposals era
props Proposals era
-> Getting
     (OMap GovActionId (GovActionState era))
     (Proposals era)
     (OMap GovActionId (GovActionState era))
-> OMap GovActionId (GovActionState era)
forall s a. s -> Getting a s a -> a
^. Getting
  (OMap GovActionId (GovActionState era))
  (Proposals era)
  (OMap GovActionId (GovActionState era))
forall era (f :: * -> *).
Functor f =>
(OMap GovActionId (GovActionState era)
 -> f (OMap GovActionId (GovActionState era)))
-> Proposals era -> f (Proposals era)
pPropsL)
      ]

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

  toSpecRep :: UTxOState era -> SpecTransM ctx (SpecRep (UTxOState era))
toSpecRep UTxOState {GovState era
UTxO era
InstantStake era
Coin
utxosUtxo :: UTxO era
utxosDeposited :: Coin
utxosFees :: Coin
utxosGovState :: GovState era
utxosInstantStake :: InstantStake era
utxosDonation :: Coin
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
utxosInstantStake :: forall era. UTxOState era -> InstantStake era
utxosDonation :: forall era. UTxOState era -> Coin
..} = do
    CertState era
certState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(CertState era)
    let
      props :: Proposals era
props = GovState era
ConwayGovState era
utxosGovState ConwayGovState era
-> Getting (Proposals era) (ConwayGovState era) (Proposals era)
-> Proposals era
forall s a. s -> Getting a s a -> a
^. Getting (Proposals era) (ConwayGovState era) (Proposals era)
forall era (f :: * -> *).
Functor f =>
(Proposals era -> f (Proposals era))
-> ConwayGovState era -> f (ConwayGovState era)
cgsProposalsL
      deposits :: SpecTransM ctx (HSMap DepositPurpose Integer)
deposits = CertState era
-> Proposals era -> SpecTransM ctx (HSMap DepositPurpose Integer)
forall era ctx.
ConwayEraCertState era =>
CertState era
-> Proposals era -> SpecTransM ctx (HSMap DepositPurpose Integer)
depositsMap CertState era
certState Proposals era
props
    HSMap (Integer, Integer) TxOut
-> Integer -> HSMap DepositPurpose Integer -> Integer -> UTxOState
Agda.MkUTxOState
      (HSMap (Integer, Integer) TxOut
 -> Integer -> HSMap DepositPurpose Integer -> Integer -> UTxOState)
-> SpecTransM ctx (HSMap (Integer, Integer) TxOut)
-> SpecTransM
     ctx
     (Integer -> HSMap DepositPurpose Integer -> Integer -> UTxOState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UTxO era -> SpecTransM ctx (SpecRep (UTxO era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UTxO era
utxosUtxo
      SpecTransM
  ctx
  (Integer -> HSMap DepositPurpose Integer -> Integer -> UTxOState)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (HSMap DepositPurpose Integer -> Integer -> UTxOState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
utxosFees
      SpecTransM
  ctx (HSMap DepositPurpose Integer -> Integer -> UTxOState)
-> SpecTransM ctx (HSMap DepositPurpose Integer)
-> SpecTransM ctx (Integer -> UTxOState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ctx (HSMap DepositPurpose Integer)
deposits
      SpecTransM ctx (Integer -> UTxOState)
-> SpecTransM ctx Integer -> SpecTransM ctx UTxOState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
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)
  , SpecRep (CertState era) ~ Agda.CertState
  , ConwayEraCertState era
  , CertState era ~ ConwayCertState 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 :: UTxOState era
lsCertState :: CertState era
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsCertState :: forall era. LedgerState era -> CertState era
..}) = do
    let
      props :: Proposals era
props = UTxOState era -> GovState era
forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
lsUTxOState ConwayGovState era
-> Getting (Proposals era) (ConwayGovState era) (Proposals era)
-> Proposals era
forall s a. s -> Getting a s a -> a
^. (Proposals era -> Const (Proposals era) (Proposals era))
-> GovState era -> Const (Proposals era) (GovState era)
Getting (Proposals era) (ConwayGovState era) (Proposals era)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Proposals era)
Lens' (GovState era) (Proposals era)
proposalsGovStateL
      deposits :: SpecTransM Any (HSMap DepositPurpose Integer)
deposits = CertState era
-> Proposals era -> SpecTransM Any (HSMap DepositPurpose Integer)
forall era ctx.
ConwayEraCertState era =>
CertState era
-> Proposals era -> SpecTransM ctx (HSMap DepositPurpose Integer)
depositsMap CertState era
lsCertState Proposals era
props
    UTxOState
-> [((Integer, Integer), GovActionState)] -> CertState -> LState
Agda.MkLState
      (UTxOState
 -> [((Integer, Integer), GovActionState)] -> CertState -> LState)
-> SpecTransM ctx UTxOState
-> SpecTransM
     ctx ([((Integer, Integer), GovActionState)] -> CertState -> LState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConwayCertState era
-> SpecTransM (ConwayCertState era) UTxOState
-> SpecTransM ctx UTxOState
forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx CertState era
ConwayCertState era
lsCertState (UTxOState era
-> SpecTransM (ConwayCertState era) (SpecRep (UTxOState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UTxOState era
lsUTxOState)
      SpecTransM
  ctx ([((Integer, Integer), GovActionState)] -> CertState -> LState)
-> SpecTransM ctx [((Integer, Integer), GovActionState)]
-> SpecTransM ctx (CertState -> LState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Proposals era -> SpecTransM ctx (SpecRep (Proposals era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Proposals era
props
      SpecTransM ctx (CertState -> LState)
-> SpecTransM ctx CertState -> SpecTransM ctx LState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM Any (HSMap DepositPurpose Integer)
-> SpecTransM
     (SpecTransM Any (HSMap DepositPurpose Integer)) CertState
-> SpecTransM ctx CertState
forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx SpecTransM Any (HSMap DepositPurpose Integer)
deposits (ConwayCertState era
-> SpecTransM
     (SpecTransM Any (HSMap DepositPurpose Integer))
     (SpecRep (ConwayCertState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CertState era
ConwayCertState 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)
  , SpecRep (CertState era) ~ Agda.CertState
  , ConwayEraCertState era
  , CertState era ~ ConwayCertState 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 :: forall era. LedgerState era -> UTxOState era
lsUTxOState :: UTxOState era
lsUTxOState}, ChainAccountState
SnapShots
NonMyopic
esChainAccountState :: ChainAccountState
esSnapshots :: SnapShots
esNonMyopic :: NonMyopic
esChainAccountState :: forall era. EpochState era -> ChainAccountState
esSnapshots :: forall era. EpochState era -> SnapShots
esNonMyopic :: forall era. EpochState era -> NonMyopic
..}) =
    Acnt
-> Snapshots -> LState -> EnactState -> RatifyState -> EpochState
Agda.MkEpochState
      (Acnt
 -> Snapshots -> LState -> EnactState -> RatifyState -> EpochState)
-> SpecTransM ctx Acnt
-> SpecTransM
     ctx
     (Snapshots -> LState -> EnactState -> RatifyState -> EpochState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ChainAccountState -> SpecTransM ctx (SpecRep ChainAccountState)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ChainAccountState
esChainAccountState
      SpecTransM
  ctx
  (Snapshots -> LState -> EnactState -> RatifyState -> EpochState)
-> SpecTransM ctx Snapshots
-> SpecTransM
     ctx (LState -> EnactState -> RatifyState -> EpochState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SnapShots -> SpecTransM ctx (SpecRep SnapShots)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SnapShots
esSnapshots
      SpecTransM ctx (LState -> EnactState -> RatifyState -> EpochState)
-> SpecTransM ctx LState
-> SpecTransM ctx (EnactState -> RatifyState -> EpochState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> LedgerState era -> SpecTransM ctx (SpecRep (LedgerState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep LedgerState era
esLState
      SpecTransM ctx (EnactState -> RatifyState -> EpochState)
-> SpecTransM ctx EnactState
-> SpecTransM ctx (RatifyState -> EpochState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EnactState era -> SpecTransM ctx (SpecRep (EnactState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EnactState era
enactState
      SpecTransM ctx (RatifyState -> EpochState)
-> SpecTransM ctx RatifyState -> SpecTransM ctx EpochState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RatifyState era -> SpecTransM ctx (SpecRep (RatifyState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep RatifyState era
ratifyState
    where
      enactState :: EnactState era
enactState = GovState era -> EnactState era
forall era. ConwayEraGov era => GovState era -> EnactState era
mkEnactState (GovState era -> EnactState era) -> GovState era -> EnactState era
forall a b. (a -> b) -> a -> b
$ UTxOState era -> GovState era
forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
lsUTxOState
      ratifyState :: RatifyState era
ratifyState = EnactState era
-> Seq (GovActionState era)
-> Set GovActionId
-> Bool
-> RatifyState era
forall era.
EnactState era
-> Seq (GovActionState era)
-> Set GovActionId
-> Bool
-> RatifyState era
RatifyState EnactState era
enactState Seq (GovActionState era)
forall a. Monoid a => a
mempty Set GovActionId
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 {PoolDistr
SnapShot
Coin
ssStakeMark :: SnapShot
ssStakeMarkPoolDistr :: PoolDistr
ssStakeSet :: SnapShot
ssStakeGo :: SnapShot
ssFee :: Coin
$sel:ssFee:SnapShots :: SnapShots -> Coin
$sel:ssStakeGo:SnapShots :: SnapShots -> SnapShot
$sel:ssStakeMark:SnapShots :: SnapShots -> SnapShot
$sel:ssStakeMarkPoolDistr:SnapShots :: SnapShots -> PoolDistr
$sel:ssStakeSet:SnapShots :: SnapShots -> SnapShot
..}) =
    Snapshot -> Snapshot -> Snapshot -> Integer -> Snapshots
Agda.MkSnapshots
      (Snapshot -> Snapshot -> Snapshot -> Integer -> Snapshots)
-> SpecTransM ctx Snapshot
-> SpecTransM ctx (Snapshot -> Snapshot -> Integer -> Snapshots)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnapShot -> SpecTransM ctx (SpecRep SnapShot)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SnapShot
ssStakeMark
      SpecTransM ctx (Snapshot -> Snapshot -> Integer -> Snapshots)
-> SpecTransM ctx Snapshot
-> SpecTransM ctx (Snapshot -> Integer -> Snapshots)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SnapShot -> SpecTransM ctx (SpecRep SnapShot)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SnapShot
ssStakeSet
      SpecTransM ctx (Snapshot -> Integer -> Snapshots)
-> SpecTransM ctx Snapshot -> SpecTransM ctx (Integer -> Snapshots)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SnapShot -> SpecTransM ctx (SpecRep SnapShot)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SnapShot
ssStakeGo
      SpecTransM ctx (Integer -> Snapshots)
-> SpecTransM ctx Integer -> SpecTransM ctx Snapshots
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
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)
ssStake :: Stake
ssDelegations :: VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
ssPoolParams :: VMap VB VB (KeyHash 'StakePool) PoolParams
$sel:ssDelegations:SnapShot :: SnapShot -> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
$sel:ssPoolParams:SnapShot :: SnapShot -> VMap VB VB (KeyHash 'StakePool) PoolParams
$sel:ssStake:SnapShot :: SnapShot -> Stake
..}) =
    HSMap Credential Integer -> HSMap Credential Integer -> Snapshot
Agda.MkSnapshot
      (HSMap Credential Integer -> HSMap Credential Integer -> Snapshot)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM ctx (HSMap Credential Integer -> Snapshot)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Stake -> SpecTransM ctx (SpecRep Stake)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Stake
ssStake
      SpecTransM ctx (HSMap Credential Integer -> Snapshot)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM ctx Snapshot
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (Credential 'Staking) (KeyHash 'StakePool)
-> SpecTransM
     ctx (SpecRep (Map (Credential 'Staking) (KeyHash 'StakePool)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
-> Map (Credential 'Staking) (KeyHash 'StakePool)
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) = Map (Credential 'Staking) (CompactForm Coin)
-> SpecTransM
     ctx (SpecRep (Map (Credential 'Staking) (CompactForm Coin)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map (Credential 'Staking) (CompactForm Coin)
 -> SpecTransM
      ctx (SpecRep (Map (Credential 'Staking) (CompactForm Coin))))
-> Map (Credential 'Staking) (CompactForm Coin)
-> SpecTransM
     ctx (SpecRep (Map (Credential 'Staking) (CompactForm Coin)))
forall a b. (a -> b) -> a -> b
$ VMap VB VP (Credential 'Staking) (CompactForm Coin)
-> Map (Credential 'Staking) (CompactForm Coin)
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 ChainAccountState where
  type SpecRep ChainAccountState = Agda.Acnt

  toSpecRep :: ChainAccountState -> SpecTransM ctx (SpecRep ChainAccountState)
toSpecRep (ChainAccountState {Coin
casTreasury :: Coin
casReserves :: Coin
casTreasury :: ChainAccountState -> Coin
casReserves :: ChainAccountState -> Coin
..}) =
    Integer -> Integer -> Acnt
Agda.MkAcnt
      (Integer -> Integer -> Acnt)
-> SpecTransM ctx Integer -> SpecTransM ctx (Integer -> Acnt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
casTreasury
      SpecTransM ctx (Integer -> Acnt)
-> SpecTransM ctx Integer -> SpecTransM ctx Acnt
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
casReserves

instance SpecTranslate ctx DeltaCoin where
  type SpecRep DeltaCoin = Integer

  toSpecRep :: DeltaCoin -> SpecTransM ctx (SpecRep DeltaCoin)
toSpecRep (DeltaCoin Integer
x) = Integer -> SpecTransM ctx Integer
forall a. a -> SpecTransM ctx a
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
      (Integer
 -> Integer
 -> Integer
 -> HSMap Credential Integer
 -> HsRewardUpdate)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (Integer -> Integer -> HSMap Credential Integer -> HsRewardUpdate)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeltaCoin -> SpecTransM ctx (SpecRep DeltaCoin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DeltaCoin
deltaT
      SpecTransM
  ctx
  (Integer -> Integer -> HSMap Credential Integer -> HsRewardUpdate)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (Integer -> HSMap Credential Integer -> HsRewardUpdate)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DeltaCoin -> SpecTransM ctx (SpecRep DeltaCoin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DeltaCoin
deltaR
      SpecTransM
  ctx (Integer -> HSMap Credential Integer -> HsRewardUpdate)
-> SpecTransM ctx Integer
-> SpecTransM ctx (HSMap Credential Integer -> HsRewardUpdate)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DeltaCoin -> SpecTransM ctx (SpecRep DeltaCoin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DeltaCoin
deltaF
      SpecTransM ctx (HSMap Credential Integer -> HsRewardUpdate)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM ctx HsRewardUpdate
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (Credential 'Staking) Coin
-> SpecTransM ctx (SpecRep (Map (Credential 'Staking) Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map (Credential 'Staking) Coin
rwds
    where
      (RewardUpdate {RewardEvent
DeltaCoin
NonMyopic
deltaT :: DeltaCoin
deltaR :: DeltaCoin
deltaF :: DeltaCoin
rs :: RewardEvent
nonMyopic :: NonMyopic
deltaT :: RewardUpdate -> DeltaCoin
deltaR :: RewardUpdate -> DeltaCoin
rs :: RewardUpdate -> RewardEvent
deltaF :: RewardUpdate -> DeltaCoin
nonMyopic :: RewardUpdate -> NonMyopic
..}, RewardEvent
_) = ShelleyBase (RewardUpdate, RewardEvent)
-> (RewardUpdate, RewardEvent)
forall a. ShelleyBase a -> a
runShelleyBase (ShelleyBase (RewardUpdate, RewardEvent)
 -> (RewardUpdate, RewardEvent))
-> ShelleyBase (RewardUpdate, RewardEvent)
-> (RewardUpdate, RewardEvent)
forall a b. (a -> b) -> a -> b
$ PulsingRewUpdate -> ShelleyBase (RewardUpdate, RewardEvent)
completeRupd PulsingRewUpdate
x
      rwds :: Map (Credential 'Staking) Coin
rwds = (Reward -> Coin) -> Set Reward -> Coin
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Set.foldMap Reward -> Coin
rewardAmount (Set Reward -> Coin)
-> RewardEvent -> Map (Credential 'Staking) Coin
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)
  , SpecRep (CertState era) ~ Agda.CertState
  , ConwayEraCertState era
  , CertState era ~ ConwayCertState 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
EpochNo
BlocksMade
StashedAVVMAddresses era
EpochState era
nesEL :: EpochNo
nesBprev :: BlocksMade
nesBcur :: BlocksMade
nesEs :: EpochState era
nesRu :: StrictMaybe PulsingRewUpdate
nesPd :: PoolDistr
stashedAVVMAddresses :: 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
..}) =
    Integer -> EpochState -> Maybe HsRewardUpdate -> NewEpochState
Agda.MkNewEpochState
      (Integer -> EpochState -> Maybe HsRewardUpdate -> NewEpochState)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (EpochState -> Maybe HsRewardUpdate -> NewEpochState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
nesEL
      SpecTransM
  ctx (EpochState -> Maybe HsRewardUpdate -> NewEpochState)
-> SpecTransM ctx EpochState
-> SpecTransM ctx (Maybe HsRewardUpdate -> NewEpochState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochState era -> SpecTransM ctx (SpecRep (EpochState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochState era
nesEs
      SpecTransM ctx (Maybe HsRewardUpdate -> NewEpochState)
-> SpecTransM ctx (Maybe HsRewardUpdate)
-> SpecTransM ctx NewEpochState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe PulsingRewUpdate
-> SpecTransM ctx (SpecRep (StrictMaybe PulsingRewUpdate))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe PulsingRewUpdate
nesRu