----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Examples.Existentials.CRCPolynomial -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- Portability : portable -- -- 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. ----------------------------------------------------------------------------- module Data.SBV.Examples.Existentials.CRCPolynomial where import Data.SBV ----------------------------------------------------------------------------- -- * Modeling 48 bit words ----------------------------------------------------------------------------- -- | SBV doesn't support 48 bit words natively. So, we represent them -- as a tuple, 32 high-bits and 16 low-bits. type SWord48 = (SWord32, SWord16) -- | Compute the 16 bit CRC of a 48 bit message, using the given polynomial crc_48_16 :: SWord48 -> SWord16 -> [SBool] crc_48_16 msg poly = crcBV 16 msgBits polyBits where (hi, lo) = msg msgBits = blastBE hi ++ blastBE lo polyBits = blastBE poly -- | Count the differing bits in the message and the corresponding CRC diffCount :: (SWord48, [SBool]) -> (SWord48, [SBool]) -> SWord8 diffCount ((h1, l1), crc1) ((h2, l2), crc2) = count xorBits where bits1 = blastBE h1 ++ blastBE l1 ++ crc1 bits2 = blastBE h2 ++ blastBE l2 ++ crc2 -- xor will give us a false if bits match, true if they differ xorBits = zipWith (<+>) bits1 bits2 count [] = 0 count (b:bs) = let r = count bs in ite b (1+r) 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 -> SWord48 -> SWord48 -> SBool crcGood hd poly sent received = sent ./= received ==> diffCount (sent, crcSent) (received, crcReceived) .>= hd where crcSent = crc_48_16 sent poly crcReceived = crc_48_16 received poly -- | Generate good CRC polynomials for 48-bit words, given the hamming distance @hd@. genPoly :: SWord8 -> IO () genPoly hd = do res <- allSatWith z3 $ do -- the polynomial is existentially specified p <- exists "polynomial" -- sent word, universal s <- do sh <- forall "sh" sl <- forall "sl" return (sh, sl) -- received word, universal r <- do rh <- forall "rh" rl <- forall "rl" return (rh, rl) -- 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. return $ sbvTestBit p 0 &&& crcGood hd p s r cnt <- displayModels disp res putStrLn $ "Found: " ++ show cnt ++ " polynomail(s)." where disp :: Int -> (Bool, Word16) -> IO () disp n (_, s) = do putStrLn $ "Polynomial #" ++ show n ++ ". x^16 + " ++ showPolynomial False 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^2 + x + 1 -- Polynomial #2. x^16 + x^15 + x^2 + 1 -- Polynomial #3. x^16 + x^15 + x^14 + 1 -- Polynomial #4. x^16 + x^15 + x^2 + x + 1 -- Polynomial #5. x^16 + x^14 + x + 1 -- ... -- @ -- -- 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 = genPoly 4