Add a prover-validate flag and pass it to SBV (default: off)

This should address the issue reported in https://github.com/GaloisInc/cryptol/issues/558

src/Cryptol/REPL/Command.hs

@@ -574,6 +574,7 @@ onlineProveSat isSat str mfile = do
   proverName <- getKnownUser "prover"
   verbose <- getKnownUser "debug"
   satNum <- getUserSatNum
+  modelValidate <- getUserProverValidate
   parseExpr <- replParseExpr str
   (_, expr, schema) <- replCheckExpr parseExpr
   validEvalContext expr
@@ -584,6 +585,7 @@ onlineProveSat isSat str mfile = do
           pcQueryType    = if isSat then SatQuery satNum else ProveQuery
         , pcProverName   = proverName
         , pcVerbose      = verbose
+        , pcValidate     = modelValidate
         , pcProverStats  = timing
         , pcExtraDecls   = decls
         , pcSmtFile      = mfile
@@ -597,6 +599,7 @@ onlineProveSat isSat str mfile = do
 offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
 offlineProveSat isSat str mfile = do
   verbose <- getKnownUser "debug"
+  modelValidate <- getUserProverValidate
   parseExpr <- replParseExpr str
   (_, expr, schema) <- replCheckExpr parseExpr
   decls <- fmap M.deDecls getDynEnv
@@ -605,6 +608,7 @@ offlineProveSat isSat str mfile = do
           pcQueryType    = if isSat then SatQuery (SomeSat 0) else ProveQuery
         , pcProverName   = "offline"
         , pcVerbose      = verbose
+        , pcValidate     = modelValidate
         , pcProverStats  = timing
         , pcExtraDecls   = decls
         , pcSmtFile      = mfile

src/Cryptol/REPL/Monad.hs

@@ -62,6 +62,7 @@ module Cryptol.REPL.Monad (
   , userOptions
   , getUserSatNum
   , getUserShowProverStats
+  , getUserProverValidate
 
     -- ** Configurable Output
   , getPutStr
@@ -709,6 +710,9 @@ badIsEnv x = panic "fromEnvVal" [ "[REPL] Expected a `" ++ x ++ "` value." ]
 getUserShowProverStats :: REPL Bool
 getUserShowProverStats = getKnownUser "prover-stats"
 
+getUserProverValidate :: REPL Bool
+getUserProverValidate = getKnownUser "prover-validate"
+
 -- Environment Options ---------------------------------------------------------
 
 type OptionMap = Trie OptionDescr
@@ -795,6 +799,9 @@ userOptions  = mkOptionMap
 
   , simpleOpt "prover-stats" (EnvBool True) noCheck
     "Enable prover timing statistics."
+
+  , simpleOpt "prover-validate" (EnvBool False) noCheck
+    "Validate :sat examples and :prove counter-examples for correctness."
   ]
 
 

src/Cryptol/Symbolic.hs

@@ -93,6 +93,8 @@ data ProverCommand = ProverCommand {
     -- ^ Which prover to use (one of the strings in 'proverConfigs')
   , pcVerbose :: Bool
     -- ^ Verbosity flag passed to SBV
+  , pcValidate :: Bool
+    -- ^ Model validation flag passed to SBV
   , pcProverStats :: !(IORef ProverStats)
     -- ^ Record timing information here
   , pcExtraDecls :: [DeclGroup]
@@ -148,7 +150,10 @@ satProve ProverCommand {..} =
                                                }]
 
 
-  let provers' = [ p { SBV.timing = SaveTiming pcProverStats, SBV.verbose = pcVerbose } | p <- provers ]
+  let provers' = [ p { SBV.timing = SaveTiming pcProverStats
+                     , SBV.verbose = pcVerbose
+                     , SBV.validateModel = pcValidate
+                     } | p <- provers ]
   let tyFn = if isSat then existsFinType else forallFinType
   let lPutStrLn = M.withLogger logPutStrLn
   let doEval :: MonadIO m => Eval.Eval a -> m a