moves-rwth / caesar

Deductive verification infrastructure for probabilistic programs

Caesar

Caesar is a deductive verification platform for probabilistic programs. It accepts input in a verification language called HeyVL. Caesar generates so-called verification conditions of the HeyVL input program(s). These verification conditions are in the form of logical formulas of a logic we call HeyLo. If the verification conditions are valid, then we say the HeyVL program verifies. If a counter-example is found, Caesar will reject the input program.

This is research software and we're still working on a nice user interface, documentation, and fixing bugs. Do not hesitate to open an issue or send an email to [email protected] with questions or ideas. I am also happy to discuss anything via Zoom as well!

The documentation is available at www.caesarverifier.org. Start at with the introduction, then walk through the getting started guide.

We have an OOPSLA 2023 paper on Caesar and its theory: A Deductive Verification Infrastructure for Probabilistic Programs. You can find the preprint on arxiv.

There is also a development guide if you want to work on Caesar itself.

caesar's Issues

vscode extension: better status bar information

Right now, when verification fails, the status bar shows "Verified". This is very confusing. Ideally, we'd distinguish between verification errors, type errors, syntax errors, timeouts, and successful verification.

In addition, the extension seems to show "Et tu Brute?" in the status bar if the verifier never started. This is the case if the server does not automatically start (which is unfortunately the default right now). If the server never started, we should print something like "Caesar not started".

better error message for proc calls whose results are assigned to input variables

Right now, if an input variable is assigned the result of a proc/dist call, then the error message will be confusing, saying e.g. expected Bool, found (Bool).

Example:

proc test(input: Bool) -> () {
    input = flip(0.5)
}

VSCode Extension: Bundling and output directory cleanup

This extension consists of 245 files, out of which 186 are JavaScript files. For performance reasons, you should bundle your extension: https://aka.ms/vscode-bundle-extension . You should also exclude unnecessary files by adding them to your .vscodeignore: https://aka.ms/vscode-vscodeignore

Also, the out directory seems not to be cleaned when the extension is built, possibly resulting in (very) old files being included in the extension package.

VSCode Extension: Binary name on Windows is missing 'exe'

On Windows, the binary name is caesar.exe and not just caesar. After the automatic download, the extension will not find caesar and will uninstall itself again. Currently, there are no logs about this happening and there's no error message.

vscode extension: handle timeouts and show waiting icon

Right now, timeouts crash the LSP server, leading to ugly errors and requiring a restart. We should properly a) indicate with a gutter icon that verification is currently running and b) just had a timeout. In addition, a timeout shouldn't clear all verification information from the UI.

Document expression syntax

We should really have more documentation on all the supported expressions.

vc explanations: somehow indicate side conditions?

at the moment, our vc explanations for high-level constructs such as while loops or proc calls just show the invariant/pre as the explanation, but they don't ever show that there are side-conditions. ideally, we'd somehow also show that e.g. I <= Phi(I) must hold, referencing the loop body's pre explanation as part of Phi(I).

Drop z3-sys dependency

We can now get the Z3 version directly from the high-level API: prove-rs/z3.rs@a1d6458

CI: Extension publishing fails

See https://github.com/moves-rwth/caesar/actions/runs/9150425689/job/25155182535.

I've tried to publish locally, and now I'm getting again:

This extension consists of 1356 files, out of which 830 are JavaScript files. For performance reasons, you should bundle your extension: https://aka.ms/vscode-bundle-extension . You should also exclude unnecessary files by adding them to your .vscodeignore: https://aka.ms/vscode-vscodeignore

See #16.

The CI script seems to have this --out parameter for which I cannot find the documentation?

npm run package -- --out caesar-${{ inputs.version }}.vsix

Add support for other SMT solvers

We should add support for other SMT solvers, especially for the final SAT call. I don't think we need to adapt stuff like the lazy unfolder just now.

Support for other solvers should be implemented by calling external binaries (not via some native API). Then we could experiment with CVC5 and @ffrohn's SwInE tool. Especially the latter could be extremely useful if we could obtain counterexamples when reasoning about exponentials.

procs documentation is kinda bad

The documentation on procedures does not explain in an approachable way what exactly a specification means and how it can be formally understood. The page mostly talks about the lowering to "core HeyVL", but not the high-level interpretation.

Update Z3 dependency

With the upcoming z3.rs release, we should do the following:

• Check for regressions due to the solver update
• Use the new high-level Version type (see prove-rs/z3.rs@a1d6458) and drop our explicit z3-sys dependency
• Update our Real pretty-printing code to support printing non-rational values (see prove-rs/z3.rs@42bae5f)

vc explanations: add support for the unroll proof rule

It would be really useful to get nicely formatted output from --explain-vc for loops annotated with the @unroll proof rule as well.

vc explanations: handle proc calls

It seems that vc explanations crashes when proc calls are used in the code.

Deprecate usage of minus operator for monus

The - symbol for monus on expectations has been confusing on many occasions already. We should really warn on its usage and add a separate operator/function for monus to be more explicit.

calculus annotations: check proc calls

According to the documentation, calculus annotations do not check that proc calls are sound: they do not check that a proc only calls procs (and vice versa for coprocs), and neither do they check that the callee's calculus corresponds to the caller's calculus. Warnings/errors for these should be added.

Print proper error message when while loops are used without proof rule

Right now, Caesar has a panic when it tries to vcgen for programs that contain while loops. A nice DIagnostic would be much better.

slicing and tick statements

Right now, we do not handle slice tick statements by default. However, I think we might want to slice tick statements by default as well, just only after all assertions have been determined as guaranteed to be irrelevant for an error. In addition, we need to check that we don't introduce regressions (looking at the coupon collector) that could break by another statement being sliced.

add support for power operator

Caesar should have support for a power operator. Z3 even supports powers on Real and Int types natively! The exponent is always a non-negative integer if I understood correctly.

Since we often use powers in expectations, our implementation should support EUReal bases as well. Extra cases: \infty^0 == 0 and \infty^exponent == \infty for exponent != 0.

Update to new ariadne version

The new version of ariadne directly supports byte spans, which could allow us to simplify our own diagnostic code. See https://github.com/zesterer/ariadne/blob/main/CHANGELOG.md.

vc explanations: incorporate counterexamples

When verification fails with a counterexample, the vc explanations could also be printed to the user with values for those variables that we get from the counterexample. this would be a more localized version of the pre-quantity that is printed for the whole proc.

Rewrite tests to use proof rule annotations

At some point we should rewrite the tests in tests and pgcl/examples-pgcl/ to use our new proof rule annotations by @umutdural. They should also use the new calculus annotations from #7.

This would allow us to remove the pgcl2heyvl tool from the code. It would also prevent issues like f68c682.

core vc explanations: pre from induction is not shown

For some reason, the computed pre from code generated by the @induction proof rule is not shown by the --explain-core-vc option. It works with the --explain-vc option. Debugging suggests the code thinks that the first statement of the generated code is not contained in its own surrounding block, but I do not know why.

slicing: algorithm incorrectly assumes at least one assert is needed for an error

The slicing for errors algorithm incorrectly assumes that at least one assert is needed to obtain an error. It therefore sets a search interval of 1..slice_vars for the PartialMinimizer. However, when the slice solver actually returns a counterexample with zero slice vars enabled, then PartialMinimizer::add_result will encounter an assertion failure since zero is not in the search interval.

An input program that crashes Caesar because of this is the following:

coproc cex() -> ()
    pre 0
    post 0
{
    tick 1
}

vc explanations: add support for guarded fraction normal form

To better be able to see patterns in the generated pres, especially from the @unroll proof rule (#19), a normalization of the pre could help. A normal form in the style of [b1] * quant1 * poly(vars)/poly(vars) + ... [bn] * quantn * poly(vars)/poly(vars) where poly(vars) are multivariate polynomials in terms of program variables.

For this normal form, expressions that cannot be simplified (such as a function call exp(2, x)) would be treated as another variable in the polynomial, and we would get e.g. [true] * 1 * exp(2, x).