{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

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

import Cardano.Ledger.Api
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Core (PParamsHKD)
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  StashedAVVMAddresses,
  UTxOState (..),
 )
import Constrained.API
import Data.Functor.Identity (Identity)
import Data.Kind (Type)
import Data.Map (Map)
import Data.TreeDiff
import Data.Typeable
import Test.Cardano.Ledger.Constrained.Conway.Cert (
  testConwayCert,
  testGenesisCert,
  testShelleyCert,
 )
import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic (prettyE)
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.WellFormed
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (irewardSpec)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
import Test.Hspec
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck (
  Gen,
  Property,
  counterexample,
  property,
  withMaxSuccess,
 )

-- ====================================================================================
-- Some Specifications are constrained by types (say 'x') that do not appear in the type being
-- specified. We use the strategy of passing (Term x) as inputs to those specifcations.
-- For example, the AccountState must have sufficient capacity to support the InstantaneousRewards
-- So we pass a (Term AccountState) as input to 'instantaneousRewardsSpec' which then
-- constrains both the AccountState Term and the 'instantaneousRewardsSpec' so that they are consistent.
-- In order to create tests, we need specifications that are fully applied, so we write combinators
-- to lift (Term a -> Spec b) functions to (Specification a -> Gen(Specification b))
-- The idea is to combine several Specifications to get a Gen(composed specifations)
-- For example (dstateSpec @Shelley !$! accountStateSpec !*! poolMapSpec)
-- is a (Gen (Specification (DState Shelley)))
-- If a Specification takes an actual PParams (not a (Term PParams)), like
-- lederstateSpec, we can combine it like this using the Functor <$>, rather than our !$!
-- (ledgerStateSpec <$> genConwayFn pparamsSpec !*! accountStateSpec !*! epochNoSpec)
-- ====================================================================================

-- GenFromSpec fixed at
genConwayFn :: (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn :: forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn = forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec

-- Analagous to <$> except the function to be applied takes a (Term a -> t) instead of (a -> t)
infixr 6 !$!
(!$!) ::
  forall t a.
  HasSpec a =>
  (Term a -> t) -> Specification a -> Gen t
!$! :: forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
(!$!) Term a -> t
bf Specification a
specA = do a
a <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @a Specification a
specA; forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term a -> t
bf (forall a. HasSpec a => a -> Term a
lit a
a))

-- Analagous to <*> except the function to be applied takes a Gen (Term a -> t) instead of F (a -> t)
infixl 4 !*!
(!*!) ::
  forall t a.
  HasSpec a =>
  Gen (Term a -> t) -> Specification a -> Gen t
!*! :: forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
(!*!) Gen (Term a -> t)
gentf Specification a
specA = do a
a <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @a Specification a
specA; Term a -> t
f <- Gen (Term a -> t)
gentf; forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term a -> t
f (forall a. HasSpec a => a -> Term a
lit a
a))

poolMapSpec ::
  Specification (Map (KeyHash 'StakePool) PoolParams)
poolMapSpec :: Specification (Map (KeyHash 'StakePool) PoolParams)
poolMapSpec = forall t. (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize (Integer -> Integer -> SizeSpec
rangeSize Integer
8 Integer
8)

delegationsSpec ::
  Specification
    (Map (Credential 'Staking) (KeyHash 'StakePool))
delegationsSpec :: Specification (Map (Credential 'Staking) (KeyHash 'StakePool))
delegationsSpec = (forall t. (HasSpec t, Sized t) => SizeSpec -> Specification t
hasSize (Integer -> Integer -> SizeSpec
rangeSize Integer
8 Integer
12))

-- ====================================================================
-- HSpec tests
-- ===================================================================

soundSpec ::
  forall t. (HasSpec t, ToExpr t) => Gen (Specification t) -> Gen Property
soundSpec :: forall t.
(HasSpec t, ToExpr t) =>
Gen (Specification t) -> Gen Property
soundSpec Gen (Specification t)
specGen = do
  Specification t
spect <- Gen (Specification t)
specGen
  t
x <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn @t Specification t
spect
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
      forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => a -> String
show (Doc
"Does not meet spec\n" forall a. Semigroup a => a -> a -> a
<> forall x. ToExpr x => x -> Doc
prettyE t
x)) (forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec t
x Specification t
spect)

soundSpecWith ::
  forall t.
  (HasSpec t, ToExpr t) =>
  Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith :: forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith Int
n Gen (Specification t)
specx = forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it (forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @t))) forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ (forall t.
(HasSpec t, ToExpr t) =>
Gen (Specification t) -> Gen Property
soundSpec @t Gen (Specification t)
specx)

-- | A bunch of soundness tests on different LederTypes, all in the same Era.
--   The idea is to run this suite on every era.
specSuite ::
  forall (era :: Type).
  ( EraSpecLedger era
  , ToExpr (GovState era)
  , ToExpr (TxOut era)
  , ToExpr (InstantStake era)
  , ToExpr (PParamsHKD Identity era)
  , ToExpr (StashedAVVMAddresses era)
  , HasSpec (InstantStake era)
  , CertState era ~ ShelleyCertState era
  ) =>
  Int -> Spec
specSuite :: forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite Int
n = do
  let universe :: Gen (WitUniv era)
universe = forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(PState era) (Int
5 forall a. Num a => a -> a -> a
* Int
n) (forall era.
Era era =>
WitUniv era -> Term EpochNo -> Specification (PState era)
pstateSpec @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (WitUniv era)
universe forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification EpochNo
epochNoSpec)

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(DState era)
    (Int
5 forall a. Num a => a -> a -> a
* Int
n)
    forall a b. (a -> b) -> a -> b
$ do
      WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
      forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term (Map (KeyHash 'StakePool) PoolParams)
-> Specification (DState era)
dstateSpec @era WitUniv era
univ forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
!$! Specification ChainAccountState
accountStateSpec forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification (Map (KeyHash 'StakePool) PoolParams)
poolMapSpec

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(VState era)
    (Int
10 forall a. Num a => a -> a -> a
* Int
n)
    forall a b. (a -> b) -> a -> b
$ do
      WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
25
      ( forall era.
Era era =>
WitUniv era
-> Term EpochNo
-> Term (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
-> Specification (VState era)
vstateSpec @era WitUniv era
univ
          forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
!$! Specification EpochNo
epochNoSpec
          forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! (forall era.
WitUniv era
-> Specification
     (Map (Credential 'DRepRole) (Set (Credential 'Staking)))
goodDrep @era WitUniv era
univ)
        )

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(CertState era)
    (Int
5 forall a. Num a => a -> a -> a
* Int
n)
    forall a b. (a -> b) -> a -> b
$ do
      WitUniv era
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50
      (forall era.
EraSpecLedger era =>
WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (CertState era)
certStateSpec @era WitUniv era
univ {- (lit drepRoleCredSet) -} forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
!$! Specification ChainAccountState
accountStateSpec forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification EpochNo
epochNoSpec)

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(UTxO era) (Int
5 forall a. Num a => a -> a -> a
* Int
n) (forall era.
EraSpecTxOut era =>
WitUniv era
-> Term (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Specification (UTxO era)
utxoSpecWit @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (WitUniv era)
universe forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification (Map (Credential 'Staking) (KeyHash 'StakePool))
delegationsSpec)

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(UTxOState era) (Int
2 forall a. Num a => a -> a -> a
* Int
n) (forall era.
(WellFormed (CertState era) era, EraSpecLedger era) =>
Gen (Specification (UTxOState era))
utxoStateGen @era)

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(GovState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    (forall era.
EraSpecLedger era =>
PParams era -> Specification (GovState era)
govStateSpec @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec)

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(LedgerState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    ( forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term ChainAccountState
-> Term EpochNo
-> Specification (LedgerState era)
ledgerStateSpec
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
100 forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification ChainAccountState
accountStateSpec forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification EpochNo
epochNoSpec
    )
  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(EpochState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    (forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era -> Term EpochNo -> Specification (EpochState era)
epochStateSpec @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50 forall t a.
HasSpec a =>
Gen (Term a -> t) -> Specification a -> Gen t
!*! Specification EpochNo
epochNoSpec)
  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(NewEpochState era)
    (Int
2 forall a. Num a => a -> a -> a
* Int
n)
    (forall era.
EraSpecLedger era =>
PParams era -> WitUniv era -> Specification (NewEpochState era)
newEpochStateSpec @era forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
50)

spec :: Spec
spec :: Spec
spec = do
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify GenesisCert" (forall era.
(AtMostEra BabbageEra era, EraSpecDeleg era, EraSpecPParams era,
 GenScript era) =>
Gen Property
testGenesisCert @ShelleyEra)
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify ShelleyCert" (forall era.
(Era era, AtMostEra BabbageEra era, EraSpecPParams era,
 EraSpecDeleg era, GenScript era, EraCertState era) =>
Gen Property
testShelleyCert @BabbageEra)
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify ConwayCert" Gen Property
testConwayCert
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Soundness of WellFormed types from the Cardano Ledger: " forall a b. (a -> b) -> a -> b
$ do
    forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(ProtVer, ProtVer) Int
100 (forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification (ProtVer, ProtVer)
protVersCanfollow)
    forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @InstantaneousRewards
      Int
20
      (forall era.
EraSpecTxOut era =>
WitUniv era
-> Term ChainAccountState -> Specification InstantaneousRewards
irewardSpec @ShelleyEra (forall era. EraUniverse era => Int -> WitUniv era
eraWitUniv @ShelleyEra Int
50) forall t a. HasSpec a => (Term a -> t) -> Specification a -> Gen t
!$! Specification ChainAccountState
accountStateSpec)
    forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @SnapShots
      Int
10
      (Term SnapShot -> Specification SnapShots
snapShotsSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. HasSpec a => a -> Term a
lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
(EraCertState era, EraStake era) =>
LedgerState era -> SnapShot
getMarkSnapShot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t era. WellFormed t era => Gen t
wff @(LedgerState ConwayEra) @ConwayEra))
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @ShelleyEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @AllegraEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @MaryEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @AlonzoEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @BabbageEra Int
10
  forall era.
(EraSpecLedger era, ToExpr (GovState era), ToExpr (TxOut era),
 ToExpr (InstantStake era), ToExpr (PParamsHKD Identity era),
 ToExpr (StashedAVVMAddresses era), HasSpec (InstantStake era),
 CertState era ~ ShelleyCertState era) =>
Int -> Spec
specSuite @ShelleyEra Int
10

utxoStateGen ::
  forall era.
  ( WellFormed (CertState era) era
  , EraSpecLedger era
  ) =>
  Gen (Specification (UTxOState era))
utxoStateGen :: forall era.
(WellFormed (CertState era) era, EraSpecLedger era) =>
Gen (Specification (UTxOState era))
utxoStateGen =
  forall era.
(EraSpecLedger era, HasSpec (InstantStake era)) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec @era
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn @(PParams era) forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
25
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. HasSpec a => a -> Term a
lit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t era. WellFormed t era => Gen t
wff @(CertState era) @era)