| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.SBV.Tools.Polynomial
Contents
Description
Implementation of polynomial arithmetic
Synopsis
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
Minimal complete definition
Methods
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. Mathematicians 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 usually 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.
Instances
crc :: (SFiniteBits a, SFiniteBits 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 nth 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 nth 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
mby addingn0 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 sFalse at the end (i.e., zero-bits); which nicely pads it when considered as an unsigned number in little-endian form.