From 78b3c28fae94164b73cd1773066959b234d32812 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Wed, 28 Aug 2024 20:51:32 +0000
Subject: [PATCH 01/23] Add command to run Kani from the root and from CI w/
 cache

---
 .gitignore                        |   2 +
 doc/book.toml                     |   1 +
 kani-version.toml                 |   6 ++
 run-kani.sh                       | 172 ++++++++++++++++++++++++++++++
 scripts/run_update_with_checks.sh |  44 ++++----
 5 files changed, 203 insertions(+), 22 deletions(-)
 create mode 100644 kani-version.toml
 create mode 100755 run-kani.sh

diff --git a/.gitignore b/.gitignore
index 367d4db4df2f7..9eb2bba2d7422 100644
--- a/.gitignore
+++ b/.gitignore
@@ -19,7 +19,9 @@ Session.vim
 ## Build
 /book/
 /build/
+/kani_build/
 /target
+/library/target
 *.rlib
 *.rmeta
 *.mir
diff --git a/doc/book.toml b/doc/book.toml
index 7f5e1329fef4d..078022e148f1f 100644
--- a/doc/book.toml
+++ b/doc/book.toml
@@ -12,6 +12,7 @@ build-dir = "../book"
 site-url = "/verify-rust-std/"
 git-repository-url = "https://github.com/model-checking/verify-rust-std"
 edit-url-template = "https://github.com/model-checking/verify-rust-std/edit/main/doc/{path}"
+no-section-label = true
 
 [output.html.playground]
 runnable = false
diff --git a/kani-version.toml b/kani-version.toml
new file mode 100644
index 0000000000000..95110639a4e6d
--- /dev/null
+++ b/kani-version.toml
@@ -0,0 +1,6 @@
+# This version should be updated whenever there is a change that makes this version of kani
+# incomaptible with the verify-std repo.
+
+[kani]
+kani-version = "0.54.0"
+commit = "e2a209bcb847803e8a5abb20ef7002b109ed0bf6"
diff --git a/run-kani.sh b/run-kani.sh
new file mode 100755
index 0000000000000..4c88cefcae304
--- /dev/null
+++ b/run-kani.sh
@@ -0,0 +1,172 @@
+#!/bin/bash
+
+set -e
+
+usage() {
+    echo "Usage: $0 [directory]"
+    echo "If directory is not provided, the current directory will be used."
+}
+
+if [[ "$1" == "-h" || "$1" == "--help" ]]; then
+    usage
+    exit 0
+fi
+
+# Set working directory
+if [[ -n "$1" ]]; then
+    if [[ ! -d "$1" ]]; then
+        echo "Error: Specified directory does not exist."
+        usage
+        exit 1
+    fi
+    WORK_DIR=$(realpath "$1")
+else
+    WORK_DIR=$(pwd)
+fi
+
+cd "$WORK_DIR" || exit 1
+
+log() {
+    echo "$(date '+%Y-%m-%d %H:%M:%S') - $1" | tee -a "$LOG_FILE"
+}
+
+error_exit() {
+    log "ERROR: $1"
+    exit 1
+}
+
+# Default values
+DEFAULT_TOML_FILE="kani-version.toml"
+DEFAULT_REPO_URL="https://github.com/model-checking/kani.git"
+DEFAULT_TARGET_DIR="kani_repo"
+DEFAULT_BRANCH_NAME="features/verify-rust-std"
+
+# Use environment variables if set, otherwise use defaults
+TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE}
+REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
+TARGET_DIR=${KANI_TARGET_DIR:-$DEFAULT_TARGET_DIR}
+BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
+
+os_name=$(uname -s)
+
+# Function to read commit ID from TOML file
+read_commit_from_toml() {
+    local file="$1"
+    if [ ! -f "$file" ]; then
+        echo "Error: TOML file not found: $file" >&2
+        exit 1
+    fi
+    local commit=$(grep '^commit *=' "$file" | sed 's/^commit *= *"\(.*\)"/\1/')
+    if [ -z "$commit" ]; then
+        echo "Error: 'commit' field not found in TOML file" >&2
+        exit 1
+    fi
+    echo "$commit"
+}
+
+clone_repo() {
+    local repo_url="$1"
+    local directory="$2"
+    local branch="$3"
+    local commit="$4"
+    git clone --depth 1 -b "$branch" "$repo_url" "$directory"
+    cd "$directory"
+    git checkout "$commit"
+    cd - > /dev/null
+}
+
+checkout_commit() {
+    local directory="$1"
+    local commit="$2"
+    cd "$directory"
+    git checkout "$commit"
+    cd ..
+}
+
+get_current_commit() {
+    local directory="$1"
+    if [ -d "$directory/.git" ]; then
+        git -C "$directory" rev-parse HEAD
+    else
+        echo ""
+    fi
+}
+
+build_project() {
+    local directory="$1"
+    cd "$directory"
+    cargo build-dev --release
+    cd ..
+}
+
+get_kani_path() {
+    local build_dir="$1"
+    echo "$(realpath "$build_dir/scripts/kani")"
+}
+
+run_kani_command() {
+    local kani_path="$1"
+    shift
+    "$kani_path" "$@"
+}
+
+# Check if binary exists and is up to date
+check_binary_exists() {
+    local build_dir="$1"
+    local expected_commit="$2"
+    local kani_path="$build_dir/scripts/kani"
+
+    if [ -f "$kani_path" ]; then
+        local current_commit=$(get_current_commit "$build_dir")
+        if [ "$current_commit" = "$expected_commit" ]; then
+            return 0
+        fi
+    fi
+    return 1
+}
+
+
+main() {
+    local current_dir=$(pwd)
+    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"
+
+    # Read commit ID from TOML file
+    commit=$(read_commit_from_toml "$TOML_FILE")
+    echo "Kani commit: $commit"
+
+    # Check if binary already exists and is up to date
+    if check_binary_exists "$build_dir" "$commit"; then
+        echo "Kani binary is up to date. Skipping build."
+    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_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
+
+        # Build project
+        build_project "$build_dir"
+
+        echo "Kani build completed successfully!"
+    fi
+
+    # Get the path to the Kani executable
+    kani_path=$(get_kani_path "$build_dir")
+    echo "Kani executable path: $kani_path"
+
+    echo "Running Kani command..."
+    "$kani_path" --version
+
+    echo "Running Kani verify-std command..."
+    cd $current_dir
+    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates
+}
+
+main
diff --git a/scripts/run_update_with_checks.sh b/scripts/run_update_with_checks.sh
index e7419f34d4901..d47d69680b837 100755
--- a/scripts/run_update_with_checks.sh
+++ b/scripts/run_update_with_checks.sh
@@ -135,47 +135,47 @@ fi
 
 echo "------------------------------------"
 # Call the first script to update the subtree
-echo "Update subtree in Main"
+echo "Update subtree in main"
 source $BASE_HOME_DIR/scripts/pull_from_upstream.sh "$TEMP_HOME_DIR" $TOOLCHAIN_DATE $COMMIT_HASH
-OUTPUT_SCRIPT1=("$?")
-if [ "${#OUTPUT_SCRIPT1[@]}" -eq 0 ]; then
-    echo "script1.sh failed to run."
+pull_from_upstream=("$?")
+if [ "${#pull_from_upstream[@]}" -eq 0 ]; then
+    echo "pull_from_upstream.sh failed to run."
     exit 1
 else
-    echo "script1.sh completed successfully."
+    echo "Pulled from upstream succesfully."
 fi
 
 # Call the second script
-echo "Running script2.sh..."
+echo "Updating toolchain..."
 source $BASE_HOME_DIR/scripts/update_toolchain_date.sh "$TEMP_HOME_DIR" "$TOOLCHAIN_DATE"
-OUTPUT_SCRIPT2=("$?")
-if [ "${#OUTPUT_SCRIPT2[@]}" -eq 0 ]; then
-    echo "script2.sh failed to run."
+update_toolchain_date=("$?")
+if [ "${#update_toolchain_date[@]}" -eq 0 ]; then
+    echo "update_toolchain_date.sh failed to run."
     exit 1
 else
-    echo "Update toolchain ran successfully."
+    echo "Toolchain updated succesfully."
 fi
 
 # Call the third script
-echo "Running script3.sh..."
+echo "echo "Checking compatiblity with kani..."
 source $BASE_HOME_DIR/scripts/check_rustc.sh "$TEMP_HOME_DIR"
-OUTPUT_SCRIPT3=("$?")
-if [ "${#OUTPUT_SCRIPT3[@]}" -eq 0 ]; then
-    echo "script3.sh failed to run."
+check_rustc=("$?")
+if [ "${#check_rustc[@]}" -eq 0 ]; then
+    echo "check_rustc.sh failed to run."
     exit 1
 else
-    echo "script3.sh completed successfully."
+    echo "Changes compatible with latest rustc."
 fi
 
-# Call the fourth script
-echo "Running script4.sh..."
-source $BASE_HOME_DIR/scripts/check_kani.sh "$TEMP_HOME_DIR"
-OUTPUT_SCRIPT4=("$?")
-if [ "${#OUTPUT_SCRIPT4[@]}" -eq 0 ]; then
-    echo "script4.sh failed to run."
+# Checking compatiblity with kani
+echo "Checking compatiblity with kani..."
+source $BASE_HOME_DIR/run-kani.sh "$TEMP_HOME_DIR"
+check_kani=("$?")
+if [ "${#check_kani[@]}" -eq 0 ]; then
+    echo "check_kani.sh failed to run."
     exit 1
 else
-    echo "script4.sh completed successfully."
+    echo "Changes compatible with kani's features/verify-std branch."
 fi
 
 # TODO: Issue a Pull Request from the sync branch of the temp repo

From 3c83c5cf5a4600fb23135880792cefc513defca4 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 18:36:05 +0000
Subject: [PATCH 02/23] Remove log and error_exit

---
 run-kani.sh | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/run-kani.sh b/run-kani.sh
index 4c88cefcae304..d3a531717b097 100755
--- a/run-kani.sh
+++ b/run-kani.sh
@@ -26,15 +26,6 @@ fi
 
 cd "$WORK_DIR" || exit 1
 
-log() {
-    echo "$(date '+%Y-%m-%d %H:%M:%S') - $1" | tee -a "$LOG_FILE"
-}
-
-error_exit() {
-    log "ERROR: $1"
-    exit 1
-}
-
 # Default values
 DEFAULT_TOML_FILE="kani-version.toml"
 DEFAULT_REPO_URL="https://github.com/model-checking/kani.git"

From 614af4962df2829ec866892b339e3b3e53135f94 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 18:39:46 +0000
Subject: [PATCH 03/23] Update CI

---
 .github/workflows/kani.yml        |  2 +-
 scripts/check_kani.sh             | 55 -------------------------------
 scripts/run_update_with_checks.sh |  6 ++--
 3 files changed, 4 insertions(+), 59 deletions(-)
 delete mode 100644 scripts/check_kani.sh

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index da0928998976c..3853c577cc071 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -35,4 +35,4 @@ jobs:
           submodules: true
 
       - name: Run Kani Script
-        run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head
+        run: bash ./head/run-kani.sh ${{github.workspace}}/head
diff --git a/scripts/check_kani.sh b/scripts/check_kani.sh
deleted file mode 100644
index c93499cb7a398..0000000000000
--- a/scripts/check_kani.sh
+++ /dev/null
@@ -1,55 +0,0 @@
-#!/bin/bash
-
-set -e
-
-# Set the working directories
-VERIFY_RUST_STD_DIR="$1"
-KANI_DIR=$(mktemp -d)
-
-RUNNER_TEMP=$(mktemp -d)
-
-# Get the OS name
-os_name=$(uname -s)
-
-# Checkout your local repository
-echo "Checking out local repository..."
-echo
-cd "$VERIFY_RUST_STD_DIR"
-
-# Checkout the Kani repository
-echo "Checking out Kani repository..."
-echo
-git clone --depth 1 -b features/verify-rust-std https://github.com/model-checking/kani.git "$KANI_DIR"
-
-# Check the OS and
-# Setup dependencies for Kani
-echo "Setting up dependencies for Kani..."
-echo
-cd "$KANI_DIR"
-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
-
-# Build Kani
-echo "Building Kani..."
-echo
-cargo build-dev --release
-# echo "$(pwd)/scripts" >> $PATH
-
-# Run tests
-echo "Running tests..."
-echo
-cd "$VERIFY_RUST_STD_DIR"
-$KANI_DIR/scripts/kani verify-std -Z unstable-options $VERIFY_RUST_STD_DIR/library --target-dir "$RUNNER_TEMP" -Z function-contracts -Z mem-predicates
-
-echo "Tests completed."
-echo
-
-# Clean up the Kani directory (optional)
-rm -rf "$KANI_DIR"
-rm -rf "$RUNNER_TEMP"
-# rm -rf "$VERIFY_RUST_STD_DIR"
diff --git a/scripts/run_update_with_checks.sh b/scripts/run_update_with_checks.sh
index d47d69680b837..03c4d1657a911 100755
--- a/scripts/run_update_with_checks.sh
+++ b/scripts/run_update_with_checks.sh
@@ -170,9 +170,9 @@ fi
 # Checking compatiblity with kani
 echo "Checking compatiblity with kani..."
 source $BASE_HOME_DIR/run-kani.sh "$TEMP_HOME_DIR"
-check_kani=("$?")
-if [ "${#check_kani[@]}" -eq 0 ]; then
-    echo "check_kani.sh failed to run."
+run_kani=("$?")
+if [ "${#run_kani[@]}" -eq 0 ]; then
+    echo "run_kani.sh failed to run."
     exit 1
 else
     echo "Changes compatible with kani's features/verify-std branch."

From 9ba9aae215504197d648075f30318dd001e3c614 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 19:12:04 +0000
Subject: [PATCH 04/23] Change output-format to terse

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

diff --git a/run-kani.sh b/run-kani.sh
index d3a531717b097..f4a77928d1bbb 100755
--- a/run-kani.sh
+++ b/run-kani.sh
@@ -157,7 +157,7 @@ main() {
 
     echo "Running Kani verify-std command..."
     cd $current_dir
-    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates
+    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse
 }
 
 main

From ec92080e5b144cc20bf5047a29e336b94fa9ca18 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 19:13:35 +0000
Subject: [PATCH 05/23] Remove version number from toml

---
 kani-version.toml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/kani-version.toml b/kani-version.toml
index 95110639a4e6d..1d0982a4290a3 100644
--- a/kani-version.toml
+++ b/kani-version.toml
@@ -2,5 +2,4 @@
 # incomaptible with the verify-std repo.
 
 [kani]
-kani-version = "0.54.0"
 commit = "e2a209bcb847803e8a5abb20ef7002b109ed0bf6"

From 70f9d40fa90af32cfbf34d868830c8e31620ac1c Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 19:18:42 +0000
Subject: [PATCH 06/23] Add dependency installation based on the os

---
 run-kani.sh | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/run-kani.sh b/run-kani.sh
index f4a77928d1bbb..f436d1db3f525 100755
--- a/run-kani.sh
+++ b/run-kani.sh
@@ -86,6 +86,15 @@ get_current_commit() {
 build_project() {
     local directory="$1"
     cd "$directory"
+
+    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
+
     cargo build-dev --release
     cd ..
 }

From f9557beaacb4980728ad0b9cec6263ecdfc15899 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 19:34:55 +0000
Subject: [PATCH 07/23] Modify trigger for kani.yml

---
 .github/workflows/kani.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 3853c577cc071..b8413581f9f0c 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -9,7 +9,7 @@ on:
     paths:
       - 'library/**'
       - '.github/workflows/kani.yml'
-      - 'scripts/check_kani.sh'
+      - 'run-kani.sh'
 
 defaults:
   run:

From 882a0658601a04149b2d098a962137a56a83db3b Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 20:45:13 +0000
Subject: [PATCH 08/23] Add CI workflow to test entrypoint script

---
 .github/workflows/check_entrypoint.yml | 49 ++++++++++++++++++++++
 run-kani.sh                            | 57 +++++++++++++++++++++-----
 2 files changed, 96 insertions(+), 10 deletions(-)
 create mode 100644 .github/workflows/check_entrypoint.yml

diff --git a/.github/workflows/check_entrypoint.yml b/.github/workflows/check_entrypoint.yml
new file mode 100644
index 0000000000000..1338b99c35bb4
--- /dev/null
+++ b/.github/workflows/check_entrypoint.yml
@@ -0,0 +1,49 @@
+# This workflow is responsible for verifying the standard library with Kani.
+
+name: Kani
+on:
+  workflow_dispatch:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+        - '.github/workflows/check_entrypoint.yml'
+        - '.github/workflows/kani.yml'
+        - 'run-kani.sh'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  build:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        # Kani does not support windows.
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+    steps:
+      - name: Checkout Library
+        uses: actions/checkout@v4
+        with:
+          path: head
+          submodules: true
+
+      - name: Run Kani Script with a path
+        run: bash ./head/run-kani.sh -p ${{github.workspace}}/head
+
+      - name: Run Kani Script with --kani-args and -p
+        run: bash ./head/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
+
+      - name: Run Kani Script without -p
+        working-directory: ${{github.workspace}}/head
+        run: bash ./head/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
+
+      - name: Run Kani Script without any arguments
+        working-directory: ${{github.workspace}}/head
+        run: bash ./head/run-kani.sh
diff --git a/run-kani.sh b/run-kani.sh
index f436d1db3f525..8c07421d52750 100755
--- a/run-kani.sh
+++ b/run-kani.sh
@@ -3,23 +3,54 @@
 set -e
 
 usage() {
-    echo "Usage: $0 [directory]"
-    echo "If directory is not provided, the current directory will be used."
+    echo "Usage: $0 [options] [-p <path>] [--k-args <command arguments>]"
+    echo "Options:"
+    echo "  -h, --help         Show this help message"
+    echo "  -p, --path <path>  Specify a path (optional)"
+    echo "  --kani-args           Optional: Arguments to pass to the command"
+    exit 1
 }
 
-if [[ "$1" == "-h" || "$1" == "--help" ]]; then
-    usage
-    exit 0
-fi
+# Initialize variables
+command_args=""
+path=""
+
+# Parse command line arguments
+while [[ $# -gt 0 ]]; do
+    case $1 in
+        -h|--help)
+            usage
+            ;;
+        -p|--path)
+            if [[ -n $2 ]]; then
+                path=$2
+                shift 2
+            else
+                echo "Error: Path argument is missing"
+                usage
+            fi
+            ;;
+        --kani-args)
+            shift  # Remove --k-args from the argument list
+            command_args="$@"  # Capture all remaining arguments
+            break  # Stop processing further arguments
+            ;;
+        *)
+            # If --k-args is not used, treat all remaining arguments as command arguments
+            command_args="$@"
+            break
+            ;;
+    esac
+done
 
 # Set working directory
-if [[ -n "$1" ]]; then
-    if [[ ! -d "$1" ]]; then
+if [[ -n "$path" ]]; then
+    if [[ ! -d "$path" ]]; then
         echo "Error: Specified directory does not exist."
         usage
         exit 1
     fi
-    WORK_DIR=$(realpath "$1")
+    WORK_DIR=$(realpath "$path")
 else
     WORK_DIR=$(pwd)
 fi
@@ -166,7 +197,13 @@ main() {
 
     echo "Running Kani verify-std command..."
     cd $current_dir
-    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse
+
+    # Run the command with the provided arguments (if any)
+    if [ -n "$command_args" ]; then
+        "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args
+    else
+        "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse
+    fi
 }
 
 main

From d3009c3db14e5e226d94acc7680339aeb5753044 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 20:50:58 +0000
Subject: [PATCH 09/23] Add --path to kani.yml check

---
 .github/workflows/kani.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index b8413581f9f0c..4b2e87e99bff0 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -35,4 +35,4 @@ jobs:
           submodules: true
 
       - name: Run Kani Script
-        run: bash ./head/run-kani.sh ${{github.workspace}}/head
+        run: bash ./head/run-kani.sh --path ${{github.workspace}}/head

From 329ef6a2bb31a9cff4012610627409ff28f7d1f5 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 21:06:51 +0000
Subject: [PATCH 10/23] Rename check name

---
 .github/workflows/kani.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 4b2e87e99bff0..b937f85eecc03 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -1,6 +1,6 @@
 # This workflow is responsible for verifying the standard library with Kani.
 
-name: Kani
+name: Check entry-point
 on:
   workflow_dispatch:
   pull_request:

From aba4ecfa84ee31728bb02aa7ec588c839b695d89 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 21:21:25 +0000
Subject: [PATCH 11/23] Fix workflow names

---
 .github/workflows/check_entrypoint.yml | 16 ++++++----------
 .github/workflows/kani.yml             |  2 +-
 2 files changed, 7 insertions(+), 11 deletions(-)

diff --git a/.github/workflows/check_entrypoint.yml b/.github/workflows/check_entrypoint.yml
index 1338b99c35bb4..cbdc9be54fd5f 100644
--- a/.github/workflows/check_entrypoint.yml
+++ b/.github/workflows/check_entrypoint.yml
@@ -1,15 +1,15 @@
 # This workflow is responsible for verifying the standard library with Kani.
 
-name: Kani
+name: Check entry-point
 on:
   workflow_dispatch:
   pull_request:
     branches: [ main ]
   push:
     paths:
-        - '.github/workflows/check_entrypoint.yml'
-        - '.github/workflows/kani.yml'
-        - 'run-kani.sh'
+      - '.github/workflows/check_entrypoint.yml'
+      - '.github/workflows/kani.yml'
+      - 'run-kani.sh'
 
 defaults:
   run:
@@ -34,9 +34,6 @@ jobs:
           path: head
           submodules: true
 
-      - name: Run Kani Script with a path
-        run: bash ./head/run-kani.sh -p ${{github.workspace}}/head
-
       - name: Run Kani Script with --kani-args and -p
         run: bash ./head/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
 
@@ -44,6 +41,5 @@ jobs:
         working-directory: ${{github.workspace}}/head
         run: bash ./head/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
 
-      - name: Run Kani Script without any arguments
-        working-directory: ${{github.workspace}}/head
-        run: bash ./head/run-kani.sh
+      - name: Run Kani Script with a path
+        run: bash ./head/run-kani.sh -p ${{github.workspace}}/head
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index b937f85eecc03..4b2e87e99bff0 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -1,6 +1,6 @@
 # This workflow is responsible for verifying the standard library with Kani.
 
-name: Check entry-point
+name: Kani
 on:
   workflow_dispatch:
   pull_request:

From 739d8989ad20cca8a9265b2b2541fcacc599f207 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Fri, 6 Sep 2024 21:27:30 +0000
Subject: [PATCH 12/23] Fix step for without -p

---
 .github/workflows/check_entrypoint.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/check_entrypoint.yml b/.github/workflows/check_entrypoint.yml
index cbdc9be54fd5f..f13ae4d7c88f8 100644
--- a/.github/workflows/check_entrypoint.yml
+++ b/.github/workflows/check_entrypoint.yml
@@ -39,7 +39,7 @@ jobs:
 
       - name: Run Kani Script without -p
         working-directory: ${{github.workspace}}/head
-        run: bash ./head/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
+        run: bash ./run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
 
       - name: Run Kani Script with a path
         run: bash ./head/run-kani.sh -p ${{github.workspace}}/head

From 0ddbd8f9a6c1494d06e438933648fe4af23e9810 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Tue, 10 Sep 2024 15:12:22 +0000
Subject: [PATCH 13/23] Remove entry point workflow and move kani script

---
 .github/workflows/check_entrypoint.yml        | 45 ----------
 .github/workflows/kani.yml                    | 11 ++-
 library/Cargo.lock                            | 86 +++++++++++++++++++
 run-kani.sh => scripts/run-kani.sh            | 14 ++-
 .../kani-version.toml                         |  2 +-
 5 files changed, 102 insertions(+), 56 deletions(-)
 delete mode 100644 .github/workflows/check_entrypoint.yml
 rename run-kani.sh => scripts/run-kani.sh (91%)
 rename kani-version.toml => tool_config/kani-version.toml (73%)

diff --git a/.github/workflows/check_entrypoint.yml b/.github/workflows/check_entrypoint.yml
deleted file mode 100644
index f13ae4d7c88f8..0000000000000
--- a/.github/workflows/check_entrypoint.yml
+++ /dev/null
@@ -1,45 +0,0 @@
-# This workflow is responsible for verifying the standard library with Kani.
-
-name: Check entry-point
-on:
-  workflow_dispatch:
-  pull_request:
-    branches: [ main ]
-  push:
-    paths:
-      - '.github/workflows/check_entrypoint.yml'
-      - '.github/workflows/kani.yml'
-      - 'run-kani.sh'
-
-defaults:
-  run:
-    shell: bash
-
-jobs:
-  build:
-    runs-on: ${{ matrix.os }}
-    strategy:
-      matrix:
-        # Kani does not support windows.
-        os: [ubuntu-latest, macos-latest]
-        include:
-          - os: ubuntu-latest
-            base: ubuntu
-          - os: macos-latest
-            base: macos
-    steps:
-      - name: Checkout Library
-        uses: actions/checkout@v4
-        with:
-          path: head
-          submodules: true
-
-      - name: Run Kani Script with --kani-args and -p
-        run: bash ./head/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
-
-      - name: Run Kani Script without -p
-        working-directory: ${{github.workspace}}/head
-        run: bash ./run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
-
-      - name: Run Kani Script with a path
-        run: bash ./head/run-kani.sh -p ${{github.workspace}}/head
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 4b2e87e99bff0..81f2d61930b32 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -9,7 +9,7 @@ on:
     paths:
       - 'library/**'
       - '.github/workflows/kani.yml'
-      - 'run-kani.sh'
+      - 'scripts/run-kani.sh'
 
 defaults:
   run:
@@ -35,4 +35,11 @@ jobs:
           submodules: true
 
       - name: Run Kani Script
-        run: bash ./head/run-kani.sh --path ${{github.workspace}}/head
+        run: bash ./head/scripts/run-kani.sh --path ${{github.workspace}}/head
+
+      - name: Run Kani Script with --kani-args and -p
+        run: bash ./head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
+
+      - name: Run Kani Script without -p
+        working-directory: ${{github.workspace}}/head
+        run: bash ./scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
diff --git a/library/Cargo.lock b/library/Cargo.lock
index 223b61456c267..18a30390ae29a 100644
--- a/library/Cargo.lock
+++ b/library/Cargo.lock
@@ -72,6 +72,7 @@ version = "0.0.0"
 dependencies = [
  "rand",
  "rand_xorshift",
+ "safety",
 ]
 
 [[package]]
@@ -219,6 +220,39 @@ dependencies = [
  "unwind",
 ]
 
+[[package]]
+name = "proc-macro-error"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
+dependencies = [
+ "proc-macro-error-attr",
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro-error-attr"
+version = "1.0.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "version_check",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.86"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77"
+dependencies = [
+ "unicode-ident",
+]
+
 [[package]]
 name = "proc_macro"
 version = "0.0.0"
@@ -236,6 +270,15 @@ dependencies = [
  "core",
 ]
 
+[[package]]
+name = "quote"
+version = "1.0.37"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
+dependencies = [
+ "proc-macro2",
+]
+
 [[package]]
 name = "r-efi"
 version = "4.5.0"
@@ -312,6 +355,16 @@ dependencies = [
  "std",
 ]
 
+[[package]]
+name = "safety"
+version = "0.1.0"
+dependencies = [
+ "proc-macro-error",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.77",
+]
+
 [[package]]
 name = "std"
 version = "0.0.0"
@@ -352,6 +405,27 @@ dependencies = [
  "rustc-std-workspace-core",
 ]
 
+[[package]]
+name = "syn"
+version = "1.0.109"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
+dependencies = [
+ "proc-macro2",
+ "unicode-ident",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.77"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9f35bcdf61fd8e7be6caf75f429fdca8beb3ed76584befb503b1569faee373ed"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "sysroot"
 version = "0.0.0"
@@ -371,6 +445,12 @@ dependencies = [
  "std",
 ]
 
+[[package]]
+name = "unicode-ident"
+version = "1.0.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
+
 [[package]]
 name = "unicode-width"
 version = "0.1.13"
@@ -404,6 +484,12 @@ dependencies = [
  "rustc-std-workspace-core",
 ]
 
+[[package]]
+name = "version_check"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
+
 [[package]]
 name = "wasi"
 version = "0.11.0+wasi-snapshot-preview1"
diff --git a/run-kani.sh b/scripts/run-kani.sh
similarity index 91%
rename from run-kani.sh
rename to scripts/run-kani.sh
index 8c07421d52750..77f302ff93495 100755
--- a/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -6,8 +6,8 @@ usage() {
     echo "Usage: $0 [options] [-p <path>] [--k-args <command arguments>]"
     echo "Options:"
     echo "  -h, --help         Show this help message"
-    echo "  -p, --path <path>  Specify a path (optional)"
-    echo "  --kani-args           Optional: Arguments to pass to the command"
+    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 "  --kani-args        Optional: Arguments to pass to the command"
     exit 1
 }
 
@@ -31,9 +31,9 @@ while [[ $# -gt 0 ]]; do
             fi
             ;;
         --kani-args)
-            shift  # Remove --k-args from the argument list
-            command_args="$@"  # Capture all remaining arguments
-            break  # Stop processing further arguments
+            shift
+            command_args="$@"
+            break
             ;;
         *)
             # If --k-args is not used, treat all remaining arguments as command arguments
@@ -58,15 +58,13 @@ fi
 cd "$WORK_DIR" || exit 1
 
 # Default values
-DEFAULT_TOML_FILE="kani-version.toml"
+DEFAULT_TOML_FILE="tool_config/kani-version.toml"
 DEFAULT_REPO_URL="https://github.com/model-checking/kani.git"
-DEFAULT_TARGET_DIR="kani_repo"
 DEFAULT_BRANCH_NAME="features/verify-rust-std"
 
 # Use environment variables if set, otherwise use defaults
 TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE}
 REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
-TARGET_DIR=${KANI_TARGET_DIR:-$DEFAULT_TARGET_DIR}
 BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
 
 os_name=$(uname -s)
diff --git a/kani-version.toml b/tool_config/kani-version.toml
similarity index 73%
rename from kani-version.toml
rename to tool_config/kani-version.toml
index 1d0982a4290a3..df854dfcfeac2 100644
--- a/kani-version.toml
+++ b/tool_config/kani-version.toml
@@ -2,4 +2,4 @@
 # incomaptible with the verify-std repo.
 
 [kani]
-commit = "e2a209bcb847803e8a5abb20ef7002b109ed0bf6"
+commit = "cda1b30c935c327a8d4ccba0add9f30b9612863f"

From c18d6d5cd4612d3ded8d29a6b42ac490cf883281 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Tue, 10 Sep 2024 15:34:16 +0000
Subject: [PATCH 14/23] Add comments

---
 scripts/run-kani.sh | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 77f302ff93495..5c7741e3d98e7 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -3,11 +3,11 @@
 set -e
 
 usage() {
-    echo "Usage: $0 [options] [-p <path>] [--k-args <command arguments>]"
+    echo "Usage: $0 [options] [-p <path>] [--kani-args <command arguments>]"
     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 "  --kani-args        Optional: Arguments to pass to the command"
+    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
 }
 
@@ -16,6 +16,7 @@ command_args=""
 path=""
 
 # Parse command line arguments
+# TODO: Improve parsing with getopts
 while [[ $# -gt 0 ]]; do
     case $1 in
         -h|--help)
@@ -36,8 +37,6 @@ while [[ $# -gt 0 ]]; do
             break
             ;;
         *)
-            # If --k-args is not used, treat all remaining arguments as command arguments
-            command_args="$@"
             break
             ;;
     esac

From 98f213c6599e1afa2fb7f309a6d3d6dda636460f Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
Date: Fri, 13 Sep 2024 15:21:28 -0400
Subject: [PATCH 15/23] Apply suggestions from code review

Co-authored-by: Michael Tautschnig <mt@debian.org>
---
 .github/workflows/kani.yml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 81f2d61930b32..559f0d7f0b60e 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -35,11 +35,11 @@ jobs:
           submodules: true
 
       - name: Run Kani Script
-        run: bash ./head/scripts/run-kani.sh --path ${{github.workspace}}/head
+        run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 
       - name: Run Kani Script with --kani-args and -p
-        run: bash ./head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
+        run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
 
       - name: Run Kani Script without -p
         working-directory: ${{github.workspace}}/head
-        run: bash ./scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
+        run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut

From 5c06ed5566e9e8cd344f02418296aaa1d2f9dc47 Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Tue, 22 Oct 2024 11:22:58 -0400
Subject: [PATCH 16/23] Address PR comments

---
 scripts/run-kani.sh | 56 +++++++++++++++++++--------------------------
 1 file changed, 24 insertions(+), 32 deletions(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 5c7741e3d98e7..2427a59740ed7 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -54,7 +54,7 @@ else
     WORK_DIR=$(pwd)
 fi
 
-cd "$WORK_DIR" || exit 1
+cd "$WORK_DIR"
 
 # Default values
 DEFAULT_TOML_FILE="tool_config/kani-version.toml"
@@ -66,17 +66,15 @@ TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE}
 REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
 BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
 
-os_name=$(uname -s)
-
 # Function to read commit ID from TOML file
 read_commit_from_toml() {
     local file="$1"
-    if [ ! -f "$file" ]; then
+    if [[ ! -f "$file" ]]; then
         echo "Error: TOML file not found: $file" >&2
         exit 1
     fi
     local commit=$(grep '^commit *=' "$file" | sed 's/^commit *= *"\(.*\)"/\1/')
-    if [ -z "$commit" ]; then
+    if [[ -z "$commit" ]]; then
         echo "Error: 'commit' field not found in TOML file" >&2
         exit 1
     fi
@@ -88,18 +86,10 @@ clone_repo() {
     local directory="$2"
     local branch="$3"
     local commit="$4"
-    git clone --depth 1 -b "$branch" "$repo_url" "$directory"
-    cd "$directory"
-    git checkout "$commit"
-    cd - > /dev/null
-}
-
-checkout_commit() {
-    local directory="$1"
-    local commit="$2"
-    cd "$directory"
+    git clone --depth 1 "$repo_url" "$directory"
+    pushd -q "$directory"
     git checkout "$commit"
-    cd ..
+    popd -q
 }
 
 get_current_commit() {
@@ -111,20 +101,21 @@ get_current_commit() {
     fi
 }
 
-build_project() {
+build_kani() {
     local directory="$1"
-    cd "$directory"
+    pushd -q "$directory"
+    os_name=$(uname -s)
 
-    if [ "$os_name" == "Linux" ]; then
+    if [[ "$os_name" == "Linux" ]]; then
         ./scripts/setup/ubuntu/install_deps.sh
-    elif [ "$os_name" == "Darwin" ]; then
+    elif [[ "$os_name" == "Darwin" ]]; then
         ./scripts/setup/macos/install_deps.sh
     else
         echo "Unknown operating system"
     fi
 
     cargo build-dev --release
-    cd ..
+    popd -q
 }
 
 get_kani_path() {
@@ -144,9 +135,9 @@ check_binary_exists() {
     local expected_commit="$2"
     local kani_path="$build_dir/scripts/kani"
 
-    if [ -f "$kani_path" ]; then
+    if [[ -f "$kani_path" ]]; then
         local current_commit=$(get_current_commit "$build_dir")
-        if [ "$current_commit" = "$expected_commit" ]; then
+        if [[ "$current_commit" = "$expected_commit" ]]; then
             return 0
         fi
     fi
@@ -155,7 +146,6 @@ check_binary_exists() {
 
 
 main() {
-    local current_dir=$(pwd)
     local build_dir="$WORK_DIR/kani_build"
     local temp_dir_target=$(mktemp -d)
 
@@ -180,7 +170,7 @@ main() {
         clone_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
 
         # Build project
-        build_project "$build_dir"
+        build_kani "$build_dir"
 
         echo "Kani build completed successfully!"
     fi
@@ -193,14 +183,16 @@ main() {
     "$kani_path" --version
 
     echo "Running Kani verify-std command..."
-    cd $current_dir
 
-    # Run the command with the provided arguments (if any)
-    if [ -n "$command_args" ]; then
-        "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args
-    else
-        "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse
-    fi
+    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args
+
 }
 
 main
+
+cleanup()
+{
+  rm -rf "$temp_dir_target"
+}
+
+trap cleanup EXIT

From 4ceae2ec4c083f8d923c4bb3fcec4da587a74075 Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Tue, 22 Oct 2024 12:41:28 -0400
Subject: [PATCH 17/23] Fix Kani script and CI path

---
 .github/workflows/kani.yml    | 42 ++++++++++++++++++++++++++---------
 scripts/run-kani.sh           | 16 ++++++-------
 tool_config/kani-version.toml |  2 +-
 3 files changed, 40 insertions(+), 20 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 559f0d7f0b60e..39836a5140601 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -1,6 +1,5 @@
-# This workflow is responsible for verifying the standard library with Kani.
+name: Kani Rust Verification
 
-name: Kani
 on:
   workflow_dispatch:
   pull_request:
@@ -16,11 +15,11 @@ defaults:
     shell: bash
 
 jobs:
-  build:
+  check-kani-on-std:
+    name: Verify Rust Code (Default Configuration)
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        # Kani does not support windows.
         os: [ubuntu-latest, macos-latest]
         include:
           - os: ubuntu-latest
@@ -28,18 +27,41 @@ jobs:
           - os: macos-latest
             base: macos
     steps:
-      - name: Checkout Library
+      # Step 1: Check out the repository
+      - name: Checkout Repository
         uses: actions/checkout@v4
         with:
           path: head
           submodules: true
 
-      - name: Run Kani Script
+      # Step 2: Run Kani on the std library (default configuration)
+      - name: Run Kani Verification (Default)
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 
-      - name: Run Kani Script with --kani-args and -p
-        run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
+  test-kani-script:
+    name: Verify Rust Code (Custom Configuration)
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          path: head
+          submodules: true
+
+      # Step 2: Test Kani verification script with specific arguments
+      - name: Run Kani Verification (Custom Args)
+        run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse
 
-      - name: Run Kani Script without -p
+      # Step 3: Test Kani verification script in the repository directory
+      - name: Run Kani Verification (In Repo Directory)
         working-directory: ${{github.workspace}}/head
-        run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut
+        run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 2427a59740ed7..70e0d682ad9ea 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -81,15 +81,15 @@ read_commit_from_toml() {
     echo "$commit"
 }
 
-clone_repo() {
+clone_kani_repo() {
     local repo_url="$1"
     local directory="$2"
     local branch="$3"
     local commit="$4"
-    git clone --depth 1 "$repo_url" "$directory"
-    pushd -q "$directory"
+    git clone "$repo_url" "$directory"
+    pushd "$directory"
     git checkout "$commit"
-    popd -q
+    popd
 }
 
 get_current_commit() {
@@ -103,7 +103,7 @@ get_current_commit() {
 
 build_kani() {
     local directory="$1"
-    pushd -q "$directory"
+    pushd "$directory"
     os_name=$(uname -s)
 
     if [[ "$os_name" == "Linux" ]]; then
@@ -115,7 +115,7 @@ build_kani() {
     fi
 
     cargo build-dev --release
-    popd -q
+    popd
 }
 
 get_kani_path() {
@@ -154,7 +154,6 @@ main() {
 
     # Read commit ID from TOML file
     commit=$(read_commit_from_toml "$TOML_FILE")
-    echo "Kani commit: $commit"
 
     # Check if binary already exists and is up to date
     if check_binary_exists "$build_dir" "$commit"; then
@@ -167,7 +166,7 @@ main() {
         mkdir -p "$build_dir"
 
         # Clone repository and checkout specific commit
-        clone_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
+        clone_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
 
         # Build project
         build_kani "$build_dir"
@@ -185,7 +184,6 @@ main() {
     echo "Running Kani verify-std command..."
 
     "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args
-
 }
 
 main
diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml
index df854dfcfeac2..2a42cd37544ef 100644
--- a/tool_config/kani-version.toml
+++ b/tool_config/kani-version.toml
@@ -2,4 +2,4 @@
 # incomaptible with the verify-std repo.
 
 [kani]
-commit = "cda1b30c935c327a8d4ccba0add9f30b9612863f"
+commit = "1c38609ec35f591898b94ec39427d1b5b0cad824"

From 12e4f44e12e8b7f2ccb39b7b3553ec0ca5c95f76 Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Tue, 22 Oct 2024 12:46:41 -0400
Subject: [PATCH 18/23] Removed cargo.lock from PR

---
 library/Cargo.lock | 580 ---------------------------------------------
 1 file changed, 580 deletions(-)
 delete mode 100644 library/Cargo.lock

diff --git a/library/Cargo.lock b/library/Cargo.lock
deleted file mode 100644
index 6b72727613c06..0000000000000
--- a/library/Cargo.lock
+++ /dev/null
@@ -1,580 +0,0 @@
-# This file is automatically @generated by Cargo.
-# It is not intended for manual editing.
-version = 3
-
-[[package]]
-name = "addr2line"
-version = "0.22.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6e4503c46a5c0c7844e948c9a4d6acd9f50cccb4de1c48eb9e291ea17470c678"
-dependencies = [
- "compiler_builtins",
- "gimli 0.29.0",
- "rustc-std-workspace-alloc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "adler"
-version = "1.0.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "alloc"
-version = "0.0.0"
-dependencies = [
- "compiler_builtins",
- "core",
- "rand",
- "rand_xorshift",
-]
-
-[[package]]
-name = "allocator-api2"
-version = "0.2.18"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5c6cb57a04249c6480766f7f7cef5467412af1490f8d1e243141daddada3264f"
-
-[[package]]
-name = "cc"
-version = "1.0.99"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "96c51067fd44124faa7f870b4b1c969379ad32b2ba805aa959430ceaa384f695"
-
-[[package]]
-name = "cfg-if"
-version = "1.0.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "compiler_builtins"
-version = "0.1.123"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b47fcbecb558bdad78c7d3a998523c60a50dd6cd046d5fe74163e309e878fff7"
-dependencies = [
- "cc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "core"
-version = "0.0.0"
-dependencies = [
- "rand",
- "rand_xorshift",
- "safety",
-]
-
-[[package]]
-name = "dlmalloc"
-version = "0.2.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3264b043b8e977326c1ee9e723da2c1f8d09a99df52cacf00b4dbce5ac54414d"
-dependencies = [
- "cfg-if",
- "compiler_builtins",
- "libc",
- "rustc-std-workspace-core",
- "windows-sys",
-]
-
-[[package]]
-name = "fortanix-sgx-abi"
-version = "0.5.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "57cafc2274c10fab234f176b25903ce17e690fca7597090d50880e047a0389c5"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "getopts"
-version = "0.2.21"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "14dbbfd5c71d70241ecf9e6f13737f7b5ce823821063188d7e46c41d371eebd5"
-dependencies = [
- "rustc-std-workspace-core",
- "rustc-std-workspace-std",
- "unicode-width",
-]
-
-[[package]]
-name = "gimli"
-version = "0.28.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4271d37baee1b8c7e4b708028c57d816cf9d2434acb33a549475f78c181f6253"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-alloc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "gimli"
-version = "0.29.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "40ecd4077b5ae9fd2e9e169b102c6c330d0605168eb0e8bf79952b256dbefffd"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-alloc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "hashbrown"
-version = "0.14.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1"
-dependencies = [
- "allocator-api2",
- "compiler_builtins",
- "rustc-std-workspace-alloc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "hermit-abi"
-version = "0.4.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fbf6a919d6cf397374f7dfeeea91d974c7c0a7221d0d0f4f20d859d329e53fcc"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-alloc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "libc"
-version = "0.2.158"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d8adc4bb1803a324070e64a98ae98f38934d91957a99cfb3a43dcbc01bc56439"
-dependencies = [
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "memchr"
-version = "2.5.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "miniz_oxide"
-version = "0.7.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b8a240ddb74feaf34a79a7add65a741f3167852fba007066dcac1ca548d89c08"
-dependencies = [
- "adler",
- "compiler_builtins",
- "rustc-std-workspace-alloc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "object"
-version = "0.36.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3f203fa8daa7bb185f760ae12bd8e097f63d17041dcdcaf675ac54cdf863170e"
-dependencies = [
- "compiler_builtins",
- "memchr",
- "rustc-std-workspace-alloc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "panic_abort"
-version = "0.0.0"
-dependencies = [
- "alloc",
- "cfg-if",
- "compiler_builtins",
- "core",
- "libc",
-]
-
-[[package]]
-name = "panic_unwind"
-version = "0.0.0"
-dependencies = [
- "alloc",
- "cfg-if",
- "compiler_builtins",
- "core",
- "libc",
- "unwind",
-]
-
-[[package]]
-name = "proc-macro-error"
-version = "1.0.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
-dependencies = [
- "proc-macro-error-attr",
- "proc-macro2",
- "quote",
- "syn 1.0.109",
- "version_check",
-]
-
-[[package]]
-name = "proc-macro-error-attr"
-version = "1.0.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
-dependencies = [
- "proc-macro2",
- "quote",
- "version_check",
-]
-
-[[package]]
-name = "proc-macro2"
-version = "1.0.86"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77"
-dependencies = [
- "unicode-ident",
-]
-
-[[package]]
-name = "proc_macro"
-version = "0.0.0"
-dependencies = [
- "core",
- "std",
-]
-
-[[package]]
-name = "profiler_builtins"
-version = "0.0.0"
-dependencies = [
- "cc",
- "compiler_builtins",
- "core",
-]
-
-[[package]]
-name = "quote"
-version = "1.0.37"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
-dependencies = [
- "proc-macro2",
-]
-
-[[package]]
-name = "r-efi"
-version = "4.5.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e9e935efc5854715dfc0a4c9ef18dc69dee0ec3bf9cc3ab740db831c0fdd86a3"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "r-efi-alloc"
-version = "1.0.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "31d6f09fe2b6ad044bc3d2c34ce4979796581afd2f1ebc185837e02421e02fd7"
-dependencies = [
- "compiler_builtins",
- "r-efi",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "rand"
-version = "0.8.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
-dependencies = [
- "rand_core",
-]
-
-[[package]]
-name = "rand_core"
-version = "0.6.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
-
-[[package]]
-name = "rand_xorshift"
-version = "0.3.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d25bf25ec5ae4a3f1b92f929810509a2f53d7dca2f50b794ff57e3face536c8f"
-dependencies = [
- "rand_core",
-]
-
-[[package]]
-name = "rustc-demangle"
-version = "0.1.24"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "rustc-std-workspace-alloc"
-version = "1.99.0"
-dependencies = [
- "alloc",
-]
-
-[[package]]
-name = "rustc-std-workspace-core"
-version = "1.99.0"
-dependencies = [
- "core",
-]
-
-[[package]]
-name = "rustc-std-workspace-std"
-version = "1.99.0"
-dependencies = [
- "std",
-]
-
-[[package]]
-name = "safety"
-version = "0.1.0"
-dependencies = [
- "proc-macro-error",
- "proc-macro2",
- "quote",
- "syn 2.0.77",
-]
-
-[[package]]
-name = "std"
-version = "0.0.0"
-dependencies = [
- "addr2line",
- "alloc",
- "cfg-if",
- "compiler_builtins",
- "core",
- "dlmalloc",
- "fortanix-sgx-abi",
- "hashbrown",
- "hermit-abi",
- "libc",
- "miniz_oxide",
- "object",
- "panic_abort",
- "panic_unwind",
- "profiler_builtins",
- "r-efi",
- "r-efi-alloc",
- "rand",
- "rand_xorshift",
- "rustc-demangle",
- "std_detect",
- "unwind",
- "wasi",
- "windows-targets 0.0.0",
-]
-
-[[package]]
-name = "std_detect"
-version = "0.1.5"
-dependencies = [
- "cfg-if",
- "compiler_builtins",
- "libc",
- "rustc-std-workspace-alloc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "syn"
-version = "1.0.109"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
-dependencies = [
- "proc-macro2",
- "unicode-ident",
-]
-
-[[package]]
-name = "syn"
-version = "2.0.77"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9f35bcdf61fd8e7be6caf75f429fdca8beb3ed76584befb503b1569faee373ed"
-dependencies = [
- "proc-macro2",
- "quote",
- "unicode-ident",
-]
-
-[[package]]
-name = "sysroot"
-version = "0.0.0"
-dependencies = [
- "proc_macro",
- "std",
- "test",
-]
-
-[[package]]
-name = "test"
-version = "0.0.0"
-dependencies = [
- "core",
- "getopts",
- "libc",
- "std",
-]
-
-[[package]]
-name = "unicode-ident"
-version = "1.0.12"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
-
-[[package]]
-name = "unicode-width"
-version = "0.1.13"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0336d538f7abc86d282a4189614dfaa90810dfc2c6f6427eaf88e16311dd225d"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-core",
- "rustc-std-workspace-std",
-]
-
-[[package]]
-name = "unwind"
-version = "0.0.0"
-dependencies = [
- "cfg-if",
- "compiler_builtins",
- "core",
- "libc",
- "unwinding",
-]
-
-[[package]]
-name = "unwinding"
-version = "0.2.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "37a19a21a537f635c16c7576f22d0f2f7d63353c1337ad4ce0d8001c7952a25b"
-dependencies = [
- "compiler_builtins",
- "gimli 0.28.1",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "version_check"
-version = "0.9.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
-
-[[package]]
-name = "wasi"
-version = "0.11.0+wasi-snapshot-preview1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
-dependencies = [
- "compiler_builtins",
- "rustc-std-workspace-alloc",
- "rustc-std-workspace-core",
-]
-
-[[package]]
-name = "windows-sys"
-version = "0.52.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
-dependencies = [
- "windows-targets 0.52.5",
-]
-
-[[package]]
-name = "windows-targets"
-version = "0.0.0"
-
-[[package]]
-name = "windows-targets"
-version = "0.52.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb"
-dependencies = [
- "windows_aarch64_gnullvm",
- "windows_aarch64_msvc",
- "windows_i686_gnu",
- "windows_i686_gnullvm",
- "windows_i686_msvc",
- "windows_x86_64_gnu",
- "windows_x86_64_gnullvm",
- "windows_x86_64_msvc",
-]
-
-[[package]]
-name = "windows_aarch64_gnullvm"
-version = "0.52.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263"
-
-[[package]]
-name = "windows_aarch64_msvc"
-version = "0.52.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6"
-
-[[package]]
-name = "windows_i686_gnu"
-version = "0.52.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670"
-
-[[package]]
-name = "windows_i686_gnullvm"
-version = "0.52.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9"
-
-[[package]]
-name = "windows_i686_msvc"
-version = "0.52.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf"
-
-[[package]]
-name = "windows_x86_64_gnu"
-version = "0.52.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9"
-
-[[package]]
-name = "windows_x86_64_gnullvm"
-version = "0.52.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596"
-
-[[package]]
-name = "windows_x86_64_msvc"
-version = "0.52.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0"

From 0943f8f1b521e1e82890e4fb4a2dbf5d9e4f6243 Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Tue, 22 Oct 2024 12:50:18 -0400
Subject: [PATCH 19/23] Remove cargo.lock from PR entirely

---
 library/Cargo.lock | 494 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 494 insertions(+)
 create mode 100644 library/Cargo.lock

diff --git a/library/Cargo.lock b/library/Cargo.lock
new file mode 100644
index 0000000000000..54ad052c52322
--- /dev/null
+++ b/library/Cargo.lock
@@ -0,0 +1,494 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "addr2line"
+version = "0.22.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6e4503c46a5c0c7844e948c9a4d6acd9f50cccb4de1c48eb9e291ea17470c678"
+dependencies = [
+ "compiler_builtins",
+ "gimli 0.29.0",
+ "rustc-std-workspace-alloc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "adler"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "alloc"
+version = "0.0.0"
+dependencies = [
+ "compiler_builtins",
+ "core",
+ "rand",
+ "rand_xorshift",
+]
+
+[[package]]
+name = "allocator-api2"
+version = "0.2.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c6cb57a04249c6480766f7f7cef5467412af1490f8d1e243141daddada3264f"
+
+[[package]]
+name = "cc"
+version = "1.0.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "96c51067fd44124faa7f870b4b1c969379ad32b2ba805aa959430ceaa384f695"
+
+[[package]]
+name = "cfg-if"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "compiler_builtins"
+version = "0.1.123"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b47fcbecb558bdad78c7d3a998523c60a50dd6cd046d5fe74163e309e878fff7"
+dependencies = [
+ "cc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "core"
+version = "0.0.0"
+dependencies = [
+ "rand",
+ "rand_xorshift",
+]
+
+[[package]]
+name = "dlmalloc"
+version = "0.2.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3264b043b8e977326c1ee9e723da2c1f8d09a99df52cacf00b4dbce5ac54414d"
+dependencies = [
+ "cfg-if",
+ "compiler_builtins",
+ "libc",
+ "rustc-std-workspace-core",
+ "windows-sys",
+]
+
+[[package]]
+name = "fortanix-sgx-abi"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57cafc2274c10fab234f176b25903ce17e690fca7597090d50880e047a0389c5"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "getopts"
+version = "0.2.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "14dbbfd5c71d70241ecf9e6f13737f7b5ce823821063188d7e46c41d371eebd5"
+dependencies = [
+ "rustc-std-workspace-core",
+ "rustc-std-workspace-std",
+ "unicode-width",
+]
+
+[[package]]
+name = "gimli"
+version = "0.28.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4271d37baee1b8c7e4b708028c57d816cf9d2434acb33a549475f78c181f6253"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-alloc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "gimli"
+version = "0.29.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "40ecd4077b5ae9fd2e9e169b102c6c330d0605168eb0e8bf79952b256dbefffd"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-alloc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.14.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1"
+dependencies = [
+ "allocator-api2",
+ "compiler_builtins",
+ "rustc-std-workspace-alloc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "hermit-abi"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fbf6a919d6cf397374f7dfeeea91d974c7c0a7221d0d0f4f20d859d329e53fcc"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-alloc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "libc"
+version = "0.2.158"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d8adc4bb1803a324070e64a98ae98f38934d91957a99cfb3a43dcbc01bc56439"
+dependencies = [
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "memchr"
+version = "2.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "miniz_oxide"
+version = "0.7.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b8a240ddb74feaf34a79a7add65a741f3167852fba007066dcac1ca548d89c08"
+dependencies = [
+ "adler",
+ "compiler_builtins",
+ "rustc-std-workspace-alloc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "object"
+version = "0.36.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f203fa8daa7bb185f760ae12bd8e097f63d17041dcdcaf675ac54cdf863170e"
+dependencies = [
+ "compiler_builtins",
+ "memchr",
+ "rustc-std-workspace-alloc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "panic_abort"
+version = "0.0.0"
+dependencies = [
+ "alloc",
+ "cfg-if",
+ "compiler_builtins",
+ "core",
+ "libc",
+]
+
+[[package]]
+name = "panic_unwind"
+version = "0.0.0"
+dependencies = [
+ "alloc",
+ "cfg-if",
+ "compiler_builtins",
+ "core",
+ "libc",
+ "unwind",
+]
+
+[[package]]
+name = "proc_macro"
+version = "0.0.0"
+dependencies = [
+ "core",
+ "std",
+]
+
+[[package]]
+name = "profiler_builtins"
+version = "0.0.0"
+dependencies = [
+ "cc",
+ "compiler_builtins",
+ "core",
+]
+
+[[package]]
+name = "r-efi"
+version = "4.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e9e935efc5854715dfc0a4c9ef18dc69dee0ec3bf9cc3ab740db831c0fdd86a3"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "r-efi-alloc"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "31d6f09fe2b6ad044bc3d2c34ce4979796581afd2f1ebc185837e02421e02fd7"
+dependencies = [
+ "compiler_builtins",
+ "r-efi",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "rand"
+version = "0.8.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
+dependencies = [
+ "rand_core",
+]
+
+[[package]]
+name = "rand_core"
+version = "0.6.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
+
+[[package]]
+name = "rand_xorshift"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d25bf25ec5ae4a3f1b92f929810509a2f53d7dca2f50b794ff57e3face536c8f"
+dependencies = [
+ "rand_core",
+]
+
+[[package]]
+name = "rustc-demangle"
+version = "0.1.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "rustc-std-workspace-alloc"
+version = "1.99.0"
+dependencies = [
+ "alloc",
+]
+
+[[package]]
+name = "rustc-std-workspace-core"
+version = "1.99.0"
+dependencies = [
+ "core",
+]
+
+[[package]]
+name = "rustc-std-workspace-std"
+version = "1.99.0"
+dependencies = [
+ "std",
+]
+
+[[package]]
+name = "std"
+version = "0.0.0"
+dependencies = [
+ "addr2line",
+ "alloc",
+ "cfg-if",
+ "compiler_builtins",
+ "core",
+ "dlmalloc",
+ "fortanix-sgx-abi",
+ "hashbrown",
+ "hermit-abi",
+ "libc",
+ "miniz_oxide",
+ "object",
+ "panic_abort",
+ "panic_unwind",
+ "profiler_builtins",
+ "r-efi",
+ "r-efi-alloc",
+ "rand",
+ "rand_xorshift",
+ "rustc-demangle",
+ "std_detect",
+ "unwind",
+ "wasi",
+ "windows-targets 0.0.0",
+]
+
+[[package]]
+name = "std_detect"
+version = "0.1.5"
+dependencies = [
+ "cfg-if",
+ "compiler_builtins",
+ "libc",
+ "rustc-std-workspace-alloc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "sysroot"
+version = "0.0.0"
+dependencies = [
+ "proc_macro",
+ "std",
+ "test",
+]
+
+[[package]]
+name = "test"
+version = "0.0.0"
+dependencies = [
+ "core",
+ "getopts",
+ "libc",
+ "std",
+]
+
+[[package]]
+name = "unicode-width"
+version = "0.1.13"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0336d538f7abc86d282a4189614dfaa90810dfc2c6f6427eaf88e16311dd225d"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-core",
+ "rustc-std-workspace-std",
+]
+
+[[package]]
+name = "unwind"
+version = "0.0.0"
+dependencies = [
+ "cfg-if",
+ "compiler_builtins",
+ "core",
+ "libc",
+ "unwinding",
+]
+
+[[package]]
+name = "unwinding"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "37a19a21a537f635c16c7576f22d0f2f7d63353c1337ad4ce0d8001c7952a25b"
+dependencies = [
+ "compiler_builtins",
+ "gimli 0.28.1",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "wasi"
+version = "0.11.0+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
+dependencies = [
+ "compiler_builtins",
+ "rustc-std-workspace-alloc",
+ "rustc-std-workspace-core",
+]
+
+[[package]]
+name = "windows-sys"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
+dependencies = [
+ "windows-targets 0.52.5",
+]
+
+[[package]]
+name = "windows-targets"
+version = "0.0.0"
+
+[[package]]
+name = "windows-targets"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb"
+dependencies = [
+ "windows_aarch64_gnullvm",
+ "windows_aarch64_msvc",
+ "windows_i686_gnu",
+ "windows_i686_gnullvm",
+ "windows_i686_msvc",
+ "windows_x86_64_gnu",
+ "windows_x86_64_gnullvm",
+ "windows_x86_64_msvc",
+]
+
+[[package]]
+name = "windows_aarch64_gnullvm"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263"
+
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6"
+
+[[package]]
+name = "windows_i686_gnu"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670"
+
+[[package]]
+name = "windows_i686_gnullvm"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9"
+
+[[package]]
+name = "windows_i686_msvc"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf"
+
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9"
+
+[[package]]
+name = "windows_x86_64_gnullvm"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596"
+
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0"

From b2f84d7c25bfc9742077a1765386374f316ba8e3 Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Tue, 22 Oct 2024 12:56:20 -0400
Subject: [PATCH 20/23] Address PR comments

---
 scripts/run-kani.sh               |  3 +--
 scripts/run_update_with_checks.sh | 44 +++++++++++++++----------------
 2 files changed, 23 insertions(+), 24 deletions(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 70e0d682ad9ea..15277f5ff1ad4 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -47,7 +47,6 @@ if [[ -n "$path" ]]; then
     if [[ ! -d "$path" ]]; then
         echo "Error: Specified directory does not exist."
         usage
-        exit 1
     fi
     WORK_DIR=$(realpath "$path")
 else
@@ -133,7 +132,7 @@ run_kani_command() {
 check_binary_exists() {
     local build_dir="$1"
     local expected_commit="$2"
-    local kani_path="$build_dir/scripts/kani"
+    local kani_path=$(get_kani_path "$build_dir")
 
     if [[ -f "$kani_path" ]]; then
         local current_commit=$(get_current_commit "$build_dir")
diff --git a/scripts/run_update_with_checks.sh b/scripts/run_update_with_checks.sh
index 03c4d1657a911..e7419f34d4901 100755
--- a/scripts/run_update_with_checks.sh
+++ b/scripts/run_update_with_checks.sh
@@ -135,47 +135,47 @@ fi
 
 echo "------------------------------------"
 # Call the first script to update the subtree
-echo "Update subtree in main"
+echo "Update subtree in Main"
 source $BASE_HOME_DIR/scripts/pull_from_upstream.sh "$TEMP_HOME_DIR" $TOOLCHAIN_DATE $COMMIT_HASH
-pull_from_upstream=("$?")
-if [ "${#pull_from_upstream[@]}" -eq 0 ]; then
-    echo "pull_from_upstream.sh failed to run."
+OUTPUT_SCRIPT1=("$?")
+if [ "${#OUTPUT_SCRIPT1[@]}" -eq 0 ]; then
+    echo "script1.sh failed to run."
     exit 1
 else
-    echo "Pulled from upstream succesfully."
+    echo "script1.sh completed successfully."
 fi
 
 # Call the second script
-echo "Updating toolchain..."
+echo "Running script2.sh..."
 source $BASE_HOME_DIR/scripts/update_toolchain_date.sh "$TEMP_HOME_DIR" "$TOOLCHAIN_DATE"
-update_toolchain_date=("$?")
-if [ "${#update_toolchain_date[@]}" -eq 0 ]; then
-    echo "update_toolchain_date.sh failed to run."
+OUTPUT_SCRIPT2=("$?")
+if [ "${#OUTPUT_SCRIPT2[@]}" -eq 0 ]; then
+    echo "script2.sh failed to run."
     exit 1
 else
-    echo "Toolchain updated succesfully."
+    echo "Update toolchain ran successfully."
 fi
 
 # Call the third script
-echo "echo "Checking compatiblity with kani..."
+echo "Running script3.sh..."
 source $BASE_HOME_DIR/scripts/check_rustc.sh "$TEMP_HOME_DIR"
-check_rustc=("$?")
-if [ "${#check_rustc[@]}" -eq 0 ]; then
-    echo "check_rustc.sh failed to run."
+OUTPUT_SCRIPT3=("$?")
+if [ "${#OUTPUT_SCRIPT3[@]}" -eq 0 ]; then
+    echo "script3.sh failed to run."
     exit 1
 else
-    echo "Changes compatible with latest rustc."
+    echo "script3.sh completed successfully."
 fi
 
-# Checking compatiblity with kani
-echo "Checking compatiblity with kani..."
-source $BASE_HOME_DIR/run-kani.sh "$TEMP_HOME_DIR"
-run_kani=("$?")
-if [ "${#run_kani[@]}" -eq 0 ]; then
-    echo "run_kani.sh failed to run."
+# Call the fourth script
+echo "Running script4.sh..."
+source $BASE_HOME_DIR/scripts/check_kani.sh "$TEMP_HOME_DIR"
+OUTPUT_SCRIPT4=("$?")
+if [ "${#OUTPUT_SCRIPT4[@]}" -eq 0 ]; then
+    echo "script4.sh failed to run."
     exit 1
 else
-    echo "Changes compatible with kani's features/verify-std branch."
+    echo "script4.sh completed successfully."
 fi
 
 # TODO: Issue a Pull Request from the sync branch of the temp repo

From 525ba7e38053e437f5f0df43fdcab25d66eb36d4 Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Tue, 22 Oct 2024 12:58:35 -0400
Subject: [PATCH 21/23] Fix build jobs names

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

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 39836a5140601..ebb829a75e866 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -16,7 +16,7 @@ defaults:
 
 jobs:
   check-kani-on-std:
-    name: Verify Rust Code (Default Configuration)
+    name: Verify std Code with Kani
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
@@ -35,11 +35,11 @@ jobs:
           submodules: true
 
       # Step 2: Run Kani on the std library (default configuration)
-      - name: Run Kani Verification (Default)
+      - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 
   test-kani-script:
-    name: Verify Rust Code (Custom Configuration)
+    name: Test Kani Script
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:

From 56845d96627a1fc7dd0346553391ab5758567f05 Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Tue, 22 Oct 2024 13:04:04 -0400
Subject: [PATCH 22/23] Rename steps

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

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index ebb829a75e866..6dec32c1620ec 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -1,4 +1,4 @@
-name: Kani Rust Verification
+name: Kani
 
 on:
   workflow_dispatch:
@@ -16,7 +16,7 @@ defaults:
 
 jobs:
   check-kani-on-std:
-    name: Verify std Code with Kani
+    name: Verify std library
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
@@ -39,7 +39,7 @@ jobs:
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 
   test-kani-script:
-    name: Test Kani Script
+    name: Test Kani script
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
@@ -58,10 +58,10 @@ jobs:
           submodules: true
 
       # Step 2: Test Kani verification script with specific arguments
-      - name: Run Kani Verification (Custom Args)
+      - name: Test Kani script (Custom Args)
         run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse
 
       # Step 3: Test Kani verification script in the repository directory
-      - name: Run Kani Verification (In Repo Directory)
+      - name: Test Kani script (In Repo Directory)
         working-directory: ${{github.workspace}}/head
         run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse

From d348149f3ada56c0da3300b25ce828276fb3704a Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Wed, 23 Oct 2024 14:37:56 -0400
Subject: [PATCH 23/23] Update branch commit ID and add git submodule update in
 case of local copies not doing it.

---
 scripts/run-kani.sh           | 1 +
 tool_config/kani-version.toml | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 15277f5ff1ad4..8ce27dac5d207 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -113,6 +113,7 @@ build_kani() {
         echo "Unknown operating system"
     fi
 
+    git submodule update --init --recursive
     cargo build-dev --release
     popd
 }
diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml
index 2a42cd37544ef..59b19da6a5958 100644
--- a/tool_config/kani-version.toml
+++ b/tool_config/kani-version.toml
@@ -2,4 +2,4 @@
 # incomaptible with the verify-std repo.
 
 [kani]
-commit = "1c38609ec35f591898b94ec39427d1b5b0cad824"
+commit = "5f8f513d297827cfdce4c48065e51973ba563068"