mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Add CVC5 support
This patch: * Makes the necessary changes on the `cryptol` and `cryptol-remote-api` side needed add `cvc5`, `w4-cvc5`, and `sbv-cvc5` solvers. This requires SBV 9.1 or later to include the changes from LeventErkok/sbv#630, which re-exports CVC5-related functionality from all of the places that Cryptol imports from. * Adds a test case to ensure that basic CVC5 support works. * Updates the CI and Dockerfile to ensure that CVC5 is included from the `what4-solvers` bindists. Fixes #1503.
This commit is contained in:
parent
4c1c5fc681
commit
c810821d10
3
.github/ci.sh
vendored
3
.github/ci.sh
vendored
@ -77,7 +77,7 @@ install_system_deps() {
|
|||||||
cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
|
cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
|
||||||
export PATH=$BIN:$PATH
|
export PATH=$BIN:$PATH
|
||||||
echo "$BIN" >> "$GITHUB_PATH"
|
echo "$BIN" >> "$GITHUB_PATH"
|
||||||
is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices
|
is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices
|
||||||
}
|
}
|
||||||
|
|
||||||
check_docs() {
|
check_docs() {
|
||||||
@ -132,6 +132,7 @@ zip_dist_with_solvers() {
|
|||||||
sname="${name}-with-solvers"
|
sname="${name}-with-solvers"
|
||||||
cp "$(which abc)" dist/bin/
|
cp "$(which abc)" dist/bin/
|
||||||
cp "$(which cvc4)" dist/bin/
|
cp "$(which cvc4)" dist/bin/
|
||||||
|
cp "$(which cvc5)" dist/bin/
|
||||||
cp "$(which yices)" dist/bin/
|
cp "$(which yices)" dist/bin/
|
||||||
cp "$(which yices-smt2)" dist/bin/
|
cp "$(which yices-smt2)" dist/bin/
|
||||||
cp "$(which z3)" dist/bin/
|
cp "$(which z3)" dist/bin/
|
||||||
|
1
.github/workflows/ci.yml
vendored
1
.github/workflows/ci.yml
vendored
@ -315,6 +315,7 @@ jobs:
|
|||||||
.github/ci.sh install_system_deps
|
.github/ci.sh install_system_deps
|
||||||
.github/ci.sh deps bin/abc*
|
.github/ci.sh deps bin/abc*
|
||||||
.github/ci.sh deps bin/cvc4*
|
.github/ci.sh deps bin/cvc4*
|
||||||
|
.github/ci.sh deps bin/cvc5*
|
||||||
.github/ci.sh deps bin/yices-smt2*
|
.github/ci.sh deps bin/yices-smt2*
|
||||||
.github/ci.sh deps bin/z3*
|
.github/ci.sh deps bin/z3*
|
||||||
ghc_ver="$(ghc --numeric-version)"
|
ghc_ver="$(ghc --numeric-version)"
|
||||||
|
@ -30,10 +30,14 @@
|
|||||||
* Add a syntax highlight file for Vim,
|
* Add a syntax highlight file for Vim,
|
||||||
available in `syntax-highlight/cryptol.vim`
|
available in `syntax-highlight/cryptol.vim`
|
||||||
|
|
||||||
* Add `:new-seed` and `:set-seed` commands to the REPL.
|
* Add `:new-seed` and `:set-seed` commands to the REPL.
|
||||||
These affect random test generation,
|
These affect random test generation,
|
||||||
and help write reproducable Cryptol scripts.
|
and help write reproducable Cryptol scripts.
|
||||||
|
|
||||||
|
* Add support for the CVC5 solver, which can be selected with
|
||||||
|
`:set prover=cvc5`. If you want to specify a What4 or SBV backend, you can
|
||||||
|
use `:set prover=w4-cvc5` or `:set prover=sbv-cvc5`, respectively.
|
||||||
|
|
||||||
## Bug fixes
|
## Bug fixes
|
||||||
|
|
||||||
* Fix a bug in the What4 backend that could cause applications of `(@)` with
|
* Fix a bug in the What4 backend that could cause applications of `(@)` with
|
||||||
|
@ -40,6 +40,7 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
|
|||||||
RUN ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
|
RUN ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
|
||||||
# && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \
|
# && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \
|
||||||
&& ! $(cryptol -c ":s prover=cvc4" | 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=abc" | tail -n +2 | grep -q .) \
|
||||||
# && ! $(cryptol -c ":s prover=boolector" | 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 .)
|
&& ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .)
|
||||||
|
@ -25,7 +25,7 @@ predicates written in Cryptol against randomly-generated test vectors
|
|||||||
(in the style of
|
(in the style of
|
||||||
[QuickCheck](http://hackage.haskell.org/package/QuickCheck)). There is
|
[QuickCheck](http://hackage.haskell.org/package/QuickCheck)). There is
|
||||||
also a `:prove` command, which calls out to SMT solvers, such as
|
also a `:prove` command, which calls out to SMT solvers, such as
|
||||||
Yices, Z3, or CVC4, to prove predicates for all possible inputs.
|
Yices, Z3, CVC4, or CVC5, to prove predicates for all possible inputs.
|
||||||
|
|
||||||
# Getting Cryptol Binaries
|
# Getting Cryptol Binaries
|
||||||
|
|
||||||
|
@ -207,7 +207,7 @@ constraints: any.BoundedChan ==1.0.3.0,
|
|||||||
s-cargot -build-example,
|
s-cargot -build-example,
|
||||||
any.safe ==0.3.19,
|
any.safe ==0.3.19,
|
||||||
any.safe-exceptions ==0.1.7.3,
|
any.safe-exceptions ==0.1.7.3,
|
||||||
any.sbv ==9.0,
|
any.sbv ==9.2,
|
||||||
any.scientific ==0.3.7.0,
|
any.scientific ==0.3.7.0,
|
||||||
scientific -bytestring-builder -integer-simple,
|
scientific -bytestring-builder -integer-simple,
|
||||||
any.scotty ==0.12.1,
|
any.scotty ==0.12.1,
|
||||||
|
@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0,
|
|||||||
s-cargot -build-example,
|
s-cargot -build-example,
|
||||||
any.safe ==0.3.19,
|
any.safe ==0.3.19,
|
||||||
any.safe-exceptions ==0.1.7.3,
|
any.safe-exceptions ==0.1.7.3,
|
||||||
any.sbv ==9.0,
|
any.sbv ==9.2,
|
||||||
any.scientific ==0.3.7.0,
|
any.scientific ==0.3.7.0,
|
||||||
scientific -bytestring-builder -integer-simple,
|
scientific -bytestring-builder -integer-simple,
|
||||||
any.scotty ==0.12.1,
|
any.scotty ==0.12.1,
|
||||||
|
@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0,
|
|||||||
s-cargot -build-example,
|
s-cargot -build-example,
|
||||||
any.safe ==0.3.19,
|
any.safe ==0.3.19,
|
||||||
any.safe-exceptions ==0.1.7.3,
|
any.safe-exceptions ==0.1.7.3,
|
||||||
any.sbv ==9.0,
|
any.sbv ==9.2,
|
||||||
any.scientific ==0.3.7.0,
|
any.scientific ==0.3.7.0,
|
||||||
scientific -bytestring-builder -integer-simple,
|
scientific -bytestring-builder -integer-simple,
|
||||||
any.scotty ==0.12.1,
|
any.scotty ==0.12.1,
|
||||||
|
@ -557,7 +557,7 @@ Parameter fields
|
|||||||
|
|
||||||
|
|
||||||
``prover``
|
``prover``
|
||||||
The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``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``.
|
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``.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@ -52,6 +52,7 @@ class OfflineSolver(Solver):
|
|||||||
# Cryptol-supported SMT configurations/solvers
|
# Cryptol-supported SMT configurations/solvers
|
||||||
# (see Cryptol.Symbolic.SBV Haskell module)
|
# (see Cryptol.Symbolic.SBV Haskell module)
|
||||||
CVC4: OnlineSolver = OnlineSolver("cvc4")
|
CVC4: OnlineSolver = OnlineSolver("cvc4")
|
||||||
|
CVC5: OnlineSolver = OnlineSolver("cvc5")
|
||||||
YICES: OnlineSolver = OnlineSolver("yices")
|
YICES: OnlineSolver = OnlineSolver("yices")
|
||||||
Z3: OnlineSolver = OnlineSolver("z3")
|
Z3: OnlineSolver = OnlineSolver("z3")
|
||||||
BOOLECTOR: OnlineSolver = OnlineSolver("boolector")
|
BOOLECTOR: OnlineSolver = OnlineSolver("boolector")
|
||||||
@ -60,6 +61,7 @@ ABC: OnlineSolver = OnlineSolver("abc")
|
|||||||
OFFLINE: OfflineSolver = OfflineSolver("offline")
|
OFFLINE: OfflineSolver = OfflineSolver("offline")
|
||||||
ANY: OnlineSolver = OnlineSolver("any")
|
ANY: OnlineSolver = OnlineSolver("any")
|
||||||
SBV_CVC4: OnlineSolver = OnlineSolver("sbv-cvc4")
|
SBV_CVC4: OnlineSolver = OnlineSolver("sbv-cvc4")
|
||||||
|
SBV_CVC5: OnlineSolver = OnlineSolver("sbv-cvc5")
|
||||||
SBV_YICES: OnlineSolver = OnlineSolver("sbv-yices")
|
SBV_YICES: OnlineSolver = OnlineSolver("sbv-yices")
|
||||||
SBV_Z3: OnlineSolver = OnlineSolver("sbv-z3")
|
SBV_Z3: OnlineSolver = OnlineSolver("sbv-z3")
|
||||||
SBV_BOOLECTOR: OnlineSolver = OnlineSolver("sbv-boolector")
|
SBV_BOOLECTOR: OnlineSolver = OnlineSolver("sbv-boolector")
|
||||||
@ -68,6 +70,7 @@ SBV_ABC: OnlineSolver = OnlineSolver("sbv-abc")
|
|||||||
SBV_OFFLINE: OfflineSolver = OfflineSolver("sbv-offline")
|
SBV_OFFLINE: OfflineSolver = OfflineSolver("sbv-offline")
|
||||||
SBV_ANY: OnlineSolver = OnlineSolver("sbv-any")
|
SBV_ANY: OnlineSolver = OnlineSolver("sbv-any")
|
||||||
W4_CVC4: OnlineSolver = OnlineSolver("w4-cvc4")
|
W4_CVC4: OnlineSolver = OnlineSolver("w4-cvc4")
|
||||||
|
W4_CVC5: OnlineSolver = OnlineSolver("w4-cvc5")
|
||||||
W4_YICES: OnlineSolver = OnlineSolver("w4-yices")
|
W4_YICES: OnlineSolver = OnlineSolver("w4-yices")
|
||||||
W4_Z3: OnlineSolver = OnlineSolver("w4-z3")
|
W4_Z3: OnlineSolver = OnlineSolver("w4-z3")
|
||||||
W4_BOOLECTOR: OnlineSolver = OnlineSolver("w4-boolector")
|
W4_BOOLECTOR: OnlineSolver = OnlineSolver("w4-boolector")
|
||||||
|
@ -73,7 +73,7 @@ library
|
|||||||
pretty,
|
pretty,
|
||||||
prettyprinter >= 1.7.0,
|
prettyprinter >= 1.7.0,
|
||||||
process >= 1.2,
|
process >= 1.2,
|
||||||
sbv >= 8.10 && < 9.1,
|
sbv >= 9.1 && < 9.3,
|
||||||
simple-smt >= 0.9.7,
|
simple-smt >= 0.9.7,
|
||||||
stm >= 2.4,
|
stm >= 2.4,
|
||||||
strict,
|
strict,
|
||||||
|
@ -200,7 +200,7 @@ displayHelp errs = do
|
|||||||
, "via the `:edit` command"
|
, "via the `:edit` command"
|
||||||
]
|
]
|
||||||
)
|
)
|
||||||
, ( "SBV_{ABC,BOOLECTOR,CVC4,MATHSAT,YICES,Z3}_OPTIONS"
|
, ( "SBV_{ABC,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"
|
||||||
, [ "A string of command-line arguments to be passed to the"
|
, [ "A string of command-line arguments to be passed to the"
|
||||||
, "corresponding solver invoked for `:sat` and `:prove`"
|
, "corresponding solver invoked for `:sat` and `:prove`"
|
||||||
, "when using a prover via SBV"
|
, "when using a prover via SBV"
|
||||||
|
@ -81,6 +81,7 @@ doSBVEval m =
|
|||||||
proverConfigs :: [(String, SBV.SMTConfig)]
|
proverConfigs :: [(String, SBV.SMTConfig)]
|
||||||
proverConfigs =
|
proverConfigs =
|
||||||
[ ("cvc4" , SBV.cvc4 )
|
[ ("cvc4" , SBV.cvc4 )
|
||||||
|
, ("cvc5" , SBV.cvc5 )
|
||||||
, ("yices" , SBV.yices )
|
, ("yices" , SBV.yices )
|
||||||
, ("z3" , SBV.z3 )
|
, ("z3" , SBV.z3 )
|
||||||
, ("boolector", SBV.boolector)
|
, ("boolector", SBV.boolector)
|
||||||
@ -90,6 +91,7 @@ proverConfigs =
|
|||||||
, ("any" , SBV.defaultSMTCfg )
|
, ("any" , SBV.defaultSMTCfg )
|
||||||
|
|
||||||
, ("sbv-cvc4" , SBV.cvc4 )
|
, ("sbv-cvc4" , SBV.cvc4 )
|
||||||
|
, ("sbv-cvc5" , SBV.cvc5 )
|
||||||
, ("sbv-yices" , SBV.yices )
|
, ("sbv-yices" , SBV.yices )
|
||||||
, ("sbv-z3" , SBV.z3 )
|
, ("sbv-z3" , SBV.z3 )
|
||||||
, ("sbv-boolector", SBV.boolector)
|
, ("sbv-boolector", SBV.boolector)
|
||||||
|
@ -83,6 +83,7 @@ import qualified What4.SWord as SW
|
|||||||
import What4.Solver
|
import What4.Solver
|
||||||
import qualified What4.Solver.Boolector as W4
|
import qualified What4.Solver.Boolector as W4
|
||||||
import qualified What4.Solver.CVC4 as W4
|
import qualified What4.Solver.CVC4 as W4
|
||||||
|
import qualified What4.Solver.CVC5 as W4
|
||||||
import qualified What4.Solver.ExternalABC as W4
|
import qualified What4.Solver.ExternalABC as W4
|
||||||
import qualified What4.Solver.Yices as W4
|
import qualified What4.Solver.Yices as W4
|
||||||
import qualified What4.Solver.Z3 as W4
|
import qualified What4.Solver.Z3 as W4
|
||||||
@ -161,6 +162,7 @@ data W4ProverConfig
|
|||||||
proverConfigs :: [(String, W4ProverConfig)]
|
proverConfigs :: [(String, W4ProverConfig)]
|
||||||
proverConfigs =
|
proverConfigs =
|
||||||
[ ("w4-cvc4" , W4ProverConfig cvc4OnlineAdapter)
|
[ ("w4-cvc4" , W4ProverConfig cvc4OnlineAdapter)
|
||||||
|
, ("w4-cvc5" , W4ProverConfig cvc5OnlineAdapter)
|
||||||
, ("w4-yices" , W4ProverConfig yicesOnlineAdapter)
|
, ("w4-yices" , W4ProverConfig yicesOnlineAdapter)
|
||||||
, ("w4-z3" , W4ProverConfig z3OnlineAdapter)
|
, ("w4-z3" , W4ProverConfig z3OnlineAdapter)
|
||||||
, ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter)
|
, ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter)
|
||||||
@ -186,6 +188,11 @@ cvc4OnlineAdapter =
|
|||||||
AnOnlineAdapter "CVC4" W4.cvc4Features W4.cvc4Options
|
AnOnlineAdapter "CVC4" W4.cvc4Features W4.cvc4Options
|
||||||
(Proxy :: Proxy (W4.Writer W4.CVC4))
|
(Proxy :: Proxy (W4.Writer W4.CVC4))
|
||||||
|
|
||||||
|
cvc5OnlineAdapter :: AnAdapter
|
||||||
|
cvc5OnlineAdapter =
|
||||||
|
AnOnlineAdapter "CVC5" W4.cvc5Features W4.cvc5Options
|
||||||
|
(Proxy :: Proxy (W4.Writer W4.CVC5))
|
||||||
|
|
||||||
boolectorOnlineAdapter :: AnAdapter
|
boolectorOnlineAdapter :: AnAdapter
|
||||||
boolectorOnlineAdapter =
|
boolectorOnlineAdapter =
|
||||||
AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions
|
AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions
|
||||||
@ -195,6 +202,7 @@ allSolvers :: W4ProverConfig
|
|||||||
allSolvers = W4Portfolio
|
allSolvers = W4Portfolio
|
||||||
$ z3OnlineAdapter :|
|
$ z3OnlineAdapter :|
|
||||||
[ cvc4OnlineAdapter
|
[ cvc4OnlineAdapter
|
||||||
|
, cvc5OnlineAdapter
|
||||||
, boolectorOnlineAdapter
|
, boolectorOnlineAdapter
|
||||||
, yicesOnlineAdapter
|
, yicesOnlineAdapter
|
||||||
, AnAdapter W4.externalABCAdapter
|
, AnAdapter W4.externalABCAdapter
|
||||||
|
4
tests/issues/issue1503.cry
Normal file
4
tests/issues/issue1503.cry
Normal 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)
|
11
tests/issues/issue1503.icry
Normal file
11
tests/issues/issue1503.icry
Normal file
@ -0,0 +1,11 @@
|
|||||||
|
:l issue1503.cry
|
||||||
|
|
||||||
|
:set prover=w4-cvc5
|
||||||
|
:prove add_mul_lemma
|
||||||
|
|
||||||
|
// We avoid testing sbv-cvc5 for now, as using CVC5 with SBV on Windows will go
|
||||||
|
// likely go into an infinite loop.
|
||||||
|
// See https://github.com/LeventErkok/sbv/issues/644.
|
||||||
|
//
|
||||||
|
// :set prover=sbv-cvc5
|
||||||
|
// :prove add_mul_lemma
|
4
tests/issues/issue1503.icry.stdout
Normal file
4
tests/issues/issue1503.icry.stdout
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
Loading module Cryptol
|
||||||
|
Loading module Cryptol
|
||||||
|
Loading module Main
|
||||||
|
Q.E.D.
|
Loading…
Reference in New Issue
Block a user