Make names of `impl` more stable

[W95Psp]

Currently, the name of an tranlsated impl uses a disambiguator given by Rust, which, morally, is a unique counter. Adding an impl or moving an impl results in changes in names.

We should have a more stable naming mechanism. One idea could be to use a hash.

That was an issue for @gaetan-sbt, who was writing a shim for a crate. A module in that shim had only one impl while the original module in the crate had multiple. Thus, the naming was wrong. The workaround is to add more impl blocks to "bump the disambiguation". That's pretty fragile and ugly.

@gaetan-sbt was pointing me to https://rust-lang.github.io/rfcs/2603-rust-symbol-name-mangling-v0.html, that's a great read, and might give us interesting ideas for something better than just a hash.

Action items:

• [x] figure out exactly what design we want for those names (decision: use a hash)
• [ ] change the name policity in that direction
• [ ] rename everything by hand in existing hand-written code (e.g. the proofs-lib)

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

That's still relevant, and something we need for what @cmester0 is busy with (core). https://rust-lang.github.io/rfcs/2603-rust-symbol-name-mangling-v0.html is super interesting, but overkill for us: we don't need to recover full Rust names from generated names.

After thinking about that and discussing the design, we will use a hash instead of the discriminant value given by Rust. The difficulty of this is the existing hand-written code... I may implement this feature, but guard it behind a env var or a flag.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.