AeneasVerif
Add an attribute to mark definitions as `opaque`
It is currently possible to pass an option to Charon to mark some modules as opaque, so that Charon will not look inside those definitions (it treats them similarly to external definitions). This option is a bit coarse grained: it would be good to be able to individually mark the functions with a charon::opaque attribute. In order not to confuse the Aeneas users, I suggest introducing a aeneas::opaque attribute which does the same, and generally speaking introducing both a charon::... and an aeneas::... version of every new attribute.
Note: rustc will complain about such an attribute because it will try to find a macro with that name. Adding
#![feature(register_tool)]
#![register_tool(charon)]
at the top of each file that uses the attributes should solve the problem I hope. We can think of a cleaner solution afterwards. (See here for details about this feature).
Ok, thanks for looking into this. My understanding is that there are clean ways of doing this, but I'm indeed not aware of the details. It might be worth looking at other verification projects which use attributes (e.g., Verus or Creusot).
Creusot defines a proc-macro for their #[ensures]/#[invariant] etc attributes. That's one of the options available (and you started doing something like that with the attributes crate).
What do you recommend doing? I initially thought that was the only way of doing, but I would prefer a way which doesn't require adding a dependency to Charon directly in the Rust code.
register_tool is the simplest right now. I've heard discussions on the rustc side about what the best design for this feature would be, so I'd suggest using it for now and they'll likely figure out something more practical, e.g. a line to add in your Cargo.toml.
In case it helps, in Kani, we pass feature(register_tool) as part of the Rust flags:
https://github.com/model-checking/kani/blob/4a889397bba73fb76f0a21aad66171daad0b2b31/kani-driver/src/call_single_file.rs#L175-L178
https://github.com/AeneasVerif/charon/pull/227 allows the attribute on definitions; it would be nice to also allow the attribute on modules.
These attributes are supported on modules since one of the recent PRs that overhauled opaque handling.