Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Implementation of polynomial arithmetic

- class (Num a, Bits a) => Polynomial a where
- crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b
- crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
- ites :: SBool -> [SBool] -> [SBool] -> [SBool]
- mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
- addPoly :: [SBool] -> [SBool] -> [SBool]

# Polynomial arithmetic and CRCs

class (Num a, Bits a) => Polynomial a where Source #

Implements polynomial addition, multiplication, division, and modulus operations
over GF(2^n). NB. Similar to `sQuotRem`

, division by `0`

is interpreted as follows:

`x ``pDivMod`

0 = (0, x)

for all `x`

(including `0`

)

Minimal complete definition: `pMult`

, `pDivMod`

, `showPolynomial`

polynomial :: [Int] -> a Source #

Given bit-positions to be set, create a polynomial For instance

polynomial [0, 1, 3] :: SWord8

will evaluate to `11`

, since it sets the bits `0`

, `1`

, and `3`

. Mathematicans would write this polynomial
as `x^3 + x + 1`

. And in fact, `showPoly`

will show it like that.

Add two polynomials in GF(2^n).

pMult :: (a, a, [Int]) -> a Source #

Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by the polynomial as specified by coefficients of the third argument. Note that the third argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles, so this should not be a problem in practice.)

Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't fit into the resulting size.

Divide two polynomials in GF(2^n), see above note for division by 0.

Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0.

pDivMod :: a -> a -> (a, a) Source #

Division and modulus packed together.

showPoly :: a -> String Source #

Display a polynomial like a mathematician would (over the monomial `x`

), with a type.

showPolynomial :: Bool -> a -> String Source #

Display a polynomial like a mathematician would (over the monomial `x`

), the first argument
controls if the final type is shown as well.

crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b Source #

crcBV :: Int -> [SBool] -> [SBool] -> [SBool] Source #

Compute CRCs over bit-vectors. The call `crcBV n m p`

computes
the CRC of the message `m`

with respect to polynomial `p`

. The
inputs are assumed to be blasted big-endian. The number
`n`

specifies how many bits of CRC is needed. Note that `n`

is actually the degree of the polynomial `p`

, and thus it seems
redundant to pass it in. However, in a typical proof context,
the polynomial can be symbolic, so we cannot compute the degree
easily. While this can be worked-around by generating code that
accounts for all possible degrees, the resulting code would
be unnecessarily big and complicated, and much harder to reason
with. (Also note that a CRC is just the remainder from the
polynomial division, but this routine is much faster in practice.)

NB. The `n`

th bit of the polynomial `p`

*must* be set for the CRC
to be computed correctly. Note that the polynomial argument `p`

will
not even have this bit present most of the time, as it will typically
contain bits `0`

through `n-1`

as usual in the CRC literature. The higher
order `n`

th bit is simply assumed to be set, as it does not make
sense to use a polynomial of a lesser degree. This is usually not a problem
since CRC polynomials are designed and expressed this way.

NB. The literature on CRC's has many variants on how CRC's are computed. We follow the following simple procedure:

- Extend the message
`m`

by adding`n`

0 bits on the right - Divide the polynomial thus obtained by the
`p`

- The remainder is the CRC value.

There are many variants on final XOR's, reversed polynomials etc., so
it is essential to double check you use the correct *algorithm*.

ites :: SBool -> [SBool] -> [SBool] -> [SBool] Source #

Run down a boolean condition over two lists. Note that this is different than zipWith as shorter list is assumed to be filled with false at the end (i.e., zero-bits); which nicely pads it when considered as an unsigned number in little-endian form.