From 8f5512db864f3c568766b7f5b90d83a31320445c Mon Sep 17 00:00:00 2001
From: Daniel Tu <135958699+danielhumanmod@users.noreply.github.com>
Date: Wed, 20 Nov 2024 09:15:54 -0800
Subject: [PATCH 01/13] Contracts & Harnesses for `swap`, `replace`, and
 `drop_in_place` (#144)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

# Description
This PR introduces function contracts and proof harness for the NonNull
pointer in the Rust core library. Specifically, it verifies three new
APIs—`swap`, `replace`, and `drop_in_place` with Kani. These changes
enhance the functionality of memory operations for NonNull pointers.

# Change Overview
Covered APIs:
1. NonNull::swap: Swaps the values at two mutable locations of the same
type
2. NonNull::replace: Replaces the pointer's value, returning the old
value
3. NonNull::drop_in_place: Executes the destructor (if any) of the
pointed-to value

Resolves #53

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 library/core/src/ptr/non_null.rs | 63 +++++++++++++++++++++++++++++++-
 1 file changed, 62 insertions(+), 1 deletion(-)

diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index e6f5bff9eca60..4834c8009ec44 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -10,7 +10,6 @@ use crate::ub_checks::assert_unsafe_precondition;
 use crate::{fmt, hash, intrinsics, ptr};
 use safety::{ensures, requires};
 
-
 #[cfg(kani)]
 use crate::kani;
 #[cfg(kani)]
@@ -1060,6 +1059,8 @@ impl<T: ?Sized> NonNull<T> {
     /// [`ptr::drop_in_place`]: crate::ptr::drop_in_place()
     #[inline(always)]
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure self is aligned, initialized, and valid for read
+    #[requires(ub_checks::can_write(self.as_ptr() as *mut()))] // Ensure self is valid for write
     pub unsafe fn drop_in_place(self) {
         // SAFETY: the caller must uphold the safety contract for `drop_in_place`.
         unsafe { ptr::drop_in_place(self.as_ptr()) }
@@ -1151,6 +1152,9 @@ impl<T: ?Sized> NonNull<T> {
     /// [`ptr::replace`]: crate::ptr::replace()
     #[inline(always)]
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[cfg_attr(kani, kani::modifies(self.as_ptr()))]
+    #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self is aligned, initialized, and valid for read
+    #[requires(ub_checks::can_write(self.as_ptr()))] // Ensure self is valid for write
     pub unsafe fn replace(self, src: T) -> T
     where
         T: Sized,
@@ -1169,6 +1173,9 @@ impl<T: ?Sized> NonNull<T> {
     #[inline(always)]
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_unstable(feature = "const_swap", issue = "83163")]
+    #[cfg_attr(kani, kani::modifies(self.as_ptr(), with.as_ptr()))]
+    #[requires(ub_checks::can_dereference(self.as_ptr()) && ub_checks::can_write(self.as_ptr()))]
+    #[requires(ub_checks::can_dereference(with.as_ptr()) && ub_checks::can_write(with.as_ptr()))]
     pub const unsafe fn swap(self, with: NonNull<T>)
     where
         T: Sized,
@@ -2118,4 +2125,58 @@ mod verify {
             let _ = ptr.get_unchecked_mut(lower..upper);
         }
     }
+
+    #[kani::proof_for_contract(NonNull::replace)]
+    pub fn non_null_check_replace() {
+        let mut x: i32 = kani::any();
+        let mut y: i32 = kani::any();
+
+        let origin_ptr = NonNull::new(&mut x as *mut i32).unwrap();
+        unsafe {
+            let captured_original = ptr::read(origin_ptr.as_ptr());
+            let replaced = origin_ptr.replace(y);
+            let after_replace = ptr::read(origin_ptr.as_ptr());
+
+            assert_eq!(captured_original, replaced);
+            assert_eq!(after_replace, y)
+        }
+    }
+
+    #[kani::proof_for_contract(NonNull::drop_in_place)]
+    pub fn non_null_check_drop_in_place() {
+        struct Droppable {
+            value: i32,
+        }
+        
+        impl Drop for Droppable {
+            fn drop(&mut self) {
+            }
+        }
+
+        let mut droppable = Droppable { value: kani::any() };
+        let ptr = NonNull::new(&mut droppable as *mut Droppable).unwrap();
+        unsafe {
+            ptr.drop_in_place();
+        }
+    }
+
+    #[kani::proof_for_contract(NonNull::swap)]
+    pub fn non_null_check_swap() {
+        let mut a: i32 = kani::any();
+        let mut b: i32 = kani::any();
+
+        let ptr_a = NonNull::new(&mut a as *mut i32).unwrap();
+        let ptr_b = NonNull::new(&mut b as *mut i32).unwrap();
+
+        unsafe {
+            let old_a = ptr::read(ptr_a.as_ptr());
+            let old_b = ptr::read(ptr_b.as_ptr());
+            ptr_a.swap(ptr_b);
+            // Verify that the values have been swapped.
+            let new_a = ptr::read(ptr_a.as_ptr());
+            let new_b = ptr::read(ptr_b.as_ptr());
+            assert_eq!(old_a, new_b);
+            assert_eq!(old_b, new_a);
+        }
+    }
 }

From 971befd78b5e59456280724e8c67bf1a3b43c42b Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 20 Nov 2024 11:43:45 -0800
Subject: [PATCH 02/13] Improve run-kani script to use default target (#172)

Use default target folder instead of using a temporary folder. Users are
still able to customize the folder using Kani argument.

Avoid needless updates when Kani dependencies are
already up-to-date.

Fixes #170
---
 scripts/run-kani.sh | 63 ++++++++++++++++++++++++++-------------------
 1 file changed, 36 insertions(+), 27 deletions(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index e8f0dc42193d6..e32bb22c23f56 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -92,15 +92,26 @@ read_commit_from_toml() {
     echo "$commit"
 }
 
-clone_kani_repo() {
+setup_kani_repo() {
     local repo_url="$1"
     local directory="$2"
     local branch="$3"
     local commit="$4"
-    git clone "$repo_url" "$directory"
-    pushd "$directory"
-    git checkout "$commit"
-    popd
+
+    if [[ ! -d "${directory}" ]]; then
+        mkdir -p "${directory}"
+        pushd "${directory}" > /dev/null
+
+        git init . >& /dev/null
+        git remote add origin "${repo_url}" >& /dev/null
+    else
+        pushd "${directory}" > /dev/null
+    fi
+
+    git fetch --depth 1 origin "$commit" --quiet
+    git checkout "$commit" --quiet
+    git submodule update --init --recursive --depth 1 --quiet
+    popd > /dev/null
 }
 
 get_current_commit() {
@@ -115,17 +126,22 @@ get_current_commit() {
 build_kani() {
     local directory="$1"
     pushd "$directory"
-    os_name=$(uname -s)
-
-    if [[ "$os_name" == "Linux" ]]; then
-        ./scripts/setup/ubuntu/install_deps.sh
-    elif [[ "$os_name" == "Darwin" ]]; then
-        ./scripts/setup/macos/install_deps.sh
+    source "kani-dependencies"
+    # Check if installed versions are correct.
+    if ./scripts/check-cbmc-version.py --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} && ./scripts/check_kissat_version.sh; then
+        echo "Dependencies are up-to-date"
     else
-        echo "Unknown operating system"
+        os_name=$(uname -s)
+
+        if [[ "$os_name" == "Linux" ]]; then
+            ./scripts/setup/ubuntu/install_deps.sh
+        elif [[ "$os_name" == "Darwin" ]]; then
+            ./scripts/setup/macos/install_deps.sh
+        else
+            echo "Unknown operating system"
+        fi
     fi
 
-    git submodule update --init --recursive
     cargo build-dev --release
     popd
 }
@@ -147,11 +163,15 @@ check_binary_exists() {
     local expected_commit="$2"
     local kani_path=$(get_kani_path "$build_dir")
 
-    if [[ -f "$kani_path" ]]; then
+    if [[ -d "${build_dir}" ]]; then
         local current_commit=$(get_current_commit "$build_dir")
         if [[ "$current_commit" = "$expected_commit" ]]; then
             return 0
+        else
+            echo "Kani repository is out of date. Rebuilding..."
         fi
+    else
+        echo "Kani repository not found. Creating..."
     fi
     return 1
 }
@@ -159,7 +179,6 @@ check_binary_exists() {
 
 main() {
     local build_dir="$WORK_DIR/kani_build"
-    local temp_dir_target=$(mktemp -d)
 
     echo "Using TOML file: $TOML_FILE"
     echo "Using repository URL: $REPO_URL"
@@ -173,12 +192,8 @@ main() {
     else
         echo "Building Kani from commit: $commit"
 
-        # Remove old build directory if it exists
-        rm -rf "$build_dir"
-        mkdir -p "$build_dir"
-
         # Clone repository and checkout specific commit
-        clone_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
+        setup_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
 
         # Build project
         build_kani "$build_dir"
@@ -195,7 +210,7 @@ main() {
 
     if [[ "$run_command" == "verify-std" ]]; then
         echo "Running Kani verify-std command..."
-        "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" \
+        "$kani_path" verify-std -Z unstable-options ./library \
             -Z function-contracts \
             -Z mem-predicates \
             -Z loop-contracts \
@@ -211,9 +226,3 @@ main() {
 
 main
 
-cleanup()
-{
-  rm -rf "$temp_dir_target"
-}
-
-trap cleanup EXIT

From a8dd9753fb7d02f9e023083bb5642f804dcb671b Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 20 Nov 2024 15:02:19 -0500
Subject: [PATCH 03/13] Add @jswrenn to reviewers list (#175)

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 .github/pull_requests.toml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml
index d5d88e0b9fca5..a83cebe76609e 100644
--- a/.github/pull_requests.toml
+++ b/.github/pull_requests.toml
@@ -15,5 +15,6 @@ members = [
     "carolynzech",
     "robdockins",
     "HuStmpHrrr",
-    "Eh2406"
+    "Eh2406",
+    "jswrenn"
 ]

From 406b1c196a08c69444351721a41bc73922f48c9b Mon Sep 17 00:00:00 2001
From: Bhuwan Pandit <bhuwanpandit109@gmail.com>
Date: Fri, 22 Nov 2024 15:27:06 +0000
Subject: [PATCH 04/13] docs(0005): typo fix in the challenge docs (#178)

This PR, just fixes a typo for a function name in the challenge docs.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 doc/src/challenges/0005-linked-list.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md
index a5c931712025a..0215bbd029714 100644
--- a/doc/src/challenges/0005-linked-list.md
+++ b/doc/src/challenges/0005-linked-list.md
@@ -23,7 +23,7 @@ The memory safety of the following public functions that iterating over the inte
 
 | Function | Location |
 |---------|---------|
-|clearn | alloc::collections::linked_list |
+|clear| alloc::collections::linked_list |
 |contains| alloc::collections::linked_list |
 |split_off| alloc::collections::linked_list |
 |remove| alloc::collections::linked_list |

From e2db4357df2f596d0fe96b0ba3c9afc01c7a67f7 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 22 Nov 2024 10:21:46 -0800
Subject: [PATCH 05/13] Add reward information to the repository and challenges
 (#176)

I also postponed the end date of all challenges, and fixed the date
format.

Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
---
 README.md                                     | 19 +++++++++----------
 doc/src/challenge_template.md                 |  6 ++++--
 doc/src/challenges/0001-core-transmutation.md |  5 +++--
 doc/src/challenges/0002-intrinsics-memory.md  |  5 +++--
 .../challenges/0003-pointer-arithmentic.md    |  6 +++---
 doc/src/challenges/0004-btree-node.md         |  5 +++--
 doc/src/challenges/0005-linked-list.md        |  5 +++--
 doc/src/challenges/0006-nonnull.md            |  5 +++--
 doc/src/challenges/0007-atomic-types.md       |  5 +++--
 doc/src/challenges/0008-smallsort.md          |  5 +++--
 doc/src/challenges/0009-duration.md           |  5 +++--
 doc/src/challenges/0010-string.md             |  5 +++--
 doc/src/challenges/0011-floats-ints.md        |  5 +++--
 doc/src/challenges/0012-nonzero.md            |  5 +++--
 doc/src/challenges/0013-cstr.md               |  5 +++--
 doc/src/intro.md                              | 14 ++++++++++++--
 16 files changed, 64 insertions(+), 41 deletions(-)

diff --git a/README.md b/README.md
index 41cf22c3a7c7a..2417adde4e446 100644
--- a/README.md
+++ b/README.md
@@ -7,7 +7,7 @@
 This repository is a fork of the official Rust programming
 language repository, created solely to verify the Rust standard
 library. It should not be used as an alternative to the official
-Rust releases. The repository is tool agnostic and welcomes the addition of 
+Rust releases. The repository is tool agnostic and welcomes the addition of
 new tools.
 
 The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
@@ -15,16 +15,15 @@ The goal is to have a verified [Rust standard library](https://doc.rust-lang.org
 2. Creating new techniques to perform scalable verification
 3. Apply techniques to verify previously unverified parts of the standard library.
 
-## [Kani](https://github.com/model-checking/kani)
+For that we are launching a contest that includes a series of challenges that focus on verifying
+memory safety and a subset of undefined behaviors in the Rust standard library.
+Each challenge describes the goal, the success criteria, and whether it has a financial award to be awarded upon its
+successful completion.
 
-The Kani Rust Verifier is a bit-precise model checker for Rust.
-Kani verifies:
-* Memory safety (e.g., null pointer dereferences)
-* User-specified assertions (i.e `assert!(...)`)
-* The absence of panics (eg., `unwrap()` on `None` values)
-* The absence of some types of unexpected behavior (e.g., arithmetic overflows).
+See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules
+and the list of existing challenges.
 
-You can find out more about Kani from the [Kani book](https://model-checking.github.io/kani/) or the [Kani repository on Github](https://github.com/model-checking/kani).
+We welcome everyone to participate!
 
 ## Contact
 
@@ -40,7 +39,7 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more
 Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
 See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details.
 
-## Rust
+### Rust
 Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
 
 See [the Rust repository](https://github.com/rust-lang/rust) for details.
diff --git a/doc/src/challenge_template.md b/doc/src/challenge_template.md
index 50461e2a4e7c4..a39fad01050f1 100644
--- a/doc/src/challenge_template.md
+++ b/doc/src/challenge_template.md
@@ -3,8 +3,9 @@
 - **Status:** *One of the following: \[Open | Resolved | Expired\]*
 - **Solution:** *Option field to point to the PR that solved this challenge.*
 - **Tracking Issue:** *Link to issue*
-- **Start date:** *YY/MM/DD*
-- **End date:** *YY/MM/DD*
+- **Start date:** *YYYY/MM/DD*
+- **End date:** *YYYY/MM/DD*
+- **Reward:** *TBD*[^reward]
 
 -------------------
 
@@ -49,3 +50,4 @@ Note: All solutions to verification challenges need to satisfy the criteria esta
 in addition to the ones listed above.
 
 [^challenge_id]: The number of the challenge sorted by publication date.
+[^reward]: Leave it as TBD when creating a new challenge. This should only be filled by the reward committee.
diff --git a/doc/src/challenges/0001-core-transmutation.md b/doc/src/challenges/0001-core-transmutation.md
index 2b53256b3c34e..66352a0ecb273 100644
--- a/doc/src/challenges/0001-core-transmutation.md
+++ b/doc/src/challenges/0001-core-transmutation.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
-- **Start date:** 2024-06-12
-- **End date:** 2024-12-10
+- **Start date:** *2024/06/12*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md
index 185e04e5a3e2a..31c1c43225250 100644
--- a/doc/src/challenges/0002-intrinsics-memory.md
+++ b/doc/src/challenges/0002-intrinsics-memory.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
-- **Start date:** *24/06/12*
-- **End date:** *24/12/10*
+- **Start date:** *2024/06/12*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md
index 5362983ffe0f3..902d3a7f55752 100644
--- a/doc/src/challenges/0003-pointer-arithmentic.md
+++ b/doc/src/challenges/0003-pointer-arithmentic.md
@@ -1,10 +1,10 @@
 # Challenge 3: Verifying Raw Pointer Arithmetic Operations
 
 - **Status:** Open
-- **Solution:**
 - **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76)
-- **Start date:** 24/06/24
-- **End date:** 24/12/10
+- **Start date:** *2024/06/24*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md
index 835d71365292f..838d9199b400b 100644
--- a/doc/src/challenges/0004-btree-node.md
+++ b/doc/src/challenges/0004-btree-node.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77)
-- **Start date:** *2024-07-01*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/07/01*
+- **End date:** *2025/04/10*
+- **Reward:** *10,000 USD*
 
 -------------------
 
diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md
index 0215bbd029714..b10d6e743cf14 100644
--- a/doc/src/challenges/0005-linked-list.md
+++ b/doc/src/challenges/0005-linked-list.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
-- **Start date:** *24/07/01*
-- **End date:** *24/12/10*
+- **Start date:** *2024/07/01*
+- **End date:** *2025/04/10*
+- **Reward:** *5,000 USD*
 
 -------------------
 
diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md
index 923e00427ad62..86cb8366a36a2 100644
--- a/doc/src/challenges/0006-nonnull.md
+++ b/doc/src/challenges/0006-nonnull.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
-- **Start date:** *2024-08-16*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/16*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md
index 69bff582f7751..eecaf24f5b37e 100644
--- a/doc/src/challenges/0007-atomic-types.md
+++ b/doc/src/challenges/0007-atomic-types.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83)
-- **Start date:** *2024-10-30*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/10/30*
+- **End date:** *2025/04/10*
+- **Reward:** *10,000 USD*
 
 -------------------
 
diff --git a/doc/src/challenges/0008-smallsort.md b/doc/src/challenges/0008-smallsort.md
index c6632af9af837..1052031506517 100644
--- a/doc/src/challenges/0008-smallsort.md
+++ b/doc/src/challenges/0008-smallsort.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56)
-- **Start date:** *2024-08-17*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/17*
+- **End date:** *2025/04/10*
+- **Reward:** *10,000 USD*
 
 -------------------
 
diff --git a/doc/src/challenges/0009-duration.md b/doc/src/challenges/0009-duration.md
index e2af60ec6c1bb..674c296b3742b 100644
--- a/doc/src/challenges/0009-duration.md
+++ b/doc/src/challenges/0009-duration.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#72](https://github.com/model-checking/verify-rust-std/issues/72)
-- **Start date:** *2024-08-20*
-- **End date:** *2024-12-20*
+- **Start date:** *2024/08/20*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md
index 4783841bee429..8d884f34a55c7 100644
--- a/doc/src/challenges/0010-string.md
+++ b/doc/src/challenges/0010-string.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#61](https://github.com/model-checking/verify-rust-std/issues/61)
-- **Start date:** *2024-08-19*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/19*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md
index 9dde411c527ca..1a1c872b88f1f 100644
--- a/doc/src/challenges/0011-floats-ints.md
+++ b/doc/src/challenges/0011-floats-ints.md
@@ -3,8 +3,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59)
-- **Start date:** *2024-08-20*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/20*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md
index 15d2abbb8eb3c..d5252cd939da7 100644
--- a/doc/src/challenges/0012-nonzero.md
+++ b/doc/src/challenges/0012-nonzero.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71)
-- **Start date:** *2024-08-23*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/23*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md
index ff6048701e50f..bb0a20808ebd2 100644
--- a/doc/src/challenges/0013-cstr.md
+++ b/doc/src/challenges/0013-cstr.md
@@ -3,8 +3,9 @@
 - **Status:** Open
 - **Solution:**
 - **Tracking Issue:** [#150](https://github.com/model-checking/verify-rust-std/issues/150)
-- **Start date:** 2024/11/04
-- **End date:** 2025/01/31
+- **Start date:** *2024/11/04*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 ## Goal
diff --git a/doc/src/intro.md b/doc/src/intro.md
index 441d339dcf72d..47e50a97a2ae6 100644
--- a/doc/src/intro.md
+++ b/doc/src/intro.md
@@ -6,12 +6,22 @@ library](https://doc.rust-lang.org/std/). The goal of this is
 to provide automated verification that can be used to verify that a
 given Rust standard library implementation is safe.
 
+Verifying the Rust libraries is difficult because:
+1. Lack of a specification,
+2. Lack of an existing verification mechanism in the Rust ecosystem,
+3. The large size of the verification problem,
+4. The unknowns of scalable verification.
+
+Given the magnitude and scope of the effort, we believe this should be a community owned effort.
+For that, we are launching a contest that includes a series of challenges that focus on verifying
+memory safety and a subset of undefined behaviors in the Rust standard library.
+
 Efforts are largely classified in the following areas:
 
 1. Contributing to the core mechanism of verifying the rust standard library
 2. Creating new techniques to perform scalable verification
 3. Apply techniques to verify previously unverified parts of the standard library.
 
+There is a financial award tied to each challenge per its specification, which is awarded upon its successful completion.
 
-We encourage everyone to watch this repository to be notified of any
-changes.
\ No newline at end of file
+We encourage everyone to watch this repository to be notified of any changes.
\ No newline at end of file

From 4c86400ea7d9f606c7f1da1e0943f16d1542a635 Mon Sep 17 00:00:00 2001
From: stogaru <143449212+stogaru@users.noreply.github.com>
Date: Fri, 22 Nov 2024 12:23:43 -0800
Subject: [PATCH 06/13] Contract and Harnesses for `<*const T>::offset_from`
 (#154)

Towards #76

### Changes

* Adds contracts for `<*const T>::offset_from`.
* Adds harnesses for the function verifying:
    * All integer types
    * Tuples (composite types)
    * Unit Type
* Accomplishes this using a macro.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Carolyn Zech <cmzech@amazon.com>
---
 library/core/src/ptr/const_ptr.rs | 160 ++++++++++++++++++++++++++++++
 1 file changed, 160 insertions(+)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index 57a7c0fc0925c..c7f762dabe3d3 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less};
 use crate::intrinsics::const_eval_select;
 use crate::mem::SizedTypeProperties;
 use crate::slice::{self, SliceIndex};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
 
 impl<T: ?Sized> *const T {
     /// Returns `true` if the pointer is null.
@@ -667,6 +671,16 @@ impl<T: ?Sized> *const T {
     #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")]
     #[inline]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // Ensures subtracting `origin` from `self` doesn't overflow
+        (self as isize).checked_sub(origin as isize).is_some() &&
+        // Ensure the distance between `self` and `origin` is aligned to `T`
+        (self as isize - origin as isize) % (mem::size_of::<T>() as isize) == 0 &&
+        // Ensure both pointers are in the same allocation or are pointing to the same address
+        (self as isize == origin as isize || kani::mem::same_allocation(self, origin))
+    )]
+    // The result should equal the distance in terms of elements of type `T` as per the documentation above
+    #[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::<T>() as isize))]
     pub const unsafe fn offset_from(self, origin: *const T) -> isize
     where
         T: Sized,
@@ -1899,3 +1913,149 @@ impl<T: ?Sized> PartialOrd for *const T {
         *self >= *other
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use crate::kani;
+    use core::mem;
+    use kani::PointerGenerator;
+
+    // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0
+    #[kani::proof_for_contract(<*const ()>::offset_from)]
+    #[kani::should_panic]
+    pub fn check_const_offset_from_unit() {
+        let val: () = ();
+        let src_ptr: *const () = &val;
+        let dest_ptr: *const () = &val;
+        unsafe {
+            dest_ptr.offset_from(src_ptr);
+        }
+    }
+
+    // Array size bound for kani::any_array
+    const ARRAY_LEN: usize = 40;
+
+    macro_rules! generate_offset_from_harness {
+        ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
+            // Proof for a single element
+            #[kani::proof_for_contract(<*const $type>::offset_from)]
+            pub fn $proof_name1() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<gen_size>::new();
+                let mut generator2 = PointerGenerator::<gen_size>::new();
+                let ptr1: *const $type = generator1.any_in_bounds().ptr;
+                let ptr2: *const $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.offset_from(ptr2);
+                }
+            }
+
+            // Proof for large arrays
+            #[kani::proof_for_contract(<*const $type>::offset_from)]
+            pub fn $proof_name2() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let ptr1: *const $type = generator1.any_in_bounds().ptr;
+                let ptr2: *const $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.offset_from(ptr2);
+                }
+            }
+        };
+    }
+
+    generate_offset_from_harness!(
+        u8,
+        check_const_offset_from_u8,
+        check_const_offset_from_u8_arr
+    );
+    generate_offset_from_harness!(
+        u16,
+        check_const_offset_from_u16,
+        check_const_offset_from_u16_arr
+    );
+    generate_offset_from_harness!(
+        u32,
+        check_const_offset_from_u32,
+        check_const_offset_from_u32_arr
+    );
+    generate_offset_from_harness!(
+        u64,
+        check_const_offset_from_u64,
+        check_const_offset_from_u64_arr
+    );
+    generate_offset_from_harness!(
+        u128,
+        check_const_offset_from_u128,
+        check_const_offset_from_u128_arr
+    );
+    generate_offset_from_harness!(
+        usize,
+        check_const_offset_from_usize,
+        check_const_offset_from_usize_arr
+    );
+
+    generate_offset_from_harness!(
+        i8,
+        check_const_offset_from_i8,
+        check_const_offset_from_i8_arr
+    );
+    generate_offset_from_harness!(
+        i16,
+        check_const_offset_from_i16,
+        check_const_offset_from_i16_arr
+    );
+    generate_offset_from_harness!(
+        i32,
+        check_const_offset_from_i32,
+        check_const_offset_from_i32_arr
+    );
+    generate_offset_from_harness!(
+        i64,
+        check_const_offset_from_i64,
+        check_const_offset_from_i64_arr
+    );
+    generate_offset_from_harness!(
+        i128,
+        check_const_offset_from_i128,
+        check_const_offset_from_i128_arr
+    );
+    generate_offset_from_harness!(
+        isize,
+        check_const_offset_from_isize,
+        check_const_offset_from_isize_arr
+    );
+
+    generate_offset_from_harness!(
+        (i8, i8),
+        check_const_offset_from_tuple_1,
+        check_const_offset_from_tuple_1_arr
+    );
+    generate_offset_from_harness!(
+        (f64, bool),
+        check_const_offset_from_tuple_2,
+        check_const_offset_from_tuple_2_arr
+    );
+    generate_offset_from_harness!(
+        (u32, i16, f32),
+        check_const_offset_from_tuple_3,
+        check_const_offset_from_tuple_3_arr
+    );
+    generate_offset_from_harness!(
+        ((), bool, u8, u16, i32, f64, i128, usize),
+        check_const_offset_from_tuple_4,
+        check_const_offset_from_tuple_4_arr
+    );
+}

From b81906d2bb53c5a8c2a78ec6b1e8c99ac6177a33 Mon Sep 17 00:00:00 2001
From: Eli Gancena <eligancena@gmail.com>
Date: Sat, 23 Nov 2024 17:17:22 -0400
Subject: [PATCH 07/13] Update tool_template.md (#183)

Typo

pr fixes typo found in verification tool template

Resolves #NA

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 doc/src/tool_template.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/src/tool_template.md b/doc/src/tool_template.md
index 5e7b054ed6891..c5d56b97b80d5 100644
--- a/doc/src/tool_template.md
+++ b/doc/src/tool_template.md
@@ -25,7 +25,7 @@ _Please list the license(s) that are used by your tool, and if to your knowledge
 3. \[and so on...\]
 
 ## Artifacts
-_If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._
+_If there are noteworthy examples of using the tool to perform verification, please include them in this section.Links, papers, etc._
 
 ## CI & Versioning
 _Please describe how you version the tool and how it will be supported in CI pipelines._

From 5e44e6e86a021633d20b610ea76574a11a7e95e7 Mon Sep 17 00:00:00 2001
From: JY <53210261+Jimmycreative@users.noreply.github.com>
Date: Mon, 25 Nov 2024 08:56:41 -0800
Subject: [PATCH 08/13] Contracts & Harnesses for len, is_empty, is_aligned,
 and is_aligned_to (#128)

Changes
added contract and harness for len, is_empty, is_aligned, and
is_aligned_to in the non-null library.

```
Complete - 4 successfully verified harnesses, 0 failures, 4 total.
```

---------

Co-authored-by: Carolyn Zech <cmzech@amazon.com>
---
 library/core/src/ptr/non_null.rs | 77 ++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)

diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index 4834c8009ec44..aa224db211933 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -1387,6 +1387,7 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[stable(feature = "pointer_is_aligned", since = "1.79.0")]
     #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")]
+    #[ensures(|result: &bool| *result == (self.as_ptr().addr() % core::mem::align_of::<T>() == 0))]
     pub const fn is_aligned(self) -> bool
     where
         T: Sized,
@@ -1502,6 +1503,8 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[unstable(feature = "pointer_is_aligned_to", issue = "96284")]
     #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")]
+    #[requires(align.is_power_of_two())]
+    #[ensures(|result: &bool| *result == (self.as_ptr().addr() % align == 0))] // Ensure the returned value is correct based on the given alignment
     pub const fn is_aligned_to(self, align: usize) -> bool {
         self.pointer.is_aligned_to(align)
     }
@@ -1881,6 +1884,14 @@ mod verify {
     use crate::ptr::null_mut;
     use kani::PointerGenerator;
 
+    impl<T> kani::Arbitrary for NonNull<T> {
+        fn any() -> Self {
+            let ptr: *mut T = kani::any::<usize>() as *mut T;
+            kani::assume(!ptr.is_null());
+            NonNull::new(ptr).expect("Non-null pointer expected")
+        }
+    }
+
     // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
     #[kani::proof_for_contract(NonNull::new_unchecked)]
     pub fn non_null_check_new_unchecked() {
@@ -2179,4 +2190,70 @@ mod verify {
             assert_eq!(old_b, new_a);
         }
     }
+
+    #[kani::proof]
+    pub fn non_null_check_len() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i8> = kani::any();
+        // Create a non-deterministic size using kani::any()
+        let size: usize = kani::any();
+        // Create a NonNull slice from the non-null pointer and size
+        let non_null_slice: NonNull<[i8]> = NonNull::slice_from_raw_parts(non_null_ptr, size);
+
+        // Perform the length check
+        let len = non_null_slice.len();
+        assert!(len == size);
+    }
+
+    #[kani::proof]
+    pub fn non_null_check_is_empty() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i8> = kani::any();
+        // Create a non-deterministic size using kani::any(), constrained to zero
+        let size: usize = 0;
+
+        // Create a NonNull slice from the non-null pointer and size
+        let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(non_null_ptr, size) };
+
+        // Perform the is_empty check
+        let is_empty = non_null_slice.is_empty();
+        assert!(is_empty);
+    }
+
+    #[kani::proof_for_contract(NonNull::is_aligned)]
+    pub fn non_null_slice_is_aligned_check() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i32> = kani::any();
+
+        // Perform the alignment check
+        let result = non_null_ptr.is_aligned();
+
+    }
+
+    #[kani::proof_for_contract(NonNull::is_aligned_to)]
+    pub fn non_null_check_is_aligned_to() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i32> = kani::any();
+
+        // Create a non-deterministic alignment using kani::any()
+        let align: usize = kani::any();
+        kani::assume(align > 0); // Ensure alignment is greater than zero
+
+        // Perform the alignment check
+        let result = non_null_ptr.is_aligned_to(align);
+            
+    }
+
+    #[kani::proof]
+    #[kani::should_panic] // Add this if we expect a panic when the alignment is invalid
+    pub fn non_null_check_is_aligned_to_no_power_two() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i32> = kani::any();
+
+        // Create a non-deterministic alignment value using kani::any()
+        let align: usize = kani::any();
+
+        // Perform the alignment check
+        let result = non_null_ptr.is_aligned_to(align);
+    }
 }

From 07318dfc34aba23b0e04793cdcd9414629f2b774 Mon Sep 17 00:00:00 2001
From: Qinyuan Wu <53478459+QinyuanWu@users.noreply.github.com>
Date: Mon, 25 Nov 2024 14:18:26 -0800
Subject: [PATCH 09/13] Contracts and harnesses for `dangling`,
 `from_raw_parts`,  `slice_from_raw_parts`, `to_raw_parts` in NonNull (#127)

Towards #53

Contracts and harnesses for `dangling`, `from_raw_parts`,
`slice_from_raw_parts`, `to_raw_parts` in NonNull
### Discussion

1. `NonNull::slice_from_raw_parts`:
[requested](https://github.com/model-checking/kani/issues/3693) new Kani
API to compare byte by byte
2. `NonNull::to_raw_parts`: [unstable vtable comparison
'Eq'](https://github.com/model-checking/verify-rust-std/discussions/139)

### Verification Result
```
SUMMARY:
 ** 0 of 141 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.17378491s

Complete - 6 successfully verified harnesses, 0 failures, 6 total.
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 library/core/src/ptr/non_null.rs | 130 +++++++++++++++++++++++++++++++
 1 file changed, 130 insertions(+)

diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index aa224db211933..915473ee027f0 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -112,6 +112,7 @@ impl<T: Sized> NonNull<T> {
     #[rustc_const_stable(feature = "const_nonnull_dangling", since = "1.36.0")]
     #[must_use]
     #[inline]
+    #[ensures(|result| !result.pointer.is_null() && result.pointer.is_aligned())]
     pub const fn dangling() -> Self {
         // SAFETY: ptr::dangling_mut() returns a non-null well-aligned pointer.
         unsafe {
@@ -269,6 +270,7 @@ impl<T: ?Sized> NonNull<T> {
     #[unstable(feature = "ptr_metadata", issue = "81513")]
     #[rustc_const_unstable(feature = "ptr_metadata", issue = "81513")]
     #[inline]
+    #[ensures(|result| !result.pointer.is_null())]
     pub const fn from_raw_parts(
         data_pointer: NonNull<()>,
         metadata: <T as super::Pointee>::Metadata,
@@ -287,6 +289,8 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use = "this returns the result of the operation, \
                   without modifying the original"]
     #[inline]
+    #[ensures(|(data_ptr, metadata)| !data_ptr.as_ptr().is_null())]
+    #[ensures(|(data_ptr, metadata)| self.as_ptr() as *const () == data_ptr.as_ptr() as *const ())]
     pub const fn to_raw_parts(self) -> (NonNull<()>, <T as super::Pointee>::Metadata) {
         (self.cast(), super::metadata(self.as_ptr()))
     }
@@ -1536,6 +1540,9 @@ impl<T> NonNull<[T]> {
     #[rustc_const_stable(feature = "const_slice_from_raw_parts_mut", since = "1.83.0")]
     #[must_use]
     #[inline]
+    #[ensures(|result| !result.pointer.is_null()
+        && result.pointer as *const T == data.pointer
+        && unsafe { result.as_ref() }.len() == len)]
     pub const fn slice_from_raw_parts(data: NonNull<T>, len: usize) -> Self {
         // SAFETY: `data` is a `NonNull` pointer which is necessarily non-null
         unsafe { Self::new_unchecked(super::slice_from_raw_parts_mut(data.as_ptr(), len)) }
@@ -1884,6 +1891,20 @@ mod verify {
     use crate::ptr::null_mut;
     use kani::PointerGenerator;
 
+    trait SampleTrait {
+        fn get_value(&self) -> i32;
+    }
+
+    struct SampleStruct {
+        value: i32,
+    }
+
+    impl SampleTrait for SampleStruct {
+        fn get_value(&self) -> i32 {
+            self.value
+        }
+    }
+
     impl<T> kani::Arbitrary for NonNull<T> {
         fn any() -> Self {
             let ptr: *mut T = kani::any::<usize>() as *mut T;
@@ -2035,6 +2056,115 @@ mod verify {
         let offset = nonnull_xptr.align_offset(invalid_align);
     }
 
+    // pub const fn dangling() -> Self
+    #[kani::proof_for_contract(NonNull::dangling)]
+    pub fn non_null_check_dangling() {
+        // unsigned integer types
+        let ptr_u8 = NonNull::<u8>::dangling();
+        let ptr_u16 = NonNull::<u16>::dangling();
+        let ptr_u32 = NonNull::<u32>::dangling();
+        let ptr_u64 = NonNull::<u64>::dangling();
+        let ptr_u128 = NonNull::<u128>::dangling();
+        let ptr_usize = NonNull::<usize>::dangling();
+        // signed integer types
+        let ptr_i8 = NonNull::<i8>::dangling();
+        let ptr_i16 = NonNull::<i16>::dangling();
+        let ptr_i32 = NonNull::<i32>::dangling();
+        let ptr_i64 = NonNull::<i64>::dangling();
+        let ptr_i128 = NonNull::<i128>::dangling();
+        let ptr_isize = NonNull::<isize>::dangling();
+        // unit type
+        let ptr_unit = NonNull::<()>::dangling();
+        // zero length slice from dangling unit pointer
+        let zero_len_slice =  NonNull::slice_from_raw_parts(ptr_unit, 0);
+    }
+
+    // pub const fn from_raw_parts(data_pointer: NonNull<()>, metadata: <T as super::Pointee>::Metadata,) -> NonNull<T>
+    #[kani::proof_for_contract(NonNull::from_raw_parts)]
+    #[kani::unwind(101)]
+    pub fn non_null_check_from_raw_parts() {
+        const ARR_LEN: usize = 100;
+        // Create a non-deterministic array and its slice
+        let arr: [i8; ARR_LEN] = kani::any();
+        let arr_slice = kani::slice::any_slice_of_array(&arr);
+        // Get a raw NonNull pointer to the start of the slice
+        let arr_slice_raw_ptr = NonNull::new(arr_slice.as_ptr() as *mut ()).unwrap();
+        // Create NonNull pointer from the start pointer and the length of the slice
+        let nonnull_slice = NonNull::<[i8]>::from_raw_parts(arr_slice_raw_ptr, arr_slice.len());
+        // Ensure slice content is preserved, runtime at this step is proportional to ARR_LEN
+        unsafe {
+            kani::assert(arr_slice == nonnull_slice.as_ref(), "slice content must be preserve");
+        }
+
+        // zero-length dangling pointer example
+        let dangling_ptr = NonNull::<()>::dangling();
+        let zero_length = NonNull::<[()]>::from_raw_parts(dangling_ptr, 0);
+    }
+
+    #[kani::proof_for_contract(NonNull::from_raw_parts)]
+    pub fn non_null_check_from_raw_part_trait() {
+        // Create a SampleTrait object from SampleStruct
+        let sample_struct = SampleStruct { value: kani::any() };
+        let trait_object: &dyn SampleTrait = &sample_struct;
+
+        // Get the raw data pointer and metadata for the trait object
+        let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap();
+        // Safety: For trait objects, the metadata must come from a pointer to the same underlying erased type
+        let metadata = core::ptr::metadata(trait_object);
+
+        // Create NonNull<dyn MyTrait> from the data pointer and metadata
+        let nonnull_trait_object: NonNull<dyn SampleTrait> = NonNull::from_raw_parts(trait_ptr, metadata);
+
+        unsafe {
+            // Ensure trait method and member is preserved
+            kani::assert( trait_object.get_value() == nonnull_trait_object.as_ref().get_value(), "trait method and member must correctly preserve");
+        }
+    }
+
+    // pub const fn slice_from_raw_parts(data: NonNull<T>, len: usize) -> Self
+    #[kani::proof_for_contract(NonNull::slice_from_raw_parts)]
+    #[kani::unwind(1001)]
+    pub fn non_null_check_slice_from_raw_parts() {
+        const ARR_LEN: usize = 1000;
+        // Create a non-deterministic array
+        let mut arr: [i8; ARR_LEN] = kani::any();
+        // Get a raw NonNull pointer to the start of the slice
+        let arr_raw_ptr = NonNull::new(arr.as_mut_ptr()).unwrap();
+        // Create NonNull slice from the start pointer and ends at random slice_len
+        // Safety: https://doc.rust-lang.org/std/slice/fn.from_raw_parts.html
+        let slice_len: usize = kani::any();
+        kani::assume(slice_len <= ARR_LEN);
+        let nonnull_slice = NonNull::<[i8]>::slice_from_raw_parts(arr_raw_ptr, slice_len);
+        // Ensure slice content is preserved, runtime at this step is proportional to ARR_LEN
+        unsafe {
+            kani::assert(&arr[..slice_len] == nonnull_slice.as_ref(), "slice content must be preserve");
+        }
+
+        // TODO: zero-length example blocked by kani issue [#3670](https://github.com/model-checking/kani/issues/3670)
+        //let dangling_ptr = NonNull::<()>::dangling();
+        //let zero_length = NonNull::<[()]>::slice_from_raw_parts(dangling_ptr, 0);
+    }
+
+
+    // pub const fn to_raw_parts(self) -> (NonNull<()>, <T as super::Pointee>::Metadata)
+    #[kani::proof_for_contract(NonNull::to_raw_parts)]
+    pub fn non_null_check_to_raw_parts() {
+        // Create a SampleTrait object from SampleStruct
+        let sample_struct = SampleStruct { value: kani::any() };
+        let trait_object: &dyn SampleTrait = &sample_struct;
+
+        // Get the raw data pointer and metadata for the trait object
+        let trait_ptr = NonNull::from(trait_object).cast::<()>(); //both have eq failure
+        //let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap(); //Question: what's the difference
+        // Safety: For trait objects, the metadata must come from a pointer to the same underlying erased type
+        let metadata = core::ptr::metadata(trait_object);
+
+        // Create NonNull<dyn MyTrait> from the data pointer and metadata
+        let nonnull_trait_object: NonNull<dyn SampleTrait> = NonNull::from_raw_parts(trait_ptr, metadata);
+        let (decomposed_data_ptr, decomposed_metadata) = NonNull::to_raw_parts(nonnull_trait_object);
+    }
+
+
     #[kani::proof_for_contract(NonNull::as_mut)]
     pub fn non_null_check_as_mut() {
         let mut x: i32 = kani::any();

From 82da845a15dbffa36dc08f755cc0d0b4d5212b0f Mon Sep 17 00:00:00 2001
From: Yenyun035 <57857379+Yenyun035@users.noreply.github.com>
Date: Mon, 25 Nov 2024 17:46:39 -0800
Subject: [PATCH 10/13] CStr Safety invariant & Harnesses for
 `from_bytes_until_nul` (#180)

Towards #150

### Changes
* Added a `CStr` Safety Invariant
* Added a harness for `from_bytes_until_nul`, the harness covers:
    * The input slice contains a single null byte at the end;
    * The input slice contains no null bytes;
    * The input slice contains intermediate null bytes

### Discussion
* [Safety invariant
implementation](https://github.com/model-checking/verify-rust-std/issues/150#issuecomment-2492853570)
* [Input array
generation](https://github.com/model-checking/verify-rust-std/discussions/181)

### Verification Result
`./scripts/run-kani.sh --kani-args --harness ffi::c_str::verify`

```
// array size 16
Checking harness ffi::c_str::verify::check_from_bytes_until_nul...

VERIFICATION RESULT:
 ** 0 of 140 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 7.3023376s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 library/core/src/ffi/c_str.rs | 43 +++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs
index 93dd351b02958..2a65b2415f7d3 100644
--- a/library/core/src/ffi/c_str.rs
+++ b/library/core/src/ffi/c_str.rs
@@ -9,6 +9,11 @@ use crate::ptr::NonNull;
 use crate::slice::memchr;
 use crate::{fmt, intrinsics, ops, slice, str};
 
+use crate::ub_checks::Invariant;
+
+#[cfg(kani)]
+use crate::kani;
+
 // FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link
 //   depends on where the item is being documented. however, since this is libcore, we can't
 //   actually reference libstd or liballoc in intra-doc links. so, the best we can do is remove the
@@ -207,6 +212,22 @@ impl fmt::Display for FromBytesWithNulError {
     }
 }
 
+#[unstable(feature = "ub_checks", issue = "none")]
+impl Invariant for &CStr {
+    /**
+     * Safety invariant of a valid CStr:
+     * 1. An empty CStr should have a null byte.
+     * 2. A valid CStr should end with a null-terminator and contains
+     *    no intermediate null bytes.
+     */
+    fn is_safe(&self) -> bool {
+        let bytes: &[c_char] = &self.inner;
+        let len = bytes.len();
+
+        !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0)
+    }
+}
+
 impl CStr {
     /// Wraps a raw C string with a safe C string wrapper.
     ///
@@ -833,3 +854,25 @@ impl Iterator for Bytes<'_> {
 
 #[unstable(feature = "cstr_bytes", issue = "112115")]
 impl FusedIterator for Bytes<'_> {}
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError>
+    #[kani::proof]
+    #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32
+    fn check_from_bytes_until_nul() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        // Covers the case of a single null byte at the end, no null bytes, as
+        // well as intermediate null bytes
+        let slice = kani::slice::any_slice_of_array(&string);
+
+        let result = CStr::from_bytes_until_nul(slice);
+        if let Ok(c_str) = result {
+            assert!(c_str.is_safe());
+        }
+    }
+}
\ No newline at end of file

From 688b15bfa092fe3f56c8b71596845192a41469a9 Mon Sep 17 00:00:00 2001
From: JY <53210261+Jimmycreative@users.noreply.github.com>
Date: Tue, 26 Nov 2024 20:30:26 -0800
Subject: [PATCH 11/13] Contracts & Harnesses for `non_null::sub` and
 `non_null::sub_ptr` and `non_null::offset_from` (#93)

Towards https://github.com/model-checking/verify-rust-std/issues/53

Changes
added contract and harness for non_null::sub
added contract and harness for non_null::sub_ptr

Revalidation
To revalidate the verification results, run kani verify-std -Z
unstable-options "path/to/library" -Z function-contracts -Z
mem-predicates --harness ptr::non_null::verify This will run both
harnesses. All default checks should pass:

```
SUMMARY:
 ** 0 of 1622 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.3814842s

SUMMARY:
 ** 0 of 1780 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 0.44192737s

Complete - 2 successfully verified harnesses, 0 failures, 2 total.
```

### Clarifying Questions
The proof now only handles the array with a fixed size and uses a random
element in the arr for subtraction. The element is i32 type. Is this ok
for the current stage? Or maybe we need to consider other types such as
i64, etc and maybe change the arr to a bigger size?

---------

Co-authored-by: OwO <owo@OwOs-MacBook-Pro.local>
Co-authored-by: Qinyuan Wu <qinyuanw@andrew.cmu.edu>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
---
 library/core/src/ptr/non_null.rs | 87 ++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)

diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index 915473ee027f0..42ea9d75896d3 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -665,6 +665,12 @@ impl<T: ?Sized> NonNull<T> {
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
     #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))]
+    #[requires(
+        count.checked_mul(core::mem::size_of::<T>()).is_some() &&
+        count * core::mem::size_of::<T>() <= isize::MAX as usize && 
+        kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_sub(count))
+    )]
+    #[ensures(|result: &NonNull<T>| result.as_ptr() == self.as_ptr().offset(-(count as isize)))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -794,6 +800,11 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[requires( 
+        (kani::mem::same_allocation(self.as_ptr(), origin.as_ptr()) && 
+        ((self.as_ptr().addr() - origin.as_ptr().addr()) % core::mem::size_of::<T>() == 0))
+    )] // Ensure both pointers meet safety conditions for offset_from
+    #[ensures(|result: &isize| *result == (self.as_ptr() as isize - origin.as_ptr() as isize) / core::mem::size_of::<T>() as isize)]
     pub const unsafe fn offset_from(self, origin: NonNull<T>) -> isize
     where
         T: Sized,
@@ -887,6 +898,13 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[unstable(feature = "ptr_sub_ptr", issue = "95892")]
     #[rustc_const_unstable(feature = "const_ptr_sub_ptr", issue = "95892")]
+    #[requires(
+        self.as_ptr().addr().checked_sub(subtracted.as_ptr().addr()).is_some() &&
+        kani::mem::same_allocation(self.as_ptr(), subtracted.as_ptr()) &&
+        (self.as_ptr().addr()) >= (subtracted.as_ptr().addr()) &&
+        (self.as_ptr().addr() - subtracted.as_ptr().addr()) % core::mem::size_of::<T>() == 0
+    )]
+    #[ensures(|result: &usize| *result == self.as_ptr().offset_from(subtracted.as_ptr()) as usize)]
     pub const unsafe fn sub_ptr(self, subtracted: NonNull<T>) -> usize
     where
         T: Sized,
@@ -2386,4 +2404,73 @@ mod verify {
         // Perform the alignment check
         let result = non_null_ptr.is_aligned_to(align);
     }
+
+    #[kani::proof_for_contract(NonNull::sub)]
+    pub fn non_null_check_sub() {
+        const SIZE: usize = 10000;
+        let mut generator = kani::PointerGenerator::<SIZE>::new();
+        // Get a raw pointer from the generator within bounds
+        let raw_ptr: *mut i32 = generator.any_in_bounds().ptr;
+        // Create a non-null pointer from the raw pointer
+        let ptr = unsafe { NonNull::new(raw_ptr).unwrap() };
+        // Create a non-deterministic count value
+        let count: usize = kani::any();
+
+        unsafe {
+            let result = ptr.sub(count);
+        }
+    }
+    
+    #[kani::proof_for_contract(NonNull::sub_ptr)]
+    pub fn non_null_check_sub_ptr() {
+        const SIZE: usize = core::mem::size_of::<i32>() * 1000;
+        let mut generator1 = kani::PointerGenerator::<SIZE>::new();
+        let mut generator2 = kani::PointerGenerator::<SIZE>::new();
+
+        let ptr: *mut i32 = if kani::any() {
+            generator1.any_in_bounds().ptr as *mut i32
+        } else {
+            generator2.any_in_bounds().ptr as *mut i32
+        };
+
+        let origin: *mut i32 = if kani::any() {
+            generator1.any_in_bounds().ptr as *mut i32
+        } else {
+            generator2.any_in_bounds().ptr as *mut i32
+        };
+
+        let ptr_nonnull = unsafe { NonNull::new(ptr).unwrap() };
+        let origin_nonnull = unsafe { NonNull::new(origin).unwrap() };
+
+        unsafe {
+            let distance = ptr_nonnull.sub_ptr(origin_nonnull);
+        }
+    }
+
+    #[kani::proof_for_contract(NonNull::offset_from)]
+    #[kani::should_panic]
+    pub fn non_null_check_offset_from() {
+        const SIZE: usize = core::mem::size_of::<i32>() * 1000;
+        let mut generator1 = kani::PointerGenerator::<SIZE>::new();
+        let mut generator2 = kani::PointerGenerator::<SIZE>::new();
+
+        let ptr: *mut i32 = if kani::any() {
+            generator1.any_in_bounds().ptr as *mut i32
+        } else {
+            generator2.any_in_bounds().ptr as *mut i32
+        };
+
+        let origin: *mut i32 = if kani::any() {
+            generator1.any_in_bounds().ptr as *mut i32
+        } else {
+            generator2.any_in_bounds().ptr as *mut i32
+        };
+
+        let ptr_nonnull = unsafe { NonNull::new(ptr).unwrap() };
+        let origin_nonnull = unsafe { NonNull::new(origin).unwrap() };
+
+        unsafe {
+            let distance = ptr_nonnull.offset_from(origin_nonnull);
+        }
+    }
 }

From 716c6af923e1d2daf14aa437483a30af772c9afa Mon Sep 17 00:00:00 2001
From: rahulku <luhark@amazon.com>
Date: Wed, 27 Nov 2024 09:27:12 -0800
Subject: [PATCH 12/13] Add two more reviewers (#190)

Add two more reviewers to our list.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 .github/pull_requests.toml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml
index a83cebe76609e..6c11ebfeb3691 100644
--- a/.github/pull_requests.toml
+++ b/.github/pull_requests.toml
@@ -16,5 +16,7 @@ members = [
     "robdockins",
     "HuStmpHrrr",
     "Eh2406",
-    "jswrenn"
+    "jswrenn",
+    "havelund",
+    "jorajeev"
 ]

From 014965a3b54c056d8cd1d08e3aebc5d5c61356b9 Mon Sep 17 00:00:00 2001
From: stogaru <143449212+stogaru@users.noreply.github.com>
Date: Wed, 27 Nov 2024 13:55:57 -0800
Subject: [PATCH 13/13] Contracts and Harnesses for `<*mut T>::add`, `sub` and
 `offset` (#113)

Towards #76

### Changes
* Adds contracts for `<*mut T>::add`, `<*mut T>::sub` and `<*mut
T>::offset`
* Adds proofs for contracts of the above functions verifying the pointee
types:
  * All integer types
  * Tuples (composite type)
  * Unit Type
* Defines a macro for add and sub and another for offset.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Yifei Wang <1277495324@qq.com>
Co-authored-by: MayureshJoshi25 <jmayuresh25@gmail.com>
Co-authored-by: Yifei Wang <40480373+xsxszab@users.noreply.github.com>
---
 library/core/src/ptr/mut_ptr.rs | 177 ++++++++++++++++++++++++++++++++
 1 file changed, 177 insertions(+)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 7aa6a309a06b5..34ab472735915 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less};
 use crate::intrinsics::const_eval_select;
 use crate::mem::SizedTypeProperties;
 use crate::slice::{self, SliceIndex};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
 
 impl<T: ?Sized> *mut T {
     /// Returns `true` if the pointer is null.
@@ -400,6 +404,22 @@ impl<T: ?Sized> *mut T {
     #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned.
+    // These conditions are not verified as part of the preconditions.
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
+        count.checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
+        // Precondition 2: adding the computed offset to `self` does not cause overflow
+        (self as isize).checked_add((count * core::mem::size_of::<T>() as isize)).is_some() &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_offset(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn offset(self, count: isize) -> *mut T
     where
         T: Sized,
@@ -998,6 +1018,23 @@ impl<T: ?Sized> *mut T {
     #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned.
+    // These conditions are not verified as part of the preconditions.
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
+        count.checked_mul(core::mem::size_of::<T>()).is_some() &&
+        count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+        // Precondition 2: adding the computed offset to `self` does not cause overflow
+        (self as isize).checked_add((count * core::mem::size_of::<T>()) as isize).is_some() &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_add(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1107,6 +1144,23 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned.
+    // These conditions are not verified as part of the preconditions.
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
+        count.checked_mul(core::mem::size_of::<T>()).is_some() &&
+        count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+        // Precondition 2: subtracting the computed offset from `self` does not cause overflow
+        (self as isize).checked_sub((count * core::mem::size_of::<T>()) as isize).is_some() &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_sub(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_sub(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -2302,3 +2356,126 @@ impl<T: ?Sized> PartialOrd for *mut T {
         *self >= *other
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use crate::kani;
+
+    /// This macro generates proofs for contracts on `add`, `sub`, and `offset`
+    /// operations for pointers to integer, composite, and unit types.
+    /// - `$type`: Specifies the pointee type.
+    /// - `$proof_name`: Specifies the name of the generated proof for contract.
+    macro_rules! generate_mut_arithmetic_harness {
+        ($type:ty, $proof_name:ident, add) => {
+            #[kani::proof_for_contract(<*mut $type>::add)]
+            pub fn $proof_name() {
+                // 200 bytes are large enough to cover all pointee types used for testing
+                const BUF_SIZE: usize = 200;
+                let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+                let test_ptr: *mut $type = generator.any_in_bounds().ptr;
+                let count: usize = kani::any();
+                unsafe {
+                    test_ptr.add(count);
+                }
+            }
+        };
+        ($type:ty, $proof_name:ident, sub) => {
+            #[kani::proof_for_contract(<*mut $type>::sub)]
+            pub fn $proof_name() {
+                // 200 bytes are large enough to cover all pointee types used for testing
+                const BUF_SIZE: usize = 200;
+                let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+                let test_ptr: *mut $type = generator.any_in_bounds().ptr;
+                let count: usize = kani::any();
+                unsafe {
+                    test_ptr.sub(count);
+                }
+            }
+        };
+        ($type:ty, $proof_name:ident, offset) => {
+            #[kani::proof_for_contract(<*mut $type>::offset)]
+            pub fn $proof_name() {
+                // 200 bytes are large enough to cover all pointee types used for testing
+                const BUF_SIZE: usize = 200;
+                let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+                let test_ptr: *mut $type = generator.any_in_bounds().ptr;
+                let count: isize = kani::any();
+                unsafe {
+                    test_ptr.offset(count);
+                }
+            }
+        };
+    }
+
+    // <*mut T>:: add() integer types verification
+    generate_mut_arithmetic_harness!(i8, check_mut_add_i8, add);
+    generate_mut_arithmetic_harness!(i16, check_mut_add_i16, add);
+    generate_mut_arithmetic_harness!(i32, check_mut_add_i32, add);
+    generate_mut_arithmetic_harness!(i64, check_mut_add_i64, add);
+    generate_mut_arithmetic_harness!(i128, check_mut_add_i128, add);
+    generate_mut_arithmetic_harness!(isize, check_mut_add_isize, add);
+    // Due to a bug of kani this test case is malfunctioning for now.
+    // Tracking issue: https://github.com/model-checking/kani/issues/3743
+    // generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add);
+    generate_mut_arithmetic_harness!(u16, check_mut_add_u16, add);
+    generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add);
+    generate_mut_arithmetic_harness!(u64, check_mut_add_u64, add);
+    generate_mut_arithmetic_harness!(u128, check_mut_add_u128, add);
+    generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add);
+
+    // <*mut T>:: add() unit type verification
+    generate_mut_arithmetic_harness!((), check_mut_add_unit, add);
+
+    // <*mut T>:: add() composite types verification
+    generate_mut_arithmetic_harness!((i8, i8), check_mut_add_tuple_1, add);
+    generate_mut_arithmetic_harness!((f64, bool), check_mut_add_tuple_2, add);
+    generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_add_tuple_3, add);
+    generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_add_tuple_4, add);
+
+    // <*mut T>:: sub() integer types verification
+    generate_mut_arithmetic_harness!(i8, check_mut_sub_i8, sub);
+    generate_mut_arithmetic_harness!(i16, check_mut_sub_i16, sub);
+    generate_mut_arithmetic_harness!(i32, check_mut_sub_i32, sub);
+    generate_mut_arithmetic_harness!(i64, check_mut_sub_i64, sub);
+    generate_mut_arithmetic_harness!(i128, check_mut_sub_i128, sub);
+    generate_mut_arithmetic_harness!(isize, check_mut_sub_isize, sub);
+    generate_mut_arithmetic_harness!(u8, check_mut_sub_u8, sub);
+    generate_mut_arithmetic_harness!(u16, check_mut_sub_u16, sub);
+    generate_mut_arithmetic_harness!(u32, check_mut_sub_u32, sub);
+    generate_mut_arithmetic_harness!(u64, check_mut_sub_u64, sub);
+    generate_mut_arithmetic_harness!(u128, check_mut_sub_u128, sub);
+    generate_mut_arithmetic_harness!(usize, check_mut_sub_usize, sub);
+
+    // <*mut T>:: sub() unit type verification
+    generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub);
+
+    // <*mut T>:: sub() composite types verification
+    generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub);
+    generate_mut_arithmetic_harness!((f64, bool), check_mut_sub_tuple_2, sub);
+    generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub);
+    generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub);
+
+    // fn <*mut T>::offset() integer types verification
+    generate_mut_arithmetic_harness!(i8, check_mut_offset_i8, offset);
+    generate_mut_arithmetic_harness!(i16, check_mut_offset_i16, offset);
+    generate_mut_arithmetic_harness!(i32, check_mut_offset_i32, offset);
+    generate_mut_arithmetic_harness!(i64, check_mut_offset_i64, offset);
+    generate_mut_arithmetic_harness!(i128, check_mut_offset_i128, offset);
+    generate_mut_arithmetic_harness!(isize, check_mut_offset_isize, offset);
+    generate_mut_arithmetic_harness!(u8, check_mut_offset_u8, offset);
+    generate_mut_arithmetic_harness!(u16, check_mut_offset_u16, offset);
+    generate_mut_arithmetic_harness!(u32, check_mut_offset_u32, offset);
+    generate_mut_arithmetic_harness!(u64, check_mut_offset_u64, offset);
+    generate_mut_arithmetic_harness!(u128, check_mut_offset_u128, offset);
+    generate_mut_arithmetic_harness!(usize, check_mut_offset_usize, offset);
+
+    // fn <*mut T>::offset() unit type verification
+    generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset);
+
+    // fn <*mut T>::offset() composite type verification
+    generate_mut_arithmetic_harness!((i8, i8), check_mut_offset_tuple_1, offset);
+    generate_mut_arithmetic_harness!((f64, bool), check_mut_offset_tuple_2, offset);
+    generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_offset_tuple_3, offset);
+    generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_offset_tuple_4, offset);
+}