{-# 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