{-# 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
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"MiniTrace" Spec
MiniTrace.spec
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Generators" (Spec -> Spec) -> Spec -> Spec
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
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Conformance" (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
$ 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
      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
$ 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
      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
$ 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
      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
$ 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
    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
$ 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
      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
$ 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
      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
$ 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
      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
$ 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
      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
$ 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
      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
$ 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
      -- 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
$ 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
      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
$ 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
      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
$ 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
      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
$ 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
    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