Unexpected __CPROVER_exists failure

[azcwagner]

CBMC version: 5.12 (cbmc-5.12)
Operating system: macOS Catalina Version 10.15.4
Exact command line resulting in the issue: Run s2n_constant_time_equals proof.
What behaviour did you expect: Verification Successful.
What happened instead: assertion __CPROVER_exists failed.

To reproduce the issue, clone https://github.com/awslabs/s2n and include the changes in aws/s2n-tls#2072; then, go to s2n/tests/cbmc/proofs/s2n_safety_constant_time_equals dir. run make report and the report should be available under html/index.html in about 30 seconds.

In the report I observed the following result:

Warnings:
warning: ignoring exists

Errors
In tests/cbmc/proofs/s2n_safety_constant_time_equals/s2n_safety_constant_time_equals_harness.c
In s2n_safety_constant_time_equals_harness
Line 47:
[trace] assertion __CPROVER_exists {size_t i; (i >= 0 && i < len) && (a[i] != b[i])}

[azcwagner]

@tautschnig There seems to be some disagreement among the documentation about the status of quantifier support in CBMC.

• From http://www.cprover.org/cprover-manual/cbmc/assertions/:
  “Future CPROVER releases will support explicit quantifiers with a syntax that resembles Spec#"

• From http://www.cprover.org/cbmc/language_features.html:
  “Standard ANSI-C expressions are allowed as assertions; in addition, Spec#-style quantifiers are supported."

Are existential quantifiers fully supported in v5.12?

[martin-cs]

It depends on the back-end and how they are used (in an assume or an assert). In some cases they can be flattened into the implicit existential quantification around all variables. For example if you assert that something should hold for all values, then this equivalent to creating a non-deterministic variable for the failure point / witness and asserting that that particular case fails.

The inbuilt back-end makes a best-effort go at it : https://github.com/diffblue/cbmc/blob/develop/src/solvers/flattening/boolbv_quantifier.cpp I think @tautschnig is the last person to work on it.

The SMT back-end will translate them https://github.com/diffblue/cbmc/blob/develop/src/solvers/smt2/smt2_conv.cpp#L1786 but this is really old code and I don't know if it is much used. Maybe CVC4 might be able to handle what is generated?

HTH

[hannes-steffenhagen-diffblue]

Are existential quantifiers fully supported in v5.12?

I believe the answer to this question is a "not really, no". The syntax is supported and it works in some cases, but off the top of my head I can’t tell you exactly in what cases it works. As Martin says, the backend tries to convert the quantifiers into something it knows how to handle, but if that fails you get the warning message you report here.

[feliperodri]

@hannes-steffenhagen-diffblue I guess we conclude that "existential quantifiers are still not fully supported," correct? Should we close this issue?