{-# 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.Hspec (Expectation, Spec, describe, it, shouldSatisfy)
import Test.Hspec.QuickCheck (modifyMaxSuccess, prop)
import Test.QuickCheck

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 -> Spec
tests :: Lock -> Spec
tests Lock
lock =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Crypto.KES" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    Proxy (SingleKES Ed25519DSIGN) -> String -> Spec
forall v. KESAlgorithm v => Proxy v -> String -> Spec
testKESAlloc (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(SingleKES Ed25519DSIGN)) String
"SingleKES"
    Proxy (Sum1KES Ed25519DSIGN Blake2b_256) -> String -> Spec
forall v. KESAlgorithm v => Proxy v -> String -> Spec
testKESAlloc (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Sum1KES Ed25519DSIGN Blake2b_256)) String
"Sum1KES"
    Proxy (Sum2KES Ed25519DSIGN Blake2b_256) -> String -> Spec
forall v. KESAlgorithm v => Proxy v -> String -> Spec
testKESAlloc (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Sum2KES Ed25519DSIGN Blake2b_256)) String
"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 -> String -> Spec
testKESAlgorithm @(MockKES 7) Lock
lock String
"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 -> String -> Spec
testKESAlgorithm @(SimpleKES Ed25519DSIGN 7) Lock
lock String
"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 -> String -> Spec
testKESAlgorithm @(SingleKES Ed25519DSIGN) Lock
lock String
"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 -> String -> Spec
testKESAlgorithm @(Sum1KES Ed25519DSIGN Blake2b_256) Lock
lock String
"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 -> String -> Spec
testKESAlgorithm @(Sum2KES Ed25519DSIGN Blake2b_256) Lock
lock String
"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 -> String -> Spec
testKESAlgorithm @(Sum5KES Ed25519DSIGN Blake2b_256) Lock
lock String
"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 -> String -> Spec
testKESAlgorithm @(CompactSum1KES Ed25519DSIGN Blake2b_256) Lock
lock String
"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 -> String -> Spec
testKESAlgorithm @(CompactSum2KES Ed25519DSIGN Blake2b_256) Lock
lock String
"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 -> String -> Spec
testKESAlgorithm @(CompactSum5KES Ed25519DSIGN Blake2b_256) Lock
lock String
"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) -> String
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 :: String
hexstr = ByteString -> String
hexBS ByteString
bytes
     in String
"SignKeySingleKES (SignKeyEd25519DSIGNM " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hexstr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

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

instance Show (SignKeyKES (CompactSingleKES Ed25519DSIGN)) where
  show :: SignKeyKES (CompactSingleKES Ed25519DSIGN) -> String
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 :: String
hexstr = ByteString -> String
hexBS ByteString
bytes
     in String
"SignKeyCompactSingleKES (SignKeyEd25519DSIGNM " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hexstr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance Show (SignKeyKES (CompactSumKES h d)) where
  show :: SignKeyKES (CompactSumKES h d) -> String
show SignKeyKES (CompactSumKES h d)
_ = String
"<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 -> String -> Gen (UnsoundPureSignKeyKES k)
forall a. HasCallStack => String -> a
error String
"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 ->
  Spec
testKESAlloc :: forall v. KESAlgorithm v => Proxy v -> String -> Spec
testKESAlloc Proxy v
_p String
n =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
n (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Low-level mlocked allocations" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      -- it "updateKey" $ testMLockUpdateKeyKES _p
      String -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"genKey" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$ Proxy v -> Expectation
forall v. KESAlgorithm v => Proxy v -> Expectation
testMLockGenKeyKES Proxy v
_p

eventTracer :: IORef [event] -> Tracer IO event
eventTracer :: forall event. IORef [event] -> Tracer IO event
eventTracer IORef [event]
logVar = (event -> Expectation) -> Tracer IO event
forall (m :: * -> *) a. (a -> m ()) -> Tracer m a
Tracer (\event
ev -> Expectation -> Expectation
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Expectation -> Expectation) -> Expectation -> Expectation
forall a b. (a -> b) -> a -> b
$ IORef [event] -> ([event] -> ([event], ())) -> Expectation
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 String
_) = Set WordPtr -> Set WordPtr
forall a. a -> a
id

testMLockGenKeyKES ::
  forall v.
  KESAlgorithm v =>
  Proxy v ->
  Expectation
testMLockGenKeyKES :: forall v. KESAlgorithm v => Proxy v -> Expectation
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 -> Expectation
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Expectation) -> AllocEvent -> Expectation
forall a b. (a -> b) -> a -> b
$ String -> AllocEvent
MarkerEv String
"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 -> Expectation
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Expectation) -> AllocEvent -> Expectation
forall a b. (a -> b) -> a -> b
$ String -> AllocEvent
MarkerEv String
"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 -> Expectation
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Expectation) -> AllocEvent -> Expectation
forall a b. (a -> b) -> a -> b
$ String -> AllocEvent
MarkerEv String
"forget key"
  MLockedAllocator IO -> SignKeyKES v -> Expectation
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 -> Expectation
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Expectation) -> AllocEvent -> Expectation
forall a b. (a -> b) -> a -> b
$ String -> AllocEvent
MarkerEv String
"forget seed"
  MLockedSeed (SeedSizeKES v) -> Expectation
forall (m :: * -> *) (n :: Nat). MonadST m => MLockedSeed n -> m ()
mlockedSeedFinalize MLockedSeed (SeedSizeKES v)
seed
  Tracer IO AllocEvent -> AllocEvent -> Expectation
forall (m :: * -> *) a. Tracer m a -> a -> m ()
traceWith Tracer IO AllocEvent
tracer (AllocEvent -> Expectation) -> AllocEvent -> Expectation
forall a b. (a -> b) -> a -> b
$ String -> AllocEvent
MarkerEv String
"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
  [() | AllocEv WordPtr
_ <- [AllocEvent]
after] [()] -> ([()] -> Bool) -> Expectation
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> Expectation
`shouldSatisfy` (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) -- some allocations happened
  Set WordPtr
evset Set WordPtr -> (Set WordPtr -> Bool) -> Expectation
forall a. (HasCallStack, Show a) => a -> (a -> Bool) -> Expectation
`shouldSatisfy` Set WordPtr -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null -- all allocations deallocated

{-# 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 ->
  Spec
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 -> String -> Spec
testKESAlgorithm Lock
lock String
n =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
n (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"only gen signkey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ forall v.
KESAlgorithm v =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_onlyGenSignKeyKES @v Lock
lock
    String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"only gen verkey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ forall v.
KESAlgorithm v =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_onlyGenVerKeyKES @v Lock
lock
    String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"one update signkey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_oneUpdateSignKeyKES @v Lock
lock
    String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"all updates signkey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_allUpdatesSignKeyKES @v Lock
lock
    String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"total periods" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
Lock -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_totalPeriodsKES @v Lock
lock
    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"NoThunks" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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)
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"SignKey evolved" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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) -> Expectation)
-> (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)
            (Expectation
-> (SignKeyKES v -> Expectation)
-> Maybe (SignKeyKES v)
-> Expectation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Expectation
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) SignKeyKES v -> Expectation
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)
      String
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Sig" ((PinnedSizedBytes (SeedSizeKES v) -> Message -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
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)
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey DirectSerialise" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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)
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"SignKey DirectSerialise" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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)
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey DirectDeserialise" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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)
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"SignKey DirectDeserialise" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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 -> Expectation)
-> (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 -> Expectation
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)
    String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"same VerKey " ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Property
prop_deriveVerKeyKES @v
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"no forgotten chunks in signkey" (Property -> Spec) -> Property -> Spec
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)
    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"serialisation" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"raw ser only" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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) -> Expectation)
-> (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)
                (Expectation
-> (SignKeyKES v -> Expectation)
-> Maybe (SignKeyKES v)
-> Expectation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Expectation
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) SignKeyKES v -> Expectation
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
$
              String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (ByteString -> String
forall a. Show a => a -> String
show ByteString
serialized) Bool
equals
        String
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
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
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"size" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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)
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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))
        String
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
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)
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"direct CBOR" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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.
        String
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
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
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"UnsoundSignKeyKES" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"To/FromCBOR class" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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.
        String
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
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
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"ToCBOR size" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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.
        String
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
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
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"direct matches class" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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.
        String
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Sig" ((Message -> PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (Message -> PinnedSizedBytes (SeedSizeKES v) -> Property)
-> Spec
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
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"DirectSerialise" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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'
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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 -> Expectation)
-> (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 -> Expectation
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
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                (String
"Serialized: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ByteString -> String
hexBS ByteString
serialized String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (length: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (ByteString -> Int
BS.length ByteString
serialized) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")
              (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Bool
equals
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"DirectSerialise matches raw" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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
        String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"SignKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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
    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"verify" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String
-> (PinnedSizedBytes (SeedSizeKES v) -> Gen Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"positive" ((PinnedSizedBytes (SeedSizeKES v) -> Gen Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Gen Property) -> Spec
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
      String
-> (PinnedSizedBytes (SeedSizeKES v)
    -> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"negative (key)" ((PinnedSizedBytes (SeedSizeKES v)
  -> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
 -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v)
    -> PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
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
      String
-> (PinnedSizedBytes (SeedSizeKES v)
    -> Message -> Message -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"negative (message)" ((PinnedSizedBytes (SeedSizeKES v)
  -> Message -> Message -> Property)
 -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v)
    -> Message -> Message -> Property)
-> Spec
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
      (Int -> Int) -> Spec -> Spec
forall a. (Int -> Int) -> SpecWith a -> SpecWith a
modifyMaxSuccess (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
50) (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$
        String
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"negative (period)" ((PinnedSizedBytes (SeedSizeKES v) -> Message -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
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
    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"serialisation of all KES evolutions" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"VerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$ forall v.
(ContextKES v ~ (), KESAlgorithm v) =>
PinnedSizedBytes (SeedSizeKES v) -> Property
prop_serialise_VerKeyKES @v
      String
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Sig" ((PinnedSizedBytes (SeedSizeKES v) -> Message -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
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.
    --
    --  describe "forgetting" $ do
    --    prop "key overwritten after forget" $ prop_key_overwritten_after_forget (Proxy @v)

    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"unsound pure" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"genKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"updateKES" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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
      String -> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"deriveVerKey" ((PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Property) -> Spec
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
      String
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"sign" ((PinnedSizedBytes (SeedSizeKES v) -> Message -> Property) -> Spec)
-> (PinnedSizedBytes (SeedSizeKES v) -> Message -> Property)
-> Spec
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 -> Expectation) -> (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 -> Expectation
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 -> Expectation
forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk
    Expectation
-> (SignKeyKES v -> Expectation)
-> Maybe (SignKeyKES v)
-> Expectation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Expectation
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) SignKeyKES v -> Expectation
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 =
  Expectation -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (Expectation -> Property)
-> (Expectation -> Expectation) -> Expectation -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lock -> Expectation -> Expectation
forall a. Lock -> IO a -> IO a
withLock Lock
lock (Expectation -> Property) -> Expectation -> Property
forall a b. (a -> b) -> a -> b
$ do
    IO [()] -> Expectation
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO [()] -> Expectation) -> IO [()] -> Expectation
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 -> Expectation) -> IO [()])
-> (SignKeyKES v -> Expectation) -> IO [()]
forall a b. (a -> b) -> a -> b
$ Expectation -> SignKeyKES v -> Expectation
forall a b. a -> b -> a
const (() -> Expectation
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 (Expectation -> SignKeyKES v -> Expectation
forall a b. a -> b -> a
const (Expectation -> SignKeyKES v -> Expectation)
-> (() -> Expectation) -> () -> SignKeyKES v -> Expectation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Expectation
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> SignKeyKES v -> Expectation)
-> () -> SignKeyKES v -> Expectation
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
==>
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Int -> String
forall a. Show a => a -> String
show Int
totalPeriods) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
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 -> Expectation
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
$
      String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ([VerKeyKES v] -> String
forall a. Show a => a -> String
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 -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> 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) String
"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 -> Expectation
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 String ()
verResult = ContextKES v
-> VerKeyKES v -> Word -> Message -> SigKES v -> Either String ()
forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either String ()
forall a.
(Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either String ()
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
$
                  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"period " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> String
forall a. Show a => a -> String
show Word
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"/" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
totalPeriods) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                    Either String ()
verResult Either String () -> Either String () -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== () -> Either String ()
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 -> Expectation
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 String ()
verResult = ContextKES v
-> VerKeyKES v -> Word -> Message -> SigKES v -> Either String ()
forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either String ()
forall a.
(Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either String ()
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
$
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"period " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> String
forall a. Show a => a -> String
show Word
t) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Either String ()
verResult Either String () -> Either String () -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=/= () -> Either String ()
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 -> Expectation
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 String ()
verResult = ContextKES v
-> VerKeyKES v -> Word -> Message -> SigKES v -> Either String ()
forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either String ()
forall a.
(Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either String ()
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
$
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"period " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> String
forall a. Show a => a -> String
show Word
t) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Either String ()
verResult Either String () -> Either String () -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=/= () -> Either String ()
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 -> Expectation
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
          [ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"periods " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Word, Word) -> String
forall a. Show a => a -> String
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 String ()
forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either String ()
forall a.
(Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either String ()
verifyKES () VerKeyKES v
vk Word
t' Message
x SigKES v
sig Either String () -> Either String () -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=/= () -> Either String ()
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
$
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"period " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> String
forall a. Show a => a -> String
show Word
t) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"vkey " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VerKeyKES v -> String
forall a. Show a => a -> String
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
$
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"period " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word -> String
forall a. Show a => a -> String
show Word
t) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"vkey " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SignKeyKES v -> String
forall a. Show a => a -> String
show SignKeyKES v
sk) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"sig " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SigKES v -> String
forall a. Show a => a -> String
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 -> Expectation
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 -> Expectation
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 -> Expectation
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
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (ByteString -> String
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 -> Expectation)
-> (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 -> Expectation
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) -> Expectation)
-> (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)
      (Expectation
-> (SignKeyKES v -> Expectation)
-> Maybe (SignKeyKES v)
-> Expectation
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> Expectation
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) SignKeyKES v -> Expectation
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
$ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 -> Expectation)
-> (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 -> Expectation
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 (String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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