{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards #-}

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

import Cardano.Ledger.CertState
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Shelley.API.Types

import Constrained

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Crypto (StandardCrypto)
import Test.Cardano.Ledger.Constrained.Conway.Deleg
import Test.Cardano.Ledger.Constrained.Conway.GovCert
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams
import Test.Cardano.Ledger.Constrained.Conway.Pool

certEnvSpec ::
  IsConwayUniv fn =>
  Specification fn (CertEnv (ConwayEra StandardCrypto))
certEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (CertEnv (ConwayEra StandardCrypto))
certEnvSpec =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (CertEnv (ConwayEra StandardCrypto))
ce ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (CertEnv (ConwayEra StandardCrypto))
ce forall a b. (a -> b) -> a -> b
$ \Term fn SlotNo
_slot Term fn (PParams (ConwayEra StandardCrypto))
pp Term fn EpochNo
_currEpoch Term fn (StrictMaybe (Committee (ConwayEra StandardCrypto)))
_currCommittee Term
  fn
  (Map
     (GovPurposeId 'CommitteePurpose (ConwayEra StandardCrypto))
     (GovActionState (ConwayEra StandardCrypto)))
_proposals ->
      [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PParams (ConwayEra StandardCrypto))
pp forall (fn :: [*] -> * -> *) era.
(EraPP era, BaseUniverse fn) =>
Specification fn (PParams era)
pparamsSpec
      ]

certStateSpec ::
  IsConwayUniv fn =>
  Specification fn (CertState (ConwayEra StandardCrypto))
certStateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (CertState (ConwayEra StandardCrypto))
certStateSpec =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (CertState (ConwayEra StandardCrypto))
cs ->
    forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (CertState (ConwayEra StandardCrypto))
cs forall a b. (a -> b) -> a -> b
$ \Term fn (VState (ConwayEra StandardCrypto))
vState Term fn (PState (ConwayEra StandardCrypto))
pState Term fn (DState (ConwayEra StandardCrypto))
dState ->
      [ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (VState (ConwayEra StandardCrypto))
vState forall (fn :: [*] -> * -> *).
Specification fn (VState (ConwayEra StandardCrypto))
vStateSpec
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PState (ConwayEra StandardCrypto))
pState forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (PState (ConwayEra StandardCrypto))
pStateSpec
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (DState (ConwayEra StandardCrypto))
dState forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (DState (ConwayEra StandardCrypto))
dStateSpec
      ]

txCertSpec ::
  IsConwayUniv fn =>
  CertEnv (ConwayEra StandardCrypto) ->
  CertState (ConwayEra StandardCrypto) ->
  Specification fn (ConwayTxCert (ConwayEra StandardCrypto))
txCertSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
CertEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (ConwayTxCert (ConwayEra StandardCrypto))
txCertSpec (CertEnv SlotNo
slot PParams (ConwayEra StandardCrypto)
pp EpochNo
ce StrictMaybe (Committee (ConwayEra StandardCrypto))
cc Map
  (GovPurposeId 'CommitteePurpose (ConwayEra StandardCrypto))
  (GovActionState (ConwayEra StandardCrypto))
cp) certState :: CertState (ConwayEra StandardCrypto)
certState@CertState {DState (ConwayEra StandardCrypto)
PState (ConwayEra StandardCrypto)
VState (ConwayEra StandardCrypto)
certVState :: forall era. CertState era -> VState era
certPState :: forall era. CertState era -> PState era
certDState :: forall era. CertState era -> DState era
certDState :: DState (ConwayEra StandardCrypto)
certPState :: PState (ConwayEra StandardCrypto)
certVState :: VState (ConwayEra StandardCrypto)
..} =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (ConwayTxCert (ConwayEra StandardCrypto))
txCert ->
    forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
      Term fn (ConwayTxCert (ConwayEra StandardCrypto))
txCert
      -- These weights try to make it equally likely that each of the many certs
      -- across the 3 categories are chosen at similar frequencies.
      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \Term fn (ConwayDelegCert StandardCrypto)
delegCert -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (ConwayDelegCert StandardCrypto)
delegCert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayDelegEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (ConwayDelegCert StandardCrypto)
delegCertSpec ConwayDelegEnv (ConwayEra StandardCrypto)
delegEnv CertState (ConwayEra StandardCrypto)
certState)
      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term fn (PoolCert StandardCrypto)
poolCert -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PoolCert StandardCrypto)
poolCert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
PoolEnv (ConwayEra StandardCrypto)
-> PState (ConwayEra StandardCrypto)
-> Specification fn (PoolCert StandardCrypto)
poolCertSpec PoolEnv (ConwayEra StandardCrypto)
poolEnv PState (ConwayEra StandardCrypto)
certPState)
      (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
3 forall a b. (a -> b) -> a -> b
$ \Term fn (ConwayGovCert StandardCrypto)
govCert -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (ConwayGovCert StandardCrypto)
govCert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
ConwayGovCertEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (ConwayGovCert StandardCrypto)
govCertSpec ConwayGovCertEnv (ConwayEra StandardCrypto)
govCertEnv CertState (ConwayEra StandardCrypto)
certState)
  where
    delegEnv :: ConwayDelegEnv (ConwayEra StandardCrypto)
delegEnv = forall era.
PParams era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
-> ConwayDelegEnv era
ConwayDelegEnv PParams (ConwayEra StandardCrypto)
pp (forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams PState (ConwayEra StandardCrypto)
certPState)
    poolEnv :: PoolEnv (ConwayEra StandardCrypto)
poolEnv = forall era. SlotNo -> PParams era -> PoolEnv era
PoolEnv SlotNo
slot PParams (ConwayEra StandardCrypto)
pp
    govCertEnv :: ConwayGovCertEnv (ConwayEra StandardCrypto)
govCertEnv = forall era.
PParams era
-> EpochNo
-> StrictMaybe (Committee era)
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
-> ConwayGovCertEnv era
ConwayGovCertEnv PParams (ConwayEra StandardCrypto)
pp EpochNo
ce StrictMaybe (Committee (ConwayEra StandardCrypto))
cc Map
  (GovPurposeId 'CommitteePurpose (ConwayEra StandardCrypto))
  (GovActionState (ConwayEra StandardCrypto))
cp