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

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

import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin
import Cardano.Ledger.Compactible (Compactible (..))
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Shelley.LedgerState
import Data.Foldable (Foldable (..))
import qualified Data.Foldable as Set
import Data.Functor.Identity (Identity)
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.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance
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.Conway.TreeDiff
import Test.Cardano.Ledger.Shelley.Utils (runShelleyBase)

instance
  ( SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , Inject ctx (VotingProcedures era)
  , Inject ctx (Map RewardAccount Coin)
  ) =>
  SpecTranslate ctx (CertEnv era)
  where
  type SpecRep (CertEnv era) = Agda.CertEnv
  toSpecRep :: CertEnv era -> SpecTransM ctx (SpecRep (CertEnv era))
toSpecRep CertEnv {Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
StrictMaybe (Committee era)
PParams era
EpochNo
cePParams :: PParams era
ceCurrentEpoch :: EpochNo
ceCurrentCommittee :: StrictMaybe (Committee era)
ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
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 <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(VotingProcedures era)
    withdrawals <- askCtx @(Map RewardAccount Coin)
    let ccColdCreds = (Committee era -> Set (Credential ColdCommitteeRole))
-> StrictMaybe (Committee era)
-> Set (Credential ColdCommitteeRole)
forall m a. Monoid m => (a -> m) -> StrictMaybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Map (Credential ColdCommitteeRole) EpochNo
-> Set (Credential ColdCommitteeRole)
forall k a. Map k a -> Set k
keysSet (Map (Credential ColdCommitteeRole) EpochNo
 -> Set (Credential ColdCommitteeRole))
-> (Committee era -> Map (Credential ColdCommitteeRole) EpochNo)
-> Committee era
-> Set (Credential ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Committee era -> Map (Credential ColdCommitteeRole) EpochNo
forall era.
Committee era -> Map (Credential ColdCommitteeRole) EpochNo
committeeMembers) StrictMaybe (Committee era)
ceCurrentCommittee
    Agda.MkCertEnv
      <$> toSpecRep ceCurrentEpoch
      <*> toSpecRep cePParams
      <*> toSpecRep votes
      <*> toSpecRep withdrawals
      <*> toSpecRep ccColdCreds

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

instance Era era => SpecTranslate ctx (ConwayTxCert era) where
  type SpecRep (ConwayTxCert era) = Agda.DCert

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

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

instance
  ( SpecTranslate ctx (TxOut era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  , GovState era ~ ConwayGovState era
  , Inject ctx (CertState era)
  , ConwayEraCertState era
  ) =>
  SpecTranslate ctx (UTxOState era)
  where
  type SpecRep (UTxOState era) = Agda.UTxOState

  toSpecRep :: UTxOState era -> SpecTransM ctx (SpecRep (UTxOState era))
toSpecRep UTxOState {GovState era
InstantStake era
UTxO era
Coin
utxosUtxo :: UTxO era
utxosDeposited :: Coin
utxosFees :: Coin
utxosGovState :: GovState era
utxosInstantStake :: InstantStake era
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 <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(CertState era)
    let
      props = GovState era
ConwayGovState era
utxosGovState ConwayGovState era
-> Getting (Proposals era) (ConwayGovState era) (Proposals era)
-> Proposals era
forall s a. s -> Getting a s a -> a
^. Getting (Proposals era) (ConwayGovState era) (Proposals era)
forall era (f :: * -> *).
Functor f =>
(Proposals era -> f (Proposals era))
-> ConwayGovState era -> f (ConwayGovState era)
cgsProposalsL
      deposits = CertState era
-> Proposals era -> SpecTransM ctx (HSMap DepositPurpose Integer)
forall era ctx.
ConwayEraCertState era =>
CertState era
-> Proposals era -> SpecTransM ctx (HSMap DepositPurpose Integer)
depositsMap CertState era
certState Proposals era
props
    Agda.MkUTxOState
      <$> toSpecRep utxosUtxo
      <*> toSpecRep utxosFees
      <*> deposits
      <*> toSpecRep utxosDonation

instance
  ( ConwayEraGov era
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , SpecRep (TxOut era) ~ Agda.TxOut
  , GovState era ~ ConwayGovState era
  , SpecTranslate (CertState era) (TxOut era)
  , SpecRep (CertState era) ~ Agda.CertState
  , ConwayEraCertState era
  , CertState era ~ ConwayCertState era
  ) =>
  SpecTranslate ctx (LedgerState era)
  where
  type SpecRep (LedgerState era) = Agda.LState

  toSpecRep :: LedgerState era -> SpecTransM ctx (SpecRep (LedgerState era))
toSpecRep (LedgerState {CertState era
UTxOState era
lsUTxOState :: UTxOState era
lsCertState :: CertState era
lsCertState :: forall era. LedgerState era -> CertState era
lsUTxOState :: forall era. LedgerState era -> UTxOState era
..}) = do
    let
      props :: Proposals era
props = UTxOState era -> GovState era
forall era. UTxOState era -> GovState era
utxosGovState UTxOState era
lsUTxOState ConwayGovState era
-> Getting (Proposals era) (ConwayGovState era) (Proposals era)
-> Proposals era
forall s a. s -> Getting a s a -> a
^. (Proposals era -> Const (Proposals era) (Proposals era))
-> GovState era -> Const (Proposals era) (GovState era)
Getting (Proposals era) (ConwayGovState era) (Proposals era)
forall era.
ConwayEraGov era =>
Lens' (GovState era) (Proposals era)
Lens' (GovState era) (Proposals era)
proposalsGovStateL
      deposits :: SpecTransM (ZonkAny 0) (HSMap DepositPurpose Integer)
deposits = CertState era
-> Proposals era
-> SpecTransM (ZonkAny 0) (HSMap DepositPurpose Integer)
forall era ctx.
ConwayEraCertState era =>
CertState era
-> Proposals era -> SpecTransM ctx (HSMap DepositPurpose Integer)
depositsMap CertState era
lsCertState Proposals era
props
    UTxOState
-> [((Integer, Integer), GovActionState)] -> CertState -> LState
Agda.MkLState
      (UTxOState
 -> [((Integer, Integer), GovActionState)] -> CertState -> LState)
-> SpecTransM ctx UTxOState
-> SpecTransM
     ctx ([((Integer, Integer), GovActionState)] -> CertState -> LState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConwayCertState era
-> SpecTransM (ConwayCertState era) UTxOState
-> SpecTransM ctx UTxOState
forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx CertState era
ConwayCertState era
lsCertState (UTxOState era
-> SpecTransM (ConwayCertState era) (SpecRep (UTxOState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UTxOState era
lsUTxOState)
      SpecTransM
  ctx ([((Integer, Integer), GovActionState)] -> CertState -> LState)
-> SpecTransM ctx [((Integer, Integer), GovActionState)]
-> SpecTransM ctx (CertState -> LState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Proposals era -> SpecTransM ctx (SpecRep (Proposals era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Proposals era
props
      SpecTransM ctx (CertState -> LState)
-> SpecTransM ctx CertState -> SpecTransM ctx LState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SpecTransM (ZonkAny 0) (HSMap DepositPurpose Integer)
-> SpecTransM
     (SpecTransM (ZonkAny 0) (HSMap DepositPurpose Integer)) CertState
-> SpecTransM ctx CertState
forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx SpecTransM (ZonkAny 0) (HSMap DepositPurpose Integer)
deposits (ConwayCertState era
-> SpecTransM
     (SpecTransM (ZonkAny 0) (HSMap DepositPurpose Integer))
     (SpecRep (ConwayCertState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep CertState era
ConwayCertState era
lsCertState)

instance
  ( EraPParams era
  , ConwayEraGov era
  , SpecTranslate [GovActionState era] (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate [GovActionState era] (PParamsHKD StrictMaybe era)
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , ToExpr (PParamsHKD StrictMaybe era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  , GovState era ~ ConwayGovState era
  , SpecTranslate (CertState era) (TxOut era)
  , SpecRep (CertState era) ~ Agda.CertState
  , ConwayEraCertState era
  , CertState era ~ ConwayCertState era
  ) =>
  SpecTranslate ctx (EpochState era)
  where
  type SpecRep (EpochState era) = Agda.EpochState

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

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

  toSpecRep :: SnapShots -> SpecTransM ctx (SpecRep 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 ctx Snapshot
-> SpecTransM ctx (Snapshot -> Snapshot -> Integer -> Snapshots)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SnapShot -> SpecTransM ctx (SpecRep SnapShot)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SnapShot
ssStakeMark
      SpecTransM ctx (Snapshot -> Snapshot -> Integer -> Snapshots)
-> SpecTransM ctx Snapshot
-> SpecTransM ctx (Snapshot -> Integer -> Snapshots)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SnapShot -> SpecTransM ctx (SpecRep SnapShot)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SnapShot
ssStakeSet
      SpecTransM ctx (Snapshot -> Integer -> Snapshots)
-> SpecTransM ctx Snapshot -> SpecTransM ctx (Integer -> Snapshots)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SnapShot -> SpecTransM ctx (SpecRep SnapShot)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep SnapShot
ssStakeGo
      SpecTransM ctx (Integer -> Snapshots)
-> SpecTransM ctx Integer -> SpecTransM ctx Snapshots
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
ssFee

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

  toSpecRep :: SnapShot -> SpecTransM ctx (SpecRep SnapShot)
toSpecRep (SnapShot {Stake
VMap VB VB (KeyHash StakePool) StakePoolParams
VMap VB VB (Credential Staking) (KeyHash StakePool)
ssStake :: Stake
ssDelegations :: VMap VB VB (Credential Staking) (KeyHash StakePool)
ssPoolParams :: VMap VB VB (KeyHash StakePool) StakePoolParams
ssDelegations :: SnapShot -> VMap VB VB (Credential Staking) (KeyHash StakePool)
ssPoolParams :: SnapShot -> VMap VB VB (KeyHash StakePool) StakePoolParams
ssStake :: SnapShot -> Stake
..}) =
    HSMap Credential Integer
-> HSMap Credential Integer
-> HSMap Integer StakePoolParams
-> Snapshot
Agda.MkSnapshot
      (HSMap Credential Integer
 -> HSMap Credential Integer
 -> HSMap Integer StakePoolParams
 -> Snapshot)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM
     ctx
     (HSMap Credential Integer
      -> HSMap Integer StakePoolParams -> Snapshot)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Stake -> SpecTransM ctx (SpecRep Stake)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Stake
ssStake
      SpecTransM
  ctx
  (HSMap Credential Integer
   -> HSMap Integer StakePoolParams -> Snapshot)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM ctx (HSMap Integer StakePoolParams -> Snapshot)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (Credential Staking) (KeyHash StakePool)
-> SpecTransM
     ctx (SpecRep (Map (Credential Staking) (KeyHash StakePool)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VMap VB VB (Credential Staking) (KeyHash StakePool)
-> Map (Credential Staking) (KeyHash StakePool)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
VMap kv vv k v -> Map k v
VMap.toMap VMap VB VB (Credential Staking) (KeyHash StakePool)
ssDelegations)
      SpecTransM ctx (HSMap Integer StakePoolParams -> Snapshot)
-> SpecTransM ctx (HSMap Integer StakePoolParams)
-> SpecTransM ctx Snapshot
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (KeyHash StakePool) StakePoolParams
-> SpecTransM
     ctx (SpecRep (Map (KeyHash StakePool) StakePoolParams))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (VMap VB VB (KeyHash StakePool) StakePoolParams
-> Map (KeyHash StakePool) StakePoolParams
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) StakePoolParams
ssPoolParams)

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

  toSpecRep :: Stake -> SpecTransM ctx (SpecRep Stake)
toSpecRep (Stake VMap VB VP (Credential Staking) (CompactForm Coin)
stake) = Map (Credential Staking) (CompactForm Coin)
-> SpecTransM
     ctx (SpecRep (Map (Credential Staking) (CompactForm Coin)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep (Map (Credential Staking) (CompactForm Coin)
 -> SpecTransM
      ctx (SpecRep (Map (Credential Staking) (CompactForm Coin))))
-> Map (Credential Staking) (CompactForm Coin)
-> SpecTransM
     ctx (SpecRep (Map (Credential Staking) (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 ctx ChainAccountState where
  type SpecRep ChainAccountState = Agda.Acnt

  toSpecRep :: ChainAccountState -> SpecTransM ctx (SpecRep ChainAccountState)
toSpecRep (ChainAccountState {Coin
casTreasury :: Coin
casReserves :: Coin
casReserves :: ChainAccountState -> Coin
casTreasury :: ChainAccountState -> Coin
..}) =
    Integer -> Integer -> Acnt
Agda.MkAcnt
      (Integer -> Integer -> Acnt)
-> SpecTransM ctx Integer -> SpecTransM ctx (Integer -> Acnt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
casTreasury
      SpecTransM ctx (Integer -> Acnt)
-> SpecTransM ctx Integer -> SpecTransM ctx Acnt
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coin -> SpecTransM ctx (SpecRep Coin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Coin
casReserves

instance SpecTranslate ctx DeltaCoin where
  type SpecRep DeltaCoin = Integer

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

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

  toSpecRep :: PulsingRewUpdate -> SpecTransM ctx (SpecRep PulsingRewUpdate)
toSpecRep PulsingRewUpdate
x =
    Integer
-> Integer -> Integer -> HSMap Credential Integer -> HsRewardUpdate
Agda.MkRewardUpdate
      (Integer
 -> Integer
 -> Integer
 -> HSMap Credential Integer
 -> HsRewardUpdate)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (Integer -> Integer -> HSMap Credential Integer -> HsRewardUpdate)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeltaCoin -> SpecTransM ctx (SpecRep DeltaCoin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DeltaCoin
deltaT
      SpecTransM
  ctx
  (Integer -> Integer -> HSMap Credential Integer -> HsRewardUpdate)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (Integer -> HSMap Credential Integer -> HsRewardUpdate)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DeltaCoin -> SpecTransM ctx (SpecRep DeltaCoin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DeltaCoin
deltaR
      SpecTransM
  ctx (Integer -> HSMap Credential Integer -> HsRewardUpdate)
-> SpecTransM ctx Integer
-> SpecTransM ctx (HSMap Credential Integer -> HsRewardUpdate)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DeltaCoin -> SpecTransM ctx (SpecRep DeltaCoin)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep DeltaCoin
deltaF
      SpecTransM ctx (HSMap Credential Integer -> HsRewardUpdate)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM ctx HsRewardUpdate
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (Credential Staking) Coin
-> SpecTransM ctx (SpecRep (Map (Credential Staking) Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep 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
  ( EraPParams era
  , ConwayEraGov era
  , SpecTranslate ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecTranslate [GovActionState era] (PParamsHKD Identity era)
  , SpecTranslate [GovActionState era] (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , ToExpr (PParamsHKD StrictMaybe era)
  , SpecRep (TxOut era) ~ Agda.TxOut
  , GovState era ~ ConwayGovState era
  , SpecTranslate (CertState era) (TxOut era)
  , SpecRep (CertState era) ~ Agda.CertState
  , ConwayEraCertState era
  , CertState era ~ ConwayCertState era
  ) =>
  SpecTranslate ctx (NewEpochState era)
  where
  type SpecRep (NewEpochState era) = Agda.NewEpochState

  toSpecRep :: NewEpochState era -> SpecTransM ctx (SpecRep (NewEpochState era))
toSpecRep (NewEpochState {StrictMaybe PulsingRewUpdate
PoolDistr
EpochNo
BlocksMade
StashedAVVMAddresses era
EpochState era
nesEL :: EpochNo
nesBprev :: BlocksMade
nesBcur :: BlocksMade
nesEs :: EpochState era
nesRu :: StrictMaybe PulsingRewUpdate
nesPd :: PoolDistr
stashedAVVMAddresses :: StashedAVVMAddresses era
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 ctx Integer
-> SpecTransM
     ctx
     (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 ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
nesEL
      SpecTransM
  ctx
  (HSMap Integer Integer
   -> HSMap Integer Integer
   -> EpochState
   -> Maybe HsRewardUpdate
   -> HSMap Integer Integer
   -> NewEpochState)
-> SpecTransM ctx (HSMap Integer Integer)
-> SpecTransM
     ctx
     (HSMap Integer Integer
      -> EpochState
      -> Maybe HsRewardUpdate
      -> HSMap Integer Integer
      -> NewEpochState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlocksMade -> SpecTransM ctx (SpecRep BlocksMade)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep BlocksMade
nesBprev
      SpecTransM
  ctx
  (HSMap Integer Integer
   -> EpochState
   -> Maybe HsRewardUpdate
   -> HSMap Integer Integer
   -> NewEpochState)
-> SpecTransM ctx (HSMap Integer Integer)
-> SpecTransM
     ctx
     (EpochState
      -> Maybe HsRewardUpdate -> HSMap Integer Integer -> NewEpochState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlocksMade -> SpecTransM ctx (SpecRep BlocksMade)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep BlocksMade
nesBcur
      SpecTransM
  ctx
  (EpochState
   -> Maybe HsRewardUpdate -> HSMap Integer Integer -> NewEpochState)
-> SpecTransM ctx EpochState
-> SpecTransM
     ctx
     (Maybe HsRewardUpdate -> HSMap Integer Integer -> NewEpochState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochState era -> SpecTransM ctx (SpecRep (EpochState era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochState era
nesEs
      SpecTransM
  ctx
  (Maybe HsRewardUpdate -> HSMap Integer Integer -> NewEpochState)
-> SpecTransM ctx (Maybe HsRewardUpdate)
-> SpecTransM ctx (HSMap Integer Integer -> NewEpochState)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictMaybe PulsingRewUpdate
-> SpecTransM ctx (SpecRep (StrictMaybe PulsingRewUpdate))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe PulsingRewUpdate
nesRu
      SpecTransM ctx (HSMap Integer Integer -> NewEpochState)
-> SpecTransM ctx (HSMap Integer Integer)
-> SpecTransM ctx NewEpochState
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (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 ctx (HSMap Integer Integer)
-> SpecTransM ctx (HSMap Integer Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PoolDistr -> SpecTransM ctx (SpecRep PoolDistr)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep 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