{-# 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.CertState
import Cardano.Ledger.Compactible
import Cardano.Ledger.Core
import Cardano.Ledger.EpochBoundary
import Cardano.Ledger.Keys.Bootstrap
import Cardano.Ledger.UTxO
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 =
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @t)) 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 =
  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 =
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @t)) 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 =
  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 =
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @(t era))) 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 =
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @(t era))) 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 =
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @t)) 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 =
  forall t.
(Show t, Eq t, Typeable t, HasCallStack) =>
Trip t t -> Version -> Version -> t -> Expectation
roundTripRangeExpectation
    (forall a b. (a -> Encoding) -> (forall s. Decoder s b) -> Trip a b
mkTrip forall a. EncCBOR a => a -> Encoding
encCBOR 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 =
  forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @(t era))) 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
  , 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)
  , HasCallStack
  ) =>
  Spec
roundTripCoreEraTypesSpec :: forall era.
(EraTx 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), HasCallStack) =>
Spec
roundTripCoreEraTypesSpec = do
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Core Type Families" 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, ToCBOR t, DecCBOR (Annotator t),
 Arbitrary t, HasCallStack) =>
Spec
roundTripAnnEraSpec @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, ToCBOR t, DecCBOR (Annotator t),
 Arbitrary t, HasCallStack) =>
Spec
roundTripAnnEraSpec @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 a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Core State Types" forall a b. (a -> b) -> a -> b
$ do
    forall era t.
(Era era, Show t, Eq t, ToCBOR t, DecCBOR (Annotator t),
 Arbitrary t, HasCallStack) =>
Spec
roundTripAnnEraSpec @era @BootstrapWitness
    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 @VState
    forall era (t :: * -> *).
(Era era, Show (t era), Eq (t era), EncCBOR (t era),
 DecShareCBOR (t era), Arbitrary (t era), HasCallStack) =>
Spec
roundTripShareEraTypeSpec @era @CertState
    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 = 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 = 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 forall {k} (t :: k). Proxy t
Proxy 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 =
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Predicate Failures" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rs' :: [Symbol]). EraRuleProof era rs' -> Spec
go 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 = 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)
      forall (rs' :: [Symbol]). EraRuleProof era rs' -> Spec
go EraRuleProof era xs
x