Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805/// Defines the specifications for operator traits.////// This file specifies the behavior of operator traits for integers when the trait method is invoked./// Preconditions for some operator trait method are required to prevent overflow and underflow.////// - For primitive integer types, the expression `lhs $op rhs` is directly handled by the verifier/// without relying on trait specifications defined here, avoiding additional trigger costs./// However, calling `lhs.add(rhs)` or T::add(lhs, rhs) will trigger the corresponding trait method/// - If an operator is overloaded for a custom type, both `lhs $op rhs` and `lhs.add(rhs)` invoke the/// corresponding trait method for verification./// and its preconditions are enforced./// - Since this crate (vstd) defines the extension traits AddSpec, SubSpec, etc.,/// this crate is also allowed to implement these extension traits for known std types/// like u8, u16, etc. Rust's coherence rules prevent other crates from implementing/// these extension traits for std types. If this is a problem, as a last-resort workaround,/// other crates can assume axioms about the extension traits as an alternative to implementing/// them directly.use super::super::prelude::*;
macro_rules! def_un_ops_spec { ($trait:path, $extrait: ident, $spec_trait:ident, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident) => { $crate::vstd::prelude::verus! { #[verifier::external_trait_specification] #[verifier::external_trait_extension($spec_trait via $impl_trait)] pub trait $extrait { type ExternalTraitSpecificationFor: $trait;
type Output;
spec fn $obeys() -> bool;
spec fn $req(self) -> bool where Self: Sized;
spec fn $spec(self) -> Self::Output where Self: Sized;
fn $fun(self) -> (ret: Self::Output) requires self.$req(), ensures Self::$obeys() ==> ret == self.$spec(); } }};}
macro_rules! def_bin_ops_spec { ($trait:path, $extrait: ident, $spec_trait:ident, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident) => { $crate::vstd::prelude::verus! { #[verifier::external_trait_specification] #[verifier::external_trait_extension($spec_trait via $impl_trait)] pub trait $extrait<Rhs = Self> { type ExternalTraitSpecificationFor: $trait<Rhs>;
type Output;
spec fn $obeys() -> bool;
spec fn $req(self, rhs: Rhs) -> bool where Self: Sized;
spec fn $spec(self, rhs: Rhs) -> Self::Output where Self: Sized;
fn $fun(self, rhs: Rhs) -> (ret: Self::Output) requires self.$req(rhs), ensures Self::$obeys() ==> ret == self.$spec(rhs); } }};}
macro_rules! def_bin_ops_assign_spec { ($trait:path, $extrait: ident, $spec_trait:ident, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident) => { $crate::vstd::prelude::verus! { #[verifier::external_trait_specification] #[verifier::external_trait_extension($spec_trait via $impl_trait)] pub trait $extrait<Rhs = Self> { type ExternalTraitSpecificationFor: $trait<Rhs>;
spec fn $obeys() -> bool;
spec fn $req(&self, rhs: Rhs) -> bool;
spec fn $spec(&self, rhs: Rhs) -> &Self;
fn $fun(&mut self, rhs: Rhs) requires self.$req(rhs), ensures Self::$obeys() ==> &*final(self) == old(self).$spec(rhs); } }};}
def_un_ops_spec!( core::ops::Neg, ExNeg, NegSpec, NegSpecImpl, neg, obeys_neg_spec, neg_req, neg_spec);
def_un_ops_spec!( core::ops::Not, ExNot, NotSpec, NotSpecImpl, not, obeys_not_spec, not_req, not_spec);
def_bin_ops_spec!( core::ops::Add, ExAdd, AddSpec, AddSpecImpl, add, obeys_add_spec, add_req, add_spec);
def_bin_ops_assign_spec!( core::ops::AddAssign, ExAddAssign, AddAssignSpec, AddAssignSpecImpl, add_assign, obeys_add_assign_spec, add_assign_req, add_assign_spec);
def_bin_ops_spec!( core::ops::Sub, ExSub, SubSpec, SubSpecImpl, sub, obeys_sub_spec, sub_req, sub_spec);
def_bin_ops_assign_spec!( core::ops::SubAssign, ExSubAssign, SubAssignSpec, SubAssignSpecImpl, sub_assign, obeys_sub_assign_spec, sub_assign_req, sub_assign_spec);
def_bin_ops_spec!( core::ops::Mul, ExMul, MulSpec, MulSpecImpl, mul, obeys_mul_spec, mul_req, mul_spec);
def_bin_ops_assign_spec!( core::ops::MulAssign, ExMulAssign, MulAssignSpec, MulAssignSpecImpl, mul_assign, obeys_mul_assign_spec, mul_assign_req, mul_assign_spec);
def_bin_ops_spec!( core::ops::Div, ExDiv, DivSpec, DivSpecImpl, div, obeys_div_spec, div_req, div_spec);
def_bin_ops_assign_spec!( core::ops::DivAssign, ExDivAssign, DivAssignSpec, DivAssignSpecImpl, div_assign, obeys_div_assign_spec, div_assign_req, div_assign_spec);
def_bin_ops_spec!( core::ops::Rem, ExRem, RemSpec, RemSpecImpl, rem, obeys_rem_spec, rem_req, rem_spec);
def_bin_ops_assign_spec!( core::ops::RemAssign, ExRemAssign, RemAssignSpec, RemAssignSpecImpl, rem_assign, obeys_rem_assign_spec, rem_assign_req, rem_assign_spec);
def_bin_ops_spec!( core::ops::BitAnd, ExBitAnd, BitAndSpec, BitAndSpecImpl, bitand, obeys_bitand_spec, bitand_req, bitand_spec);
def_bin_ops_assign_spec!( core::ops::BitAndAssign, ExBitAndAssign, BitAndAssignSpec, BitAndAssignSpecImpl, bitand_assign, obeys_bitand_assign_spec, bitand_assign_req, bitand_assign_spec);
def_bin_ops_spec!( core::ops::BitOr, ExBitOr, BitOrSpec, BitOrSpecImpl, bitor, obeys_bitor_spec, bitor_req, bitor_spec);
def_bin_ops_assign_spec!( core::ops::BitOrAssign, ExBitOrAssign, BitOrAssignSpec, BitOrAssignSpecImpl, bitor_assign, obeys_bitor_assign_spec, bitor_assign_req, bitor_assign_spec);
def_bin_ops_spec!( core::ops::BitXor, ExBitXor, BitXorSpec, BitXorSpecImpl, bitxor, obeys_bitxor_spec, bitxor_req, bitxor_spec);
def_bin_ops_assign_spec!( core::ops::BitXorAssign, ExBitXorAssign, BitXorAssignSpec, BitXorAssignSpecImpl, bitxor_assign, obeys_bitxor_assign_spec, bitxor_assign_req, bitxor_assign_spec);
def_bin_ops_spec!( core::ops::Shl, ExShl, ShlSpec, ShlSpecImpl, shl, obeys_shl_spec, shl_req, shl_spec);
def_bin_ops_assign_spec!( core::ops::ShlAssign, ExShlAssign, ShlAssignSpec, ShlAssignSpecImpl, shl_assign, obeys_shl_assign_spec, shl_assign_req, shl_assign_spec);
def_bin_ops_spec!( core::ops::Shr, ExShr, ShrSpec, ShrSpecImpl, shr, obeys_shr_spec, shr_req, shr_spec);
def_bin_ops_assign_spec!( core::ops::ShrAssign, ExShrAssign, ShrAssignSpec, ShrAssignSpecImpl, shr_assign, obeys_shr_assign_spec, shr_assign_req, shr_assign_spec);
macro_rules! def_uop_impls { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, [$(($typ:ty, $req_expr:expr, $spec_expr:expr))*]) => { $crate::vstd::prelude::verus! { $( impl $impl_trait for $typ { open spec fn $obeys() -> bool { true }
open spec fn $req($self) -> bool { $req_expr }
open spec fn $spec($self) -> Self::Output { $spec_expr } }
pub assume_specification[ <$typ as $trait>::$fun ](x: $typ) -> $typ; )* }};}
macro_rules! def_bop_impls { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, [$(($typ:ty, $req_expr:expr, $spec_expr:expr))*]) => { $crate::vstd::prelude::verus! { $( impl $impl_trait for $typ { open spec fn $obeys() -> bool { true }
open spec fn $req($self, $rhs: $typ) -> bool { $req_expr }
open spec fn $spec($self, $rhs: $typ) -> Self::Output { $spec_expr } }
pub assume_specification[ <$typ as $trait>::$fun ](x: $typ, y: $typ) -> $typ; )* }};}
macro_rules! def_bop_assign_impls { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, [$(($typ:ty, $req_expr:expr, $spec_expr:expr))*]) => { $crate::vstd::prelude::verus! { $( impl $impl_trait for $typ { open spec fn $obeys() -> bool { true }
open spec fn $req(&$self, $rhs: $typ) -> bool { $req_expr }
open spec fn $spec(&$self, $rhs: $typ) -> &Self { &$spec_expr } }
pub assume_specification[ <$typ as $trait>::$fun ](x: &mut $typ, y: $typ); )* }};}
macro_rules! def_uop_impls_no_check { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_uop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, [ $( ( $typ, true, $op $self ) )* ]); }};}
macro_rules! def_uop_impls_check_overflow { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_uop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, [ $( ( $typ, ($op $self) as $typ == ($op $self), ($op $self) as $typ ) )* ]); }};}
macro_rules! def_bop_impls_no_check { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, true, $self $op $rhs ) )* ]); }};}
macro_rules! def_bop_assign_impls_no_check { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, true, $self $op $rhs ) )* ]); }};}
macro_rules! def_bop_impls_check_overflow { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, ($self $op $rhs) as $typ == ($self $op $rhs), ($self $op $rhs) as $typ ) )* ]); }};}
macro_rules! def_bop_assign_impls_check_overflow { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, ($self $op $rhs) as $typ == ($self $op $rhs), ($self $op $rhs) as $typ ) )* ]); }};}
macro_rules! def_bop_impls_unsigned_div_rem { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, $rhs != 0, $self $op $rhs ) )* ]); }};}
macro_rules! def_bop_assign_impls_unsigned_div_rem { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, $rhs != 0, $self $op $rhs ) )* ]); }};}
// Signed div/rem needs to:// - check for overflow (e.g. (-128i8) / (-1im))// - express truncating div, rem in terms of euclidean /, %macro_rules! def_bop_impls_signed_div_rem { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:path, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, $rhs != 0 && !($self == $typ::MIN && $rhs == -1), $op($self as int, $rhs as int) as $typ ) )* ]); }};}
macro_rules! def_bop_assign_impls_signed_div_rem { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:path, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, $rhs != 0 && !($self == $typ::MIN && $rhs == -1), $op($self as int, $rhs as int) as $typ ) )* ]); }};}
// TODO: there are many more combinations of primitive integer types supported by Shl and Shr,// such as (Self = u8, Rhs = u64)macro_rules! def_bop_impls_shift { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, 0 <= $rhs && $rhs < $typ::BITS, $self $op $rhs ) )* ]); }};}
macro_rules! def_bop_assign_impls_shift { ($trait:path, $impl_trait:ident, $fun:ident, $obeys:ident, $req:ident, $spec:ident, $self:ident, $rhs:ident, $op:tt, [$($typ:ty)*]) => { $crate::vstd::prelude::verus! { def_bop_assign_impls!($trait, $impl_trait, $fun, $obeys, $req, $spec, $self, $rhs, [ $( ( $typ, 0 <= $rhs && $rhs < $typ::BITS, $self $op $rhs ) )* ]); }};}
def_uop_impls_check_overflow!(core::ops::Neg, NegSpecImpl, neg, obeys_neg_spec, neg_req, neg_spec, self, -, [ isize i8 i16 i32 i64 i128]);
def_uop_impls_no_check!(core::ops::Not, NotSpecImpl, not, obeys_not_spec, not_req, not_spec, self, !, [ bool usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_impls_check_overflow!(core::ops::Add, AddSpecImpl, add, obeys_add_spec, add_req, add_spec, self, rhs, +, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_check_overflow!(core::ops::AddAssign, AddAssignSpecImpl, add_assign, obeys_add_assign_spec, add_assign_req, add_assign_spec, self, rhs, +, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_impls_check_overflow!(core::ops::Sub, SubSpecImpl, sub, obeys_sub_spec, sub_req, sub_spec, self, rhs, -, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_check_overflow!(core::ops::SubAssign, SubAssignSpecImpl, sub_assign, obeys_sub_assign_spec, sub_assign_req, sub_assign_spec, self, rhs, -, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_impls_check_overflow!(core::ops::Mul, MulSpecImpl, mul, obeys_mul_spec, mul_req, mul_spec, self, rhs, *, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_check_overflow!(core::ops::MulAssign, MulAssignSpecImpl, mul_assign, obeys_mul_assign_spec, mul_assign_req, mul_assign_spec, self, rhs, *, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_impls_unsigned_div_rem!(core::ops::Div, DivSpecImpl, div, obeys_div_spec, div_req, div_spec, self, rhs, /, [ usize u8 u16 u32 u64 u128]);
def_bop_assign_impls_unsigned_div_rem!(core::ops::DivAssign, DivAssignSpecImpl, div_assign, obeys_div_assign_spec, div_assign_req, div_assign_spec, self, rhs, /, [ usize u8 u16 u32 u64 u128]);
def_bop_impls_signed_div_rem!(core::ops::Div, DivSpecImpl, div, obeys_div_spec, div_req, div_spec, self, rhs, super::super::arithmetic::div_mod::rust_div, [ isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_signed_div_rem!(core::ops::DivAssign, DivAssignSpecImpl, div_assign, obeys_div_assign_spec, div_assign_req, div_assign_spec, self, rhs, super::super::arithmetic::div_mod::rust_div, [ isize i8 i16 i32 i64 i128]);
def_bop_impls_unsigned_div_rem!(core::ops::Rem, RemSpecImpl, rem, obeys_rem_spec, rem_req, rem_spec, self, rhs, %, [ usize u8 u16 u32 u64 u128]);
def_bop_assign_impls_unsigned_div_rem!(core::ops::RemAssign, RemAssignSpecImpl, rem_assign, obeys_rem_assign_spec, rem_assign_req, rem_assign_spec, self, rhs, %, [ usize u8 u16 u32 u64 u128]);
def_bop_impls_signed_div_rem!(core::ops::Rem, RemSpecImpl, rem, obeys_rem_spec, rem_req, rem_spec, self, rhs, super::super::arithmetic::div_mod::rust_rem, [ isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_signed_div_rem!(core::ops::RemAssign, RemAssignSpecImpl, rem_assign, obeys_rem_assign_spec, rem_assign_req, rem_assign_spec, self, rhs, super::super::arithmetic::div_mod::rust_rem, [ isize i8 i16 i32 i64 i128]);
def_bop_impls_no_check!(core::ops::BitAnd, BitAndSpecImpl, bitand, obeys_bitand_spec, bitand_req, bitand_spec, self, rhs, &, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_no_check!(core::ops::BitAndAssign, BitAndAssignSpecImpl, bitand_assign, obeys_bitand_assign_spec, bitand_assign_req, bitand_assign_spec, self, rhs, &, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_impls_no_check!(core::ops::BitOr, BitOrSpecImpl, bitor, obeys_bitor_spec, bitor_req, bitor_spec, self, rhs, |, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_no_check!(core::ops::BitOrAssign, BitOrAssignSpecImpl, bitor_assign, obeys_bitor_assign_spec, bitor_assign_req, bitor_assign_spec, self, rhs, |, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_impls_no_check!(core::ops::BitXor, BitXorSpecImpl, bitxor, obeys_bitxor_spec, bitxor_req, bitxor_spec, self, rhs, ^, [ bool usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_no_check!(core::ops::BitXorAssign, BitXorAssignSpecImpl, bitxor_assign, obeys_bitxor_assign_spec, bitxor_assign_req, bitxor_assign_spec, self, rhs, ^, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_impls_shift!(core::ops::Shl, ShlSpecImpl, shl, obeys_shl_spec, shl_req, shl_spec, self, rhs, <<, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_shift!(core::ops::ShlAssign, ShlAssignSpecImpl, shl_assign, obeys_shl_assign_spec, shl_assign_req, shl_assign_spec, self, rhs, <<, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_impls_shift!(core::ops::Shr, ShrSpecImpl, shr, obeys_shr_spec, shr_req, shr_spec, self, rhs, >>, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
def_bop_assign_impls_shift!(core::ops::ShrAssign, ShrAssignSpecImpl, shr_assign, obeys_shr_assign_spec, shr_assign_req, shr_assign_spec, self, rhs, >>, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
verus! {
#[verusfmt::skip]// Note: we do not assume that floating point types have obeys_*_spec() == true// because Rust floating point operations are not guaranteed to be deterministic.// (See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md )// Instead, we ensure an uninterpreted function about the result,// which can be used to trigger user-supplied axioms.#[verusfmt::skip]
pub uninterp spec fn neg_ensures<A>(x: A, o: A) -> bool;
pub uninterp spec fn add_ensures<A>(x: A, y: A, o: A) -> bool;
pub uninterp spec fn sub_ensures<A>(x: A, y: A, o: A) -> bool;
pub uninterp spec fn mul_ensures<A>(x: A, y: A, o: A) -> bool;
pub uninterp spec fn div_ensures<A>(x: A, y: A, o: A) -> bool;
pub assume_specification[ <f32 as core::ops::Neg>::neg ](x: f32) -> (o: f32) ensures neg_ensures::<f32>(x, o),;
pub assume_specification[ <f32 as core::ops::Add>::add ](x: f32, y: f32) -> (o: f32) ensures add_ensures::<f32>(x, y, o),;
pub assume_specification[ <f32 as core::ops::Sub>::sub ](x: f32, y: f32) -> (o: f32) ensures sub_ensures::<f32>(x, y, o),;
pub assume_specification[ <f32 as core::ops::Mul>::mul ](x: f32, y: f32) -> (o: f32) ensures mul_ensures::<f32>(x, y, o),;
pub assume_specification[ <f32 as core::ops::Div>::div ](x: f32, y: f32) -> (o: f32) ensures div_ensures::<f32>(x, y, o),;
pub assume_specification[ <f64 as core::ops::Neg>::neg ](x: f64) -> (o: f64) ensures neg_ensures::<f64>(x, o),;
pub assume_specification[ <f64 as core::ops::Add>::add ](x: f64, y: f64) -> (o: f64) ensures add_ensures::<f64>(x, y, o),;
pub assume_specification[ <f64 as core::ops::Sub>::sub ](x: f64, y: f64) -> (o: f64) ensures sub_ensures::<f64>(x, y, o),;
pub assume_specification[ <f64 as core::ops::Mul>::mul ](x: f64, y: f64) -> (o: f64) ensures mul_ensures::<f64>(x, y, o),;
pub assume_specification[ <f64 as core::ops::Div>::div ](x: f64, y: f64) -> (o: f64) ensures div_ensures::<f64>(x, y, o),;
} // verus!