From 8e2f0b94c51f38f8fb0700ed5a869fac3a1b5ffa Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 27 Feb 2023 16:38:48 -0500 Subject: [PATCH] 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. --- .github/ci.sh | 3 ++- CHANGES.md | 6 +++++- Dockerfile | 1 + README.md | 2 +- cryptol-remote-api/python/cryptol/solver.py | 3 +++ cryptol.cabal | 2 +- cryptol/Main.hs | 2 +- src/Cryptol/Symbolic/SBV.hs | 2 ++ src/Cryptol/Symbolic/What4.hs | 8 ++++++++ tests/issues/issue1503.cry | 4 ++++ tests/issues/issue1503.icry | 7 +++++++ 11 files changed, 35 insertions(+), 5 deletions(-) create mode 100644 tests/issues/issue1503.cry create mode 100644 tests/issues/issue1503.icry diff --git a/.github/ci.sh b/.github/ci.sh index dc536f6a4..f36602ba9 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -77,7 +77,7 @@ install_system_deps() { cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT export PATH=$BIN:$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() { @@ -132,6 +132,7 @@ zip_dist_with_solvers() { sname="${name}-with-solvers" cp "$(which abc)" dist/bin/ cp "$(which cvc4)" dist/bin/ + cp "$(which cvc5)" dist/bin/ cp "$(which yices)" dist/bin/ cp "$(which yices-smt2)" dist/bin/ cp "$(which z3)" dist/bin/ diff --git a/CHANGES.md b/CHANGES.md index d12b799e6..608081c52 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -30,10 +30,14 @@ * Add a syntax highlight file for 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, 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 * Fix a bug in the What4 backend that could cause applications of `(@)` with diff --git a/Dockerfile b/Dockerfile index d9a7b5bc0..8d8d4c729 100644 --- a/Dockerfile +++ b/Dockerfile @@ -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 .) \ # && ! $(cryptol -c ":s prover=mathsat" | 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=z3" | tail -n +2 | grep -q .) diff --git a/README.md b/README.md index 826408440..0dd7d1ce2 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,7 @@ predicates written in Cryptol against randomly-generated test vectors (in the style of [QuickCheck](http://hackage.haskell.org/package/QuickCheck)). There is 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 diff --git a/cryptol-remote-api/python/cryptol/solver.py b/cryptol-remote-api/python/cryptol/solver.py index 99484fcf4..d8246e2a7 100644 --- a/cryptol-remote-api/python/cryptol/solver.py +++ b/cryptol-remote-api/python/cryptol/solver.py @@ -52,6 +52,7 @@ def without_hash_consing(self) -> 'OfflineSolver': # Cryptol-supported SMT configurations/solvers # (see Cryptol.Symbolic.SBV Haskell module) CVC4: OnlineSolver = OnlineSolver("cvc4") +CVC5: OnlineSolver = OnlineSolver("cvc5") YICES: OnlineSolver = OnlineSolver("yices") Z3: OnlineSolver = OnlineSolver("z3") BOOLECTOR: OnlineSolver = OnlineSolver("boolector") @@ -60,6 +61,7 @@ def without_hash_consing(self) -> 'OfflineSolver': OFFLINE: OfflineSolver = OfflineSolver("offline") ANY: OnlineSolver = OnlineSolver("any") 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_BOOLECTOR: OnlineSolver = OnlineSolver("sbv-boolector") @@ -68,6 +70,7 @@ def without_hash_consing(self) -> 'OfflineSolver': SBV_OFFLINE: OfflineSolver = OfflineSolver("sbv-offline") SBV_ANY: OnlineSolver = OnlineSolver("sbv-any") 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_BOOLECTOR: OnlineSolver = OnlineSolver("w4-boolector") diff --git a/cryptol.cabal b/cryptol.cabal index 7dac3d7e7..1f690cfb4 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -73,7 +73,7 @@ library pretty, prettyprinter >= 1.7.0, process >= 1.2, - sbv >= 8.10 && < 9.1, + sbv >= 9.1 && < 9.3, simple-smt >= 0.9.7, stm >= 2.4, strict, diff --git a/cryptol/Main.hs b/cryptol/Main.hs index 13e001b71..253c84937 100644 --- a/cryptol/Main.hs +++ b/cryptol/Main.hs @@ -200,7 +200,7 @@ displayHelp errs = do , "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" , "corresponding solver invoked for `:sat` and `:prove`" , "when using a prover via SBV" diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs index 7679c9648..2e3e895bc 100644 --- a/src/Cryptol/Symbolic/SBV.hs +++ b/src/Cryptol/Symbolic/SBV.hs @@ -81,6 +81,7 @@ doSBVEval m = proverConfigs :: [(String, SBV.SMTConfig)] proverConfigs = [ ("cvc4" , SBV.cvc4 ) + , ("cvc5" , SBV.cvc5 ) , ("yices" , SBV.yices ) , ("z3" , SBV.z3 ) , ("boolector", SBV.boolector) @@ -90,6 +91,7 @@ proverConfigs = , ("any" , SBV.defaultSMTCfg ) , ("sbv-cvc4" , SBV.cvc4 ) + , ("sbv-cvc5" , SBV.cvc5 ) , ("sbv-yices" , SBV.yices ) , ("sbv-z3" , SBV.z3 ) , ("sbv-boolector", SBV.boolector) diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs index 1e9f290df..d7cb7f8ca 100644 --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -83,6 +83,7 @@ import qualified What4.SWord as SW import What4.Solver import qualified What4.Solver.Boolector 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.Yices as W4 import qualified What4.Solver.Z3 as W4 @@ -161,6 +162,7 @@ data W4ProverConfig proverConfigs :: [(String, W4ProverConfig)] proverConfigs = [ ("w4-cvc4" , W4ProverConfig cvc4OnlineAdapter) + , ("w4-cvc5" , W4ProverConfig cvc5OnlineAdapter) , ("w4-yices" , W4ProverConfig yicesOnlineAdapter) , ("w4-z3" , W4ProverConfig z3OnlineAdapter) , ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter) @@ -186,6 +188,11 @@ cvc4OnlineAdapter = AnOnlineAdapter "CVC4" W4.cvc4Features W4.cvc4Options (Proxy :: Proxy (W4.Writer W4.CVC4)) +cvc5OnlineAdapter :: AnAdapter +cvc5OnlineAdapter = + AnOnlineAdapter "CVC5" W4.cvc5Features W4.cvc5Options + (Proxy :: Proxy (W4.Writer W4.CVC5)) + boolectorOnlineAdapter :: AnAdapter boolectorOnlineAdapter = AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions @@ -195,6 +202,7 @@ allSolvers :: W4ProverConfig allSolvers = W4Portfolio $ z3OnlineAdapter :| [ cvc4OnlineAdapter + , cvc5OnlineAdapter , boolectorOnlineAdapter , yicesOnlineAdapter , AnAdapter W4.externalABCAdapter diff --git a/tests/issues/issue1503.cry b/tests/issues/issue1503.cry new file mode 100644 index 000000000..ddf17798e --- /dev/null +++ b/tests/issues/issue1503.cry @@ -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) diff --git a/tests/issues/issue1503.icry b/tests/issues/issue1503.icry new file mode 100644 index 000000000..e6f2e9682 --- /dev/null +++ b/tests/issues/issue1503.icry @@ -0,0 +1,7 @@ +:l issue1503.cry + +:set prover=w4-cvc5 +:prove add_mul_lemma + +:set prover=sbv-cvc5 +:prove add_mul_lemma