From 3c79dfa6489b7d3c0e3aec5736f06e9d351313b8 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 18 Apr 2025 18:38:25 +0000
Subject: [PATCH 01/29] Add autoharness to run-kani script and use in CI

For now, do not run any actual harnesses.
---
 .github/workflows/kani.yml | 32 ++++++++++++++++++++++++++++++++
 scripts/run-kani.sh        | 16 +++++++++++++---
 2 files changed, 45 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 90463ec8574c6..561407c0b9365 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -53,6 +53,38 @@ jobs:
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
    
+  kani-autoharness:
+    name: Verify std library using autoharness
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+      fail-fast: false
+
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Run Kani autoharness on the std library for selected functions.
+      # Uses "--include-pattern no::such::function" to make sure we do not try
+      # to run across all possible functions as that may take a lot longer than
+      # expected
+      - name: Run Kani Verification
+        run: |
+          scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern no:such::function:: \
+            --harness-timeout 5m \
+            --default-unwind 1000 \
+            --jobs=3 --output-format=terse
+
   run-kani-list:
     name: Kani List
     runs-on: ubuntu-latest
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 200bd957180d6..e0537707fd0d3 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -34,7 +34,7 @@ while [[ $# -gt 0 ]]; do
             fi
             ;;
         --run)
-            if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics") ]]; then
+            if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics" || $2 == "autoharness") ]]; then
                 run_command=$2
                 shift 2
             else
@@ -297,13 +297,23 @@ main() {
                 --enable-unstable \
                 --cbmc-args --object-bits 12
         fi
+      elif [[ "$run_command" == "autoharness" ]]; then
+          # Run verification for a subset of automatically generated harnesses
+          # (not in parallel)
+          echo "Running Kani autoharness command..."
+          "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \
+              $unstable_args \
+              --no-assert-contracts \
+              $command_args \
+              --enable-unstable \
+              --cbmc-args --object-bits 12
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
-        "$kani_path" list -Z list $unstable_args ./library --std --format markdown
+        "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format markdown
     elif [[ "$run_command" == "metrics" ]]; then
         local current_dir=$(pwd)
         echo "Running Kani list command..."
-        "$kani_path" list -Z list $unstable_args ./library --std --format json
+        "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format json
         pushd scripts/kani-std-analysis
         echo "Running Kani's std-analysis command..."
         ./std-analysis.sh $build_dir

From 5adba8b0efcf5d5423c0cad866df1c61a7af305d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 Apr 2025 11:30:40 +0000
Subject: [PATCH 02/29] Remove Kani harnesses from time::Duration that
 autoharness takes care of

---
 .github/workflows/kani.yml | 11 +++++++----
 library/core/src/time.rs   | 24 ------------------------
 2 files changed, 7 insertions(+), 28 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 561407c0b9365..0c29abc4e06b5 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -74,13 +74,16 @@ jobs:
           submodules: true
 
       # Step 2: Run Kani autoharness on the std library for selected functions.
-      # Uses "--include-pattern no::such::function" to make sure we do not try
-      # to run across all possible functions as that may take a lot longer than
-      # expected
+      # Uses "--include-pattern" to make sure we do not try to run across all
+      # possible functions as that may take a lot longer than expected
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
-            --include-pattern no:such::function:: \
+            --include-pattern time::Duration::from_micros \
+            --include-pattern time::Duration::from_millis \
+            --include-pattern time::Duration::from_nanos \
+            --include-pattern time::Duration::from_secs \
+            --exclude-pattern time::Duration::from_secs_f \
             --harness-timeout 5m \
             --default-unwind 1000 \
             --jobs=3 --output-format=terse
diff --git a/library/core/src/time.rs b/library/core/src/time.rs
index c0d67cc51edf5..f0a7e36fd4b0f 100644
--- a/library/core/src/time.rs
+++ b/library/core/src/time.rs
@@ -1756,30 +1756,6 @@ pub mod duration_verify {
         let _ = Duration::new(secs, nanos);
     }
 
-    #[kani::proof_for_contract(Duration::from_secs)]
-    fn duration_from_secs() {
-        let secs = kani::any::<u64>();
-        let _ = Duration::from_secs(secs);
-    }
-
-    #[kani::proof_for_contract(Duration::from_millis)]
-    fn duration_from_millis() {
-        let ms = kani::any::<u64>();
-        let _ = Duration::from_millis(ms);
-    }
-
-    #[kani::proof_for_contract(Duration::from_micros)]
-    fn duration_from_micros() {
-        let micros = kani::any::<u64>();
-        let _ = Duration::from_micros(micros);
-    }
-
-    #[kani::proof_for_contract(Duration::from_nanos)]
-    fn duration_from_nanos() {
-        let nanos = kani::any::<u64>();
-        let _ = Duration::from_nanos(nanos);
-    }
-
     #[kani::proof_for_contract(Duration::as_secs)]
     fn duration_as_secs() {
         let dur = safe_duration();

From 60cb5311452386e0f2ebd7ea1670c2bf5fec11f0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 Apr 2025 11:33:16 +0000
Subject: [PATCH 03/29] Use autoharness for ptr::align_offset::mod_inv

This also solves the problem that we cannot write a harness for a nested
function, and hence previously had to copy it.
---
 .github/workflows/kani.yml  |  1 +
 library/core/src/ptr/mod.rs | 71 +++++--------------------------------
 2 files changed, 9 insertions(+), 63 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 0c29abc4e06b5..49a67e2e03a7f 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -79,6 +79,7 @@ jobs:
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern ptr::align_offset::mod_inv \
             --include-pattern time::Duration::from_micros \
             --include-pattern time::Duration::from_millis \
             --include-pattern time::Duration::from_nanos \
diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index 6ea47e6a6f517..e87cbb027cd8c 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -1941,6 +1941,14 @@ pub(crate) unsafe fn align_offset<T: Sized>(p: *const T, a: usize) -> usize {
     /// * `x < m`; (if `x ≥ m`, pass in `x % m` instead)
     ///
     /// Implementation of this function shall not panic. Ever.
+    #[safety::requires(m.is_power_of_two())]
+    #[safety::requires(x < m)]
+    // TODO: add ensures contract to check that the answer is indeed correct
+    // This will require quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html)
+    // so that we can add a precondition that gcd(x, m) = 1 like so:
+    // ∀d, d > 0 ∧ x % d = 0 ∧ m % d = 0 → d = 1
+    // With this precondition, we can then write this postcondition to check the correctness of the answer:
+    // #[safety::ensures(|result| wrapping_mul(*result, x) % m == 1)]
     #[inline]
     const unsafe fn mod_inv(x: usize, m: usize) -> usize {
         /// Multiplicative modular inverse table modulo 2⁴ = 16.
@@ -2549,67 +2557,4 @@ mod verify {
         let p = kani::any::<usize>() as *const [char; 5];
         check_align_offset(p);
     }
-
-    // This function lives inside align_offset, so it is not publicly accessible (hence this copy).
-    #[safety::requires(m.is_power_of_two())]
-    #[safety::requires(x < m)]
-    // TODO: add ensures contract to check that the answer is indeed correct
-    // This will require quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html)
-    // so that we can add a precondition that gcd(x, m) = 1 like so:
-    // ∀d, d > 0 ∧ x % d = 0 ∧ m % d = 0 → d = 1
-    // With this precondition, we can then write this postcondition to check the correctness of the answer:
-    // #[safety::ensures(|result| wrapping_mul(*result, x) % m == 1)]
-    const unsafe fn mod_inv_copy(x: usize, m: usize) -> usize {
-        /// Multiplicative modular inverse table modulo 2⁴ = 16.
-        ///
-        /// Note, that this table does not contain values where inverse does not exist (i.e., for
-        /// `0⁻¹ mod 16`, `2⁻¹ mod 16`, etc.)
-        const INV_TABLE_MOD_16: [u8; 8] = [1, 11, 13, 7, 9, 3, 5, 15];
-        /// Modulo for which the `INV_TABLE_MOD_16` is intended.
-        const INV_TABLE_MOD: usize = 16;
-
-        // SAFETY: `m` is required to be a power-of-two, hence non-zero.
-        let m_minus_one = unsafe { unchecked_sub(m, 1) };
-        let mut inverse = INV_TABLE_MOD_16[(x & (INV_TABLE_MOD - 1)) >> 1] as usize;
-        let mut mod_gate = INV_TABLE_MOD;
-        // We iterate "up" using the following formula:
-        //
-        // $$ xy ≡ 1 (mod 2ⁿ) → xy (2 - xy) ≡ 1 (mod 2²ⁿ) $$
-        //
-        // This application needs to be applied at least until `2²ⁿ ≥ m`, at which point we can
-        // finally reduce the computation to our desired `m` by taking `inverse mod m`.
-        //
-        // This computation is `O(log log m)`, which is to say, that on 64-bit machines this loop
-        // will always finish in at most 4 iterations.
-        loop {
-            // y = y * (2 - xy) mod n
-            //
-            // Note, that we use wrapping operations here intentionally – the original formula
-            // uses e.g., subtraction `mod n`. It is entirely fine to do them `mod
-            // usize::MAX` instead, because we take the result `mod n` at the end
-            // anyway.
-            if mod_gate >= m {
-                break;
-            }
-            inverse = wrapping_mul(inverse, wrapping_sub(2usize, wrapping_mul(x, inverse)));
-            let (new_gate, overflow) = mul_with_overflow(mod_gate, mod_gate);
-            if overflow {
-                break;
-            }
-            mod_gate = new_gate;
-        }
-        inverse & m_minus_one
-    }
-
-    // The specification for mod_inv states that it cannot ever panic.
-    // Verify that is the case, given that the function's safety preconditions are met.
-
-    // TODO: Once https://github.com/model-checking/kani/issues/3467 is fixed,
-    // move this harness inside `align_offset` and delete `mod_inv_copy`
-    #[kani::proof_for_contract(mod_inv_copy)]
-    fn check_mod_inv() {
-        let x = kani::any::<usize>();
-        let m = kani::any::<usize>();
-        unsafe { mod_inv_copy(x, m) };
-    }
 }

From ef9b0fba606ff32fd928ce7e7ebbe3d9d626c1ad Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 Apr 2025 11:38:28 +0000
Subject: [PATCH 04/29] Use autoharness for several Alignment functions

---
 .github/workflows/kani.yml        |  7 +++++
 library/core/src/ptr/alignment.rs | 46 -------------------------------
 2 files changed, 7 insertions(+), 46 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 49a67e2e03a7f..2e5ea5170f380 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -80,11 +80,18 @@ jobs:
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
             --include-pattern ptr::align_offset::mod_inv \
+            --include-pattern ptr::alignment::Alignment::as_nonzero \
+            --include-pattern ptr::alignment::Alignment::as_usize \
+            --include-pattern ptr::alignment::Alignment::log2 \
+            --include-pattern ptr::alignment::Alignment::mask \
+            --include-pattern ptr::alignment::Alignment::new \
+            --include-pattern ptr::alignment::Alignment::new_unchecked \
             --include-pattern time::Duration::from_micros \
             --include-pattern time::Duration::from_millis \
             --include-pattern time::Duration::from_nanos \
             --include-pattern time::Duration::from_secs \
             --exclude-pattern time::Duration::from_secs_f \
+            --exclude-pattern ::precondition_check \
             --harness-timeout 5m \
             --default-unwind 1000 \
             --jobs=3 --output-format=terse
diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs
index c14c2b67c3ddf..c6843a2a05e69 100644
--- a/library/core/src/ptr/alignment.rs
+++ b/library/core/src/ptr/alignment.rs
@@ -410,50 +410,4 @@ mod verify {
     // pub fn check_of_i32() {
     //     let _ = Alignment::of::<i32>();
     // }
-
-    // pub const fn new(align: usize) -> Option<Self>
-    #[kani::proof_for_contract(Alignment::new)]
-    pub fn check_new() {
-        let a = kani::any::<usize>();
-        let _ = Alignment::new(a);
-    }
-
-    // pub const unsafe fn new_unchecked(align: usize) -> Self
-    #[kani::proof_for_contract(Alignment::new_unchecked)]
-    pub fn check_new_unchecked() {
-        let a = kani::any::<usize>();
-        unsafe {
-            let _ = Alignment::new_unchecked(a);
-        }
-    }
-
-    // pub const fn as_usize(self) -> usize
-    #[kani::proof_for_contract(Alignment::as_usize)]
-    pub fn check_as_usize() {
-        let a = kani::any::<usize>();
-        if let Some(alignment) = Alignment::new(a) {
-            assert_eq!(alignment.as_usize(), a);
-        }
-    }
-
-    // pub const fn as_nonzero(self) -> NonZero<usize>
-    #[kani::proof_for_contract(Alignment::as_nonzero)]
-    pub fn check_as_nonzero() {
-        let alignment = kani::any::<Alignment>();
-        let _ = alignment.as_nonzero();
-    }
-
-    // pub const fn log2(self) -> u32
-    #[kani::proof_for_contract(Alignment::log2)]
-    pub fn check_log2() {
-        let alignment = kani::any::<Alignment>();
-        let _ = alignment.log2();
-    }
-
-    // pub const fn mask(self) -> usize
-    #[kani::proof_for_contract(Alignment::mask)]
-    pub fn check_mask() {
-        let alignment = kani::any::<Alignment>();
-        let _ = alignment.mask();
-    }
 }

From 2ce92f2ff183f7540f18349bf5f379fd413bcc53 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 Apr 2025 13:19:55 +0000
Subject: [PATCH 05/29] Don't use doc comment

---
 library/core/src/ptr/alignment.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs
index c6843a2a05e69..08f5e7af4f220 100644
--- a/library/core/src/ptr/alignment.rs
+++ b/library/core/src/ptr/alignment.rs
@@ -404,7 +404,7 @@ mod verify {
         }
     }
 
-    /// FIXME, c.f. https://github.com/model-checking/kani/issues/3905
+    // FIXME, c.f. https://github.com/model-checking/kani/issues/3905
     // // pub const fn of<T>() -> Self
     // #[kani::proof_for_contract(Alignment::of)]
     // pub fn check_of_i32() {

From a1bbbbbd67aabe70a65681783855073cbad460c9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 23 Apr 2025 08:04:27 +0000
Subject: [PATCH 06/29] Squash duplicate space in markdown file

---
 .github/workflows/kani.yml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 2e5ea5170f380..bce3d2f22fdb0 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -109,8 +109,14 @@ jobs:
 
       # Step 2: Run list on the std library
       - name: Run Kani List
-        run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
-      
+        run: |
+          head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
+          # remove duplicate white space to reduce file size (GitHub permits at
+          # most one 1MB)
+          ls -l ${{github.workspace}}/head/kani-list.md
+          perl -p -i -e 's/ +/ /g' ${{github.workspace}}/head/kani-list.md
+          ls -l ${{github.workspace}}/head/kani-list.md
+
       # Step 3: Add output to job summary
       - name: Add Kani List output to job summary
         uses: actions/github-script@v6

From 267fa99fd1aa28b62ff0ad678072160f2527eba1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 24 Apr 2025 08:04:01 +0000
Subject: [PATCH 07/29] Use .0 instead of .as_usize

---
 library/core/src/ptr/alignment.rs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs
index 08f5e7af4f220..6095e408ff71e 100644
--- a/library/core/src/ptr/alignment.rs
+++ b/library/core/src/ptr/alignment.rs
@@ -16,7 +16,9 @@ use crate::{cmp, fmt, hash, mem, num};
 #[unstable(feature = "ptr_alignment_type", issue = "102070")]
 #[derive(Copy, Clone, PartialEq, Eq)]
 #[repr(transparent)]
-#[invariant(self.as_usize().is_power_of_two())]
+// uses .0 instead of .as_usize() to permit proving as_usize so that its proof does not itself use
+// as_usize
+#[invariant((self.0 as usize).is_power_of_two())]
 pub struct Alignment(AlignmentEnum);
 
 // Alignment is `repr(usize)`, but via extra steps.

From d4c6ec5807c83bc64b2d2cb9bd54aed7a5db5a34 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 24 Apr 2025 20:07:44 +0000
Subject: [PATCH 08/29] Make autoharness in run-kani.sh --run list optional

---
 .github/workflows/kani-metrics.yml |  2 +-
 .github/workflows/kani.yml         |  2 +-
 scripts/run-kani.sh                | 17 +++++++++++++++--
 3 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml
index 84945e236a4ed..106ed3e160b4b 100644
--- a/.github/workflows/kani-metrics.yml
+++ b/.github/workflows/kani-metrics.yml
@@ -26,7 +26,7 @@ jobs:
         python-version: '3.x'
 
     - name: Compute Kani Metrics
-      run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
+      run: ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
 
     - name: Create Pull Request
       uses: peter-evans/create-pull-request@v7
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index bce3d2f22fdb0..deecc28346895 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -110,7 +110,7 @@ jobs:
       # Step 2: Run list on the std library
       - name: Run Kani List
         run: |
-          head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
+          head/scripts/run-kani.sh --run list --with-autoharness --path ${{github.workspace}}/head
           # remove duplicate white space to reduce file size (GitHub permits at
           # most one 1MB)
           ls -l ${{github.workspace}}/head/kani-list.md
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index e0537707fd0d3..b14d1b2d3383d 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -16,6 +16,7 @@ usage() {
 command_args=""
 path=""
 run_command="verify-std"
+with_autoharness="false"
 
 # Parse command line arguments
 # TODO: Improve parsing with getopts
@@ -42,6 +43,10 @@ while [[ $# -gt 0 ]]; do
                 usage
             fi
             ;;
+        --with-autoharness)
+            with_autoharness="true"
+            shift
+            ;;
         --kani-args)
             shift
             command_args="$@"
@@ -309,11 +314,19 @@ main() {
               --cbmc-args --object-bits 12
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
-        "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format markdown
+        if [[ "$with_autoharness" == "true" ]]; then
+            "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format markdown
+        else
+            "$kani_path" list -Z list $unstable_args ./library --std --format markdown
+        fi
     elif [[ "$run_command" == "metrics" ]]; then
         local current_dir=$(pwd)
         echo "Running Kani list command..."
-        "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format json
+        if [[ "$with_autoharness" == "true" ]]; then
+            "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format json
+        else
+            "$kani_path" list -Z list $unstable_args ./library --std --format json
+        fi
         pushd scripts/kani-std-analysis
         echo "Running Kani's std-analysis command..."
         ./std-analysis.sh $build_dir

From 8064562ea1bdf7b0a6c36185dc7487ee26af5286 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 24 Apr 2025 20:11:01 +0000
Subject: [PATCH 09/29] Amend help

---
 scripts/run-kani.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index b14d1b2d3383d..9f4c3be3c80fc 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -7,7 +7,8 @@ usage() {
     echo "Options:"
     echo "  -h, --help         Show this help message"
     echo "  -p, --path <path>  Optional: Specify a path to a copy of the std library. For example, if you want to run the script from an outside directory."
-    echo "  --run <verify-std|list|metrics>  Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, or collect Kani-specific metrics. Defaults to 'verify-std' if not specified."
+    echo "  --run <verify-std|list|metrics|autoharness>  Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, collect Kani-specific metrics, or run verification with autoharness support. Defaults to 'verify-std' if not specified."
+    echo "  --with-autoharness Include autoharness information in list or metrics commands.
     echo "  --kani-args  <command arguments to kani>  Optional: Arguments to pass to the command. Simply pass them in the same way you would to the Kani binary. This should be the last argument."
     exit 1
 }

From 96baf9d8f3bcc674a137bdec10885534f28b07be Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 24 Apr 2025 20:19:43 +0000
Subject: [PATCH 10/29] Fix help

---
 scripts/run-kani.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 9f4c3be3c80fc..84c419d745d0c 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -8,7 +8,7 @@ usage() {
     echo "  -h, --help         Show this help message"
     echo "  -p, --path <path>  Optional: Specify a path to a copy of the std library. For example, if you want to run the script from an outside directory."
     echo "  --run <verify-std|list|metrics|autoharness>  Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, collect Kani-specific metrics, or run verification with autoharness support. Defaults to 'verify-std' if not specified."
-    echo "  --with-autoharness Include autoharness information in list or metrics commands.
+    echo "  --with-autoharness Include autoharness information in list or metrics commands."
     echo "  --kani-args  <command arguments to kani>  Optional: Arguments to pass to the command. Simply pass them in the same way you would to the Kani binary. This should be the last argument."
     exit 1
 }

From e7d44282645bca66584ca68a9a2c577f8ec07657 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 20:16:48 +0000
Subject: [PATCH 11/29] Use autoharness for
 unicode::unicode_data::conversions::to_{lower,upper}

---
 .github/workflows/kani.yml      |  1 +
 library/core/src/unicode/mod.rs | 18 ------------------
 2 files changed, 1 insertion(+), 18 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index deecc28346895..7a991a7dd62c4 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -91,6 +91,7 @@ jobs:
             --include-pattern time::Duration::from_nanos \
             --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 5m \
             --default-unwind 1000 \
diff --git a/library/core/src/unicode/mod.rs b/library/core/src/unicode/mod.rs
index 92394340152d0..49dbdeb1a6d1c 100644
--- a/library/core/src/unicode/mod.rs
+++ b/library/core/src/unicode/mod.rs
@@ -33,21 +33,3 @@ mod unicode_data;
 /// [Unicode 11.0 or later, Section 3.1 Versions of the Unicode Standard](https://www.unicode.org/versions/Unicode11.0.0/ch03.pdf#page=4).
 #[stable(feature = "unicode_version", since = "1.45.0")]
 pub const UNICODE_VERSION: (u8, u8, u8) = unicode_data::UNICODE_VERSION;
-
-#[cfg(kani)]
-mod verify {
-    use super::conversions::{to_lower, to_upper};
-    use crate::kani;
-
-    /// Checks that `to_upper` does not trigger UB or panics for all valid characters.
-    #[kani::proof]
-    fn check_to_upper_safety() {
-        let _ = to_upper(kani::any());
-    }
-
-    /// Checks that `to_lower` does not trigger UB or panics for all valid characters.
-    #[kani::proof]
-    fn check_to_lower_safety() {
-        let _ = to_lower(kani::any());
-    }
-}

From 721fb78ce7e3d4384fa5a613c7839dde0ca3d2cc Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 20:22:33 +0000
Subject: [PATCH 12/29] Use autoharness for
 alloc::layout::Layout::from_size_align{,_unchecked}

---
 .github/workflows/kani.yml       |  1 +
 library/core/src/alloc/layout.rs | 18 ------------------
 2 files changed, 1 insertion(+), 18 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 7a991a7dd62c4..7b34c25caf868 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -79,6 +79,7 @@ jobs:
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ptr::align_offset::mod_inv \
             --include-pattern ptr::alignment::Alignment::as_nonzero \
             --include-pattern ptr::alignment::Alignment::as_usize \
diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index f3df9c6916812..17871634b0ad4 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -637,24 +637,6 @@ mod verify {
         }
     }
 
-    // pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError>
-    #[kani::proof_for_contract(Layout::from_size_align)]
-    pub fn check_from_size_align() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        let _ = Layout::from_size_align(s, a);
-    }
-
-    // pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self
-    #[kani::proof_for_contract(Layout::from_size_align_unchecked)]
-    pub fn check_from_size_align_unchecked() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        unsafe {
-            let _ = Layout::from_size_align_unchecked(s, a);
-        }
-    }
-
     // pub const fn size(&self) -> usize
     #[kani::proof]
     pub fn check_size() {

From 2fd26a6741baecc36a89b71aaada9e272cc66e7c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 20:24:41 +0000
Subject: [PATCH 13/29] Use autoharness for
 ascii::ascii_char::AsciiChar::from_u8{,_unchecked}

---
 .github/workflows/kani.yml           |  1 +
 library/core/src/ascii/ascii_char.rs | 20 --------------------
 2 files changed, 1 insertion(+), 20 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 7b34c25caf868..9aac68910913e 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -80,6 +80,7 @@ jobs:
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
             --include-pattern alloc::layout::Layout::from_size_align \
+            --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern ptr::align_offset::mod_inv \
             --include-pattern ptr::alignment::Alignment::as_nonzero \
             --include-pattern ptr::alignment::Alignment::as_usize \
diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index aca4503f5a6c0..6fce682b33dbb 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -621,23 +621,3 @@ impl fmt::Debug for AsciiChar {
         f.write_str(buf[..len].as_str())
     }
 }
-
-#[cfg(kani)]
-#[unstable(feature = "kani", issue = "none")]
-mod verify {
-    use AsciiChar;
-
-    use super::*;
-
-    #[kani::proof_for_contract(AsciiChar::from_u8)]
-    fn check_from_u8() {
-        let b: u8 = kani::any();
-        AsciiChar::from_u8(b);
-    }
-
-    #[kani::proof_for_contract(AsciiChar::from_u8_unchecked)]
-    fn check_from_u8_unchecked() {
-        let b: u8 = kani::any();
-        unsafe { AsciiChar::from_u8_unchecked(b) };
-    }
-}

From 889b8cd5398dfbc2f9d95488b2aab359c652f838 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 20:26:33 +0000
Subject: [PATCH 14/29] Use autoharness for char::convert::from_u32_unchecked

---
 .github/workflows/kani.yml       |  1 +
 library/core/src/char/convert.rs | 12 ------------
 2 files changed, 1 insertion(+), 12 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 9aac68910913e..7e5fd08939119 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -81,6 +81,7 @@ jobs:
           scripts/run-kani.sh --run autoharness --kani-args \
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
+            --include-pattern char::convert::from_u32_unchecked \
             --include-pattern ptr::align_offset::mod_inv \
             --include-pattern ptr::alignment::Alignment::as_nonzero \
             --include-pattern ptr::alignment::Alignment::as_usize \
diff --git a/library/core/src/char/convert.rs b/library/core/src/char/convert.rs
index cc1632182b231..ff4ff38290e63 100644
--- a/library/core/src/char/convert.rs
+++ b/library/core/src/char/convert.rs
@@ -288,15 +288,3 @@ pub(super) const fn from_digit(num: u32, radix: u32) -> Option<char> {
         None
     }
 }
-
-#[cfg(kani)]
-#[unstable(feature = "kani", issue = "none")]
-mod verify {
-    use super::*;
-
-    #[kani::proof_for_contract(from_u32_unchecked)]
-    fn check_from_u32_unchecked() {
-        let i: u32 = kani::any();
-        unsafe { from_u32_unchecked(i) };
-    }
-}

From 0c1b5c3f158f3f614e36818f3a0c123b16361349 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 20:37:24 +0000
Subject: [PATCH 15/29] Use autoharness for num::<impl *>::wrapping_sh{l,r}

---
 .github/workflows/kani.yml  | 12 +++++++
 library/core/src/num/mod.rs | 62 -------------------------------------
 2 files changed, 12 insertions(+), 62 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 7e5fd08939119..8998252fc849d 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,6 +82,18 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern "num::<impl i8>::wrapping_sh" \
+            --include-pattern "num::<impl i16>::wrapping_sh" \
+            --include-pattern "num::<impl i32>::wrapping_sh" \
+            --include-pattern "num::<impl i64>::wrapping_sh" \
+            --include-pattern "num::<impl i128>::wrapping_sh" \
+            --include-pattern "num::<impl isize>::wrapping_sh" \
+            --include-pattern "num::<impl u8>::wrapping_sh" \
+            --include-pattern "num::<impl u16>::wrapping_sh" \
+            --include-pattern "num::<impl u32>::wrapping_sh" \
+            --include-pattern "num::<impl u64>::wrapping_sh" \
+            --include-pattern "num::<impl u128>::wrapping_sh" \
+            --include-pattern "num::<impl usize>::wrapping_sh" \
             --include-pattern ptr::align_offset::mod_inv \
             --include-pattern ptr::alignment::Alignment::as_nonzero \
             --include-pattern ptr::alignment::Alignment::as_usize \
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 0b0a51d120f24..6638bda03ec72 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1752,19 +1752,6 @@ mod verify {
         }
     }
 
-    // Verify `wrapping_{shl, shr}` which internally uses `unchecked_{shl,shr}`
-    macro_rules! generate_wrapping_shift_harness {
-        ($type:ty, $method:ident, $harness_name:ident) => {
-            #[kani::proof_for_contract($type::$method)]
-            pub fn $harness_name() {
-                let num1: $type = kani::any::<$type>();
-                let num2: u32 = kani::any::<u32>();
-
-                let _ = num1.$method(num2);
-            }
-        };
-    }
-
     // Part 3: Float to Integer Conversion function Harness Generation Macro
     macro_rules! generate_to_int_unchecked_harness {
         ($floatType:ty, $($intType:ty, $harness_name:ident),+) => {
@@ -2142,55 +2129,6 @@ mod verify {
         (u64::MAX / 2) + 10u64
     );
 
-    // Part_2 `wrapping_shl` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
-    //
-    // Target contracts:
-    // #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
-    //
-    // Target function:
-    // pub const fn wrapping_shl(self, rhs: u32) -> Self
-    //
-    // This function performs an panic-free bitwise left shift operation.
-    generate_wrapping_shift_harness!(i8, wrapping_shl, checked_wrapping_shl_i8);
-    generate_wrapping_shift_harness!(i16, wrapping_shl, checked_wrapping_shl_i16);
-    generate_wrapping_shift_harness!(i32, wrapping_shl, checked_wrapping_shl_i32);
-    generate_wrapping_shift_harness!(i64, wrapping_shl, checked_wrapping_shl_i64);
-    generate_wrapping_shift_harness!(i128, wrapping_shl, checked_wrapping_shl_i128);
-    generate_wrapping_shift_harness!(isize, wrapping_shl, checked_wrapping_shl_isize);
-    generate_wrapping_shift_harness!(u8, wrapping_shl, checked_wrapping_shl_u8);
-    generate_wrapping_shift_harness!(u16, wrapping_shl, checked_wrapping_shl_u16);
-    generate_wrapping_shift_harness!(u32, wrapping_shl, checked_wrapping_shl_u32);
-    generate_wrapping_shift_harness!(u64, wrapping_shl, checked_wrapping_shl_u64);
-    generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128);
-    generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize);
-
-    // Part_2 `wrapping_shr` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
-    //
-    // Target contracts:
-    // #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
-    // Target function:
-    // pub const fn wrapping_shr(self, rhs: u32) -> Self {
-    //
-    // This function performs an panic-free bitwise right shift operation.
-    generate_wrapping_shift_harness!(i8, wrapping_shr, checked_wrapping_shr_i8);
-    generate_wrapping_shift_harness!(i16, wrapping_shr, checked_wrapping_shr_i16);
-    generate_wrapping_shift_harness!(i32, wrapping_shr, checked_wrapping_shr_i32);
-    generate_wrapping_shift_harness!(i64, wrapping_shr, checked_wrapping_shr_i64);
-    generate_wrapping_shift_harness!(i128, wrapping_shr, checked_wrapping_shr_i128);
-    generate_wrapping_shift_harness!(isize, wrapping_shr, checked_wrapping_shr_isize);
-    generate_wrapping_shift_harness!(u8, wrapping_shr, checked_wrapping_shr_u8);
-    generate_wrapping_shift_harness!(u16, wrapping_shr, checked_wrapping_shr_u16);
-    generate_wrapping_shift_harness!(u32, wrapping_shr, checked_wrapping_shr_u32);
-    generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64);
-    generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128);
-    generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);
-
     // `f{16,32,64,128}::to_int_unchecked` proofs
     //
     // Target integer types:

From 2144ebe1d29e647827d132814aca39d6b8622983 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 20:39:28 +0000
Subject: [PATCH 16/29] Use autoharness for num::<impl *>::unchecked_sh{l,r}

---
 .github/workflows/kani.yml  | 12 +++++++
 library/core/src/num/mod.rs | 63 -------------------------------------
 2 files changed, 12 insertions(+), 63 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 8998252fc849d..560cd7db267dd 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,6 +82,18 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern "num::<impl i8>::unchecked_sh" \
+            --include-pattern "num::<impl i16>::unchecked_sh" \
+            --include-pattern "num::<impl i32>::unchecked_sh" \
+            --include-pattern "num::<impl i64>::unchecked_sh" \
+            --include-pattern "num::<impl i128>::unchecked_sh" \
+            --include-pattern "num::<impl isize>::unchecked_sh" \
+            --include-pattern "num::<impl u8>::unchecked_sh" \
+            --include-pattern "num::<impl u16>::unchecked_sh" \
+            --include-pattern "num::<impl u32>::unchecked_sh" \
+            --include-pattern "num::<impl u64>::unchecked_sh" \
+            --include-pattern "num::<impl u128>::unchecked_sh" \
+            --include-pattern "num::<impl usize>::unchecked_sh" \
             --include-pattern "num::<impl i8>::wrapping_sh" \
             --include-pattern "num::<impl i16>::wrapping_sh" \
             --include-pattern "num::<impl i32>::wrapping_sh" \
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 6638bda03ec72..717ef1bb1ef5d 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1651,21 +1651,6 @@ mod verify {
         }
     }
 
-    // Verify `unchecked_{shl, shr}`
-    macro_rules! generate_unchecked_shift_harness {
-        ($type:ty, $method:ident, $harness_name:ident) => {
-            #[kani::proof_for_contract($type::$method)]
-            pub fn $harness_name() {
-                let num1: $type = kani::any::<$type>();
-                let num2: u32 = kani::any::<u32>();
-
-                unsafe {
-                    num1.$method(num2);
-                }
-            }
-        };
-    }
-
     macro_rules! generate_unchecked_neg_harness {
         ($type:ty, $harness_name:ident) => {
             #[kani::proof_for_contract($type::unchecked_neg)]
@@ -1965,54 +1950,6 @@ mod verify {
         usize::MAX
     );
 
-    // unchecked_shr proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
-    //
-    // Target contracts:
-    // #[requires(rhs < <$ActualT>::BITS)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
-    generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8);
-    generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16);
-    generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32);
-    generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64);
-    generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128);
-    generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize);
-    generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8);
-    generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16);
-    generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32);
-    generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
-    generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
-    generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
-
-    // `unchecked_shl` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
-    //
-    // Target contracts:
-    // #[requires(shift < Self::BITS)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_shl(self, shift: u32) -> Self
-    //
-    // This function performs an unchecked bitwise left shift operation.
-    generate_unchecked_shift_harness!(i8, unchecked_shl, checked_unchecked_shl_i8);
-    generate_unchecked_shift_harness!(i16, unchecked_shl, checked_unchecked_shl_i16);
-    generate_unchecked_shift_harness!(i32, unchecked_shl, checked_unchecked_shl_i32);
-    generate_unchecked_shift_harness!(i64, unchecked_shl, checked_unchecked_shl_i64);
-    generate_unchecked_shift_harness!(i128, unchecked_shl, checked_unchecked_shl_i128);
-    generate_unchecked_shift_harness!(isize, unchecked_shl, checked_unchecked_shl_isize);
-    generate_unchecked_shift_harness!(u8, unchecked_shl, checked_unchecked_shl_u8);
-    generate_unchecked_shift_harness!(u16, unchecked_shl, checked_unchecked_shl_u16);
-    generate_unchecked_shift_harness!(u32, unchecked_shl, checked_unchecked_shl_u32);
-    generate_unchecked_shift_harness!(u64, unchecked_shl, checked_unchecked_shl_u64);
-    generate_unchecked_shift_harness!(u128, unchecked_shl, checked_unchecked_shl_u128);
-    generate_unchecked_shift_harness!(usize, unchecked_shl, checked_unchecked_shl_usize);
-
     // `unchecked_sub` proofs
     //
     // Target types:

From e7b0dc459bad1a7c77e181b46e16b9592dc50e7b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 20:42:20 +0000
Subject: [PATCH 17/29] Use autoharness for num::<impl i*>::unchecked_neg

---
 .github/workflows/kani.yml  |  6 ++++++
 library/core/src/num/mod.rs | 30 ------------------------------
 2 files changed, 6 insertions(+), 30 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 560cd7db267dd..2c2b6d19e870a 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,6 +82,12 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern "num::<impl i8>::unchecked_neg" \
+            --include-pattern "num::<impl i16>::unchecked_neg" \
+            --include-pattern "num::<impl i32>::unchecked_neg" \
+            --include-pattern "num::<impl i64>::unchecked_neg" \
+            --include-pattern "num::<impl i128>::unchecked_neg" \
+            --include-pattern "num::<impl isize>::unchecked_neg" \
             --include-pattern "num::<impl i8>::unchecked_sh" \
             --include-pattern "num::<impl i16>::unchecked_sh" \
             --include-pattern "num::<impl i32>::unchecked_sh" \
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 717ef1bb1ef5d..f6e7b4ee88698 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1651,19 +1651,6 @@ mod verify {
         }
     }
 
-    macro_rules! generate_unchecked_neg_harness {
-        ($type:ty, $harness_name:ident) => {
-            #[kani::proof_for_contract($type::unchecked_neg)]
-            pub fn $harness_name() {
-                let num1: $type = kani::any::<$type>();
-
-                unsafe {
-                    num1.unchecked_neg();
-                }
-            }
-        };
-    }
-
     /// A macro to generate Kani proof harnesses for the `carrying_mul` method,
     ///
     /// The macro creates multiple harnesses for different ranges of input values,
@@ -1776,23 +1763,6 @@ mod verify {
     generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
     generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
 
-    // `unchecked_neg` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128,size} -- 6 types in total
-    //
-    // Target contracts:
-    // #[requires(self != $SelfT::MIN)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_neg(self) -> Self
-    generate_unchecked_neg_harness!(i8, checked_unchecked_neg_i8);
-    generate_unchecked_neg_harness!(i16, checked_unchecked_neg_i16);
-    generate_unchecked_neg_harness!(i32, checked_unchecked_neg_i32);
-    generate_unchecked_neg_harness!(i64, checked_unchecked_neg_i64);
-    generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128);
-    generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize);
-
     // `unchecked_mul` proofs
     //
     // Target types:

From 153f5d160fded677772d03e9e07654be771c78ef Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 20:44:01 +0000
Subject: [PATCH 18/29] Use autoharness for num::<impl *>::unchecked_{add,sub}

---
 .github/workflows/kani.yml  | 24 ++++++++++++++++++
 library/core/src/num/mod.rs | 50 -------------------------------------
 2 files changed, 24 insertions(+), 50 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 2c2b6d19e870a..abfde63c5dcfe 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,6 +82,18 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern "num::<impl i8>::unchecked_add" \
+            --include-pattern "num::<impl i16>::unchecked_add" \
+            --include-pattern "num::<impl i32>::unchecked_add" \
+            --include-pattern "num::<impl i64>::unchecked_add" \
+            --include-pattern "num::<impl i128>::unchecked_add" \
+            --include-pattern "num::<impl isize>::unchecked_add" \
+            --include-pattern "num::<impl u8>::unchecked_add" \
+            --include-pattern "num::<impl u16>::unchecked_add" \
+            --include-pattern "num::<impl u32>::unchecked_add" \
+            --include-pattern "num::<impl u64>::unchecked_add" \
+            --include-pattern "num::<impl u128>::unchecked_add" \
+            --include-pattern "num::<impl usize>::unchecked_add" \
             --include-pattern "num::<impl i8>::unchecked_neg" \
             --include-pattern "num::<impl i16>::unchecked_neg" \
             --include-pattern "num::<impl i32>::unchecked_neg" \
@@ -100,6 +112,18 @@ jobs:
             --include-pattern "num::<impl u64>::unchecked_sh" \
             --include-pattern "num::<impl u128>::unchecked_sh" \
             --include-pattern "num::<impl usize>::unchecked_sh" \
+            --include-pattern "num::<impl i8>::unchecked_sub" \
+            --include-pattern "num::<impl i16>::unchecked_sub" \
+            --include-pattern "num::<impl i32>::unchecked_sub" \
+            --include-pattern "num::<impl i64>::unchecked_sub" \
+            --include-pattern "num::<impl i128>::unchecked_sub" \
+            --include-pattern "num::<impl isize>::unchecked_sub" \
+            --include-pattern "num::<impl u8>::unchecked_sub" \
+            --include-pattern "num::<impl u16>::unchecked_sub" \
+            --include-pattern "num::<impl u32>::unchecked_sub" \
+            --include-pattern "num::<impl u64>::unchecked_sub" \
+            --include-pattern "num::<impl u128>::unchecked_sub" \
+            --include-pattern "num::<impl usize>::unchecked_sub" \
             --include-pattern "num::<impl i8>::wrapping_sh" \
             --include-pattern "num::<impl i16>::wrapping_sh" \
             --include-pattern "num::<impl i32>::wrapping_sh" \
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index f6e7b4ee88698..8736982cf4013 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1739,30 +1739,6 @@ mod verify {
         }
     }
 
-    // `unchecked_add` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
-    //
-    // Target contracts:
-    // Preconditions: No overflow should occur
-    // #[requires(!self.overflowing_add(rhs).1)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
-    generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
-    generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16);
-    generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32);
-    generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64);
-    generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128);
-    generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize);
-    generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8);
-    generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16);
-    generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32);
-    generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
-    generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
-    generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
-
     // `unchecked_mul` proofs
     //
     // Target types:
@@ -1920,32 +1896,6 @@ mod verify {
         usize::MAX
     );
 
-    // `unchecked_sub` proofs
-    //
-    // Target types:
-    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
-    //
-    // Target contracts:
-    // Preconditions: No overflow should occur
-    // #[requires(!self.overflowing_sub(rhs).1)]
-    //
-    // Target function:
-    // pub const unsafe fn unchecked_sub(self, rhs: Self)  -> Self
-    //
-    // This function performs an unchecked subtraction operation.
-    generate_unchecked_math_harness!(i8, unchecked_sub, checked_unchecked_sub_i8);
-    generate_unchecked_math_harness!(i16, unchecked_sub, checked_unchecked_sub_i16);
-    generate_unchecked_math_harness!(i32, unchecked_sub, checked_unchecked_sub_i32);
-    generate_unchecked_math_harness!(i64, unchecked_sub, checked_unchecked_sub_i64);
-    generate_unchecked_math_harness!(i128, unchecked_sub, checked_unchecked_sub_i128);
-    generate_unchecked_math_harness!(isize, unchecked_sub, checked_unchecked_sub_isize);
-    generate_unchecked_math_harness!(u8, unchecked_sub, checked_unchecked_sub_u8);
-    generate_unchecked_math_harness!(u16, unchecked_sub, checked_unchecked_sub_u16);
-    generate_unchecked_math_harness!(u32, unchecked_sub, checked_unchecked_sub_u32);
-    generate_unchecked_math_harness!(u64, unchecked_sub, checked_unchecked_sub_u64);
-    generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128);
-    generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize);
-
     // Part_2 `carrying_mul` proofs
     //
     // ====================== u8 Harnesses ======================

From bc70538d68b1c475374207415a00d9b6e726e2ce Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 20:54:05 +0000
Subject: [PATCH 19/29] Use autoharness for convert::num::<impl
 convert::From<num::nonzero::NonZero<*>> for num::nonzero::NonZero<*>>::from

---
 .github/workflows/kani.yml      |  1 +
 library/core/src/convert/num.rs | 68 ---------------------------------
 2 files changed, 1 insertion(+), 68 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index abfde63c5dcfe..472cc4cf4fe77 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,6 +82,7 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern "convert::num::<impl convert::From<num::nonzero::NonZero<" \
             --include-pattern "num::<impl i8>::unchecked_add" \
             --include-pattern "num::<impl i16>::unchecked_add" \
             --include-pattern "num::<impl i32>::unchecked_add" \
diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs
index 7786a3b7b0288..2df5735ed2bc7 100644
--- a/library/core/src/convert/num.rs
+++ b/library/core/src/convert/num.rs
@@ -601,74 +601,6 @@ impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);
 mod verify {
     use super::*;
 
-    // Generate harnesses for `NonZero::<Large>::from(NonZero<Small>)`.
-    macro_rules! generate_nonzero_int_from_nonzero_int_harness {
-        ($Small:ty => $Large:ty, $harness:ident) => {
-            #[kani::proof]
-            pub fn $harness() {
-                let x: NonZero<$Small> = kani::any();
-                let _ = NonZero::<$Large>::from(x);
-            }
-        };
-    }
-
-    // This bundles the calls to `generate_nonzero_int_from_nonzero_int_harness`
-    // macro into segregated namespaces for better organization and usability.
-    macro_rules! generate_nonzero_int_from_nonzero_int_harnesses {
-        ($ns:ident, $Small:ty => $($Large:tt),+ $(,)?) => {
-            mod $ns {
-                use super::*;
-
-                $(
-                    mod $Large {
-                        use super::*;
-
-                        generate_nonzero_int_from_nonzero_int_harness!(
-                            $Small => $Large,
-                            check_nonzero_int_from_nonzero_int
-                        );
-                    }
-                )+
-            }
-        };
-    }
-
-    // non-zero unsigned integer -> non-zero integer, infallible
-    generate_nonzero_int_from_nonzero_int_harnesses!(
-        check_nonzero_int_from_u8,
-        u8 => u16, u32, u64, u128, usize, i16, i32, i64, i128, isize,
-    );
-    generate_nonzero_int_from_nonzero_int_harnesses!(
-        check_nonzero_int_from_u16,
-        u16 => u32, u64, u128, usize, i32, i64, i128,
-    );
-    generate_nonzero_int_from_nonzero_int_harnesses!(
-        check_nonzero_int_from_u32,
-        u32 => u64, u128, i64, i128,
-    );
-    generate_nonzero_int_from_nonzero_int_harnesses!(
-        check_nonzero_int_from_u64,
-        u64 => u128, i128,
-    );
-
-    // non-zero signed integer -> non-zero signed integer, infallible
-    generate_nonzero_int_from_nonzero_int_harnesses!(
-        check_nonzero_int_from_i8,
-        i8 => i16, i32, i64, i128, isize,
-    );
-    generate_nonzero_int_from_nonzero_int_harnesses!(
-        check_nonzero_int_from_i16,
-        i16 => i32, i64, i128, isize,
-    );
-    generate_nonzero_int_from_nonzero_int_harnesses!(
-        check_nonzero_int_from_i32,
-        i32 => i64, i128,
-    );
-    generate_nonzero_int_from_nonzero_int_harnesses!(
-        check_nonzero_int_from_i64,
-        i64 => i128,
-    );
-
     // Generates harnesses for `NonZero::<target>::try_from(NonZero<source>)`.
     // Since the function may be fallible or infallible depending on `source` and `target`,
     // this macro supports generating both cases.

From a0daec5b908e815e392051300a4854c60592ca6a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 21:05:09 +0000
Subject: [PATCH 20/29] Use autoharness for
 num::nonzero::NonZero::<*>::count_ones

---
 .github/workflows/kani.yml      | 12 ++++++++++++
 library/core/src/num/nonzero.rs | 27 +--------------------------
 2 files changed, 13 insertions(+), 26 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 472cc4cf4fe77..cf75bde93abe8 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -137,6 +137,18 @@ jobs:
             --include-pattern "num::<impl u64>::wrapping_sh" \
             --include-pattern "num::<impl u128>::wrapping_sh" \
             --include-pattern "num::<impl usize>::wrapping_sh" \
+            --include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i64>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i128>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<isize>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u8>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u16>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u32>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u64>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u128>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<usize>::count_ones" \
             --include-pattern ptr::align_offset::mod_inv \
             --include-pattern ptr::alignment::Alignment::as_nonzero \
             --include-pattern ptr::alignment::Alignment::as_usize \
diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
index d11e729c2b520..ac5e5e2fe50ec 100644
--- a/library/core/src/num/nonzero.rs
+++ b/library/core/src/num/nonzero.rs
@@ -721,6 +721,7 @@ macro_rules! nonzero_integer {
             #[must_use = "this returns the result of the operation, \
                         without modifying the original"]
             #[inline(always)]
+            #[ensures(|result| result.get() > 0)]
             pub const fn count_ones(self) -> NonZero<u32> {
                 // SAFETY:
                 // `self` is non-zero, which means it has at least one bit set, which means
@@ -2572,32 +2573,6 @@ mod verify {
     nonzero_check_clamp_panic!(core::num::NonZeroU128, nonzero_check_clamp_panic_for_u128);
     nonzero_check_clamp_panic!(core::num::NonZeroUsize, nonzero_check_clamp_panic_for_usize);
 
-    macro_rules! nonzero_check_count_ones {
-        ($nonzero_type:ty, $nonzero_check_count_ones_for:ident) => {
-            #[kani::proof]
-            pub fn $nonzero_check_count_ones_for() {
-                let x: $nonzero_type = kani::any();
-                let result = x.count_ones();
-                // Since x is non-zero, count_ones should never return 0
-                assert!(result.get() > 0);
-            }
-        };
-    }
-
-    // Use the macro to generate different versions of the function for multiple types
-    nonzero_check_count_ones!(core::num::NonZeroI8, nonzero_check_count_ones_for_i8);
-    nonzero_check_count_ones!(core::num::NonZeroI16, nonzero_check_count_ones_for_i16);
-    nonzero_check_count_ones!(core::num::NonZeroI32, nonzero_check_count_ones_for_i32);
-    nonzero_check_count_ones!(core::num::NonZeroI64, nonzero_check_count_ones_for_i64);
-    nonzero_check_count_ones!(core::num::NonZeroI128, nonzero_check_count_ones_for_i128);
-    nonzero_check_count_ones!(core::num::NonZeroIsize, nonzero_check_count_ones_for_isize);
-    nonzero_check_count_ones!(core::num::NonZeroU8, nonzero_check_count_ones_for_u8);
-    nonzero_check_count_ones!(core::num::NonZeroU16, nonzero_check_count_ones_for_u16);
-    nonzero_check_count_ones!(core::num::NonZeroU32, nonzero_check_count_ones_for_u32);
-    nonzero_check_count_ones!(core::num::NonZeroU64, nonzero_check_count_ones_for_u64);
-    nonzero_check_count_ones!(core::num::NonZeroU128, nonzero_check_count_ones_for_u128);
-    nonzero_check_count_ones!(core::num::NonZeroUsize, nonzero_check_count_ones_for_usize);
-
     macro_rules! nonzero_check_rotate_left_and_right {
         ($nonzero_type:ty, $nonzero_check_rotate_for:ident) => {
             #[kani::proof]

From f079d4cf1724dc90718fc5aa613dbd3ca3d2ec55 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 21:11:24 +0000
Subject: [PATCH 21/29] Use autoharness for
 num::nonzero::NonZero::<*>::rotate_{left,right}

---
 .github/workflows/kani.yml      | 12 ++++++++++++
 library/core/src/num/nonzero.rs | 30 ++++--------------------------
 2 files changed, 16 insertions(+), 26 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index cf75bde93abe8..67ecff04709fc 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -149,6 +149,18 @@ jobs:
             --include-pattern "num::nonzero::NonZero::<u64>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<u128>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<usize>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i8>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i16>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i32>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i64>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i128>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<isize>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u8>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u16>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u32>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u64>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u128>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<usize>::rotate_" \
             --include-pattern ptr::align_offset::mod_inv \
             --include-pattern ptr::alignment::Alignment::as_nonzero \
             --include-pattern ptr::alignment::Alignment::as_usize \
diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
index ac5e5e2fe50ec..83ebd7fbe1922 100644
--- a/library/core/src/num/nonzero.rs
+++ b/library/core/src/num/nonzero.rs
@@ -755,6 +755,8 @@ macro_rules! nonzero_integer {
             #[must_use = "this returns the result of the operation, \
                         without modifying the original"]
             #[inline(always)]
+            #[ensures(|result| result.get() > 0)]
+            #[ensures(|result| result.rotate_right(n).get() == old(self).get())]
             pub const fn rotate_left(self, n: u32) -> Self {
                 let result = self.get().rotate_left(n);
                 // SAFETY: Rotating bits preserves the property int > 0.
@@ -788,6 +790,8 @@ macro_rules! nonzero_integer {
             #[must_use = "this returns the result of the operation, \
                         without modifying the original"]
             #[inline(always)]
+            #[ensures(|result| result.get() > 0)]
+            #[ensures(|result| result.rotate_left(n).get() == old(self).get())]
             pub const fn rotate_right(self, n: u32) -> Self {
                 let result = self.get().rotate_right(n);
                 // SAFETY: Rotating bits preserves the property int > 0.
@@ -2572,30 +2576,4 @@ mod verify {
     nonzero_check_clamp_panic!(core::num::NonZeroU64, nonzero_check_clamp_panic_for_u64);
     nonzero_check_clamp_panic!(core::num::NonZeroU128, nonzero_check_clamp_panic_for_u128);
     nonzero_check_clamp_panic!(core::num::NonZeroUsize, nonzero_check_clamp_panic_for_usize);
-
-    macro_rules! nonzero_check_rotate_left_and_right {
-        ($nonzero_type:ty, $nonzero_check_rotate_for:ident) => {
-            #[kani::proof]
-            pub fn $nonzero_check_rotate_for() {
-                let x: $nonzero_type = kani::any();
-                let n: u32 = kani::any();
-                let result = x.rotate_left(n).rotate_right(n);
-                assert!(result == x);
-            }
-        };
-    }
-
-    // Use the macro to generate different versions of the function for multiple types
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI8, nonzero_check_rotate_for_i8);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI16, nonzero_check_rotate_for_i16);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI32, nonzero_check_rotate_for_i32);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI64, nonzero_check_rotate_for_i64);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI128, nonzero_check_rotate_for_i128);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroIsize, nonzero_check_rotate_for_isize);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU8, nonzero_check_rotate_for_u8);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU16, nonzero_check_rotate_for_u16);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU32, nonzero_check_rotate_for_u32);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU64, nonzero_check_rotate_for_u64);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU128, nonzero_check_rotate_for_u128);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroUsize, nonzero_check_rotate_for_usize);
 }

From 1e17495fb00fe7827f4ee87afbf9fc6b3819bf28 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 21:25:58 +0000
Subject: [PATCH 22/29] Use array for command_args to ensure quoting is
 retained

---
 scripts/run-kani.sh | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 84c419d745d0c..547f315074c60 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -14,7 +14,7 @@ usage() {
 }
 
 # Initialize variables
-command_args=""
+declare -a command_args
 path=""
 run_command="verify-std"
 with_autoharness="false"
@@ -50,7 +50,7 @@ while [[ $# -gt 0 ]]; do
             ;;
         --kani-args)
             shift
-            command_args="$@"
+            command_args=("$@")
             break
             ;;
         *)
@@ -217,7 +217,7 @@ run_verification_subset() {
         $harness_args --exact \
         -j \
         --output-format=terse \
-        $command_args \
+        "${command_args[@]}" \
         --enable-unstable \
         --cbmc-args --object-bits 12
 }
@@ -299,7 +299,7 @@ main() {
             "$kani_path" verify-std -Z unstable-options ./library \
                 $unstable_args \
                 --no-assert-contracts \
-                $command_args \
+                "${command_args[@]}" \
                 --enable-unstable \
                 --cbmc-args --object-bits 12
         fi
@@ -310,7 +310,7 @@ main() {
           "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \
               $unstable_args \
               --no-assert-contracts \
-              $command_args \
+              "${command_args[@]}" \
               --enable-unstable \
               --cbmc-args --object-bits 12
     elif [[ "$run_command" == "list" ]]; then

From 7798495f9bd95f0a8f8e5afd1fc89cba4b8ff6f6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 21:29:10 +0000
Subject: [PATCH 23/29] Do not try to use unset CBMC_PATCH variable

---
 scripts/run-kani.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 547f315074c60..87b5a78c97a74 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -151,7 +151,7 @@ build_kani() {
     source "kani-dependencies"
     # Check if installed versions are correct.
     if ./scripts/check-cbmc-version.py \
-            --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} --patch ${CBMC_PATCH} \
+            --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} \
             && ./scripts/check_kissat_version.sh; then
         echo "Dependencies are up-to-date"
     else

From 308f6a1cd596898ae4128fffc822fe9bfc57ff49 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 21:37:55 +0000
Subject: [PATCH 24/29] Revert "Use autoharness for convert::num::<impl
 convert::From<num::nonzero::NonZero<*>> for num::nonzero::NonZero<*>>::from"

This reverts commit bc70538d68b1c475374207415a00d9b6e726e2ce.
---
 .github/workflows/kani.yml      |  1 -
 library/core/src/convert/num.rs | 68 +++++++++++++++++++++++++++++++++
 2 files changed, 68 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 67ecff04709fc..80ebaaaf053eb 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,7 +82,6 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
-            --include-pattern "convert::num::<impl convert::From<num::nonzero::NonZero<" \
             --include-pattern "num::<impl i8>::unchecked_add" \
             --include-pattern "num::<impl i16>::unchecked_add" \
             --include-pattern "num::<impl i32>::unchecked_add" \
diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs
index 2df5735ed2bc7..7786a3b7b0288 100644
--- a/library/core/src/convert/num.rs
+++ b/library/core/src/convert/num.rs
@@ -601,6 +601,74 @@ impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);
 mod verify {
     use super::*;
 
+    // Generate harnesses for `NonZero::<Large>::from(NonZero<Small>)`.
+    macro_rules! generate_nonzero_int_from_nonzero_int_harness {
+        ($Small:ty => $Large:ty, $harness:ident) => {
+            #[kani::proof]
+            pub fn $harness() {
+                let x: NonZero<$Small> = kani::any();
+                let _ = NonZero::<$Large>::from(x);
+            }
+        };
+    }
+
+    // This bundles the calls to `generate_nonzero_int_from_nonzero_int_harness`
+    // macro into segregated namespaces for better organization and usability.
+    macro_rules! generate_nonzero_int_from_nonzero_int_harnesses {
+        ($ns:ident, $Small:ty => $($Large:tt),+ $(,)?) => {
+            mod $ns {
+                use super::*;
+
+                $(
+                    mod $Large {
+                        use super::*;
+
+                        generate_nonzero_int_from_nonzero_int_harness!(
+                            $Small => $Large,
+                            check_nonzero_int_from_nonzero_int
+                        );
+                    }
+                )+
+            }
+        };
+    }
+
+    // non-zero unsigned integer -> non-zero integer, infallible
+    generate_nonzero_int_from_nonzero_int_harnesses!(
+        check_nonzero_int_from_u8,
+        u8 => u16, u32, u64, u128, usize, i16, i32, i64, i128, isize,
+    );
+    generate_nonzero_int_from_nonzero_int_harnesses!(
+        check_nonzero_int_from_u16,
+        u16 => u32, u64, u128, usize, i32, i64, i128,
+    );
+    generate_nonzero_int_from_nonzero_int_harnesses!(
+        check_nonzero_int_from_u32,
+        u32 => u64, u128, i64, i128,
+    );
+    generate_nonzero_int_from_nonzero_int_harnesses!(
+        check_nonzero_int_from_u64,
+        u64 => u128, i128,
+    );
+
+    // non-zero signed integer -> non-zero signed integer, infallible
+    generate_nonzero_int_from_nonzero_int_harnesses!(
+        check_nonzero_int_from_i8,
+        i8 => i16, i32, i64, i128, isize,
+    );
+    generate_nonzero_int_from_nonzero_int_harnesses!(
+        check_nonzero_int_from_i16,
+        i16 => i32, i64, i128, isize,
+    );
+    generate_nonzero_int_from_nonzero_int_harnesses!(
+        check_nonzero_int_from_i32,
+        i32 => i64, i128,
+    );
+    generate_nonzero_int_from_nonzero_int_harnesses!(
+        check_nonzero_int_from_i64,
+        i64 => i128,
+    );
+
     // Generates harnesses for `NonZero::<target>::try_from(NonZero<source>)`.
     // Since the function may be fallible or infallible depending on `source` and `target`,
     // this macro supports generating both cases.

From a90ba682cff74633034cb0a7d2eeb2e0d1826284 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 21:38:00 +0000
Subject: [PATCH 25/29] Revert "Use autoharness for num::<impl
 *>::unchecked_{add,sub}"

This reverts commit 153f5d160fded677772d03e9e07654be771c78ef.
---
 .github/workflows/kani.yml  | 24 ------------------
 library/core/src/num/mod.rs | 50 +++++++++++++++++++++++++++++++++++++
 2 files changed, 50 insertions(+), 24 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 80ebaaaf053eb..ecbdf07e31689 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,18 +82,6 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
-            --include-pattern "num::<impl i8>::unchecked_add" \
-            --include-pattern "num::<impl i16>::unchecked_add" \
-            --include-pattern "num::<impl i32>::unchecked_add" \
-            --include-pattern "num::<impl i64>::unchecked_add" \
-            --include-pattern "num::<impl i128>::unchecked_add" \
-            --include-pattern "num::<impl isize>::unchecked_add" \
-            --include-pattern "num::<impl u8>::unchecked_add" \
-            --include-pattern "num::<impl u16>::unchecked_add" \
-            --include-pattern "num::<impl u32>::unchecked_add" \
-            --include-pattern "num::<impl u64>::unchecked_add" \
-            --include-pattern "num::<impl u128>::unchecked_add" \
-            --include-pattern "num::<impl usize>::unchecked_add" \
             --include-pattern "num::<impl i8>::unchecked_neg" \
             --include-pattern "num::<impl i16>::unchecked_neg" \
             --include-pattern "num::<impl i32>::unchecked_neg" \
@@ -112,18 +100,6 @@ jobs:
             --include-pattern "num::<impl u64>::unchecked_sh" \
             --include-pattern "num::<impl u128>::unchecked_sh" \
             --include-pattern "num::<impl usize>::unchecked_sh" \
-            --include-pattern "num::<impl i8>::unchecked_sub" \
-            --include-pattern "num::<impl i16>::unchecked_sub" \
-            --include-pattern "num::<impl i32>::unchecked_sub" \
-            --include-pattern "num::<impl i64>::unchecked_sub" \
-            --include-pattern "num::<impl i128>::unchecked_sub" \
-            --include-pattern "num::<impl isize>::unchecked_sub" \
-            --include-pattern "num::<impl u8>::unchecked_sub" \
-            --include-pattern "num::<impl u16>::unchecked_sub" \
-            --include-pattern "num::<impl u32>::unchecked_sub" \
-            --include-pattern "num::<impl u64>::unchecked_sub" \
-            --include-pattern "num::<impl u128>::unchecked_sub" \
-            --include-pattern "num::<impl usize>::unchecked_sub" \
             --include-pattern "num::<impl i8>::wrapping_sh" \
             --include-pattern "num::<impl i16>::wrapping_sh" \
             --include-pattern "num::<impl i32>::wrapping_sh" \
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 8736982cf4013..f6e7b4ee88698 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1739,6 +1739,30 @@ mod verify {
         }
     }
 
+    // `unchecked_add` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // Preconditions: No overflow should occur
+    // #[requires(!self.overflowing_add(rhs).1)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
+    generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
+    generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16);
+    generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32);
+    generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64);
+    generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128);
+    generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize);
+    generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8);
+    generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16);
+    generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32);
+    generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
+    generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
+    generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
+
     // `unchecked_mul` proofs
     //
     // Target types:
@@ -1896,6 +1920,32 @@ mod verify {
         usize::MAX
     );
 
+    // `unchecked_sub` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // Preconditions: No overflow should occur
+    // #[requires(!self.overflowing_sub(rhs).1)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_sub(self, rhs: Self)  -> Self
+    //
+    // This function performs an unchecked subtraction operation.
+    generate_unchecked_math_harness!(i8, unchecked_sub, checked_unchecked_sub_i8);
+    generate_unchecked_math_harness!(i16, unchecked_sub, checked_unchecked_sub_i16);
+    generate_unchecked_math_harness!(i32, unchecked_sub, checked_unchecked_sub_i32);
+    generate_unchecked_math_harness!(i64, unchecked_sub, checked_unchecked_sub_i64);
+    generate_unchecked_math_harness!(i128, unchecked_sub, checked_unchecked_sub_i128);
+    generate_unchecked_math_harness!(isize, unchecked_sub, checked_unchecked_sub_isize);
+    generate_unchecked_math_harness!(u8, unchecked_sub, checked_unchecked_sub_u8);
+    generate_unchecked_math_harness!(u16, unchecked_sub, checked_unchecked_sub_u16);
+    generate_unchecked_math_harness!(u32, unchecked_sub, checked_unchecked_sub_u32);
+    generate_unchecked_math_harness!(u64, unchecked_sub, checked_unchecked_sub_u64);
+    generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128);
+    generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize);
+
     // Part_2 `carrying_mul` proofs
     //
     // ====================== u8 Harnesses ======================

From 3aefe477dcbd7a8cbbe6bd2f34acdeb0dfd2de9c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 21:38:06 +0000
Subject: [PATCH 26/29] Revert "Use autoharness for num::<impl
 i*>::unchecked_neg"

This reverts commit e7b0dc459bad1a7c77e181b46e16b9592dc50e7b.
---
 .github/workflows/kani.yml  |  6 ------
 library/core/src/num/mod.rs | 30 ++++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index ecbdf07e31689..0525156046731 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,12 +82,6 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
-            --include-pattern "num::<impl i8>::unchecked_neg" \
-            --include-pattern "num::<impl i16>::unchecked_neg" \
-            --include-pattern "num::<impl i32>::unchecked_neg" \
-            --include-pattern "num::<impl i64>::unchecked_neg" \
-            --include-pattern "num::<impl i128>::unchecked_neg" \
-            --include-pattern "num::<impl isize>::unchecked_neg" \
             --include-pattern "num::<impl i8>::unchecked_sh" \
             --include-pattern "num::<impl i16>::unchecked_sh" \
             --include-pattern "num::<impl i32>::unchecked_sh" \
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index f6e7b4ee88698..717ef1bb1ef5d 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1651,6 +1651,19 @@ mod verify {
         }
     }
 
+    macro_rules! generate_unchecked_neg_harness {
+        ($type:ty, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::unchecked_neg)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+
+                unsafe {
+                    num1.unchecked_neg();
+                }
+            }
+        };
+    }
+
     /// A macro to generate Kani proof harnesses for the `carrying_mul` method,
     ///
     /// The macro creates multiple harnesses for different ranges of input values,
@@ -1763,6 +1776,23 @@ mod verify {
     generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
     generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
 
+    // `unchecked_neg` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} -- 6 types in total
+    //
+    // Target contracts:
+    // #[requires(self != $SelfT::MIN)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_neg(self) -> Self
+    generate_unchecked_neg_harness!(i8, checked_unchecked_neg_i8);
+    generate_unchecked_neg_harness!(i16, checked_unchecked_neg_i16);
+    generate_unchecked_neg_harness!(i32, checked_unchecked_neg_i32);
+    generate_unchecked_neg_harness!(i64, checked_unchecked_neg_i64);
+    generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128);
+    generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize);
+
     // `unchecked_mul` proofs
     //
     // Target types:

From dcc1959287ae9e2c67d84b389b315b0203027040 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 21:38:11 +0000
Subject: [PATCH 27/29] Revert "Use autoharness for num::<impl
 *>::unchecked_sh{l,r}"

This reverts commit 2144ebe1d29e647827d132814aca39d6b8622983.
---
 .github/workflows/kani.yml  | 12 -------
 library/core/src/num/mod.rs | 63 +++++++++++++++++++++++++++++++++++++
 2 files changed, 63 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 0525156046731..9acf835ab5f26 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,18 +82,6 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
-            --include-pattern "num::<impl i8>::unchecked_sh" \
-            --include-pattern "num::<impl i16>::unchecked_sh" \
-            --include-pattern "num::<impl i32>::unchecked_sh" \
-            --include-pattern "num::<impl i64>::unchecked_sh" \
-            --include-pattern "num::<impl i128>::unchecked_sh" \
-            --include-pattern "num::<impl isize>::unchecked_sh" \
-            --include-pattern "num::<impl u8>::unchecked_sh" \
-            --include-pattern "num::<impl u16>::unchecked_sh" \
-            --include-pattern "num::<impl u32>::unchecked_sh" \
-            --include-pattern "num::<impl u64>::unchecked_sh" \
-            --include-pattern "num::<impl u128>::unchecked_sh" \
-            --include-pattern "num::<impl usize>::unchecked_sh" \
             --include-pattern "num::<impl i8>::wrapping_sh" \
             --include-pattern "num::<impl i16>::wrapping_sh" \
             --include-pattern "num::<impl i32>::wrapping_sh" \
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 717ef1bb1ef5d..6638bda03ec72 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1651,6 +1651,21 @@ mod verify {
         }
     }
 
+    // Verify `unchecked_{shl, shr}`
+    macro_rules! generate_unchecked_shift_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: u32 = kani::any::<u32>();
+
+                unsafe {
+                    num1.$method(num2);
+                }
+            }
+        };
+    }
+
     macro_rules! generate_unchecked_neg_harness {
         ($type:ty, $harness_name:ident) => {
             #[kani::proof_for_contract($type::unchecked_neg)]
@@ -1950,6 +1965,54 @@ mod verify {
         usize::MAX
     );
 
+    // unchecked_shr proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[requires(rhs < <$ActualT>::BITS)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
+    generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8);
+    generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16);
+    generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32);
+    generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64);
+    generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128);
+    generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize);
+    generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8);
+    generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16);
+    generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32);
+    generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
+    generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
+    generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
+
+    // `unchecked_shl` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[requires(shift < Self::BITS)]
+    //
+    // Target function:
+    // pub const unsafe fn unchecked_shl(self, shift: u32) -> Self
+    //
+    // This function performs an unchecked bitwise left shift operation.
+    generate_unchecked_shift_harness!(i8, unchecked_shl, checked_unchecked_shl_i8);
+    generate_unchecked_shift_harness!(i16, unchecked_shl, checked_unchecked_shl_i16);
+    generate_unchecked_shift_harness!(i32, unchecked_shl, checked_unchecked_shl_i32);
+    generate_unchecked_shift_harness!(i64, unchecked_shl, checked_unchecked_shl_i64);
+    generate_unchecked_shift_harness!(i128, unchecked_shl, checked_unchecked_shl_i128);
+    generate_unchecked_shift_harness!(isize, unchecked_shl, checked_unchecked_shl_isize);
+    generate_unchecked_shift_harness!(u8, unchecked_shl, checked_unchecked_shl_u8);
+    generate_unchecked_shift_harness!(u16, unchecked_shl, checked_unchecked_shl_u16);
+    generate_unchecked_shift_harness!(u32, unchecked_shl, checked_unchecked_shl_u32);
+    generate_unchecked_shift_harness!(u64, unchecked_shl, checked_unchecked_shl_u64);
+    generate_unchecked_shift_harness!(u128, unchecked_shl, checked_unchecked_shl_u128);
+    generate_unchecked_shift_harness!(usize, unchecked_shl, checked_unchecked_shl_usize);
+
     // `unchecked_sub` proofs
     //
     // Target types:

From 7162c25fc70711de4fd03b3dbb2dabacd492fdcc Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 25 Apr 2025 21:39:00 +0000
Subject: [PATCH 28/29] Revert "Use autoharness for num::<impl
 *>::wrapping_sh{l,r}"

This reverts commit 0c1b5c3f158f3f614e36818f3a0c123b16361349.
---
 .github/workflows/kani.yml  | 12 -------
 library/core/src/num/mod.rs | 62 +++++++++++++++++++++++++++++++++++++
 2 files changed, 62 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 9acf835ab5f26..bc28f54824135 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -82,18 +82,6 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
-            --include-pattern "num::<impl i8>::wrapping_sh" \
-            --include-pattern "num::<impl i16>::wrapping_sh" \
-            --include-pattern "num::<impl i32>::wrapping_sh" \
-            --include-pattern "num::<impl i64>::wrapping_sh" \
-            --include-pattern "num::<impl i128>::wrapping_sh" \
-            --include-pattern "num::<impl isize>::wrapping_sh" \
-            --include-pattern "num::<impl u8>::wrapping_sh" \
-            --include-pattern "num::<impl u16>::wrapping_sh" \
-            --include-pattern "num::<impl u32>::wrapping_sh" \
-            --include-pattern "num::<impl u64>::wrapping_sh" \
-            --include-pattern "num::<impl u128>::wrapping_sh" \
-            --include-pattern "num::<impl usize>::wrapping_sh" \
             --include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 6638bda03ec72..0b0a51d120f24 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -1752,6 +1752,19 @@ mod verify {
         }
     }
 
+    // Verify `wrapping_{shl, shr}` which internally uses `unchecked_{shl,shr}`
+    macro_rules! generate_wrapping_shift_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: u32 = kani::any::<u32>();
+
+                let _ = num1.$method(num2);
+            }
+        };
+    }
+
     // Part 3: Float to Integer Conversion function Harness Generation Macro
     macro_rules! generate_to_int_unchecked_harness {
         ($floatType:ty, $($intType:ty, $harness_name:ident),+) => {
@@ -2129,6 +2142,55 @@ mod verify {
         (u64::MAX / 2) + 10u64
     );
 
+    // Part_2 `wrapping_shl` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
+    //
+    // Target function:
+    // pub const fn wrapping_shl(self, rhs: u32) -> Self
+    //
+    // This function performs an panic-free bitwise left shift operation.
+    generate_wrapping_shift_harness!(i8, wrapping_shl, checked_wrapping_shl_i8);
+    generate_wrapping_shift_harness!(i16, wrapping_shl, checked_wrapping_shl_i16);
+    generate_wrapping_shift_harness!(i32, wrapping_shl, checked_wrapping_shl_i32);
+    generate_wrapping_shift_harness!(i64, wrapping_shl, checked_wrapping_shl_i64);
+    generate_wrapping_shift_harness!(i128, wrapping_shl, checked_wrapping_shl_i128);
+    generate_wrapping_shift_harness!(isize, wrapping_shl, checked_wrapping_shl_isize);
+    generate_wrapping_shift_harness!(u8, wrapping_shl, checked_wrapping_shl_u8);
+    generate_wrapping_shift_harness!(u16, wrapping_shl, checked_wrapping_shl_u16);
+    generate_wrapping_shift_harness!(u32, wrapping_shl, checked_wrapping_shl_u32);
+    generate_wrapping_shift_harness!(u64, wrapping_shl, checked_wrapping_shl_u64);
+    generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128);
+    generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize);
+
+    // Part_2 `wrapping_shr` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
+    // Target function:
+    // pub const fn wrapping_shr(self, rhs: u32) -> Self {
+    //
+    // This function performs an panic-free bitwise right shift operation.
+    generate_wrapping_shift_harness!(i8, wrapping_shr, checked_wrapping_shr_i8);
+    generate_wrapping_shift_harness!(i16, wrapping_shr, checked_wrapping_shr_i16);
+    generate_wrapping_shift_harness!(i32, wrapping_shr, checked_wrapping_shr_i32);
+    generate_wrapping_shift_harness!(i64, wrapping_shr, checked_wrapping_shr_i64);
+    generate_wrapping_shift_harness!(i128, wrapping_shr, checked_wrapping_shr_i128);
+    generate_wrapping_shift_harness!(isize, wrapping_shr, checked_wrapping_shr_isize);
+    generate_wrapping_shift_harness!(u8, wrapping_shr, checked_wrapping_shr_u8);
+    generate_wrapping_shift_harness!(u16, wrapping_shr, checked_wrapping_shr_u16);
+    generate_wrapping_shift_harness!(u32, wrapping_shr, checked_wrapping_shr_u32);
+    generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64);
+    generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128);
+    generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);
+
     // `f{16,32,64,128}::to_int_unchecked` proofs
     //
     // Target integer types:

From 83dfb824a02e1262e83f7f150cf92eeb598e25e6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 29 Apr 2025 09:27:40 +0000
Subject: [PATCH 29/29] Clarify use

---
 .github/workflows/kani.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index bc28f54824135..71251fab40860 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -75,7 +75,9 @@ jobs:
 
       # Step 2: Run Kani autoharness on the std library for selected functions.
       # Uses "--include-pattern" to make sure we do not try to run across all
-      # possible functions as that may take a lot longer than expected
+      # possible functions as that may take a lot longer than expected. Instead,
+      # explicitly list all functions (or prefixes thereof) the proofs of which
+      # are known to pass.
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \