Meta: Improve Rust annotations for code specifications (requires, ensures, decreases, invariant)

[karthikbhargavan]

We use a mixture of Rust and target-language (fstar!) annotations in our code right now and there are a number of limitations around where we can add these annotations and what we can write in them. After having gained experience in annotating various codebases now, we should revisit the design of our annotation system and make it uniform and robust.

Some related issues:

• Allow all hax-lib attributes on impl elements #1183
• Better loop invariants #858
• Allow decreases classes to prove termination #1233
• self in requires clause gets renamed to self__ #1224
• Macro: requires and ensures should produce doc strings #1178
• ensures/requires on traits and impls: better ergonomics #829
• requires and ensure clauses on traits: add inheritance #789
• hax_lib::attributes: impls: requires clause not available in ensures  #784
• Ghost variables for proofs #1167
• Cannot access previous struct fields in refine attributes #904
• Reference an &mut _ binder in fstar! inside loop invariant #861
• Macros: preconditions that generates an debug_assert! #1268
• fstar! macro specialized for booleans #1269
• Requires and ensures: allow multiple per function #1270