Apply simplification to Imp and Iff connectives #4533
Conversation
| @@ -177,7 +177,7 @@ method EuclidGcd(X: pos, Y: pos) returns (gcd: pos) | |||
| // ------------------------------------------------------------------------------------------------------ | |||
| // The alternative definitions that follow allow the two cases in the GCD algorithm to look more similar. | |||
|
|
|||
| lemma GcdSubtractAlt(x: pos, y: pos) | |||
| lemma {:resource_limit "150e6"} GcdSubtractAlt(x: pos, y: pos) | |||
There was a problem hiding this comment.
Why is this now needed? If we're improving verification performance, why would we need to raise resource limits?
There was a problem hiding this comment.
That example was just incredibly brittle, and for things in that state it seems that any change, even one that overall should be a simplification, can throw things off the rails. Changing things as simple as the filenames passed in as arguments to the :captureState attribute was enough to change resource use by an order of magnitude. I've refactored that test, and one other, to be less brittle, and they no longer require raised resource limits.
The remaining failures will, I believe, be fixed by brittleness reductions included in #4597, so let's merge that one first, update this PR, and see if everything is good.
This one exhibited order-of-magnitude changes in resource use due to changes as simple as the length of the filename in each :captureState attribute. Making Gcd opaque reduced resource use by at least two orders of magnitude.
| @@ -303,7 +303,7 @@ abstract module {:disableNonlinearArithmetic} Std.Arithmetic.LittleEndianNat { | |||
|
|
|||
| /* The nat representation of a sequence and its least significant position are | |||
| congruent. */ | |||
| lemma LemmaSeqLswModEquivalence(xs: seq<digit>) | |||
| lemma {:resource_limit "10e6"} LemmaSeqLswModEquivalence(xs: seq<digit>) | |||
There was a problem hiding this comment.
Oh, it looks like it isn't! Good catch.
Boogie applies simplification to
Bpl.AndandBpl.Or, but not toBpl.ImpandBpl.Iff. Dafny provides wrapper methods to apply these connectives which also apply simplification toImpandIff; however they do not seem to be used consistently and are missing some cases.This PR replaces all direct usages of the Boogie methods
Bpl.And,Bpl.Or,Bpl.ImpandBpl.Iffwith wrappers from Dafny, and adds code to avoid addingtrueaxioms in cases where I noticed this happens. (A better solution might be to provide a single point for adding axioms where this check could be added.)By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.