Data.SBV.Examples.Existentials.CRCPolynomial

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.

Modeling 48 bit words

type SWord48 = (SWord32, SWord16)

SBV doesn't support 48 bit words natively. So, we represent them as a tuple, 32 high-bits and 16 low-bits.

crc_48_16 :: SWord48 -> SWord16 -> [SBool]

Compute the 16 bit CRC of a 48 bit message, using the given polynomial

diffCount :: (SWord48, [SBool]) -> (SWord48, [SBool]) -> SWord8

Count the differing bits in the message and the corresponding CRC

crcGood :: SWord8 -> SWord16 -> SWord48 -> SWord48 -> SBool

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.

genPoly :: SWord8 -> IO ()

Generate good CRC polynomials for 48-bit words, given the hamming distance hd.

findHD4Polynomials :: IO ()

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^2 + x + 1
   Polynomial #4. x^16 + x^14 + x^10 + 1
   Polynomial #5. x^16 + x^14 + x^9 + 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.)