Allow impls to be opaque

[maximebuyse]

This is needed for #1070 (comment), we already have opaque types of which this will be an extension.

[maximebuyse]

We need this for both functions and impls. When we see this opaque attribute we should add the val in the fsti, and and assume new name: type in the fst.

[maximebuyse]

We should make sure that we "kill" the body of opaque stuff early to avoid errors in the engine phases about them.

[karthikbhargavan]

Let's use this as a first step towards making opaque anything we do not want to handle, including raw mutable pointers, static globals etc. That needs a design document.

[karthikbhargavan]

This needs to be refined for use in libcrux.
When the impl has hax_lib::attributes, we sometimes rely on the specific post-condition within the impl. In these cases, don't want the whole impl to be opaque, instead we only want its fields to be opaque in the interface. In the worst case, if the fields cannot be made opaque, it would be better to leave the implementation in the interface.

This needs to be integrated within the opaque design, perhaps giving the user control over what appears where, with good defaults.