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

{- HLINT ignore "Use head" -}

module Test.Crypto.KES (
  tests,
)
where

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance
  ( EqST (SignKeyKES d)
  , Eq (VerKeyKES d)
  , KnownNat (SeedSizeKES d)
  ) =>
  EqST (SignKeyKES (SumKES h d))
  where
  equalsM :: forall (m :: * -> *).
MonadST m =>
SignKeyKES (SumKES h d) -> SignKeyKES (SumKES h d) -> m Bool
equalsM (SignKeySumKES SignKeyKES d
s MLockedSeed (SeedSizeKES d)
r VerKeyKES d
v1 VerKeyKES d
v2) (SignKeySumKES SignKeyKES d
s' MLockedSeed (SeedSizeKES d)
r' VerKeyKES d
v1' VerKeyKES d
v2') =
    (SignKeyKES d
s, MLockedSeed (SeedSizeKES d)
r, forall a. a -> PureEqST a
PureEqST VerKeyKES d
v1, forall a. a -> PureEqST a
PureEqST VerKeyKES d
v2) forall (m :: * -> *) a. (MonadST m, EqST a) => a -> a -> m Bool
==! (SignKeyKES d
s', MLockedSeed (SeedSizeKES d)
r', forall a. a -> PureEqST a
PureEqST VerKeyKES d
v1', 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, forall a. a -> PureEqST a
PureEqST VerKeyKES d
v1, forall a. a -> PureEqST a
PureEqST VerKeyKES d
v2) forall (m :: * -> *) a. (MonadST m, EqST a) => a -> a -> m Bool
==! (SignKeyKES d
s', MLockedSeed (SeedSizeKES d)
r', forall a. a -> PureEqST a
PureEqST VerKeyKES d
v1', 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Int -> Gen [a]
vector (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
seedSizeKES (forall {k} (t :: k). Proxy t
Proxy @k))
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes ByteString
bytes
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- 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 forall a. Eq a => a -> a -> Bool
== Word
current =
              forall a. a -> Maybe a
Just UnsoundPureSignKeyKES k
sk
          | Word
target forall a. Ord a => a -> a -> Bool
> Word
current =
              Word
-> Word
-> UnsoundPureSignKeyKES k
-> Maybe (UnsoundPureSignKeyKES k)
updateTo Word
target (forall a. Enum a => a -> a
succ Word
current) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall v.
UnsoundPureKESAlgorithm v =>
ContextKES v
-> UnsoundPureSignKeyKES v
-> Word
-> Maybe (UnsoundPureSignKeyKES v)
unsoundPureUpdateKES ContextKES k
ctx UnsoundPureSignKeyKES k
sk Word
current
          | Bool
otherwise =
              forall a. Maybe a
Nothing
    Word
period <- forall a. (Bounded a, Integral a) => (a, a) -> Gen a
chooseBoundedIntegral (Word
0, forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
totalPeriodsKES (forall {k} (t :: k). Proxy t
Proxy @k) forall a. Num a => a -> a -> a
- Word
1)
    UnsoundPureSignKeyKES k
sk0 <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return UnsoundPureSignKeyKES k
sk
      Maybe (UnsoundPureSignKeyKES k)
Nothing -> forall a. HasCallStack => TestName -> a
error TestName
"Attempted to generate SignKeyKES evolved beyond max period"

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

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

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

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

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

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

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

      TestName -> [TestTree] -> TestTree
testGroup
        TestName
"unsound pure"
        [ forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"genKey" forall a b. (a -> b) -> a -> b
$ forall v.
(UnsoundPureKESAlgorithm v, EqST (SignKeyKES v)) =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureGenKey @v forall {k} (t :: k). Proxy t
Proxy
        , forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"updateKES" 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 forall {k} (t :: k). Proxy t
Proxy
        , forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"deriveVerKey" forall a b. (a -> b) -> a -> b
$ forall v.
UnsoundPureKESAlgorithm v =>
Proxy v -> PinnedSizedBytes (SeedSizeKES v) -> Property
prop_unsoundPureDeriveVerKey @v forall {k} (t :: k). Proxy t
Proxy
        , forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"sign" 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 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 =
  forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
    (forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES)
    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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). PinnedSizedBytes n -> ByteString
psbToByteString forall a b. (a -> b) -> a -> b
$ PinnedSizedBytes (SeedSizeKES v)
psb
   in 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 =
  forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ forall a. Lock -> IO a -> IO a
withLock Lock
lock forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const 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 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Applicative m => m a -> m Property
doesNotThrow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v (m :: * -> *).
(KESAlgorithm v, 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 =
  forall prop. Testable prop => IO prop -> Property
ioProperty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lock -> IO a -> IO a
withLock Lock
lock forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB 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' <- forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
ContextKES v -> SignKeyKES v -> Word -> m (Maybe (SignKeyKES v))
updateKES () SignKeyKES v
sk Word
0
    forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES Maybe (SignKeyKES v)
msk'
    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 =
  forall prop. Testable prop => IO prop -> Property
ioProperty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lock -> IO a -> IO a
withLock Lock
lock forall a b. (a -> b) -> a -> b
$ do
    forall (f :: * -> *) a. Functor f => f a -> f ()
void 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 forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const (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 =
  forall prop. Testable prop => IO prop -> Property
ioProperty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lock -> IO a -> IO a
withLock Lock
lock 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 (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ())
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
      Int
totalPeriods forall a. Ord a => a -> a -> Bool
> Int
0 forall prop. Testable prop => Bool -> prop -> Property
==>
        forall prop. Testable prop => TestName -> prop -> Property
counterexample (forall a. Show a => a -> TestName
show Int
totalPeriods) forall a b. (a -> b) -> a -> b
$
          forall prop. Testable prop => TestName -> prop -> Property
counterexample (forall a. Show a => a -> TestName
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length [()]
sks) forall a b. (a -> b) -> a -> b
$
            forall (t :: * -> *) a. Foldable t => t a -> Int
length [()]
sks forall a. (Eq a, Show a) => a -> a -> Property
=== Int
totalPeriods
  where
    totalPeriods :: Int
    totalPeriods :: Int
totalPeriods = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
totalPeriodsKES (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 =
  forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ do
    VerKeyKES v
vk_0 <- do
      SignKeyKES v
sk_0 <- forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB 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 <- forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0
      forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0
      forall (m :: * -> *) a. Monad m => a -> m a
return VerKeyKES v
vk_0

    [VerKeyKES v]
vks <- forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES_ PinnedSizedBytes (SeedSizeKES v)
seedPSB forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
      forall prop. Testable prop => TestName -> prop -> Property
counterexample (forall a. Show a => a -> TestName
show [VerKeyKES v]
vks) forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => [prop] -> Property
conjoin (forall a b. (a -> b) -> [a] -> [b]
map (VerKeyKES v
vk_0 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] <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
totalPeriods forall a. Arbitrary a => Gen a
arbitrary
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => prop -> Property
checkCoverage forall a b. (a -> b) -> a -> b
$
      forall prop.
Testable prop =>
Double -> Bool -> TestName -> prop -> Property
cover Double
1 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Message]
xs forall a. Ord a => a -> a -> Bool
>= Int
totalPeriods) TestName
"Message count covers total periods" forall a b. (a -> b) -> a -> b
$
        Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Message]
xs) forall prop. Testable prop => Bool -> prop -> Property
==>
          forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$ do
              SignKeyKES v
sk_0 <- forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB 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 <- forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0
              forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0
              forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
                let x :: Message
x = forall a. [a] -> [a]
cycle [Message]
xs forall a. [a] -> Int -> a
!! forall a b. (Integral a, Num b) => a -> b
fromIntegral Word
t
                SigKES v
sig <- forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
                let verResult :: Either TestName ()
verResult = forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
verifyKES () VerKeyKES v
vk Word
t Message
x SigKES v
sig
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
                  forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Word
t forall a. [a] -> [a] -> [a]
++ TestName
"/" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Int
totalPeriods) forall a b. (a -> b) -> a -> b
$
                    Either TestName ()
verResult forall a. (Eq a, Show a) => a -> a -> Property
=== forall a b. b -> Either a b
Right ()
  where
    totalPeriods :: Int
    totalPeriods :: Int
totalPeriods = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
totalPeriodsKES (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 forall a. Eq a => a -> a -> Bool
/= PinnedSizedBytes (SeedSizeKES v)
seedPSB' forall prop. Testable prop => Bool -> prop -> Property
==> forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$ do
    SignKeyKES v
sk_0' <- forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB' 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' <- forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0'
    forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0'
    forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      SigKES v
sig <- forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
      let verResult :: Either TestName ()
verResult = forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
verifyKES () VerKeyKES v
vk' Word
t Message
x SigKES v
sig
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Word
t) forall a b. (a -> b) -> a -> b
$
          Either TestName ()
verResult forall a. (Eq a, Show a) => a -> a -> Property
=/= 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 forall a. Eq a => a -> a -> Bool
/= Message
x' forall prop. Testable prop => Bool -> prop -> Property
==> forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$ do
    SignKeyKES v
sk_0 <- forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB 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 <- forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0
    forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0
    forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      SigKES v
sig <- forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
      let verResult :: Either TestName ()
verResult = forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
verifyKES () VerKeyKES v
vk Word
t Message
x' SigKES v
sig
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Word
t) forall a b. (a -> b) -> a -> b
$
          Either TestName ()
verResult forall a. (Eq a, Show a) => a -> a -> Property
=/= 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 =
  forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$ do
    SignKeyKES v
sk_0 <- forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB 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 <- forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk_0
    forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk_0
    forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      SigKES v
sig <- forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => [prop] -> Property
conjoin
          [ forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"periods " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (Word
t, Word
t')) forall a b. (a -> b) -> a -> b
$
              forall v a.
(KESAlgorithm v, Signable v a, HasCallStack) =>
ContextKES v
-> VerKeyKES v -> Word -> a -> SigKES v -> Either TestName ()
verifyKES () VerKeyKES v
vk Word
t' Message
x SigKES v
sig forall a. (Eq a, Show a) => a -> a -> Property
=/= forall a b. b -> Either a b
Right ()
          | Word
t' <- [Word
0 .. Word
totalPeriods forall a. Num a => a -> a -> a
- Word
1]
          , Word
t forall a. Eq a => a -> a -> Bool
/= Word
t'
          ]
  where
    totalPeriods :: Word
    totalPeriods :: Word
totalPeriods = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
totalPeriodsKES (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 =
  forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall prop. Testable prop => [prop] -> Property
conjoin 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 forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      VerKeyKES v
vk <- forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES SignKeyKES v
sk
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Word
t) forall a b. (a -> b) -> a -> b
$
          forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"vkey " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show VerKeyKES v
vk) forall a b. (a -> b) -> a -> b
$
            forall a.
(Eq a, Show a) =>
(a -> ByteString) -> (ByteString -> Maybe a) -> a -> Property
prop_raw_serialise
              forall v. KESAlgorithm v => VerKeyKES v -> ByteString
rawSerialiseVerKeyKES
              forall v. KESAlgorithm v => ByteString -> Maybe (VerKeyKES v)
rawDeserialiseVerKeyKES
              VerKeyKES v
vk
              forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. forall a.
(Eq a, Show a) =>
(a -> Encoding) -> (forall s. Decoder s a) -> a -> Property
prop_cbor_with
                forall v. KESAlgorithm v => VerKeyKES v -> Encoding
encodeVerKeyKES
                forall v s. KESAlgorithm v => Decoder s (VerKeyKES v)
decodeVerKeyKES
                VerKeyKES v
vk
              forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. forall a. (a -> ByteString) -> Word -> a -> Property
prop_size_serialise
                forall v. KESAlgorithm v => VerKeyKES v -> ByteString
rawSerialiseVerKeyKES
                (forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeVerKeyKES (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 =
  forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall prop. Testable prop => [prop] -> Property
conjoin 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 forall a b. (a -> b) -> a -> b
$ \Word
t SignKeyKES v
sk -> do
      SigKES v
sig <- forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
t Message
x SignKeyKES v
sk
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"period " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Word
t) forall a b. (a -> b) -> a -> b
$
          forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"vkey " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show SignKeyKES v
sk) forall a b. (a -> b) -> a -> b
$
            forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"sig " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show SigKES v
sig) forall a b. (a -> b) -> a -> b
$
              forall a.
(Eq a, Show a) =>
(a -> ByteString) -> (ByteString -> Maybe a) -> a -> Property
prop_raw_serialise
                forall v. KESAlgorithm v => SigKES v -> ByteString
rawSerialiseSigKES
                forall v. KESAlgorithm v => ByteString -> Maybe (SigKES v)
rawDeserialiseSigKES
                SigKES v
sig
                forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. forall a.
(Eq a, Show a) =>
(a -> Encoding) -> (forall s. Decoder s a) -> a -> Property
prop_cbor_with
                  forall v. KESAlgorithm v => SigKES v -> Encoding
encodeSigKES
                  forall v s. KESAlgorithm v => Decoder s (SigKES v)
decodeSigKES
                  SigKES v
sig
                forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. forall a. (a -> ByteString) -> Word -> a -> Property
prop_size_serialise
                  forall v. KESAlgorithm v => SigKES v -> ByteString
rawSerialiseSigKES
                  (forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSigKES (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
  forall v a.
(KESAlgorithm v, ContextKES v ~ ()) =>
PinnedSizedBytes (SeedSizeKES v)
-> (Word -> SignKeyKES v -> IO a) -> IO [a]
withAllUpdatesKES PinnedSizedBytes (SeedSizeKES v)
seedPSB (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 = forall (m :: * -> *) (n :: Nat) a.
(MonadST m, MonadThrow m, KnownNat n) =>
PinnedSizedBytes n -> (MLockedSeed n -> m a) -> m a
withMLockedSeedFromPSB PinnedSizedBytes (SeedSizeKES v)
seedPSB forall a b. (a -> b) -> a -> b
$ \MLockedSeed (SeedSizeKES v)
seed -> do
  SignKeyKES v
sk_0 <- 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' <- 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
          forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk
          forall (m :: * -> *) a. Monad m => a -> m a
return [a
x]
        Just SignKeyKES v
sk' -> do
          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 forall a. Num a => a -> a -> a
+ Word
1)
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a
x 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 =
  forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
    (forall (n :: Nat). MLockedSizedBytes n -> MLockedSeed n
MLockedSeed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (n :: Nat) (m :: * -> *).
(KnownNat n, MonadST m) =>
ByteString -> m (MLockedSizedBytes n)
mlsbFromByteString (Int -> Word8 -> ByteString
BS.replicate (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall {k} (t :: k). Proxy t
Proxy @n)) Word8
0))
    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 =
  forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
    (forall (m :: * -> *) (n :: Nat) a.
(MonadThrow m, MonadST m, KnownNat n) =>
(MLockedSeed n -> m a) -> m a
withNullSeed forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
MLockedSeed (SeedSizeKES v) -> m (SignKeyKES v)
genKeyKES)
    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 =
  forall prop. Testable prop => IO prop -> Property
ioProperty 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 forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
    let Int
size :: Int = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall v (proxy :: * -> *). KESAlgorithm v => proxy v -> Word
sizeSignKeyKES Proxy v
kesAlgorithm
    ByteString
serialized <- forall (m :: * -> *) a.
(DirectSerialise a, MonadST m, MonadThrow m) =>
Int -> a -> m ByteString
directSerialiseToBS Int
size SignKeyKES v
sk
    forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES SignKeyKES v
sk
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => TestName -> prop -> Property
counterexample (ByteString -> TestName
hexBS ByteString
serialized) 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 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 (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 = forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ do
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes forall a b. (a -> b) -> a -> b
$ 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
  forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
    forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
      (forall v (m :: * -> *).
(UnsoundPureKESAlgorithm v, MonadST m, MonadThrow m) =>
UnsoundPureSignKeyKES v -> m (SignKeyKES v)
unsoundPureSignKeyKESToSoundSignKeyKES UnsoundPureSignKeyKES v
skPure)
      forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES
      (forall a (m :: * -> *). (EqST a, MonadST m) => a -> a -> 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 = forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ do
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes forall a b. (a -> b) -> a -> b
$ 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 <- forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m (VerKeyKES v)
deriveVerKeyKES
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ VerKeyKES v
vkPure 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 = forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ do
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes forall a b. (a -> b) -> a -> b
$ 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 = forall v.
UnsoundPureKESAlgorithm v =>
ContextKES v
-> UnsoundPureSignKeyKES v
-> Word
-> Maybe (UnsoundPureSignKeyKES v)
unsoundPureUpdateKES () UnsoundPureSignKeyKES v
skPure Word
0
  forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk -> do
    forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
      (forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
ContextKES v -> SignKeyKES v -> Word -> m (Maybe (SignKeyKES v))
updateKES () SignKeyKES v
sk Word
0)
      (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES)
      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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True
              Just SignKeyKES v
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"pure does not update, but should" forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
False
          Just UnsoundPureSignKeyKES v
skPure' ->
            forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
              (forall v (m :: * -> *).
(UnsoundPureKESAlgorithm v, MonadST m, MonadThrow m) =>
UnsoundPureSignKeyKES v -> m (SignKeyKES v)
unsoundPureSignKeyKESToSoundSignKeyKES UnsoundPureSignKeyKES v
skPure')
              forall v (m :: * -> *).
(KESAlgorithm v, MonadST m, MonadThrow m) =>
SignKeyKES v -> m ()
forgetSignKeyKES
              forall a b. (a -> b) -> a -> b
$ \SignKeyKES v
sk'' ->
                case Maybe (SignKeyKES v)
sk'Maybe of
                  Maybe (SignKeyKES v)
Nothing ->
                    forall (m :: * -> *) a. Monad m => a -> m a
return (forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"pure updates, but shouldn't" forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
False)
                  Just SignKeyKES v
sk' ->
                    forall prop. Testable prop => prop -> Property
property forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (EqST a, MonadST m) => a -> a -> 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 = forall prop. Testable prop => IO prop -> Property
ioProperty forall a b. (a -> b) -> a -> b
$ do
  let seed :: Seed
seed = ByteString -> Seed
mkSeedFromBytes forall a b. (a -> b) -> a -> b
$ 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 = forall v a.
(UnsoundPureKESAlgorithm v, Signable v a) =>
ContextKES v -> Word -> a -> UnsoundPureSignKeyKES v -> SigKES v
unsoundPureSignKES () Word
0 Message
msg UnsoundPureSignKeyKES v
skPure
  SigKES v
sig <- forall v b.
KESAlgorithm v =>
PinnedSizedBytes (SeedSizeKES v) -> (SignKeyKES v -> IO b) -> IO b
withSK PinnedSizedBytes (SeedSizeKES v)
seedPSB forall a b. (a -> b) -> a -> b
$ forall v a (m :: * -> *).
(KESAlgorithm v, Signable v a, MonadST m, MonadThrow m) =>
ContextKES v -> Word -> a -> SignKeyKES v -> m (SigKES v)
signKES () Word
0 Message
msg
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SigKES v
sigPure forall a. (Eq a, Show a) => a -> a -> Property
=== SigKES v
sig