{-# 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
import Data.Bifunctor (Bifunctor (..))
import Data.Map.Strict (Map)
import qualified Lib 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) = 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) = forall era. ConwayCertExecContext era -> VotingProcedures era
ccecVotes ConwayCertExecContext ConwayEra
x

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

  genExecContext :: HasCallStack => Gen (ExecContext fn "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 <- forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall (fn :: [*] -> * -> *) era.
(Reflect era, IsConwayUniv fn) =>
WitUniv era
-> Integer -> Specification fn (ConwayCertExecContext era)
conwayCertExecContextSpec WitUniv ConwayEra
univ Integer
5)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
ccec)

  environmentSpec :: HasCallStack =>
ExecContext fn "GOVCERT" ConwayEra
-> Specification fn (ExecEnvironment fn "GOVCERT" ConwayEra)
environmentSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) = forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
WitUniv ConwayEra -> Specification fn (ConwayGovCertEnv ConwayEra)
govCertEnvSpec WitUniv ConwayEra
univ

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

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

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

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment fn "GOVCERT" ConwayEra)
-> SpecRep (ExecState fn "GOVCERT" ConwayEra)
-> SpecRep (ExecSignal fn "GOVCERT" ConwayEra)
-> Either
     OpaqueErrorString (SpecRep (ExecState fn "GOVCERT" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment fn "GOVCERT" ConwayEra)
env (Agda.MkCertState DState
dState PState
pState GState
vState) SpecRep (ExecSignal fn "GOVCERT" ConwayEra)
sig =
    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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
ComputationResult T_String_6 a -> Either OpaqueErrorString a
unComputationResult forall a b. (a -> b) -> a -> b
$
      CertEnv
-> GState -> DCert -> T_ComputationResult_46 T_String_6 GState
Agda.govCertStep SpecRep (ExecEnvironment fn "GOVCERT" ConwayEra)
env GState
vState SpecRep (ExecSignal fn "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"