----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Examples.Uninterpreted.AUF -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- -- Formalizes and proves the following theorem, about arithmetic, -- uninterpreted functions, and arrays. (For reference, see <http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf> -- slide number 24): -- -- @ -- x + 2 = y implies f (read (write (a, x, 3), y - 2)) = f (y - x + 1) -- @ -- -- We interpret the types as follows (other interpretations certainly possible): -- -- [/x/] 'SWord32' (32-bit unsigned address) -- -- [/y/] 'SWord32' (32-bit unsigned address) -- -- [/a/] An array, indexed by 32-bit addresses, returning 32-bit unsigned integers -- -- [/f/] An uninterpreted function of type @'SWord32' -> 'SWord64'@ -- -- The function @read@ and @write@ are usual array operations. ----------------------------------------------------------------------------- module Data.SBV.Examples.Uninterpreted.AUF where import Data.SBV -------------------------------------------------------------- -- * Model using functional arrays -------------------------------------------------------------- -- | The array type, takes symbolic 32-bit unsigned indexes -- and stores 32-bit unsigned symbolic values. These are -- functional arrays where reading before writing a cell -- throws an exception. type A = SFunArray Word32 Word32 -- | Uninterpreted function in the theorem f :: SWord32 -> SWord64 f = uninterpret "f" -- | Correctness theorem. We state it for all values of @x@, @y@, and -- the array @a@. We also take an arbitrary initializer for the array. thm1 :: SWord32 -> SWord32 -> A -> SWord32 -> SBool thm1 x y a initVal = lhs ==> rhs where a' = resetArray a initVal -- initialize array lhs = x + 2 .== y rhs = f (readArray (writeArray a' x 3) (y - 2)) .== f (y - x + 1) -- | Prints Q.E.D. when run, as expected -- -- >>> proveThm1 -- Q.E.D. proveThm1 :: IO ThmResult proveThm1 = prove $ do x <- free "x" y <- free "y" a <- newArray "a" Nothing i <- free "initVal" return $ thm1 x y a i -------------------------------------------------------------- -- * Model using SMT arrays -------------------------------------------------------------- -- | This version directly uses SMT-arrays and hence does not need an initializer. -- Reading an element before writing to it returns an arbitrary value. type B = SArray Word32 Word32 -- | Same as 'thm1', except we don't need an initializer with the 'SArray' model. thm2 :: SWord32 -> SWord32 -> B -> SBool thm2 x y a = lhs ==> rhs where lhs = x + 2 .== y rhs = f (readArray (writeArray a x 3) (y - 2)) .== f (y - x + 1) -- | Prints Q.E.D. when run, as expected: -- -- >>> proveThm2 -- Q.E.D. proveThm2 :: IO ThmResult proveThm2 = prove $ do x <- free "x" y <- free "y" a <- newArray "b" Nothing return $ thm2 x y a