Add loop_invariants for some Int power functions

[thanhnguyen-aws]

Is PR add loop_invariants for checked_pow, wrapping_pow, overflowing_pow functions in library/core/src/num/uint_macros.rs and library/core/src/num/int_macros.rs.

NOTE: This PR requires the Kani version which supports loop loops.

Side notes:

• We need the feature that separate panic and other UBs to verify the function strict_pow, because this function calls strict_mul, which will panic when overflow happens.
• The function pow can overflow and may require contracts, such as

#[kani::requires(self.checked_pow(exp).is_some())]
#[kani::ensures(|x| *x == self.checked_pow(exp).unwrap())]

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

NOTE: This PR requires the Kani version which supports loop loops.

#326 will give us the automation fix to have a PR created that updates this repo to such a version.