<commit_before>{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
module CryptolServer.Sat
  ( proveSat
  , proveSatDescr
  , ProveSatParams(..)
  )
  where

import qualified Argo.Doc as Doc
import Control.Applicative
import Control.Monad.IO.Class
import Data.Aeson ((.=), (.:), (.:?), (.!=), FromJSON, ToJSON)
import qualified Data.Aeson as Aeson
import qualified Data.Aeson.Types as Aeson
import qualified Data.Aeson as JSON
import Data.IORef
import qualified Data.List as List
import Data.Scientific (floatingOrInteger)
import Data.Text (Text)
import qualified Data.Text as T

import Cryptol.Eval.Concrete (Value)
import Cryptol.Eval.Type (TValue, tValTy)
import Cryptol.ModuleSystem (checkExpr)
import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv)
import Cryptol.REPL.Command (withRWTempFile)
import Cryptol.Symbolic ( ProverCommand(..), ProverResult(..), QueryType(..)
                        , SatNum(..), CounterExampleType(..))
import qualified Cryptol.Symbolic.SBV as SBV
import qualified Cryptol.Symbolic.What4 as W4
import Cryptol.TypeCheck.AST (Expr)
import Cryptol.TypeCheck.Solve (defaultReplExpr)

import CryptolServer
import CryptolServer.Exceptions (evalPolyErr, proverError)
import CryptolServer.Data.Expression
import CryptolServer.Data.Type
import Data.Text.IO as TIO
import System.IO (hSeek,SeekMode(..))

proveSatDescr :: Doc.Block
proveSatDescr =
  Doc.Paragraph
    [ Doc.Text "Find a value which satisfies the given predicate, or show that it is valid."
    , Doc.Text "(i.e., find a value which when passed as the argument produces true or show that for all possible arguments the predicate will produce true)."]



proveSat :: ProveSatParams -> CryptolCommand ProveSatResult
proveSat (ProveSatParams queryType (ProverName proverName) jsonExpr hConsing) = do
  e <- getExpr jsonExpr
  (_expr, ty, schema) <- liftModuleCmd (checkExpr e)
  -- TODO validEvalContext expr, ty, schema
  decls <- deDecls . meDynEnv <$> getModuleEnv
  s <- getTCSolver
  perhapsDef <- liftIO (defaultReplExpr s ty schema)
  case perhapsDef of
    Nothing -> raise (evalPolyErr schema)
    Just (_tys, checked) -> do
      timing <- liftIO $ newIORef 0
      let cmd =
            ProverCommand
            { pcQueryType    = queryType
            , pcProverName   = proverName
            , pcVerbose      = True
            , pcProverStats  = timing
            , pcExtraDecls   = decls
            , pcSmtFile      = Nothing
            , pcExpr         = checked
            , pcSchema       = schema
            , pcValidate     = False
            , pcIgnoreSafety = False
            }
      res <- if proverName `elem` ["offline","sbv-offline","w4-offline"]
             then offlineProveSat proverName cmd hConsing
             else onlineProveSat  proverName cmd hConsing
      _stats <- liftIO (readIORef timing)
      pure res


getProverConfig ::
  -- | Prover name.
  String ->
  CryptolCommand (Either SBV.SBVProverConfig W4.W4ProverConfig)
getProverConfig proverName =
  if proverName `elem` W4.proverNames then do
    liftIO (W4.setupProver proverName) >>= \case
      Left msg -> raise $ proverError $ "error setting up " ++ proverName ++ ": " ++ msg
      Right (_ws, w4Cfg) -> pure $ Right w4Cfg<commit_msg>cryptol-remote-api: Don't use verbose SBV settings (#1379)<commit_after>{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
module CryptolServer.Sat
  ( proveSat
  , proveSatDescr
  , ProveSatParams(..)
  )
  where

import qualified Argo.Doc as Doc
import Control.Applicative
import Control.Monad.IO.Class
import Data.Aeson ((.=), (.:), (.:?), (.!=), FromJSON, ToJSON)
import qualified Data.Aeson as Aeson
import qualified Data.Aeson.Types as Aeson
import qualified Data.Aeson as JSON
import Data.IORef
import qualified Data.List as List
import Data.Scientific (floatingOrInteger)
import Data.Text (Text)
import qualified Data.Text as T

import Cryptol.Eval.Concrete (Value)
import Cryptol.Eval.Type (TValue, tValTy)
import Cryptol.ModuleSystem (checkExpr)
import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv)
import Cryptol.REPL.Command (withRWTempFile)
import Cryptol.Symbolic ( ProverCommand(..), ProverResult(..), QueryType(..)
                        , SatNum(..), CounterExampleType(..))
import qualified Cryptol.Symbolic.SBV as SBV
import qualified Cryptol.Symbolic.What4 as W4
import Cryptol.TypeCheck.AST (Expr)
import Cryptol.TypeCheck.Solve (defaultReplExpr)

import CryptolServer
import CryptolServer.Exceptions (evalPolyErr, proverError)
import CryptolServer.Data.Expression
import CryptolServer.Data.Type
import Data.Text.IO as TIO
import System.IO (hSeek,SeekMode(..))

proveSatDescr :: Doc.Block
proveSatDescr =
  Doc.Paragraph
    [ Doc.Text "Find a value which satisfies the given predicate, or show that it is valid."
    , Doc.Text "(i.e., find a value which when passed as the argument produces true or show that for all possible arguments the predicate will produce true)."]



proveSat :: ProveSatParams -> CryptolCommand ProveSatResult
proveSat (ProveSatParams queryType (ProverName proverName) jsonExpr hConsing) = do
  e <- getExpr jsonExpr
  (_expr, ty, schema) <- liftModuleCmd (checkExpr e)
  -- TODO validEvalContext expr, ty, schema
  decls <- deDecls . meDynEnv <$> getModuleEnv
  s <- getTCSolver
  perhapsDef <- liftIO (defaultReplExpr s ty schema)
  case perhapsDef of
    Nothing -> raise (evalPolyErr schema)
    Just (_tys, checked) -> do
      timing <- liftIO $ newIORef 0
      let cmd =
            ProverCommand
            { pcQueryType    = queryType
            , pcProverName   = proverName
            , pcVerbose      = False
            , pcProverStats  = timing
            , pcExtraDecls   = decls
            , pcSmtFile      = Nothing
            , pcExpr         = checked
            , pcSchema       = schema
            , pcValidate     = False
            , pcIgnoreSafety = False
            }
      res <- if proverName `elem` ["offline","sbv-offline","w4-offline"]
             then offlineProveSat proverName cmd hConsing
             else onlineProveSat  proverName cmd hConsing
      _stats <- liftIO (readIORef timing)
      pure res


getProverConfig ::
  -- | Prover name.
  String ->
  CryptolCommand (Either SBV.SBVProverConfig W4.W4ProverConfig)
getProverConfig proverName =
  if proverName `elem` W4.proverNames then do
    liftIO (W4.setupProver proverName) >>= \case
      Left msg -> raise $ proverError $ "error setting up " ++ proverName ++ ": " ++ msg
      Right (_ws, w4Cfg) -> pure $ Right w4Cfg
{'fraction_non_alphanumeric': 0.09756455399061033, 'fraction_numerical': 0.0035211267605633804, 'mean_word_length': 3.1190332326283987, 'pattern_counts': {'":': 2, '<': 21, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5001235', 'n_tokens_mistral': 2240, 'n_tokens_neox': 2108, 'n_words': 601}