Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537#![allow(unused_imports)]use super::super::arithmetic::div_mod::{rust_div, rust_rem};use super::super::prelude::*;use super::super::wrapping::*;
use core::cmp::Ordering;
verus! {
/// The smallest multiple of `y` that is `>= x` (for `y > 0`), matching the value/// std's `next_multiple_of` / `checked_next_multiple_of` compute.pub open spec fn next_multiple_of(x: int, y: int) -> int recommends y > 0,{ if x % y == 0 { x } else { x + (y - x % y) }}
} // verus!macro_rules! num_specs { ($uN: ty, $iN: ty, $mod_u_tmp:ident, $mod_i_tmp:ident, $mod_u:ident, $mod_i:ident, $range:expr) => { verus! {
// Unsigned ints (u8, u16, etc.)
// Put in separate module to avoid name collisions. // Names don't matter - the user uses the stdlib functions. mod $mod_u_tmp { use super::*;
pub assume_specification[<$uN as Clone>::clone](x: &$uN) -> (res: $uN) ensures res == x;
impl super::super::cmp::PartialEqSpecImpl for $uN { open spec fn obeys_eq_spec() -> bool { true }
open spec fn eq_spec(&self, other: &$uN) -> bool { *self == *other } }
impl super::super::cmp::PartialOrdSpecImpl for $uN { open spec fn obeys_partial_cmp_spec() -> bool { true }
open spec fn partial_cmp_spec(&self, other: &$uN) -> Option<Ordering> { if *self < *other { Some(Ordering::Less) } else if *self > *other { Some(Ordering::Greater) } else { Some(Ordering::Equal) } } }
impl super::super::cmp::OrdSpecImpl for $uN { open spec fn obeys_cmp_spec() -> bool { true }
open spec fn cmp_spec(&self, other: &$uN) -> Ordering { if *self < *other { Ordering::Less } else if *self > *other { Ordering::Greater } else { Ordering::Equal } } }
pub assume_specification[<$uN as PartialEq<$uN>>::eq](x: &$uN, y: &$uN) -> bool;
pub assume_specification[<$uN as PartialEq<$uN>>::ne](x: &$uN, y: &$uN) -> bool;
pub assume_specification[<$uN as Ord>::cmp](x: &$uN, y: &$uN) -> Ordering;
pub assume_specification[<$uN as PartialOrd<$uN>>::partial_cmp](x: &$uN, y: &$uN) -> Option<Ordering>;
pub assume_specification[<$uN as PartialOrd<$uN>>::lt](x: &$uN, y: &$uN) -> bool;
pub assume_specification[<$uN as PartialOrd<$uN>>::le](x: &$uN, y: &$uN) -> bool;
pub assume_specification[<$uN as PartialOrd<$uN>>::gt](x: &$uN, y: &$uN) -> bool;
pub assume_specification[<$uN as PartialOrd<$uN>>::ge](x: &$uN, y: &$uN) -> bool;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::wrapping_add](x: $uN, y: $uN) -> $uN returns $mod_u::wrapping_add(x, y) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::wrapping_add_signed](x: $uN, y: $iN) -> $uN returns $mod_u::wrapping_add_signed(x, y) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::wrapping_sub](x: $uN, y: $uN) -> $uN returns $mod_u::wrapping_sub(x, y) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::wrapping_mul](x: $uN, y: $uN) -> $uN returns $mod_u::wrapping_mul(x, y) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::wrapping_shl](x: $uN, rhs: u32) -> $uN returns $mod_u::wrapping_shl(x, rhs) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::wrapping_shr](x: $uN, rhs: u32) -> $uN returns $mod_u::wrapping_shr(x, rhs) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::checked_add](x: $uN, y: $uN) -> Option<$uN> returns ( if x + y > <$uN>::MAX { None } else { Some((x + y) as $uN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::checked_add_signed](x: $uN, y: $iN) -> Option<$uN> returns ( if x + y > <$uN>::MAX || x + y < 0 { None } else { Some((x + y) as $uN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::checked_sub](x: $uN, y: $uN) -> Option<$uN> returns ( if x - y < 0 { None } else { Some((x - y) as $uN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::checked_mul](x: $uN, y: $uN) -> Option<$uN> returns ( if x * y > <$uN>::MAX { None } else { Some((x * y) as $uN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::checked_next_multiple_of](x: $uN, rhs: $uN) -> Option<$uN> returns ( if rhs == 0 { None } else if next_multiple_of(x as int, rhs as int) > <$uN>::MAX { None } else { Some(next_multiple_of(x as int, rhs as int) as $uN) } ) no_unwind;
pub open spec fn checked_div(x: $uN, y: $uN) -> Option<$uN> { if y == 0 { None } else { Some(x / y) } }
#[verifier::when_used_as_spec(checked_div)] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::checked_div](lhs: $uN, rhs: $uN) -> (result: Option<$uN>) ensures result == checked_div(lhs, rhs), no_unwind;
#[verifier::when_used_as_spec(checked_div)] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::checked_div_euclid](lhs: $uN, rhs: $uN) -> (result: Option<$uN>) ensures // checked_div is the same as checked_div_euclid for unsigned ints result == checked_div(lhs, rhs), no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::checked_rem](lhs: $uN, rhs: $uN) -> Option<$uN> returns ( if rhs == 0 { None } else { Some((lhs % rhs) as $uN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::checked_rem_euclid](lhs: $uN, rhs: $uN) -> Option<$uN> returns ( if rhs == 0 { None } else { Some((lhs % rhs) as $uN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::saturating_add](x: $uN, y: $uN) -> $uN returns ( if x + y > <$uN>::MAX { <$uN>::MAX } else { (x + y) as $uN } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::saturating_sub](x: $uN, y: $uN) -> $uN returns ( if x - y < <$uN>::MIN { <$uN>::MIN } else { (x - y) as $uN } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::saturating_mul](x: $uN, y: $uN) -> $uN returns ( if x * y > <$uN>::MAX { <$uN>::MAX } else { (x * y) as $uN } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$uN>::is_multiple_of](x: $uN, y: $uN) -> bool returns ( if y == 0 { x == 0 } else { x % y == 0 } ) no_unwind; }
// Signed ints (i8, i16, etc.)
mod $mod_i_tmp { use super::*;
pub assume_specification[<$iN as Clone>::clone](x: &$iN) -> (res: $iN) ensures res == x;
impl super::super::cmp::PartialEqSpecImpl for $iN { open spec fn obeys_eq_spec() -> bool { true }
open spec fn eq_spec(&self, other: &$iN) -> bool { *self == *other } }
impl super::super::cmp::PartialOrdSpecImpl for $iN { open spec fn obeys_partial_cmp_spec() -> bool { true }
open spec fn partial_cmp_spec(&self, other: &$iN) -> Option<Ordering> { if *self < *other { Some(Ordering::Less) } else if *self > *other { Some(Ordering::Greater) } else { Some(Ordering::Equal) } } }
impl super::super::cmp::OrdSpecImpl for $iN { open spec fn obeys_cmp_spec() -> bool { true }
open spec fn cmp_spec(&self, other: &$iN) -> Ordering { if *self < *other { Ordering::Less } else if *self > *other { Ordering::Greater } else { Ordering::Equal } } }
pub assume_specification[<$iN as PartialEq<$iN>>::eq](x: &$iN, y: &$iN) -> bool;
pub assume_specification[<$iN as PartialEq<$iN>>::ne](x: &$iN, y: &$iN) -> bool;
pub assume_specification[<$iN as Ord>::cmp](x: &$iN, y: &$iN) -> Ordering;
pub assume_specification[<$iN as PartialOrd<$iN>>::partial_cmp](x: &$iN, y: &$iN) -> Option<Ordering>;
pub assume_specification[<$iN as PartialOrd<$iN>>::lt](x: &$iN, y: &$iN) -> bool;
pub assume_specification[<$iN as PartialOrd<$iN>>::le](x: &$iN, y: &$iN) -> bool;
pub assume_specification[<$iN as PartialOrd<$iN>>::gt](x: &$iN, y: &$iN) -> bool;
pub assume_specification[<$iN as PartialOrd<$iN>>::ge](x: &$iN, y: &$iN) -> bool;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::wrapping_add](x: $iN, y: $iN) -> $iN returns $mod_i::wrapping_add(x, y) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::wrapping_add_unsigned](x: $iN, y: $uN) -> $iN returns $mod_i::wrapping_add_unsigned(x, y) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::wrapping_sub](x: $iN, y: $iN) -> (res: $iN) returns $mod_i::wrapping_sub(x, y) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::wrapping_mul](x: $iN, y: $iN) -> $iN returns $mod_i::wrapping_mul(x, y) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::wrapping_shl](x: $iN, rhs: u32) -> $iN returns $mod_i::wrapping_shl(x, rhs) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::wrapping_shr](x: $iN, rhs: u32) -> $iN returns $mod_i::wrapping_shr(x, rhs) opens_invariants none no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::checked_add](x: $iN, y: $iN) -> Option<$iN> returns ( if x + y > <$iN>::MAX || x + y < <$iN>::MIN { None } else { Some((x + y) as $iN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::checked_add_unsigned](x: $iN, y: $uN) -> Option<$iN> returns ( if x + y > <$iN>::MAX { None } else { Some((x + y) as $iN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::checked_sub](x: $iN, y: $iN) -> Option<$iN> returns ( if x - y > <$iN>::MAX || x - y < <$iN>::MIN { None } else { Some((x - y) as $iN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::checked_sub_unsigned](x: $iN, y: $uN) -> Option<$iN> returns ( if x - y < <$iN>::MIN { None } else { Some((x - y) as $iN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::checked_mul](x: $iN, y: $iN) -> Option<$iN> returns ( if x * y > <$iN>::MAX || x * y < <$iN>::MIN { None } else { Some((x * y) as $iN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::checked_div](lhs: $iN, rhs: $iN) -> Option<$iN> returns ( if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) { None } else { Some(rust_div(lhs as int, rhs as int) as $iN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::checked_div_euclid](lhs: $iN, rhs: $iN) -> Option<$iN> returns ( if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) { None } else { Some((lhs / rhs) as $iN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::checked_rem](lhs: $iN, rhs: $iN) -> Option<$iN> returns ( if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) { None } else { Some(rust_rem(lhs as int, rhs as int) as $iN) } ) no_unwind;
#[verifier::allow_in_spec] #[cfg(not(verus_verify_core))] pub assume_specification[<$iN>::checked_rem_euclid](lhs: $iN, rhs: $iN) -> Option<$iN> returns ( if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) { None } else { Some((lhs % rhs) as $iN) } ) no_unwind; }
} };}
num_specs!(u8, i8, u8_specs_tmp, i8_specs_tmp, u8_specs, i8_specs, 0x100);num_specs!(u16, i16, u16_specs_tmp, i16_specs_tmp, u16_specs, i16_specs, 0x1_0000);num_specs!(u32, i32, u32_specs_tmp, i32_specs_tmp, u32_specs, i32_specs, 0x1_0000_0000);num_specs!(u64, i64, u64_specs_tmp, i64_specs_tmp, u64_specs, i64_specs, 0x1_0000_0000_0000_0000);num_specs!( u128, i128, u128_specs_tmp, i128_specs_tmp, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000);num_specs!( usize, isize, usize_specs_tmp, isize_specs_tmp, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1));