{-# 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.Coin (Coin)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.Shelley.Rules hiding (epochNo, slotNo)
import Constrained.API hiding (forAll)
import Constrained.TheKnot (shrinkWithSpec)
import Control.Monad.Reader
import Control.State.Transition.Extended
import qualified Data.List.NonEmpty as NE
import Data.Map (Map)
import Data.Set (Set)
import Test.Cardano.Ledger.Common (ToExpr (..))
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.Pool
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse (WitUniv, genWitUniv, witness)
import Test.Cardano.Ledger.Shelley.Utils
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 <- Specification (Set (Credential 'DRepRole))
-> Gen (Set (Credential 'DRepRole))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (WitUniv ConwayEra -> Specification (Set (Credential 'DRepRole))
forall era.
Era era =>
WitUniv era -> Specification (Set (Credential 'DRepRole))
delegateeSpec WitUniv ConwayEra
univ)
  Map RewardAccount Coin
wdrls <- Specification (Map RewardAccount Coin)
-> Gen (Map RewardAccount Coin)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec ((Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Map RewardAccount Coin) -> Pred)
 -> Specification (Map RewardAccount Coin))
-> (Term (Map RewardAccount Coin) -> Pred)
-> Specification (Map RewardAccount Coin)
forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
x -> WitUniv ConwayEra -> Term (Map RewardAccount Coin) -> Pred
forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv ConwayEra
univ Term (Map RewardAccount Coin)
x)
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
 Map RewardAccount Coin)
-> Gen
     (WitUniv ConwayEra, Set (Credential 'DRepRole),
      Map RewardAccount Coin)
forall a. a -> Gen a
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 a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec :: forall a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec Specification a
spec = (Specification a -> Gen a
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification a
spec, Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
spec)

stsPropertyV2 ::
  forall r 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
  , Testable p
  , HasSpec env
  , HasSpec st
  , HasSpec sig
  , ToExpr env
  , ToExpr st
  , ToExpr sig
  , ToExpr fail
  ) =>
  Specification env ->
  (env -> Specification st) ->
  (env -> st -> Specification sig) ->
  (env -> st -> sig -> st -> p) ->
  Property
stsPropertyV2 :: forall (r :: Symbol) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 Specification env
specEnv env -> Specification st
specState env -> st -> Specification sig
specSig env -> st -> sig -> st -> p
prop =
  forall (r :: Symbol) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> Specification st)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2' @r Specification env
specEnv env -> Specification st
specState env -> st -> Specification sig
specSig (\env
env st
_ sig
_ -> env -> Specification st
specState env
env) env -> st -> sig -> st -> p
prop

stsPropertyV2' ::
  forall r 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
  , Testable p
  , HasSpec env
  , HasSpec st
  , HasSpec sig
  , ToExpr env
  , ToExpr st
  , ToExpr sig
  , ToExpr fail
  ) =>
  Specification env ->
  (env -> Specification st) ->
  (env -> st -> Specification 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 st) ->
  (env -> st -> sig -> st -> p) ->
  Property
stsPropertyV2' :: forall (r :: Symbol) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> Specification st)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2' Specification env
specEnv env -> Specification st
specState env -> st -> Specification sig
specSig env -> st -> sig -> Specification st
specPostState env -> st -> sig -> st -> p
prop =
  (Gen env -> (env -> [env]) -> (env -> Property) -> Property)
-> (Gen env, env -> [env]) -> (env -> Property) -> Property
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Gen env -> (env -> [env]) -> (env -> Property) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind (Specification env -> (Gen env, env -> [env])
forall a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec Specification env
specEnv) ((env -> Property) -> Property) -> (env -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \env
env ->
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Expr -> String
forall a. Show a => a -> String
show (Expr -> String) -> Expr -> String
forall a b. (a -> b) -> a -> b
$ env -> Expr
forall a. ToExpr a => a -> Expr
toExpr env
env) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      (Gen st -> (st -> [st]) -> (st -> Property) -> Property)
-> (Gen st, st -> [st]) -> (st -> Property) -> Property
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Gen st -> (st -> [st]) -> (st -> Property) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind (Specification st -> (Gen st, st -> [st])
forall a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec (Specification st -> (Gen st, st -> [st]))
-> Specification st -> (Gen st, st -> [st])
forall a b. (a -> b) -> a -> b
$ env -> Specification st
specState env
env) ((st -> Property) -> Property) -> (st -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \st
st ->
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Expr -> String
forall a. Show a => a -> String
show (Expr -> String) -> Expr -> String
forall a b. (a -> b) -> a -> b
$ st -> Expr
forall a. ToExpr a => a -> Expr
toExpr st
st) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          (Gen sig -> (sig -> [sig]) -> (sig -> Property) -> Property)
-> (Gen sig, sig -> [sig]) -> (sig -> Property) -> Property
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Gen sig -> (sig -> [sig]) -> (sig -> Property) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind (Specification sig -> (Gen sig, sig -> [sig])
forall a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec (Specification sig -> (Gen sig, sig -> [sig]))
-> Specification sig -> (Gen sig, sig -> [sig])
forall a b. (a -> b) -> a -> b
$ env -> st -> Specification sig
specSig env
env st
st) ((sig -> Property) -> Property) -> (sig -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \sig
sig ->
            String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Expr -> String
forall a. Show a => a -> String
show (Expr -> String) -> Expr -> String
forall a b. (a -> b) -> a -> b
$ sig -> Expr
forall a. ToExpr a => a -> Expr
toExpr sig
sig) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              ShelleyBase Property -> Property
forall a. ShelleyBase a -> a
runShelleyBase (ShelleyBase Property -> Property)
-> ShelleyBase Property -> Property
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) (RuleContext 'Transition (EraRule r ConwayEra)
 -> ReaderT
      Globals
      Identity
      (Either
         (NonEmpty (PredicateFailure (EraRule r ConwayEra)))
         (State (EraRule r ConwayEra))))
-> RuleContext 'Transition (EraRule r ConwayEra)
-> ReaderT
     Globals
     Identity
     (Either
        (NonEmpty (PredicateFailure (EraRule r ConwayEra)))
        (State (EraRule r ConwayEra)))
forall a b. (a -> b) -> a -> b
$ (Environment (EraRule r ConwayEra), State (EraRule r ConwayEra),
 Signal (EraRule r ConwayEra))
-> TRC (EraRule r ConwayEra)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (env
Environment (EraRule r ConwayEra)
env, st
State (EraRule r ConwayEra)
st, sig
Signal (EraRule r ConwayEra)
sig)
                Property -> ShelleyBase Property
forall a. a -> ReaderT Globals Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> ShelleyBase Property)
-> Property -> ShelleyBase Property
forall a b. (a -> b) -> a -> b
$ case Either (NonEmpty fail) st
res of
                  Left NonEmpty fail
pfailures -> String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Expr -> String
forall a. Show a => a -> String
show (Expr -> String) -> Expr -> String
forall a b. (a -> b) -> a -> b
$ NonEmpty fail -> Expr
forall a. ToExpr a => a -> Expr
toExpr NonEmpty fail
pfailures) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False
                  Right st
st' ->
                    case st
-> Specification st -> NonEmpty String -> Maybe (NonEmpty String)
forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE
                      st
st
                      (env -> st -> sig -> Specification st
specPostState env
env st
st sig
sig)
                      (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"conformsToSpecE fails in STS tests") of
                      Just NonEmpty String
es -> String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines (NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty String
es)) Bool
False
                      Maybe (NonEmpty String)
Nothing ->
                        String -> p -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                          ( (Expr, String) -> String
forall a. Show a => a -> String
show
                              (st -> Expr
forall a. ToExpr a => a -> Expr
toExpr st
st', Specification st -> String
forall a. Show a => a -> String
show (env -> Specification st
specState env
env))
                          )
                          (p -> Property) -> p -> Property
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) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"GOV"
    Specification (GovEnv ConwayEra)
govEnvSpec
    GovEnv ConwayEra -> Specification (Proposals ConwayEra)
govProposalsSpec
    GovEnv ConwayEra
-> Proposals ConwayEra -> Specification (GovSignal ConwayEra)
govProceduresSpec
    -- TODO: we should probably check more things here
    ((GovEnv ConwayEra
  -> Proposals ConwayEra
  -> GovSignal ConwayEra
  -> Proposals ConwayEra
  -> Bool)
 -> Property)
-> (GovEnv ConwayEra
    -> Proposals ConwayEra
    -> GovSignal ConwayEra
    -> Proposals ConwayEra
    -> Bool)
-> Property
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"
--     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) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> Specification st)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2' @"EPOCH"
    Specification ()
forall deps a. SpecificationD deps a
TrueSpec
    (\()
_env -> Term EpochNo -> Specification (EpochState ConwayEra)
epochStateSpec (EpochNo -> Term EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
epochNo))
    (\()
_env EpochState ConwayEra
_st -> EpochNo -> Specification EpochNo
epochSignalSpec EpochNo
epochNo)
    (\()
_env EpochState ConwayEra
_st EpochNo
_newEpoch -> Specification (EpochState ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec)
    -- (\_env _st newEpoch -> epochStateSpec (lit newEpoch))
    ((()
  -> EpochState ConwayEra -> EpochNo -> EpochState ConwayEra -> Bool)
 -> Property)
-> (()
    -> EpochState ConwayEra -> EpochNo -> EpochState ConwayEra -> Bool)
-> Property
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) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"ENACT"
    Specification ()
forall deps a. SpecificationD deps a
TrueSpec
    (\()
_env -> Specification (EnactState ConwayEra)
forall deps a. SpecificationD deps 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 -> Specification (EnactSignal ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec)
    ((()
  -> EnactState ConwayEra
  -> EnactSignal ConwayEra
  -> EnactState ConwayEra
  -> Bool)
 -> Property)
-> (()
    -> EnactState ConwayEra
    -> EnactSignal ConwayEra
    -> EnactState ConwayEra
    -> Bool)
-> Property
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) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"UTXOS"
    Specification (UtxoEnv ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec
    (\UtxoEnv ConwayEra
_env -> Specification (UTxOState ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec)
    (\UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st -> Specification (AlonzoTx ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec)
    ((UtxoEnv ConwayEra
  -> UTxOState ConwayEra
  -> AlonzoTx ConwayEra
  -> UTxOState ConwayEra
  -> Bool)
 -> Property)
-> (UtxoEnv ConwayEra
    -> UTxOState ConwayEra
    -> AlonzoTx ConwayEra
    -> UTxOState ConwayEra
    -> Bool)
-> Property
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"
--    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"
--     TrueSpec
--     (\_env -> TrueSpec)
--     (\_env _st -> TrueSpec)
--     $ \_env _st _sig _st' -> True

prop_RATIFY :: Property
prop_RATIFY :: Property
prop_RATIFY =
  forall (r :: Symbol) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"RATIFY"
    Specification (RatifyEnv ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec
    (\RatifyEnv ConwayEra
_env -> Specification (RatifyState ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec)
    (\RatifyEnv ConwayEra
_env RatifyState ConwayEra
_st -> Specification (RatifySignal ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec)
    -- TODO: we should probably check more things here
    ((RatifyEnv ConwayEra
  -> RatifyState ConwayEra
  -> RatifySignal ConwayEra
  -> RatifyState ConwayEra
  -> Bool)
 -> Property)
-> (RatifyEnv ConwayEra
    -> RatifyState ConwayEra
    -> RatifySignal ConwayEra
    -> RatifyState ConwayEra
    -> Bool)
-> Property
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"
--     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 =
  Gen
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
   Map RewardAccount Coin)
-> ((WitUniv ConwayEra, Set (Credential 'DRepRole),
     Map RewardAccount Coin)
    -> Property)
-> Property
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) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"CERT"
          (WitUniv ConwayEra -> Specification (CertEnv ConwayEra)
forall era.
EraSpecPParams era =>
WitUniv era -> Specification (CertEnv era)
certEnvSpec WitUniv ConwayEra
conwayWitUniv)
          (\CertEnv ConwayEra
_env -> WitUniv ConwayEra
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState ConwayEra)
forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec WitUniv ConwayEra
conwayWitUniv Set (Credential 'DRepRole)
conwayDelegatees Map RewardAccount Coin
conwayWdrls)
          (\CertEnv ConwayEra
env ConwayCertState ConwayEra
st -> WitUniv ConwayEra
-> CertEnv ConwayEra
-> CertState ConwayEra
-> Specification (ConwayTxCert ConwayEra)
forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec WitUniv ConwayEra
conwayWitUniv CertEnv ConwayEra
env CertState ConwayEra
ConwayCertState ConwayEra
st)
          -- TODO: we should probably check more things here
          ((CertEnv ConwayEra
  -> ConwayCertState ConwayEra
  -> ConwayTxCert ConwayEra
  -> ConwayCertState ConwayEra
  -> Bool)
 -> Property)
-> (CertEnv ConwayEra
    -> ConwayCertState ConwayEra
    -> ConwayTxCert ConwayEra
    -> ConwayCertState ConwayEra
    -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \CertEnv ConwayEra
_env ConwayCertState ConwayEra
_st ConwayTxCert ConwayEra
_sig ConwayCertState ConwayEra
_st' -> Bool
True
    )

prop_DELEG :: Property
prop_DELEG :: Property
prop_DELEG =
  Gen
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
   Map RewardAccount Coin)
-> ((WitUniv ConwayEra, Set (Credential 'DRepRole),
     Map RewardAccount Coin)
    -> Property)
-> Property
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) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"DELEG"
          Specification (ConwayDelegEnv ConwayEra)
forall era.
EraSpecPParams era =>
Specification (ConwayDelegEnv era)
delegEnvSpec
          (\ConwayDelegEnv ConwayEra
_env -> WitUniv ConwayEra
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState ConwayEra)
forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec WitUniv ConwayEra
conwayWitUniv Set (Credential 'DRepRole)
conwayDelegatees Map RewardAccount Coin
conwayWdrls)
          ConwayDelegEnv ConwayEra
-> CertState ConwayEra -> Specification ConwayDelegCert
ConwayDelegEnv ConwayEra
-> ConwayCertState ConwayEra -> Specification ConwayDelegCert
forall era.
(EraPParams era, ConwayEraCertState era) =>
ConwayDelegEnv era
-> CertState era -> Specification ConwayDelegCert
conwayDelegCertSpec
          ((ConwayDelegEnv ConwayEra
  -> ConwayCertState ConwayEra
  -> ConwayDelegCert
  -> ConwayCertState ConwayEra
  -> Bool)
 -> Property)
-> (ConwayDelegEnv ConwayEra
    -> ConwayCertState ConwayEra
    -> ConwayDelegCert
    -> ConwayCertState ConwayEra
    -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \ConwayDelegEnv ConwayEra
_env ConwayCertState ConwayEra
_st ConwayDelegCert
_sig ConwayCertState ConwayEra
_st' -> Bool
True
    )

prop_POOL :: Property
prop_POOL :: Property
prop_POOL =
  Gen
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
   Map RewardAccount Coin)
-> ((WitUniv ConwayEra, Set (Credential 'DRepRole),
     Map RewardAccount Coin)
    -> Property)
-> Property
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) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"POOL"
          (WitUniv ConwayEra -> Specification (PoolEnv ConwayEra)
forall era.
EraSpecPParams era =>
WitUniv era -> Specification (PoolEnv era)
poolEnvSpec WitUniv ConwayEra
conwayWitUniv)
          (\PoolEnv ConwayEra
_env -> WitUniv ConwayEra -> Specification (PState ConwayEra)
forall era. Era era => WitUniv era -> Specification (PState era)
pStateSpec WitUniv ConwayEra
conwayWitUniv)
          (\PoolEnv ConwayEra
env PState ConwayEra
st -> forall era.
EraSpecPParams era =>
WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert
poolCertSpec @ConwayEra WitUniv ConwayEra
conwayWitUniv PoolEnv ConwayEra
env PState ConwayEra
st)
          ((PoolEnv ConwayEra
  -> PState ConwayEra -> PoolCert -> PState ConwayEra -> Bool)
 -> Property)
-> (PoolEnv ConwayEra
    -> PState ConwayEra -> PoolCert -> PState ConwayEra -> Bool)
-> Property
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 =
  Gen
  (WitUniv ConwayEra, Set (Credential 'DRepRole),
   Map RewardAccount Coin)
-> ((WitUniv ConwayEra, Set (Credential 'DRepRole),
     Map RewardAccount Coin)
    -> Property)
-> Property
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) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"GOVCERT"
          (WitUniv ConwayEra -> Specification (ConwayGovCertEnv ConwayEra)
govCertEnvSpec WitUniv ConwayEra
conwayWitUniv)
          (\ConwayGovCertEnv ConwayEra
_env -> WitUniv ConwayEra
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState ConwayEra)
forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec WitUniv ConwayEra
conwayWitUniv Set (Credential 'DRepRole)
conwayDelegatees Map RewardAccount Coin
conwayWdrls)
          (\ConwayGovCertEnv ConwayEra
env ConwayCertState ConwayEra
st -> WitUniv ConwayEra
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
forall era.
EraCertState era =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
govCertSpec WitUniv ConwayEra
conwayWitUniv ConwayGovCertEnv ConwayEra
env CertState ConwayEra
ConwayCertState ConwayEra
st)
          ((ConwayGovCertEnv ConwayEra
  -> ConwayCertState ConwayEra
  -> ConwayGovCert
  -> ConwayCertState ConwayEra
  -> Bool)
 -> Property)
-> (ConwayGovCertEnv ConwayEra
    -> ConwayCertState ConwayEra
    -> ConwayGovCert
    -> ConwayCertState ConwayEra
    -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \ConwayGovCertEnv ConwayEra
_env ConwayCertState ConwayEra
_st ConwayGovCert
_sig ConwayCertState ConwayEra
_st' -> Bool
True
    )

prop_UTXOW :: Property
prop_UTXOW :: Property
prop_UTXOW =
  forall (r :: Symbol) 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, Testable p,
 HasSpec env, HasSpec st, HasSpec sig, ToExpr env, ToExpr st,
 ToExpr sig, ToExpr fail) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"UTXOW"
    Specification (UtxoEnv ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec
    (\UtxoEnv ConwayEra
_env -> Specification (UTxOState ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec)
    (\UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st -> Specification (AlonzoTx ConwayEra)
forall deps a. SpecificationD deps a
TrueSpec)
    ((UtxoEnv ConwayEra
  -> UTxOState ConwayEra
  -> AlonzoTx ConwayEra
  -> UTxOState ConwayEra
  -> Bool)
 -> Property)
-> (UtxoEnv ConwayEra
    -> UTxOState ConwayEra
    -> AlonzoTx ConwayEra
    -> UTxOState ConwayEra
    -> Bool)
-> Property
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"
--    utxoEnvSpec
--    utxoStateSpec
--    (utxoTxSpec ctx)
--    $ \_env _st _sig _st' -> True

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

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

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

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

-- prop_TICK :: Property
-- prop_TICK =
--   stsPropertyV2 @"TICK"
--     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`
      String -> (EpochNo -> Property) -> TestTree
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"
    [ String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_GOVCERT" Property
prop_GOVCERT
    , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_POOL" Property
prop_POOL
    , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_DELEG" Property
prop_DELEG
    , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_ENACT" Property
prop_ENACT
    , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_RATIFY" Property
prop_RATIFY
    , String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_CERT" Property
prop_CERT
    , String -> Property -> TestTree
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
      ,-} String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_UTXOW" Property
prop_UTXOW
    , String -> Property -> TestTree
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
    , String -> (EpochNo -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"prop_EPOCH" EpochNo -> Property
prop_EPOCH
    ]