{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Cardano.Ledger.Core.Binary.RoundTrip (
  RuleListEra (..),
  EraRuleProof (..),

  -- * Spec
  roundTripEraSpec,
  roundTripAnnEraSpec,
  roundTripEraTypeSpec,
  roundTripAnnEraTypeSpec,
  roundTripShareEraSpec,
  roundTripShareEraTypeSpec,

  -- * Expectation
  roundTripEraExpectation,
  roundTripEraTypeExpectation,
  roundTripAnnEraExpectation,
  roundTripAnnEraTypeExpectation,
  roundTripShareEraExpectation,
  roundTripShareEraTypeExpectation,
  roundTripCoreEraTypesSpec,
  roundTripAllPredicateFailures,
) where

import Cardano.Ledger.Binary
import Cardano.Ledger.Compactible
import Cardano.Ledger.Core
import Cardano.Ledger.State
import Control.State.Transition.Extended (STS (..))
import Data.Typeable
import GHC.TypeLits (Symbol)
import Test.Cardano.Ledger.Binary.RoundTrip
import Test.Cardano.Ledger.Common
import Test.Cardano.Ledger.Core.Arbitrary ()

-- | QuickCheck property spec that uses `roundTripEraExpectation`
roundTripEraSpec ::
  forall era t.
  (Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t, HasCallStack) =>
  Spec
roundTripEraSpec :: forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec =
  String -> (t -> Expectation) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (TypeRep -> String
forall a. Show a => a -> String
show (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy t -> TypeRep) -> Proxy t -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)) ((t -> Expectation) -> Spec) -> (t -> Expectation) -> Spec
forall a b. (a -> b) -> a -> b
$ forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, HasCallStack) =>
t -> Expectation
roundTripEraExpectation @era @t

-- | Roundtrip CBOR testing for types and type families that implement
-- EncCBOR/DecCBOR. Requires TypeApplication of an @@era@
roundTripEraExpectation ::
  forall era t.
  (Era era, Show t, Eq t, EncCBOR t, DecCBOR t, HasCallStack) =>
  t ->
  Expectation
roundTripEraExpectation :: forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, HasCallStack) =>
t -> Expectation
roundTripEraExpectation =
  Version -> Version -> t -> Expectation
forall t.
(Show t, Eq t, EncCBOR t, DecCBOR t, HasCallStack) =>
Version -> Version -> t -> Expectation
roundTripCborRangeExpectation (forall era. Era era => Version
eraProtVerLow @era) (forall era. Era era => Version
eraProtVerHigh @era)

-- | QuickCheck property spec that uses `roundTripAnnEraExpectation`
roundTripAnnEraSpec ::
  forall era t.
  (Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t), Arbitrary t, HasCallStack) =>
  Spec
roundTripAnnEraSpec :: forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 Arbitrary t, HasCallStack) =>
Spec
roundTripAnnEraSpec =
  String -> (t -> Expectation) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (TypeRep -> String
forall a. Show a => a -> String
show (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy t -> TypeRep) -> Proxy t -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)) ((t -> Expectation) -> Spec) -> (t -> Expectation) -> Spec
forall a b. (a -> b) -> a -> b
$ forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 HasCallStack) =>
t -> Expectation
roundTripAnnEraExpectation @era @t

-- | Similar to `roundTripEraExpectation`, but for Annotator decoders. Note the
-- constraint `ToCBOR` vs `EncCBOR`, this is due to the requirement for memoized types
-- to be already fully encoded.
roundTripAnnEraExpectation ::
  forall era t.
  (Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t), HasCallStack) =>
  t ->
  Expectation
roundTripAnnEraExpectation :: forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 HasCallStack) =>
t -> Expectation
roundTripAnnEraExpectation =
  Version -> Version -> t -> Expectation
forall t.
(Show t, Eq t, ToCBOR t, DecCBOR (Annotator t), HasCallStack) =>
Version -> Version -> t -> Expectation
roundTripAnnRangeExpectation (forall era. Era era => Version
eraProtVerLow @era) (forall era. Era era => Version
eraProtVerHigh @era)

-- | QuickCheck property spec that uses `roundTripEraTypeExpectation`
roundTripEraTypeSpec ::
  forall era t.
  ( Era era
  , Show (t era)
  , Eq (t era)
  , EncCBOR (t era)
  , DecCBOR (t era)
  , Arbitrary (t era)
  , HasCallStack
  ) =>
  Spec
roundTripEraTypeSpec :: forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecCBOR (t era), Arbitrary (t era), HasCallStack) =>
Spec
roundTripEraTypeSpec =
  String -> (t era -> Expectation) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (TypeRep -> String
forall a. Show a => a -> String
show (Proxy (t era) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy (t era) -> TypeRep) -> Proxy (t era) -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(t era))) ((t era -> Expectation) -> Spec) -> (t era -> Expectation) -> Spec
forall a b. (a -> b) -> a -> b
$ forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecCBOR (t era), HasCallStack) =>
t era -> Expectation
roundTripEraTypeExpectation @era @t

-- | Roundtrip CBOR testing for types that implement EncCBOR/DecCBOR. Unlike
-- `roundTripEraExpectation`, this function can't be used with type families, but the
-- types of this function are unambiguous.
roundTripEraTypeExpectation ::
  forall era t.
  (Era era, Show (t era), Eq (t era), EncCBOR (t era), DecCBOR (t era), HasCallStack) =>
  t era ->
  Expectation
roundTripEraTypeExpectation :: forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecCBOR (t era), HasCallStack) =>
t era -> Expectation
roundTripEraTypeExpectation = forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, HasCallStack) =>
t -> Expectation
roundTripEraExpectation @era @(t era)

-- | QuickCheck property spec that uses `roundTripAnnEraTypeExpectation`
roundTripAnnEraTypeSpec ::
  forall era t.
  ( Era era
  , Show (t era)
  , Eq (t era)
  , ToCBOR (t era)
  , DecCBOR (Annotator (t era))
  , Arbitrary (t era)
  , HasCallStack
  ) =>
  Spec
roundTripAnnEraTypeSpec :: forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), ToCBOR (t era),
 DecCBOR (Annotator (t era)), Arbitrary (t era), HasCallStack) =>
Spec
roundTripAnnEraTypeSpec =
  String -> (t era -> Expectation) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (TypeRep -> String
forall a. Show a => a -> String
show (Proxy (t era) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy (t era) -> TypeRep) -> Proxy (t era) -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(t era))) ((t era -> Expectation) -> Spec) -> (t era -> Expectation) -> Spec
forall a b. (a -> b) -> a -> b
$ forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), ToCBOR (t era),
 DecCBOR (Annotator (t era)), HasCallStack) =>
t era -> Expectation
roundTripAnnEraTypeExpectation @era @t

-- | Same as `roundTripAnnEraExpectation`, but is not suitable for type families.
roundTripAnnEraTypeExpectation ::
  forall era t.
  ( Era era
  , Show (t era)
  , Eq (t era)
  , ToCBOR (t era)
  , DecCBOR (Annotator (t era))
  , HasCallStack
  ) =>
  t era ->
  Expectation
roundTripAnnEraTypeExpectation :: forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), ToCBOR (t era),
 DecCBOR (Annotator (t era)), HasCallStack) =>
t era -> Expectation
roundTripAnnEraTypeExpectation = forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 HasCallStack) =>
t -> Expectation
roundTripAnnEraExpectation @era @(t era)

-- | QuickCheck property spec that uses `roundTripShareEraExpectation`
roundTripShareEraSpec ::
  forall era t.
  (Era era, Show t, Eq t, EncCBOR t, DecShareCBOR t, Arbitrary t, HasCallStack) =>
  Spec
roundTripShareEraSpec :: forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecShareCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripShareEraSpec =
  String -> (t -> Expectation) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (TypeRep -> String
forall a. Show a => a -> String
show (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy t -> TypeRep) -> Proxy t -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t)) ((t -> Expectation) -> Spec) -> (t -> Expectation) -> Spec
forall a b. (a -> b) -> a -> b
$ forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecShareCBOR t, HasCallStack) =>
t -> Expectation
roundTripShareEraExpectation @era @t

-- | Roundtrip CBOR testing for types and type families that implement
-- EncCBOR/DecShareCBOR. Requires TypeApplication of an @@era@
roundTripShareEraExpectation ::
  forall era t.
  (Era era, Show t, Eq t, EncCBOR t, DecShareCBOR t, HasCallStack) =>
  t ->
  Expectation
roundTripShareEraExpectation :: forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecShareCBOR t, HasCallStack) =>
t -> Expectation
roundTripShareEraExpectation =
  Trip t t -> Version -> Version -> t -> Expectation
forall t.
(Show t, Eq t, Typeable t, HasCallStack) =>
Trip t t -> Version -> Version -> t -> Expectation
roundTripRangeExpectation
    ((t -> Encoding) -> (forall s. Decoder s t) -> Trip t t
forall a b. (a -> Encoding) -> (forall s. Decoder s b) -> Trip a b
mkTrip t -> Encoding
forall a. EncCBOR a => a -> Encoding
encCBOR Decoder s t
forall s. Decoder s t
forall a s. DecShareCBOR a => Decoder s a
decNoShareCBOR)
    (forall era. Era era => Version
eraProtVerLow @era)
    (forall era. Era era => Version
eraProtVerHigh @era)

-- | QuickCheck property spec that uses `roundTripShareEraTypeExpectation`
roundTripShareEraTypeSpec ::
  forall era t.
  ( Era era
  , Show (t era)
  , Eq (t era)
  , EncCBOR (t era)
  , DecShareCBOR (t era)
  , Arbitrary (t era)
  , HasCallStack
  ) =>
  Spec
roundTripShareEraTypeSpec :: forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecShareCBOR (t era), Arbitrary (t era), HasCallStack) =>
Spec
roundTripShareEraTypeSpec =
  String -> (t era -> Expectation) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (TypeRep -> String
forall a. Show a => a -> String
show (Proxy (t era) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy (t era) -> TypeRep) -> Proxy (t era) -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(t era))) ((t era -> Expectation) -> Spec) -> (t era -> Expectation) -> Spec
forall a b. (a -> b) -> a -> b
$ forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecShareCBOR (t era), HasCallStack) =>
t era -> Expectation
roundTripShareEraTypeExpectation @era @t

-- | Roundtrip CBOR testing for types that implement EncCBOR/DecShareCBOR. Unlike
-- `roundTripShareEraExpectation`, this function can't be used with type families, but the
-- types of this function are unambiguous.
roundTripShareEraTypeExpectation ::
  forall era t.
  (Era era, Show (t era), Eq (t era), EncCBOR (t era), DecShareCBOR (t era), HasCallStack) =>
  t era ->
  Expectation
roundTripShareEraTypeExpectation :: forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecShareCBOR (t era), HasCallStack) =>
t era -> Expectation
roundTripShareEraTypeExpectation = forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecShareCBOR t, HasCallStack) =>
t -> Expectation
roundTripShareEraExpectation @era @(t era)

-- | CBOR RoundTrip spec for all the core types and type families that are parametrized on era.
roundTripCoreEraTypesSpec ::
  forall era.
  ( EraTx era
  , EraCertState era
  , Arbitrary (Tx era)
  , Arbitrary (TxBody era)
  , Arbitrary (TxOut era)
  , Arbitrary (TxCert era)
  , Arbitrary (TxWits era)
  , Arbitrary (TxAuxData era)
  , Arbitrary (Value era)
  , Arbitrary (CompactForm (Value era))
  , Arbitrary (Script era)
  , Arbitrary (PParams era)
  , Arbitrary (PParamsUpdate era)
  , Arbitrary (CertState era)
  , DecCBOR (Script era)
  , DecCBOR (TxAuxData era)
  , DecCBOR (TxWits era)
  , DecCBOR (TxBody era)
  , DecCBOR (Tx era)
  , HasCallStack
  ) =>
  Spec
roundTripCoreEraTypesSpec :: forall era.
(EraTx era, EraCertState era, Arbitrary (Tx era),
 Arbitrary (TxBody era), Arbitrary (TxOut era),
 Arbitrary (TxCert era), Arbitrary (TxWits era),
 Arbitrary (TxAuxData era), Arbitrary (Value era),
 Arbitrary (CompactForm (Value era)), Arbitrary (Script era),
 Arbitrary (PParams era), Arbitrary (PParamsUpdate era),
 Arbitrary (CertState era), DecCBOR (Script era),
 DecCBOR (TxAuxData era), DecCBOR (TxWits era),
 DecCBOR (TxBody era), DecCBOR (Tx era), HasCallStack) =>
Spec
roundTripCoreEraTypesSpec = do
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Core Type Families" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(Value era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(CompactForm (Value era))
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(TxOut era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(TxCert era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(PParams era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(PParamsUpdate era)
    forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 Arbitrary t, HasCallStack) =>
Spec
roundTripAnnEraSpec @era @(Script era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(Script era)
    forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 Arbitrary t, HasCallStack) =>
Spec
roundTripAnnEraSpec @era @(TxAuxData era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(TxAuxData era)
    forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 Arbitrary t, HasCallStack) =>
Spec
roundTripAnnEraSpec @era @(TxWits era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(TxWits era)
    forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 Arbitrary t, HasCallStack) =>
Spec
roundTripAnnEraSpec @era @(TxBody era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(TxBody era)
    forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 Arbitrary t, HasCallStack) =>
Spec
roundTripAnnEraSpec @era @(Tx era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(Tx era)
    String -> (TxOut era -> Expectation) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (String
"MemPack/CBOR Roundtrip " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TypeRep -> String
forall a. Show a => a -> String
show (Proxy (TxOut era) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy (TxOut era) -> TypeRep) -> Proxy (TxOut era) -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(TxOut era))) ((TxOut era -> Expectation) -> Spec)
-> (TxOut era -> Expectation) -> Spec
forall a b. (a -> b) -> a -> b
$
      forall t.
(Show t, Eq t, Typeable t, HasCallStack) =>
Trip t t -> Version -> Version -> t -> Expectation
roundTripRangeExpectation @(TxOut era)
        ((TxOut era -> Encoding)
-> (forall s. Decoder s (TxOut era))
-> Trip (TxOut era) (TxOut era)
forall a b. (a -> Encoding) -> (forall s. Decoder s b) -> Trip a b
mkTrip TxOut era -> Encoding
forall a. MemPack a => a -> Encoding
encodeMemPack Decoder s (TxOut era)
forall s. Decoder s (TxOut era)
forall a s. DecShareCBOR a => Decoder s a
decNoShareCBOR)
        (forall era. Era era => Version
eraProtVerLow @era)
        (forall era. Era era => Version
eraProtVerHigh @era)
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecShareCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripShareEraSpec @era @(CertState era)
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Core State Types" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecShareCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripShareEraSpec @era @SnapShots
    forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecShareCBOR (t era), Arbitrary (t era), HasCallStack) =>
Spec
roundTripShareEraTypeSpec @era @DState
    forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecShareCBOR (t era), Arbitrary (t era), HasCallStack) =>
Spec
roundTripShareEraTypeSpec @era @PState
    forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecShareCBOR (t era), Arbitrary (t era), HasCallStack) =>
Spec
roundTripShareEraTypeSpec @era @CommitteeState
    forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecShareCBOR (t era), Arbitrary (t era), HasCallStack) =>
Spec
roundTripShareEraTypeSpec @era @UTxO

data EraRuleProof era (rs :: [Symbol]) where
  EraRuleProofEmpty :: EraRuleProof era '[]
  EraRuleProofHead ::
    ( Show (EraRuleFailure r era)
    , Eq (EraRuleFailure r era)
    , EncCBOR (EraRuleFailure r era)
    , DecCBOR (EraRuleFailure r era)
    , Arbitrary (EraRuleFailure r era)
    , EraRuleFailure r era ~ PredicateFailure (EraRule r era)
    ) =>
    Proxy r ->
    EraRuleProof era xs ->
    EraRuleProof era (r ': xs)

class UnliftRules era (rs :: [Symbol]) where
  unliftEraRuleProofs :: EraRuleProof era rs

instance UnliftRules era '[] where
  unliftEraRuleProofs :: EraRuleProof era '[]
unliftEraRuleProofs = EraRuleProof era '[]
forall era. EraRuleProof era '[]
EraRuleProofEmpty

instance
  ( Show (EraRuleFailure r era)
  , Eq (EraRuleFailure r era)
  , EncCBOR (EraRuleFailure r era)
  , DecCBOR (EraRuleFailure r era)
  , Arbitrary (EraRuleFailure r era)
  , EraRuleFailure r era ~ PredicateFailure (EraRule r era)
  , UnliftRules era rs
  ) =>
  UnliftRules era (r ': rs)
  where
  unliftEraRuleProofs :: EraRuleProof era (r : rs)
unliftEraRuleProofs = Proxy r -> EraRuleProof era rs -> EraRuleProof era (r : rs)
forall (r :: Symbol) era (xs :: [Symbol]).
(Show (EraRuleFailure r era), Eq (EraRuleFailure r era),
 EncCBOR (EraRuleFailure r era), DecCBOR (EraRuleFailure r era),
 Arbitrary (EraRuleFailure r era),
 EraRuleFailure r era ~ PredicateFailure (EraRule r era)) =>
Proxy r -> EraRuleProof era xs -> EraRuleProof era (r : xs)
EraRuleProofHead Proxy r
forall {k} (t :: k). Proxy t
Proxy EraRuleProof era rs
forall era (rs :: [Symbol]).
UnliftRules era rs =>
EraRuleProof era rs
unliftEraRuleProofs

class
  UnliftRules era (EraRules era) =>
  RuleListEra era
  where
  type EraRules era :: [Symbol]

roundTripAllPredicateFailures ::
  forall era.
  ( RuleListEra era
  , Era era
  , HasCallStack
  ) =>
  Spec
roundTripAllPredicateFailures :: forall era. (RuleListEra era, Era era, HasCallStack) => Spec
roundTripAllPredicateFailures =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Predicate Failures" (Spec -> Spec)
-> (EraRuleProof era (EraRules era) -> Spec)
-> EraRuleProof era (EraRules era)
-> Spec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EraRuleProof era (EraRules era) -> Spec
forall (rs' :: [Symbol]). EraRuleProof era rs' -> Spec
go (EraRuleProof era (EraRules era) -> Spec)
-> EraRuleProof era (EraRules era) -> Spec
forall a b. (a -> b) -> a -> b
$ forall era (rs :: [Symbol]).
UnliftRules era rs =>
EraRuleProof era rs
unliftEraRuleProofs @era @(EraRules era)
  where
    go :: EraRuleProof era rs' -> Spec
    go :: forall (rs' :: [Symbol]). EraRuleProof era rs' -> Spec
go EraRuleProof era rs'
EraRuleProofEmpty = () -> Spec
forall a. a -> SpecM () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    go (EraRuleProofHead (Proxy r
Proxy :: Proxy r) EraRuleProof era xs
x) = do
      forall era t.
(Era era, Show t, Eq t, EncCBOR t, DecCBOR t, Arbitrary t,
 HasCallStack) =>
Spec
roundTripEraSpec @era @(EraRuleFailure r era)
      EraRuleProof era xs -> Spec
forall (rs' :: [Symbol]). EraRuleProof era rs' -> Spec
go EraRuleProof era xs
x