-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.WeakestPreconditions.GCD
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proof of correctness of an imperative GCD (greatest-common divisor)
-- algorithm, using weakest preconditions. The termination measure here
-- illustrates the use of lexicographic ordering. Also, since symbolic
-- version of GCD is not symbolically terminating, this is another
-- example of using uninterpreted functions and axioms as one writes
-- specifications for WP proofs.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE TypeFamilies          #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.WeakestPreconditions.GCD where

import Data.SBV
import Data.SBV.Tools.WeakestPreconditions

import GHC.Generics (Generic)

-- Access Prelude's gcd, but qualified:
import Prelude hiding (gcd)
import qualified Prelude as P (gcd)

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV
-- >>> import Data.SBV.Control
-- >>> import Data.SBV.Tools.WeakestPreconditions
#endif

-- * Program state

-- | The state for the sum program, parameterized over a base type @a@.
data GCDS a = GCDS { forall a. GCDS a -> a
x :: a    -- ^ First value
                   , forall a. GCDS a -> a
y :: a    -- ^ Second value
                   , forall a. GCDS a -> a
i :: a    -- ^ Copy of x to be modified
                   , forall a. GCDS a -> a
j :: a    -- ^ Copy of y to be modified
                   }
                   deriving (Int -> GCDS a -> ShowS
[GCDS a] -> ShowS
GCDS a -> String
(Int -> GCDS a -> ShowS)
-> (GCDS a -> String) -> ([GCDS a] -> ShowS) -> Show (GCDS a)
forall a. Show a => Int -> GCDS a -> ShowS
forall a. Show a => [GCDS a] -> ShowS
forall a. Show a => GCDS a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> GCDS a -> ShowS
showsPrec :: Int -> GCDS a -> ShowS
$cshow :: forall a. Show a => GCDS a -> String
show :: GCDS a -> String
$cshowList :: forall a. Show a => [GCDS a] -> ShowS
showList :: [GCDS a] -> ShowS
Show, (forall x. GCDS a -> Rep (GCDS a) x)
-> (forall x. Rep (GCDS a) x -> GCDS a) -> Generic (GCDS a)
forall x. Rep (GCDS a) x -> GCDS a
forall x. GCDS a -> Rep (GCDS a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (GCDS a) x -> GCDS a
forall a x. GCDS a -> Rep (GCDS a) x
$cfrom :: forall a x. GCDS a -> Rep (GCDS a) x
from :: forall x. GCDS a -> Rep (GCDS a) x
$cto :: forall a x. Rep (GCDS a) x -> GCDS a
to :: forall x. Rep (GCDS a) x -> GCDS a
Generic, Bool -> SBool -> GCDS a -> GCDS a -> GCDS a
(Bool -> SBool -> GCDS a -> GCDS a -> GCDS a)
-> (forall b.
    (Ord b, SymVal b, Num b, Num (SBV b)) =>
    [GCDS a] -> GCDS a -> SBV b -> GCDS a)
-> Mergeable (GCDS a)
forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[GCDS a] -> GCDS a -> SBV b -> GCDS a
forall a.
Mergeable a =>
Bool -> SBool -> GCDS a -> GCDS a -> GCDS a
forall a b.
(Mergeable a, Ord b, SymVal b, Num b, Num (SBV b)) =>
[GCDS a] -> GCDS a -> SBV b -> GCDS a
forall a.
(Bool -> SBool -> a -> a -> a)
-> (forall b.
    (Ord b, SymVal b, Num b, Num (SBV b)) =>
    [a] -> a -> SBV b -> a)
-> Mergeable a
$csymbolicMerge :: forall a.
Mergeable a =>
Bool -> SBool -> GCDS a -> GCDS a -> GCDS a
symbolicMerge :: Bool -> SBool -> GCDS a -> GCDS a -> GCDS a
$cselect :: forall a b.
(Mergeable a, Ord b, SymVal b, Num b, Num (SBV b)) =>
[GCDS a] -> GCDS a -> SBV b -> GCDS a
select :: forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[GCDS a] -> GCDS a -> SBV b -> GCDS a
Mergeable, Functor GCDS
Foldable GCDS
(Functor GCDS, Foldable GCDS) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> GCDS a -> f (GCDS b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    GCDS (f a) -> f (GCDS a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> GCDS a -> m (GCDS b))
-> (forall (m :: * -> *) a. Monad m => GCDS (m a) -> m (GCDS a))
-> Traversable GCDS
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => GCDS (m a) -> m (GCDS a)
forall (f :: * -> *) a. Applicative f => GCDS (f a) -> f (GCDS a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> GCDS a -> m (GCDS b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> GCDS a -> f (GCDS b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> GCDS a -> f (GCDS b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> GCDS a -> f (GCDS b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => GCDS (f a) -> f (GCDS a)
sequenceA :: forall (f :: * -> *) a. Applicative f => GCDS (f a) -> f (GCDS a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> GCDS a -> m (GCDS b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> GCDS a -> m (GCDS b)
$csequence :: forall (m :: * -> *) a. Monad m => GCDS (m a) -> m (GCDS a)
sequence :: forall (m :: * -> *) a. Monad m => GCDS (m a) -> m (GCDS a)
Traversable, (forall a b. (a -> b) -> GCDS a -> GCDS b)
-> (forall a b. a -> GCDS b -> GCDS a) -> Functor GCDS
forall a b. a -> GCDS b -> GCDS a
forall a b. (a -> b) -> GCDS a -> GCDS b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> GCDS a -> GCDS b
fmap :: forall a b. (a -> b) -> GCDS a -> GCDS b
$c<$ :: forall a b. a -> GCDS b -> GCDS a
<$ :: forall a b. a -> GCDS b -> GCDS a
Functor, (forall m. Monoid m => GCDS m -> m)
-> (forall m a. Monoid m => (a -> m) -> GCDS a -> m)
-> (forall m a. Monoid m => (a -> m) -> GCDS a -> m)
-> (forall a b. (a -> b -> b) -> b -> GCDS a -> b)
-> (forall a b. (a -> b -> b) -> b -> GCDS a -> b)
-> (forall b a. (b -> a -> b) -> b -> GCDS a -> b)
-> (forall b a. (b -> a -> b) -> b -> GCDS a -> b)
-> (forall a. (a -> a -> a) -> GCDS a -> a)
-> (forall a. (a -> a -> a) -> GCDS a -> a)
-> (forall a. GCDS a -> [a])
-> (forall a. GCDS a -> Bool)
-> (forall a. GCDS a -> Int)
-> (forall a. Eq a => a -> GCDS a -> Bool)
-> (forall a. Ord a => GCDS a -> a)
-> (forall a. Ord a => GCDS a -> a)
-> (forall a. Num a => GCDS a -> a)
-> (forall a. Num a => GCDS a -> a)
-> Foldable GCDS
forall a. Eq a => a -> GCDS a -> Bool
forall a. Num a => GCDS a -> a
forall a. Ord a => GCDS a -> a
forall m. Monoid m => GCDS m -> m
forall a. GCDS a -> Bool
forall a. GCDS a -> Int
forall a. GCDS a -> [a]
forall a. (a -> a -> a) -> GCDS a -> a
forall m a. Monoid m => (a -> m) -> GCDS a -> m
forall b a. (b -> a -> b) -> b -> GCDS a -> b
forall a b. (a -> b -> b) -> b -> GCDS a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => GCDS m -> m
fold :: forall m. Monoid m => GCDS m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> GCDS a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> GCDS a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> GCDS a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> GCDS a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> GCDS a -> b
foldr :: forall a b. (a -> b -> b) -> b -> GCDS a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> GCDS a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> GCDS a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> GCDS a -> b
foldl :: forall b a. (b -> a -> b) -> b -> GCDS a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> GCDS a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> GCDS a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> GCDS a -> a
foldr1 :: forall a. (a -> a -> a) -> GCDS a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> GCDS a -> a
foldl1 :: forall a. (a -> a -> a) -> GCDS a -> a
$ctoList :: forall a. GCDS a -> [a]
toList :: forall a. GCDS a -> [a]
$cnull :: forall a. GCDS a -> Bool
null :: forall a. GCDS a -> Bool
$clength :: forall a. GCDS a -> Int
length :: forall a. GCDS a -> Int
$celem :: forall a. Eq a => a -> GCDS a -> Bool
elem :: forall a. Eq a => a -> GCDS a -> Bool
$cmaximum :: forall a. Ord a => GCDS a -> a
maximum :: forall a. Ord a => GCDS a -> a
$cminimum :: forall a. Ord a => GCDS a -> a
minimum :: forall a. Ord a => GCDS a -> a
$csum :: forall a. Num a => GCDS a -> a
sum :: forall a. Num a => GCDS a -> a
$cproduct :: forall a. Num a => GCDS a -> a
product :: forall a. Num a => GCDS a -> a
Foldable)

-- | Show instance for t'GCDS'. The above deriving clause would work just as well,
-- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (GCDS (SBV a)) where
   show :: GCDS (SBV a) -> String
show (GCDS SBV a
x SBV a
y SBV a
i SBV a
j) = String
"{x = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SBV a
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", y = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SBV a
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", i = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SBV a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", j = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SBV a
j String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
     where sh :: SBV a -> String
sh SBV a
v = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"<symbolic>" a -> String
forall a. Show a => a -> String
show (SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
v)

-- | 'Queriable instance for our state
instance Queriable IO (GCDS SInteger) where
  type QueryResult (GCDS SInteger) = GCDS Integer
  create :: QueryT IO G
create = SInteger -> SInteger -> SInteger -> SInteger -> G
forall a. a -> a -> a -> a -> GCDS a
GCDS (SInteger -> SInteger -> SInteger -> SInteger -> G)
-> QueryT IO SInteger
-> QueryT IO (SInteger -> SInteger -> SInteger -> G)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO SInteger
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_ QueryT IO (SInteger -> SInteger -> SInteger -> G)
-> QueryT IO SInteger -> QueryT IO (SInteger -> SInteger -> G)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO SInteger
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_ QueryT IO (SInteger -> SInteger -> G)
-> QueryT IO SInteger -> QueryT IO (SInteger -> G)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO SInteger
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_ QueryT IO (SInteger -> G) -> QueryT IO SInteger -> QueryT IO G
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO SInteger
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_

-- | Helper type synonym
type G = GCDS SInteger

-- * The algorithm

-- | The imperative GCD algorithm, assuming strictly positive @x@ and @y@:
--
-- @
--    i = x
--    j = y
--    while i != j      -- While not equal
--      if i > j
--         i = i - j    -- i is greater; reduce it by j
--      else
--         j = j - i    -- j is greater; reduce it by i
-- @
--
-- When the loop terminates, @i@ equals @j@ and contains @GCD(x, y)@.
algorithm :: Stmt G
algorithm :: Stmt G
algorithm = [Stmt G] -> Stmt G
forall st. [Stmt st] -> Stmt st
Seq [ String -> (G -> SBool) -> Stmt G
forall st. String -> (st -> SBool) -> Stmt st
assert String
"x > 0, y > 0" ((G -> SBool) -> Stmt G) -> (G -> SBool) -> Stmt G
forall a b. (a -> b) -> a -> b
$ \GCDS{SInteger
x :: forall a. GCDS a -> a
x :: SInteger
x, SInteger
y :: forall a. GCDS a -> a
y :: SInteger
y} -> SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0
                , (G -> G) -> Stmt G
forall st. (st -> st) -> Stmt st
Assign ((G -> G) -> Stmt G) -> (G -> G) -> Stmt G
forall a b. (a -> b) -> a -> b
$ \st :: G
st@GCDS{SInteger
x :: forall a. GCDS a -> a
x :: SInteger
x, SInteger
y :: forall a. GCDS a -> a
y :: SInteger
y} -> G
st{i = x, j = y}
                , String
-> (G -> SBool)
-> Maybe (Measure G)
-> (G -> SBool)
-> Stmt G
-> Stmt G
forall st.
String
-> Invariant st
-> Maybe (Measure st)
-> Invariant st
-> Stmt st
-> Stmt st
While String
"i != j"
                        G -> SBool
inv
                        (Measure G -> Maybe (Measure G)
forall a. a -> Maybe a
Just Measure G
forall a. GCDS a -> [a]
msr)
                        (\GCDS{SInteger
i :: forall a. GCDS a -> a
i :: SInteger
i, SInteger
j :: forall a. GCDS a -> a
j :: SInteger
j} -> SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
j)
                        (Stmt G -> Stmt G) -> Stmt G -> Stmt G
forall a b. (a -> b) -> a -> b
$ (G -> SBool) -> Stmt G -> Stmt G -> Stmt G
forall st. Invariant st -> Stmt st -> Stmt st -> Stmt st
If (\GCDS{SInteger
i :: forall a. GCDS a -> a
i :: SInteger
i, SInteger
j :: forall a. GCDS a -> a
j :: SInteger
j} -> SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
j)
                             ((G -> G) -> Stmt G
forall st. (st -> st) -> Stmt st
Assign ((G -> G) -> Stmt G) -> (G -> G) -> Stmt G
forall a b. (a -> b) -> a -> b
$ \st :: G
st@GCDS{SInteger
i :: forall a. GCDS a -> a
i :: SInteger
i, SInteger
j :: forall a. GCDS a -> a
j :: SInteger
j} -> G
st{i = i - j})
                             ((G -> G) -> Stmt G
forall st. (st -> st) -> Stmt st
Assign ((G -> G) -> Stmt G) -> (G -> G) -> Stmt G
forall a b. (a -> b) -> a -> b
$ \st :: G
st@GCDS{SInteger
i :: forall a. GCDS a -> a
i :: SInteger
i, SInteger
j :: forall a. GCDS a -> a
j :: SInteger
j} -> G
st{j = j - i})
                ]
  where -- This invariant simply states that the value of the gcd remains the same
        -- through the iterations.
        inv :: G -> SBool
inv GCDS{SInteger
x :: forall a. GCDS a -> a
x :: SInteger
x, SInteger
y :: forall a. GCDS a -> a
y :: SInteger
y, SInteger
i :: forall a. GCDS a -> a
i :: SInteger
i, SInteger
j :: forall a. GCDS a -> a
j :: SInteger
j} = SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
j SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger -> SInteger -> SInteger
gcd SInteger
x SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcd SInteger
i SInteger
j

        -- The measure can be taken as @i+j@ going down. However, we
        -- can be more explicit and use the lexicographic nature: Notice
        -- that in each iteration either @i@ goes down, or it stays the same
        -- and @j@ goes down; and they never go below @0@. So we can
        -- have the pair and use the lexicographic ordering.
        msr :: GCDS a -> [a]
msr GCDS{a
i :: forall a. GCDS a -> a
i :: a
i, a
j :: forall a. GCDS a -> a
j :: a
j} = [a
i, a
j]

-- | Symbolic GCD as our specification. Note that we cannot
-- really implement the GCD function since it is not
-- symbolically terminating.  So, we instead uninterpret and
-- axiomatize it below.
--
-- NB. The concrete part of the definition is only used in calls to 'traceExecution'
-- and is not needed for the proof. If you don't need to call 'traceExecution', you
-- can simply ignore that part and directly uninterpret. In that case, we simply
-- use Prelude's version.
gcd :: SInteger -> SInteger -> SInteger
gcd :: SInteger -> SInteger -> SInteger
gcd SInteger
x SInteger
y
 | Just Integer
i <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
x, Just Integer
j <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
y
 = Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
P.gcd Integer
i Integer
j)
 | Bool
True
 = String -> SInteger -> SInteger -> SInteger
forall a. SMTDefinable a => String -> a
uninterpret String
"gcd" SInteger
x SInteger
y

-- | Constraints and axioms we need to state explicitly to tell
-- the SMT solver about our specification for GCD.
axiomatizeGCD :: Symbolic ()
axiomatizeGCD :: Symbolic ()
axiomatizeGCD = do (Forall (ZonkAny 0) Integer -> SBool) -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall (ZonkAny 0) Integer -> SBool) -> Symbolic ())
-> (Forall (ZonkAny 0) Integer -> SBool) -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ \(Forall SInteger
x)            -> SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0            SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
gcd SInteger
x SInteger
x     SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x
                   (Forall (ZonkAny 1) Integer -> Forall (ZonkAny 2) Integer -> SBool)
-> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall (ZonkAny 1) Integer
  -> Forall (ZonkAny 2) Integer -> SBool)
 -> Symbolic ())
-> (Forall (ZonkAny 1) Integer
    -> Forall (ZonkAny 2) Integer -> SBool)
-> Symbolic ()
forall a b. (a -> b) -> a -> b
$ \(Forall SInteger
x) (Forall SInteger
y) -> SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
gcd (SInteger
xSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
y) SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcd SInteger
x SInteger
y
                   (Forall (ZonkAny 3) Integer -> Forall (ZonkAny 4) Integer -> SBool)
-> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall (ZonkAny 3) Integer
  -> Forall (ZonkAny 4) Integer -> SBool)
 -> Symbolic ())
-> (Forall (ZonkAny 3) Integer
    -> Forall (ZonkAny 4) Integer -> SBool)
-> Symbolic ()
forall a b. (a -> b) -> a -> b
$ \(Forall SInteger
x) (Forall SInteger
y) -> SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.=> SInteger -> SInteger -> SInteger
gcd SInteger
x (SInteger
ySInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
x) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcd SInteger
x SInteger
y

-- | Precondition for our program: @x@ and @y@ must be strictly positive
pre :: G -> SBool
pre :: G -> SBool
pre GCDS{SInteger
x :: forall a. GCDS a -> a
x :: SInteger
x, SInteger
y :: forall a. GCDS a -> a
y :: SInteger
y} = SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0 SBool -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
0

-- | Postcondition for our program: @i == j@ and @i = gcd x y@
post :: G -> SBool
post :: G -> SBool
post GCDS{SInteger
x :: forall a. GCDS a -> a
x :: SInteger
x, SInteger
y :: forall a. GCDS a -> a
y :: SInteger
y, SInteger
i :: forall a. GCDS a -> a
i :: SInteger
i, SInteger
j :: forall a. GCDS a -> a
j :: SInteger
j} = SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
j SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger -> SInteger -> SInteger
gcd SInteger
x SInteger
y

-- | Stability condition: Program must leave @x@ and @y@ unchanged.
noChange :: Stable G
noChange :: Stable G
noChange = [String -> (G -> SInteger) -> G -> G -> (String, SBool)
forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"x" G -> SInteger
forall a. GCDS a -> a
x, String -> (G -> SInteger) -> G -> G -> (String, SBool)
forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"y" G -> SInteger
forall a. GCDS a -> a
y]

-- | A program is the algorithm, together with its pre- and post-conditions.
imperativeGCD :: Program G
imperativeGCD :: Program G
imperativeGCD = Program { setup :: Symbolic ()
setup         = Symbolic ()
axiomatizeGCD
                        , precondition :: G -> SBool
precondition  = G -> SBool
pre
                        , program :: Stmt G
program       = Stmt G
algorithm
                        , postcondition :: G -> SBool
postcondition = G -> SBool
post
                        , stability :: Stable G
stability     = Stable G
noChange
                        }

-- * Correctness

-- | With the axioms in place, it is trivial to establish correctness:
--
-- >>> correctness
-- Total correctness is established.
-- Q.E.D.
--
-- Note that I found this proof to be quite fragile: If you do not get the algorithm right
-- or the axioms aren't in place, z3 simply goes to an infinite loop, instead of providing
-- counter-examples. Of course, this is to be expected with the quantifiers present.
correctness :: IO (ProofResult (GCDS Integer))
correctness :: IO (ProofResult (GCDS Integer))
correctness = WPConfig -> Program G -> IO (ProofResult (GCDS Integer))
forall st res.
(Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) =>
WPConfig -> Program st -> IO (ProofResult res)
wpProveWith WPConfig
defaultWPCfg{wpVerbose=True} Program G
imperativeGCD

-- * Concrete execution
-- $concreteExec

{- $concreteExec

Example concrete run. As we mentioned in the definition for 'gcd', the concrete-execution
function cannot deal with uninterpreted functions and axioms for obvious reasons. In those
cases we revert to the concrete definition. Here's an example run:

>>> traceExecution imperativeGCD $ GCDS {x = 14, y = 4, i = 0, j = 0}
*** Precondition holds, starting execution:
  {x = 14, y = 4, i = 0, j = 0}
===> [1.1] Conditional, taking the "then" branch
  {x = 14, y = 4, i = 0, j = 0}
===> [1.1.1] Skip
  {x = 14, y = 4, i = 0, j = 0}
===> [1.2] Assign
  {x = 14, y = 4, i = 14, j = 4}
===> [1.3] Loop "i != j": condition holds, executing the body
  {x = 14, y = 4, i = 14, j = 4}
===> [1.3.{1}] Conditional, taking the "then" branch
  {x = 14, y = 4, i = 14, j = 4}
===> [1.3.{1}.1] Assign
  {x = 14, y = 4, i = 10, j = 4}
===> [1.3] Loop "i != j": condition holds, executing the body
  {x = 14, y = 4, i = 10, j = 4}
===> [1.3.{2}] Conditional, taking the "then" branch
  {x = 14, y = 4, i = 10, j = 4}
===> [1.3.{2}.1] Assign
  {x = 14, y = 4, i = 6, j = 4}
===> [1.3] Loop "i != j": condition holds, executing the body
  {x = 14, y = 4, i = 6, j = 4}
===> [1.3.{3}] Conditional, taking the "then" branch
  {x = 14, y = 4, i = 6, j = 4}
===> [1.3.{3}.1] Assign
  {x = 14, y = 4, i = 2, j = 4}
===> [1.3] Loop "i != j": condition holds, executing the body
  {x = 14, y = 4, i = 2, j = 4}
===> [1.3.{4}] Conditional, taking the "else" branch
  {x = 14, y = 4, i = 2, j = 4}
===> [1.3.{4}.2] Assign
  {x = 14, y = 4, i = 2, j = 2}
===> [1.3] Loop "i != j": condition fails, terminating
  {x = 14, y = 4, i = 2, j = 2}
*** Program successfully terminated, post condition holds of the final state:
  {x = 14, y = 4, i = 2, j = 2}
Program terminated successfully. Final state:
  {x = 14, y = 4, i = 2, j = 2}

As expected, @gcd 14 4@ is @2@.
-}