{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}

module Test.Cardano.Crypto.Signing.Safe (
  tests,
) where

import Cardano.Crypto.Signing (
  noPassSafeSigner,
  safeToVerification,
  toVerification,
 )
import Cardano.Prelude
import Hedgehog (
  Property,
  checkParallel,
  discover,
  forAll,
  property,
  (===),
 )
import Test.Cardano.Crypto.Gen (genSigningKey)

--------------------------------------------------------------------------------
-- Main Test Action
--------------------------------------------------------------------------------

tests :: IO Bool
tests :: IO Bool
tests = Group -> IO Bool
forall (m :: * -> *). MonadIO m => Group -> m Bool
checkParallel $$String
[(PropertyName, Property)]
Property
String -> GroupName
String -> PropertyName
GroupName -> [(PropertyName, Property)] -> Group
discover

--------------------------------------------------------------------------------
-- Safe Signing Properties
--------------------------------------------------------------------------------

-- | Making a 'SafeSigner' from a 'SigningKey' preserves the 'VerificationKey'
--
-- Since SafeSigner was simplified, this is a completely trivial property.
--
-- Definitions:
--
-- > safeToVerification (SafeSigner sk _) = toVerification sk
-- > noPassSafeSigner sk = SafeSigner sk emptyPassphrase
--
-- Theorem:
--
-- > safeToVerification (noPassSafeSigner sk) = toVerification sk
--
-- Proof:
--
-- >   safeToVerification (noPassSafeSigner sk)
-- >
-- > = { by expanding definition of noPassSafeSigner }
-- >
-- >   safeToVerification (SafeSigner sk emptyPassphrase)
-- >
-- > = { by expanding definition of safeToVerification }
-- >
-- >   toVerification sk
prop_safeSignerPreservesVerificationKey :: Property
prop_safeSignerPreservesVerificationKey :: Property
prop_safeSignerPreservesVerificationKey = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  SigningKey
sk <- Gen SigningKey -> PropertyT IO SigningKey
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen SigningKey
genSigningKey
  SafeSigner -> VerificationKey
safeToVerification (SigningKey -> SafeSigner
noPassSafeSigner SigningKey
sk) VerificationKey -> VerificationKey -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== SigningKey -> VerificationKey
toVerification SigningKey
sk