copilot: Add example of how to use proveWithCounterExample. Refs #589.

Currently, the `Copilot.Theorem.What4.prove` function returns a list of
results, where each result contains a `SatResult` that describes whether a
property is `Valid`, `Invalid`, or `Unknown`. The `Invalid` result has the
limitation that it does not give any information about a specific
counterexample that could drive Copilot into falsifying the property, however.
This makes it challenging to interpret what the results of prove mean.

To demonstrate how to effectively use the newly added `proveWithCounterExample`
function, this commit adds a new `examples/what4/ArithmeticCounterExamples.hs`
function that behaves like `examples/what4/Arithmetic.hs`, but using
`proveWithCounterExamples` instead of `prove`.

Author: RyanGlScott

copilot/copilot.cabal

@@ -86,6 +86,19 @@ executable what4-arithmetic
     else
       buildable: False
 
+executable what4-arithmetic-counterexamples
+    main-is:                ArithmeticCounterExamples.hs
+    hs-source-dirs:         examples/what4
+    build-depends:          base
+                          , containers
+                          , copilot
+                          , copilot-theorem
+    default-language:       Haskell2010
+    if flag(examples)
+      buildable: True
+    else
+      buildable: False
+
 executable what4-structs
     main-is:                Structs.hs
     hs-source-dirs:         examples/what4

copilot/examples/what4/ArithmeticCounterExamples.hs

@@ -0,0 +1,110 @@
+-- | An example showing the usage of the What4 backend in copilot-theorem for
+-- simple arithmetic. This example uses the 'proveWithCounterExamples' function
+-- to demonstrate counterexamples in the event of invalid properties.
+
+module Main where
+
+import qualified Prelude as P
+import Control.Monad (void, forM_)
+import qualified Data.Map as Map
+
+import Language.Copilot
+import Copilot.Theorem.What4
+
+spec :: Spec
+spec = do
+  -- Define some external streams. Their values are not important, so external
+  -- streams suffice.
+  let eint8  :: Stream Int8
+      eint8  = extern "eint8" Nothing
+      eword8 :: Stream Word8
+      eword8 = extern "eword8" Nothing
+      efloat :: Stream Float
+      efloat = extern "efloat" Nothing
+
+  -- The simplest example involving numbers: equality on constant values.
+  void $ prop "Example 1" (forAll ((constant (1 :: Int8)) == (constant 1)))
+
+  -- Testing "a < a + 1". This should fail, because it isn't true.
+  void $ prop "Example 2" (forAll (eint8 < (eint8 + 1)))
+
+  -- Adding another condition to the above property to make it true.
+  void $ prop "Example 3" (forAll ((eint8 < (eint8 + 1)) || (eint8 == 127)))
+
+  -- Just like the previous example, but with words.
+  void $ prop "Example 4" (forAll ((eword8 < (eword8 + 1)) || (eword8 == 255)))
+
+  -- An example with floats.
+  void $ prop "Example 5" (forAll ((2 * efloat) == (efloat + efloat)))
+
+  -- Another example with floats. This fails, because it isn't true.
+  void $ prop "Example 6" (forAll ((efloat + 1) /= efloat))
+
+main :: IO ()
+main = do
+  spec' <- reify spec
+
+  -- Use Z3 to prove the properties.
+  results <- proveWithCounterExample Z3 spec'
+
+  -- Print the results.
+  forM_ results $ \(nm, res) -> do
+    putStr $ nm <> ": "
+    case res of
+      ValidCex -> putStrLn "valid"
+      InvalidCex cex -> do
+        putStrLn "invalid"
+        putStrLn $ ppCounterExample cex
+      UnknownCex -> putStrLn "unknown"
+
+-- | Pretty-print a counterexample for user display.
+ppCounterExample :: CounterExample -> String
+ppCounterExample cex
+    | any P.not (baseCases cex)
+    = if Map.null baseCaseVals
+        then
+          "  All possible extern values during the base case(s) " P.++
+          "constitute a counterexample."
+        else
+          unlines $
+            "  The base cases failed with the following extern values:" :
+            map
+              (\((name, _), val) -> "    " P.++ name P.++ ": " P.++ show val)
+              (Map.toList baseCaseVals)
+
+    | P.not (inductionStep cex)
+    = if Map.null inductionStepVals
+        then
+          "  All possible extern values during the induction step " P.++
+          "constitute a counterexample."
+        else
+          unlines $
+            "  The induction step failed with the following extern values:" :
+            map
+              (\((name, _), val) -> "    " P.++ name P.++ ": " P.++ show val)
+              (Map.toList inductionStepVals)
+
+    | otherwise
+    = error $
+        "ppCounterExample: " P.++
+        "Counterexample without failing base cases or induction step"
+  where
+    allExternVals = concreteExternValues cex
+
+    baseCaseVals =
+      Map.filterWithKey
+        (\(_, offset) _ ->
+          case offset of
+            AbsoluteOffset {} -> True
+            RelativeOffset {} -> False
+        )
+        allExternVals
+
+    inductionStepVals =
+      Map.filterWithKey
+        (\(_, offset) _ ->
+          case offset of
+            AbsoluteOffset {} -> False
+            RelativeOffset {} -> True
+        )
+        allExternVals