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

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)

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

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)

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

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 #-}

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,15 +186,15 @@ 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.
 --
 -- 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.

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)

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:
 --

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)

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')))
 

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

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,17 +373,23 @@ 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
 
         -- 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