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

Copyright (c) Levent Erkok BSD3 erkokl@gmail.com experimental None Haskell2010

Data.SBV.Examples.Existentials.CRCPolynomial

Contents

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

# 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

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

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