{-# 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 (AccountAddress)
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 AccountAddress Coin
ccecWithdrawals :: !(Map AccountAddress 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 AccountAddress Coin) where
  inject :: ConwayCertExecContext era -> Map AccountAddress Coin
inject = ConwayCertExecContext era -> Map AccountAddress Coin
forall era. ConwayCertExecContext era -> Map AccountAddress 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 AccountAddress Coin
-> VotingProcedures era -> ConwayCertExecContext era
forall era.
Map AccountAddress Coin
-> VotingProcedures era -> ConwayCertExecContext era
ConwayCertExecContext
      (Map AccountAddress Coin
 -> VotingProcedures era -> ConwayCertExecContext era)
-> Gen (Map AccountAddress Coin)
-> Gen (VotingProcedures era -> ConwayCertExecContext era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Map AccountAddress 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 AccountAddress Coin
_ VotingProcedures era
_) =
    let ConwayCertExecContext {Map AccountAddress Coin
VotingProcedures era
ccecWithdrawals :: forall era. ConwayCertExecContext era -> Map AccountAddress Coin
ccecVotes :: forall era. ConwayCertExecContext era -> VotingProcedures era
ccecWithdrawals :: Map AccountAddress 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 AccountAddress Coin
 -> VotingProcedures era -> ConwayCertExecContext era)
-> Encode
     (Closed Dense)
     (Map AccountAddress Coin
      -> VotingProcedures era -> ConwayCertExecContext era)
forall t. t -> Encode (Closed Dense) t
Rec Map AccountAddress Coin
-> VotingProcedures era -> ConwayCertExecContext era
forall era.
Map AccountAddress Coin
-> VotingProcedures era -> ConwayCertExecContext era
ConwayCertExecContext
            Encode
  (Closed Dense)
  (Map AccountAddress Coin
   -> VotingProcedures era -> ConwayCertExecContext era)
-> Encode (Closed Dense) (Map AccountAddress 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 AccountAddress Coin
-> Encode (Closed Dense) (Map AccountAddress Coin)
forall t. EncCBOR t => t -> Encode (Closed Dense) t
To Map AccountAddress 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 AccountAddress Coin
 -> VotingProcedures era -> ConwayCertExecContext era)
-> Decode
     (Closed Dense)
     (Map AccountAddress Coin
      -> VotingProcedures era -> ConwayCertExecContext era)
forall t. t -> Decode (Closed Dense) t
RecD Map AccountAddress Coin
-> VotingProcedures era -> ConwayCertExecContext era
forall era.
Map AccountAddress Coin
-> VotingProcedures era -> ConwayCertExecContext era
ConwayCertExecContext
        Decode
  (Closed Dense)
  (Map AccountAddress Coin
   -> VotingProcedures era -> ConwayCertExecContext era)
-> Decode (Closed (ZonkAny 1)) (Map AccountAddress 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 (ZonkAny 1)) (Map AccountAddress Coin)
forall t (w :: Wrapped). DecCBOR t => Decode w t
From
        Decode
  (Closed Dense) (VotingProcedures era -> ConwayCertExecContext era)
-> Decode (Closed (ZonkAny 0)) (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 (ZonkAny 0)) (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