Add opaque modifier

[dnezam]

Once opaque has been merged into gobra, it may be useful to add opaque to specific functions.

Candidates

• Pow(x, e int) int in math/math.gobra
• Pow2(e int) int in math/math.gobra

It may also make sense to see which functions Dafny has marked as opaque.

[dnezam]

Additionally, we should make sure lemmas are opaque as well. These are usually functions that return Unit. Once closed has been implemented in Gobra, they should probably be updated to that.

[jcp19]

Once closed has been implemented in Gobra, they should probably be updated to that.

I am no longer sure if we need to have a closed keyword. In particular when we implement the access modifiers in Gobra, we might opt for never revealing the definition of all imported functions. This is, essentially, what Dafny does. All that is known about a function is the properties that are exposed via public lemmas. If that is the case, then the closed modifier becomes trivially unnecessary.

Related links:

• Problems with selective importing gobra#166
• Private Specification, Partial Struct Encoding, and Constructor gobra#619

[dnezam]

In particular when we implement the access modifiers in Gobra, we might opt for never revealing the definition of all imported functions.

What happens to pure functions where we actually do want to reveal the definitions by default? From what I understand, this used to be the way it works but was ultimately dropped because adding the body of those functions as a specification was a bit annoying.

Additionally, I think closed only becomes unnecessary for packages that are being imported while still being useful for times where we do not import packages: from what we learned from the experiments, I think it is fair to say that we want to hide proofs of lemmas. At the moment, this is achieved using opaque, but nothing is stopping the user to simply reveal the proof in the same package. This makes opaque feel a bit like a hack in situations like this. With this argument, the question boils down to whether it is worth implementing closed such that the idea of "this body can never be revealed" can be nicely expressed in Gobra (in contrast to opaque's "this body may be revealed, but not by default").

[jcp19]

I'm still thinking about what the best design would be. The comments here state my current position, which might easily change in the future.

What happens to pure functions where we actually do want to reveal the definitions by default?

I'm not too concerned with those. The user can always introduce a lemma that states that the function is equal to its body. We can even have syntactic sugar for that (an open function :D). What concerns me at the moment is that there is no clear way of separating, in a function, what is an implementation detail, and what are the properties that any implementation of the function will always uphold. Because of that, proofs in clients tend to be too coupled with the specific way a function is implemented (for example, the fact that we traverse some data structure in a given order instead of another totally different but acceptable order). Obviously, with closed, we could essentially hide unnecessary details but the question here is what would be the best default. My gut feeling is that, in large developments, it is better to have a more restrictive default which hides more information and open functions on a per-need basis, rather than opening all functions by default and close-ing the body on a "I need to make this faster" basis, or on an "I need to satisfy the type-checker" basis.

From what I understand, this used to be the way it works but was ultimately dropped because adding the body of those functions as a specification was a bit annoying.

I'm not sure I understand this. At the moment, Gobra reveals (and essentially checks) the body of all imported functions.

Additionally, I think closed only becomes unnecessary for packages that are being imported while still being useful for times where we do not import packages: from what we learned from the experiments, I think it is fair to say that we want to hide proofs of lemmas. At the moment, this is achieved using opaque, but nothing is stopping the user to simply reveal the proof in the same package. This makes opaque feel a bit like a hack in situations like this. With this argument, the question boils down to whether it is worth implementing closed such that the idea of "this body can never be revealed" can be nicely expressed in Gobra (in contrast to opaque's "this body may be revealed, but not by default").

I am not sure I agree with this. I don't think that the ability to state "this body can never be revealed" is necessary or useful inside a package, especially considering that reveal-ing is not the default - the user, who is an author of the package, is explicitly opting in to reveal a function.

[dnezam]

I'm not sure I understand this. At the moment, Gobra reveals (and essentially checks) the body of all imported functions.

If I understood correctly, this was not always the case. However, I might be misremembering and at the end of the day probably boils down on what the better defaults are.

Either way, thanks for the clarification!