{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool where

import Cardano.Ledger.BaseTypes (Network (Testnet))
import Cardano.Ledger.Binary (EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Core
import qualified Cardano.Ledger.Shelley.Rules as Shelley
import Cardano.Ledger.State
import qualified Data.Map.Strict as Map
import qualified MAlonzo.Code.Ledger.Conway.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance.SpecTranslate.Base (
  SpecTranslate (SpecRep, toSpecRep),
  toSpecRepMap,
 )
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()

instance SpecTranslate ConwayEra (Shelley.PoolEnv ConwayEra) where
  type SpecRep ConwayEra (Shelley.PoolEnv ConwayEra) = Agda.PParams

  toSpecRep :: PoolEnv ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (PoolEnv ConwayEra))
     (SpecRep ConwayEra (PoolEnv ConwayEra))
toSpecRep (Shelley.PoolEnv EpochNo
_ PParams ConwayEra
pp) = PParams ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (PParams ConwayEra))
     (SpecRep ConwayEra (PParams ConwayEra))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep PParams ConwayEra
pp

instance SpecTranslate ConwayEra (PState ConwayEra) where
  type SpecRep ConwayEra (PState ConwayEra) = Agda.PState

  toSpecRep :: PState ConwayEra
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (PState ConwayEra))
     (SpecRep ConwayEra (PState ConwayEra))
toSpecRep PState {Map (KeyHash StakePool) StakePoolParams
Map (KeyHash StakePool) StakePoolState
Map (KeyHash StakePool) EpochNo
Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
psVRFKeyHashes :: Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
psStakePools :: Map (KeyHash StakePool) StakePoolState
psFutureStakePoolParams :: Map (KeyHash StakePool) StakePoolParams
psRetiring :: Map (KeyHash StakePool) EpochNo
psFutureStakePoolParams :: forall era. PState era -> Map (KeyHash StakePool) StakePoolParams
psRetiring :: forall era. PState era -> Map (KeyHash StakePool) EpochNo
psStakePools :: forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psVRFKeyHashes :: forall era.
PState era -> Map (VRFVerKeyHash StakePoolVRF) (NonZero Word64)
..} =
    HSMap Integer StakePoolParams
-> HSMap Integer StakePoolParams -> HSMap Integer Integer -> PState
Agda.MkPState
      (HSMap Integer StakePoolParams
 -> HSMap Integer StakePoolParams
 -> HSMap Integer Integer
 -> PState)
-> SpecTransM ConwayEra () (HSMap Integer StakePoolParams)
-> SpecTransM
     ConwayEra
     ()
     (HSMap Integer StakePoolParams -> HSMap Integer Integer -> PState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (KeyHash StakePool) StakePoolParams
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (KeyHash StakePool))
        (SpecRep ConwayEra StakePoolParams))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap ((KeyHash StakePool -> StakePoolState -> StakePoolParams)
-> Map (KeyHash StakePool) StakePoolState
-> Map (KeyHash StakePool) StakePoolParams
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (Network -> KeyHash StakePool -> StakePoolState -> StakePoolParams
stakePoolStateToStakePoolParams Network
Testnet) Map (KeyHash StakePool) StakePoolState
psStakePools)
      SpecTransM
  ConwayEra
  ()
  (HSMap Integer StakePoolParams -> HSMap Integer Integer -> PState)
-> SpecTransM ConwayEra () (HSMap Integer StakePoolParams)
-> SpecTransM ConwayEra () (HSMap Integer Integer -> PState)
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (KeyHash StakePool) StakePoolParams
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (KeyHash StakePool))
        (SpecRep ConwayEra StakePoolParams))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map (KeyHash StakePool) StakePoolParams
psFutureStakePoolParams
      SpecTransM ConwayEra () (HSMap Integer Integer -> PState)
-> SpecTransM ConwayEra () (HSMap Integer Integer)
-> SpecTransM ConwayEra () PState
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map (KeyHash StakePool) EpochNo
-> SpecTransM
     ConwayEra
     ()
     (HSMap
        (SpecRep ConwayEra (KeyHash StakePool))
        (SpecRep ConwayEra EpochNo))
forall era k v ctx.
(SpecTranslate era k, SpecTranslate era v, SpecContext era k ~ ctx,
 SpecContext era v ~ ctx) =>
Map k v
-> SpecTransM era ctx (HSMap (SpecRep era k) (SpecRep era v))
toSpecRepMap Map (KeyHash StakePool) EpochNo
psRetiring

-- | This instance is only used for conformance testing (e.g. @ExecSpecRule@).
-- This instance uses arbitrary tags (0 and 1) that don't match the CDDL spec.
--
-- The actual spec-compliant CBOR encoding that follows the CDDL is handled by 'encodePoolCert'.
instance EncCBOR PoolCert where
  encCBOR :: PoolCert -> Encoding
encCBOR =
    Encode Open PoolCert -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode Open PoolCert -> Encoding)
-> (PoolCert -> Encode Open PoolCert) -> PoolCert -> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      RegPool StakePoolParams
pp -> (StakePoolParams -> PoolCert)
-> Word -> Encode Open (StakePoolParams -> PoolCert)
forall t. t -> Word -> Encode Open t
Sum StakePoolParams -> PoolCert
RegPool Word
0 Encode Open (StakePoolParams -> PoolCert)
-> Encode (Closed Dense) StakePoolParams -> Encode Open PoolCert
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> StakePoolParams -> Encode (Closed Dense) StakePoolParams
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To StakePoolParams
pp
      RetirePool KeyHash StakePool
kh EpochNo
eNo -> (KeyHash StakePool -> EpochNo -> PoolCert)
-> Word -> Encode Open (KeyHash StakePool -> EpochNo -> PoolCert)
forall t. t -> Word -> Encode Open t
Sum KeyHash StakePool -> EpochNo -> PoolCert
RetirePool Word
1 Encode Open (KeyHash StakePool -> EpochNo -> PoolCert)
-> Encode (Closed Dense) (KeyHash StakePool)
-> Encode Open (EpochNo -> PoolCert)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> KeyHash StakePool -> Encode (Closed Dense) (KeyHash StakePool)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To KeyHash StakePool
kh Encode Open (EpochNo -> PoolCert)
-> Encode (Closed Dense) EpochNo -> Encode Open PoolCert
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode (Closed r) a -> Encode w t
!> EpochNo -> Encode (Closed Dense) EpochNo
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To EpochNo
eNo

instance SpecTranslate ConwayEra PoolCert where
  type SpecRep ConwayEra PoolCert = Agda.DCert

  toSpecRep :: PoolCert
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra PoolCert)
     (SpecRep ConwayEra PoolCert)
toSpecRep (RegPool p :: StakePoolParams
p@StakePoolParams {sppId :: StakePoolParams -> KeyHash StakePool
sppId = KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash}) =
    Integer -> StakePoolParams -> DCert
Agda.Regpool
      (Integer -> StakePoolParams -> DCert)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (StakePoolParams -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hash ADDRHASH (VerKeyDSIGN DSIGN)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
     (SpecRep ConwayEra (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash
      SpecTransM ConwayEra () (StakePoolParams -> DCert)
-> SpecTransM ConwayEra () StakePoolParams
-> SpecTransM ConwayEra () DCert
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StakePoolParams
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra StakePoolParams)
     (SpecRep ConwayEra StakePoolParams)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep StakePoolParams
p
  toSpecRep (RetirePool (KeyHash Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash) EpochNo
e) =
    Integer -> Integer -> DCert
Agda.Retirepool
      (Integer -> Integer -> DCert)
-> SpecTransM ConwayEra () Integer
-> SpecTransM ConwayEra () (Integer -> DCert)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hash ADDRHASH (VerKeyDSIGN DSIGN)
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
     (SpecRep ConwayEra (Hash ADDRHASH (VerKeyDSIGN DSIGN)))
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep Hash ADDRHASH (VerKeyDSIGN DSIGN)
ppHash
      SpecTransM ConwayEra () (Integer -> DCert)
-> SpecTransM ConwayEra () Integer -> SpecTransM ConwayEra () DCert
forall a b.
SpecTransM ConwayEra () (a -> b)
-> SpecTransM ConwayEra () a -> SpecTransM ConwayEra () b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> EpochNo
-> SpecTransM
     ConwayEra
     (SpecContext ConwayEra EpochNo)
     (SpecRep ConwayEra EpochNo)
forall era a.
SpecTranslate era a =>
a -> SpecTransM era (SpecContext era a) (SpecRep era a)
toSpecRep EpochNo
e