Fix: Opaque functions guaranteed to be opaque until revealed #3779
Conversation
…fny-lang/dafny into fix-3719-opaque-leaked-lambda
There was a problem hiding this comment.
Nice improvement! I suspect it could be valuable to recommend Dafny developers put assert false on any path they expect to be unreachable, as a general practice. It makes things clearer, and sometimes makes proofs faster. And, in the case where we warn about unreachable code, it would be easy to filter out those that explicitly included assert false.
| C, Processed := C - {v}, Processed + {v}; | ||
| ghost var pathToV := Find(source, v, paths); | ||
|
|
There was a problem hiding this comment.
Is there a reason to remove these blank lines?
There was a problem hiding this comment.
No indeed that does not improve verifiability :-)
| } | ||
| } | ||
| } | ||
| } | ||
| } | ||
| } | ||
|
|
||
| private void MaybeCreateRevealableConstant(Function f) { |
There was a problem hiding this comment.
The "Maybe" part of the name suggests to me that it may or may not be appropriate to have a revealable constant at all. But here it just indicates that the operation is idempotent--it's performed only once. For that purpose, I suggest still just naming the method CreateRevealableConstant.
Test/git-issues/git-issue-3719.dfy
Outdated
| opaque function inc(x:nat) : nat { x + 1 } | ||
|
|
||
| // Intermediatary to force lambda | ||
| predicate CheckThis(p: ()->bool) { p() } |
There was a problem hiding this comment.
Formatting:
- Use one space after
: - Use no space before
: - Use a space before and after
->
There was a problem hiding this comment.
Right, I had just taken the provided test without reformatting.
Test/git-issues/git-issue-3719a.dfy
Outdated
| } | ||
|
|
||
| lemma Test() { | ||
| assert 1 == R(1) by {reveal R(); } |
There was a problem hiding this comment.
Formatting: Add one space between { and reveal.
Source/DafnyCore/DafnyPrelude.bpl
Outdated
| axiom (forall $ly: LayerType, b: bool :: | ||
| { CanRevealFuel(AsFuelBottom($ly), b) } | ||
| CanRevealFuel(AsFuelBottom($ly), b) | ||
| == $LZ); |
There was a problem hiding this comment.
Well done in figuring out the problem and suggesting a solution. I don't think we ever equate anything with $LZ elsewhere. Because of that, my hunch is that it's better to write the axiom as
axiom (forall $ly: LayerType, b: bool ::
{ CanRevealFuel(AsFuelBottom($ly), b) }
CanRevealFuel(AsFuelBottom($ly), b) == AsFuelBottom($ly));In fact, even more, since the first axiom (LL 514-516) says that CanRevealFuel commutes with $LS, provided the second parameter is known to equal true, I think it seems appropriate to do the analogous thing for the second axiom. That is, I suggest writing the second axiom as
axiom (forall $ly: LayerType, b: bool ::
{ CanRevealFuel(AsFuelBottom($ly), b) }
CanRevealFuel(AsFuelBottom($ly), b) == AsFuelBottom(CanRevealFuel($ly, b)));
This PR fixes #3719 and (implements) fixes #3778
I added the corresponding test.
In an upcoming PR, we might be able to remove the old mechanism "StartFuelAssert"/"StartFuel" of picking the fuel from the defniition site and letting user define their fuel at the call site, but this is independent.
This is the first PR of a series that will ensure opaqueness is consistent.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.