re-attach flux::spec

Author: ranjitjhala

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 {

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 _: () = {};

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