Merge branch 'main' into flt2dec-chal

Author: feliperodri

.github/workflows/flux.yml

@@ -8,8 +8,8 @@ on:
     branches: [main]
 
 env:
-  FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "f5e57bec353e2eb3550d2b7ba086462264dfa290"
+  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/setup@v2.7.0
-        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/setup-z3@v1.6.1

.github/workflows/update-subtree.yml

@@ -214,16 +214,12 @@ jobs:
 
         # Try to automatically patch the VeriFast proofs
         pushd verifast-proofs
-        if bash ./patch-verifast-proofs.sh; then
-          if ! git diff --quiet; then
-            git -c user.name=gitbot -c user.email=git@bot \
-              commit . -m "Update VeriFast proofs"
-          else
-            # The original files have not changed; no updates to the VeriFast proofs are necessary.
-            true
-          fi
+        ./patch-verifast-proofs.sh
+        if ! git diff --quiet; then
+          git -c user.name=gitbot -c user.email=git@bot \
+            commit . -m "Update VeriFast proofs"
         else
-          # Patching the VeriFast proofs failed; requires manual intervention.
+          # The original files have not changed; no updates to the VeriFast proofs are necessary.
           true
         fi
         popd

.github/workflows/verifast-negative.yml

@@ -27,19 +27,5 @@ jobs:
       - name: Checkout Repository
         uses: actions/checkout@v4
 
-      - name: Install VeriFast
-        run: |
-          cd ~
-          curl -OL https://github.com/verifast/verifast/releases/download/25.08/verifast-25.08-linux.tar.gz
-          # https://github.com/verifast/verifast/attestations/10123891
-          echo '1e40019d6add91bf72141c86f4007f2fe1eef67f453cb7fb8f1f5ab7d31d509f  verifast-25.08-linux.tar.gz' | shasum -a 256 -c
-          tar xf verifast-25.08-linux.tar.gz
-
-      - name: Install the Rust toolchain used by VeriFast
-        run: rustup toolchain install nightly-2025-04-09
-
       - name: Run VeriFast Verification
-        run: |
-          export PATH=~/verifast-25.08/bin:$PATH
-          cd verifast-proofs
-          bash check-verifast-proofs-negative.sh
+        run: verifast-proofs/check-verifast-proofs-negative.sh

.github/workflows/verifast.yml

@@ -24,22 +24,8 @@ jobs:
       - name: Checkout Repository
         uses: actions/checkout@v4
 
-      - name: Install VeriFast
-        run: |
-          cd ~
-          curl -OL https://github.com/verifast/verifast/releases/download/25.08/verifast-25.08-linux.tar.gz
-          # https://github.com/verifast/verifast/attestations/10123891
-          echo '1e40019d6add91bf72141c86f4007f2fe1eef67f453cb7fb8f1f5ab7d31d509f  verifast-25.08-linux.tar.gz' | shasum -a 256 -c
-          tar xf verifast-25.08-linux.tar.gz
-
-      - name: Install the Rust toolchain used by VeriFast
-        run: rustup toolchain install nightly-2025-04-09
-
       - name: Run VeriFast Verification
-        run: |
-          export PATH=~/verifast-25.08/bin:$PATH
-          cd verifast-proofs
-          bash check-verifast-proofs.sh
+        run: verifast-proofs/check-verifast-proofs.sh
 
   notify-btj:
     name: Notify @btj

library/Cargo.lock

@@ -23,8 +23,6 @@ safety = { path = "../contracts/safety" }
 compiler-builtins-mem = ['compiler_builtins/mem']
 compiler-builtins-c = ["compiler_builtins/c"]
 compiler-builtins-no-f16-f128 = ["compiler_builtins/no-f16-f128"]
-# Make panics and failed asserts immediately abort without formatting any message
-panic_immediate_abort = ["core/panic_immediate_abort"]
 # Choose algorithms that are optimized for binary size instead of runtime performance
 optimize_for_size = ["core/optimize_for_size"]
 

library/alloc/Cargo.toml

@@ -408,12 +408,12 @@ pub const fn handle_alloc_error(layout: Layout) -> ! {
         }
     }
 
-    #[cfg(not(feature = "panic_immediate_abort"))]
+    #[cfg(not(panic = "immediate-abort"))]
     {
         core::intrinsics::const_eval_select((layout,), ct_error, rt_error)
     }
 
-    #[cfg(feature = "panic_immediate_abort")]
+    #[cfg(panic = "immediate-abort")]
     ct_error(layout)
 }
 

library/alloc/src/alloc.rs

@@ -290,8 +290,6 @@ impl<T> Box<T> {
     /// # Examples
     ///
     /// ```
-    /// #![feature(new_zeroed_alloc)]
-    ///
     /// let zero = Box::<u32>::new_zeroed();
     /// let zero = unsafe { zero.assume_init() };
     ///
@@ -301,7 +299,7 @@ impl<T> Box<T> {
     /// [zeroed]: mem::MaybeUninit::zeroed
     #[cfg(not(no_global_oom_handling))]
     #[inline]
-    #[unstable(feature = "new_zeroed_alloc", issue = "129396")]
+    #[stable(feature = "new_zeroed_alloc", since = "CURRENT_RUSTC_VERSION")]
     #[must_use]
     pub fn new_zeroed() -> Box<mem::MaybeUninit<T>> {
         Self::new_zeroed_in(Global)
@@ -358,7 +356,6 @@ impl<T> Box<T> {
     /// # Ok::<(), std::alloc::AllocError>(())
     /// ```
     #[unstable(feature = "allocator_api", issue = "32838")]
-    // #[unstable(feature = "new_uninit", issue = "63291")]
     #[inline]
     pub fn try_new_uninit() -> Result<Box<mem::MaybeUninit<T>>, AllocError> {
         Box::try_new_uninit_in(Global)
@@ -384,7 +381,6 @@ impl<T> Box<T> {
     ///
     /// [zeroed]: mem::MaybeUninit::zeroed
     #[unstable(feature = "allocator_api", issue = "32838")]
-    // #[unstable(feature = "new_uninit", issue = "63291")]
     #[inline]
     pub fn try_new_zeroed() -> Result<Box<mem::MaybeUninit<T>>, AllocError> {
         Box::try_new_zeroed_in(Global)
@@ -463,7 +459,6 @@ impl<T, A: Allocator> Box<T, A> {
     #[unstable(feature = "allocator_api", issue = "32838")]
     #[cfg(not(no_global_oom_handling))]
     #[must_use]
-    // #[unstable(feature = "new_uninit", issue = "63291")]
     pub fn new_uninit_in(alloc: A) -> Box<mem::MaybeUninit<T>, A>
     where
         A: Allocator,
@@ -496,7 +491,6 @@ impl<T, A: Allocator> Box<T, A> {
     /// # Ok::<(), std::alloc::AllocError>(())
     /// ```
     #[unstable(feature = "allocator_api", issue = "32838")]
-    // #[unstable(feature = "new_uninit", issue = "63291")]
     pub fn try_new_uninit_in(alloc: A) -> Result<Box<mem::MaybeUninit<T>, A>, AllocError>
     where
         A: Allocator,
@@ -532,7 +526,6 @@ impl<T, A: Allocator> Box<T, A> {
     /// [zeroed]: mem::MaybeUninit::zeroed
     #[unstable(feature = "allocator_api", issue = "32838")]
     #[cfg(not(no_global_oom_handling))]
-    // #[unstable(feature = "new_uninit", issue = "63291")]
     #[must_use]
     pub fn new_zeroed_in(alloc: A) -> Box<mem::MaybeUninit<T>, A>
     where
@@ -570,7 +563,6 @@ impl<T, A: Allocator> Box<T, A> {
     ///
     /// [zeroed]: mem::MaybeUninit::zeroed
     #[unstable(feature = "allocator_api", issue = "32838")]
-    // #[unstable(feature = "new_uninit", issue = "63291")]
     pub fn try_new_zeroed_in(alloc: A) -> Result<Box<mem::MaybeUninit<T>, A>, AllocError>
     where
         A: Allocator,
@@ -627,6 +619,37 @@ impl<T, A: Allocator> Box<T, A> {
     pub fn into_inner(boxed: Self) -> T {
         *boxed
     }
+
+    /// Consumes the `Box` without consuming its allocation, returning the wrapped value and a `Box`
+    /// to the uninitialized memory where the wrapped value used to live.
+    ///
+    /// This can be used together with [`write`](Box::write) to reuse the allocation for multiple
+    /// boxed values.
+    ///
+    /// # Examples
+    ///
+    /// ```
+    /// #![feature(box_take)]
+    ///
+    /// let c = Box::new(5);
+    ///
+    /// // take the value out of the box
+    /// let (value, uninit) = Box::take(c);
+    /// assert_eq!(value, 5);
+    ///
+    /// // reuse the box for a second value
+    /// let c = Box::write(uninit, 6);
+    /// assert_eq!(*c, 6);
+    /// ```
+    #[unstable(feature = "box_take", issue = "147212")]
+    pub fn take(boxed: Self) -> (T, Box<mem::MaybeUninit<T>, A>) {
+        unsafe {
+            let (raw, alloc) = Box::into_raw_with_allocator(boxed);
+            let value = raw.read();
+            let uninit = Box::from_raw_in(raw.cast::<mem::MaybeUninit<T>>(), alloc);
+            (value, uninit)
+        }
+    }
 }
 
 impl<T> Box<[T]> {
@@ -640,7 +663,7 @@ impl<T> Box<[T]> {
     /// values[0].write(1);
     /// values[1].write(2);
     /// values[2].write(3);
-    /// let values = unsafe {values.assume_init() };
+    /// let values = unsafe { values.assume_init() };
     ///
     /// assert_eq!(*values, [1, 2, 3])
     /// ```
@@ -660,8 +683,6 @@ impl<T> Box<[T]> {
     /// # Examples
     ///
     /// ```
-    /// #![feature(new_zeroed_alloc)]
-    ///
     /// let values = Box::<[u32]>::new_zeroed_slice(3);
     /// let values = unsafe { values.assume_init() };
     ///
@@ -670,7 +691,7 @@ impl<T> Box<[T]> {
     ///
     /// [zeroed]: mem::MaybeUninit::zeroed
     #[cfg(not(no_global_oom_handling))]
-    #[unstable(feature = "new_zeroed_alloc", issue = "129396")]
+    #[stable(feature = "new_zeroed_alloc", since = "CURRENT_RUSTC_VERSION")]
     #[must_use]
     pub fn new_zeroed_slice(len: usize) -> Box<[mem::MaybeUninit<T>]> {
         unsafe { RawVec::with_capacity_zeroed(len).into_box(len) }
@@ -785,7 +806,6 @@ impl<T, A: Allocator> Box<[T], A> {
     /// ```
     #[cfg(not(no_global_oom_handling))]
     #[unstable(feature = "allocator_api", issue = "32838")]
-    // #[unstable(feature = "new_uninit", issue = "63291")]
     #[must_use]
     pub fn new_uninit_slice_in(len: usize, alloc: A) -> Box<[mem::MaybeUninit<T>], A> {
         unsafe { RawVec::with_capacity_in(len, alloc).into_box(len) }
@@ -813,7 +833,6 @@ impl<T, A: Allocator> Box<[T], A> {
     /// [zeroed]: mem::MaybeUninit::zeroed
     #[cfg(not(no_global_oom_handling))]
     #[unstable(feature = "allocator_api", issue = "32838")]
-    // #[unstable(feature = "new_uninit", issue = "63291")]
     #[must_use]
     pub fn new_zeroed_slice_in(len: usize, alloc: A) -> Box<[mem::MaybeUninit<T>], A> {
         unsafe { RawVec::with_capacity_zeroed_in(len, alloc).into_box(len) }
@@ -1718,7 +1737,7 @@ impl Default for Box<str> {
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "pin_default_impls", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "pin_default_impls", since = "1.91.0")]
 impl<T> Default for Pin<Box<T>>
 where
     T: ?Sized,