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

-- | Example showing usage of clocks to generate periodically recurring truth
-- values.

module Copilot.Verifier.Examples.ShouldPass.Clock 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(..))

-- | We need to force a type for the argument of `period`.
p :: Word8
p :: Word8
p = Word8
5

-- | Both have the same period, but a different phase.
clkStream :: Stream Bool
clkStream :: Stream Bool
clkStream  = Period Word8 -> Phase Word8 -> Stream Bool
forall a. Integral a => Period a -> Phase a -> Stream Bool
clk (Word8 -> Period Word8
forall a. Integral a => a -> Period a
period Word8
p) (Word8 -> Phase Word8
forall a. Integral a => a -> Phase a
phase Word8
0)

clkStream' :: Stream Bool
clkStream' :: Stream Bool
clkStream' = Period Word8 -> Phase Word8 -> Stream Bool
forall a. Integral a => Period a -> Phase a -> Stream Bool
clk (Word8 -> Period Word8
forall a. Integral a => a -> Period a
period Word8
p) (Word8 -> Phase Word8
forall a. Integral a => a -> Phase a
phase Word8
2)

spec :: Spec
spec :: Spec
spec = do
  Name -> Stream Bool -> Spec
forall a. Typed a => Name -> Stream a -> Spec
observer Name
"clk"  Stream Bool
clkStream
  Name -> Stream Bool -> Spec
forall a. Typed a => Name -> Stream a -> Spec
observer Name
"clk'" Stream Bool
clkStream'
  PropRef Universal
_ <- Name -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. Name -> Prop a -> Writer [SpecItem] (PropRef a)
prop Name
"clksPhase" (Stream Bool -> Prop Universal
forAll (Stream Bool
clkStream Stream Bool -> Stream Bool -> Stream Bool
forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
== Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
2 Stream Bool
clkStream'))
  PropRef Universal
_ <- Name -> Prop Universal -> Writer [SpecItem] (PropRef Universal)
forall a. Name -> Prop a -> Writer [SpecItem] (PropRef a)
prop Name
"clksDistinct" (Stream Bool -> Prop Universal
forAll (Stream Bool -> Stream Bool
not (Stream Bool
clkStream Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
clkStream')))
  Name -> Stream Bool -> [Arg] -> Spec
trigger Name
"clksHigh" (Stream Bool
clkStream Stream Bool -> Stream Bool -> Stream Bool
&& Stream Bool
clkStream') []


verifySpec :: Verbosity -> IO ()
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
"clock" Spec
s