    -----------------------------------------------------------------------------
    -- |
    -- 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 {a}. (Num a, Mergeable a) => [SBool] -> a
    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] -> a
    count []     = a
    0
            count (SBool
    b:[SBool]
    bs) = let r :: a
    r = [SBool] -> a
    count [SBool]
    bs in SBool -> a -> a -> a
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    b (a
    1a -> a -> a
    forall a. Num a => a -> a -> a
    +a
    r) a
    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 () -> IO AllSatResult
    forall a. Satisfiable 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 () -> IO AllSatResult)
    -> SymbolicT IO () -> IO AllSatResult
    forall a b. (a -> b) -> a -> b
    $ do
                                    SWord16
    poly <- String -> Symbolic SWord16
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "polynomial" -- the polynomial is existentially specified
                                    (Forall Any (WordN 48) -> Forall Any (WordN 48) -> SBool)
    -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any (WordN 48) -> Forall Any (WordN 48) -> SBool)
     -> SymbolicT IO ())
    -> (Forall Any (WordN 48) -> Forall Any (WordN 48) -> SBool)
    -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SWord 48
    sent) (Forall SWord 48
    received) ->
                                       -- 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.
                                       SWord16 -> Int -> SBool
    forall a. SFiniteBits a => SBV a -> Int -> SBool
    sTestBit SWord16
    poly Int
    0 SBool -> SBool -> SBool
    .&& SWord8 -> SWord16 -> SWord 48 -> SWord 48 -> SBool
    crcGood SWord8
    hd SWord16
    poly SWord 48
    sent SWord 48
    received
                           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
    " polynomial(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.
    --
    -- We have:
    --
    -- >>> findHD4Polynomials 2
    -- Polynomial #1. x^16 + x^3 + x^2 + 1
    -- Polynomial #2. x^16 + x^2 + x + 1
    -- Found: 2 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, as the generation of these polynomials is rather slow.)
    findHD4Polynomials :: Int -> IO ()
    findHD4Polynomials :: Int -> IO ()
    findHD4Polynomials = SWord8 -> Int -> IO ()
    genPoly SWord8
    4

    {- HLint ignore crc_48_16 "Use camelCase" -}