Hide statements #5562
Hide statements #5562
Conversation
keyboardDrummer
added
the
run-integration-tests
| s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); | ||
|
|
||
| } else if (stmt is HideRevealStmt hideRevealStmt) { | ||
| hideRevealStmt.ResolvedStatements.ForEach(ss => Visit(ss, true, "a reveal statement")); |
There was a problem hiding this comment.
| hideRevealStmt.ResolvedStatements.ForEach(ss => Visit(ss, true, "a reveal statement")); | |
| hideRevealStmt.ResolvedStatements.ForEach(ss => Visit(ss, true, "a hide or reveal statement")); |
There was a problem hiding this comment.
Or perhaps it could look at the mode and say either "hide" or "reveal" depending on which it is.
| method Foo(x: nat) { | ||
| hide nat; | ||
| if (*) { | ||
| assert x > 0; // Fails because nat is hidden |
| var x := Bar(); | ||
| if (*) { | ||
| reveal Bar; | ||
| assert x; |
There was a problem hiding this comment.
I'm a little worried that the difference in behavior of hide on functions vs. methods could cause confusion. It makes sense in the "hide the things that are normally visible" interpretation, though, so I'm not too worried. :)
There was a problem hiding this comment.
The expect file for this input is:
revealMethods.dfy(8,11): Error: only functions and constants can be revealed
1 resolution/type errors detected in revealMethods.dfy
In the future I'll allow hide and revealing methods, and then a hidden method will also hide the ensures clause.
There was a problem hiding this comment.
Ah, right! Okay, then I have no concern. :)
| @@ -1032,9 +1031,6 @@ This list is not exhaustive but can definitely be useful to provide the next ste | |||
| <br><br>`assert A == B;`<br>`callLemma(x);`<br>`assert B == C;`<br> | [`calc == {`](#sec-calc-statement)<br> ` A;`<br> ` B;`<br> ` { callLemma(x); }`<br> ` C;`<br>`};`<br>`assert A == B;`<br>where the [`calc`](#sec-calc-statement) statement can be used to make intermediate computation steps explicit. Works with `<`, `>`, `<=`, `>=`, `==>`, `<==` and `<==>` for example. | |||
| <br><br><br>`assert A ==> B;` | `if A {`<br> ` assert B;`<br>`};`<br>`assert A ==> B;` | |||
| <br><br>`assert A && B;` | `assert A;`<br>`assert B;`<br>`assert A && B;` | |||
| <br>`assert P(x);`<br>where `P` is an [`{:opaque}`](#sec-opaque) predicate | [`reveal P();`](#sec-reveal-statement)<br>`assert P(x);`<br><br> | |||
| `assert P(x);`<br>where `P` is an [`{:opaque}`](#sec-opaque) predicate<br><br> | [`assert P(x) by {`](#sec-assert-statement)<br>[ ` reveal P();`](#sec-reveal-statement)<br>`}` | |||
| `assert P(x);`<br>where `P` is not an [`{:opaque}`](#sec-opaque) predicate with a lot of `&&` in its body and is assumed | Make `P` [`{:opaque}`](#sec-opaque) so that if it's assumed, it can be proven more easily. You can always [reveal](#sec-reveal-statement) it when needed. | |||
There was a problem hiding this comment.
Maybe change this to suggesting the use of hide?
There was a problem hiding this comment.
On the left it could say:
hide P;
...
assert P(x);and on the right then
hide P;
...
reveal P;
assert P(x);But I can't imagine anyone would need this tip.
There was a problem hiding this comment.
Yeah, I think you're probably right about that.
Description
opaque, can still be hidden usinghide. Hiding all functions can be done usinghide *. Hide statements can be used as an alternative to making functionsopaque, and unlikeopaque, allow optimizing the performance of specific proofs in your codebase without affecting the remaining code.How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.