Data.SBV.Tools.Polynomial

Implementation of polynomial arithmetic

Polynomial arithmetic and CRCs

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

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

pMult, pDivMod, showPolynomial

Methods

polynomial :: [Int] -> a

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.

pAdd :: a -> a -> a

Add two polynomials in GF(2^n).

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

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.

pDiv :: a -> a -> a

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

pMod :: a -> a -> a

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

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

Division and modulus packed together.

showPoly :: a -> String

Display a polynomial like a mathematician would (over the monomial x), with a type.

showPolynomial :: Bool -> a -> String

Display a polynomial like a mathematician would (over the monomial x), the first argument controls if the final type is shown as well.

Instances

Polynomial Word8

Methods

polynomial :: [Int] -> Word8

pAdd :: Word8 -> Word8 -> Word8

pMult :: (Word8, Word8, [Int]) -> Word8

pDiv :: Word8 -> Word8 -> Word8

pMod :: Word8 -> Word8 -> Word8

pDivMod :: Word8 -> Word8 -> (Word8, Word8)

showPoly :: Word8 -> String

showPolynomial :: Bool -> Word8 -> String

Polynomial Word16

Methods

polynomial :: [Int] -> Word16

pAdd :: Word16 -> Word16 -> Word16

pMult :: (Word16, Word16, [Int]) -> Word16

pDiv :: Word16 -> Word16 -> Word16

pMod :: Word16 -> Word16 -> Word16

pDivMod :: Word16 -> Word16 -> (Word16, Word16)

showPoly :: Word16 -> String

showPolynomial :: Bool -> Word16 -> String

Polynomial Word32

Methods

polynomial :: [Int] -> Word32

pAdd :: Word32 -> Word32 -> Word32

pMult :: (Word32, Word32, [Int]) -> Word32

pDiv :: Word32 -> Word32 -> Word32

pMod :: Word32 -> Word32 -> Word32

pDivMod :: Word32 -> Word32 -> (Word32, Word32)

showPoly :: Word32 -> String

showPolynomial :: Bool -> Word32 -> String

Polynomial Word64

Methods

polynomial :: [Int] -> Word64

pAdd :: Word64 -> Word64 -> Word64

pMult :: (Word64, Word64, [Int]) -> Word64

pDiv :: Word64 -> Word64 -> Word64

pMod :: Word64 -> Word64 -> Word64

pDivMod :: Word64 -> Word64 -> (Word64, Word64)

showPoly :: Word64 -> String

showPolynomial :: Bool -> Word64 -> String

Polynomial SWord64

Methods

polynomial :: [Int] -> SWord64

pAdd :: SWord64 -> SWord64 -> SWord64

pMult :: (SWord64, SWord64, [Int]) -> SWord64

pDiv :: SWord64 -> SWord64 -> SWord64

pMod :: SWord64 -> SWord64 -> SWord64

pDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64)

showPoly :: SWord64 -> String

showPolynomial :: Bool -> SWord64 -> String

Polynomial SWord32

Methods

polynomial :: [Int] -> SWord32

pAdd :: SWord32 -> SWord32 -> SWord32

pMult :: (SWord32, SWord32, [Int]) -> SWord32

pDiv :: SWord32 -> SWord32 -> SWord32

pMod :: SWord32 -> SWord32 -> SWord32

pDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32)

showPoly :: SWord32 -> String

showPolynomial :: Bool -> SWord32 -> String

Polynomial SWord16

Methods

polynomial :: [Int] -> SWord16

pAdd :: SWord16 -> SWord16 -> SWord16

pMult :: (SWord16, SWord16, [Int]) -> SWord16

pDiv :: SWord16 -> SWord16 -> SWord16

pMod :: SWord16 -> SWord16 -> SWord16

pDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16)

showPoly :: SWord16 -> String

showPolynomial :: Bool -> SWord16 -> String

Polynomial SWord8

Methods

polynomial :: [Int] -> SWord8

pAdd :: SWord8 -> SWord8 -> SWord8

pMult :: (SWord8, SWord8, [Int]) -> SWord8

pDiv :: SWord8 -> SWord8 -> SWord8

pMod :: SWord8 -> SWord8 -> SWord8

pDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8)

showPoly :: SWord8 -> String

showPolynomial :: Bool -> SWord8 -> String

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

Compute CRC's over polynomials, i.e., symbolic words. The first Int argument plays the same role as the one in the crcBV function.

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

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

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.

mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])

Compute modulus/remainder of polynomials on bit-vectors.

addPoly :: [SBool] -> [SBool] -> [SBool]

Add two polynomials