From 5b08e817fb6d23485bc86553a820135896fc54b1 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 5 Mar 2025 16:59:35 -0500 Subject: [PATCH 1/9] copilot-core: Preserve proposition quantifiers. Refs Copilot-Language#254. Currently, `copilot-language` remembers whether a proposition (i.e., a stream of booleans) is quantified universally (i.e., using `forAll`) or existentially (i.e., using `exists`). When translating from `copilot-language` to `copilot-core`, however, the quantifier is discarded. This means that a `copilot-core` `Property` does not record any quantifier information at all, making it impossible for downstream libraries that use `copilot-core` to handle universal quantification differently from existential quantification. This commit changes the `copilot-core` API to preserve quantifier information. Specifically, it introduces a `Prop` data type in `copilot-core` (largely inspired by a data type of the same name in `copilot-language`) to record a proposition's quantifier, and it changes the `propertyExpr :: Expr Bool` field of `copilot-core`'s `Property` data type to `propertyProp :: Prop`. This commit also introduces an `extractProp :: Prop -> Expr Bool` function for retrieving the underlying boolean expression. Generally, this function should not be used, as different quantifiers usually require different treatment, and misuse of the `extractProp` function can potentially lead to unsoundness. There are a handful of places where the use of `extractProp` is justified, however. In each such place, a comment should be left to justify why the use of `extractProp` is sound. --- copilot-core/src/Copilot/Core/Spec.hs | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/copilot-core/src/Copilot/Core/Spec.hs b/copilot-core/src/Copilot/Core/Spec.hs index 7a71c780e..6614d0621 100644 --- a/copilot-core/src/Copilot/Core/Spec.hs +++ b/copilot-core/src/Copilot/Core/Spec.hs @@ -20,6 +20,8 @@ module Copilot.Core.Spec , Trigger (..) , Spec (..) , Property (..) + , Prop (..) + , extractProp ) where @@ -62,9 +64,26 @@ data Trigger = Trigger -- universally quantified over time. data Property = Property { propertyName :: Name - , propertyExpr :: Expr Bool + , propertyProp :: Prop } +-- | A proposition, representing a boolean stream that is existentially or +-- universally quantified over time. +data Prop + = Forall (Expr Bool) + | Exists (Expr Bool) + +-- | Extract the underlying stream from a quantified proposition. +-- +-- Think carefully before using this function, as this function will remove the +-- quantifier from a proposition. Universally quantified streams usually require +-- separate treatment from existentially quantified ones, so carelessly using +-- this function to remove quantifiers can result in hard-to-spot soundness +-- bugs. +extractProp :: Prop -> Expr Bool +extractProp (Forall e) = e +extractProp (Exists e) = e + -- | A Copilot specification is a list of streams, together with monitors on -- these streams implemented as observers, triggers or properties. data Spec = Spec From 0c3e7021d395563aa9ce10d7daab0dca5505689e Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 5 Mar 2025 17:03:18 -0500 Subject: [PATCH 2/9] copilot-language: Preserve proposition quantifiers. Refs Copilot-Language#254. Currently, `copilot-language` remembers whether a proposition (i.e., a stream of booleans) is quantified universally (i.e., using `forAll`) or existentially (i.e., using `exists`). When translating from `copilot-language` to `copilot-core`, however, the quantifier is discarded. This means that a `copilot-core` `Property` does not record any quantifier information at all, making it impossible for downstream libraries that use `copilot-core` to handle universal quantification differently from existential quantification. Now that `copilot-core` preserves quantifier information in its API, this commit updates `copilot-language` to respect quantifiers when translating into `copilot-core`. --- .../src/Copilot/Language/Analyze.hs | 13 +++++++++++-- copilot-language/src/Copilot/Language/Reify.hs | 18 +++++++++++++++--- copilot-language/src/Copilot/Language/Spec.hs | 12 +++++++++--- 3 files changed, 35 insertions(+), 8 deletions(-) diff --git a/copilot-language/src/Copilot/Language/Analyze.hs b/copilot-language/src/Copilot/Language/Analyze.hs index 04de14ed4..e7065f7b4 100644 --- a/copilot-language/src/Copilot/Language/Analyze.hs +++ b/copilot-language/src/Copilot/Language/Analyze.hs @@ -110,7 +110,11 @@ analyzeObserver refStreams (Observer _ e) = analyzeExpr refStreams e -- -- This function can fail with one of the exceptions in 'AnalyzeException'. analyzeProperty :: IORef Env -> Property -> IO () -analyzeProperty refStreams (Property _ e) = analyzeExpr refStreams e +analyzeProperty refStreams (Property _ p) = + -- Soundness note: it is OK to call `extractProp` here to drop the quantifier + -- from the proposition `p`, as the analysis does not depend on what the + -- quantifier is. + analyzeExpr refStreams (extractProp p) data SeenExtern = NoExtern | SeenFun @@ -291,7 +295,12 @@ specExts refStreams spec = do env' args propertyExts :: ExternEnv -> Property -> IO ExternEnv - propertyExts env (Property _ stream) = collectExts refStreams stream env + propertyExts env (Property _ p) = + -- Soundness note: it is OK to call `extractProp` here to drop the + -- quantifier from the proposition `p`. This is because we are simply + -- gathering externs from `p`, and the presence of externs does not depend + -- on what the quantifier is. + collectExts refStreams (extractProp p) env theoremExts :: ExternEnv -> (Property, UProof) -> IO ExternEnv theoremExts env (p, _) = propertyExts env p diff --git a/copilot-language/src/Copilot/Language/Reify.hs b/copilot-language/src/Copilot/Language/Reify.hs index 092458b78..60bae450b 100644 --- a/copilot-language/src/Copilot/Language/Reify.hs +++ b/copilot-language/src/Copilot/Language/Reify.hs @@ -4,6 +4,7 @@ -- specification. {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE Safe #-} @@ -105,11 +106,22 @@ mkProperty -> IORef [Core.Stream] -> Property -> IO Core.Property -mkProperty refMkId refStreams refMap (Property name guard) = do - w1 <- mkExpr refMkId refStreams refMap guard +mkProperty refMkId refStreams refMap (Property name p) = do + p' <- mkProp refMkId refStreams refMap p return Core.Property { Core.propertyName = name - , Core.propertyExpr = w1 } + , Core.propertyProp = p' } + +-- | Transform a Copilot proposition into a Copilot Core proposition. +mkProp :: IORef Int + -> IORef (Map Core.Id) + -> IORef [Core.Stream] + -> Prop a + -> IO Core.Prop +mkProp refMkId refStreams refMap prop = + case prop of + Forall e -> Core.Forall <$> mkExpr refMkId refStreams refMap e + Exists e -> Core.Exists <$> mkExpr refMkId refStreams refMap e -- | Transform a Copilot stream expression into a Copilot Core expression. {-# INLINE mkExpr #-} diff --git a/copilot-language/src/Copilot/Language/Spec.hs b/copilot-language/src/Copilot/Language/Spec.hs index b5fc94b61..0127cd24b 100644 --- a/copilot-language/src/Copilot/Language/Spec.hs +++ b/copilot-language/src/Copilot/Language/Spec.hs @@ -153,7 +153,7 @@ trigger name e args = tell [TriggerItem $ Trigger name e args] -- | A property, representing a boolean stream that is existentially or -- universally quantified over time. data Property where - Property :: String -> Stream Bool -> Property + Property :: String -> Prop a -> Property -- | A proposition, representing the quantification of a boolean streams over -- time. @@ -170,6 +170,12 @@ exists :: Stream Bool -> Prop Existential exists = Exists -- | Extract the underlying stream from a quantified proposition. +-- +-- Think carefully before using this function, as this function will remove the +-- quantifier from a proposition. Universally quantified streams usually require +-- separate treatment from existentially quantified ones, so carelessly using +-- this function to remove quantifiers can result in hard-to-spot soundness +-- bugs. extractProp :: Prop a -> Stream Bool extractProp (Forall p) = p extractProp (Exists p) = p @@ -180,7 +186,7 @@ extractProp (Exists p) = p -- This function returns, in the monadic context, a reference to the -- proposition. prop :: String -> Prop a -> Writer [SpecItem] (PropRef a) -prop name e = tell [PropertyItem $ Property name (extractProp e)] +prop name e = tell [PropertyItem $ Property name e] >> return (PropRef name) -- | A theorem, or proposition together with a proof. @@ -188,7 +194,7 @@ prop name e = tell [PropertyItem $ Property name (extractProp e)] -- This function returns, in the monadic context, a reference to the -- proposition. theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a) -theorem name e (Proof p) = tell [TheoremItem (Property name (extractProp e), p)] +theorem name e (Proof p) = tell [TheoremItem (Property name e, p)] >> return (PropRef name) -- | Construct a function argument from a stream. From 8e46a139b96da91ffd4e078af3c1526e6230467c Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 5 Mar 2025 17:06:14 -0500 Subject: [PATCH 3/9] copilot-prettyprinter: Preserve proposition quantifiers. Refs Copilot-Language#254. Currently, `copilot-language` remembers whether a proposition (i.e., a stream of booleans) is quantified universally (i.e., using `forAll`) or existentially (i.e., using `exists`). When translating from `copilot-language` to `copilot-core`, however, the quantifier is discarded. This means that a `copilot-core` `Property` does not record any quantifier information at all, making it impossible for downstream libraries that use `copilot-core` to handle universal quantification differently from existential quantification. Now that `copilot-core` preserves quantifier information in its API, this commit updates `copilot-prettyprinter` to pretty-print quantifier information appropriately. --- copilot-prettyprinter/src/Copilot/PrettyPrint.hs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/copilot-prettyprinter/src/Copilot/PrettyPrint.hs b/copilot-prettyprinter/src/Copilot/PrettyPrint.hs index 50be4466f..4bbad626b 100644 --- a/copilot-prettyprinter/src/Copilot/PrettyPrint.hs +++ b/copilot-prettyprinter/src/Copilot/PrettyPrint.hs @@ -175,10 +175,15 @@ ppProperty :: Property -> Doc ppProperty Property { propertyName = name - , propertyExpr = e } + , propertyProp = p } = text "property \"" <> text name <> text "\"" <+> text "=" - <+> ppExpr e + <+> ppProp p + +-- | Pretty-print a Copilot proposition. +ppProp :: Prop -> Doc +ppProp (Forall e) = text "forall" <+> parens (ppExpr e) +ppProp (Exists e) = text "exists" <+> parens (ppExpr e) -- | Pretty-print a Copilot specification, in the following order: -- From bce4c104862757b229dc931b1a35e477b64d3a39 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 5 Mar 2025 17:07:58 -0500 Subject: [PATCH 4/9] copilot-theorem: Preserve proposition quantifiers. Refs Copilot-Language#254. Currently, `copilot-language` remembers whether a proposition (i.e., a stream of booleans) is quantified universally (i.e., using `forAll`) or existentially (i.e., using `exists`). When translating from `copilot-language` to `copilot-core`, however, the quantifier is discarded. This means that a `copilot-core` `Property` does not record any quantifier information at all, making it impossible for downstream libraries that use `copilot-core` to handle universal quantification differently from existential quantification. Now that `copilot-core` preserves quantifier information in its API, this commit updates `copilot-theorem` to make use of quantifier information when proving theorems. --- copilot-theorem/src/Copilot/Theorem/IL/Translate.hs | 9 +++++++-- .../src/Copilot/Theorem/TransSys/Translate.hs | 2 +- copilot-theorem/src/Copilot/Theorem/What4.hs | 9 +++++---- copilot-theorem/tests/Test/Copilot/Theorem/What4.hs | 2 +- 4 files changed, 14 insertions(+), 8 deletions(-) diff --git a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs index 0bb6bfa37..c1a6606ba 100644 --- a/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/IL/Translate.hs @@ -63,8 +63,13 @@ translate' b (C.Spec {C.specStreams, C.specProperties}) = runTrans b $ do localConstraints <- popLocalConstraints properties <- Map.fromList <$> forM specProperties - (\(C.Property {C.propertyName, C.propertyExpr}) -> do - e' <- expr propertyExpr + (\(C.Property {C.propertyName, C.propertyProp}) -> do + -- Soundness note: it is OK to call `extractProp` here to drop the + -- quantifier from the proposition `propertyProp`. This is because we + -- IL translation always occurs within the context of a function that + -- returns a `Proof`, and these `Proof` functions are always careful to + -- use `Prover`s that respect the propositions's quantifier. + e' <- expr (C.extractProp propertyProp) propConds <- popLocalConstraints return (propertyName, (propConds, e'))) diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs index cc557e429..68ddb8806 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs @@ -139,7 +139,7 @@ streamOfProp :: C.Property -> C.Stream streamOfProp prop = C.Stream { C.streamId = 42 , C.streamBuffer = [] - , C.streamExpr = C.propertyExpr prop + , C.streamExpr = C.extractProp (C.propertyProp prop) , C.streamExprType = C.Bool } stream :: C.Stream -> Trans Node diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs index eb692378f..3cf43861d 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4.hs @@ -350,9 +350,10 @@ 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) -- State the base cases for k induction. base_cases <- forM [0 .. maxBufLen - 1] $ \i -> do - xe <- translateExpr sym mempty (CS.propertyExpr pr) (AbsoluteOffset i) + xe <- translateExpr sym mempty prop (AbsoluteOffset i) case xe of XBool p -> return p _ -> expectedBool "Property" xe @@ -360,7 +361,7 @@ proveInternal solver spec k = do -- Translate the induction hypothesis for all values up to maxBufLen in -- the past ind_hyps <- forM [0 .. maxBufLen-1] $ \i -> do - xe <- translateExpr sym mempty (CS.propertyExpr pr) (RelativeOffset i) + xe <- translateExpr sym mempty prop (RelativeOffset i) case xe of XBool hyp -> return hyp _ -> expectedBool "Property" xe @@ -369,7 +370,7 @@ proveInternal solver spec k = do ind_goal <- do xe <- translateExpr sym mempty - (CS.propertyExpr pr) + prop (RelativeOffset maxBufLen) case xe of XBool p -> return p @@ -599,7 +600,7 @@ computeAssumptions sym properties spec = -- user-provided property assumptions. specPropertyExprs :: [CE.Expr Bool] specPropertyExprs = - [ CS.propertyExpr p + [ CS.extractProp (CS.propertyProp p) | p <- CS.specProperties spec , elem (CS.propertyName p) properties ] diff --git a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs b/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs index 751310b5e..03e6b8dad 100644 --- a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs +++ b/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs @@ -251,7 +251,7 @@ checkCounterExample solver propName spec cexPred = do -- 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] + Spec propStreams [] [] [Copilot.Property propName (Copilot.Forall propExpr)] -- | Equality for 'SatResult'. -- From d1392428abc45c5b42017cf494f31b50da2abf66 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 4 Feb 2025 08:03:05 -0500 Subject: [PATCH 5/9] 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`. --- copilot-theorem/src/Copilot/Theorem/What4.hs | 41 +++++++++- .../tests/Test/Copilot/Theorem/What4.hs | 79 +++++++++++++++---- 2 files changed, 105 insertions(+), 15 deletions(-) diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs index 3cf43861d..818ac9b3a 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/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 diff --git a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs b/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs index 03e6b8dad..edd137700 100644 --- a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs +++ b/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs @@ -1,4 +1,6 @@ -{-# 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 #-} @@ -6,11 +8,15 @@ 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 From 3ea5f1206c608528fbfca44e527d888eba7036e6 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 4 Feb 2025 13:33:55 -0500 Subject: [PATCH 6/9] copilot-core: Document changes in CHANGELOG. Refs #254. --- copilot-core/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 69de85d76..dc86d9739 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,6 +1,7 @@ -2025-02-24 +2025-02-28 * Fix typo in documentation. (#587) * Add a Show instance for Type. (#589) + * Add a Prop type to capture how a property is quantified. (#254) 2025-01-07 * Version bump (4.2). (#577) From b4664cd1d1b2a90ff2ed3ff5a91793aaa048f096 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 4 Feb 2025 13:36:14 -0500 Subject: [PATCH 7/9] copilot-language: Document changes in CHANGELOG. Refs #254. --- copilot-language/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index f4668a9e1..2aa4f6008 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,5 +1,6 @@ -2025-01-28 +2025-02-28 * Fix typo in documentation. (#587) + * Record how a Property's underlying proposition is quantified. (#254) 2025-01-07 * Version bump (4.2). (#577) From 88a67f5eb876b25cbc440e5810247d5df7f4352c Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 4 Feb 2025 13:37:42 -0500 Subject: [PATCH 8/9] copilot-prettyprinter: Document changes in CHANGELOG. Refs #254. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index b51261ae8..f930b53d0 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2025-02-28 + * Update pretty-printing to handle Props. (#254) + 2025-01-07 * Version bump (4.2). (#577) * Remove uses of Copilot.Core.Expr.UExpr.uExprExpr. (#565) From 700508abfcefea5c59517e0bdc3087735fdaa692 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 4 Feb 2025 13:42:29 -0500 Subject: [PATCH 9/9] copilot-theorem: Document changes in CHANGELOG. Refs #254. --- copilot-theorem/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index f503de4e0..1c76ef96a 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,7 +1,8 @@ -2025-02-24 +2025-02-28 * Fix multiple typos in README. (#560) * Fix typo in documentation. (#587) * Add function to produce counterexamples for invalid properties. (#589) + * Reject existentially quantified properties in What4 backend. (#254) 2025-01-07 * Version bump (4.2). (#577)