{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg () where import Cardano.Ledger.BaseTypes import Cardano.Ledger.Conway.Rules ( ConwayDelegEnv (..), ConwayDelegPredFailure, ) import Cardano.Ledger.Conway.TxCert ( ConwayDelegCert (..), getStakePoolDelegatee, getVoteDelegatee, ) import Cardano.Ledger.Core import Cardano.Ledger.Credential (Credential) import Cardano.Ledger.Shelley.LedgerState (DState (..)) import Cardano.Ledger.Shelley.Rules import qualified Cardano.Ledger.UMap as UMap import qualified Data.Map.Strict as Map import Data.Set (Set) import qualified MAlonzo.Code.Ledger.Foreign.API as Agda import Test.Cardano.Ledger.Conformance ( hashToInteger, ) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base import Test.Cardano.Ledger.Conformance.SpecTranslate.Core instance ( SpecRep (PParamsHKD Identity era) ~ Agda.PParams , SpecTranslate ctx (PParamsHKD Identity era) , Inject ctx (Set (Credential 'DRepRole)) ) => SpecTranslate ctx (ConwayDelegEnv era) where type SpecRep (ConwayDelegEnv era) = Agda.DelegEnv toSpecRep :: ConwayDelegEnv era -> SpecTransM ctx (SpecRep (ConwayDelegEnv era)) toSpecRep ConwayDelegEnv {Map (KeyHash 'StakePool) PoolParams PParams era cdePParams :: PParams era cdePools :: Map (KeyHash 'StakePool) PoolParams cdePParams :: forall era. ConwayDelegEnv era -> PParams era cdePools :: forall era. ConwayDelegEnv era -> Map (KeyHash 'StakePool) PoolParams ..} = do Set (Credential 'DRepRole) delegatees <- forall b ctx. Inject ctx b => SpecTransM ctx b askCtx @(Set (Credential 'DRepRole)) PParams -> HSMap Integer PoolParams -> HSSet Credential -> DelegEnv Agda.MkDelegEnv (PParams -> HSMap Integer PoolParams -> HSSet Credential -> DelegEnv) -> SpecTransM ctx PParams -> SpecTransM ctx (HSMap Integer PoolParams -> HSSet Credential -> DelegEnv) forall (f :: * -> *) a b. Functor 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 cdePParams SpecTransM ctx (HSMap Integer PoolParams -> HSSet Credential -> DelegEnv) -> SpecTransM ctx (HSMap Integer PoolParams) -> SpecTransM ctx (HSSet Credential -> DelegEnv) 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 Integer PoolParams -> SpecTransM ctx (SpecRep (Map Integer PoolParams)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep ((KeyHash 'StakePool -> Integer) -> Map (KeyHash 'StakePool) PoolParams -> Map Integer PoolParams forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a Map.mapKeys (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer forall a b. Hash a b -> Integer hashToInteger (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer) -> (KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN)) -> KeyHash 'StakePool -> Integer forall b c a. (b -> c) -> (a -> b) -> a -> c . KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN) forall (r :: KeyRole). KeyHash r -> Hash ADDRHASH (VerKeyDSIGN DSIGN) unKeyHash) Map (KeyHash 'StakePool) PoolParams cdePools) SpecTransM ctx (HSSet Credential -> DelegEnv) -> SpecTransM ctx (HSSet Credential) -> SpecTransM ctx DelegEnv 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 'DRepRole) -> SpecTransM ctx (SpecRep (Set (Credential 'DRepRole))) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Set (Credential 'DRepRole) delegatees instance SpecTranslate ctx ConwayDelegCert where type SpecRep ConwayDelegCert = Agda.DCert toSpecRep :: ConwayDelegCert -> SpecTransM ctx (SpecRep ConwayDelegCert) toSpecRep (ConwayRegCert StakeCredential c StrictMaybe Coin d) = Credential -> Integer -> DCert Agda.Reg (Credential -> Integer -> DCert) -> SpecTransM ctx Credential -> SpecTransM ctx (Integer -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep StakeCredential c 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 <*> SpecTransM ctx Integer -> (Coin -> SpecTransM ctx Integer) -> StrictMaybe Coin -> SpecTransM ctx Integer forall a b. a -> (b -> a) -> StrictMaybe b -> a strictMaybe (Integer -> SpecTransM ctx Integer forall a. a -> SpecTransM ctx a forall (f :: * -> *) a. Applicative f => a -> f a pure Integer 0) Coin -> SpecTransM ctx Integer Coin -> SpecTransM ctx (SpecRep Coin) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep StrictMaybe Coin d toSpecRep (ConwayUnRegCert StakeCredential c StrictMaybe Coin d) = Credential -> Maybe Integer -> DCert Agda.Dereg (Credential -> Maybe Integer -> DCert) -> SpecTransM ctx Credential -> SpecTransM ctx (Maybe Integer -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep StakeCredential c SpecTransM ctx (Maybe Integer -> DCert) -> SpecTransM ctx (Maybe 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 <*> StrictMaybe Coin -> SpecTransM ctx (SpecRep (StrictMaybe Coin)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep StrictMaybe Coin d toSpecRep (ConwayDelegCert StakeCredential c Delegatee d) = Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert Agda.Delegate (Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert) -> SpecTransM ctx Credential -> SpecTransM ctx (Maybe VDeleg -> Maybe Integer -> Integer -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep StakeCredential c SpecTransM ctx (Maybe VDeleg -> Maybe Integer -> Integer -> DCert) -> SpecTransM ctx (Maybe VDeleg) -> SpecTransM ctx (Maybe Integer -> Integer -> 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 <*> Maybe DRep -> SpecTransM ctx (SpecRep (Maybe DRep)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (Delegatee -> Maybe DRep getVoteDelegatee Delegatee d) SpecTransM ctx (Maybe Integer -> Integer -> DCert) -> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx (Integer -> 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 <*> Maybe Integer -> SpecTransM ctx (SpecRep (Maybe Integer)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer forall a b. Hash a b -> Integer hashToInteger (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer) -> (KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN)) -> KeyHash 'StakePool -> Integer forall b c a. (b -> c) -> (a -> b) -> a -> c . KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN) forall (r :: KeyRole). KeyHash r -> Hash ADDRHASH (VerKeyDSIGN DSIGN) unKeyHash (KeyHash 'StakePool -> Integer) -> Maybe (KeyHash 'StakePool) -> Maybe Integer forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Delegatee -> Maybe (KeyHash 'StakePool) getStakePoolDelegatee Delegatee d) 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 <*> Integer -> SpecTransM ctx Integer forall a. a -> SpecTransM ctx a forall (f :: * -> *) a. Applicative f => a -> f a pure Integer 0 toSpecRep (ConwayRegDelegCert StakeCredential s Delegatee d Coin c) = Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert Agda.Delegate (Credential -> Maybe VDeleg -> Maybe Integer -> Integer -> DCert) -> SpecTransM ctx Credential -> SpecTransM ctx (Maybe VDeleg -> Maybe Integer -> Integer -> DCert) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StakeCredential -> SpecTransM ctx (SpecRep StakeCredential) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep StakeCredential s SpecTransM ctx (Maybe VDeleg -> Maybe Integer -> Integer -> DCert) -> SpecTransM ctx (Maybe VDeleg) -> SpecTransM ctx (Maybe Integer -> Integer -> 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 <*> Maybe DRep -> SpecTransM ctx (SpecRep (Maybe DRep)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (Delegatee -> Maybe DRep getVoteDelegatee Delegatee d) SpecTransM ctx (Maybe Integer -> Integer -> DCert) -> SpecTransM ctx (Maybe Integer) -> SpecTransM ctx (Integer -> 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 <*> Maybe Integer -> SpecTransM ctx (SpecRep (Maybe Integer)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer forall a b. Hash a b -> Integer hashToInteger (Hash ADDRHASH (VerKeyDSIGN DSIGN) -> Integer) -> (KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN)) -> KeyHash 'StakePool -> Integer forall b c a. (b -> c) -> (a -> b) -> a -> c . KeyHash 'StakePool -> Hash ADDRHASH (VerKeyDSIGN DSIGN) forall (r :: KeyRole). KeyHash r -> Hash ADDRHASH (VerKeyDSIGN DSIGN) unKeyHash (KeyHash 'StakePool -> Integer) -> Maybe (KeyHash 'StakePool) -> Maybe Integer forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Delegatee -> Maybe (KeyHash 'StakePool) getStakePoolDelegatee Delegatee d) 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 <*> Coin -> SpecTransM ctx (SpecRep Coin) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep Coin c instance SpecTranslate ctx (ConwayDelegPredFailure era) where type SpecRep (ConwayDelegPredFailure era) = OpaqueErrorString toSpecRep :: ConwayDelegPredFailure era -> SpecTransM ctx (SpecRep (ConwayDelegPredFailure 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) -> (ConwayDelegPredFailure era -> OpaqueErrorString) -> ConwayDelegPredFailure era -> SpecTransM ctx OpaqueErrorString forall b c a. (b -> c) -> (a -> b) -> a -> c . ConwayDelegPredFailure era -> OpaqueErrorString forall a. ToExpr a => a -> OpaqueErrorString showOpaqueErrorString instance SpecTranslate ctx (DState era) where type SpecRep (DState era) = Agda.DState toSpecRep :: DState era -> SpecTransM ctx (SpecRep (DState era)) toSpecRep DState {Map FutureGenDeleg GenDelegPair InstantaneousRewards GenDelegs UMap dsUnified :: UMap dsFutureGenDelegs :: Map FutureGenDeleg GenDelegPair dsGenDelegs :: GenDelegs dsIRewards :: InstantaneousRewards dsUnified :: forall era. DState era -> UMap dsFutureGenDelegs :: forall era. DState era -> Map FutureGenDeleg GenDelegPair dsGenDelegs :: forall era. DState era -> GenDelegs dsIRewards :: forall era. DState era -> InstantaneousRewards ..} = HSMap Credential VDeleg -> HSMap Credential Integer -> HSMap Credential Integer -> HSMap DepositPurpose Integer -> DState Agda.MkDState (HSMap Credential VDeleg -> HSMap Credential Integer -> HSMap Credential Integer -> HSMap DepositPurpose Integer -> DState) -> SpecTransM ctx (HSMap Credential VDeleg) -> SpecTransM ctx (HSMap Credential Integer -> HSMap Credential Integer -> HSMap DepositPurpose Integer -> DState) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Map StakeCredential DRep -> SpecTransM ctx (SpecRep (Map StakeCredential DRep)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (UMap -> Map StakeCredential DRep UMap.dRepMap UMap dsUnified) SpecTransM ctx (HSMap Credential Integer -> HSMap Credential Integer -> HSMap DepositPurpose Integer -> DState) -> SpecTransM ctx (HSMap Credential Integer) -> SpecTransM ctx (HSMap Credential Integer -> HSMap DepositPurpose Integer -> DState) 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 StakeCredential (KeyHash 'StakePool) -> SpecTransM ctx (SpecRep (Map StakeCredential (KeyHash 'StakePool))) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (UMap -> Map StakeCredential (KeyHash 'StakePool) UMap.sPoolMap UMap dsUnified) SpecTransM ctx (HSMap Credential Integer -> HSMap DepositPurpose Integer -> DState) -> SpecTransM ctx (HSMap Credential Integer) -> SpecTransM ctx (HSMap DepositPurpose Integer -> DState) 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 StakeCredential Coin -> SpecTransM ctx (SpecRep (Map StakeCredential Coin)) forall ctx a. SpecTranslate ctx a => a -> SpecTransM ctx (SpecRep a) toSpecRep (UMap -> Map StakeCredential Coin UMap.rewardMap UMap dsUnified) SpecTransM ctx (HSMap DepositPurpose Integer -> DState) -> SpecTransM ctx (HSMap DepositPurpose Integer) -> SpecTransM ctx DState 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 where deposits :: Map DepositPurpose Coin deposits = (StakeCredential -> DepositPurpose) -> Map StakeCredential Coin -> Map DepositPurpose Coin forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a Map.mapKeys StakeCredential -> DepositPurpose CredentialDeposit (UMap -> Map StakeCredential Coin UMap.depositMap UMap dsUnified)