{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE TypeApplications #-}

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

import Cardano.Ledger.Conway (Conway)
import Test.Cardano.Ledger.Conformance (conformsToImpl, inputsGenerateWithin)
import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway ()
import qualified Test.Cardano.Ledger.Conformance.ExecSpecRule.MiniTrace as MiniTrace
import qualified Test.Cardano.Ledger.Conformance.Imp.Ratify 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" @Conway Int
60_000_000
    forall (fn :: Univ) (rule :: Symbol) era.
ExecSpecRule fn rule era =>
Int -> Spec
inputsGenerateWithin @ConwayFn @"ENACT" @Conway 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) =>
Property
conformsToImpl @"ENACT" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"RATIFY" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"EPOCH" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"NEWEPOCH" @ConwayFn @Conway
    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) =>
Property
conformsToImpl @"DELEG" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"GOVCERT" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"POOL" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"CERT" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"CERTS" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"GOV" @ConwayFn @Conway
      forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop 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) =>
Property
conformsToImpl @"UTXO" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"UTXOW" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"LEDGER" @ConwayFn @Conway
      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) =>
Property
conformsToImpl @"LEDGERS" @ConwayFn @Conway
    forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"ImpTests" forall a b. (a -> b) -> a -> b
$ do
      Spec
RatifyImp.spec