{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert () where import Cardano.Ledger.Address (RewardAccount) import Cardano.Ledger.BaseTypes import Cardano.Ledger.Coin (Coin (..)) import Cardano.Ledger.Conway.Core import Cardano.Ledger.Conway.Governance import Cardano.Ledger.Conway.Rules (ConwayGovCertEnv (..)) import Cardano.Ledger.Conway.State import Cardano.Ledger.Conway.TxCert (ConwayGovCert (..)) import Cardano.Ledger.Credential (Credential (..)) import Data.Default (Default (..)) import Data.Functor.Identity (Identity) import Data.Map.Strict (Map, keysSet) import qualified Data.Map.Strict as Map import Data.Maybe (mapMaybe) import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base import Test.Cardano.Ledger.Conformance.SpecTranslate.Core instance SpecTranslate ctx ConwayGovCert where type SpecRep ConwayGovCert = Agda.DCert toSpecRep :: ConwayGovCert -> SpecTransM ctx (SpecRep ConwayGovCert) toSpecRep (ConwayRegDRep Credential 'DRepRole c Coin d StrictMaybe Anchor a) = Credential -> Integer -> Anchor -> DCert Agda.Regdrep (Credential -> Integer -> Anchor -> DCert) -> SpecTransM ctx Credential -> SpecTransM ctx (Integer -> Anchor -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Credential 'DRepRole -> SpecTransM ctx (SpecRep (Credential 'DRepRole)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'DRepRole c SpecTransM ctx (Integer -> Anchor -> DCert) -> SpecTransM ctx Integer -> SpecTransM ctx (Anchor -> DCert) 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 d SpecTransM ctx (Anchor -> DCert) -> SpecTransM ctx Anchor -> SpecTransM ctx DCert 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 <*> Anchor -> SpecTransM ctx (SpecRep Anchor) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (Anchor -> StrictMaybe Anchor -> Anchor forall a. a -> StrictMaybe a -> a fromSMaybe Anchor forall a. Default a => a def StrictMaybe Anchor a) toSpecRep (ConwayUnRegDRep Credential 'DRepRole c Coin d) = Credential -> Integer -> DCert Agda.Deregdrep (Credential -> Integer -> DCert) -> SpecTransM ctx Credential -> SpecTransM ctx (Integer -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Credential 'DRepRole -> SpecTransM ctx (SpecRep (Credential 'DRepRole)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'DRepRole c SpecTransM ctx (Integer -> DCert) -> SpecTransM ctx Integer -> SpecTransM ctx DCert 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 d toSpecRep (ConwayUpdateDRep Credential 'DRepRole c StrictMaybe Anchor a) = Credential -> Integer -> Anchor -> DCert Agda.Regdrep (Credential -> Integer -> Anchor -> DCert) -> SpecTransM ctx Credential -> SpecTransM ctx (Integer -> Anchor -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Credential 'DRepRole -> SpecTransM ctx (SpecRep (Credential 'DRepRole)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'DRepRole c SpecTransM ctx (Integer -> Anchor -> DCert) -> SpecTransM ctx Integer -> SpecTransM ctx (Anchor -> DCert) 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 <*> Integer -> SpecTransM ctx Integer forall a. a -> SpecTransM ctx a forall (f :: * -> *) a. Applicative f => a -> f a pure Integer 0 SpecTransM ctx (Anchor -> DCert) -> SpecTransM ctx Anchor -> SpecTransM ctx DCert 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 <*> Anchor -> SpecTransM ctx (SpecRep Anchor) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (Anchor -> StrictMaybe Anchor -> Anchor forall a. a -> StrictMaybe a -> a fromSMaybe Anchor forall a. Default a => a def StrictMaybe Anchor a) toSpecRep (ConwayAuthCommitteeHotKey Credential 'ColdCommitteeRole c Credential 'HotCommitteeRole h) = Credential -> Maybe Credential -> DCert Agda.Ccreghot (Credential -> Maybe Credential -> DCert) -> SpecTransM ctx Credential -> SpecTransM ctx (Maybe Credential -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Credential 'ColdCommitteeRole -> SpecTransM ctx (SpecRep (Credential 'ColdCommitteeRole)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'ColdCommitteeRole c SpecTransM ctx (Maybe Credential -> DCert) -> SpecTransM ctx (Maybe Credential) -> SpecTransM ctx DCert 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 (Credential 'HotCommitteeRole) -> SpecTransM ctx (SpecRep (StrictMaybe (Credential 'HotCommitteeRole))) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (Credential 'HotCommitteeRole -> StrictMaybe (Credential 'HotCommitteeRole) forall a. a -> StrictMaybe a SJust Credential 'HotCommitteeRole h) toSpecRep (ConwayResignCommitteeColdKey Credential 'ColdCommitteeRole c StrictMaybe Anchor _) = Credential -> Maybe Credential -> DCert Agda.Ccreghot (Credential -> Maybe Credential -> DCert) -> SpecTransM ctx Credential -> SpecTransM ctx (Maybe Credential -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Credential 'ColdCommitteeRole -> SpecTransM ctx (SpecRep (Credential 'ColdCommitteeRole)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Credential 'ColdCommitteeRole c SpecTransM ctx (Maybe Credential -> DCert) -> SpecTransM ctx (Maybe Credential) -> SpecTransM ctx DCert 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 (Credential Any) -> SpecTransM ctx (SpecRep (StrictMaybe (Credential Any))) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (forall a. StrictMaybe a SNothing @(Credential _)) instance ( SpecTranslate ctx (PParamsHKD Identity era) , SpecRep (PParamsHKD Identity era) ~ Agda.PParams , Inject ctx (VotingProcedures era) , Inject ctx (Map RewardAccount Coin) ) => SpecTranslate ctx (ConwayGovCertEnv era) where type SpecRep (ConwayGovCertEnv era) = Agda.CertEnv toSpecRep :: ConwayGovCertEnv era -> SpecTransM ctx (SpecRep (ConwayGovCertEnv era)) toSpecRep ConwayGovCertEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState era) StrictMaybe (Committee era) PParams era EpochNo cgcePParams :: PParams era cgceCurrentEpoch :: EpochNo cgceCurrentCommittee :: StrictMaybe (Committee era) cgceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState era) cgcePParams :: forall era. ConwayGovCertEnv era -> PParams era cgceCurrentEpoch :: forall era. ConwayGovCertEnv era -> EpochNo cgceCurrentCommittee :: forall era. ConwayGovCertEnv era -> StrictMaybe (Committee era) cgceCommitteeProposals :: forall era. ConwayGovCertEnv 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 propGetCCMembers :: GovAction era -> Maybe (Set (Credential 'ColdCommitteeRole)) propGetCCMembers (UpdateCommittee StrictMaybe (GovPurposeId 'CommitteePurpose) _ Set (Credential 'ColdCommitteeRole) _ Map (Credential 'ColdCommitteeRole) EpochNo x UnitInterval _) = Set (Credential 'ColdCommitteeRole) -> Maybe (Set (Credential 'ColdCommitteeRole)) forall a. a -> Maybe a Just (Set (Credential 'ColdCommitteeRole) -> Maybe (Set (Credential 'ColdCommitteeRole))) -> Set (Credential 'ColdCommitteeRole) -> Maybe (Set (Credential 'ColdCommitteeRole)) forall a b. (a -> b) -> a -> b $ Map (Credential 'ColdCommitteeRole) EpochNo -> Set (Credential 'ColdCommitteeRole) forall k a. Map k a -> Set k keysSet Map (Credential 'ColdCommitteeRole) EpochNo x propGetCCMembers GovAction era _ = Maybe (Set (Credential 'ColdCommitteeRole)) forall a. Maybe a Nothing potentialCCMembers :: Map k (GovActionState era) -> Set (Credential 'ColdCommitteeRole) potentialCCMembers = [Set (Credential 'ColdCommitteeRole)] -> Set (Credential 'ColdCommitteeRole) forall a. Monoid a => [a] -> a mconcat ([Set (Credential 'ColdCommitteeRole)] -> Set (Credential 'ColdCommitteeRole)) -> (Map k (GovActionState era) -> [Set (Credential 'ColdCommitteeRole)]) -> Map k (GovActionState era) -> Set (Credential 'ColdCommitteeRole) forall b c a. (b -> c) -> (a -> b) -> a -> c . (GovActionState era -> Maybe (Set (Credential 'ColdCommitteeRole))) -> [GovActionState era] -> [Set (Credential 'ColdCommitteeRole)] forall a b. (a -> Maybe b) -> [a] -> [b] mapMaybe (GovAction era -> Maybe (Set (Credential 'ColdCommitteeRole)) forall {era}. GovAction era -> Maybe (Set (Credential 'ColdCommitteeRole)) propGetCCMembers (GovAction era -> Maybe (Set (Credential 'ColdCommitteeRole))) -> (GovActionState era -> GovAction era) -> GovActionState era -> Maybe (Set (Credential 'ColdCommitteeRole)) forall b c a. (b -> c) -> (a -> b) -> a -> c . ProposalProcedure era -> GovAction era forall era. ProposalProcedure era -> GovAction era pProcGovAction (ProposalProcedure era -> GovAction era) -> (GovActionState era -> ProposalProcedure era) -> GovActionState era -> GovAction era forall b c a. (b -> c) -> (a -> b) -> a -> c . GovActionState era -> ProposalProcedure era forall era. GovActionState era -> ProposalProcedure era gasProposalProcedure) ([GovActionState era] -> [Set (Credential 'ColdCommitteeRole)]) -> (Map k (GovActionState era) -> [GovActionState era]) -> Map k (GovActionState era) -> [Set (Credential 'ColdCommitteeRole)] forall b c a. (b -> c) -> (a -> b) -> a -> c . Map k (GovActionState era) -> [GovActionState era] forall k a. Map k a -> [a] Map.elems 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) cgceCurrentCommittee Set (Credential 'ColdCommitteeRole) -> Set (Credential 'ColdCommitteeRole) -> Set (Credential 'ColdCommitteeRole) forall a. Semigroup a => a -> a -> a <> Map (GovPurposeId 'CommitteePurpose) (GovActionState era) -> Set (Credential 'ColdCommitteeRole) forall {k} {era}. Map k (GovActionState era) -> Set (Credential 'ColdCommitteeRole) potentialCCMembers Map (GovPurposeId 'CommitteePurpose) (GovActionState era) cgceCommitteeProposals 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 cgceCurrentEpoch 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 cgcePParams 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 SpecTranslate ctx (VState era) where type SpecRep (VState era) = Agda.GState toSpecRep :: VState era -> SpecTransM ctx (SpecRep (VState era)) toSpecRep VState {Map (Credential 'DRepRole) DRepState CommitteeState era EpochNo vsDReps :: Map (Credential 'DRepRole) DRepState vsCommitteeState :: CommitteeState era vsNumDormantEpochs :: EpochNo vsDReps :: forall era. VState era -> Map (Credential 'DRepRole) DRepState vsCommitteeState :: forall era. VState era -> CommitteeState era vsNumDormantEpochs :: forall era. VState era -> EpochNo ..} = do HSMap Credential Integer -> HSMap Credential (Maybe Credential) -> HSMap DepositPurpose Integer -> GState Agda.MkGState (HSMap Credential Integer -> HSMap Credential (Maybe Credential) -> HSMap DepositPurpose Integer -> GState) -> SpecTransM ctx (HSMap Credential Integer) -> SpecTransM ctx (HSMap Credential (Maybe Credential) -> HSMap DepositPurpose Integer -> GState) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Map (Credential 'DRepRole) EpochNo -> SpecTransM ctx (SpecRep (Map (Credential 'DRepRole) EpochNo)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (EpochNo -> EpochNo updateExpiry (EpochNo -> EpochNo) -> (DRepState -> EpochNo) -> DRepState -> EpochNo forall b c a. (b -> c) -> (a -> b) -> a -> c . DRepState -> EpochNo drepExpiry (DRepState -> EpochNo) -> Map (Credential 'DRepRole) DRepState -> Map (Credential 'DRepRole) EpochNo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Map (Credential 'DRepRole) DRepState vsDReps) SpecTransM ctx (HSMap Credential (Maybe Credential) -> HSMap DepositPurpose Integer -> GState) -> SpecTransM ctx (HSMap Credential (Maybe Credential)) -> SpecTransM ctx (HSMap DepositPurpose Integer -> GState) 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 'ColdCommitteeRole) (StrictMaybe (Credential 'HotCommitteeRole)) -> SpecTransM ctx (SpecRep (Map (Credential 'ColdCommitteeRole) (StrictMaybe (Credential 'HotCommitteeRole)))) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (CommitteeAuthorization -> StrictMaybe (Credential 'HotCommitteeRole) committeeCredentialToStrictMaybe (CommitteeAuthorization -> StrictMaybe (Credential 'HotCommitteeRole)) -> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization -> Map (Credential 'ColdCommitteeRole) (StrictMaybe (Credential 'HotCommitteeRole)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> CommitteeState era -> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization forall era. CommitteeState era -> Map (Credential 'ColdCommitteeRole) CommitteeAuthorization csCommitteeCreds CommitteeState era vsCommitteeState) SpecTransM ctx (HSMap DepositPurpose Integer -> GState) -> SpecTransM ctx (HSMap DepositPurpose Integer) -> SpecTransM ctx GState 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 where transEntry :: (a, DRepState) -> SpecTransM ctx (DepositPurpose, Integer) transEntry (a cred, DRepState val) = (,) (DepositPurpose -> Integer -> (DepositPurpose, Integer)) -> SpecTransM ctx DepositPurpose -> SpecTransM ctx (Integer -> (DepositPurpose, Integer)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> (Credential -> DepositPurpose Agda.DRepDeposit (Credential -> DepositPurpose) -> SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> a -> SpecTransM ctx (SpecRep a) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep a cred) SpecTransM ctx (Integer -> (DepositPurpose, Integer)) -> SpecTransM ctx Integer -> SpecTransM ctx (DepositPurpose, Integer) 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 <*> CompactForm Coin -> SpecTransM ctx (SpecRep (CompactForm Coin)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (DRepState -> CompactForm Coin drepDeposit DRepState val) deposits :: SpecTransM ctx (HSMap DepositPurpose Integer) deposits = [(DepositPurpose, Integer)] -> HSMap DepositPurpose Integer forall k v. [(k, v)] -> HSMap k v Agda.MkHSMap ([(DepositPurpose, Integer)] -> HSMap DepositPurpose Integer) -> SpecTransM ctx [(DepositPurpose, Integer)] -> SpecTransM ctx (HSMap DepositPurpose Integer) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> ((Credential 'DRepRole, DRepState) -> SpecTransM ctx (DepositPurpose, Integer)) -> [(Credential 'DRepRole, DRepState)] -> SpecTransM ctx [(DepositPurpose, Integer)] forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> [a] -> f [b] traverse (Credential 'DRepRole, DRepState) -> SpecTransM ctx (DepositPurpose, Integer) forall {a} {ctx}. (SpecRep a ~ Credential, SpecTranslate ctx a) => (a, DRepState) -> SpecTransM ctx (DepositPurpose, Integer) transEntry (Map (Credential 'DRepRole) DRepState -> [(Credential 'DRepRole, DRepState)] forall k a. Map k a -> [(k, a)] Map.toList Map (Credential 'DRepRole) DRepState vsDReps) updateExpiry :: EpochNo -> EpochNo updateExpiry = (Word64 -> Word64 -> Word64) -> EpochNo -> EpochNo -> EpochNo binOpEpochNo Word64 -> Word64 -> Word64 forall a. Num a => a -> a -> a (+) EpochNo vsNumDormantEpochs