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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

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

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
Polynomial Word8 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial Word16 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial Word32 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial Word64 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial SWord64 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial SWord32 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial SWord16 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial SWord8 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

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