{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# 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 =
  (Term (CertEnv era) -> Pred) -> Specification (CertEnv era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (CertEnv era) -> Pred) -> Specification (CertEnv era))
-> (Term (CertEnv era) -> Pred) -> Specification (CertEnv era)
forall a b. (a -> b) -> a -> b
$ \Term (CertEnv era)
ce ->
    Term (CertEnv era)
-> FunTy (MapList Term (ProductAsList (CertEnv era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CertEnv era)
ce (FunTy (MapList Term (ProductAsList (CertEnv era))) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList (CertEnv era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (PParams era)
pp TermD Deps EpochNo
_currEpoch TermD Deps (StrictMaybe (Committee era))
_currCommittee TermD
  Deps (Map (GovPurposeId 'CommitteePurpose) (GovActionState era))
_proposals ->
      [ Term (PParams era) -> Specification (PParams era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParams era)
pp Specification (PParams era)
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 = (Term (Set (Credential DRepRole)) -> [Pred])
-> Specification (Set (Credential DRepRole))
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Set (Credential DRepRole)) -> [Pred])
 -> Specification (Set (Credential DRepRole)))
-> (Term (Set (Credential DRepRole)) -> [Pred])
-> Specification (Set (Credential DRepRole))
forall a b. (a -> b) -> a -> b
$ \Term (Set (Credential DRepRole))
x ->
  [ WitUniv era -> Term (Set (Credential DRepRole)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Set (Credential DRepRole))
x
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential DRepRole)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set (Credential DRepRole))
x Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
20
  , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential DRepRole)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set (Credential DRepRole))
x Term Integer -> Term Integer -> Term Bool
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 =
  (Term (ShelleyCertState era) -> Pred)
-> Specification (ShelleyCertState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ShelleyCertState era) -> Pred)
 -> Specification (ShelleyCertState era))
-> (Term (ShelleyCertState era) -> Pred)
-> Specification (ShelleyCertState era)
forall a b. (a -> b) -> a -> b
$ \Term (ShelleyCertState era)
cs ->
    Term (ShelleyCertState era)
-> FunTy
     (MapList Term (ProductAsList (ShelleyCertState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ShelleyCertState era)
cs (FunTy (MapList Term (ProductAsList (ShelleyCertState era))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ShelleyCertState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (PState era)
pState Term (DState era)
dState ->
      [ Term (PState era) -> Specification (PState era) -> Pred
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)
      , Term (DState era) -> Specification (DState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (DState era)
dState (forall era.
(Era era, HasSpec (Accounts 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 =
  (Term (ConwayCertState era) -> Pred)
-> Specification (ConwayCertState era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ConwayCertState era) -> Pred)
 -> Specification (ConwayCertState era))
-> (Term (ConwayCertState era) -> Pred)
-> Specification (ConwayCertState era)
forall a b. (a -> b) -> a -> b
$ \Term (ConwayCertState era)
cs ->
    Term (ConwayCertState era)
-> FunTy
     (MapList Term (ProductAsList (ConwayCertState era))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayCertState era)
cs (FunTy (MapList Term (ProductAsList (ConwayCertState era))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayCertState era))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (VState era)
vState Term (PState era)
pState Term (DState era)
dState ->
      [ Term (PState era) -> Specification (PState era) -> Pred
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)
      , Term (DState era) -> Specification (DState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (DState era)
dState (forall era.
(Era era, HasSpec (Accounts era)) =>
WitUniv era -> Map RewardAccount Coin -> Specification (DState era)
dStateSpec @era WitUniv era
univ Map RewardAccount Coin
wdrls)
      , Term (VState era) -> Specification (VState era) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (VState era)
vState (WitUniv era
-> Set (Credential DRepRole) -> Specification (VState era)
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) (GovActionState era)
cp) CertState era
certState =
  (Term (ConwayTxCert era) -> Pred)
-> Specification (ConwayTxCert era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ConwayTxCert era) -> Pred)
 -> Specification (ConwayTxCert era))
-> (Term (ConwayTxCert era) -> Pred)
-> Specification (ConwayTxCert era)
forall a b. (a -> b) -> a -> b
$ \Term (ConwayTxCert era)
txCert ->
    Term (ConwayTxCert era)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (ConwayTxCert era))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (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.
      (Int
-> FunTy (MapList Term (Args ConwayDelegCert)) Pred
-> Weighted (BinderD Deps) ConwayDelegCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args ConwayDelegCert)) Pred
 -> Weighted (BinderD Deps) ConwayDelegCert)
-> FunTy (MapList Term (Args ConwayDelegCert)) Pred
-> Weighted (BinderD Deps) ConwayDelegCert
forall a b. (a -> b) -> a -> b
$ \Term ConwayDelegCert
delegCert -> Term ConwayDelegCert -> Specification ConwayDelegCert -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ConwayDelegCert
delegCert (Specification ConwayDelegCert -> Pred)
-> Specification ConwayDelegCert -> Pred
forall a b. (a -> b) -> a -> b
$ ConwayDelegEnv era
-> CertState era -> Specification ConwayDelegCert
forall era.
(EraPParams era, ConwayEraCertState era) =>
ConwayDelegEnv era
-> CertState era -> Specification ConwayDelegCert
conwayDelegCertSpec ConwayDelegEnv era
delegEnv CertState era
certState)
      (Int
-> FunTy (MapList Term (Args PoolCert)) Pred
-> Weighted (BinderD Deps) PoolCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args PoolCert)) Pred
 -> Weighted (BinderD Deps) PoolCert)
-> FunTy (MapList Term (Args PoolCert)) Pred
-> Weighted (BinderD Deps) PoolCert
forall a b. (a -> b) -> a -> b
$ \Term PoolCert
poolCert -> Term PoolCert -> Specification PoolCert -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolCert
poolCert (Specification PoolCert -> Pred) -> Specification PoolCert -> Pred
forall a b. (a -> b) -> a -> b
$ WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert
forall era.
EraSpecPParams era =>
WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert
poolCertSpec WitUniv era
univ PoolEnv era
poolEnv PState era
certPState)
      (Int
-> FunTy (MapList Term (Args ConwayGovCert)) Pred
-> Weighted (BinderD Deps) ConwayGovCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy (MapList Term (Args ConwayGovCert)) Pred
 -> Weighted (BinderD Deps) ConwayGovCert)
-> FunTy (MapList Term (Args ConwayGovCert)) Pred
-> Weighted (BinderD Deps) ConwayGovCert
forall a b. (a -> b) -> a -> b
$ \Term ConwayGovCert
govCert -> Term ConwayGovCert -> Specification ConwayGovCert -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term ConwayGovCert
govCert (Specification ConwayGovCert -> Pred)
-> Specification ConwayGovCert -> Pred
forall a b. (a -> b) -> a -> b
$ WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
forall era.
EraCertState era =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
govCertSpec WitUniv era
univ ConwayGovCertEnv era
ConwayGovCertEnv ConwayEra
govCertEnv CertState era
CertState ConwayEra
certState)
  where
    certPState :: PState era
certPState = CertState era
ConwayCertState ConwayEra
certState ConwayCertState ConwayEra
-> Getting (PState era) (ConwayCertState ConwayEra) (PState era)
-> PState era
forall s a. s -> Getting a s a -> a
^. (PState era -> Const (PState era) (PState era))
-> CertState era -> Const (PState era) (CertState era)
Getting (PState era) (ConwayCertState ConwayEra) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL
    delegEnv :: ConwayDelegEnv era
delegEnv = PParams era
-> Map (KeyHash StakePool) StakePoolState -> ConwayDelegEnv era
forall era.
PParams era
-> Map (KeyHash StakePool) StakePoolState -> ConwayDelegEnv era
ConwayDelegEnv PParams era
pp (PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
certPState)
    poolEnv :: PoolEnv era
poolEnv = EpochNo -> PParams era -> PoolEnv era
forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv EpochNo
ce PParams era
pp
    govCertEnv :: ConwayGovCertEnv era
govCertEnv = PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> ConwayGovCertEnv era
forall era.
PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
-> ConwayGovCertEnv era
ConwayGovCertEnv PParams era
pp EpochNo
ce StrictMaybe (Committee era)
cc Map (GovPurposeId 'CommitteePurpose) (GovActionState era)
cp

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

-- | Genesis delegations only work through the Babbage era. Hence the (AtMostEra "Babbage" era)
genesisDelegCertSpec ::
  forall era.
  (AtMostEra "Babbage" era, Era era) =>
  DState era -> Specification GenesisDelegCert
genesisDelegCertSpec :: forall era.
(AtMostEra "Babbage" era, Era era) =>
DState era -> Specification GenesisDelegCert
genesisDelegCertSpec DState era
ds =
  let (KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF)
vrfKeyHashes, KeyHash GenesisRole -> Set (KeyHash GenesisDelegate)
coldKeyHashes) = DState era
-> (KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF),
    KeyHash GenesisRole -> Set (KeyHash GenesisDelegate))
forall era.
DState era
-> (KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF),
    KeyHash GenesisRole -> Set (KeyHash GenesisDelegate))
computeSets DState era
ds
      GenDelegs Map (KeyHash GenesisRole) GenDelegPair
genDelegs = DState era -> GenDelegs
forall era. DState era -> GenDelegs
dsGenDelegs DState era
ds
   in (Term GenesisDelegCert -> Pred) -> Specification GenesisDelegCert
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term GenesisDelegCert -> Pred) -> Specification GenesisDelegCert)
-> (Term GenesisDelegCert -> Pred)
-> Specification GenesisDelegCert
forall a b. (a -> b) -> a -> b
$ \ Term GenesisDelegCert
[var|gdc|] ->
        Term GenesisDelegCert
-> FunTy (MapList Term (ProductAsList GenesisDelegCert)) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenesisDelegCert
gdc (FunTy (MapList Term (ProductAsList GenesisDelegCert)) [Pred]
 -> Pred)
-> FunTy (MapList Term (ProductAsList GenesisDelegCert)) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (KeyHash GenesisRole)
[var|gkh|] Term (KeyHash GenesisDelegate)
[var|vkh|] Term (VRFVerKeyHash GenDelegVRF)
[var|hashVrf|] ->
          [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (KeyHash GenesisRole)
-> Term (Map (KeyHash GenesisRole) GenDelegPair) -> Term Bool
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term Bool
mapMember_ Term (KeyHash GenesisRole)
gkh (Map (KeyHash GenesisRole) GenDelegPair
-> Term (Map (KeyHash GenesisRole) GenDelegPair)
forall a. HasSpec a => a -> Term a
lit Map (KeyHash GenesisRole) GenDelegPair
genDelegs)
          , Term (KeyHash GenesisRole)
-> (KeyHash GenesisRole -> Set (KeyHash GenesisDelegate))
-> (Term (Set (KeyHash GenesisDelegate)) -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (KeyHash GenesisRole)
gkh KeyHash GenesisRole -> Set (KeyHash GenesisDelegate)
coldKeyHashes (\ Term (Set (KeyHash GenesisDelegate))
[var|coldkeys|] -> Term (KeyHash GenesisDelegate)
-> Term (Set (KeyHash GenesisDelegate)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (KeyHash GenesisDelegate)
vkh Term (Set (KeyHash GenesisDelegate))
coldkeys)
          , Term (KeyHash GenesisRole)
-> (KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF))
-> (Term (Set (VRFVerKeyHash GenDelegVRF)) -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (KeyHash GenesisRole)
gkh KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF)
vrfKeyHashes (\ Term (Set (VRFVerKeyHash GenDelegVRF))
[var|vrfkeys|] -> Term (VRFVerKeyHash GenDelegVRF)
-> Term (Set (VRFVerKeyHash GenDelegVRF)) -> Term Bool
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 GenesisRole -> Set (VRFVerKeyHash GenDelegVRF)
  , KeyHash GenesisRole -> Set (KeyHash GenesisDelegate)
  )
computeSets :: forall era.
DState era
-> (KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF),
    KeyHash GenesisRole -> Set (KeyHash GenesisDelegate))
computeSets DState era
ds =
  let genDelegs :: Map (KeyHash GenesisRole) GenDelegPair
genDelegs = GenDelegs -> Map (KeyHash GenesisRole) GenDelegPair
unGenDelegs (DState era -> GenDelegs
forall era. DState era -> GenDelegs
dsGenDelegs DState era
ds)
      futureGenDelegs :: Map FutureGenDeleg GenDelegPair
futureGenDelegs = DState era -> Map FutureGenDeleg GenDelegPair
forall era. DState era -> Map FutureGenDeleg GenDelegPair
dsFutureGenDelegs DState era
ds
      cod :: KeyHash GenesisRole -> Set GenDelegPair
cod KeyHash GenesisRole
gkh = [GenDelegPair] -> Set GenDelegPair
forall a. Ord a => [a] -> Set a
Set.fromList ([GenDelegPair] -> Set GenDelegPair)
-> [GenDelegPair] -> Set GenDelegPair
forall a b. (a -> b) -> a -> b
$ Map (KeyHash GenesisRole) GenDelegPair -> [GenDelegPair]
forall k a. Map k a -> [a]
Map.elems (Map (KeyHash GenesisRole) GenDelegPair -> [GenDelegPair])
-> Map (KeyHash GenesisRole) GenDelegPair -> [GenDelegPair]
forall a b. (a -> b) -> a -> b
$ KeyHash GenesisRole
-> Map (KeyHash GenesisRole) GenDelegPair
-> Map (KeyHash GenesisRole) GenDelegPair
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete KeyHash GenesisRole
gkh Map (KeyHash GenesisRole) GenDelegPair
genDelegs
      fod :: KeyHash GenesisRole -> Set GenDelegPair
fod KeyHash GenesisRole
gkh =
        [GenDelegPair] -> Set GenDelegPair
forall a. Ord a => [a] -> Set a
Set.fromList ([GenDelegPair] -> Set GenDelegPair)
-> [GenDelegPair] -> Set GenDelegPair
forall a b. (a -> b) -> a -> b
$ Map FutureGenDeleg GenDelegPair -> [GenDelegPair]
forall k a. Map k a -> [a]
Map.elems (Map FutureGenDeleg GenDelegPair -> [GenDelegPair])
-> Map FutureGenDeleg GenDelegPair -> [GenDelegPair]
forall a b. (a -> b) -> a -> b
$ (FutureGenDeleg -> GenDelegPair -> Bool)
-> Map FutureGenDeleg GenDelegPair
-> Map FutureGenDeleg GenDelegPair
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\(FutureGenDeleg SlotNo
_ KeyHash GenesisRole
g) GenDelegPair
_ -> KeyHash GenesisRole
g KeyHash GenesisRole -> KeyHash GenesisRole -> Bool
forall a. Eq a => a -> a -> Bool
/= KeyHash GenesisRole
gkh) Map FutureGenDeleg GenDelegPair
futureGenDelegs
      currentColdKeyHashes :: KeyHash GenesisRole -> Set (KeyHash GenesisDelegate)
currentColdKeyHashes KeyHash GenesisRole
gkh = (GenDelegPair -> KeyHash GenesisDelegate)
-> Set GenDelegPair -> Set (KeyHash GenesisDelegate)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> KeyHash GenesisDelegate
genDelegKeyHash (KeyHash GenesisRole -> Set GenDelegPair
cod KeyHash GenesisRole
gkh)
      currentVrfKeyHashes :: KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF)
currentVrfKeyHashes KeyHash GenesisRole
gkh = (GenDelegPair -> VRFVerKeyHash GenDelegVRF)
-> Set GenDelegPair -> Set (VRFVerKeyHash GenDelegVRF)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> VRFVerKeyHash GenDelegVRF
genDelegVrfHash (KeyHash GenesisRole -> Set GenDelegPair
cod KeyHash GenesisRole
gkh)
      futureColdKeyHashes :: KeyHash GenesisRole -> Set (KeyHash GenesisDelegate)
futureColdKeyHashes KeyHash GenesisRole
gkh = (GenDelegPair -> KeyHash GenesisDelegate)
-> Set GenDelegPair -> Set (KeyHash GenesisDelegate)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> KeyHash GenesisDelegate
genDelegKeyHash (KeyHash GenesisRole -> Set GenDelegPair
fod KeyHash GenesisRole
gkh)
      futureVrfKeyHashes :: KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF)
futureVrfKeyHashes KeyHash GenesisRole
gkh = (GenDelegPair -> VRFVerKeyHash GenDelegVRF)
-> Set GenDelegPair -> Set (VRFVerKeyHash GenDelegVRF)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map GenDelegPair -> VRFVerKeyHash GenDelegVRF
genDelegVrfHash (KeyHash GenesisRole -> Set GenDelegPair
fod KeyHash GenesisRole
gkh)
      coldKeyHashes :: KeyHash GenesisRole -> Set (KeyHash GenesisDelegate)
coldKeyHashes KeyHash GenesisRole
gkh = KeyHash GenesisRole -> Set (KeyHash GenesisDelegate)
currentColdKeyHashes KeyHash GenesisRole
gkh Set (KeyHash GenesisDelegate)
-> Set (KeyHash GenesisDelegate) -> Set (KeyHash GenesisDelegate)
forall a. Semigroup a => a -> a -> a
<> KeyHash GenesisRole -> Set (KeyHash GenesisDelegate)
futureColdKeyHashes KeyHash GenesisRole
gkh
      vrfKeyHashes :: KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF)
vrfKeyHashes KeyHash GenesisRole
gkh = KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF)
currentVrfKeyHashes KeyHash GenesisRole
gkh Set (VRFVerKeyHash GenDelegVRF)
-> Set (VRFVerKeyHash GenDelegVRF)
-> Set (VRFVerKeyHash GenDelegVRF)
forall a. Semigroup a => a -> a -> a
<> KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF)
futureVrfKeyHashes KeyHash GenesisRole
gkh
   in (KeyHash GenesisRole -> Set (VRFVerKeyHash GenDelegVRF)
vrfKeyHashes, KeyHash GenesisRole -> Set (KeyHash GenesisDelegate)
coldKeyHashes)

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

shelleyTxCertSpec ::
  forall era.
  (AtMostEra "Babbage" era, EraSpecPParams era, EraAccounts era) =>
  WitUniv era ->
  CertEnv era ->
  ShelleyCertState era ->
  Specification (ShelleyTxCert era)
shelleyTxCertSpec :: forall era.
(AtMostEra "Babbage" era, EraSpecPParams era, EraAccounts 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) (GovActionState era)
_) (ShelleyCertState PState era
pstate DState era
dstate) =
  (Term (ShelleyTxCert era) -> Pred)
-> Specification (ShelleyTxCert era)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ShelleyTxCert era) -> Pred)
 -> Specification (ShelleyTxCert era))
-> (Term (ShelleyTxCert era) -> Pred)
-> Specification (ShelleyTxCert era)
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.
    (Term (ShelleyTxCert era)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (ShelleyTxCert era))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (ShelleyTxCert era)
shelleyTxCert)
      ( Int
-> FunTy (MapList Term (Args ShelleyDelegCert)) Pred
-> Weighted (BinderD Deps) ShelleyDelegCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
5 (FunTy (MapList Term (Args ShelleyDelegCert)) Pred
 -> Weighted (BinderD Deps) ShelleyDelegCert)
-> FunTy (MapList Term (Args ShelleyDelegCert)) Pred
-> Weighted (BinderD Deps) ShelleyDelegCert
forall a b. (a -> b) -> a -> b
$ \ Term ShelleyDelegCert
[var|deleg|] ->
          Term ShelleyDelegCert -> Specification ShelleyDelegCert -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
            Term ShelleyDelegCert
deleg
            ( forall era.
(EraPParams era, EraAccounts era) =>
WitUniv era
-> ConwayDelegEnv era
-> DState era
-> Specification ShelleyDelegCert
shelleyDelegCertSpec @era
                WitUniv era
univ
                (PParams era
-> Map (KeyHash StakePool) StakePoolState -> ConwayDelegEnv era
forall era.
PParams era
-> Map (KeyHash StakePool) StakePoolState -> ConwayDelegEnv era
ConwayDelegEnv PParams era
pp (PState era -> Map (KeyHash StakePool) StakePoolState
forall era. PState era -> Map (KeyHash StakePool) StakePoolState
psStakePools PState era
pstate))
                DState era
dstate
            )
      )
      ( Int
-> FunTy (MapList Term (Args PoolCert)) Pred
-> Weighted (BinderD Deps) PoolCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
3 (FunTy (MapList Term (Args PoolCert)) Pred
 -> Weighted (BinderD Deps) PoolCert)
-> FunTy (MapList Term (Args PoolCert)) Pred
-> Weighted (BinderD Deps) PoolCert
forall a b. (a -> b) -> a -> b
$ \ Term PoolCert
[var|poolCert|] -> Term PoolCert -> Specification PoolCert -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term PoolCert
poolCert (Specification PoolCert -> Pred) -> Specification PoolCert -> Pred
forall a b. (a -> b) -> a -> b
$ WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert
forall era.
EraSpecPParams era =>
WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert
poolCertSpec WitUniv era
univ (EpochNo -> PParams era -> PoolEnv era
forall era. EpochNo -> PParams era -> PoolEnv era
PoolEnv EpochNo
currEpoch PParams era
pp) PState era
pstate
      )
      (Int
-> FunTy (MapList Term (Args GenesisDelegCert)) Pred
-> Weighted (BinderD Deps) GenesisDelegCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args GenesisDelegCert)) Pred
 -> Weighted (BinderD Deps) GenesisDelegCert)
-> FunTy (MapList Term (Args GenesisDelegCert)) Pred
-> Weighted (BinderD Deps) GenesisDelegCert
forall a b. (a -> b) -> a -> b
$ \ Term GenesisDelegCert
[var|genesis|] -> Term GenesisDelegCert -> Specification GenesisDelegCert -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term GenesisDelegCert
genesis (forall era.
(AtMostEra "Babbage" era, Era era) =>
DState era -> Specification GenesisDelegCert
genesisDelegCertSpec @era DState era
dstate))
      (Int
-> FunTy (MapList Term (Args MIRCert)) Bool
-> Weighted (BinderD Deps) MIRCert
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args MIRCert)) Bool
 -> Weighted (BinderD Deps) MIRCert)
-> FunTy (MapList Term (Args MIRCert)) Bool
-> Weighted (BinderD Deps) MIRCert
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 = WitUniv ShelleyEra
-> CertEnv ShelleyEra
-> CertState ShelleyEra
-> Specification (TxCert ShelleyEra)
WitUniv ShelleyEra
-> CertEnv ShelleyEra
-> ShelleyCertState ShelleyEra
-> Specification (ShelleyTxCert ShelleyEra)
forall era.
(AtMostEra "Babbage" era, EraSpecPParams era, EraAccounts era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert ShelleyEra -> CertKey
txCertKey = TxCert ShelleyEra -> CertKey
ShelleyTxCert ShelleyEra -> CertKey
forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv ShelleyEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState ShelleyEra)
certStateSpec = WitUniv ShelleyEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState ShelleyEra)
WitUniv ShelleyEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState ShelleyEra)
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 = WitUniv AllegraEra
-> CertEnv AllegraEra
-> CertState AllegraEra
-> Specification (TxCert AllegraEra)
WitUniv AllegraEra
-> CertEnv AllegraEra
-> ShelleyCertState AllegraEra
-> Specification (ShelleyTxCert AllegraEra)
forall era.
(AtMostEra "Babbage" era, EraSpecPParams era, EraAccounts era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert AllegraEra -> CertKey
txCertKey = TxCert AllegraEra -> CertKey
ShelleyTxCert AllegraEra -> CertKey
forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv AllegraEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState AllegraEra)
certStateSpec = WitUniv AllegraEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState AllegraEra)
WitUniv AllegraEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState AllegraEra)
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 = WitUniv MaryEra
-> CertEnv MaryEra
-> CertState MaryEra
-> Specification (TxCert MaryEra)
WitUniv MaryEra
-> CertEnv MaryEra
-> ShelleyCertState MaryEra
-> Specification (ShelleyTxCert MaryEra)
forall era.
(AtMostEra "Babbage" era, EraSpecPParams era, EraAccounts era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert MaryEra -> CertKey
txCertKey = TxCert MaryEra -> CertKey
ShelleyTxCert MaryEra -> CertKey
forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv MaryEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState MaryEra)
certStateSpec = WitUniv MaryEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState MaryEra)
WitUniv MaryEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState MaryEra)
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 = WitUniv AlonzoEra
-> CertEnv AlonzoEra
-> CertState AlonzoEra
-> Specification (TxCert AlonzoEra)
WitUniv AlonzoEra
-> CertEnv AlonzoEra
-> ShelleyCertState AlonzoEra
-> Specification (ShelleyTxCert AlonzoEra)
forall era.
(AtMostEra "Babbage" era, EraSpecPParams era, EraAccounts era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert AlonzoEra -> CertKey
txCertKey = TxCert AlonzoEra -> CertKey
ShelleyTxCert AlonzoEra -> CertKey
forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv AlonzoEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState AlonzoEra)
certStateSpec = WitUniv AlonzoEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState AlonzoEra)
WitUniv AlonzoEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState AlonzoEra)
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 = WitUniv BabbageEra
-> CertEnv BabbageEra
-> CertState BabbageEra
-> Specification (TxCert BabbageEra)
WitUniv BabbageEra
-> CertEnv BabbageEra
-> ShelleyCertState BabbageEra
-> Specification (ShelleyTxCert BabbageEra)
forall era.
(AtMostEra "Babbage" era, EraSpecPParams era, EraAccounts era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec
  txCertKey :: TxCert BabbageEra -> CertKey
txCertKey = TxCert BabbageEra -> CertKey
ShelleyTxCert BabbageEra -> CertKey
forall era. ShelleyTxCert era -> CertKey
shelleyTxCertKey
  certStateSpec :: WitUniv BabbageEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState BabbageEra)
certStateSpec = WitUniv BabbageEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState BabbageEra)
WitUniv BabbageEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (ShelleyCertState BabbageEra)
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 = WitUniv ConwayEra
-> CertEnv ConwayEra
-> CertState ConwayEra
-> Specification (TxCert ConwayEra)
WitUniv ConwayEra
-> CertEnv ConwayEra
-> CertState ConwayEra
-> Specification (ConwayTxCert ConwayEra)
forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec
  txCertKey :: TxCert ConwayEra -> CertKey
txCertKey = TxCert ConwayEra -> CertKey
ConwayTxCert ConwayEra -> CertKey
forall era. ConwayTxCert era -> CertKey
conwayTxCertKey
  certStateSpec :: WitUniv ConwayEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState ConwayEra)
certStateSpec = WitUniv ConwayEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState ConwayEra)
WitUniv ConwayEra
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (ConwayCertState ConwayEra)
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 GenesisRole)
  | MirKey !MIRPot
  deriving (CertKey -> CertKey -> Bool
(CertKey -> CertKey -> Bool)
-> (CertKey -> CertKey -> Bool) -> Eq CertKey
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CertKey -> CertKey -> Bool
== :: CertKey -> CertKey -> Bool
$c/= :: CertKey -> CertKey -> Bool
/= :: CertKey -> CertKey -> Bool
Eq, Int -> CertKey -> ShowS
[CertKey] -> ShowS
CertKey -> String
(Int -> CertKey -> ShowS)
-> (CertKey -> String) -> ([CertKey] -> ShowS) -> Show CertKey
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CertKey -> ShowS
showsPrec :: Int -> CertKey -> ShowS
$cshow :: CertKey -> String
show :: CertKey -> String
$cshowList :: [CertKey] -> ShowS
showList :: [CertKey] -> ShowS
Show, Eq CertKey
Eq CertKey =>
(CertKey -> CertKey -> Ordering)
-> (CertKey -> CertKey -> Bool)
-> (CertKey -> CertKey -> Bool)
-> (CertKey -> CertKey -> Bool)
-> (CertKey -> CertKey -> Bool)
-> (CertKey -> CertKey -> CertKey)
-> (CertKey -> CertKey -> CertKey)
-> Ord 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
$ccompare :: CertKey -> CertKey -> Ordering
compare :: CertKey -> CertKey -> Ordering
$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
>= :: CertKey -> CertKey -> Bool
$cmax :: CertKey -> CertKey -> CertKey
max :: CertKey -> CertKey -> CertKey
$cmin :: CertKey -> CertKey -> CertKey
min :: CertKey -> CertKey -> CertKey
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 StakePoolParams
x)) = KeyHash StakePool -> CertKey
PoolKey (StakePoolParams -> KeyHash StakePool
sppId StakePoolParams
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 StakePoolParams
x)) = KeyHash StakePool -> CertKey
PoolKey (StakePoolParams -> KeyHash StakePool
sppId StakePoolParams
x)
shelleyTxCertKey (ShelleyTxCertPool (RetirePool KeyHash StakePool
x EpochNo
_)) = KeyHash StakePool -> CertKey
PoolKey KeyHash StakePool
x
shelleyTxCertKey (ShelleyTxCertGenesisDeleg (GenesisDelegCert KeyHash GenesisRole
a KeyHash GenesisDelegate
_ VRFVerKeyHash GenDelegVRF
_)) = KeyHash GenesisRole -> CertKey
GenesisKey KeyHash GenesisRole
a
shelleyTxCertKey (ShelleyTxCertMir (MIRCert MIRPot
p MIRTarget
_)) = MIRPot -> CertKey
MirKey MIRPot
p

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

testGenesisCert ::
  forall era.
  (AtMostEra "Babbage" era, EraSpecDeleg era, EraSpecPParams era, GenScript era) => Gen Property
testGenesisCert :: forall era.
(AtMostEra "Babbage" era, EraSpecDeleg era, EraSpecPParams era,
 GenScript era) =>
Gen Property
testGenesisCert = do
  univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
  wdrls <- genFromSpec (constrained $ \Term (Map RewardAccount Coin)
x -> WitUniv era -> Term (Map RewardAccount Coin) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Map RewardAccount Coin)
x)
  dstate <- genFromSpec @(DState era) (dStateSpec @era univ wdrls)
  let spec = DState era -> Specification GenesisDelegCert
forall era.
(AtMostEra "Babbage" era, Era era) =>
DState era -> Specification GenesisDelegCert
genesisDelegCertSpec DState era
dstate
  ans <- genFromSpec spec
  pure $ property (conformsToSpec ans spec)

testShelleyCert ::
  forall era.
  ( Era era
  , AtMostEra "Babbage" era
  , EraSpecPParams era
  , EraSpecDeleg era
  , GenScript era
  , EraCertState era
  ) =>
  Gen Property
testShelleyCert :: forall era.
(Era era, AtMostEra "Babbage" era, EraSpecPParams era,
 EraSpecDeleg era, GenScript era, EraCertState era) =>
Gen Property
testShelleyCert = do
  univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
  wdrls <- genFromSpec (constrained $ \Term (Map RewardAccount Coin)
x -> WitUniv era -> Term (Map RewardAccount Coin) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ Term (Map RewardAccount Coin)
x)
  delegatees <- genFromSpec (delegateeSpec univ)
  env <- genFromSpec @(CertEnv era) (certEnvSpec @era univ)
  dstate <-
    genFromSpec @(ShelleyCertState era)
      (shelleyCertStateSpec @era univ delegatees wdrls)
  let spec = WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
forall era.
(AtMostEra "Babbage" era, EraSpecPParams era, EraAccounts era) =>
WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
shelleyTxCertSpec WitUniv era
univ CertEnv era
env ShelleyCertState era
dstate
  ans <- genFromSpec spec
  let 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"
  pure (classify True tag (property (conformsToSpec ans spec)))

testConwayCert :: Gen Property
testConwayCert :: Gen Property
testConwayCert = do
  univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
200
  env <- genFromSpec @(CertEnv ConwayEra) (certEnvSpec @ConwayEra univ)
  wdrls <- genFromSpec (constrained $ \Term (Map RewardAccount Coin)
x -> WitUniv ConwayEra -> Term (Map RewardAccount Coin) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv ConwayEra
univ Term (Map RewardAccount Coin)
x)
  delegatees <- genFromSpec (delegateeSpec univ)
  dstate <-
    genFromSpec @(CertState ConwayEra)
      (conwayCertStateSpec univ delegatees wdrls)
  let spec :: Specification (ConwayTxCert ConwayEra)
      spec = WitUniv ConwayEra
-> CertEnv ConwayEra
-> CertState ConwayEra
-> Specification (ConwayTxCert ConwayEra)
forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec WitUniv ConwayEra
univ CertEnv ConwayEra
env CertState ConwayEra
ConwayCertState ConwayEra
dstate
  ans <- genFromSpec spec
  let 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 StakePoolParams
_)) -> 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"
  pure (classify True tag (conformsToSpec ans spec))