mldsa-0.1.0.0: tests/Tests.hs
-- |
-- Module : Main
-- License : BSD-3-Clause
-- Copyright : (c) 2026 Olivier Chéron
--
-- The ML-DSA test suite. Can be instanciated twice, with and without the
-- @ML_DSA_TESTING@ macro to run property testing with assertions enabled in
-- the internal modules.
--
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
module Main (main) where
import Data.ByteArray (Bytes)
import qualified Data.ByteArray as B
import Crypto.Hash (hashWith)
import Crypto.Hash.Algorithms
import Control.Monad
import Data.List (isPrefixOf)
import Data.Maybe (fromJust)
import Data.Proxy
import GHC.IO.Exception (IOErrorType(..))
import System.Directory (doesFileExist)
import System.FileLock (FileLock, SharedExclusive(..), unlockFile, withFileLock)
import System.IO.Error (catchIOError, mkIOError)
import System.Process (readProcess)
#ifdef ML_DSA_TESTING
import Data.Bits
import Data.Word
import GHC.TypeNats
import Foreign.Ptr (plusPtr)
import Auxiliary
import BlockN (BlockN)
import Builder (Builder)
import Marking (Leak(..), SecurityMarking(..))
import Math
import Matrix
import Vector
import qualified BlockN
import qualified Builder
#endif
import Crypto.PubKey.ML_DSA as Lib
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck
import qualified KeyGen
import qualified SigExt
import qualified SigGen
import qualified SigVer
import qualified Vectors
arbitraryBytes :: Int -> Gen Bytes
arbitraryBytes n = B.pack <$> vectorOf n arbitrary
#ifdef ML_DSA_TESTING
truncateRq :: Word32 -> Rq Sec -> Rq Sec
truncateRq m = fromJust . fromCoeffs . map f . toCoeffs
where f = toZq . (`mod` m) . fromZq
truncateRq' :: Word32 -> Rq Sec -> Rq Sec
truncateRq' m = fromJust . fromCoeffs . map f . toCoeffs
where f = toZq . (\x -> x `mod` (2 * m - 1) + 8380418 - m) . fromZq
newtype FE = FE { unFE :: Zq } deriving Show
instance Arbitrary FE where
#if (MIN_VERSION_tasty_quickcheck(0,10,2))
arbitrary = FE . toZq <$> chooseBoundedIntegral (0, 8380416)
#else
arbitrary = FE . toZq <$> choose (0, 8380416)
#endif
newtype ME = ME { unME :: Mq } deriving Show
instance Arbitrary ME where
arbitrary = ME . toMontgomery . unFE <$> arbitrary
newtype Poly = Poly (Rq Sec) deriving Show
instance Arbitrary Poly where
arbitrary = do
coeffs <- map unFE <$> vectorOf 256 arbitrary
let a = fromJust (fromCoeffs coeffs)
return (Poly a)
newtype PolyNTT = PolyNTT (Tq Sec) deriving Show
instance Arbitrary PolyNTT where
arbitrary = (\(Poly f) -> PolyNTT (ntt f)) <$> arbitrary
arbitraryHints :: Gen Hints
arbitraryHints = fromJust . fromBools <$> vectorOf 256 h
where h = elements (True : replicate 9 False) -- probability 1/10
arbitraryHintsVector :: KnownNat k => proxy k -> Gen (Vector k Hints)
arbitraryHintsVector _ = Vector.replicateM arbitraryHints
countHints :: Vector n Hints -> Word
countHints = Vector.foldl' countFrom 0
newtype D = D Int deriving Show
instance Arbitrary D where
arbitrary = sized $ \n -> D <$> choose (0, min n 22)
data Dim = forall (n :: Nat). KnownNat n => Dim (Proxy n)
instance Show Dim where
show (Dim n) = show n
instance Arbitrary Dim where
arbitrary = sized $ \n -> toDim <$> choose (1, min (1 + n) 9)
toDim :: Int -> Dim
toDim n = case someNatVal (fromIntegral n) of SomeNat p -> Dim p
type VElem = Mq -- test with any ring but Tq would also work here
arbitraryVector :: KnownNat n => proxy n -> Gen (Vector n VElem)
arbitraryVector _ = Vector.replicateM (unME <$> arbitrary)
arbitraryMatrix :: (KnownNat m, KnownNat n) => proxy n -> proxy m -> Gen (Vector n (Vector m VElem))
arbitraryMatrix _ m = Vector.replicateM (arbitraryVector m)
simpleBitPackBytes :: Int -> BlockN Sec 256 Word32 -> Bytes
simpleBitPackBytes d = runBytes . simpleBitPack d
runPubBytes :: Builder Pub -> Bytes
runPubBytes = Builder.run
runPubUnaligned :: Builder Pub -> UnalignedBytes
runPubUnaligned = Builder.runRelaxed
runBytes :: Builder Sec -> Bytes
runBytes = runPubBytes . leak
runUnaligned :: Builder Sec -> UnalignedBytes
runUnaligned = runPubUnaligned . leak
newtype UnalignedBytes = UnalignedBytes (B.View Bytes)
deriving (Eq,Ord,Show)
instance Semigroup UnalignedBytes where
UnalignedBytes a <> UnalignedBytes b =
B.allocAndFreeze (na + nb) $ \p -> do
B.copyByteArrayToPtr a p
B.copyByteArrayToPtr b (p `plusPtr` na)
where
na = B.length a
nb = B.length b
instance Monoid UnalignedBytes where
mempty = B.convert (B.empty :: Bytes)
instance B.ByteArrayAccess UnalignedBytes where
length (UnalignedBytes v) = B.length v
withByteArray (UnalignedBytes v) = B.withByteArray v
instance B.ByteArray UnalignedBytes where
allocRet n f = do
let build ba = UnalignedBytes (B.dropView ba offset)
(a, ba) <- B.allocRet (n + offset) $ \p -> f (p `plusPtr` offset)
return (a, build ba)
where offset = 1
#endif
data P = forall a. (ParamSet a, Show a) => P (Proxy a)
instance Show P where
show (P p) = show p
instance Arbitrary P where
arbitrary = elements
[ P (Proxy :: Proxy ML_DSA_44)
, P (Proxy :: Proxy ML_DSA_65)
, P (Proxy :: Proxy ML_DSA_87)
]
toP :: String -> P
toP "ML-DSA-44" = P (Proxy :: Proxy ML_DSA_44)
toP "ML-DSA-65" = P (Proxy :: Proxy ML_DSA_65)
toP "ML-DSA-87" = P (Proxy :: Proxy ML_DSA_87)
toP paramSet = error ("unknown parameter set " ++ paramSet)
data PH = forall alg. (PreHashAlgorithm alg, Show alg) => PH (Proxy alg)
instance Show PH where
show (PH ph) = show ph
instance Arbitrary PH where
arbitrary = elements
[ PH (Proxy :: Proxy SHA224)
, PH (Proxy :: Proxy SHA256)
, PH (Proxy :: Proxy SHA384)
, PH (Proxy :: Proxy SHA512)
, PH (Proxy :: Proxy SHA512t_224)
, PH (Proxy :: Proxy SHA512t_256)
, PH (Proxy :: Proxy SHA3_224)
, PH (Proxy :: Proxy SHA3_256)
, PH (Proxy :: Proxy SHA3_384)
, PH (Proxy :: Proxy SHA3_512)
, PH (Proxy :: Proxy (SHAKE128 256))
, PH (Proxy :: Proxy (SHAKE256 512))
]
toPH :: String -> PH
toPH "SHA2-224" = PH (Proxy :: Proxy SHA224)
toPH "SHA2-256" = PH (Proxy :: Proxy SHA256)
toPH "SHA2-384" = PH (Proxy :: Proxy SHA384)
toPH "SHA2-512" = PH (Proxy :: Proxy SHA512)
toPH "SHA2-512/224" = PH (Proxy :: Proxy SHA512t_224)
toPH "SHA2-512/256" = PH (Proxy :: Proxy SHA512t_256)
toPH "SHA3-224" = PH (Proxy :: Proxy SHA3_224)
toPH "SHA3-256" = PH (Proxy :: Proxy SHA3_256)
toPH "SHA3-384" = PH (Proxy :: Proxy SHA3_384)
toPH "SHA3-512" = PH (Proxy :: Proxy SHA3_512)
toPH "SHAKE-128" = PH (Proxy :: Proxy (SHAKE128 256))
toPH "SHAKE-256" = PH (Proxy :: Proxy (SHAKE256 512))
toPH hashAlg = error ("unknown hash algorithm " ++ hashAlg)
preHash :: Proxy alg -> alg
preHash _ = undefined
withPreHash :: String -> (forall alg. PreHashAlgorithm alg => alg -> r) -> r
withPreHash s f = case toPH s of
PH ph -> f (preHash ph)
newtype Ctx = Ctx { unCtx :: Context } deriving Show
instance Arbitrary Ctx where
arbitrary = sized $ \n -> do
len <- choose (0, min n 255)
Ctx . fromJust . Lib.context <$> arbitraryBytes len
newtype Msg = Msg { unMsg :: Bytes } deriving Show
instance Arbitrary Msg where
arbitrary = Msg . B.pack <$> arbitrary
newtype ExternalMu = ExternalMu { unExternalMu :: Mu } deriving Show
instance Arbitrary ExternalMu where
arbitrary = ExternalMu . fromJust . Lib.externalMu <$> arbitraryBytes 64
withVectors :: (IO () -> TestTree) -> TestTree
withVectors = withResource alloc free
where
scriptPath = "tests/get-vectors.sh"
free _ = return ()
whenNeeded action = do
keyGenExists <- doesFileExist "tests/keyGen.json.gz"
sigGenExists <- doesFileExist "tests/sigGen.json.gz"
sigVerExists <- doesFileExist "tests/sigVer.json.gz"
unless (keyGenExists && sigGenExists && sigVerExists) action
alloc = withTestLock Shared $ \lock -> whenNeeded $ do
unlockFile lock -- sanity before lock upgrade
withTestLock Exclusive $ \_ -> whenNeeded $ catchIOError
(void $ readProcess "/bin/sh" [scriptPath] "")
(\e ->
let msg = "Could not download test vectors, you will need to run the script `" ++
scriptPath ++ "' manually. Script failure was: " ++ show e
in ioError (mkIOError OtherError msg Nothing Nothing)
)
withTestLock :: SharedExclusive -> (FileLock -> IO a) -> IO a
withTestLock mode what = do
-- locking a hidden file in the directory prevents a race condition between
-- two instances of the test suite trying both to download the test vectors
-- (otherwise one instance may try to run with files not fully downloaded
-- yet by the other instance)
let path = "tests/.lock"
exists <- doesFileExist path
unless exists $ writeFile path "DO NOT DELETE"
withFileLock path mode what
keyGenVectors :: (String -> IO ()) -> Assertion
keyGenVectors step = do
step "Reading test vectors ..."
file <- Vectors.readJson "tests/keyGen.json.gz"
forM_ (Vectors.testGroups file) $ \group -> do
let paramSet = KeyGen.parameterSet group
step paramSet
case toP paramSet of
P p -> forM_ (KeyGen.tests group) $ \t -> do
let tcId = KeyGen.tcId t
pks = Lib.encode pk
sks = Lib.encode sk
(pk, sk) = fromJust $ Lib.generateWith p (KeyGen.seed t)
assertEqual ("pk mismatch for tcId=" ++ show tcId) (KeyGen.pk t) pks
assertEqual ("sk mismatch for tcId=" ++ show tcId) (KeyGen.sk t) sks
sigGenVectors :: (String -> IO ()) -> Assertion
sigGenVectors step = do
step "Reading test vectors ..."
file <- Vectors.readJson "tests/sigGen.json.gz"
forM_ (Vectors.testGroups file) $ \group -> do
let paramSet = SigGen.parameterSet group
step (paramSet ++ " (" ++ mode group ++ ")")
case toP paramSet of
P p -> case SigGen.payload group of
SigGen.ModePure tests ->
forM_ tests (testExt doSignPure p)
SigGen.ModePreHash tests ->
forM_ tests (testExt doSignPreHash p)
SigGen.ModeExternalMu tests ->
forM_ tests (testExt doSignExternalMu p)
SigGen.ModeInternal tests ->
forM_ tests (testExt doSignInternal p)
where
mode group
| SigGen.signatureInterface group == "external" = SigGen.preHash group
| SigGen.externalMu group = "external µ"
| otherwise = SigGen.signatureInterface group
testExt signExtWith p test =
assertEqual ("sig mismatch for tcId=" ++ show tcId) sig' sig
where
tcId = SigGen.tcId test
ext = SigGen.tcExt test
sk = fromJust $ Lib.decode p (SigGen.skEnc test)
sig' = fromJust $ Lib.decode p (SigGen.sigEnc test)
rnd = maybe Lib.deterministic (fromJust . Lib.randomness) (SigGen.rndEnc test)
sig = signExtWith ext rnd sk
doSignPure ext rnd sk = Lib.signWith rnd sk m ctx
where
m = SigExt.msgEncP ext
ctx = fromJust $ Lib.context (SigExt.ctxEncP ext)
doSignPreHash ext rnd sk = withPreHash (SigExt.hashPH ext) $ \alg ->
let phm = hashWith alg m
in Lib.signDigestWith rnd sk phm ctx
where
m = SigExt.msgEncPH ext
ctx = fromJust $ Lib.context (SigExt.ctxEncPH ext)
doSignExternalMu ext rnd sk = Lib.signExternalMuWith rnd sk mu
where mu = fromJust $ Lib.externalMu (SigExt.muEncEM ext)
doSignInternal ext rnd sk = Lib.signInternalWith rnd sk m
where m = SigExt.msgEncIM ext
sigVerVectors :: (String -> IO ()) -> Assertion
sigVerVectors step = do
step "Reading test vectors ..."
file <- Vectors.readJson "tests/sigVer.json.gz"
forM_ (Vectors.testGroups file) $ \group -> do
let paramSet = SigVer.parameterSet group
step (paramSet ++ " (" ++ mode group ++ ")")
case toP paramSet of
P p -> case SigVer.payload group of
SigVer.ModePure tests ->
forM_ tests (testExt doVerifyPure p)
SigVer.ModePreHash tests ->
forM_ tests (testExt doVerifyPreHash p)
SigVer.ModeExternalMu tests ->
forM_ tests (testExt doVerifyExternalMu p)
SigVer.ModeInternal tests ->
forM_ tests (testExt doVerifyInternal p)
where
mode group
| SigVer.signatureInterface group == "external" = SigVer.preHash group
| SigVer.externalMu group = "external µ"
| otherwise = SigVer.signatureInterface group
testExt doVerify p test =
case Lib.decode p (SigVer.sigEnc test) of
Just sig -> do
assertBool ("opposite outcome for tcId=" ++ show tcId)
(SigVer.testPassed test == doVerify ext pk sig)
Nothing ->
assertBool ("could not decode signature for tcId=" ++ show tcId)
("modified signature - " `isPrefixOf` SigVer.reason test)
where
tcId = SigVer.tcId test
ext = SigVer.tcExt test
pk = fromJust $ Lib.decode p (SigVer.pkEnc test)
doVerifyPure ext pk sig = Lib.verify pk m sig ctx
where
m = SigExt.msgEncP ext
ctx = fromJust $ Lib.context (SigExt.ctxEncP ext)
doVerifyPreHash ext pk sig = withPreHash (SigExt.hashPH ext) $ \alg ->
let phm = hashWith alg m
in Lib.verifyDigest pk phm sig ctx
where
m = SigExt.msgEncPH ext
ctx = fromJust $ Lib.context (SigExt.ctxEncPH ext)
doVerifyExternalMu ext pk = Lib.verifyExternalMu pk mu
where mu = fromJust $ Lib.externalMu (SigExt.muEncEM ext)
doVerifyInternal ext pk = Lib.verifyInternal pk m
where m = SigExt.msgEncIM ext
main :: IO ()
main = defaultMain $ testGroup "mldsa"
[ withVectors $ \_ -> testGroup "vectors"
[ testCaseSteps "keyGen" keyGenVectors
, testCaseSteps "sigGen" sigGenVectors
, testCaseSteps "sigVer" sigVerVectors
]
, testGroup "properties"
[ testGroup "ML-DSA"
[ testProperty "sign/verify (pure)" $ \(P p) (Msg m) (Ctx ctx) -> ioProperty $ do
(pk, sk) <- Lib.generate p
sig <- Lib.sign sk m ctx
return (Lib.verify pk m sig ctx)
, testProperty "sign/verify (preHash)" $ \(P p) (PH ph) (Msg m) (Ctx ctx) -> ioProperty $ do
(pk, sk) <- Lib.generate p
let phm = hashWith (preHash ph) m
sig <- Lib.signDigest sk phm ctx
return (Lib.verifyDigest pk phm sig ctx)
, testProperty "sign/verify (external µ)" $ \(P p) (ExternalMu mu) -> ioProperty $ do
(pk, sk) <- Lib.generate p
sig <- Lib.signExternalMu sk mu
return (Lib.verifyExternalMu pk mu sig)
, testProperty "sign/verify (internal)" $ \(P p) (Msg m) -> ioProperty $ do
(pk, sk) <- Lib.generate p
sig <- Lib.signInternal sk m
return (Lib.verifyInternal pk m sig)
, testProperty "encode/decode keys" $ \(P p) -> ioProperty $ do
(pk, sk) <- Lib.generate p
return $ conjoin
[ Just pk === Lib.decode p (Lib.encode pk :: Bytes)
, Just sk === Lib.decode p (Lib.encode sk :: Bytes)
]
, testProperty "encode/decode signatures" $ \(P p) (Msg m) (Ctx ctx) -> ioProperty $ do
(_, sk) <- Lib.generate p
sig <- Lib.sign sk m ctx
return $ Just sig === Lib.decode p (Lib.encode sig :: Bytes)
, testProperty "toPublic" $ \(P p) -> ioProperty $ do
(ek, sk) <- Lib.generate p
return (ek === toPublic sk)
, testProperty "checkKeyPair" $ \(P p) -> ioProperty $
checkKeyPair <$> Lib.generate p
]
#ifdef ML_DSA_TESTING
, testGroup "bitRev8"
[ testCase "powers of two" $
let powers = [1, 2, 4, 8, 16, 32, 64, 128]
in reverse powers @=? map bitRev8 powers
, testProperty "or" $ \a b ->
bitRev8 (a .|. b) === bitRev8 a .|. bitRev8 b
, testProperty "not" $ \a ->
let comp = xor 255
in bitRev8 (comp a) === comp (bitRev8 a)
, testProperty "involutive" $ \a ->
a === bitRev8 (bitRev8 a)
, testProperty "preserves bit count" $ \a ->
popCount a === popCount (bitRev8 a)
]
, testGroup "compression"
[ testProperty "powerTwoRound" $ \(FE r) ->
let (r1, r0) = powerTwoRoundZq r
in fromZq r === (fromZq r1 + fromZq r0) `mod` 8380417 .&&.
(fromZq r1 `mod` 8192 == 0) .&&.
(fromZq r0 <= 4096 .||. fromZq r0 > 8380417 - 4096)
, testProperty "decompose" $ \(FE r) -> do
gamma2 <- elements [ 95232, 261888 ]
let (r1, r0) = decomposeZq gamma2 r
return $ r === toZq (2 * gamma2 * r1) .+ r0 .&&.
(fromZq r0 <= gamma2 .||. fromZq r0 > 8380417 - gamma2)
]
, testGroup "hints"
[ testProperty "fromBools . toBools == id " $ do
a <- arbitraryHints
return $ Just a === fromBools (toBools a)
, testProperty "toBools . fromBools == id " $ do
a <- vector 256
return $ Just a === (toBools <$> fromBools a)
, testProperty "useHint . makeHint" $ \(Poly z') (Poly r) -> do
gamma2 <- elements [ 95232, 261888 ]
let z = truncateRq' gamma2 z' -- to ensure |z| < gamma2
return $ useHint gamma2 (makeHint gamma2 z r) r === highBits gamma2 (r .+ z)
]
, testGroup "conversions"
[ testProperty "simpleBitPack . simpleBitUnpack == id" $ \(D d) -> do
b <- arbitraryBytes (32 * d)
return (b === runBytes (simpleBitPack d (simpleBitUnpack d b)))
, testProperty "simpleBitPack . simpleBitUnpack == id (unaligned)" $ \(D d) -> do
b <- arbitraryBytes (32 * d)
return (B.convert b === runUnaligned (simpleBitPack d (simpleBitUnpack d b)))
, testProperty "simpleBitPack 8" $ \x ->
B.replicate 256 x === simpleBitPackBytes 8 (BlockN.replicate $ fromIntegral x)
, testCase "simpleBitPack 1 (zeros)" $
B.replicate 32 0 @=? simpleBitPackBytes 1 (BlockN.replicate 0)
, testCase "simpleBitPack 1 (ones)" $
B.replicate 32 255 @=? simpleBitPackBytes 1 (BlockN.replicate 1)
, testProperty "simpleBitPack10 . simpleBitUnpack10 == id" $ do
b <- arbitraryBytes 320
return (b === runPubBytes (simpleBitPack10 (simpleBitUnpack10 b)))
, testProperty "simpleBitPack10 . simpleBitUnpack10 == id (unaligned)" $ do
b <- arbitraryBytes 320
return (B.convert b === runPubUnaligned (simpleBitPack10 (simpleBitUnpack10 b)))
, testProperty "bitPackSafe . bitUnpackSafe == id" $ \(D d) -> do
b <- arbitraryBytes (32 * d)
return (b === runBytes (bitPackSafe d (bitUnpackSafe d b)))
, testProperty "bitPackSafe . bitUnpackSafe == id (unaligned)" $ \(D d) -> do
b <- arbitraryBytes (32 * d)
return (B.convert b === runUnaligned (bitPackSafe d (bitUnpackSafe d b)))
, testProperty "bitUnpack . bitPack == id" $ \(FE t) (Poly w') ->
let w = truncateRq (fromZq t) w'
m = getNorm (norm w)
d = 33 - countLeadingZeros m
in Just w === bitUnpack m d (runBytes $ bitPack m d w)
, testProperty "bitUnpack . bitPack == id (unaligned)" $ \(FE t) (Poly w') ->
let w = truncateRq (fromZq t) w'
m = getNorm (norm w)
d = 33 - countLeadingZeros m
in Just w === bitUnpack m d (runUnaligned $ bitPack m d w)
, testProperty "hintBitUnpack . hintBitPack == id" $ \(Dim k) extra -> do
h <- arbitraryHintsVector k
let omega = fromIntegral (extra + countHints h)
return $ omega < 256 ==>
Just h === hintBitUnpack omega (runBytes $ hintBitPack omega h)
, testProperty "hintBitUnpack . hintBitPack == id (unaligned)" $ \(Dim k) extra -> do
h <- arbitraryHintsVector k
let omega = fromIntegral (extra + countHints h)
return $ omega < 256 ==>
Just h === hintBitUnpack omega (runUnaligned $ hintBitPack omega h)
]
, testGroup "Zq"
[ testProperty "toZq . fromZq == id " $ \(FE a) ->
a === toZq (fromZq a)
, testProperty "fromZq . toZq == id " $ \a ->
mod a 8380417 === fromZq (toZq a)
, testCase "field order" $ zero @=? toZq 8380417
, testProperty "addition with zero" $ \(FE a) ->
conjoin [ a === zero .+ a
, a === a .+ zero
]
, testProperty "addition associative" $ \(FE a) (FE b) (FE c) ->
a .+ (b .+ c) === (a .+ b) .+ c
, testProperty "addition commutative" $ \(FE a) (FE b) ->
a .+ b === b .+ a
, testProperty "substraction with zero" $ \(FE a) ->
a === a .- zero
, testProperty "substraction non-associative" $ \(FE a) (FE b) (FE c) ->
a .- (b .- c) === (a .- b) .+ c
, testProperty "substraction anti-commutative" $ \(FE a) (FE b) ->
a .- b === neg (b .- a)
, testProperty "negation" $ \(FE a) ->
neg a === zero .- a
, testProperty "double negation" $ \(FE a) ->
a === neg (neg a)
, testProperty "multiplication with zero" $ \(FE a) ->
conjoin [ zero === zero .* a
, zero === a .* zero
]
, testProperty "multiplication with one" $ \(FE a) ->
conjoin [ a === one .* a
, a === a .* one
]
, testProperty "multiplication associative" $ \(FE a) (FE b) (FE c) ->
a .* (b .* c) === (a .* b) .* c
, testProperty "multiplication commutative" $ \(FE a) (FE b) ->
a .* b === b .* a
, testProperty "multiplication distributive" $ \(FE a) (FE b) (FE c) ->
conjoin [ (a .* b) .+ (a .* c) === a .* (b .+ c)
, (b .* a) .+ (c .* a) === (b .+ c) .* a
]
]
, testGroup "Mq"
[ testProperty "toMontgomery . fromMontgomery == id " $ \(ME a) ->
a === toMontgomery (fromMontgomery a)
, testProperty "fromMontgomery . toMontgomery == id" $ \(FE a) ->
a === fromMontgomery (toMontgomery a)
, testProperty "addition with zero" $ \(ME a) ->
conjoin [ a === zero .+ a
, a === a .+ zero
]
, testProperty "addition associative" $ \(ME a) (ME b) (ME c) ->
a .+ (b .+ c) === (a .+ b) .+ c
, testProperty "addition commutative" $ \(ME a) (ME b) ->
a .+ b === b .+ a
, testProperty "substraction with zero" $ \(ME a) ->
a === a .- zero
, testProperty "substraction non-associative" $ \(ME a) (ME b) (ME c) ->
a .- (b .- c) === (a .- b) .+ c
, testProperty "substraction anti-commutative" $ \(ME a) (ME b) ->
a .- b === neg (b .- a)
, testProperty "negation" $ \(ME a) ->
neg a === zero .- a
, testProperty "double negation" $ \(ME a) ->
a === neg (neg a)
, testProperty "multiplication with zero" $ \(ME a) ->
conjoin [ zero === zero .* a
, zero === a .* zero
]
, testProperty "multiplication with one" $ \(ME a) ->
conjoin [ a === one .* a
, a === a .* one
]
, testProperty "multiplication associative" $ \(ME a) (ME b) (ME c) ->
a .* (b .* c) === (a .* b) .* c
, testProperty "multiplication commutative" $ \(ME a) (ME b) ->
a .* b === b .* a
, testProperty "multiplication distributive" $ \(ME a) (ME b) (ME c) ->
conjoin [ (a .* b) .+ (a .* c) === a .* (b .+ c)
, (b .* a) .+ (c .* a) === (b .+ c) .* a
]
]
, testGroup "Rq"
[ testProperty "fromCoeffs . toCoeffs == id " $ \(Poly a) ->
Just a === fromCoeffs (toCoeffs a)
, testProperty "addition with zero" $ \(Poly a) ->
conjoin [ a === zero .+ a
, a === a .+ zero
]
, testProperty "addition associative" $ \(Poly a) (Poly b) (Poly c) ->
a .+ (b .+ c) === (a .+ b) .+ c
, testProperty "addition commutative" $ \(Poly a) (Poly b) ->
a .+ b === b .+ a
, testProperty "substraction with zero" $ \(Poly a) ->
a === a .- zero
, testProperty "substraction non-associative" $ \(Poly a) (Poly b) (Poly c) ->
a .- (b .- c) === (a .- b) .+ c
, testProperty "substraction anti-commutative" $ \(Poly a) (Poly b) ->
a .- b === neg (b .- a)
, testProperty "negation" $ \(Poly a) ->
neg a === zero .- a
, testProperty "double negation" $ \(Poly a) ->
a === neg (neg a)
, testCase "norm zero" $ norm (zero :: Rq Sec) @=? 0
, testProperty "norm positiveness" $ \(Poly a) ->
(norm a == 0) === (a == zero)
, testProperty "norm even" $ \(Poly a) ->
norm (neg a) === norm a
, testProperty "norm sub-additivity" $ \(Poly a) (Poly b) ->
norm (a .+ b) <= norm a + norm b
]
, testGroup "Tq"
[ testProperty "nttInv . ntt == id" $ \(Poly a) ->
a === nttInv (ntt a)
, testProperty "addition with zero" $ \(PolyNTT a) ->
conjoin [ a === zero .+ a
, a === a .+ zero
]
, testProperty "addition associative" $ \(PolyNTT a) (PolyNTT b) (PolyNTT c) ->
a .+ (b .+ c) === (a .+ b) .+ c
, testProperty "addition commutative" $ \(PolyNTT a) (PolyNTT b) ->
a .+ b === b .+ a
, testProperty "substraction with zero" $ \(PolyNTT a) ->
a === a .- zero
, testProperty "substraction non-associative" $ \(PolyNTT a) (PolyNTT b) (PolyNTT c) ->
a .- (b .- c) === (a .- b) .+ c
, testProperty "substraction anti-commutative" $ \(PolyNTT a) (PolyNTT b) ->
a .- b === neg (b .- a)
, testProperty "negation" $ \(PolyNTT a) ->
neg a === zero .- a
, testProperty "double negation" $ \(PolyNTT a) ->
a === neg (neg a)
, testProperty "multiplication with zero" $ \(PolyNTT a) ->
conjoin [ zero === zero .* a
, zero === a .* zero
]
, testProperty "multiplication with one" $ \(PolyNTT a) ->
conjoin [ a === one .* a
, a === a .* one
]
, testProperty "multiplication associative" $ \(PolyNTT a) (PolyNTT b) (PolyNTT c) ->
a .* (b .* c) === (a .* b) .* c
, testProperty "multiplication commutative" $ \(PolyNTT a) (PolyNTT b) ->
a .* b === b .* a
, testProperty "multiplication distributive" $ \(PolyNTT a) (PolyNTT b) (PolyNTT c) ->
conjoin [ (a .* b) .+ (a .* c) === a .* (b .+ c)
, (b .* a) .+ (c .* a) === (b .+ c) .* a
]
, testProperty "mulAdd" $ \(PolyNTT a) (PolyNTT b) (PolyNTT c) ->
a .* b .+ c === mulAdd a b c
]
, testGroup "Vector"
[ testProperty "addition with zero" $ \(Dim n) -> do
a <- arbitraryVector n
return $ conjoin
[ a === zero .+ a
, a === a .+ zero
]
, testProperty "addition associative" $ \(Dim n) -> do
(a, b, c) <- (,,) <$> arbitraryVector n <*> arbitraryVector n <*> arbitraryVector n
return (a .+ (b .+ c) === (a .+ b) .+ c)
, testProperty "addition commutative" $ \(Dim n) -> do
(a, b) <- (,) <$> arbitraryVector n <*> arbitraryVector n
return (a .+ b === b .+ a)
, testProperty "substraction with zero" $ \(Dim n) -> do
a <- arbitraryVector n
return (a === a .- zero)
, testProperty "substraction non-associative" $ \(Dim n) -> do
(a, b, c) <- (,,) <$> arbitraryVector n <*> arbitraryVector n <*> arbitraryVector n
return (a .- (b .- c) === (a .- b) .+ c)
, testProperty "substraction anti-commutative" $ \(Dim n) -> do
(a, b) <- (,) <$> arbitraryVector n <*> arbitraryVector n
return (a .- b === neg (b .- a))
, testProperty "negation" $ \(Dim n) -> do
a <- arbitraryVector n
return (neg a === zero .- a)
, testProperty "double negation" $ \(Dim n) -> do
a <- arbitraryVector n
return (a === neg (neg a))
, testProperty "dot product commutative" $ \(Dim n) -> do
(u, v) <- (,) <$> arbitraryVector n <*> arbitraryVector n
return (u `dot` v === v `dot` u)
, testProperty "dot product distributive" $ \(Dim n) -> do
(u, v, w) <- (,,) <$> arbitraryVector n <*> arbitraryVector n <*> arbitraryVector n
return $ conjoin
[ u `dot` (v .+ w) === (u `dot` v) .+ (u `dot` w)
, (u .+ v) `dot` w === (u `dot` w) .+ (v `dot` w)
]
]
, testGroup "Matrix"
[ testProperty "mmul distributive left" $ \(Dim n) (Dim m) -> do
(a, b, u) <- (,,) <$> arbitraryMatrix n m <*> arbitraryMatrix n m <*> arbitraryVector m
return ((a .+ b) `mmul` u === (a `mmul` u) .+ (b `mmul` u))
, testProperty "mmul distributive right" $ \(Dim n) (Dim m) -> do
(a, u, v) <- (,,) <$> arbitraryMatrix n m <*> arbitraryVector m <*> arbitraryVector m
return (a `mmul` (u .+ v) === (a `mmul` u) .+ (a `mmul` v))
, testProperty "mmulAdd definition" $ \(Dim n) (Dim m) -> do
(a, u, v) <- (,,) <$> arbitraryMatrix n m <*> arbitraryVector m <*> arbitraryVector n
return (mmulAdd a u v == (a `mmul` u) .+ v)
, testProperty "mmulAdd distributive left" $ \(Dim n) (Dim m) -> do
(a, b, u, v) <- (,,,) <$> arbitraryMatrix n m <*> arbitraryMatrix n m <*> arbitraryVector m <*> arbitraryVector n
return (mmulAdd (a .+ b) u v === mmulAdd a u (mmulAdd b u zero) .+ v)
, testProperty "mmulAdd distributive right" $ \(Dim n) (Dim m) -> do
(a, u, v, w) <- (,,,) <$> arbitraryMatrix n m <*> arbitraryVector m <*> arbitraryVector m <*> arbitraryVector n
return (mmulAdd a (u .+ v) w === mmulAdd a u (mmulAdd a v w))
]
#endif
]
]