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

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert () where

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin
import Cardano.Ledger.Compactible (Compactible (..))
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
import Cardano.Ledger.Rewards (rewardAmount)
import Cardano.Ledger.Shelley.LedgerState
import Data.Foldable (Foldable (..))
import qualified Data.Foldable as Set
import Data.Map.Strict (Map, keysSet)
import qualified Data.Map.Strict as Map
import qualified Data.OMap.Strict as OMap
import qualified Data.VMap as VMap
import Lens.Micro
import Lens.Micro.Extras (view)
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTransM,
  SpecTranslate (..),
  askSpecTransM,
  toSpecRepMap,
  withCtxSpecTransM,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool ()
import Test.Cardano.Ledger.Conformance.Utils (
  bimapMHSMap,
  unionsHSMap,
 )
import Test.Cardano.Ledger.Shelley.Utils (runShelleyBase)

instance SpecTranslate ConwayEra (Conway.CertEnv ConwayEra) where
  type SpecRep ConwayEra (Conway.CertEnv ConwayEra) = Agda.CertEnv
  type
    SpecContext ConwayEra (Conway.CertEnv ConwayEra) =
      (VotingProcedures ConwayEra, Map AccountAddress Coin)
  toSpecRep :: CertEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (CertEnv ConwayEra))
     (SpecRep ConwayEra (CertEnv ConwayEra))
toSpecRep Conway.CertEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
StrictMaybe (Committee ConwayEra)
PParams ConwayEra
EpochNo
cePParams :: PParams ConwayEra
ceCurrentEpoch :: EpochNo
ceCurrentCommittee :: StrictMaybe (Committee ConwayEra)
ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState ConwayEra)
ceCommitteeProposals :: forall era.
CertEnv era
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
ceCurrentCommittee :: forall era. CertEnv era -> StrictMaybe (Committee era)
ceCurrentEpoch :: forall era. CertEnv era -> EpochNo
cePParams :: forall era. CertEnv 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 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)
ceCurrentCommittee
    withCtxSpecTransM () $
      Agda.MkCertEnv
        <$> toSpecRep ceCurrentEpoch
        <*> toSpecRep cePParams
        <*> toSpecRep votes
        <*> toSpecRepMap withdrawals
        <*> toSpecRep ccColdCreds

instance SpecTranslate ConwayEra (ConwayCertState ConwayEra) where
  type SpecRep ConwayEra (ConwayCertState ConwayEra) = Agda.CertState
  toSpecRep :: ConwayCertState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayCertState ConwayEra))
     (SpecRep ConwayEra (ConwayCertState ConwayEra))
toSpecRep ConwayCertState {DState ConwayEra
PState ConwayEra
VState ConwayEra
conwayCertVState :: VState ConwayEra
conwayCertPState :: PState ConwayEra
conwayCertDState :: DState ConwayEra
conwayCertDState :: forall era. ConwayCertState era -> DState era
conwayCertPState :: forall era. ConwayCertState era -> PState era
conwayCertVState :: forall era. ConwayCertState era -> VState era
..} =
    DState -> PState -> GState -> CertState
Agda.MkCertState
      (DState -> PState -> GState -> CertState)
-> SpecTransM ConwayEra () DState
-> SpecTransM ConwayEra () (PState -> GState -> CertState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (DState ConwayEra))
     (SpecRep ConwayEra (DState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DState ConwayEra
conwayCertDState
      SpecTransM ConwayEra () (PState -> GState -> CertState)
-> SpecTransM ConwayEra () PState
-> SpecTransM ConwayEra () (GState -> CertState)
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
<*> PState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (PState ConwayEra))
     (SpecRep ConwayEra (PState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PState ConwayEra
conwayCertPState
      SpecTransM ConwayEra () (GState -> CertState)
-> SpecTransM ConwayEra () GState
-> SpecTransM ConwayEra () CertState
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
<*> VState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (VState ConwayEra))
     (SpecRep ConwayEra (VState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep VState ConwayEra
conwayCertVState

instance SpecTranslate ConwayEra (ConwayTxCert ConwayEra) where
  type SpecRep ConwayEra (ConwayTxCert ConwayEra) = Agda.DCert

  toSpecRep :: ConwayTxCert ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayTxCert ConwayEra))
     (SpecRep ConwayEra (ConwayTxCert ConwayEra))
toSpecRep (ConwayTxCertPool PoolCert
p) = PoolCert
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra PoolCert)
     (SpecRep ConwayEra PoolCert)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PoolCert
p
  toSpecRep (ConwayTxCertGov ConwayGovCert
c) = ConwayGovCert
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra ConwayGovCert)
     (SpecRep ConwayEra ConwayGovCert)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ConwayGovCert
c
  toSpecRep (ConwayTxCertDeleg ConwayDelegCert
x) = ConwayDelegCert
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra ConwayDelegCert)
     (SpecRep ConwayEra ConwayDelegCert)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ConwayDelegCert
x

depositsMap ::
  CertState ConwayEra ->
  Proposals ConwayEra ->
  SpecTransM ConwayEra () (Agda.HSMap Agda.DepositPurpose Integer)
depositsMap :: CertState ConwayEra
-> Proposals ConwayEra
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
depositsMap CertState ConwayEra
certState Proposals ConwayEra
props =
  [HSMap DepositPurpose Integer] -> HSMap DepositPurpose Integer
forall k v. Ord k => [HSMap k v] -> HSMap k v
unionsHSMap
    ([HSMap DepositPurpose Integer] -> HSMap DepositPurpose Integer)
-> SpecTransM ConwayEra () [HSMap DepositPurpose Integer]
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecTransM ConwayEra () (HSMap DepositPurpose Integer)]
-> SpecTransM ConwayEra () [HSMap DepositPurpose Integer]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
      [ (Credential Staking -> SpecTransM ConwayEra () DepositPurpose)
-> (AccountState ConwayEra -> SpecTransM ConwayEra () Integer)
-> HSMap (Credential Staking) (AccountState ConwayEra)
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
forall (m :: * -> *) k k' v v'.
Applicative m =>
(k -> m k') -> (v -> m v') -> HSMap k v -> m (HSMap k' v')
bimapMHSMap
          ((Credential -> DepositPurpose)
-> SpecTransM ConwayEra () Credential
-> SpecTransM ConwayEra () DepositPurpose
forall a b.
(a -> b) -> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Credential -> DepositPurpose
Agda.CredentialDeposit (SpecTransM ConwayEra () Credential
 -> SpecTransM ConwayEra () DepositPurpose)
-> (Credential Staking -> SpecTransM ConwayEra () Credential)
-> Credential Staking
-> SpecTransM ConwayEra () DepositPurpose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Credential Staking -> SpecTransM ConwayEra () Credential
Credential Staking
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential Staking))
     (SpecRep ConwayEra (Credential Staking))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep)
          (Coin -> SpecTransM ConwayEra () Integer
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 -> SpecTransM ConwayEra () Integer)
-> (AccountState ConwayEra -> Coin)
-> AccountState ConwayEra
-> SpecTransM ConwayEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (AccountState ConwayEra -> CompactForm Coin)
-> AccountState ConwayEra
-> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (CompactForm Coin) (AccountState ConwayEra) (CompactForm Coin)
-> AccountState ConwayEra -> CompactForm Coin
forall a s. Getting a s a -> s -> a
view Getting
  (CompactForm Coin) (AccountState ConwayEra) (CompactForm Coin)
forall era.
EraAccounts era =>
Lens' (AccountState era) (CompactForm Coin)
Lens' (AccountState ConwayEra) (CompactForm Coin)
depositAccountStateL)
          ([(Credential Staking, AccountState ConwayEra)]
-> HSMap (Credential Staking) (AccountState ConwayEra)
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(Credential Staking, AccountState ConwayEra)]
 -> HSMap (Credential Staking) (AccountState ConwayEra))
-> (Map (Credential Staking) (AccountState ConwayEra)
    -> [(Credential Staking, AccountState ConwayEra)])
-> Map (Credential Staking) (AccountState ConwayEra)
-> HSMap (Credential Staking) (AccountState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Credential Staking) (AccountState ConwayEra)
-> [(Credential Staking, AccountState ConwayEra)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (Credential Staking) (AccountState ConwayEra)
 -> HSMap (Credential Staking) (AccountState ConwayEra))
-> Map (Credential Staking) (AccountState ConwayEra)
-> HSMap (Credential Staking) (AccountState ConwayEra)
forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
ConwayCertState ConwayEra
certState ConwayCertState ConwayEra
-> Getting
     (Map (Credential Staking) (AccountState ConwayEra))
     (ConwayCertState ConwayEra)
     (Map (Credential Staking) (AccountState ConwayEra))
-> Map (Credential Staking) (AccountState ConwayEra)
forall s a. s -> Getting a s a -> a
^. (DState ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (DState ConwayEra))
-> CertState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (CertState ConwayEra)
(DState ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (DState ConwayEra))
-> ConwayCertState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (ConwayCertState ConwayEra)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState ConwayEra) (DState ConwayEra)
certDStateL ((DState ConwayEra
  -> Const
       (Map (Credential Staking) (AccountState ConwayEra))
       (DState ConwayEra))
 -> ConwayCertState ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (ConwayCertState ConwayEra))
-> ((Map (Credential Staking) (AccountState ConwayEra)
     -> Const
          (Map (Credential Staking) (AccountState ConwayEra))
          (Map (Credential Staking) (AccountState ConwayEra)))
    -> DState ConwayEra
    -> Const
         (Map (Credential Staking) (AccountState ConwayEra))
         (DState ConwayEra))
-> Getting
     (Map (Credential Staking) (AccountState ConwayEra))
     (ConwayCertState ConwayEra)
     (Map (Credential Staking) (AccountState ConwayEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (Accounts ConwayEra))
-> DState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (DState ConwayEra)
(ConwayAccounts ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (ConwayAccounts ConwayEra))
-> DState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (DState ConwayEra)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL ((ConwayAccounts ConwayEra
  -> Const
       (Map (Credential Staking) (AccountState ConwayEra))
       (ConwayAccounts ConwayEra))
 -> DState ConwayEra
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (DState ConwayEra))
-> ((Map (Credential Staking) (AccountState ConwayEra)
     -> Const
          (Map (Credential Staking) (AccountState ConwayEra))
          (Map (Credential Staking) (AccountState ConwayEra)))
    -> ConwayAccounts ConwayEra
    -> Const
         (Map (Credential Staking) (AccountState ConwayEra))
         (ConwayAccounts ConwayEra))
-> (Map (Credential Staking) (AccountState ConwayEra)
    -> Const
         (Map (Credential Staking) (AccountState ConwayEra))
         (Map (Credential Staking) (AccountState ConwayEra)))
-> DState ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (DState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState ConwayEra)
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (Map (Credential Staking) (AccountState ConwayEra)))
-> Accounts ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (Accounts ConwayEra)
(Map (Credential Staking) (AccountState ConwayEra)
 -> Const
      (Map (Credential Staking) (AccountState ConwayEra))
      (Map (Credential Staking) (AccountState ConwayEra)))
-> ConwayAccounts ConwayEra
-> Const
     (Map (Credential Staking) (AccountState ConwayEra))
     (ConwayAccounts ConwayEra)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens'
  (Accounts ConwayEra)
  (Map (Credential Staking) (AccountState ConwayEra))
accountsMapL)
      , (KeyHash StakePool -> SpecTransM ConwayEra () DepositPurpose)
-> (Coin -> SpecTransM ConwayEra () Integer)
-> HSMap (KeyHash StakePool) Coin
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
forall (m :: * -> *) k k' v v'.
Applicative m =>
(k -> m k') -> (v -> m v') -> HSMap k v -> m (HSMap k' v')
bimapMHSMap
          ((Integer -> DepositPurpose)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () DepositPurpose
forall a b.
(a -> b) -> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> DepositPurpose
Agda.PoolDeposit (SpecTransM ConwayEra () Integer
 -> SpecTransM ConwayEra () DepositPurpose)
-> (KeyHash StakePool -> SpecTransM ConwayEra () Integer)
-> KeyHash StakePool
-> SpecTransM ConwayEra () DepositPurpose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KeyHash StakePool -> SpecTransM ConwayEra () Integer
KeyHash StakePool
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (KeyHash StakePool))
     (SpecRep ConwayEra (KeyHash StakePool))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep)
          Coin -> SpecTransM ConwayEra () Integer
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
          ([(KeyHash StakePool, Coin)] -> HSMap (KeyHash StakePool) Coin
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(KeyHash StakePool, Coin)] -> HSMap (KeyHash StakePool) Coin)
-> (Map (KeyHash StakePool) Coin -> [(KeyHash StakePool, Coin)])
-> Map (KeyHash StakePool) Coin
-> HSMap (KeyHash StakePool) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (KeyHash StakePool) Coin -> [(KeyHash StakePool, Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (KeyHash StakePool) Coin -> HSMap (KeyHash StakePool) Coin)
-> Map (KeyHash StakePool) Coin -> HSMap (KeyHash StakePool) Coin
forall a b. (a -> b) -> a -> b
$ CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin)
-> (StakePoolState -> CompactForm Coin) -> StakePoolState -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StakePoolState -> CompactForm Coin
spsDeposit (StakePoolState -> Coin)
-> Map (KeyHash StakePool) StakePoolState
-> Map (KeyHash StakePool) Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CertState ConwayEra
ConwayCertState ConwayEra
certState ConwayCertState ConwayEra
-> Getting
     (Map (KeyHash StakePool) StakePoolState)
     (ConwayCertState ConwayEra)
     (Map (KeyHash StakePool) StakePoolState)
-> Map (KeyHash StakePool) StakePoolState
forall s a. s -> Getting a s a -> a
^. (PState ConwayEra
 -> Const
      (Map (KeyHash StakePool) StakePoolState) (PState ConwayEra))
-> CertState ConwayEra
-> Const
     (Map (KeyHash StakePool) StakePoolState) (CertState ConwayEra)
(PState ConwayEra
 -> Const
      (Map (KeyHash StakePool) StakePoolState) (PState ConwayEra))
-> ConwayCertState ConwayEra
-> Const
     (Map (KeyHash StakePool) StakePoolState)
     (ConwayCertState ConwayEra)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState ConwayEra) (PState ConwayEra)
certPStateL ((PState ConwayEra
  -> Const
       (Map (KeyHash StakePool) StakePoolState) (PState ConwayEra))
 -> ConwayCertState ConwayEra
 -> Const
      (Map (KeyHash StakePool) StakePoolState)
      (ConwayCertState ConwayEra))
-> ((Map (KeyHash StakePool) StakePoolState
     -> Const
          (Map (KeyHash StakePool) StakePoolState)
          (Map (KeyHash StakePool) StakePoolState))
    -> PState ConwayEra
    -> Const
         (Map (KeyHash StakePool) StakePoolState) (PState ConwayEra))
-> Getting
     (Map (KeyHash StakePool) StakePoolState)
     (ConwayCertState ConwayEra)
     (Map (KeyHash StakePool) StakePoolState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash StakePool) StakePoolState
 -> Const
      (Map (KeyHash StakePool) StakePoolState)
      (Map (KeyHash StakePool) StakePoolState))
-> PState ConwayEra
-> Const
     (Map (KeyHash StakePool) StakePoolState) (PState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash StakePool) StakePoolState
 -> f (Map (KeyHash StakePool) StakePoolState))
-> PState era -> f (PState era)
psStakePoolsL)
      , (Credential DRepRole -> SpecTransM ConwayEra () DepositPurpose)
-> (DRepState -> SpecTransM ConwayEra () Integer)
-> HSMap (Credential DRepRole) DRepState
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
forall (m :: * -> *) k k' v v'.
Applicative m =>
(k -> m k') -> (v -> m v') -> HSMap k v -> m (HSMap k' v')
bimapMHSMap
          ((Credential -> DepositPurpose)
-> SpecTransM ConwayEra () Credential
-> SpecTransM ConwayEra () DepositPurpose
forall a b.
(a -> b) -> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Credential -> DepositPurpose
Agda.DRepDeposit (SpecTransM ConwayEra () Credential
 -> SpecTransM ConwayEra () DepositPurpose)
-> (Credential DRepRole -> SpecTransM ConwayEra () Credential)
-> Credential DRepRole
-> SpecTransM ConwayEra () DepositPurpose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Credential DRepRole -> SpecTransM ConwayEra () Credential
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)
          (CompactForm Coin -> SpecTransM ConwayEra () Integer
CompactForm Coin
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (CompactForm Coin))
     (SpecRep ConwayEra (CompactForm Coin))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (CompactForm Coin -> SpecTransM ConwayEra () Integer)
-> (DRepState -> CompactForm Coin)
-> DRepState
-> SpecTransM ConwayEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DRepState -> CompactForm Coin
drepDeposit)
          ([(Credential DRepRole, DRepState)]
-> HSMap (Credential DRepRole) DRepState
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(Credential DRepRole, DRepState)]
 -> HSMap (Credential DRepRole) DRepState)
-> (Map (Credential DRepRole) DRepState
    -> [(Credential DRepRole, DRepState)])
-> Map (Credential DRepRole) DRepState
-> HSMap (Credential DRepRole) DRepState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Credential DRepRole) DRepState
-> [(Credential DRepRole, DRepState)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (Credential DRepRole) DRepState
 -> HSMap (Credential DRepRole) DRepState)
-> Map (Credential DRepRole) DRepState
-> HSMap (Credential DRepRole) DRepState
forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
ConwayCertState ConwayEra
certState ConwayCertState ConwayEra
-> Getting
     (Map (Credential DRepRole) DRepState)
     (ConwayCertState ConwayEra)
     (Map (Credential DRepRole) DRepState)
-> Map (Credential DRepRole) DRepState
forall s a. s -> Getting a s a -> a
^. (VState ConwayEra
 -> Const (Map (Credential DRepRole) DRepState) (VState ConwayEra))
-> CertState ConwayEra
-> Const
     (Map (Credential DRepRole) DRepState) (CertState ConwayEra)
(VState ConwayEra
 -> Const (Map (Credential DRepRole) DRepState) (VState ConwayEra))
-> ConwayCertState ConwayEra
-> Const
     (Map (Credential DRepRole) DRepState) (ConwayCertState ConwayEra)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState ConwayEra) (VState ConwayEra)
certVStateL ((VState ConwayEra
  -> Const (Map (Credential DRepRole) DRepState) (VState ConwayEra))
 -> ConwayCertState ConwayEra
 -> Const
      (Map (Credential DRepRole) DRepState) (ConwayCertState ConwayEra))
-> ((Map (Credential DRepRole) DRepState
     -> Const
          (Map (Credential DRepRole) DRepState)
          (Map (Credential DRepRole) DRepState))
    -> VState ConwayEra
    -> Const (Map (Credential DRepRole) DRepState) (VState ConwayEra))
-> Getting
     (Map (Credential DRepRole) DRepState)
     (ConwayCertState ConwayEra)
     (Map (Credential DRepRole) DRepState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential DRepRole) DRepState
 -> Const
      (Map (Credential DRepRole) DRepState)
      (Map (Credential DRepRole) DRepState))
-> VState ConwayEra
-> Const (Map (Credential DRepRole) DRepState) (VState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(Map (Credential DRepRole) DRepState
 -> f (Map (Credential DRepRole) DRepState))
-> VState era -> f (VState era)
vsDRepsL)
      , (GovActionId -> SpecTransM ConwayEra () DepositPurpose)
-> (GovActionState ConwayEra -> SpecTransM ConwayEra () Integer)
-> HSMap GovActionId (GovActionState ConwayEra)
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
forall (m :: * -> *) k k' v v'.
Applicative m =>
(k -> m k') -> (v -> m v') -> HSMap k v -> m (HSMap k' v')
bimapMHSMap
          (((Integer, Integer) -> DepositPurpose)
-> SpecTransM ConwayEra () (Integer, Integer)
-> SpecTransM ConwayEra () DepositPurpose
forall a b.
(a -> b) -> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer, Integer) -> DepositPurpose
Agda.GovActionDeposit (SpecTransM ConwayEra () (Integer, Integer)
 -> SpecTransM ConwayEra () DepositPurpose)
-> (GovActionId -> SpecTransM ConwayEra () (Integer, Integer))
-> GovActionId
-> SpecTransM ConwayEra () DepositPurpose
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionId -> SpecTransM ConwayEra () (Integer, Integer)
GovActionId
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra GovActionId)
     (SpecRep ConwayEra GovActionId)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep)
          (Coin -> SpecTransM ConwayEra () Integer
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 -> SpecTransM ConwayEra () Integer)
-> (GovActionState ConwayEra -> Coin)
-> GovActionState ConwayEra
-> SpecTransM ConwayEra () Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GovActionState ConwayEra -> Coin
forall era. GovActionState era -> Coin
gasDeposit)
          ([(GovActionId, GovActionState ConwayEra)]
-> HSMap GovActionId (GovActionState ConwayEra)
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(GovActionId, GovActionState ConwayEra)]
 -> HSMap GovActionId (GovActionState ConwayEra))
-> (OMap GovActionId (GovActionState ConwayEra)
    -> [(GovActionId, GovActionState ConwayEra)])
-> OMap GovActionId (GovActionState ConwayEra)
-> HSMap GovActionId (GovActionState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMap GovActionId (GovActionState ConwayEra)
-> [(GovActionId, GovActionState ConwayEra)]
forall k v. Ord k => OMap k v -> [(k, v)]
OMap.assocList (OMap GovActionId (GovActionState ConwayEra)
 -> HSMap GovActionId (GovActionState ConwayEra))
-> OMap GovActionId (GovActionState ConwayEra)
-> HSMap GovActionId (GovActionState ConwayEra)
forall a b. (a -> b) -> a -> b
$ Proposals ConwayEra
props Proposals ConwayEra
-> Getting
     (OMap GovActionId (GovActionState ConwayEra))
     (Proposals ConwayEra)
     (OMap GovActionId (GovActionState ConwayEra))
-> OMap GovActionId (GovActionState ConwayEra)
forall s a. s -> Getting a s a -> a
^. Getting
  (OMap GovActionId (GovActionState ConwayEra))
  (Proposals ConwayEra)
  (OMap GovActionId (GovActionState ConwayEra))
forall era (f :: * -> *).
Functor f =>
(OMap GovActionId (GovActionState era)
 -> f (OMap GovActionId (GovActionState era)))
-> Proposals era -> f (Proposals era)
pPropsL)
      ]

instance SpecTranslate ConwayEra (UTxOState ConwayEra) where
  type SpecRep ConwayEra (UTxOState ConwayEra) = Agda.UTxOState
  type SpecContext ConwayEra (UTxOState ConwayEra) = CertState ConwayEra

  toSpecRep :: UTxOState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (UTxOState ConwayEra))
     (SpecRep ConwayEra (UTxOState ConwayEra))
toSpecRep UTxOState {GovState ConwayEra
InstantStake ConwayEra
UTxO ConwayEra
Coin
utxosUtxo :: UTxO ConwayEra
utxosDeposited :: Coin
utxosFees :: Coin
utxosGovState :: GovState ConwayEra
utxosInstantStake :: InstantStake ConwayEra
utxosDonation :: Coin
utxosDonation :: forall era. UTxOState era -> Coin
utxosInstantStake :: forall era. UTxOState era -> InstantStake era
utxosGovState :: forall era. UTxOState era -> GovState era
utxosFees :: forall era. UTxOState era -> Coin
utxosDeposited :: forall era. UTxOState era -> Coin
utxosUtxo :: forall era. UTxOState era -> UTxO era
..} = do
    certState <- SpecTransM
  ConwayEra (ConwayCertState ConwayEra) (ConwayCertState ConwayEra)
forall era ctx. SpecTransM era ctx ctx
askSpecTransM
    let
      props = GovState ConwayEra
ConwayGovState ConwayEra
utxosGovState ConwayGovState ConwayEra
-> Getting
     (Proposals ConwayEra)
     (ConwayGovState ConwayEra)
     (Proposals ConwayEra)
-> Proposals ConwayEra
forall s a. s -> Getting a s a -> a
^. Getting
  (Proposals ConwayEra)
  (ConwayGovState ConwayEra)
  (Proposals ConwayEra)
forall era (f :: * -> *).
Functor f =>
(Proposals era -> f (Proposals era))
-> ConwayGovState era -> f (ConwayGovState era)
cgsProposalsL
      deposits = CertState ConwayEra
-> Proposals ConwayEra
-> SpecTransM ConwayEra () (HSMap DepositPurpose Integer)
depositsMap CertState ConwayEra
ConwayCertState ConwayEra
certState Proposals ConwayEra
props
    withCtxSpecTransM () $
      Agda.MkUTxOState
        <$> toSpecRep utxosUtxo
        <*> toSpecRep utxosFees
        <*> deposits
        <*> toSpecRep utxosDonation

instance SpecTranslate ConwayEra (LedgerState ConwayEra) where
  type SpecRep ConwayEra (LedgerState ConwayEra) = Agda.LState

  toSpecRep :: LedgerState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (LedgerState ConwayEra))
     (SpecRep ConwayEra (LedgerState ConwayEra))
toSpecRep (LedgerState {CertState ConwayEra
UTxOState ConwayEra
lsUTxOState :: UTxOState ConwayEra
lsCertState :: CertState ConwayEra
lsCertState :: forall era. LedgerState era -> CertState era
lsUTxOState :: forall era. LedgerState era -> UTxOState era
..}) =
    UTxOState
-> [((Integer, Integer), GovActionState)] -> CertState -> LState
Agda.MkLState
      (UTxOState
 -> [((Integer, Integer), GovActionState)] -> CertState -> LState)
-> SpecTransM ConwayEra () UTxOState
-> SpecTransM
     ConwayEra
     ()
     ([((Integer, Integer), GovActionState)] -> CertState -> LState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConwayCertState ConwayEra
-> SpecTransM ConwayEra (ConwayCertState ConwayEra) UTxOState
-> SpecTransM ConwayEra () UTxOState
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM CertState ConwayEra
ConwayCertState ConwayEra
lsCertState (UTxOState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (UTxOState ConwayEra))
     (SpecRep ConwayEra (UTxOState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UTxOState ConwayEra
lsUTxOState)
      SpecTransM
  ConwayEra
  ()
  ([((Integer, Integer), GovActionState)] -> CertState -> LState)
-> SpecTransM ConwayEra () [((Integer, Integer), GovActionState)]
-> SpecTransM ConwayEra () (CertState -> LState)
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
<*> Proposals ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Proposals ConwayEra))
     (SpecRep ConwayEra (Proposals ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Proposals ConwayEra
props
      SpecTransM ConwayEra () (CertState -> LState)
-> SpecTransM ConwayEra () CertState
-> SpecTransM ConwayEra () LState
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
<*> ConwayCertState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (ConwayCertState ConwayEra))
     (SpecRep ConwayEra (ConwayCertState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep CertState ConwayEra
ConwayCertState ConwayEra
lsCertState
    where
      props :: Proposals ConwayEra
props = UTxOState ConwayEra -> GovState ConwayEra
forall era. UTxOState era -> GovState era
utxosGovState UTxOState ConwayEra
lsUTxOState ConwayGovState ConwayEra
-> Getting
     (Proposals ConwayEra)
     (ConwayGovState ConwayEra)
     (Proposals ConwayEra)
-> Proposals ConwayEra
forall s a. s -> Getting a s a -> a
^. (Proposals ConwayEra
 -> Const (Proposals ConwayEra) (Proposals ConwayEra))
-> GovState ConwayEra
-> Const (Proposals ConwayEra) (GovState ConwayEra)
Getting
  (Proposals ConwayEra)
  (ConwayGovState ConwayEra)
  (Proposals ConwayEra)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Proposals era)
Lens' (GovState ConwayEra) (Proposals ConwayEra)
proposalsGovStateL

instance SpecTranslate ConwayEra (EpochState ConwayEra) where
  type SpecRep ConwayEra (EpochState ConwayEra) = Agda.EpochState

  toSpecRep :: EpochState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (EpochState ConwayEra))
     (SpecRep ConwayEra (EpochState ConwayEra))
toSpecRep (EpochState {esLState :: forall era. EpochState era -> LedgerState era
esLState = esLState :: LedgerState ConwayEra
esLState@LedgerState {UTxOState ConwayEra
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsUTxOState :: UTxOState ConwayEra
lsUTxOState}, ChainAccountState
SnapShots
NonMyopic
esChainAccountState :: ChainAccountState
esSnapshots :: SnapShots
esNonMyopic :: NonMyopic
esNonMyopic :: forall era. EpochState era -> NonMyopic
esSnapshots :: forall era. EpochState era -> SnapShots
esChainAccountState :: forall era. EpochState era -> ChainAccountState
..}) =
    Acnt
-> Snapshots -> LState -> EnactState -> RatifyState -> EpochState
Agda.MkEpochState
      (Acnt
 -> Snapshots -> LState -> EnactState -> RatifyState -> EpochState)
-> SpecTransM ConwayEra () Acnt
-> SpecTransM
     ConwayEra
     ()
     (Snapshots -> LState -> EnactState -> RatifyState -> EpochState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ChainAccountState
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra ChainAccountState)
     (SpecRep ConwayEra ChainAccountState)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep ChainAccountState
esChainAccountState
      SpecTransM
  ConwayEra
  ()
  (Snapshots -> LState -> EnactState -> RatifyState -> EpochState)
-> SpecTransM ConwayEra () Snapshots
-> SpecTransM
     ConwayEra () (LState -> EnactState -> RatifyState -> EpochState)
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
<*> SnapShots
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra SnapShots)
     (SpecRep ConwayEra SnapShots)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SnapShots
esSnapshots
      SpecTransM
  ConwayEra () (LState -> EnactState -> RatifyState -> EpochState)
-> SpecTransM ConwayEra () LState
-> SpecTransM
     ConwayEra () (EnactState -> RatifyState -> EpochState)
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
<*> LedgerState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (LedgerState ConwayEra))
     (SpecRep ConwayEra (LedgerState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep LedgerState ConwayEra
esLState
      SpecTransM ConwayEra () (EnactState -> RatifyState -> EpochState)
-> SpecTransM ConwayEra () EnactState
-> SpecTransM ConwayEra () (RatifyState -> EpochState)
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
<*> EnactState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (EnactState ConwayEra))
     (SpecRep ConwayEra (EnactState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep EnactState ConwayEra
enactState
      SpecTransM ConwayEra () (RatifyState -> EpochState)
-> SpecTransM ConwayEra () RatifyState
-> SpecTransM ConwayEra () EpochState
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
<*> [GovActionState ConwayEra]
-> SpecTransM ConwayEra [GovActionState ConwayEra] RatifyState
-> SpecTransM ConwayEra () RatifyState
forall ctx era a ctx'.
ctx -> SpecTransM era ctx a -> SpecTransM era ctx' a
withCtxSpecTransM [GovActionState ConwayEra]
govActions (RatifyState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (RatifyState ConwayEra))
     (SpecRep ConwayEra (RatifyState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep RatifyState ConwayEra
ratifyState)
    where
      enactState :: EnactState ConwayEra
enactState = GovState ConwayEra -> EnactState ConwayEra
forall era. ConwayEraGov era => GovState era -> EnactState era
mkEnactState (GovState ConwayEra -> EnactState ConwayEra)
-> GovState ConwayEra -> EnactState ConwayEra
forall a b. (a -> b) -> a -> b
$ UTxOState ConwayEra -> GovState ConwayEra
forall era. UTxOState era -> GovState era
utxosGovState UTxOState ConwayEra
lsUTxOState
      ratifyState :: RatifyState ConwayEra
ratifyState = ConwayGovState ConwayEra -> RatifyState ConwayEra
forall era.
(ConwayEraAccounts era, EraStake era) =>
ConwayGovState era -> RatifyState era
getRatifyState (ConwayGovState ConwayEra -> RatifyState ConwayEra)
-> ConwayGovState ConwayEra -> RatifyState ConwayEra
forall a b. (a -> b) -> a -> b
$ UTxOState ConwayEra -> GovState ConwayEra
forall era. UTxOState era -> GovState era
utxosGovState UTxOState ConwayEra
lsUTxOState
      govActions :: [GovActionState ConwayEra]
govActions = OMap GovActionId (GovActionState ConwayEra)
-> [GovActionState ConwayEra]
forall a. OMap GovActionId a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (OMap GovActionId (GovActionState ConwayEra)
 -> [GovActionState ConwayEra])
-> OMap GovActionId (GovActionState ConwayEra)
-> [GovActionState ConwayEra]
forall a b. (a -> b) -> a -> b
$ UTxOState ConwayEra
lsUTxOState UTxOState ConwayEra
-> Getting
     (OMap GovActionId (GovActionState ConwayEra))
     (UTxOState ConwayEra)
     (OMap GovActionId (GovActionState ConwayEra))
-> OMap GovActionId (GovActionState ConwayEra)
forall s a. s -> Getting a s a -> a
^. (GovState ConwayEra
 -> Const
      (OMap GovActionId (GovActionState ConwayEra)) (GovState ConwayEra))
-> UTxOState ConwayEra
-> Const
     (OMap GovActionId (GovActionState ConwayEra)) (UTxOState ConwayEra)
(ConwayGovState ConwayEra
 -> Const
      (OMap GovActionId (GovActionState ConwayEra))
      (ConwayGovState ConwayEra))
-> UTxOState ConwayEra
-> Const
     (OMap GovActionId (GovActionState ConwayEra)) (UTxOState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(GovState era -> f (GovState era))
-> UTxOState era -> f (UTxOState era)
utxosGovStateL ((ConwayGovState ConwayEra
  -> Const
       (OMap GovActionId (GovActionState ConwayEra))
       (ConwayGovState ConwayEra))
 -> UTxOState ConwayEra
 -> Const
      (OMap GovActionId (GovActionState ConwayEra))
      (UTxOState ConwayEra))
-> ((OMap GovActionId (GovActionState ConwayEra)
     -> Const
          (OMap GovActionId (GovActionState ConwayEra))
          (OMap GovActionId (GovActionState ConwayEra)))
    -> ConwayGovState ConwayEra
    -> Const
         (OMap GovActionId (GovActionState ConwayEra))
         (ConwayGovState ConwayEra))
-> Getting
     (OMap GovActionId (GovActionState ConwayEra))
     (UTxOState ConwayEra)
     (OMap GovActionId (GovActionState ConwayEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Proposals ConwayEra
 -> Const
      (OMap GovActionId (GovActionState ConwayEra))
      (Proposals ConwayEra))
-> GovState ConwayEra
-> Const
     (OMap GovActionId (GovActionState ConwayEra)) (GovState ConwayEra)
(Proposals ConwayEra
 -> Const
      (OMap GovActionId (GovActionState ConwayEra))
      (Proposals ConwayEra))
-> ConwayGovState ConwayEra
-> Const
     (OMap GovActionId (GovActionState ConwayEra))
     (ConwayGovState ConwayEra)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Proposals era)
Lens' (GovState ConwayEra) (Proposals ConwayEra)
proposalsGovStateL ((Proposals ConwayEra
  -> Const
       (OMap GovActionId (GovActionState ConwayEra))
       (Proposals ConwayEra))
 -> ConwayGovState ConwayEra
 -> Const
      (OMap GovActionId (GovActionState ConwayEra))
      (ConwayGovState ConwayEra))
-> Getting
     (OMap GovActionId (GovActionState ConwayEra))
     (Proposals ConwayEra)
     (OMap GovActionId (GovActionState ConwayEra))
-> (OMap GovActionId (GovActionState ConwayEra)
    -> Const
         (OMap GovActionId (GovActionState ConwayEra))
         (OMap GovActionId (GovActionState ConwayEra)))
-> ConwayGovState ConwayEra
-> Const
     (OMap GovActionId (GovActionState ConwayEra))
     (ConwayGovState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (OMap GovActionId (GovActionState ConwayEra))
  (Proposals ConwayEra)
  (OMap GovActionId (GovActionState ConwayEra))
forall era (f :: * -> *).
Functor f =>
(OMap GovActionId (GovActionState era)
 -> f (OMap GovActionId (GovActionState era)))
-> Proposals era -> f (Proposals era)
pPropsL

instance SpecTranslate ConwayEra SnapShots where
  type SpecRep ConwayEra SnapShots = Agda.Snapshots

  toSpecRep :: SnapShots
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra SnapShots)
     (SpecRep ConwayEra SnapShots)
toSpecRep (SnapShots {PoolDistr
SnapShot
Coin
ssStakeMark :: SnapShot
ssStakeMarkPoolDistr :: PoolDistr
ssStakeSet :: SnapShot
ssStakeGo :: SnapShot
ssFee :: Coin
ssFee :: SnapShots -> Coin
ssStakeGo :: SnapShots -> SnapShot
ssStakeMark :: SnapShots -> SnapShot
ssStakeMarkPoolDistr :: SnapShots -> PoolDistr
ssStakeSet :: SnapShots -> SnapShot
..}) =
    Snapshot -> Snapshot -> Snapshot -> Integer -> Snapshots
Agda.MkSnapshots
      (Snapshot -> Snapshot -> Snapshot -> Integer -> Snapshots)
-> SpecTransM ConwayEra () Snapshot
-> SpecTransM
     ConwayEra () (Snapshot -> Snapshot -> Integer -> Snapshots)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnapShot
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra SnapShot)
     (SpecRep ConwayEra SnapShot)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SnapShot
ssStakeMark
      SpecTransM
  ConwayEra () (Snapshot -> Snapshot -> Integer -> Snapshots)
-> SpecTransM ConwayEra () Snapshot
-> SpecTransM ConwayEra () (Snapshot -> Integer -> Snapshots)
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
<*> SnapShot
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra SnapShot)
     (SpecRep ConwayEra SnapShot)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SnapShot
ssStakeSet
      SpecTransM ConwayEra () (Snapshot -> Integer -> Snapshots)
-> SpecTransM ConwayEra () Snapshot
-> SpecTransM ConwayEra () (Integer -> Snapshots)
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
<*> SnapShot
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra SnapShot)
     (SpecRep ConwayEra SnapShot)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep SnapShot
ssStakeGo
      SpecTransM ConwayEra () (Integer -> Snapshots)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () Snapshots
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
ssFee

instance SpecTranslate ConwayEra SnapShot where
  type SpecRep ConwayEra SnapShot = Agda.Snapshot

  toSpecRep :: SnapShot
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra SnapShot)
     (SpecRep ConwayEra SnapShot)
toSpecRep (SnapShot {ActiveStake
NonZero Coin
VMap VB VB (KeyHash StakePool) StakePoolSnapShot
ssActiveStake :: ActiveStake
ssTotalActiveStake :: NonZero Coin
ssStakePoolsSnapShot :: VMap VB VB (KeyHash StakePool) StakePoolSnapShot
ssActiveStake :: SnapShot -> ActiveStake
ssStakePoolsSnapShot :: SnapShot -> VMap VB VB (KeyHash StakePool) StakePoolSnapShot
ssTotalActiveStake :: SnapShot -> NonZero Coin
..}) =
    HSMap Credential Integer
-> HSMap Credential Integer
-> HSMap Integer StakePoolParams
-> Snapshot
Agda.MkSnapshot
      (HSMap Credential Integer
 -> HSMap Credential Integer
 -> HSMap Integer StakePoolParams
 -> Snapshot)
-> SpecTransM ConwayEra () (HSMap Credential Integer)
-> SpecTransM
     ConwayEra
     ()
     (HSMap Credential Integer
      -> HSMap Integer StakePoolParams -> Snapshot)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Stake
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Stake) (SpecRep ConwayEra Stake)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (VMap VB VP (Credential Staking) (CompactForm Coin) -> Stake
Stake (VMap VB VP (Credential Staking) (CompactForm Coin) -> Stake)
-> VMap VB VP (Credential Staking) (CompactForm Coin) -> Stake
forall a b. (a -> b) -> a -> b
$ Map (Credential Staking) (CompactForm Coin)
-> VMap VB VP (Credential Staking) (CompactForm Coin)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (Map (Credential Staking) (CompactForm Coin)
 -> VMap VB VP (Credential Staking) (CompactForm Coin))
-> Map (Credential Staking) (CompactForm Coin)
-> VMap VB VP (Credential Staking) (CompactForm Coin)
forall a b. (a -> b) -> a -> b
$ (StakeWithDelegation -> CompactForm Coin)
-> Map (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) (CompactForm Coin)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (NonZero (CompactForm Coin) -> CompactForm Coin
forall a. NonZero a -> a
unNonZero (NonZero (CompactForm Coin) -> CompactForm Coin)
-> (StakeWithDelegation -> NonZero (CompactForm Coin))
-> StakeWithDelegation
-> CompactForm Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StakeWithDelegation -> NonZero (CompactForm Coin)
swdStake) Map (Credential Staking) StakeWithDelegation
activeStakeMap)
      SpecTransM
  ConwayEra
  ()
  (HSMap Credential Integer
   -> HSMap Integer StakePoolParams -> Snapshot)
-> SpecTransM ConwayEra () (HSMap Credential Integer)
-> SpecTransM
     ConwayEra () (HSMap Integer StakePoolParams -> Snapshot)
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 Staking) (KeyHash StakePool)
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (Credential Staking))
        (SpecRep ConwayEra (KeyHash StakePool)))
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 ((StakeWithDelegation -> KeyHash StakePool)
-> Map (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) (KeyHash StakePool)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map StakeWithDelegation -> KeyHash StakePool
swdDelegation Map (Credential Staking) StakeWithDelegation
activeStakeMap)
      SpecTransM ConwayEra () (HSMap Integer StakePoolParams -> Snapshot)
-> SpecTransM ConwayEra () (HSMap Integer StakePoolParams)
-> SpecTransM ConwayEra () Snapshot
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 (KeyHash StakePool) StakePoolSnapShot
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (KeyHash StakePool))
        (SpecRep ConwayEra StakePoolSnapShot))
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 (VMap VB VB (KeyHash StakePool) StakePoolSnapShot
-> Map (KeyHash StakePool) StakePoolSnapShot
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap VMap VB VB (KeyHash StakePool) StakePoolSnapShot
ssStakePoolsSnapShot)
    where
      activeStakeMap :: Map (Credential Staking) StakeWithDelegation
activeStakeMap = VMap VB VS (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) StakeWithDelegation
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap (VMap VB VS (Credential Staking) StakeWithDelegation
 -> Map (Credential Staking) StakeWithDelegation)
-> VMap VB VS (Credential Staking) StakeWithDelegation
-> Map (Credential Staking) StakeWithDelegation
forall a b. (a -> b) -> a -> b
$ ActiveStake -> VMap VB VS (Credential Staking) StakeWithDelegation
unActiveStake ActiveStake
ssActiveStake

instance SpecTranslate ConwayEra StakePoolSnapShot where
  type SpecRep ConwayEra StakePoolSnapShot = Agda.StakePoolParams

  toSpecRep :: StakePoolSnapShot
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra StakePoolSnapShot)
     (SpecRep ConwayEra StakePoolSnapShot)
toSpecRep StakePoolSnapShot {Int
Rational
Set (KeyHash Staking)
AccountId
VRFVerKeyHash StakePoolVRF
Coin
CompactForm Coin
UnitInterval
spssStake :: CompactForm Coin
spssStakeRatio :: Rational
spssSelfDelegatedOwners :: Set (KeyHash Staking)
spssSelfDelegatedOwnersStake :: Coin
spssVrf :: VRFVerKeyHash StakePoolVRF
spssPledge :: Coin
spssCost :: Coin
spssMargin :: UnitInterval
spssNumDelegators :: Int
spssAccountId :: AccountId
spssAccountId :: StakePoolSnapShot -> AccountId
spssCost :: StakePoolSnapShot -> Coin
spssMargin :: StakePoolSnapShot -> UnitInterval
spssNumDelegators :: StakePoolSnapShot -> Int
spssPledge :: StakePoolSnapShot -> Coin
spssSelfDelegatedOwners :: StakePoolSnapShot -> Set (KeyHash Staking)
spssSelfDelegatedOwnersStake :: StakePoolSnapShot -> Coin
spssStake :: StakePoolSnapShot -> CompactForm Coin
spssStakeRatio :: StakePoolSnapShot -> Rational
spssVrf :: StakePoolSnapShot -> VRFVerKeyHash StakePoolVRF
..} =
    HSSet Integer
-> Integer -> Rational -> Integer -> Credential -> StakePoolParams
Agda.StakePoolParams
      (HSSet Integer
 -> Integer -> Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM ConwayEra () (HSSet Integer)
-> SpecTransM
     ConwayEra
     ()
     (Integer -> Rational -> Integer -> Credential -> StakePoolParams)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (KeyHash Staking)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Set (KeyHash Staking)))
     (SpecRep ConwayEra (Set (KeyHash Staking)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Set (KeyHash Staking)
spssSelfDelegatedOwners
      SpecTransM
  ConwayEra
  ()
  (Integer -> Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM ConwayEra () Integer
-> SpecTransM
     ConwayEra () (Rational -> Integer -> Credential -> StakePoolParams)
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
spssCost
      SpecTransM
  ConwayEra () (Rational -> Integer -> Credential -> StakePoolParams)
-> SpecTransM ConwayEra () Rational
-> SpecTransM
     ConwayEra () (Integer -> Credential -> StakePoolParams)
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
<*> UnitInterval
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra UnitInterval)
     (SpecRep ConwayEra UnitInterval)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep UnitInterval
spssMargin
      SpecTransM ConwayEra () (Integer -> Credential -> StakePoolParams)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (Credential -> StakePoolParams)
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
spssPledge
      SpecTransM ConwayEra () (Credential -> StakePoolParams)
-> SpecTransM ConwayEra () Credential
-> SpecTransM ConwayEra () StakePoolParams
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
<*> Credential Staking
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Credential Staking))
     (SpecRep ConwayEra (Credential Staking))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep (AccountId -> Credential Staking
unAccountId AccountId
spssAccountId)

instance SpecTranslate ConwayEra Stake where
  type SpecRep ConwayEra Stake = Agda.HSMap Agda.Credential Agda.Coin

  toSpecRep :: Stake
-> SpecTransM
     ConwayEra (SpecContext ConwayEra Stake) (SpecRep ConwayEra Stake)
toSpecRep (Stake VMap VB VP (Credential Staking) (CompactForm Coin)
stake) = Map (Credential Staking) (CompactForm Coin)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra Stake)
     (HSMap
        (SpecRep ConwayEra (Credential Staking))
        (SpecRep ConwayEra (CompactForm Coin)))
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 (Map (Credential Staking) (CompactForm Coin)
 -> SpecTransM
      ConwayEra
      (SpecContext ConwayEra Stake)
      (HSMap
         (SpecRep ConwayEra (Credential Staking))
         (SpecRep ConwayEra (CompactForm Coin))))
-> Map (Credential Staking) (CompactForm Coin)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra Stake)
     (HSMap
        (SpecRep ConwayEra (Credential Staking))
        (SpecRep ConwayEra (CompactForm Coin)))
forall a b. (a -> b) -> a -> b
$ VMap VB VP (Credential Staking) (CompactForm Coin)
-> Map (Credential Staking) (CompactForm Coin)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap VMap VB VP (Credential Staking) (CompactForm Coin)
stake

instance SpecTranslate ConwayEra ChainAccountState where
  type SpecRep ConwayEra ChainAccountState = Agda.Acnt

  toSpecRep :: ChainAccountState
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra ChainAccountState)
     (SpecRep ConwayEra ChainAccountState)
toSpecRep (ChainAccountState {Coin
casTreasury :: Coin
casReserves :: Coin
casReserves :: ChainAccountState -> Coin
casTreasury :: ChainAccountState -> Coin
..}) =
    Integer -> Integer -> Acnt
Agda.MkAcnt
      (Integer -> Integer -> Acnt)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (Integer -> Acnt)
forall (f :: * -> *) a b. Functor 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
casTreasury
      SpecTransM ConwayEra () (Integer -> Acnt)
-> SpecTransM ConwayEra () Integer -> SpecTransM ConwayEra () Acnt
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
casReserves

instance SpecTranslate ConwayEra DeltaCoin where
  type SpecRep ConwayEra DeltaCoin = Integer

  toSpecRep :: DeltaCoin
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra DeltaCoin)
     (SpecRep ConwayEra DeltaCoin)
toSpecRep (DeltaCoin Integer
x) = Integer -> SpecTransM ConwayEra () Integer
forall a. a -> SpecTransM ConwayEra () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
x

instance SpecTranslate ConwayEra PulsingRewUpdate where
  type SpecRep ConwayEra PulsingRewUpdate = Agda.HsRewardUpdate

  toSpecRep :: PulsingRewUpdate
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra PulsingRewUpdate)
     (SpecRep ConwayEra PulsingRewUpdate)
toSpecRep PulsingRewUpdate
x =
    Integer
-> Integer -> Integer -> HSMap Credential Integer -> HsRewardUpdate
Agda.MkRewardUpdate
      (Integer
 -> Integer
 -> Integer
 -> HSMap Credential Integer
 -> HsRewardUpdate)
-> SpecTransM ConwayEra () Integer
-> SpecTransM
     ConwayEra
     ()
     (Integer -> Integer -> HSMap Credential Integer -> HsRewardUpdate)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeltaCoin
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra DeltaCoin)
     (SpecRep ConwayEra DeltaCoin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DeltaCoin
deltaT
      SpecTransM
  ConwayEra
  ()
  (Integer -> Integer -> HSMap Credential Integer -> HsRewardUpdate)
-> SpecTransM ConwayEra () Integer
-> SpecTransM
     ConwayEra
     ()
     (Integer -> HSMap Credential Integer -> HsRewardUpdate)
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
<*> DeltaCoin
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra DeltaCoin)
     (SpecRep ConwayEra DeltaCoin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DeltaCoin
deltaR
      SpecTransM
  ConwayEra
  ()
  (Integer -> HSMap Credential Integer -> HsRewardUpdate)
-> SpecTransM ConwayEra () Integer
-> SpecTransM
     ConwayEra () (HSMap Credential Integer -> HsRewardUpdate)
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
<*> DeltaCoin
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra DeltaCoin)
     (SpecRep ConwayEra DeltaCoin)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep DeltaCoin
deltaF
      SpecTransM
  ConwayEra () (HSMap Credential Integer -> HsRewardUpdate)
-> SpecTransM ConwayEra () (HSMap Credential Integer)
-> SpecTransM ConwayEra () HsRewardUpdate
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 Staking) Coin
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (Credential Staking)) (SpecRep ConwayEra Coin))
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 Map (Credential Staking) Coin
rwds
    where
      (RewardUpdate {RewardEvent
DeltaCoin
NonMyopic
deltaT :: DeltaCoin
deltaR :: DeltaCoin
deltaF :: DeltaCoin
rs :: RewardEvent
nonMyopic :: NonMyopic
nonMyopic :: RewardUpdate -> NonMyopic
deltaF :: RewardUpdate -> DeltaCoin
rs :: RewardUpdate -> RewardEvent
deltaR :: RewardUpdate -> DeltaCoin
deltaT :: RewardUpdate -> DeltaCoin
..}, RewardEvent
_) = ShelleyBase (RewardUpdate, RewardEvent)
-> (RewardUpdate, RewardEvent)
forall a. ShelleyBase a -> a
runShelleyBase (ShelleyBase (RewardUpdate, RewardEvent)
 -> (RewardUpdate, RewardEvent))
-> ShelleyBase (RewardUpdate, RewardEvent)
-> (RewardUpdate, RewardEvent)
forall a b. (a -> b) -> a -> b
$ PulsingRewUpdate -> ShelleyBase (RewardUpdate, RewardEvent)
completeRupd PulsingRewUpdate
x
      rwds :: Map (Credential Staking) Coin
rwds = (Reward -> Coin) -> Set Reward -> Coin
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Set.foldMap Reward -> Coin
rewardAmount (Set Reward -> Coin)
-> RewardEvent -> Map (Credential Staking) Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewardEvent
rs

instance SpecTranslate ConwayEra (NewEpochState ConwayEra) where
  type SpecRep ConwayEra (NewEpochState ConwayEra) = Agda.NewEpochState

  toSpecRep :: NewEpochState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (NewEpochState ConwayEra))
     (SpecRep ConwayEra (NewEpochState ConwayEra))
toSpecRep (NewEpochState {StrictMaybe PulsingRewUpdate
PoolDistr
EpochNo
BlocksMade
StashedAVVMAddresses ConwayEra
EpochState ConwayEra
nesEL :: EpochNo
nesBprev :: BlocksMade
nesBcur :: BlocksMade
nesEs :: EpochState ConwayEra
nesRu :: StrictMaybe PulsingRewUpdate
nesPd :: PoolDistr
stashedAVVMAddresses :: StashedAVVMAddresses ConwayEra
stashedAVVMAddresses :: forall era. NewEpochState era -> StashedAVVMAddresses era
nesPd :: forall era. NewEpochState era -> PoolDistr
nesRu :: forall era. NewEpochState era -> StrictMaybe PulsingRewUpdate
nesEs :: forall era. NewEpochState era -> EpochState era
nesBcur :: forall era. NewEpochState era -> BlocksMade
nesBprev :: forall era. NewEpochState era -> BlocksMade
nesEL :: forall era. NewEpochState era -> EpochNo
..}) =
    Integer
-> HSMap Integer Integer
-> HSMap Integer Integer
-> EpochState
-> Maybe HsRewardUpdate
-> HSMap Integer Integer
-> NewEpochState
Agda.MkNewEpochState
      (Integer
 -> HSMap Integer Integer
 -> HSMap Integer Integer
 -> EpochState
 -> Maybe HsRewardUpdate
 -> HSMap Integer Integer
 -> NewEpochState)
-> SpecTransM ConwayEra () Integer
-> SpecTransM
     ConwayEra
     ()
     (HSMap Integer Integer
      -> HSMap Integer Integer
      -> EpochState
      -> Maybe HsRewardUpdate
      -> HSMap Integer Integer
      -> NewEpochState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EpochNo
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra EpochNo)
     (SpecRep ConwayEra EpochNo)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep EpochNo
nesEL
      SpecTransM
  ConwayEra
  ()
  (HSMap Integer Integer
   -> HSMap Integer Integer
   -> EpochState
   -> Maybe HsRewardUpdate
   -> HSMap Integer Integer
   -> NewEpochState)
-> SpecTransM ConwayEra () (HSMap Integer Integer)
-> SpecTransM
     ConwayEra
     ()
     (HSMap Integer Integer
      -> EpochState
      -> Maybe HsRewardUpdate
      -> HSMap Integer Integer
      -> NewEpochState)
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
<*> BlocksMade
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra BlocksMade)
     (SpecRep ConwayEra BlocksMade)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep BlocksMade
nesBprev
      SpecTransM
  ConwayEra
  ()
  (HSMap Integer Integer
   -> EpochState
   -> Maybe HsRewardUpdate
   -> HSMap Integer Integer
   -> NewEpochState)
-> SpecTransM ConwayEra () (HSMap Integer Integer)
-> SpecTransM
     ConwayEra
     ()
     (EpochState
      -> Maybe HsRewardUpdate -> HSMap Integer Integer -> NewEpochState)
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
<*> BlocksMade
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra BlocksMade)
     (SpecRep ConwayEra BlocksMade)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep BlocksMade
nesBcur
      SpecTransM
  ConwayEra
  ()
  (EpochState
   -> Maybe HsRewardUpdate -> HSMap Integer Integer -> NewEpochState)
-> SpecTransM ConwayEra () EpochState
-> SpecTransM
     ConwayEra
     ()
     (Maybe HsRewardUpdate -> HSMap Integer Integer -> NewEpochState)
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
<*> EpochState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (EpochState ConwayEra))
     (SpecRep ConwayEra (EpochState ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep EpochState ConwayEra
nesEs
      SpecTransM
  ConwayEra
  ()
  (Maybe HsRewardUpdate -> HSMap Integer Integer -> NewEpochState)
-> SpecTransM ConwayEra () (Maybe HsRewardUpdate)
-> SpecTransM ConwayEra () (HSMap Integer Integer -> NewEpochState)
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 PulsingRewUpdate
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (StrictMaybe PulsingRewUpdate))
     (SpecRep ConwayEra (StrictMaybe PulsingRewUpdate))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep StrictMaybe PulsingRewUpdate
nesRu
      SpecTransM ConwayEra () (HSMap Integer Integer -> NewEpochState)
-> SpecTransM ConwayEra () (HSMap Integer Integer)
-> SpecTransM ConwayEra () NewEpochState
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
<*> (HSMap Integer Integer -> HSMap Integer Integer
forall {b} {k}. (Eq b, Num b) => HSMap k b -> HSMap k b
filterZeroEntries (HSMap Integer Integer -> HSMap Integer Integer)
-> SpecTransM ConwayEra () (HSMap Integer Integer)
-> SpecTransM ConwayEra () (HSMap Integer Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PoolDistr
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra PoolDistr)
     (SpecRep ConwayEra PoolDistr)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PoolDistr
nesPd)
    where
      -- The specification does not include zero entries in general
      -- while the implementation might. So we filter them out here for the sake
      -- of comparing results.
      --
      -- The discrepancy is discussed here:
      -- https://github.com/IntersectMBO/cardano-ledger/issues/5306
      filterZeroEntries :: HSMap k b -> HSMap k b
filterZeroEntries (Agda.MkHSMap [(k, b)]
lst) =
        [(k, b)] -> HSMap k b
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(k, b)] -> HSMap k b) -> [(k, b)] -> HSMap k b
forall a b. (a -> b) -> a -> b
$ ((k, b) -> Bool) -> [(k, b)] -> [(k, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((b -> b -> Bool
forall a. Eq a => a -> a -> Bool
/= b
0) (b -> Bool) -> ((k, b) -> b) -> (k, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k, b) -> b
forall a b. (a, b) -> b
snd) [(k, b)]
lst