From fc33cbd55a2d8f70e19e9cbcb5bcc4365404c228 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 +- cabal.GHC-8.10.7.config | 2 +- cabal.GHC-9.2.4.config | 2 +- cabal.GHC-9.4.4.config | 2 +- cryptol-remote-api/docs/Cryptol.rst | 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 +++++++ 15 files changed, 39 insertions(+), 9 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/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config index 6fc6e450c..dc6a3adbc 100644 --- a/cabal.GHC-8.10.7.config +++ b/cabal.GHC-8.10.7.config @@ -207,7 +207,7 @@ constraints: any.BoundedChan ==1.0.3.0, s-cargot -build-example, any.safe ==0.3.19, any.safe-exceptions ==0.1.7.3, - any.sbv ==9.0, + any.sbv ==9.2, any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12.1, diff --git a/cabal.GHC-9.2.4.config b/cabal.GHC-9.2.4.config index 3d21ea619..95f60406b 100644 --- a/cabal.GHC-9.2.4.config +++ b/cabal.GHC-9.2.4.config @@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0, s-cargot -build-example, any.safe ==0.3.19, any.safe-exceptions ==0.1.7.3, - any.sbv ==9.0, + any.sbv ==9.2, any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12.1, diff --git a/cabal.GHC-9.4.4.config b/cabal.GHC-9.4.4.config index ea5146d5f..a8b341b6b 100644 --- a/cabal.GHC-9.4.4.config +++ b/cabal.GHC-9.4.4.config @@ -208,7 +208,7 @@ constraints: any.BoundedChan ==1.0.3.0, s-cargot -build-example, any.safe ==0.3.19, any.safe-exceptions ==0.1.7.3, - any.sbv ==9.0, + any.sbv ==9.2, any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12.1, diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst index 38f6144d8..54a4c6160 100644 --- a/cryptol-remote-api/docs/Cryptol.rst +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -557,7 +557,7 @@ Parameter fields ``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``. 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