From f5fa3bedbe6e71c98386bd3a95207fdfb548d5a9 Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Wed, 30 Jul 2025 19:56:47 -0700
Subject: [PATCH 1/7] Verify time.rs

---
 library/core/Cargo.toml              |  7 ++++-
 library/core/src/ascii/ascii_char.rs |  2 +-
 library/core/src/flux_info.rs        | 46 ++++++++++++++++++++++++++--
 library/core/src/num/niche_types.rs  |  6 ++++
 library/core/src/pat.rs              |  4 +++
 5 files changed, 61 insertions(+), 4 deletions(-)

diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index e676e88f4d4d8..0f5692e7cd289 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -47,4 +47,9 @@ check-cfg = [
 
 [package.metadata.flux]
 enabled = true
-include = [ "src/ascii{*.rs,/**/*.rs}" ]
+include = [ "src/ascii*.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..e190f16559459 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -536,8 +536,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..1d81eb7f40b07 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -4,12 +4,54 @@
 /// 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)
+    }
+}]
+#[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]         // 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]         // https://github.com/flux-rs/flux/issues/1185
+        fn clone(self: &Self) -> Self;
+    }
+
+    impl Debug for time::Duration {
+        #[trusted]         // 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/niche_types.rs b/library/core/src/num/niche_types.rs
index d57b1d433e51c..db0c63a94465c 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<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)}]))] // NOTE: `val == 0` comments are stale(?)
             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/pat.rs b/library/core/src/pat.rs
index 91d015b1bc53f..84f4c8fe56330 100644
--- a/library/core/src/pat.rs
+++ b/library/core/src/pat.rs
@@ -16,6 +16,7 @@ macro_rules! pattern_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 +34,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 +63,14 @@ impl_range_pat! {
     u8, u16, u32, u64, u128, usize,
 }
 
+#[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"),

From aa7871ae366345d9cf66d4b2dd3841968b76abde Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Thu, 31 Jul 2025 14:53:47 -0700
Subject: [PATCH 2/7] lazy overflow checking

---
 library/core/Cargo.toml       | 3 ++-
 library/core/src/flux_info.rs | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index 0f5692e7cd289..9586ae0c5ea59 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -47,8 +47,9 @@ check-cfg = [
 
 [package.metadata.flux]
 enabled = true
+check_overflow = "lazy"
 include = [ "src/ascii*.rs",
-            "src/pat.rs", 
+            "src/pat.rs",
             "src/bstr/*.rs",
             "src/hash/*.rs",
             "src/time.rs",
diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 1d81eb7f40b07..777af78c34ea4 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -54,4 +54,4 @@
         fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result;
     }
 }]
-const _: () = {};
+const _: () = ();

From b4b51ed0c2df960e5da7bb757665a336053aa70e Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Thu, 31 Jul 2025 16:48:03 -0700
Subject: [PATCH 3/7] Put reason inside attribute

---
 library/core/src/flux_info.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 777af78c34ea4..4eb721825980a 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -35,7 +35,7 @@
         }
 
         impl BuildHasherDefault {
-            #[trusted]         // https://github.com/flux-rs/flux/issues/1185
+            #[trusted(reason="https://github.com/flux-rs/flux/issues/1185")]
             fn new() -> Self;
         }
     }
@@ -45,13 +45,13 @@
     }
 
     impl Clone for hash::BuildHasherDefault {
-        #[trusted]         // https://github.com/flux-rs/flux/issues/1185
+        #[trusted(reason="https://github.com/flux-rs/flux/issues/1185")]
         fn clone(self: &Self) -> Self;
     }
 
     impl Debug for time::Duration {
-        #[trusted]         // 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;
     }
 }]
-const _: () = ();
+const _: () = {};

From 918a46b41ce735d1cd126ec2a35f6f8471af0d45 Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Fri, 1 Aug 2025 09:33:36 -0700
Subject: [PATCH 4/7] Add specs for digit_unchecked + comments

---
 library/core/src/ascii/ascii_char.rs |  2 ++
 library/core/src/num/uint_macros.rs  |  1 +
 library/core/src/pat.rs              | 15 +++++++++++++++
 3 files changed, 18 insertions(+)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index e190f16559459..06a4b23b87642 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,7 @@ 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.)
+    #[cfg_attr(flux, flux::spec(fn(d: u8{d < 10}) -> Self))]
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
     #[track_caller]
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 84f4c8fe56330..ffef40f82cbf6 100644
--- a/library/core/src/pat.rs
+++ b/library/core/src/pat.rs
@@ -13,6 +13,18 @@ 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.
@@ -63,6 +75,8 @@ 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 {
@@ -70,6 +84,7 @@ impl const RangePattern for char {
 
     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) {

From 1750a08037c183467e212ac1127753438d5de57f Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Fri, 1 Aug 2025 10:04:39 -0700
Subject: [PATCH 5/7] Fix formatting

---
 library/core/src/pat.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/library/core/src/pat.rs b/library/core/src/pat.rs
index ffef40f82cbf6..064bd467e3648 100644
--- a/library/core/src/pat.rs
+++ b/library/core/src/pat.rs
@@ -84,7 +84,6 @@ impl const RangePattern for char {
 
     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) {

From 5cf4d9083ac14a811fcb10963958503e97904691 Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Mon, 4 Aug 2025 09:07:19 -0700
Subject: [PATCH 6/7] Add comment about `d < 10` vs `d < 64`

---
 library/core/src/ascii/ascii_char.rs | 3 +++
 library/core/src/num/niche_types.rs  | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index 06a4b23b87642..5d1a34ddd9cd8 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -517,6 +517,9 @@ 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]
diff --git a/library/core/src/num/niche_types.rs b/library/core/src/num/niche_types.rs
index db0c63a94465c..5e9394b62773c 100644
--- a/library/core/src/num/niche_types.rs
+++ b/library/core/src/num/niche_types.rs
@@ -53,7 +53,7 @@ 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)}]))] // NOTE: `val == 0` comments are stale(?)
+            #[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) }

From 0375ccda1766b1e20b31a7524d0bb9c5516d99f2 Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Tue, 9 Sep 2025 11:37:29 -0300
Subject: [PATCH 7/7] Add refinements to num/mod.rs

---
 library/core/Cargo.toml       |  1 +
 library/core/src/flux_info.rs | 35 ++++++++++++++++++++++++++++++++++-
 library/core/src/num/mod.rs   |  5 +++++
 3 files changed, 40 insertions(+), 1 deletion(-)

diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index 9586ae0c5ea59..be16d046a9d4a 100644
--- a/library/core/Cargo.toml
+++ b/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",
diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 4eb721825980a..068d3cf830d81 100644
--- a/library/core/src/flux_info.rs
+++ b/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;
     }
 }]
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")]