Check Prop more strictly; implement boolToProp.

We strengthen the invariants on Prop to require that they
have type saw-core type `Prop`, which is now possible
because we fixed a bug in `scTypeOf`.

Implement `boolToProp` to treat boolean terms as propositions.

src/SAWScript/Builtins.hs

@@ -860,8 +860,7 @@ satPrintPrim script t = do
 -- 'Integer' parameter is the number of random tests to run.
 quickCheckPrintPrim :: Options -> SharedContext -> Integer -> TypedTerm -> IO ()
 quickCheckPrintPrim opts sc numTests tt =
-  do let tm = ttTerm tt
-     prop <- predicateToProp sc Universal tm
+  do prop <- predicateToProp sc Universal (ttTerm tt)
      satq <- propToSATQuery sc mempty prop
      testGen <- prepareSATQuery sc satq
      runManyTests testGen numTests >>= \case

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -270,7 +270,7 @@ verifyObligations cc mspec tactic assumes asserts =
      let nm = mspec ^. csMethodName
      stats <- forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) -> do
        goal   <- io $ scImplies sc assume assert
-       goal'  <- io $ predicateToProp sc Universal goal
+       goal'  <- io $ boolToProp sc [] goal -- TODO, generalize over inputs
        let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
            proofgoal = ProofGoal n "vc" goalname goal'
        res <- runProofScript tactic proofgoal

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -598,7 +598,7 @@ verifyObligations cc mspec tactic assumes asserts =
      stats <-
        forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) ->
        do goal   <- io $ scImplies sc assume assert
-          goal'  <- io $ predicateToProp sc Universal goal
+          goal'  <- io $ boolToProp sc [] goal
           let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
               proofgoal = ProofGoal n "vc" goalname goal'
           res <- runProofScript tactic proofgoal
@@ -764,7 +764,7 @@ assumptionsContainContradiction cc tactic assumptions =
          assume <- scAndList sc (toListOf (folded . Crucible.labeledPred) assumptions)
          -- implies falsehood
          goal  <- scImplies sc assume =<< toSC sym st (W4.falsePred sym)
-         goal' <- predicateToProp sc Universal goal
+         goal' <- boolToProp sc [] goal
          return $ ProofGoal 0 "vc" "vacuousness check" goal'
      res <- runProofScript tactic pgl
      case res of

src/SAWScript/Proof.hs

@@ -57,6 +57,7 @@ module SAWScript.Proof
 
   , Quantification(..)
   , predicateToProp
+  , boolToProp
 
   , ProofState
   , psTimeout
@@ -95,20 +96,20 @@ import Verifier.SAW.Term.Pretty (SawDoc)
 import Verifier.SAW.SCTypeCheck (scTypeCheckError)
 
 import Verifier.SAW.Simulator.Concrete (evalSharedTerm)
-import Verifier.SAW.Simulator.Value (asFirstOrderTypeValue)
+import Verifier.SAW.Simulator.Value (asFirstOrderTypeValue, Value(..), TValue(..))
 
 import SAWScript.Position
 import SAWScript.Prover.SolverStats
 import SAWScript.Crucible.Common as Common
 import qualified Verifier.SAW.Simulator.What4 as W4Sim
 import qualified Verifier.SAW.Simulator.What4.ReturnTrip as W4Sim
 
--- | A proposition is a saw-core type (i.e. a term of type @sort n@
--- for some @n@). In particular, this includes any pi type whose
--- result type is a proposition. The argument of a pi type represents
+-- | A proposition is a saw-core type of type `Prop`.
+-- In particular, this includes any pi type whose result
+-- type is a proposition. The argument of a pi type represents
 -- a universally quantified variable.
 newtype Prop = Prop Term
-  -- INVARIANT: The type of the given term is a sort
+  -- INVARIANT: The type of the given term is `Prop`
 
 unProp :: Prop -> Term
 unProp (Prop tm) = tm
@@ -118,10 +119,25 @@ unProp (Prop tm) = tm
 --   is a sort.
 termToProp :: SharedContext -> Term -> IO Prop
 termToProp sc tm =
-   do ty <- scWhnf sc =<< scTypeOf sc tm
-      case asSort ty of
-        Nothing -> fail $ unlines [ "termToProp: Term is not a proposition", showTerm tm ]
-        Just _s -> return (Prop tm)
+   do mmap <- scGetModuleMap sc
+      ty <- scTypeOf sc tm
+      case evalSharedTerm mmap mempty mempty ty of
+        TValue (VSort s) | s == propSort -> return (Prop tm)
+        _ -> fail $ unlines [ "termToProp: Term is not a proposition", showTerm tm, showTerm ty ]
+
+
+-- | Turn a boolean-valued saw-core term into a proposition by asserting
+--   that it is equal to the true boolean value.  Generalize the proposition
+--   by universally quantifing over the variables given in the list.
+boolToProp :: SharedContext -> [ExtCns Term] -> Term -> IO Prop
+boolToProp sc vars tm =
+  do mmap <- scGetModuleMap sc
+     ty <- scTypeOf sc tm
+     case evalSharedTerm mmap mempty mempty ty of
+       TValue VBoolType ->
+         do p0 <- scEqTrue sc tm
+            Prop <$> scGeneralizeExts sc vars p0
+       _ -> fail $ unlines [ "boolToProp: Term is not a boolean", showTerm tm, showTerm ty ]
 
 -- | Return the saw-core term that represents this proposition.
 propToTerm :: SharedContext -> Prop -> IO Term
@@ -418,6 +434,7 @@ data ProofGoal =
 data Quantification = Existential | Universal
   deriving Eq
 
+
 -- | Convert a term with a function type of any arity into a pi type.
 -- Negate the term if the result type is @Bool@ and the quantification
 -- is 'Existential'.
@@ -433,7 +450,7 @@ predicateToProp sc quant = loop []
         do (argTs, resT) <- asPiList <$> scTypeOf' sc env t
            let toPi [] t0 =
                  case asBoolType resT of
-                   Nothing -> return t0 -- TODO: check quantification  TODO2: should this just be an error?
+                   Nothing -> fail $ unlines ["predicateToProp : Expected boolean result type but got", showTerm resT]
                    Just () ->
                      case quant of
                        Universal -> scEqTrue sc t0

src/SAWScript/Prover/MRSolver.hs

@@ -21,7 +21,7 @@ import Verifier.SAW.Term.Functor
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Recognizer
 
-import SAWScript.Proof (predicateToProp, Quantification(..))
+import SAWScript.Proof (boolToProp)
 import qualified SAWScript.Prover.SBV as SBV
 
 import Prelude
@@ -281,7 +281,7 @@ mrProvable bool_prop =
      path_prop <- mrPathCondition <$> get
      bool_prop' <- liftSC2 scImplies path_prop bool_prop
      sc <- mrSC <$> get
-     prop <- liftIO (predicateToProp sc Universal bool_prop')
+     prop <- liftIO (boolToProp sc [] bool_prop')
      (smt_res, _) <- liftSC1 (SBV.proveUnintSBV smt_conf mempty timeout) prop
      case smt_res of
        Just _ -> return False

src/SAWScript/X86.hs

@@ -132,7 +132,7 @@ import Verifier.SAW.Cryptol.Prelude(scLoadPreludeModule,scLoadCryptolModule)
 
 -- SAWScript
 import SAWScript.X86Spec hiding (Prop)
-import SAWScript.Proof(predicateToProp, Quantification(Universal), Prop)
+import SAWScript.Proof(boolToProp, Prop)
 import SAWScript.Crucible.Common (newSAWCoreBackend, sawCoreState)
 
 
@@ -540,7 +540,7 @@ data Goal = Goal
 
 -- | The proposition that needs proving (i.e., assumptions imply conclusion)
 gGoal :: SharedContext -> Goal -> IO Prop
-gGoal sc g0 = predicateToProp sc Universal =<< go (gAssumes g)
+gGoal sc g0 = boolToProp sc [] =<< go (gAssumes g)
   where
   g = g0 { gAssumes = mapMaybe skip (gAssumes g0) }