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:
- GF(2^n) Multiplication
- GF(2^n) Division
- GF(2^n) Modulus
- GF(2^n) Division/Modulus, packed together
Note that addition in GF(2^n) is simply
xor, so no custom function is provided.
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.
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 multiplication is associative, note that associativity proofs are notoriously hard for SAT/SMT solvers