Fix the sync-2025-10-09 PR

.github/workflows/flux.yml

@@ -8,8 +8,8 @@ on:
     branches: [main]
 
 env:
-  FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "e01e0cd595af33b32faf6c96b032574478c29d5c"
+  FLUX_VERSION: "6b080b32801f923bfb590ac48e729de38f829f21"
+  FIXPOINT_VERSION: "nightly-10-15-2025"
 
 jobs:
   check-flux-on-core:
@@ -25,27 +25,22 @@ jobs:
           echo ~/.cargo/bin >> $GITHUB_PATH
           echo ~/.local/bin >> $GITHUB_PATH
 
-      - name: Cache fixpoint
-        uses: actions/cache@v4
-        id: cache-fixpoint
-        with:
-          path: ~/.local/bin/fixpoint
-          key: fixpoint-bin-${{ runner.os }}-${{ env.FIXPOINT_VERSION }}
+      - name: Download and install fixpoint
+        run: |
+          set -e
+          NAME="fixpoint-x86_64-linux-gnu.tar.gz"
+          URL="https://github.com/ucsd-progsys/liquid-fixpoint/releases/download/${FIXPOINT_VERSION}/${NAME}"
 
-      - name: Install Haskell
-        if: steps.cache-fixpoint.outputs.cache-hit != 'true'
-        uses: haskell-actions/[email protected]
-        with:
-          enable-stack: true
-          stack-version: "2.15.7"
+          echo "Downloading from $URL"
+          curl -fsSL --retry 3 -o "$NAME" "$URL"
 
-      - name: Install fixpoint
-        if: steps.cache-fixpoint.outputs.cache-hit != 'true'
-        run: |
-          git clone https://github.com/ucsd-progsys/liquid-fixpoint.git
-          cd liquid-fixpoint
-          git checkout $FIXPOINT_VERSION
-          stack install --fast --flag liquid-fixpoint:-link-z3-as-a-library
+          echo "Extracting archive"
+          tar -xzf "$NAME"
+          mkdir -p ~/.local/bin
+          cp fixpoint ~/.local/bin/fixpoint
+
+          echo "Cleaning up"
+          rm -f "$NAME"
 
       - name: Install Z3
         uses: cda-tum/[email protected]

library/core/src/flux_info.rs

@@ -1,5 +1,10 @@
 //! This file contains auxiliary definitions for Flux
 
+
+use crate::hash;
+use crate::time;
+
+
 /// List of properties tracked for the result of primitive bitwise operations.
 /// 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>
@@ -65,26 +70,28 @@
               ntail: usize{v: v <= 8}, // how many bytes in tail are valid
               _marker: PhantomData<S>,
             }
+
+            impl hash::Hasher for Hasher {
+                fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // mut-ref-unfolding
+            }
         }
 
         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 clone::Clone for 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;
+    mod time {
+        impl fmt::Debug for Duration {
+            #[trusted(reason="modular arithmetic invariant inside nested fmt_decimal")]
+            fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result;
+        }
     }
 }]
 const _: () = {};