Misc PR: core extraction features, traits, generic improvements...

[W95Psp]

This PR is a bit unfortunate, it's packing a huge number of interleaved features...
However, each the (basic) CI is green on each and every commit, and I extensively cleaned up the history, so things should not be too much messed up.

Previous description:

This PR tweaks Hax so that it is able to translate Rust's core library.

This PR adds a special mode for the exporter when exporting core. The environment variable HAX_CORE_EXTRACTION_MODE disables attributes and makes every function body be unit (for now. This should be panic or something).

On about 20 000 definitions, for now, we're able to extract 19 000 definitions (without body). That takes about one minute. Things that fail to extract trigger the following errors:

error[HAX0000]: (AST import) Unsafe blocks are not allowed.
occurences: 213
error[HAX0001]: (AndMutDefSite) something is not implemented yet.
occurences: 13
error[HAX0001]: (AST import) something is not implemented yet.
occurences: 111
error[HAX0001]: (FStar backend) something is not implemented yet.
occurences: 294
error[HAX0002]: (AndMutDefSite) Fatal error: something we considered as impossible occurred! Please report this by submitting an issue on GitHub!
occurences: 5
error[HAX0003]: (RefMut) The mutation of this &mut is not allowed here.
occurences: 270
error[HAX0008]: (reject_RawOrMutPointer) ExplicitRejection { reason: "unknown reason" }
occurences: 1

I've tweaked and fixed some bugs in the F* backend, now I'm at a point where F* complains because of module cycles. That means we're producing syntaxically correct code for the whole core crate!

My plan is thus to implement #203.

I push the current F* extraction there: https://github.com/W95Psp/rust/tree/hax/library/core/proofs/fstar/extraction

[franziskuskiefer]

Let's get this in.
Just add something in a readme for that one nit.