{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.GovCert () where

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin (Coin (..))
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 Cardano.Ledger.Dijkstra (DijkstraEra)
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.Dijkstra.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Dijkstra.Base

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

  toSpecRep :: ConwayGovCert
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra ConwayGovCert)
     (SpecRep DijkstraEra ConwayGovCert)
toSpecRep (ConwayRegDRep Credential DRepRole
c Coin
d StrictMaybe Anchor
a) =
    Credential -> Integer -> Anchor -> DCert
Agda.Regdrep
      (Credential -> Integer -> Anchor -> DCert)
-> SpecTransM DijkstraEra () Credential
-> SpecTransM DijkstraEra () (Integer -> Anchor -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential DRepRole))
     (SpecRep DijkstraEra (Credential DRepRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential DRepRole
c
      SpecTransM DijkstraEra () (Integer -> Anchor -> DCert)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Anchor -> DCert)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra Coin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Coin
d
      SpecTransM DijkstraEra () (Anchor -> DCert)
-> SpecTransM DijkstraEra () Anchor
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Anchor)
     (SpecRep DijkstraEra 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 DijkstraEra () Credential
-> SpecTransM DijkstraEra () (Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential DRepRole))
     (SpecRep DijkstraEra (Credential DRepRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential DRepRole
c
      SpecTransM DijkstraEra () (Integer -> DCert)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Coin)
     (SpecRep DijkstraEra 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 DijkstraEra () Credential
-> SpecTransM DijkstraEra () (Integer -> Anchor -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential DRepRole
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential DRepRole))
     (SpecRep DijkstraEra (Credential DRepRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential DRepRole
c
      SpecTransM DijkstraEra () (Integer -> Anchor -> DCert)
-> SpecTransM DijkstraEra () Integer
-> SpecTransM DijkstraEra () (Anchor -> DCert)
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> SpecTransM DijkstraEra () Integer
forall a. a -> SpecTransM DijkstraEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0
      SpecTransM DijkstraEra () (Anchor -> DCert)
-> SpecTransM DijkstraEra () Anchor
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Anchor
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra Anchor)
     (SpecRep DijkstraEra 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 DijkstraEra () Credential
-> SpecTransM DijkstraEra () (Maybe Credential -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential ColdCommitteeRole
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential ColdCommitteeRole))
     (SpecRep DijkstraEra (Credential ColdCommitteeRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential ColdCommitteeRole
c
      SpecTransM DijkstraEra () (Maybe Credential -> DCert)
-> SpecTransM DijkstraEra () (Maybe Credential)
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (Credential HotCommitteeRole)
-> SpecTransM
     DijkstraEra
     (SpecContext
        DijkstraEra (StrictMaybe (Credential HotCommitteeRole)))
     (SpecRep DijkstraEra (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 DijkstraEra () Credential
-> SpecTransM DijkstraEra () (Maybe Credential -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Credential ColdCommitteeRole
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (Credential ColdCommitteeRole))
     (SpecRep DijkstraEra (Credential ColdCommitteeRole))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Credential ColdCommitteeRole
c
      SpecTransM DijkstraEra () (Maybe Credential -> DCert)
-> SpecTransM DijkstraEra () (Maybe Credential)
-> SpecTransM DijkstraEra () DCert
forall a b.
SpecTransM DijkstraEra () (a -> b)
-> SpecTransM DijkstraEra () a -> SpecTransM DijkstraEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe (Credential (ZonkAny 0))
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (StrictMaybe (Credential (ZonkAny 0))))
     (SpecRep DijkstraEra (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 DijkstraEra (Conway.ConwayGovCertEnv DijkstraEra) where
  type SpecRep DijkstraEra (Conway.ConwayGovCertEnv DijkstraEra) = Agda.CertEnv
  type
    SpecContext DijkstraEra (Conway.ConwayGovCertEnv DijkstraEra) =
      (VotingProcedures DijkstraEra, Map AccountAddress Coin)

  -- TODO Dijkstra: the new ceDirectDeposits field defaults to empty here; the
  -- value should be plumbed from the transaction body's directDeposits.
  toSpecRep :: ConwayGovCertEnv DijkstraEra
-> SpecTransM
     DijkstraEra
     (SpecContext DijkstraEra (ConwayGovCertEnv DijkstraEra))
     (SpecRep DijkstraEra (ConwayGovCertEnv DijkstraEra))
toSpecRep Conway.ConwayGovCertEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState DijkstraEra)
StrictMaybe (Committee DijkstraEra)
PParams DijkstraEra
EpochNo
cgcePParams :: PParams DijkstraEra
cgceCurrentEpoch :: EpochNo
cgceCurrentCommittee :: StrictMaybe (Committee DijkstraEra)
cgceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState DijkstraEra)
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
  DijkstraEra
  (VotingProcedures DijkstraEra, Map AccountAddress Coin)
  (VotingProcedures DijkstraEra, 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 DijkstraEra -> Set (Credential ColdCommitteeRole))
-> StrictMaybe (Committee DijkstraEra)
-> 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 DijkstraEra
    -> Map (Credential ColdCommitteeRole) EpochNo)
-> Committee DijkstraEra
-> Set (Credential ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Committee DijkstraEra -> Map (Credential ColdCommitteeRole) EpochNo
forall era.
Committee era -> Map (Credential ColdCommitteeRole) EpochNo
committeeMembers) StrictMaybe (Committee DijkstraEra)
cgceCurrentCommittee
            Set (Credential ColdCommitteeRole)
-> Set (Credential ColdCommitteeRole)
-> Set (Credential ColdCommitteeRole)
forall a. Semigroup a => a -> a -> a
<> Map (GovPurposeId 'CommitteePurpose) (GovActionState DijkstraEra)
-> Set (Credential ColdCommitteeRole)
forall {k} {era}.
Map k (GovActionState era) -> Set (Credential ColdCommitteeRole)
potentialCCMembers Map (GovPurposeId 'CommitteePurpose) (GovActionState DijkstraEra)
cgceCommitteeProposals
    withCtxSpecTransM () $
      Agda.MkCertEnv
        <$> toSpecRep cgceCurrentEpoch
        <*> toSpecRep cgcePParams
        <*> toSpecRep votes
        <*> toSpecRepMap withdrawals
        <*> toSpecRep ccColdCreds
        <*> pure (Agda.MkHSMap [])

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

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