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

-- | States that the unit polynomial @1@, is the unit element
multUnit :: GF28 -> SBool
multUnit :: GF28 -> SBool
multUnit 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 [Int
0]   -- x@0

-- | States that multiplication is commutative
multComm :: GF28 -> GF28 -> SBool
multComm :: GF28 -> GF28 -> SBool
multComm GF28
x 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 GF28
x GF28
y 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 GF28
x 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
.== GF28
0) ((GF28
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 (GF28
a, 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