Bounded integers

[W95Psp]

This PR:

• renames the method refine (from the trait Refine, which is implemented by types for which refine types have been defined) into check ("check" is less "refinement-oriented" vocabulary and conveys the right intuition);
• adds an invariant method to the Refinement trait, so that one can check whether a value satisfies a refinement;
• use that invariant method to generate a debug_assert! that ensures the refinement holds at runtime (in debug mode only);
• add a no_debug_runtime_check option to disable that runtime check even in debug mode (useful since that check requires the refined type to impl Clone);
• introduces a module num_traits that defines a small trait hierarchy for operations we want to support on machine integers;
• introduces a series of refined type BoundedT, for any machine integer T, all of those types implement traits from num_traits;
• rewrite the chacha20 example using BoundedUsize<0, 15> instead of preconditions (that reformulation of chacha20 TC in F*).

This PR builds on #643.

TODO:

• figure out how to name & where to put hax-bounded-integers;
• add bounded math integers (let's first merge Add support for math integers #629) this is not possible right now because we'd need adt_const_params;
• move the example out of the crate bounded math crate, or at least behind a #[test];
• derive more impls for traits on BoundedTs

Future work:

• implement MachineInt for every primitive type?

[W95Psp]

The CI is failing because of the hax-bounded-integers not being found by the CI, I will fix that after your review @franziskuskiefer, I expect us to want hax-bounded-integers somewhere else anyway

[franziskuskiefer]

We'll want to do changes here. But let's get something in and improve later when we know better what exactly we need.