{-# 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 =
  (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 era) (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.
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 =
  (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.
EraSpecDeleg 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 era) (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) PoolParams -> ConwayDelegEnv era
forall era.
PParams era
-> Map (KeyHash 'StakePool) PoolParams -> ConwayDelegEnv era
ConwayDelegEnv PParams era
pp (PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams 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 era) (GovActionState era)
-> ConwayGovCertEnv era
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) = DState era
-> (KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF),
    KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate))
forall era.
DState era
-> (KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF),
    KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate))
computeSets DState era
ds
      GenDelegs Map (KeyHash 'Genesis) 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 'Genesis)
[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 'Genesis)
-> Term (Set (KeyHash 'Genesis)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (KeyHash 'Genesis)
gkh (Term (Map (KeyHash 'Genesis) GenDelegPair)
-> Term (Set (KeyHash 'Genesis))
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_ (Map (KeyHash 'Genesis) GenDelegPair
-> Term (Map (KeyHash 'Genesis) GenDelegPair)
forall a. HasSpec a => a -> Term a
lit Map (KeyHash 'Genesis) GenDelegPair
genDelegs))
          , Term (KeyHash 'Genesis)
-> (KeyHash 'Genesis -> 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 'Genesis)
gkh KeyHash 'Genesis -> 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 'Genesis)
-> (KeyHash 'Genesis -> 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 'Genesis)
gkh KeyHash 'Genesis -> 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 '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 (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 'Genesis -> Set GenDelegPair
cod KeyHash 'Genesis
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 'Genesis) GenDelegPair -> [GenDelegPair]
forall k a. Map k a -> [a]
Map.elems (Map (KeyHash 'Genesis) GenDelegPair -> [GenDelegPair])
-> Map (KeyHash 'Genesis) GenDelegPair -> [GenDelegPair]
forall a b. (a -> b) -> a -> b
$ KeyHash 'Genesis
-> Map (KeyHash 'Genesis) GenDelegPair
-> Map (KeyHash 'Genesis) GenDelegPair
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 =
        [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 'Genesis
g) GenDelegPair
_ -> KeyHash 'Genesis
g KeyHash 'Genesis -> KeyHash 'Genesis -> Bool
forall a. Eq a => a -> a -> Bool
/= KeyHash 'Genesis
gkh) Map FutureGenDeleg GenDelegPair
futureGenDelegs
      currentColdKeyHashes :: KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
currentColdKeyHashes KeyHash 'Genesis
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 'Genesis -> Set GenDelegPair
cod KeyHash 'Genesis
gkh)
      currentVrfKeyHashes :: KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
currentVrfKeyHashes KeyHash 'Genesis
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 'Genesis -> Set GenDelegPair
cod KeyHash 'Genesis
gkh)
      futureColdKeyHashes :: KeyHash 'Genesis -> Set (KeyHash 'GenesisDelegate)
futureColdKeyHashes KeyHash 'Genesis
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 'Genesis -> Set GenDelegPair
fod KeyHash 'Genesis
gkh)
      futureVrfKeyHashes :: KeyHash 'Genesis -> Set (VRFVerKeyHash 'GenDelegVRF)
futureVrfKeyHashes KeyHash 'Genesis
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 '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 Set (KeyHash 'GenesisDelegate)
-> Set (KeyHash 'GenesisDelegate) -> Set (KeyHash 'GenesisDelegate)
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 Set (VRFVerKeyHash 'GenDelegVRF)
-> Set (VRFVerKeyHash 'GenDelegVRF)
-> Set (VRFVerKeyHash 'GenDelegVRF)
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) =
  (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 =>
WitUniv era
-> ConwayDelegEnv era
-> DState era
-> Specification ShelleyDelegCert
shelleyDelegCertSpec @era
                WitUniv era
univ
                (PParams era
-> Map (KeyHash 'StakePool) PoolParams -> ConwayDelegEnv era
forall era.
PParams era
-> Map (KeyHash 'StakePool) PoolParams -> ConwayDelegEnv era
ConwayDelegEnv PParams era
pp (PState era -> Map (KeyHash 'StakePool) PoolParams
forall era. PState era -> Map (KeyHash 'StakePool) PoolParams
psStakePoolParams 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 BabbageEra 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 BabbageEra era, EraSpecPParams 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 BabbageEra era, EraSpecPParams 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 BabbageEra era, EraSpecPParams 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 BabbageEra era, EraSpecPParams 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 BabbageEra era, EraSpecPParams 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 'Genesis)
  | 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 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 <- Specification (Map RewardAccount Coin)
-> Gen (Map RewardAccount Coin)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec ((Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map RewardAccount Coin) -> Pred)
 -> Specification (Map RewardAccount Coin))
-> (Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a b. (a -> b) -> a -> b
$ \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 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 = DState era -> Specification GenesisDelegCert
forall era.
(AtMostEra BabbageEra era, Era era) =>
DState era -> Specification GenesisDelegCert
genesisDelegCertSpec DState era
dstate
  GenesisDelegCert
ans <- Specification GenesisDelegCert -> Gen GenesisDelegCert
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification GenesisDelegCert
spec
  Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property (GenesisDelegCert -> Specification GenesisDelegCert -> Bool
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 <- Specification (Map RewardAccount Coin)
-> Gen (Map RewardAccount Coin)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec ((Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map RewardAccount Coin) -> Pred)
 -> Specification (Map RewardAccount Coin))
-> (Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a b. (a -> b) -> a -> b
$ \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)
  Set (Credential 'DRepRole)
delegatees <- Specification (Set (Credential 'DRepRole))
-> Gen (Set (Credential 'DRepRole))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv era -> Specification (Set (Credential 'DRepRole))
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 = WitUniv era
-> CertEnv era
-> ShelleyCertState era
-> Specification (ShelleyTxCert era)
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 <- Specification (ShelleyTxCert era) -> Gen (ShelleyTxCert era)
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"
  Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
True String
tag (Bool -> Property
forall prop. Testable prop => prop -> Property
property (ShelleyTxCert era -> Specification (ShelleyTxCert era) -> Bool
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 <- Specification (Map RewardAccount Coin)
-> Gen (Map RewardAccount Coin)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec ((Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map RewardAccount Coin) -> Pred)
 -> Specification (Map RewardAccount Coin))
-> (Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a b. (a -> b) -> a -> b
$ \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)
  Set (Credential 'DRepRole)
delegatees <- Specification (Set (Credential 'DRepRole))
-> Gen (Set (Credential 'DRepRole))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv ConwayEra -> Specification (Set (Credential 'DRepRole))
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)
      (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 WitUniv ConwayEra
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
wdrls)
  let spec :: Specification (ConwayTxCert ConwayEra)
      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
  ConwayTxCert ConwayEra
ans <- Specification (ConwayTxCert ConwayEra)
-> Gen (ConwayTxCert ConwayEra)
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"
  Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> String -> Bool -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
True String
tag (ConwayTxCert ConwayEra
-> Specification (ConwayTxCert ConwayEra) -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec ConwayTxCert ConwayEra
ans Specification (ConwayTxCert ConwayEra)
spec))