sbv-8.0: SBVTestSuite/TestSuite/Crypto/RC4.hs

-----------------------------------------------------------------------------
-- |
-- Module    : TestSuite.Crypto.RC4
-- Author    : Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test suite for Documentation.SBV.Examples.Crypto.RC4
-----------------------------------------------------------------------------

module TestSuite.Crypto.RC4(tests) where

import Data.SBV.Tools.STree
import Documentation.SBV.Examples.Crypto.RC4

import Utils.SBVTestFramework

tests :: TestTree
tests =
  testGroup "Crypto.RC4"
    [ testCase "rc4swap" (assertIsThm readWrite)
    ]

readWrite :: SBV Word8 -> SBV Word8 -> SBV Bool
readWrite i j = readSTree (writeSTree initS i j) i .== j