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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (
  ConwayCertExecContext (..),
) where

import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes (Inject (..))
import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
import Cardano.Ledger.Binary.Coders (Decode (..), Encode (..), decode, encode, (!>), (<!))
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core (Era)
import Cardano.Ledger.Conway.Governance (VotingProcedures)
import Control.DeepSeq (NFData)
import Data.Map.Strict (Map)
import GHC.Generics (Generic)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Common (Arbitrary (..), ToExpr)
import Test.Cardano.Ledger.Conformance (ExecSpecRule (..), runFromAgdaFunction)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base ()

data ConwayCertExecContext era
  = ConwayCertExecContext
  { forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals :: !(Map RewardAccount Coin)
  , forall era. ConwayCertExecContext era -> VotingProcedures era
ccecVotes :: !(VotingProcedures era)
  }
  deriving ((forall x.
 ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x)
-> (forall x.
    Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era)
-> Generic (ConwayCertExecContext era)
forall x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
forall x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
forall era x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
$cfrom :: forall era x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
from :: forall x.
ConwayCertExecContext era -> Rep (ConwayCertExecContext era) x
$cto :: forall era x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
to :: forall x.
Rep (ConwayCertExecContext era) x -> ConwayCertExecContext era
Generic, ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
(ConwayCertExecContext era -> ConwayCertExecContext era -> Bool)
-> (ConwayCertExecContext era -> ConwayCertExecContext era -> Bool)
-> Eq (ConwayCertExecContext era)
forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
== :: ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
$c/= :: forall era.
ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
/= :: ConwayCertExecContext era -> ConwayCertExecContext era -> Bool
Eq, Int -> ConwayCertExecContext era -> ShowS
[ConwayCertExecContext era] -> ShowS
ConwayCertExecContext era -> String
(Int -> ConwayCertExecContext era -> ShowS)
-> (ConwayCertExecContext era -> String)
-> ([ConwayCertExecContext era] -> ShowS)
-> Show (ConwayCertExecContext era)
forall era. Int -> ConwayCertExecContext era -> ShowS
forall era. [ConwayCertExecContext era] -> ShowS
forall era. ConwayCertExecContext era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall era. Int -> ConwayCertExecContext era -> ShowS
showsPrec :: Int -> ConwayCertExecContext era -> ShowS
$cshow :: forall era. ConwayCertExecContext era -> String
show :: ConwayCertExecContext era -> String
$cshowList :: forall era. [ConwayCertExecContext era] -> ShowS
showList :: [ConwayCertExecContext era] -> ShowS
Show)

instance Era era => NFData (ConwayCertExecContext era)

instance Inject (ConwayCertExecContext era) (Map RewardAccount Coin) where
  inject :: ConwayCertExecContext era -> Map RewardAccount Coin
inject = ConwayCertExecContext era -> Map RewardAccount Coin
forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals

instance Inject (ConwayCertExecContext era) (VotingProcedures era) where
  inject :: ConwayCertExecContext era -> VotingProcedures era
inject = ConwayCertExecContext era -> VotingProcedures era
forall era. ConwayCertExecContext era -> VotingProcedures era
ccecVotes

instance Era era => Arbitrary (ConwayCertExecContext era) where
  arbitrary :: Gen (ConwayCertExecContext era)
arbitrary =
    Map RewardAccount Coin
-> VotingProcedures era -> ConwayCertExecContext era
forall era.
Map RewardAccount Coin
-> VotingProcedures era -> ConwayCertExecContext era
ConwayCertExecContext
      (Map RewardAccount Coin
 -> VotingProcedures era -> ConwayCertExecContext era)
-> Gen (Map RewardAccount Coin)
-> Gen (VotingProcedures era -> ConwayCertExecContext era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Map RewardAccount Coin)
forall a. Arbitrary a => Gen a
arbitrary
      Gen (VotingProcedures era -> ConwayCertExecContext era)
-> Gen (VotingProcedures era) -> Gen (ConwayCertExecContext era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (VotingProcedures era)
forall a. Arbitrary a => Gen a
arbitrary

instance Era era => EncCBOR (ConwayCertExecContext era) where
  encCBOR :: ConwayCertExecContext era -> Encoding
encCBOR x :: ConwayCertExecContext era
x@(ConwayCertExecContext Map RewardAccount Coin
_ VotingProcedures era
_) =
    let ConwayCertExecContext {Map RewardAccount Coin
VotingProcedures era
ccecWithdrawals :: forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecVotes :: forall era. ConwayCertExecContext era -> VotingProcedures era
ccecWithdrawals :: Map RewardAccount Coin
ccecVotes :: VotingProcedures era
..} = ConwayCertExecContext era
x
     in Encode ('Closed 'Dense) (ConwayCertExecContext era) -> Encoding
forall (w :: Wrapped) t. Encode w t -> Encoding
encode (Encode ('Closed 'Dense) (ConwayCertExecContext era) -> Encoding)
-> Encode ('Closed 'Dense) (ConwayCertExecContext era) -> Encoding
forall a b. (a -> b) -> a -> b
$
          (Map RewardAccount Coin
 -> VotingProcedures era -> ConwayCertExecContext era)
-> Encode
     ('Closed 'Dense)
     (Map RewardAccount Coin
      -> VotingProcedures era -> ConwayCertExecContext era)
forall t. t -> Encode ('Closed 'Dense) t
Rec Map RewardAccount Coin
-> VotingProcedures era -> ConwayCertExecContext era
forall era.
Map RewardAccount Coin
-> VotingProcedures era -> ConwayCertExecContext era
ConwayCertExecContext
            Encode
  ('Closed 'Dense)
  (Map RewardAccount Coin
   -> VotingProcedures era -> ConwayCertExecContext era)
-> Encode ('Closed 'Dense) (Map RewardAccount Coin)
-> Encode
     ('Closed 'Dense)
     (VotingProcedures era -> ConwayCertExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> Map RewardAccount Coin
-> Encode ('Closed 'Dense) (Map RewardAccount Coin)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To Map RewardAccount Coin
ccecWithdrawals
            Encode
  ('Closed 'Dense)
  (VotingProcedures era -> ConwayCertExecContext era)
-> Encode ('Closed 'Dense) (VotingProcedures era)
-> Encode ('Closed 'Dense) (ConwayCertExecContext era)
forall (w :: Wrapped) a t (r :: Density).
Encode w (a -> t) -> Encode ('Closed r) a -> Encode w t
!> VotingProcedures era
-> Encode ('Closed 'Dense) (VotingProcedures era)
forall t. EncCBOR t => t -> Encode ('Closed 'Dense) t
To VotingProcedures era
ccecVotes

instance Era era => DecCBOR (ConwayCertExecContext era) where
  decCBOR :: forall s. Decoder s (ConwayCertExecContext era)
decCBOR =
    Decode ('Closed 'Dense) (ConwayCertExecContext era)
-> Decoder s (ConwayCertExecContext era)
forall t (w :: Wrapped) s. Typeable t => Decode w t -> Decoder s t
decode (Decode ('Closed 'Dense) (ConwayCertExecContext era)
 -> Decoder s (ConwayCertExecContext era))
-> Decode ('Closed 'Dense) (ConwayCertExecContext era)
-> Decoder s (ConwayCertExecContext era)
forall a b. (a -> b) -> a -> b
$
      (Map RewardAccount Coin
 -> VotingProcedures era -> ConwayCertExecContext era)
-> Decode
     ('Closed 'Dense)
     (Map RewardAccount Coin
      -> VotingProcedures era -> ConwayCertExecContext era)
forall t. t -> Decode ('Closed 'Dense) t
RecD Map RewardAccount Coin
-> VotingProcedures era -> ConwayCertExecContext era
forall era.
Map RewardAccount Coin
-> VotingProcedures era -> ConwayCertExecContext era
ConwayCertExecContext
        Decode
  ('Closed 'Dense)
  (Map RewardAccount Coin
   -> VotingProcedures era -> ConwayCertExecContext era)
-> Decode ('Closed Any) (Map RewardAccount Coin)
-> Decode
     ('Closed 'Dense)
     (VotingProcedures era -> ConwayCertExecContext era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (Map RewardAccount Coin)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Decode
  ('Closed 'Dense)
  (VotingProcedures era -> ConwayCertExecContext era)
-> Decode ('Closed Any) (VotingProcedures era)
-> Decode ('Closed 'Dense) (ConwayCertExecContext era)
forall a (w1 :: Wrapped) t (w :: Density).
Typeable a =>
Decode w1 (a -> t) -> Decode ('Closed w) a -> Decode w1 t
<! Decode ('Closed Any) (VotingProcedures era)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From

instance Era era => ToExpr (ConwayCertExecContext era)

instance ExecSpecRule "CERT" ConwayEra where
  type ExecContext "CERT" ConwayEra = ConwayCertExecContext ConwayEra

  runAgdaRule :: HasCallStack =>
SpecTRC "CERT" ConwayEra
-> Either Text (SpecState "CERT" ConwayEra)
runAgdaRule = (SpecEnvironment "CERT" ConwayEra
 -> SpecState "CERT" ConwayEra
 -> SpecSignal "CERT" ConwayEra
 -> ComputationResult Text (SpecState "CERT" ConwayEra))
-> SpecTRC "CERT" ConwayEra
-> Either Text (SpecState "CERT" ConwayEra)
forall (rule :: Symbol) era.
(SpecEnvironment rule era
 -> SpecState rule era
 -> SpecSignal rule era
 -> ComputationResult Text (SpecState rule era))
-> SpecTRC rule era -> Either Text (SpecState rule era)
runFromAgdaFunction CertEnv
-> CertState -> DCert -> T_ComputationResult_44 Text CertState
SpecEnvironment "CERT" ConwayEra
-> SpecState "CERT" ConwayEra
-> SpecSignal "CERT" ConwayEra
-> ComputationResult Text (SpecState "CERT" ConwayEra)
Agda.certStep