SIMD: add a model

[W95Psp]

This PR inits a new crate, minicore.
For now, this covers only a small subset of core::arch::x86_64 and core::arch::x86.

This PR adds:

• abstractions for bit and bitvecs
• some specifications written in Rust (mainly a backport of what can be found in F* in fstar-helpers)
• tests

[franziskuskiefer]

Thanks. This looks like it's quite ready though.

Let's move this into a separate directory for proofs (where we can move the other proof related parts too). Having this on the top level clutters things even more. We'll move crates as well soon.

Also, the high level description needs to explain what this crate is doing and how.

[franziskuskiefer]

All of these functions should get a description of what they are doing when we want to use this as a source of truth.

[W95Psp]

I can copy-paste docs from rust core or intel, shall I do that?

[franziskuskiefer]

The rust docs are pretty limited and sometimes wrong I think. But the the gist from the intel docs with a link would be good.

[W95Psp]

Thanks for the review.
Shall I move that crate to fstar-helpers then?

[franziskuskiefer]

Shall I move that crate to fstar-helpers then?

Yeah, I guess that should be a more general verification folder or something like that at some point. But we can start using it for that and rename later. There is the formal_verification directory that has all the stuff on other projects that we could also repurpose. But fstar-helpers sounds the easiest for now.

[W95Psp]

I did the changes, but I'm not sure about the docs of the intrinsics actually.
Those are specifications: so adding the imperative style spec from intel seems a bit odd.

I wonder if we should not instead expose the body of the function as docstring, somehow.
Anyway, that's not clear, I think we should think about a good style before commiting to copy/pasting 10 snippets of code from the intel doc.

Review re-requested