copilot-theorem: Add test cases for 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.

A prior commit has introduced a `proveWithCounterExample` function, which
provides a counterexample when a property is proven invalid.

This commit updates the test suite to ensure that basic uses of
`proveWithCounterExample` work as intended.

Author: RyanGlScott

copilot-theorem/copilot-theorem.cabal

@@ -121,6 +121,7 @@ test-suite unit-tests
 
   build-depends:
       base
+    , HUnit
     , QuickCheck
     , test-framework
     , test-framework-quickcheck2

copilot-theorem/tests/Test/Copilot/Theorem/What4.hs

@@ -10,22 +10,25 @@ import Data.Int                             (Int8)
 import Data.Word                            (Word32)
 import Test.Framework                       (Test, testGroup)
 import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.HUnit                           (assertFailure)
 import Test.QuickCheck                      (Arbitrary (arbitrary), Property,
                                              arbitrary, forAll)
 import Test.QuickCheck.Monadic              (monadicIO, run)
 
 -- External imports: Copilot
-import           Copilot.Core.Expr      (Expr (Const, Op1, Op2))
+import           Copilot.Core.Expr      (Expr (Const, Drop, Op1, Op2), Id)
 import           Copilot.Core.Operators (Op1 (..), Op2 (..))
-import           Copilot.Core.Spec      (Spec (..))
+import           Copilot.Core.Spec      (Spec (..), Stream (..))
 import qualified Copilot.Core.Spec      as Copilot
 import           Copilot.Core.Type      (Field (..),
                                          Struct (toValues, typeName),
                                          Type (Struct), Typed (typeOf),
                                          Value (..))
 
 -- Internal imports: Modules being tested
-import Copilot.Theorem.What4 (SatResult (..), Solver (..), prove)
+import Copilot.Theorem.What4 (CounterExample (..), SatResult (..),
+                              SatResultCex (..), Solver (..), prove,
+                              proveWithCounterExample)
 
 -- * Constants
 
@@ -37,6 +40,8 @@ tests =
     , testProperty "Prove via Z3 that false is invalid" testProveZ3False
     , testProperty "Prove via Z3 that x == x is valid"  testProveZ3EqConst
     , testProperty "Prove via Z3 that a struct update is valid" testProveZ3StructUpdate
+    , testProperty "Counterexample with invalid base case" testCounterExampleBaseCase
+    , testProperty "Counterexample with invalid induction step" testCounterExampleInductionStep
     ]
 
 -- * Individual tests
@@ -53,7 +58,7 @@ testProveZ3True =
     propName = "prop"
 
     spec :: Spec
-    spec = propSpec propName $ Const typeOf True
+    spec = propSpec propName [] $ Const typeOf True
 
 -- | Test that Z3 is able to prove the following expression invalid:
 -- @
@@ -67,7 +72,7 @@ testProveZ3False =
     propName = "prop"
 
     spec :: Spec
-    spec = propSpec propName $ Const typeOf False
+    spec = propSpec propName [] $ Const typeOf False
 
 -- | Test that Z3 is able to prove the following expresion valid:
 -- @
@@ -81,7 +86,7 @@ testProveZ3EqConst = forAll arbitrary $ \x ->
     propName = "prop"
 
     spec :: Int8 -> Spec
-    spec x = propSpec propName $
+    spec x = propSpec propName [] $
       Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)
 
 -- | Test that Z3 is able to prove the following expresion valid:
@@ -97,7 +102,7 @@ testProveZ3StructUpdate = forAll arbitrary $ \x ->
     propName = "prop"
 
     spec :: TestStruct -> Spec
-    spec s = propSpec propName $
+    spec s = propSpec propName [] $
       Op2
         (Eq typeOf)
         (getField
@@ -116,6 +121,70 @@ testProveZ3StructUpdate = forAll arbitrary $ \x ->
         add1 :: Expr Word32 -> Expr Word32
         add1 x = Op2 (Add typeOf) x (Const typeOf 1)
 
+-- | Test that Z3 is able to produce a counterexample to the following property,
+-- where the base case is proved invalid:
+--
+-- @
+--   let s :: Stream Bool
+--       s = [False] ++ constant True
+--   in forAll s
+-- @
+testCounterExampleBaseCase :: Property
+testCounterExampleBaseCase =
+    monadicIO $ run $
+      checkCounterExample Z3 propName spec $ \cex ->
+        pure $ not $ and $ baseCases cex
+  where
+    propName :: String
+    propName = "prop"
+
+    -- s = [False] ++ constant True
+    s :: Stream
+    s = Stream
+      { streamId       = sId
+      , streamBuffer   = [False]
+      , streamExpr     = Const typeOf True
+      , streamExprType = typeOf
+      }
+
+    sId :: Id
+    sId = 0
+
+    spec :: Spec
+    spec = propSpec propName [s] $ Drop typeOf 0 sId
+
+-- | Test that Z3 is able to produce a counterexample to the following property,
+-- where the induction step is proved invalid:
+--
+-- @
+--   let s :: Stream Bool
+--       s = [True] ++ constant False
+--   in forAll s
+-- @
+testCounterExampleInductionStep :: Property
+testCounterExampleInductionStep =
+    monadicIO $ run $
+      checkCounterExample Z3 propName spec $ \cex ->
+        pure $ not $ inductionStep cex
+  where
+    propName :: String
+    propName = "prop"
+
+    -- s = [True] ++ constant False
+    s :: Stream
+    s = Stream
+      { streamId       = sId
+      , streamBuffer   = [True]
+      , streamExpr     = Const typeOf False
+      , streamExprType = typeOf
+      }
+
+    sId :: Id
+    sId = 0
+
+    spec :: Spec
+    spec = propSpec propName [s] $ Drop typeOf 0 sId
+
 -- | A simple data type with a 'Struct' instance and a 'Field'. This is only
 -- used as part of 'testProveZ3StructUpdate'.
 newtype TestStruct = TestStruct { testField :: Field "testField" Word32 }
@@ -145,12 +214,44 @@ checkResult solver propName spec expectation = do
   -- does not exist in the results, in which case the lookup returns 'Nothing'.
   return $ propResult == Just expectation
 
+-- | Check that the solver produces an invalid result for the given property and
+-- that the resulting 'CounterExample' satifies the given predicate.
+checkCounterExample :: Solver
+                    -> String
+                    -> Spec
+                    -> (CounterExample -> IO Bool)
+                    -> IO Bool
+checkCounterExample solver propName spec cexPred = do
+  results <- proveWithCounterExample solver spec
+
+  -- Find the satisfiability result for propName. If the property name does not
+  -- exist in the results, raise an assertion failure.
+  propResult <-
+    case lookup propName results of
+      Just propResult ->
+        pure propResult
+      Nothing ->
+        assertFailure $
+          "Could not find property in results: " ++ propName
+
+  -- Assert that the solver returned an invalid result and pass the
+  -- counterexample to the predicate. If the result is anything other than
+  -- invalid, raise an assertion failure.
+  case propResult of
+    InvalidCex cex ->
+      cexPred cex
+    ValidCex {} ->
+      assertFailure "Expected invalid result, but result was valid"
+    UnknownCex {} ->
+      assertFailure "Expected invalid result, but result was unknown"
+
 -- * Auxiliary
 
--- | Build a 'Spec' that contains one property with the given name and defined
--- by the given boolean expression.
-propSpec :: String -> Expr Bool -> Spec
-propSpec propName propExpr = Spec [] [] [] [Copilot.Property propName propExpr]
+-- | Build a 'Spec' that contains one property with the given name, which
+-- contains the given streams, and is defined by the given boolean expression.
+propSpec :: String -> [Stream] -> Expr Bool -> Spec
+propSpec propName propStreams propExpr =
+  Spec propStreams [] [] [Copilot.Property propName propExpr]
 
 -- | Equality for 'SatResult'.
 --