Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137//! Properties of floating point values.use super::prelude::*;
verus! {
pub trait FloatBitsProperties { type Bits;
spec fn to_bits_spec(&self) -> Self::Bits;
// All bits except sign bit spec fn to_bits_abs_spec(&self) -> Self::Bits;
// Sign bit is true (may apply to zero, subnormal, normal, infinite, NaN) spec fn is_sign_negative_spec(&self) -> bool;
// Zero, subnormal, or normal (not infinite, not NaN) spec fn is_finite_spec(&self) -> bool;
// Positive or negative infinity (not zero, not subnormal, not normal, not NaN) spec fn is_infinite_spec(&self) -> bool;
// A NaN value (not zero, not subnormal, not normal, not infinity) spec fn is_nan_spec(&self) -> bool;}
impl FloatBitsProperties for f32 { type Bits = u32;
open spec fn to_bits_spec(&self) -> u32 { f32_to_bits(*self) }
open spec fn to_bits_abs_spec(&self) -> u32 { let bits = self.to_bits_spec(); if bits >= 0x8000_0000 { (bits - 0x8000_0000) as u32 } else { bits } }
// Sign bit is true (may apply to zero, subnormal, normal, infinite, NaN) open spec fn is_sign_negative_spec(&self) -> bool { self.to_bits_spec() >= 0x8000_0000 }
open spec fn is_finite_spec(&self) -> bool { self.to_bits_abs_spec() < 0x7f80_0000 }
open spec fn is_infinite_spec(&self) -> bool { self.to_bits_abs_spec() == 0x7f80_0000 }
open spec fn is_nan_spec(&self) -> bool { self.to_bits_abs_spec() > 0x7f80_0000 }}
impl FloatBitsProperties for f64 { type Bits = u64;
open spec fn to_bits_spec(&self) -> u64 { f64_to_bits(*self) }
open spec fn to_bits_abs_spec(&self) -> u64 { let bits = self.to_bits_spec(); if bits >= 0x8000_0000_0000_0000 { (bits - 0x8000_0000_0000_0000) as u64 } else { bits } }
// Sign bit is true (may apply to zero, subnormal, normal, infinite, NaN) open spec fn is_sign_negative_spec(&self) -> bool { self.to_bits_spec() >= 0x8000_0000_0000_0000 }
open spec fn is_finite_spec(&self) -> bool { self.to_bits_abs_spec() < 0x7ff0_0000_0000_0000 }
open spec fn is_infinite_spec(&self) -> bool { self.to_bits_abs_spec() == 0x7ff0_0000_0000_0000 }
open spec fn is_nan_spec(&self) -> bool { self.to_bits_abs_spec() > 0x7ff0_0000_0000_0000 }}
pub assume_specification[ <f32 as Clone>::clone ](f: &f32) -> (res: f32) ensures res == f,;
pub assume_specification[ <f64 as Clone>::clone ](f: &f64) -> (res: f64) ensures res == f,;
#[verifier::external_trait_specification]pub trait ExIeeeFloatCast<To> { type ExternalTraitSpecificationFor: IeeeFloatCast<To>;}
// deterministic IEEE cast#[verifier::inline]pub open spec fn ieee_float_cast<From: Copy + IeeeFloatCast<To>, To>(from: From) -> To { from.ieee_cast()}
// (possibly) non-deterministic Rust castpub uninterp spec fn float_cast_spec<From, To>(from: From, to: To) -> bool;
// Used only for internal Verus translation of "as" operator;// this is not meant to be called directly by user code,// and it is not actually compiled to executable code#[cfg(verus_keep_ghost)]#[doc(hidden)]#[verifier::external_body]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::float::float_cast")]#[verifier::when_used_as_spec(ieee_float_cast)]pub fn float_cast<From: Copy + IeeeFloatCast<To>, To>(from: From) -> (to: To) ensures float_cast_spec(from, to), opens_invariants none no_unwind{ unimplemented!{}}
} // verus!