Merge subtree update for toolchain nightly-2026-09-25

.github/workflows/book.yml

@@ -18,14 +18,16 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v4
 
+      # Build the book tools with stable: inside this repo, rust-toolchain.toml would select the
+      # pinned nightly, whose proc_macro no longer has features older dependencies rely on.
       - name: Install mdbook
         run: |
-          cargo install mdbook --version "^0.4" --locked
+          cargo +stable install mdbook --version "^0.4" --locked
           echo "${HOME}/.cargo/bin" >> $GITHUB_PATH
 
       # Removed --locked for now since it is broken due to old proc_macro feature.
       - name: Install linkchecker
-        run: cargo install mdbook-linkcheck --version "^0.7"
+        run: cargo +stable install mdbook-linkcheck --version "^0.7"
 
       - name: Build Documentation
         run: mdbook build doc

.github/workflows/flux.yml

@@ -8,7 +8,7 @@ on:
     branches: [main]
 
 env:
-  FLUX_VERSION: "9c1b5e278791f57eed1fd109816bbe180423fa9d"
+  FLUX_VERSION: "849ef7c31ce06ec92e211050ac2f5bc8c543896d"
   FIXPOINT_VERSION: "nightly-2026-07-20"
 
 jobs:

.github/workflows/kani.yml

@@ -101,6 +101,11 @@ jobs:
       # Notes:
       # - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of
       #   core_arch::x86:: functions that are known to verify successfully.
+      # - __rdl_dealloc/__rdl_realloc are excluded until their contracts require ptr
+      #   to come from the allocator (#712).
+      # - unicode::unicode_data::conversions::to_* are not listed for now: since the
+      #   Unicode tables were regenerated (nightly-2026-09-25) they exceed the 10m
+      #   timeout on macOS and the ubuntu runner died while verifying them.
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
@@ -109,6 +114,7 @@ jobs:
             --include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::backward_unchecked" \
             --include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::forward_unchecked" \
             --include-pattern alloc::__default_lib_allocator:: \
+            --exclude-pattern "alloc::__default_lib_allocator::__rdl_(dealloc|realloc)" \
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern "<char[[:space:]]as[[:space:]]ascii::AsciiExt>::is_ascii" \
@@ -206,7 +212,6 @@ jobs:
             --exclude-pattern time::Duration::from_nanos_u128 \
             --include-pattern time::Duration::from_secs \
             --exclude-pattern time::Duration::from_secs_f \
-            --include-pattern unicode::unicode_data::conversions::to_ \
             --exclude-pattern ::precondition_check \
             --harness-timeout 10m \
             --default-unwind 1000 \
@@ -263,6 +268,11 @@ jobs:
 
       # Step 2: Run list on the std library
       - name: Run Kani Metrics
+        # Under Kani each library crate takes 1-12 GB to compile; compiling them in parallel
+        # exceeds the 16 GB of an ubuntu-latest runner, which then dies with "The runner has
+        # received a shutdown signal". One crate at a time peaks at the largest one (std).
+        env:
+          CARGO_BUILD_JOBS: 1
         run: |
           scripts/run-kani.sh --run metrics --with-autoharness
           pushd /tmp/std_lib_analysis
@@ -359,6 +369,11 @@ jobs:
 
       # Step 2: Run list on the std library
       - name: Run Kani List
+        # Under Kani each library crate takes 1-12 GB to compile; compiling them in parallel
+        # exceeds the 16 GB of an ubuntu-latest runner, which then dies with "The runner has
+        # received a shutdown signal". One crate at a time peaks at the largest one (std).
+        env:
+          CARGO_BUILD_JOBS: 1
         run: |
           head/scripts/run-kani.sh --run list --with-autoharness --path ${{github.workspace}}/head
           # remove duplicate white space to reduce file size (GitHub permits at