Skip to main content

The Caesar Tool

The caesar verifier takes a HeyVL program as input and tries to determine whether it verifies.

Compile the caesar binary with cargo build --release. The executable can be found at target/release/caesar. In the following, we just write caesar for the executable. Omit --release for the a binary with less optimizations; the result will be in target/debug/caesar.

Print help: caesar --help.

Verify HeyVL files: caesar file1.heyvl file2.heyvl ... Adding --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 --timeout 60. Set a memory limit of 16000 megabytes with --mem 16000.

Print tracing messages: Caesar uses the tracing library to print (debugging) information during its operation. Set the RUST_LOG environment variable to specify a filter, e.g. export RUST_LOG="caesar=debug" or export RUST_LOG="caesar::smt=trace".

Print intermediate data:

  • With the --print-parsed flag, Caesar pretty-prints the HeyVL code after parsing.
  • With the --print-core flag, Caesar prints the HeyVL code after parsing, type-checking, and desugaring.
  • With the --print-theorem flag, Caesar prints the theorem that is encoded into SMT.
  • With the --print-smt flag, Caesar prints the SMT-LIB query for each verification task. You can also use --smt-dir DIR with a directory DIR to have Caesar write the SMT-LIB queries to files in DIR.

More topics: