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

Documentation.SBV.Examples.Misc.Polynomials

Description

Simple usage of polynomials over GF(2^n), using Rijndael's finite field: http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field

The functions available are:

pMult
  GF(2^n) Multiplication
pDiv
  GF(2^n) Division
pMod
  GF(2^n) Modulus
pDivMod
  GF(2^n) Division/Modulus, packed together

Note that addition in GF(2^n) is simply `xor`, so no custom function is provided.

Synopsis

- type GF28 = SWord8
- gfMult :: GF28 -> GF28 -> GF28
- multUnit :: GF28 -> SBool
- multComm :: GF28 -> GF28 -> SBool
- multAssoc :: GF28 -> GF28 -> GF28 -> SBool
- polyDivMod :: GF28 -> GF28 -> SBool
- testGF28 :: IO ()

# Documentation

type GF28 = SWord8 Source #

Helper synonym for representing GF(2^8); which are merely 8-bit unsigned words. Largest term in such a polynomial has degree 7.

gfMult :: GF28 -> GF28 -> GF28 Source #

Multiplication in Rijndael's field; usual polynomial multiplication followed by reduction by the irreducible polynomial. The irreducible used by Rijndael's field is the polynomial `x^8 + x^4 + x^3 + x + 1`, which we write by giving it's exponents in SBV. See: http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field. Note that the irreducible itself is not in GF28! It has a degree of 8.

NB. You can use the `showPoly` function to print polynomials nicely, as a mathematician would write.

multUnit :: GF28 -> SBool Source #

States that the unit polynomial `1`, is the unit element

multComm :: GF28 -> GF28 -> SBool Source #

States that multiplication is commutative

multAssoc :: GF28 -> GF28 -> GF28 -> SBool Source #

States that multiplication is associative, note that associativity proofs are notoriously hard for SAT/SMT solvers

polyDivMod :: GF28 -> GF28 -> SBool Source #

States that the usual multiplication rule holds over GF(2^n) polynomials Checks:

       if (a, b) = x pDivMod y then x = y pMult a + b

being careful about `y = 0`. When divisor is 0, then quotient is defined to be 0 and the remainder is the numerator. (Note that addition is simply `xor` in GF(2^8).)

testGF28 :: IO () Source #

Queries