sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.Existentials.CRCPolynomial

Contents

- Modeling 48 bit words

Description

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.

Synopsis

- type SWord48 = (SWord32, SWord16)
- crc_48_16 :: SWord48 -> SWord16 -> [SBool]
- diffCount :: (SWord48, [SBool]) -> (SWord48, [SBool]) -> SWord8
- crcGood :: SWord8 -> SWord16 -> SWord48 -> SWord48 -> SBool
- genPoly :: SWord8 -> IO ()
- findHD4Polynomials :: IO ()

# Modeling 48 bit words

type SWord48 = (SWord32, SWord16) Source #

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] Source #

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

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

Count the differing bits in the message and the corresponding CRC

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

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 () Source #

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

findHD4Polynomials :: IO () Source #

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.)