sbv-8.7: 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

Data.SBV.Tools.Polynomial

Contents

- Polynomial arithmetic and CRCs

Description

Implementation of polynomial arithmetic

Synopsis

- class (Num a, Bits a) => Polynomial a where
  - polynomial :: [Int] -> a
  - pAdd :: a -> a -> a
  - pMult :: (a, a, [Int]) -> a
  - pDiv :: a -> a -> a
  - pMod :: a -> a -> a
  - pDivMod :: a -> a -> (a, a)
  - showPoly :: a -> String
  - showPolynomial :: Bool -> a -> String
- crc :: (SFiniteBits a, SFiniteBits 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`

Minimal complete definition

pMult, pDivMod, showPolynomial

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`. Mathematicans would write this polynomial as `x^3 + x + 1`. And in fact, `showPoly` will show it like that.

pAdd :: a -> a -> a Source #

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.

pDiv :: a -> a -> a Source #

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

pMod :: a -> a -> a Source #

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

Instances details

Polynomial Word8 Source # |

Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [Int] -> Word8 Source #

pAdd :: Word8 -> Word8 -> Word8 Source #

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

pDiv :: Word8 -> Word8 -> Word8 Source #

pMod :: Word8 -> Word8 -> Word8 Source #

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

showPoly :: Word8 -> String Source #

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

Polynomial Word16 Source # |

Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [Int] -> Word16 Source #

pAdd :: Word16 -> Word16 -> Word16 Source #

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

pDiv :: Word16 -> Word16 -> Word16 Source #

pMod :: Word16 -> Word16 -> Word16 Source #

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

showPoly :: Word16 -> String Source #

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

Polynomial Word32 Source # |

Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [Int] -> Word32 Source #

pAdd :: Word32 -> Word32 -> Word32 Source #

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

pDiv :: Word32 -> Word32 -> Word32 Source #

pMod :: Word32 -> Word32 -> Word32 Source #

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

showPoly :: Word32 -> String Source #

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

Polynomial Word64 Source # |

Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [Int] -> Word64 Source #

pAdd :: Word64 -> Word64 -> Word64 Source #

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

pDiv :: Word64 -> Word64 -> Word64 Source #

pMod :: Word64 -> Word64 -> Word64 Source #

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

showPoly :: Word64 -> String Source #

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

Polynomial SWord64 Source # |

Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [Int] -> SWord64 Source #

pAdd :: SWord64 -> SWord64 -> SWord64 Source #

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

pDiv :: SWord64 -> SWord64 -> SWord64 Source #

pMod :: SWord64 -> SWord64 -> SWord64 Source #

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

showPoly :: SWord64 -> String Source #

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

Polynomial SWord32 Source # |

Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [Int] -> SWord32 Source #

pAdd :: SWord32 -> SWord32 -> SWord32 Source #

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

pDiv :: SWord32 -> SWord32 -> SWord32 Source #

pMod :: SWord32 -> SWord32 -> SWord32 Source #

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

showPoly :: SWord32 -> String Source #

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

Polynomial SWord16 Source # |

Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [Int] -> SWord16 Source #

pAdd :: SWord16 -> SWord16 -> SWord16 Source #

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

pDiv :: SWord16 -> SWord16 -> SWord16 Source #

pMod :: SWord16 -> SWord16 -> SWord16 Source #

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

showPoly :: SWord16 -> String Source #

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

Polynomial SWord8 Source # |

Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [Int] -> SWord8 Source #

pAdd :: SWord8 -> SWord8 -> SWord8 Source #

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

pDiv :: SWord8 -> SWord8 -> SWord8 Source #

pMod :: SWord8 -> SWord8 -> SWord8 Source #

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

showPoly :: SWord8 -> String Source #

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

(KnownNat n, IsNonZero n) => Polynomial (SWord n) Source # |

Instance details

Defined in Data.SBV.Tools.Polynomial

Methods

polynomial :: [Int] -> SWord n Source #

pAdd :: SWord n -> SWord n -> SWord n Source #

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

pDiv :: SWord n -> SWord n -> SWord n Source #

pMod :: SWord n -> SWord n -> SWord n Source #

pDivMod :: SWord n -> SWord n -> (SWord n, SWord n) Source #

showPoly :: SWord n -> String Source #

showPolynomial :: Bool -> SWord n -> String Source #

crc :: (SFiniteBits a, SFiniteBits b) => Int -> SBV a -> SBV b -> SBV b Source #

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

Compute modulus/remainder of polynomials on bit-vectors.

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

Add two polynomials