Rust Engine: global identifiers: add view and rendering

[W95Psp]

Identifiers in hax are wrapper around DefIds from rustc.
DefId consists in flat paths from crate name to the item name.

Printing such names in a consistent way across backend is a bit difficult. Names are not actually flat: a field for instance, always has a parent constructor, which always has a parent type.

When printing names, this is very handy to have: various backend have different namespace, and different requirements.

This PR introduces the concept of a View: a strongly-typed, hierarchical representation of a Rust path.
A View is a list of path segments, where each segment carries:

• its kind (crate, module, type, trait, impl, assoc item, constructor, field, etc.),
• whether it's named or unnamed (e.g. impl, anon const),
• links to its parent segment (e.g. field → constructor → type).

This makes paths robust to traversal, disambiguation, and rendering, while directly encoding rustc's invariants about what can appear where.

The PR also provides nice traits to deal with per-backend name printing, but those are a bit rough for now.
They don't handle a lot for you out of the box (e.g. name clashes, reserved names, etc.).
I will address that in a follow up PR.

This PR fixes #1599.

[maximebuyse]

Generally looks good. I mostly looked at documentation (and it looks great!). I tested on a Lean example and it seems to produce weird stuff. hax_machine_int_le becomes Rust_primitives.Hax.Machine_int.le so it doesn't work with names defined in the lib. And pre/post conditions have weird names like Crate._.requires or Crate.__1.ensures (that's probably less of a problem because we need to improve name rendering for those anyway). Do we want to fix this in a follow up PR? Because I guess this will break examples like Barrett or chacha.

[W95Psp]

Thanks for the review, ah indeed, I was mainly using Lean to test my rendering mechanism.
I will revert the Lean changes (will be easier for @clementblaudeau to work with probably)!

[W95Psp]

(just noticed @keks is out, since @jschneider-bensch is out as well, I'm asking you @franziskuskiefer)

[franziskuskiefer]

generally lgtm but there are panics in here again.

[franziskuskiefer]

Thanks for addressing the panic issue. That solution sounds good to me.
Maybe clearly separating out the binary and library use case would also help.
But I just want to avoid pushing the problem up the stack by crashing without offering a good way of handling this for the caller.

[W95Psp]

Sounds good.
I opened #1630 as a follow up, which will address your two other questions.