Verify safety of NonZero operations (Challenge 12)

Add verification harnesses for all remaining NonZero functions:
bit operations (count_ones, swap_bytes, reverse_bits, rotate_left,
rotate_right), byte order (from_be, from_le, to_be, to_le), bitor
(all 3 impls), checked/saturating arithmetic (checked_mul,
saturating_mul, checked_add, saturating_add, checked_pow,
saturating_pow), power of two (checked_next_power_of_two), midpoint,
isqrt, signed operations (neg, abs, checked_abs, overflowing_abs,
saturating_abs, wrapping_abs, unsigned_abs, checked_neg,
overflowing_neg, wrapping_neg), and from_mut.

Remove trivial loop_invariant(true) annotations from primitive
checked_pow that caused CBMC assigns check interference with
NonZero::new_unchecked verification.

Total: 385 harnesses pass (376 new + 9 existing).

Author: jrey8343

library/core/src/num/int_macros.rs

@@ -1736,7 +1736,6 @@ macro_rules! int_impl {
             let mut base = self;
             let mut acc: Self = 1;
 
-            #[safety::loop_invariant(true)]
             loop {
                 if (exp & 1) == 1 {
                     acc = try_opt!(acc.checked_mul(base));