copilot-theorem: 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-theorem` to make use of quantifier information when
proving theorems.

Author: RyanGlScott

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

@@ -350,17 +350,18 @@ 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
 
         -- 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
       ]

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