Add example demonstrating array update support. Fixes #63.

This is adapted from a similar example in the upstream `copilot` repo.

copilot-verifier/copilot-verifier.cabal

@@ -116,6 +116,7 @@ library copilot-verifier-examples
     Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge
     Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
     Copilot.Verifier.Examples.ShouldPass.Structs
+    Copilot.Verifier.Examples.ShouldPass.UpdateArray
     Copilot.Verifier.Examples.ShouldPass.Voting
     Copilot.Verifier.Examples.ShouldPass.WCV
 

copilot-verifier/examples/Copilot/Verifier/Examples.hs

@@ -41,6 +41,7 @@ import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge   a
 import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge   as Pass.ShiftRTooLarge
 import qualified Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap    as Pass.SubSignedWrap
 import qualified Copilot.Verifier.Examples.ShouldPass.Structs                  as Structs
+import qualified Copilot.Verifier.Examples.ShouldPass.UpdateArray              as UpdateArray
 import qualified Copilot.Verifier.Examples.ShouldPass.Voting                   as Voting
 import qualified Copilot.Verifier.Examples.ShouldPass.WCV                      as WCV
 
@@ -72,6 +73,7 @@ shouldPassExamples verb = Map.fromList
     , example "Heater" (Heater.verifySpec verb)
     , example "IntOps" (IntOps.verifySpec verb)
     , example "Structs" (Structs.verifySpec verb)
+    , example "UpdateArray" (UpdateArray.verifySpec verb)
     , example "Voting" (Voting.verifySpec verb)
     , example "WCV" (WCV.verifySpec verb)
 

copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/UpdateArray.hs

@@ -0,0 +1,32 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds        #-}
+
+-- | An example showing of using @copilot-verifier@ to verify a specification
+-- involving arrays where individual elements are updated.
+module Copilot.Verifier.Examples.ShouldPass.UpdateArray where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let pair :: Stream (Array 2 Word32)
+      pair = extern "pair" Nothing
+
+  -- Check equality, indexing into array and modifying the value. Note that
+  -- this is trivial by equality.
+  trigger "trig_1"
+    (((pair !! 0 =$ (+1)) ! 0) == ((pair ! 0) + 1))
+    [arg pair]
+
+  -- Same as previous example, but get a different array index (so should be
+  -- false).
+  trigger "trig_2"
+    (((pair !! 0 =$ (+1)) ! 1) == ((pair ! 0) + 1))
+    [arg pair]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "updateArray"