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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert) where

import Cardano.Ledger.BaseTypes (Inject (..))
import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.TxCert (ConwayDelegCert (..))
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyRole (..))
import Constrained.API
import Data.Bifunctor (second)
import Data.Set (Set)
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.Conformance.ExecSpecRule.Core ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
import Test.Cardano.Ledger.Constrained.Conway
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

instance
  Inject
    (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
    (Set (Credential 'DRepRole))
  where
  inject :: (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
-> Set (Credential 'DRepRole)
inject (WitUniv ConwayEra
_, ConwayCertExecContext ConwayEra
x) = forall era. ConwayCertExecContext era -> Set (Credential 'DRepRole)
ccecDelegatees ConwayCertExecContext ConwayEra
x

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

  genExecContext :: HasCallStack => Gen (ExecContext "DELEG" 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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
Era era =>
WitUniv era -> Integer -> Specification (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 "DELEG" ConwayEra
-> Specification (ExecEnvironment "DELEG" ConwayEra)
environmentSpec ExecContext "DELEG" ConwayEra
_ = forall era.
EraSpecPParams era =>
Specification (ConwayDelegEnv era)
delegEnvSpec

  stateSpec :: HasCallStack =>
ExecContext "DELEG" ConwayEra
-> ExecEnvironment "DELEG" ConwayEra
-> Specification (ExecState "DELEG" ConwayEra)
stateSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
ccec) ExecEnvironment "DELEG" ConwayEra
_env =
    forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec @ConwayEra 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 "DELEG" ConwayEra
-> ExecEnvironment "DELEG" ConwayEra
-> ExecState "DELEG" ConwayEra
-> Specification (ExecSignal "DELEG" ConwayEra)
signalSpec ExecContext "DELEG" ConwayEra
_ = forall era.
(EraPParams era, ConwayEraCertState era) =>
ConwayDelegEnv era
-> CertState era -> Specification ConwayDelegCert
conwayDelegCertSpec

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "DELEG" ConwayEra)
-> SpecRep (ExecState "DELEG" ConwayEra)
-> SpecRep (ExecSignal "DELEG" ConwayEra)
-> Either OpaqueErrorString (SpecRep (ExecState "DELEG" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "DELEG" ConwayEra)
env (Agda.MkCertState DState
dState PState
pState GState
vState) SpecRep (ExecSignal "DELEG" ConwayEra)
sig =
    forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second
      (\DState
dState' -> DState -> PState -> GState -> CertState
Agda.MkCertState DState
dState' PState
pState GState
vState)
      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
$ DelegEnv
-> DState -> DCert -> T_ComputationResult_46 T_String_6 DState
Agda.delegStep SpecRep (ExecEnvironment "DELEG" ConwayEra)
env DState
dState SpecRep (ExecSignal "DELEG" ConwayEra)
sig

  classOf :: ExecSignal "DELEG" ConwayEra -> Maybe String
classOf = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayDelegCert -> String
nameDelegCert

nameDelegCert :: ConwayDelegCert -> String
nameDelegCert :: ConwayDelegCert -> String
nameDelegCert ConwayRegCert {} = String
"RegKey"
nameDelegCert ConwayUnRegCert {} = String
"UnRegKey"
nameDelegCert ConwayDelegCert {} = String
"DelegateWithKey"
nameDelegCert ConwayRegDelegCert {} = String
"RegK&DelegateWithKey"