----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Examples.Polynomials.Polynomials -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- -- 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. ----------------------------------------------------------------------------- module Data.SBV.Examples.Polynomials.Polynomials where import Data.SBV -- | Helper synonym for representing GF(2^8); which are merely 8-bit unsigned words. Largest -- term in such a polynomial has degree 7. type GF28 = SWord8 -- | 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. (<*>) :: GF28 -> GF28 -> GF28 a <*> b = pMult (a, b, [8, 4, 3, 1, 0]) -- | States that the unit polynomial @1@, is the unit element multUnit :: GF28 -> SBool multUnit x = (x <*> unit) .== x where unit = polynomial [0] -- x@0 -- | States that multiplication is commutative multComm :: GF28 -> GF28 -> SBool multComm x y = (x <*> y) .== (y <*> x) -- | States that multiplication is associative, note that associativity -- proofs are notoriously hard for SAT/SMT solvers multAssoc :: GF28 -> GF28 -> GF28 -> SBool multAssoc x y z = ((x <*> y) <*> z) .== (x <*> (y <*> z)) -- | 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).) polyDivMod :: GF28 -> GF28 -> SBool polyDivMod x y = ite (y .== 0) ((0, x) .== (a, b)) (x .== y <*> a `xor` b) where (a, b) = x `pDivMod` y -- | Queries testGF28 :: IO () testGF28 = do print =<< prove multUnit print =<< prove multComm -- print =<< prove multAssoc -- takes too long; see above note.. print =<< prove polyDivMod