GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-10-26 14:20:59 +03:00
Code Issues Projects Releases Wiki Activity

feat: support for all solver backends for cryptol server/client (#1224)

Browse Source 
* feat: support for all solver backends for cryptol server/client
* chore: update server docs w.r.t. sat related functionality
* chore: reduce trailing whitespace
* chore: deduplicate usage of helper
* chore: misc build fixes
* chore: type annotation fixes
This commit is contained in:
Andrew Kent 2021-07-02 07:27:40 -07:00 committed by GitHub
parent dfae4580e3
commit 571f0dd249
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 253 additions and 81 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
cryptol-remote-api/cryptol-remote-api.cabal
View File

@ -42,6 +42,7 @@ common deps
bytestring ^>= 0.10.8,
containers >=0.6.0.1 && <0.7,
cryptol >= 2.9.0,
directory,
filepath ^>= 1.4,
lens >= 4.17 && < 4.20,
mtl ^>= 2.2,

20
cryptol-remote-api/docs/Cryptol.rst
View File

@ -557,7 +557,7 @@ Parameter fields
``prover``
The SMT solver to use to check for satisfiability. I.e., one of the following: ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``, .
The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-offline``, ``w4-any``, ``cvc4``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
@ -576,27 +576,37 @@ Parameter fields
``hash consing``
Whether or not to use hash consing of terms (if available).``true`` to enable or ``false`` to disable.
Return fields
+++++++++++++
``result``
A string (one of ``unsatisfiable``, ``invalid``, or ``satisfied``) indicating the result of checking for validity, satisfiability, or safety.
Either a string indicating the result of checking for validity, satisfiability, or safety---i.e., one of ``unsatisfiable``, ``invalid``, or ``satisfied``---or the string literal ``offline`` indicating an offline solver option was selected and the contents of the SMT query will be returned instead of a SAT result.
``counterexample type``
Only used if the ``result`` is ``invalid``.This describes the variety of counterexample that was produced. This can be either ``safety violation`` or ``predicate falsified``.
Only used if the ``result`` is ``invalid``. This describes the variety of counterexample that was produced. This can be either ``safety violation`` or ``predicate falsified``.
``counterexample``
Only used if the ``result`` is ``invalid``.A list of objects where each object has an ``expr``field, indicating a counterexample expression, and a ``type``field, indicating the type of the expression.
Only used if the ``result`` is ``invalid``. A list of objects where each object has an ``expr``field, indicating a counterexample expression, and a ``type``field, indicating the type of the expression.
``models``
Only used if the ``result`` is ``satisfied``.A list of list of objects where each object has an ``expr``field, indicating a expression in a model, and a ``type``field, indicating the type of the expression.
Only used if the ``result`` is ``satisfied``. A list of list of objects where each object has an ``expr``field, indicating a expression in a model, and a ``type``field, indicating the type of the expression.
``query``
Only used if the ``result`` is ``offline``. The raw textual contents of the requested SMT query which can inspected or manually given to an SMT solver.

15
cryptol-remote-api/python/cryptol/commands.py
View File

@ -9,7 +9,7 @@ from typing_extensions import Literal
import argo_client.interaction as argo
from argo_client.interaction import HasProtocolState
from . import solver
from .solver import Solver, OfflineSmtQuery
from .bitvector import BV
from .opaque import OpaqueValue
@ -167,12 +167,13 @@ class SmtQueryType(str, Enum):
SAT = 'sat'
class CryptolProveSat(argo.Command):
def __init__(self, connection : HasProtocolState, qtype : SmtQueryType, expr : Any, solver : solver.Solver, count : Optional[int]) -> None:
def __init__(self, connection : HasProtocolState, qtype : SmtQueryType, expr : Any, solver : Solver, count : Optional[int]) -> None:
super(CryptolProveSat, self).__init__(
'prove or satisfy',
{'query type': qtype,
'expression': expr,
'prover': solver,
'prover': solver.name(),
'hash consing': "true" if solver.hash_consing() else "false",
'result count': 'all' if count is None else count},
connection
)
@ -193,19 +194,21 @@ class CryptolProveSat(argo.Command):
return [from_cryptol_arg(arg['expr'])
for m in res['models']
for arg in m]
elif res['result'] == 'offline':
return OfflineSmtQuery(content=res['query'])
else:
raise ValueError("Unknown SMT result: " + str(res))
class CryptolProve(CryptolProveSat):
def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None:
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
super(CryptolProve, self).__init__(connection, SmtQueryType.PROVE, expr, solver, 1)
class CryptolSat(CryptolProveSat):
def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver, count : int) -> None:
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver, count : int) -> None:
super(CryptolSat, self).__init__(connection, SmtQueryType.SAT, expr, solver, count)
class CryptolSafe(CryptolProveSat):
def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver) -> None:
def __init__(self, connection : HasProtocolState, expr : Any, solver : Solver) -> None:
super(CryptolSafe, self).__init__(connection, SmtQueryType.SAFE, expr, solver, 1)
class CryptolNames(argo.Command):

32
cryptol-remote-api/python/cryptol/solver.py
View File

@ -1,7 +1,35 @@
"""Cryptol solver-related definitions"""
from typing import NewType
Solver = NewType('Solver', str)
from dataclasses import dataclass
@dataclass
class OfflineSmtQuery():
"""An SMTLIB2 script -- produced when an `offline` prover is used."""
content: str
class Solver():
"""An SMT solver mode selectable for Cryptol. Compare with the `:set prover` options in
the Cryptol REPL."""
__name: str
__hash_consing: bool
def __init__(self, name:str, hash_consing:bool=True) -> None:
self.__name = name
self.__hash_consing = hash_consing
def name(self) -> str:
"""Returns a string describing the solver setup which Cryptol will recognize -- i.e.,
see the options available via `:set prover = NAME`."""
return self.__name
def hash_consing(self) -> bool:
"""Returns whether hash consing is enabled (if applicable)."""
return self.__hash_consing
def without_hash_consing(self) -> 'Solver':
"""Returns an identical solver but with hash consing disabled (if applicable)."""
return Solver(name=self.__name, hash_consing=False)
# Cryptol-supported SMT configurations/solvers
# (see Cryptol.Symbolic.SBV Haskell module)
@ -25,5 +53,5 @@ W4_CVC4: Solver = Solver("w4-cvc4")
W4_YICES: Solver = Solver("w4-yices")
W4_Z3: Solver = Solver("w4-z3")
W4_BOOLECTOR: Solver = Solver("w4-boolector")
W4_MATHSAT: Solver = Solver("w4-offline")
W4_OFFLINE: Solver = Solver("w4-offline")
W4_ABC: Solver = Solver("w4-any")

15
cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py
View File

@ -54,7 +54,7 @@ class CryptolTests(unittest.TestCase):
# self.assertEqual(add(BV(8,1), BV(8,2)), BV(8,3))
# self.assertEqual(add(BV(8,255), BV(8,1)), BV(8,0))
def test_sat(self):
def test_sat_and_prove(self):
c = self.c
# test a single sat model can be returned
rootsOf9 = c.sat('isSqrtOf9').result()
@ -81,6 +81,13 @@ class CryptolTests(unittest.TestCase):
# check for a valid condition
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]').result())
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.Z3).result())
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3).result())
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.W4_Z3.without_hash_consing()).result())
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]', solver.SBV_Z3).result())
self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.OFFLINE).result(), solver.OfflineSmtQuery)
self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.SBV_OFFLINE).result(), solver.OfflineSmtQuery)
self.assertIsInstance(c.prove('\\(x : [8]) -> x == reverse (reverse x)', solver.W4_OFFLINE).result(), solver.OfflineSmtQuery)
def test_check(self):
c = self.c
@ -146,6 +153,12 @@ class CryptolTests(unittest.TestCase):
res = c.safe("\\x -> x / (x:[8])").result()
self.assertEqual(res, [BV(size=8, value=0)])
res = c.safe("\\x -> x / (x:[8])", solver.Z3).result()
self.assertEqual(res, [BV(size=8, value=0)])
res = c.safe("\\x -> x / (x:[8])", solver.W4_Z3).result()
self.assertEqual(res, [BV(size=8, value=0)])
def test_many_usages_one_connection(self):
c = self.c

243
cryptol-remote-api/src/CryptolServer/Sat.hs
View File

@ -14,9 +14,12 @@ module CryptolServer.Sat
import qualified Argo.Doc as Doc
import Control.Applicative
import Control.Monad.IO.Class
import Data.Aeson ((.=), (.:), FromJSON, ToJSON)
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
@ -25,9 +28,11 @@ 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 Cryptol.Symbolic.SBV (proverNames, satProve, setupProver)
import qualified Cryptol.Symbolic.SBV as SBV
import qualified Cryptol.Symbolic.What4 as W4
import Cryptol.TypeCheck.AST (Expr)
import Cryptol.TypeCheck.Solve (defaultReplExpr)
@ -35,6 +40,8 @@ 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 =
@ -42,61 +49,134 @@ proveSatDescr =
[ 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 (Prover name) jsonExpr) =
do e <- getExpr jsonExpr
(_expr, ty, schema) <- liftModuleCmd (checkExpr e)
-- TODO validEvalContext expr, ty, schema
me <- getModuleEnv
let decls = deDecls (meDynEnv me)
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 = name
, pcVerbose = True -- verbose
, pcProverStats = timing
, pcExtraDecls = decls
, pcSmtFile = Nothing -- mfile
, pcExpr = checked
, pcSchema = schema
, pcValidate = False
, pcIgnoreSafety = False
}
sbvCfg <- liftIO (setupProver name) >>= \case
Left msg -> error msg
Right (_ws, sbvCfg) -> return sbvCfg
(_firstProver, res) <- liftModuleCmd $ satProve sbvCfg cmd
_stats <- liftIO (readIORef timing)
case res of
ProverError msg -> raise (proverError msg)
EmptyResult -> error "got empty result for online prover!"
CounterExample cexType es -> Invalid cexType <$> satResult es
ThmResult _ts -> pure Unsatisfiable
AllSatResult results ->
Satisfied <$> traverse satResult results
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
else if proverName `elem` SBV.proverNames then do
liftIO (SBV.setupProver proverName) >>= \case
Left msg -> raise $ proverError $ "error setting up " ++ proverName ++ ": " ++ msg
Right (_ws, sbvCfg) -> pure $ Left sbvCfg
else do
raise $ proverError
$ proverName ++ "is not a recognized solver;"
++ " please choose one of the following instead: "
++ (show $ W4.proverNames ++ SBV.proverNames)
offlineProveSat ::
-- | Prover name.
String ->
ProverCommand ->
-- | Whether hash consing is enabled.
Bool ->
CryptolCommand ProveSatResult
offlineProveSat proverName cmd hConsing = do
getProverConfig proverName >>= \case
Left sbvCfg -> do
result <- liftModuleCmd $ SBV.satProveOffline sbvCfg cmd
case result of
Left msg -> do
raise $ proverError $ "error setting up " ++ proverName ++ ": " ++ msg
Right smtlib -> pure $ OfflineSMTQuery $ T.pack smtlib
Right w4Cfg -> do
smtlibRef <- liftIO $ newIORef ("" :: Text)
result <- liftModuleCmd $
W4.satProveOffline w4Cfg hConsing False cmd $ \f -> do
withRWTempFile "smtOutput.tmp" $ \h -> do
f h
hSeek h AbsoluteSeek 0
contents <- TIO.hGetContents h
writeIORef smtlibRef contents
case result of
Just errMsg -> raise $ proverError $ "encountered an error using " ++ proverName ++ " to generate a query: " ++ errMsg
Nothing -> do
smtlib <- liftIO $ readIORef smtlibRef
pure $ OfflineSMTQuery smtlib
onlineProveSat ::
-- | Prover name.
String ->
ProverCommand ->
-- | Type of expression sat is being called for.
Bool ->
CryptolCommand ProveSatResult
onlineProveSat proverName cmd hConsing = do
res <-
getProverConfig proverName >>= \case
Left sbvCfg -> do
(_firstProver, res) <- liftModuleCmd $ SBV.satProve sbvCfg cmd
_stats <- liftIO (readIORef (pcProverStats cmd))
pure res
Right w4Cfg -> do
(_firstProver, res) <-
liftModuleCmd $ W4.satProve w4Cfg hConsing False {- warn uninterp fns -} cmd
_stats <- liftIO (readIORef (pcProverStats cmd))
pure res
case res of
ProverError msg -> raise (proverError msg)
EmptyResult -> raise $ proverError "got empty result for online prover!"
CounterExample cexType es -> Invalid cexType <$> convertSatResult es
ThmResult _ts -> pure Unsatisfiable
AllSatResult results ->
Satisfied <$> traverse convertSatResult results
where
satResult :: [(TValue, Expr, Value)] -> CryptolCommand [(JSONType, Expression)]
satResult es = traverse result es
result (t, _, v) = do
me <- readBack t v
case me of
Nothing -> error $ "type is not convertable: " ++ (show t)
Just e -> pure (JSONType mempty (tValTy t), e)
convertSatResult :: [(TValue, Expr, Value)] -> CryptolCommand [(JSONType, Expression)]
convertSatResult es = traverse result es
where
result :: forall b. (TValue, b, Value) -> CryptolCommand (JSONType, Expression)
result (t, _, v) = do
me <- readBack t v
case me of
Nothing -> error $ "type is not convertable: " ++ (show t)
Just e -> pure (JSONType mempty (tValTy t), e)
data ProveSatResult
= Unsatisfiable
| Invalid CounterExampleType [(JSONType, Expression)]
| Satisfied [[(JSONType, Expression)]]
| OfflineSMTQuery Text
instance ToJSON ProveSatResult where
toJSON Unsatisfiable = JSON.object ["result" .= ("unsatisfiable" :: Text)]
@ -124,25 +204,25 @@ instance ToJSON ProveSatResult where
| res <- xs
]
]
toJSON (OfflineSMTQuery smtlib) =
JSON.object [ "result" .= ("offline" :: Text)
, "query" .= smtlib
]
newtype ProverName = ProverName String
newtype Prover = Prover String
instance FromJSON Prover where
parseJSON =
JSON.withText "prover name" $
\txt ->
let str = T.unpack txt
in if str `elem` proverNames
then return (Prover str)
else empty
instance FromJSON ProverName where
parseJSON (Aeson.String name) = pure $ ProverName $ T.unpack name
parseJSON invalid =
Aeson.prependFailure "parsing prover name failed, "
(Aeson.typeMismatch "String" invalid)
data ProveSatParams =
ProveSatParams
{ queryType :: QueryType
, prover :: Prover
, prover :: ProverName
, expression :: Expression
, w4HashConsing :: Bool
}
instance FromJSON ProveSatParams where
@ -153,7 +233,12 @@ instance FromJSON ProveSatParams where
expression <- o .: "expression"
numResults <- (o .: "result count" >>= num)
queryType <- (o .: "query type" >>= getQueryType numResults)
pure ProveSatParams{queryType, prover, expression}
hConsing <- (o .:? "hash consing" >>= onOrOff) .!= True
pure $ ProveSatParams
{ queryType = queryType,
prover = prover,
expression = expression,
w4HashConsing = hConsing}
where
getQueryType numResults =
(JSON.withText "query" $
@ -169,13 +254,25 @@ instance FromJSON ProveSatParams where
case floatingOrInteger s of
Left (_float :: Double) -> empty
Right int -> pure (SomeSat int)) v)
onOrOff Nothing = pure Nothing
onOrOff (Just val) =
(JSON.withText "hash consing"
(\case
"on" -> pure $ Just True
"true" -> pure $ Just True
"yes" -> pure $ Just True
"off" -> pure $ Just False
"false" -> pure $ Just False
"no" -> pure $ Just False
_ -> empty)
val)
instance Doc.DescribedMethod ProveSatParams ProveSatResult where
parameterFieldDescription =
[("prover",
Doc.Paragraph ([Doc.Text "The SMT solver to use to check for satisfiability. I.e., one of the following: "]
++ (concat (map (\p -> [Doc.Literal (T.pack p), Doc.Text ", "]) proverNames))
++ (List.intersperse (Doc.Text ", ") $ map (Doc.Literal . T.pack) $ W4.proverNames ++ SBV.proverNames)
++ [Doc.Text "."]))
, ("expression",
Doc.Paragraph [ Doc.Text "The function to check for validity, satisfiability, or safety"
@ -197,15 +294,22 @@ instance Doc.DescribedMethod ProveSatParams ProveSatResult where
, Doc.Text ")."
]
)
, ("hash consing",
Doc.Paragraph [Doc.Text "Whether or not to use hash consing of terms (if available)."
, Doc.Literal "true", Doc.Text" to enable or ", Doc.Literal "false", Doc.Text " to disable."])
]
resultFieldDescription =
[ ("result",
Doc.Paragraph [ Doc.Text "A string (one of "
Doc.Paragraph [ Doc.Text "Either a string indicating the result of checking for validity, satisfiability, or safety"
, Doc.Text "---i.e., one of "
, Doc.Literal "unsatisfiable", Doc.Text ", "
, Doc.Literal "invalid", Doc.Text ", or "
, Doc.Literal "satisfied"
, Doc.Text ") indicating the result of checking for validity, satisfiability, or safety."
, Doc.Literal "satisfied", Doc.Text "---"
, Doc.Text "or the string literal "
, Doc.Literal "offline"
, Doc.Text " indicating an offline solver option was selected and the contents of the SMT query will be"
, Doc.Text " returned instead of a SAT result."
])
, ("counterexample type",
Doc.Paragraph $ onlyIfResultIs "invalid" ++
@ -224,7 +328,12 @@ instance Doc.DescribedMethod ProveSatParams ProveSatResult where
, Doc.Literal "expr", Doc.Text "field, indicating a expression in a model, and a "
, Doc.Literal "type", Doc.Text "field, indicating the type of the expression."
])
, ("query",
Doc.Paragraph $ onlyIfResultIs "offline" ++
[ Doc.Text "The raw textual contents of the requested SMT query which can inspected or manually"
, Doc.Text " given to an SMT solver."
])
]
where
onlyIfResultIs val = [ Doc.Text "Only used if the " , Doc.Literal "result"
, Doc.Text " is ", Doc.Literal val, Doc.Text "." ]
, Doc.Text " is ", Doc.Literal val, Doc.Text ". " ]

7
cryptol-remote-api/update_docs.sh Executable file
View File

@ -0,0 +1,7 @@
#! /bin/bash
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
pushd $DIR/docs
cabal run exe:cryptol-remote-api --verbose=0 -- doc > Cryptol.rst
popd

1
src/Cryptol/REPL/Command.hs
View File

@ -46,6 +46,7 @@ module Cryptol.REPL.Command (
-- Misc utilities
, handleCtrlC
, sanitize
, withRWTempFile
-- To support Notebook interface (might need to refactor)
, replParse