copilot-language: Preserve proposition quantifiers. Refs #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`.

Author: RyanGlScott

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.