Merge branch 'develop-what4-respect-quantifiers-T254'. Close #254.

**Description**

`Copilot.Language.Spec.prop` and `Copilot.Language.Spec.theorem` are both
reified into as a bare stream of booleans, and do not retain information about
whether the `Prop` passed as argument was a `Forall` or an `Exists`. Because
this information is not retained when later using `Copilot.Theorem.Prove.prove`
to check the properties, the results returned by the SMT solvers may be
incorrect.

**Type**

- Bug: Information is lost, leading to unexpected results .

**Additional context**

None.

**Requester**

- Rob Dockins.

**Method to check presence of bug**

The issue can be detected with the following sample programs:

```haskell
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Data.Foldable
import Data.Functor

import Copilot.Theorem.What4
import Language.Copilot

trueThenFalses :: Stream Bool
trueThenFalses = [True] ++ constant False

spec :: Spec
spec = do
  void $ prop "forAll trueThenFalses (should be invalid)" (forAll trueThenFalses)
  void $ prop "exists trueThenFalses (should be valid)" (exists trueThenFalses)

main :: IO ()
main = do
  spec' <- reify spec
  results <- prove Z3 spec'
  forM_ results $ \(nm, res) -> do
    putStr $ nm <> ": "
    case res of
      Valid   -> putStrLn "valid"
      Invalid -> putStrLn "invalid"
      Unknown -> putStrLn "unknown"
```

The following Dockerfile runs the prover on a Copilot spec that proves an
existential, which produces an exception caught by the program (as expected),
after which it prints the message "Success". If an exception is not caught, the
program exits with an error code.

```
--- Dockerfile-verify-254
FROM ubuntu:focal

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config \
      z3

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup
RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.10.1
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.10.1
RUN cabal update

ADD What4Existential.hs /tmp/What4Existential.hs

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-sandbox init \
  && cabal v1-install alex happy --constraint='happy <= 2' \
  && cabal v1-install $NAME/copilot**/ \
  && cabal v1-exec -- runhaskell /tmp/What4Existential.hs \
  && echo "Success"

--- What4Existential.hs
{-# LANGUAGE NoImplicitPrelude   #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Main (main) where

import Control.Exception ( SomeException, handle )
import Data.Foldable     ( forM_ )
import Data.Functor      ( void )
import System.Exit       ( exitFailure, exitSuccess )

import Copilot.Theorem.What4
import Language.Copilot

main :: IO ()
main = do
  handle (\(_ :: SomeException) -> exitSuccess) $ do
    proveSpec specF
    proveSpec specE
    putStrLn "The What4 backend tried to prove an existential proposition"
  exitFailure

proveSpec :: Spec -> IO ()
proveSpec spec = do
  spec' <- reify spec
  results <- prove Z3 spec'
  forM_ results $ \(nm, res) -> do
    putStr $ nm <> ": "
    case res of
      Valid   -> putStrLn "valid"
      Invalid -> putStrLn "invalid"
      Unknown -> putStrLn "unknown"

specF :: Spec
specF = void $
  prop "forAll trueThenFalses (should be invalid)" (forAll trueThenFalses)

specE :: Spec
specE = void $
  prop
    "exists trueThenFalses (shouldn't have a known result)"
    (exists trueThenFalses)

trueThenFalses :: Stream Bool
trueThenFalses = [True] ++ constant False
```

Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-254
```

**Expected result**

Running the specs above or a similar variant via What4 should yield `valid`
when the property is indeed valid (the second property above), indicating that
respects the quantifier is being respected.

If the prover is not able to prove a property of that kind, a suitable error
message should be printed.

Running the dockerfile above prints "Success", indicating that copilot-theorem
correctly detected that one of the properties is existential and cannot be
handled by the What4 backend.

**Proposed solution**

Modify `copilot-core` to introduce a type to represent existentially or
universally quantified properties, keeping enough information about the
quantifier.

Modify `copilot-language` to carry enough information about the quantifier
used.

Modify `copilot-theorem` to ensure a proper encoding of the property when
connecting to What4, and refuse to prove the property when the result would be
incorrect by throwing an exception.

Modify `copilot-prettyprinter` to handle the new type of quantified properties.

**Further notes**

None.

Author: ivanperez-keera

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