diff --git a/Data/SBV/Examples/Polynomials/Polynomials.hs b/Data/SBV/Examples/Polynomials/Polynomials.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Polynomials/Polynomials.hs @@ -0,0 +1,78 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Polynomials.Polynomials +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- Portability : portable +-- +-- Simple usage of polynomials over GF(2^n), using Rijndael's +-- 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: . +-- 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 diff --git a/Data/SBV/TestSuite/Polynomials/Polynomials.hs b/Data/SBV/TestSuite/Polynomials/Polynomials.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/TestSuite/Polynomials/Polynomials.hs @@ -0,0 +1,25 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.TestSuite.Polynomials.Polynomials +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- Portability : portable +-- +-- Test suite for Data.SBV.Examples.Polynomials.Polynomials +----------------------------------------------------------------------------- + +module Data.SBV.TestSuite.Polynomials.Polynomials(testSuite) where + +import Data.SBV +import Data.SBV.Internals +import Data.SBV.Examples.Polynomials.Polynomials + +-- Test suite +testSuite :: SBVTestSuite +testSuite = mkTestSuite $ \_ -> test [ + "polynomial-1" ~: assert =<< isTheorem multUnit + , "polynomial-2" ~: assert =<< isTheorem multComm + , "polynomial-3" ~: assert =<< isTheorem polyDivMod + ] diff --git a/SBVUnitTest/SBVUnitTest.hs b/SBVUnitTest/SBVUnitTest.hs --- a/SBVUnitTest/SBVUnitTest.hs +++ b/SBVUnitTest/SBVUnitTest.hs @@ -39,16 +39,17 @@ import qualified Data.SBV.TestSuite.CRC.GenPoly as T12(testSuite) import qualified Data.SBV.TestSuite.CRC.Parity as T13(testSuite) import qualified Data.SBV.TestSuite.CRC.USB5 as T14(testSuite) -import qualified Data.SBV.TestSuite.PrefixSum.PrefixSum as T15(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.DogCatMouse as T16(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.MagicSquare as T17(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.NQueens as T18(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.PowerSet as T19(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.Sudoku as T20(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.Temperature as T21(testSuite) -import qualified Data.SBV.TestSuite.Puzzles.U2Bridge as T22(testSuite) -import qualified Data.SBV.TestSuite.Uninterpreted.AUF as T23(testSuite) -import qualified Data.SBV.TestSuite.Uninterpreted.Uninterpreted as T24(testSuite) +import qualified Data.SBV.TestSuite.Polynomials.Polynomials as T15(testSuite) +import qualified Data.SBV.TestSuite.PrefixSum.PrefixSum as T16(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.DogCatMouse as T17(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.MagicSquare as T18(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.NQueens as T19(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.PowerSet as T20(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.Sudoku as T21(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.Temperature as T22(testSuite) +import qualified Data.SBV.TestSuite.Puzzles.U2Bridge as T23(testSuite) +import qualified Data.SBV.TestSuite.Uninterpreted.AUF as T24(testSuite) +import qualified Data.SBV.TestSuite.Uninterpreted.Uninterpreted as T25(testSuite) testCollection :: [SBVTestSuite] testCollection = [ @@ -58,6 +59,7 @@ , T13.testSuite, T14.testSuite, T15.testSuite, T16.testSuite , T17.testSuite, T18.testSuite, T19.testSuite, T20.testSuite , T21.testSuite, T22.testSuite, T23.testSuite, T24.testSuite + , T25.testSuite ] -- No user serviceable parts below.. diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 0.9.3 +Version: 0.9.4 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers. Description: Adds support for symbolic bit vectors, allowing formal models of bit-precise @@ -42,6 +42,7 @@ , Data.SBV.Internals , Data.SBV.Examples.BitPrecise.BitTricks , Data.SBV.Examples.BitPrecise.Legato + , Data.SBV.Examples.Polynomials.Polynomials , Data.SBV.Examples.Puzzles.DogCatMouse , Data.SBV.Examples.Puzzles.MagicSquare , Data.SBV.Examples.Puzzles.NQueens @@ -93,6 +94,7 @@ , Data.SBV.TestSuite.CRC.Parity , Data.SBV.TestSuite.CRC.USB5 , Data.SBV.TestSuite.PrefixSum.PrefixSum + , Data.SBV.TestSuite.Polynomials.Polynomials , Data.SBV.TestSuite.Puzzles.DogCatMouse , Data.SBV.TestSuite.Puzzles.MagicSquare , Data.SBV.TestSuite.Puzzles.NQueens