Sum.hs

-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.ProofTools.Sum
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Example inductive proof to show partial correctness of the traditional
-- for-loop sum algorithm:
--
-- @
--     s = 0
--     i = 0
--     while i <= n:
--        s += i
--        i++
-- @
--
-- We prove the loop invariant and establish partial correctness that
-- @s@ is the sum of all numbers up to and including @n@ upon termination.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE TypeFamilies          #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.ProofTools.Sum where

import Data.SBV
import Data.SBV.Tools.Induction

-- * System state

-- | System state. We simply have two components, parameterized
-- over the type so we can put in both concrete and symbolic values.
data S a = S { s :: a, i :: a, n :: a } deriving (Show, Traversable, Functor, Foldable)

-- | 'Queriable instance for our state
instance Queriable IO (S SInteger) where
  type QueryResult (S SInteger) = S Integer
  create = S <$> freshVar_ <*> freshVar_ <*> freshVar_

-- | Encoding partial correctness of the sum algorithm. We have:
--
-- >>> sumCorrect
-- Q.E.D.
sumCorrect :: IO (InductionResult (S Integer))
sumCorrect = induct chatty setup initial trans strengthenings inv goal
  where -- Set this to True for SBV to print steps as it proceeds
        -- through the inductive proof
        chatty :: Bool
        chatty = False

        -- This is where we would put solver options, typically via
        -- calls to 'Data.SBV.setOption'. We do not need any for this problem,
        -- so we simply do nothing.
        setup :: Symbolic ()
        setup = pure ()

        -- Initially, @s@ and @i@ are both @0@. We also require @n@ to be at least @0@.
        initial :: S SInteger -> SBool
        initial S{s, i, n} = s .== 0 .&& i .== 0 .&& n .>= 0

        -- We code the algorithm almost literally in SBV notation:
        trans :: S SInteger -> S SInteger -> SBool
        trans S{s, i, n} S{s = s', i = i', n = n'} = (s', i', n') .== ite (i .<= n)
                                                                          (s+i, i+1, n)
                                                                          (s  , i  , n)

        -- No strengthenings needed for this problem!
        strengthenings :: [(String, S SInteger -> SBool)]
        strengthenings = []

        -- Loop invariant: @i@ remains at most @n+1@ and @s@ the sum of
        -- all the numbers up-to @i-1@.
        inv :: S SInteger -> SBool
        inv S{s, i, n} =    i .<= n+1
                        .&& s .== (i * (i - 1)) `sDiv` 2

        -- Final goal. When the termination condition holds, the sum is
        -- equal to all the numbers up to and including @n@. Note that
        -- SBV does not prove the termination condition; it simply is
        -- the indication that the loop has ended as specified by the user.
        goal :: S SInteger -> (SBool, SBool)
        goal S{s, i, n} = (i .== n+1, s .== (n * (n+1)) `sDiv` 2)