{-# 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 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 hiding (witness)
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

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

-- | 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
  univ <- forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv @ConwayEra Int
200
  delegatees <- genFromSpec (delegateeSpec univ)
  wdrls <- genFromSpec (constrained $ \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)
  pure (univ, delegatees, 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 =
  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)

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
theProp =
  (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
                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)
                pure $ case 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
theProp 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 a. Specification 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 a. Specification 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 a. Specification a
trueSpec
    (\()
_env -> Specification (EnactState ConwayEra)
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 -> Specification (EnactSignal ConwayEra)
forall a. Specification 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 a. Specification a
trueSpec
    (\UtxoEnv ConwayEra
_env -> Specification (UTxOState ConwayEra)
forall a. Specification a
trueSpec)
    (\UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st -> Specification (Tx TopTx ConwayEra)
forall a. Specification a
trueSpec)
    ((UtxoEnv ConwayEra
  -> UTxOState ConwayEra
  -> Tx TopTx ConwayEra
  -> UTxOState ConwayEra
  -> Bool)
 -> Property)
-> (UtxoEnv ConwayEra
    -> UTxOState ConwayEra
    -> Tx TopTx ConwayEra
    -> UTxOState ConwayEra
    -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st Tx TopTx 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 a. Specification a
trueSpec
    (\RatifyEnv ConwayEra
_env -> Specification (RatifyState ConwayEra)
forall a. Specification a
trueSpec)
    (\RatifyEnv ConwayEra
_env RatifyState ConwayEra
_st -> Specification (RatifySignal ConwayEra)
forall a. Specification 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 a. Specification a
trueSpec
    (\UtxoEnv ConwayEra
_env -> Specification (UTxOState ConwayEra)
forall a. Specification a
trueSpec)
    (\UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st -> Specification (Tx TopTx ConwayEra)
forall a. Specification a
trueSpec)
    ((UtxoEnv ConwayEra
  -> UTxOState ConwayEra
  -> Tx TopTx ConwayEra
  -> UTxOState ConwayEra
  -> Bool)
 -> Property)
-> (UtxoEnv ConwayEra
    -> UTxOState ConwayEra
    -> Tx TopTx ConwayEra
    -> UTxOState ConwayEra
    -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \UtxoEnv ConwayEra
_env UTxOState ConwayEra
_st Tx TopTx 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 :: Spec
tests_STS :: Spec
tests_STS =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"STS property tests" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Spec
govTests
    -- utxoTests
    -- prop "prop_LEDGER" prop_LEDGER
    -- 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) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_EPOCH" EpochNo -> Property
prop_EPOCH

govTests :: Spec
govTests :: Spec
govTests =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"GOV tests" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_GOVCERT" Property
prop_GOVCERT
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_POOL" Property
prop_POOL
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_DELEG" Property
prop_DELEG
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_ENACT" Property
prop_ENACT
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_RATIFY" Property
prop_RATIFY
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_CERT" Property
prop_CERT
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_GOV" Property
prop_GOV

utxoTests :: Spec
utxoTests :: Spec
utxoTests =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"UTXO* rules" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    -- prop "prop_UTXO" prop_UTXO
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_UTXOW" Property
prop_UTXOW
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_UTXOS" Property
prop_UTXOS

epoch :: Spec
epoch :: Spec
epoch =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"STS property tests" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Spec
govTests
    String -> (EpochNo -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"prop_EPOCH" EpochNo -> Property
prop_EPOCH