v1.0-alpha

This proof is (essentially) complete. Some minor tweaks might still be done, but they will mainly be either stylistic or performance tweaks (if any).

One possible direction to prove further would be to have a conversion from int->nat128 to vale_msg len and vice-versa that works nicely alongside MsgEquivalence to have a stronger proof at Poly1305.Equivalence. To work on this, there is the shrinked-domain-vale branch, with the latest commit at the time of this v1.0-alpha release being b3b89a3