Merge remote-tracking branch 'origin/main' into verify-intrinsics

Author: celinval

.github/workflows/kani.yml

@@ -1,6 +1,5 @@
-# This workflow is responsible for verifying the standard library with Kani.
-
 name: Kani
+
 on:
   workflow_dispatch:
   pull_request:
@@ -9,30 +8,60 @@ on:
     paths:
       - 'library/**'
       - '.github/workflows/kani.yml'
-      - 'scripts/check_kani.sh'
+      - 'scripts/run-kani.sh'
 
 defaults:
   run:
     shell: bash
 
 jobs:
-  build:
+  check-kani-on-std:
+    name: Verify std library
     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
+      # Step 1: Check out the repository
+      - name: Checkout Repository
         uses: actions/checkout@v4
         with:
           path: head
           submodules: true
 
-      - name: Run Kani Script
-        run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head
+      # Step 2: Run Kani on the std library (default configuration)
+      - name: Run Kani Verification
+        run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
+
+  test-kani-script:
+    name: Test Kani script
+    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: 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: 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

.gitignore

@@ -19,6 +19,7 @@ Session.vim
 ## Build
 /book/
 /build/
+/kani_build/
 /target
 library/target
 *.rlib

README.md

@@ -47,4 +47,4 @@ See [the Rust repository](https://github.com/rust-lang/rust) for details.
 
 ## Introducing a New Tool
 
-Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool.
+Please use the [template available in this repository](./doc/src/tool_template.md) to introduce a new verification tool.

library/alloc/Cargo.toml

@@ -11,6 +11,7 @@ edition = "2021"
 [dependencies]
 core = { path = "../core" }
 compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] }
+safety = { path = "../contracts/safety" }
 
 [dev-dependencies]
 rand = { version = "0.8.5", default-features = false, features = ["alloc"] }

library/alloc/src/lib.rs

@@ -91,6 +91,7 @@
 //
 // Library features:
 // tidy-alphabetical-start
+#![cfg_attr(kani, feature(kani))]
 #![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))]
 #![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))]
 #![feature(alloc_layout_extra)]

library/core/src/num/int_macros.rs

@@ -2160,6 +2160,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[rustc_allow_const_fn_unstable(unchecked_shifts)]
+        #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
         pub const fn wrapping_shl(self, rhs: u32) -> Self {
             // SAFETY: the masking by the bitsize of the type ensures that we do not shift
             // out of bounds
@@ -2190,6 +2191,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[rustc_allow_const_fn_unstable(unchecked_shifts)]
+        #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
         pub const fn wrapping_shr(self, rhs: u32) -> Self {
             // SAFETY: the masking by the bitsize of the type ensures that we do not shift
             // out of bounds

library/core/src/num/mod.rs

@@ -1657,6 +1657,51 @@ mod verify {
             }
         }
     }
+    
+    /// A macro to generate Kani proof harnesses for the `carrying_mul` method,
+    ///
+    /// The macro creates multiple harnesses for different ranges of input values,
+    /// allowing testing of both small and large inputs.
+    ///
+    /// # Parameters:
+    /// - `$type`: The integer type (e.g., u8, u16) for which the `carrying_mul` function is being tested.
+    /// - `$wide_type`: A wider type to simulate the multiplication (e.g., u16 for u8, u32 for u16).
+    /// - `$harness_name`: The name of the Kani harness to be generated.
+    /// - `$min`: The minimum value for the range of inputs for `lhs`, `rhs`, and `carry_in`.
+    /// - `$max`: The maximum value for the range of inputs for `lhs`, `rhs`, and `carry_in`.
+    macro_rules! generate_carrying_mul_intervals {
+        ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
+            $(
+                #[kani::proof]
+                pub fn $harness_name() {
+                    let lhs: $type = kani::any::<$type>();
+                    let rhs: $type = kani::any::<$type>();
+                    let carry_in: $type = kani::any::<$type>();
+    
+                    kani::assume(lhs >= $min && lhs <= $max);
+                    kani::assume(rhs >= $min && rhs <= $max);
+                    kani::assume(carry_in >= $min && carry_in <= $max);
+    
+                    // Perform the carrying multiplication
+                    let (result, carry_out) = lhs.carrying_mul(rhs, carry_in);
+    
+                    // Manually compute the expected result and carry using wider type
+                    let wide_result = (lhs as $wide_type)
+                        .wrapping_mul(rhs as $wide_type)
+                        .wrapping_add(carry_in as $wide_type);
+    
+                    let expected_result = wide_result as $type;
+                    let expected_carry = (wide_result >> <$type>::BITS) as $type;
+    
+                    // Assert the result and carry are correct
+                    assert_eq!(result, expected_result);
+                    assert_eq!(carry_out, expected_carry);
+                }
+            )+
+        }
+    }
+    
+    
 
     // Part 2 : Nested unsafe functions Generation Macros --> https://github.com/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md
 
@@ -1687,6 +1732,19 @@ mod verify {
         }
     }
 
+    // Verify `wrapping_{shl, shr}` which internally uses `unchecked_{shl,shr}`
+    macro_rules! generate_wrapping_shift_harness {
+        ($type:ty, $method:ident, $harness_name:ident) => {
+            #[kani::proof_for_contract($type::$method)]
+            pub fn $harness_name() {
+                let num1: $type = kani::any::<$type>();
+                let num2: u32 = kani::any::<u32>();
+
+                let _ = num1.$method(num2);
+            }
+        }
+    }
+
     // `unchecked_add` proofs
     //
     // Target types:
@@ -1728,7 +1786,7 @@ mod verify {
     generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128);
     generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize);
 
-    // unchecked_mul proofs
+    // `unchecked_mul` proofs
     //
     // Target types:
     // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total, with different interval checks for each.
@@ -1879,8 +1937,37 @@ mod verify {
     generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128);
     generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize);
 
+
+    // Part_2 `carrying_mul` proofs 
+    // 
+    // ====================== u8 Harnesses ======================
+    /// Kani proof harness for `carrying_mul` on `u8` type with full range of values.
+    generate_carrying_mul_intervals!(u8, u16,
+        carrying_mul_u8_full_range, 0u8, u8::MAX
+    );
+
+    // ====================== u16 Harnesses ======================
+    /// Kani proof harness for `carrying_mul` on `u16` type with full range of values.
+    generate_carrying_mul_intervals!(u16, u32,
+        carrying_mul_u16_full_range, 0u16, u16::MAX
+    );
+
+    // ====================== u32 Harnesses ======================
+    generate_carrying_mul_intervals!(u32, u64,
+        carrying_mul_u32_small, 0u32, 10u32,
+        carrying_mul_u32_large, u32::MAX - 10u32, u32::MAX,
+        carrying_mul_u32_mid_edge, (u32::MAX / 2) - 10u32, (u32::MAX / 2) + 10u32
+    );
+
+    // ====================== u64 Harnesses ======================
+    generate_carrying_mul_intervals!(u64, u128,
+        carrying_mul_u64_small, 0u64, 10u64,
+        carrying_mul_u64_large, u64::MAX - 10u64, u64::MAX,
+        carrying_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64
+    );
+
 
-    // Part 2 : Proof harnesses 
+    // Part_2 `widening_mul` proofs
 
     // ====================== u8 Harnesses ======================
     generate_widening_mul_intervals!(u8, u16, widening_mul_u8, 0u8, u8::MAX);
@@ -1905,4 +1992,55 @@ mod verify {
         widening_mul_u64_large, u64::MAX - 10u64, u64::MAX,
         widening_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64
     );
+
+    // Part_2 `wrapping_shl` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
+    //
+    // Target function:
+    // pub const fn wrapping_shl(self, rhs: u32) -> Self
+    //
+    // This function performs an panic-free bitwise left shift operation.
+    generate_wrapping_shift_harness!(i8, wrapping_shl, checked_wrapping_shl_i8);
+    generate_wrapping_shift_harness!(i16, wrapping_shl, checked_wrapping_shl_i16);
+    generate_wrapping_shift_harness!(i32, wrapping_shl, checked_wrapping_shl_i32);
+    generate_wrapping_shift_harness!(i64, wrapping_shl, checked_wrapping_shl_i64);
+    generate_wrapping_shift_harness!(i128, wrapping_shl, checked_wrapping_shl_i128);
+    generate_wrapping_shift_harness!(isize, wrapping_shl, checked_wrapping_shl_isize);
+    generate_wrapping_shift_harness!(u8, wrapping_shl, checked_wrapping_shl_u8);
+    generate_wrapping_shift_harness!(u16, wrapping_shl, checked_wrapping_shl_u16);
+    generate_wrapping_shift_harness!(u32, wrapping_shl, checked_wrapping_shl_u32);
+    generate_wrapping_shift_harness!(u64, wrapping_shl, checked_wrapping_shl_u64);
+    generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128);
+    generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize);
+
+    // Part_2 `wrapping_shr` proofs
+    //
+    // Target types:
+    // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
+    //
+    // Target contracts:
+    // #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
+    // Target function:
+    // pub const fn wrapping_shr(self, rhs: u32) -> Self {
+    //
+    // This function performs an panic-free bitwise right shift operation.
+    generate_wrapping_shift_harness!(i8, wrapping_shr, checked_wrapping_shr_i8);
+    generate_wrapping_shift_harness!(i16, wrapping_shr, checked_wrapping_shr_i16);
+    generate_wrapping_shift_harness!(i32, wrapping_shr, checked_wrapping_shr_i32);
+    generate_wrapping_shift_harness!(i64, wrapping_shr, checked_wrapping_shr_i64);
+    generate_wrapping_shift_harness!(i128, wrapping_shr, checked_wrapping_shr_i128);
+    generate_wrapping_shift_harness!(isize, wrapping_shr, checked_wrapping_shr_isize);
+    generate_wrapping_shift_harness!(u8, wrapping_shr, checked_wrapping_shr_u8);
+    generate_wrapping_shift_harness!(u16, wrapping_shr, checked_wrapping_shr_u16);
+    generate_wrapping_shift_harness!(u32, wrapping_shr, checked_wrapping_shr_u32);
+    generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64);
+    generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128);
+    generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);
+
 }
+

library/core/src/num/uint_macros.rs

@@ -2138,6 +2138,7 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[rustc_allow_const_fn_unstable(unchecked_shifts)]
+        #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
         pub const fn wrapping_shl(self, rhs: u32) -> Self {
             // SAFETY: the masking by the bitsize of the type ensures that we do not shift
             // out of bounds
@@ -2171,6 +2172,7 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline(always)]
         #[rustc_allow_const_fn_unstable(unchecked_shifts)]
+        #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
         pub const fn wrapping_shr(self, rhs: u32) -> Self {
             // SAFETY: the masking by the bitsize of the type ensures that we do not shift
             // out of bounds

library/std/Cargo.toml

@@ -26,6 +26,7 @@ hashbrown = { version = "0.14", default-features = false, features = [
 std_detect = { path = "../stdarch/crates/std_detect", default-features = false, features = [
     'rustc-dep-of-std',
 ] }
+safety = { path = "../contracts/safety" }
 
 # Dependencies of the `backtrace` crate
 rustc-demangle = { version = "0.1.24", features = ['rustc-dep-of-std'] }

library/std/src/lib.rs

@@ -269,6 +269,7 @@
 #![cfg_attr(any(windows, target_os = "uefi"), feature(round_char_boundary))]
 #![cfg_attr(target_family = "wasm", feature(stdarch_wasm_atomic_wait))]
 #![cfg_attr(target_arch = "wasm64", feature(simd_wasm64))]
+#![cfg_attr(kani, feature(kani))]
 //
 // Language features:
 // tidy-alphabetical-start