{-# 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 (..),
 )
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.Base
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()

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) StakePoolState
PParams era
cdePParams :: PParams era
cdePools :: Map (KeyHash StakePool) StakePoolState
cdePools :: forall era.
ConwayDelegEnv era -> Map (KeyHash StakePool) StakePoolState
cdePParams :: forall era. ConwayDelegEnv era -> PParams era
..} = do
    delegatees <- forall b ctx. Inject ctx b => SpecTransM ctx b
askCtx @(Set (Credential DRepRole))
    Agda.MkDelegEnv
      <$> toSpecRep cdePParams
      <*> toSpecRep
        ( Map.mapKeys (hashToInteger . unKeyHash) $
            Map.mapWithKey (`stakePoolStateToStakePoolParams` Testnet) cdePools
        )
      <*> toSpecRep delegatees

instance SpecTranslate ctx ConwayDelegCert where
  type SpecRep ConwayDelegCert = Agda.DCert

  toSpecRep :: ConwayDelegCert -> SpecTransM ctx (SpecRep ConwayDelegCert)
toSpecRep (ConwayRegCert Credential Staking
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
<$> Credential Staking -> SpecTransM ctx (SpecRep (Credential Staking))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential Staking
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 Credential Staking
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
<$> Credential Staking -> SpecTransM ctx (SpecRep (Credential Staking))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential Staking
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 Credential Staking
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
<$> Credential Staking -> SpecTransM ctx (SpecRep (Credential Staking))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential Staking
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 Credential Staking
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
<$> Credential Staking -> SpecTransM ctx (SpecRep (Credential Staking))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep Credential Staking
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 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 (Credential Staking) DRep
-> SpecTransM ctx (SpecRep (Map (Credential Staking) DRep))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ((AccountState era -> Maybe DRep)
-> Map (Credential Staking) (AccountState era)
-> Map (Credential Staking) 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 (Credential Staking) (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 (Credential Staking) (KeyHash StakePool)
-> SpecTransM
     ctx (SpecRep (Map (Credential Staking) (KeyHash StakePool)))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ((AccountState era -> Maybe (KeyHash StakePool))
-> Map (Credential Staking) (AccountState era)
-> Map (Credential Staking) (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 (Credential Staking) (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 (Credential Staking) Coin
-> SpecTransM ctx (SpecRep (Map (Credential Staking) Coin))
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep ((AccountState era -> Coin)
-> Map (Credential Staking) (AccountState era)
-> Map (Credential Staking) 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 (Credential Staking) (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
<*> SpecTransM ctx (HSMap DepositPurpose Integer)
deposits
    where
      accountsMap :: Map (Credential Staking) (AccountState era)
accountsMap = DState era
dState DState era
-> Getting
     (Map (Credential Staking) (AccountState era))
     (DState era)
     (Map (Credential Staking) (AccountState era))
-> Map (Credential Staking) (AccountState era)
forall s a. s -> Getting a s a -> a
^. (Accounts era
 -> Const
      (Map (Credential Staking) (AccountState era)) (Accounts era))
-> DState era
-> Const (Map (Credential Staking) (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 (Credential Staking) (AccountState era)) (Accounts era))
 -> DState era
 -> Const
      (Map (Credential Staking) (AccountState era)) (DState era))
-> ((Map (Credential Staking) (AccountState era)
     -> Const
          (Map (Credential Staking) (AccountState era))
          (Map (Credential Staking) (AccountState era)))
    -> Accounts era
    -> Const
         (Map (Credential Staking) (AccountState era)) (Accounts era))
-> Getting
     (Map (Credential Staking) (AccountState era))
     (DState era)
     (Map (Credential Staking) (AccountState era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential Staking) (AccountState era)
 -> Const
      (Map (Credential Staking) (AccountState era))
      (Map (Credential Staking) (AccountState era)))
-> Accounts era
-> Const
     (Map (Credential Staking) (AccountState era)) (Accounts era)
forall era.
EraAccounts era =>
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
Lens' (Accounts era) (Map (Credential Staking) (AccountState era))
accountsMapL
      deposits :: SpecTransM ctx (HSMap DepositPurpose Integer)
deposits = do
        let
          m :: Map (Credential Staking) Coin
m = (AccountState era -> Coin)
-> Map (Credential Staking) (AccountState era)
-> Map (Credential Staking) 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 (Credential Staking) (AccountState era)
accountsMap
          transEntry :: (a, a) -> SpecTransM ctx (DepositPurpose, SpecRep a)
transEntry (a
cred, a
val) =
            (,)
              (DepositPurpose -> SpecRep a -> (DepositPurpose, SpecRep a))
-> SpecTransM ctx DepositPurpose
-> SpecTransM ctx (SpecRep a -> (DepositPurpose, SpecRep a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Credential -> DepositPurpose
Agda.CredentialDeposit (Credential -> DepositPurpose)
-> SpecTransM ctx Credential -> SpecTransM ctx DepositPurpose
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
cred)
              SpecTransM ctx (SpecRep a -> (DepositPurpose, SpecRep a))
-> SpecTransM ctx (SpecRep a)
-> SpecTransM ctx (DepositPurpose, SpecRep a)
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
<*> a -> SpecTransM ctx (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
val
        [(DepositPurpose, Integer)] -> HSMap DepositPurpose Integer
forall k v. [(k, v)] -> HSMap k v
Agda.MkHSMap ([(DepositPurpose, Integer)] -> HSMap DepositPurpose Integer)
-> SpecTransM ctx [(DepositPurpose, Integer)]
-> SpecTransM ctx (HSMap DepositPurpose Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Credential Staking, Coin)
 -> SpecTransM ctx (DepositPurpose, Integer))
-> [(Credential Staking, Coin)]
-> SpecTransM ctx [(DepositPurpose, Integer)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Credential Staking, Coin)
-> SpecTransM ctx (DepositPurpose, Integer)
(Credential Staking, Coin)
-> SpecTransM ctx (DepositPurpose, SpecRep Coin)
forall {a} {ctx} {a}.
(SpecRep a ~ Credential, SpecTranslate ctx a,
 SpecTranslate ctx a) =>
(a, a) -> SpecTransM ctx (DepositPurpose, SpecRep a)
transEntry (Map (Credential Staking) Coin -> [(Credential Staking, Coin)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Credential Staking) Coin
m)