diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index ac7b1fca9fa87..c03021f009703 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2264,4 +2264,224 @@ mod verify { nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); + + macro_rules! nonzero_check_cmp { + ($nonzero_type:ty, $nonzero_check_cmp_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_cmp_for() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + if x < y { + assert!(x.cmp(&y) == core::cmp::Ordering::Less); + } else if x > y { + assert!(x.cmp(&y) == core::cmp::Ordering::Greater); + } else { + assert!(x.cmp(&y) == core::cmp::Ordering::Equal); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_cmp!(core::num::NonZeroI8, nonzero_check_cmp_for_i8); + nonzero_check_cmp!(core::num::NonZeroI16, nonzero_check_cmp_for_i16); + nonzero_check_cmp!(core::num::NonZeroI32, nonzero_check_cmp_for_i32); + nonzero_check_cmp!(core::num::NonZeroI64, nonzero_check_cmp_for_i64); + nonzero_check_cmp!(core::num::NonZeroI128, nonzero_check_cmp_for_i128); + nonzero_check_cmp!(core::num::NonZeroIsize, nonzero_check_cmp_for_isize); + nonzero_check_cmp!(core::num::NonZeroU8, nonzero_check_cmp_for_u8); + nonzero_check_cmp!(core::num::NonZeroU16, nonzero_check_cmp_for_u16); + nonzero_check_cmp!(core::num::NonZeroU32, nonzero_check_cmp_for_u32); + nonzero_check_cmp!(core::num::NonZeroU64, nonzero_check_cmp_for_u64); + nonzero_check_cmp!(core::num::NonZeroU128, nonzero_check_cmp_for_u128); + nonzero_check_cmp!(core::num::NonZeroUsize, nonzero_check_cmp_for_usize); + + + macro_rules! nonzero_check_max { + ($nonzero_type:ty, $nonzero_check_max_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_max_for() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x.max(y); + if x > y { + assert!(result == x); + } else { + assert!(result == y); + } + } + }; + } + + nonzero_check_max!(core::num::NonZeroI8, nonzero_check_max_for_i8); + nonzero_check_max!(core::num::NonZeroI16, nonzero_check_max_for_i16); + nonzero_check_max!(core::num::NonZeroI32, nonzero_check_max_for_i32); + nonzero_check_max!(core::num::NonZeroI64, nonzero_check_max_for_i64); + nonzero_check_max!(core::num::NonZeroI128, nonzero_check_max_for_i128); + nonzero_check_max!(core::num::NonZeroIsize, nonzero_check_max_for_isize); + nonzero_check_max!(core::num::NonZeroU8, nonzero_check_max_for_u8); + nonzero_check_max!(core::num::NonZeroU16, nonzero_check_max_for_u16); + nonzero_check_max!(core::num::NonZeroU32, nonzero_check_max_for_u32); + nonzero_check_max!(core::num::NonZeroU64, nonzero_check_max_for_u64); + nonzero_check_max!(core::num::NonZeroU128, nonzero_check_max_for_u128); + nonzero_check_max!(core::num::NonZeroUsize, nonzero_check_max_for_usize); + + + macro_rules! nonzero_check_min { + ($nonzero_type:ty, $nonzero_check_min_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_min_for() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x.min(y); + if x < y { + assert!(result == x); + } else { + assert!(result == y); + } + } + }; + } + + nonzero_check_min!(core::num::NonZeroI8, nonzero_check_min_for_i8); + nonzero_check_min!(core::num::NonZeroI16, nonzero_check_min_for_i16); + nonzero_check_min!(core::num::NonZeroI32, nonzero_check_min_for_i32); + nonzero_check_min!(core::num::NonZeroI64, nonzero_check_min_for_i64); + nonzero_check_min!(core::num::NonZeroI128, nonzero_check_min_for_i128); + nonzero_check_min!(core::num::NonZeroIsize, nonzero_check_min_for_isize); + nonzero_check_min!(core::num::NonZeroU8, nonzero_check_min_for_u8); + nonzero_check_min!(core::num::NonZeroU16, nonzero_check_min_for_u16); + nonzero_check_min!(core::num::NonZeroU32, nonzero_check_min_for_u32); + nonzero_check_min!(core::num::NonZeroU64, nonzero_check_min_for_u64); + nonzero_check_min!(core::num::NonZeroU128, nonzero_check_min_for_u128); + nonzero_check_min!(core::num::NonZeroUsize, nonzero_check_min_for_usize); + + + macro_rules! nonzero_check_clamp { + ($nonzero_type:ty, $nonzero_check_clamp_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_clamp_for() { + let x: $nonzero_type = kani::any(); + let min: $nonzero_type = kani::any(); + let max: $nonzero_type = kani::any(); + // Ensure min <= max, so the function should no panic + kani::assume(min <= max); + // Use the clamp function and check the result + let result = x.clamp(min, max); + if x < min { + assert!(result == min); + } else if x > max { + assert!(result == max); + } else { + assert!(result == x); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_clamp!(core::num::NonZeroI8, nonzero_check_clamp_for_i8); + nonzero_check_clamp!(core::num::NonZeroI16, nonzero_check_clamp_for_16); + nonzero_check_clamp!(core::num::NonZeroI32, nonzero_check_clamp_for_32); + nonzero_check_clamp!(core::num::NonZeroI64, nonzero_check_clamp_for_64); + nonzero_check_clamp!(core::num::NonZeroI128, nonzero_check_clamp_for_128); + nonzero_check_clamp!(core::num::NonZeroIsize, nonzero_check_clamp_for_isize); + nonzero_check_clamp!(core::num::NonZeroU8, nonzero_check_clamp_for_u8); + nonzero_check_clamp!(core::num::NonZeroU16, nonzero_check_clamp_for_u16); + nonzero_check_clamp!(core::num::NonZeroU32, nonzero_check_clamp_for_u32); + nonzero_check_clamp!(core::num::NonZeroU64, nonzero_check_clamp_for_u64); + nonzero_check_clamp!(core::num::NonZeroU128, nonzero_check_clamp_for_u128); + nonzero_check_clamp!(core::num::NonZeroUsize, nonzero_check_clamp_for_usize); + + + macro_rules! nonzero_check_clamp_panic { + ($nonzero_type:ty, $nonzero_check_clamp_for:ident) => { + #[kani::proof] + #[kani::should_panic] + pub fn $nonzero_check_clamp_for() { + let x: $nonzero_type = kani::any(); + let min: $nonzero_type = kani::any(); + let max: $nonzero_type = kani::any(); + // Ensure min > max, so the function should panic + kani::assume(min > max); + // Use the clamp function and check the result + let result = x.clamp(min, max); + if x < min { + assert!(result == min); + } else if x > max { + assert!(result == max); + } else { + assert!(result == x); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_clamp_panic!(core::num::NonZeroI8, nonzero_check_clamp_panic_for_i8); + nonzero_check_clamp_panic!(core::num::NonZeroI16, nonzero_check_clamp_panic_for_16); + nonzero_check_clamp_panic!(core::num::NonZeroI32, nonzero_check_clamp_panic_for_32); + nonzero_check_clamp_panic!(core::num::NonZeroI64, nonzero_check_clamp_panic_for_64); + nonzero_check_clamp_panic!(core::num::NonZeroI128, nonzero_check_clamp_panic_for_128); + nonzero_check_clamp_panic!(core::num::NonZeroIsize, nonzero_check_clamp_panic_for_isize); + nonzero_check_clamp_panic!(core::num::NonZeroU8, nonzero_check_clamp_panic_for_u8); + nonzero_check_clamp_panic!(core::num::NonZeroU16, nonzero_check_clamp_panic_for_u16); + nonzero_check_clamp_panic!(core::num::NonZeroU32, nonzero_check_clamp_panic_for_u32); + nonzero_check_clamp_panic!(core::num::NonZeroU64, nonzero_check_clamp_panic_for_u64); + nonzero_check_clamp_panic!(core::num::NonZeroU128, nonzero_check_clamp_panic_for_u128); + nonzero_check_clamp_panic!(core::num::NonZeroUsize, nonzero_check_clamp_panic_for_usize); + + + macro_rules! nonzero_check_count_ones { + ($nonzero_type:ty, $nonzero_check_count_ones_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_count_ones_for() { + let x: $nonzero_type = kani::any(); + let result = x.count_ones(); + // Since x is non-zero, count_ones should never return 0 + assert!(result.get() > 0); + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_count_ones!(core::num::NonZeroI8, nonzero_check_count_ones_for_i8); + nonzero_check_count_ones!(core::num::NonZeroI16, nonzero_check_count_ones_for_i16); + nonzero_check_count_ones!(core::num::NonZeroI32, nonzero_check_count_ones_for_i32); + nonzero_check_count_ones!(core::num::NonZeroI64, nonzero_check_count_ones_for_i64); + nonzero_check_count_ones!(core::num::NonZeroI128, nonzero_check_count_ones_for_i128); + nonzero_check_count_ones!(core::num::NonZeroIsize, nonzero_check_count_ones_for_isize); + nonzero_check_count_ones!(core::num::NonZeroU8, nonzero_check_count_ones_for_u8); + nonzero_check_count_ones!(core::num::NonZeroU16, nonzero_check_count_ones_for_u16); + nonzero_check_count_ones!(core::num::NonZeroU32, nonzero_check_count_ones_for_u32); + nonzero_check_count_ones!(core::num::NonZeroU64, nonzero_check_count_ones_for_u64); + nonzero_check_count_ones!(core::num::NonZeroU128, nonzero_check_count_ones_for_u128); + nonzero_check_count_ones!(core::num::NonZeroUsize, nonzero_check_count_ones_for_usize); + + + macro_rules! nonzero_check_rotate_left_and_right { + ($nonzero_type:ty, $nonzero_check_rotate_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_rotate_for() { + let x: $nonzero_type = kani::any(); + let n: u32 = kani::any(); + let result = x.rotate_left(n).rotate_right(n); + assert!(result == x); + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_rotate_left_and_right!(core::num::NonZeroI8, nonzero_check_rotate_for_i8); + nonzero_check_rotate_left_and_right!(core::num::NonZeroI16, nonzero_check_rotate_for_i16); + nonzero_check_rotate_left_and_right!(core::num::NonZeroI32, nonzero_check_rotate_for_i32); + nonzero_check_rotate_left_and_right!(core::num::NonZeroI64, nonzero_check_rotate_for_i64); + nonzero_check_rotate_left_and_right!(core::num::NonZeroI128, nonzero_check_rotate_for_i128); + nonzero_check_rotate_left_and_right!(core::num::NonZeroIsize, nonzero_check_rotate_for_isize); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU8, nonzero_check_rotate_for_u8); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU16, nonzero_check_rotate_for_u16); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU32, nonzero_check_rotate_for_u32); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU64, nonzero_check_rotate_for_u64); + nonzero_check_rotate_left_and_right!(core::num::NonZeroU128, nonzero_check_rotate_for_u128); + nonzero_check_rotate_left_and_right!(core::num::NonZeroUsize, nonzero_check_rotate_for_usize); } diff --git a/library/core/src/time.rs b/library/core/src/time.rs index 2d93148bac09f..21b92453ecd26 100644 --- a/library/core/src/time.rs +++ b/library/core/src/time.rs @@ -19,10 +19,16 @@ //! assert_eq!(total, Duration::new(10, 7)); //! ``` +use safety::{ensures, Invariant}; use crate::fmt; use crate::iter::Sum; use crate::ops::{Add, AddAssign, Div, DivAssign, Mul, MulAssign, Sub, SubAssign}; +#[cfg(kani)] +use crate::kani; + +use crate::ub_checks::Invariant; + const NANOS_PER_SEC: u32 = 1_000_000_000; const NANOS_PER_MILLI: u32 = 1_000_000; const NANOS_PER_MICRO: u32 = 1_000; @@ -43,6 +49,12 @@ const DAYS_PER_WEEK: u64 = 7; #[rustc_layout_scalar_valid_range_end(999_999_999)] struct Nanoseconds(u32); +impl Invariant for Nanoseconds { + fn is_safe(&self) -> bool { + self.0 < NANOS_PER_SEC + } +} + impl Nanoseconds { // SAFETY: 0 is within the valid range const ZERO: Self = unsafe { Nanoseconds(0) }; @@ -95,6 +107,7 @@ impl Default for Nanoseconds { #[stable(feature = "duration", since = "1.3.0")] #[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)] #[cfg_attr(not(test), rustc_diagnostic_item = "Duration")] +#[derive(Invariant)] pub struct Duration { secs: u64, nanos: Nanoseconds, // Always 0 <= nanos < NANOS_PER_SEC @@ -208,6 +221,7 @@ impl Duration { #[inline] #[must_use] #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")] + #[ensures(|duration| duration.is_safe())] pub const fn new(secs: u64, nanos: u32) -> Duration { if nanos < NANOS_PER_SEC { // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range @@ -238,6 +252,8 @@ impl Duration { #[must_use] #[inline] #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")] + #[ensures(|duration| duration.is_safe())] + #[ensures(|duration| duration.secs == secs)] pub const fn from_secs(secs: u64) -> Duration { Duration { secs, nanos: Nanoseconds::ZERO } } @@ -258,6 +274,7 @@ impl Duration { #[must_use] #[inline] #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")] + #[ensures(|duration| duration.is_safe())] pub const fn from_millis(millis: u64) -> Duration { let secs = millis / MILLIS_PER_SEC; let subsec_millis = (millis % MILLIS_PER_SEC) as u32; @@ -284,6 +301,7 @@ impl Duration { #[must_use] #[inline] #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")] + #[ensures(|duration| duration.is_safe())] pub const fn from_micros(micros: u64) -> Duration { let secs = micros / MICROS_PER_SEC; let subsec_micros = (micros % MICROS_PER_SEC) as u32; @@ -315,6 +333,7 @@ impl Duration { #[must_use] #[inline] #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")] + #[ensures(|duration| duration.is_safe())] pub const fn from_nanos(nanos: u64) -> Duration { const NANOS_PER_SEC: u64 = self::NANOS_PER_SEC as u64; let secs = nanos / NANOS_PER_SEC; @@ -485,6 +504,7 @@ impl Duration { #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")] #[must_use] #[inline] + #[ensures(|secs| *secs == self.secs)] pub const fn as_secs(&self) -> u64 { self.secs } @@ -508,6 +528,7 @@ impl Duration { #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")] #[must_use] #[inline] + #[ensures(|ms| *ms == self.nanos.0 / NANOS_PER_MILLI)] pub const fn subsec_millis(&self) -> u32 { self.nanos.0 / NANOS_PER_MILLI } @@ -531,6 +552,7 @@ impl Duration { #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")] #[must_use] #[inline] + #[ensures(|ms| *ms == self.nanos.0 / NANOS_PER_MICRO)] pub const fn subsec_micros(&self) -> u32 { self.nanos.0 / NANOS_PER_MICRO } @@ -554,6 +576,7 @@ impl Duration { #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")] #[must_use] #[inline] + #[ensures(|nanos| *nanos == self.nanos.0)] pub const fn subsec_nanos(&self) -> u32 { self.nanos.0 } @@ -572,6 +595,7 @@ impl Duration { #[rustc_const_stable(feature = "duration_as_u128", since = "1.33.0")] #[must_use] #[inline] + #[ensures(|ms| *ms == self.secs as u128 * MILLIS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MILLI) as u128)] pub const fn as_millis(&self) -> u128 { self.secs as u128 * MILLIS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MILLI) as u128 } @@ -590,6 +614,7 @@ impl Duration { #[rustc_const_stable(feature = "duration_as_u128", since = "1.33.0")] #[must_use] #[inline] + #[ensures(|ms| *ms == self.secs as u128 * MICROS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MICRO) as u128)] pub const fn as_micros(&self) -> u128 { self.secs as u128 * MICROS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MICRO) as u128 } @@ -647,6 +672,7 @@ impl Duration { without modifying the original"] #[inline] #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")] + #[ensures(|duration| duration.is_none() || duration.unwrap().is_safe())] pub const fn checked_add(self, rhs: Duration) -> Option { if let Some(mut secs) = self.secs.checked_add(rhs.secs) { let mut nanos = self.nanos.0 + rhs.nanos.0; @@ -705,6 +731,7 @@ impl Duration { without modifying the original"] #[inline] #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")] + #[ensures(|duration| duration.is_none() || duration.unwrap().is_safe())] pub const fn checked_sub(self, rhs: Duration) -> Option { if let Some(mut secs) = self.secs.checked_sub(rhs.secs) { let nanos = if self.nanos.0 >= rhs.nanos.0 { @@ -761,6 +788,7 @@ impl Duration { without modifying the original"] #[inline] #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")] + #[ensures(|duration| duration.is_none() || duration.unwrap().is_safe())] pub const fn checked_mul(self, rhs: u32) -> Option { // Multiply nanoseconds as u64, because it cannot overflow that way. let total_nanos = self.nanos.0 as u64 * rhs as u64; @@ -816,6 +844,7 @@ impl Duration { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|duration| rhs == 0 || duration.unwrap().is_safe())] #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")] pub const fn checked_div(self, rhs: u32) -> Option { if rhs != 0 { @@ -823,6 +852,7 @@ impl Duration { let (mut nanos, extra_nanos) = (self.nanos.0 / rhs, self.nanos.0 % rhs); nanos += ((extra_secs * (NANOS_PER_SEC as u64) + extra_nanos as u64) / (rhs as u64)) as u32; + #[cfg(not(kani))] debug_assert!(nanos < NANOS_PER_SEC); Some(Duration::new(secs, nanos)) } else { @@ -1698,3 +1728,213 @@ impl Duration { ) } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod duration_verify { + use crate::kani; + use super::*; + + impl kani::Arbitrary for Duration { + fn any() -> Duration { + let secs = kani::any::(); + let nanos = kani::any::(); + Duration::new(secs, nanos) + } + } + + fn safe_duration() -> Duration { + let secs = kani::any::(); + let nanos = kani::any::(); + kani::assume(nanos < NANOS_PER_SEC || secs.checked_add((nanos / NANOS_PER_SEC) as u64).is_some()); + Duration::new(secs, nanos) + } + + #[kani::proof_for_contract(Duration::new)] + fn duration_new() { + let _ = safe_duration(); + } + + #[kani::proof_for_contract(Duration::new)] + #[kani::should_panic] + fn duration_new_panics() { + let secs = kani::any::(); + let nanos = kani::any::(); + let _ = Duration::new(secs, nanos); + } + + #[kani::proof_for_contract(Duration::from_secs)] + fn duration_from_secs() { + let secs = kani::any::(); + let _ = Duration::from_secs(secs); + } + + #[kani::proof_for_contract(Duration::from_millis)] + fn duration_from_millis() { + let ms = kani::any::(); + let _ = Duration::from_millis(ms); + } + + #[kani::proof_for_contract(Duration::from_micros)] + fn duration_from_micros() { + let micros = kani::any::(); + let _ = Duration::from_micros(micros); + } + + #[kani::proof_for_contract(Duration::from_nanos)] + fn duration_from_nanos() { + let nanos = kani::any::(); + let _ = Duration::from_nanos(nanos); + } + + #[kani::proof_for_contract(Duration::as_secs)] + fn duration_as_secs() { + let dur = safe_duration(); + let _ = dur.as_secs(); + } + + #[kani::proof_for_contract(Duration::as_secs)] + #[kani::should_panic] + fn duration_as_secs_panics() { + let dur = kani::any::(); + let _ = dur.as_secs(); + } + + #[kani::proof_for_contract(Duration::subsec_millis)] + fn duration_subsec_millis() { + let dur = safe_duration(); + let _ = dur.subsec_millis(); + } + + #[kani::proof_for_contract(Duration::subsec_millis)] + #[kani::should_panic] + fn duration_subsec_millis_panics() { + let dur = kani::any::(); + let _ = dur.subsec_millis(); + } + + #[kani::proof_for_contract(Duration::subsec_micros)] + fn duration_subsec_micros() { + let dur = safe_duration(); + let _ = dur.subsec_micros(); + } + + #[kani::proof_for_contract(Duration::subsec_micros)] + #[kani::should_panic] + fn duration_subsec_micros_panics() { + let dur = kani::any::(); + let _ = dur.subsec_micros(); + } + + #[kani::proof_for_contract(Duration::subsec_nanos)] + fn duration_subsec_nanos() { + let dur = safe_duration(); + let _ = dur.subsec_nanos(); + } + + #[kani::proof_for_contract(Duration::subsec_nanos)] + #[kani::should_panic] + fn duration_subsec_nanos_panics() { + let dur = kani::any::(); + let _ = dur.subsec_nanos(); + } + + #[kani::proof_for_contract(Duration::as_millis)] + fn duration_as_millis() { + let dur = safe_duration(); + let _ = dur.as_millis(); + } + + #[kani::proof_for_contract(Duration::as_millis)] + #[kani::should_panic] + fn duration_as_millis_panics() { + let dur = kani::any::(); + let _ = dur.as_millis(); + } + + #[kani::proof_for_contract(Duration::as_micros)] + fn duration_as_micros() { + let dur = safe_duration(); + let _ = dur.as_micros(); + } + + #[kani::proof_for_contract(Duration::as_micros)] + #[kani::should_panic] + fn duration_as_micros_panics() { + let dur = kani::any::(); + let _ = dur.as_micros(); + } + + #[kani::proof] + fn duration_as_nanos() { + let dur = safe_duration(); + let _ = dur.as_nanos(); + } + + #[kani::proof] + #[kani::should_panic] + fn duration_as_nanos_panics() { + let dur = kani::any::(); + let _ = dur.as_nanos(); + } + + #[kani::proof_for_contract(Duration::checked_add)] + fn duration_checked_add() { + let d0 = safe_duration(); + let d1 = safe_duration(); + let _ = d0.checked_add(d1); + } + + #[kani::proof_for_contract(Duration::checked_add)] + #[kani::should_panic] + fn duration_checked_add_panics() { + let d0 = kani::any::(); + let d1 = kani::any::(); + let _ = d0.checked_add(d1); + } + + #[kani::proof_for_contract(Duration::checked_sub)] + fn duration_checked_sub() { + let d0 = safe_duration(); + let d1 = safe_duration(); + let _ = d0.checked_sub(d1); + } + + #[kani::proof_for_contract(Duration::checked_sub)] + #[kani::should_panic] + fn duration_checked_sub_panics() { + let d0 = kani::any::(); + let d1 = kani::any::(); + let _ = d0.checked_sub(d1); + } + + #[kani::proof_for_contract(Duration::checked_mul)] + fn duration_checked_mul() { + let d0 = safe_duration(); + let amt = kani::any::(); + let _ = d0.checked_mul(amt); + } + + #[kani::proof_for_contract(Duration::checked_mul)] + #[kani::should_panic] + fn duration_checked_mul_panics() { + let d0 = kani::any::(); + let amt = kani::any::(); + let _ = d0.checked_mul(amt); + } + + #[kani::proof_for_contract(Duration::checked_div)] + fn duration_checked_div() { + let d0 = safe_duration(); + let amt = kani::any::(); + let _ = d0.checked_div(amt); + } + + #[kani::proof_for_contract(Duration::checked_div)] + #[kani::should_panic] + fn duration_checked_div_panics() { + let d0 = kani::any::(); + let amt = kani::any::(); + let _ = d0.checked_div(amt); + } +}