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

Draft: Add Bitwuzla support

Browse Source 
[ci skip]
This commit is contained in:
Ryan Scott 2024-01-09 10:16:17 -05:00
parent df4c9df73c
commit c41c222584
12 changed files with 50 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
CHANGES.md
View File

@ -64,6 +64,12 @@
default is used when the foreign implementation cannot be found, or if the FFI
is unavailable. The `:set evalForeign` REPL option controls this behavior.
## New features
* Add support for the Bitwuzla SMT solver, which can be selected with
`:set prover=bitwuzla`. If you want to specify a What4 or SBV backend, you can
use `:set prover=w4-bitwuzla` or `:set prover=sbv-bitwuzla`, respectively.
## Bug fixes
* Fixed #1455, making anything in scope of the functor in scope at the REPL as

3
Dockerfile
View File

@ -46,7 +46,8 @@ RUN ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=cvc5" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \
# && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=bitvector" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
&& ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .)
RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
&& cp -r lib/* rootfs/"${CRYPTOLPATH}"

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

@ -711,7 +711,7 @@ Parameter fields
``prover``
The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-cvc5``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, ``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-cvc5``, ``w4-yices``, ``w4-z3``, ``w4-bitwuzla``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``bitwuzla``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, ``sbv-yices``, ``sbv-z3``, ``sbv-bitwuzla``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.

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

@ -55,6 +55,7 @@ CVC4: OnlineSolver = OnlineSolver("cvc4")
CVC5: OnlineSolver = OnlineSolver("cvc5")
YICES: OnlineSolver = OnlineSolver("yices")
Z3: OnlineSolver = OnlineSolver("z3")
BITWUZLA: OnlineSolver = OnlineSolver("bitwuzla")
BOOLECTOR: OnlineSolver = OnlineSolver("boolector")
MATHSAT: OnlineSolver = OnlineSolver("mathsat")
ABC: OnlineSolver = OnlineSolver("abc")
@ -64,6 +65,7 @@ SBV_CVC4: OnlineSolver = OnlineSolver("sbv-cvc4")
SBV_CVC5: OnlineSolver = OnlineSolver("sbv-cvc5")
SBV_YICES: OnlineSolver = OnlineSolver("sbv-yices")
SBV_Z3: OnlineSolver = OnlineSolver("sbv-z3")
SBV_BITWUZLA: OnlineSolver = OnlineSolver("sbv-bitwuzla")
SBV_BOOLECTOR: OnlineSolver = OnlineSolver("sbv-boolector")
SBV_MATHSAT: OnlineSolver = OnlineSolver("sbv-mathsat")
SBV_ABC: OnlineSolver = OnlineSolver("sbv-abc")
@ -73,6 +75,7 @@ W4_CVC4: OnlineSolver = OnlineSolver("w4-cvc4")
W4_CVC5: OnlineSolver = OnlineSolver("w4-cvc5")
W4_YICES: OnlineSolver = OnlineSolver("w4-yices")
W4_Z3: OnlineSolver = OnlineSolver("w4-z3")
W4_BITWUZLA: OnlineSolver = OnlineSolver("w4-bitwuzla")
W4_BOOLECTOR: OnlineSolver = OnlineSolver("w4-boolector")
W4_OFFLINE: OfflineSolver = OfflineSolver("w4-offline")
W4_ABC: OnlineSolver = OnlineSolver("w4-abc")

12
cryptol-remote-api/python/tests/cryptol/test_smt.py
View File

@ -55,25 +55,31 @@ class TestSMT(unittest.TestCase):
ex_true = '\(x : [128]) -> negate (complement x + 1) == complement (negate x) + 1'
solvers = \
[solver.CVC4,
solver.CVC5,
solver.YICES,
solver.Z3,
#solver.BOOLECTOR,
solver.BITWUZLA,
solver.BOOLECTOR,
#solver.MATHSAT,
solver.ABC,
#solver.OFFLINE,
solver.ANY,
solver.SBV_CVC4,
solver.SBV_CVC5,
solver.SBV_YICES,
solver.SBV_Z3,
#solver.SBV_BOOLECTOR,
solver.SBV_BITWUZLA,
solver.SBV_BOOLECTOR,
#solver.SBV_MATHSAT,
solver.SBV_ABC,
#solver.SBV_OFFLINE,
solver.SBV_ANY,
solver.W4_CVC4,
solver.W4_CVC5,
solver.W4_YICES,
solver.W4_Z3,
#solver.W4_BOOLECTOR,
solver.W4_BITWUZLA,
solver.W4_BOOLECTOR,
#solver.W4_OFFLINE,
solver.W4_ABC,
solver.W4_ANY]

2
cryptol.cabal
View File

@ -85,7 +85,7 @@ library
mtl >= 2.2.1,
time >= 1.6.0.1,
panic >= 0.3,
what4 >= 1.4 && < 1.7
what4 >= 1.6 && < 1.7
if impl(ghc >= 9.0)
build-depends: ghc-bignum >= 1.0 && < 1.4

2
cryptol/Main.hs
View File

@ -200,7 +200,7 @@ displayHelp errs = do
, "via the `:edit` command"
]
)
, ( "SBV_{ABC,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"
, ( "SBV_{ABC,BITWUZLA,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"
, [ "A string of command-line arguments to be passed to the"
, "corresponding solver invoked for `:sat` and `:prove`"
, "when using a prover via SBV"

2
src/Cryptol/Symbolic/SBV.hs
View File

@ -88,6 +88,7 @@ proverConfigs =
, ("cvc5" , SBV.cvc5 )
, ("yices" , SBV.yices )
, ("z3" , SBV.z3 )
, ("bitwuzla" , SBV.bitwuzla )
, ("boolector", SBV.boolector)
, ("mathsat" , SBV.mathSAT )
, ("abc" , SBV.abc )
@ -98,6 +99,7 @@ proverConfigs =
, ("sbv-cvc5" , SBV.cvc5 )
, ("sbv-yices" , SBV.yices )
, ("sbv-z3" , SBV.z3 )
, ("sbv-bitwuzla" , SBV.bitwuzla )
, ("sbv-boolector", SBV.boolector)
, ("sbv-mathsat" , SBV.mathSAT )
, ("sbv-abc" , SBV.abc )

8
src/Cryptol/Symbolic/What4.hs
View File

@ -81,6 +81,7 @@ import qualified What4.SatResult as W4
import qualified What4.SFloat as W4
import qualified What4.SWord as SW
import What4.Solver
import qualified What4.Solver.Bitwuzla as W4
import qualified What4.Solver.Boolector as W4
import qualified What4.Solver.CVC4 as W4
import qualified What4.Solver.CVC5 as W4
@ -165,6 +166,7 @@ proverConfigs =
, ("w4-cvc5" , W4ProverConfig cvc5OnlineAdapter)
, ("w4-yices" , W4ProverConfig yicesOnlineAdapter)
, ("w4-z3" , W4ProverConfig z3OnlineAdapter)
, ("w4-bitwuzla" , W4ProverConfig bitwuzlaOnlineAdapter)
, ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter)
, ("w4-abc" , W4ProverConfig (AnAdapter W4.externalABCAdapter))
@ -193,6 +195,11 @@ cvc5OnlineAdapter =
AnOnlineAdapter "CVC5" W4.cvc5Features W4.cvc5Options
(Proxy :: Proxy (W4.Writer W4.CVC5))
bitwuzlaOnlineAdapter :: AnAdapter
bitwuzlaOnlineAdapter =
AnOnlineAdapter "Bitwuzla" W4.bitwuzlaFeatures W4.bitwuzlaOptions
(Proxy :: Proxy (W4.Writer W4.Bitwuzla))
boolectorOnlineAdapter :: AnAdapter
boolectorOnlineAdapter =
AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions
@ -203,6 +210,7 @@ allSolvers = W4Portfolio
$ z3OnlineAdapter :|
[ cvc4OnlineAdapter
, cvc5OnlineAdapter
, bitwuzlaOnlineAdapter
, boolectorOnlineAdapter
, yicesOnlineAdapter
, AnAdapter W4.externalABCAdapter

4
tests/issues/bitwuzla.cry Normal file
View File

@ -0,0 +1,4 @@
add_mul_lemma : Integer -> Integer -> Integer -> Integer -> Bit
add_mul_lemma m n p q =
(0 <= m /\ 0 <= n /\ 0 <= p /\ 0 <= q /\ n < q /\ p < m) ==>
(m * n + p < m * q)

8
tests/issues/bitwuzla.icry Normal file
View File

@ -0,0 +1,8 @@
// TODO RGS: File an issue about this, rename the name of this test accordingly
:l bitwuzla.cry
:set prover=w4-cvc5
:prove add_mul_lemma
:set prover=sbv-cvc5
:prove add_mul_lemma

5
tests/issues/bitwuzla.icry.stdout Normal file
View File

@ -0,0 +1,5 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
Q.E.D.
Q.E.D.