{-# 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.Compactible (fromCompact) import Cardano.Ledger.Conway.Rules ( ConwayDelegEnv (..), ConwayDelegPredFailure, ) import Cardano.Ledger.Conway.State import Cardano.Ledger.Conway.TxCert ( ConwayDelegCert (..), getDRepDelegatee, getStakePoolDelegatee, ) import Cardano.Ledger.Core import Cardano.Ledger.Credential (Credential) import Cardano.Ledger.Shelley.Rules import qualified Data.Map.Strict as Map import Data.Set (Set) import Lens.Micro 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 getDRepDelegatee 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 getDRepDelegatee 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 ConwayEraAccounts era => SpecTranslate ctx (DState era) where type SpecRep (DState era) = Agda.DState toSpecRep :: DState era -> SpecTransM ctx (SpecRep (DState era)) toSpecRep DState era dState = 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 ((AccountState era -> Maybe DRep) -> Map StakeCredential (AccountState era) -> Map StakeCredential DRep forall a b k. (a -> Maybe b) -> Map k a -> Map k b Map.mapMaybe (AccountState era -> Getting (Maybe DRep) (AccountState era) (Maybe DRep) -> Maybe DRep forall s a. s -> Getting a s a -> a ^. Getting (Maybe DRep) (AccountState era) (Maybe DRep) forall era. ConwayEraAccounts era => Lens' (AccountState era) (Maybe DRep) Lens' (AccountState era) (Maybe DRep) dRepDelegationAccountStateL) Map StakeCredential (AccountState era) accountsMap) 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 ((AccountState era -> Maybe (KeyHash 'StakePool)) -> Map StakeCredential (AccountState era) -> Map StakeCredential (KeyHash 'StakePool) forall a b k. (a -> Maybe b) -> Map k a -> Map k b Map.mapMaybe (AccountState era -> Getting (Maybe (KeyHash 'StakePool)) (AccountState era) (Maybe (KeyHash 'StakePool)) -> Maybe (KeyHash 'StakePool) forall s a. s -> Getting a s a -> a ^. Getting (Maybe (KeyHash 'StakePool)) (AccountState era) (Maybe (KeyHash 'StakePool)) forall era. EraAccounts era => Lens' (AccountState era) (Maybe (KeyHash 'StakePool)) Lens' (AccountState era) (Maybe (KeyHash 'StakePool)) stakePoolDelegationAccountStateL) Map StakeCredential (AccountState era) accountsMap) 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 ((AccountState era -> Coin) -> Map StakeCredential (AccountState era) -> Map StakeCredential Coin forall a b k. (a -> b) -> Map k a -> Map k b Map.map (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 . (AccountState era -> Getting (CompactForm Coin) (AccountState era) (CompactForm Coin) -> CompactForm Coin forall s a. s -> Getting a s a -> a ^. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin) forall era. EraAccounts era => Lens' (AccountState era) (CompactForm Coin) Lens' (AccountState era) (CompactForm Coin) balanceAccountStateL)) Map StakeCredential (AccountState era) accountsMap) 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 accountsMap :: Map StakeCredential (AccountState era) accountsMap = DState era dState DState era -> Getting (Map StakeCredential (AccountState era)) (DState era) (Map StakeCredential (AccountState era)) -> Map StakeCredential (AccountState era) forall s a. s -> Getting a s a -> a ^. (Accounts era -> Const (Map StakeCredential (AccountState era)) (Accounts era)) -> DState era -> Const (Map StakeCredential (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 StakeCredential (AccountState era)) (Accounts era)) -> DState era -> Const (Map StakeCredential (AccountState era)) (DState era)) -> ((Map StakeCredential (AccountState era) -> Const (Map StakeCredential (AccountState era)) (Map StakeCredential (AccountState era))) -> Accounts era -> Const (Map StakeCredential (AccountState era)) (Accounts era)) -> Getting (Map StakeCredential (AccountState era)) (DState era) (Map StakeCredential (AccountState era)) forall b c a. (b -> c) -> (a -> b) -> a -> c . (Map StakeCredential (AccountState era) -> Const (Map StakeCredential (AccountState era)) (Map StakeCredential (AccountState era))) -> Accounts era -> Const (Map StakeCredential (AccountState era)) (Accounts era) forall era. EraAccounts era => Lens' (Accounts era) (Map StakeCredential (AccountState era)) Lens' (Accounts era) (Map StakeCredential (AccountState era)) accountsMapL 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 ((AccountState era -> Coin) -> Map StakeCredential (AccountState era) -> Map StakeCredential Coin forall a b k. (a -> b) -> Map k a -> Map k b Map.map (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 . (AccountState era -> Getting (CompactForm Coin) (AccountState era) (CompactForm Coin) -> CompactForm Coin forall s a. s -> Getting a s a -> a ^. Getting (CompactForm Coin) (AccountState era) (CompactForm Coin) forall era. EraAccounts era => Lens' (AccountState era) (CompactForm Coin) Lens' (AccountState era) (CompactForm Coin) depositAccountStateL)) Map StakeCredential (AccountState era) accountsMap)