{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}

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

import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..))
import Cardano.Ledger.BaseTypes (Inject (..))
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway.Governance (
  RatifySignal (..),
  VotingProcedures (..),
 )
import Cardano.Ledger.Conway.Rules (GovSignal (..))
import Cardano.Ledger.Core
import Constrained.API
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
-- \| This is where most of the ExecSpecRule instances are defined
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (
  nameCerts,
  nameDelegCert,
  nameEnact,
  nameEpoch,
  nameGovCert,
  namePoolCert,
  nameTxCert,
 )
import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (..))
import Test.Cardano.Ledger.Generic.Proof (Proof (..), WitRule (..), goSTS)
import qualified Test.Cardano.Ledger.Generic.Proof as Proof

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

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

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

minitraceProp ::
  forall s e.
  ( ExecSpecRule s e
  , ExecState s e ~ State (EraRule s e)
  , PrettyA (Signal (EraRule s e))
  , PrettyA (State (EraRule s e))
  ) =>
  WitRule s e ->
  Int ->
  (Signal (EraRule s e) -> String) ->
  Gen Property
minitraceProp :: forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e
-> Int -> (Signal (EraRule s e) -> [Char]) -> Gen Property
minitraceProp WitRule s e
witrule Int
n0 Signal (EraRule s e) -> [Char]
namef = do
  Either [[Char]] [Signal (EraRule s e)]
ans <- forall (s :: Symbol) e.
(ExecSpecRule s e, ExecState s e ~ State (EraRule s e),
 PrettyA (Signal (EraRule s e)), PrettyA (State (EraRule s e))) =>
WitRule s e -> Int -> Gen (Either [[Char]] [Signal (EraRule s e)])
minitraceEither @s @e WitRule s e
witrule Int
n0
  case Either [[Char]] [Signal (EraRule s e)]
ans of
    Left [[Char]]
zs -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([[Char]] -> [Char]
unlines [[Char]]
zs) (Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False)
    Right [Signal (EraRule s e)]
sigs -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ (Signal (EraRule s e) -> [Char])
-> [Signal (EraRule s e)] -> Property -> Property
forall x. (x -> [Char]) -> [x] -> Property -> Property
classifyFirst Signal (EraRule s e) -> [Char]
namef [Signal (EraRule s e)]
sigs (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
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 -> [Char]) -> [x] -> Property -> Property
classifyMany x -> [Char]
_ [] Property
p = Property
p
classifyMany x -> [Char]
f (x
x : [x]
xs) Property
p = (x -> [Char]) -> [x] -> Property -> Property
forall x. (x -> [Char]) -> [x] -> Property -> Property
classifyMany x -> [Char]
f [x]
xs (Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
classify Bool
True (x -> [Char]
f x
x) Property
p)

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

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

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

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

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

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