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) 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 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) 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. 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) 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: -- 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) 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..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,9 +373,15 @@ 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 + -- 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 (CS.propertyExpr pr) (AbsoluteOffset i) + xe <- translateExpr sym mempty prop (AbsoluteOffset i) case xe of XBool p -> return p _ -> expectedBool "Property" xe @@ -360,7 +389,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 +398,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 @@ -419,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 @@ -580,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 @@ -599,9 +636,12 @@ 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 + , 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 751310b5e..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,13 +268,41 @@ 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 = - Spec propStreams [] [] [Copilot.Property propName 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'. --