creusot
creusot copied to clipboard
creusot-rs
Fix #127
Adds a #[creusot::decl::opaque] annotation which prevents using the body of a definition in dependencies.
What do you mean by "dependencies"? Ideally, this should have the same semantics as the pub keyword...
Good point, we need to do a check similar to with pub for this to be actually useful. I propose that we only allow it to be visible in child modules, as that is by far simpler to implement than the pub(super), pub(crate) etc.. variants.
Sure, but there is also the question of what happens when we use pub use. Some thinking needs to be done to get the right design.
Actually, I have an idea: we could simply decide that the body of a logical definition is private as soon as it mentions a private "dummy" symbol. It is then easy to make a logical definition public but opaque, by making it body mention a private symbol (this could be automatized with a macro).
This way, we do not have to reinvent a new system of opacity in parallel to the default one of Rust. And by carefully managing the opacity of the "dummy" symbol, we can give the desired opacity to the definition.
What do you think?
By body do you mean the recursive expansion of every referenced function? If not how is this different than just tagging each function with an 'opaque' attribute?
By body do you mean the recursive expansion of every referenced function?
Not the "recursive" expansion. I simply mean the body of the definition. I.e., the body of a definition can be made public if it mentions public bu opaque symbols.
If not how is this different than just tagging each function with an 'opaque' attribute?
I don't really see what you mean, but my point is that by doing what I propose, we can rely on Rust's visibility mechanism, which is simple yet quite expressive thanks to the pub use construct, which makes it possible to re-export a symbol with different visibility.
Perhaps something which could be complicated if we want to implement that in Creusot is whether there exists in rustc's API a function to tell whether a symbol is public, either directly or using a different (re-exported) name. Is there such an an API?
I don't really see what you mean, but my point is that by doing what I propose, we can rely on Rust's visibility mechanism, which is simple yet quite expressive thanks to the pub use construct, which makes it possible to re-export a symbol with different visibility.
What I'm suggesting and what is implemented in this PR does just that. All we do is tag functions as opaque with a special attribute, which seems to be equivalent to checking if it contains a opaque_dummy symbol in its body?
Perhaps something which could be complicated if we want to implement that in Creusot is whether there exists in rustc's API a function to tell whether a symbol is public, either directly or using a different (re-exported) name. Is there such an an API?
Yes, rustc calculates a DefId visibility graph/tree which can answer the following query: is "A visible from B?"
What I'm suggesting and what is implemented in this PR does just that. All we do is tag functions as opaque with a special attribute, which seems to be equivalent to checking if it contains a opaque_dummy symbol in its body?
Right, this has the same semantics as if opaque_dummy was fully private. This is surely useful.
But to really handle visibility correctly, we need to do the check of visibility of symbols used in the body (am I correct that we still do not do that?). This is required because we don't want to make visible a private symbol used in a public definition. This is useful, because thanks to the trick I described above, we can really fine-tune visibility in the cases the opaque attribute does not do want we want.
This is required because we don't want to make visible a private symbol used in a public definition.
Ok, sorry I understand what you mean now, I wasn't getting the point you're driving at. I think the ideal solution is for us to only clone the interface of functions which should be private so that a public body can still refer to private symbols.
We should be cautious, though, because AFAIR, the interface module of a logical definition does not contain its contracts, right? An the contracts need to be public even for opaque definitions
Quoting myself:
I would still like this change to happen in the future, but I will do it properly using actual function contracts instead.