Introduce Prop newtype wrapper for Terms representing propositions as types

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -275,7 +275,7 @@ verifyObligations cc mspec tactic assumes asserts =
        goal   <- io $ scImplies sc assume assert
        goal'  <- io $ scGeneralizeExts sc (getAllExts goal) =<< scEqTrue sc goal
        let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
-           proofgoal = ProofGoal n "vc" goalname goal'
+           proofgoal = ProofGoal n "vc" goalname (Prop goal')
        r      <- evalStateT tactic (startProof proofgoal)
        case r of
          Unsat stats -> return stats

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -401,7 +401,7 @@ verifyObligations cc mspec tactic assumes asserts = do
     goal   <- io $ scImplies sc assume assert
     goal'  <- io $ scGeneralizeExts sc (getAllExts goal) =<< scEqTrue sc goal
     let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
-        proofgoal = ProofGoal n "vc" goalname goal'
+        proofgoal = ProofGoal n "vc" goalname (Prop goal')
     r <- evalStateT tactic (startProof proofgoal)
     case r of
       Unsat stats -> return stats

src/SAWScript/Interpreter.hs

@@ -1099,78 +1099,78 @@ primitives = Map.fromList
     ]
 
   , prim "abc"                 "ProofScript SatResult"
-    (pureVal satABC)
+    (pureVal proveABC)
     Current
     [ "Use the ABC theorem prover to prove the current goal." ]
 
   , prim "boolector"           "ProofScript SatResult"
-    (pureVal satBoolector)
+    (pureVal proveBoolector)
     Current
     [ "Use the Boolector theorem prover to prove the current goal." ]
 
   , prim "cvc4"                "ProofScript SatResult"
-    (pureVal satCVC4)
+    (pureVal proveCVC4)
     Current
     [ "Use the CVC4 theorem prover to prove the current goal." ]
 
   , prim "z3"                  "ProofScript SatResult"
-    (pureVal satZ3)
+    (pureVal proveZ3)
     Current
     [ "Use the Z3 theorem prover to prove the current goal." ]
 
   , prim "mathsat"             "ProofScript SatResult"
-    (pureVal satMathSAT)
+    (pureVal proveMathSAT)
     Current
     [ "Use the MathSAT theorem prover to prove the current goal." ]
 
   , prim "yices"               "ProofScript SatResult"
-    (pureVal satYices)
+    (pureVal proveYices)
     Current
     [ "Use the Yices theorem prover to prove the current goal." ]
 
   , prim "unint_z3"            "[String] -> ProofScript SatResult"
-    (pureVal satUnintZ3)
+    (pureVal proveUnintZ3)
     Current
     [ "Use the Z3 theorem prover to prove the current goal. Leave the"
     , "given list of names, as defined with 'define', as uninterpreted."
     ]
 
   , prim "unint_cvc4"            "[String] -> ProofScript SatResult"
-    (pureVal satUnintCVC4)
+    (pureVal proveUnintCVC4)
     Current
     [ "Use the CVC4 theorem prover to prove the current goal. Leave the"
     , "given list of names, as defined with 'define', as uninterpreted."
     ]
 
   , prim "unint_yices"           "[String] -> ProofScript SatResult"
-    (pureVal satUnintYices)
+    (pureVal proveUnintYices)
     Current
     [ "Use the Yices theorem prover to prove the current goal. Leave the"
     , "given list of names, as defined with 'define', as uninterpreted."
     ]
 
   , prim "offline_aig"         "String -> ProofScript SatResult"
-    (pureVal satAIG)
+    (pureVal offline_aig)
     Current
     [ "Write the current goal to the given file in AIGER format." ]
 
   , prim "offline_cnf"         "String -> ProofScript SatResult"
-    (pureVal satCNF)
+    (pureVal offline_cnf)
     Current
     [ "Write the current goal to the given file in CNF format." ]
 
   , prim "offline_extcore"     "String -> ProofScript SatResult"
-    (pureVal satExtCore)
+    (pureVal offline_extcore)
     Current
     [ "Write the current goal to the given file in SAWCore format." ]
 
   , prim "offline_smtlib2"     "String -> ProofScript SatResult"
-    (pureVal satSMTLib2)
+    (pureVal offline_smtlib2)
     Current
     [ "Write the current goal to the given file in SMT-Lib2 format." ]
 
   , prim "offline_unint_smtlib2"  "[String] -> String -> ProofScript SatResult"
-    (pureVal satUnintSMTLib2)
+    (pureVal offline_unint_smtlib2)
     Current
     [ "Write the current goal to the given file in SMT-Lib2 format,"
     , "leaving the listed functions uninterpreted."
@@ -1195,7 +1195,7 @@ primitives = Map.fromList
     , "temporary file holding the AIG version of the formula."]
 
   , prim "rme"                 "ProofScript SatResult"
-    (pureVal satRME)
+    (pureVal proveRME)
     Current
     [ "Prove the current goal by expansion to Reed-Muller Normal Form." ]
 
@@ -1205,26 +1205,26 @@ primitives = Map.fromList
     [ "Succeed only if the proof goal is a literal 'True'." ]
 
   , prim "w4"                  "ProofScript SatResult"
-    (pureVal satWhat4_Z3)
+    (pureVal w4_z3)
     Current
     [ "Prove the current goal using What4 (Z3 backend)." ]
 
   , prim "w4_unint_z3"         "[String] -> ProofScript SatResult"
-    (pureVal satWhat4_UnintZ3)
+    (pureVal w4_unint_z3)
     Current
     [ "Prove the current goal using What4 (Z3 backend). Leave the"
     , "given list of names, as defined with 'define', as uninterpreted."
     ]
 
   , prim "w4_unint_yices"         "[String] -> ProofScript SatResult"
-    (pureVal satWhat4_UnintYices)
+    (pureVal w4_unint_yices)
     Current
     [ "Prove the current goal using What4 (Yices backend). Leave the"
     , "given list of names, as defined with 'define', as uninterpreted."
     ]
 
   , prim "w4_unint_cvc4"         "[String] -> ProofScript SatResult"
-    (pureVal satWhat4_UnintCVC4)
+    (pureVal w4_unint_cvc4)
     Current
     [ "Prove the current goal using What4 (CVC4 backend). Leave the"
     , "given list of names, as defined with 'define', as uninterpreted."

src/SAWScript/JavaBuiltins.hs

@@ -251,7 +251,7 @@ verifyJava bic opts cls mname overrides setup = do
               let exts = getAllExts g
               gprop <- io $ scGeneralizeExts jsc exts =<< scEqTrue jsc g
               io $ doExtraChecks opts bsc gprop
-              let goal = ProofGoal n "vc" (vsVCName vs) gprop
+              let goal = ProofGoal n "vc" (vsVCName vs) (Prop gprop)
               r <- evalStateT script (startProof goal)
               case r of
                 SS.Unsat _ -> liftIO $ printOutLn opts Debug "Valid."

src/SAWScript/Proof.hs

@@ -11,19 +11,24 @@ import Verifier.SAW.Recognizer
 import Verifier.SAW.SharedTerm
 import SAWScript.Prover.SolverStats
 
--- | A theorem must contain a boolean term, possibly surrounded by one
--- or more lambdas which are interpreted as universal quantifiers.
-data Theorem = Theorem { thmTerm :: Term }
+-- | 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 universally quantified variable.
+newtype Prop = Prop { unProp :: Term }
 
--- | A ProofGoal is a term of type @sort n@, or a pi type of any arity
--- with a @sort n@ result type. The abstracted arguments are treated
--- as universally quantified.
+-- | A theorem is a proposition which has been wrapped in a
+-- constructor indicating that it has already been proved.
+data Theorem = Theorem { thmProp :: Prop }
+
+-- | A @ProofGoal@ contains a proposition to be proved, along with
+-- some metadata.
 data ProofGoal =
   ProofGoal
   { goalNum  :: Int
   , goalType :: String
   , goalName :: String
-  , goalTerm :: Term
+  , goalProp :: Prop
   }
 
 data Quantification = Existential | Universal
@@ -49,12 +54,12 @@ makeProofGoal sc quant gnum gtype gname t =
 -- | 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'.
-predicateToProp :: SharedContext -> Quantification -> [Term] -> Term -> IO Term
+predicateToProp :: SharedContext -> Quantification -> [Term] -> Term -> IO Prop
 predicateToProp sc quant env t =
   case asLambda t of
     Just (x, ty, body) ->
-      do body' <- predicateToProp sc quant (ty : env) body
-         scPi sc x ty body'
+      do Prop body' <- predicateToProp sc quant (ty : env) body
+         Prop <$> scPi sc x ty body'
     Nothing ->
       do (argTs, resT) <- asPiList <$> scTypeOf' sc env t
          let toPi [] t0 =
@@ -69,14 +74,14 @@ predicateToProp sc quant env t =
                   t2 <- scApply sc t1 =<< scLocalVar sc 0
                   t3 <- toPi tys t2
                   scPi sc x xT t3
-         toPi argTs t
+         Prop <$> toPi argTs t
 
 -- | Turn a pi type with an @EqTrue@ result into a lambda term with a
 -- boolean result type. This function exists to interface the new
 -- pi-type proof goals with older proof tactic implementations that
 -- expect the old lambda-term representation.
-propToPredicate :: SharedContext -> Term -> IO Term
-propToPredicate sc goal =
+propToPredicate :: SharedContext -> Prop -> IO Term
+propToPredicate sc (Prop goal) =
   do let (args, t1) = asPiList goal
      t2 <- asEqTrue t1
      scLambdaList sc args t2
@@ -97,5 +102,5 @@ startProof g = ProofState [g] g mempty Nothing
 finishProof :: ProofState -> (SolverStats, Maybe Theorem)
 finishProof (ProofState gs concl stats _) =
   case gs of
-    []    -> (stats, Just (Theorem (goalTerm concl)))
+    []    -> (stats, Just (Theorem (goalProp concl)))
     _ : _ -> (stats, Nothing)

src/SAWScript/Prover/ABC.hs

@@ -1,4 +1,4 @@
-module SAWScript.Prover.ABC (satABC) where
+module SAWScript.Prover.ABC (proveABC) where
 
 
 import qualified Data.AIG as AIG
@@ -8,22 +8,21 @@ import           Verifier.SAW.TypedTerm
 import           Verifier.SAW.FiniteValue
 import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 
-import SAWScript.Proof(propToPredicate)
+import SAWScript.Proof(Prop, propToPredicate)
 import SAWScript.Prover.SolverStats (SolverStats, solverStats)
 import SAWScript.Prover.Rewrite(rewriteEqs)
 import SAWScript.SAWCorePrimitives( bitblastPrimitives )
 import SAWScript.Prover.Util
          (liftCexBB, bindAllExts, checkBooleanSchema)
 
--- | Bit-blast a @Term@ representing a theorem and check its
--- satisfiability using ABC.
-satABC ::
+-- | Bit-blast a proposition and check its validity using ABC.
+proveABC ::
   (AIG.IsAIG l g) =>
   AIG.Proxy l g ->
   SharedContext ->
-  Term ->
-  IO (Maybe [(String,FirstOrderValue)], SolverStats)
-satABC proxy sc goal =
+  Prop ->
+  IO (Maybe [(String, FirstOrderValue)], SolverStats)
+proveABC proxy sc goal =
   do t0 <- propToPredicate sc goal
      TypedTerm schema t <-
         (bindAllExts sc t0 >>= rewriteEqs sc >>= mkTypedTerm sc)

src/SAWScript/Prover/Exporter.hs

@@ -1,6 +1,6 @@
 {-# Language ViewPatterns #-}
 module SAWScript.Prover.Exporter
-  ( satWithExporter
+  ( proveWithExporter
   , adaptExporter
 
     -- * External formats
@@ -14,6 +14,7 @@ module SAWScript.Prover.Exporter
   , write_smtlib2
   , writeUnintSMTLib2
   , writeCore
+  , writeCoreProp
 
     -- * Misc
   , bitblastPrim
@@ -36,34 +37,34 @@ import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 
 
 import SAWScript.SAWCorePrimitives( bitblastPrimitives )
-import SAWScript.Proof (predicateToProp, Quantification(..))
+import SAWScript.Proof (Prop(..), predicateToProp, Quantification(..))
 import SAWScript.Prover.SolverStats
 import SAWScript.Prover.Rewrite
 import SAWScript.Prover.Util
-import SAWScript.Prover.SBV(prepSBV)
+import SAWScript.Prover.SBV (prepNegatedSBV)
 import SAWScript.Value
 
 
-satWithExporter ::
-  (SharedContext -> FilePath -> Term -> IO ()) ->
+proveWithExporter ::
+  (SharedContext -> FilePath -> Prop -> IO ()) ->
   String ->
   SharedContext ->
-  Term ->
+  Prop ->
   IO SolverStats
-satWithExporter exporter path sc goal =
+proveWithExporter exporter path sc goal =
   do exporter sc path goal
-     let stats = solverStats ("offline: "++ path) (scSharedSize goal)
+     let stats = solverStats ("offline: "++ path) (scSharedSize (unProp goal))
      return stats
 
 -- | Converts an old-style exporter (which expects to take a predicate
 -- as an argument) into a new-style one (which takes a pi-type proposition).
 adaptExporter ::
   (SharedContext -> FilePath -> Term -> IO ()) ->
-  (SharedContext -> FilePath -> Term -> IO ())
-adaptExporter exporter sc path goal =
+  (SharedContext -> FilePath -> Prop -> IO ())
+adaptExporter exporter sc path (Prop goal) =
   do let (args, concl) = asPiList goal
      p <- asEqTrue concl
-     p' <- scNot sc p
+     p' <- scNot sc p -- is this right?
      t <- scLambdaList sc args p'
      exporter sc path t
 
@@ -148,9 +149,9 @@ write_cnf sc f (TypedTerm schema t) = do
   AIGProxy proxy <- getProxy
   io $ writeCNF proxy sc f t
 
--- | Write a @Term@ representing a theorem to an SMT-Lib version
--- 2 file.
-writeSMTLib2 :: SharedContext -> FilePath -> Term -> IO ()
+-- | Write a proposition to an SMT-Lib version 2 file.
+-- TODO: say something about convention for negation
+writeSMTLib2 :: SharedContext -> FilePath -> Prop -> IO ()
 writeSMTLib2 sc f t = writeUnintSMTLib2 [] sc f t
 
 -- | Write a @Term@ representing a predicate (i.e. a monomorphic
@@ -161,18 +162,21 @@ write_smtlib2 sc f (TypedTerm schema t) = do
   p <- predicateToProp sc Universal [] t
   writeSMTLib2 sc f p
 
--- | Write a @Term@ representing a theorem to an SMT-Lib version
--- 2 file, treating some constants as uninterpreted.
-writeUnintSMTLib2 :: [String] -> SharedContext -> FilePath -> Term -> IO ()
-writeUnintSMTLib2 unints sc f t = do
-  (_, _, l) <- prepSBV sc unints t
-  let isSat = False -- term is a proof goal with universally-quantified variables
-  txt <- SBV.generateSMTBenchmark isSat l
-  writeFile f txt
+-- | Write a proposition to an SMT-Lib version 2 file, treating some
+-- constants as uninterpreted.
+writeUnintSMTLib2 :: [String] -> SharedContext -> FilePath -> Prop -> IO ()
+writeUnintSMTLib2 unints sc f t =
+  do (_, _, l) <- prepNegatedSBV sc unints t
+     let isSat = True -- l is encoded as an existential formula
+     txt <- SBV.generateSMTBenchmark isSat l
+     writeFile f txt
 
 writeCore :: FilePath -> Term -> IO ()
 writeCore path t = writeFile path (scWriteExternal t)
 
+writeCoreProp :: FilePath -> Prop -> IO ()
+writeCoreProp path (Prop t) = writeFile path (scWriteExternal t)
+
 
 -- | Tranlsate a SAWCore term into an AIG
 bitblastPrim :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> Term -> IO (AIG.Network l g)
@@ -186,5 +190,3 @@ bitblastPrim proxy sc t = do
 -}
   BBSim.withBitBlastedTerm proxy sc bitblastPrimitives t' $ \be ls -> do
     return (AIG.Network be (toList ls))
-
-