Add refinements to num/mod.rs

Author: nilehmann

library/core/Cargo.toml

@@ -49,6 +49,7 @@ check-cfg = [
 enabled = true
 check_overflow = "lazy"
 include = [ "src/ascii*.rs",
+            "src/num/mod.rs",
             "src/pat.rs",
             "src/bstr/*.rs",
             "src/hash/*.rs",

library/core/src/flux_info.rs

@@ -19,6 +19,39 @@
     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 {
@@ -50,7 +83,7 @@
     }
 
     impl Debug for time::Duration {
-        #[trusted(reason="modular arithmetic invariant inside nested fmt_decimal")]         
+        #[trusted(reason="modular arithmetic invariant inside nested fmt_decimal")]
         fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result;
     }
 }]

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