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

module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (nameTxCert) where

import Cardano.Ledger.Conway
import Cardano.Ledger.Conway.TxCert (ConwayTxCert (..))
import Constrained.API
import qualified MAlonzo.Code.Ledger.Foreign.API as Agda
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert (nameGovCert)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool (namePoolCert)
import Test.Cardano.Ledger.Constrained.Conway
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse

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

  genExecContext :: HasCallStack => Gen (ExecContext "CERT" 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 "CERT" ConwayEra
-> Specification (ExecEnvironment "CERT" ConwayEra)
environmentSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) = forall era.
EraSpecPParams era =>
WitUniv era -> Specification (CertEnv era)
certEnvSpec @ConwayEra WitUniv ConwayEra
univ

  stateSpec :: HasCallStack =>
ExecContext "CERT" ConwayEra
-> ExecEnvironment "CERT" ConwayEra
-> Specification (ExecState "CERT" ConwayEra)
stateSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
ccec) ExecEnvironment "CERT" ConwayEra
_ =
    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 "CERT" ConwayEra
-> ExecEnvironment "CERT" ConwayEra
-> ExecState "CERT" ConwayEra
-> Specification (ExecSignal "CERT" ConwayEra)
signalSpec (WitUniv ConwayEra
univ, ConwayCertExecContext ConwayEra
_) ExecEnvironment "CERT" ConwayEra
env ExecState "CERT" ConwayEra
state = forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec @ConwayEra WitUniv ConwayEra
univ CertEnv ConwayEra
ExecEnvironment "CERT" ConwayEra
env CertState ConwayEra
ExecState "CERT" ConwayEra
state

  runAgdaRule :: HasCallStack =>
SpecRep (ExecEnvironment "CERT" ConwayEra)
-> SpecRep (ExecState "CERT" ConwayEra)
-> SpecRep (ExecSignal "CERT" ConwayEra)
-> Either OpaqueErrorString (SpecRep (ExecState "CERT" ConwayEra))
runAgdaRule SpecRep (ExecEnvironment "CERT" ConwayEra)
env SpecRep (ExecState "CERT" ConwayEra)
st SpecRep (ExecSignal "CERT" ConwayEra)
sig =
    ComputationResult Text CertState
-> Either OpaqueErrorString CertState
forall a. ComputationResult Text a -> Either OpaqueErrorString a
unComputationResult (ComputationResult Text CertState
 -> Either OpaqueErrorString CertState)
-> ComputationResult Text CertState
-> Either OpaqueErrorString CertState
forall a b. (a -> b) -> a -> b
$
      CertEnv -> CertState -> DCert -> ComputationResult Text CertState
Agda.certStep CertEnv
SpecRep (ExecEnvironment "CERT" ConwayEra)
env CertState
SpecRep (ExecState "CERT" ConwayEra)
st DCert
SpecRep (ExecSignal "CERT" ConwayEra)
sig

  classOf :: ExecSignal "CERT" ConwayEra -> Maybe String
classOf = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> (ConwayTxCert ConwayEra -> String)
-> ConwayTxCert ConwayEra
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConwayTxCert ConwayEra -> String
nameTxCert

nameTxCert :: ConwayTxCert ConwayEra -> String
nameTxCert :: ConwayTxCert ConwayEra -> String
nameTxCert (ConwayTxCertDeleg ConwayDelegCert
x) = ConwayDelegCert -> String
nameDelegCert ConwayDelegCert
x
nameTxCert (ConwayTxCertPool PoolCert
x) = PoolCert -> String
namePoolCert PoolCert
x
nameTxCert (ConwayTxCertGov ConwayGovCert
x) = ConwayGovCert -> String
nameGovCert ConwayGovCert
x