Not completing verification of simple incorrect program in the presence of inductive axiom

[danyalette]

Hi there,

I'm not sure if this is a bug or not. Perhaps someone with more knowledge about Caesar could let me know.

When I attempt to check a simple incorrect program such as

proc t() -> ()
    pre 1.1
    post 1
{ }

the verifier hangs if the program also includes an inductive axiom such as

domain Exponentials {
    func exp(base: UReal, exponent: UInt): EUReal

    axiom exp_base forall base: UReal. exp(base, 0) == 1
    axiom exp_step forall base: UReal, exponent: UInt. exp(base, exponent + 1) == base * exp(base, exponent)
}

I am using Caesar via the VSCode extension.
Here are the logs from checking the above program without the axioms:

[Info - 13:16:17] Client: verifying document. file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl
2024-10-24T17:16:17.827597Z  INFO parse{path=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280) raw=false}:parse_decls{file_id=FileId(9)}: caesar::front::parser: close time.busy=1.16ms time.idle=1.01µs
2024-10-24T17:16:17.827612Z  INFO parse{path=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280) raw=false}: caesar::driver: close time.busy=1.18ms time.idle=2.08µs
2024-10-24T17:16:17.828607Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=972µs time.idle=425ns
2024-10-24T17:16:17.829581Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=950µs time.idle=544ns
2024-10-24T17:16:17.830681Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=1.08ms time.idle=674ns
2024-10-24T17:16:17.831651Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=947µs time.idle=576ns
2024-10-24T17:16:17.832625Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=957µs time.idle=393ns
2024-10-24T17:16:17.832662Z  INFO init_distributions: caesar::intrinsic::distributions: close time.busy=5.03ms time.idle=301ns
2024-10-24T17:16:17.832671Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:forward_declare: caesar::driver: close time.busy=573ns time.idle=310ns
2024-10-24T17:16:17.832676Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:resolve: caesar::driver: close time.busy=597ns time.idle=203ns
2024-10-24T17:16:17.832681Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:tycheck: caesar::driver: close time.busy=1.81µs time.idle=258ns
2024-10-24T17:16:17.832684Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:check_monotonicity: caesar::driver: close time.busy=443ns time.idle=222ns
2024-10-24T17:16:17.832687Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:apply_encodings: caesar::driver: close time.busy=241ns time.idle=205ns
2024-10-24T17:16:17.832693Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:desugar_spec_calls: caesar::driver: close time.busy=1.36µs time.idle=196ns
2024-10-24T17:16:17.832699Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:prepare_slicing: caesar::driver: close time.busy=3.97µs time.idle=218ns
2024-10-24T17:16:17.832702Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:vcgen: caesar::driver: close time.busy=501ns time.idle=200ns
2024-10-24T17:16:17.836904Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:unfolding: caesar::driver: close time.busy=4.20ms time.idle=605ns
2024-10-24T17:16:17.836930Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:apply_subst: caesar::vc::subst: close time.busy=12.0µs time.idle=612ns
2024-10-24T17:16:17.836936Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}: caesar::driver: Verification condition stats num_exprs=10 num_quants=0 depths=[n=5 m=4.800 σ=1.470 [2, 7] p50=7 p90=7 p99=7]
2024-10-24T17:16:17.836942Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:boolify: caesar::driver: close time.busy=1.22µs time.idle=265ns
2024-10-24T17:16:17.837906Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:translation to Z3: caesar::driver: close time.busy=11.7µs time.idle=598ns
2024-10-24T17:16:17.837928Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:simplify query: caesar::driver: close time.busy=15.1µs time.idle=215ns
2024-10-24T17:16:17.841254Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:SAT check:slice_while_failing:at most n statements{n=1 res=Sat}: caesar::slicing::solver: close time.busy=746µs time.idle=453ns
2024-10-24T17:16:17.841303Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:SAT check:slice_while_failing:at most n statements{n=0 min_accept=1 res=Unsat}: caesar::slicing::solver: close time.busy=40.0µs time.idle=294ns
2024-10-24T17:16:17.841307Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:SAT check:slice_while_failing: caesar::slicing::solver: slicing successful enabled=1 removed_statements=0 from_first_model=0
2024-10-24T17:16:17.841376Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:SAT check:slice_while_failing: caesar::slicing::solver: close time.busy=882µs time.idle=530ns
2024-10-24T17:16:17.841747Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}:SAT check: caesar::driver: close time.busy=3.82ms time.idle=302ns
2024-10-24T17:16:17.842001Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 280)::t}: caesar::driver: close time.busy=9.33ms time.idle=5.06ms
[Info - 13:16:17] Client: completed verification. file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl

Here are the logs from restarting the server and then checking with the above program with the axioms:

[Info - 13:13:43] Client: restarting.
[Info - 13:13:43] Client: stopping Caesar server.
[Error - 13:13:45] Stopping server timed out
[Error - 13:13:45] Client: failed to stop Caesar server: Error: Stopping the server timed out
[Info - 13:13:45] Client: starting Caesar server.
[Info  - 13:13:45] Client: created language client and registered callbacks.
Command: /home/danya/.config/Code/User/globalStorage/rwth-moves.caesar/caesar-download/caesar --language-server --debug --timeout 300
Caesar version: 2.0.8 (efe661459f8179566c8ed4b521bf99648e7548a3)
Build: Tue, 25 Jun 2024 13:37:56 +0000 (GitHub Actions)
Profile: release. Features: DEFAULT, STATIC_LINK_Z3. Target: x86_64-unknown-linux-gnu, Host: x86_64-unknown-linux-gnu
Z3 version: 4.12.1.0 3012293c35eadbfd73e5b94adbe50b0cc44ffb83 NOTFOUND

2024-10-24T17:13:45.214311Z  INFO caesar::servers::lsp: initializing with VSCode extension 2.0.8
[Error - 13:13:47] Server process exited with signal SIGKILL.
[Info - 13:13:14] Client: verifying document. file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl
2024-10-24T17:13:14.920783Z  INFO parse{path=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279) raw=false}:parse_decls{file_id=FileId(9)}: caesar::front::parser: close time.busy=1.49ms time.idle=625ns
2024-10-24T17:13:14.920797Z  INFO parse{path=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279) raw=false}: caesar::driver: close time.busy=1.51ms time.idle=1.65µs
2024-10-24T17:13:14.921735Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=910µs time.idle=401ns
2024-10-24T17:13:14.922740Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=985µs time.idle=362ns
2024-10-24T17:13:14.923652Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=898µs time.idle=406ns
2024-10-24T17:13:14.924601Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=934µs time.idle=328ns
2024-10-24T17:13:14.925528Z  INFO init_distributions:parse_bare_decl{file=<builtin>}: caesar::front::parser: close time.busy=915µs time.idle=303ns
2024-10-24T17:13:14.925564Z  INFO init_distributions: caesar::intrinsic::distributions: close time.busy=4.74ms time.idle=415ns
2024-10-24T17:13:14.925571Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::Exponentials}:forward_declare: caesar::driver: close time.busy=564ns time.idle=247ns
2024-10-24T17:13:14.925575Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:forward_declare: caesar::driver: close time.busy=259ns time.idle=191ns
2024-10-24T17:13:14.925580Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::Exponentials}:resolve: caesar::driver: close time.busy=2.75µs time.idle=206ns
2024-10-24T17:13:14.925583Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:resolve: caesar::driver: close time.busy=272ns time.idle=176ns
2024-10-24T17:13:14.925594Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::Exponentials}:tycheck: caesar::driver: close time.busy=8.86µs time.idle=191ns
2024-10-24T17:13:14.925597Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::Exponentials}:check_monotonicity: caesar::driver: close time.busy=100ns time.idle=203ns
2024-10-24T17:13:14.925599Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:tycheck: caesar::driver: close time.busy=316ns time.idle=164ns
2024-10-24T17:13:14.925601Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:check_monotonicity: caesar::driver: close time.busy=354ns time.idle=167ns
2024-10-24T17:13:14.925605Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::Exponentials}:apply_encodings: caesar::driver: close time.busy=776ns time.idle=179ns
2024-10-24T17:13:14.925607Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:apply_encodings: caesar::driver: close time.busy=129ns time.idle=165ns
2024-10-24T17:13:14.925609Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::Exponentials}: caesar::driver: close time.busy=26.9µs time.idle=4.78ms
2024-10-24T17:13:14.925615Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:desugar_spec_calls: caesar::driver: close time.busy=1.14µs time.idle=193ns
2024-10-24T17:13:14.925621Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:prepare_slicing: caesar::driver: close time.busy=4.32µs time.idle=201ns
2024-10-24T17:13:14.925624Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:vcgen: caesar::driver: close time.busy=558ns time.idle=198ns
2024-10-24T17:13:14.934345Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:unfolding: caesar::driver: close time.busy=8.72ms time.idle=583ns
2024-10-24T17:13:14.934374Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:apply_subst: caesar::vc::subst: close time.busy=9.35µs time.idle=817ns
2024-10-24T17:13:14.934380Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}: caesar::driver: Verification condition stats num_exprs=10 num_quants=0 depths=[n=5 m=4.800 σ=1.470 [2, 7] p50=7 p90=7 p99=7]
2024-10-24T17:13:14.934386Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:boolify: caesar::driver: close time.busy=1.11µs time.idle=228ns
2024-10-24T17:13:14.938350Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:translation to Z3: caesar::driver: close time.busy=8.63µs time.idle=877ns
2024-10-24T17:13:14.938386Z  INFO item{name=file:///home/danya/Documents/caesar/caesar/tests/domains/ohfive.heyvl (version 279)::t}:simplify query: caesar::driver: close time.busy=23.0µs time.idle=259ns

[Philipp15b]

Hello Danya! Thanks for your interest and the bug report. Indeed, you raise a real issue. The whole area of reasoning with quantifiers is something we're currently working on and I hope will improve in the next couple of weeks. Let me try to sort the underlying issues.

Root problem:
The SMT solver that we use (Z3) wants to give you a counter-example for verification. But this counter-example also needs to include a full definition for all uninterpreted functions (here: exp). Unfortunately, Z3 cannot give such a definition for a recursive function, even if your axioms fully specify the function.

Short-term fix:
I advise to set the timeout to a short duration (e.g. 10 seconds). Most problems either verify in that time or will be stuck forever. So we treat a timeout as a verification failure.

Our ideas for Caesar improvements:
There are a bunch of things that we are working on to improve this usability issue in Caesar.

• Don't include the function exp in a verification query that does not require it. To verify t, it is obvious that one does not need to think about exp at all. So we can simplify our SMT query to obtain counter-examples.
  • Doing this manually would fix your immediate issue. We also sometimes put only the relevant definitions in one .heyvl file to avoid this issue.
  • Ideally, this should be done automatically. We'll address this in an upcoming change.
  • But more interesting and common are cases are those where exp is required for a verification problem. The following bullet points address those.
• Many deductive verifiers such as the ones based on Boogie (e.g. Dafny, but also Viper) implement a technique called limited functions to make it easier for the SMT solver to return counterexamples. This is currently a work in progress in PR Limited functions #54 by @ole-thoeb.
  • The counterexamples might be false ones, i.e. not actually counterexamples in the formal weakest pre-expectation setting, but a relaxed one. For example, one might get values for the initial state with which you wouldn't get a counterexample on paper.
  • This seems to be something that works pretty well in practice, so we're implementing that.
• Starting on Nov 1st, we have a project that looks into using @ffrohn's work on SMT with Exponentials in Caesar. This would give us a built-in definition for exponentials in Caesar, and we'd get true counter-examples and easier verification without having to specify axioms manually. Early tests suggest this works pretty well.

Let me know if this is helpful to you. I'm also always happy to have a Zoom meeting to chat about Caesar usage (just send an email to [email protected]).

[danyalette]

Hi Phillipp,

Thanks so much for the detailed answer! All your suggestions are helpful. As you might imagine, I am most interested in the case in which the uninterpreted function plays a role in the program I am attempting to verify.

I have not had a chance to dig into the Caesar code to see what exactly is generated as a Z3 query. However, I suppose I imagined that the declaration of an uninterpreted function f could be understood in the context of proc(x) pre a post b as "exists f that satisfies these axioms and forall x. a <= b". In this case, the negation (which should be unsatisfiable iff the verification condition is valid) would be "forall f. satisfying these axioms => exists x. a > b". Under this interpretation, a model witnessing the satisfiability of the latter would not involve giving a definition for f. Intuitively, this makes sense to me because, when I declare an uninterpreted function with axioms, I generally have a specific one in mind, as in the case of exp.

I appreciate your offer to have a Zoom. I am OK for now but I may be in touch in the future :)

Best wishes,

Danya

[Philipp15b]

Hello Danya,

I think there might be a small mistake there. If you have an uninterpreted function f, some axioms, and a proc p(x) -> (y) pre a post b { body }, then the corresponding verification query is something like the following. We want to check that this statement is true:

∀f. axioms ⇒ (∀x. (pre ≤ vp[p](post)))

where vp is the verification pre-expectation transformer from our paper (think weakest pre-condition).

For the SMT solver, we ask for a counterexample to this formula. If there is no counterexample, we know the formula is a theorem.
Thus, the SMT query that we send is of the following form:

∃f. axioms && (∃x. (pre && pre > vp[p](post)))

Notice that this is just an existential query.

In short:

• A counterexample is just an interpretation of f satisfying the axioms and inputs x, such that pre > vp[p](post).
• To verify p, we check against all possible interpretations for f that satisfy the axioms.

The fact that a counterexample only requires giving one definition of f makes it very puzzling that the SMT solver struggles to give a definition of exp in a counter-example. After all, we've fully specified it! But it seems that's not as easy as it looks like in the general case :)

Checking against all possible interpretations of f is nice because this allows only partially specifying uninterpreted functions. While exp is usually axiomatized so that it is unique (just via its recursive definition), you might also want to say e.g. that f is just any monotonic function without being more concrete. Then a counterexample includes a definition of one monotonic function.

All of this is done just like in other deductive verifiers such as Dafny/Boogie. Except for the quantitative vp, it's very much the same.

I hope that helps!
Best,
Philipp

[danyalette]

Hi Philipp, thanks for the detailed reply! I inferred that what you described was the case; I just expected a different behaviour 😄