{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# 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

import Test.Cardano.Ledger.Constrained.Conway.Cert
import Test.Cardano.Ledger.Constrained.Conway.Deleg
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 Test.QuickCheck
import Test.Tasty
import Test.Tasty.QuickCheck

------------------------------------------------------------------------
-- 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 StandardCrypto
  , 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 StandardCrypto, 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 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 => [Char] -> prop -> Property
counterexample (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> Doc a
ppString [Char]
"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 => [Char] -> prop -> Property
counterexample (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> Doc a
ppString [Char]
"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 => [Char] -> prop -> Property
counterexample (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> Doc a
ppString [Char]
"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 era) 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 => [Char] -> prop -> Property
counterexample (forall a. Show a => a -> [Char]
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' ->
                    forall prop. Testable prop => [Char] -> prop -> Property
counterexample
                      ( forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$
                          forall a. [Char] -> Doc a
ppString [Char]
"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. [Char] -> Doc a
ppString ([Char]
"\nspec = \n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (env -> Specification fn st
specState env
env))
                      )
                      forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec @fn st
st' (env -> Specification fn st
specState env
env) forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. 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 StandardCrypto, 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 StandardCrypto))
govEnvSpec
    forall (fn :: Univ).
IsConwayUniv fn =>
GovEnv (ConwayEra StandardCrypto)
-> Specification fn (Proposals (ConwayEra StandardCrypto))
govProposalsSpec
    forall (fn :: Univ).
IsConwayUniv fn =>
GovEnv (ConwayEra StandardCrypto)
-> Proposals (ConwayEra StandardCrypto)
-> Specification fn (GovSignal (ConwayEra StandardCrypto))
govProceduresSpec
    -- TODO: we should probably check more things here
    forall a b. (a -> b) -> a -> b
$ \GovEnv (ConwayEra StandardCrypto)
_env Proposals (ConwayEra StandardCrypto)
_st GovSignal (ConwayEra StandardCrypto)
_sig Proposals (ConwayEra StandardCrypto)
_st' -> Bool
True

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

prop_EPOCH :: Property
prop_EPOCH :: Property
prop_EPOCH =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra StandardCrypto, 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 @"EPOCH" @ConwayFn
    forall (fn :: Univ) a. Specification fn a
TrueSpec
    (\()
_env -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    (\()
_env EpochState (ConwayEra StandardCrypto)
_st -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    forall a b. (a -> b) -> a -> b
$ \()
_env EpochState (ConwayEra StandardCrypto)
_st EpochNo
_sig EpochState (ConwayEra StandardCrypto)
_st' -> Bool
True

prop_ENACT :: Property
prop_ENACT :: Property
prop_ENACT =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra StandardCrypto, 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 StandardCrypto)
_st -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    forall a b. (a -> b) -> a -> b
$ \()
_env EnactState (ConwayEra StandardCrypto)
_st EnactSignal (ConwayEra StandardCrypto)
_sig EnactState (ConwayEra StandardCrypto)
_st' -> Bool
True

prop_UTXOS :: Property
prop_UTXOS :: Property
prop_UTXOS =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra StandardCrypto, 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 StandardCrypto)
_env -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    (\UtxoEnv (ConwayEra StandardCrypto)
_env UTxOState (ConwayEra StandardCrypto)
_st -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    forall a b. (a -> b) -> a -> b
$ \UtxoEnv (ConwayEra StandardCrypto)
_env UTxOState (ConwayEra StandardCrypto)
_st AlonzoTx (ConwayEra StandardCrypto)
_sig UTxOState (ConwayEra StandardCrypto)
_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 StandardCrypto, 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 StandardCrypto)
_env -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    (\RatifyEnv (ConwayEra StandardCrypto)
_env RatifyState (ConwayEra StandardCrypto)
_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 StandardCrypto)
_env RatifyState (ConwayEra StandardCrypto)
_st RatifySignal (ConwayEra StandardCrypto)
_sig RatifyState (ConwayEra StandardCrypto)
_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 (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra StandardCrypto, 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).
IsConwayUniv fn =>
Specification fn (CertEnv (ConwayEra StandardCrypto))
certEnvSpec
    (\CertEnv (ConwayEra StandardCrypto)
_env -> forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn (CertState (ConwayEra StandardCrypto))
certStateSpec)
    (\CertEnv (ConwayEra StandardCrypto)
env CertState (ConwayEra StandardCrypto)
st -> forall (fn :: Univ).
IsConwayUniv fn =>
CertEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (ConwayTxCert (ConwayEra StandardCrypto))
txCertSpec CertEnv (ConwayEra StandardCrypto)
env CertState (ConwayEra StandardCrypto)
st)
    -- TODO: we should probably check more things here
    forall a b. (a -> b) -> a -> b
$ \CertEnv (ConwayEra StandardCrypto)
_env CertState (ConwayEra StandardCrypto)
_st ConwayTxCert (ConwayEra StandardCrypto)
_sig CertState (ConwayEra StandardCrypto)
_st' -> Bool
True

prop_DELEG :: Property
prop_DELEG :: Property
prop_DELEG =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra StandardCrypto, 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 (fn :: Univ).
IsConwayUniv fn =>
Specification fn (ConwayDelegEnv (ConwayEra StandardCrypto))
delegEnvSpec
    (\ConwayDelegEnv (ConwayEra StandardCrypto)
_env -> forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn (CertState (ConwayEra StandardCrypto))
certStateSpec)
    forall (fn :: Univ).
IsConwayUniv fn =>
ConwayDelegEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (ConwayDelegCert StandardCrypto)
delegCertSpec
    forall a b. (a -> b) -> a -> b
$ \ConwayDelegEnv (ConwayEra StandardCrypto)
_env CertState (ConwayEra StandardCrypto)
_st ConwayDelegCert StandardCrypto
_sig CertState (ConwayEra StandardCrypto)
_st' -> Bool
True

prop_POOL :: Property
prop_POOL :: Property
prop_POOL =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra StandardCrypto, 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).
IsConwayUniv fn =>
Specification fn (PoolEnv (ConwayEra StandardCrypto))
poolEnvSpec
    (\PoolEnv (ConwayEra StandardCrypto)
_env -> forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn (PState (ConwayEra StandardCrypto))
pStateSpec)
    (\PoolEnv (ConwayEra StandardCrypto)
env PState (ConwayEra StandardCrypto)
st -> forall (fn :: Univ).
IsConwayUniv fn =>
PoolEnv (ConwayEra StandardCrypto)
-> PState (ConwayEra StandardCrypto)
-> Specification fn (PoolCert StandardCrypto)
poolCertSpec PoolEnv (ConwayEra StandardCrypto)
env PState (ConwayEra StandardCrypto)
st)
    forall a b. (a -> b) -> a -> b
$ \PoolEnv (ConwayEra StandardCrypto)
_env PState (ConwayEra StandardCrypto)
_st PoolCert StandardCrypto
_sig PState (ConwayEra StandardCrypto)
_st' -> Bool
True

prop_GOVCERT :: Property
prop_GOVCERT :: Property
prop_GOVCERT =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra StandardCrypto, 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 =>
Specification fn (ConwayGovCertEnv (ConwayEra StandardCrypto))
govCertEnvSpec
    (\ConwayGovCertEnv (ConwayEra StandardCrypto)
_env -> forall (fn :: Univ).
IsConwayUniv fn =>
Specification fn (CertState (ConwayEra StandardCrypto))
certStateSpec)
    (\ConwayGovCertEnv (ConwayEra StandardCrypto)
env CertState (ConwayEra StandardCrypto)
st -> forall (fn :: Univ).
IsConwayUniv fn =>
ConwayGovCertEnv (ConwayEra StandardCrypto)
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (ConwayGovCert StandardCrypto)
govCertSpec ConwayGovCertEnv (ConwayEra StandardCrypto)
env CertState (ConwayEra StandardCrypto)
st)
    forall a b. (a -> b) -> a -> b
$ \ConwayGovCertEnv (ConwayEra StandardCrypto)
_env CertState (ConwayEra StandardCrypto)
_st ConwayGovCert StandardCrypto
_sig CertState (ConwayEra StandardCrypto)
_st' -> Bool
True

prop_UTXOW :: Property
prop_UTXOW :: Property
prop_UTXOW =
  forall (r :: Symbol) (fn :: Univ) era env st sig fail p.
(era ~ ConwayEra StandardCrypto, 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 StandardCrypto)
_env -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    (\UtxoEnv (ConwayEra StandardCrypto)
_env UTxOState (ConwayEra StandardCrypto)
_st -> forall (fn :: Univ) a. Specification fn a
TrueSpec)
    forall a b. (a -> b) -> a -> b
$ \UtxoEnv (ConwayEra StandardCrypto)
_env UTxOState (ConwayEra StandardCrypto)
_st AlonzoTx (ConwayEra StandardCrypto)
_sig UTxOState (ConwayEra StandardCrypto)
_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 =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"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`
    -- , testProperty "prop_EPOCH" prop_EPOCH
    -- , testProperty "prop_LEDGER" prop_LEDGER
    ]

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

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

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