1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
-- | An example showing the usage of the What4 backend in copilot-theorem for
-- structs and arrays. Particular focus is on nested structs.
-- For general usage of structs, refer to the general structs example.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
module Main where
import qualified Prelude as P
import Control.Monad (void, forM_)
import GHC.Generics (Generic)
import Language.Copilot
import Copilot.Theorem.What4
-- | Definition for `Volts`.
data Volts = Volts
{ numVolts :: Field "numVolts" Word16
, flag :: Field "flag" Bool
}
deriving Generic
-- | `Struct` instance for `Volts`.
instance Struct Volts where
typeName = typeNameDefault
toValues = toValuesDefault
-- Note that we do not implement `updateField` here. `updateField` is only
-- needed to make updates to structs work in the Copilot interpreter, and we
-- do not use the interpreter in this example. (See
-- `examples/StructsUpdateField.hs` for an example that does implement
-- `updateField`.)
-- | `Volts` instance for `Typed`.
instance Typed Volts where
typeOf = typeOfDefault
data Battery = Battery
{ temp :: Field "temp" Word16
, volts :: Field "volts" (Array 10 Volts)
, other :: Field "other" (Array 10 (Array 5 Word32))
}
deriving Generic
-- | `Battery` instance for `Struct`.
instance Struct Battery where
typeName = typeNameDefault
toValues = toValuesDefault
-- Note that we do not implement `updateField` here for the same reasons as in
-- the `Struct Volts` instance above.
-- | `Battery` instance for `Typed`.
instance Typed Battery where
typeOf = typeOfDefault
spec :: Spec
spec = do
let battery :: Stream Battery
battery = extern "battery" Nothing
-- Check equality, indexing into nested structs and arrays. Note that this is
-- trivial by equality.
void $ prop "Example 1" $ forAll $
(((battery#volts) ! 0)#numVolts) == (((battery#volts) ! 0)#numVolts)
-- Same as previous example, but get a different array index (so should be
-- false).
void $ prop "Example 2" $ forAll $
(((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4)
-- Update a struct field, then check it for equality.
void $ prop "Example 3" $ forAll $
((battery ## temp =$ (+1))#temp == (battery#temp + 1))
main :: IO ()
main = do
spec' <- reify spec
-- Use Z3 to prove the properties.
results <- prove Z3 spec'
-- Print the results.
forM_ results $ \(nm, res) -> do
putStr $ nm <> ": "
case res of
Valid -> putStrLn "valid"
Invalid -> putStrLn "invalid"
Unknown -> putStrLn "unknown"
|
