Parity.hs

-----------------------------------------------------------------------------
-- |
-- Module      :  TestSuite.CRC.Parity
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Test suite for Examples.CRC.Parity
-----------------------------------------------------------------------------

module TestSuite.CRC.Parity(tests) where

import Utils.SBVTestFramework

tests :: TestTree
tests =
  testGroup "CRC.Parity"
    [ testCase "parity" (assertIsThm parityOK)
    ]

parity :: SWord64 -> SBool
parity x = bnot (isOdd cnt)
  where cnt :: SWord8
        cnt = sum $ map oneIf $ blastLE x

isOdd :: SWord8 -> SBool
isOdd = lsb

-- Example suggested by Lee Pike
-- If x and y differ in odd-number of bits, then their parities are flipped
parityOK :: SWord64 -> SWord64 -> SBool
parityOK x y = isOdd cnt ==> px .== bnot py
  where cnt = sum $ map oneIf $ zipWith (./=) (blastLE x) (blastLE y)
        px  = parity x
        py  = parity y