-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.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.
-----------------------------------------------------------------------------

{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Uninterpreted.AUF where

import Data.SBV

--------------------------------------------------------------
-- * Model using functional arrays
--------------------------------------------------------------

-- | Uninterpreted function in the theorem
f :: SWord32 -> SWord64
f :: SWord32 -> SWord64
f = String -> SWord32 -> SWord64
forall a. Uninterpreted a => String -> a
uninterpret String
"f"

-- | Correctness theorem. We state it for all values of @x@, @y@, and
-- the given array @a@. Note that we're being generic in the type of
-- array we're expecting.
thm :: SymArray a => SWord32 -> SWord32 -> a Word32 Word32 -> SBool
thm :: SWord32 -> SWord32 -> a Word32 Word32 -> SBool
thm SWord32
x SWord32
y a Word32 Word32
a = SBool
lhs SBool -> SBool -> SBool
.=> SBool
rhs
  where lhs :: SBool
lhs = SWord32
x SWord32 -> SWord32 -> SWord32
forall a. Num a => a -> a -> a
+ SWord32
2 SWord32 -> SWord32 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord32
y
        rhs :: SBool
rhs =     SWord32 -> SWord64
f (a Word32 Word32 -> SWord32 -> SWord32
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray (a Word32 Word32 -> SWord32 -> SWord32 -> a Word32 Word32
forall (array :: * -> * -> *) b a.
(SymArray array, SymVal b) =>
array a b -> SBV a -> SBV b -> array a b
writeArray a Word32 Word32
a SWord32
x SWord32
3) (SWord32
y SWord32 -> SWord32 -> SWord32
forall a. Num a => a -> a -> a
- SWord32
2))
              SWord64 -> SWord64 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord32 -> SWord64
f (SWord32
y SWord32 -> SWord32 -> SWord32
forall a. Num a => a -> a -> a
- SWord32
x SWord32 -> SWord32 -> SWord32
forall a. Num a => a -> a -> a
+ SWord32
1)

-- | Prove it using SMT-Lib arrays.
--
-- >>> proveSArray
-- Q.E.D.
proveSArray :: IO ThmResult
proveSArray :: IO ThmResult
proveSArray = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
                SWord32
x <- String -> Symbolic SWord32
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"x"
                SWord32
y <- String -> Symbolic SWord32
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"y"
                SArray Word32 Word32
a :: SArray Word32 Word32 <- Maybe SWord32 -> Symbolic (SArray Word32 Word32)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
Maybe (SBV b) -> Symbolic (array a b)
newArray_ Maybe SWord32
forall a. Maybe a
Nothing
                SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SWord32 -> SWord32 -> SArray Word32 Word32 -> SBool
forall (a :: * -> * -> *).
SymArray a =>
SWord32 -> SWord32 -> a Word32 Word32 -> SBool
thm SWord32
x SWord32
y SArray Word32 Word32
a

-- | Prove it using SBV's internal functional arrays.
--
-- >>> proveSFunArray
-- Q.E.D.
proveSFunArray :: IO ThmResult
proveSFunArray :: IO ThmResult
proveSFunArray = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
                SWord32
x <- String -> Symbolic SWord32
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"x"
                SWord32
y <- String -> Symbolic SWord32
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"y"
                SFunArray Word32 Word32
a :: SFunArray Word32 Word32 <- Maybe SWord32 -> Symbolic (SFunArray Word32 Word32)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
Maybe (SBV b) -> Symbolic (array a b)
newArray_ Maybe SWord32
forall a. Maybe a
Nothing
                SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SWord32 -> SWord32 -> SFunArray Word32 Word32 -> SBool
forall (a :: * -> * -> *).
SymArray a =>
SWord32 -> SWord32 -> a Word32 Word32 -> SBool
thm SWord32
x SWord32
y SFunArray Word32 Word32
a