{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool where import Cardano.Ledger.Core import Cardano.Ledger.Shelley.Rules import Cardano.Ledger.State import qualified Data.Map.Strict as Map import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base () instance ( SpecRep (PParamsHKD Identity era) ~ Agda.PParams , SpecTranslate ctx (PParamsHKD Identity era) ) => SpecTranslate ctx (PoolEnv era) where type SpecRep (PoolEnv era) = Agda.PParams toSpecRep :: PoolEnv era -> SpecTransM ctx (SpecRep (PoolEnv era)) toSpecRep (PoolEnv EpochNo _ PParams era pp) = PParams era -> SpecTransM ctx (SpecRep (PParams era)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep PParams era pp instance SpecTranslate ctx (PState era) where type SpecRep (PState era) = Agda.PState toSpecRep :: PState era -> SpecTransM ctx (SpecRep (PState era)) toSpecRep PState {Map (KeyHash 'StakePool) StakePoolState Map (KeyHash 'StakePool) EpochNo Map (VRFVerKeyHash 'StakePoolVRF) (NonZero Word64) psVRFKeyHashes :: Map (VRFVerKeyHash 'StakePoolVRF) (NonZero Word64) psStakePools :: Map (KeyHash 'StakePool) StakePoolState psFutureStakePools :: Map (KeyHash 'StakePool) StakePoolState psRetiring :: Map (KeyHash 'StakePool) EpochNo psVRFKeyHashes :: forall era. PState era -> Map (VRFVerKeyHash 'StakePoolVRF) (NonZero Word64) psStakePools :: forall era. PState era -> Map (KeyHash 'StakePool) StakePoolState psFutureStakePools :: forall era. PState era -> Map (KeyHash 'StakePool) StakePoolState psRetiring :: forall era. PState era -> Map (KeyHash 'StakePool) EpochNo ..} = HSMap Integer StakePoolParams -> HSMap Integer Integer -> PState Agda.MkPState (HSMap Integer StakePoolParams -> HSMap Integer Integer -> PState) -> SpecTransM ctx (HSMap Integer StakePoolParams) -> SpecTransM ctx (HSMap Integer Integer -> PState) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Map (KeyHash 'StakePool) PoolParams -> SpecTransM ctx (SpecRep (Map (KeyHash 'StakePool) PoolParams)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep ((KeyHash 'StakePool -> StakePoolState -> PoolParams) -> Map (KeyHash 'StakePool) StakePoolState -> Map (KeyHash 'StakePool) PoolParams forall k a b. (k -> a -> b) -> Map k a -> Map k b Map.mapWithKey KeyHash 'StakePool -> StakePoolState -> PoolParams stakePoolStateToPoolParams Map (KeyHash 'StakePool) StakePoolState psStakePools) SpecTransM ctx (HSMap Integer Integer -> PState) -> SpecTransM ctx (HSMap Integer Integer) -> SpecTransM ctx PState 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) EpochNo -> SpecTransM ctx (SpecRep (Map (KeyHash 'StakePool) EpochNo)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Map (KeyHash 'StakePool) EpochNo psRetiring instance SpecTranslate ctx PoolCert where type SpecRep PoolCert = Agda.DCert toSpecRep :: PoolCert -> SpecTransM ctx (SpecRep PoolCert) toSpecRep (RegPool p :: PoolParams p@PoolParams {ppId :: PoolParams -> KeyHash 'StakePool ppId = KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN) ppHash}) = Integer -> StakePoolParams -> DCert Agda.Regpool (Integer -> StakePoolParams -> DCert) -> SpecTransM ctx Integer -> SpecTransM ctx (StakePoolParams -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Hash ADDRHASH (VerKeyDSIGN DSIGN) -> SpecTransM ctx (SpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN))) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN) ppHash SpecTransM ctx (StakePoolParams -> DCert) -> SpecTransM ctx StakePoolParams -> SpecTransM ctx DCert 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 <*> PoolParams -> SpecTransM ctx (SpecRep PoolParams) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep PoolParams p toSpecRep (RetirePool (KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN) ppHash) EpochNo e) = Integer -> Integer -> DCert Agda.Retirepool (Integer -> Integer -> DCert) -> SpecTransM ctx Integer -> SpecTransM ctx (Integer -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Hash ADDRHASH (VerKeyDSIGN DSIGN) -> SpecTransM ctx (SpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN))) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN) ppHash SpecTransM ctx (Integer -> DCert) -> SpecTransM ctx Integer -> SpecTransM ctx DCert 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 <*> EpochNo -> SpecTransM ctx (SpecRep EpochNo) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep EpochNo e