{-# 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.CertState
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Rules
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
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
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 fn era.
  (EraSpecPParams era, IsConwayUniv fn) =>
  WitUniv era -> Specification fn (CertEnv era)
certEnvSpec :: forall (fn :: Univ) era.
(EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (CertEnv era)
certEnvSpec WitUniv era
_univ =
  forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (CertEnv era)
ce ->
    forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (CertEnv era)
ce forall a b. (a -> b) -> a -> b
$ \Term fn (PParams era)
pp Term fn EpochNo
_currEpoch Term fn (StrictMaybe (Committee era))
_currCommittee Term
  fn (Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
_proposals ->
      [ forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PParams era)
pp forall (fn :: Univ) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec
      ]

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

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

conwayTxCertSpec ::
  forall fn era.
  (IsConwayUniv fn, era ~ ConwayEra) =>
  WitUniv era ->
  CertEnv era ->
  CertState era ->
  Specification fn (ConwayTxCert era)
conwayTxCertSpec :: forall (fn :: Univ) era.
(IsConwayUniv fn, era ~ ConwayEra) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ConwayTxCert era)
conwayTxCertSpec WitUniv era
univ (CertEnv PParams era
pp EpochNo
ce StrictMaybe (Committee era)
cc Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
cp) certState :: CertState era
certState@CertState {DState era
PState era
VState era
certVState :: forall era. CertState era -> VState era
certPState :: forall era. CertState era -> PState era
certDState :: forall era. CertState era -> DState era
certDState :: DState era
certPState :: PState era
certVState :: VState era
..} =
  forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (ConwayTxCert era)
txCert ->
    forall (fn :: Univ) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
      Term fn (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 (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \Term fn ConwayDelegCert
delegCert -> forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn ConwayDelegCert
delegCert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) era.
(EraPParams era, IsConwayUniv fn) =>
ConwayDelegEnv era
-> CertState era -> Specification fn ConwayDelegCert
conwayDelegCertSpec ConwayDelegEnv era
delegEnv CertState era
certState)
      (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term fn PoolCert
poolCert -> forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn PoolCert
poolCert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) era.
(EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> PoolEnv era -> PState era -> Specification fn PoolCert
poolCertSpec WitUniv era
univ PoolEnv era
poolEnv PState era
certPState)
      (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
2 forall a b. (a -> b) -> a -> b
$ \Term fn ConwayGovCert
govCert -> forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn ConwayGovCert
govCert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification fn ConwayGovCert
govCertSpec WitUniv era
univ ConwayGovCertEnv era
govCertEnv CertState era
certState)
  where
    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 fn era.
  (AtMostEra BabbageEra era, IsConwayUniv fn, Era era) =>
  DState era -> Specification fn GenesisDelegCert
genesisDelegCertSpec :: forall (fn :: Univ) era.
(AtMostEra BabbageEra era, IsConwayUniv fn, Era era) =>
DState era -> Specification fn 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 (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn GenesisDelegCert
[var|gdc|] ->
        forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn GenesisDelegCert
gdc forall a b. (a -> b) -> a -> b
$ \ Term fn (KeyHash 'Genesis)
[var|gkh|] Term fn (KeyHash 'GenesisDelegate)
[var|vkh|] Term fn (VRFVerKeyHash 'GenDelegVRF)
[var|hashVrf|] ->
          [ forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (KeyHash 'Genesis)
gkh (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ (forall a (fn :: Univ). Show a => a -> Term fn a
lit Map (KeyHash 'Genesis) GenDelegPair
genDelegs))
          , forall (fn :: Univ) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (KeyHash 'Genesis)
gkh KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
coldKeyHashes (\ Term fn (Set (KeyHash 'GenesisDelegate))
[var|coldkeys|] -> forall a (fn :: Univ).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (KeyHash 'GenesisDelegate)
vkh Term fn (Set (KeyHash 'GenesisDelegate))
coldkeys)
          , forall (fn :: Univ) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (KeyHash 'Genesis)
gkh KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
vrfKeyHashes (\ Term fn (Set (VRFVerKeyHash 'GenDelegVRF))
[var|vrfkeys|] -> forall a (fn :: Univ).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (VRFVerKeyHash 'GenDelegVRF)
hashVrf Term fn (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 fn era.
  (AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
  WitUniv era ->
  CertEnv era ->
  CertState era ->
  Specification fn (ShelleyTxCert era)
shelleyTxCertSpec :: forall (fn :: Univ) era.
(AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ShelleyTxCert era)
shelleyTxCertSpec WitUniv era
univ (CertEnv PParams era
pp EpochNo
currEpoch StrictMaybe (Committee era)
_ Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
_) (CertState VState era
_vstate PState era
pstate DState era
dstate) =
  forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (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 (fn :: Univ) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn (ShelleyTxCert era)
shelleyTxCert)
      ( forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
5 forall a b. (a -> b) -> a -> b
$ \ Term fn ShelleyDelegCert
[var|deleg|] ->
          forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies
            Term fn ShelleyDelegCert
deleg
            ( forall (fn :: Univ) era.
(EraPParams era, IsConwayUniv fn) =>
WitUniv era
-> ConwayDelegEnv era
-> DState era
-> Specification fn ShelleyDelegCert
shelleyDelegCertSpec @fn @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 (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \ Term fn PoolCert
[var|poolCert|] -> forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn PoolCert
poolCert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) era.
(EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> PoolEnv era -> PState era -> Specification fn PoolCert
poolCertSpec WitUniv era
univ (forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv EpochNo
currEpoch PParams era
pp) PState era
pstate
      )
      (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term fn GenesisDelegCert
[var|genesis|] -> forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn GenesisDelegCert
genesis (forall (fn :: Univ) era.
(AtMostEra BabbageEra era, IsConwayUniv fn, Era era) =>
DState era -> Specification fn GenesisDelegCert
genesisDelegCertSpec @fn @era DState era
dstate))
      (forall (fn :: Univ) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \ Term fn MIRCert
[var|_mir|] -> Bool
False) -- By design, we never generate a MIR cert

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

class
  ( IsConwayUniv fn
  , HasSpec fn (TxCert era)
  , Era era
  ) =>
  EraSpecCert era fn
  where
  txCertSpec :: WitUniv era -> CertEnv era -> CertState era -> Specification fn (TxCert era)
  txCertKey :: TxCert era -> CertKey

instance IsConwayUniv fn => EraSpecCert ShelleyEra fn where
  txCertSpec :: WitUniv ShelleyEra
-> CertEnv ShelleyEra
-> CertState ShelleyEra
-> Specification fn (TxCert ShelleyEra)
txCertSpec = forall (fn :: Univ) era.
(AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert ShelleyEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
instance IsConwayUniv fn => EraSpecCert AllegraEra fn where
  txCertSpec :: WitUniv AllegraEra
-> CertEnv AllegraEra
-> CertState AllegraEra
-> Specification fn (TxCert AllegraEra)
txCertSpec = forall (fn :: Univ) era.
(AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert AllegraEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
instance IsConwayUniv fn => EraSpecCert MaryEra fn where
  txCertSpec :: WitUniv MaryEra
-> CertEnv MaryEra
-> CertState MaryEra
-> Specification fn (TxCert MaryEra)
txCertSpec = forall (fn :: Univ) era.
(AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert MaryEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
instance IsConwayUniv fn => EraSpecCert AlonzoEra fn where
  txCertSpec :: WitUniv AlonzoEra
-> CertEnv AlonzoEra
-> CertState AlonzoEra
-> Specification fn (TxCert AlonzoEra)
txCertSpec = forall (fn :: Univ) era.
(AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert AlonzoEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
instance IsConwayUniv fn => EraSpecCert BabbageEra fn where
  txCertSpec :: WitUniv BabbageEra
-> CertEnv BabbageEra
-> CertState BabbageEra
-> Specification fn (TxCert BabbageEra)
txCertSpec = forall (fn :: Univ) era.
(AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert BabbageEra -> CertKey
txCertKey = forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
instance IsConwayUniv fn => EraSpecCert ConwayEra fn where
  txCertSpec :: WitUniv ConwayEra
-> CertEnv ConwayEra
-> CertState ConwayEra
-> Specification fn (TxCert ConwayEra)
txCertSpec = forall (fn :: Univ) era.
(IsConwayUniv fn, era ~ ConwayEra) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ConwayTxCert era)
conwayTxCertSpec
  txCertKey :: TxCert ConwayEra -> CertKey
txCertKey = forall era. ConwayTxCert era -> CertKey
conwayTxCertKey

-- | 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 (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term ConwayFn (Map RewardAccount Coin)
x -> forall (fn :: Univ) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term ConwayFn (Map RewardAccount Coin)
x)
  DState era
dstate <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(DState era) (forall (fn :: Univ) era.
(IsConwayUniv fn, EraSpecDeleg era) =>
WitUniv era
-> Map RewardAccount Coin -> Specification fn (DState era)
dStateSpec @ConwayFn @era WitUniv era
univ Map RewardAccount Coin
wdrls)
  let spec :: Specification ConwayFn GenesisDelegCert
spec = forall (fn :: Univ) era.
(AtMostEra BabbageEra era, IsConwayUniv fn, Era era) =>
DState era -> Specification fn GenesisDelegCert
genesisDelegCertSpec @ConwayFn DState era
dstate
  GenesisDelegCert
ans <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn Specification ConwayFn 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 (fn :: Univ) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec GenesisDelegCert
ans Specification ConwayFn GenesisDelegCert
spec)

testShelleyCert ::
  forall era.
  (Era era, AtMostEra BabbageEra era, EraSpecPParams era, EraSpecDeleg era, GenScript era) =>
  Gen Property
testShelleyCert :: forall era.
(Era era, AtMostEra BabbageEra era, EraSpecPParams era,
 EraSpecDeleg era, GenScript 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 (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term ConwayFn (Map RewardAccount Coin)
x -> forall (fn :: Univ) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv era
univ Term ConwayFn (Map RewardAccount Coin)
x)
  Set (Credential 'DRepRole)
delegatees <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
WitUniv era -> Specification fn (Set (Credential 'DRepRole))
delegateeSpec WitUniv era
univ)
  CertEnv era
env <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertEnv era) (forall (fn :: Univ) era.
(EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (CertEnv era)
certEnvSpec @ConwayFn @era WitUniv era
univ)
  CertState era
dstate <-
    forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertState era) (forall (fn :: Univ) era.
(IsConwayUniv fn, EraSpecDeleg era, Era era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (CertState era)
certStateSpec @ConwayFn @era WitUniv era
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
wdrls)
  let spec :: Specification
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (ShelleyTxCert era)
spec = forall (fn :: Univ) era.
(AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ShelleyTxCert era)
shelleyTxCertSpec WitUniv era
univ CertEnv era
env CertState era
dstate
  ShelleyTxCert era
ans <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn Specification
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (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 (fn :: Univ) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec ShelleyTxCert era
ans Specification
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  (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 (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertEnv ConwayEra) (forall (fn :: Univ) era.
(EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (CertEnv era)
certEnvSpec @ConwayFn @ConwayEra WitUniv ConwayEra
univ)
  Map RewardAccount Coin
wdrls <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term ConwayFn (Map RewardAccount Coin)
x -> forall (fn :: Univ) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv ConwayEra
univ Term ConwayFn (Map RewardAccount Coin)
x)
  Set (Credential 'DRepRole)
delegatees <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
WitUniv era -> Specification fn (Set (Credential 'DRepRole))
delegateeSpec WitUniv ConwayEra
univ)
  CertState ConwayEra
dstate <-
    forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertState ConwayEra)
      (forall (fn :: Univ) era.
(IsConwayUniv fn, EraSpecDeleg era, Era era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (CertState era)
certStateSpec @ConwayFn @ConwayEra WitUniv ConwayEra
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
wdrls)
  let spec :: Specification ConwayFn (ConwayTxCert ConwayEra)
      spec :: Specification ConwayFn (ConwayTxCert ConwayEra)
spec = forall (fn :: Univ) era.
(IsConwayUniv fn, era ~ ConwayEra) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ConwayTxCert era)
conwayTxCertSpec WitUniv ConwayEra
univ CertEnv ConwayEra
env CertState ConwayEra
dstate
  ConwayTxCert ConwayEra
ans <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn Specification ConwayFn (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 (fn :: Univ) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec ConwayTxCert ConwayEra
ans Specification ConwayFn (ConwayTxCert ConwayEra)
spec))