{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE TypeApplications #-}
module Test.Cardano.Ledger.Conformance.Spec.Conway (spec) where
import Cardano.Ledger.Conway (ConwayEra)
import Test.Cardano.Ledger.Conformance (conformsToImpl, inputsGenerateWithin)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway ()
import Test.Cardano.Ledger.Conformance.ExecSpecRule.MiniTrace qualified as MiniTrace
import Test.Cardano.Ledger.Conformance.Imp qualified as Imp (spec)
import Test.Cardano.Ledger.Conformance.Imp.Ratify qualified as RatifyImp
import Test.Cardano.Ledger.Conway.ImpTest ()
import Test.Cardano.Ledger.Imp.Common
spec :: Spec
spec :: Spec
spec = do
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"MiniTrace" Spec
MiniTrace.spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Generators" forall a b. (a -> b) -> a -> b
$ do
forall (rule :: Symbol) era. ExecSpecRule rule era => Int -> Spec
inputsGenerateWithin @"GOV" @ConwayEra Int
60_000_000
forall (rule :: Symbol) era. ExecSpecRule rule era => Int -> Spec
inputsGenerateWithin @"ENACT" @ConwayEra Int
60_000_000
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Conformance" forall a b. (a -> b) -> a -> b
$ do
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Ticks transition graph" forall a b. (a -> b) -> a -> b
$ do
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"ENACT" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"ENACT" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"RATIFY" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"RATIFY" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"EPOCH" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"EPOCH" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"NEWEPOCH" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"NEWEPOCH" @ConwayEra
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Blocks transition graph" forall a b. (a -> b) -> a -> b
$ do
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"DELEG" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"DELEG" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"GOVCERT" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"GOVCERT" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"POOL" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"POOL" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"CERT" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"CERT" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"CERTS" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"CERTS" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"GOV" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"GOV" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"UTXO" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"UTXO" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"UTXOW" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"UTXOW" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"LEDGER" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"LEDGER" @ConwayEra
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"LEDGERS" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) era.
(ShelleyEraImp era, ExecSpecRule rule era,
ForAllExecSpecRep NFData rule era,
ForAllExecSpecRep ToExpr rule era,
NFData (SpecRep (PredicateFailure (EraRule rule era))),
NFData (ExecContext rule era),
ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
ToExpr (ExecContext rule era),
SpecTranslate (ExecContext rule era) (State (EraRule rule era)),
Eq (SpecRep (PredicateFailure (EraRule rule era))),
Inject (State (EraRule rule era)) (ExecState rule era),
Eq (SpecRep (ExecState rule era)),
SpecTranslate (ExecContext rule era) (ExecState rule era),
FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
FixupSpecRep (SpecRep (ExecState rule era)),
EncCBOR (ExecContext rule era),
EncCBOR (Environment (EraRule rule era)),
EncCBOR (State (EraRule rule era)),
EncCBOR (Signal (EraRule rule era)), HasCallStack,
NFData (PredicateFailure (EraRule rule era)),
ToExpr (PredicateFailure (EraRule rule era))) =>
Property
conformsToImpl @"LEDGERS" @ConwayEra
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"ImpTests" forall a b. (a -> b) -> a -> b
$ do
Spec
RatifyImp.spec
Spec
Imp.spec