{-# 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.Credential (Credential)
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  UTxOState (..),
 )
import Constrained.API
import Data.Kind (Type)
import Data.Map (Map)
import Data.TreeDiff
import Data.Typeable
import Test.Cardano.Ledger.Constrained.Conway.Cert (
  testConwayCert,
  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.WitnessUniverse
import Test.Cardano.Ledger.Conway.Era
import Test.Hspec hiding (context)
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 = Specification a -> Gen a
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 <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @a Specification a
specA; pure (bf (lit 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 <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec @a Specification a
specA; f <- gentf; pure (f (lit a))

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

poolRegSpec ::
  forall era. Era era => WitUniv era -> Specification (Map (KeyHash StakePool) StakePoolState)
poolRegSpec :: forall era.
Era era =>
WitUniv era
-> Specification (Map (KeyHash StakePool) StakePoolState)
poolRegSpec WitUniv era
univ = (Term (Map (KeyHash StakePool) StakePoolState) -> [Pred])
-> Specification (Map (KeyHash StakePool) StakePoolState)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map (KeyHash StakePool) StakePoolState) -> [Pred])
 -> Specification (Map (KeyHash StakePool) StakePoolState))
-> (Term (Map (KeyHash StakePool) StakePoolState) -> [Pred])
-> Specification (Map (KeyHash StakePool) StakePoolState)
forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash StakePool) StakePoolState)
poolRegMap ->
  [ WitUniv era -> Term (Set (KeyHash StakePool)) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash StakePool) StakePoolState)
-> Term (Set (KeyHash StakePool))
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_ Term (Map (KeyHash StakePool) StakePoolState)
poolRegMap)
  , WitUniv era -> Term [StakePoolState] -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (Term (Map (KeyHash StakePool) StakePoolState)
-> Term [StakePoolState]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash StakePool) StakePoolState)
poolRegMap)
  , Term (Map (KeyHash StakePool) StakePoolState)
-> Specification (Map (KeyHash StakePool) StakePoolState) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (KeyHash StakePool) StakePoolState)
poolRegMap (SizeSpec -> Specification (Map (KeyHash StakePool) StakePoolState)
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
  spect <- Gen (Specification t)
specGen
  x <- genConwayFn @t spect
  pure $
    property $
      counterexample (show ("Does not meet spec\n" <> prettyE x)) (conformsToSpec x 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 = String -> Property -> SpecWith (Arg Property)
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it (TypeRep -> String
forall a. Show a => a -> String
show (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))) (Property -> SpecWith (Arg Property))
-> Property -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Gen Property -> Property
forall prop. Testable prop => prop -> Property
property (Gen Property -> Property) -> Gen 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).
  ( era ~ ConwayEra
  , ShelleyEraTest era
  ) =>
  Int -> Spec
specSuite :: forall era. (era ~ ConwayEra, ShelleyEraTest 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 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (PState era)) -> SpecWith (Arg Property))
-> Gen (Specification (PState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
    univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
    pStateSpec @era univ !$! epochNoSpec

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(DState era) (Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (DState era)) -> SpecWith (Arg Property))
-> Gen (Specification (DState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
    univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
    context <- genCertContext @era univ
    poolreg <- genFromSpec (poolRegSpec univ)
    pure (conwayDStateSpec @era univ context (lit poolreg))

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(VState era) (Int
10 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (VState era)) -> SpecWith (Arg Property))
-> Gen (Specification (VState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
    univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
    whodelegates <- genFromSpec (goodDrep @era univ)
    epoch <- genFromSpec epochNoSpec
    pure (vStateSpec @era univ (lit epoch) whodelegates)

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(CertState era) (Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (CertState era)) -> SpecWith (Arg Property))
-> Gen (Specification (CertState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
    univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @era Int
200
    context <- genCertContext @era univ
    epn <- genFromSpec epochNoSpec
    pure (conwayCertStateSpec univ context (lit epn))

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(UTxO era) (Int
5 Int -> Int -> Int
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 (WitUniv era
 -> Term (Map (Credential Staking) (KeyHash StakePool))
 -> Specification (UTxO era))
-> Gen (WitUniv era)
-> Gen
     (Term (Map (Credential Staking) (KeyHash StakePool))
      -> Specification (UTxO era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (WitUniv era)
universe Gen
  (Term (Map (Credential Staking) (KeyHash StakePool))
   -> Specification (UTxO era))
-> Specification (Map (Credential Staking) (KeyHash StakePool))
-> Gen (Specification (UTxO era))
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) Gen (Specification (UTxOState era))
Gen (Specification (UTxOState ConwayEra))
utxoStateGen

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(GovState era) (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (GovState era)) -> SpecWith (Arg Property))
-> Gen (Specification (GovState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
    pp <- Specification (PParams ConwayEra) -> Gen (PParams ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification (PParams ConwayEra)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
    pure (conwayGovStateSpec pp (testGovEnv pp))

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(LedgerState era) (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (LedgerState era)) -> SpecWith (Arg Property))
-> Gen (Specification (LedgerState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
    pp <- Specification (PParams era) -> Gen (PParams era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
    univ <- genWitUniv @era 200
    context <- genCertContext @era univ
    epn <- genFromSpec epochNoSpec
    pure (ledgerStateSpec pp univ context (lit epn))

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(EpochState era) (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (EpochState era)) -> SpecWith (Arg Property))
-> Gen (Specification (EpochState era)) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
    pp <- Specification (PParams era) -> Gen (PParams era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
    univ <- genWitUniv @era 200
    context <- genCertContext @era univ
    epn <- genFromSpec epochNoSpec
    pure (epochStateSpec @era pp univ context (lit epn))

  forall t.
(HasSpec t, ToExpr t) =>
Int -> Gen (Specification t) -> SpecWith (Arg Property)
soundSpecWith @(NewEpochState era) (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) (Gen (Specification (NewEpochState era))
 -> SpecWith (Arg Property))
-> Gen (Specification (NewEpochState era))
-> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
    pp <- Specification (PParams era) -> Gen (PParams era)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn Specification (PParams era)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
    univ <- genWitUniv @era 200
    context <- genCertContext @era univ
    pure (newEpochStateSpec @era pp univ context)

spec :: Spec
spec :: Spec
spec = do
  String -> Gen Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify ShelleyCert" (forall era.
(Era era, AtMostEra "Babbage" era, EraSpecPParams era,
 EraSpecDeleg era, GenScript era, EraCertState era) =>
Gen Property
testShelleyCert @BabbageEra)
  String -> Gen Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classify ConwayCert" Gen Property
testConwayCert
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Soundness of WellFormed types from the Cardano Ledger: " (Spec -> Spec) -> Spec -> Spec
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 (Specification (ProtVer, ProtVer)
-> Gen (Specification (ProtVer, ProtVer))
forall a. a -> Gen a
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 @SnapShots Int
10 (Gen (Specification SnapShots) -> SpecWith (Arg Property))
-> Gen (Specification SnapShots) -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
      pp <- Specification (PParams ConwayEra) -> Gen (PParams ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn Specification (PParams ConwayEra)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
      ls <- lsX pp
      pure (snapShotsSpec (lit (getMarkSnapShot ls)))

  forall era. (era ~ ConwayEra, ShelleyEraTest era) => Int -> Spec
specSuite @ConwayEra Int
10

utxoStateGen :: Gen (Specification (UTxOState ConwayEra))
utxoStateGen :: Gen (Specification (UTxOState ConwayEra))
utxoStateGen =
  forall era.
(HasSpec (InstantStake era), era ~ ConwayEra) =>
PParams era
-> WitUniv era
-> Term (CertState era)
-> Specification (UTxOState era)
utxoStateSpec @ConwayEra
    (PParams ConwayEra
 -> WitUniv ConwayEra
 -> TermD Deps (ConwayCertState ConwayEra)
 -> Specification (UTxOState ConwayEra))
-> Gen (PParams ConwayEra)
-> Gen
     (WitUniv ConwayEra
      -> TermD Deps (ConwayCertState ConwayEra)
      -> Specification (UTxOState ConwayEra))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genConwayFn @(PParams ConwayEra) Specification (PParams ConwayEra)
forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
    Gen
  (WitUniv ConwayEra
   -> TermD Deps (ConwayCertState ConwayEra)
   -> Specification (UTxOState ConwayEra))
-> Gen (WitUniv ConwayEra)
-> Gen
     (TermD Deps (ConwayCertState ConwayEra)
      -> Specification (UTxOState ConwayEra))
forall a b. Gen (a -> b) -> Gen a -> Gen b
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 @ConwayEra Int
25
    Gen
  (TermD Deps (ConwayCertState ConwayEra)
   -> Specification (UTxOState ConwayEra))
-> Gen (TermD Deps (ConwayCertState ConwayEra))
-> Gen (Specification (UTxOState ConwayEra))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ConwayCertState ConwayEra -> TermD Deps (ConwayCertState ConwayEra)
forall a. HasSpec a => a -> Term a
lit (ConwayCertState ConwayEra
 -> TermD Deps (ConwayCertState ConwayEra))
-> Gen (ConwayCertState ConwayEra)
-> Gen (TermD Deps (ConwayCertState ConwayEra))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. (era ~ ConwayEra) => Gen (CertState era)
csX @ConwayEra)