{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

{- HLINT ignore "Use head" -}

module Test.Crypto.KES (
  tests,
)
where

import qualified Data.ByteString as BS
import qualified Data.Foldable as F (foldl')
import Data.IORef
import Data.Proxy (Proxy (..))
import Data.Set (Set)
import qualified Data.Set as Set
import Foreign.Ptr (WordPtr)
import GHC.TypeNats (KnownNat, natVal)

import Control.Monad (void)
import Control.Monad.Class.MonadST
import Control.Monad.Class.MonadThrow
import Control.Monad.IO.Class (liftIO)
import Control.Tracer

import Cardano.Crypto.DSIGN hiding (Signable)
import Cardano.Crypto.DirectSerialise (DirectDeserialise, DirectSerialise)
import Cardano.Crypto.Hash
import Cardano.Crypto.KES
import Cardano.Crypto.Libsodium
import Cardano.Crypto.Libsodium.MLockedSeed
import Cardano.Crypto.PinnedSizedBytes
import Cardano.Crypto.Seed (mkSeedFromBytes)
import Cardano.Crypto.Util (SignableRepresentation (..))

import Test.QuickCheck
import Test.Tasty (TestTree, adjustOption, testGroup)
import Test.Tasty.HUnit (Assertion, assertBool, assertEqual, testCase)
import Test.Tasty.QuickCheck (QuickCheckMaxSize (..), testProperty)

import Test.Crypto.AllocLog
import Test.Crypto.EqST
import Test.Crypto.Instances (withMLockedSeedFromPSB)
import Test.Crypto.Util (
  FromCBOR,
  Lock,
  Message,
  ToCBOR,
  directDeserialiseFromBS,
  directSerialiseToBS,
  doesNotThrow,
  hexBS,
  noExceptionsThrown,
  prop_cbor,
  prop_cbor_direct_vs_class,
  prop_cbor_size,
  prop_cbor_with,
  prop_no_thunks_IO,
  prop_raw_serialise,
  prop_size_serialise,
  withLock,
 )

{- HLINT ignore "Reduce duplication" -}
{- HLINT ignore "Use head" -}

--
-- The list of all tests
--
tests :: Lock -> TestTree
tests :: Lock -> TestTree
tests Lock
lock =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Crypto.KES"
    [ Proxy (SingleKES Ed25519DSIGN) -> TestName -> TestTree
forall v. KESAlgorithm v => Proxy v -> TestName -> TestTree
testKESAlloc (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(SingleKES Ed25519DSIGN)) TestName
"SingleKES"
    , Proxy (Sum1KES Ed25519DSIGN Blake2b_256) -> TestName -> TestTree
forall v. KESAlgorithm v => Proxy v -> TestName -> TestTree
testKESAlloc (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Sum1KES Ed25519DSIGN Blake2b_256)) TestName
"Sum1KES"
    , Proxy (Sum2KES Ed25519DSIGN Blake2b_256) -> TestName -> TestTree
forall v. KESAlgorithm v => Proxy v -> TestName -> TestTree
testKESAlloc (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Sum2KES Ed25519DSIGN Blake2b_256)) TestName
"Sum2KES"
    , forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm @(MockKES 7) Lock
lock TestName
"MockKES"
    , forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm @(SimpleKES Ed25519DSIGN 7) Lock
lock TestName
"SimpleKES"
    , forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm @(SingleKES Ed25519DSIGN) Lock
lock TestName
"SingleKES"
    , forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm @(Sum1KES Ed25519DSIGN Blake2b_256) Lock
lock TestName
"Sum1KES"
    , forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm @(Sum2KES Ed25519DSIGN Blake2b_256) Lock
lock TestName
"Sum2KES"
    , forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm @(Sum5KES Ed25519DSIGN Blake2b_256) Lock
lock TestName
"Sum5KES"
    , forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm @(CompactSum1KES Ed25519DSIGN Blake2b_256) Lock
lock TestName
"CompactSum1KES"
    , forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm @(CompactSum2KES Ed25519DSIGN Blake2b_256) Lock
lock TestName
"CompactSum2KES"
    , forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm @(CompactSum5KES Ed25519DSIGN Blake2b_256) Lock
lock TestName
"CompactSum5KES"
    ]

--------------------------------------------------------------------------------
-- Show and Eq instances
--------------------------------------------------------------------------------

-- We normally ensure that we avoid naively comparing signing keys by not
-- providing instances, but for tests it is fine, so we provide the orphan
-- instances here.

instance Show (SignKeyKES (SingleKES Ed25519DSIGN)) where
  show :: SignKeyKES (SingleKES Ed25519DSIGN) -> TestName
show (SignKeySingleKES (SignKeyEd25519DSIGNM MLockedSizedBytes CRYPTO_SIGN_ED25519_SECRETKEYBYTES
mlsb)) =
    let bytes :: ByteString
bytes = MLockedSizedBytes CRYPTO_SIGN_ED25519_SECRETKEYBYTES -> ByteString
forall (n :: Nat). KnownNat n => MLockedSizedBytes n -> ByteString
mlsbAsByteString MLockedSizedBytes CRYPTO_SIGN_ED25519_SECRETKEYBYTES
mlsb
        hexstr :: TestName
hexstr = ByteString -> TestName
hexBS ByteString
bytes
     in TestName
"SignKeySingleKES (SignKeyEd25519DSIGNM " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ TestName
hexstr TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ TestName
")"

instance Show (SignKeyKES (SumKES h d)) where
  show :: SignKeyKES (SumKES h d) -> TestName
show SignKeyKES (SumKES h d)
_ = TestName
"<SignKeySumKES>"

instance Show (SignKeyKES (CompactSingleKES Ed25519DSIGN)) where
  show :: SignKeyKES (CompactSingleKES Ed25519DSIGN) -> TestName
show (SignKeyCompactSingleKES (SignKeyEd25519DSIGNM MLockedSizedBytes CRYPTO_SIGN_ED25519_SECRETKEYBYTES
mlsb)) =
    let bytes :: ByteString
bytes = MLockedSizedBytes CRYPTO_SIGN_ED25519_SECRETKEYBYTES -> ByteString
forall (n :: Nat). KnownNat n => MLockedSizedBytes n -> ByteString
mlsbAsByteString MLockedSizedBytes CRYPTO_SIGN_ED25519_SECRETKEYBYTES
mlsb
        hexstr :: TestName
hexstr = ByteString -> TestName
hexBS ByteString
bytes
     in TestName
"SignKeyCompactSingleKES (SignKeyEd25519DSIGNM " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ TestName
hexstr TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ TestName
")"

instance Show (SignKeyKES (CompactSumKES h d)) where
  show :: SignKeyKES (CompactSumKES h d) -> TestName
show SignKeyKES (CompactSumKES h d)
_ = TestName
"<SignKeyCompactSumKES>"

deriving via (PureEqST (SignKeyKES (MockKES t))) instance EqST (SignKeyKES (MockKES t))

deriving newtype instance EqST (SignKeyDSIGNM d) => EqST (SignKeyKES (SingleKES d))

instance
  ( EqST (SignKeyKES d)
  , Eq (VerKeyKES d)
  , KnownNat (SeedSizeKES d)
  ) =>
  EqST (SignKeyKES (SumKES h d))
  where
  equalsM :: forall (m :: * -> *).
MonadST m =>
SignKeyKES (SumKES h d) -> SignKeyKES (SumKES h d) -> m Bool
equalsM (SignKeySumKES SignKeyKES d
s MLockedSeed (SeedSizeKES d)
r VerKeyKES d
v1 VerKeyKES d
v2) (SignKeySumKES SignKeyKES d
s' MLockedSeed (SeedSizeKES d)
r' VerKeyKES d
v1' VerKeyKES d
v2') =
    (SignKeyKES d
s, MLockedSeed (SeedSizeKES d)
r, VerKeyKES d -> PureEqST (VerKeyKES d)
forall a. a -> PureEqST a
PureEqST VerKeyKES d
v1, VerKeyKES d -> PureEqST (VerKeyKES d)
forall a. a -> PureEqST a
PureEqST VerKeyKES d
v2) (SignKeyKES d, MLockedSeed (SeedSizeKES d), PureEqST (VerKeyKES d),
 PureEqST (VerKeyKES d))
-> (SignKeyKES d, MLockedSeed (SeedSizeKES d),
    PureEqST (VerKeyKES d), PureEqST (VerKeyKES d))
-> m Bool
forall (m :: * -> *) a. (MonadST m, EqST a) => a -> a -> m Bool
==! (SignKeyKES d
s', MLockedSeed (SeedSizeKES d)
r', VerKeyKES d -> PureEqST (VerKeyKES d)
forall a. a -> PureEqST a
PureEqST VerKeyKES d
v1', VerKeyKES d -> PureEqST (VerKeyKES d)
forall a. a -> PureEqST a
PureEqST VerKeyKES d
v2')

deriving newtype instance EqST (SignKeyDSIGNM d) => EqST (SignKeyKES (CompactSingleKES d))

instance
  ( EqST (SignKeyKES d)
  , Eq (VerKeyKES d)
  , KnownNat (SeedSizeKES d)
  ) =>
  EqST (SignKeyKES (CompactSumKES h d))
  where
  equalsM :: forall (m :: * -> *).
MonadST m =>
SignKeyKES (CompactSumKES h d)
-> SignKeyKES (CompactSumKES h d) -> m Bool
equalsM (SignKeyCompactSumKES SignKeyKES d
s MLockedSeed (SeedSizeKES d)
r VerKeyKES d
v1 VerKeyKES d
v2) (SignKeyCompactSumKES SignKeyKES d
s' MLockedSeed (SeedSizeKES d)
r' VerKeyKES d
v1' VerKeyKES d
v2') =
    (SignKeyKES d
s, MLockedSeed (SeedSizeKES d)
r, VerKeyKES d -> PureEqST (VerKeyKES d)
forall a. a -> PureEqST a
PureEqST VerKeyKES d
v1, VerKeyKES d -> PureEqST (VerKeyKES d)
forall a. a -> PureEqST a
PureEqST VerKeyKES d
v2) (SignKeyKES d, MLockedSeed (SeedSizeKES d), PureEqST (VerKeyKES d),
 PureEqST (VerKeyKES d))
-> (SignKeyKES d, MLockedSeed (SeedSizeKES d),
    PureEqST (VerKeyKES d), PureEqST (VerKeyKES d))
-> m Bool
forall (m :: * -> *) a. (MonadST m, EqST a) => a -> a -> m Bool
==! (SignKeyKES d
s', MLockedSeed (SeedSizeKES d)
r', VerKeyKES d -> PureEqST (VerKeyKES d)
forall a. a -> PureEqST a
PureEqST VerKeyKES d
v1', VerKeyKES d -> PureEqST (VerKeyKES d)
forall a. a -> PureEqST a
PureEqST VerKeyKES d
v2')

--------------------------------------------------------------------------------
-- Arbitrary instances
--------------------------------------------------------------------------------

genInitialSignKeyKES :: forall k. UnsoundPureKESAlgorithm k => Gen (UnsoundPureSignKeyKES k)
genInitialSignKeyKES :: forall k.
UnsoundPureKESAlgorithm k =>
Gen (UnsoundPureSignKeyKES k)
genInitialSignKeyKES = do
  ByteString
bytes <- [Word8] -> ByteString
BS.pack ([Word8] -> ByteString) -> Gen [Word8] -> Gen ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen [Word8]
forall a. Arbitrary a => Int -> Gen [a]
vector (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy k -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
seedSizeKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @k))
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes ByteString
bytes
  UnsoundPureSignKeyKES k -> Gen (UnsoundPureSignKeyKES k)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnsoundPureSignKeyKES k -> Gen (UnsoundPureSignKeyKES k))
-> UnsoundPureSignKeyKES k -> Gen (UnsoundPureSignKeyKES k)
forall a b. (a -> b) -> a -> b
$ Seed -> UnsoundPureSignKeyKES k
forall v.
UnsoundPureKESAlgorithm v =>
Seed -> UnsoundPureSignKeyKES v
unsoundPureGenKeyKES Seed
seed

instance (UnsoundPureKESAlgorithm k, Arbitrary (ContextKES k)) => Arbitrary (UnsoundPureSignKeyKES k) where
  arbitrary :: Gen (UnsoundPureSignKeyKES k)
arbitrary = do
    ContextKES k
ctx <- Gen (ContextKES k)
forall a. Arbitrary a => Gen a
arbitrary
    let updateTo :: Period -> Period -> UnsoundPureSignKeyKES k -> Maybe (UnsoundPureSignKeyKES k)
        updateTo :: Word
-> Word
-> UnsoundPureSignKeyKES k
-> Maybe (UnsoundPureSignKeyKES k)
updateTo Word
target Word
current UnsoundPureSignKeyKES k
sk
          | Word
target Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
current =
              UnsoundPureSignKeyKES k -> Maybe (UnsoundPureSignKeyKES k)
forall a. a -> Maybe a
Just UnsoundPureSignKeyKES k
sk
          | Word
target Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
> Word
current =
              Word
-> Word
-> UnsoundPureSignKeyKES k
-> Maybe (UnsoundPureSignKeyKES k)
updateTo Word
target (Word -> Word
forall a. Enum a => a -> a
succ Word
current) (UnsoundPureSignKeyKES k -> Maybe (UnsoundPureSignKeyKES k))
-> Maybe (UnsoundPureSignKeyKES k)
-> Maybe (UnsoundPureSignKeyKES k)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ContextKES k
-> UnsoundPureSignKeyKES k
-> Word
-> Maybe (UnsoundPureSignKeyKES k)
forall v.
UnsoundPureKESAlgorithm v =>
ContextKES v
-> UnsoundPureSignKeyKES v
-> Word
-> Maybe (UnsoundPureSignKeyKES v)
unsoundPureUpdateKES ContextKES k
ctx UnsoundPureSignKeyKES k
sk Word
current
          | Bool
otherwise =
              Maybe (UnsoundPureSignKeyKES k)
forall a. Maybe a
Nothing
    Word
period <- (Word, Word) -> Gen Word
forall a. (Bounded a, Integral a) => (a, a) -> Gen a
chooseBoundedIntegral (Word
0, Proxy k -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
forall (proxy :: * -> *). proxy k -> Word
totalPeriodsKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @k) Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1)
    UnsoundPureSignKeyKES k
sk0 <- Gen (UnsoundPureSignKeyKES k)
forall k.
UnsoundPureKESAlgorithm k =>
Gen (UnsoundPureSignKeyKES k)
genInitialSignKeyKES
    let skMay :: Maybe (UnsoundPureSignKeyKES k)
skMay = Word
-> Word
-> UnsoundPureSignKeyKES k
-> Maybe (UnsoundPureSignKeyKES k)
updateTo Word
period Word
0 UnsoundPureSignKeyKES k
sk0
    case Maybe (UnsoundPureSignKeyKES k)
skMay of
      Just UnsoundPureSignKeyKES k
sk -> UnsoundPureSignKeyKES k -> Gen (UnsoundPureSignKeyKES k)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return UnsoundPureSignKeyKES k
sk
      Maybe (UnsoundPureSignKeyKES k)
Nothing -> TestName -> Gen (UnsoundPureSignKeyKES k)
forall a. HasCallStack => TestName -> a
error TestName
"Attempted to generate SignKeyKES evolved beyond max period"

instance (UnsoundPureKESAlgorithm k, Arbitrary (ContextKES k)) => Arbitrary (VerKeyKES k) where
  arbitrary :: Gen (VerKeyKES k)
arbitrary = UnsoundPureSignKeyKES k -> VerKeyKES k
forall v.
UnsoundPureKESAlgorithm v =>
UnsoundPureSignKeyKES v -> VerKeyKES v
unsoundPureDeriveVerKeyKES (UnsoundPureSignKeyKES k -> VerKeyKES k)
-> Gen (UnsoundPureSignKeyKES k) -> Gen (VerKeyKES k)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (UnsoundPureSignKeyKES k)
forall a. Arbitrary a => Gen a
arbitrary

instance (UnsoundPureKESAlgorithm k, Signable k ByteString, Arbitrary (ContextKES k)) => Arbitrary (SigKES k) where
  arbitrary :: Gen (SigKES k)
arbitrary = do
    UnsoundPureSignKeyKES k
sk <- Gen (UnsoundPureSignKeyKES k)
forall a. Arbitrary a => Gen a
arbitrary
    ByteString
signable <- [Word8] -> ByteString
BS.pack ([Word8] -> ByteString) -> Gen [Word8] -> Gen ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word8 -> Gen [Word8]
forall a. Gen a -> Gen [a]
listOf Gen Word8
forall a. Arbitrary a => Gen a
arbitrary
    ContextKES k
ctx <- Gen (ContextKES k)
forall a. Arbitrary a => Gen a
arbitrary
    SigKES k -> Gen (SigKES k)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (SigKES k -> Gen (SigKES k)) -> SigKES k -> Gen (SigKES k)
forall a b. (a -> b) -> a -> b
$ ContextKES k
-> Word -> ByteString -> UnsoundPureSignKeyKES k -> SigKES k
forall v a.
(UnsoundPureKESAlgorithm v, Signable v a) =>
ContextKES v -> Word -> a -> UnsoundPureSignKeyKES v -> SigKES v
forall a.
Signable k a =>
ContextKES k -> Word -> a -> UnsoundPureSignKeyKES k -> SigKES k
unsoundPureSignKES ContextKES k
ctx Word
0 ByteString
signable UnsoundPureSignKeyKES k
sk

--------------------------------------------------------------------------------
-- Tests
--------------------------------------------------------------------------------

testKESAlloc ::
  forall v.
  KESAlgorithm v =>
  Proxy v ->
  String ->
  TestTree
testKESAlloc :: forall v. KESAlgorithm v => Proxy v -> TestName -> TestTree
testKESAlloc Proxy v
_p TestName
n =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
n
    [ TestName -> [TestTree] -> TestTree
testGroup
        TestName
"Low-level mlocked allocations"
        [ TestName -> Assertion -> TestTree
testCase TestName
"genKey" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ Proxy v -> Assertion
forall v. KESAlgorithm v => Proxy v -> Assertion
testMLockGenKeyKES Proxy v
_p
        -- , testCase "updateKey" $ testMLockUpdateKeyKES _p
        ]
    ]

eventTracer :: IORef [event] -> Tracer IO event
eventTracer :: forall event. IORef [event] -> Tracer IO event
eventTracer IORef [event]
logVar = (event -> Assertion) -> Tracer IO event
forall (m :: * -> *) a. (a -> m ()) -> Tracer m a
Tracer (\event
ev -> Assertion -> Assertion
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Assertion -> Assertion) -> Assertion -> Assertion
forall a b. (a -> b) -> a -> b
$ IORef [event] -> ([event] -> ([event], ())) -> Assertion
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef [event]
logVar (\[event]
acc -> ([event]
acc [event] -> [event] -> [event]
forall a. [a] -> [a] -> [a]
++ [event
ev], ())))

matchAllocLog :: [AllocEvent] -> Set WordPtr
matchAllocLog :: [AllocEvent] -> Set WordPtr
matchAllocLog = (Set WordPtr -> AllocEvent -> Set WordPtr)
-> Set WordPtr -> [AllocEvent] -> Set WordPtr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' ((AllocEvent -> Set WordPtr -> Set WordPtr)
-> Set WordPtr -> AllocEvent -> Set WordPtr
forall a b c. (a -> b -> c) -> b -> a -> c
flip AllocEvent -> Set WordPtr -> Set WordPtr
go) Set WordPtr
forall a. Set a
Set.empty
  where
    go :: AllocEvent -> Set WordPtr -> Set WordPtr
go (AllocEv WordPtr
ptr) = WordPtr -> Set WordPtr -> Set WordPtr
forall a. Ord a => a -> Set a -> Set a
Set.insert WordPtr
ptr
    go (FreeEv WordPtr
ptr) = WordPtr -> Set WordPtr -> Set WordPtr
forall a. Ord a => a -> Set a -> Set a
Set.delete WordPtr
ptr
    go (MarkerEv TestName
_) = Set WordPtr -> Set WordPtr
forall a. a -> a
id

testMLockGenKeyKES ::
  forall v.
  KESAlgorithm v =>
  Proxy v ->
  Assertion
testMLockGenKeyKES :: forall v. KESAlgorithm v => Proxy v -> Assertion
testMLockGenKeyKES Proxy v
_p = do
  IORef [AllocEvent]
accumVar <- [AllocEvent] -> IO (IORef [AllocEvent])
forall a. a -> IO (IORef a)
newIORef []
  let tracer :: Tracer IO AllocEvent
tracer = IORef [AllocEvent] -> Tracer IO AllocEvent
forall event. IORef [event] -> Tracer IO event
eventTracer IORef [AllocEvent]
accumVar
  let allocator :: MLockedAllocator IO
allocator = Tracer IO AllocEvent -> MLockedAllocator IO -> MLockedAllocator IO
mkLoggingAllocator Tracer IO AllocEvent
tracer MLockedAllocator IO
forall (m :: * -> *). MonadST m => MLockedAllocator m
mlockedMalloc
  Tracer IO AllocEvent -> AllocEvent -> Assertion
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Assertion) -> AllocEvent -> Assertion
forall a b. (a -> b) -> a -> b
$ TestName -> AllocEvent
MarkerEv TestName
"gen seed"
  MLockedSeed (SeedSizeKES v)
seed :: MLockedSeed (SeedSizeKES v) <-
    MLockedSizedBytes (SeedSizeKES v) -> MLockedSeed (SeedSizeKES v)
forall (n :: Nat). MLockedSizedBytes n -> MLockedSeed n
MLockedSeed (MLockedSizedBytes (SeedSizeKES v) -> MLockedSeed (SeedSizeKES v))
-> IO (MLockedSizedBytes (SeedSizeKES v))
-> IO (MLockedSeed (SeedSizeKES v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MLockedAllocator IO
-> ByteString -> IO (MLockedSizedBytes (SeedSizeKES v))
forall (n :: Nat) (m :: * -> *).
(KnownNat n, MonadST m) =>
MLockedAllocator m -> ByteString -> m (MLockedSizedBytes n)
mlsbFromByteStringWith MLockedAllocator IO
allocator (Int -> Word8 -> ByteString
BS.replicate Int
1024 Word8
23)
  Tracer IO AllocEvent -> AllocEvent -> Assertion
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Assertion) -> AllocEvent -> Assertion
forall a b. (a -> b) -> a -> b
$ TestName -> AllocEvent
MarkerEv TestName
"gen key"
  SignKeyKES v
sk <- forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedAllocator m
-> MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKESWith @v MLockedAllocator IO
allocator MLockedSeed (SeedSizeKES v)
seed
  Tracer IO AllocEvent -> AllocEvent -> Assertion
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Assertion) -> AllocEvent -> Assertion
forall a b. (a -> b) -> a -> b
$ TestName -> AllocEvent
MarkerEv TestName
"forget key"
  MLockedAllocator IO -> SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedAllocator m -> SignKeyKES v -> m ()
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
MLockedAllocator m -> SignKeyKES v -> m ()
forgetSignKeyKESWith MLockedAllocator IO
allocator SignKeyKES v
sk
  Tracer IO AllocEvent -> AllocEvent -> Assertion
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Assertion) -> AllocEvent -> Assertion
forall a b. (a -> b) -> a -> b
$ TestName -> AllocEvent
MarkerEv TestName
"forget seed"
  MLockedSeed (SeedSizeKES v) -> Assertion
forall (m :: * -> *) (n :: Nat). MonadST m => MLockedSeed n -> m ()
mlockedSeedFinalize MLockedSeed (SeedSizeKES v)
seed
  Tracer IO AllocEvent -> AllocEvent -> Assertion
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Assertion) -> AllocEvent -> Assertion
forall a b. (a -> b) -> a -> b
$ TestName -> AllocEvent
MarkerEv TestName
"done"
  [AllocEvent]
after <- IORef [AllocEvent] -> IO [AllocEvent]
forall a. IORef a -> IO a
readIORef IORef [AllocEvent]
accumVar
  let evset :: Set WordPtr
evset = [AllocEvent] -> Set WordPtr
matchAllocLog [AllocEvent]
after
  HasCallStack => TestName -> Bool -> Assertion
TestName -> Bool -> Assertion
assertBool TestName
"some allocations happened" (Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([()] -> Bool) -> [()] -> Bool
forall a b. (a -> b) -> a -> b
$ [() | AllocEv WordPtr
_ <- [AllocEvent]
after])
  TestName -> Set WordPtr -> Set WordPtr -> Assertion
forall a.
(Eq a, Show a, HasCallStack) =>
TestName -> a -> a -> Assertion
assertEqual TestName
"all allocations deallocated" Set WordPtr
forall a. Set a
Set.empty Set WordPtr
evset

{-# NOINLINE testKESAlgorithm #-}
testKESAlgorithm ::
  forall v.
  ( ToCBOR (VerKeyKES v)
  , FromCBOR (VerKeyKES v)
  , EqST (SignKeyKES v) -- only monadic EqST for signing keys
  , Show (SignKeyKES v) -- fake instance defined locally
  , Eq (UnsoundPureSignKeyKES v)
  , Show (UnsoundPureSignKeyKES v)
  , ToCBOR (SigKES v)
  , FromCBOR (SigKES v)
  , Signable v ~ SignableRepresentation
  , ContextKES v ~ ()
  , UnsoundKESAlgorithm v
  , UnsoundPureKESAlgorithm v
  , DirectSerialise (SignKeyKES v)
  , DirectSerialise (VerKeyKES v)
  , DirectDeserialise (SignKeyKES v)
  , DirectDeserialise (VerKeyKES v)
  ) =>
  Lock ->
  String ->
  TestTree
testKESAlgorithm :: forall v.
(ToCBOR (VerKeyKES v), FromCBOR (VerKeyKES v), EqST (SignKeyKES v),
 Show (SignKeyKES v), Eq (UnsoundPureSignKeyKES v),
 Show (UnsoundPureSignKeyKES v), ToCBOR (SigKES v),
 FromCBOR (SigKES v), Signable v ~ SignableRepresentation,
 ContextKES v ~ (), UnsoundKESAlgorithm v,
 UnsoundPureKESAlgorithm v, DirectSerialise (SignKeyKES v),
 DirectSerialise (VerKeyKES v), DirectDeserialise (SignKeyKES v),
 DirectDeserialise (VerKeyKES v)) =>
Lock -> TestName -> TestTree
testKESAlgorithm Lock
lock TestName
n =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
n
    [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"only gen signkey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
KESAlgorithm v =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_onlyGenSignKeyKES @v Lock
lock
    , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"only gen verkey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
KESAlgorithm v =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_onlyGenVerKeyKES @v Lock
lock
    , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"one update signkey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_oneUpdateSignKeyKES @v Lock
lock
    , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"all updates signkey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_allUpdatesSignKeyKES @v Lock
lock
    , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"total periods" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_totalPeriodsKES @v Lock
lock
    , TestName -> [TestTree] -> TestTree
testGroup
        TestName
"NoThunks"
        [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
            forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk ->
              IO (VerKeyKES v) -> IO Property
forall a. NoThunks a => IO a -> IO Property
prop_no_thunks_IO (SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk)
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
            forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$
              IO (SignKeyKES v) -> IO Property
forall a. NoThunks a => IO a -> IO Property
prop_no_thunks_IO (IO (SignKeyKES v) -> IO Property)
-> (SignKeyKES v -> IO (SignKeyKES v))
-> SignKeyKES v
-> IO Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SignKeyKES v -> IO (SignKeyKES v)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"SignKey evolved" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
            forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk ->
              IO (Maybe (SignKeyKES v))
-> (Maybe (SignKeyKES v) -> Assertion)
-> (Maybe (SignKeyKES v) -> IO Property)
-> IO Property
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
                (ContextKES v -> SignKeyKES v -> Word -> IO (Maybe (SignKeyKES v))
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
ContextKES v -> SignKeyKES v -> Word -> m (Maybe (SignKeyKES v))
updateKES () SignKeyKES v
sk Word
0)
                (Assertion
-> (SignKeyKES v -> Assertion) -> Maybe (SignKeyKES v) -> Assertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Assertion
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES)
                (IO (Maybe (SignKeyKES v)) -> IO Property
forall a. NoThunks a => IO a -> IO Property
prop_no_thunks_IO (IO (Maybe (SignKeyKES v)) -> IO Property)
-> (Maybe (SignKeyKES v) -> IO (Maybe (SignKeyKES v)))
-> Maybe (SignKeyKES v)
-> IO Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (SignKeyKES v) -> IO (Maybe (SignKeyKES v))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return)
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Sig" ((PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
 -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ \PinnedSizedBytes (SeedSizeKES v)
seedPSB (Message
msg :: Message) ->
            IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ Lock -> IO Property -> IO Property
forall a. Lock -> IO a -> IO a
withLock Lock
lock (IO Property -> IO Property) -> IO Property -> IO Property
forall a b. (a -> b) -> a -> b
$ ([Property] -> Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin (IO [Property] -> IO Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> a -> b
$ forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES @v PinnedSizedBytes (SeedSizeKES v)
seedPSB ((Word -> SignKeyKES v -> IO Property) -> IO [Property])
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
              IO (SigKES v) -> IO Property
forall a. NoThunks a => IO a -> IO Property
prop_no_thunks_IO (ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
msg SignKeyKES v
sk)
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey DirectSerialise" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
            forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
              VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
              ByteString
direct <- Int -> VerKeyKES v -> IO ByteString
forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeVerKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)) VerKeyKES v
vk
              IO ByteString -> IO Property
forall a. NoThunks a => IO a -> IO Property
prop_no_thunks_IO (ByteString -> IO ByteString
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> IO ByteString) -> ByteString -> IO ByteString
forall a b. (a -> b) -> a -> b
$! ByteString
direct)
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"SignKey DirectSerialise" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
            forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
              ByteString
direct <- Int -> SignKeyKES v -> IO ByteString
forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSignKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)) SignKeyKES v
sk
              IO ByteString -> IO Property
forall a. NoThunks a => IO a -> IO Property
prop_no_thunks_IO (ByteString -> IO ByteString
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString -> IO ByteString) -> ByteString -> IO ByteString
forall a b. (a -> b) -> a -> b
$! ByteString
direct)
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey DirectDeserialise" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
            forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
              VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
              ByteString
direct <- Int -> VerKeyKES v -> IO ByteString
forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeVerKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)) (VerKeyKES v -> IO ByteString) -> VerKeyKES v -> IO ByteString
forall a b. (a -> b) -> a -> b
$! VerKeyKES v
vk
              IO (VerKeyKES v) -> IO Property
forall a. NoThunks a => IO a -> IO Property
prop_no_thunks_IO (forall (m :: * -> *) a.
(DirectDeserialise a, MonadST m, MonadThrow m) =>
ByteString -> m a
directDeserialiseFromBS @IO @(VerKeyKES v) (ByteString -> IO (VerKeyKES v)) -> ByteString -> IO (VerKeyKES v)
forall a b. (a -> b) -> a -> b
$! ByteString
direct)
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"SignKey DirectDeserialise" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
            forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
              ByteString
direct <- Int -> SignKeyKES v -> IO ByteString
forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSignKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)) SignKeyKES v
sk
              IO (SignKeyKES v)
-> (SignKeyKES v -> Assertion)
-> (SignKeyKES v -> IO Property)
-> IO Property
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
                (forall (m :: * -> *) a.
(DirectDeserialise a, MonadST m, MonadThrow m) =>
ByteString -> m a
directDeserialiseFromBS @IO @(SignKeyKES v) (ByteString -> IO (SignKeyKES v))
-> ByteString -> IO (SignKeyKES v)
forall a b. (a -> b) -> a -> b
$! ByteString
direct)
                SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES
                (IO (SignKeyKES v) -> IO Property
forall a. NoThunks a => IO a -> IO Property
prop_no_thunks_IO (IO (SignKeyKES v) -> IO Property)
-> (SignKeyKES v -> IO (SignKeyKES v))
-> SignKeyKES v
-> IO Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SignKeyKES v -> IO (SignKeyKES v)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return)
        ]
    , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"same VerKey " ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Property
prop_deriveVerKeyKES @v
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"no forgotten chunks in signkey" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Proxy v -> Property
forall v.
(UnsoundKESAlgorithm v, DirectSerialise (SignKeyKES v)) =>
Proxy v -> Property
prop_noErasedBlocksInKey (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)
    , TestName -> [TestTree] -> TestTree
testGroup
        TestName
"serialisation"
        [ TestName -> [TestTree] -> TestTree
testGroup
            TestName
"raw ser only"
            [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ (ByteString -> Maybe (VerKeyKES v)
forall v. KESAlgorithm v => ByteString -> Maybe (VerKeyKES v)
rawDeserialiseVerKeyKES (ByteString -> Maybe (VerKeyKES v))
-> (VerKeyKES v -> ByteString)
-> VerKeyKES v
-> Maybe (VerKeyKES v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerKeyKES v -> ByteString
forall v. KESAlgorithm v => VerKeyKES v -> ByteString
rawSerialiseVerKeyKES (VerKeyKES v -> Maybe (VerKeyKES v))
-> VerKeyKES v -> Maybe (VerKeyKES v)
forall a b. (a -> b) -> a -> b
$ VerKeyKES v
vk) Maybe (VerKeyKES v) -> Maybe (VerKeyKES v) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== VerKeyKES v -> Maybe (VerKeyKES v)
forall a. a -> Maybe a
Just VerKeyKES v
vk
            , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  ByteString
serialized <- SignKeyKES v -> IO ByteString
forall v (m :: * -> *).
(UnsoundKESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ByteString
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m ByteString
rawSerialiseSignKeyKES SignKeyKES v
sk
                  Bool
equals <-
                    IO (Maybe (SignKeyKES v))
-> (Maybe (SignKeyKES v) -> Assertion)
-> (Maybe (SignKeyKES v) -> IO Bool)
-> IO Bool
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
                      (ByteString -> IO (Maybe (SignKeyKES v))
forall v (m :: * -> *).
(UnsoundKESAlgorithm v, MonadST m, MonadThrow m) =>
ByteString -> m (Maybe (SignKeyKES v))
rawDeserialiseSignKeyKES ByteString
serialized)
                      (Assertion
-> (SignKeyKES v -> Assertion) -> Maybe (SignKeyKES v) -> Assertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Assertion
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES)
                      (\Maybe (SignKeyKES v)
msk' -> SignKeyKES v -> Maybe (SignKeyKES v)
forall a. a -> Maybe a
Just SignKeyKES v
sk Maybe (SignKeyKES v) -> Maybe (SignKeyKES v) -> IO Bool
forall (m :: * -> *) a. (MonadST m, EqST a) => a -> a -> m Bool
==! Maybe (SignKeyKES v)
msk')
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
                    TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (ByteString -> TestName
forall a. Show a => a -> TestName
show ByteString
serialized) Bool
equals
            , TestName
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
 -> TestTree)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ \(Message
msg :: Message) ->
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  SigKES v
sig :: SigKES v <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
0 Message
msg SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ (ByteString -> Maybe (SigKES v)
forall v. KESAlgorithm v => ByteString -> Maybe (SigKES v)
rawDeserialiseSigKES (ByteString -> Maybe (SigKES v))
-> (SigKES v -> ByteString) -> SigKES v -> Maybe (SigKES v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigKES v -> ByteString
forall v. KESAlgorithm v => SigKES v -> ByteString
rawSerialiseSigKES (SigKES v -> Maybe (SigKES v)) -> SigKES v -> Maybe (SigKES v)
forall a b. (a -> b) -> a -> b
$ SigKES v
sig) Maybe (SigKES v) -> Maybe (SigKES v) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== SigKES v -> Maybe (SigKES v)
forall a. a -> Maybe a
Just SigKES v
sig
            ]
        , TestName -> [TestTree] -> TestTree
testGroup
            TestName
"size"
            [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word) -> (VerKeyKES v -> Int) -> VerKeyKES v -> Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length (ByteString -> Int)
-> (VerKeyKES v -> ByteString) -> VerKeyKES v -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerKeyKES v -> ByteString
forall v. KESAlgorithm v => VerKeyKES v -> ByteString
rawSerialiseVerKeyKES (VerKeyKES v -> Word) -> VerKeyKES v -> Word
forall a b. (a -> b) -> a -> b
$ VerKeyKES v
vk) Word -> Word -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeVerKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)
            , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Bool)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Bool)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  ByteString
serialized <- SignKeyKES v -> IO ByteString
forall v (m :: * -> *).
(UnsoundKESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ByteString
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m ByteString
rawSerialiseSignKeyKES SignKeyKES v
sk
                  Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate ((Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word) -> (ByteString -> Int) -> ByteString -> Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length (ByteString -> Word) -> ByteString -> Word
forall a b. (a -> b) -> a -> b
$ ByteString
serialized) Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSignKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v))
            , TestName
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
 -> TestTree)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ \(Message
msg :: Message) ->
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  SigKES v
sig :: SigKES v <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
0 Message
msg SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word) -> (SigKES v -> Int) -> SigKES v -> Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length (ByteString -> Int) -> (SigKES v -> ByteString) -> SigKES v -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigKES v -> ByteString
forall v. KESAlgorithm v => SigKES v -> ByteString
rawSerialiseSigKES (SigKES v -> Word) -> SigKES v -> Word
forall a b. (a -> b) -> a -> b
$ SigKES v
sig) Word -> Word -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSigKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)
            ]
        , TestName -> [TestTree] -> TestTree
testGroup
            TestName
"direct CBOR"
            [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ (VerKeyKES v -> Encoding)
-> (forall s. Decoder s (VerKeyKES v)) -> VerKeyKES v -> Property
forall a.
(Eq a, Show a) =>
(a -> Encoding) -> (forall s. Decoder s a) -> a -> Property
prop_cbor_with VerKeyKES v -> Encoding
forall v. KESAlgorithm v => VerKeyKES v -> Encoding
encodeVerKeyKES Decoder s (VerKeyKES v)
forall s. Decoder s (VerKeyKES v)
forall v s. KESAlgorithm v => Decoder s (VerKeyKES v)
decodeVerKeyKES VerKeyKES v
vk
            , -- No CBOR testing for SignKey: sign keys are stored in MLocked memory
              -- and require IO for access.
              TestName
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
 -> TestTree)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ \(Message
msg :: Message) ->
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  SigKES v
sig :: SigKES v <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
0 Message
msg SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ (SigKES v -> Encoding)
-> (forall s. Decoder s (SigKES v)) -> SigKES v -> Property
forall a.
(Eq a, Show a) =>
(a -> Encoding) -> (forall s. Decoder s a) -> a -> Property
prop_cbor_with SigKES v -> Encoding
forall v. KESAlgorithm v => SigKES v -> Encoding
encodeSigKES Decoder s (SigKES v)
forall s. Decoder s (SigKES v)
forall v s. KESAlgorithm v => Decoder s (SigKES v)
decodeSigKES SigKES v
sig
            , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"UnsoundSignKeyKES" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ \PinnedSizedBytes (SeedSizeKES v)
seedPSB ->
                let UnsoundPureSignKeyKES v
sk :: UnsoundPureSignKeyKES v = PinnedSizedBytes (SeedSizeKES v) -> UnsoundPureSignKeyKES v
forall v.
UnsoundPureKESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> UnsoundPureSignKeyKES v
mkUnsoundPureSignKeyKES PinnedSizedBytes (SeedSizeKES v)
seedPSB
                 in (UnsoundPureSignKeyKES v -> Encoding)
-> (forall s. Decoder s (UnsoundPureSignKeyKES v))
-> UnsoundPureSignKeyKES v
-> Property
forall a.
(Eq a, Show a) =>
(a -> Encoding) -> (forall s. Decoder s a) -> a -> Property
prop_cbor_with UnsoundPureSignKeyKES v -> Encoding
forall v.
UnsoundPureKESAlgorithm v =>
UnsoundPureSignKeyKES v -> Encoding
encodeUnsoundPureSignKeyKES Decoder s (UnsoundPureSignKeyKES v)
forall s. Decoder s (UnsoundPureSignKeyKES v)
forall v s.
UnsoundPureKESAlgorithm v =>
Decoder s (UnsoundPureSignKeyKES v)
decodeUnsoundPureSignKeyKES UnsoundPureSignKeyKES v
sk
            ]
        , TestName -> [TestTree] -> TestTree
testGroup
            TestName
"To/FromCBOR class"
            [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ VerKeyKES v -> Property
forall a. (ToCBOR a, FromCBOR a, Eq a, Show a) => a -> Property
prop_cbor VerKeyKES v
vk
            , -- No To/FromCBOR for 'SignKeyKES', see above.
              TestName
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
 -> TestTree)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ \(Message
msg :: Message) ->
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  SigKES v
sig :: SigKES v <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
0 Message
msg SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ SigKES v -> Property
forall a. (ToCBOR a, FromCBOR a, Eq a, Show a) => a -> Property
prop_cbor SigKES v
sig
            ]
        , TestName -> [TestTree] -> TestTree
testGroup
            TestName
"ToCBOR size"
            [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ VerKeyKES v -> Property
forall a. ToCBOR a => a -> Property
prop_cbor_size VerKeyKES v
vk
            , -- No To/FromCBOR for 'SignKeyKES', see above.
              TestName
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
 -> TestTree)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ \(Message
msg :: Message) ->
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  SigKES v
sig :: SigKES v <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
0 Message
msg SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ SigKES v -> Property
forall a. ToCBOR a => a -> Property
prop_cbor_size SigKES v
sig
            ]
        , TestName -> [TestTree] -> TestTree
testGroup
            TestName
"direct matches class"
            [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ (VerKeyKES v -> Encoding) -> VerKeyKES v -> Property
forall a. ToCBOR a => (a -> Encoding) -> a -> Property
prop_cbor_direct_vs_class VerKeyKES v -> Encoding
forall v. KESAlgorithm v => VerKeyKES v -> Encoding
encodeVerKeyKES VerKeyKES v
vk
            , -- No CBOR testing for SignKey: sign keys are stored in MLocked memory
              -- and require IO for access.
              TestName
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
 -> TestTree)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ \(Message
msg :: Message) ->
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  SigKES v
sig :: SigKES v <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
0 Message
msg SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ (SigKES v -> Encoding) -> SigKES v -> Property
forall a. ToCBOR a => (a -> Encoding) -> a -> Property
prop_cbor_direct_vs_class SigKES v -> Encoding
forall v. KESAlgorithm v => SigKES v -> Encoding
encodeSigKES SigKES v
sig
            ]
        , TestName -> [TestTree] -> TestTree
testGroup
            TestName
"DirectSerialise"
            [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
                  ByteString
serialized <- Int -> VerKeyKES v -> IO ByteString
forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeVerKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)) VerKeyKES v
vk
                  VerKeyKES v
vk' <- ByteString -> IO (VerKeyKES v)
forall (m :: * -> *) a.
(DirectDeserialise a, MonadST m, MonadThrow m) =>
ByteString -> m a
directDeserialiseFromBS ByteString
serialized
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ VerKeyKES v
vk VerKeyKES v -> VerKeyKES v -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== VerKeyKES v
vk'
            , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  ByteString
serialized <- Int -> SignKeyKES v -> IO ByteString
forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSignKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)) SignKeyKES v
sk
                  Bool
equals <-
                    IO (SignKeyKES v)
-> (SignKeyKES v -> Assertion)
-> (SignKeyKES v -> IO Bool)
-> IO Bool
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
                      (ByteString -> IO (SignKeyKES v)
forall (m :: * -> *) a.
(DirectDeserialise a, MonadST m, MonadThrow m) =>
ByteString -> m a
directDeserialiseFromBS ByteString
serialized)
                      SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES
                      (SignKeyKES v
sk SignKeyKES v -> SignKeyKES v -> IO Bool
forall (m :: * -> *) a. (MonadST m, EqST a) => a -> a -> m Bool
==!)
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
                    (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                      (TestName
"Serialized: " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ ByteString -> TestName
hexBS ByteString
serialized TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ TestName
" (length: " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> TestName
forall a. Show a => a -> TestName
show (ByteString -> Int
BS.length ByteString
serialized) TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ TestName
")")
                    (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Bool
equals
            ]
        , TestName -> [TestTree] -> TestTree
testGroup
            TestName
"DirectSerialise matches raw"
            [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  VerKeyKES v
vk :: VerKeyKES v <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
                  ByteString
direct <- Int -> VerKeyKES v -> IO ByteString
forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeVerKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)) VerKeyKES v
vk
                  let raw :: ByteString
raw = VerKeyKES v -> ByteString
forall v. KESAlgorithm v => VerKeyKES v -> ByteString
rawSerialiseVerKeyKES VerKeyKES v
vk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ ByteString
direct ByteString -> ByteString -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ByteString
raw
            , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
                forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
                  ByteString
direct <- Int -> SignKeyKES v -> IO ByteString
forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS (Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSignKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v)) SignKeyKES v
sk
                  ByteString
raw <- SignKeyKES v -> IO ByteString
forall v (m :: * -> *).
(UnsoundKESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ByteString
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m ByteString
rawSerialiseSignKeyKES SignKeyKES v
sk
                  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ ByteString
direct ByteString -> ByteString -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ByteString
raw
            ]
        ]
    , TestName -> [TestTree] -> TestTree
testGroup
        TestName
"verify"
        [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Gen Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"positive" ((PinnedSizedBytes (SeedSizeKES v) -> Gen Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Gen Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Gen Property
prop_verifyKES_positive @v
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v)
    -> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"negative (key)" ((PinnedSizedBytes (SeedSizeKES v)
  -> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
 -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v)
    -> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v)
-> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property
prop_verifyKES_negative_key @v
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v)
    -> Message -> Message -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"negative (message)" ((PinnedSizedBytes (SeedSizeKES v)
  -> Message -> Message -> Property)
 -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v)
    -> Message -> Message -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Message -> Message -> Property
prop_verifyKES_negative_message @v
        , (QuickCheckMaxSize -> QuickCheckMaxSize) -> TestTree -> TestTree
forall v. IsOption v => (v -> v) -> TestTree -> TestTree
adjustOption (\(QuickCheckMaxSize Int
sz) -> Int -> QuickCheckMaxSize
QuickCheckMaxSize (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
sz Int
50)) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
            TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"negative (period)" ((PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
 -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$
              forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Message -> Property
prop_verifyKES_negative_period @v
        ]
    , TestName -> [TestTree] -> TestTree
testGroup
        TestName
"serialisation of all KES evolutions"
        [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Property
prop_serialise_VerKeyKES @v
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Sig" ((PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
 -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 Show (SignKeyKES v), KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Message -> Property
prop_serialise_SigKES @v
        ]
    , -- TODO: this doesn't pass right now, see
      -- 'prop_key_overwritten_after_forget' for details.
      --
      -- , testGroup "forgetting"
      --   [ testProperty "key overwritten after forget" $ prop_key_overwritten_after_forget (Proxy @v)
      --   ]

      TestName -> [TestTree] -> TestTree
testGroup
        TestName
"unsound pure"
        [ TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"genKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(UnsoundPureKESAlgorithm v, EqST (SignKeyKES v)) =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureGenKey @v Proxy v
forall {k} (t :: k). Proxy t
Proxy
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"updateKES" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(UnsoundPureKESAlgorithm v, ContextKES v ~ (),
 EqST (SignKeyKES v)) =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureUpdateKES @v Proxy v
forall {k} (t :: k). Proxy t
Proxy
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"deriveVerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
UnsoundPureKESAlgorithm v =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureDeriveVerKey @v Proxy v
forall {k} (t :: k). Proxy t
Proxy
        , TestName
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"sign" ((PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
 -> TestTree)
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$ forall v.
(UnsoundPureKESAlgorithm v, ContextKES v ~ (),
 Signable v Message) =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property
prop_unsoundPureSign @v Proxy v
forall {k} (t :: k). Proxy t
Proxy
        ]
    ]

-- | Wrap an IO action that requires a 'SignKeyKES' into one that takes an
-- mlocked seed to generate the key from. The key is bracketed off to ensure
-- timely forgetting. Special care must be taken to not leak the key outside of
-- the wrapped action (be particularly mindful of thunks and unsafe key access
-- here).
withSK ::
  KESAlgorithm v =>
  PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK :: forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB =
  IO (SignKeyKES v)
-> (SignKeyKES v -> Assertion) -> (SignKeyKES v -> IO b) -> IO b
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
    (PinnedSizedBytes (SeedSizeKES v)
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES)
    SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES

mkUnsoundPureSignKeyKES ::
  UnsoundPureKESAlgorithm v =>
  PinnedSizedBytes (SeedSizeKES v) -> UnsoundPureSignKeyKES v
mkUnsoundPureSignKeyKES :: forall v.
UnsoundPureKESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> UnsoundPureSignKeyKES v
mkUnsoundPureSignKeyKES PinnedSizedBytes (SeedSizeKES v)
psb =
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes (ByteString -> Seed)
-> (PinnedSizedBytes (SeedSizeKES v) -> ByteString)
-> PinnedSizedBytes (SeedSizeKES v)
-> Seed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PinnedSizedBytes (SeedSizeKES v) -> ByteString
forall (n :: Nat). PinnedSizedBytes n -> ByteString
psbToByteString (PinnedSizedBytes (SeedSizeKES v) -> Seed)
-> PinnedSizedBytes (SeedSizeKES v) -> Seed
forall a b. (a -> b) -> a -> b
$ PinnedSizedBytes (SeedSizeKES v)
psb
   in Seed -> UnsoundPureSignKeyKES v
forall v.
UnsoundPureKESAlgorithm v =>
Seed -> UnsoundPureSignKeyKES v
unsoundPureGenKeyKES Seed
seed

-- | Wrap an IO action that requires a 'SignKeyKES' into a 'Property' that
-- takes a non-mlocked seed (provided as a 'PinnedSizedBytes' of the
-- appropriate size). The key, and the mlocked seed necessary to generate it,
-- are bracketed off, to ensure timely forgetting and avoid leaking mlocked
-- memory. Special care must be taken to not leak the key outside of the
-- wrapped action (be particularly mindful of thunks and unsafe key access
-- here).
ioPropertyWithSK ::
  forall v a.
  (Testable a, KESAlgorithm v) =>
  Lock ->
  (SignKeyKES v -> IO a) ->
  PinnedSizedBytes (SeedSizeKES v) ->
  Property
ioPropertyWithSK :: forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK Lock
lock SignKeyKES v -> IO a
action PinnedSizedBytes (SeedSizeKES v)
seedPSB =
  IO a -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO a -> Property) -> IO a -> Property
forall a b. (a -> b) -> a -> b
$ Lock -> IO a -> IO a
forall a. Lock -> IO a -> IO a
withLock Lock
lock (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$ PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO a) -> IO a
forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB SignKeyKES v -> IO a
action

-- TODO: This doesn't actually pass right now, for various reasons:
-- - MockKES and SimpleKES don't actually implement secure forgetting;
--   forgetSignKeyKES is a no-op for these algorithms, and obviously that means
--   forgetting won't actually erase the key
-- prop_key_overwritten_after_forget
--   :: forall v.
--      (KESAlgorithm IO v
--      )
--   => Proxy v
--   -> PinnedSizedBytes (SeedSizeKES v)
--   -> Property
-- prop_key_overwritten_after_forget _ seedPSB =
--   ioProperty . withMLSBFromPSB seedPSB $ \seed -> do
--     sk <- genKeyKES @IO @v seed
--
--     before <- rawSerialiseSignKeyKES sk
--     forgetSignKeyKES sk
--     after <- rawSerialiseSignKeyKES sk
--
--     NaCl.mlsbFinalize seed
--
--     return (before =/= after)

prop_onlyGenSignKeyKES ::
  forall v.
  KESAlgorithm v =>
  Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_onlyGenSignKeyKES :: forall v.
KESAlgorithm v =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_onlyGenSignKeyKES Lock
lock =
  forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ IO Property -> SignKeyKES v -> IO Property
forall a b. a -> b -> a
const IO Property
forall (m :: * -> *). Applicative m => m Property
noExceptionsThrown

prop_onlyGenVerKeyKES ::
  forall v.
  KESAlgorithm v =>
  Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_onlyGenVerKeyKES :: forall v.
KESAlgorithm v =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_onlyGenVerKeyKES Lock
lock =
  forall v a.
(Testable a, KESAlgorithm v) =>
Lock
-> (SignKeyKES v -> IO a)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
ioPropertyWithSK @v Lock
lock ((SignKeyKES v -> IO Property)
 -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> (SignKeyKES v -> IO Property)
-> PinnedSizedBytes (SeedSizeKES v)
-> Property
forall a b. (a -> b) -> a -> b
$ IO (VerKeyKES v) -> IO Property
forall (m :: * -> *) a. Applicative m => m a -> m Property
doesNotThrow (IO (VerKeyKES v) -> IO Property)
-> (SignKeyKES v -> IO (VerKeyKES v))
-> SignKeyKES v
-> IO Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES

prop_oneUpdateSignKeyKES ::
  forall v.
  ( ContextKES v ~ ()
  , KESAlgorithm v
  ) =>
  Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_oneUpdateSignKeyKES :: forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_oneUpdateSignKeyKES Lock
lock PinnedSizedBytes (SeedSizeKES v)
seedPSB =
  IO Bool -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Bool -> Property)
-> ((MLockedSeed (SeedSizeKES v) -> IO Bool) -> IO Bool)
-> (MLockedSeed (SeedSizeKES v) -> IO Bool)
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lock -> IO Bool -> IO Bool
forall a. Lock -> IO a -> IO a
withLock Lock
lock (IO Bool -> IO Bool)
-> ((MLockedSeed (SeedSizeKES v) -> IO Bool) -> IO Bool)
-> (MLockedSeed (SeedSizeKES v) -> IO Bool)
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PinnedSizedBytes (SeedSizeKES v)
-> (MLockedSeed (SeedSizeKES v) -> IO Bool) -> IO Bool
forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB ((MLockedSeed (SeedSizeKES v) -> IO Bool) -> Property)
-> (MLockedSeed (SeedSizeKES v) -> IO Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \MLockedSeed (SeedSizeKES v)
seed -> do
    SignKeyKES v
sk <- forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES @v MLockedSeed (SeedSizeKES v)
seed
    Maybe (SignKeyKES v)
msk' <- ContextKES v -> SignKeyKES v -> Word -> IO (Maybe (SignKeyKES v))
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
ContextKES v -> SignKeyKES v -> Word -> m (Maybe (SignKeyKES v))
updateKES () SignKeyKES v
sk Word
0
    SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk
    Assertion
-> (SignKeyKES v -> Assertion) -> Maybe (SignKeyKES v) -> Assertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Assertion
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES Maybe (SignKeyKES v)
msk'
    Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

prop_allUpdatesSignKeyKES ::
  forall v.
  ( ContextKES v ~ ()
  , KESAlgorithm v
  ) =>
  Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_allUpdatesSignKeyKES :: forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_allUpdatesSignKeyKES Lock
lock PinnedSizedBytes (SeedSizeKES v)
seedPSB =
  Assertion -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (Assertion -> Property)
-> (Assertion -> Assertion) -> Assertion -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lock -> Assertion -> Assertion
forall a. Lock -> IO a -> IO a
withLock Lock
lock (Assertion -> Property) -> Assertion -> Property
forall a b. (a -> b) -> a -> b
$ do
    IO [()] -> Assertion
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO [()] -> Assertion) -> IO [()] -> Assertion
forall a b. (a -> b) -> a -> b
$ forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES_ @v PinnedSizedBytes (SeedSizeKES v)
seedPSB ((SignKeyKES v -> Assertion) -> IO [()])
-> (SignKeyKES v -> Assertion) -> IO [()]
forall a b. (a -> b) -> a -> b
$ Assertion -> SignKeyKES v -> Assertion
forall a b. a -> b -> a
const (() -> Assertion
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

-- | If we start with a signing key, we can evolve it a number of times so that
-- the total number of signing keys (including the initial one) equals the
-- total number of periods for this algorithm.
prop_totalPeriodsKES ::
  forall v.
  ( ContextKES v ~ ()
  , KESAlgorithm v
  ) =>
  Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_totalPeriodsKES :: forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_totalPeriodsKES Lock
lock PinnedSizedBytes (SeedSizeKES v)
seed =
  IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property)
-> (IO Property -> IO Property) -> IO Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lock -> IO Property -> IO Property
forall a. Lock -> IO a -> IO a
withLock Lock
lock (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    [()]
sks <- forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES_ @v PinnedSizedBytes (SeedSizeKES v)
seed (Assertion -> SignKeyKES v -> Assertion
forall a b. a -> b -> a
const (Assertion -> SignKeyKES v -> Assertion)
-> (() -> Assertion) -> () -> SignKeyKES v -> Assertion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Assertion
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> SignKeyKES v -> Assertion)
-> () -> SignKeyKES v -> Assertion
forall a b. (a -> b) -> a -> b
$ ())
    Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
      Int
totalPeriods Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (Int -> TestName
forall a. Show a => a -> TestName
show Int
totalPeriods) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (Int -> TestName
forall a. Show a => a -> TestName
show (Int -> TestName) -> Int -> TestName
forall a b. (a -> b) -> a -> b
$ [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [()]
sks) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [()]
sks Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Int
totalPeriods
  where
    totalPeriods :: Int
    totalPeriods :: Int
totalPeriods = Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
forall (proxy :: * -> *). proxy v -> Word
totalPeriodsKES (Proxy v
forall {k} (t :: k). Proxy t
Proxy :: Proxy v))

-- | If we start with a signing key, and all its evolutions, the verification
-- keys we derive from each one are the same.
prop_deriveVerKeyKES ::
  forall v.
  ( ContextKES v ~ ()
  , KESAlgorithm v
  ) =>
  PinnedSizedBytes (SeedSizeKES v) -> Property
prop_deriveVerKeyKES :: forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Property
prop_deriveVerKeyKES PinnedSizedBytes (SeedSizeKES v)
seedPSB =
  IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    VerKeyKES v
vk_0 <- do
      SignKeyKES v
sk_0 <- PinnedSizedBytes (SeedSizeKES v)
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB ((MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
 -> IO (SignKeyKES v))
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall a b. (a -> b) -> a -> b
$ forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES @v
      VerKeyKES v
vk_0 <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0
      SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0
      VerKeyKES v -> IO (VerKeyKES v)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return VerKeyKES v
vk_0

    [VerKeyKES v]
vks <- PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO (VerKeyKES v)) -> IO [VerKeyKES v]
forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES_ PinnedSizedBytes (SeedSizeKES v)
seedPSB SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES
    Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
      TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample ([VerKeyKES v] -> TestName
forall a. Show a => a -> TestName
show [VerKeyKES v]
vks) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ((VerKeyKES v -> Property) -> [VerKeyKES v] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (VerKeyKES v
vk_0 VerKeyKES v -> VerKeyKES v -> Property
forall a. (Eq a, Show a) => a -> a -> Property
===) [VerKeyKES v]
vks)

-- | If we take an initial signing key, a sequence of messages to sign, and
-- sign each one with an updated key, we can verify each one for the
-- corresponding period.
prop_verifyKES_positive ::
  forall v.
  ( ContextKES v ~ ()
  , Signable v ~ SignableRepresentation
  , KESAlgorithm v
  ) =>
  PinnedSizedBytes (SeedSizeKES v) -> Gen Property
prop_verifyKES_positive :: forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Gen Property
prop_verifyKES_positive PinnedSizedBytes (SeedSizeKES v)
seedPSB = do
  [Message]
xs :: [Message] <- Int -> Gen Message -> Gen [Message]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
totalPeriods Gen Message
forall a. Arbitrary a => Gen a
arbitrary
  Property -> Gen Property
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
    Property -> Property
forall prop. Testable prop => prop -> Property
checkCoverage (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      Double -> Bool -> TestName -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> TestName -> prop -> Property
cover Double
1 ([Message] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Message]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
totalPeriods) TestName
"Message count covers total periods" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        Bool -> Bool
not ([Message] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Message]
xs) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
          IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$
            ([Property] -> Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin (IO [Property] -> IO Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> a -> b
$ do
              SignKeyKES v
sk_0 <- PinnedSizedBytes (SeedSizeKES v)
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB ((MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
 -> IO (SignKeyKES v))
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall a b. (a -> b) -> a -> b
$ forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES @v
              VerKeyKES v
vk <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0
              SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0
              PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB ((Word -> SignKeyKES v -> IO Property) -> IO [Property])
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
                let x :: Message
x = [Message] -> [Message]
forall a. HasCallStack => [a] -> [a]
cycle [Message]
xs [Message] -> Int -> Message
forall a. HasCallStack => [a] -> Int -> a
!! Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
t
                SigKES v
sig <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
                let verResult :: Either TestName ()
verResult = ContextKES v
-> VerKeyKES v -> Word -> Message -> SigKES v -> Either TestName ()
forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
forall a.
(Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
verifyKES () VerKeyKES v
vk Word
t Message
x SigKES v
sig
                Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
                  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> TestName
forall a. Show a => a -> TestName
show Word
t TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ TestName
"/" TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> TestName
forall a. Show a => a -> TestName
show Int
totalPeriods) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                    Either TestName ()
verResult Either TestName () -> Either TestName () -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== () -> Either TestName ()
forall a b. b -> Either a b
Right ()
  where
    totalPeriods :: Int
    totalPeriods :: Int
totalPeriods = Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
forall (proxy :: * -> *). proxy v -> Word
totalPeriodsKES (Proxy v
forall {k} (t :: k). Proxy t
Proxy :: Proxy v))

-- | If we sign a message @a@with one list of signing key evolutions, if we
-- try to verify the signature (and message @a@) using a verification key
-- corresponding to a different signing key, then the verification fails.
prop_verifyKES_negative_key ::
  forall v.
  ( ContextKES v ~ ()
  , Signable v ~ SignableRepresentation
  , KESAlgorithm v
  ) =>
  PinnedSizedBytes (SeedSizeKES v) ->
  PinnedSizedBytes (SeedSizeKES v) ->
  Message ->
  Property
prop_verifyKES_negative_key :: forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v)
-> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property
prop_verifyKES_negative_key PinnedSizedBytes (SeedSizeKES v)
seedPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB' Message
x =
  PinnedSizedBytes (SeedSizeKES v)
seedPSB PinnedSizedBytes (SeedSizeKES v)
-> PinnedSizedBytes (SeedSizeKES v) -> Bool
forall a. Eq a => a -> a -> Bool
/= PinnedSizedBytes (SeedSizeKES v)
seedPSB' Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ ([Property] -> Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin (IO [Property] -> IO Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> a -> b
$ do
    SignKeyKES v
sk_0' <- PinnedSizedBytes (SeedSizeKES v)
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB' ((MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
 -> IO (SignKeyKES v))
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall a b. (a -> b) -> a -> b
$ forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES @v
    VerKeyKES v
vk' <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0'
    SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0'
    PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB ((Word -> SignKeyKES v -> IO Property) -> IO [Property])
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      SigKES v
sig <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
      let verResult :: Either TestName ()
verResult = ContextKES v
-> VerKeyKES v -> Word -> Message -> SigKES v -> Either TestName ()
forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
forall a.
(Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
verifyKES () VerKeyKES v
vk' Word
t Message
x SigKES v
sig
      Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> TestName
forall a. Show a => a -> TestName
show Word
t) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Either TestName ()
verResult Either TestName () -> Either TestName () -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=/= () -> Either TestName ()
forall a b. b -> Either a b
Right ()

-- | If we sign a message @a@with one list of signing key evolutions, if we
-- try to verify the signature with a message other than @a@, then the
-- verification fails.
prop_verifyKES_negative_message ::
  forall v.
  ( ContextKES v ~ ()
  , Signable v ~ SignableRepresentation
  , KESAlgorithm v
  ) =>
  PinnedSizedBytes (SeedSizeKES v) ->
  Message ->
  Message ->
  Property
prop_verifyKES_negative_message :: forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Message -> Message -> Property
prop_verifyKES_negative_message PinnedSizedBytes (SeedSizeKES v)
seedPSB Message
x Message
x' =
  Message
x Message -> Message -> Bool
forall a. Eq a => a -> a -> Bool
/= Message
x' Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ ([Property] -> Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin (IO [Property] -> IO Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> a -> b
$ do
    SignKeyKES v
sk_0 <- PinnedSizedBytes (SeedSizeKES v)
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB ((MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
 -> IO (SignKeyKES v))
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall a b. (a -> b) -> a -> b
$ forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES @v
    VerKeyKES v
vk <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0
    SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0
    PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB ((Word -> SignKeyKES v -> IO Property) -> IO [Property])
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      SigKES v
sig <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
      let verResult :: Either TestName ()
verResult = ContextKES v
-> VerKeyKES v -> Word -> Message -> SigKES v -> Either TestName ()
forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
forall a.
(Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
verifyKES () VerKeyKES v
vk Word
t Message
x' SigKES v
sig
      Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> TestName
forall a. Show a => a -> TestName
show Word
t) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Either TestName ()
verResult Either TestName () -> Either TestName () -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=/= () -> Either TestName ()
forall a b. b -> Either a b
Right ()

-- | If we sign a message @a@with one list of signing key evolutions, if we
-- try to verify the signature (and message @a@) using the right verification
-- key but at a different period than the key used for signing, then the
-- verification fails.
prop_verifyKES_negative_period ::
  forall v.
  ( ContextKES v ~ ()
  , Signable v ~ SignableRepresentation
  , KESAlgorithm v
  ) =>
  PinnedSizedBytes (SeedSizeKES v) ->
  Message ->
  Property
prop_verifyKES_negative_period :: forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Message -> Property
prop_verifyKES_negative_period PinnedSizedBytes (SeedSizeKES v)
seedPSB Message
x =
  IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ ([Property] -> Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin (IO [Property] -> IO Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> a -> b
$ do
    SignKeyKES v
sk_0 <- PinnedSizedBytes (SeedSizeKES v)
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB ((MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
 -> IO (SignKeyKES v))
-> (MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v))
-> IO (SignKeyKES v)
forall a b. (a -> b) -> a -> b
$ forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES @v
    VerKeyKES v
vk <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0
    SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0
    PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB ((Word -> SignKeyKES v -> IO Property) -> IO [Property])
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      SigKES v
sig <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
      Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
        [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
          [ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"periods " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ (Word, Word) -> TestName
forall a. Show a => a -> TestName
show (Word
t, Word
t')) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              ContextKES v
-> VerKeyKES v -> Word -> Message -> SigKES v -> Either TestName ()
forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
forall a.
(Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
verifyKES () VerKeyKES v
vk Word
t' Message
x SigKES v
sig Either TestName () -> Either TestName () -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=/= () -> Either TestName ()
forall a b. b -> Either a b
Right ()
          | Word
t' <- [Word
0 .. Word
totalPeriods Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1]
          , Word
t Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
/= Word
t'
          ]
  where
    totalPeriods :: Word
    totalPeriods :: Word
totalPeriods = Word -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
forall (proxy :: * -> *). proxy v -> Word
totalPeriodsKES (Proxy v
forall {k} (t :: k). Proxy t
Proxy :: Proxy v))

-- | Check 'prop_raw_serialise', 'prop_cbor_with' and 'prop_size_serialise'
-- for 'VerKeyKES' on /all/ the KES key evolutions.
prop_serialise_VerKeyKES ::
  forall v.
  ( ContextKES v ~ ()
  , KESAlgorithm v
  ) =>
  PinnedSizedBytes (SeedSizeKES v) ->
  Property
prop_serialise_VerKeyKES :: forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Property
prop_serialise_VerKeyKES PinnedSizedBytes (SeedSizeKES v)
seedPSB =
  IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ ([Property] -> Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin (IO [Property] -> IO Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> a -> b
$ do
    forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES @v PinnedSizedBytes (SeedSizeKES v)
seedPSB ((Word -> SignKeyKES v -> IO Property) -> IO [Property])
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      VerKeyKES v
vk <- SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
      Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> TestName
forall a. Show a => a -> TestName
show Word
t) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"vkey " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ VerKeyKES v -> TestName
forall a. Show a => a -> TestName
show VerKeyKES v
vk) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            (VerKeyKES v -> ByteString)
-> (ByteString -> Maybe (VerKeyKES v)) -> VerKeyKES v -> Property
forall a.
(Eq a, Show a) =>
(a -> ByteString) -> (ByteString -> Maybe a) -> a -> Property
prop_raw_serialise
              VerKeyKES v -> ByteString
forall v. KESAlgorithm v => VerKeyKES v -> ByteString
rawSerialiseVerKeyKES
              ByteString -> Maybe (VerKeyKES v)
forall v. KESAlgorithm v => ByteString -> Maybe (VerKeyKES v)
rawDeserialiseVerKeyKES
              VerKeyKES v
vk
              Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. (VerKeyKES v -> Encoding)
-> (forall s. Decoder s (VerKeyKES v)) -> VerKeyKES v -> Property
forall a.
(Eq a, Show a) =>
(a -> Encoding) -> (forall s. Decoder s a) -> a -> Property
prop_cbor_with
                VerKeyKES v -> Encoding
forall v. KESAlgorithm v => VerKeyKES v -> Encoding
encodeVerKeyKES
                Decoder s (VerKeyKES v)
forall s. Decoder s (VerKeyKES v)
forall v s. KESAlgorithm v => Decoder s (VerKeyKES v)
decodeVerKeyKES
                VerKeyKES v
vk
              Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. (VerKeyKES v -> ByteString) -> Word -> VerKeyKES v -> Property
forall a. (a -> ByteString) -> Word -> a -> Property
prop_size_serialise
                VerKeyKES v -> ByteString
forall v. KESAlgorithm v => VerKeyKES v -> ByteString
rawSerialiseVerKeyKES
                (Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeVerKeyKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v))
                VerKeyKES v
vk

-- | Check 'prop_raw_serialise', 'prop_cbor_with' and 'prop_size_serialise'
-- for 'SigKES' on /all/ the KES key evolutions.
prop_serialise_SigKES ::
  forall v.
  ( ContextKES v ~ ()
  , Signable v ~ SignableRepresentation
  , Show (SignKeyKES v)
  , KESAlgorithm v
  ) =>
  PinnedSizedBytes (SeedSizeKES v) ->
  Message ->
  Property
prop_serialise_SigKES :: forall v.
(ContextKES v ~ (), Signable v ~ SignableRepresentation,
 Show (SignKeyKES v), KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Message -> Property
prop_serialise_SigKES PinnedSizedBytes (SeedSizeKES v)
seedPSB Message
x =
  IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ ([Property] -> Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin (IO [Property] -> IO Property) -> IO [Property] -> IO Property
forall a b. (a -> b) -> a -> b
$ do
    forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES @v PinnedSizedBytes (SeedSizeKES v)
seedPSB ((Word -> SignKeyKES v -> IO Property) -> IO [Property])
-> (Word -> SignKeyKES v -> IO Property) -> IO [Property]
forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      SigKES v
sig <- ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
      Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$
        TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> TestName
forall a. Show a => a -> TestName
show Word
t) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"vkey " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ SignKeyKES v -> TestName
forall a. Show a => a -> TestName
show SignKeyKES v
sk) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"sig " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ SigKES v -> TestName
forall a. Show a => a -> TestName
show SigKES v
sig) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              (SigKES v -> ByteString)
-> (ByteString -> Maybe (SigKES v)) -> SigKES v -> Property
forall a.
(Eq a, Show a) =>
(a -> ByteString) -> (ByteString -> Maybe a) -> a -> Property
prop_raw_serialise
                SigKES v -> ByteString
forall v. KESAlgorithm v => SigKES v -> ByteString
rawSerialiseSigKES
                ByteString -> Maybe (SigKES v)
forall v. KESAlgorithm v => ByteString -> Maybe (SigKES v)
rawDeserialiseSigKES
                SigKES v
sig
                Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. (SigKES v -> Encoding)
-> (forall s. Decoder s (SigKES v)) -> SigKES v -> Property
forall a.
(Eq a, Show a) =>
(a -> Encoding) -> (forall s. Decoder s a) -> a -> Property
prop_cbor_with
                  SigKES v -> Encoding
forall v. KESAlgorithm v => SigKES v -> Encoding
encodeSigKES
                  Decoder s (SigKES v)
forall s. Decoder s (SigKES v)
forall v s. KESAlgorithm v => Decoder s (SigKES v)
decodeSigKES
                  SigKES v
sig
                Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. (SigKES v -> ByteString) -> Word -> SigKES v -> Property
forall a. (a -> ByteString) -> Word -> a -> Property
prop_size_serialise
                  SigKES v -> ByteString
forall v. KESAlgorithm v => SigKES v -> ByteString
rawSerialiseSigKES
                  (Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSigKES (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @v))
                  SigKES v
sig

--
-- KES test utils
--

withAllUpdatesKES_ ::
  forall v a.
  ( KESAlgorithm v
  , ContextKES v ~ ()
  ) =>
  PinnedSizedBytes (SeedSizeKES v) ->
  (SignKeyKES v -> IO a) ->
  IO [a]
withAllUpdatesKES_ :: forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES_ PinnedSizedBytes (SeedSizeKES v)
seedPSB SignKeyKES v -> IO a
f = do
  PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB ((SignKeyKES v -> IO a) -> Word -> SignKeyKES v -> IO a
forall a b. a -> b -> a
const SignKeyKES v -> IO a
f)

withAllUpdatesKES ::
  forall v a.
  ( KESAlgorithm v
  , ContextKES v ~ ()
  ) =>
  PinnedSizedBytes (SeedSizeKES v) ->
  (Word -> SignKeyKES v -> IO a) ->
  IO [a]
withAllUpdatesKES :: forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB Word -> SignKeyKES v -> IO a
f = PinnedSizedBytes (SeedSizeKES v)
-> (MLockedSeed (SeedSizeKES v) -> IO [a]) -> IO [a]
forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB ((MLockedSeed (SeedSizeKES v) -> IO [a]) -> IO [a])
-> (MLockedSeed (SeedSizeKES v) -> IO [a]) -> IO [a]
forall a b. (a -> b) -> a -> b
$ \MLockedSeed (SeedSizeKES v)
seed -> do
  SignKeyKES v
sk_0 <- MLockedSeed (SeedSizeKES v) -> IO (SignKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES MLockedSeed (SeedSizeKES v)
seed
  SignKeyKES v -> Word -> IO [a]
go SignKeyKES v
sk_0 Word
0
  where
    go :: SignKeyKES v -> Word -> IO [a]
    go :: SignKeyKES v -> Word -> IO [a]
go SignKeyKES v
sk Word
t = do
      a
x <- Word -> SignKeyKES v -> IO a
f Word
t SignKeyKES v
sk
      Maybe (SignKeyKES v)
msk' <- ContextKES v -> SignKeyKES v -> Word -> IO (Maybe (SignKeyKES v))
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
ContextKES v -> SignKeyKES v -> Word -> m (Maybe (SignKeyKES v))
updateKES () SignKeyKES v
sk Word
t
      case Maybe (SignKeyKES v)
msk' of
        Maybe (SignKeyKES v)
Nothing -> do
          SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk
          [a] -> IO [a]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [a
x]
        Just SignKeyKES v
sk' -> do
          SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk
          [a]
xs <- SignKeyKES v -> Word -> IO [a]
go SignKeyKES v
sk' (Word
t Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1)
          [a] -> IO [a]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> IO [a]) -> [a] -> IO [a]
forall a b. (a -> b) -> a -> b
$ a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs

withNullSeed :: forall m n a. (MonadThrow m, MonadST m, KnownNat n) => (MLockedSeed n -> m a) -> m a
withNullSeed :: forall (m :: * -> *) (n :: Nat) a.
(MonadThrow m, MonadST m, KnownNat n) =>
(MLockedSeed n -> m a) -> m a
withNullSeed =
  m (MLockedSeed n)
-> (MLockedSeed n -> m ()) -> (MLockedSeed n -> m a) -> m a
forall a b c. m a -> (a -> m b) -> (a -> m c) -> m c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
    (MLockedSizedBytes n -> MLockedSeed n
forall (n :: Nat). MLockedSizedBytes n -> MLockedSeed n
MLockedSeed (MLockedSizedBytes n -> MLockedSeed n)
-> m (MLockedSizedBytes n) -> m (MLockedSeed n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ByteString -> m (MLockedSizedBytes n)
forall (n :: Nat) (m :: * -> *).
(KnownNat n, MonadST m) =>
ByteString -> m (MLockedSizedBytes n)
mlsbFromByteString (Int -> Word8 -> ByteString
BS.replicate (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) Word8
0))
    MLockedSeed n -> m ()
forall (m :: * -> *) (n :: Nat). MonadST m => MLockedSeed n -> m ()
mlockedSeedFinalize

withNullSK ::
  forall m v a.
  (KESAlgorithm v, MonadThrow m, MonadST m) =>
  (SignKeyKES v -> m a) -> m a
withNullSK :: forall (m :: * -> *) v a.
(KESAlgorithm v, MonadThrow m, MonadST m) =>
(SignKeyKES v -> m a) -> m a
withNullSK =
  m (SignKeyKES v)
-> (SignKeyKES v -> m ()) -> (SignKeyKES v -> m a) -> m a
forall a b c. m a -> (a -> m b) -> (a -> m c) -> m c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
    ((MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v))
-> m (SignKeyKES v)
forall (m :: * -> *) (n :: Nat) a.
(MonadThrow m, MonadST m, KnownNat n) =>
(MLockedSeed n -> m a) -> m a
withNullSeed MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES)
    SignKeyKES v -> m ()
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES

-- | This test detects whether a sign key contains references to pool-allocated
-- blocks of memory that have been forgotten by the time the key is complete.
-- We do this based on the fact that the pooled allocator erases memory blocks
-- by overwriting them with series of 0xff bytes; thus we cut the serialized
-- key up into chunks of 16 bytes, and if any of those chunks is entirely
-- filled with 0xff bytes, we assume that we're looking at erased memory.
prop_noErasedBlocksInKey ::
  forall v.
  UnsoundKESAlgorithm v =>
  DirectSerialise (SignKeyKES v) =>
  Proxy v ->
  Property
prop_noErasedBlocksInKey :: forall v.
(UnsoundKESAlgorithm v, DirectSerialise (SignKeyKES v)) =>
Proxy v -> Property
prop_noErasedBlocksInKey Proxy v
kesAlgorithm =
  IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property)
-> ((SignKeyKES v -> IO Property) -> IO Property)
-> (SignKeyKES v -> IO Property)
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) v a.
(KESAlgorithm v, MonadThrow m, MonadST m) =>
(SignKeyKES v -> m a) -> m a
withNullSK @IO @v ((SignKeyKES v -> IO Property) -> Property)
-> (SignKeyKES v -> IO Property) -> Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
    let Int
size :: Int = Word -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word -> Int) -> Word -> Int
forall a b. (a -> b) -> a -> b
$ Proxy v -> Word
forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSignKeyKES Proxy v
kesAlgorithm
    ByteString
serialized <- Int -> SignKeyKES v -> IO ByteString
forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS Int
size SignKeyKES v
sk
    SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk
    Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (ByteString -> TestName
hexBS ByteString
serialized) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (ByteString -> Bool
hasLongRunOfFF ByteString
serialized)

hasLongRunOfFF :: ByteString -> Bool
hasLongRunOfFF :: ByteString -> Bool
hasLongRunOfFF ByteString
bs
  | ByteString -> Int
BS.length ByteString
bs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
16 =
      Bool
False
  | Bool
otherwise =
      let first16 :: ByteString
first16 = Int -> ByteString -> ByteString
BS.take Int
16 ByteString
bs
          remainder :: ByteString
remainder = Int -> ByteString -> ByteString
BS.drop Int
16 ByteString
bs
       in (Word8 -> Bool) -> ByteString -> Bool
BS.all (Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0xFF) ByteString
first16 Bool -> Bool -> Bool
|| ByteString -> Bool
hasLongRunOfFF ByteString
remainder

prop_unsoundPureGenKey ::
  forall v.
  ( UnsoundPureKESAlgorithm v
  , EqST (SignKeyKES v)
  ) =>
  Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureGenKey :: forall v.
(UnsoundPureKESAlgorithm v, EqST (SignKeyKES v)) =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureGenKey Proxy v
_ PinnedSizedBytes (SeedSizeKES v)
seedPSB = IO Bool -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Bool -> Property) -> IO Bool -> Property
forall a b. (a -> b) -> a -> b
$ do
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes (ByteString -> Seed) -> ByteString -> Seed
forall a b. (a -> b) -> a -> b
$ PinnedSizedBytes (SeedSizeKES v) -> ByteString
forall (n :: Nat). PinnedSizedBytes n -> ByteString
psbToByteString PinnedSizedBytes (SeedSizeKES v)
seedPSB
  let skPure :: UnsoundPureSignKeyKES v
skPure = forall v.
UnsoundPureKESAlgorithm v =>
Seed -> UnsoundPureSignKeyKES v
unsoundPureGenKeyKES @v Seed
seed
  PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO Bool) -> IO Bool
forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB ((SignKeyKES v -> IO Bool) -> IO Bool)
-> (SignKeyKES v -> IO Bool) -> IO Bool
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
    IO (SignKeyKES v)
-> (SignKeyKES v -> Assertion)
-> (SignKeyKES v -> IO Bool)
-> IO Bool
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
      (UnsoundPureSignKeyKES v -> IO (SignKeyKES v)
forall v (m :: * -> *).
(UnsoundPureKESAlgorithm v, MonadST m, MonadThrow m) =>
UnsoundPureSignKeyKES v -> m (SignKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
UnsoundPureSignKeyKES v -> m (SignKeyKES v)
unsoundPureSignKeyKESToSoundSignKeyKES UnsoundPureSignKeyKES v
skPure)
      SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES
      (SignKeyKES v -> SignKeyKES v -> IO Bool
forall a (m :: * -> *). (EqST a, MonadST m) => a -> a -> m Bool
forall (m :: * -> *).
MonadST m =>
SignKeyKES v -> SignKeyKES v -> m Bool
equalsM SignKeyKES v
sk)

prop_unsoundPureDeriveVerKey ::
  forall v.
  UnsoundPureKESAlgorithm v =>
  Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureDeriveVerKey :: forall v.
UnsoundPureKESAlgorithm v =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureDeriveVerKey Proxy v
_ PinnedSizedBytes (SeedSizeKES v)
seedPSB = IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes (ByteString -> Seed) -> ByteString -> Seed
forall a b. (a -> b) -> a -> b
$ PinnedSizedBytes (SeedSizeKES v) -> ByteString
forall (n :: Nat). PinnedSizedBytes n -> ByteString
psbToByteString PinnedSizedBytes (SeedSizeKES v)
seedPSB
  let skPure :: UnsoundPureSignKeyKES v
skPure = forall v.
UnsoundPureKESAlgorithm v =>
Seed -> UnsoundPureSignKeyKES v
unsoundPureGenKeyKES @v Seed
seed
      vkPure :: VerKeyKES v
vkPure = forall v.
UnsoundPureKESAlgorithm v =>
UnsoundPureSignKeyKES v -> VerKeyKES v
unsoundPureDeriveVerKeyKES @v UnsoundPureSignKeyKES v
skPure
  VerKeyKES v
vk <- PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO (VerKeyKES v)) -> IO (VerKeyKES v)
forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB SignKeyKES v -> IO (VerKeyKES v)
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES
  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ VerKeyKES v
vkPure VerKeyKES v -> VerKeyKES v -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== VerKeyKES v
vk

prop_unsoundPureUpdateKES ::
  forall v.
  ( UnsoundPureKESAlgorithm v
  , ContextKES v ~ ()
  , EqST (SignKeyKES v)
  ) =>
  Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureUpdateKES :: forall v.
(UnsoundPureKESAlgorithm v, ContextKES v ~ (),
 EqST (SignKeyKES v)) =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureUpdateKES Proxy v
_ PinnedSizedBytes (SeedSizeKES v)
seedPSB = IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes (ByteString -> Seed) -> ByteString -> Seed
forall a b. (a -> b) -> a -> b
$ PinnedSizedBytes (SeedSizeKES v) -> ByteString
forall (n :: Nat). PinnedSizedBytes n -> ByteString
psbToByteString PinnedSizedBytes (SeedSizeKES v)
seedPSB
  let skPure :: UnsoundPureSignKeyKES v
skPure = forall v.
UnsoundPureKESAlgorithm v =>
Seed -> UnsoundPureSignKeyKES v
unsoundPureGenKeyKES @v Seed
seed
      skPure'Maybe :: Maybe (UnsoundPureSignKeyKES v)
skPure'Maybe = ContextKES v
-> UnsoundPureSignKeyKES v
-> Word
-> Maybe (UnsoundPureSignKeyKES v)
forall v.
UnsoundPureKESAlgorithm v =>
ContextKES v
-> UnsoundPureSignKeyKES v
-> Word
-> Maybe (UnsoundPureSignKeyKES v)
unsoundPureUpdateKES () UnsoundPureSignKeyKES v
skPure Word
0
  PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO Property) -> IO Property
forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB ((SignKeyKES v -> IO Property) -> IO Property)
-> (SignKeyKES v -> IO Property) -> IO Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
    IO (Maybe (SignKeyKES v))
-> (Maybe (SignKeyKES v) -> Assertion)
-> (Maybe (SignKeyKES v) -> IO Property)
-> IO Property
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
      (ContextKES v -> SignKeyKES v -> Word -> IO (Maybe (SignKeyKES v))
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
ContextKES v -> SignKeyKES v -> Word -> m (Maybe (SignKeyKES v))
updateKES () SignKeyKES v
sk Word
0)
      (Assertion
-> (SignKeyKES v -> Assertion) -> Maybe (SignKeyKES v) -> Assertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Assertion
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES)
      ((Maybe (SignKeyKES v) -> IO Property) -> IO Property)
-> (Maybe (SignKeyKES v) -> IO Property) -> IO Property
forall a b. (a -> b) -> a -> b
$ \Maybe (SignKeyKES v)
sk'Maybe -> do
        case Maybe (UnsoundPureSignKeyKES v)
skPure'Maybe of
          Maybe (UnsoundPureSignKeyKES v)
Nothing ->
            case Maybe (SignKeyKES v)
sk'Maybe of
              Maybe (SignKeyKES v)
Nothing -> Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
              Just SignKeyKES v
_ -> Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"pure does not update, but should" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False
          Just UnsoundPureSignKeyKES v
skPure' ->
            IO (SignKeyKES v)
-> (SignKeyKES v -> Assertion)
-> (SignKeyKES v -> IO Property)
-> IO Property
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
              (UnsoundPureSignKeyKES v -> IO (SignKeyKES v)
forall v (m :: * -> *).
(UnsoundPureKESAlgorithm v, MonadST m, MonadThrow m) =>
UnsoundPureSignKeyKES v -> m (SignKeyKES v)
forall (m :: * -> *).
(MonadST m, MonadThrow m) =>
UnsoundPureSignKeyKES v -> m (SignKeyKES v)
unsoundPureSignKeyKESToSoundSignKeyKES UnsoundPureSignKeyKES v
skPure')
              SignKeyKES v -> Assertion
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES
              ((SignKeyKES v -> IO Property) -> IO Property)
-> (SignKeyKES v -> IO Property) -> IO Property
forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk'' ->
                case Maybe (SignKeyKES v)
sk'Maybe of
                  Maybe (SignKeyKES v)
Nothing ->
                    Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"pure updates, but shouldn't" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False)
                  Just SignKeyKES v
sk' ->
                    Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> IO Bool -> IO Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SignKeyKES v -> SignKeyKES v -> IO Bool
forall a (m :: * -> *). (EqST a, MonadST m) => a -> a -> m Bool
forall (m :: * -> *).
MonadST m =>
SignKeyKES v -> SignKeyKES v -> m Bool
equalsM SignKeyKES v
sk' SignKeyKES v
sk''

prop_unsoundPureSign ::
  forall v.
  ( UnsoundPureKESAlgorithm v
  , ContextKES v ~ ()
  , Signable v Message
  ) =>
  Proxy v ->
  PinnedSizedBytes (SeedSizeKES v) ->
  Message ->
  Property
prop_unsoundPureSign :: forall v.
(UnsoundPureKESAlgorithm v, ContextKES v ~ (),
 Signable v Message) =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property
prop_unsoundPureSign Proxy v
_ PinnedSizedBytes (SeedSizeKES v)
seedPSB Message
msg = IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes (ByteString -> Seed) -> ByteString -> Seed
forall a b. (a -> b) -> a -> b
$ PinnedSizedBytes (SeedSizeKES v) -> ByteString
forall (n :: Nat). PinnedSizedBytes n -> ByteString
psbToByteString PinnedSizedBytes (SeedSizeKES v)
seedPSB
  let skPure :: UnsoundPureSignKeyKES v
skPure = forall v.
UnsoundPureKESAlgorithm v =>
Seed -> UnsoundPureSignKeyKES v
unsoundPureGenKeyKES @v Seed
seed
      sigPure :: SigKES v
sigPure = ContextKES v
-> Word -> Message -> UnsoundPureSignKeyKES v -> SigKES v
forall v a.
(UnsoundPureKESAlgorithm v, Signable v a) =>
ContextKES v -> Word -> a -> UnsoundPureSignKeyKES v -> SigKES v
forall a.
Signable v a =>
ContextKES v -> Word -> a -> UnsoundPureSignKeyKES v -> SigKES v
unsoundPureSignKES () Word
0 Message
msg UnsoundPureSignKeyKES v
skPure
  SigKES v
sig <- PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO (SigKES v)) -> IO (SigKES v)
forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB ((SignKeyKES v -> IO (SigKES v)) -> IO (SigKES v))
-> (SignKeyKES v -> IO (SigKES v)) -> IO (SigKES v)
forall a b. (a -> b) -> a -> b
$ ContextKES v -> Word -> Message -> SignKeyKES v -> IO (SigKES v)
forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
forall a (m :: * -> *).
(Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
0 Message
msg
  Property -> IO Property
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ SigKES v
sigPure SigKES v -> SigKES v -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== SigKES v
sig