copilot-theorem: Reject existentially quantified propositions in What4 backend. Refs #254.

The functions in `Copilot.Theorem.What4` (e.g., `prove`) take a proposition and
attempt to prove that it is valid at all possible time steps. Currently, these
functions do this regardless of whether the proposition is universally
quantified or existentially quantified, which is unsound. The reason that this
happens is because the functions call `extractProp` on the proposition being
proven, causing the proposition's quantifier not to be taken into account.

This commit removes the unsound uses of `extractProp` and instead checks if the
proposition was actually quantified universally (i.e., with a `Forall`), which
is the intended use case for `Copilot.Theorem.What4`. If the proposition was
instead quantified existentially (i.e., with an `Exists`), then a
`ProveException` will be thrown. Warnings have been added to Haddocks of the
relevant functions that can potentially throw a `ProveException`.

Author: RyanGlScott

copilot-theorem/src/Copilot/Theorem/What4.hs

@@ -32,6 +32,12 @@
 -- We perform @k@-induction on all the properties in a given specification where
 -- @k@ is chosen to be the maximum amount of delay on any of the involved
 -- streams. This is a heuristic choice, but often effective.
+--
+-- The functions in this module are only designed to prove universally
+-- quantified propositions (i.e., propositions that use @forAll@). Attempting to
+-- prove an existentially quantified proposition (i.e., propositions that use
+-- @exists@) will cause a 'UnexpectedExistentialProposition' exception to be
+-- thrown.
 module Copilot.Theorem.What4
   ( -- * Proving properties about Copilot specifications
     prove
@@ -40,6 +46,7 @@ module Copilot.Theorem.What4
   , proveWithCounterExample
   , SatResultCex(..)
   , CounterExample(..)
+  , ProveException(..)
     -- * Bisimulation proofs about @copilot-c99@ code
   , computeBisimulationProofBundle
   , BisimulationProofBundle(..)
@@ -63,6 +70,7 @@ import qualified What4.InterpretedFloatingPoint as WFP
 import qualified What4.Solver                   as WS
 import qualified What4.Solver.DReal             as WS
 
+import Control.Exception (Exception, throw)
 import Control.Monad (forM)
 import Control.Monad.State
 import qualified Data.BitVector.Sized as BV
@@ -257,9 +265,24 @@ data CounterExample = CounterExample
     }
   deriving Show
 
+-- | Exceptions that can arise when attempting a proof.
+data ProveException
+  = UnexpectedExistentialProposition
+    -- ^ The functions in "Copilot.Theorem.What4" can only prove properties with
+    -- universally quantified propositions. The functions in
+    -- "Copilot.Theorem.What4" will throw this exception if they encounter an
+    -- existentially quantified proposition.
+  deriving Show
+
+instance Exception ProveException
+
 -- | Attempt to prove all of the properties in a spec via an SMT solver (which
 -- must be installed locally on the host). Return an association list mapping
 -- the names of each property to the result returned by the solver.
+--
+-- PRE: All of the properties in the 'CS.Spec' use universally quantified
+-- propositions. Attempting to supply an existentially quantified proposition
+-- will cause a 'UnexpectedExistentialProposition' exception to be thrown.
 prove :: Solver
       -- ^ Solver to use
       -> CS.Spec
@@ -350,7 +373,12 @@ proveInternal solver spec k = do
   -- This process performs k-induction where we use @k = maxBufLen@.
   -- The choice for @k@ is heuristic, but often effective.
   let proveProperties = forM (CS.specProperties spec) $ \pr -> do
-        let prop = CS.extractProp (CS.propertyProp pr)
+        -- This function only supports universally quantified propositions, so
+        -- throw an exception if we encounter an existentially quantified
+        -- proposition.
+        let prop = case CS.propertyProp pr of
+                     CS.Forall p  -> p
+                     CS.Exists {} -> throw UnexpectedExistentialProposition
         -- State the base cases for k induction.
         base_cases <- forM [0 .. maxBufLen - 1] $ \i -> do
           xe <- translateExpr sym mempty prop (AbsoluteOffset i)
@@ -420,6 +448,10 @@ proveInternal solver spec k = do
 -- to carry out a bisimulation proof that establishes a correspondence between
 -- the states of the Copilot stream program and the C code that @copilot-c99@
 -- would generate for that Copilot program.
+--
+-- PRE: All of the properties in the 'CS.Spec' use universally quantified
+-- propositions. Attempting to supply an existentially quantified proposition
+-- will cause a 'UnexpectedExistentialProposition' exception to be thrown.
 computeBisimulationProofBundle ::
      WFP.IsInterpretedFloatSymExprBuilder sym
   => sym
@@ -581,6 +613,10 @@ computeExternalInputs sym = do
     return (nm, Some tp, v)
 
 -- | Compute the user-provided property assumptions in a Copilot program.
+--
+-- PRE: All of the properties in the 'CS.Spec' use universally quantified
+-- propositions. Attempting to supply an existentially quantified proposition
+-- will cause a 'UnexpectedExistentialProposition' exception to be thrown.
 computeAssumptions ::
      forall sym.
      WFP.IsInterpretedFloatSymExprBuilder sym
@@ -603,6 +639,9 @@ computeAssumptions sym properties spec =
       [ CS.extractProp (CS.propertyProp p)
       | p <- CS.specProperties spec
       , elem (CS.propertyName p) properties
+      , let prop = case CS.propertyProp p of
+                     CS.Forall pr -> pr
+                     CS.Exists {} -> throw UnexpectedExistentialProposition
       ]
 
     -- Compute all of the what4 predicates corresponding to each user-provided

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

@@ -1,16 +1,22 @@
-{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
 -- The following warning is disabled due to a necessary instance of SatResult
 -- defined in this module.
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 -- | Test copilot-theorem:Copilot.Theorem.What4.
 module Test.Copilot.Theorem.What4 where
 
 -- External imports
+import Control.Exception                    (Exception, try)
 import Data.Int                             (Int8)
+import Data.Proxy                           (Proxy (..))
+import Data.Typeable                        (typeRep)
 import Data.Word                            (Word32)
 import Test.Framework                       (Test, testGroup)
 import Test.Framework.Providers.QuickCheck2 (testProperty)
-import Test.HUnit                           (assertFailure)
+import Test.HUnit                           (Assertion, assertBool,
+                                             assertFailure)
 import Test.QuickCheck                      (Arbitrary (arbitrary), Property,
                                              arbitrary, forAll)
 import Test.QuickCheck.Monadic              (monadicIO, run)
@@ -26,9 +32,9 @@ import           Copilot.Core.Type      (Field (..),
                                          Value (..))
 
 -- Internal imports: Modules being tested
-import Copilot.Theorem.What4 (CounterExample (..), SatResult (..),
-                              SatResultCex (..), Solver (..), prove,
-                              proveWithCounterExample)
+import Copilot.Theorem.What4 (CounterExample (..), ProveException (..),
+                              SatResult (..), SatResultCex (..), Solver (..),
+                              prove, proveWithCounterExample)
 
 -- * Constants
 
@@ -42,6 +48,7 @@ tests =
     , 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
+    , testProperty "Check that the What4 backend rejects existential quantification" testWhat4ExistsException
     ]
 
 -- * Individual tests
@@ -58,7 +65,7 @@ testProveZ3True =
     propName = "prop"
 
     spec :: Spec
-    spec = propSpec propName [] $ Const typeOf True
+    spec = forallPropSpec propName [] $ Const typeOf True
 
 -- | Test that Z3 is able to prove the following expression invalid:
 -- @
@@ -72,7 +79,7 @@ testProveZ3False =
     propName = "prop"
 
     spec :: Spec
-    spec = propSpec propName [] $ Const typeOf False
+    spec = forallPropSpec propName [] $ Const typeOf False
 
 -- | Test that Z3 is able to prove the following expresion valid:
 -- @
@@ -86,7 +93,7 @@ testProveZ3EqConst = forAll arbitrary $ \x ->
     propName = "prop"
 
     spec :: Int8 -> Spec
-    spec x = propSpec propName [] $
+    spec x = forallPropSpec propName [] $
       Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)
 
 -- | Test that Z3 is able to prove the following expresion valid:
@@ -102,7 +109,7 @@ testProveZ3StructUpdate = forAll arbitrary $ \x ->
     propName = "prop"
 
     spec :: TestStruct -> Spec
-    spec s = propSpec propName [] $
+    spec s = forallPropSpec propName [] $
       Op2
         (Eq typeOf)
         (getField
@@ -151,7 +158,7 @@ testCounterExampleBaseCase =
     sId = 0
 
     spec :: Spec
-    spec = propSpec propName [s] $ Drop typeOf 0 sId
+    spec = forallPropSpec 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:
@@ -183,7 +190,23 @@ testCounterExampleInductionStep =
     sId = 0
 
     spec :: Spec
-    spec = propSpec propName [s] $ Drop typeOf 0 sId
+    spec = forallPropSpec propName [s] $ Drop typeOf 0 sId
+
+-- | Test that @copilot-theorem@'s @what4@ backend will throw an exception if it
+-- attempts to prove an existentially quantified proposition.
+testWhat4ExistsException :: Property
+testWhat4ExistsException =
+    monadicIO $ run $
+      checkException (prove Z3 spec) isUnexpectedExistentialProposition
+  where
+    isUnexpectedExistentialProposition :: ProveException -> Bool
+    isUnexpectedExistentialProposition UnexpectedExistentialProposition = True
+
+    propName :: String
+    propName = "prop"
+
+    spec :: Spec
+    spec = existsPropSpec propName [] $ Const typeOf True
 
 -- | A simple data type with a 'Struct' instance and a 'Field'. This is only
 -- used as part of 'testProveZ3StructUpdate'.
@@ -245,14 +268,42 @@ checkCounterExample solver propName spec cexPred = do
     UnknownCex {} ->
       assertFailure "Expected invalid result, but result was unknown"
 
+-- | Check that the given 'IO' action throws a particular exception. This is
+-- largely taken from the implementation of @shouldThrow@ in
+-- @hspec-expectations@ (note that this test suite uses @test-framework@ instead
+-- of @hspec@).
+checkException :: forall e a. Exception e => IO a -> (e -> Bool) -> Assertion
+checkException action p = do
+    r <- try action
+    case r of
+      Right _ ->
+        assertFailure $
+          "did not get expected exception: " ++ exceptionType
+      Left e ->
+        assertBool
+          ("predicate failed on expected exception: " ++ exceptionType ++
+           "\n" ++ show e)
+          (p e)
+  where
+    -- String representation of the expected exception's type
+    exceptionType = show $ typeRep $ Proxy @e
+
 -- * Auxiliary
 
 -- | 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 =
+-- contains the given streams, and is defined by the given boolean expression,
+-- which is universally quantified.
+forallPropSpec :: String -> [Stream] -> Expr Bool -> Spec
+forallPropSpec propName propStreams propExpr =
   Spec propStreams [] [] [Copilot.Property propName (Copilot.Forall 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,
+-- which is existentially quantified.
+existsPropSpec :: String -> [Stream] -> Expr Bool -> Spec
+existsPropSpec propName propStreams propExpr =
+  Spec propStreams [] [] [Copilot.Property propName (Copilot.Exists propExpr)]
+
 -- | Equality for 'SatResult'.
 --
 -- This is an orphan instance, so we suppress the warning that GHC would