{-# 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 (..),
  ConwayGovCertPredFailure,
 )
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 (ConwayGovCertPredFailure era) where
  type SpecRep (ConwayGovCertPredFailure era) = OpaqueErrorString

  toSpecRep :: ConwayGovCertPredFailure era
-> SpecTransM ctx (SpecRep (ConwayGovCertPredFailure era))
toSpecRep = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString)
-> (ConwayGovCertPredFailure era -> OpaqueErrorString)
-> ConwayGovCertPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayGovCertPredFailure era -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString

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
<*> Map DepositPurpose (CompactForm Coin)
-> SpecTransM ctx (SpecRep (Map DepositPurpose (CompactForm Coin)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map DepositPurpose (CompactForm Coin)
deposits
    where
      deposits :: Map DepositPurpose (CompactForm Coin)
deposits = (Credential 'DRepRole -> DepositPurpose)
-> Map (Credential 'DRepRole) (CompactForm Coin)
-> Map DepositPurpose (CompactForm Coin)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Credential 'DRepRole -> DepositPurpose
DRepDeposit (DRepState -> CompactForm Coin
drepDeposit (DRepState -> CompactForm Coin)
-> Map (Credential 'DRepRole) DRepState
-> Map (Credential 'DRepRole) (CompactForm Coin)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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