{-# 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.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.Generic.PrettyCore
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 <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall era.
Era era =>
WitUniv era -> Specification (Set (Credential 'DRepRole))
delegateeSpec WitUniv ConwayEra
univ)
  Map RewardAccount Coin
wdrls <- forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
x -> (forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv ConwayEra
univ Term (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 a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec :: forall a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec Specification a
spec = (forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification a
spec, 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
  , PrettyA st
  , PrettyA sig
  , PrettyA env
  , PrettyA fail
  , Testable p
  , HasSpec env
  , HasSpec st
  , HasSpec sig
  ) =>
  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, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec env,
 HasSpec st, HasSpec sig) =>
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, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec env,
 HasSpec st, HasSpec sig) =>
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
  , PrettyA st
  , PrettyA sig
  , PrettyA env
  , PrettyA fail
  , Testable p
  , HasSpec env
  , HasSpec st
  , HasSpec sig
  ) =>
  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, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec env,
 HasSpec st, HasSpec sig) =>
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 =
  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 a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec Specification 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 a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec forall a b. (a -> b) -> a -> b
$ env -> Specification 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 a. HasSpec a => Specification a -> GenShrink a
genShrinkFromSpec forall a b. (a -> b) -> a -> b
$ env -> st -> Specification 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 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)
                      (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 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) 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 env,
 HasSpec st, HasSpec sig) =>
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
    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, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec env,
 HasSpec st, HasSpec sig) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> Specification st)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2' @"EPOCH"
    forall a. Specification a
TrueSpec
    (\()
_env -> Term EpochNo -> Specification (EpochState ConwayEra)
epochStateSpec (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 -> forall a. Specification 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) 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 env,
 HasSpec st, HasSpec sig) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"ENACT"
    forall a. Specification a
TrueSpec
    (\()
_env -> forall a. Specification 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 a. Specification 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) 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 env,
 HasSpec st, HasSpec sig) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"UTXOS"
    forall a. Specification a
TrueSpec
    (\UtxoEnv ConwayEra
_env -> forall a. Specification a
TrueSpec)
    (\UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st -> forall a. Specification 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"
--    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, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec env,
 HasSpec st, HasSpec sig) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"RATIFY"
    forall a. Specification a
TrueSpec
    (\RatifyEnv ConwayEra
_env -> forall a. Specification a
TrueSpec)
    (\RatifyEnv ConwayEra
_env RatifyState ConwayEra
_st -> forall a. Specification 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"
--     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) 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 env,
 HasSpec st, HasSpec sig) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"CERT"
          (forall era.
EraSpecPParams era =>
WitUniv era -> Specification (CertEnv era)
certEnvSpec WitUniv ConwayEra
conwayWitUniv)
          (\CertEnv ConwayEra
_env -> 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 -> forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec WitUniv ConwayEra
conwayWitUniv CertEnv ConwayEra
env ConwayCertState ConwayEra
st)
          -- TODO: we should probably check more things here
          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 =
  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, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec env,
 HasSpec st, HasSpec sig) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"DELEG"
          forall era.
EraSpecPParams era =>
Specification (ConwayDelegEnv era)
delegEnvSpec
          (\ConwayDelegEnv ConwayEra
_env -> 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)
          forall era.
(EraPParams era, ConwayEraCertState era) =>
ConwayDelegEnv era
-> CertState era -> Specification ConwayDelegCert
conwayDelegCertSpec
          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 =
  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, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec env,
 HasSpec st, HasSpec sig) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"POOL"
          (forall era.
EraSpecPParams era =>
WitUniv era -> Specification (PoolEnv era)
poolEnvSpec WitUniv ConwayEra
conwayWitUniv)
          (\PoolEnv ConwayEra
_env -> 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)
          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) 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 env,
 HasSpec st, HasSpec sig) =>
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 -> 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 -> forall era.
EraCertState era =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
govCertSpec WitUniv ConwayEra
conwayWitUniv ConwayGovCertEnv ConwayEra
env ConwayCertState ConwayEra
st)
          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, PrettyA st,
 PrettyA sig, PrettyA env, PrettyA fail, Testable p, HasSpec env,
 HasSpec st, HasSpec sig) =>
Specification env
-> (env -> Specification st)
-> (env -> st -> Specification sig)
-> (env -> st -> sig -> st -> p)
-> Property
stsPropertyV2 @"UTXOW"
    forall a. Specification a
TrueSpec
    (\UtxoEnv ConwayEra
_env -> forall a. Specification a
TrueSpec)
    (\UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st -> forall a. Specification 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"
--    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`
      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
    ]