{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Specs necessary to generate, environment, state, and signal
-- for the CERT rule
module Test.Cardano.Ledger.Constrained.Conway.Cert where

import Cardano.Ledger.Allegra (AllegraEra)
import Cardano.Ledger.Alonzo (AlonzoEra)
import Cardano.Ledger.Babbage (BabbageEra)
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Core
import Cardano.Ledger.Mary (MaryEra)
import Cardano.Ledger.Shelley (ShelleyEra)
import Cardano.Ledger.Shelley.API.Types
import Cardano.Ledger.Shelley.TxCert (ShelleyTxCert (..))
import Constrained.API
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Lens.Micro ((^.))
import Test.Cardano.Ledger.Constrained.Conway.Deleg
import Test.Cardano.Ledger.Constrained.Conway.GovCert
import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
import Test.Cardano.Ledger.Constrained.Conway.PParams
import Test.Cardano.Ledger.Constrained.Conway.Pool
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.QuickCheck hiding (forAll, witness)

certEnvSpec ::
  forall era.
  EraSpecPParams era =>
  WitUniv era -> Specification (CertEnv era)
certEnvSpec :: forall era.
EraSpecPParams era =>
WitUniv era -> Specification (CertEnv era)
certEnvSpec WitUniv era
_univ =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (CertEnv era)
ce ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CertEnv era)
ce forall a b. (a -> b) -> a -> b
$ \Term (PParams era)
pp Term EpochNo
_currEpoch Term (StrictMaybe (Committee era))
_currCommittee Term
  (Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
_proposals ->
      [ forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParams era)
pp forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
      ]

delegateeSpec ::
  Era era =>
  WitUniv era ->
  Specification (Set (Credential 'DRepRole))
delegateeSpec :: forall era.
Era era =>
WitUniv era -> Specification (Set (Credential 'DRepRole))
delegateeSpec WitUniv era
univ = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Set (Credential 'DRepRole))
x ->
  [ forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Set (Credential 'DRepRole))
x
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall t. (HasSpec t, Sized t) => Term t -> Term Integer
sizeOf_ Term (Set (Credential 'DRepRole))
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
20
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall t. (HasSpec t, Sized t) => Term t -> Term Integer
sizeOf_ Term (Set (Credential 'DRepRole))
x forall a. OrdLike a => Term a -> Term a -> Term Bool
>=. Term Integer
10
  ]

shelleyCertStateSpec ::
  forall era.
  (EraSpecDeleg era, EraCertState era) =>
  WitUniv era ->
  Set (Credential 'DRepRole) ->
  Map (RewardAccount) Coin ->
  Specification (ShelleyCertState era)
shelleyCertStateSpec :: forall era.
(EraSpecDeleg era, EraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState era)
shelleyCertStateSpec WitUniv era
univ Set (Credential 'DRepRole)
_delegatees Map RewardAccount Coin
wdrls =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (ShelleyCertState era)
cs ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ShelleyCertState era)
cs forall a b. (a -> b) -> a -> b
$ \Term (PState era)
pState Term (DState era)
dState ->
      [ forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PState era)
pState (forall era. Era era => WitUniv era -> Specification (PState era)
pStateSpec @era WitUniv era
univ)
      , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (DState era)
dState (forall era.
EraSpecDeleg era =>
WitUniv era -> Map RewardAccount Coin -> Specification (DState era)
dStateSpec @era WitUniv era
univ Map RewardAccount Coin
wdrls)
      ]

conwayCertStateSpec ::
  forall era.
  (EraSpecDeleg era, EraCertState era, ConwayEraCertState era) =>
  WitUniv era ->
  Set (Credential 'DRepRole) ->
  Map (RewardAccount) Coin ->
  Specification (ConwayCertState era)
conwayCertStateSpec :: forall era.
(EraSpecDeleg era, EraCertState era, ConwayEraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ConwayCertState era)
conwayCertStateSpec WitUniv era
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
wdrls =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (ConwayCertState era)
cs ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayCertState era)
cs forall a b. (a -> b) -> a -> b
$ \Term (VState era)
vState Term (PState era)
pState Term (DState era)
dState ->
      [ forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PState era)
pState (forall era. Era era => WitUniv era -> Specification (PState era)
pStateSpec @era WitUniv era
univ)
      , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (DState era)
dState (forall era.
EraSpecDeleg era =>
WitUniv era -> Map RewardAccount Coin -> Specification (DState era)
dStateSpec @era WitUniv era
univ Map RewardAccount Coin
wdrls)
      , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (VState era)
vState (forall era.
Era era =>
WitUniv era
-> Set (Credential 'DRepRole) -> Specification (VState era)
vStateSpec WitUniv era
univ Set (Credential 'DRepRole)
delegatees)
      ]

conwayTxCertSpec ::
  forall era.
  era ~ ConwayEra =>
  WitUniv era ->
  CertEnv era ->
  CertState era ->
  Specification (ConwayTxCert era)
conwayTxCertSpec :: forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec WitUniv era
univ (CertEnv PParams era
pp EpochNo
ce StrictMaybe (Committee era)
cc Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
cp) CertState era
certState =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (ConwayTxCert era)
txCert ->
    forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn
      Term (ConwayTxCert era)
txCert
      -- These weights try to make it equally likely that each of the many certs
      -- across the 3 categories are chosen at similar frequencies.
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \Term ConwayDelegCert
delegCert -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ConwayDelegCert
delegCert forall a b. (a -> b) -> a -> b
$ forall era.
(EraPParams era, ConwayEraCertState era) =>
ConwayDelegEnv era
-> CertState era -> Specification ConwayDelegCert
conwayDelegCertSpec ConwayDelegEnv era
delegEnv CertState era
certState)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term PoolCert
poolCert -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolCert
poolCert forall a b. (a -> b) -> a -> b
$ forall era.
EraSpecPParams era =>
WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert
poolCertSpec WitUniv era
univ PoolEnv era
poolEnv PState era
certPState)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
2 forall a b. (a -> b) -> a -> b
$ \Term ConwayGovCert
govCert -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ConwayGovCert
govCert forall a b. (a -> b) -> a -> b
$ forall era.
EraCertState era =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
govCertSpec WitUniv era
univ ConwayGovCertEnv era
govCertEnv CertState era
certState)
  where
    certPState :: PState era
certPState = CertState era
certState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL
    delegEnv :: ConwayDelegEnv era
delegEnv = forall era.
PParams era
-> Map (KeyHash 'StakePool) PoolParams -> ConwayDelegEnv era
ConwayDelegEnv PParams era
pp (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
certPState)
    poolEnv :: PoolEnv era
poolEnv = forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv EpochNo
ce PParams era
pp
    govCertEnv :: ConwayGovCertEnv era
govCertEnv = forall era.
PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
-> ConwayGovCertEnv era
ConwayGovCertEnv PParams era
pp EpochNo
ce StrictMaybe (Committee era)
cc Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
cp

-- ==============================================================
-- Shelley Certs

-- | Genesis delegations only work through the Babbage era. Hence the (AtMostEra BabbageEra era)
genesisDelegCertSpec ::
  forall era.
  (AtMostEra BabbageEra era, Era era) =>
  DState era -> Specification GenesisDelegCert
genesisDelegCertSpec :: forall era.
(AtMostEra BabbageEra era, Era era) =>
DState era -> Specification GenesisDelegCert
genesisDelegCertSpec DState era
ds =
  let (KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
vrfKeyHashes, KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
coldKeyHashes) = forall era.
DState era
-> (KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF),
    KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate))
computeSets DState era
ds
      GenDelegs Map (KeyHash 'Genesis) GenDelegPair
genDelegs = forall era. DState era -> GenDelegs
dsGenDelegs DState era
ds
   in forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term GenesisDelegCert
[var|gdc|] ->
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenesisDelegCert
gdc forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash 'Genesis)
[var|gkh|] Term (KeyHash 'GenesisDelegate)
[var|vkh|] Term (VRFVerKeyHash 'GenDelegVRF)
[var|hashVrf|] ->
          [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (KeyHash 'Genesis)
gkh (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ (forall a. HasSpec a => a -> Term a
lit Map (KeyHash 'Genesis) GenDelegPair
genDelegs))
          , forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (KeyHash 'Genesis)
gkh KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
coldKeyHashes (\ Term (Set (KeyHash 'GenesisDelegate))
[var|coldkeys|] -> forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (KeyHash 'GenesisDelegate)
vkh Term (Set (KeyHash 'GenesisDelegate))
coldkeys)
          , forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (KeyHash 'Genesis)
gkh KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
vrfKeyHashes (\ Term (Set (VRFVerKeyHash 'GenDelegVRF))
[var|vrfkeys|] -> forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (VRFVerKeyHash 'GenDelegVRF)
hashVrf Term (Set (VRFVerKeyHash 'GenDelegVRF))
vrfkeys)
          ]

-- | Compute 2 functions from the DState. Each function, given a KeyHash,
--   returns a Set of 'Hashes', we expect certain things to be in those sets.
--   This mimics what happens in the Cardano.Ledger.Shelley.Rules.Deleg module
computeSets ::
  DState era ->
  ( KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
  , KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
  )
computeSets :: forall era.
DState era
-> (KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF),
    KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate))
computeSets DState era
ds =
  let genDelegs :: Map (KeyHash 'Genesis) GenDelegPair
genDelegs = GenDelegs -> Map (KeyHash 'Genesis) GenDelegPair
unGenDelegs (forall era. DState era -> GenDelegs
dsGenDelegs DState era
ds)
      futureGenDelegs :: Map FutureGenDeleg GenDelegPair
futureGenDelegs = forall era. DState era -> Map FutureGenDeleg GenDelegPair
dsFutureGenDelegs DState era
ds
      cod :: KeyHash 'Genesis -> Set GenDelegPair
cod KeyHash 'Genesis
gkh = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Map k a
Map.delete KeyHash 'Genesis
gkh Map (KeyHash 'Genesis) GenDelegPair
genDelegs
      fod :: KeyHash 'Genesis -> Set GenDelegPair
fod KeyHash 'Genesis
gkh =
        forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\(FutureGenDeleg SlotNo
_ KeyHash 'Genesis
g) GenDelegPair
_ -> KeyHash 'Genesis
g forall a. Eq a => a -> a -> Bool
/= KeyHash 'Genesis
gkh) Map FutureGenDeleg GenDelegPair
futureGenDelegs
      currentColdKeyHashes :: KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
currentColdKeyHashes KeyHash 'Genesis
gkh = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> KeyHash 'GenesisDelegate
genDelegKeyHash (KeyHash 'Genesis -> Set GenDelegPair
cod KeyHash 'Genesis
gkh)
      currentVrfKeyHashes :: KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
currentVrfKeyHashes KeyHash 'Genesis
gkh = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> VRFVerKeyHash 'GenDelegVRF
genDelegVrfHash (KeyHash 'Genesis -> Set GenDelegPair
cod KeyHash 'Genesis
gkh)
      futureColdKeyHashes :: KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
futureColdKeyHashes KeyHash 'Genesis
gkh = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> KeyHash 'GenesisDelegate
genDelegKeyHash (KeyHash 'Genesis -> Set GenDelegPair
fod KeyHash 'Genesis
gkh)
      futureVrfKeyHashes :: KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
futureVrfKeyHashes KeyHash 'Genesis
gkh = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> VRFVerKeyHash 'GenDelegVRF
genDelegVrfHash (KeyHash 'Genesis -> Set GenDelegPair
fod KeyHash 'Genesis
gkh)
      coldKeyHashes :: KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
coldKeyHashes KeyHash 'Genesis
gkh = KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
currentColdKeyHashes KeyHash 'Genesis
gkh forall a. Semigroup a => a -> a -> a
<> KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
futureColdKeyHashes KeyHash 'Genesis
gkh
      vrfKeyHashes :: KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
vrfKeyHashes KeyHash 'Genesis
gkh = KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
currentVrfKeyHashes KeyHash 'Genesis
gkh forall a. Semigroup a => a -> a -> a
<> KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
futureVrfKeyHashes KeyHash 'Genesis
gkh
   in (KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
vrfKeyHashes, KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
coldKeyHashes)

-- =======================================

shelleyTxCertSpec ::
  forall era.
  (AtMostEra BabbageEra era, EraSpecPParams era) =>
  WitUniv era ->
  CertEnv era ->
  ShelleyCertState era ->
  Specification (ShelleyTxCert era)
shelleyTxCertSpec :: forall era.
(AtMostEra BabbageEra era, EraSpecPParams era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec WitUniv era
univ (CertEnv PParams era
pp EpochNo
currEpoch StrictMaybe (Committee era)
_ Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
_) (ShelleyCertState PState era
pstate DState era
dstate) =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (ShelleyTxCert era)
[var|shelleyTxCert|] ->
    -- These weights try to make it equally likely that each of the many certs
    -- across the 3 categories are chosen at similar frequencies.
    (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term (ShelleyTxCert era)
shelleyTxCert)
      ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
5 forall a b. (a -> b) -> a -> b
$ \ Term ShelleyDelegCert
[var|deleg|] ->
          forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
            Term ShelleyDelegCert
deleg
            ( forall era.
EraPParams era =>
WitUniv era
-> ConwayDelegEnv era
-> DState era
-> Specification ShelleyDelegCert
shelleyDelegCertSpec @era
                WitUniv era
univ
                (forall era.
PParams era
-> Map (KeyHash 'StakePool) PoolParams -> ConwayDelegEnv era
ConwayDelegEnv PParams era
pp (forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams PState era
pstate))
                DState era
dstate
            )
      )
      ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \ Term PoolCert
[var|poolCert|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolCert
poolCert forall a b. (a -> b) -> a -> b
$ forall era.
EraSpecPParams era =>
WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert
poolCertSpec WitUniv era
univ (forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv EpochNo
currEpoch PParams era
pp) PState era
pstate
      )
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term GenesisDelegCert
[var|genesis|] -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term GenesisDelegCert
genesis (forall era.
(AtMostEra BabbageEra era, Era era) =>
DState era -> Specification GenesisDelegCert
genesisDelegCertSpec @era DState era
dstate))
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term MIRCert
[var|_mir|] -> Bool
False) -- By design, we never generate a MIR cert

-- =========================================================================
-- Making Cert Era parametric with the EraSpecCert class

class
  ( HasSpec (TxCert era)
  , EraCertState era
  ) =>
  EraSpecCert era
  where
  txCertSpec :: WitUniv era -> CertEnv era -> CertState era -> Specification (TxCert era)
  txCertKey :: TxCert era -> CertKey
  certStateSpec ::
    WitUniv era ->
    Set (Credential 'DRepRole) ->
    Map (RewardAccount) Coin ->
    Specification (CertState era)

instance EraSpecCert ShelleyEra where
  txCertSpec :: WitUniv ShelleyEra
-> CertEnv ShelleyEra
-> CertState ShelleyEra
-> Specification (TxCert ShelleyEra)
txCertSpec = forall era.
(AtMostEra BabbageEra era, EraSpecPParams era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert ShelleyEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv ShelleyEra
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState ShelleyEra)
certStateSpec = forall era.
(EraSpecDeleg era, EraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState era)
shelleyCertStateSpec
instance EraSpecCert AllegraEra where
  txCertSpec :: WitUniv AllegraEra
-> CertEnv AllegraEra
-> CertState AllegraEra
-> Specification (TxCert AllegraEra)
txCertSpec = forall era.
(AtMostEra BabbageEra era, EraSpecPParams era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert AllegraEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv AllegraEra
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState AllegraEra)
certStateSpec = forall era.
(EraSpecDeleg era, EraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState era)
shelleyCertStateSpec
instance EraSpecCert MaryEra where
  txCertSpec :: WitUniv MaryEra
-> CertEnv MaryEra
-> CertState MaryEra
-> Specification (TxCert MaryEra)
txCertSpec = forall era.
(AtMostEra BabbageEra era, EraSpecPParams era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert MaryEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv MaryEra
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState MaryEra)
certStateSpec = forall era.
(EraSpecDeleg era, EraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState era)
shelleyCertStateSpec
instance EraSpecCert AlonzoEra where
  txCertSpec :: WitUniv AlonzoEra
-> CertEnv AlonzoEra
-> CertState AlonzoEra
-> Specification (TxCert AlonzoEra)
txCertSpec = forall era.
(AtMostEra BabbageEra era, EraSpecPParams era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert AlonzoEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv AlonzoEra
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState AlonzoEra)
certStateSpec = forall era.
(EraSpecDeleg era, EraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState era)
shelleyCertStateSpec
instance EraSpecCert BabbageEra where
  txCertSpec :: WitUniv BabbageEra
-> CertEnv BabbageEra
-> CertState BabbageEra
-> Specification (TxCert BabbageEra)
txCertSpec = forall era.
(AtMostEra BabbageEra era, EraSpecPParams era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert BabbageEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv BabbageEra
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState BabbageEra)
certStateSpec = forall era.
(EraSpecDeleg era, EraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState era)
shelleyCertStateSpec
instance EraSpecCert ConwayEra where
  txCertSpec :: WitUniv ConwayEra
-> CertEnv ConwayEra
-> CertState ConwayEra
-> Specification (TxCert ConwayEra)
txCertSpec = forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec
  txCertKey :: TxCert ConwayEra -> CertKey
txCertKey = forall era. ConwayTxCert era -> CertKey
conwayTxCertKey
  certStateSpec :: WitUniv ConwayEra
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState ConwayEra)
certStateSpec = forall era.
(EraSpecDeleg era, EraCertState era, ConwayEraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ConwayCertState era)
conwayCertStateSpec

-- | Used to aggregate the key used in registering a Certificate. Different
--   certificates use different kinds of Keys, that allows us to use one
--   type to represent all kinds of keys (Similar to DepositPurpose)
data CertKey
  = StakeKey !(Credential 'Staking)
  | PoolKey !(KeyHash 'StakePool)
  | DRepKey !(Credential 'DRepRole)
  | ColdKey !(Credential 'ColdCommitteeRole)
  | GenesisKey !(KeyHash 'Genesis)
  | MirKey !MIRPot
  deriving (CertKey -> CertKey -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CertKey -> CertKey -> Bool
$c/= :: CertKey -> CertKey -> Bool
== :: CertKey -> CertKey -> Bool
$c== :: CertKey -> CertKey -> Bool
Eq, Int -> CertKey -> ShowS
[CertKey] -> ShowS
CertKey -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CertKey] -> ShowS
$cshowList :: [CertKey] -> ShowS
show :: CertKey -> String
$cshow :: CertKey -> String
showsPrec :: Int -> CertKey -> ShowS
$cshowsPrec :: Int -> CertKey -> ShowS
Show, Eq CertKey
CertKey -> CertKey -> Bool
CertKey -> CertKey -> Ordering
CertKey -> CertKey -> CertKey
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CertKey -> CertKey -> CertKey
$cmin :: CertKey -> CertKey -> CertKey
max :: CertKey -> CertKey -> CertKey
$cmax :: CertKey -> CertKey -> CertKey
>= :: CertKey -> CertKey -> Bool
$c>= :: CertKey -> CertKey -> Bool
> :: CertKey -> CertKey -> Bool
$c> :: CertKey -> CertKey -> Bool
<= :: CertKey -> CertKey -> Bool
$c<= :: CertKey -> CertKey -> Bool
< :: CertKey -> CertKey -> Bool
$c< :: CertKey -> CertKey -> Bool
compare :: CertKey -> CertKey -> Ordering
$ccompare :: CertKey -> CertKey -> Ordering
Ord)

-- | Compute the aggregate key type of a Certificater
conwayTxCertKey :: ConwayTxCert era -> CertKey
conwayTxCertKey :: forall era. ConwayTxCert era -> CertKey
conwayTxCertKey (ConwayTxCertDeleg (ConwayRegCert Credential 'Staking
x StrictMaybe Coin
_)) = Credential 'Staking -> CertKey
StakeKey Credential 'Staking
x
conwayTxCertKey (ConwayTxCertDeleg (ConwayUnRegCert Credential 'Staking
x StrictMaybe Coin
_)) = Credential 'Staking -> CertKey
StakeKey Credential 'Staking
x
conwayTxCertKey (ConwayTxCertDeleg (ConwayDelegCert Credential 'Staking
x Delegatee
_)) = Credential 'Staking -> CertKey
StakeKey Credential 'Staking
x
conwayTxCertKey (ConwayTxCertDeleg (ConwayRegDelegCert Credential 'Staking
x Delegatee
_ Coin
_)) = Credential 'Staking -> CertKey
StakeKey Credential 'Staking
x
conwayTxCertKey (ConwayTxCertPool (RegPool PoolParams
x)) = KeyHash 'StakePool -> CertKey
PoolKey (PoolParams -> KeyHash 'StakePool
ppId PoolParams
x)
conwayTxCertKey (ConwayTxCertPool (RetirePool KeyHash 'StakePool
x EpochNo
_)) = KeyHash 'StakePool -> CertKey
PoolKey KeyHash 'StakePool
x
conwayTxCertKey (ConwayTxCertGov (ConwayRegDRep Credential 'DRepRole
x Coin
_ StrictMaybe Anchor
_)) = Credential 'DRepRole -> CertKey
DRepKey Credential 'DRepRole
x
conwayTxCertKey (ConwayTxCertGov (ConwayUnRegDRep Credential 'DRepRole
x Coin
_)) = Credential 'DRepRole -> CertKey
DRepKey Credential 'DRepRole
x
conwayTxCertKey (ConwayTxCertGov (ConwayUpdateDRep Credential 'DRepRole
x StrictMaybe Anchor
_)) = Credential 'DRepRole -> CertKey
DRepKey Credential 'DRepRole
x
conwayTxCertKey (ConwayTxCertGov (ConwayAuthCommitteeHotKey Credential 'ColdCommitteeRole
x Credential 'HotCommitteeRole
_)) = Credential 'ColdCommitteeRole -> CertKey
ColdKey Credential 'ColdCommitteeRole
x
conwayTxCertKey (ConwayTxCertGov (ConwayResignCommitteeColdKey Credential 'ColdCommitteeRole
x StrictMaybe Anchor
_)) = Credential 'ColdCommitteeRole -> CertKey
ColdKey Credential 'ColdCommitteeRole
x

shelleyTxCertKey :: ShelleyTxCert era -> CertKey
shelleyTxCertKey :: forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey (ShelleyTxCertDelegCert (ShelleyRegCert Credential 'Staking
x)) = Credential 'Staking -> CertKey
StakeKey Credential 'Staking
x
shelleyTxCertKey (ShelleyTxCertDelegCert (ShelleyUnRegCert Credential 'Staking
x)) = Credential 'Staking -> CertKey
StakeKey Credential 'Staking
x
shelleyTxCertKey (ShelleyTxCertDelegCert (ShelleyDelegCert Credential 'Staking
x KeyHash 'StakePool
_)) = Credential 'Staking -> CertKey
StakeKey Credential 'Staking
x
shelleyTxCertKey (ShelleyTxCertPool (RegPool PoolParams
x)) = KeyHash 'StakePool -> CertKey
PoolKey (PoolParams -> KeyHash 'StakePool
ppId PoolParams
x)
shelleyTxCertKey (ShelleyTxCertPool (RetirePool KeyHash 'StakePool
x EpochNo
_)) = KeyHash 'StakePool -> CertKey
PoolKey KeyHash 'StakePool
x
shelleyTxCertKey (ShelleyTxCertGenesisDeleg (GenesisDelegCert KeyHash 'Genesis
a KeyHash 'GenesisDelegate
_ VRFVerKeyHash 'GenDelegVRF
_)) = KeyHash 'Genesis -> CertKey
GenesisKey KeyHash 'Genesis
a
shelleyTxCertKey (ShelleyTxCertMir (MIRCert MIRPot
p MIRTarget
_)) = MIRPot -> CertKey
MirKey MIRPot
p

-- =====================================================

testGenesisCert ::
  forall era.
  (AtMostEra BabbageEra era, EraSpecDeleg era, EraSpecPParams era, GenScript era) => Gen Property
testGenesisCert :: forall era.
(AtMostEra BabbageEra era, EraSpecDeleg era, EraSpecPParams era,
 GenScript era) =>
Gen Property
testGenesisCert = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
  Map RewardAccount Coin
wdrls <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
x -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Map RewardAccount Coin)
x)
  DState era
dstate <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(DState era) (forall era.
EraSpecDeleg era =>
WitUniv era -> Map RewardAccount Coin -> Specification (DState era)
dStateSpec @era WitUniv era
univ Map RewardAccount Coin
wdrls)
  let spec :: Specification GenesisDelegCert
spec = forall era.
(AtMostEra BabbageEra era, Era era) =>
DState era -> Specification GenesisDelegCert
genesisDelegCertSpec DState era
dstate
  GenesisDelegCert
ans <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification GenesisDelegCert
spec
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property (forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec GenesisDelegCert
ans Specification GenesisDelegCert
spec)

testShelleyCert ::
  forall era.
  ( Era era
  , AtMostEra BabbageEra era
  , EraSpecPParams era
  , EraSpecDeleg era
  , GenScript era
  , EraCertState era
  ) =>
  Gen Property
testShelleyCert :: forall era.
(Era era, AtMostEra BabbageEra era, EraSpecPParams era,
 EraSpecDeleg era, GenScript era, EraCertState era) =>
Gen Property
testShelleyCert = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
  Map RewardAccount Coin
wdrls <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
x -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Map RewardAccount Coin)
x)
  Set (Credential 'DRepRole)
delegatees <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
Era era =>
WitUniv era -> Specification (Set (Credential 'DRepRole))
delegateeSpec WitUniv era
univ)
  CertEnv era
env <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertEnv era) (forall era.
EraSpecPParams era =>
WitUniv era -> Specification (CertEnv era)
certEnvSpec @era WitUniv era
univ)
  ShelleyCertState era
dstate <-
    forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(ShelleyCertState era)
      (forall era.
(EraSpecDeleg era, EraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState era)
shelleyCertStateSpec @era WitUniv era
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
wdrls)
  let spec :: Specification (ShelleyTxCert era)
spec = forall era.
(AtMostEra BabbageEra era, EraSpecPParams era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec WitUniv era
univ CertEnv era
env ShelleyCertState era
dstate
  ShelleyTxCert era
ans <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification (ShelleyTxCert era)
spec
  let tag :: String
tag = case ShelleyTxCert era
ans of
        ShelleyTxCertDelegCert ShelleyDelegCert
x -> case ShelleyDelegCert
x of
          ShelleyRegCert {} -> String
"Register"
          ShelleyUnRegCert {} -> String
"UnRegister"
          ShelleyDelegCert {} -> String
"Delegate"
        ShelleyTxCertPool PoolCert
x -> case PoolCert
x of
          RegPool {} -> String
"RegPool"
          RetirePool {} -> String
"RetirePool"
        ShelleyTxCertGenesisDeleg GenesisDelegCert
_ -> String
"Genesis"
        ShelleyTxCertMir MIRCert
_ -> String
"Mir"
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
True String
tag (forall prop. Testable prop => prop -> Property
property (forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec ShelleyTxCert era
ans Specification (ShelleyTxCert era)
spec)))

testConwayCert :: Gen Property
testConwayCert :: Gen Property
testConwayCert = do
  WitUniv ConwayEra
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
200
  CertEnv ConwayEra
env <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertEnv ConwayEra) (forall era.
EraSpecPParams era =>
WitUniv era -> Specification (CertEnv era)
certEnvSpec @ConwayEra WitUniv ConwayEra
univ)
  Map RewardAccount Coin
wdrls <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
x -> forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv ConwayEra
univ Term (Map RewardAccount Coin)
x)
  Set (Credential 'DRepRole)
delegatees <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
Era era =>
WitUniv era -> Specification (Set (Credential 'DRepRole))
delegateeSpec WitUniv ConwayEra
univ)
  ConwayCertState ConwayEra
dstate <-
    forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertState ConwayEra)
      (forall era.
(EraSpecDeleg era, EraCertState era, ConwayEraCertState era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (ConwayCertState era)
conwayCertStateSpec WitUniv ConwayEra
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
wdrls)
  let spec :: Specification (ConwayTxCert ConwayEra)
      spec :: Specification (ConwayTxCert ConwayEra)
spec = forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec WitUniv ConwayEra
univ CertEnv ConwayEra
env ConwayCertState ConwayEra
dstate
  ConwayTxCert ConwayEra
ans <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification (ConwayTxCert ConwayEra)
spec
  let tag :: String
tag = case ConwayTxCert ConwayEra
ans of
        (ConwayTxCertDeleg (ConwayRegCert Credential 'Staking
_ StrictMaybe Coin
_)) -> String
"Register"
        (ConwayTxCertDeleg (ConwayUnRegCert Credential 'Staking
_ StrictMaybe Coin
_)) -> String
"UnRegister"
        (ConwayTxCertDeleg (ConwayDelegCert Credential 'Staking
_ Delegatee
_)) -> String
"Delegate"
        (ConwayTxCertDeleg (ConwayRegDelegCert Credential 'Staking
_ Delegatee
_ Coin
_)) -> String
"Register&Delegate"
        (ConwayTxCertPool (RegPool PoolParams
_)) -> String
"RegPool"
        (ConwayTxCertPool (RetirePool KeyHash 'StakePool
_ EpochNo
_)) -> String
"RetirePool"
        (ConwayTxCertGov (ConwayRegDRep Credential 'DRepRole
_ Coin
_ StrictMaybe Anchor
_)) -> String
"RegDRep"
        (ConwayTxCertGov (ConwayUnRegDRep Credential 'DRepRole
_ Coin
_)) -> String
"UnRegDRep"
        (ConwayTxCertGov (ConwayUpdateDRep Credential 'DRepRole
_ StrictMaybe Anchor
_)) -> String
"UpdateDRep"
        (ConwayTxCertGov (ConwayAuthCommitteeHotKey Credential 'ColdCommitteeRole
_ Credential 'HotCommitteeRole
_)) -> String
"AuthCommittee"
        (ConwayTxCertGov (ConwayResignCommitteeColdKey Credential 'ColdCommitteeRole
_ StrictMaybe Anchor
_)) -> String
"ResignCommittee"
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
True String
tag (forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec ConwayTxCert ConwayEra
ans Specification (ConwayTxCert ConwayEra)
spec))