----------------------------------------------------------------------------- -- | -- Module : TestSuite.Crypto.AES -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- -- Test suite for Data.SBV.Examples.Crypto.AES ----------------------------------------------------------------------------- module TestSuite.Crypto.AES(testSuite) where import Data.SBV import Data.SBV.Internals import Data.SBV.Examples.Crypto.AES import SBVTest -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \goldCheck -> test [ "aes128Enc" ~: compileToC' "aes128Enc" (aes128EncDec True) `goldCheck` "aes128Enc.gold" , "aes128Dec" ~: compileToC' "aes128Dec" (aes128EncDec False) `goldCheck` "aes128Dec.gold" , "aes128Lib" ~: compileToCLib' "aes128Lib" aes128Comps `goldCheck` "aes128Lib.gold" ] where aes128EncDec d = do pt <- cgInputArr 4 "pt" key <- cgInputArr 4 "key" cgSetDriverValues $ repeat 0 let (encKs, decKs) = aesKeySchedule key res | d = aesEncrypt pt encKs | True = aesDecrypt pt decKs cgOutputArr "ct" res aes128Comps = [(f, setVals c) | (f, c) <- aes128LibComponents] setVals c = cgSetDriverValues (repeat 0) >> c