Make it possible to hide the body of public logic function

[jhjourdan]

@xldenis proposed to have an #[opaque] attribute. That's a possibility, indeed.

Then the default is that the body is public when the function is public, which is good, after all.

When the body of a logic function uses private symbols, what should we do? We should either emit an error or make the function opaque automatically. I guess the less surprising behavior is to emit an error.

(I guess Creusot is already doing something when the spec of a function (logic or program) mentions a private symbol (type, function, trait, ....), isn't it?)

[xldenis]

When the body of a logic function uses private symbols, what should we do? We should either emit an error or make the function opaque automatically. I guess the less surprising behavior is to emit an error.

Yes, the nature of transparent functions means you can't hide a private body in a public one, so privacy is viral.

(I guess Creusot is already doing something when the spec of a function (logic or program) mentions a private symbol (type, function, trait, ....), isn't it?)

Nothing special, I believe that's actually a bug. It should be able to construct a program which exposes a private symbol in its specs.

[xldenis]

An initial design that @jhjourdan and I seem to have settled on is the following:

• #[predicate] and #[logic] functions are transparent wherever they are visible by default.
• If a transparent function uses a private or less visible symbol or type in its body it raises an error asking the function to be made opaque
• An #[opaque] attribute can be used to render the function opaque.

We also discussed an improvement which would allow the opacity to be a subset of the visibility of a function, but I believe this should be left as a second iteration on the concept.

[xldenis]

Fixed through the addition of opacity and the #[open(..)] annotation.