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: diff --git a/library/Cargo.lock b/library/Cargo.lock index a9a611fe1ed56..3e34ee6173741 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" @@ -200,6 +204,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" @@ -216,6 +253,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" @@ -300,6 +346,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" @@ -329,6 +385,7 @@ dependencies = [ "rand", "rand_xorshift", "rustc-demangle", + "safety", "std_detect", "unwind", "wasi", @@ -345,6 +402,27 @@ dependencies = [ "libc", ] +[[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" @@ -365,6 +443,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" @@ -397,6 +481,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..16130fa08f802 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -47,4 +47,9 @@ check-cfg = [ [package.metadata.flux] enabled = true -include = [ "src/ascii{*.rs,/**/*.rs}" ] +include = [ "src/ascii{*.rs,/**/*.rs}", + "src/pat{*.rs,/**/*.rs}", + "src/bstr{*.rs,/**/*.rs}", + "src/hash{*.rs,/**/*.rs}", + "src/time{*.rs,/**/*.rs}", + ] diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs index 63e77df7cf317..5b8220833481a 100644 --- a/library/core/src/ascii/ascii_char.rs +++ b/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 diff --git a/library/core/src/flux_info.rs b/library/core/src/flux_info.rs index c1aa8f1506cff..f5f30a83230e0 100644 --- a/library/core/src/flux_info.rs +++ b/library/core/src/flux_info.rs @@ -4,12 +4,59 @@ /// See the following link for more information on how extensible properties for primitive operations work: /// #[flux::defs { + + fn as_int(x:int) -> int { + x + } + + 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, + } + } + + impl BuildHasherDefault { + #[trusted] // https://github.com/flux-rs/flux/issues/1185 + fn new() -> Self; + } + } + + impl Hasher for hash::sip::Hasher { + fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // mut-ref-unfolding + } + + impl Clone for hash::BuildHasherDefault { + #[trusted] // https://github.com/flux-rs/flux/issues/1185 + fn clone(self: &Self) -> Self; + } + + impl Debug for time::Duration { + #[trusted] // modular arithmetic invariant inside nested fmt_decimal + fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result; } }] const _: () = {}; diff --git a/library/core/src/num/niche_types.rs b/library/core/src/num/niche_types.rs index b92561c9e356d..2f3779253486a 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))] pub const fn new(val: $int) -> Option { 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)}]))] // 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 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.) 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{::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{::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"),