Merge branch 'main' into daniel/byte_operation

Author: danielhumanmod

.gitignore

@@ -20,6 +20,7 @@ Session.vim
 /book/
 /build/
 /target
+library/target
 *.rlib
 *.rmeta
 *.mir

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.

doc/src/SUMMARY.md

@@ -3,8 +3,8 @@
 [Introduction](intro.md)
 
 - [General Rules](./general-rules.md)
-  - [Challenge Template](./template.md)
-  - [Tool application](./todo.md)
+  - [Challenge Template](./challenge_template.md)
+  - [Tool Application Template](./tool_template.md)
 
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)

doc/src/template.md renamed to doc/src/challenge_template.md

@@ -39,7 +39,7 @@ A proposed solution to a verification problem will only **be reviewed** if all t
 * The contribution must be automated and should be checked and pass as part of the PR checks.
 * All tools used by the solution must be in [the list of accepted tools](tools.md#approved-tools),
   and previously integrated in the repository.
-  If that is not the case, please submit a separate [tool application first](todo.md).
+  If that is not the case, please submit a separate [tool application first](./general-rules.md#tool-applications).
 * There is no restriction on the number of contributors for a solution.
   Make sure you have the rights to submit your solution and that all contributors are properly mentioned.
 * The solution cannot impact the runtime logic of the standard library unless the change is proposed and incorporated
@@ -56,7 +56,7 @@ The type of obstacles users face may depend on which part of the standard librar
 Everyone is welcome to submit new challenge proposals for review by our committee.
 Follow the following steps to create a new proposal:
 
-1. Create a tracking issue using the Issue template [Challenge Proposal](template.md) for your challenge.
+1. Create a tracking issue using the [challenge template](./challenge_template.md) for your challenge.
 2. In your fork of this repository do the following:
     1. Copy the template file (`book/src/challenge_template.md`) to `book/src/challenges/<ID_NUMBER>-<challenge-name>.md`.
     2. Fill in the details according to the template instructions.
@@ -69,7 +69,7 @@ Follow the following steps to create a new proposal:
 
 Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools):
 
-* Any new tool that participants want to enable will require an application using the Issue template [Tool application](todo.md).
+* Any new tool that participants want to enable will require an application using the [tool application template](./tool_template.md).
 * The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS
 * A new tool application should clearly specify the differences to existing techniques and provide sufficient background
   of why this is needed.

doc/src/general-rules.md

@@ -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"] }

doc/src/todo.md

@@ -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)]

.github/TOOL_REQUEST_TEMPLATE.md renamed to doc/src/tool_template.md

@@ -511,6 +511,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_add(rhs).1)]
         pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -663,6 +664,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
         pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -815,6 +817,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(!self.overflowing_mul(rhs).1)]
         pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1164,6 +1167,8 @@ macro_rules! int_impl {
         #[rustc_const_unstable(feature = "unchecked_neg", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(self != $SelfT::MIN)]
+        #[ensures(|result| *result == -self)]
         pub const unsafe fn unchecked_neg(self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1297,6 +1302,7 @@ macro_rules! int_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < <$ActualT>::BITS)] 
         pub const unsafe fn unchecked_shl(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -1423,6 +1429,7 @@ macro_rules! int_impl {
         #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+        #[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
         pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,
@@ -2153,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
@@ -2183,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