Embedding machine integers as machine integer constants

[mtzguido]

Currently, we consider that the value for a machine integer (say U32) is a term of the form FStar.UInt32.uint_to_t 42, or potentially UInt32.__uint_to_t 42, and rely as well on some Meta_desugared nodes to recognize them for printing. The code handling all this is quite brittle, and tricky to maintain. For instance, it used to be the case that we did not even check the module name of the "constructor" uint_to_t, which meant we may use the U64 operations on SizeT, and viceversa (which happened to work ok, but was definitely a concern, see #3178 and #3180, the problem was introduced after the refactoring of the primops/embeddings, which made the checks stricter).

This PR tries to get us closer to a more canonical answer for "what is a machine integer in F*?" by using machine integer constants (which we already had) to represent them, much like we do for mathematical integers. Now, uint_to_t is simply a normalizer step that reduces to such a value. The embeddings, desugaring, printing, and extraction become slightly simpler by doing this. At any point a constant can be "unfolded" to a uint_to_t application, which is what, e.g., the encoding does to handle them.

I tested everest and got a green, except that I need a 2-line patch to HACL* to add some assertions (my best guess is just instability).

A question remains though:

All machine integer modules have an implementation as an inductive containing a refined int. So, there is still a double view. I think this is benign for the time being, even if the module is friended, as the encoding will work on unfolded literals.
But, I'm having second thought as I type this... On the upside, there is no question about what a machine integer value is, it must be a Tm_constant.