add some loop invariants

Author: thanhnguyen-aws

library/core/src/num/int_macros.rs

@@ -1588,7 +1588,8 @@ 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));
@@ -2299,6 +2300,7 @@ macro_rules! int_impl {
             let mut acc: Self = 1;
 
             if intrinsics::is_val_statically_known(exp) {
+                #[safety::loop_invariant(exp>=1)]
                 while exp > 1 {
                     if (exp & 1) == 1 {
                         acc = acc.wrapping_mul(base);
@@ -2316,6 +2318,7 @@ macro_rules! int_impl {
                 // at compile time. We can't use the same code for the constant
                 // exponent case because LLVM is currently unable to unroll
                 // this loop.
+                #[safety::loop_invariant(true)]
                 loop {
                     if (exp & 1) == 1 {
                         acc = acc.wrapping_mul(base);
@@ -2928,7 +2931,8 @@ macro_rules! int_impl {
             let mut overflown = false;
             // Scratch space for storing results of overflowing_mul.
             let mut r;
-
+            
+            #[safety::loop_invariant(true)]
             loop {
                 if (exp & 1) == 1 {
                     r = acc.overflowing_mul(base);

library/core/src/num/uint_macros.rs

@@ -1402,7 +1402,7 @@ macro_rules! uint_impl {
                     n = self.ilog2() / (base.ilog2() + 1);
                     r = base.pow(n);
                 }
-
+                #[safety::loop_invariant(base > 1 && r > 1 && r <= s && n <= r)]
                 while r <= self / base {
                     n += 1;
                     r *= base;