    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Misc.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 Documentation.SBV.Examples.Misc.Polynomials where

    import Data.SBV
    import Data.SBV.Tools.Polynomial

    {-# OPTIONS_GHC -Wall -Werror #-}

    -- | 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.
    gfMult :: GF28 -> GF28 -> GF28
    a :: GF28
    a gfMult :: GF28 -> GF28 -> GF28
    `gfMult` b :: GF28
    b = (GF28, GF28, [Int]) -> GF28
    forall a. Polynomial a => (a, a, [Int]) -> a
    pMult (GF28
    a, GF28
    b, [8, 4, 3, 1, 0])

    -- | States that the unit polynomial @1@, is the unit element
    multUnit :: GF28 -> SBool
    multUnit :: GF28 -> SBool
    multUnit x :: GF28
    x = (GF28
    x GF28 -> GF28 -> GF28
    `gfMult` GF28
    unit) GF28 -> GF28 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== GF28
    x
      where unit :: GF28
    unit = [Int] -> GF28
    forall a. Polynomial a => [Int] -> a
    polynomial [0]   -- x@0

    -- | States that multiplication is commutative
    multComm :: GF28 -> GF28 -> SBool
    multComm :: GF28 -> GF28 -> SBool
    multComm x :: GF28
    x y :: GF28
    y = (GF28
    x GF28 -> GF28 -> GF28
    `gfMult` GF28
    y) GF28 -> GF28 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (GF28
    y GF28 -> GF28 -> GF28
    `gfMult` GF28
    x)

    -- | States that multiplication is associative, note that associativity
    -- proofs are notoriously hard for SAT/SMT solvers
    multAssoc :: GF28 -> GF28 -> GF28 -> SBool
    multAssoc :: GF28 -> GF28 -> GF28 -> SBool
    multAssoc x :: GF28
    x y :: GF28
    y z :: GF28
    z = ((GF28
    x GF28 -> GF28 -> GF28
    `gfMult` GF28
    y) GF28 -> GF28 -> GF28
    `gfMult` GF28
    z) GF28 -> GF28 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (GF28
    x GF28 -> GF28 -> GF28
    `gfMult` (GF28
    y GF28 -> GF28 -> GF28
    `gfMult` GF28
    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 :: GF28 -> GF28 -> SBool
    polyDivMod x :: GF28
    x y :: GF28
    y = SBool -> SBool -> SBool -> SBool
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (GF28
    y GF28 -> GF28 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 0) ((0, GF28
    x) (GF28, GF28) -> (GF28, GF28) -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (GF28
    a, GF28
    b)) (GF28
    x GF28 -> GF28 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (GF28
    y GF28 -> GF28 -> GF28
    `gfMult` GF28
    a) GF28 -> GF28 -> GF28
    forall a. Bits a => a -> a -> a
    `xor` GF28
    b)
      where (a :: GF28
    a, b :: GF28
    b) = GF28
    x GF28 -> GF28 -> (GF28, GF28)
    forall a. Polynomial a => a -> a -> (a, a)
    `pDivMod` GF28
    y

    -- | Queries
    testGF28 :: IO ()
    testGF28 :: IO ()
    testGF28 = do
      ThmResult -> IO ()
    forall a. Show a => a -> IO ()
    print (ThmResult -> IO ()) -> IO ThmResult -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (GF28 -> SBool) -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove GF28 -> SBool
    multUnit
      ThmResult -> IO ()
    forall a. Show a => a -> IO ()
    print (ThmResult -> IO ()) -> IO ThmResult -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (GF28 -> GF28 -> SBool) -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove GF28 -> GF28 -> SBool
    multComm
      -- print =<< prove multAssoc -- takes too long; see above note..
      ThmResult -> IO ()
    forall a. Show a => a -> IO ()
    print (ThmResult -> IO ()) -> IO ThmResult -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (GF28 -> GF28 -> SBool) -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove GF28 -> GF28 -> SBool
    polyDivMod