Add Flux specifications to path/bstr/hash/time

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",
+ ]

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

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:
 /// <https://flux-rs.github.io/flux/guide/specifications.html#extensible-properties-for-primitive-ops>
 #[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<S>,
+ }
+ }
+
+ 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 _: () = {};

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")]

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<Self[{val: cast(val)}]>))]
  pub const fn new(val: $int) -> Option<Self> {
  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.)

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!(

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{<Self as RangePattern>::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{<char as RangePattern>::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"),