Simplify Flux contract for int conversion (model-checking#416)

Update the version of Flux and simplify contracts for int conversion as
discussed in
model-checking#403 (comment).

Note that this also includes an update in Flux to the toolchain version
matching the one in verify-rust-std, which should fix [this CI
failure](https://github.com/model-checking/verify-rust-std/actions/runs/16326340547/job/46117341963).
Our PR became out of sync between toolchain updates. We apologize for
that!

---------

Co-authored-by: Ranjit Jhala <[email protected]>

Author: nilehmann

.github/workflows/flux.yml

@@ -9,7 +9,7 @@ on:
 
 env:
   FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "192362760b73ea517d0349f7167661a02175b24f"
+  FLUX_VERSION: "844e2fc0caa6aa96d72f2fcb627a27bf2495d82e"
 
 jobs:
   check-flux-on-core:

library/core/src/convert/num.rs

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