Skip to content

Commit

Permalink
Add Bitwuzla support
Browse files Browse the repository at this point in the history
Bumps the following submodules to bring in Bitwuzla-related changes:

* GaloisInc/cryptol#1786
* GaloisInc/crucible#1270

Fixes #2172.
RyanGlScott committed Jan 9, 2025
1 parent ac8ce90 commit bd095a4
Showing 18 changed files with 121 additions and 21 deletions.
4 changes: 3 additions & 1 deletion .github/ci.sh
Original file line number Diff line number Diff line change
@@ -75,7 +75,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" cvc5 && is_exe "$BIN" yices
is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices && is_exe "$BIN" bitwuzla && is_exe "$BIN" boolector
}

build_cryptol() {
@@ -121,6 +121,8 @@ zip_dist_with_solvers() {
# should be at least as portable (in terms of dynamic library
# dependencies) as the SAW binaries.
cp "$BIN/abc" dist/bin/
cp "$BIN/bitwuzla" dist/bin/
cp "$BIN/boolector" dist/bin/
cp "$BIN/cvc4" dist/bin/
cp "$BIN/cvc5" dist/bin/
cp "$BIN/yices" dist/bin/
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -2,6 +2,8 @@

## New Features

* Add a `bitwuzla` family of proof scripts that use the Bitwuzla SMT solver.

* Add a `:tenv` REPL command, which is like `:env` but prints the type
environment instead of the variable environment. `:t` is still short
for `:type`.
2 changes: 1 addition & 1 deletion deps/cryptol
Submodule cryptol updated 96 files
+47 −0 .github/check_book_update.sh
+7 −6 .github/ci.sh
+21 −0 .github/workflows/book.yml
+22 −4 .github/workflows/ci.yml
+8 −2 .github/workflows/docs.yml
+5 −0 .gitignore
+26 −3 CHANGES.md
+45 −1 CONTRIBUTING.md
+3 −2 Dockerfile
+6 −5 README.md
+114 −0 api-tests/Main.hs
+2 −0 cryptol-remote-api/CHANGELOG.md
+1 −1 cryptol-remote-api/Dockerfile
+5 −0 cryptol-remote-api/cryptol-eval-server/Main.hs
+1 −0 cryptol-remote-api/cryptol-remote-api.cabal
+5 −0 cryptol-remote-api/cryptol-remote-api/Main.hs
+32 −1 cryptol-remote-api/docs/Cryptol.rst
+9 −1 cryptol-remote-api/python/CHANGELOG.md
+6 −0 cryptol-remote-api/python/cryptol/commands.py
+12 −4 cryptol-remote-api/python/cryptol/connection.py
+16 −0 cryptol-remote-api/python/cryptol/cryptoltypes.py
+4 −0 cryptol-remote-api/python/cryptol/single_connection.py
+3 −0 cryptol-remote-api/python/cryptol/solver.py
+8 −0 cryptol-remote-api/python/cryptol/synchronous.py
+4 −4 cryptol-remote-api/python/poetry.lock
+2 −2 cryptol-remote-api/python/pyproject.toml
+18 −0 cryptol-remote-api/python/tests/cryptol/test-files/Modules.cry
+1 −1 cryptol-remote-api/python/tests/cryptol/test_filedeps.py
+33 −0 cryptol-remote-api/python/tests/cryptol/test_modules.py
+9 −3 cryptol-remote-api/python/tests/cryptol/test_smt.py
+1 −1 cryptol-remote-api/src/CryptolServer.hs
+4 −2 cryptol-remote-api/src/CryptolServer/Exceptions.hs
+2 −1 cryptol-remote-api/src/CryptolServer/FileDeps.hs
+84 −0 cryptol-remote-api/src/CryptolServer/Modules.hs
+60 −16 cryptol-repl-internal/REPL/Haskeline.hs
+0 −0 cryptol-repl-internal/REPL/Logo.hs
+58 −14 cryptol.cabal
+67 −22 cryptol/Main.hs
+1 −0 cve-reports/.gitignore
+116 −0 cve-reports/README.md
+11 −0 cve-reports/bin/cvecheck-all.sh
+48 −0 cve-reports/bin/cvecheck-build.sh
+34 −0 cve-reports/bin/cvecheck-consolidated.sh
+29 −0 cve-reports/bin/cvecheck-hs.sh
+28 −0 cve-reports/bin/cvecheck-py.sh
+4 −0 cve-reports/bin/variables.sh
+8 −8 dev/dev_setup.sh
+ docs/ProgrammingCryptol.pdf
+32 −0 docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
+3 −3 docs/ProgrammingCryptol/prims/Primitives.tex
+17 −6 docs/README.md
+132 −0 docs/RefMan/Project.rst
+1 −0 docs/RefMan/RefMan.rst
+1 −0 examples/AE.cry
+13 −4 lib/CryptolTC.z3
+38 −22 src/Cryptol/Eval/Generic.hs
+2 −1 src/Cryptol/IR/FreeVars.hs
+59 −27 src/Cryptol/ModuleSystem/Base.hs
+32 −13 src/Cryptol/ModuleSystem/Env.hs
+30 −14 src/Cryptol/ModuleSystem/Fingerprint.hs
+21 −12 src/Cryptol/ModuleSystem/Monad.hs
+2 −2 src/Cryptol/Parser.y
+12 −10 src/Cryptol/Parser/NoInclude.hs
+24 −8 src/Cryptol/Parser/ParserUtils.hs
+205 −0 src/Cryptol/Project.hs
+126 −0 src/Cryptol/Project/Cache.hs
+62 −0 src/Cryptol/Project/Config.hs
+211 −0 src/Cryptol/Project/Monad.hs
+138 −66 src/Cryptol/REPL/Command.hs
+16 −0 src/Cryptol/REPL/Monad.hs
+2 −0 src/Cryptol/Symbolic/SBV.hs
+8 −0 src/Cryptol/Symbolic/What4.hs
+3 −1 src/Cryptol/TypeCheck/Solver/SMT.hs
+4 −1 src/Cryptol/TypeCheck/TypePat.hs
+25 −6 src/Cryptol/Utils/Ident.hs
+5 −1 src/Cryptol/Utils/PP.hs
+3 −1 tests/docstrings/T02.cry
+9 −0 tests/docstrings/T12.cry
+2 −0 tests/docstrings/T12.icry
+4 −0 tests/docstrings/T12.icry.stdout
+2 −2 tests/examples/allexamples.icry.stdout
+2 −0 tests/issues/T1440.cry
+5 −5 tests/issues/T1440.icry.stdout
+1 −0 tests/issues/T1494_1.cry
+2 −2 tests/issues/T1494_1.icry.stdout
+5 −0 tests/issues/issue1749.cry
+2 −0 tests/issues/issue1749.icry
+4 −0 tests/issues/issue1749.icry.stdout
+3 −0 tests/issues/issue1786.cry
+7 −0 tests/issues/issue1786.icry
+5 −0 tests/issues/issue1786.icry.stdout
+2 −0 tests/issues/issue731.cry
+1 −1 tests/issues/issue731.icry
+1 −1 tests/issues/issue731.icry.stdout
+4 −0 tests/issues/issue_1314.icry
+301 −0 tests/issues/issue_1314.icry.stdout
14 changes: 10 additions & 4 deletions doc/manual/manual.md
Original file line number Diff line number Diff line change
@@ -1154,10 +1154,10 @@ sawscript> sat_print abc {{ \(x:[8]) -> x+x == x*2 }}
Sat: [x = 0]
~~~~

In addition to these, the `boolector`, `cvc4`, `cvc5`, `mathsat`, and `yices`
provers are available. The internal decision procedure `rme`, short for
Reed-Muller Expansion, is an automated prover that works particularly
well on the Galois field operations that show up, for example, in AES.
In addition to these, the `bitwuzla`, `boolector`, `cvc4`, `cvc5`, `mathsat`,
and `yices` provers are available. The internal decision procedure `rme`, short
for Reed-Muller Expansion, is an automated prover that works particularly well
on the Galois field operations that show up, for example, in AES.

In more complex cases, some pre-processing can be helpful or necessary
before handing the problem off to an automated prover. The
@@ -1220,6 +1220,8 @@ provers is to unfold everything before sending a goal to a prover.
However, with some provers it is possible to indicate that specific
named subterms should be represented as uninterpreted functions.

* `unint_bitwuzla : [String] -> ProofScript ()`

* `unint_cvc4 : [String] -> ProofScript ()`

* `unint_cvc5 : [String] -> ProofScript ()`
@@ -1241,6 +1243,8 @@ Note that each of the `unint_*` tactics have variants that are prefixed
with `sbv_` and `w4_`. The `sbv_`-prefixed tactics make use of the SBV
library to represent and solve SMT queries:

* `sbv_unint_bitwuzla : [String] -> ProofScript ()`

* `sbv_unint_cvc4 : [String] -> ProofScript ()`

* `sbv_unint_cvc5 : [String] -> ProofScript ()`
@@ -1251,6 +1255,8 @@ library to represent and solve SMT queries:

The `w4_`-prefixed tactics make use of the What4 library instead of SBV:

* `w4_unint_bitwuzla : [String] -> ProofScript ()`

* `w4_unint_cvc4 : [String] -> ProofScript ()`

* `w4_unint_cvc5 : [String] -> ProofScript ()`
Binary file modified doc/manual/manual.pdf
Binary file not shown.
5 changes: 3 additions & 2 deletions doc/tutorial/tutorial.md
Original file line number Diff line number Diff line change
@@ -295,8 +295,9 @@ this automatically, but for flexibility the `write_smtlib2` primitive
passes the given term through unchanged, because it might be used for
either satisfiability or validity checking.

The SMT-Lib export capabilities in SAWScript make use of the Haskell
SBV package, and support ABC, Boolector, CVC4, CVC5, MathSAT, Yices, and Z3.
The SMT-Lib export capabilities in SAWScript make use of the Haskell SBV
package, and support ABC, Bitwuzla, Boolector, CVC4, CVC5, MathSAT, Yices, and
Z3.

\newpage

10 changes: 10 additions & 0 deletions intTests/test_bitwuzla/test.saw
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
let
{{
add_mul_lemma : [64] -> [64] -> [64] -> Bit
add_mul_lemma m n p =
m * (n + p) == (m * n) + (m * p)
}};

prove bitwuzla {{ add_mul_lemma }};
prove sbv_bitwuzla {{ add_mul_lemma }};
prove (w4_unint_bitwuzla []) {{ add_mul_lemma }};
3 changes: 3 additions & 0 deletions intTests/test_bitwuzla/test.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
set -e

$SAW test.saw
11 changes: 11 additions & 0 deletions saw-remote-api/python/saw_client/proofscript.py
Original file line number Diff line number Diff line change
@@ -21,6 +21,14 @@ class ABC_SBV(Prover):
def to_json(self) -> Any:
return { "name": "sbv-abc" }

class Bitwuzla(Prover):
def to_json(self) -> Any:
return { "name": "bitwuzla" }

class Bitwuzla_SBV(Prover):
def to_json(self) -> Any:
return { "name": "sbv-bitwuzla" }

class Boolector(Prover):
def to_json(self) -> Any:
return { "name": "boolector" }
@@ -126,6 +134,9 @@ def to_json(self) -> Any:
rme = UseProver(RME())
boolector = UseProver(Boolector())

def bitwuzla(unints : List[str]) -> ProofTactic
return UseProver(Bitwuzla(unints))

def cvc4(unints : List[str]) -> ProofTactic:
return UseProver(CVC4(unints))

14 changes: 7 additions & 7 deletions saw-remote-api/python/saw_client/solver_cache.py
Original file line number Diff line number Diff line change
@@ -17,7 +17,7 @@
# External solvers supported by SBV (adapted from SBV.Solver)
Literal["ABC"],
Literal["Boolector"],
Literal["Bitwuzla"], # NOTE: Not currently supported by SAW
Literal["Bitwuzla"],
Literal["CVC4"],
Literal["CVC5"],
Literal["DReal"], # NOTE: Not currently supported by SAW
@@ -52,7 +52,7 @@ def __post_init__(self):

def load_solver_cache_entry(enc):
obj = cbor2.loads(enc)
opts = obj['opts'] if 'opts' in obj else []
opts = obj['opts'] if 'opts' in obj else []
t = dateutil.parser.isoparse(obj['t'])
return SolverCacheEntry(obj.get('cexs'), obj['nm'], obj['vs'], opts, t)

@@ -88,35 +88,35 @@ def __init__(self, path : Optional[str] = None):
def __len__(self):
with self.env.begin() as txn:
return txn.stat()['entries']

def __getitem__(self, k : bytes):
if not isinstance(k, bytes) or len(k) != 32:
raise ValueError("solver cache key must be a 256-bit `bytes` value")
with self.env.begin() as txn:
v = txn.get(cbor2.dumps(k))
if v is None: raise KeyError
return load_solver_cache_entry(v)

def __setitem__(self, k : bytes, v : SolverCacheEntry):
if not isinstance(k, bytes) or len(k) != 32:
raise ValueError("solver cache key must be a 256-bit `bytes` value")
if not isinstance(v, SolverCacheEntry):
raise ValueError("solver cache value must be a `SolverCacheEntry` object")
with self.env.begin(write = True) as txn:
txn.put(cbor2.dumps(k), cbor2.dumps(v, default=solver_cache_entry_encoder), overwrite=True)

def __delitem__(self, k : bytes):
if not isinstance(k, bytes) or len(k) != 32:
raise ValueError("solver cache key must be a 256-bit `bytes` value")
with self.env.begin(write = True) as txn:
txn.delete(cbor2.dumps(k))

def _iter(self, keys, values, fn):
with self.env.begin() as txn:
with txn.cursor() as curs:
for v in curs.iternext(keys, values):
yield fn(v)

def __iter__(self): yield from self._iter(True, False, cbor2.loads)
def keys (self): yield from self._iter(True, False, cbor2.loads)
def values (self): yield from self._iter(False, True, load_solver_cache_entry)
7 changes: 7 additions & 0 deletions saw-remote-api/src/SAWServer/ProofScript.hs
Original file line number Diff line number Diff line change
@@ -55,6 +55,7 @@ import Verifier.SAW.TermNet (merge)
data Prover
= RME
| SBV_ABC_SMTLib
| SBV_Bitwuzla [String]
| SBV_Boolector [String]
| SBV_CVC4 [String]
| SBV_CVC5 [String]
@@ -63,6 +64,7 @@ data Prover
| SBV_Z3 [String]
| W4_ABC_SMTLib
| W4_ABC_Verilog
| W4_Bitwuzla [String]
| W4_Boolector [String]
| W4_CVC4 [String]
| W4_CVC5 [String]
@@ -87,12 +89,14 @@ instance FromJSON Prover where
let unints = fromMaybe [] <$> o .:? "uninterpreted functions"
case name of
"abc" -> pure W4_ABC_SMTLib
"bitwuzla" -> SBV_Bitwuzla <$> unints
"boolector" -> SBV_Boolector <$> unints
"cvc4" -> SBV_CVC4 <$> unints
"cvc5" -> SBV_CVC5 <$> unints
"mathsat" -> SBV_MathSAT <$> unints
"rme" -> pure RME
"sbv-abc" -> pure SBV_ABC_SMTLib
"sbv-bitwuzla" -> SBV_Bitwuzla <$> unints
"sbv-boolector" -> SBV_Boolector <$> unints
"sbv-cvc4" -> SBV_CVC4 <$> unints
"sbv-cvc5" -> SBV_CVC5 <$> unints
@@ -101,6 +105,7 @@ instance FromJSON Prover where
"sbv-z3" -> SBV_Z3 <$> unints
"w4-abc-smtlib" -> pure W4_ABC_SMTLib
"w4-abc-verilog" -> pure W4_ABC_Verilog
"w4-bitwuzla" -> W4_Bitwuzla <$> unints
"w4-boolector" -> W4_Boolector <$> unints
"w4-cvc4" -> W4_CVC4 <$> unints
"w4-cvc5" -> W4_CVC5 <$> unints
@@ -277,6 +282,7 @@ interpretProofScript (ProofScript ts) = go ts
case p of
RME -> return $ SB.proveRME
SBV_ABC_SMTLib -> return $ SB.proveABC_SBV
SBV_Bitwuzla unints -> return $ SB.proveUnintBitwuzla unints
SBV_Boolector unints -> return $ SB.proveUnintBoolector unints
SBV_CVC4 unints -> return $ SB.proveUnintCVC4 unints
SBV_CVC5 unints -> return $ SB.proveUnintCVC5 unints
@@ -285,6 +291,7 @@ interpretProofScript (ProofScript ts) = go ts
SBV_Z3 unints -> return $ SB.proveUnintZ3 unints
W4_ABC_SMTLib -> return $ SB.w4_abc_smtlib2
W4_ABC_Verilog -> return $ SB.w4_abc_verilog
W4_Bitwuzla unints -> return $ SB.w4_unint_bitwuzla unints
W4_Boolector unints -> return $ SB.w4_unint_boolector unints
W4_CVC4 unints -> return $ SB.w4_unint_cvc4 unints
W4_CVC5 unints -> return $ SB.w4_unint_cvc5 unints
16 changes: 16 additions & 0 deletions src/SAWScript/Builtins.hs
Original file line number Diff line number Diff line change
@@ -1051,6 +1051,9 @@ wrapW4ProveExporter f unints path ext = do
proveABC_SBV :: ProofScript ()
proveABC_SBV = proveSBV SBV.abc

proveBitwuzla :: ProofScript ()
proveBitwuzla = proveSBV SBV.bitwuzla

proveBoolector :: ProofScript ()
proveBoolector = proveSBV SBV.boolector

@@ -1069,6 +1072,9 @@ proveMathSAT = proveSBV SBV.mathSAT
proveYices :: ProofScript ()
proveYices = proveSBV SBV.yices

proveUnintBitwuzla :: [String] -> ProofScript ()
proveUnintBitwuzla = proveUnintSBV SBV.bitwuzla

proveUnintBoolector :: [String] -> ProofScript ()
proveUnintBoolector = proveUnintSBV SBV.boolector

@@ -1092,6 +1098,9 @@ proveUnintYices = proveUnintSBV SBV.yices
w4_abc_smtlib2 :: ProofScript ()
w4_abc_smtlib2 = wrapW4Prover ABC [W4_SMTLib2] Prover.proveWhat4_abc []

w4_bitwuzla :: ProofScript ()
w4_bitwuzla = wrapW4Prover Bitwuzla [] Prover.proveWhat4_bitwuzla []

w4_boolector :: ProofScript ()
w4_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector []

@@ -1107,6 +1116,9 @@ w4_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5 []
w4_yices :: ProofScript ()
w4_yices = wrapW4Prover Yices [] Prover.proveWhat4_yices []

w4_unint_bitwuzla :: [String] -> ProofScript ()
w4_unint_bitwuzla = wrapW4Prover Bitwuzla [] Prover.proveWhat4_bitwuzla

w4_unint_boolector :: [String] -> ProofScript ()
w4_unint_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector

@@ -1125,6 +1137,10 @@ w4_unint_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5
w4_unint_yices :: [String] -> ProofScript ()
w4_unint_yices = wrapW4Prover Yices [] Prover.proveWhat4_yices

offline_w4_unint_bitwuzla :: [String] -> String -> ProofScript ()
offline_w4_unint_bitwuzla unints path =
wrapW4ProveExporter Prover.proveExportWhat4_bitwuzla unints path ".smt2"

offline_w4_unint_z3 :: [String] -> String -> ProofScript ()
offline_w4_unint_z3 unints path =
wrapW4ProveExporter Prover.proveExportWhat4_z3 unints path ".smt2"
38 changes: 38 additions & 0 deletions src/SAWScript/Interpreter.hs
Original file line number Diff line number Diff line change
@@ -2184,6 +2184,11 @@ primitives = Map.fromList
Current
[ "Use the ABC theorem prover to prove the current goal." ]

, prim "bitwuzla" "ProofScript ()"
(pureVal proveBitwuzla)
Current
[ "Use the Bitwuzla theorem prover to prove the current goal." ]

, prim "boolector" "ProofScript ()"
(pureVal proveBoolector)
Current
@@ -2214,6 +2219,13 @@ primitives = Map.fromList
Current
[ "Use the Yices theorem prover to prove the current goal." ]

, prim "unint_bitwuzla" "[String] -> ProofScript ()"
(pureVal proveUnintBitwuzla)
Current
[ "Use the Bitwuzla theorem prover to prove the current goal. Leave the"
, "given list of names as uninterpreted."
]

, prim "unint_z3" "[String] -> ProofScript ()"
(pureVal proveUnintZ3)
Current
@@ -2242,6 +2254,11 @@ primitives = Map.fromList
, "given list of names as uninterpreted."
]

, prim "sbv_bitwuzla" "ProofScript ()"
(pureVal proveBitwuzla)
Current
[ "Use the Bitwuzla theorem prover to prove the current goal." ]

, prim "sbv_boolector" "ProofScript ()"
(pureVal proveBoolector)
Current
@@ -2272,6 +2289,13 @@ primitives = Map.fromList
Current
[ "Use the Yices theorem prover to prove the current goal." ]

, prim "sbv_unint_bitwuzla" "[String] -> ProofScript ()"
(pureVal proveUnintBitwuzla)
Current
[ "Use the Bitwuzla theorem prover to prove the current goal. Leave the"
, "given list of names as uninterpreted."
]

, prim "sbv_unint_z3" "[String] -> ProofScript ()"
(pureVal proveUnintZ3)
Current
@@ -2388,6 +2412,13 @@ primitives = Map.fromList
Current
[ "Prove the current goal using What4 (Z3 backend)." ]

, prim "w4_unint_bitwuzla" "[String] -> ProofScript ()"
(pureVal w4_unint_bitwuzla)
Current
[ "Prove the current goal using What4 (Bitwuzla backend). Leave the"
, "given list of names as uninterpreted."
]

, prim "w4_unint_z3" "[String] -> ProofScript ()"
(pureVal w4_unint_z3)
Current
@@ -2447,6 +2478,13 @@ primitives = Map.fromList
, "using the What4 backend."
]

, prim "offline_w4_unint_bitwuzla" "[String] -> String -> ProofScript ()"
(pureVal offline_w4_unint_bitwuzla)
Current
[ "Write the current goal to the given file using What4 (Bitwuzla backend)"
, " in SMT-Lib2 format. Leave the given list of names as uninterpreted."
]

, prim "offline_w4_unint_z3" "[String] -> String -> ProofScript ()"
(pureVal offline_w4_unint_z3)
Current
2 changes: 1 addition & 1 deletion src/SAWScript/Prover/SBV.hs
Original file line number Diff line number Diff line change
@@ -2,7 +2,7 @@ module SAWScript.Prover.SBV
( proveUnintSBV
, proveUnintSBVIO
, SBV.SMTConfig
, SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector
, SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector, SBV.bitwuzla
) where

import System.Directory
Loading

0 comments on commit bd095a4

Please sign in to comment.