{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Conformance.Spec.Conway (
  spec,
  genFromBundle,
  genFromBundle_,
) where

import Cardano.Ledger.Core (EraRule)
import Constrained.API
import Control.Monad.Cont (ContT (..))
import Control.Monad.Trans (MonadTrans (..))
import Control.State.Transition.Extended (STS (..), TRC (..))
import Data.Map.Strict qualified as Map
import Test.Cardano.Ledger.Conformance (ExecSpecRule (..), ForAllExecTypes, testConformance)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (ConwayCertExecContext (..))
import Test.Cardano.Ledger.Conformance.Imp qualified as Imp (spec)
import Test.Cardano.Ledger.Conformance.Imp.Ratify qualified as RatifyImp
import Test.Cardano.Ledger.Constrained.Conway (genUtxoExecContext)
import Test.Cardano.Ledger.Constrained.Conway.MiniTrace (
  ConstrainedGeneratorBundle (..),
  ConwayCertGenContext (..),
  constrainedCert,
  constrainedCerts,
  constrainedDeleg,
  constrainedEnact,
  constrainedEpoch,
  constrainedGov,
  constrainedGovCert,
  constrainedPool,
  constrainedRatify,
  constrainedUtxo,
 )
import Test.Cardano.Ledger.Conway.ImpTest (ImpTestM, impAnn)
import Test.Cardano.Ledger.Imp.Common
import UnliftIO (MonadIO (..), evaluateDeep)

conformsToImpl ::
  forall rule era.
  ExecSpecRule rule era =>
  Gen (ExecContext rule era, TRC (EraRule rule era)) ->
  Property
conformsToImpl :: forall (rule :: Symbol) era.
ExecSpecRule rule era =>
Gen (ExecContext rule era, TRC (EraRule rule era)) -> Property
conformsToImpl Gen (ExecContext rule era, TRC (EraRule rule era))
genInputs = forall prop. Testable prop => prop -> Property
property @(ImpTestM era Property) (ImpTestM era Property -> Property)
-> (ContT Property (ImpM (LedgerSpec era)) Property
    -> ImpTestM era Property)
-> ContT Property (ImpM (LedgerSpec era)) Property
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ContT Property (ImpM (LedgerSpec era)) Property
-> (Property -> ImpTestM era Property) -> ImpTestM era Property
forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
`runContT` Property -> ImpTestM era Property
forall a. a -> ImpM (LedgerSpec era) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) (ContT Property (ImpM (LedgerSpec era)) Property -> Property)
-> ContT Property (ImpM (LedgerSpec era)) Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  let
    deepEvalAnn :: String -> String
deepEvalAnn String
s = String
"Deep evaluating " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
s
    deepEval :: a -> String -> t (ImpM t) ()
deepEval a
x String
s = do
      a
_ <- ImpM t a -> t (ImpM t) a
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ImpM t a -> t (ImpM t) a) -> ImpM t a -> t (ImpM t) a
forall a b. (a -> b) -> a -> b
$ String -> ImpM t a -> ImpM t a
forall a t. NFData a => String -> ImpM t a -> ImpM t a
impAnn (String -> String
deepEvalAnn String
s) (IO a -> ImpM t a
forall a. IO a -> ImpM t a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (a -> IO a
forall (m :: * -> *) a. (MonadIO m, NFData a) => a -> m a
evaluateDeep a
x))
      () -> t (ImpM t) ()
forall a. a -> t (ImpM t) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  (ExecContext rule era
ctx, trc :: TRC (EraRule rule era)
trc@(TRC (Environment (EraRule rule era)
env, State (EraRule rule era)
st, Signal (EraRule rule era)
sig))) <- ImpM
  (LedgerSpec era) (ExecContext rule era, TRC (EraRule rule era))
-> ContT
     Property
     (ImpM (LedgerSpec era))
     (ExecContext rule era, TRC (EraRule rule era))
forall (m :: * -> *) a. Monad m => m a -> ContT Property m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ImpM
   (LedgerSpec era) (ExecContext rule era, TRC (EraRule rule era))
 -> ContT
      Property
      (ImpM (LedgerSpec era))
      (ExecContext rule era, TRC (EraRule rule era)))
-> ImpM
     (LedgerSpec era) (ExecContext rule era, TRC (EraRule rule era))
-> ContT
     Property
     (ImpM (LedgerSpec era))
     (ExecContext rule era, TRC (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ Gen (ExecContext rule era, TRC (EraRule rule era))
-> ImpM
     (LedgerSpec era) (ExecContext rule era, TRC (EraRule rule era))
forall a. Gen a -> ImpM (LedgerSpec era) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen Gen (ExecContext rule era, TRC (EraRule rule era))
genInputs
  ExecContext rule era
-> String -> ContT Property (ImpM (LedgerSpec era)) ()
forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval ExecContext rule era
ctx String
"context"
  Environment (EraRule rule era)
-> String -> ContT Property (ImpM (LedgerSpec era)) ()
forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval Environment (EraRule rule era)
env String
"environment"
  State (EraRule rule era)
-> String -> ContT Property (ImpM (LedgerSpec era)) ()
forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval State (EraRule rule era)
st String
"state"
  Signal (EraRule rule era)
-> String -> ContT Property (ImpM (LedgerSpec era)) ()
forall {t :: (* -> *) -> * -> *} {t} {a}.
(Monad (t (ImpM t)), MonadTrans t, NFData a) =>
a -> String -> t (ImpM t) ()
deepEval Signal (EraRule rule era)
sig String
"signal"
  Property -> ContT Property (ImpM (LedgerSpec era)) Property
forall a. a -> ContT Property (ImpM (LedgerSpec era)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> ContT Property (ImpM (LedgerSpec era)) Property)
-> Property -> ContT Property (ImpM (LedgerSpec era)) Property
forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(HasCallStack, ExecSpecRule rule era) =>
ExecContext rule era -> TRC (EraRule rule era) -> Property
testConformance @rule @era ExecContext rule era
ctx TRC (EraRule rule era)
trc

genFromBundle_ ::
  ( HasSpec (Environment (EraRule rule era))
  , HasSpec (State (EraRule rule era))
  , HasSpec (Signal (EraRule rule era))
  , Arbitrary (ExecContext rule era)
  ) =>
  ConstrainedGeneratorBundle ctx rule era ->
  Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle_ :: forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era
-> Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle_ ConstrainedGeneratorBundle ctx rule era
x = ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
forall (rule :: Symbol) era ctx.
ForAllExecTypes HasSpec rule era =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle ConstrainedGeneratorBundle ctx rule era
x ((ctx
  -> Environment (EraRule rule era)
  -> State (EraRule rule era)
  -> Signal (EraRule rule era)
  -> Gen (ExecContext rule era))
 -> Gen (ExecContext rule era, TRC (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ \ctx
_ Environment (EraRule rule era)
_ State (EraRule rule era)
_ Signal (EraRule rule era)
_ -> Gen (ExecContext rule era)
forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary

genFromBundle ::
  ForAllExecTypes HasSpec rule era =>
  ConstrainedGeneratorBundle ctx rule era ->
  ( ctx ->
    Environment (EraRule rule era) ->
    State (EraRule rule era) ->
    Signal (EraRule rule era) ->
    Gen (ExecContext rule era)
  ) ->
  Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle :: forall (rule :: Symbol) era ctx.
ForAllExecTypes HasSpec rule era =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle ConstrainedGeneratorBundle {Gen ctx
ctx -> Specification (Environment (EraRule rule era))
ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbContextGen :: Gen ctx
cgbEnvironmentSpec :: ctx -> Specification (Environment (EraRule rule era))
cgbStateSpec :: ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbSignalSpec :: ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbContextGen :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era -> Gen ctx
cgbEnvironmentSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx -> Specification (Environment (EraRule rule era))
cgbStateSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbSignalSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
..} ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Gen (ExecContext rule era)
genExecContext = do
  ctx
ctx <- Gen ctx
cgbContextGen
  Environment (EraRule rule era)
env <- Specification (Environment (EraRule rule era))
-> Gen (Environment (EraRule rule era))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (Specification (Environment (EraRule rule era))
 -> Gen (Environment (EraRule rule era)))
-> Specification (Environment (EraRule rule era))
-> Gen (Environment (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ ctx -> Specification (Environment (EraRule rule era))
cgbEnvironmentSpec ctx
ctx
  State (EraRule rule era)
st <- Specification (State (EraRule rule era))
-> Gen (State (EraRule rule era))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (Specification (State (EraRule rule era))
 -> Gen (State (EraRule rule era)))
-> Specification (State (EraRule rule era))
-> Gen (State (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbStateSpec ctx
ctx Environment (EraRule rule era)
env
  Signal (EraRule rule era)
sig <- Specification (Signal (EraRule rule era))
-> Gen (Signal (EraRule rule era))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (Specification (Signal (EraRule rule era))
 -> Gen (Signal (EraRule rule era)))
-> Specification (Signal (EraRule rule era))
-> Gen (Signal (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbSignalSpec ctx
ctx Environment (EraRule rule era)
env State (EraRule rule era)
st
  (,(Environment (EraRule rule era), State (EraRule rule era),
 Signal (EraRule rule era))
-> TRC (EraRule rule era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment (EraRule rule era)
env, State (EraRule rule era)
st, Signal (EraRule rule era)
sig)) (ExecContext rule era
 -> (ExecContext rule era, TRC (EraRule rule era)))
-> Gen (ExecContext rule era)
-> Gen (ExecContext rule era, TRC (EraRule rule era))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Gen (ExecContext rule era)
genExecContext ctx
ctx Environment (EraRule rule era)
env State (EraRule rule era)
st Signal (EraRule rule era)
sig

conformsToImplConstrained ::
  forall ctx rule era.
  ( ExecSpecRule rule era
  , ForAllExecTypes HasSpec rule era
  ) =>
  ConstrainedGeneratorBundle ctx rule era ->
  ( ctx ->
    Environment (EraRule rule era) ->
    State (EraRule rule era) ->
    Signal (EraRule rule era) ->
    Gen (ExecContext rule era)
  ) ->
  Property
conformsToImplConstrained :: forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle ctx rule era
bundle ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Gen (ExecContext rule era)
genExecContext =
  forall (rule :: Symbol) era.
ExecSpecRule rule era =>
Gen (ExecContext rule era, TRC (EraRule rule era)) -> Property
conformsToImpl @rule @era (Gen (ExecContext rule era, TRC (EraRule rule era)) -> Property)
-> Gen (ExecContext rule era, TRC (EraRule rule era)) -> Property
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
forall (rule :: Symbol) era ctx.
ForAllExecTypes HasSpec rule era =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Gen (ExecContext rule era, TRC (EraRule rule era))
genFromBundle ConstrainedGeneratorBundle ctx rule era
bundle ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Signal (EraRule rule era)
-> Gen (ExecContext rule era)
genExecContext

conformsToImplConstrained_ ::
  ( ExecSpecRule rule era
  , ForAllExecTypes HasSpec rule era
  , Arbitrary (ExecContext rule era)
  ) =>
  ConstrainedGeneratorBundle ctx rule era ->
  Property
conformsToImplConstrained_ :: forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle ctx rule era
bundle = ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle ctx rule era
bundle ((ctx
  -> Environment (EraRule rule era)
  -> State (EraRule rule era)
  -> Signal (EraRule rule era)
  -> Gen (ExecContext rule era))
 -> Property)
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
forall a b. (a -> b) -> a -> b
$ \ctx
_ Environment (EraRule rule era)
_ State (EraRule rule era)
_ Signal (EraRule rule era)
_ -> Gen (ExecContext rule era)
forall a (m :: * -> *). (Arbitrary a, MonadGen m) => m a
arbitrary

spec :: Spec
spec :: Spec
spec = do
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Conformance with constrained generators" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Ticks transition graph" (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
"ENACT" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
        ConstrainedGeneratorBundle EpochNo "ENACT" ConwayEra
-> (EpochNo
    -> Environment (EraRule "ENACT" ConwayEra)
    -> State (EraRule "ENACT" ConwayEra)
    -> Signal (EraRule "ENACT" ConwayEra)
    -> Gen (ExecContext "ENACT" ConwayEra))
-> Property
forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle EpochNo "ENACT" ConwayEra
constrainedEnact ((EpochNo
  -> Environment (EraRule "ENACT" ConwayEra)
  -> State (EraRule "ENACT" ConwayEra)
  -> Signal (EraRule "ENACT" ConwayEra)
  -> Gen (ExecContext "ENACT" ConwayEra))
 -> Property)
-> (EpochNo
    -> Environment (EraRule "ENACT" ConwayEra)
    -> State (EraRule "ENACT" ConwayEra)
    -> Signal (EraRule "ENACT" ConwayEra)
    -> Gen (ExecContext "ENACT" ConwayEra))
-> Property
forall a b. (a -> b) -> a -> b
$
          \EpochNo
curEpoch Environment (EraRule "ENACT" ConwayEra)
_ State (EraRule "ENACT" ConwayEra)
_ Signal (EraRule "ENACT" ConwayEra)
_ -> EpochNo -> Gen EpochNo
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EpochNo
curEpoch
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"RATIFY" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle
  [GovActionState ConwayEra] "RATIFY" ConwayEra
-> Property
forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle
  [GovActionState ConwayEra] "RATIFY" ConwayEra
constrainedRatify
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"EPOCH" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra -> Property
forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra
constrainedEpoch
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"NEWEPOCH" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra -> Property
forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra
constrainedEpoch
    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Blocks transition graph" (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
"DELEG" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
        ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "DELEG"
  ConwayEra
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "DELEG" ConwayEra)
    -> State (EraRule "DELEG" ConwayEra)
    -> Signal (EraRule "DELEG" ConwayEra)
    -> Gen (ExecContext "DELEG" ConwayEra))
-> Property
forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "DELEG"
  ConwayEra
constrainedDeleg (((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  -> Environment (EraRule "DELEG" ConwayEra)
  -> State (EraRule "DELEG" ConwayEra)
  -> Signal (EraRule "DELEG" ConwayEra)
  -> Gen (ExecContext "DELEG" ConwayEra))
 -> Property)
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "DELEG" ConwayEra)
    -> State (EraRule "DELEG" ConwayEra)
    -> Signal (EraRule "DELEG" ConwayEra)
    -> Gen (ExecContext "DELEG" ConwayEra))
-> Property
forall a b. (a -> b) -> a -> b
$
          \(WitUniv ConwayEra
_, ConwayCertGenContext {Map RewardAccount Coin
Map (Credential 'DRepRole) (Set (Credential 'Staking))
VotingProcedures ConwayEra
ccccWithdrawals :: Map RewardAccount Coin
ccccVotes :: VotingProcedures ConwayEra
ccccDelegatees :: Map (Credential 'DRepRole) (Set (Credential 'Staking))
ccccWithdrawals :: forall era. ConwayCertGenContext era -> Map RewardAccount Coin
ccccVotes :: forall era. ConwayCertGenContext era -> VotingProcedures era
ccccDelegatees :: forall era.
ConwayCertGenContext era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
..}) Environment (EraRule "DELEG" ConwayEra)
_ State (EraRule "DELEG" ConwayEra)
_ Signal (EraRule "DELEG" ConwayEra)
_ -> ExecContext "DELEG" ConwayEra
-> Gen (ExecContext "DELEG" ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecContext "DELEG" ConwayEra
 -> Gen (ExecContext "DELEG" ConwayEra))
-> ExecContext "DELEG" ConwayEra
-> Gen (ExecContext "DELEG" ConwayEra)
forall a b. (a -> b) -> a -> b
$ Map (Credential 'DRepRole) (Set (Credential 'Staking))
-> Set (Credential 'DRepRole)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'DRepRole) (Set (Credential 'Staking))
ccccDelegatees
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"GOVCERT" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "GOVCERT"
  ConwayEra
-> Property
forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "GOVCERT"
  ConwayEra
constrainedGovCert
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"POOL" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle (WitUniv ConwayEra) "POOL" ConwayEra
-> Property
forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle (WitUniv ConwayEra) "POOL" ConwayEra
constrainedPool
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"CERT" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERT"
  ConwayEra
-> Property
forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERT"
  ConwayEra
constrainedCert
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"CERTS" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
        ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERTS"
  ConwayEra
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "CERTS" ConwayEra)
    -> State (EraRule "CERTS" ConwayEra)
    -> Signal (EraRule "CERTS" ConwayEra)
    -> Gen (ExecContext "CERTS" ConwayEra))
-> Property
forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERTS"
  ConwayEra
constrainedCerts (((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  -> Environment (EraRule "CERTS" ConwayEra)
  -> State (EraRule "CERTS" ConwayEra)
  -> Signal (EraRule "CERTS" ConwayEra)
  -> Gen (ExecContext "CERTS" ConwayEra))
 -> Property)
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "CERTS" ConwayEra)
    -> State (EraRule "CERTS" ConwayEra)
    -> Signal (EraRule "CERTS" ConwayEra)
    -> Gen (ExecContext "CERTS" ConwayEra))
-> Property
forall a b. (a -> b) -> a -> b
$
          \(WitUniv ConwayEra
_, ConwayCertGenContext {Map RewardAccount Coin
Map (Credential 'DRepRole) (Set (Credential 'Staking))
VotingProcedures ConwayEra
ccccWithdrawals :: forall era. ConwayCertGenContext era -> Map RewardAccount Coin
ccccVotes :: forall era. ConwayCertGenContext era -> VotingProcedures era
ccccDelegatees :: forall era.
ConwayCertGenContext era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
ccccWithdrawals :: Map RewardAccount Coin
ccccVotes :: VotingProcedures ConwayEra
ccccDelegatees :: Map (Credential 'DRepRole) (Set (Credential 'Staking))
..}) Environment (EraRule "CERTS" ConwayEra)
_ State (EraRule "CERTS" ConwayEra)
_ Signal (EraRule "CERTS" ConwayEra)
_ ->
            ExecContext "CERTS" ConwayEra
-> Gen (ExecContext "CERTS" ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecContext "CERTS" ConwayEra
 -> Gen (ExecContext "CERTS" ConwayEra))
-> ExecContext "CERTS" ConwayEra
-> Gen (ExecContext "CERTS" ConwayEra)
forall a b. (a -> b) -> a -> b
$
              ConwayCertExecContext
                { ccecVotes :: VotingProcedures ConwayEra
ccecVotes = VotingProcedures ConwayEra
ccccVotes
                , ccecWithdrawals :: Map RewardAccount Coin
ccecWithdrawals = Map RewardAccount Coin
ccccWithdrawals
                }
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"GOV" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle () "GOV" ConwayEra -> Property
forall (rule :: Symbol) era ctx.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle () "GOV" ConwayEra
constrainedGov
      -- UTXO is disabled due to: https://github.com/IntersectMBO/cardano-ledger/issues/4876
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"UTXO" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> State (EraRule "UTXO" ConwayEra)
    -> Signal (EraRule "UTXO" ConwayEra)
    -> Gen (ExecContext "UTXO" ConwayEra))
-> Property
forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
constrainedUtxo ((UtxoExecContext ConwayEra
  -> Environment (EraRule "UTXO" ConwayEra)
  -> State (EraRule "UTXO" ConwayEra)
  -> Signal (EraRule "UTXO" ConwayEra)
  -> Gen (ExecContext "UTXO" ConwayEra))
 -> Property)
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> State (EraRule "UTXO" ConwayEra)
    -> Signal (EraRule "UTXO" ConwayEra)
    -> Gen (ExecContext "UTXO" ConwayEra))
-> Property
forall a b. (a -> b) -> a -> b
$ \UtxoExecContext ConwayEra
_ Environment (EraRule "UTXO" ConwayEra)
_ State (EraRule "UTXO" ConwayEra)
_ Signal (EraRule "UTXO" ConwayEra)
_ -> Gen (ExecContext "UTXO" ConwayEra)
Gen (UtxoExecContext ConwayEra)
genUtxoExecContext
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"UTXOW" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> State (EraRule "UTXO" ConwayEra)
    -> Signal (EraRule "UTXO" ConwayEra)
    -> Gen (ExecContext "UTXO" ConwayEra))
-> Property
forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
constrainedUtxo ((UtxoExecContext ConwayEra
  -> Environment (EraRule "UTXO" ConwayEra)
  -> State (EraRule "UTXO" ConwayEra)
  -> Signal (EraRule "UTXO" ConwayEra)
  -> Gen (ExecContext "UTXO" ConwayEra))
 -> Property)
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> State (EraRule "UTXO" ConwayEra)
    -> Signal (EraRule "UTXO" ConwayEra)
    -> Gen (ExecContext "UTXO" ConwayEra))
-> Property
forall a b. (a -> b) -> a -> b
$ \UtxoExecContext ConwayEra
_ Environment (EraRule "UTXO" ConwayEra)
_ State (EraRule "UTXO" ConwayEra)
_ Signal (EraRule "UTXO" ConwayEra)
_ -> Gen (ExecContext "UTXO" ConwayEra)
Gen (UtxoExecContext ConwayEra)
genUtxoExecContext
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"LEDGER" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> State (EraRule "UTXO" ConwayEra)
    -> Signal (EraRule "UTXO" ConwayEra)
    -> Gen (ExecContext "UTXO" ConwayEra))
-> Property
forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
constrainedUtxo ((UtxoExecContext ConwayEra
  -> Environment (EraRule "UTXO" ConwayEra)
  -> State (EraRule "UTXO" ConwayEra)
  -> Signal (EraRule "UTXO" ConwayEra)
  -> Gen (ExecContext "UTXO" ConwayEra))
 -> Property)
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> State (EraRule "UTXO" ConwayEra)
    -> Signal (EraRule "UTXO" ConwayEra)
    -> Gen (ExecContext "UTXO" ConwayEra))
-> Property
forall a b. (a -> b) -> a -> b
$ \UtxoExecContext ConwayEra
_ Environment (EraRule "UTXO" ConwayEra)
_ State (EraRule "UTXO" ConwayEra)
_ Signal (EraRule "UTXO" ConwayEra)
_ -> Gen (ExecContext "UTXO" ConwayEra)
Gen (UtxoExecContext ConwayEra)
genUtxoExecContext
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"LEDGERS" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$ ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> State (EraRule "UTXO" ConwayEra)
    -> Signal (EraRule "UTXO" ConwayEra)
    -> Gen (ExecContext "UTXO" ConwayEra))
-> Property
forall ctx (rule :: Symbol) era.
(ExecSpecRule rule era, ForAllExecTypes HasSpec rule era) =>
ConstrainedGeneratorBundle ctx rule era
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Signal (EraRule rule era)
    -> Gen (ExecContext rule era))
-> Property
conformsToImplConstrained ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
constrainedUtxo ((UtxoExecContext ConwayEra
  -> Environment (EraRule "UTXO" ConwayEra)
  -> State (EraRule "UTXO" ConwayEra)
  -> Signal (EraRule "UTXO" ConwayEra)
  -> Gen (ExecContext "UTXO" ConwayEra))
 -> Property)
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> State (EraRule "UTXO" ConwayEra)
    -> Signal (EraRule "UTXO" ConwayEra)
    -> Gen (ExecContext "UTXO" ConwayEra))
-> Property
forall a b. (a -> b) -> a -> b
$ \UtxoExecContext ConwayEra
_ Environment (EraRule "UTXO" ConwayEra)
_ State (EraRule "UTXO" ConwayEra)
_ Signal (EraRule "UTXO" ConwayEra)
_ -> Gen (ExecContext "UTXO" ConwayEra)
Gen (UtxoExecContext ConwayEra)
genUtxoExecContext
    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"ImpTests" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      Spec
RatifyImp.spec
      Spec
Imp.spec