{-# 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
      -- UTXO is disabled due to: https://github.com/IntersectMBO/cardano-ledger/issues/4876
      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