feat(hax-lib): intro. hax feature

[W95Psp]

This PR introduces a (default) hax feature on hax-lib.

When this feature is disabled:

• hax-lib-macros defines identity proc-macros, and keeps its dependencies to a minimum (only quote and syn)
• hax-lib becomes a one-module tiny and "inert" library, with only hax-lib-macros as a dependency (when the feature macros is enabled)

Fixes #639.

[karthikbhargavan]

I tested this on libcrux and it appears to work well.

[karthikbhargavan]

@franziskuskiefer fixed the flags on this PR, and now the hax engine fails because of this error:

# File "lib/concrete_ident_generated.ml", lines 1-476, characters 0-94:
#   1 | type t = 
#   2 |       Hax_lib_protocol__crypto__Impl_5__from_bytes
#   3 |     | Core__result__Impl__E
#   4 |     | Core__ops__control_flow__ControlFlow__Break
#   5 |     | Core__ops__bit__BitAnd__bitand
# ...
# 473 |     | Core__cmp__PartialEq__eq__'__1
# 474 |     | Rust_primitives__hax__control_flow_monad__moption
# 475 |     | Core__array__iter__Impl__T
# 476 |     | Core__iter__traits__iterator__Iterator[@@deriving show, yojson, compare, sexp, eq, hash]
# Error: Two constructors are named Hax_lib__assert

This is because the hax-engine also depends on hax-lib to extract names, and with the new cfg flags, something is going wrong in the way this is used.

@W95Psp: maybe this will be easy for you to fix.

[franziskuskiefer]

Clearing the review. Re-request when it's ready to look at.

[W95Psp]

The engine is fixed and the library is fixed as well, things are passing CI.
@karthikbhargavan can you check if that's working fine on MLKEM?

[franziskuskiefer]

Looks good to me now. The main thing I checked is that we are really not getting any dependencies or code when not using the hax cfg.

[karthikbhargavan]

libcrux proofs use hax_lib::loop_invariant!; so this needs to be in the dummy-lib.

[W95Psp]

I fixed it, now it should be fine!

[karthikbhargavan]

This works for me now. Thanks!