added limits to multiplication proofs, reduced duplicacy in code by using macros to generate proof harnesses

Author: rajathkotyal

library/core/src/num/int_macros.rs

@@ -512,7 +512,6 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_add(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -818,7 +817,6 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(!self.overflowing_mul(rhs).1)]
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1428,7 +1426,6 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
-        #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,