Potential Unsoundness in Prelude.bpl #4400
Assignees
Labels
during 3: execution of incorrect program
An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec
introduced: pre-2009
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
logic
An inconsistency in Dafny's logic (e.g. in the Boogie prelude)
priority: not yet
Will reconsider working on this when we're looking for work
Comments
|
I am not quite sure how Dafny uses Using Of course this does not verify using z3, since it is not an FOL ATP. But If I run this with Looks like the symbol names are scrambled, and the axioms are only selectively included in a deeply nested |
atomb
added
logic
|
Thank you for investigating and reporting this! For completeness, would you be able to list the entire set of axioms that you removed? |
|
Yes sir. I added I think it is possible that these sets are not minimized. I did not attempt to perform deeper manual inspection other than the first one. |
|
I was looking at the refutation and noticed the following, maybe it would provide some context. The multiset is encoded as an array from
which eventually becomes a contradiction
i.e., From the prelude This implies Combining with the refutation above, we end up with I do not see why this axiom is not doing its job though, maybe related to polymorphism + boxes? Btw it might be interesting to see what happens with the other encodings. Dafny does not currently use the monomorphic encoding (which Boogie uses by default). Could you perhaps try the following?
I believe this experiment would not work directly from Dafny due to pruning, and there is currently no way to disable pruning through an option in Dafny. Printing a Boogie file and using Boogie on that should work though! In Boogie pruning is off by default. |
|
Interesting,
The remaining two asserts correspond to the same two axioms reported above. If I remove all four, |
|
Thanks for finding this bug, @yizhou7! Here is a different example that lets you prove procedure False()
ensures false;
{
var bx: Box;
var s: MultiSet Box;
var u: MultiSet Box;
bx := $Box(0);
s := MultiSet#Singleton(bx);
s := s[bx := -10];
u := MultiSet#UnionOne(s, bx);
assert u[bx] == -9; // by "union-ing increases count by one" axiom
assert 0 <= u[bx]; // by "pure containment axiom" axiom
assert false;
}The multiset axioms seem to be missing some kind of |
|
For the example above that @RustanLeino gave, changing the containment axiom as follows fixes this, but I suspect this is not the only issue (and probably not a good fix): (Added |
keyboardDrummer
added
the
during 3: execution of incorrect program
keyboardDrummer
added
the
priority: not yet
|
The following stripped down version of the prelude is kind of like iterations 1 and 2 above, and verifies (proving false) with Vampire. A very interesting thing I observed. however, is that removing the The comment after it shows that someone was already skeptical about it. :) I'm going to see whether anything fails with the definition for |
|
Is it the minimal file already, i.e. if you remove any other declarations, will it stop managing proving false? |
Yes, unless I'm misremembering. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I naively took
Prelude.bpland added this to the end (otherwiseboogiewould not emit an SMT file).I then ran
boogie(version3.0.0) to log the generated SMT query (dotnetversion6.0.412):I ran this with
vampire(version4.8), it reported that a refutation (unsat):From the proof, it seems like these two axioms from
Prelude.bplare causing the problem:I removed the two conflicting asserts from the SMT file, a new refutation was found. In fact there seemed to be 4 disjoint sets of conflicting asserts. That is, I repeated the following until
vampirewas not able to immediately find a refutation, and 4 disjoint sets of asserts were reported:vampirefinds a new refutationThe text was updated successfully, but these errors were encountered: