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

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

# 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.

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.

States that the unit polynomial 1, is the unit element

States that multiplication is commutative

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

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).)

Queries