{-# 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 #-}

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.Shelley.LedgerState
import Constrained.API
import Data.Map (Map)
import Test.Cardano.Ledger.Constrained.Conway.Deleg (witnessedKeyHashStakePoolMapSpec)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (
  accountStateSpec,
  conwayCertStateSpec,
  conwayDStateSpec,
  conwayGovStateSpec,
  epochNoSpec,
  epochStateSpec,
  genCertContext,
  getMarkSnapShot,
  govEnvSpec,
  ledgerStateSpec,
  newEpochStateSpec,
  pStateSpec,
  snapShotSpec,
  snapShotsSpec,
  utxoSpecWit,
  utxoStateSpec,
  vStateSpec,
  whoDelegatesSpec,
 )
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) Specification (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 @era 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) (WitUniv era -> Term EpochNo -> Specification (PState era)
forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pStateSpec WitUniv era
univ (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))

dsX :: forall era. era ~ ConwayEra => Gen (DState era)
dsX :: forall era. (era ~ ConwayEra) => Gen (DState era)
dsX = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
100
  CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
  Map (KeyHash 'StakePool) StakePoolState
khppMap <- Specification (Map (KeyHash 'StakePool) StakePoolState)
-> Gen (Map (KeyHash 'StakePool) StakePoolState)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv era
-> Specification (Map (KeyHash 'StakePool) StakePoolState)
forall era.
Era era =>
WitUniv era
-> Specification (Map (KeyHash 'StakePool) StakePoolState)
witnessedKeyHashStakePoolMapSpec WitUniv era
univ)
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(DState era) (WitUniv era
-> CertContext
-> Term (Map (KeyHash 'StakePool) StakePoolState)
-> Specification (DState era)
forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertContext
-> Term (Map (KeyHash 'StakePool) StakePoolState)
-> Specification (DState era)
conwayDStateSpec WitUniv era
univ CertContext
context (Map (KeyHash 'StakePool) StakePoolState
-> Term (Map (KeyHash 'StakePool) StakePoolState)
forall a. HasSpec a => a -> Term a
lit Map (KeyHash 'StakePool) StakePoolState
khppMap))

conwayDStateGen ::
  forall era. era ~ ConwayEra => Gen (DState era)
conwayDStateGen :: forall era. (era ~ ConwayEra) => Gen (DState era)
conwayDStateGen = forall era. (era ~ ConwayEra) => Gen (DState era)
dsX @ConwayEra

vsX :: forall era. (GenScript era, era ~ ConwayEra) => Gen (VState era)
vsX :: forall era. (GenScript era, era ~ ConwayEra) => Gen (VState era)
vsX = do
  WitUniv era
univ <- Int -> Gen (WitUniv era)
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))
whodelegates <- Specification
  (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Gen (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
forall era.
Era era =>
WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
whoDelegatesSpec WitUniv era
univ)
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(VState era) (WitUniv era
-> Term EpochNo
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (VState era)
forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Specification (VState era)
vStateSpec WitUniv era
univ (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epoch) Map (Credential 'DRepRole) (Set (Credential 'Staking))
whodelegates)

csX :: forall era. era ~ ConwayEra => Gen (CertState era)
csX :: forall era. (era ~ ConwayEra) => Gen (CertState era)
csX = do
  WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
300
  CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
  Specification (ConwayCertState ConwayEra)
-> Gen (ConwayCertState ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv ConwayEra
-> CertContext
-> Term EpochNo
-> Specification (ConwayCertState ConwayEra)
conwayCertStateSpec WitUniv era
WitUniv ConwayEra
univ CertContext
context (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit (Word64 -> EpochNo
EpochNo Word64
10)))

utxoX :: forall era. era ~ ConwayEra => Gen (UTxO era)
utxoX :: forall era. (era ~ ConwayEra) => 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))
      (SizeSpec
-> Specification (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 (Map (Credential 'Staking) (KeyHash 'StakePool)
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
forall a. HasSpec a => a -> Term a
lit Map (Credential 'Staking) (KeyHash 'StakePool)
cs))

utxostateX ::
  forall era.
  (era ~ ConwayEra, HasSpec (InstantStake era)) =>
  PParams era ->
  Gen (UTxOState era)
utxostateX :: forall era.
(era ~ ConwayEra, 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
  ConwayCertState ConwayEra
certstate <- forall era. (era ~ ConwayEra) => Gen (CertState era)
csX @era
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(UTxOState era) (PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec PParams era
pp WitUniv era
univ (ConwayCertState ConwayEra -> Term (ConwayCertState ConwayEra)
forall a. HasSpec a => a -> Term a
lit ConwayCertState ConwayEra
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) (PParams ConwayEra
-> GovEnv ConwayEra -> Specification (ConwayGovState ConwayEra)
conwayGovStateSpec PParams ConwayEra
pp GovEnv ConwayEra
env)

lsX ::
  forall era. (era ~ ConwayEra, HasSpec (InstantStake era)) => PParams era -> Gen (LedgerState era)
lsX :: forall era.
(era ~ ConwayEra, 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
200
  CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
  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) (PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (LedgerState era)
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ CertContext
context (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))

esX ::
  forall era.
  (era ~ ConwayEra, HasSpec (InstantStake era)) =>
  PParams era ->
  Gen (EpochState era)
esX :: forall era.
(era ~ ConwayEra, 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
200
  CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
  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) (PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (EpochState era)
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (EpochState era)
epochStateSpec PParams era
pp WitUniv era
univ CertContext
context (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epoch))

nesX ::
  forall era.
  (era ~ ConwayEra, HasSpec (InstantStake era)) =>
  PParams era ->
  Gen (NewEpochState era)
nesX :: forall era.
(era ~ ConwayEra, 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
200
  CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
  forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @(NewEpochState era) (PParams era
-> WitUniv era -> CertContext -> Specification (NewEpochState era)
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era -> CertContext -> Specification (NewEpochState era)
newEpochStateSpec PParams era
pp WitUniv era
univ CertContext
context)

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

snapsX ::
  forall era.
  ( HasSpec (InstantStake era)
  , era ~ ConwayEra
  ) =>
  PParams era ->
  Gen SnapShots
snapsX :: forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
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
200
  CertContext
context <- forall era. Era era => WitUniv era -> Gen CertContext
genCertContext @era WitUniv era
univ
  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) (PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (LedgerState era)
forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> CertContext
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec PParams era
pp WitUniv era
univ CertContext
context (EpochNo -> Term EpochNo
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 (SnapShot -> Term SnapShot
forall a. HasSpec a => a -> Term a
lit (LedgerState era -> SnapShot
forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot LedgerState era
ls)))

instanRewX :: forall era. (era ~ ConwayEra, EraSpecTxOut era) => Gen InstantaneousRewards
instanRewX :: forall era.
(era ~ ConwayEra, 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 (ChainAccountState -> Term ChainAccountState
forall a. HasSpec a => a -> Term a
lit ChainAccountState
acct))

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

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

  -- \| Generate a constrained PParams if one is needed
  wff :: Gen t
  wff = do
    pp <- ppX @era
    wffWithPP pp

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

instance (EraSpecPParams era, HasSpec (InstantStake era)) => WellFormed (PParams era) era where
  wff = ppX @era
  wffWithPP = pure

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

instance
  (GenScript era, HasSpec (InstantStake era), EraSpecPParams era) =>
  WellFormed (PState era) era
  where
  wff = psX
  wffWithPP _ = psX

instance WellFormed (DState ConwayEra) ConwayEra where
  wff = conwayDStateGen
  wffWithPP _ = conwayDStateGen

instance
  (GenScript era, HasSpec (InstantStake era), EraSpecPParams era) =>
  WellFormed (VState era) era
  where
  wff = vsX
  wffWithPP _ = vsX

instance
  ( EraSpecPParams era
  , HasSpec (InstantStake era)
  , CertState era ~ ShelleyCertState era
  ) =>
  WellFormed (ShelleyCertState era) era
  where
  wff = csX @era

instance
  ( EraSpecPParams era
  , HasSpec (InstantStake era)
  , CertState era ~ ConwayCertState era
  ) =>
  WellFormed (ConwayCertState era) era
  where
  wff = csX @era

instance
  ( EraSpecPParams era
  , HasSpec (InstantStake era)
  , IsNormalType (CertState era)
  ) =>
  WellFormed (UTxO era) era
  where
  wff = utxoX

instance
  ( EraSpecPParams era
  , IsNormalType (CertState era)
  , HasSpec (InstantStake era)
  ) =>
  WellFormed (UTxOState era) era
  where
  wffWithPP = utxostateX

instance WellFormed (GovEnv ConwayEra) ConwayEra where
  wffWithPP = govenvX

instance WellFormed (ConwayGovState ConwayEra) ConwayEra where
  wffWithPP = conwaygovX

instance
  ( EraSpecPParams era
  , HasSpec (InstantStake era)
  , IsNormalType (CertState era)
  ) =>
  WellFormed (ShelleyGovState era) era
  where
  wffWithPP pp = genFromSpec @(ShelleyGovState era) (shelleyGovStateSpec pp)

instance
  ( EraSpecPParams era
  , HasSpec (InstantStake era)
  , IsNormalType (CertState era)
  ) =>
  WellFormed (LedgerState era) era
  where
  wffWithPP = lsX

instance
  ( EraSpecPParams era
  , HasSpec (InstantStake era)
  , IsNormalType (CertState era)
  ) =>
  WellFormed (EpochState era) era
  where
  wffWithPP = esX

instance
  (EraSpecPParams era, HasSpec (InstantStake era)) =>
  WellFormed (NewEpochState era) era
  where
  wffWithPP = nesX

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

instance
  ( EraSpecPParams era
  , HasSpec (InstantStake era)
  , IsNormalType (CertState era)
  ) =>
  WellFormed SnapShots era
  where
  wffWithPP = snapsX @era

instance
  (EraSpecPParams era, HasSpec (InstantStake era), EraSpecTxOut era) =>
  WellFormed InstantaneousRewards era
  where
  wff = instanRewX @era
-}