{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -O0 #-}
#endif

module Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.WellFormed where

import Cardano.Ledger.Api
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.Conway.Rules (GovEnv (..))
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley.LedgerState
import Constrained.API
import Data.Map (Map)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (
  EraSpecLedger (..),
  accountStateSpec,
  aggregateDRep,
  conwayGovStateSpec,
  dstateSpec,
  epochNoSpec,
  epochStateSpec,
  getMarkSnapShot,
  govEnvSpec,
  ledgerStateSpec,
  pstateSpec,
  shelleyGovStateSpec,
  snapShotSpec,
  snapShotsSpec,
  utxoSpecWit,
  utxoStateSpec,
  vstateSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (EraSpecTxOut (..))
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse (
  GenScript (..),
  genWitUniv,
 )
import Test.QuickCheck (Gen)

-- ==============================================================
-- Generators for all the types found in the Ledger State.
-- ==============================================================

ppX :: forall era. EraSpecPParams era => Gen (PParams era)
ppX :: forall era. EraSpecPParams era => Gen (PParams era)
ppX = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(PParams era) forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec

acctX :: Gen ChainAccountState
acctX :: Gen ChainAccountState
acctX = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec

psX :: forall era. GenScript era => Gen (PState era)
psX :: forall era. GenScript era => Gen (PState era)
psX = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
25
  EpochNo
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(PState era) (forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pstateSpec WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))

dsX :: forall era. EraSpecLedger era => Gen (DState era)
dsX :: forall era. EraSpecLedger era => Gen (DState era)
dsX = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
25
  ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
  Map (KeyHash 'StakePool) PoolParams
pools <-
    forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(Map (KeyHash 'StakePool) PoolParams)
      (forall t. (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize (Integer -> Integer -> SizeSpec
rangeSize Integer
8 Integer
8))
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(DState era) (forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
dstateSpec @era WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct) (forall a. HasSpec a => a -> Term a
lit Map (KeyHash 'StakePool) PoolParams
pools))

vsX :: forall era. GenScript era => Gen (VState era)
vsX :: forall era. GenScript era => Gen (VState era)
vsX = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
25
  EpochNo
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
  Map (Credential 'DRepRole) (Set (Credential 'Staking))
delegatees <-
    Map (Credential 'Staking) DRep
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
aggregateDRep
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec -- ensures that each credential delegates to exactly one DRep
        @(Map (Credential 'Staking) DRep)
        forall a. Specification a
TrueSpec
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(VState era) (forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Specification (VState era)
vstateSpec WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch) (forall a. HasSpec a => a -> Term a
lit Map (Credential 'DRepRole) (Set (Credential 'Staking))
delegatees))

csX :: forall era. EraSpecLedger era => Gen (CertState era)
csX :: forall era. EraSpecLedger era => Gen (CertState era)
csX = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
25
  ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
  EpochNo
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(CertState era)
    (forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState era)
certStateSpec WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct) (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))

utxoX :: forall era. EraSpecLedger era => Gen (UTxO era)
utxoX :: forall era. EraSpecLedger era => Gen (UTxO era)
utxoX = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
  Map (Credential 'Staking) (KeyHash 'StakePool)
cs <-
    forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec
      @(Map (Credential 'Staking) (KeyHash 'StakePool))
      (forall t. (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize (Integer -> Integer -> SizeSpec
rangeSize Integer
30 Integer
30))
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(UTxO era) (forall era.
EraSpecTxOut era =>
WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era)
utxoSpecWit @era WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit Map (Credential 'Staking) (KeyHash 'StakePool)
cs))

utxostateX ::
  forall era.
  ( EraSpecLedger era
  , HasSpec (InstantStake era)
  ) =>
  PParams era ->
  Gen (UTxOState era)
utxostateX :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (UTxOState era)
utxostateX PParams era
pp = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
  CertState era
certstate <- forall era. EraSpecLedger era => Gen (CertState era)
csX @era
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(UTxOState era) (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec PParams era
pp WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit CertState era
certstate))

govenvX :: PParams ConwayEra -> Gen (GovEnv ConwayEra)
govenvX :: PParams ConwayEra -> Gen (GovEnv ConwayEra)
govenvX PParams ConwayEra
pp = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(GovEnv ConwayEra) (PParams ConwayEra -> Specification (GovEnv ConwayEra)
govEnvSpec PParams ConwayEra
pp)

conwaygovX :: PParams ConwayEra -> Gen (ConwayGovState ConwayEra)
conwaygovX :: PParams ConwayEra -> Gen (ConwayGovState ConwayEra)
conwaygovX PParams ConwayEra
pp = do
  GovEnv ConwayEra
env <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(GovEnv ConwayEra) (PParams ConwayEra -> Specification (GovEnv ConwayEra)
govEnvSpec PParams ConwayEra
pp)
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(ConwayGovState ConwayEra) (EraSpecLedger ConwayEra =>
PParams ConwayEra
-> GovEnv ConwayEra -> Specification (ConwayGovState ConwayEra)
conwayGovStateSpec PParams ConwayEra
pp GovEnv ConwayEra
env)

lsX ::
  forall era.
  ( EraSpecLedger era
  , HasSpec (InstantStake era)
  ) =>
  PParams era ->
  Gen (LedgerState era)
lsX :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (LedgerState era)
lsX PParams era
pp = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
  ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
  EpochNo
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(LedgerState era) (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct) (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))

esX ::
  forall era.
  (EraSpecLedger era, HasSpec (InstantStake era)) =>
  PParams era ->
  Gen (EpochState era)
esX :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (EpochState era)
esX PParams era
pp = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
  EpochNo
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(EpochState era) (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era -> Term EpochNo -> Specification (EpochState era)
epochStateSpec PParams era
pp WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))

nesX ::
  forall era.
  (EraSpecLedger era, HasSpec (InstantStake era)) =>
  PParams era ->
  Gen (NewEpochState era)
nesX :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (NewEpochState era)
nesX PParams era
pp = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(NewEpochState era) (forall era.
EraSpecLedger era =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpec PParams era
pp WitUniv era
univ)

snapX :: Gen SnapShot
snapX :: Gen SnapShot
snapX = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @SnapShot Specification SnapShot
snapShotSpec

snapsX ::
  forall era.
  ( EraSpecLedger era
  , HasSpec (InstantStake era)
  ) =>
  PParams era ->
  Gen SnapShots
snapsX :: forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen SnapShots
snapsX PParams era
pp = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
  ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
  EpochNo
epoch <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @EpochNo Specification EpochNo
epochNoSpec
  LedgerState era
ls <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(LedgerState era) (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct) (forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @SnapShots (Term SnapShot -> Specification SnapShots
snapShotsSpec (forall a. HasSpec a => a -> Term a
lit (forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot LedgerState era
ls)))

instanRewX :: forall era. EraSpecTxOut era => Gen InstantaneousRewards
instanRewX :: forall era. EraSpecTxOut era => Gen InstantaneousRewards
instanRewX = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
  ChainAccountState
acct <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @ChainAccountState Specification ChainAccountState
accountStateSpec
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @InstantaneousRewards
    (forall era.
EraSpecTxOut era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec @era WitUniv era
univ (forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct))

-- ==============================================================
-- The WellFormed class
-- ==============================================================

class
  ( EraSpecPParams era
  , HasSpec (InstantStake era)
  , HasSpec t
  ) =>
  WellFormed t era
  where
  -- \| Well formed with PParams as input
  wffWithPP :: PParams era -> Gen t
  wffWithPP PParams era
_ = forall t era. WellFormed t era => Gen t
wff @t @era

  -- \| Generate a constrained PParams if one is needed
  wff :: Gen t
  wff = do
    PParams era
pp <- forall era. EraSpecPParams era => Gen (PParams era)
ppX @era
    forall t era. WellFormed t era => PParams era -> Gen t
wffWithPP PParams era
pp

-- ==============================================================
-- The WellFormed instances
-- ==============================================================

instance (EraSpecPParams era, HasSpec (InstantStake era)) => WellFormed (PParams era) era where
  wff :: Gen (PParams era)
wff = forall era. EraSpecPParams era => Gen (PParams era)
ppX @era
  wffWithPP :: PParams era -> Gen (PParams era)
wffWithPP = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance (EraSpecPParams era, HasSpec (InstantStake era)) => WellFormed ChainAccountState era where
  wff :: Gen ChainAccountState
wff = Gen ChainAccountState
acctX
  wffWithPP :: PParams era -> Gen ChainAccountState
wffWithPP PParams era
_ = Gen ChainAccountState
acctX

instance
  (GenScript era, HasSpec (InstantStake era), EraSpecPParams era) =>
  WellFormed (PState era) era
  where
  wff :: Gen (PState era)
wff = forall era. GenScript era => Gen (PState era)
psX
  wffWithPP :: PParams era -> Gen (PState era)
wffWithPP PParams era
_ = forall era. GenScript era => Gen (PState era)
psX

instance
  (EraSpecPParams era, HasSpec (InstantStake era), EraSpecLedger era) =>
  WellFormed (DState era) era
  where
  wff :: Gen (DState era)
wff = forall era. EraSpecLedger era => Gen (DState era)
dsX
  wffWithPP :: PParams era -> Gen (DState era)
wffWithPP PParams era
_ = forall era. EraSpecLedger era => Gen (DState era)
dsX

instance
  (GenScript era, HasSpec (InstantStake era), EraSpecPParams era) =>
  WellFormed (VState era) era
  where
  wff :: Gen (VState era)
wff = forall era. GenScript era => Gen (VState era)
vsX
  wffWithPP :: PParams era -> Gen (VState era)
wffWithPP PParams era
_ = forall era. GenScript era => Gen (VState era)
vsX

instance
  ( EraSpecPParams era
  , EraSpecLedger era
  , HasSpec (InstantStake era)
  , CertState era ~ ShelleyCertState era
  ) =>
  WellFormed (ShelleyCertState era) era
  where
  wff :: Gen (ShelleyCertState era)
wff = forall era. EraSpecLedger era => Gen (CertState era)
csX

instance
  ( EraSpecPParams era
  , EraSpecLedger era
  , HasSpec (InstantStake era)
  , IsNormalType (CertState era)
  ) =>
  WellFormed (UTxO era) era
  where
  wff :: Gen (UTxO era)
wff = forall era. EraSpecLedger era => Gen (UTxO era)
utxoX

instance
  ( EraSpecPParams era
  , EraSpecLedger era
  , IsNormalType (CertState era)
  , HasSpec (InstantStake era)
  ) =>
  WellFormed (UTxOState era) era
  where
  wffWithPP :: PParams era -> Gen (UTxOState era)
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (UTxOState era)
utxostateX

instance WellFormed (GovEnv ConwayEra) ConwayEra where
  wffWithPP :: PParams ConwayEra -> Gen (GovEnv ConwayEra)
wffWithPP = PParams ConwayEra -> Gen (GovEnv ConwayEra)
govenvX

instance WellFormed (ConwayGovState ConwayEra) ConwayEra where
  wffWithPP :: PParams ConwayEra -> Gen (ConwayGovState ConwayEra)
wffWithPP = PParams ConwayEra -> Gen (ConwayGovState ConwayEra)
conwaygovX

instance
  ( EraSpecPParams era
  , EraSpecLedger era
  , HasSpec (InstantStake era)
  , IsNormalType (CertState era)
  ) =>
  WellFormed (ShelleyGovState era) era
  where
  wffWithPP :: PParams era -> Gen (ShelleyGovState era)
wffWithPP PParams era
pp = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(ShelleyGovState era) (forall era.
EraSpecLedger era =>
PParams era -> Specification (ShelleyGovState era)
shelleyGovStateSpec PParams era
pp)

instance
  ( EraSpecPParams era
  , HasSpec (InstantStake era)
  , EraSpecLedger era
  , IsNormalType (CertState era)
  ) =>
  WellFormed (LedgerState era) era
  where
  wffWithPP :: PParams era -> Gen (LedgerState era)
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (LedgerState era)
lsX

instance
  ( EraSpecPParams era
  , EraSpecLedger era
  , HasSpec (InstantStake era)
  , IsNormalType (CertState era)
  ) =>
  WellFormed (EpochState era) era
  where
  wffWithPP :: PParams era -> Gen (EpochState era)
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (EpochState era)
esX

instance
  (EraSpecPParams era, HasSpec (InstantStake era), EraSpecLedger era) =>
  WellFormed (NewEpochState era) era
  where
  wffWithPP :: PParams era -> Gen (NewEpochState era)
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen (NewEpochState era)
nesX

instance (EraSpecPParams era, HasSpec (InstantStake era)) => WellFormed SnapShot era where
  wff :: Gen SnapShot
wff = Gen SnapShot
snapX

instance
  ( EraSpecPParams era
  , EraSpecLedger era
  , HasSpec (InstantStake era)
  , IsNormalType (CertState era)
  ) =>
  WellFormed SnapShots era
  where
  wffWithPP :: PParams era -> Gen SnapShots
wffWithPP = forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era -> Gen SnapShots
snapsX @era

instance
  (EraSpecPParams era, HasSpec (InstantStake era), EraSpecTxOut era) =>
  WellFormed InstantaneousRewards era
  where
  wff :: Gen InstantaneousRewards
wff = forall era. EraSpecTxOut era => Gen InstantaneousRewards
instanRewX @era