diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml index e676e88f4d4d8..be16d046a9d4a 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -47,4 +47,11 @@ check-cfg = [ [package.metadata.flux] enabled = true -include = [ "src/ascii{*.rs,/**/*.rs}" ] +check_overflow = "lazy" +include = [ "src/ascii*.rs", + "src/num/mod.rs", + "src/pat.rs", + "src/bstr/*.rs", + "src/hash/*.rs", + "src/time.rs", + ] diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs index 915e22629d182..5d1a34ddd9cd8 100644 --- a/library/core/src/ascii/ascii_char.rs +++ b/library/core/src/ascii/ascii_char.rs @@ -479,6 +479,7 @@ impl AsciiChar { /// `b` must be in `0..=127`, or else this is UB. #[unstable(feature = "ascii_char", issue = "110998")] #[inline] + #[cfg_attr(flux, flux::spec(fn(b: u8{b <= 127}) -> Self))] #[requires(b <= 127)] #[ensures(|result| *result as u8 == b)] pub const unsafe fn from_u8_unchecked(b: u8) -> Self { @@ -516,6 +517,10 @@ impl AsciiChar { /// when writing code using this method, since the implementation doesn't /// need something really specific, not to make those other arguments do /// something useful. It might be tightened before stabilization.) + // Only `d < 64` is required for safety as described above, but we use `d < 10` as + // in the `assert_unsafe_precondition` inside. See https://github.com/rust-lang/rust/pull/129374 + // for some context about the discrepancy. + #[cfg_attr(flux, flux::spec(fn(d: u8{d < 10}) -> Self))] #[unstable(feature = "ascii_char", issue = "110998")] #[inline] #[track_caller] @@ -536,8 +541,8 @@ impl AsciiChar { } /// Gets this ASCII character as a byte. + #[cfg_attr(flux, flux::spec(fn (Self) -> u8{v: v <= 127}))] #[unstable(feature = "ascii_char", issue = "110998")] - #[cfg_attr(flux, flux::spec(fn(Self) -> u8{v: v <= 127}))] #[inline] pub const fn to_u8(self) -> u8 { self as u8 diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs index c1aa8f1506cff..068d3cf830d81 100644 --- a/library/core/src/flux_info.rs +++ b/library/core/src/flux_info.rs @@ -4,12 +4,87 @@ /// See the following link for more information on how extensible properties for primitive operations work: /// #[flux::defs { + fn char_to_int(x:char) -> int { + cast(x) + } + property ShiftRightByFour[>>](x, y) { 16 * [>>](x, 4) == x } - property MaskBy15[&](x, y) { - [&](x, y) <= y + property MaskLess[&](x, y) { + [&](x, y) <= x && [&](x, y) <= y + } + + property ShiftLeft[<<](n, k) { + 0 < k => n <= [<<](n, k) + } + + fn is_ascii_uppercase(n: int) -> bool { + cast('A') <= n && n <= cast('Z') + } + + fn is_ascii_lowercase(n: int) -> bool { + cast('a') <= n && n <= cast('z') + } + + fn to_ascii_uppercase(n: int) -> int { + n - (cast(is_ascii_lowercase(n)) * 32) + } + + fn to_ascii_lowercase(n: int) -> int { + n + (cast(is_ascii_uppercase(n)) * 32) + } + + property BitXor0[^](x, y) { + (y == 0) => [^](x, y) == x + } + + property BitXor32[^](x, y) { + (is_ascii_lowercase(x) && y == 32) => [^](x, y) == x - 32 + } + + property BitOr0[|](x, y) { + (y == 0) => [|](x, y) == x + } + + property BitOr32[|](x, y) { + (is_ascii_uppercase(x) && y == 32) => [|](x, y) == x + 32 + } + +}] +#[flux::specs { + mod hash { + mod sip { + struct Hasher { + k0: u64, + k1: u64, + length: usize, // how many bytes we've processed + state: State, // hash State + tail: u64, // unprocessed bytes le + ntail: usize{v: v <= 8}, // how many bytes in tail are valid + _marker: PhantomData, + } + } + + impl BuildHasherDefault { + #[trusted(reason="https://github.com/flux-rs/flux/issues/1185")] + fn new() -> Self; + } + } + + impl Hasher for hash::sip::Hasher { + fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // mut-ref-unfolding + } + + impl Clone for hash::BuildHasherDefault { + #[trusted(reason="https://github.com/flux-rs/flux/issues/1185")] + fn clone(self: &Self) -> Self; + } + + impl Debug for time::Duration { + #[trusted(reason="modular arithmetic invariant inside nested fmt_decimal")] + fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result; } }] const _: () = {}; diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index d1ecbbbbb8247..df9159130973d 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -503,6 +503,7 @@ impl u8 { /// # Safety /// /// This byte must be valid ASCII, or else this is UB. + #[cfg_attr(flux, flux::spec(fn({&Self[@n] | n <= 127}) -> _))] #[must_use] #[unstable(feature = "ascii_char", issue = "110998")] #[inline] @@ -533,6 +534,7 @@ impl u8 { /// ``` /// /// [`make_ascii_uppercase`]: Self::make_ascii_uppercase + #[cfg_attr(flux, flux::spec(fn(&u8[@n]) -> u8[to_ascii_uppercase(n)]))] #[must_use = "to uppercase the value in-place, use `make_ascii_uppercase()`"] #[stable(feature = "ascii_methods_on_intrinsics", since = "1.23.0")] #[rustc_const_stable(feature = "const_ascii_methods_on_intrinsics", since = "1.52.0")] @@ -558,6 +560,7 @@ impl u8 { /// ``` /// /// [`make_ascii_lowercase`]: Self::make_ascii_lowercase + #[cfg_attr(flux, flux::spec(fn(&u8[@n]) -> u8[to_ascii_lowercase(n)]))] #[must_use = "to lowercase the value in-place, use `make_ascii_lowercase()`"] #[stable(feature = "ascii_methods_on_intrinsics", since = "1.23.0")] #[rustc_const_stable(feature = "const_ascii_methods_on_intrinsics", since = "1.52.0")] @@ -706,6 +709,7 @@ impl u8 { /// assert!(!lf.is_ascii_uppercase()); /// assert!(!esc.is_ascii_uppercase()); /// ``` + #[cfg_attr(flux, flux::spec(fn(&Self[@n]) -> bool[is_ascii_uppercase(n)]))] #[must_use] #[stable(feature = "ascii_ctype_on_intrinsics", since = "1.24.0")] #[rustc_const_stable(feature = "const_ascii_ctype_on_intrinsics", since = "1.47.0")] @@ -740,6 +744,7 @@ impl u8 { /// assert!(!lf.is_ascii_lowercase()); /// assert!(!esc.is_ascii_lowercase()); /// ``` + #[cfg_attr(flux, flux::spec(fn(&u8[@n]) -> bool[is_ascii_lowercase(n)]))] #[must_use] #[stable(feature = "ascii_ctype_on_intrinsics", since = "1.24.0")] #[rustc_const_stable(feature = "const_ascii_ctype_on_intrinsics", since = "1.47.0")] diff --git a/library/core/src/num/niche_types.rs b/library/core/src/num/niche_types.rs index d57b1d433e51c..5e9394b62773c 100644 --- a/library/core/src/num/niche_types.rs +++ b/library/core/src/num/niche_types.rs @@ -14,6 +14,9 @@ macro_rules! define_valid_range_type { $(#[$m:meta])* $vis:vis struct $name:ident($int:ident as $uint:ident in $low:literal..=$high:literal); )+) => {$( + #[cfg_attr(flux, flux::opaque)] + #[cfg_attr(flux, flux::refined_by(val: int))] + #[cfg_attr(flux, flux::invariant($low <= cast(val) && cast(val) <= $high))] #[derive(Clone, Copy, Eq)] #[repr(transparent)] #[rustc_layout_scalar_valid_range_start($low)] @@ -33,6 +36,7 @@ macro_rules! define_valid_range_type { impl $name { #[inline] + #[cfg_attr(flux, flux::spec(fn (val: $int) -> Option))] pub const fn new(val: $int) -> Option { if (val as $uint) >= ($low as $uint) && (val as $uint) <= ($high as $uint) { // SAFETY: just checked the inclusive range @@ -49,12 +53,14 @@ macro_rules! define_valid_range_type { /// Immediate language UB if `val` is not within the valid range for this /// type, as it violates the validity invariant. #[inline] + #[cfg_attr(flux, flux::spec(fn (val: $int{ $low <= cast(val) && cast(val) <= $high }) -> Self[{val:cast(val)}]))] pub const unsafe fn new_unchecked(val: $int) -> Self { // SAFETY: Caller promised that `val` is within the valid range. unsafe { $name(val) } } #[inline] + #[cfg_attr(flux, flux::spec(fn (self: Self) -> $int[cast(self.val)] ensures $low <= cast(self.val) && cast(self.val) <= $high))] pub const fn as_inner(self) -> $int { // SAFETY: This is a transparent wrapper, so unwrapping it is sound // (Not using `.0` due to MCP#807.) diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index f60b7e8202d03..39cc65a5b5ccb 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -629,6 +629,7 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[track_caller] + #[cfg_attr(flux, flux::spec(fn(self: Self, rhs: Self{self + rhs <= $MaxV}) -> Self[self + rhs]))] #[requires(!self.overflowing_add(rhs).1)] pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { assert_unsafe_precondition!( diff --git a/library/core/src/pat.rs b/library/core/src/pat.rs index 91d015b1bc53f..064bd467e3648 100644 --- a/library/core/src/pat.rs +++ b/library/core/src/pat.rs @@ -13,9 +13,22 @@ macro_rules! pattern_type { }; } +// The Flux spec for the `trait RangePattern` below uses +// [associated refinements](https://flux-rs.github.io/flux/tutorial/08-traits.html) +// The `sub_one` method may only be safe for certain values, +// e.g. when the value is not the "minimum of the type" as in the +// case of the `char` implementation below. To specify this precondition generically +// 1. at the trait level, we introduce the predicate `sub_ok` +// which characterizes the "valid" values at which `sub_one` +// can be safely called, and by default, specify this predicate +// is "true"; +// 2. at the impl level, we can provide a type-specific implementation +// of `sub_ok` that permits the verification of the impl for that type. + /// A trait implemented for integer types and `char`. /// Useful in the future for generic pattern types, but /// used right now to simplify ast lowering of pattern type ranges. +#[cfg_attr(flux, flux::assoc(fn sub_ok(self: Self) -> bool { true }))] #[unstable(feature = "pattern_type_range_trait", issue = "123646")] #[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")] #[const_trait] @@ -33,6 +46,7 @@ pub trait RangePattern { const MAX: Self; /// A compile-time helper to subtract 1 for exclusive ranges. + #[cfg_attr(flux, flux::spec(fn (self: Self{::sub_ok(self)}) -> Self))] #[lang = "RangeSub"] #[track_caller] fn sub_one(self) -> Self; @@ -61,12 +75,16 @@ impl_range_pat! { u8, u16, u32, u64, u128, usize, } +// The "associated refinement" `sub_ok` is defined as `non-zero` for `char`, to let Flux +// verify that the `self as u32 -1` in the impl does not underflow. +#[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self)}))] #[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")] impl const RangePattern for char { const MIN: Self = char::MIN; const MAX: Self = char::MAX; + #[cfg_attr(flux, flux::spec(fn (self: char{::sub_ok(self)}) -> char))] fn sub_one(self) -> Self { match char::from_u32(self as u32 - 1) { None => panic!("exclusive range to start of valid chars"),