{-# 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)