{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Test.Cardano.Ledger.Conformance.ConformanceSpec (spec) where
import Cardano.Ledger.Hashes (ADDRHASH)
import Cardano.Ledger.TxIn (TxId)
import Data.List (isInfixOf)
import Data.Typeable (Proxy (..), Typeable, typeRep)
import Test.Cardano.Ledger.Common
import Test.Cardano.Ledger.Conformance (
SpecNormalize (..),
SpecTranslate (..),
hashToInteger,
integerToHash,
runSpecTransM,
)
import Test.Cardano.Ledger.Conformance.Spec.Conway ()
import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (vkeyFromInteger, vkeyToInteger)
hashDisplayProp ::
forall a.
( Typeable a
, Arbitrary a
, SpecTranslate () a
, SpecNormalize (SpecRep a)
, ToExpr (SpecRep a)
, ToExpr a
) =>
Spec
hashDisplayProp :: forall a.
(Typeable a, Arbitrary a, SpecTranslate () a,
SpecNormalize (SpecRep a), ToExpr (SpecRep a), ToExpr a) =>
Spec
hashDisplayProp = String -> Gen Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop (TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> TypeRep -> String
forall a b. (a -> b) -> a -> b
$ Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Gen Property -> Spec) -> Gen Property -> Spec
forall a b. (a -> b) -> a -> b
$ do
a
someHash <- forall a. Arbitrary a => Gen a
arbitrary @a
let
specRes :: SpecRep a
specRes =
case () -> SpecTransM () (SpecRep a) -> Either Text (SpecRep a)
forall ctx a. ctx -> SpecTransM ctx a -> Either Text a
runSpecTransM () (SpecRep a -> SpecRep a
forall a. SpecNormalize a => a -> a
specNormalize (SpecRep a -> SpecRep a)
-> SpecTransM () (SpecRep a) -> SpecTransM () (SpecRep a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> SpecTransM () (SpecRep a)
forall ctx a.
SpecTranslate ctx a =>
a -> SpecTransM ctx (SpecRep a)
toSpecRep a
someHash) of
Left Text
e -> String -> SpecRep a
forall a. HasCallStack => String -> a
error (String -> SpecRep a) -> String -> SpecRep a
forall a b. (a -> b) -> a -> b
$ String
"Failed to translate hash: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
forall a. Show a => a -> String
show Text
e
Right SpecRep a
x -> SpecRep a
x
Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
(Property -> Gen Property)
-> (Bool -> Property) -> Bool -> Gen Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"impl expr: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. ToExpr a => a -> String
showExpr a
someHash)
(Property -> Property) -> (Bool -> Property) -> Bool -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"spec expr: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> SpecRep a -> String
forall a. ToExpr a => a -> String
showExpr SpecRep a
specRes)
(Bool -> Gen Property) -> Bool -> Gen Property
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'"') ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'"') (SpecRep a -> String
forall a. ToExpr a => a -> String
showExpr SpecRep a
specRes)) String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` a -> String
forall a. ToExpr a => a -> String
showExpr a
someHash
spec :: Spec
spec :: Spec
spec =
String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Translation" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Hashes are displayed in the same way in the implementation and in the spec" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
forall a.
(Typeable a, Arbitrary a, SpecTranslate () a,
SpecNormalize (SpecRep a), ToExpr (SpecRep a), ToExpr a) =>
Spec
hashDisplayProp @TxId
String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Utility properties" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
String -> (VKey Any -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"vkeyToInteger and vkeyFromInteger are inverses" ((VKey Any -> Property) -> Spec) -> (VKey Any -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$
\VKey Any
vk -> TxId -> Maybe (VKey Any)
forall (kd :: KeyRole). TxId -> Maybe (VKey kd)
vkeyFromInteger (VKey Any -> TxId
forall (kd :: KeyRole). VKey kd -> TxId
vkeyToInteger VKey Any
vk) Maybe (VKey Any) -> Maybe (VKey Any) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== VKey Any -> Maybe (VKey Any)
forall a. a -> Maybe a
Just VKey Any
vk
String -> (Hash ADDRHASH Any -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"hashToInteger and integerToHash are inverses" ((Hash ADDRHASH Any -> Property) -> Spec)
-> (Hash ADDRHASH Any -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$
\Hash ADDRHASH Any
h -> TxId -> Maybe (Hash ADDRHASH Any)
forall h a. HashAlgorithm h => TxId -> Maybe (Hash h a)
integerToHash (forall a b. Hash a b -> TxId
hashToInteger @ADDRHASH Hash ADDRHASH Any
h) Maybe (Hash ADDRHASH Any) -> Maybe (Hash ADDRHASH Any) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Hash ADDRHASH Any -> Maybe (Hash ADDRHASH Any)
forall a. a -> Maybe a
Just Hash ADDRHASH Any
h