Add Flux

Author: ranjitjhala

library/core/Cargo.toml

@@ -45,4 +45,10 @@ check-cfg = [
     'cfg(target_has_reliable_f16_math)',
     'cfg(target_has_reliable_f128)',
     'cfg(target_has_reliable_f128_math)',
+    'cfg(kani)',
+    'cfg(flux)'
 ]
+
+[package.metadata.flux]
+enabled = true
+include = [ "src/ascii/*" ]

library/core/src/ascii/ascii_char.rs

@@ -529,6 +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}))]
     #[inline]
     pub const fn to_u8(self) -> u8 {
         self as u8

library/core/src/convert/num.rs

@@ -69,19 +69,21 @@ 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.
             // Rustdocs on functions do not.
             #[doc = $doc]
+            $(#[$flux_attr])?
             #[inline(always)]
             fn from(small: $Small) -> Self {
                 small as Self
@@ -109,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")]);

library/core/src/flux_info.rs

@@ -0,0 +1,10 @@
+#[flux::defs {
+    property ShiftRightByFour[>>](x, y) {
+        16 * [>>](x, 4) == x
+    }
+
+    property MaskBy15[&](x, y) {
+        [&](x, y) <= y
+    }
+}]
+const _: () = {};

library/core/src/lib.rs

@@ -421,3 +421,6 @@ pub mod simd {
 }
 
 include!("primitive_docs.rs");
+
+#[cfg(flux)]
+mod flux_info;

scripts/run-flux.sh

@@ -0,0 +1,3 @@
+#!/bin/bash
+
+cargo flux -p core