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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert (nameGovCert) where

import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes (Inject (..))
import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.Governance (VotingProcedures)
import Cardano.Ledger.Conway.TxCert
import Constrained.API
import Data.Bifunctor (Bifunctor (..))
import Data.Map.Strict (Map)
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
  ConwayCertExecContext (..),
  conwayCertExecContextSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

instance Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (Map RewardAccount Coin) where
  inject :: (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
-> Map RewardAccount Coin
inject (WitUniv ConwayEra
_, ConwayCertExecContext ConwayEra
x) = ConwayCertExecContext ConwayEra -> Map RewardAccount Coin
forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals ConwayCertExecContext ConwayEra
x

instance Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (VotingProcedures ConwayEra) where
  inject :: (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
-> VotingProcedures ConwayEra
inject (WitUniv ConwayEra
_, ConwayCertExecContext ConwayEra
x) = ConwayCertExecContext ConwayEra -> VotingProcedures ConwayEra
forall era. ConwayCertExecContext era -> VotingProcedures era
ccecVotes ConwayCertExecContext ConwayEra
x

instance ExecSpecRule "GOVCERT" ConwayEra where
  type ExecContext "GOVCERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)

  genExecContext :: HasCallStack => Gen (ExecContext "GOVCERT" ConwayEra)
genExecContext = do
    WitUniv ConwayEra
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
300
    ConwayCertExecContext ConwayEra
ccec <- Specification (ConwayCertExecContext ConwayEra)
-> Gen (ConwayCertExecContext ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv ConwayEra
-> Integer -> Specification (ConwayCertExecContext ConwayEra)
forall era.
Era era =>
WitUniv era -> Integer -> Specification (ConwayCertExecContext era)
conwayCertExecContextSpec WitUniv ConwayEra
univ Integer
5)
    (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
-> Gen (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
ccec)

  environmentSpec :: HasCallStack =>
ExecContext "GOVCERT" ConwayEra
-> Specification (ExecEnvironment "GOVCERT" ConwayEra)
environmentSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) = WitUniv ConwayEra -> Specification (ConwayGovCertEnv ConwayEra)
govCertEnvSpec WitUniv ConwayEra
univ

  stateSpec :: HasCallStack =>
ExecContext "GOVCERT" ConwayEra
-> ExecEnvironment "GOVCERT" ConwayEra
-> Specification (ExecState "GOVCERT" ConwayEra)
stateSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
ccec) ExecEnvironment "GOVCERT" ConwayEra
_env =
    forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec @ConwayEra WitUniv ConwayEra
univ (ConwayCertExecContext ConwayEra -> Set (Credential 'DRepRole)
forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole)
ccecDelegatees ConwayCertExecContext ConwayEra
ccec) (ConwayCertExecContext ConwayEra -> Map RewardAccount Coin
forall era. ConwayCertExecContext era -> Map RewardAccount Coin
ccecWithdrawals ConwayCertExecContext ConwayEra
ccec)

  signalSpec :: HasCallStack =>
ExecContext "GOVCERT" ConwayEra
-> ExecEnvironment "GOVCERT" ConwayEra
-> ExecState "GOVCERT" ConwayEra
-> Specification (ExecSignal "GOVCERT" ConwayEra)
signalSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) = WitUniv ConwayEra
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
forall era.
EraCertState era =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
govCertSpec WitUniv ConwayEra
univ

  classOf :: ExecSignal "GOVCERT" ConwayEra -> Maybe String
classOf = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> (ConwayGovCert -> String) -> ConwayGovCert -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayGovCert -> String
nameGovCert

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "GOVCERT" ConwayEra)
-> SpecRep (ExecState "GOVCERT" ConwayEra)
-> SpecRep (ExecSignal "GOVCERT" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState "GOVCERT" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "GOVCERT" ConwayEra)
env (Agda.MkCertState DState
dState PState
pState GState
vState) SpecRep (ExecSignal "GOVCERT" ConwayEra)
sig =
    (GState -> CertState)
-> Either OpaqueErrorString GState
-> Either OpaqueErrorString CertState
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (DState -> PState -> GState -> CertState
Agda.MkCertState DState
dState PState
pState) (Either OpaqueErrorString GState
 -> Either
      OpaqueErrorString (SpecRep (ExecState "GOVCERT" ConwayEra)))
-> (T_ComputationResult_46 T_String_6 GState
    -> Either OpaqueErrorString GState)
-> T_ComputationResult_46 T_String_6 GState
-> Either
     OpaqueErrorString (SpecRep (ExecState "GOVCERT" ConwayEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_ComputationResult_46 T_String_6 GState
-> Either OpaqueErrorString GState
forall a.
ComputationResult T_String_6 a -> Either OpaqueErrorString a
unComputationResult (T_ComputationResult_46 T_String_6 GState
 -> Either
      OpaqueErrorString (SpecRep (ExecState "GOVCERT" ConwayEra)))
-> T_ComputationResult_46 T_String_6 GState
-> Either
     OpaqueErrorString (SpecRep (ExecState "GOVCERT" ConwayEra))
forall a b. (a -> b) -> a -> b
$
      CertEnv
-> GState -> DCert -> T_ComputationResult_46 T_String_6 GState
Agda.govCertStep CertEnv
SpecRep (ExecEnvironment "GOVCERT" ConwayEra)
env GState
vState DCert
SpecRep (ExecSignal "GOVCERT" ConwayEra)
sig

nameGovCert :: ConwayGovCert -> String
nameGovCert :: ConwayGovCert -> String
nameGovCert (ConwayRegDRep {}) = String
"ConwayRegDRep"
nameGovCert (ConwayUnRegDRep {}) = String
"ConwayUnRegDRep"
nameGovCert (ConwayUpdateDRep {}) = String
"ConwayUpdateDRep"
nameGovCert (ConwayAuthCommitteeHotKey {}) = String
"ConwayAuthCommitteeHotKey"
nameGovCert (ConwayResignCommitteeColdKey {}) = String
"ConwayResignCommitteeColdKey"