-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Existentials.CRCPolynomial
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- This program demonstrates the use of the existentials and the QBVF (quantified
-- bit-vector solver). We generate CRC polynomials of degree 16 that can be used
-- for messages of size 48-bits. The query finds all such polynomials that have hamming
-- distance is at least 4. That is, if the CRC can't tell two different 48-bit messages
-- apart, then they must differ in at least 4 bits.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Existentials.CRCPolynomial where

import Data.SBV
import Data.SBV.Tools.Polynomial

-- | Compute the 16 bit CRC of a 48 bit message, using the given polynomial
crc_48_16 :: SWord 48 -> SWord16 -> [SBool]
crc_48_16 :: SWord 48 -> SWord16 -> [SBool]
crc_48_16 SWord 48
msg SWord16
poly = Int -> [SBool] -> [SBool] -> [SBool]
crcBV Int
16 (SWord 48 -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SWord 48
msg) (SWord16 -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SWord16
poly)

-- | Count the differing bits in the message and the corresponding CRC
diffCount :: (SWord 48, [SBool]) -> (SWord 48, [SBool]) -> SWord8
diffCount :: (SWord 48, [SBool]) -> (SWord 48, [SBool]) -> SWord8
diffCount (SWord 48
d1, [SBool]
crc1) (SWord 48
d2, [SBool]
crc2) = [SBool] -> SWord8
forall p. (Num p, Mergeable p) => [SBool] -> p
count [SBool]
xorBits
  where bits1 :: [SBool]
bits1   = SWord 48 -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SWord 48
d1 [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ [SBool]
crc1
        bits2 :: [SBool]
bits2   = SWord 48 -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SWord 48
d2 [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ [SBool]
crc2
        -- xor will give us a false if bits match, true if they differ
        xorBits :: [SBool]
xorBits = (SBool -> SBool -> SBool) -> [SBool] -> [SBool] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SBool -> SBool -> SBool
(.<+>) [SBool]
bits1 [SBool]
bits2
        count :: [SBool] -> p
count []     = p
0
        count (SBool
b:[SBool]
bs) = let r :: p
r = [SBool] -> p
count [SBool]
bs in SBool -> p -> p -> p
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
b (p
1p -> p -> p
forall a. Num a => a -> a -> a
+p
r) p
r

-- | Given a hamming distance value @hd@, 'crcGood' returns @true@ if
-- the 16 bit polynomial can distinguish all messages that has at most
-- @hd@ different bits. Note that we express this conversely: If the
-- @sent@ and @received@ messages are different, then it must be the
-- case that that must differ from each other (including CRCs), in
-- more than @hd@ bits.
crcGood :: SWord8 -> SWord16 -> SWord 48 -> SWord 48 -> SBool
crcGood :: SWord8 -> SWord16 -> SWord 48 -> SWord 48 -> SBool
crcGood SWord8
hd SWord16
poly SWord 48
sent SWord 48
received =
     SWord 48
sent SWord 48 -> SWord 48 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SWord 48
received SBool -> SBool -> SBool
.=> (SWord 48, [SBool]) -> (SWord 48, [SBool]) -> SWord8
diffCount (SWord 48
sent, [SBool]
crcSent) (SWord 48
received, [SBool]
crcReceived) SWord8 -> SWord8 -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SWord8
hd
   where crcSent :: [SBool]
crcSent     = SWord 48 -> SWord16 -> [SBool]
crc_48_16 SWord 48
sent     SWord16
poly
         crcReceived :: [SBool]
crcReceived = SWord 48 -> SWord16 -> [SBool]
crc_48_16 SWord 48
received SWord16
poly

-- | Generate good CRC polynomials for 48-bit words, given the hamming distance @hd@.
genPoly :: SWord8 -> Int -> IO ()
genPoly :: SWord8 -> Int -> IO ()
genPoly SWord8
hd Int
maxCnt = do AllSatResult
res <- SMTConfig -> SymbolicT IO SBool -> IO AllSatResult
forall a. Provable a => SMTConfig -> a -> IO AllSatResult
allSatWith SMTConfig
defaultSMTCfg{allSatMaxModelCount :: Maybe Int
allSatMaxModelCount = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
maxCnt} (SymbolicT IO SBool -> IO AllSatResult)
-> SymbolicT IO SBool -> IO AllSatResult
forall a b. (a -> b) -> a -> b
$ do
                                SWord16
p <- String -> Symbolic SWord16
forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists String
"polynomial" -- the polynomial is existentially specified
                                SWord 48
s <- String -> Symbolic (SWord 48)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvForall String
"sent"       -- sent word, universal
                                SWord 48
r <- String -> Symbolic (SWord 48)
forall a. SymVal a => String -> Symbolic (SBV a)
sbvForall String
"received"   -- received word, universal
                                -- assert that the polynomial @p@ is good. Note
                                -- that we also supply the extra information that
                                -- the least significant bit must be set in the
                                -- polynomial, as all CRC polynomials have the "+1"
                                -- term in them set. This simplifies the query.
                                SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SWord16 -> Int -> SBool
forall a. SFiniteBits a => SBV a -> Int -> SBool
sTestBit SWord16
p Int
0 SBool -> SBool -> SBool
.&& SWord8 -> SWord16 -> SWord 48 -> SWord 48 -> SBool
crcGood SWord8
hd SWord16
p SWord 48
s SWord 48
r
                       Int
cnt <- ([(Bool, Word16)] -> [(Bool, Word16)])
-> (Int -> (Bool, Word16) -> IO ()) -> AllSatResult -> IO Int
forall a.
SatModel a =>
([(Bool, a)] -> [(Bool, a)])
-> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels [(Bool, Word16)] -> [(Bool, Word16)]
forall a. a -> a
id Int -> (Bool, Word16) -> IO ()
disp AllSatResult
res
                       String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
cnt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" polynomail(s)."
        where disp :: Int -> (Bool, Word16) -> IO ()
              disp :: Int -> (Bool, Word16) -> IO ()
disp Int
n (Bool
_, Word16
s) = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Polynomial #" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". x^16 + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> Word16 -> String
forall a. Polynomial a => Bool -> a -> String
showPolynomial Bool
False Word16
s

-- | Find and display all degree 16 polynomials with hamming distance at least 4, for 48 bit messages.
--
-- When run, this function prints:
--
--  @
--    Polynomial #1. x^16 + x^3 + x^2 + 1
--    Polynomial #2. x^16 + x^3 + x^2 + x + 1
--    Polynomial #3. x^16 + x^3 + x + 1
--    Polynomial #4. x^16 + x^15 + x^2 + 1
--    Polynomial #5. x^16 + x^15 + x^2 + x + 1
--    Found: 5 polynomial(s).
--  @
--
-- Note that different runs can produce different results, depending on the random
-- numbers used by the solver, solver version, etc. (Also, the solver will take some
-- time to generate these results. On my machine, the first five polynomials were
-- generated in about 5 minutes.)
findHD4Polynomials :: IO ()
findHD4Polynomials :: IO ()
findHD4Polynomials = SWord8 -> Int -> IO ()
genPoly SWord8
4 Int
cnt
  where cnt :: Int
cnt = Int
5 -- Generate at most this many polynomials

{-# ANN crc_48_16 ("HLint: ignore Use camelCase" :: String) #-}