{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Conformance.ExecSpecRule.MiniTrace where

import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..))
import Cardano.Ledger.BaseTypes (Inject (..))
import Cardano.Ledger.Conway.Governance (
  RatifySignal (..),
  VotingProcedures (..),
 )
import Cardano.Ledger.Conway.Rules (GovSignal (..))
import Cardano.Ledger.Core (EraRule)
import Constrained hiding (inject)
import Control.State.Transition.Extended (STS (..))
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import qualified Data.OSet.Strict as OSet
import Data.Proxy
import Test.Cardano.Ledger.Common
import Test.Cardano.Ledger.Conformance
import Test.Cardano.Ledger.Constrained.Conway.Instances (ConwayFn)
import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (..))
import Test.Cardano.Ledger.Generic.Proof

-- \| This is where most of the ExecSpecRule instances are defined
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (
  nameCerts,
  nameDelegCert,
  nameEnact,
  nameEpoch,
  nameGovCert,
  namePoolCert,
  nameTxCert,
 )

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

-- | Generate either a list of signals, or a list of error messages
minitraceEither ::
  forall fn s e.
  ( ExecSpecRule fn s e
  , ExecState fn s e ~ State (EraRule s e)
  , PrettyA (Signal (EraRule s e))
  , PrettyA (State (EraRule s e))
  ) =>
  WitRule s e ->
  Proxy fn ->
  Int ->
  Gen (Either [String] [Signal (EraRule s e)])
minitraceEither :: forall (fn :: Univ) (s :: Symbol) e.
(ExecSpecRule fn s e, ExecState fn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy fn -> Int -> Gen (Either [String] [Signal (EraRule s e)])
minitraceEither WitRule s e
witrule Proxy fn
Proxy Int
n0 = do
  ExecContext fn s e
ctxt <- forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
Gen (ExecContext fn rule era)
genExecContext @fn @s @e
  ExecEnvironment fn s e
env <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn (forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> Specification fn (ExecEnvironment fn rule era)
environmentSpec @fn @s @e ExecContext fn s e
ctxt)
  let env2 :: Environment (EraRule s e)
      env2 :: Environment (EraRule s e)
env2 = forall t s. Inject t s => t -> s
inject ExecEnvironment fn s e
env
  !State (EraRule s e)
state0 <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn (forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> Specification fn (ExecState fn rule era)
stateSpec @fn @s @e ExecContext fn s e
ctxt ExecEnvironment fn s e
env)
  let go :: State (EraRule s e) -> Int -> Gen (Either [String] [Signal (EraRule s e)])
      go :: State (EraRule s e)
-> Int -> Gen (Either [String] [Signal (EraRule s e)])
go State (EraRule s e)
_ Int
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right [])
      go State (EraRule s e)
state Int
n = do
        ExecSignal fn s e
signal <- forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn (forall (fn :: Univ) (rule :: Symbol) era.
(ExecSpecRule fn rule era, HasCallStack) =>
ExecContext fn rule era
-> ExecEnvironment fn rule era
-> ExecState fn rule era
-> Specification fn (ExecSignal fn rule era)
signalSpec @fn @s @e ExecContext fn s e
ctxt ExecEnvironment fn s e
env State (EraRule s e)
state)
        let signal2 :: Signal (EraRule s e)
            signal2 :: Signal (EraRule s e)
signal2 = forall t s. Inject t s => t -> s
inject ExecSignal fn s e
signal
        forall (s :: Symbol) e ans env state sig.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e),
 env ~ Environment (EraRule s e), state ~ State (EraRule s e),
 sig ~ Signal (EraRule s e)) =>
WitRule s e
-> env
-> state
-> sig
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
goSTS
          WitRule s e
witrule
          Environment (EraRule s e)
env2
          State (EraRule s e)
state
          Signal (EraRule s e)
signal2
          ( \Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
x -> case Either
  (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
x of
              Left NonEmpty (PredicateFailure (EraRule s e))
ps ->
                forall (f :: * -> *) a. Applicative f => a -> f a
pure
                  ( forall a b. a -> Either a b
Left
                      ( [ String
"\nSIGNAL = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA Signal (EraRule s e)
signal2)
                        , String
"\nSTATE = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA State (EraRule s e)
state)
                        , String
"\nPredicateFailures"
                        ]
                          forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty (PredicateFailure (EraRule s e))
ps)
                      )
                  )
              Right !State (EraRule s e)
state2 -> do
                Either [String] [Signal (EraRule s e)]
ans <- State (EraRule s e)
-> Int -> Gen (Either [String] [Signal (EraRule s e)])
go State (EraRule s e)
state2 (Int
n forall a. Num a => a -> a -> a
- Int
1)
                case Either [String] [Signal (EraRule s e)]
ans of
                  Left [String]
xs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left [String]
xs)
                  Right [Signal (EraRule s e)]
more -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall t s. Inject t s => t -> s
inject ExecSignal fn s e
signal forall a. a -> [a] -> [a]
: [Signal (EraRule s e)]
more))
          )
  State (EraRule s e)
-> Int -> Gen (Either [String] [Signal (EraRule s e)])
go State (EraRule s e)
state0 Int
n0

minitrace ::
  forall fn s e.
  ( ExecSpecRule fn s e
  , ExecState fn s e ~ State (EraRule s e)
  , PrettyA (Signal (EraRule s e))
  , PrettyA (State (EraRule s e))
  ) =>
  WitRule s e ->
  Proxy fn ->
  Int ->
  Gen [Signal (EraRule s e)]
minitrace :: forall (fn :: Univ) (s :: Symbol) e.
(ExecSpecRule fn s e, ExecState fn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e -> Proxy fn -> Int -> Gen [Signal (EraRule s e)]
minitrace WitRule s e
witrule Proxy fn
Proxy Int
n0 = do
  Either [String] [Signal (EraRule s e)]
ans <- forall (fn :: Univ) (s :: Symbol) e.
(ExecSpecRule fn s e, ExecState fn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy fn -> Int -> Gen (Either [String] [Signal (EraRule s e)])
minitraceEither @fn @s @e WitRule s e
witrule forall {k} (t :: k). Proxy t
Proxy Int
n0
  case Either [String] [Signal (EraRule s e)]
ans of
    Left [String]
zs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error ([String] -> String
unlines [String]
zs)
    Right [Signal (EraRule s e)]
zs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Signal (EraRule s e)]
zs

minitraceProp ::
  forall s e.
  ( ExecSpecRule ConwayFn s e
  , ExecState ConwayFn s e ~ State (EraRule s e)
  , PrettyA (Signal (EraRule s e))
  , PrettyA (State (EraRule s e))
  ) =>
  WitRule s e ->
  Proxy ConwayFn ->
  Int ->
  (Signal (EraRule s e) -> String) ->
  Gen Property
minitraceProp :: forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp WitRule s e
witrule Proxy ConwayFn
Proxy Int
n0 Signal (EraRule s e) -> String
namef = do
  Either [String] [Signal (EraRule s e)]
ans <- forall (fn :: Univ) (s :: Symbol) e.
(ExecSpecRule fn s e, ExecState fn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy fn -> Int -> Gen (Either [String] [Signal (EraRule s e)])
minitraceEither @ConwayFn @s @e WitRule s e
witrule forall {k} (t :: k). Proxy t
Proxy Int
n0
  case Either [String] [Signal (EraRule s e)]
ans of
    Left [String]
zs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines [String]
zs) (forall prop. Testable prop => prop -> Property
property Bool
False)
    Right [Signal (EraRule s e)]
sigs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall x. (x -> String) -> [x] -> Property -> Property
classifyFirst Signal (EraRule s e) -> String
namef [Signal (EraRule s e)]
sigs forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True

-- =======================================================
-- Classifying what is in a trace requires a function that
-- lifts a Signal to a String
-- =======================================================

classifyMany :: (x -> String) -> [x] -> Property -> Property
classifyMany :: forall x. (x -> String) -> [x] -> Property -> Property
classifyMany x -> String
_ [] Property
p = Property
p
classifyMany x -> String
f (x
x : [x]
xs) Property
p = forall x. (x -> String) -> [x] -> Property -> Property
classifyMany x -> String
f [x]
xs (forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
True (x -> String
f x
x) Property
p)

classifyFirst :: (x -> String) -> [x] -> Property -> Property
classifyFirst :: forall x. (x -> String) -> [x] -> Property -> Property
classifyFirst x -> String
_ [] Property
p = Property
p
classifyFirst x -> String
f (x
x : [x]
_) Property
p = forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
True (x -> String
f x
x) Property
p

classifyFirst' :: (x -> Maybe String) -> [x] -> Property -> Property
classifyFirst' :: forall x. (x -> Maybe String) -> [x] -> Property -> Property
classifyFirst' x -> Maybe String
_ [] Property
p = Property
p
classifyFirst' x -> Maybe String
f (x
x : [x]
_) Property
p = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Property
p (\String
s -> forall prop. Testable prop => Bool -> String -> prop -> Property
classify Bool
True String
s Property
p) (x -> Maybe String
f x
x)

nameRatify :: RatifySignal era -> String
nameRatify :: forall era. RatifySignal era -> String
nameRatify (RatifySignal StrictSeq (GovActionState era)
xs) = forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length StrictSeq (GovActionState era)
xs) forall a. [a] -> [a] -> [a]
++ String
" GovActionStates"

nameGovSignal :: GovSignal (ConwayEra StandardCrypto) -> String
nameGovSignal :: GovSignal (ConwayEra StandardCrypto) -> String
nameGovSignal (GovSignal (VotingProcedures Map
  (Voter (EraCrypto (ConwayEra StandardCrypto)))
  (Map
     (GovActionId (EraCrypto (ConwayEra StandardCrypto)))
     (VotingProcedure (ConwayEra StandardCrypto)))
m) OSet (ProposalProcedure (ConwayEra StandardCrypto))
os StrictSeq (TxCert (ConwayEra StandardCrypto))
cs) = forall a. Show a => a -> String
show (forall k a. Map k a -> Int
Map.size Map
  (Voter (EraCrypto (ConwayEra StandardCrypto)))
  (Map
     (GovActionId (EraCrypto (ConwayEra StandardCrypto)))
     (VotingProcedure (ConwayEra StandardCrypto)))
m) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. OSet a -> Int
OSet.size OSet (ProposalProcedure (ConwayEra StandardCrypto))
os) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length StrictSeq (TxCert (ConwayEra StandardCrypto))
cs)

nameAlonzoTx :: AlonzoTx era -> String
nameAlonzoTx :: forall era. AlonzoTx era -> String
nameAlonzoTx (AlonzoTx TxBody era
_body TxWits era
_wits IsValid
isV StrictMaybe (TxAuxData era)
_auxdata) = forall a. Show a => a -> String
show IsValid
isV

-- | Run one check
check :: IO ()
check :: IO ()
check = forall prop. Testable prop => prop -> IO ()
quickCheck (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "CERT" e
CERT Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 ConwayTxCert (ConwayEra StandardCrypto) -> String
nameTxCert))

-- | Run a minitrace for every instance of ExecRuleSpec
spec :: Spec
spec :: Spec
spec = do
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"50 MiniTrace tests with trace length of 50" forall a b. (a -> b) -> a -> b
$ do
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"POOL" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "POOL" e
POOL Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 forall c. PoolCert c -> String
namePoolCert))
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"DELEG" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "DELEG" e
DELEG Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 forall c. ConwayDelegCert c -> String
nameDelegCert))
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"GOVCERT" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "GOVCERT" e
GOVCERT Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 forall c. ConwayGovCert c -> String
nameGovCert))
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"CERT" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "CERT" e
CERT Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 ConwayTxCert (ConwayEra StandardCrypto) -> String
nameTxCert))
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"CERTS" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "CERTS" e
CERTS Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 Seq (ConwayTxCert (ConwayEra StandardCrypto)) -> String
nameCerts))
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"RATIFY" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "RATIFY" e
RATIFY Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 forall era. RatifySignal era -> String
nameRatify))
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"ENACT" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "ENACT" e
ENACT Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 forall era. EnactSignal era -> String
nameEnact))
    -- These properties do not have working 'signalSpec' Specifications yet.
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"GOV" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "GOV" e
GOV Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 GovSignal (ConwayEra StandardCrypto) -> String
nameGovSignal))
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"UTXO" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "UTXO" e
UTXO Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 forall era. AlonzoTx era -> String
nameAlonzoTx))
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"EPOCH" (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "EPOCH" e
EPOCH Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 EpochNo -> String
nameEpoch))
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop
      String
"NEWEPOCH"
      (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (s :: Symbol) e.
(ExecSpecRule ConwayFn s e,
 ExecState ConwayFn s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Proxy ConwayFn
-> Int
-> (Signal (EraRule s e) -> String)
-> Gen Property
minitraceProp (forall e. Proof e -> WitRule "NEWEPOCH" e
NEWEPOCH Proof (ConwayEra StandardCrypto)
Conway) (forall {k} (t :: k). Proxy t
Proxy @ConwayFn) Int
50 EpochNo -> String
nameEpoch))