{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.STS where

import Cardano.Ledger.Api
import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Shelley.Rules hiding (epochNo, slotNo)
import Control.Monad.Reader
import Control.State.Transition.Extended

import Constrained hiding (forAll)

import Test.Cardano.Ledger.Constrained.Conway.Cert
import Test.Cardano.Ledger.Constrained.Conway.Deleg
import Test.Cardano.Ledger.Constrained.Conway.Epoch
import Test.Cardano.Ledger.Constrained.Conway.Gov
import Test.Cardano.Ledger.Constrained.Conway.GovCert
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.Pool

import Test.Cardano.Ledger.Generic.PrettyCore
import Test.Cardano.Ledger.Shelley.Utils

import Cardano.Ledger.Coin (Coin)
import Cardano.Ledger.Credential (Credential)
import Constrained.Base (conformsToSpecE)
import qualified Data.List.NonEmpty as NE
import Data.Map (Map)
import Data.Set (Set)
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse (WitUniv, genWitUniv, witness)
import Test.QuickCheck hiding (witness)
import Test.Tasty
import Test.Tasty.QuickCheck hiding (witness)

-- ==================================================

-- | Several tests need some semi-randomcontext, this supplies that context
genContext ::
  Gen
    ( WitUniv ConwayEra
    , Set (Credential 'DRepRole)
    , Map RewardAccount Coin
    )
genContext :: Gen
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
   Map RewardAccount Coin)
genContext = do
  WitUniv ConwayEra
univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
200
  Set (Credential 'DRepRole)
delegatees <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
WitUniv era -> Specification fn (Set (Credential 'DRepRole))
delegateeSpec WitUniv ConwayEra
univ)
  Map RewardAccount Coin
wdrls <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn (forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term ConwayFn (Map RewardAccount Coin)
x -> (forall (fn :: Univ) era t.
Witnessed fn era t =>
WitUniv era -> Term fn t -> Pred fn
witness WitUniv ConwayEra
univ Term ConwayFn (Map RewardAccount Coin)
x))
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (WitUniv ConwayEra
univ, Set (Credential 'DRepRole)
delegatees, Map RewardAccount Coin
wdrls)

------------------------------------------------------------------------
-- Properties
------------------------------------------------------------------------

type GenShrink a = (Gen a, a -> [a])

genShrinkFromSpec :: forall fn a. HasSpec fn a => Specification fn a -> GenShrink a
genShrinkFromSpec :: forall (fn :: Univ) a.
HasSpec fn a =>
Specification fn a -> GenShrink a
genShrinkFromSpec Specification fn a
spec = (forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn Specification fn a
spec, forall (fn :: Univ) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec @fn Specification fn a
spec)

stsPropertyV2 ::
  forall r fn era env st sig fail p.
  ( era ~ ConwayEra
  , Environment (EraRule r era) ~ env
  , State (EraRule r era) ~ st
  , Signal (EraRule r era) ~ sig
  , PredicateFailure (EraRule r era) ~ fail
  , STS (EraRule r era)
  , BaseM (EraRule r era) ~ ReaderT Globals Identity
  , PrettyA st
  , PrettyA sig
  , PrettyA env
  , PrettyA fail
  , Testable p
  , HasSpec fn env
  , HasSpec fn st
  , HasSpec fn sig
  ) =>
  Specification fn env ->
  (env -> Specification fn st) ->
  (env -> st -> Specification fn sig) ->
  (env -> st -> sig -> st -> p) ->
  Property
stsPropertyV2 :: forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 Specification fn env
specEnv env -> Specification fn st
specState env -> st -> Specification fn sig
specSig env -> st -> sig -> st -> p
prop =
  forall (r :: Symbol) (fn :: Univ) env st sig fail p.
(Environment (EraRule r ConwayEra) ~ env,
 State (EraRule r ConwayEra) ~ st,
 Signal (EraRule r ConwayEra) ~ sig,
 PredicateFailure (EraRule r ConwayEra) ~ fail,
 STS (EraRule r ConwayEra),
 BaseM (EraRule r ConwayEra) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> Specification fn st)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2' @r Specification fn env
specEnv env -> Specification fn st
specState env -> st -> Specification fn sig
specSig (\env
env st
_ sig
_ -> env -> Specification fn st
specState env
env) env -> st -> sig -> st -> p
prop

stsPropertyV2' ::
  forall r fn env st sig fail p.
  ( Environment (EraRule r ConwayEra) ~ env
  , State (EraRule r ConwayEra) ~ st
  , Signal (EraRule r ConwayEra) ~ sig
  , PredicateFailure (EraRule r ConwayEra) ~ fail
  , STS (EraRule r ConwayEra)
  , BaseM (EraRule r ConwayEra) ~ ReaderT Globals Identity
  , PrettyA st
  , PrettyA sig
  , PrettyA env
  , PrettyA fail
  , Testable p
  , HasSpec fn env
  , HasSpec fn st
  , HasSpec fn sig
  ) =>
  Specification fn env ->
  (env -> Specification fn st) ->
  (env -> st -> Specification fn sig) ->
  -- This allows you to write a separate spec for the state after the transition
  -- and thus e.g. loosening requirements set only for the sake of generation
  (env -> st -> sig -> Specification fn st) ->
  (env -> st -> sig -> st -> p) ->
  Property
stsPropertyV2' :: forall (r :: Symbol) (fn :: Univ) env st sig fail p.
(Environment (EraRule r ConwayEra) ~ env,
 State (EraRule r ConwayEra) ~ st,
 Signal (EraRule r ConwayEra) ~ sig,
 PredicateFailure (EraRule r ConwayEra) ~ fail,
 STS (EraRule r ConwayEra),
 BaseM (EraRule r ConwayEra) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> Specification fn st)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2' Specification fn env
specEnv env -> Specification fn st
specState env -> st -> Specification fn sig
specSig env -> st -> sig -> Specification fn st
specPostState env -> st -> sig -> st -> p
prop =
  forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind (forall (fn :: Univ) a.
HasSpec fn a =>
Specification fn a -> GenShrink a
genShrinkFromSpec Specification fn env
specEnv) forall a b. (a -> b) -> a -> b
$ \env
env ->
    forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. String -> Doc a
ppString String
"env = " forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> Doc Ann
prettyA env
env) forall a b. (a -> b) -> a -> b
$
      forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind (forall (fn :: Univ) a.
HasSpec fn a =>
Specification fn a -> GenShrink a
genShrinkFromSpec forall a b. (a -> b) -> a -> b
$ env -> Specification fn st
specState env
env) forall a b. (a -> b) -> a -> b
$ \st
st ->
        forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. String -> Doc a
ppString String
"st = " forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> Doc Ann
prettyA st
st) forall a b. (a -> b) -> a -> b
$
          forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind (forall (fn :: Univ) a.
HasSpec fn a =>
Specification fn a -> GenShrink a
genShrinkFromSpec forall a b. (a -> b) -> a -> b
$ env -> st -> Specification fn sig
specSig env
env st
st) forall a b. (a -> b) -> a -> b
$ \sig
sig ->
            forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. String -> Doc a
ppString String
"sig = " forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> Doc Ann
prettyA sig
sig) forall a b. (a -> b) -> a -> b
$
              forall a. ShelleyBase a -> a
runShelleyBase forall a b. (a -> b) -> a -> b
$ do
                Either (NonEmpty fail) st
res <- forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTS @(EraRule r ConwayEra) forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (env
env, st
st, sig
sig)
                forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case Either (NonEmpty fail) st
res of
                  Left NonEmpty fail
pfailures -> forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall t. PrettyA t => t -> Doc Ann
prettyA NonEmpty fail
pfailures) forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
False
                  Right st
st' ->
                    case forall (fn :: Univ) a.
HasSpec fn a =>
a
-> Specification fn a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE @fn
                      st
st
                      (env -> st -> sig -> Specification fn st
specPostState env
env st
st sig
sig)
                      (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"conformsToSpecE fails in STS tests") of
                      Just NonEmpty String
es -> forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines (forall a. NonEmpty a -> [a]
NE.toList NonEmpty String
es)) Bool
False
                      Maybe (NonEmpty String)
Nothing ->
                        forall prop. Testable prop => String -> prop -> Property
counterexample
                          ( forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$
                              forall a. String -> Doc a
ppString String
"st' = "
                                forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> Doc Ann
prettyA st
st'
                                forall a. Semigroup a => a -> a -> a
<> forall a. String -> Doc a
ppString (String
"\nspec = \n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (env -> Specification fn st
specState env
env))
                          )
                          forall a b. (a -> b) -> a -> b
$ env -> st -> sig -> st -> p
prop env
env st
st sig
sig st
st'

-- STS properties ---------------------------------------------------------

prop_GOV :: Property
prop_GOV :: Property
prop_GOV =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"GOV" @ConwayFn
    forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn (GovEnv ConwayEra)
govEnvSpec
    forall (fn :: Univ).
IsConwayUniv fn =>
GovEnv ConwayEra -> Specification fn (Proposals ConwayEra)
govProposalsSpec
    forall (fn :: Univ).
IsConwayUniv fn =>
GovEnv ConwayEra
-> Proposals ConwayEra -> Specification fn (GovSignal ConwayEra)
govProceduresSpec
    -- TODO: we should probably check more things here
    forall a b. (a -> b) -> a -> b
$ \GovEnv ConwayEra
_env Proposals ConwayEra
_st GovSignal ConwayEra
_sig Proposals ConwayEra
_st' -> Bool
True

-- prop_NEWEPOCH :: Property
-- prop_NEWEPOCH =
--   stsPropertyV2 @"NEWEPOCH" @ConwayFn
--     TrueSpec
--     (\_env -> TrueSpec)
--     (\_env _st -> TrueSpec)
--     $ \_env _st _sig _st' -> True

prop_EPOCH :: EpochNo -> Property
prop_EPOCH :: EpochNo -> Property
prop_EPOCH EpochNo
epochNo =
  forall (r :: Symbol) (fn :: Univ) env st sig fail p.
(Environment (EraRule r ConwayEra) ~ env,
 State (EraRule r ConwayEra) ~ st,
 Signal (EraRule r ConwayEra) ~ sig,
 PredicateFailure (EraRule r ConwayEra) ~ fail,
 STS (EraRule r ConwayEra),
 BaseM (EraRule r ConwayEra) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> Specification fn st)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2' @"EPOCH" @ConwayFn
    forall (fn :: Univ) a. Specification fn a
TrueSpec
    (\()
_env -> Term ConwayFn EpochNo
-> Specification ConwayFn (EpochState ConwayEra)
epochStateSpec (forall a (fn :: Univ). Show a => a -> Term fn a
lit EpochNo
epochNo))
    (\()
_env EpochState ConwayEra
_st -> EpochNo -> Specification ConwayFn EpochNo
epochSignalSpec EpochNo
epochNo)
    (\()
_env EpochState ConwayEra
_st EpochNo
_newEpoch -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    -- (\_env _st newEpoch -> epochStateSpec (lit newEpoch))
    forall a b. (a -> b) -> a -> b
$ \()
_env EpochState ConwayEra
_st EpochNo
_sig EpochState ConwayEra
_st' -> Bool
True

prop_ENACT :: Property
prop_ENACT :: Property
prop_ENACT =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"ENACT" @ConwayFn
    forall (fn :: Univ) a. Specification fn a
TrueSpec
    (\()
_env -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    -- TODO: this is a bit suspect, there are preconditions on these signals in the spec so we
    -- shouldn't expect this to go through so easily.
    (\()
_env EnactState ConwayEra
_st -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    forall a b. (a -> b) -> a -> b
$ \()
_env EnactState ConwayEra
_st EnactSignal ConwayEra
_sig EnactState ConwayEra
_st' -> Bool
True

prop_UTXOS :: Property
prop_UTXOS :: Property
prop_UTXOS =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"UTXOS" @ConwayFn
    forall (fn :: Univ) a. Specification fn a
TrueSpec
    (\UtxoEnv ConwayEra
_env -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    (\UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    forall a b. (a -> b) -> a -> b
$ \UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st AlonzoTx ConwayEra
_sig UTxOState ConwayEra
_st' -> Bool
True

-- prop_LEDGER :: Property
-- prop_LEDGER = property $ do
--  pure $ stsPropertyV2 @"LEDGER" @ConwayFn
--    TrueSpec
--    (\_env -> TrueSpec)
--    -- TODO: the `GenDelegs` don't appear to be used (?!) so we just give an
--    -- empty map here. One could consider generating them instead
--    ledgerTxSpec
--    $ \_env _st _sig _st' -> True

-- prop_TICKF :: Property
-- prop_TICKF =
--   stsPropertyV2 @"TICKF" @ConwayFn
--     TrueSpec
--     (\_env -> TrueSpec)
--     (\_env _st -> TrueSpec)
--     $ \_env _st _sig _st' -> True

prop_RATIFY :: Property
prop_RATIFY :: Property
prop_RATIFY =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"RATIFY" @ConwayFn
    forall (fn :: Univ) a. Specification fn a
TrueSpec
    (\RatifyEnv ConwayEra
_env -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    (\RatifyEnv ConwayEra
_env RatifyState ConwayEra
_st -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    -- TODO: we should probably check more things here
    forall a b. (a -> b) -> a -> b
$ \RatifyEnv ConwayEra
_env RatifyState ConwayEra
_st RatifySignal ConwayEra
_sig RatifyState ConwayEra
_st' -> Bool
True

-- prop_CERTS :: Property
-- prop_CERTS =
--   stsPropertyV2 @"CERTS" @ConwayFn
--     TrueSpec
--     (\_env -> TrueSpec)
--     (\_env _st -> TrueSpec)
--     -- TODO: we should probably check more things here
--     $ \_env _st _sig _st' -> True

prop_CERT :: Property
prop_CERT :: Property
prop_CERT =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll
    Gen
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
   Map RewardAccount Coin)
genContext
    ( \(WitUniv ConwayEra
conwayWitUniv, Set (Credential 'DRepRole)
conwayDelegatees, Map RewardAccount Coin
conwayWdrls) ->
        forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"CERT" @ConwayFn
          (forall (fn :: Univ) era.
(EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (CertEnv era)
certEnvSpec WitUniv ConwayEra
conwayWitUniv)
          (\CertEnv ConwayEra
_env -> forall (fn :: Univ) era.
(IsConwayUniv fn, EraSpecDeleg era, Era era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (CertState era)
certStateSpec WitUniv ConwayEra
conwayWitUniv Set (Credential 'DRepRole)
conwayDelegatees Map RewardAccount Coin
conwayWdrls)
          (\CertEnv ConwayEra
env CertState ConwayEra
st -> forall (fn :: Univ) era.
(IsConwayUniv fn, era ~ ConwayEra) =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification fn (ConwayTxCert era)
conwayTxCertSpec WitUniv ConwayEra
conwayWitUniv CertEnv ConwayEra
env CertState ConwayEra
st)
          -- TODO: we should probably check more things here
          forall a b. (a -> b) -> a -> b
$ \CertEnv ConwayEra
_env CertState ConwayEra
_st ConwayTxCert ConwayEra
_sig CertState ConwayEra
_st' -> Bool
True
    )

prop_DELEG :: Property
prop_DELEG :: Property
prop_DELEG =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll
    Gen
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
   Map RewardAccount Coin)
genContext
    ( \(WitUniv ConwayEra
conwayWitUniv, Set (Credential 'DRepRole)
conwayDelegatees, Map RewardAccount Coin
conwayWdrls) ->
        forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"DELEG" @ConwayFn
          forall era (fn :: Univ).
(EraSpecPParams era, IsConwayUniv fn) =>
Specification fn (ConwayDelegEnv era)
delegEnvSpec
          (\ConwayDelegEnv ConwayEra
_env -> forall (fn :: Univ) era.
(IsConwayUniv fn, EraSpecDeleg era, Era era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (CertState era)
certStateSpec WitUniv ConwayEra
conwayWitUniv Set (Credential 'DRepRole)
conwayDelegatees Map RewardAccount Coin
conwayWdrls)
          forall (fn :: Univ) era.
(EraPParams era, IsConwayUniv fn) =>
ConwayDelegEnv era
-> CertState era -> Specification fn ConwayDelegCert
conwayDelegCertSpec
          forall a b. (a -> b) -> a -> b
$ \ConwayDelegEnv ConwayEra
_env CertState ConwayEra
_st ConwayDelegCert
_sig CertState ConwayEra
_st' -> Bool
True
    )

prop_POOL :: Property
prop_POOL :: Property
prop_POOL =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll
    Gen
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
   Map RewardAccount Coin)
genContext
    ( \(WitUniv ConwayEra
conwayWitUniv, Set (Credential 'DRepRole)
_, Map RewardAccount Coin
_) ->
        forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"POOL" @ConwayFn
          (forall (fn :: Univ) era.
(EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (PoolEnv era)
poolEnvSpec WitUniv ConwayEra
conwayWitUniv)
          (\PoolEnv ConwayEra
_env -> forall (fn :: Univ) era.
(Era era, IsConwayUniv fn) =>
WitUniv era -> Specification fn (PState era)
pStateSpec WitUniv ConwayEra
conwayWitUniv)
          (\PoolEnv ConwayEra
env PState ConwayEra
st -> forall (fn :: Univ) era.
(EraSpecPParams era, IsConwayUniv fn) =>
WitUniv era
-> PoolEnv era -> PState era -> Specification fn PoolCert
poolCertSpec @ConwayFn @ConwayEra WitUniv ConwayEra
conwayWitUniv PoolEnv ConwayEra
env PState ConwayEra
st)
          forall a b. (a -> b) -> a -> b
$ \PoolEnv ConwayEra
_env PState ConwayEra
_st PoolCert
_sig PState ConwayEra
_st' -> Bool
True
    )

prop_GOVCERT :: Property
prop_GOVCERT :: Property
prop_GOVCERT =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll
    Gen
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
   Map RewardAccount Coin)
genContext
    ( \(WitUniv ConwayEra
conwayWitUniv, Set (Credential 'DRepRole)
conwayDelegatees, Map RewardAccount Coin
conwayWdrls) ->
        forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"GOVCERT" @ConwayFn
          (forall (fn :: Univ).
IsConwayUniv fn =>
WitUniv ConwayEra -> Specification fn (ConwayGovCertEnv ConwayEra)
govCertEnvSpec WitUniv ConwayEra
conwayWitUniv)
          (\ConwayGovCertEnv ConwayEra
_env -> forall (fn :: Univ) era.
(IsConwayUniv fn, EraSpecDeleg era, Era era) =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification fn (CertState era)
certStateSpec WitUniv ConwayEra
conwayWitUniv Set (Credential 'DRepRole)
conwayDelegatees Map RewardAccount Coin
conwayWdrls)
          (\ConwayGovCertEnv ConwayEra
env CertState ConwayEra
st -> forall (fn :: Univ) era.
(IsConwayUniv fn, Era era) =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification fn ConwayGovCert
govCertSpec WitUniv ConwayEra
conwayWitUniv ConwayGovCertEnv ConwayEra
env CertState ConwayEra
st)
          forall a b. (a -> b) -> a -> b
$ \ConwayGovCertEnv ConwayEra
_env CertState ConwayEra
_st ConwayGovCert
_sig CertState ConwayEra
_st' -> Bool
True
    )

prop_UTXOW :: Property
prop_UTXOW :: Property
prop_UTXOW =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra, Environment (EraRule r era) ~ env,
 State (EraRule r era) ~ st, Signal (EraRule r era) ~ sig,
 PredicateFailure (EraRule r era) ~ fail, STS (EraRule r era),
 BaseM (EraRule r era) ~ ReaderT Globals Identity, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec fn env,
 HasSpec fn st, HasSpec fn sig) =>
Specification fn env
-> (env -> Specification fn st)
-> (env -> st -> Specification fn sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"UTXOW" @ConwayFn
    forall (fn :: Univ) a. Specification fn a
TrueSpec
    (\UtxoEnv ConwayEra
_env -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    (\UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    forall a b. (a -> b) -> a -> b
$ \UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st AlonzoTx ConwayEra
_sig UTxOState ConwayEra
_st' -> Bool
True

-- prop_UTXO :: Property
-- prop_UTXO = property $ do
--  ctx <- arbitrary
--  pure $ stsPropertyV2 @"UTXO" @ConwayFn
--    utxoEnvSpec
--    utxoStateSpec
--    (utxoTxSpec ctx)
--    $ \_env _st _sig _st' -> True

-- prop_BBODY :: Property
-- prop_BBODY =
--   stsPropertyV2 @"BBODY" @ConwayFn
--     TrueSpec
--     (\_env -> TrueSpec)
--     (\_env _st -> TrueSpec)
--     $ \_env _st _sig _st' -> True

-- prop_LEDGERS :: Property
-- prop_LEDGERS =
--   stsPropertyV2 @"LEDGERS" @ConwayFn
--     TrueSpec
--     (\_env -> TrueSpec)
--     (\_env _st -> TrueSpec)
--     $ \_env _st _sig _st' -> True

-- prop_RUPD :: Property
-- prop_RUPD =
--   stsPropertyV2 @"RUPD" @ConwayFn
--     TrueSpec
--     (\_env -> TrueSpec)
--     (\_env _st -> TrueSpec)
--     $ \_env _st _sig _st' -> True

-- prop_SNAP :: Property
-- prop_SNAP =
--   stsPropertyV2 @"SNAP" @ConwayFn
--     TrueSpec
--     (\_env -> TrueSpec)
--     (\_env _st -> TrueSpec)
--     $ \_env _st _sig _st' -> True

-- prop_TICK :: Property
-- prop_TICK =
--   stsPropertyV2 @"TICK" @ConwayFn
--     TrueSpec
--     (\_env -> TrueSpec)
--     (\_env _st -> TrueSpec)
--     $ \_env _st _sig _st' -> True

------------------------------------------------------------------------
-- Test Tree
------------------------------------------------------------------------

tests_STS :: TestTree
tests_STS :: TestTree
tests_STS =
  String -> [TestTree] -> TestTree
testGroup
    String
"STS property tests"
    [ TestTree
govTests
    , -- , utxoTests
      -- TODO: this is probably one of the last things we want to
      -- get passing as it depends on being able to generate a complete
      -- `EpochState era`
      forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_EPOCH" EpochNo -> Property
prop_EPOCH
      -- , testProperty "prop_LEDGER" prop_LEDGER
    ]

govTests :: TestTree
govTests :: TestTree
govTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"GOV tests"
    [ forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_GOVCERT" Property
prop_GOVCERT
    , forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_POOL" Property
prop_POOL
    , forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_DELEG" Property
prop_DELEG
    , forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_ENACT" Property
prop_ENACT
    , forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_RATIFY" Property
prop_RATIFY
    , forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_CERT" Property
prop_CERT
    , forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_GOV" Property
prop_GOV
    ]

utxoTests :: TestTree
utxoTests :: TestTree
utxoTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"UTXO* rules"
    [ {-testProperty "prop_UTXO" prop_UTXO
      ,-} forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_UTXOW" Property
prop_UTXOW
    , forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_UTXOS" Property
prop_UTXOS
    ]

epoch :: TestTree
epoch :: TestTree
epoch =
  String -> [TestTree] -> TestTree
testGroup
    String
"STS property tests"
    [ TestTree
govTests
    , forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_EPOCH" EpochNo -> Property
prop_EPOCH
    ]