{-# 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.BaseTypes
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.TxCert (ConwayGovCert (..))
import Cardano.Ledger.Credential (Credential (..))
import Data.Default (Default (..))
import Data.Map.Strict (Map, keysSet)
import qualified Data.Map.Strict as Map
import Data.Maybe (mapMaybe)
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base

instance SpecTranslate ConwayEra ConwayGovCert where
  type SpecRep ConwayEra ConwayGovCert = Agda.DCert

  toSpecRep :: ConwayGovCert
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra ConwayGovCert)
     (SpecRep ConwayEra ConwayGovCert)
toSpecRep (ConwayRegDRep Credential DRepRole
c Coin
d StrictMaybe Anchor
a) =
    Credential -> Integer -> Anchor -> DCert
Agda.Regdrep
      (Credential -> Integer -> Anchor -> DCert)
-> SpecTransM ConwayEra () Credential
-> SpecTransM ConwayEra () (Integer -> Anchor -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential DRepRole))
     (SpecRep ConwayEra (Credential DRepRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential DRepRole
c
      SpecTransM ConwayEra () (Integer -> Anchor -> DCert)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (Anchor -> DCert)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Coin) (SpecRep ConwayEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
d
      SpecTransM ConwayEra () (Anchor -> DCert)
-> SpecTransM ConwayEra () Anchor -> SpecTransM ConwayEra () DCert
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Anchor) (SpecRep ConwayEra Anchor)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era 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 ConwayEra () Credential
-> SpecTransM ConwayEra () (Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential DRepRole))
     (SpecRep ConwayEra (Credential DRepRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential DRepRole
c
      SpecTransM ConwayEra () (Integer -> DCert)
-> SpecTransM ConwayEra () Integer -> SpecTransM ConwayEra () DCert
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Coin) (SpecRep ConwayEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
d
  toSpecRep (ConwayUpdateDRep Credential DRepRole
c StrictMaybe Anchor
a) =
    Credential -> Integer -> Anchor -> DCert
Agda.Regdrep
      (Credential -> Integer -> Anchor -> DCert)
-> SpecTransM ConwayEra () Credential
-> SpecTransM ConwayEra () (Integer -> Anchor -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential DRepRole))
     (SpecRep ConwayEra (Credential DRepRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential DRepRole
c
      SpecTransM ConwayEra () (Integer -> Anchor -> DCert)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (Anchor -> DCert)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM ConwayEra () Integer
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0
      SpecTransM ConwayEra () (Anchor -> DCert)
-> SpecTransM ConwayEra () Anchor -> SpecTransM ConwayEra () DCert
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Anchor) (SpecRep ConwayEra Anchor)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era 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 ConwayEra () Credential
-> SpecTransM ConwayEra () (Maybe Credential -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential ColdCommitteeRole
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential ColdCommitteeRole))
     (SpecRep ConwayEra (Credential ColdCommitteeRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential ColdCommitteeRole
c
      SpecTransM ConwayEra () (Maybe Credential -> DCert)
-> SpecTransM ConwayEra () (Maybe Credential)
-> SpecTransM ConwayEra () DCert
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (Credential HotCommitteeRole)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (StrictMaybe (Credential HotCommitteeRole)))
     (SpecRep ConwayEra (StrictMaybe (Credential HotCommitteeRole)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era 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 ConwayEra () Credential
-> SpecTransM ConwayEra () (Maybe Credential -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential ColdCommitteeRole
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential ColdCommitteeRole))
     (SpecRep ConwayEra (Credential ColdCommitteeRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential ColdCommitteeRole
c
      SpecTransM ConwayEra () (Maybe Credential -> DCert)
-> SpecTransM ConwayEra () (Maybe Credential)
-> SpecTransM ConwayEra () DCert
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (Credential (ZonkAny 0))
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (StrictMaybe (Credential (ZonkAny 0))))
     (SpecRep ConwayEra (StrictMaybe (Credential (ZonkAny 0))))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (forall a. StrictMaybe a
SNothing @(Credential _))

instance SpecTranslate ConwayEra (Conway.ConwayGovCertEnv ConwayEra) where
  type SpecRep ConwayEra (Conway.ConwayGovCertEnv ConwayEra) = Agda.CertEnv
  type
    SpecContext ConwayEra (Conway.ConwayGovCertEnv ConwayEra) =
      (VotingProcedures ConwayEra, Map AccountAddress Coin)

  toSpecRep :: ConwayGovCertEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayGovCertEnv ConwayEra))
     (SpecRep ConwayEra (ConwayGovCertEnv ConwayEra))
toSpecRep Conway.ConwayGovCertEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
StrictMaybe (Committee ConwayEra)
PParams ConwayEra
EpochNo
cgcePParams :: PParams ConwayEra
cgceCurrentEpoch :: EpochNo
cgceCurrentCommittee :: StrictMaybe (Committee ConwayEra)
cgceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
cgceCommitteeProposals :: forall era.
ConwayGovCertEnv era
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
cgceCurrentCommittee :: forall era. ConwayGovCertEnv era -> StrictMaybe (Committee era)
cgceCurrentEpoch :: forall era. ConwayGovCertEnv era -> EpochNo
cgcePParams :: forall era. ConwayGovCertEnv era -> PParams era
..} = do
    (votes, withdrawals) <- SpecTransM
  ConwayEra
  (VotingProcedures ConwayEra, Map AccountAddress Coin)
  (VotingProcedures ConwayEra, Map AccountAddress Coin)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    let 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 =
          [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 =
          (Committee ConwayEra -> Set (Credential ColdCommitteeRole))
-> StrictMaybe (Committee ConwayEra)
-> 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 ConwayEra
    -> Map (Credential ColdCommitteeRole) EpochNo)
-> Committee ConwayEra
-> Set (Credential ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Committee ConwayEra -> Map (Credential ColdCommitteeRole) EpochNo
forall era.
Committee era -> Map (Credential ColdCommitteeRole) EpochNo
committeeMembers) StrictMaybe (Committee ConwayEra)
cgceCurrentCommittee
            Set (Credential ColdCommitteeRole)
-> Set (Credential ColdCommitteeRole)
-> Set (Credential ColdCommitteeRole)
forall a. Semigroup a => a -> a -> a
<> Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
-> Set (Credential ColdCommitteeRole)
forall {k} {era}.
Map k (GovActionState era) -> Set (Credential ColdCommitteeRole)
potentialCCMembers Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
cgceCommitteeProposals
    withCtxSpecTransM () $
      Agda.MkCertEnv
        <$> toSpecRep cgceCurrentEpoch
        <*> toSpecRep cgcePParams
        <*> toSpecRep votes
        <*> toSpecRepMap withdrawals
        <*> toSpecRep ccColdCreds

instance SpecTranslate ConwayEra (VState ConwayEra) where
  type SpecRep ConwayEra (VState ConwayEra) = Agda.GState

  toSpecRep :: VState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (VState ConwayEra))
     (SpecRep ConwayEra (VState ConwayEra))
toSpecRep VState {Map (Credential DRepRole) DRepState
CommitteeState ConwayEra
EpochNo
vsDReps :: Map (Credential DRepRole) DRepState
vsCommitteeState :: CommitteeState ConwayEra
vsNumDormantEpochs :: EpochNo
vsNumDormantEpochs :: forall era. VState era -> EpochNo
vsCommitteeState :: forall era. VState era -> CommitteeState era
vsDReps :: forall era. VState era -> Map (Credential DRepRole) DRepState
..} = 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 ConwayEra () (HSMap Credential Integer)
-> SpecTransM
     ConwayEra
     ()
     (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
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (Credential DRepRole))
        (SpecRep ConwayEra EpochNo))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap (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
  ConwayEra
  ()
  (HSMap Credential (Maybe Credential)
   -> HSMap DepositPurpose Integer -> GState)
-> SpecTransM ConwayEra () (HSMap Credential (Maybe Credential))
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer -> GState)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ( Map
  (Credential ColdCommitteeRole)
  (StrictMaybe (Credential HotCommitteeRole))
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (Credential ColdCommitteeRole))
        (SpecRep ConwayEra (StrictMaybe (Credential HotCommitteeRole))))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap
              (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 ConwayEra
-> Map (Credential ColdCommitteeRole) CommitteeAuthorization
forall era.
CommitteeState era
-> Map (Credential ColdCommitteeRole) CommitteeAuthorization
csCommitteeCreds CommitteeState ConwayEra
vsCommitteeState)
          )
      SpecTransM ConwayEra () (HSMap DepositPurpose Integer -> GState)
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
-> SpecTransM ConwayEra () GState
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
deposits
    where
      transEntry :: (a, DRepState)
-> SpecTransM era (SpecContext era a) (DepositPurpose, Integer)
transEntry (a
cred, DRepState
val) =
        (,) (DepositPurpose -> Integer -> (DepositPurpose, Integer))
-> SpecTransM era (SpecContext era a) DepositPurpose
-> SpecTransM
     era (SpecContext era a) (Integer -> (DepositPurpose, Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Credential -> DepositPurpose
Agda.DRepDeposit (Credential -> DepositPurpose)
-> SpecTransM era (SpecContext era a) Credential
-> SpecTransM era (SpecContext era a) DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM era (SpecContext era a) (SpecRep era a)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep a
cred) SpecTransM
  era (SpecContext era a) (Integer -> (DepositPurpose, Integer))
-> SpecTransM era (SpecContext era a) Integer
-> SpecTransM era (SpecContext era a) (DepositPurpose, Integer)
forall a b.
SpecTransM era (SpecContext era a) (a -> b)
-> SpecTransM era (SpecContext era a) a
-> SpecTransM era (SpecContext era a) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CompactForm Coin
-> SpecTransM
     era
     (SpecContext era (CompactForm Coin))
     (SpecRep era (CompactForm Coin))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (DRepState -> CompactForm Coin
drepDeposit DRepState
val)
      deposits :: SpecTransM ConwayEra () (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 ConwayEra () [(DepositPurpose, Integer)]
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Credential DRepRole, DRepState)
 -> SpecTransM ConwayEra () (DepositPurpose, Integer))
-> [(Credential DRepRole, DRepState)]
-> SpecTransM ConwayEra () [(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 ConwayEra () (DepositPurpose, Integer)
(Credential DRepRole, DRepState)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential DRepRole))
     (DepositPurpose, Integer)
forall {era} {a}.
(SpecRep era a ~ Credential, SpecContext era a ~ (),
 SpecTranslate era a) =>
(a, DRepState)
-> SpecTransM era (SpecContext era a) (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