{-# 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 qualified Data.Map.Strict as Map
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) = Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Set (Credential 'DRepRole)
forall k a. Map k a -> Set k
Map.keysSet (ConwayCertExecContext ConwayEra
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
forall era.
ConwayCertExecContext era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
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 <- 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
4)
    (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 "DELEG" ConwayEra
-> Specification (ExecEnvironment "DELEG" ConwayEra)
environmentSpec ExecContext "DELEG" ConwayEra
_ = Specification (ConwayDelegEnv ConwayEra)
Specification (ExecEnvironment "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 (Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Set (Credential 'DRepRole)
forall k a. Map k a -> Set k
Map.keysSet (ConwayCertExecContext ConwayEra
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
forall era.
ConwayCertExecContext era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
ccecDelegatees ConwayCertExecContext ConwayEra
ccec)) (ConwayCertExecContext ConwayEra -> Map RewardAccount Coin
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
_ = ConwayDelegEnv ConwayEra
-> CertState ConwayEra -> Specification ConwayDelegCert
ExecEnvironment "DELEG" ConwayEra
-> ExecState "DELEG" ConwayEra
-> Specification (ExecSignal "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 =
    (DState -> CertState)
-> Either OpaqueErrorString DState
-> 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
dState' -> DState -> PState -> GState -> CertState
Agda.MkCertState DState
dState' PState
pState GState
vState)
      (Either OpaqueErrorString DState
 -> Either
      OpaqueErrorString (SpecRep (ExecState "DELEG" ConwayEra)))
-> (T_ComputationResult_44 T_String_6 DState
    -> Either OpaqueErrorString DState)
-> T_ComputationResult_44 T_String_6 DState
-> Either OpaqueErrorString (SpecRep (ExecState "DELEG" ConwayEra))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_ComputationResult_44 T_String_6 DState
-> Either OpaqueErrorString DState
forall a.
ComputationResult T_String_6 a -> Either OpaqueErrorString a
unComputationResult
      (T_ComputationResult_44 T_String_6 DState
 -> Either
      OpaqueErrorString (SpecRep (ExecState "DELEG" ConwayEra)))
-> T_ComputationResult_44 T_String_6 DState
-> Either OpaqueErrorString (SpecRep (ExecState "DELEG" ConwayEra))
forall a b. (a -> b) -> a -> b
$ DelegEnv
-> DState -> DCert -> T_ComputationResult_44 T_String_6 DState
Agda.delegStep DelegEnv
SpecRep (ExecEnvironment "DELEG" ConwayEra)
env DState
dState DCert
SpecRep (ExecSignal "DELEG" ConwayEra)
sig

  classOf :: ExecSignal "DELEG" ConwayEra -> Maybe String
classOf = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> (ConwayDelegCert -> String) -> ConwayDelegCert -> Maybe String
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"