The Caesar CLI
caesar verifier takes a HeyVL program as input and tries to determine whether it verifies.
caesar binary with
cargo build --release.
The executable can be found at
In the following, we just write
caesar for the executable.
--release for the a binary with less optimizations; the result will be in
Verify HeyVL files:
caesar file1.heyvl file2.heyvl ...
--raw indicates that input files consist only of a sequence HeyVL statements and that no declarations such as procedures are expected.
Timeouts and memory limits:
Set a timeout of 60 seconds using
Set a memory limit of 16000 megabytes with
Print tracing messages:
Caesar uses the
tracing library to print (debugging) information during its operation.
RUST_LOG environment variable to specify a filter, e.g.
export RUST_LOG="caesar=debug" or
Print intermediate data:
- With the
--print-parsedflag, Caesar pretty-prints the HeyVL code after parsing.
- With the
--print-coreflag, Caesar prints the HeyVL code after parsing, type-checking, and desugaring.
- With the
--print-theoremflag, Caesar prints the theorem that is encoded into SMT.
- With the
--print-smtflag, Caesar prints the SMT-LIB query for each verification task. You can also use
--smt-dir DIRwith a directory
DIRto have Caesar write the SMT-LIB queries to files in
The following command checks all examples that we know to work. It completes in about 20s on my machine.
cargo run --release -- --raw unif_gen1.heyvl rabin1.heyvl rabin2.heyvl brp1.heyvl geo1.heyvl
You can run the benchmark set with evaluations by executing
fish run-benchmarks.fish (fish shell is required).
One possible output of
fish run-benchmarks.fish | column -ts "," is the following:
Name Result Total Time VCgen Time SAT Check Time
brp1.heyvl IND 1.54s 0.02s 1.2s
brp2.heyvl OOM 17.39s
brp3.heyvl OOM 17.29s
fail-geo1.heyvl REF 0.18s 0s 0.03s
geo1.heyvl IND 0.2s 0s 0.04s
linear01.heyvl IND 0.19s 0s 0.02s
rabin1.heyvl IND 0.5s 0s 0.03s
rabin2.heyvl IND 13.95s 0.23s 10.1s
unif_gen1.heyvl IND 6.97s 0.02s 6.61s
unif_gen2.heyvl TO 0.52s
unif_gen3.heyvl TO 0.48s
unif_gen4.heyvl OOM 17.54s
Optimizations & Alternative Implementations
By default, Caesar uses a set of optimizations to speed up validity checking of verification conditions. You can experiment with them by disabling them and choosing between alternative implementations of some algorithms.
--help for more detailed information.
- Disabling quantifier elimination:
- Strict verification condition unfolding:
- Enable e-graph optimization:
--egraph. The result is currently not used for the SMT encoding.
Most of Caesar's behaviour can be changed with command-line flags, but there are three possible SMT encodings of the
EUReal type which must be chosen from at compile time.
--features datatype-eureal to build an executable that encodes
EUReal values using SMT-LIB datatypes instead of an encoding that uses a Boolean and a Real number directly.
Our experiments have shown that this is usually slower.
You can also compile with
--features datatype-eureal-funcs to use the datatype SMT-LIB encoding where additionally implementations of multiplications, additions, and less-than-or-equal relations are encoded as SMT-LIB functions.
This is the slowest encoding, but it's the easiest to read.