-------------------------------------------------------------------------------
-- 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 :: forall a.
(Typed a, Integral a) =>
Stream Bool -> Stream Bool -> Stream a
counter Stream Bool
inc Stream Bool
reset = Stream a
cnt
  where
    cnt :: Stream a
cnt = if Stream Bool
reset then Stream a
0
          else if Stream Bool
inc then Stream a
z Stream a -> Stream a -> Stream a
forall a. Num a => a -> a -> a
+ Stream a
1
               else Stream a
z
    z :: Stream a
z = [a
0] [a] -> Stream a -> Stream a
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream a
cnt

-- Counter that resets when it reaches 256
bytecounter :: Stream Int32
bytecounter :: Stream Int32
bytecounter = Stream Bool -> Stream Bool -> Stream Int32
forall a.
(Typed a, Integral a) =>
Stream Bool -> Stream Bool -> Stream a
counter Stream Bool
true (Stream Word32
resetcounter Stream Word32 -> Stream Word32 -> Stream Word32
forall a. (Typed a, Integral a) => Stream a -> Stream a -> Stream a
`mod` Stream Word32
256 Stream Word32 -> Stream Word32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Word32
0)

resetcounter :: Stream Word32
resetcounter :: Stream Word32
resetcounter = Stream Bool -> Stream Bool -> Stream Word32
forall a.
(Typed a, Integral a) =>
Stream Bool -> Stream Bool -> Stream a
counter Stream Bool
true Stream Bool
false

bytecounter2 :: Stream Int32
bytecounter2 :: Stream Int32
bytecounter2 = Stream Bool -> Stream Bool -> Stream Int32
forall a.
(Typed a, Integral a) =>
Stream Bool -> Stream Bool -> Stream a
counter Stream Bool
true ([Bool
False] [Bool] -> Stream Bool -> Stream Bool
forall a. Typed a => [a] -> Stream a -> Stream a
++ Stream Int32
bytecounter2 Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Int32
255)

spec :: Spec
spec :: Spec
spec =
  do PropRef Universal
_ <- Name -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. Name -> Prop a -> Writer [SpecItem] (PropRef a)
prop Name
"range" (Stream Bool -> Prop Universal
forAll (Stream Int32
bytecounter Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Word32 -> Stream Int32
forall a b.
(UnsafeCast a b, Typed a, Typed b) =>
Stream a -> Stream b
unsafeCast (Stream Word32
resetcounter Stream Word32 -> Stream Word32 -> Stream Word32
forall a. (Typed a, Integral a) => Stream a -> Stream a -> Stream a
`mod` Stream Word32
256)))
     PropRef Universal
_ <- Name -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. Name -> Prop a -> Writer [SpecItem] (PropRef a)
prop Name
"range2" (Stream Bool -> Prop Universal
forAll (Stream Int32
0 Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream Int32
bytecounter2 Stream Bool -> Stream Bool -> Stream Bool
&& Stream Int32
bytecounter2 Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream Int32
255))
     PropRef Universal
_ <- Name -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. Name -> Prop a -> Writer [SpecItem] (PropRef a)
prop Name
"same"  (Stream Bool -> Prop Universal
forAll ((Stream Int32
0 Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream Int32
bytecounter2 Stream Bool -> Stream Bool -> Stream Bool
&& Stream Int32
bytecounter2 Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
<= Stream Int32
255) Stream Bool -> Stream Bool -> Stream Bool
&&
                                (Stream Int32
bytecounter Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Word32 -> Stream Int32
forall a b.
(UnsafeCast a b, Typed a, Typed b) =>
Stream a -> Stream b
unsafeCast (Stream Word32
resetcounter Stream Word32 -> Stream Word32 -> Stream Word32
forall a. (Typed a, Integral a) => Stream a -> Stream a -> Stream a
`mod` Stream Word32
256)) Stream Bool -> Stream Bool -> Stream Bool
&&
                                (Stream Int32
bytecounter Stream Int32 -> Stream Int32 -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Stream Int32
bytecounter2)))
     Name -> Stream Bool -> [Arg] -> Spec
trigger Name
"counter" Stream Bool
true [Stream Int32 -> Arg
forall a. Typed a => Stream a -> Arg
arg (Stream Int32 -> Arg) -> Stream Int32 -> Arg
forall a b. (a -> b) -> a -> b
$ Stream Int32
bytecounter, Stream Int32 -> Arg
forall a. Typed a => Stream a -> Arg
arg (Stream Int32 -> Arg) -> Stream Int32 -> Arg
forall a b. (a -> b) -> a -> b
$ Stream Int32
bytecounter2]

verifySpec :: Verbosity -> IO ()
-- verifSpec _ = interpret 1280 spec
verifySpec :: Verbosity -> IO ()
verifySpec Verbosity
verb =
  do Spec
s <- Spec -> IO Spec
forall a. Spec' a -> IO Spec
reify Spec
spec
     [(Name, SatResult)]
r <- Solver -> Spec -> IO [(Name, SatResult)]
prove Solver
Z3 Spec
s
     Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Verbosity
verb Verbosity -> Verbosity -> Bool
forall a. Ord a => a -> a -> Bool
P.>= Verbosity
Default) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
       [(Name, SatResult)] -> IO ()
forall a. Show a => a -> IO ()
print [(Name, SatResult)]
r
     VerifierOptions -> CSettings -> [Name] -> Name -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions{verbosity = verb}
                       CSettings
mkDefaultCSettings [Name
"range", Name
"range2"] Name
"counter" Spec
s