Verify time.rs

.github/workflows/flux.yml

@@ -9,7 +9,7 @@ on:
 
 env:
   FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "ebafb8d0ca32d8c0fcd2a0cfef6b1b4bd4dc4a6f"
+  FLUX_VERSION: "347252ab34de1594a7531d9bdc4477369623ead3"
 
 jobs:
   check-flux-on-core:

library/core/Cargo.toml

@@ -47,4 +47,10 @@ check-cfg = [
 
 [package.metadata.flux]
 enabled = true
-include = [ "src/ascii{*.rs,/**/*.rs}" ]
+check_overflow = "lazy"
+include = [ "src/ascii*.rs",
+            "src/pat.rs",
+            "src/bstr/*.rs",
+            "src/hash/*.rs",
+            "src/time.rs",
+          ]

library/core/src/ascii/ascii_char.rs

@@ -528,8 +528,8 @@ impl AsciiChar {
     }
 
     /// Gets this ASCII character as a byte.
+    #[cfg_attr(flux, flux::spec(fn (Self) -> u8{v: v <= 127}))]
     #[unstable(feature = "ascii_char", issue = "110998")]
-    #[cfg_attr(flux, flux::spec(fn(Self) -> u8{v: v <= 127}))]
     #[inline]
     pub const fn to_u8(self) -> u8 {
         self as u8

library/core/src/flux_info.rs

@@ -4,12 +4,54 @@
 /// See the following link for more information on how extensible properties for primitive operations work:
 /// <https://flux-rs.github.io/flux/guide/specifications.html#extensible-properties-for-primitive-ops>
 #[flux::defs {
+    fn char_to_int(x:char) -> int {
+        cast(x)
+    }
+
     property ShiftRightByFour[>>](x, y) {
         16 * [>>](x, 4) == x
     }
 
-    property MaskBy15[&](x, y) {
-        [&](x, y) <= y
+    property MaskLess[&](x, y) {
+        [&](x, y) <= x && [&](x, y) <= y
+    }
+
+    property ShiftLeft[<<](n, k) {
+        0 < k => n <= [<<](n, k)
+    }
+}]
+#[flux::specs {
+    mod hash {
+        mod sip {
+            struct Hasher {
+              k0: u64,
+              k1: u64,
+              length: usize, // how many bytes we've processed
+              state: State,  // hash State
+              tail: u64,     // unprocessed bytes le
+              ntail: usize{v: v <= 8}, // how many bytes in tail are valid
+              _marker: PhantomData<S>,
+            }
+        }
+
+        impl BuildHasherDefault {
+            #[trusted(reason="https://github.com/flux-rs/flux/issues/1185")]
+            fn new() -> Self;
+        }
+    }
+
+    impl Hasher for hash::sip::Hasher {
+        fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // mut-ref-unfolding
+    }
+
+    impl Clone for hash::BuildHasherDefault {
+        #[trusted(reason="https://github.com/flux-rs/flux/issues/1185")]
+        fn clone(self: &Self) -> Self;
+    }
+
+    impl Debug for time::Duration {
+        #[trusted(reason="modular arithmetic invariant inside nested fmt_decimal")]         
+        fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result;
     }
 }]
 const _: () = {};

library/core/src/num/niche_types.rs

@@ -14,6 +14,9 @@ macro_rules! define_valid_range_type {
         $(#[$m:meta])*
         $vis:vis struct $name:ident($int:ident as $uint:ident in $low:literal..=$high:literal);
     )+) => {$(
+        #[cfg_attr(flux, flux::opaque)]
+        #[cfg_attr(flux, flux::refined_by(val: int))]
+        #[cfg_attr(flux, flux::invariant($low <= cast(val) && cast(val) <= $high))]
         #[derive(Clone, Copy, Eq)]
         #[repr(transparent)]
         #[rustc_layout_scalar_valid_range_start($low)]
@@ -33,6 +36,7 @@ macro_rules! define_valid_range_type {
 
         impl $name {
             #[inline]
+            #[cfg_attr(flux, flux::spec(fn (val: $int) -> Option<Self[{val: cast(val)}]>))]
             pub const fn new(val: $int) -> Option<Self> {
                 if (val as $uint) >= ($low as $uint) && (val as $uint) <= ($high as $uint) {
                     // SAFETY: just checked the inclusive range
@@ -49,12 +53,14 @@ macro_rules! define_valid_range_type {
             /// Immediate language UB if `val == 0`, as it violates the validity
             /// invariant of this type.
             #[inline]
+            #[cfg_attr(flux, flux::spec(fn (val: $int{ $low <= cast(val) && cast(val) <= $high }) -> Self[{val:cast(val)}]))] // NOTE: `val == 0` comments are stale(?)
             pub const unsafe fn new_unchecked(val: $int) -> Self {
                 // SAFETY: Caller promised that `val` is non-zero.
                 unsafe { $name(val) }
             }
 
             #[inline]
+            #[cfg_attr(flux, flux::spec(fn (self: Self) -> $int[cast(self.val)] ensures $low <= cast(self.val) && cast(self.val) <= $high))]
             pub const fn as_inner(self) -> $int {
                 // SAFETY: This is a transparent wrapper, so unwrapping it is sound
                 // (Not using `.0` due to MCP#807.)

library/core/src/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"),