Counter.hs

-------------------------------------------------------------------------------
-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- | Example showing an implementation of a resettable counter.

{-# LANGUAGE RebindableSyntax #-}

module Copilot.Verifier.Examples.ShouldPass.Counter where

import Control.Monad (when)
import qualified Prelude as P

import Language.Copilot
import Copilot.Compile.C99
import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)
                        , defaultVerifierOptions, verifyWithOptions )
import Copilot.Theorem.What4 (prove, Solver(..))

-- A resettable counter
counter :: (Typed a, Integral a) => Stream Bool -> Stream Bool -> Stream a
counter inc reset = cnt
  where
    cnt = if reset then 0
          else if inc then z + 1
               else z
    z = [0] ++ cnt

-- Counter that resets when it reaches 256
bytecounter :: Stream Int32
bytecounter = counter true (resetcounter `mod` 256 == 0)

resetcounter :: Stream Word32
resetcounter = counter true false

bytecounter2 :: Stream Int32
bytecounter2 = counter true ([False] ++ bytecounter2 == 255)

spec :: Spec
spec =
  do _ <- prop "range" (forAll (bytecounter == unsafeCast (resetcounter `mod` 256)))
     _ <- prop "range2" (forAll (0 <= bytecounter2 && bytecounter2 <= 255))
     _ <- prop "same"  (forAll ((0 <= bytecounter2 && bytecounter2 <= 255) &&
                                (bytecounter == unsafeCast (resetcounter `mod` 256)) &&
                                (bytecounter == bytecounter2)))
     trigger "counter" true [arg $ bytecounter, arg $ bytecounter2]

verifySpec :: Verbosity -> IO ()
-- verifSpec _ = interpret 1280 spec
verifySpec verb =
  do s <- reify spec
     r <- prove Z3 s
     when (verb P.>= Default) $
       print r
     verifyWithOptions defaultVerifierOptions{verbosity = verb}
                       mkDefaultCSettings ["range", "range2"] "counter" s