{-# 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.Constrained.Conway
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 (fn :: Univ) (rule :: Symbol) era.
ExecSpecRule fn rule era =>
Int -> Spec
inputsGenerateWithin @ConwayFn @"GOV" @ConwayEra Int
60_000_000
    forall (fn :: Univ) (rule :: Symbol) era.
ExecSpecRule fn rule era =>
Int -> Spec
inputsGenerateWithin @ConwayFn @"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) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"RATIFY" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"EPOCH" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"NEWEPOCH" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @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) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"GOVCERT" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"POOL" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"CERT" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"CERTS" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"GOV" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @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) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"UTXOW" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"LEDGER" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @ConwayEra
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop String
"LEDGERS" forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (fn :: Univ) era.
(ShelleyEraImp era, ExecSpecRule fn rule era,
 ForAllExecSpecRep NFData fn rule era,
 ForAllExecSpecRep ToExpr fn rule era,
 NFData (SpecRep (PredicateFailure (EraRule rule era))),
 NFData (ExecContext fn rule era),
 ToExpr (SpecRep (PredicateFailure (EraRule rule era))),
 ToExpr (ExecContext fn rule era),
 SpecTranslate (ExecContext fn rule era) (State (EraRule rule era)),
 Eq (SpecRep (PredicateFailure (EraRule rule era))),
 Inject (State (EraRule rule era)) (ExecState fn rule era),
 Eq (SpecRep (ExecState fn rule era)),
 SpecTranslate (ExecContext fn rule era) (ExecState fn rule era),
 FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))),
 FixupSpecRep (SpecRep (ExecState fn rule era)),
 EncCBOR (ExecContext fn 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" @ConwayFn @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