From 1f82e22e685bb732da9c6e4972b341bd11fee674 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Thu, 26 Jun 2025 11:23:33 -0700
Subject: [PATCH 01/42] rebasing detached (step 1)

---
 library/core/src/convert/num.rs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs
index 38e46a9f210f9..293b150f32c93 100644
--- a/library/core/src/convert/num.rs
+++ b/library/core/src/convert/num.rs
@@ -69,14 +69,15 @@ macro_rules! impl_from {
             ),
         );
     };
-    ($Small:ty => $Large:ty, #[$attr:meta] $(,)?) => {
+    ($Small:ty => $Large:ty, #[$attr:meta] $(, #[$flux_attr:meta])? $(,)?) => {
         impl_from!(
             $Small => $Large,
             #[$attr],
             concat!("Converts [`", stringify!($Small), "`] to [`", stringify!($Large), "`] losslessly."),
+            $(#[$flux_attr],)?
         );
     };
-    ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(,)?) => {
+    ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(,  #[$flux_attr:meta])? $(,)?) => {
         #[$attr]
         impl From<$Small> for $Large {
             // Rustdocs on the impl block show a "[+] show undocumented items" toggle.
@@ -110,7 +111,7 @@ impl_from!(u8 => u16, #[stable(feature = "lossless_int_conv", since = "1.5.0")])
 impl_from!(u8 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u8 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u8 => u128, #[stable(feature = "i128", since = "1.26.0")]);
-impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
+impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")], #[cfg_attr(flux, flux::spec(fn(x:u8) -> usize[x]))]);
 impl_from!(u16 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u128, #[stable(feature = "i128", since = "1.26.0")]);

From 51815ed39f4538604afd86cd2f74119f550c4546 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Mon, 14 Jul 2025 14:24:01 -0700
Subject: [PATCH 02/42] update convert with cast (only)

---
 library/core/src/convert/num.rs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs
index 293b150f32c93..38e46a9f210f9 100644
--- a/library/core/src/convert/num.rs
+++ b/library/core/src/convert/num.rs
@@ -69,15 +69,14 @@ macro_rules! impl_from {
             ),
         );
     };
-    ($Small:ty => $Large:ty, #[$attr:meta] $(, #[$flux_attr:meta])? $(,)?) => {
+    ($Small:ty => $Large:ty, #[$attr:meta] $(,)?) => {
         impl_from!(
             $Small => $Large,
             #[$attr],
             concat!("Converts [`", stringify!($Small), "`] to [`", stringify!($Large), "`] losslessly."),
-            $(#[$flux_attr],)?
         );
     };
-    ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(,  #[$flux_attr:meta])? $(,)?) => {
+    ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(,)?) => {
         #[$attr]
         impl From<$Small> for $Large {
             // Rustdocs on the impl block show a "[+] show undocumented items" toggle.
@@ -111,7 +110,7 @@ impl_from!(u8 => u16, #[stable(feature = "lossless_int_conv", since = "1.5.0")])
 impl_from!(u8 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u8 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u8 => u128, #[stable(feature = "i128", since = "1.26.0")]);
-impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")], #[cfg_attr(flux, flux::spec(fn(x:u8) -> usize[x]))]);
+impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u128, #[stable(feature = "i128", since = "1.26.0")]);

From 2945adb879fa0cea12bf04dec36f5beb1e3808f8 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 12:21:43 -0700
Subject: [PATCH 03/42] DONE: pat

---
 library/Cargo.lock            | 90 +++++++++++++++++++++++++++++++++++
 library/core/Cargo.toml       |  3 +-
 library/core/src/flux_info.rs | 13 ++++-
 library/core/src/pat.rs       |  4 ++
 4 files changed, 107 insertions(+), 3 deletions(-)

diff --git a/library/Cargo.lock b/library/Cargo.lock
index c681c5935df5f..aa756e9e6aa94 100644
--- a/library/Cargo.lock
+++ b/library/Cargo.lock
@@ -28,6 +28,7 @@ version = "0.0.0"
 dependencies = [
  "compiler_builtins",
  "core",
+ "safety",
 ]
 
 [[package]]
@@ -67,6 +68,9 @@ dependencies = [
 [[package]]
 name = "core"
 version = "0.0.0"
+dependencies = [
+ "safety",
+]
 
 [[package]]
 name = "coretests"
@@ -201,6 +205,39 @@ dependencies = [
  "unwind",
 ]
 
+[[package]]
+name = "proc-macro-error"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
+dependencies = [
+ "proc-macro-error-attr",
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro-error-attr"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.95"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "02b3e5e68a3a1a02aad3ec490a98007cbc13c37cbe84a3cd7b8e406d76e7f778"
+dependencies = [
+ "unicode-ident",
+]
+
 [[package]]
 name = "proc_macro"
 version = "0.0.0"
@@ -217,6 +254,15 @@ dependencies = [
  "cc",
 ]
 
+[[package]]
+name = "quote"
+version = "1.0.40"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1885c039570dc00dcb4ff087a89e185fd56bae234ddc7f056a945bf36467248d"
+dependencies = [
+ "proc-macro2",
+]
+
 [[package]]
 name = "r-efi"
 version = "5.3.0"
@@ -301,6 +347,16 @@ dependencies = [
  "std",
 ]
 
+[[package]]
+name = "safety"
+version = "0.1.0"
+dependencies = [
+ "proc-macro-error",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.104",
+]
+
 [[package]]
 name = "shlex"
 version = "1.3.0"
@@ -330,6 +386,7 @@ dependencies = [
  "rand",
  "rand_xorshift",
  "rustc-demangle",
+ "safety",
  "std_detect",
  "unwind",
  "wasi",
@@ -346,6 +403,27 @@ dependencies = [
  "rustc-std-workspace-core",
 ]
 
+[[package]]
+name = "syn"
+version = "1.0.109"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
+dependencies = [
+ "proc-macro2",
+ "unicode-ident",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.104"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "17b6f705963418cdb9927482fa304bc562ece2fdd4f616084c50b7023b435a40"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "sysroot"
 version = "0.0.0"
@@ -366,6 +444,12 @@ dependencies = [
  "std",
 ]
 
+[[package]]
+name = "unicode-ident"
+version = "1.0.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5a5f39404a5da50712a4c1eecf25e90dd62b613502b7e925fd4e4d19b5c96512"
+
 [[package]]
 name = "unicode-width"
 version = "0.2.1"
@@ -398,6 +482,12 @@ dependencies = [
  "rustc-std-workspace-core",
 ]
 
+[[package]]
+name = "version_check"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
+
 [[package]]
 name = "wasi"
 version = "0.11.1+wasi-snapshot-preview1"
diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index e676e88f4d4d8..0ecd0a40e712a 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -47,4 +47,5 @@ check-cfg = [
 
 [package.metadata.flux]
 enabled = true
-include = [ "src/ascii{*.rs,/**/*.rs}" ]
+include = [ "src/ascii{*.rs,/**/*.rs}",
+            "src/pat{*.rs,/**/*.rs}" ]
diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index c1aa8f1506cff..82acac82a1402 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -4,12 +4,21 @@
 /// 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(c:char) -> int { 
+        cast(c) 
+    } 
+
     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)
     }
 }]
 const _: () = {};
diff --git a/library/core/src/pat.rs b/library/core/src/pat.rs
index 91d015b1bc53f..1f86d859d1f58 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;
@@ -62,11 +64,13 @@ impl_range_pat! {
 }
 
 #[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")]
+#[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self) }))]
 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 2f0f2122249af1c108e7aa59f0c3c82c1e1e9a0e Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 12:22:39 -0700
Subject: [PATCH 04/42] DONE: bstr

---
 library/core/Cargo.toml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index 0ecd0a40e712a..7b00ee9a5f6cd 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -48,4 +48,6 @@ check-cfg = [
 [package.metadata.flux]
 enabled = true
 include = [ "src/ascii{*.rs,/**/*.rs}",
-            "src/pat{*.rs,/**/*.rs}" ]
+            "src/pat{*.rs,/**/*.rs}", 
+            "src/bstr{*.rs,/**/*.rs}",
+          ]

From ff6b39d57a08f10ceb15a540c0a65b2b84f7821b Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 12:37:41 -0700
Subject: [PATCH 05/42] PAUSE: flux #1185

---
 library/core/Cargo.toml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index 7b00ee9a5f6cd..b2e057186dbae 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -50,4 +50,5 @@ enabled = true
 include = [ "src/ascii{*.rs,/**/*.rs}",
             "src/pat{*.rs,/**/*.rs}", 
             "src/bstr{*.rs,/**/*.rs}",
+            "src/hash{*.rs,/**/*.rs}",
           ]

From 857825e7ac59ad8369eb75fc4ac6c82d87a46cda Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 13:03:33 -0700
Subject: [PATCH 06/42] DONE: hash

---
 library/core/src/hash/mod.rs | 2 ++
 library/core/src/hash/sip.rs | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/library/core/src/hash/mod.rs b/library/core/src/hash/mod.rs
index a10c85640bbb6..6aaa9349a913b 100644
--- a/library/core/src/hash/mod.rs
+++ b/library/core/src/hash/mod.rs
@@ -752,6 +752,7 @@ pub struct BuildHasherDefault<H>(marker::PhantomData<fn() -> H>);
 
 impl<H> BuildHasherDefault<H> {
     /// Creates a new BuildHasherDefault for Hasher `H`.
+    #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
     #[stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     #[rustc_const_stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     pub const fn new() -> Self {
@@ -777,6 +778,7 @@ impl<H: Default + Hasher> BuildHasher for BuildHasherDefault<H> {
 
 #[stable(since = "1.7.0", feature = "build_hasher")]
 impl<H> Clone for BuildHasherDefault<H> {
+    #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
     fn clone(&self) -> BuildHasherDefault<H> {
         BuildHasherDefault(marker::PhantomData)
     }
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index 780e522c48ebf..f0fa4ac9f1026 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -53,6 +53,7 @@ struct Hasher<S: Sip> {
     length: usize, // how many bytes we've processed
     state: State,  // hash State
     tail: u64,     // unprocessed bytes le
+    #[cfg_attr(flux, flux::field(usize{v: v <= 8}))]
     ntail: usize,  // how many bytes in tail are valid
     _marker: PhantomData<S>,
 }
@@ -252,6 +253,7 @@ impl<S: Sip> super::Hasher for Hasher<S> {
     // slightly slowing down compile speeds on some benchmarks. See #69152 for
     // details.
     #[inline]
+    #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
     fn write(&mut self, msg: &[u8]) {
         let length = msg.len();
         self.length += length;

From beaa970013afbf5794625eb59db56baed8c832ee Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 13:06:44 -0700
Subject: [PATCH 07/42] NEXT: NANOSEC invariant

---
 library/core/Cargo.toml  | 1 +
 library/core/src/time.rs | 1 +
 2 files changed, 2 insertions(+)

diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index b2e057186dbae..16130fa08f802 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -51,4 +51,5 @@ include = [ "src/ascii{*.rs,/**/*.rs}",
             "src/pat{*.rs,/**/*.rs}", 
             "src/bstr{*.rs,/**/*.rs}",
             "src/hash{*.rs,/**/*.rs}",
+            "src/time{*.rs,/**/*.rs}",
           ]
diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 059ab5506ece3..29e9e8eb19bd4 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -1269,6 +1269,7 @@ impl fmt::Debug for Duration {
         ///
         /// A prefix and postfix may be added. The whole thing is padded
         /// to the formatter's `width`, if specified.
+        #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant"))]
         fn fmt_decimal(
             f: &mut fmt::Formatter<'_>,
             integer_part: u64,

From 8c29de894afb0fc83c2ea32343b466dd5e0806aa Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 15:04:39 -0700
Subject: [PATCH 08/42] NEXT: time -- needs `%` properties

---
 library/core/src/flux_info.rs       | 8 ++++++--
 library/core/src/num/niche_types.rs | 6 ++++++
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 82acac82a1402..18732a4f95dbb 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -5,8 +5,12 @@
 /// <https://flux-rs.github.io/flux/guide/specifications.html#extensible-properties-for-primitive-ops>
 #[flux::defs {
 
-    fn char_to_int(c:char) -> int { 
-        cast(c) 
+    fn as_int(x:int) -> int { 
+        x 
+    }
+
+    fn char_to_int(x:char) -> int { 
+        cast(x) 
     } 
 
     property ShiftRightByFour[>>](x, y) {
diff --git a/library/core/src/num/niche_types.rs b/library/core/src/num/niche_types.rs
index b92561c9e356d..a10db97cd370f 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(as_int($low) <= cast(val) && cast(val) <= as_int($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 == 0`, as it violates the validity
             /// invariant of this type.
             #[inline]
+            #[cfg_attr(flux, flux::spec(fn (val: $int{ as_int($low) <= cast(val) && cast(val) <= as_int($high) }) -> Self[{val:cast(val)}]))]
             pub const unsafe fn new_unchecked(val: $int) -> Self {
                 // SAFETY: Caller promised that `val` is non-zero.
                 unsafe { $name(val) }
             }
 
             #[inline]
+            #[cfg_attr(flux, flux::spec(fn (self: Self) -> $int[cast(self.val)] ensures as_int($low) <= cast(self.val) && cast(self.val) <= as_int($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.)

From c1e89cc88935110013543a1080bf8b9ea6655e3d Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 18:05:28 -0700
Subject: [PATCH 09/42] DONE: time

---
 library/core/src/num/niche_types.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/core/src/num/niche_types.rs b/library/core/src/num/niche_types.rs
index a10db97cd370f..2f3779253486a 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 == 0`, as it violates the validity
             /// invariant of this type.
             #[inline]
-            #[cfg_attr(flux, flux::spec(fn (val: $int{ as_int($low) <= cast(val) && cast(val) <= as_int($high) }) -> Self[{val:cast(val)}]))]
+            #[cfg_attr(flux, flux::spec(fn (val: $int{ as_int($low) <= cast(val) && cast(val) <= as_int($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 non-zero.
                 unsafe { $name(val) }

From 9357e64c6e53999223eef98bd6197b07ffbd96ab Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Mon, 28 Jul 2025 18:56:11 -0700
Subject: [PATCH 10/42] temp

---
 library/core/src/ascii/ascii_char.rs |  7 ++++--
 library/core/src/flux_info.rs        | 36 ++++++++++++++++++++++++----
 library/core/src/hash/sip.rs         | 19 +++++++++++----
 3 files changed, 50 insertions(+), 12 deletions(-)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index 856a8632f269d..fbdc6d3ecdb7d 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -529,7 +529,7 @@ impl AsciiChar {
 
     /// Gets this ASCII character as a byte.
     #[unstable(feature = "ascii_char", issue = "110998")]
-    #[cfg_attr(flux, flux::spec(fn(Self) -> u8{v: v <= 127}))]
+    // DETACH? #[cfg_attr(flux, flux::spec(fn(Self) -> u8{v: v <= 127}))]
     #[inline]
     pub const fn to_u8(self) -> u8 {
         self as u8
@@ -615,7 +615,10 @@ impl fmt::Debug for AsciiChar {
                 let byte = self.to_u8();
                 let hi = HEX_DIGITS[usize::from(byte >> 4)];
                 let lo = HEX_DIGITS[usize::from(byte & 0xf)];
-                ([Apostrophe, Backslash, AsciiChar::SmallX, hi, lo, Apostrophe], 6)
+                (
+                    [Apostrophe, Backslash, AsciiChar::SmallX, hi, lo, Apostrophe],
+                    6,
+                )
             }
             _ => ([Apostrophe, *self, Apostrophe, Null, Null, Null], 3),
         };
diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 18732a4f95dbb..21889d44e4741 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -5,13 +5,13 @@
 /// <https://flux-rs.github.io/flux/guide/specifications.html#extensible-properties-for-primitive-ops>
 #[flux::defs {
 
-    fn as_int(x:int) -> int { 
-        x 
+    fn as_int(x:int) -> int {
+        x
     }
 
-    fn char_to_int(x:char) -> int { 
-        cast(x) 
-    } 
+    fn char_to_int(x:char) -> int {
+        cast(x)
+    }
 
     property ShiftRightByFour[>>](x, y) {
         16 * [>>](x, 4) == x
@@ -25,4 +25,30 @@
         0 < k => n <= [<<](n, k)
     }
 }]
+#[flux::specs {
+    mod ascii {
+        // AsciiChar is `crate::ascii::Char`
+        impl Char {
+            fn to_u8(Self) -> u8{v: v <= 127};
+        }
+    }
+
+    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 Hasher for Hasher<S> {
+                fn wrote(self: &mut Self, msg: &[u8]) ensures self: Self; // FLUX:mut-ref-unfolding
+            }
+        }
+    }
+}]
 const _: () = {};
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index f0fa4ac9f1026..76d2b7af4d073 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -53,8 +53,8 @@ struct Hasher<S: Sip> {
     length: usize, // how many bytes we've processed
     state: State,  // hash State
     tail: u64,     // unprocessed bytes le
-    #[cfg_attr(flux, flux::field(usize{v: v <= 8}))]
-    ntail: usize,  // how many bytes in tail are valid
+    // DETACH? #[cfg_attr(flux, flux::field(usize{v: v <= 8}))]
+    ntail: usize, // how many bytes in tail are valid
     _marker: PhantomData<S>,
 }
 
@@ -159,7 +159,9 @@ impl SipHasher {
     #[deprecated(since = "1.13.0", note = "use `std::hash::DefaultHasher` instead")]
     #[must_use]
     pub fn new_with_keys(key0: u64, key1: u64) -> SipHasher {
-        SipHasher(SipHasher24 { hasher: Hasher::new_with_keys(key0, key1) })
+        SipHasher(SipHasher24 {
+            hasher: Hasher::new_with_keys(key0, key1),
+        })
     }
 }
 
@@ -177,7 +179,9 @@ impl SipHasher13 {
     #[unstable(feature = "hashmap_internals", issue = "none")]
     #[deprecated(since = "1.13.0", note = "use `std::hash::DefaultHasher` instead")]
     pub fn new_with_keys(key0: u64, key1: u64) -> SipHasher13 {
-        SipHasher13 { hasher: Hasher::new_with_keys(key0, key1) }
+        SipHasher13 {
+            hasher: Hasher::new_with_keys(key0, key1),
+        }
     }
 }
 
@@ -188,7 +192,12 @@ impl<S: Sip> Hasher<S> {
             k0: key0,
             k1: key1,
             length: 0,
-            state: State { v0: 0, v1: 0, v2: 0, v3: 0 },
+            state: State {
+                v0: 0,
+                v1: 0,
+                v2: 0,
+                v3: 0,
+            },
             tail: 0,
             ntail: 0,
             _marker: PhantomData,

From 27ebaaf8007d036e2075c6a271f31973c7b9281a Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 29 Jul 2025 16:29:59 -0700
Subject: [PATCH 11/42] yay, detached a trait-impl!

---
 library/core/src/flux_info.rs | 4 ++--
 library/core/src/hash/sip.rs  | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 21889d44e4741..ccaf97fb05fc2 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -45,8 +45,8 @@
               _marker: PhantomData<S>,
             }
 
-            impl Hasher for Hasher<S> {
-                fn wrote(self: &mut Self, msg: &[u8]) ensures self: Self; // FLUX:mut-ref-unfolding
+            impl Hasher for hash::sip::Hasher<S> {
+                fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // FLUX:mut-ref-unfolding
             }
         }
     }
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index 76d2b7af4d073..ab7cb73c3d2a7 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -262,7 +262,7 @@ impl<S: Sip> super::Hasher for Hasher<S> {
     // slightly slowing down compile speeds on some benchmarks. See #69152 for
     // details.
     #[inline]
-    #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
+    // #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
     fn write(&mut self, msg: &[u8]) {
         let length = msg.len();
         self.length += length;

From 5e49876f2ab2066f81b26c5d1e7629f4c7bb4027 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 29 Jul 2025 18:55:16 -0700
Subject: [PATCH 12/42] last: pat.rs

---
 library/core/src/flux_info.rs | 23 +++++++++--
 library/core/src/hash/mod.rs  |  7 +++-
 library/core/src/hash/sip.rs  |  2 +-
 library/core/src/time.rs      | 78 +++++++++++++++++++++++++++--------
 4 files changed, 86 insertions(+), 24 deletions(-)

diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index ccaf97fb05fc2..305f179f2c782 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -45,10 +45,27 @@
               _marker: PhantomData<S>,
             }
 
-            impl Hasher for hash::sip::Hasher<S> {
-                fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // FLUX:mut-ref-unfolding
-            }
+
         }
+
+        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; // FLUX: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/hash/mod.rs b/library/core/src/hash/mod.rs
index 6aaa9349a913b..a806b7aa88825 100644
--- a/library/core/src/hash/mod.rs
+++ b/library/core/src/hash/mod.rs
@@ -752,7 +752,7 @@ pub struct BuildHasherDefault<H>(marker::PhantomData<fn() -> H>);
 
 impl<H> BuildHasherDefault<H> {
     /// Creates a new BuildHasherDefault for Hasher `H`.
-    #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
+    // DETACH? #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
     #[stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     #[rustc_const_stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     pub const fn new() -> Self {
@@ -778,7 +778,10 @@ impl<H: Default + Hasher> BuildHasher for BuildHasherDefault<H> {
 
 #[stable(since = "1.7.0", feature = "build_hasher")]
 impl<H> Clone for BuildHasherDefault<H> {
-    #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
+    // DETACH? #[cfg_attr(
+    //     flux,
+    //     flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185")
+    // )]
     fn clone(&self) -> BuildHasherDefault<H> {
         BuildHasherDefault(marker::PhantomData)
     }
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index ab7cb73c3d2a7..12f9c5353cab0 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -262,7 +262,7 @@ impl<S: Sip> super::Hasher for Hasher<S> {
     // slightly slowing down compile speeds on some benchmarks. See #69152 for
     // details.
     #[inline]
-    // #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
+    // DETACH? #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
     fn write(&mut self, msg: &[u8]) {
         let length = msg.len();
         self.length += length;
diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 29e9e8eb19bd4..469e6d82b3e78 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -208,14 +208,20 @@ impl Duration {
     pub const fn new(secs: u64, nanos: u32) -> Duration {
         if nanos < NANOS_PER_SEC {
             // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range
-            Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } }
+            Duration {
+                secs,
+                nanos: unsafe { Nanoseconds::new_unchecked(nanos) },
+            }
         } else {
             let secs = secs
                 .checked_add((nanos / NANOS_PER_SEC) as u64)
                 .expect("overflow in Duration::new");
             let nanos = nanos % NANOS_PER_SEC;
             // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range
-            Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } }
+            Duration {
+                secs,
+                nanos: unsafe { Nanoseconds::new_unchecked(nanos) },
+            }
         }
     }
 
@@ -238,7 +244,10 @@ impl Duration {
     #[ensures(|duration| duration.is_safe())]
     #[ensures(|duration| duration.secs == secs)]
     pub const fn from_secs(secs: u64) -> Duration {
-        Duration { secs, nanos: Nanoseconds::ZERO }
+        Duration {
+            secs,
+            nanos: Nanoseconds::ZERO,
+        }
     }
 
     /// Creates a new `Duration` from the specified number of milliseconds.
@@ -265,7 +274,10 @@ impl Duration {
         //         => x % 1_000 < 1_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_millis * NANOS_PER_MILLI) };
 
-        Duration { secs, nanos: subsec_nanos }
+        Duration {
+            secs,
+            nanos: subsec_nanos,
+        }
     }
 
     /// Creates a new `Duration` from the specified number of microseconds.
@@ -292,7 +304,10 @@ impl Duration {
         //         => x % 1_000_000 < 1_000_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_micros * NANOS_PER_MICRO) };
 
-        Duration { secs, nanos: subsec_nanos }
+        Duration {
+            secs,
+            nanos: subsec_nanos,
+        }
     }
 
     /// Creates a new `Duration` from the specified number of nanoseconds.
@@ -324,7 +339,10 @@ impl Duration {
         // SAFETY: x % 1_000_000_000 < 1_000_000_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_nanos) };
 
-        Duration { secs, nanos: subsec_nanos }
+        Duration {
+            secs,
+            nanos: subsec_nanos,
+        }
     }
 
     /// Creates a new `Duration` from the specified number of weeks.
@@ -638,7 +656,11 @@ impl Duration {
                   without modifying the original"]
     #[inline]
     pub const fn abs_diff(self, other: Duration) -> Duration {
-        if let Some(res) = self.checked_sub(other) { res } else { other.checked_sub(self).unwrap() }
+        if let Some(res) = self.checked_sub(other) {
+            res
+        } else {
+            other.checked_sub(self).unwrap()
+        }
     }
 
     /// Checked `Duration` addition. Computes `self + other`, returning [`None`]
@@ -1135,7 +1157,8 @@ impl Add for Duration {
 
     #[inline]
     fn add(self, rhs: Duration) -> Duration {
-        self.checked_add(rhs).expect("overflow when adding durations")
+        self.checked_add(rhs)
+            .expect("overflow when adding durations")
     }
 }
 
@@ -1153,7 +1176,8 @@ impl Sub for Duration {
 
     #[inline]
     fn sub(self, rhs: Duration) -> Duration {
-        self.checked_sub(rhs).expect("overflow when subtracting durations")
+        self.checked_sub(rhs)
+            .expect("overflow when subtracting durations")
     }
 }
 
@@ -1171,7 +1195,8 @@ impl Mul<u32> for Duration {
 
     #[inline]
     fn mul(self, rhs: u32) -> Duration {
-        self.checked_mul(rhs).expect("overflow when multiplying duration by scalar")
+        self.checked_mul(rhs)
+            .expect("overflow when multiplying duration by scalar")
     }
 }
 
@@ -1200,7 +1225,8 @@ impl Div<u32> for Duration {
     #[inline]
     #[track_caller]
     fn div(self, rhs: u32) -> Duration {
-        self.checked_div(rhs).expect("divide by zero error when dividing duration by scalar")
+        self.checked_div(rhs)
+            .expect("divide by zero error when dividing duration by scalar")
     }
 }
 
@@ -1219,8 +1245,9 @@ macro_rules! sum_durations {
         let mut total_nanos: u64 = 0;
 
         for entry in $iter {
-            total_secs =
-                total_secs.checked_add(entry.secs).expect("overflow in iter::sum over durations");
+            total_secs = total_secs
+                .checked_add(entry.secs)
+                .expect("overflow in iter::sum over durations");
             total_nanos = match total_nanos.checked_add(entry.nanos.as_inner() as u64) {
                 Some(n) => n,
                 None => {
@@ -1255,6 +1282,7 @@ impl<'a> Sum<&'a Duration> for Duration {
 
 #[stable(feature = "duration_debug_impl", since = "1.27.0")]
 impl fmt::Debug for Duration {
+    // DETACH? #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant, nested"))]
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         /// Formats a floating point number in decimal notation.
         ///
@@ -1269,7 +1297,6 @@ impl fmt::Debug for Duration {
         ///
         /// A prefix and postfix may be added. The whole thing is padded
         /// to the formatter's `width`, if specified.
-        #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant"))]
         fn fmt_decimal(
             f: &mut fmt::Formatter<'_>,
             integer_part: u64,
@@ -1421,7 +1448,14 @@ impl fmt::Debug for Duration {
         let prefix = if f.sign_plus() { "+" } else { "" };
 
         if self.secs > 0 {
-            fmt_decimal(f, self.secs, self.nanos.as_inner(), NANOS_PER_SEC / 10, prefix, "s")
+            fmt_decimal(
+                f,
+                self.secs,
+                self.nanos.as_inner(),
+                NANOS_PER_SEC / 10,
+                prefix,
+                "s",
+            )
         } else if self.nanos.as_inner() >= NANOS_PER_MILLI {
             fmt_decimal(
                 f,
@@ -1509,7 +1543,9 @@ macro_rules! try_from_secs {
         const EXP_MASK: $bits_ty = (1 << $exp_bits) - 1;
 
         if $secs < 0.0 {
-            return Err(TryFromFloatSecsError { kind: TryFromFloatSecsErrorKind::Negative });
+            return Err(TryFromFloatSecsError {
+                kind: TryFromFloatSecsErrorKind::Negative,
+            });
         }
 
         let bits = $secs.to_bits();
@@ -1537,7 +1573,11 @@ macro_rules! try_from_secs {
             // f32 does not have enough precision to trigger the second branch
             // since it can not represent numbers between 0.999_999_940_395 and 1.0.
             let nanos = nanos + add_ns as u32;
-            if ($mant_bits == 23) || (nanos != NANOS_PER_SEC) { (0, nanos) } else { (1, 0) }
+            if ($mant_bits == 23) || (nanos != NANOS_PER_SEC) {
+                (0, nanos)
+            } else {
+                (1, 0)
+            }
         } else if exp < $mant_bits {
             let secs = u64::from(mant >> ($mant_bits - exp));
             let t = <$double_ty>::from((mant << exp) & MANT_MASK);
@@ -1568,7 +1608,9 @@ macro_rules! try_from_secs {
             let secs = u64::from(mant) << (exp - $mant_bits);
             (secs, 0)
         } else {
-            return Err(TryFromFloatSecsError { kind: TryFromFloatSecsErrorKind::OverflowOrNan });
+            return Err(TryFromFloatSecsError {
+                kind: TryFromFloatSecsErrorKind::OverflowOrNan,
+            });
         };
 
         Ok(Duration::new(secs, nanos))

From d6cad502cac7c14ce796b9cb03af1ec1ca1de36b Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 29 Jul 2025 19:09:55 -0700
Subject: [PATCH 13/42] done detach2

---
 library/core/src/flux_info.rs | 19 +++++++++++++++++++
 library/core/src/pat.rs       |  8 ++++----
 2 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 305f179f2c782..a807e80e57231 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -67,5 +67,24 @@
         #[trusted]         // reason = modular arithmetic invariant inside nested fmt_decimal
         fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result;
     }
+
+    mod pat {
+        trait RangePattern {
+            #[reft]
+            fn sub_ok(self: Self) -> bool { true }
+
+            fn sub_one(self: Self{<Self as RangePattern>::sub_ok(self)}) -> Self;
+        }
+    }
+
+    impl RangePattern for char {
+        #[reft]
+        fn sub_ok(self: char) -> bool {
+            0 < char_to_int(self)
+        }
+
+        fn sub_one(self: char{<char as RangePattern>::sub_ok(self)}) -> char;
+
+    }
 }]
 const _: () = {};
diff --git a/library/core/src/pat.rs b/library/core/src/pat.rs
index 1f86d859d1f58..46743b6cdbca4 100644
--- a/library/core/src/pat.rs
+++ b/library/core/src/pat.rs
@@ -16,7 +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 }))]
+// DETACH? #[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]
@@ -34,7 +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))]
+    // DETACH? #[cfg_attr(flux, flux::spec(fn (self: Self{<Self as RangePattern>::sub_ok(self)}) -> Self))]
     #[lang = "RangeSub"]
     #[track_caller]
     fn sub_one(self) -> Self;
@@ -64,13 +64,13 @@ impl_range_pat! {
 }
 
 #[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")]
-#[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self) }))]
+// DETACH? #[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self) }))]
 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))]
+    // DETACH? #[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 aed746ac7d55595d7c4732608368f98ec40124f9 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:08:00 -0700
Subject: [PATCH 14/42] remove detached

---
 library/core/src/ascii/ascii_char.rs | 1 -
 library/core/src/hash/mod.rs         | 5 -----
 library/core/src/hash/sip.rs         | 4 +---
 library/core/src/pat.rs              | 4 ----
 library/core/src/time.rs             | 1 -
 5 files changed, 1 insertion(+), 14 deletions(-)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index fbdc6d3ecdb7d..47d0c70ca397e 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -529,7 +529,6 @@ impl AsciiChar {
 
     /// Gets this ASCII character as a byte.
     #[unstable(feature = "ascii_char", issue = "110998")]
-    // DETACH? #[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/hash/mod.rs b/library/core/src/hash/mod.rs
index a806b7aa88825..a10c85640bbb6 100644
--- a/library/core/src/hash/mod.rs
+++ b/library/core/src/hash/mod.rs
@@ -752,7 +752,6 @@ pub struct BuildHasherDefault<H>(marker::PhantomData<fn() -> H>);
 
 impl<H> BuildHasherDefault<H> {
     /// Creates a new BuildHasherDefault for Hasher `H`.
-    // DETACH? #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
     #[stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     #[rustc_const_stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     pub const fn new() -> Self {
@@ -778,10 +777,6 @@ impl<H: Default + Hasher> BuildHasher for BuildHasherDefault<H> {
 
 #[stable(since = "1.7.0", feature = "build_hasher")]
 impl<H> Clone for BuildHasherDefault<H> {
-    // DETACH? #[cfg_attr(
-    //     flux,
-    //     flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185")
-    // )]
     fn clone(&self) -> BuildHasherDefault<H> {
         BuildHasherDefault(marker::PhantomData)
     }
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index 12f9c5353cab0..e90e19c14cfdb 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -53,8 +53,7 @@ struct Hasher<S: Sip> {
     length: usize, // how many bytes we've processed
     state: State,  // hash State
     tail: u64,     // unprocessed bytes le
-    // DETACH? #[cfg_attr(flux, flux::field(usize{v: v <= 8}))]
-    ntail: usize, // how many bytes in tail are valid
+    ntail: usize,  // how many bytes in tail are valid
     _marker: PhantomData<S>,
 }
 
@@ -262,7 +261,6 @@ impl<S: Sip> super::Hasher for Hasher<S> {
     // slightly slowing down compile speeds on some benchmarks. See #69152 for
     // details.
     #[inline]
-    // DETACH? #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
     fn write(&mut self, msg: &[u8]) {
         let length = msg.len();
         self.length += length;
diff --git a/library/core/src/pat.rs b/library/core/src/pat.rs
index 46743b6cdbca4..91d015b1bc53f 100644
--- a/library/core/src/pat.rs
+++ b/library/core/src/pat.rs
@@ -16,7 +16,6 @@ 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.
-// DETACH? #[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]
@@ -34,7 +33,6 @@ pub trait RangePattern {
     const MAX: Self;
 
     /// A compile-time helper to subtract 1 for exclusive ranges.
-    // DETACH? #[cfg_attr(flux, flux::spec(fn (self: Self{<Self as RangePattern>::sub_ok(self)}) -> Self))]
     #[lang = "RangeSub"]
     #[track_caller]
     fn sub_one(self) -> Self;
@@ -64,13 +62,11 @@ impl_range_pat! {
 }
 
 #[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")]
-// DETACH? #[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self) }))]
 impl const RangePattern for char {
     const MIN: Self = char::MIN;
 
     const MAX: Self = char::MAX;
 
-    // DETACH? #[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"),
diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 469e6d82b3e78..7acbacb70c83b 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -1282,7 +1282,6 @@ impl<'a> Sum<&'a Duration> for Duration {
 
 #[stable(feature = "duration_debug_impl", since = "1.27.0")]
 impl fmt::Debug for Duration {
-    // DETACH? #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant, nested"))]
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         /// Formats a floating point number in decimal notation.
         ///

From 21043037c6557cb1f181705460629372e67dd0f1 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:13:21 -0700
Subject: [PATCH 15/42] format

---
 library/core/src/ascii/ascii_char.rs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index 47d0c70ca397e..b7240840d2cca 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -614,10 +614,7 @@ impl fmt::Debug for AsciiChar {
                 let byte = self.to_u8();
                 let hi = HEX_DIGITS[usize::from(byte >> 4)];
                 let lo = HEX_DIGITS[usize::from(byte & 0xf)];
-                (
-                    [Apostrophe, Backslash, AsciiChar::SmallX, hi, lo, Apostrophe],
-                    6,
-                )
+                ([Apostrophe, Backslash, AsciiChar::SmallX, hi, lo, Apostrophe], 6)
             }
             _ => ([Apostrophe, *self, Apostrophe, Null, Null, Null], 3),
         };

From 77aa659230b6165b993dfee65a8c42c973a95680 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:15:53 -0700
Subject: [PATCH 16/42] format

---
 library/core/src/hash/sip.rs | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index e90e19c14cfdb..55725f4730dfd 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -158,9 +158,7 @@ impl SipHasher {
     #[deprecated(since = "1.13.0", note = "use `std::hash::DefaultHasher` instead")]
     #[must_use]
     pub fn new_with_keys(key0: u64, key1: u64) -> SipHasher {
-        SipHasher(SipHasher24 {
-            hasher: Hasher::new_with_keys(key0, key1),
-        })
+        SipHasher(SipHasher24 { hasher: Hasher::new_with_keys(key0, key1) })
     }
 }
 
@@ -191,12 +189,7 @@ impl<S: Sip> Hasher<S> {
             k0: key0,
             k1: key1,
             length: 0,
-            state: State {
-                v0: 0,
-                v1: 0,
-                v2: 0,
-                v3: 0,
-            },
+            state: State { v0: 0, v1: 0, v2: 0, v3: 0 },
             tail: 0,
             ntail: 0,
             _marker: PhantomData,

From b7affa6830136b1a11bcc426362f6391d5f8e043 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:16:25 -0700
Subject: [PATCH 17/42] format

---
 library/core/src/hash/sip.rs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index 55725f4730dfd..780e522c48ebf 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -176,9 +176,7 @@ impl SipHasher13 {
     #[unstable(feature = "hashmap_internals", issue = "none")]
     #[deprecated(since = "1.13.0", note = "use `std::hash::DefaultHasher` instead")]
     pub fn new_with_keys(key0: u64, key1: u64) -> SipHasher13 {
-        SipHasher13 {
-            hasher: Hasher::new_with_keys(key0, key1),
-        }
+        SipHasher13 { hasher: Hasher::new_with_keys(key0, key1) }
     }
 }
 

From 800d19a8ee6425022b2ba19b10e4987cbb26d8f6 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:19:31 -0700
Subject: [PATCH 18/42] restore time

---
 library/core/src/time.rs | 77 ++++++++++------------------------------
 1 file changed, 18 insertions(+), 59 deletions(-)

diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 7acbacb70c83b..29e9e8eb19bd4 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -208,20 +208,14 @@ impl Duration {
     pub const fn new(secs: u64, nanos: u32) -> Duration {
         if nanos < NANOS_PER_SEC {
             // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range
-            Duration {
-                secs,
-                nanos: unsafe { Nanoseconds::new_unchecked(nanos) },
-            }
+            Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } }
         } else {
             let secs = secs
                 .checked_add((nanos / NANOS_PER_SEC) as u64)
                 .expect("overflow in Duration::new");
             let nanos = nanos % NANOS_PER_SEC;
             // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range
-            Duration {
-                secs,
-                nanos: unsafe { Nanoseconds::new_unchecked(nanos) },
-            }
+            Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } }
         }
     }
 
@@ -244,10 +238,7 @@ impl Duration {
     #[ensures(|duration| duration.is_safe())]
     #[ensures(|duration| duration.secs == secs)]
     pub const fn from_secs(secs: u64) -> Duration {
-        Duration {
-            secs,
-            nanos: Nanoseconds::ZERO,
-        }
+        Duration { secs, nanos: Nanoseconds::ZERO }
     }
 
     /// Creates a new `Duration` from the specified number of milliseconds.
@@ -274,10 +265,7 @@ impl Duration {
         //         => x % 1_000 < 1_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_millis * NANOS_PER_MILLI) };
 
-        Duration {
-            secs,
-            nanos: subsec_nanos,
-        }
+        Duration { secs, nanos: subsec_nanos }
     }
 
     /// Creates a new `Duration` from the specified number of microseconds.
@@ -304,10 +292,7 @@ impl Duration {
         //         => x % 1_000_000 < 1_000_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_micros * NANOS_PER_MICRO) };
 
-        Duration {
-            secs,
-            nanos: subsec_nanos,
-        }
+        Duration { secs, nanos: subsec_nanos }
     }
 
     /// Creates a new `Duration` from the specified number of nanoseconds.
@@ -339,10 +324,7 @@ impl Duration {
         // SAFETY: x % 1_000_000_000 < 1_000_000_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_nanos) };
 
-        Duration {
-            secs,
-            nanos: subsec_nanos,
-        }
+        Duration { secs, nanos: subsec_nanos }
     }
 
     /// Creates a new `Duration` from the specified number of weeks.
@@ -656,11 +638,7 @@ impl Duration {
                   without modifying the original"]
     #[inline]
     pub const fn abs_diff(self, other: Duration) -> Duration {
-        if let Some(res) = self.checked_sub(other) {
-            res
-        } else {
-            other.checked_sub(self).unwrap()
-        }
+        if let Some(res) = self.checked_sub(other) { res } else { other.checked_sub(self).unwrap() }
     }
 
     /// Checked `Duration` addition. Computes `self + other`, returning [`None`]
@@ -1157,8 +1135,7 @@ impl Add for Duration {
 
     #[inline]
     fn add(self, rhs: Duration) -> Duration {
-        self.checked_add(rhs)
-            .expect("overflow when adding durations")
+        self.checked_add(rhs).expect("overflow when adding durations")
     }
 }
 
@@ -1176,8 +1153,7 @@ impl Sub for Duration {
 
     #[inline]
     fn sub(self, rhs: Duration) -> Duration {
-        self.checked_sub(rhs)
-            .expect("overflow when subtracting durations")
+        self.checked_sub(rhs).expect("overflow when subtracting durations")
     }
 }
 
@@ -1195,8 +1171,7 @@ impl Mul<u32> for Duration {
 
     #[inline]
     fn mul(self, rhs: u32) -> Duration {
-        self.checked_mul(rhs)
-            .expect("overflow when multiplying duration by scalar")
+        self.checked_mul(rhs).expect("overflow when multiplying duration by scalar")
     }
 }
 
@@ -1225,8 +1200,7 @@ impl Div<u32> for Duration {
     #[inline]
     #[track_caller]
     fn div(self, rhs: u32) -> Duration {
-        self.checked_div(rhs)
-            .expect("divide by zero error when dividing duration by scalar")
+        self.checked_div(rhs).expect("divide by zero error when dividing duration by scalar")
     }
 }
 
@@ -1245,9 +1219,8 @@ macro_rules! sum_durations {
         let mut total_nanos: u64 = 0;
 
         for entry in $iter {
-            total_secs = total_secs
-                .checked_add(entry.secs)
-                .expect("overflow in iter::sum over durations");
+            total_secs =
+                total_secs.checked_add(entry.secs).expect("overflow in iter::sum over durations");
             total_nanos = match total_nanos.checked_add(entry.nanos.as_inner() as u64) {
                 Some(n) => n,
                 None => {
@@ -1296,6 +1269,7 @@ impl fmt::Debug for Duration {
         ///
         /// A prefix and postfix may be added. The whole thing is padded
         /// to the formatter's `width`, if specified.
+        #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant"))]
         fn fmt_decimal(
             f: &mut fmt::Formatter<'_>,
             integer_part: u64,
@@ -1447,14 +1421,7 @@ impl fmt::Debug for Duration {
         let prefix = if f.sign_plus() { "+" } else { "" };
 
         if self.secs > 0 {
-            fmt_decimal(
-                f,
-                self.secs,
-                self.nanos.as_inner(),
-                NANOS_PER_SEC / 10,
-                prefix,
-                "s",
-            )
+            fmt_decimal(f, self.secs, self.nanos.as_inner(), NANOS_PER_SEC / 10, prefix, "s")
         } else if self.nanos.as_inner() >= NANOS_PER_MILLI {
             fmt_decimal(
                 f,
@@ -1542,9 +1509,7 @@ macro_rules! try_from_secs {
         const EXP_MASK: $bits_ty = (1 << $exp_bits) - 1;
 
         if $secs < 0.0 {
-            return Err(TryFromFloatSecsError {
-                kind: TryFromFloatSecsErrorKind::Negative,
-            });
+            return Err(TryFromFloatSecsError { kind: TryFromFloatSecsErrorKind::Negative });
         }
 
         let bits = $secs.to_bits();
@@ -1572,11 +1537,7 @@ macro_rules! try_from_secs {
             // f32 does not have enough precision to trigger the second branch
             // since it can not represent numbers between 0.999_999_940_395 and 1.0.
             let nanos = nanos + add_ns as u32;
-            if ($mant_bits == 23) || (nanos != NANOS_PER_SEC) {
-                (0, nanos)
-            } else {
-                (1, 0)
-            }
+            if ($mant_bits == 23) || (nanos != NANOS_PER_SEC) { (0, nanos) } else { (1, 0) }
         } else if exp < $mant_bits {
             let secs = u64::from(mant >> ($mant_bits - exp));
             let t = <$double_ty>::from((mant << exp) & MANT_MASK);
@@ -1607,9 +1568,7 @@ macro_rules! try_from_secs {
             let secs = u64::from(mant) << (exp - $mant_bits);
             (secs, 0)
         } else {
-            return Err(TryFromFloatSecsError {
-                kind: TryFromFloatSecsErrorKind::OverflowOrNan,
-            });
+            return Err(TryFromFloatSecsError { kind: TryFromFloatSecsErrorKind::OverflowOrNan });
         };
 
         Ok(Duration::new(secs, nanos))

From 6ddfc776fae34d16fcb948451e6d5d1cc94fe48a Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:19:41 -0700
Subject: [PATCH 19/42] restore time remove flux

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

diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 29e9e8eb19bd4..059ab5506ece3 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -1269,7 +1269,6 @@ impl fmt::Debug for Duration {
         ///
         /// A prefix and postfix may be added. The whole thing is padded
         /// to the formatter's `width`, if specified.
-        #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant"))]
         fn fmt_decimal(
             f: &mut fmt::Formatter<'_>,
             integer_part: u64,

From c942c6b4072e1cb2474dc9ccca329327cfa7e6f5 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 10:20:25 -0700
Subject: [PATCH 20/42] sigh

---
 library/Cargo.lock | 90 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 90 insertions(+)

diff --git a/library/Cargo.lock b/library/Cargo.lock
index c681c5935df5f..aa756e9e6aa94 100644
--- a/library/Cargo.lock
+++ b/library/Cargo.lock
@@ -28,6 +28,7 @@ version = "0.0.0"
 dependencies = [
  "compiler_builtins",
  "core",
+ "safety",
 ]
 
 [[package]]
@@ -67,6 +68,9 @@ dependencies = [
 [[package]]
 name = "core"
 version = "0.0.0"
+dependencies = [
+ "safety",
+]
 
 [[package]]
 name = "coretests"
@@ -201,6 +205,39 @@ dependencies = [
  "unwind",
 ]
 
+[[package]]
+name = "proc-macro-error"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
+dependencies = [
+ "proc-macro-error-attr",
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro-error-attr"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.95"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "02b3e5e68a3a1a02aad3ec490a98007cbc13c37cbe84a3cd7b8e406d76e7f778"
+dependencies = [
+ "unicode-ident",
+]
+
 [[package]]
 name = "proc_macro"
 version = "0.0.0"
@@ -217,6 +254,15 @@ dependencies = [
  "cc",
 ]
 
+[[package]]
+name = "quote"
+version = "1.0.40"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1885c039570dc00dcb4ff087a89e185fd56bae234ddc7f056a945bf36467248d"
+dependencies = [
+ "proc-macro2",
+]
+
 [[package]]
 name = "r-efi"
 version = "5.3.0"
@@ -301,6 +347,16 @@ dependencies = [
  "std",
 ]
 
+[[package]]
+name = "safety"
+version = "0.1.0"
+dependencies = [
+ "proc-macro-error",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.104",
+]
+
 [[package]]
 name = "shlex"
 version = "1.3.0"
@@ -330,6 +386,7 @@ dependencies = [
  "rand",
  "rand_xorshift",
  "rustc-demangle",
+ "safety",
  "std_detect",
  "unwind",
  "wasi",
@@ -346,6 +403,27 @@ dependencies = [
  "rustc-std-workspace-core",
 ]
 
+[[package]]
+name = "syn"
+version = "1.0.109"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
+dependencies = [
+ "proc-macro2",
+ "unicode-ident",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.104"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "17b6f705963418cdb9927482fa304bc562ece2fdd4f616084c50b7023b435a40"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "sysroot"
 version = "0.0.0"
@@ -366,6 +444,12 @@ dependencies = [
  "std",
 ]
 
+[[package]]
+name = "unicode-ident"
+version = "1.0.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5a5f39404a5da50712a4c1eecf25e90dd62b613502b7e925fd4e4d19b5c96512"
+
 [[package]]
 name = "unicode-width"
 version = "0.2.1"
@@ -398,6 +482,12 @@ dependencies = [
  "rustc-std-workspace-core",
 ]
 
+[[package]]
+name = "version_check"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
+
 [[package]]
 name = "wasi"
 version = "0.11.1+wasi-snapshot-preview1"

From 83cfb471a548783a1c1ad320b8b93a666a5d08a1 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Thu, 26 Jun 2025 11:23:33 -0700
Subject: [PATCH 21/42] rebasing detached (step 1)

---
 library/core/src/convert/num.rs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs
index 1a30a75de7ef6..8e112f9184103 100644
--- a/library/core/src/convert/num.rs
+++ b/library/core/src/convert/num.rs
@@ -69,14 +69,15 @@ macro_rules! impl_from {
             ),
         );
     };
-    ($Small:ty => $Large:ty, #[$attr:meta] $(,)?) => {
+    ($Small:ty => $Large:ty, #[$attr:meta] $(, #[$flux_attr:meta])? $(,)?) => {
         impl_from!(
             $Small => $Large,
             #[$attr],
             concat!("Converts [`", stringify!($Small), "`] to [`", stringify!($Large), "`] losslessly."),
+            $(#[$flux_attr],)?
         );
     };
-    ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(,)?) => {
+    ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(,  #[$flux_attr:meta])? $(,)?) => {
         #[$attr]
         #[rustc_const_unstable(feature = "const_try", issue = "74935")]
         impl const From<$Small> for $Large {
@@ -111,7 +112,7 @@ impl_from!(u8 => u16, #[stable(feature = "lossless_int_conv", since = "1.5.0")])
 impl_from!(u8 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u8 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u8 => u128, #[stable(feature = "i128", since = "1.26.0")]);
-impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
+impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")], #[cfg_attr(flux, flux::spec(fn(x:u8) -> usize[x]))]);
 impl_from!(u16 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u128, #[stable(feature = "i128", since = "1.26.0")]);

From e10ddf475cd4ea64ad094c6e4a04715759b1ef88 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Mon, 14 Jul 2025 14:24:01 -0700
Subject: [PATCH 22/42] update convert with cast (only)

---
 library/core/src/convert/num.rs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs
index 8e112f9184103..1a30a75de7ef6 100644
--- a/library/core/src/convert/num.rs
+++ b/library/core/src/convert/num.rs
@@ -69,15 +69,14 @@ macro_rules! impl_from {
             ),
         );
     };
-    ($Small:ty => $Large:ty, #[$attr:meta] $(, #[$flux_attr:meta])? $(,)?) => {
+    ($Small:ty => $Large:ty, #[$attr:meta] $(,)?) => {
         impl_from!(
             $Small => $Large,
             #[$attr],
             concat!("Converts [`", stringify!($Small), "`] to [`", stringify!($Large), "`] losslessly."),
-            $(#[$flux_attr],)?
         );
     };
-    ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(,  #[$flux_attr:meta])? $(,)?) => {
+    ($Small:ty => $Large:ty, #[$attr:meta], $doc:expr $(,)?) => {
         #[$attr]
         #[rustc_const_unstable(feature = "const_try", issue = "74935")]
         impl const From<$Small> for $Large {
@@ -112,7 +111,7 @@ impl_from!(u8 => u16, #[stable(feature = "lossless_int_conv", since = "1.5.0")])
 impl_from!(u8 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u8 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u8 => u128, #[stable(feature = "i128", since = "1.26.0")]);
-impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")], #[cfg_attr(flux, flux::spec(fn(x:u8) -> usize[x]))]);
+impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]);
 impl_from!(u16 => u128, #[stable(feature = "i128", since = "1.26.0")]);

From ff1157ca4f5ddcf34876260052c9cdadf2d32f49 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 12:21:43 -0700
Subject: [PATCH 23/42] DONE: pat

---
 library/Cargo.lock            | 21 +++++++++++++++++++++
 library/core/Cargo.toml       |  3 ++-
 library/core/src/flux_info.rs | 13 +++++++++++--
 library/core/src/pat.rs       |  4 ++++
 4 files changed, 38 insertions(+), 3 deletions(-)

diff --git a/library/Cargo.lock b/library/Cargo.lock
index 3e34ee6173741..fc6366e278ef0 100644
--- a/library/Cargo.lock
+++ b/library/Cargo.lock
@@ -423,6 +423,27 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "syn"
+version = "1.0.109"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
+dependencies = [
+ "proc-macro2",
+ "unicode-ident",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.104"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "17b6f705963418cdb9927482fa304bc562ece2fdd4f616084c50b7023b435a40"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "sysroot"
 version = "0.0.0"
diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index e676e88f4d4d8..0ecd0a40e712a 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -47,4 +47,5 @@ check-cfg = [
 
 [package.metadata.flux]
 enabled = true
-include = [ "src/ascii{*.rs,/**/*.rs}" ]
+include = [ "src/ascii{*.rs,/**/*.rs}",
+            "src/pat{*.rs,/**/*.rs}" ]
diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index c1aa8f1506cff..82acac82a1402 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -4,12 +4,21 @@
 /// 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(c:char) -> int { 
+        cast(c) 
+    } 
+
     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)
     }
 }]
 const _: () = {};
diff --git a/library/core/src/pat.rs b/library/core/src/pat.rs
index 91d015b1bc53f..1f86d859d1f58 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;
@@ -62,11 +64,13 @@ impl_range_pat! {
 }
 
 #[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")]
+#[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self) }))]
 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 b2048f42ed009c88917d71ff4f3d2e5ccc430218 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 12:22:39 -0700
Subject: [PATCH 24/42] DONE: bstr

---
 library/core/Cargo.toml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index 0ecd0a40e712a..7b00ee9a5f6cd 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -48,4 +48,6 @@ check-cfg = [
 [package.metadata.flux]
 enabled = true
 include = [ "src/ascii{*.rs,/**/*.rs}",
-            "src/pat{*.rs,/**/*.rs}" ]
+            "src/pat{*.rs,/**/*.rs}", 
+            "src/bstr{*.rs,/**/*.rs}",
+          ]

From b90422436c26f6ecde1a05f5d74004f18bcb72b2 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 12:37:41 -0700
Subject: [PATCH 25/42] PAUSE: flux #1185

---
 library/core/Cargo.toml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index 7b00ee9a5f6cd..b2e057186dbae 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -50,4 +50,5 @@ enabled = true
 include = [ "src/ascii{*.rs,/**/*.rs}",
             "src/pat{*.rs,/**/*.rs}", 
             "src/bstr{*.rs,/**/*.rs}",
+            "src/hash{*.rs,/**/*.rs}",
           ]

From ec773f72d2ec1d800cf6f17acc4de18c47f738a1 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 13:03:33 -0700
Subject: [PATCH 26/42] DONE: hash

---
 library/core/src/hash/mod.rs | 2 ++
 library/core/src/hash/sip.rs | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/library/core/src/hash/mod.rs b/library/core/src/hash/mod.rs
index a10c85640bbb6..6aaa9349a913b 100644
--- a/library/core/src/hash/mod.rs
+++ b/library/core/src/hash/mod.rs
@@ -752,6 +752,7 @@ pub struct BuildHasherDefault<H>(marker::PhantomData<fn() -> H>);
 
 impl<H> BuildHasherDefault<H> {
     /// Creates a new BuildHasherDefault for Hasher `H`.
+    #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
     #[stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     #[rustc_const_stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     pub const fn new() -> Self {
@@ -777,6 +778,7 @@ impl<H: Default + Hasher> BuildHasher for BuildHasherDefault<H> {
 
 #[stable(since = "1.7.0", feature = "build_hasher")]
 impl<H> Clone for BuildHasherDefault<H> {
+    #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
     fn clone(&self) -> BuildHasherDefault<H> {
         BuildHasherDefault(marker::PhantomData)
     }
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index 780e522c48ebf..f0fa4ac9f1026 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -53,6 +53,7 @@ struct Hasher<S: Sip> {
     length: usize, // how many bytes we've processed
     state: State,  // hash State
     tail: u64,     // unprocessed bytes le
+    #[cfg_attr(flux, flux::field(usize{v: v <= 8}))]
     ntail: usize,  // how many bytes in tail are valid
     _marker: PhantomData<S>,
 }
@@ -252,6 +253,7 @@ impl<S: Sip> super::Hasher for Hasher<S> {
     // slightly slowing down compile speeds on some benchmarks. See #69152 for
     // details.
     #[inline]
+    #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
     fn write(&mut self, msg: &[u8]) {
         let length = msg.len();
         self.length += length;

From 94c18c11c9e418c4f0900ae17431795bca269d41 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 13:06:44 -0700
Subject: [PATCH 27/42] NEXT: NANOSEC invariant

---
 library/core/Cargo.toml  | 1 +
 library/core/src/time.rs | 1 +
 2 files changed, 2 insertions(+)

diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index b2e057186dbae..16130fa08f802 100644
--- a/library/core/Cargo.toml
+++ b/library/core/Cargo.toml
@@ -51,4 +51,5 @@ include = [ "src/ascii{*.rs,/**/*.rs}",
             "src/pat{*.rs,/**/*.rs}", 
             "src/bstr{*.rs,/**/*.rs}",
             "src/hash{*.rs,/**/*.rs}",
+            "src/time{*.rs,/**/*.rs}",
           ]
diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 059ab5506ece3..29e9e8eb19bd4 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -1269,6 +1269,7 @@ impl fmt::Debug for Duration {
         ///
         /// A prefix and postfix may be added. The whole thing is padded
         /// to the formatter's `width`, if specified.
+        #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant"))]
         fn fmt_decimal(
             f: &mut fmt::Formatter<'_>,
             integer_part: u64,

From e65a2e5b97c2f9fcf62c2c2f78f8d0090f597713 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 15:04:39 -0700
Subject: [PATCH 28/42] NEXT: time -- needs `%` properties

---
 library/core/src/flux_info.rs       | 8 ++++++--
 library/core/src/num/niche_types.rs | 6 ++++++
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 82acac82a1402..18732a4f95dbb 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -5,8 +5,12 @@
 /// <https://flux-rs.github.io/flux/guide/specifications.html#extensible-properties-for-primitive-ops>
 #[flux::defs {
 
-    fn char_to_int(c:char) -> int { 
-        cast(c) 
+    fn as_int(x:int) -> int { 
+        x 
+    }
+
+    fn char_to_int(x:char) -> int { 
+        cast(x) 
     } 
 
     property ShiftRightByFour[>>](x, y) {
diff --git a/library/core/src/num/niche_types.rs b/library/core/src/num/niche_types.rs
index b92561c9e356d..a10db97cd370f 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(as_int($low) <= cast(val) && cast(val) <= as_int($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 == 0`, as it violates the validity
             /// invariant of this type.
             #[inline]
+            #[cfg_attr(flux, flux::spec(fn (val: $int{ as_int($low) <= cast(val) && cast(val) <= as_int($high) }) -> Self[{val:cast(val)}]))]
             pub const unsafe fn new_unchecked(val: $int) -> Self {
                 // SAFETY: Caller promised that `val` is non-zero.
                 unsafe { $name(val) }
             }
 
             #[inline]
+            #[cfg_attr(flux, flux::spec(fn (self: Self) -> $int[cast(self.val)] ensures as_int($low) <= cast(self.val) && cast(self.val) <= as_int($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.)

From 3777a6c9e9969563c31dfb1b9c2f31a9a8692e0d Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 15 Jul 2025 18:05:28 -0700
Subject: [PATCH 29/42] DONE: time

---
 library/core/src/num/niche_types.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/core/src/num/niche_types.rs b/library/core/src/num/niche_types.rs
index a10db97cd370f..2f3779253486a 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 == 0`, as it violates the validity
             /// invariant of this type.
             #[inline]
-            #[cfg_attr(flux, flux::spec(fn (val: $int{ as_int($low) <= cast(val) && cast(val) <= as_int($high) }) -> Self[{val:cast(val)}]))]
+            #[cfg_attr(flux, flux::spec(fn (val: $int{ as_int($low) <= cast(val) && cast(val) <= as_int($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 non-zero.
                 unsafe { $name(val) }

From b0a9792e114b7cebd7264b3b60ad6dc5f8940835 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Mon, 28 Jul 2025 18:56:11 -0700
Subject: [PATCH 30/42] temp

---
 library/core/src/ascii/ascii_char.rs |  7 ++++--
 library/core/src/flux_info.rs        | 36 ++++++++++++++++++++++++----
 library/core/src/hash/sip.rs         | 19 +++++++++++----
 3 files changed, 50 insertions(+), 12 deletions(-)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index 63e77df7cf317..14ba7107e8561 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -529,7 +529,7 @@ impl AsciiChar {
 
     /// Gets this ASCII character as a byte.
     #[unstable(feature = "ascii_char", issue = "110998")]
-    #[cfg_attr(flux, flux::spec(fn(Self) -> u8{v: v <= 127}))]
+    // DETACH? #[cfg_attr(flux, flux::spec(fn(Self) -> u8{v: v <= 127}))]
     #[inline]
     pub const fn to_u8(self) -> u8 {
         self as u8
@@ -616,7 +616,10 @@ impl fmt::Debug for AsciiChar {
                 let byte = self.to_u8();
                 let hi = HEX_DIGITS[usize::from(byte >> 4)];
                 let lo = HEX_DIGITS[usize::from(byte & 0xf)];
-                ([Apostrophe, Backslash, AsciiChar::SmallX, hi, lo, Apostrophe], 6)
+                (
+                    [Apostrophe, Backslash, AsciiChar::SmallX, hi, lo, Apostrophe],
+                    6,
+                )
             }
             _ => ([Apostrophe, *self, Apostrophe, Null, Null, Null], 3),
         };
diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 18732a4f95dbb..21889d44e4741 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -5,13 +5,13 @@
 /// <https://flux-rs.github.io/flux/guide/specifications.html#extensible-properties-for-primitive-ops>
 #[flux::defs {
 
-    fn as_int(x:int) -> int { 
-        x 
+    fn as_int(x:int) -> int {
+        x
     }
 
-    fn char_to_int(x:char) -> int { 
-        cast(x) 
-    } 
+    fn char_to_int(x:char) -> int {
+        cast(x)
+    }
 
     property ShiftRightByFour[>>](x, y) {
         16 * [>>](x, 4) == x
@@ -25,4 +25,30 @@
         0 < k => n <= [<<](n, k)
     }
 }]
+#[flux::specs {
+    mod ascii {
+        // AsciiChar is `crate::ascii::Char`
+        impl Char {
+            fn to_u8(Self) -> u8{v: v <= 127};
+        }
+    }
+
+    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 Hasher for Hasher<S> {
+                fn wrote(self: &mut Self, msg: &[u8]) ensures self: Self; // FLUX:mut-ref-unfolding
+            }
+        }
+    }
+}]
 const _: () = {};
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index f0fa4ac9f1026..76d2b7af4d073 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -53,8 +53,8 @@ struct Hasher<S: Sip> {
     length: usize, // how many bytes we've processed
     state: State,  // hash State
     tail: u64,     // unprocessed bytes le
-    #[cfg_attr(flux, flux::field(usize{v: v <= 8}))]
-    ntail: usize,  // how many bytes in tail are valid
+    // DETACH? #[cfg_attr(flux, flux::field(usize{v: v <= 8}))]
+    ntail: usize, // how many bytes in tail are valid
     _marker: PhantomData<S>,
 }
 
@@ -159,7 +159,9 @@ impl SipHasher {
     #[deprecated(since = "1.13.0", note = "use `std::hash::DefaultHasher` instead")]
     #[must_use]
     pub fn new_with_keys(key0: u64, key1: u64) -> SipHasher {
-        SipHasher(SipHasher24 { hasher: Hasher::new_with_keys(key0, key1) })
+        SipHasher(SipHasher24 {
+            hasher: Hasher::new_with_keys(key0, key1),
+        })
     }
 }
 
@@ -177,7 +179,9 @@ impl SipHasher13 {
     #[unstable(feature = "hashmap_internals", issue = "none")]
     #[deprecated(since = "1.13.0", note = "use `std::hash::DefaultHasher` instead")]
     pub fn new_with_keys(key0: u64, key1: u64) -> SipHasher13 {
-        SipHasher13 { hasher: Hasher::new_with_keys(key0, key1) }
+        SipHasher13 {
+            hasher: Hasher::new_with_keys(key0, key1),
+        }
     }
 }
 
@@ -188,7 +192,12 @@ impl<S: Sip> Hasher<S> {
             k0: key0,
             k1: key1,
             length: 0,
-            state: State { v0: 0, v1: 0, v2: 0, v3: 0 },
+            state: State {
+                v0: 0,
+                v1: 0,
+                v2: 0,
+                v3: 0,
+            },
             tail: 0,
             ntail: 0,
             _marker: PhantomData,

From ee7396485f8c9d307bdee78b7beded9e5a4ec86f Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 29 Jul 2025 16:29:59 -0700
Subject: [PATCH 31/42] yay, detached a trait-impl!

---
 library/core/src/flux_info.rs | 4 ++--
 library/core/src/hash/sip.rs  | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 21889d44e4741..ccaf97fb05fc2 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -45,8 +45,8 @@
               _marker: PhantomData<S>,
             }
 
-            impl Hasher for Hasher<S> {
-                fn wrote(self: &mut Self, msg: &[u8]) ensures self: Self; // FLUX:mut-ref-unfolding
+            impl Hasher for hash::sip::Hasher<S> {
+                fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // FLUX:mut-ref-unfolding
             }
         }
     }
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index 76d2b7af4d073..ab7cb73c3d2a7 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -262,7 +262,7 @@ impl<S: Sip> super::Hasher for Hasher<S> {
     // slightly slowing down compile speeds on some benchmarks. See #69152 for
     // details.
     #[inline]
-    #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
+    // #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
     fn write(&mut self, msg: &[u8]) {
         let length = msg.len();
         self.length += length;

From b5b68a69b0a1827c5cd2ed054b4a18767432f680 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 29 Jul 2025 18:55:16 -0700
Subject: [PATCH 32/42] last: pat.rs

---
 library/core/src/flux_info.rs | 23 +++++++++--
 library/core/src/hash/mod.rs  |  7 +++-
 library/core/src/hash/sip.rs  |  2 +-
 library/core/src/time.rs      | 78 +++++++++++++++++++++++++++--------
 4 files changed, 86 insertions(+), 24 deletions(-)

diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index ccaf97fb05fc2..305f179f2c782 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -45,10 +45,27 @@
               _marker: PhantomData<S>,
             }
 
-            impl Hasher for hash::sip::Hasher<S> {
-                fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // FLUX:mut-ref-unfolding
-            }
+
         }
+
+        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; // FLUX: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/hash/mod.rs b/library/core/src/hash/mod.rs
index 6aaa9349a913b..a806b7aa88825 100644
--- a/library/core/src/hash/mod.rs
+++ b/library/core/src/hash/mod.rs
@@ -752,7 +752,7 @@ pub struct BuildHasherDefault<H>(marker::PhantomData<fn() -> H>);
 
 impl<H> BuildHasherDefault<H> {
     /// Creates a new BuildHasherDefault for Hasher `H`.
-    #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
+    // DETACH? #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
     #[stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     #[rustc_const_stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     pub const fn new() -> Self {
@@ -778,7 +778,10 @@ impl<H: Default + Hasher> BuildHasher for BuildHasherDefault<H> {
 
 #[stable(since = "1.7.0", feature = "build_hasher")]
 impl<H> Clone for BuildHasherDefault<H> {
-    #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
+    // DETACH? #[cfg_attr(
+    //     flux,
+    //     flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185")
+    // )]
     fn clone(&self) -> BuildHasherDefault<H> {
         BuildHasherDefault(marker::PhantomData)
     }
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index ab7cb73c3d2a7..12f9c5353cab0 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -262,7 +262,7 @@ impl<S: Sip> super::Hasher for Hasher<S> {
     // slightly slowing down compile speeds on some benchmarks. See #69152 for
     // details.
     #[inline]
-    // #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
+    // DETACH? #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
     fn write(&mut self, msg: &[u8]) {
         let length = msg.len();
         self.length += length;
diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 29e9e8eb19bd4..469e6d82b3e78 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -208,14 +208,20 @@ impl Duration {
     pub const fn new(secs: u64, nanos: u32) -> Duration {
         if nanos < NANOS_PER_SEC {
             // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range
-            Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } }
+            Duration {
+                secs,
+                nanos: unsafe { Nanoseconds::new_unchecked(nanos) },
+            }
         } else {
             let secs = secs
                 .checked_add((nanos / NANOS_PER_SEC) as u64)
                 .expect("overflow in Duration::new");
             let nanos = nanos % NANOS_PER_SEC;
             // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range
-            Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } }
+            Duration {
+                secs,
+                nanos: unsafe { Nanoseconds::new_unchecked(nanos) },
+            }
         }
     }
 
@@ -238,7 +244,10 @@ impl Duration {
     #[ensures(|duration| duration.is_safe())]
     #[ensures(|duration| duration.secs == secs)]
     pub const fn from_secs(secs: u64) -> Duration {
-        Duration { secs, nanos: Nanoseconds::ZERO }
+        Duration {
+            secs,
+            nanos: Nanoseconds::ZERO,
+        }
     }
 
     /// Creates a new `Duration` from the specified number of milliseconds.
@@ -265,7 +274,10 @@ impl Duration {
         //         => x % 1_000 < 1_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_millis * NANOS_PER_MILLI) };
 
-        Duration { secs, nanos: subsec_nanos }
+        Duration {
+            secs,
+            nanos: subsec_nanos,
+        }
     }
 
     /// Creates a new `Duration` from the specified number of microseconds.
@@ -292,7 +304,10 @@ impl Duration {
         //         => x % 1_000_000 < 1_000_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_micros * NANOS_PER_MICRO) };
 
-        Duration { secs, nanos: subsec_nanos }
+        Duration {
+            secs,
+            nanos: subsec_nanos,
+        }
     }
 
     /// Creates a new `Duration` from the specified number of nanoseconds.
@@ -324,7 +339,10 @@ impl Duration {
         // SAFETY: x % 1_000_000_000 < 1_000_000_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_nanos) };
 
-        Duration { secs, nanos: subsec_nanos }
+        Duration {
+            secs,
+            nanos: subsec_nanos,
+        }
     }
 
     /// Creates a new `Duration` from the specified number of weeks.
@@ -638,7 +656,11 @@ impl Duration {
                   without modifying the original"]
     #[inline]
     pub const fn abs_diff(self, other: Duration) -> Duration {
-        if let Some(res) = self.checked_sub(other) { res } else { other.checked_sub(self).unwrap() }
+        if let Some(res) = self.checked_sub(other) {
+            res
+        } else {
+            other.checked_sub(self).unwrap()
+        }
     }
 
     /// Checked `Duration` addition. Computes `self + other`, returning [`None`]
@@ -1135,7 +1157,8 @@ impl Add for Duration {
 
     #[inline]
     fn add(self, rhs: Duration) -> Duration {
-        self.checked_add(rhs).expect("overflow when adding durations")
+        self.checked_add(rhs)
+            .expect("overflow when adding durations")
     }
 }
 
@@ -1153,7 +1176,8 @@ impl Sub for Duration {
 
     #[inline]
     fn sub(self, rhs: Duration) -> Duration {
-        self.checked_sub(rhs).expect("overflow when subtracting durations")
+        self.checked_sub(rhs)
+            .expect("overflow when subtracting durations")
     }
 }
 
@@ -1171,7 +1195,8 @@ impl Mul<u32> for Duration {
 
     #[inline]
     fn mul(self, rhs: u32) -> Duration {
-        self.checked_mul(rhs).expect("overflow when multiplying duration by scalar")
+        self.checked_mul(rhs)
+            .expect("overflow when multiplying duration by scalar")
     }
 }
 
@@ -1200,7 +1225,8 @@ impl Div<u32> for Duration {
     #[inline]
     #[track_caller]
     fn div(self, rhs: u32) -> Duration {
-        self.checked_div(rhs).expect("divide by zero error when dividing duration by scalar")
+        self.checked_div(rhs)
+            .expect("divide by zero error when dividing duration by scalar")
     }
 }
 
@@ -1219,8 +1245,9 @@ macro_rules! sum_durations {
         let mut total_nanos: u64 = 0;
 
         for entry in $iter {
-            total_secs =
-                total_secs.checked_add(entry.secs).expect("overflow in iter::sum over durations");
+            total_secs = total_secs
+                .checked_add(entry.secs)
+                .expect("overflow in iter::sum over durations");
             total_nanos = match total_nanos.checked_add(entry.nanos.as_inner() as u64) {
                 Some(n) => n,
                 None => {
@@ -1255,6 +1282,7 @@ impl<'a> Sum<&'a Duration> for Duration {
 
 #[stable(feature = "duration_debug_impl", since = "1.27.0")]
 impl fmt::Debug for Duration {
+    // DETACH? #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant, nested"))]
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         /// Formats a floating point number in decimal notation.
         ///
@@ -1269,7 +1297,6 @@ impl fmt::Debug for Duration {
         ///
         /// A prefix and postfix may be added. The whole thing is padded
         /// to the formatter's `width`, if specified.
-        #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant"))]
         fn fmt_decimal(
             f: &mut fmt::Formatter<'_>,
             integer_part: u64,
@@ -1421,7 +1448,14 @@ impl fmt::Debug for Duration {
         let prefix = if f.sign_plus() { "+" } else { "" };
 
         if self.secs > 0 {
-            fmt_decimal(f, self.secs, self.nanos.as_inner(), NANOS_PER_SEC / 10, prefix, "s")
+            fmt_decimal(
+                f,
+                self.secs,
+                self.nanos.as_inner(),
+                NANOS_PER_SEC / 10,
+                prefix,
+                "s",
+            )
         } else if self.nanos.as_inner() >= NANOS_PER_MILLI {
             fmt_decimal(
                 f,
@@ -1509,7 +1543,9 @@ macro_rules! try_from_secs {
         const EXP_MASK: $bits_ty = (1 << $exp_bits) - 1;
 
         if $secs < 0.0 {
-            return Err(TryFromFloatSecsError { kind: TryFromFloatSecsErrorKind::Negative });
+            return Err(TryFromFloatSecsError {
+                kind: TryFromFloatSecsErrorKind::Negative,
+            });
         }
 
         let bits = $secs.to_bits();
@@ -1537,7 +1573,11 @@ macro_rules! try_from_secs {
             // f32 does not have enough precision to trigger the second branch
             // since it can not represent numbers between 0.999_999_940_395 and 1.0.
             let nanos = nanos + add_ns as u32;
-            if ($mant_bits == 23) || (nanos != NANOS_PER_SEC) { (0, nanos) } else { (1, 0) }
+            if ($mant_bits == 23) || (nanos != NANOS_PER_SEC) {
+                (0, nanos)
+            } else {
+                (1, 0)
+            }
         } else if exp < $mant_bits {
             let secs = u64::from(mant >> ($mant_bits - exp));
             let t = <$double_ty>::from((mant << exp) & MANT_MASK);
@@ -1568,7 +1608,9 @@ macro_rules! try_from_secs {
             let secs = u64::from(mant) << (exp - $mant_bits);
             (secs, 0)
         } else {
-            return Err(TryFromFloatSecsError { kind: TryFromFloatSecsErrorKind::OverflowOrNan });
+            return Err(TryFromFloatSecsError {
+                kind: TryFromFloatSecsErrorKind::OverflowOrNan,
+            });
         };
 
         Ok(Duration::new(secs, nanos))

From f2cd607ef64b7fa9dad9afe4f817bdfb63237b86 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Tue, 29 Jul 2025 19:09:55 -0700
Subject: [PATCH 33/42] done detach2

---
 library/core/src/flux_info.rs | 19 +++++++++++++++++++
 library/core/src/pat.rs       |  8 ++++----
 2 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index 305f179f2c782..a807e80e57231 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -67,5 +67,24 @@
         #[trusted]         // reason = modular arithmetic invariant inside nested fmt_decimal
         fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result;
     }
+
+    mod pat {
+        trait RangePattern {
+            #[reft]
+            fn sub_ok(self: Self) -> bool { true }
+
+            fn sub_one(self: Self{<Self as RangePattern>::sub_ok(self)}) -> Self;
+        }
+    }
+
+    impl RangePattern for char {
+        #[reft]
+        fn sub_ok(self: char) -> bool {
+            0 < char_to_int(self)
+        }
+
+        fn sub_one(self: char{<char as RangePattern>::sub_ok(self)}) -> char;
+
+    }
 }]
 const _: () = {};
diff --git a/library/core/src/pat.rs b/library/core/src/pat.rs
index 1f86d859d1f58..46743b6cdbca4 100644
--- a/library/core/src/pat.rs
+++ b/library/core/src/pat.rs
@@ -16,7 +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 }))]
+// DETACH? #[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]
@@ -34,7 +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))]
+    // DETACH? #[cfg_attr(flux, flux::spec(fn (self: Self{<Self as RangePattern>::sub_ok(self)}) -> Self))]
     #[lang = "RangeSub"]
     #[track_caller]
     fn sub_one(self) -> Self;
@@ -64,13 +64,13 @@ impl_range_pat! {
 }
 
 #[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")]
-#[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self) }))]
+// DETACH? #[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self) }))]
 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))]
+    // DETACH? #[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 52648dd2ef7368ab7dbd8d7410b1e3af5bfc7101 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:08:00 -0700
Subject: [PATCH 34/42] remove detached

---
 library/core/src/ascii/ascii_char.rs | 1 -
 library/core/src/hash/mod.rs         | 5 -----
 library/core/src/hash/sip.rs         | 4 +---
 library/core/src/pat.rs              | 4 ----
 library/core/src/time.rs             | 1 -
 5 files changed, 1 insertion(+), 14 deletions(-)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index 14ba7107e8561..2a1f5337a0664 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -529,7 +529,6 @@ impl AsciiChar {
 
     /// Gets this ASCII character as a byte.
     #[unstable(feature = "ascii_char", issue = "110998")]
-    // DETACH? #[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/hash/mod.rs b/library/core/src/hash/mod.rs
index a806b7aa88825..a10c85640bbb6 100644
--- a/library/core/src/hash/mod.rs
+++ b/library/core/src/hash/mod.rs
@@ -752,7 +752,6 @@ pub struct BuildHasherDefault<H>(marker::PhantomData<fn() -> H>);
 
 impl<H> BuildHasherDefault<H> {
     /// Creates a new BuildHasherDefault for Hasher `H`.
-    // DETACH? #[cfg_attr(flux, flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185"))]
     #[stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     #[rustc_const_stable(feature = "build_hasher_default_const_new", since = "1.85.0")]
     pub const fn new() -> Self {
@@ -778,10 +777,6 @@ impl<H: Default + Hasher> BuildHasher for BuildHasherDefault<H> {
 
 #[stable(since = "1.7.0", feature = "build_hasher")]
 impl<H> Clone for BuildHasherDefault<H> {
-    // DETACH? #[cfg_attr(
-    //     flux,
-    //     flux::trusted(reason = "https://github.com/flux-rs/flux/issues/1185")
-    // )]
     fn clone(&self) -> BuildHasherDefault<H> {
         BuildHasherDefault(marker::PhantomData)
     }
diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index 12f9c5353cab0..e90e19c14cfdb 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -53,8 +53,7 @@ struct Hasher<S: Sip> {
     length: usize, // how many bytes we've processed
     state: State,  // hash State
     tail: u64,     // unprocessed bytes le
-    // DETACH? #[cfg_attr(flux, flux::field(usize{v: v <= 8}))]
-    ntail: usize, // how many bytes in tail are valid
+    ntail: usize,  // how many bytes in tail are valid
     _marker: PhantomData<S>,
 }
 
@@ -262,7 +261,6 @@ impl<S: Sip> super::Hasher for Hasher<S> {
     // slightly slowing down compile speeds on some benchmarks. See #69152 for
     // details.
     #[inline]
-    // DETACH? #[cfg_attr(flux, flux::spec(fn (self: &mut Self, msg: &[u8]) ensures self: Self))] // FLUX:mut-ref-unfolding
     fn write(&mut self, msg: &[u8]) {
         let length = msg.len();
         self.length += length;
diff --git a/library/core/src/pat.rs b/library/core/src/pat.rs
index 46743b6cdbca4..91d015b1bc53f 100644
--- a/library/core/src/pat.rs
+++ b/library/core/src/pat.rs
@@ -16,7 +16,6 @@ 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.
-// DETACH? #[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]
@@ -34,7 +33,6 @@ pub trait RangePattern {
     const MAX: Self;
 
     /// A compile-time helper to subtract 1 for exclusive ranges.
-    // DETACH? #[cfg_attr(flux, flux::spec(fn (self: Self{<Self as RangePattern>::sub_ok(self)}) -> Self))]
     #[lang = "RangeSub"]
     #[track_caller]
     fn sub_one(self) -> Self;
@@ -64,13 +62,11 @@ impl_range_pat! {
 }
 
 #[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")]
-// DETACH? #[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self) }))]
 impl const RangePattern for char {
     const MIN: Self = char::MIN;
 
     const MAX: Self = char::MAX;
 
-    // DETACH? #[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"),
diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 469e6d82b3e78..7acbacb70c83b 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -1282,7 +1282,6 @@ impl<'a> Sum<&'a Duration> for Duration {
 
 #[stable(feature = "duration_debug_impl", since = "1.27.0")]
 impl fmt::Debug for Duration {
-    // DETACH? #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant, nested"))]
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         /// Formats a floating point number in decimal notation.
         ///

From fb2ae3faaba351bcab953947d29be242dc472369 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:13:21 -0700
Subject: [PATCH 35/42] format

---
 library/core/src/ascii/ascii_char.rs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index 2a1f5337a0664..2c9b55723bdcf 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -615,10 +615,7 @@ impl fmt::Debug for AsciiChar {
                 let byte = self.to_u8();
                 let hi = HEX_DIGITS[usize::from(byte >> 4)];
                 let lo = HEX_DIGITS[usize::from(byte & 0xf)];
-                (
-                    [Apostrophe, Backslash, AsciiChar::SmallX, hi, lo, Apostrophe],
-                    6,
-                )
+                ([Apostrophe, Backslash, AsciiChar::SmallX, hi, lo, Apostrophe], 6)
             }
             _ => ([Apostrophe, *self, Apostrophe, Null, Null, Null], 3),
         };

From 546269ed03c8e3d959b40c93e142d582345250ca Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:15:53 -0700
Subject: [PATCH 36/42] format

---
 library/core/src/hash/sip.rs | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index e90e19c14cfdb..55725f4730dfd 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -158,9 +158,7 @@ impl SipHasher {
     #[deprecated(since = "1.13.0", note = "use `std::hash::DefaultHasher` instead")]
     #[must_use]
     pub fn new_with_keys(key0: u64, key1: u64) -> SipHasher {
-        SipHasher(SipHasher24 {
-            hasher: Hasher::new_with_keys(key0, key1),
-        })
+        SipHasher(SipHasher24 { hasher: Hasher::new_with_keys(key0, key1) })
     }
 }
 
@@ -191,12 +189,7 @@ impl<S: Sip> Hasher<S> {
             k0: key0,
             k1: key1,
             length: 0,
-            state: State {
-                v0: 0,
-                v1: 0,
-                v2: 0,
-                v3: 0,
-            },
+            state: State { v0: 0, v1: 0, v2: 0, v3: 0 },
             tail: 0,
             ntail: 0,
             _marker: PhantomData,

From e3f54084cd2ae8912357468fda5e3aa35ee74292 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:16:25 -0700
Subject: [PATCH 37/42] format

---
 library/core/src/hash/sip.rs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/library/core/src/hash/sip.rs b/library/core/src/hash/sip.rs
index 55725f4730dfd..780e522c48ebf 100644
--- a/library/core/src/hash/sip.rs
+++ b/library/core/src/hash/sip.rs
@@ -176,9 +176,7 @@ impl SipHasher13 {
     #[unstable(feature = "hashmap_internals", issue = "none")]
     #[deprecated(since = "1.13.0", note = "use `std::hash::DefaultHasher` instead")]
     pub fn new_with_keys(key0: u64, key1: u64) -> SipHasher13 {
-        SipHasher13 {
-            hasher: Hasher::new_with_keys(key0, key1),
-        }
+        SipHasher13 { hasher: Hasher::new_with_keys(key0, key1) }
     }
 }
 

From 6a42b173e6427c5d79e5a544f0b90d05259a7db0 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:19:31 -0700
Subject: [PATCH 38/42] restore time

---
 library/core/src/time.rs | 77 ++++++++++------------------------------
 1 file changed, 18 insertions(+), 59 deletions(-)

diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 7acbacb70c83b..29e9e8eb19bd4 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -208,20 +208,14 @@ impl Duration {
     pub const fn new(secs: u64, nanos: u32) -> Duration {
         if nanos < NANOS_PER_SEC {
             // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range
-            Duration {
-                secs,
-                nanos: unsafe { Nanoseconds::new_unchecked(nanos) },
-            }
+            Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } }
         } else {
             let secs = secs
                 .checked_add((nanos / NANOS_PER_SEC) as u64)
                 .expect("overflow in Duration::new");
             let nanos = nanos % NANOS_PER_SEC;
             // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range
-            Duration {
-                secs,
-                nanos: unsafe { Nanoseconds::new_unchecked(nanos) },
-            }
+            Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } }
         }
     }
 
@@ -244,10 +238,7 @@ impl Duration {
     #[ensures(|duration| duration.is_safe())]
     #[ensures(|duration| duration.secs == secs)]
     pub const fn from_secs(secs: u64) -> Duration {
-        Duration {
-            secs,
-            nanos: Nanoseconds::ZERO,
-        }
+        Duration { secs, nanos: Nanoseconds::ZERO }
     }
 
     /// Creates a new `Duration` from the specified number of milliseconds.
@@ -274,10 +265,7 @@ impl Duration {
         //         => x % 1_000 < 1_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_millis * NANOS_PER_MILLI) };
 
-        Duration {
-            secs,
-            nanos: subsec_nanos,
-        }
+        Duration { secs, nanos: subsec_nanos }
     }
 
     /// Creates a new `Duration` from the specified number of microseconds.
@@ -304,10 +292,7 @@ impl Duration {
         //         => x % 1_000_000 < 1_000_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_micros * NANOS_PER_MICRO) };
 
-        Duration {
-            secs,
-            nanos: subsec_nanos,
-        }
+        Duration { secs, nanos: subsec_nanos }
     }
 
     /// Creates a new `Duration` from the specified number of nanoseconds.
@@ -339,10 +324,7 @@ impl Duration {
         // SAFETY: x % 1_000_000_000 < 1_000_000_000
         let subsec_nanos = unsafe { Nanoseconds::new_unchecked(subsec_nanos) };
 
-        Duration {
-            secs,
-            nanos: subsec_nanos,
-        }
+        Duration { secs, nanos: subsec_nanos }
     }
 
     /// Creates a new `Duration` from the specified number of weeks.
@@ -656,11 +638,7 @@ impl Duration {
                   without modifying the original"]
     #[inline]
     pub const fn abs_diff(self, other: Duration) -> Duration {
-        if let Some(res) = self.checked_sub(other) {
-            res
-        } else {
-            other.checked_sub(self).unwrap()
-        }
+        if let Some(res) = self.checked_sub(other) { res } else { other.checked_sub(self).unwrap() }
     }
 
     /// Checked `Duration` addition. Computes `self + other`, returning [`None`]
@@ -1157,8 +1135,7 @@ impl Add for Duration {
 
     #[inline]
     fn add(self, rhs: Duration) -> Duration {
-        self.checked_add(rhs)
-            .expect("overflow when adding durations")
+        self.checked_add(rhs).expect("overflow when adding durations")
     }
 }
 
@@ -1176,8 +1153,7 @@ impl Sub for Duration {
 
     #[inline]
     fn sub(self, rhs: Duration) -> Duration {
-        self.checked_sub(rhs)
-            .expect("overflow when subtracting durations")
+        self.checked_sub(rhs).expect("overflow when subtracting durations")
     }
 }
 
@@ -1195,8 +1171,7 @@ impl Mul<u32> for Duration {
 
     #[inline]
     fn mul(self, rhs: u32) -> Duration {
-        self.checked_mul(rhs)
-            .expect("overflow when multiplying duration by scalar")
+        self.checked_mul(rhs).expect("overflow when multiplying duration by scalar")
     }
 }
 
@@ -1225,8 +1200,7 @@ impl Div<u32> for Duration {
     #[inline]
     #[track_caller]
     fn div(self, rhs: u32) -> Duration {
-        self.checked_div(rhs)
-            .expect("divide by zero error when dividing duration by scalar")
+        self.checked_div(rhs).expect("divide by zero error when dividing duration by scalar")
     }
 }
 
@@ -1245,9 +1219,8 @@ macro_rules! sum_durations {
         let mut total_nanos: u64 = 0;
 
         for entry in $iter {
-            total_secs = total_secs
-                .checked_add(entry.secs)
-                .expect("overflow in iter::sum over durations");
+            total_secs =
+                total_secs.checked_add(entry.secs).expect("overflow in iter::sum over durations");
             total_nanos = match total_nanos.checked_add(entry.nanos.as_inner() as u64) {
                 Some(n) => n,
                 None => {
@@ -1296,6 +1269,7 @@ impl fmt::Debug for Duration {
         ///
         /// A prefix and postfix may be added. The whole thing is padded
         /// to the formatter's `width`, if specified.
+        #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant"))]
         fn fmt_decimal(
             f: &mut fmt::Formatter<'_>,
             integer_part: u64,
@@ -1447,14 +1421,7 @@ impl fmt::Debug for Duration {
         let prefix = if f.sign_plus() { "+" } else { "" };
 
         if self.secs > 0 {
-            fmt_decimal(
-                f,
-                self.secs,
-                self.nanos.as_inner(),
-                NANOS_PER_SEC / 10,
-                prefix,
-                "s",
-            )
+            fmt_decimal(f, self.secs, self.nanos.as_inner(), NANOS_PER_SEC / 10, prefix, "s")
         } else if self.nanos.as_inner() >= NANOS_PER_MILLI {
             fmt_decimal(
                 f,
@@ -1542,9 +1509,7 @@ macro_rules! try_from_secs {
         const EXP_MASK: $bits_ty = (1 << $exp_bits) - 1;
 
         if $secs < 0.0 {
-            return Err(TryFromFloatSecsError {
-                kind: TryFromFloatSecsErrorKind::Negative,
-            });
+            return Err(TryFromFloatSecsError { kind: TryFromFloatSecsErrorKind::Negative });
         }
 
         let bits = $secs.to_bits();
@@ -1572,11 +1537,7 @@ macro_rules! try_from_secs {
             // f32 does not have enough precision to trigger the second branch
             // since it can not represent numbers between 0.999_999_940_395 and 1.0.
             let nanos = nanos + add_ns as u32;
-            if ($mant_bits == 23) || (nanos != NANOS_PER_SEC) {
-                (0, nanos)
-            } else {
-                (1, 0)
-            }
+            if ($mant_bits == 23) || (nanos != NANOS_PER_SEC) { (0, nanos) } else { (1, 0) }
         } else if exp < $mant_bits {
             let secs = u64::from(mant >> ($mant_bits - exp));
             let t = <$double_ty>::from((mant << exp) & MANT_MASK);
@@ -1607,9 +1568,7 @@ macro_rules! try_from_secs {
             let secs = u64::from(mant) << (exp - $mant_bits);
             (secs, 0)
         } else {
-            return Err(TryFromFloatSecsError {
-                kind: TryFromFloatSecsErrorKind::OverflowOrNan,
-            });
+            return Err(TryFromFloatSecsError { kind: TryFromFloatSecsErrorKind::OverflowOrNan });
         };
 
         Ok(Duration::new(secs, nanos))

From 265fc8c224b187e458f27b29d7d539796836b414 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 08:19:41 -0700
Subject: [PATCH 39/42] restore time remove flux

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

diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index 29e9e8eb19bd4..059ab5506ece3 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -1269,7 +1269,6 @@ impl fmt::Debug for Duration {
         ///
         /// A prefix and postfix may be added. The whole thing is padded
         /// to the formatter's `width`, if specified.
-        #[cfg_attr(flux, flux::trusted(reason = "modular arithmetic invariant"))]
         fn fmt_decimal(
             f: &mut fmt::Formatter<'_>,
             integer_part: u64,

From 426b5ae9de8ce1647cb72215c8783aa2a55c0fa0 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 10:40:32 -0700
Subject: [PATCH 40/42] use main Cargo.lock

---
 library/Cargo.lock | 42 ------------------------------------------
 1 file changed, 42 deletions(-)

diff --git a/library/Cargo.lock b/library/Cargo.lock
index 758a9ce5d3858..3e34ee6173741 100644
--- a/library/Cargo.lock
+++ b/library/Cargo.lock
@@ -423,48 +423,6 @@ dependencies = [
  "unicode-ident",
 ]
 
-[[package]]
-name = "syn"
-version = "1.0.109"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
-dependencies = [
- "proc-macro2",
- "unicode-ident",
-]
-
-[[package]]
-name = "syn"
-version = "2.0.104"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "17b6f705963418cdb9927482fa304bc562ece2fdd4f616084c50b7023b435a40"
-dependencies = [
- "proc-macro2",
- "quote",
- "unicode-ident",
-]
-
-[[package]]
-name = "syn"
-version = "1.0.109"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
-dependencies = [
- "proc-macro2",
- "unicode-ident",
-]
-
-[[package]]
-name = "syn"
-version = "2.0.104"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "17b6f705963418cdb9927482fa304bc562ece2fdd4f616084c50b7023b435a40"
-dependencies = [
- "proc-macro2",
- "quote",
- "unicode-ident",
-]
-
 [[package]]
 name = "sysroot"
 version = "0.0.0"

From f5168e93ed3b571e9c253608bd52fde29f4ffb94 Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 10:53:40 -0700
Subject: [PATCH 41/42] bump flux version in yml

---
 .github/workflows/flux.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/flux.yml b/.github/workflows/flux.yml
index c1bbd32844fb9..5c803ff135d6d 100644
--- a/.github/workflows/flux.yml
+++ b/.github/workflows/flux.yml
@@ -9,7 +9,7 @@ on:
 
 env:
   FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "ebafb8d0ca32d8c0fcd2a0cfef6b1b4bd4dc4a6f"
+  FLUX_VERSION: "eb448b89b2caf3bb9d3e1ee41d1087d4651934c6"
 
 jobs:
   check-flux-on-core:

From d70c5dea3ec90a28ee3042a08d1d1b3cd206902e Mon Sep 17 00:00:00 2001
From: Ranjit Jhala <rjhala@ucsd.edu>
Date: Wed, 30 Jul 2025 15:49:17 -0700
Subject: [PATCH 42/42] re-attach flux::spec

---
 library/core/src/ascii/ascii_char.rs |  1 +
 library/core/src/flux_info.rs        | 36 ++++------------------------
 library/core/src/pat.rs              |  4 ++++
 3 files changed, 9 insertions(+), 32 deletions(-)

diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index 2c9b55723bdcf..5b8220833481a 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -528,6 +528,7 @@ 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")]
     #[inline]
     pub const fn to_u8(self) -> u8 {
diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs
index a807e80e57231..f5f30a83230e0 100644
--- a/library/core/src/flux_info.rs
+++ b/library/core/src/flux_info.rs
@@ -26,13 +26,6 @@
     }
 }]
 #[flux::specs {
-    mod ascii {
-        // AsciiChar is `crate::ascii::Char`
-        impl Char {
-            fn to_u8(Self) -> u8{v: v <= 127};
-        }
-    }
-
     mod hash {
         mod sip {
             struct Hasher {
@@ -44,47 +37,26 @@
               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
+            #[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; // FLUX:mut-ref-unfolding
+        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
+        #[trusted]         // 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
+        #[trusted]         // modular arithmetic invariant inside nested fmt_decimal
         fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result;
     }
-
-    mod pat {
-        trait RangePattern {
-            #[reft]
-            fn sub_ok(self: Self) -> bool { true }
-
-            fn sub_one(self: Self{<Self as RangePattern>::sub_ok(self)}) -> Self;
-        }
-    }
-
-    impl RangePattern for char {
-        #[reft]
-        fn sub_ok(self: char) -> bool {
-            0 < char_to_int(self)
-        }
-
-        fn sub_one(self: char{<char as RangePattern>::sub_ok(self)}) -> char;
-
-    }
 }]
 const _: () = {};
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"),