Documentation

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