{-# 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.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 qualified Data.Foldable as Set
import Data.Functor.Identity (Identity)
import Data.Map.Strict (Map, keysSet)
import qualified Data.VMap as VMap
import Lens.Micro
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.Constrained.Conway.Utxo (depositsMap)
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 era) (GovActionState era)
StrictMaybe (Committee era)
PParams era
EpochNo
cePParams :: PParams era
ceCurrentEpoch :: EpochNo
ceCurrentCommittee :: StrictMaybe (Committee era)
ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
cePParams :: forall era. CertEnv era -> PParams era
ceCurrentEpoch :: forall era. CertEnv era -> EpochNo
ceCurrentCommittee :: forall era. CertEnv era -> StrictMaybe (Committee era)
ceCommitteeProposals :: forall era.
CertEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
..} = do
    VotingProcedures era
votes <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(VotingProcedures era)
    Map RewardAccount Coin
withdrawals <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(Map RewardAccount Coin)
    let ccColdCreds :: Set (Credential 'ColdCommitteeRole)
ccColdCreds = (Committee era -> Set (Credential 'ColdCommitteeRole))
-> StrictMaybe (Committee era)
-> Set (Credential 'ColdCommitteeRole)
forall m a. Monoid m => (a -> m) -> StrictMaybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Map (Credential 'ColdCommitteeRole) EpochNo
-> Set (Credential 'ColdCommitteeRole)
forall k a. Map k a -> Set k
keysSet (Map (Credential 'ColdCommitteeRole) EpochNo
 -> Set (Credential 'ColdCommitteeRole))
-> (Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo)
-> Committee era
-> Set (Credential 'ColdCommitteeRole)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo
forall era.
Committee era -> Map (Credential 'ColdCommitteeRole) EpochNo
committeeMembers) StrictMaybe (Committee era)
ceCurrentCommittee
    Integer
-> PParams
-> [GovVote]
-> HSMap RwdAddr Integer
-> HSSet Credential
-> CertEnv
Agda.MkCertEnv
      (Integer
 -> PParams
 -> [GovVote]
 -> HSMap RwdAddr Integer
 -> HSSet Credential
 -> CertEnv)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx
     (PParams
      -> [GovVote]
      -> HSMap RwdAddr Integer
      -> HSSet Credential
      -> CertEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EpochNo -> SpecTransM ctx (SpecRep EpochNo)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep EpochNo
ceCurrentEpoch
      SpecTransM
  ctx
  (PParams
   -> [GovVote]
   -> HSMap RwdAddr Integer
   -> HSSet Credential
   -> CertEnv)
-> SpecTransM ctx PParams
-> SpecTransM
     ctx
     ([GovVote] -> HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PParams era -> SpecTransM ctx (SpecRep (PParams era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep PParams era
cePParams
      SpecTransM
  ctx
  ([GovVote] -> HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
-> SpecTransM ctx [GovVote]
-> SpecTransM
     ctx (HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VotingProcedures era
-> SpecTransM ctx (SpecRep (VotingProcedures era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep VotingProcedures era
votes
      SpecTransM
  ctx (HSMap RwdAddr Integer -> HSSet Credential -> CertEnv)
-> SpecTransM ctx (HSMap RwdAddr Integer)
-> SpecTransM ctx (HSSet Credential -> CertEnv)
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map RewardAccount Coin
-> SpecTransM ctx (SpecRep (Map RewardAccount Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map RewardAccount Coin
withdrawals
      SpecTransM ctx (HSSet Credential -> CertEnv)
-> SpecTransM ctx (HSSet Credential) -> SpecTransM ctx CertEnv
forall a b.
SpecTransM ctx (a -> b) -> SpecTransM ctx a -> SpecTransM ctx b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set (Credential 'ColdCommitteeRole)
-> SpecTransM ctx (SpecRep (Set (Credential 'ColdCommitteeRole)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Set (Credential 'ColdCommitteeRole)
ccColdCreds

instance SpecTranslate ctx (ConwayCertState era) where
  type SpecRep (ConwayCertState era) = Agda.CertState
  toSpecRep :: ConwayCertState era
-> SpecTransM ctx (SpecRep (ConwayCertState era))
toSpecRep ConwayCertState {PState era
DState era
VState era
conwayCertVState :: VState era
conwayCertPState :: PState era
conwayCertDState :: DState era
conwayCertVState :: forall era. ConwayCertState era -> VState era
conwayCertPState :: forall era. ConwayCertState era -> PState era
conwayCertDState :: forall era. ConwayCertState era -> DState 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

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
UTxO era
InstantStake era
Coin
utxosUtxo :: UTxO era
utxosDeposited :: Coin
utxosFees :: Coin
utxosGovState :: GovState era
utxosInstantStake :: InstantStake era
utxosDonation :: Coin
utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosDeposited :: forall era. UTxOState era -> Coin
utxosFees :: forall era. UTxOState era -> Coin
utxosGovState :: forall era. UTxOState era -> GovState era
utxosInstantStake :: forall era. UTxOState era -> InstantStake era
utxosDonation :: forall era. UTxOState era -> Coin
..} = do
    CertState era
certState <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(CertState era)
    let
      props :: Proposals era
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 :: Map DepositPurpose Coin
deposits = CertState era -> Proposals era -> Map DepositPurpose Coin
forall era.
ConwayEraCertState era =>
CertState era -> Proposals era -> Map DepositPurpose Coin
depositsMap CertState era
certState Proposals era
props
    HSMap (Integer, Integer) TxOut
-> Integer -> HSMap DepositPurpose Integer -> Integer -> UTxOState
Agda.MkUTxOState
      (HSMap (Integer, Integer) TxOut
 -> Integer -> HSMap DepositPurpose Integer -> Integer -> UTxOState)
-> SpecTransM ctx (HSMap (Integer, Integer) TxOut)
-> SpecTransM
     ctx
     (Integer -> HSMap DepositPurpose Integer -> Integer -> UTxOState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UTxO era -> SpecTransM ctx (SpecRep (UTxO era))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep UTxO era
utxosUtxo
      SpecTransM
  ctx
  (Integer -> HSMap DepositPurpose Integer -> Integer -> UTxOState)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (HSMap DepositPurpose Integer -> Integer -> UTxOState)
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
utxosFees
      SpecTransM
  ctx (HSMap DepositPurpose Integer -> Integer -> UTxOState)
-> SpecTransM ctx (HSMap DepositPurpose Integer)
-> SpecTransM ctx (Integer -> UTxOState)
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 DepositPurpose Coin
-> SpecTransM ctx (SpecRep (Map DepositPurpose Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Map DepositPurpose Coin
deposits
      SpecTransM ctx (Integer -> UTxOState)
-> SpecTransM ctx Integer -> SpecTransM ctx UTxOState
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
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
lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsCertState :: forall era. LedgerState era -> CertState 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 :: Map DepositPurpose Coin
deposits = CertState era -> Proposals era -> Map DepositPurpose Coin
forall era.
ConwayEraCertState era =>
CertState era -> Proposals era -> Map DepositPurpose Coin
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
<*> Map DepositPurpose Coin
-> SpecTransM (Map DepositPurpose Coin) CertState
-> SpecTransM ctx CertState
forall ctx a ctx'. ctx -> SpecTransM ctx a -> SpecTransM ctx' a
withCtx Map DepositPurpose Coin
deposits (ConwayCertState era
-> SpecTransM
     (Map DepositPurpose Coin) (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 ctx (PParamsHKD Identity era)
  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , Inject ctx [GovActionState era]
  , 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
esChainAccountState :: forall era. EpochState era -> ChainAccountState
esSnapshots :: forall era. EpochState era -> SnapShots
esNonMyopic :: forall era. EpochState era -> NonMyopic
..}) =
    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
<*> RatifyState era -> SpecTransM ctx (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 = EnactState era
-> Seq (GovActionState era)
-> Set GovActionId
-> Bool
-> RatifyState era
forall era.
EnactState era
-> Seq (GovActionState era)
-> Set GovActionId
-> Bool
-> RatifyState era
RatifyState EnactState era
enactState Seq (GovActionState era)
forall a. Monoid a => a
mempty Set GovActionId
forall a. Monoid a => a
mempty Bool
False

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
$sel:ssFee:SnapShots :: SnapShots -> Coin
$sel:ssStakeGo:SnapShots :: SnapShots -> SnapShot
$sel:ssStakeMark:SnapShots :: SnapShots -> SnapShot
$sel:ssStakeMarkPoolDistr:SnapShots :: SnapShots -> PoolDistr
$sel:ssStakeSet:SnapShots :: 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) PoolParams
VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
ssStake :: Stake
ssDelegations :: VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
ssPoolParams :: VMap VB VB (KeyHash 'StakePool) PoolParams
$sel:ssDelegations:SnapShot :: SnapShot -> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
$sel:ssPoolParams:SnapShot :: SnapShot -> VMap VB VB (KeyHash 'StakePool) PoolParams
$sel:ssStake:SnapShot :: SnapShot -> Stake
..}) =
    HSMap Credential Integer -> HSMap Credential Integer -> Snapshot
Agda.MkSnapshot
      (HSMap Credential Integer -> HSMap Credential Integer -> Snapshot)
-> SpecTransM ctx (HSMap Credential Integer)
-> SpecTransM ctx (HSMap Credential Integer -> 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 -> Snapshot)
-> SpecTransM ctx (HSMap Credential Integer)
-> 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 (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)

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
casTreasury :: ChainAccountState -> Coin
casReserves :: 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
deltaT :: RewardUpdate -> DeltaCoin
deltaR :: RewardUpdate -> DeltaCoin
rs :: RewardUpdate -> RewardEvent
deltaF :: RewardUpdate -> DeltaCoin
nonMyopic :: RewardUpdate -> NonMyopic
..}, 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)
  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
  , Inject ctx [GovActionState era]
  , 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
nesEL :: forall era. NewEpochState era -> EpochNo
nesBprev :: forall era. NewEpochState era -> BlocksMade
nesBcur :: forall era. NewEpochState era -> BlocksMade
nesEs :: forall era. NewEpochState era -> EpochState era
nesRu :: forall era. NewEpochState era -> StrictMaybe PulsingRewUpdate
nesPd :: forall era. NewEpochState era -> PoolDistr
stashedAVVMAddresses :: forall era. NewEpochState era -> StashedAVVMAddresses era
..}) =
    Integer -> EpochState -> Maybe HsRewardUpdate -> NewEpochState
Agda.MkNewEpochState
      (Integer -> EpochState -> Maybe HsRewardUpdate -> NewEpochState)
-> SpecTransM ctx Integer
-> SpecTransM
     ctx (EpochState -> Maybe HsRewardUpdate -> 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 (EpochState -> Maybe HsRewardUpdate -> NewEpochState)
-> SpecTransM ctx EpochState
-> SpecTransM ctx (Maybe HsRewardUpdate -> 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 -> NewEpochState)
-> SpecTransM ctx (Maybe HsRewardUpdate)
-> 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
<*> StrictMaybe PulsingRewUpdate
-> SpecTransM ctx (SpecRep (StrictMaybe PulsingRewUpdate))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep StrictMaybe PulsingRewUpdate
nesRu

instance SpecTranslate ctx (ConwayNewEpochPredFailure era) where
  type SpecRep (ConwayNewEpochPredFailure era) = OpaqueErrorString
  toSpecRep :: ConwayNewEpochPredFailure era
-> SpecTransM ctx (SpecRep (ConwayNewEpochPredFailure era))
toSpecRep = OpaqueErrorString -> SpecTransM ctx OpaqueErrorString
forall a. a -> SpecTransM ctx a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OpaqueErrorString -> SpecTransM ctx OpaqueErrorString)
-> (ConwayNewEpochPredFailure era -> OpaqueErrorString)
-> ConwayNewEpochPredFailure era
-> SpecTransM ctx OpaqueErrorString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayNewEpochPredFailure era -> OpaqueErrorString
forall a. ToExpr a => a -> OpaqueErrorString
showOpaqueErrorString