From 9f4fc302e229d4c96cb4c670ba06179edc1e232e Mon Sep 17 00:00:00 2001
From: Matias Scharager <matias.scharager@gmail.com>
Date: Wed, 5 Jun 2024 14:17:53 -0400
Subject: [PATCH 1/5] Change ensures into closures (#3207)

This change now separates the front facing "result" name and the
internal facing "result_kani_internal" ident where the user can specify
with the keyword "result" but then the system replaces this with the
internal representation.

If the user chooses to use a different variable name than result, this
now supports the syntax of
`#[kani::ensures(|result_var| expr)]`
where result_var can be any arbitrary name.

For example, the following test now works:
```
#[kani::ensures(|banana : &u32| *banana == a.wrapping_add(b))]
fn simple_addition(a: u32, b: u32) -> u32 {
    return a.wrapping_add(b);
}
```

In addition, the string "result_kani_internal" is now a global constant
and can be updated in a single place if needed.

Resolves #2597 since the user can specify the variable name they want
within the ensures binding

An important change is that the result is now a pass by reference
instead, so as in the example an `&u32` instead of `u32`

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

---------

Co-authored-by: Matias Scharager <mscharag@amazon.com>
---
 library/kani/src/contracts.rs                 | 10 ++--
 library/kani_macros/src/lib.rs                | 10 ++--
 .../src/sysroot/contracts/bootstrap.rs        | 12 ++--
 .../src/sysroot/contracts/check.rs            | 12 ++--
 .../src/sysroot/contracts/initialize.rs       | 28 +++++----
 .../kani_macros/src/sysroot/contracts/mod.rs  | 58 ++++++++++---------
 .../src/sysroot/contracts/replace.rs          | 18 +++---
 .../src/sysroot/contracts/shared.rs           |  4 +-
 rfc/src/rfcs/0009-function-contracts.md       | 23 ++++----
 .../arbitrary_ensures_fail.expected           |  2 +-
 .../arbitrary_ensures_fail.rs                 |  2 +-
 .../arbitrary_ensures_pass.expected           |  2 +-
 .../arbitrary_ensures_pass.rs                 |  2 +-
 .../arbitrary_requires_fail.rs                |  2 +-
 .../function-contract/attribute_complain.rs   |  2 +-
 .../attribute_no_complain.rs                  |  2 +-
 .../checking_from_external_mod.expected       |  2 +-
 .../checking_from_external_mod.rs             |  2 +-
 .../checking_in_impl.expected                 |  2 +-
 .../function-contract/checking_in_impl.rs     |  2 +-
 .../function-contract/fail_on_two.expected    |  4 +-
 .../expected/function-contract/fail_on_two.rs |  4 +-
 .../gcd_failure_code.expected                 |  4 +-
 .../function-contract/gcd_failure_code.rs     |  2 +-
 .../gcd_failure_contract.expected             |  4 +-
 .../function-contract/gcd_failure_contract.rs |  4 +-
 .../gcd_rec_code_fail.expected                |  2 +-
 .../function-contract/gcd_rec_code_fail.rs    |  2 +-
 .../gcd_rec_comparison_pass.expected          |  2 +-
 .../gcd_rec_comparison_pass.rs                |  2 +-
 .../gcd_rec_contract_fail.expected            |  2 +-
 .../gcd_rec_contract_fail.rs                  |  2 +-
 .../gcd_rec_replacement_pass.rs               |  2 +-
 .../gcd_rec_simple_pass.expected              |  2 +-
 .../function-contract/gcd_rec_simple_pass.rs  |  2 +-
 .../function-contract/gcd_replacement_fail.rs |  2 +-
 .../function-contract/gcd_replacement_pass.rs |  2 +-
 .../function-contract/gcd_success.expected    |  2 +-
 .../expected/function-contract/gcd_success.rs |  2 +-
 .../modifies/check_only_verification.rs       |  2 +-
 .../function-contract/modifies/expr_pass.rs   |  2 +-
 .../modifies/expr_replace_pass.rs             |  2 +-
 .../modifies/fail_missing_recursion_attr.rs   |  2 +-
 .../modifies/field_replace_pass.rs            |  2 +-
 .../modifies/global_replace_pass.rs           |  2 +-
 .../function-contract/modifies/havoc_pass.rs  |  2 +-
 .../modifies/havoc_pass_reordered.rs          |  2 +-
 .../modifies/mistake_condition_return.rs      |  4 +-
 .../modifies/unique_arguments.rs              |  4 +-
 .../modifies/vec_pass.expected                |  2 +-
 .../function-contract/modifies/vec_pass.rs    |  2 +-
 .../expected/function-contract/pattern_use.rs |  2 +-
 .../prohibit-pointers/allowed_const_ptr.rs    |  2 +-
 .../prohibit-pointers/allowed_mut_ref.rs      |  2 +-
 .../allowed_mut_return_ref.rs                 |  2 +-
 .../prohibit-pointers/allowed_ref.rs          |  2 +-
 .../prohibit-pointers/hidden.rs               |  2 +-
 .../prohibit-pointers/plain_pointer.rs        |  2 +-
 .../prohibit-pointers/return_pointer.rs       |  2 +-
 .../simple_ensures_fail.expected              |  4 +-
 .../function-contract/simple_ensures_fail.rs  |  2 +-
 .../simple_ensures_pass.expected              |  2 +-
 .../function-contract/simple_ensures_pass.rs  |  2 +-
 .../function-contract/simple_replace_fail.rs  |  2 +-
 .../function-contract/simple_replace_pass.rs  |  2 +-
 .../type_annotation_needed.rs                 |  2 +-
 tests/std-checks/core/src/ptr.rs              |  4 +-
 67 files changed, 161 insertions(+), 148 deletions(-)

diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs
index 4f963038cab9..65b9ec7c01cc 100644
--- a/library/kani/src/contracts.rs
+++ b/library/kani/src/contracts.rs
@@ -51,14 +51,14 @@
 //! approximation of the result of division for instance could be this:
 //!
 //! ```
-//! #[ensures(result <= dividend)]
+//! #[ensures(|result : &u32| *result <= dividend)]
 //! ```
 //!
 //! This is called a postcondition and it also has access to the arguments and
 //! is expressed in regular Rust code. The same restrictions apply as did for
-//! [`requires`][macro@requires]. In addition to the arguments the postcondition
-//! also has access to the value returned from the function in a variable called
-//! `result`.
+//! [`requires`][macro@requires]. In addition to the postcondition is expressed
+//! as a closure where the value returned from the function is passed to this
+//! closure by reference.
 //!
 //! You may combine as many [`requires`][macro@requires] and
 //! [`ensures`][macro@ensures] attributes on a single function as you please.
@@ -67,7 +67,7 @@
 //!
 //! ```
 //! #[kani::requires(divisor != 0)]
-//! #[kani::ensures(result <= dividend)]
+//! #[kani::ensures(|result : &u32| *result <= dividend)]
 //! fn my_div(dividend: u32, divisor: u32) -> u32 {
 //!   dividend / divisor
 //! }
diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs
index 0991730f8802..44a0ca78ea41 100644
--- a/library/kani_macros/src/lib.rs
+++ b/library/kani_macros/src/lib.rs
@@ -131,11 +131,11 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
 /// This is part of the function contract API, for more general information see
 /// the [module-level documentation](../kani/contracts/index.html).
 ///
-/// The contents of the attribute is a condition over the input values to the
-/// annotated function *and* its return value, accessible as a variable called
-/// `result`. All Rust syntax is supported, even calling other functions, but
-/// the computations must be side effect free, e.g. it cannot perform I/O or use
-/// mutable memory.
+/// The contents of the attribute is a closure that captures the input values to
+/// the annotated function and the input to the function is the return value of
+/// the function passed by reference. All Rust syntax is supported, even calling
+/// other functions, but the computations must be side effect free, e.g. it
+/// cannot perform I/O or use mutable memory.
 ///
 /// Kani requires each function that uses a contract (this attribute or
 /// [`requires`][macro@requires]) to have at least one designated
diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
index 8d930fdebda9..7c35cc469254 100644
--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -4,11 +4,14 @@
 //! Special way we handle the first time we encounter a contract attribute on a
 //! function.
 
-use proc_macro2::Span;
+use proc_macro2::{Ident, Span};
 use quote::quote;
 use syn::ItemFn;
 
-use super::{helpers::*, shared::identifier_for_generated_function, ContractConditionsHandler};
+use super::{
+    helpers::*, shared::identifier_for_generated_function, ContractConditionsHandler,
+    INTERNAL_RESULT_IDENT,
+};
 
 impl<'a> ContractConditionsHandler<'a> {
     /// The complex case. We are the first time a contract is handled on this function, so
@@ -80,6 +83,7 @@ impl<'a> ContractConditionsHandler<'a> {
             (quote!(#check_fn_name), quote!(#replace_fn_name))
         };
 
+        let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
         self.output.extend(quote!(
             #[allow(dead_code, unused_variables)]
             #[kanitool::is_contract_generated(recursion_wrapper)]
@@ -89,9 +93,9 @@ impl<'a> ContractConditionsHandler<'a> {
                     #call_replace(#(#args),*)
                 } else {
                     unsafe { REENTRY = true };
-                    let result = #call_check(#(#also_args),*);
+                    let #result = #call_check(#(#also_args),*);
                     unsafe { REENTRY = false };
-                    result
+                    #result
                 }
             }
         ));
diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs
index 516bd187ba7f..473535e8d8fd 100644
--- a/library/kani_macros/src/sysroot/contracts/check.rs
+++ b/library/kani_macros/src/sysroot/contracts/check.rs
@@ -10,7 +10,7 @@ use syn::{Expr, FnArg, ItemFn, Token};
 use super::{
     helpers::*,
     shared::{make_unsafe_argument_copies, try_as_result_assign_mut},
-    ContractConditionsData, ContractConditionsHandler,
+    ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
 const WRAPPER_ARG_PREFIX: &str = "_wrapper_arg_";
@@ -46,14 +46,15 @@ impl<'a> ContractConditionsHandler<'a> {
                 assert!(matches!(
                     inner.pop(),
                     Some(syn::Stmt::Expr(syn::Expr::Path(pexpr), None))
-                        if pexpr.path.get_ident().map_or(false, |id| id == "result")
+                        if pexpr.path.get_ident().map_or(false, |id| id == INTERNAL_RESULT_IDENT)
                 ));
 
+                let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
                 quote!(
                     #arg_copies
                     #(#inner)*
                     #exec_postconditions
-                    result
+                    #result
                 )
             }
             ContractConditionsData::Modifies { attr } => {
@@ -95,9 +96,10 @@ impl<'a> ContractConditionsHandler<'a> {
             } else {
                 quote!(#wrapper_name)
             };
+            let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
             syn::parse_quote!(
-                let result : #return_type = #wrapper_call(#(#args),*);
-                result
+                let #result : #return_type = #wrapper_call(#(#args),*);
+                #result
             )
         } else {
             self.annotated_fn.block.stmts.clone()
diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs
index 6452ab9ace62..aee0c21bc82d 100644
--- a/library/kani_macros/src/sysroot/contracts/initialize.rs
+++ b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -7,12 +7,13 @@ use std::collections::{HashMap, HashSet};
 
 use proc_macro::{Diagnostic, TokenStream};
 use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
-use syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ItemFn, Signature};
+use quote::quote;
+use syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ExprClosure, ItemFn};
 
 use super::{
     helpers::{chunks_by, is_token_stream_2_comma, matches_path},
     ContractConditionsData, ContractConditionsHandler, ContractConditionsType,
-    ContractFunctionState,
+    ContractFunctionState, INTERNAL_RESULT_IDENT,
 };
 
 impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState {
@@ -81,7 +82,11 @@ impl<'a> ContractConditionsHandler<'a> {
                 ContractConditionsData::Requires { attr: syn::parse(attr)? }
             }
             ContractConditionsType::Ensures => {
-                ContractConditionsData::new_ensures(&annotated_fn.sig, syn::parse(attr)?)
+                let mut data: ExprClosure = syn::parse(attr)?;
+                let argument_names = rename_argument_occurrences(&annotated_fn.sig, &mut data);
+                let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+                let app: Expr = Expr::Verbatim(quote!((#data)(&#result)));
+                ContractConditionsData::Ensures { argument_names, attr: app }
             }
             ContractConditionsType::Modifies => {
                 ContractConditionsData::new_modifies(attr, &mut output)
@@ -92,16 +97,6 @@ impl<'a> ContractConditionsHandler<'a> {
     }
 }
 impl ContractConditionsData {
-    /// Constructs a [`Self::Ensures`] from the signature of the decorated
-    /// function and the contents of the decorating attribute.
-    ///
-    /// Renames the [`Ident`]s used in `attr` and stores the translation map in
-    /// `argument_names`.
-    fn new_ensures(sig: &Signature, mut attr: Expr) -> Self {
-        let argument_names = rename_argument_occurrences(sig, &mut attr);
-        ContractConditionsData::Ensures { argument_names, attr }
-    }
-
     /// Constructs a [`Self::Modifies`] from the contents of the decorating attribute.
     ///
     /// Responsible for parsing the attribute.
@@ -129,7 +124,10 @@ impl ContractConditionsData {
 /// - Creates new names for them;
 /// - Replaces all occurrences of those idents in `attrs` with the new names and;
 /// - Returns the mapping of old names to new names.
-fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap<Ident, Ident> {
+fn rename_argument_occurrences(
+    sig: &syn::Signature,
+    attr: &mut ExprClosure,
+) -> HashMap<Ident, Ident> {
     let mut arg_ident_collector = ArgumentIdentCollector::new();
     arg_ident_collector.visit_signature(&sig);
 
@@ -144,7 +142,7 @@ fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap
         .collect::<HashMap<_, _>>();
 
     let mut ident_rewriter = Renamer(&arg_idents);
-    ident_rewriter.visit_expr_mut(attr);
+    ident_rewriter.visit_expr_closure_mut(attr);
     arg_idents
 }
 
diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index 02d2b98eb8db..bef6f8d921bc 100644
--- a/library/kani_macros/src/sysroot/contracts/mod.rs
+++ b/library/kani_macros/src/sysroot/contracts/mod.rs
@@ -159,9 +159,9 @@
 //!         call_replace(fn args...)
 //!     } else {
 //!         unsafe { reentry = true };
-//!         let result = call_check(fn args...);
+//!         let result_kani_internal = call_check(fn args...);
 //!         unsafe { reentry = false };
-//!         result
+//!         result_kani_internal
 //!     }
 //! }
 //! ```
@@ -173,7 +173,7 @@
 //!
 //! ```
 //! #[kani::requires(divisor != 0)]
-//! #[kani::ensures(result <= dividend)]
+//! #[kani::ensures(|result : &u32| *result <= dividend)]
 //! fn div(dividend: u32, divisor: u32) -> u32 {
 //!     dividend / divisor
 //! }
@@ -186,31 +186,35 @@
 //! #[kanitool::replaced_with = "div_replace_965916"]
 //! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor }
 //!
-//! #[allow(dead_code)]
-//! #[allow(unused_variables)]
-//! #[kanitool::is_contract_generated(check)]
-//! fn div_check_965916(dividend: u32, divisor: u32) -> u32 {
-//!     let dividend_renamed = kani::internal::untracked_deref(&dividend);
-//!     let divisor_renamed = kani::internal::untracked_deref(&divisor);
-//!     let result = { kani::assume(divisor != 0); { dividend / divisor } };
-//!     kani::assert(result <= dividend_renamed, "result <= dividend");
+//! #[allow(dead_code, unused_variables)]
+//! #[kanitool :: is_contract_generated(check)] fn
+//! div_check_b97df2(dividend : u32, divisor : u32) -> u32
+//! {
+//!     let dividend_renamed = kani::internal::untracked_deref(& dividend);
+//!     let divisor_renamed = kani::internal::untracked_deref(& divisor);
+//!     kani::assume(divisor != 0);
+//!     let result_kani_internal : u32 = div_wrapper_b97df2(dividend, divisor);
+//!     kani::assert(
+//!     (| result : & u32 | *result <= dividend_renamed)(& result_kani_internal),
+//!     stringify!(|result : &u32| *result <= dividend));
 //!     std::mem::forget(dividend_renamed);
 //!     std::mem::forget(divisor_renamed);
-//!     result
+//!     result_kani_internal
 //! }
 //!
-//! #[allow(dead_code)]
-//! #[allow(unused_variables)]
-//! #[kanitool::is_contract_generated(replace)]
-//! fn div_replace_965916(dividend: u32, divisor: u32) -> u32 {
-//!     kani::assert(divisor != 0, "divisor != 0");
-//!     let dividend_renamed = kani::internal::untracked_deref(&dividend);
-//!     let divisor_renamed = kani::internal::untracked_deref(&divisor);
-//!     let result = kani::any();
-//!     kani::assume(result <= dividend_renamed, "result <= dividend");
-//!     std::mem::forget(dividend_renamed);
+//! #[allow(dead_code, unused_variables)]
+//! #[kanitool :: is_contract_generated(replace)] fn
+//! div_replace_b97df2(dividend : u32, divisor : u32) -> u32
+//! {
+//!     let divisor_renamed = kani::internal::untracked_deref(& divisor);
+//!     let dividend_renamed = kani::internal::untracked_deref(& dividend);
+//!     kani::assert(divisor != 0, stringify! (divisor != 0));
+//!     let result_kani_internal : u32 = kani::any_modifies();
+//!     kani::assume(
+//!     (|result : & u32| *result <= dividend_renamed)(&result_kani_internal));
 //!     std::mem::forget(divisor_renamed);
-//!     result
+//!     std::mem::forget(dividend_renamed);
+//!     result_kani_internal
 //! }
 //!
 //! #[allow(dead_code)]
@@ -220,12 +224,12 @@
 //!     static mut REENTRY: bool = false;
 //!
 //!     if unsafe { REENTRY } {
-//!         div_replace_965916(dividend, divisor)
+//!         div_replace_b97df2(dividend, divisor)
 //!     } else {
 //!         unsafe { reentry = true };
-//!         let result = div_check_965916(dividend, divisor);
+//!         let result_kani_internal = div_check_b97df2(dividend, divisor);
 //!         unsafe { reentry = false };
-//!         result
+//!         result_kani_internal
 //!     }
 //! }
 //! ```
@@ -243,6 +247,8 @@ mod initialize;
 mod replace;
 mod shared;
 
+const INTERNAL_RESULT_IDENT: &str = "result_kani_internal";
+
 pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
     contract_main(attr, item, ContractConditionsType::Requires)
 }
diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs
index 28e401c22d48..546568dc8a1d 100644
--- a/library/kani_macros/src/sysroot/contracts/replace.rs
+++ b/library/kani_macros/src/sysroot/contracts/replace.rs
@@ -3,13 +3,13 @@
 
 //! Logic used for generating the code that replaces a function with its contract.
 
-use proc_macro2::{Ident, TokenStream as TokenStream2};
+use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
 use quote::quote;
 
 use super::{
     helpers::*,
     shared::{make_unsafe_argument_copies, try_as_result_assign},
-    ContractConditionsData, ContractConditionsHandler,
+    ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
 impl<'a> ContractConditionsHandler<'a> {
@@ -39,7 +39,8 @@ impl<'a> ContractConditionsHandler<'a> {
     fn ensure_bootstrapped_replace_body(&self) -> (Vec<syn::Stmt>, Vec<syn::Stmt>) {
         if self.is_first_emit() {
             let return_type = return_type_to_type(&self.annotated_fn.sig.output);
-            (vec![syn::parse_quote!(let result : #return_type = kani::any_modifies();)], vec![])
+            let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+            (vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)], vec![])
         } else {
             let stmts = &self.annotated_fn.block.stmts;
             let idx = stmts
@@ -70,30 +71,33 @@ impl<'a> ContractConditionsHandler<'a> {
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
                 let Self { attr_copy, .. } = self;
+                let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
                 quote!(
                     kani::assert(#attr, stringify!(#attr_copy));
                     #(#before)*
                     #(#after)*
-                    result
+                    #result
                 )
             }
             ContractConditionsData::Ensures { attr, argument_names } => {
                 let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names);
+                let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
                 quote!(
                     #arg_copies
                     #(#before)*
                     #(#after)*
                     kani::assume(#attr);
                     #copy_clean
-                    result
+                    #result
                 )
             }
             ContractConditionsData::Modifies { attr } => {
+                let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
                 quote!(
                     #(#before)*
                     #(*unsafe { kani::internal::Pointer::assignable(#attr) } = kani::any_modifies();)*
                     #(#after)*
-                    result
+                    #result
                 )
             }
         }
@@ -126,7 +130,7 @@ impl<'a> ContractConditionsHandler<'a> {
     }
 }
 
-/// Is this statement `let result : <...> = kani::any_modifies();`.
+/// Is this statement `let result_kani_internal : <...> = kani::any_modifies();`.
 fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool {
     let Some(syn::LocalInit { diverge: None, expr: e, .. }) = try_as_result_assign(stmt) else {
         return false;
diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs
index bf5a8000da50..b0f5804824ad 100644
--- a/library/kani_macros/src/sysroot/contracts/shared.rs
+++ b/library/kani_macros/src/sysroot/contracts/shared.rs
@@ -13,7 +13,7 @@ use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
 use quote::{quote, ToTokens};
 use syn::Attribute;
 
-use super::{ContractConditionsHandler, ContractFunctionState};
+use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT};
 
 impl ContractFunctionState {
     /// Do we need to emit the `is_contract_generated` tag attribute on the
@@ -114,7 +114,7 @@ macro_rules! try_as_result_assign_pat {
                     ident: result_ident,
                     subpat: None,
                     ..
-                }) if result_ident == "result"
+                }) if result_ident == INTERNAL_RESULT_IDENT
             ) => init.$convert(),
             _ => None,
         }
diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md
index dae805a7db72..deeeca66ab7a 100644
--- a/rfc/src/rfcs/0009-function-contracts.md
+++ b/rfc/src/rfcs/0009-function-contracts.md
@@ -65,7 +65,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 {
 
    ```rs
    #[kani::requires(divisor != 0)]
-   #[kani::ensures(result <= dividend)]
+   #[kani::ensures(|result : &u32| *result <= dividend)]
    fn my_div(dividend: u32, divisor: u32) -> u32 {
      dividend / divisor
    }
@@ -79,8 +79,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 {
 
    Conditions in contracts are Rust expressions which reference the
    function arguments and, in case of `ensures`, the return value of the
-   function. The return value is a special variable called `result` (see [open
-   questions](#open-questions) on a discussion about (re)naming). Syntactically
+   function. The return value is passed into the ensures closure statement by reference. Syntactically
    Kani supports any Rust expression, including function calls, defining types
    etc. However they must be side-effect free (see also side effects
    [here](#changes-to-other-components)) or Kani will throw a compile error.
@@ -132,8 +131,8 @@ fn my_div(dividend: u32, divisor: u32) -> u32 {
      let dividend = kani::any();
      let divisor = kani::any();
      kani::assume(divisor != 0); // requires
-     let result = my_div(dividend, divisor);
-     kani::assert(result <= dividend); // ensures
+     let result_kani_internal = my_div(dividend, divisor);
+     kani::assert((|result : &u32| *result <= dividend)(result_kani_internal)); // ensures
    }
    ```
 
@@ -306,7 +305,7 @@ available to `ensures`. It is used like so:
 
 ```rs
 impl<T> Vec<T> {
-  #[kani::ensures(old(self.is_empty()) || result.is_some())]
+  #[kani::ensures(|result : &Option<T>| old(self.is_empty()) || result.is_some())]
   fn pop(&mut self) -> Option<T> {
     ...
   }
@@ -324,8 +323,8 @@ Note also that `old` is syntax, not a function and implemented as an extraction
 and lifting during code generation. It can reference e.g. `pop`'s arguments but
 not local variables. Compare the following
 
-**Invalid ❌:** `#[kani::ensures({ let x = self.is_empty(); old(x) } || result.is_some())]`</br>
-**Valid ✅:** `#[kani::ensures(old({ let x = self.is_empty(); x }) || result.is_some())]`
+**Invalid ❌:** `#[kani::ensures(|result : &Option<T>| { let x = self.is_empty(); old(x) } || result.is_some())]`</br>
+**Valid ✅:** `#[kani::ensures(|result : &Option<T>| old({ let x = self.is_empty(); x }) || result.is_some())]`
 
 And it will only be recognized as `old(...)`, not as `let old1 = old; old1(...)` etc.
 
@@ -410,7 +409,7 @@ the below example:
 
 ```rs
 impl<T> Vec<T> {
-  #[kani::ensures(self.is_empty() || self.len() == old(self.len()) - 1)]
+  #[kani::ensures(|result : &Option<T>| self.is_empty() || self.len() == old(self.len()) - 1)]
   fn pop(&mut self) -> Option<T> {
     ...
   }
@@ -425,8 +424,8 @@ following:
 impl<T> Vec<T> {
   fn check_pop(&mut self) -> Option<T> {
     let old_1 = self.len();
-    let result = Self::pop(self);
-    kani::assert(self.is_empty() || self.len() == old_1 - 1)
+    let result_kani_internal = Self::pop(self);
+    kani::assert((|result : &Option<T>| self.is_empty() || self.len() == old_1 - 1)(result_kani_internal))
   }
 }
 ```
@@ -450,7 +449,7 @@ sensible contract for it might look as follows:
 
 ```rs
 impl<T> Vec<T> {
-  #[ensures(self.len() == result.0.len() + result.1.len())]
+  #[ensures(|result : &(&mut [T], &mut [T])| self.len() == result.0.len() + result.1.len())]
   fn split_at_mut(&mut self, i: usize) -> (&mut [T], &mut [T]) {
     ...
   }
diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected
index 0a59d2cea5eb..4b70f8364e05 100644
--- a/tests/expected/function-contract/arbitrary_ensures_fail.expected
+++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: FAILURE\
-- Description: "result == x"\
+- Description: "|result : &u32| *result == x"\
 in function max 
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs
index 91638b1cc037..8d66402180d7 100644
--- a/tests/expected/function-contract/arbitrary_ensures_fail.rs
+++ b/tests/expected/function-contract/arbitrary_ensures_fail.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::ensures(result == x)]
+#[kani::ensures(|result : &u32| *result == x)]
 fn max(x: u32, y: u32) -> u32 {
     if x > y { x } else { y }
 }
diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected
index 85619fa84c22..9eee213789b9 100644
--- a/tests/expected/function-contract/arbitrary_ensures_pass.expected
+++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "result == x || result == y"\
+- Description: "|result : &u32| *result == x || *result == y"\
 in function max
      
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.rs b/tests/expected/function-contract/arbitrary_ensures_pass.rs
index df8d3a2361fb..86302f705925 100644
--- a/tests/expected/function-contract/arbitrary_ensures_pass.rs
+++ b/tests/expected/function-contract/arbitrary_ensures_pass.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::ensures(result == x || result == y)]
+#[kani::ensures(|result : &u32| *result == x || *result == y)]
 fn max(x: u32, y: u32) -> u32 {
     if x > y { x } else { y }
 }
diff --git a/tests/expected/function-contract/arbitrary_requires_fail.rs b/tests/expected/function-contract/arbitrary_requires_fail.rs
index d052e19b0335..78ab1b77bf10 100644
--- a/tests/expected/function-contract/arbitrary_requires_fail.rs
+++ b/tests/expected/function-contract/arbitrary_requires_fail.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::ensures(result <= dividend)]
+#[kani::ensures(|result : &u32| *result <= dividend)]
 fn div(dividend: u32, divisor: u32) -> u32 {
     dividend / divisor
 }
diff --git a/tests/expected/function-contract/attribute_complain.rs b/tests/expected/function-contract/attribute_complain.rs
index f16e975c2001..8532889e1eca 100644
--- a/tests/expected/function-contract/attribute_complain.rs
+++ b/tests/expected/function-contract/attribute_complain.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-#[kani::ensures(true)]
+#[kani::ensures(|result| true)]
 fn always() {}
 
 #[kani::proof_for_contract(always)]
diff --git a/tests/expected/function-contract/attribute_no_complain.rs b/tests/expected/function-contract/attribute_no_complain.rs
index bcf1f0cadafd..b3004b24f4d4 100644
--- a/tests/expected/function-contract/attribute_no_complain.rs
+++ b/tests/expected/function-contract/attribute_no_complain.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-#[kani::ensures(true)]
+#[kani::ensures(|result| true)]
 fn always() {}
 
 #[kani::proof]
diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected
index c31b5c389fc8..e181e6b2ad17 100644
--- a/tests/expected/function-contract/checking_from_external_mod.expected
+++ b/tests/expected/function-contract/checking_from_external_mod.expected
@@ -1,5 +1,5 @@
 - Status: SUCCESS\
-- Description: "(result == x) | (result == y)"\
+- Description: "|result : &u32| (*result == x) | (*result == y)"\
 in function max
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/checking_from_external_mod.rs b/tests/expected/function-contract/checking_from_external_mod.rs
index 43d1551f9aef..ea01cfadd511 100644
--- a/tests/expected/function-contract/checking_from_external_mod.rs
+++ b/tests/expected/function-contract/checking_from_external_mod.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::ensures((result == x) | (result == y))]
+#[kani::ensures(|result : &u32| (*result == x) | (*result == y))]
 fn max(x: u32, y: u32) -> u32 {
     if x > y { x } else { y }
 }
diff --git a/tests/expected/function-contract/checking_in_impl.expected b/tests/expected/function-contract/checking_in_impl.expected
index d5a390be8425..cfe84c06fc85 100644
--- a/tests/expected/function-contract/checking_in_impl.expected
+++ b/tests/expected/function-contract/checking_in_impl.expected
@@ -1,5 +1,5 @@
 - Status: SUCCESS\
-- Description: "(result == self) | (result == y)"\
+- Description: "|result : &WrappedInt| (*result == self) | (*result == y)"\
 in function WrappedInt::max
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/checking_in_impl.rs b/tests/expected/function-contract/checking_in_impl.rs
index 7d5c0506d9df..8721e7fffb7f 100644
--- a/tests/expected/function-contract/checking_in_impl.rs
+++ b/tests/expected/function-contract/checking_in_impl.rs
@@ -8,7 +8,7 @@ extern crate kani;
 struct WrappedInt(u32);
 
 impl WrappedInt {
-    #[kani::ensures((result == self) | (result == y))]
+    #[kani::ensures(|result : &WrappedInt| (*result == self) | (*result == y))]
     fn max(self, y: WrappedInt) -> WrappedInt {
         Self(if self.0 > y.0 { self.0 } else { y.0 })
     }
diff --git a/tests/expected/function-contract/fail_on_two.expected b/tests/expected/function-contract/fail_on_two.expected
index 32fc28012d3a..79cc3d572af0 100644
--- a/tests/expected/function-contract/fail_on_two.expected
+++ b/tests/expected/function-contract/fail_on_two.expected
@@ -7,6 +7,6 @@ Failed Checks: internal error: entered unreachable code: fail on two
 
 assertion\
 - Status: FAILURE\
-- Description: "result < 3"
+- Description: "|result : &i32| *result < 3"
 
-Failed Checks: result < 3
+Failed Checks: |result : &i32| *result < 3
diff --git a/tests/expected/function-contract/fail_on_two.rs b/tests/expected/function-contract/fail_on_two.rs
index 605065449194..32ad74c31cd9 100644
--- a/tests/expected/function-contract/fail_on_two.rs
+++ b/tests/expected/function-contract/fail_on_two.rs
@@ -16,7 +16,7 @@
 //! once because the postcondition is violated). If instead the hypothesis (e.g.
 //! contract replacement) is used we'd expect the verification to succeed.
 
-#[kani::ensures(result < 3)]
+#[kani::ensures(|result : &i32| *result < 3)]
 #[kani::recursion]
 fn fail_on_two(i: i32) -> i32 {
     match i {
@@ -32,7 +32,7 @@ fn harness() {
     let _ = fail_on_two(first);
 }
 
-#[kani::ensures(result < 3)]
+#[kani::ensures(|result : &i32| *result < 3)]
 #[kani::recursion]
 fn fail_on_two_in_postcondition(i: i32) -> i32 {
     let j = i + 1;
diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected
index c7fe5a721abb..ca21817c8329 100644
--- a/tests/expected/function-contract/gcd_failure_code.expected
+++ b/tests/expected/function-contract/gcd_failure_code.expected
@@ -1,8 +1,8 @@
 assertion\
 - Status: FAILURE\
-- Description: "result != 0 && x % result == 0 && y % result == 0"\
+- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0"\
 in function gcd
 
-Failed Checks: result != 0 && x % result == 0 && y % result == 0
+Failed Checks: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/gcd_failure_code.rs b/tests/expected/function-contract/gcd_failure_code.rs
index f76e04b75fee..118cc3c930e5 100644
--- a/tests/expected/function-contract/gcd_failure_code.rs
+++ b/tests/expected/function-contract/gcd_failure_code.rs
@@ -5,7 +5,7 @@ type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
-#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
     let mut min = y;
diff --git a/tests/expected/function-contract/gcd_failure_contract.expected b/tests/expected/function-contract/gcd_failure_contract.expected
index aeadfb563ab9..4bb02ab36f49 100644
--- a/tests/expected/function-contract/gcd_failure_contract.expected
+++ b/tests/expected/function-contract/gcd_failure_contract.expected
@@ -1,8 +1,8 @@
 assertion\
 - Status: FAILURE\
-- Description: "result != 0 && x % result == 1 && y % result == 0"\
+- Description: "|result : &T| *result != 0 && x % *result == 1 && y % *result == 0"\
 in function gcd\
 	 
-Failed Checks: result != 0 && x % result == 1 && y % result == 0
+Failed Checks: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/gcd_failure_contract.rs b/tests/expected/function-contract/gcd_failure_contract.rs
index 6b835466c5a0..d4eea8ceb98c 100644
--- a/tests/expected/function-contract/gcd_failure_contract.rs
+++ b/tests/expected/function-contract/gcd_failure_contract.rs
@@ -5,8 +5,8 @@ type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
-// Changed `0` to `1` in `x % result == 0` to mess with this contract
-#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)]
+// Changed `0` to `1` in `x % *result == 0` to mess with this contract
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 1 && y % *result == 0)]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
     let mut min = y;
diff --git a/tests/expected/function-contract/gcd_rec_code_fail.expected b/tests/expected/function-contract/gcd_rec_code_fail.expected
index 80dbaadbf4c7..863392098be4 100644
--- a/tests/expected/function-contract/gcd_rec_code_fail.expected
+++ b/tests/expected/function-contract/gcd_rec_code_fail.expected
@@ -1,3 +1,3 @@
-Failed Checks: result != 0 && x % result == 0 && y % result == 0
+Failed Checks: |result : &T| *result != 0 && x % *result == 0 && y % *result == 0
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/gcd_rec_code_fail.rs b/tests/expected/function-contract/gcd_rec_code_fail.rs
index da38318e2a66..90260f56d4dc 100644
--- a/tests/expected/function-contract/gcd_rec_code_fail.rs
+++ b/tests/expected/function-contract/gcd_rec_code_fail.rs
@@ -5,7 +5,7 @@ type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
-#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
 #[kani::recursion]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.expected b/tests/expected/function-contract/gcd_rec_comparison_pass.expected
index da647dfd40aa..0556bfc50204 100644
--- a/tests/expected/function-contract/gcd_rec_comparison_pass.expected
+++ b/tests/expected/function-contract/gcd_rec_comparison_pass.expected
@@ -4,6 +4,6 @@ assertion\
 
 assertion\
 - Status: SUCCESS\
-- Description: "result != 0 && x % result == 0 && y % result == 0"
+- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0"
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.rs b/tests/expected/function-contract/gcd_rec_comparison_pass.rs
index 1db9691ae8e4..ae5fbbe9b60f 100644
--- a/tests/expected/function-contract/gcd_rec_comparison_pass.rs
+++ b/tests/expected/function-contract/gcd_rec_comparison_pass.rs
@@ -5,7 +5,7 @@ type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
-#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
 #[kani::recursion]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.expected b/tests/expected/function-contract/gcd_rec_contract_fail.expected
index bfb470192a39..6cc0354ca89a 100644
--- a/tests/expected/function-contract/gcd_rec_contract_fail.expected
+++ b/tests/expected/function-contract/gcd_rec_contract_fail.expected
@@ -1,3 +1,3 @@
-Failed Checks: result != 0 && x % result == 1 && y % result == 0
+Failed Checks: |result : &T| *result != 0 && x % *result == 1 && y % *result == 0
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.rs b/tests/expected/function-contract/gcd_rec_contract_fail.rs
index 3fe34cb2effc..2306db0e9353 100644
--- a/tests/expected/function-contract/gcd_rec_contract_fail.rs
+++ b/tests/expected/function-contract/gcd_rec_contract_fail.rs
@@ -6,7 +6,7 @@ type T = u8;
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
 // Changed `0` to `1` in `x % result == 0` to mess with this contract
-#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)]
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 1 && y % *result == 0)]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
     let mut min = y;
diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.rs b/tests/expected/function-contract/gcd_rec_replacement_pass.rs
index d8a5bbd234ed..0fd04b0076ba 100644
--- a/tests/expected/function-contract/gcd_rec_replacement_pass.rs
+++ b/tests/expected/function-contract/gcd_rec_replacement_pass.rs
@@ -5,7 +5,7 @@ type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
-#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
     let mut min = y;
diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.expected b/tests/expected/function-contract/gcd_rec_simple_pass.expected
index da647dfd40aa..0556bfc50204 100644
--- a/tests/expected/function-contract/gcd_rec_simple_pass.expected
+++ b/tests/expected/function-contract/gcd_rec_simple_pass.expected
@@ -4,6 +4,6 @@ assertion\
 
 assertion\
 - Status: SUCCESS\
-- Description: "result != 0 && x % result == 0 && y % result == 0"
+- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0"
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.rs b/tests/expected/function-contract/gcd_rec_simple_pass.rs
index 464e3d8bbea1..626a48aa5ec2 100644
--- a/tests/expected/function-contract/gcd_rec_simple_pass.rs
+++ b/tests/expected/function-contract/gcd_rec_simple_pass.rs
@@ -5,7 +5,7 @@ type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
-#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
 #[kani::recursion]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
diff --git a/tests/expected/function-contract/gcd_replacement_fail.rs b/tests/expected/function-contract/gcd_replacement_fail.rs
index 8bd59c5c14fe..0186a369c3b2 100644
--- a/tests/expected/function-contract/gcd_replacement_fail.rs
+++ b/tests/expected/function-contract/gcd_replacement_fail.rs
@@ -5,7 +5,7 @@ type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
-#[kani::ensures(result != 0 && x % result == 0)]
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 0)]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
     let mut min = y;
diff --git a/tests/expected/function-contract/gcd_replacement_pass.rs b/tests/expected/function-contract/gcd_replacement_pass.rs
index 9827dd3a1512..b45241198737 100644
--- a/tests/expected/function-contract/gcd_replacement_pass.rs
+++ b/tests/expected/function-contract/gcd_replacement_pass.rs
@@ -5,7 +5,7 @@ type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
-#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
     let mut min = y;
diff --git a/tests/expected/function-contract/gcd_success.expected b/tests/expected/function-contract/gcd_success.expected
index 73b531d424b9..e5885dd11179 100644
--- a/tests/expected/function-contract/gcd_success.expected
+++ b/tests/expected/function-contract/gcd_success.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "result != 0 && x % result == 0 && y % result == 0"\
+- Description: "|result : &T| *result != 0 && x % *result == 0 && y % *result == 0"\
 in function gcd
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/gcd_success.rs b/tests/expected/function-contract/gcd_success.rs
index d3a2c75b7d20..3b983a230b60 100644
--- a/tests/expected/function-contract/gcd_success.rs
+++ b/tests/expected/function-contract/gcd_success.rs
@@ -5,7 +5,7 @@ type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
-#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)]
+#[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
 fn gcd(x: T, y: T) -> T {
     let mut max = x;
     let mut min = y;
diff --git a/tests/expected/function-contract/modifies/check_only_verification.rs b/tests/expected/function-contract/modifies/check_only_verification.rs
index 2f247a718ae9..9f3fb3614733 100644
--- a/tests/expected/function-contract/modifies/check_only_verification.rs
+++ b/tests/expected/function-contract/modifies/check_only_verification.rs
@@ -7,7 +7,7 @@
 
 #[kani::requires(*ptr < 100)]
 #[kani::modifies(ptr)]
-#[kani::ensures(result == 100)]
+#[kani::ensures(|result : &u32| *result == 100)]
 fn modify(ptr: &mut u32) -> u32 {
     *ptr += 1;
     *ptr
diff --git a/tests/expected/function-contract/modifies/expr_pass.rs b/tests/expected/function-contract/modifies/expr_pass.rs
index 65e561df48a2..9a6f46a6aaaa 100644
--- a/tests/expected/function-contract/modifies/expr_pass.rs
+++ b/tests/expected/function-contract/modifies/expr_pass.rs
@@ -7,7 +7,7 @@
 
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
-#[kani::ensures(**ptr < 101)]
+#[kani::ensures(|result| **ptr < 101)]
 fn modify(ptr: &mut Box<u32>) {
     *ptr.as_mut() += 1;
 }
diff --git a/tests/expected/function-contract/modifies/expr_replace_pass.rs b/tests/expected/function-contract/modifies/expr_replace_pass.rs
index 8be1ef2cbaee..779280dd46b4 100644
--- a/tests/expected/function-contract/modifies/expr_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/expr_replace_pass.rs
@@ -4,7 +4,7 @@
 
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
-#[kani::ensures(**ptr == prior + 1)]
+#[kani::ensures(|result| **ptr == prior + 1)]
 fn modify(ptr: &mut Box<u32>, prior: u32) {
     *ptr.as_mut() += 1;
 }
diff --git a/tests/expected/function-contract/modifies/fail_missing_recursion_attr.rs b/tests/expected/function-contract/modifies/fail_missing_recursion_attr.rs
index 644b641e731e..5e9b96e021f7 100644
--- a/tests/expected/function-contract/modifies/fail_missing_recursion_attr.rs
+++ b/tests/expected/function-contract/modifies/fail_missing_recursion_attr.rs
@@ -5,7 +5,7 @@
 //! Check whether Kani fails if users forgot to annotate recursive
 //! functions with `#[kani::recursion]` when using function contracts.
 
-#[kani::ensures(result < 3)]
+#[kani::ensures(|result : &i32| *result < 3)]
 fn fail_on_two(i: i32) -> i32 {
     match i {
         0 => fail_on_two(i + 1),
diff --git a/tests/expected/function-contract/modifies/field_replace_pass.rs b/tests/expected/function-contract/modifies/field_replace_pass.rs
index a6ae4ea4a7e0..1bbbaf31121a 100644
--- a/tests/expected/function-contract/modifies/field_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/field_replace_pass.rs
@@ -8,7 +8,7 @@ struct S<'a> {
 }
 #[kani::requires(*s.target < 100)]
 #[kani::modifies(s.target)]
-#[kani::ensures(*s.target == prior + 1)]
+#[kani::ensures(|result| *s.target == prior + 1)]
 fn modify(s: S, prior: u32) {
     *s.target += 1;
 }
diff --git a/tests/expected/function-contract/modifies/global_replace_pass.rs b/tests/expected/function-contract/modifies/global_replace_pass.rs
index 333348f25ce4..69d36bd96033 100644
--- a/tests/expected/function-contract/modifies/global_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/global_replace_pass.rs
@@ -5,7 +5,7 @@
 static mut PTR: u32 = 0;
 
 #[kani::modifies(&mut PTR)]
-#[kani::ensures(PTR == src)]
+#[kani::ensures(|result| PTR == src)]
 unsafe fn modify(src: u32) {
     PTR = src;
 }
diff --git a/tests/expected/function-contract/modifies/havoc_pass.rs b/tests/expected/function-contract/modifies/havoc_pass.rs
index aa5bcada1a26..ebdd139727d3 100644
--- a/tests/expected/function-contract/modifies/havoc_pass.rs
+++ b/tests/expected/function-contract/modifies/havoc_pass.rs
@@ -3,7 +3,7 @@
 // kani-flags: -Zfunction-contracts
 
 #[kani::modifies(dst)]
-#[kani::ensures(*dst == src)]
+#[kani::ensures(|result| *dst == src)]
 fn copy(src: u32, dst: &mut u32) {
     *dst = src;
 }
diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.rs b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs
index dc5f370179e5..43581ee677a6 100644
--- a/tests/expected/function-contract/modifies/havoc_pass_reordered.rs
+++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs
@@ -3,7 +3,7 @@
 // kani-flags: -Zfunction-contracts
 
 // These two are reordered in comparison to `havoc_pass` and we expect the test case to pass still
-#[kani::ensures(*dst == src)]
+#[kani::ensures(|result| *dst == src)]
 #[kani::modifies(dst)]
 fn copy(src: u32, dst: &mut u32) {
     *dst = src;
diff --git a/tests/expected/function-contract/modifies/mistake_condition_return.rs b/tests/expected/function-contract/modifies/mistake_condition_return.rs
index 484819af4248..b2d6ad6a8a55 100644
--- a/tests/expected/function-contract/modifies/mistake_condition_return.rs
+++ b/tests/expected/function-contract/modifies/mistake_condition_return.rs
@@ -16,8 +16,8 @@
 // However, contract instrumentation will create a separate non-deterministic
 // value to return in this function that can only be constrained by using the
 // `result` keyword. Thus the correct condition would be
-// `#[kani::ensures(result == 100)]`.
-#[kani::ensures(*ptr == 100)]
+// `#[kani::ensures(|result| result == 100)]`.
+#[kani::ensures(|result| *ptr == 100)]
 fn modify(ptr: &mut u32) -> u32 {
     *ptr += 1;
     *ptr
diff --git a/tests/expected/function-contract/modifies/unique_arguments.rs b/tests/expected/function-contract/modifies/unique_arguments.rs
index 396ba4c5b036..ea4502bde2ad 100644
--- a/tests/expected/function-contract/modifies/unique_arguments.rs
+++ b/tests/expected/function-contract/modifies/unique_arguments.rs
@@ -4,8 +4,8 @@
 
 #[kani::modifies(a)]
 #[kani::modifies(b)]
-#[kani::ensures(*a == 1)]
-#[kani::ensures(*b == 2)]
+#[kani::ensures(|result| *a == 1)]
+#[kani::ensures(|result| *b == 2)]
 fn two_pointers(a: &mut u32, b: &mut u32) {
     *a = 1;
     *b = 2;
diff --git a/tests/expected/function-contract/modifies/vec_pass.expected b/tests/expected/function-contract/modifies/vec_pass.expected
index d31486f2dcc6..4d5407fdd850 100644
--- a/tests/expected/function-contract/modifies/vec_pass.expected
+++ b/tests/expected/function-contract/modifies/vec_pass.expected
@@ -15,6 +15,6 @@ in function modify_replace
 
 assertion\
 - Status: SUCCESS\
-- Description: "v[0] == src"
+- Description: "|result| v[0] == src"
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/modifies/vec_pass.rs b/tests/expected/function-contract/modifies/vec_pass.rs
index 1e40a2a08eb7..e3ac28ac3b3d 100644
--- a/tests/expected/function-contract/modifies/vec_pass.rs
+++ b/tests/expected/function-contract/modifies/vec_pass.rs
@@ -4,7 +4,7 @@
 
 #[kani::requires(v.len() > 0)]
 #[kani::modifies(&v[0])]
-#[kani::ensures(v[0] == src)]
+#[kani::ensures(|result| v[0] == src)]
 fn modify(v: &mut Vec<u32>, src: u32) {
     v[0] = src
 }
diff --git a/tests/expected/function-contract/pattern_use.rs b/tests/expected/function-contract/pattern_use.rs
index a51312acd2f0..ead1c1538b4d 100644
--- a/tests/expected/function-contract/pattern_use.rs
+++ b/tests/expected/function-contract/pattern_use.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::ensures(result <= dividend)]
+#[kani::ensures(|result : &u32| *result <= dividend)]
 fn div((dividend, divisor): (u32, u32)) -> u32 {
     dividend / divisor
 }
diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs
index 3d88fc0926ed..1b3653951ad1 100644
--- a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs
+++ b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs
@@ -4,7 +4,7 @@
 
 #![allow(unreachable_code, unused_variables)]
 
-#[kani::ensures(true)]
+#[kani::ensures(|result| true)]
 fn allowed_pointer(t: *const bool) {}
 
 #[kani::proof_for_contract(allowed_pointer)]
diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs
index 22771f76632d..2c41bf28d741 100644
--- a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs
+++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs
@@ -4,7 +4,7 @@
 
 #![allow(unreachable_code, unused_variables)]
 
-#[kani::ensures(true)]
+#[kani::ensures(|result| true)]
 fn allowed_mut_ref(t: &mut bool) {}
 
 #[kani::proof_for_contract(allowed_mut_ref)]
diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs
index e5151396898d..fdab681e0c05 100644
--- a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs
+++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs
@@ -17,7 +17,7 @@ impl<'a> kani::Arbitrary for ArbitraryPointer<&'a mut bool> {
     }
 }
 
-#[kani::ensures(true)]
+#[kani::ensures(|result| true)]
 fn allowed_mut_return_ref<'a>() -> ArbitraryPointer<&'a mut bool> {
     ArbitraryPointer(unsafe { &mut B as &'a mut bool })
 }
diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs
index 3dd4145eff9c..cef3e87ee0f2 100644
--- a/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs
+++ b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs
@@ -4,7 +4,7 @@
 
 #![allow(unreachable_code, unused_variables)]
 
-#[kani::ensures(true)]
+#[kani::ensures(|result| true)]
 fn allowed_ref(t: &bool) {}
 
 #[kani::proof_for_contract(allowed_ref)]
diff --git a/tests/expected/function-contract/prohibit-pointers/hidden.rs b/tests/expected/function-contract/prohibit-pointers/hidden.rs
index 9ca23fe6b2e1..1a9b7a475479 100644
--- a/tests/expected/function-contract/prohibit-pointers/hidden.rs
+++ b/tests/expected/function-contract/prohibit-pointers/hidden.rs
@@ -6,7 +6,7 @@
 
 struct HidesAPointer(*mut u32);
 
-#[kani::ensures(true)]
+#[kani::ensures(|result| true)]
 fn hidden_pointer(h: HidesAPointer) {}
 
 #[kani::proof_for_contract(hidden_pointer)]
diff --git a/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs b/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs
index 24e9d006a9c0..868327e15046 100644
--- a/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs
+++ b/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs
@@ -4,7 +4,7 @@
 
 #![allow(unreachable_code, unused_variables)]
 
-#[kani::ensures(true)]
+#[kani::ensures(|result| true)]
 fn plain_pointer(t: *mut i32) {}
 
 #[kani::proof_for_contract(plain_pointer)]
diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs
index 2bacdca9bbb6..6314129ddf89 100644
--- a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs
+++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::ensures(unsafe{ *result == *input })]
+#[kani::ensures(|result : &*const usize| unsafe{ **result == *input })]
 fn return_pointer(input: *const usize) -> *const usize {
     input
 }
diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected
index 8e9b42d42640..360242d07daf 100644
--- a/tests/expected/function-contract/simple_ensures_fail.expected
+++ b/tests/expected/function-contract/simple_ensures_fail.expected
@@ -1,8 +1,8 @@
 assertion\
 - Status: FAILURE\
-- Description: "result == x"\
+- Description: "|result : &u32| *result == x"\
 in function max
 
-Failed Checks: result == x
+Failed Checks: |result : &u32| *result == x
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs
index 687853612dcc..43521b171ea7 100644
--- a/tests/expected/function-contract/simple_ensures_fail.rs
+++ b/tests/expected/function-contract/simple_ensures_fail.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::ensures(result == x)]
+#[kani::ensures(|result : &u32| *result == x)]
 fn max(x: u32, y: u32) -> u32 {
     if x > y { x } else { y }
 }
diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected
index 5a7874964413..bdcde74c3bfe 100644
--- a/tests/expected/function-contract/simple_ensures_pass.expected
+++ b/tests/expected/function-contract/simple_ensures_pass.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "(result == x) | (result == y)"\
+- Description: "|result : &u32| (*result == x) | (*result == y)"\
 in function max
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/simple_ensures_pass.rs b/tests/expected/function-contract/simple_ensures_pass.rs
index 2d36f5c96e88..7be58fef3b04 100644
--- a/tests/expected/function-contract/simple_ensures_pass.rs
+++ b/tests/expected/function-contract/simple_ensures_pass.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::ensures((result == x) | (result == y))]
+#[kani::ensures(|result : &u32| (*result == x) | (*result == y))]
 fn max(x: u32, y: u32) -> u32 {
     if x > y { x } else { y }
 }
diff --git a/tests/expected/function-contract/simple_replace_fail.rs b/tests/expected/function-contract/simple_replace_fail.rs
index 33a531a3aef7..dd448d2cdee6 100644
--- a/tests/expected/function-contract/simple_replace_fail.rs
+++ b/tests/expected/function-contract/simple_replace_fail.rs
@@ -3,7 +3,7 @@
 // kani-flags: -Zfunction-contracts
 
 #[kani::requires(divisor != 0)]
-#[kani::ensures(result <= dividend)]
+#[kani::ensures(|result : &u32| *result <= dividend)]
 fn div(dividend: u32, divisor: u32) -> u32 {
     dividend / divisor
 }
diff --git a/tests/expected/function-contract/simple_replace_pass.rs b/tests/expected/function-contract/simple_replace_pass.rs
index 0dcc6cd59fe3..7c57cc6a0b7f 100644
--- a/tests/expected/function-contract/simple_replace_pass.rs
+++ b/tests/expected/function-contract/simple_replace_pass.rs
@@ -3,7 +3,7 @@
 // kani-flags: -Zfunction-contracts
 
 #[kani::requires(divisor != 0)]
-#[kani::ensures(result <= dividend)]
+#[kani::ensures(|result : &u32| *result <= dividend)]
 fn div(dividend: u32, divisor: u32) -> u32 {
     dividend / divisor
 }
diff --git a/tests/expected/function-contract/type_annotation_needed.rs b/tests/expected/function-contract/type_annotation_needed.rs
index 09b20443d47b..5a3b9fbae5b0 100644
--- a/tests/expected/function-contract/type_annotation_needed.rs
+++ b/tests/expected/function-contract/type_annotation_needed.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-#[kani::ensures(result.is_some())]
+#[kani::ensures(|result : &Option<T>| result.is_some())]
 fn or_default<T: Default>(opt: Option<T>) -> Option<T> {
     opt.or(Some(T::default()))
 }
diff --git a/tests/std-checks/core/src/ptr.rs b/tests/std-checks/core/src/ptr.rs
index 847b8fd1c138..49cf9e168214 100644
--- a/tests/std-checks/core/src/ptr.rs
+++ b/tests/std-checks/core/src/ptr.rs
@@ -9,8 +9,8 @@ pub mod contracts {
     use super::*;
     use kani::{ensures, implies, mem::*, modifies, requires};
 
-    #[ensures(implies!(ptr.is_null() => result.is_none()))]
-    #[ensures(implies!(!ptr.is_null() => result.is_some()))]
+    #[ensures(|result : &Option<NonNull<T>>| implies!(ptr.is_null() => result.is_none()))]
+    #[ensures(|result : &Option<NonNull<T>>| implies!(!ptr.is_null() => result.is_some()))]
     pub fn new<T>(ptr: *mut T) -> Option<NonNull<T>> {
         NonNull::new(ptr)
     }

From a6332fc2ed04c5a72e4671835ef584c0b31c4f3b Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Thu, 6 Jun 2024 16:07:04 -0400
Subject: [PATCH 2/5] (Re)introduce `Invariant` trait (#3190)

This PR reintroduces the `Invariant` trait as a mechanism for the
specification of type safety invariants. The trait is defined in the
Kani library where we also provide `Invariant` implementations for
primitive types.

In contrast to the previous `Invariant` trait, this version doesn't
require the `Arbitrary` bound (i.e., it has the same requirements as
`Arbitrary`). This way, the user isn't required to provide an
`Arbitrary` implementation in addition to the `Invariant` one.

Related #3095
---
 library/kani/src/arbitrary.rs           |   6 +-
 library/kani/src/invariant.rs           | 102 ++++++++++++++++++++++++
 library/kani/src/lib.rs                 |   2 +
 tests/kani/Invariant/invariant_impls.rs |  38 +++++++++
 tests/kani/Invariant/percentage.rs      |  62 ++++++++++++++
 5 files changed, 207 insertions(+), 3 deletions(-)
 create mode 100644 library/kani/src/invariant.rs
 create mode 100644 tests/kani/Invariant/invariant_impls.rs
 create mode 100644 tests/kani/Invariant/percentage.rs

diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs
index 938f3c30968f..3f1adc787b79 100644
--- a/library/kani/src/arbitrary.rs
+++ b/library/kani/src/arbitrary.rs
@@ -1,8 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! This module introduces the Arbitrary trait as well as implementation for primitive types and
-//! other std containers.
+//! This module introduces the `Arbitrary` trait as well as implementation for
+//! primitive types and other std containers.
 
 use std::{
     marker::{PhantomData, PhantomPinned},
@@ -66,7 +66,7 @@ trivial_arbitrary!(i64);
 trivial_arbitrary!(i128);
 trivial_arbitrary!(isize);
 
-// We do not constraint floating points values per type spec. Users must add assumptions to their
+// We do not constrain floating points values per type spec. Users must add assumptions to their
 // verification code if they want to eliminate NaN, infinite, or subnormal.
 trivial_arbitrary!(f32);
 trivial_arbitrary!(f64);
diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs
new file mode 100644
index 000000000000..f118f94e995c
--- /dev/null
+++ b/library/kani/src/invariant.rs
@@ -0,0 +1,102 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module introduces the `Invariant` trait as well as its implementation
+//! for primitive types.
+
+/// This trait should be used to specify and check type safety invariants for a
+/// type. For type invariants, we refer to the definitions in the Rust's Unsafe
+/// Code Guidelines Reference:
+/// <https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#validity-and-safety-invariant>
+///
+/// In summary, the reference distinguishes two kinds of type invariants:
+///  - *Validity invariant*: An invariant that all data must uphold any time
+///    it's accessed or copied in a typed manner. This invariant is exploited by
+///    the compiler to perform optimizations.
+///  - *Safety invariant*: An invariant that safe code may assume all data to
+///    uphold. This invariant can be temporarily violated by unsafe code, but
+///    must always be upheld when interfacing with unknown safe code.
+///
+/// Therefore, validity invariants must be upheld at all times, while safety
+/// invariants only need to be upheld at the boundaries to safe code.
+///
+/// Safety invariants are particularly interesting for user-defined types, and
+/// the `Invariant` trait allows you to check them with Kani.
+///
+/// It can also be used in tests. It's a programmatic way to specify (in Rust)
+/// properties over your data types. Since it's written in Rust, it can be used
+/// for static and dynamic checking.
+///
+/// For example, let's say you're creating a type that represents a date:
+///
+/// ```rust
+/// #[derive(kani::Arbitrary)]
+/// pub struct MyDate {
+///   day: u8,
+///   month: u8,
+///   year: i64,
+/// }
+/// ```
+/// You can specify its safety invariant as:
+/// ```rust
+/// impl kani::Invariant for MyDate {
+///   fn is_safe(&self) -> bool {
+///     self.month > 0
+///       && self.month <= 12
+///       && self.day > 0
+///       && self.day <= days_in_month(self.year, self.month)
+///   }
+/// }
+/// ```
+/// And use it to check that your APIs are safe:
+/// ```rust
+/// #[kani::proof]
+/// fn check_increase_date() {
+///   let mut date: MyDate = kani::any();
+///   // Increase date by one day
+///   increase_date(date, 1);
+///   assert!(date.is_safe());
+/// }
+/// ```
+pub trait Invariant
+where
+    Self: Sized,
+{
+    fn is_safe(&self) -> bool;
+}
+
+/// Any value is considered safe for the type
+macro_rules! trivial_invariant {
+    ( $type: ty ) => {
+        impl Invariant for $type {
+            #[inline(always)]
+            fn is_safe(&self) -> bool {
+                true
+            }
+        }
+    };
+}
+
+trivial_invariant!(u8);
+trivial_invariant!(u16);
+trivial_invariant!(u32);
+trivial_invariant!(u64);
+trivial_invariant!(u128);
+trivial_invariant!(usize);
+
+trivial_invariant!(i8);
+trivial_invariant!(i16);
+trivial_invariant!(i32);
+trivial_invariant!(i64);
+trivial_invariant!(i128);
+trivial_invariant!(isize);
+
+// We do not constrain the safety invariant for floating points types.
+// Users can create a new type wrapping the floating point type and define an
+// invariant that checks for NaN, infinite, or subnormal values.
+trivial_invariant!(f32);
+trivial_invariant!(f64);
+
+trivial_invariant!(());
+trivial_invariant!(bool);
+trivial_invariant!(char);
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 341dd6752916..e81ddbe7904b 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -23,6 +23,7 @@ pub mod arbitrary;
 #[cfg(feature = "concrete_playback")]
 mod concrete_playback;
 pub mod futures;
+pub mod invariant;
 pub mod mem;
 pub mod shadow;
 pub mod slice;
@@ -37,6 +38,7 @@ mod models;
 pub use arbitrary::Arbitrary;
 #[cfg(feature = "concrete_playback")]
 pub use concrete_playback::concrete_playback_run;
+pub use invariant::Invariant;
 
 #[cfg(not(feature = "concrete_playback"))]
 /// NOP `concrete_playback` for type checking during verification mode.
diff --git a/tests/kani/Invariant/invariant_impls.rs b/tests/kani/Invariant/invariant_impls.rs
new file mode 100644
index 000000000000..4f00f4134956
--- /dev/null
+++ b/tests/kani/Invariant/invariant_impls.rs
@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check the `Invariant` implementations that we include in the Kani library
+//! with respect to the underlying type invariants.
+extern crate kani;
+use kani::Invariant;
+
+macro_rules! check_safe_type {
+    ( $type: ty ) => {
+        let value: $type = kani::any();
+        assert!(value.is_safe());
+    };
+}
+
+#[kani::proof]
+fn check_safe_impls() {
+    check_safe_type!(u8);
+    check_safe_type!(u16);
+    check_safe_type!(u32);
+    check_safe_type!(u64);
+    check_safe_type!(u128);
+    check_safe_type!(usize);
+
+    check_safe_type!(i8);
+    check_safe_type!(i16);
+    check_safe_type!(i32);
+    check_safe_type!(i64);
+    check_safe_type!(i128);
+    check_safe_type!(isize);
+
+    check_safe_type!(f32);
+    check_safe_type!(f64);
+
+    check_safe_type!(());
+    check_safe_type!(bool);
+    check_safe_type!(char);
+}
diff --git a/tests/kani/Invariant/percentage.rs b/tests/kani/Invariant/percentage.rs
new file mode 100644
index 000000000000..f3976f48e249
--- /dev/null
+++ b/tests/kani/Invariant/percentage.rs
@@ -0,0 +1,62 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `Invariant` implementation behaves as expected when used on a
+//! custom type.
+
+extern crate kani;
+use kani::Invariant;
+
+// We use the default `Arbitrary` implementation, which allows values that
+// shouldn't be considered safe for the `Percentage` type.
+#[derive(kani::Arbitrary)]
+struct Percentage(u8);
+
+impl Percentage {
+    pub fn try_new(val: u8) -> Result<Self, String> {
+        if val <= 100 {
+            Ok(Self(val))
+        } else {
+            Err(String::from("error: invalid percentage value"))
+        }
+    }
+
+    pub fn value(&self) -> u8 {
+        self.0
+    }
+
+    pub fn increase(&self, other: u8) -> Percentage {
+        let amount = self.0 + other;
+        Percentage::try_new(amount.min(100)).unwrap()
+    }
+}
+
+impl kani::Invariant for Percentage {
+    fn is_safe(&self) -> bool {
+        self.0 <= 100
+    }
+}
+
+#[kani::proof]
+fn check_assume_safe() {
+    let percentage: Percentage = kani::any();
+    kani::assume(percentage.is_safe());
+    assert!(percentage.value() <= 100);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_assert_safe() {
+    let percentage: Percentage = kani::any();
+    assert!(percentage.is_safe());
+}
+
+#[kani::proof]
+fn check_increase_safe() {
+    let percentage: Percentage = kani::any();
+    kani::assume(percentage.is_safe());
+    let amount = kani::any();
+    kani::assume(amount <= 100);
+    let new_percentage = percentage.increase(amount);
+    assert!(new_percentage.is_safe());
+}

From e9eeef72d0d6617019b0f46d67e471f13e2120e8 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 6 Jun 2024 13:53:34 -0700
Subject: [PATCH 3/5] Remove empty box creation from contracts impl (#3233)

There seems to be an issue in CBMC contracts implementation that it
assumes that `free` must have a body. However, slicing can remove `free`
body if the harness does not allocate anything.

https://github.com/diffblue/cbmc/issues/8317

We used to create an empty Box before to force `free` to be in scope.
Instead, just invoke `free(NULL)` which is a no-op.

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

Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
---
 .../codegen_cprover_gotoc/overrides/hooks.rs  | 40 +++++++++++++++++++
 library/kani/src/internal.rs                  | 14 +++++++
 .../kani_macros/src/sysroot/contracts/mod.rs  |  2 +-
 3 files changed, 55 insertions(+), 1 deletion(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index 9b2f9e770d32..d66e16b6ce59 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -458,6 +458,45 @@ impl GotocHook for UntrackedDeref {
     }
 }
 
+struct InitContracts;
+
+/// CBMC contracts currently has a limitation where `free` has to be in scope.
+/// However, if there is no dynamic allocation in the harness, slicing removes `free` from the
+/// scope.
+///
+/// Thus, this function will basically translate into:
+/// ```c
+/// // This is a no-op.
+/// free(NULL);
+/// ```
+impl GotocHook for InitContracts {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniInitContracts")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 0,);
+        let loc = gcx.codegen_span_stable(span);
+        Stmt::block(
+            vec![
+                BuiltinFn::Free
+                    .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc)
+                    .as_stmt(loc),
+                Stmt::goto(bb_label(target.unwrap()), loc),
+            ],
+            loc,
+        )
+    }
+}
+
 pub fn fn_hooks() -> GotocHooks {
     GotocHooks {
         hooks: vec![
@@ -472,6 +511,7 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
             Rc::new(UntrackedDeref),
+            Rc::new(InitContracts),
         ],
     }
 }
diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
index d2f2970d1c05..a910c333b112 100644
--- a/library/kani/src/internal.rs
+++ b/library/kani/src/internal.rs
@@ -76,3 +76,17 @@ impl<'a, T> Pointer<'a> for *mut T {
 pub fn untracked_deref<T>(_: &T) -> T {
     todo!()
 }
+
+/// CBMC contracts currently has a limitation where `free` has to be in scope.
+/// However, if there is no dynamic allocation in the harness, slicing removes `free` from the
+/// scope.
+///
+/// Thus, this function will basically translate into:
+/// ```c
+/// // This is a no-op.
+/// free(NULL);
+/// ```
+#[inline(never)]
+#[doc(hidden)]
+#[rustc_diagnostic_item = "KaniInitContracts"]
+pub fn init_contracts() {}
diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index bef6f8d921bc..de3b5da123ed 100644
--- a/library/kani_macros/src/sysroot/contracts/mod.rs
+++ b/library/kani_macros/src/sysroot/contracts/mod.rs
@@ -294,7 +294,7 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream {
         #[kanitool::proof_for_contract = stringify!(#args)]
         #(#attrs)*
         #vis #sig {
-            let _ = std::boxed::Box::new(0_usize);
+            kani::internal::init_contracts();
             #block
         }
     )

From dcbf3aafa92e5c40e1eb7da7c5475b152c4222d5 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 6 Jun 2024 15:13:12 -0700
Subject: [PATCH 4/5] Add a new verify-std subcommand to Kani (#3231)

This subcommand will take the path to the standard library.

It will then use `cargo build -Z build-std` to build the custom standard
library and verify any harness found during the build.

## Call out

- So far I only performed manual tests. I'm going to add a few unit
tests and a script in the next revision.

Resolves #3226

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

---------

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
---
 kani-compiler/src/kani_middle/intrinsics.rs   |   7 +-
 kani-driver/src/args/mod.rs                   |  10 ++
 kani-driver/src/args/std_args.rs              |  77 +++++++++++
 kani-driver/src/call_cargo.rs                 | 125 ++++++++++++------
 kani-driver/src/call_single_file.rs           |  56 +++++---
 kani-driver/src/concrete_playback/playback.rs |   6 +-
 kani-driver/src/main.rs                       |  33 +++--
 kani-driver/src/project.rs                    |  32 +++++
 kani-driver/src/session.rs                    |   5 +
 kani_metadata/src/unstable.rs                 |   4 +-
 library/kani_core/src/lib.rs                  |   3 +
 tools/build-kani/src/main.rs                  |   3 +-
 12 files changed, 290 insertions(+), 71 deletions(-)
 create mode 100644 kani-driver/src/args/std_args.rs

diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs
index 51e6140b7e1a..82a75a91f1ad 100644
--- a/kani-compiler/src/kani_middle/intrinsics.rs
+++ b/kani-compiler/src/kani_middle/intrinsics.rs
@@ -57,7 +57,12 @@ impl<'tcx> ModelIntrinsics<'tcx> {
         let arg_ty = args[0].node.ty(&self.local_decls, tcx);
         if arg_ty.is_simd() {
             // Get the stub definition.
-            let stub_id = tcx.get_diagnostic_item(Symbol::intern("KaniModelSimdBitmask")).unwrap();
+            let Some(stub_id) = tcx.get_diagnostic_item(Symbol::intern("KaniModelSimdBitmask"))
+            else {
+                // This should only happen when verifying the standard library.
+                // We don't need to warn here, since the backend will print unsupported constructs.
+                return;
+            };
             debug!(?func, ?stub_id, "replace_simd_bitmask");
 
             // Get SIMD information from the type.
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 36d9e0af2d0e..f0c9cb0c4e8d 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -6,6 +6,7 @@ pub mod assess_args;
 pub mod cargo;
 pub mod common;
 pub mod playback_args;
+pub mod std_args;
 
 pub use assess_args::*;
 
@@ -90,6 +91,8 @@ pub struct StandaloneArgs {
 pub enum StandaloneSubcommand {
     /// Execute concrete playback testcases of a local crate.
     Playback(Box<playback_args::KaniPlaybackArgs>),
+    /// Verify the rust standard library.
+    VerifyStd(Box<std_args::VerifyStdArgs>),
 }
 
 #[derive(Debug, clap::Parser)]
@@ -448,6 +451,13 @@ fn check_no_cargo_opt(is_set: bool, name: &str) -> Result<(), Error> {
 impl ValidateArgs for StandaloneArgs {
     fn validate(&self) -> Result<(), Error> {
         self.verify_opts.validate()?;
+
+        match &self.command {
+            Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?,
+            // TODO: Invoke PlaybackArgs::validate()
+            None | Some(StandaloneSubcommand::Playback(..)) => {}
+        };
+
         // Cargo target arguments.
         check_no_cargo_opt(self.verify_opts.target.bins, "--bins")?;
         check_no_cargo_opt(self.verify_opts.target.lib, "--lib")?;
diff --git a/kani-driver/src/args/std_args.rs b/kani-driver/src/args/std_args.rs
new file mode 100644
index 000000000000..3818b6261010
--- /dev/null
+++ b/kani-driver/src/args/std_args.rs
@@ -0,0 +1,77 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Implements the `verify-std` subcommand handling.
+
+use crate::args::{ValidateArgs, VerificationArgs};
+use clap::error::ErrorKind;
+use clap::{Error, Parser};
+use kani_metadata::UnstableFeature;
+use std::path::PathBuf;
+
+/// Verify a local version of the Rust standard library.
+///
+/// This is an **unstable option** and it the standard library version must be compatible with
+/// Kani's toolchain version.
+#[derive(Debug, Parser)]
+pub struct VerifyStdArgs {
+    /// The path to the folder containing the crates for the Rust standard library.
+    /// Note that this directory must be named `library` as used in the Rust toolchain and
+    /// repository.
+    pub std_path: PathBuf,
+
+    #[command(flatten)]
+    pub verify_opts: VerificationArgs,
+}
+
+impl ValidateArgs for VerifyStdArgs {
+    fn validate(&self) -> Result<(), Error> {
+        self.verify_opts.validate()?;
+
+        if !self
+            .verify_opts
+            .common_args
+            .unstable_features
+            .contains(UnstableFeature::UnstableOptions)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                "The `verify-std` subcommand is unstable and requires -Z unstable-options",
+            ));
+        }
+
+        if !self.std_path.exists() {
+            Err(Error::raw(
+                ErrorKind::InvalidValue,
+                format!(
+                    "Invalid argument: `<STD_PATH>` argument `{}` does not exist",
+                    self.std_path.display()
+                ),
+            ))
+        } else if !self.std_path.is_dir() {
+            Err(Error::raw(
+                ErrorKind::InvalidValue,
+                format!(
+                    "Invalid argument: `<STD_PATH>` argument `{}` is not a directory",
+                    self.std_path.display()
+                ),
+            ))
+        } else {
+            let full_path = self.std_path.canonicalize()?;
+            let dir = full_path.file_stem().unwrap();
+            if dir != "library" {
+                Err(Error::raw(
+                    ErrorKind::InvalidValue,
+                    format!(
+                        "Invalid argument: Expected `<STD_PATH>` to point to the `library` folder \
+                    containing the standard library crates.\n\
+                    Found `{}` folder instead",
+                        dir.to_string_lossy()
+                    ),
+                ))
+            } else {
+                Ok(())
+            }
+        }
+    }
+}
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 2d5d36306e21..ebf61e153c46 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -2,20 +2,22 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::args::VerificationArgs;
-use crate::call_single_file::to_rustc_arg;
+use crate::call_single_file::{to_rustc_arg, LibConfig};
 use crate::project::Artifact;
-use crate::session::{setup_cargo_command, KaniSession};
+use crate::session::{lib_folder, lib_no_core_folder, setup_cargo_command, KaniSession};
 use crate::util;
 use anyhow::{bail, Context, Result};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
-use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target};
+use cargo_metadata::{
+    Artifact as RustcArtifact, Message, Metadata, MetadataCommand, Package, Target,
+};
 use kani_metadata::{ArtifactType, CompilerArtifactStub};
 use std::ffi::{OsStr, OsString};
 use std::fmt::{self, Display};
 use std::fs::{self, File};
 use std::io::BufReader;
 use std::io::IsTerminal;
-use std::path::PathBuf;
+use std::path::{Path, PathBuf};
 use std::process::Command;
 use tracing::{debug, trace};
 
@@ -43,6 +45,47 @@ pub struct CargoOutputs {
 }
 
 impl KaniSession {
+    /// Create a new cargo library in the given path.
+    pub fn cargo_init_lib(&self, path: &Path) -> Result<()> {
+        let mut cmd = setup_cargo_command()?;
+        cmd.args(["init", "--lib", path.to_string_lossy().as_ref()]);
+        self.run_terminal(cmd)
+    }
+
+    pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result<Vec<Artifact>> {
+        let lib_path = lib_no_core_folder().unwrap();
+        let mut rustc_args = self.kani_rustc_flags(LibConfig::new_no_core(lib_path));
+        rustc_args.push(to_rustc_arg(self.kani_compiler_flags()).into());
+        rustc_args.push(self.reachability_arg().into());
+
+        let mut cargo_args: Vec<OsString> = vec!["build".into()];
+        cargo_args.append(&mut cargo_config_args());
+
+        // Configuration needed to parse cargo compilation status.
+        cargo_args.push("--message-format".into());
+        cargo_args.push("json-diagnostic-rendered-ansi".into());
+        cargo_args.push("-Z".into());
+        cargo_args.push("build-std=panic_abort,core,std".into());
+
+        if self.args.common_args.verbose {
+            cargo_args.push("-v".into());
+        }
+
+        // Since we are verifying the standard library, we set the reachability to all crates.
+        let mut cmd = setup_cargo_command()?;
+        cmd.args(&cargo_args)
+            .current_dir(krate_path)
+            .env("RUSTC", &self.kani_compiler)
+            // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
+            // https://doc.rust-lang.org/cargo/reference/environment-variables.html
+            .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
+            .env("CARGO_TERM_PROGRESS_WHEN", "never")
+            .env("__CARGO_TESTS_ONLY_SRC_ROOT", std_path.as_os_str());
+
+        let build_artifacts = self.run_build(cmd)?;
+        Ok(build_artifacts.into_iter().filter_map(map_kani_artifact).collect())
+    }
+
     /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir`
     pub fn cargo_build(&self, keep_going: bool) -> Result<CargoOutputs> {
         let build_target = env!("TARGET"); // see build.rs
@@ -60,7 +103,8 @@ impl KaniSession {
             fs::remove_dir_all(&target_dir)?;
         }
 
-        let mut rustc_args = self.kani_rustc_flags();
+        let lib_path = lib_folder().unwrap();
+        let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
         rustc_args.push(to_rustc_arg(self.kani_compiler_flags()).into());
 
         let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
@@ -120,7 +164,7 @@ impl KaniSession {
                     .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
                     .env("CARGO_TERM_PROGRESS_WHEN", "never");
 
-                match self.run_cargo(cmd, verification_target.target()) {
+                match self.run_build_target(cmd, verification_target.target()) {
                     Err(err) => {
                         if keep_going {
                             let target_str = format!("{verification_target}");
@@ -179,9 +223,9 @@ impl KaniSession {
 
     /// Run cargo and collect any error found.
     /// We also collect the metadata file generated during compilation if any.
-    fn run_cargo(&self, cargo_cmd: Command, target: &Target) -> Result<Option<Artifact>> {
+    fn run_build(&self, cargo_cmd: Command) -> Result<Vec<RustcArtifact>> {
         let support_color = std::io::stdout().is_terminal();
-        let mut artifact = None;
+        let mut artifacts = vec![];
         if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? {
             let reader = BufReader::new(cargo_process.stdout.take().unwrap());
             let mut error_count = 0;
@@ -211,33 +255,9 @@ impl KaniSession {
                         }
                     },
                     Message::CompilerArtifact(rustc_artifact) => {
-                        /// Compares two targets, and falls back to a weaker
-                        /// comparison where we avoid dashes in their names.
-                        fn same_target(t1: &Target, t2: &Target) -> bool {
-                            (t1 == t2)
-                                || (t1.name.replace('-', "_") == t2.name.replace('-', "_")
-                                    && t1.kind == t2.kind
-                                    && t1.src_path == t2.src_path
-                                    && t1.edition == t2.edition
-                                    && t1.doctest == t2.doctest
-                                    && t1.test == t2.test
-                                    && t1.doc == t2.doc)
-                        }
-                        // This used to be `rustc_artifact == *target`, but it
-                        // started to fail after the `cargo` change in
-                        // <https://github.com/rust-lang/cargo/pull/12783>
-                        //
-                        // We should revisit this check after a while to see if
-                        // it's not needed anymore or it can be restricted to
-                        // certain cases.
-                        // TODO: <https://github.com/model-checking/kani/issues/3111>
-                        if same_target(&rustc_artifact.target, target) {
-                            debug_assert!(
-                                artifact.is_none(),
-                                "expected only one artifact for `{target:?}`",
-                            );
-                            artifact = Some(rustc_artifact);
-                        }
+                        // Compares two targets, and falls back to a weaker
+                        // comparison where we avoid dashes in their names.
+                        artifacts.push(rustc_artifact)
                     }
                     Message::BuildScriptExecuted(_) | Message::BuildFinished(_) => {
                         // do nothing
@@ -263,11 +283,40 @@ impl KaniSession {
                 );
             }
         }
+        Ok(artifacts)
+    }
+
+    /// Run cargo and collect any error found.
+    /// We also collect the metadata file generated during compilation if any for the given target.
+    fn run_build_target(&self, cargo_cmd: Command, target: &Target) -> Result<Option<Artifact>> {
+        /// This used to be `rustc_artifact == *target`, but it
+        /// started to fail after the `cargo` change in
+        /// <https://github.com/rust-lang/cargo/pull/12783>
+        ///
+        /// We should revisit this check after a while to see if
+        /// it's not needed anymore or it can be restricted to
+        /// certain cases.
+        /// TODO: <https://github.com/model-checking/kani/issues/3111>
+        fn same_target(t1: &Target, t2: &Target) -> bool {
+            (t1 == t2)
+                || (t1.name.replace('-', "_") == t2.name.replace('-', "_")
+                    && t1.kind == t2.kind
+                    && t1.src_path == t2.src_path
+                    && t1.edition == t2.edition
+                    && t1.doctest == t2.doctest
+                    && t1.test == t2.test
+                    && t1.doc == t2.doc)
+        }
+
+        let artifacts = self.run_build(cargo_cmd)?;
+        debug!(?artifacts, "run_build_target");
+
         // We generate kani specific artifacts only for the build target. The build target is
         // always the last artifact generated in a build, and all the other artifacts are related
-        // to dependencies or build scripts. Hence, we need to invoke `map_kani_artifact` only
-        // for the last compiler artifact.
-        Ok(artifact.and_then(map_kani_artifact))
+        // to dependencies or build scripts.
+        Ok(artifacts.into_iter().rev().find_map(|artifact| {
+            if same_target(&artifact.target, target) { map_kani_artifact(artifact) } else { None }
+        }))
     }
 }
 
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 1c8d63d6d87a..335d9840e0e7 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -9,6 +9,39 @@ use std::process::Command;
 
 use crate::session::{lib_folder, KaniSession};
 
+pub struct LibConfig {
+    args: Vec<OsString>,
+}
+
+impl LibConfig {
+    pub fn new(path: PathBuf) -> LibConfig {
+        let sysroot = &path.parent().unwrap();
+        let kani_std_rlib = path.join("libstd.rlib");
+        let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap());
+        let args = [
+            "--sysroot",
+            sysroot.to_str().unwrap(),
+            "-L",
+            path.to_str().unwrap(),
+            "--extern",
+            "kani",
+            "--extern",
+            kani_std_wrapper.as_str(),
+        ]
+        .map(OsString::from)
+        .to_vec();
+        LibConfig { args }
+    }
+
+    pub fn new_no_core(path: PathBuf) -> LibConfig {
+        LibConfig {
+            args: ["-L", path.to_str().unwrap(), "--extern", "kani_core"]
+                .map(OsString::from)
+                .to_vec(),
+        }
+    }
+}
+
 impl KaniSession {
     /// Used by `kani` and not `cargo-kani` to process a single Rust file into a `.symtab.json`
     // TODO: Move these functions to be part of the builder.
@@ -21,7 +54,8 @@ impl KaniSession {
         let mut kani_args = self.kani_compiler_flags();
         kani_args.push(format!("--reachability={}", self.reachability_mode()));
 
-        let mut rustc_args = self.kani_rustc_flags();
+        let lib_path = lib_folder().unwrap();
+        let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
         rustc_args.push(file.into());
         rustc_args.push("--out-dir".into());
         rustc_args.push(OsString::from(outdir.as_os_str()));
@@ -119,9 +153,8 @@ impl KaniSession {
     }
 
     /// This function generates all rustc configurations required by our goto-c codegen.
-    pub fn kani_rustc_flags(&self) -> Vec<OsString> {
-        let lib_path = lib_folder().unwrap();
-        let mut flags: Vec<_> = base_rustc_flags(lib_path);
+    pub fn kani_rustc_flags(&self, lib_config: LibConfig) -> Vec<OsString> {
+        let mut flags: Vec<_> = base_rustc_flags(lib_config);
         // We only use panic abort strategy for verification since we cannot handle unwind logic.
         flags.extend_from_slice(
             &[
@@ -156,10 +189,7 @@ impl KaniSession {
 }
 
 /// Common flags used for compiling user code for verification and playback flow.
-pub fn base_rustc_flags(lib_path: PathBuf) -> Vec<OsString> {
-    let kani_std_rlib = lib_path.join("libstd.rlib");
-    let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap());
-    let sysroot = lib_path.parent().unwrap();
+pub fn base_rustc_flags(lib_config: LibConfig) -> Vec<OsString> {
     let mut flags = [
         "-C",
         "overflow-checks=on",
@@ -176,18 +206,12 @@ pub fn base_rustc_flags(lib_path: PathBuf) -> Vec<OsString> {
         "crate-attr=feature(register_tool)",
         "-Z",
         "crate-attr=register_tool(kanitool)",
-        "--sysroot",
-        sysroot.to_str().unwrap(),
-        "-L",
-        lib_path.to_str().unwrap(),
-        "--extern",
-        "kani",
-        "--extern",
-        kani_std_wrapper.as_str(),
     ]
     .map(OsString::from)
     .to_vec();
 
+    flags.extend(lib_config.args);
+
     // e.g. compiletest will set 'compile-flags' here and we should pass those down to rustc
     // and we fail in `tests/kani/Match/match_bool.rs`
     if let Ok(str) = std::env::var("RUSTFLAGS") {
diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs
index d8c1762da92b..c56694ad32fd 100644
--- a/kani-driver/src/concrete_playback/playback.rs
+++ b/kani-driver/src/concrete_playback/playback.rs
@@ -6,7 +6,7 @@
 use crate::args::common::Verbosity;
 use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFormat};
 use crate::call_cargo::cargo_config_args;
-use crate::call_single_file::base_rustc_flags;
+use crate::call_single_file::{base_rustc_flags, LibConfig};
 use crate::session::{lib_playback_folder, setup_cargo_command, InstallType};
 use crate::{session, util};
 use anyhow::Result;
@@ -70,7 +70,7 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result<PathBuf>
         util::info_operation("Building", args.input.to_string_lossy().deref());
     }
 
-    let mut rustc_args = base_rustc_flags(lib_playback_folder()?);
+    let mut rustc_args = base_rustc_flags(LibConfig::new(lib_playback_folder()?));
     rustc_args.push("--test".into());
     rustc_args.push(OsString::from(&args.input));
     rustc_args.push(format!("--crate-name={TEST_BIN_NAME}").into());
@@ -96,7 +96,7 @@ fn cargo_test(args: CargoPlaybackArgs) -> Result<()> {
     let install = InstallType::new()?;
     let mut cmd = setup_cargo_command()?;
 
-    let rustc_args = base_rustc_flags(lib_playback_folder()?);
+    let rustc_args = base_rustc_flags(LibConfig::new(lib_playback_folder()?));
     let mut cargo_args: Vec<OsString> = vec!["test".into()];
 
     if args.playback.common_opts.verbose() {
diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index 798625560970..3bb38ed1294c 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -94,17 +94,28 @@ fn standalone_main() -> Result<()> {
     let args = args::StandaloneArgs::parse();
     check_is_valid(&args);
 
-    if let Some(StandaloneSubcommand::Playback(args)) = args.command {
-        return playback_standalone(*args);
-    }
-
-    let session = session::KaniSession::new(args.verify_opts)?;
-
-    if !session.args.common_args.quiet {
-        print_kani_version(InvocationType::Standalone);
-    }
-
-    let project = project::standalone_project(&args.input.unwrap(), args.crate_name, &session)?;
+    let (session, project) = match args.command {
+        Some(StandaloneSubcommand::Playback(args)) => return playback_standalone(*args),
+        Some(StandaloneSubcommand::VerifyStd(args)) => {
+            let session = KaniSession::new(args.verify_opts)?;
+            if !session.args.common_args.quiet {
+                print_kani_version(InvocationType::Standalone);
+            }
+
+            let project = project::std_project(&args.std_path, &session)?;
+            (session, project)
+        }
+        None => {
+            let session = KaniSession::new(args.verify_opts)?;
+            if !session.args.common_args.quiet {
+                print_kani_version(InvocationType::Standalone);
+            }
+
+            let project =
+                project::standalone_project(&args.input.unwrap(), args.crate_name, &session)?;
+            (session, project)
+        }
+    };
     if session.args.only_codegen { Ok(()) } else { verify_project(project, session) }
 }
 
diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
index fcf3805ab3df..dfcc9eb3ac46 100644
--- a/kani-driver/src/project.rs
+++ b/kani-driver/src/project.rs
@@ -23,6 +23,8 @@ use anyhow::{Context, Result};
 use kani_metadata::{
     artifact::convert_type, ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata,
 };
+use std::env::current_dir;
+use std::fs;
 use std::fs::File;
 use std::io::BufWriter;
 use std::ops::Deref;
@@ -383,3 +385,33 @@ fn standalone_artifact(out_dir: &Path, crate_name: &String, typ: ArtifactType) -
     let _ = path.set_extension(typ);
     Artifact { path, typ }
 }
+
+/// Verify the custom version of the standard library in the given path.
+///
+/// Note that we assume that `std_path` points to a directory named "library".
+/// This should be checked as part of the argument validation.
+pub(crate) fn std_project(std_path: &Path, session: &KaniSession) -> Result<Project> {
+    // Create output directory
+    let outdir = if let Some(target_dir) = &session.args.target_dir {
+        target_dir.clone()
+    } else {
+        current_dir()?.join("target")
+    };
+    fs::create_dir_all(&outdir)?; // This is a no-op if directory exists.
+    let outdir = outdir.canonicalize()?;
+
+    // Create dummy crate needed to build using `cargo -Z build-std`
+    let dummy_crate = outdir.join("kani_verify_std");
+    if dummy_crate.exists() {
+        fs::remove_dir_all(&dummy_crate)?;
+    }
+    session.cargo_init_lib(&dummy_crate)?;
+
+    // Build cargo project for dummy crate.
+    let std_path = std_path.canonicalize()?;
+    let outputs = session.cargo_build_std(std_path.parent().unwrap(), &dummy_crate)?;
+
+    // Get the metadata and return a Kani project.
+    let metadata = outputs.iter().map(|md_file| from_json(md_file)).collect::<Result<Vec<_>>>()?;
+    Project::try_new(session, outdir, metadata, None, None)
+}
diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
index 8cf4a20450f5..bf02aaef7426 100644
--- a/kani-driver/src/session.rs
+++ b/kani-driver/src/session.rs
@@ -280,6 +280,11 @@ pub fn lib_playback_folder() -> Result<PathBuf> {
     Ok(base_folder()?.join("playback/lib"))
 }
 
+/// Return the path for the folder where the pre-compiled rust libraries with no_core.
+pub fn lib_no_core_folder() -> Result<PathBuf> {
+    Ok(base_folder()?.join("no_core/lib"))
+}
+
 /// Return the base folder for the entire kani installation.
 pub fn base_folder() -> Result<PathBuf> {
     Ok(bin_folder()?
diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs
index d7b73678a836..929322858d2a 100644
--- a/kani_metadata/src/unstable.rs
+++ b/kani_metadata/src/unstable.rs
@@ -87,8 +87,10 @@ pub enum UnstableFeature {
     /// Automatically check that no invalid value is produced which is considered UB in Rust.
     /// Note that this does not include checking uninitialized value.
     ValidValueChecks,
-    /// Ghost state and shadow memory APIs
+    /// Ghost state and shadow memory APIs.
     GhostState,
+    /// Enable an unstable option or subcommand.
+    UnstableOptions,
 }
 
 impl UnstableFeature {
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index 00b5efbe719c..a5cd40d71e92 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -3,3 +3,6 @@
 
 //! This is placeholder for the new `kani_core` library.
 #![feature(no_core)]
+#![no_core]
+
+pub use kani_macros::*;
diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs
index 3f1bc26cfbbb..2c181d69d6e5 100644
--- a/tools/build-kani/src/main.rs
+++ b/tools/build-kani/src/main.rs
@@ -10,7 +10,7 @@
 mod parser;
 mod sysroot;
 
-use crate::sysroot::{build_bin, build_lib, kani_playback_lib, kani_sysroot_lib};
+use crate::sysroot::{build_bin, build_lib, kani_no_core_lib, kani_playback_lib, kani_sysroot_lib};
 use anyhow::{bail, Result};
 use clap::Parser;
 use std::{ffi::OsString, path::Path, process::Command};
@@ -102,6 +102,7 @@ fn bundle_kani(dir: &Path) -> Result<()> {
     // 4. Pre-compiled library files
     cp_dir(&kani_sysroot_lib(), dir)?;
     cp_dir(&kani_playback_lib().parent().unwrap(), dir)?;
+    cp_dir(&kani_no_core_lib().parent().unwrap(), dir)?;
 
     // 5. Record the exact toolchain and rustc version we use
     std::fs::write(dir.join("rust-toolchain-version"), env!("RUSTUP_TOOLCHAIN"))?;

From 0bb1325e5f5e20dfdc89f292fd4bf71e6362066a Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 6 Jun 2024 20:02:22 -0700
Subject: [PATCH 5/5] Add a regression test for running `verify-std` command.
 (#3236)

In #3226, we added a new command that allow Kani to verify properties in
a custom standard library. In this PR, we create a script test that
create a modified version of the standard library and runs Kani against
it.

I also moved the script based tests to run after the more generic
regression jobs. I think the script jobs are a bit harder to debug, they
may take longer, and they are usually very specific to a few features.
So probably best if we run the more generic tests first.
---
 Cargo.toml                                    |  1 +
 kani-driver/src/call_cargo.rs                 |  2 +
 scripts/kani-regression.sh                    |  2 +-
 .../verify_std_cmd/config.yml                 |  4 +
 .../verify_std_cmd/verify_std.expected        | 11 +++
 .../verify_std_cmd/verify_std.sh              | 91 +++++++++++++++++++
 6 files changed, 110 insertions(+), 1 deletion(-)
 create mode 100644 tests/script-based-pre/verify_std_cmd/config.yml
 create mode 100644 tests/script-based-pre/verify_std_cmd/verify_std.expected
 create mode 100755 tests/script-based-pre/verify_std_cmd/verify_std.sh

diff --git a/Cargo.toml b/Cargo.toml
index e4ff44f42ddc..641cbaf961be 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -68,4 +68,5 @@ exclude = [
   "tests/script-based-pre",
   "tests/script-based-pre/build-cache-bin/target/new_dep",
   "tests/script-based-pre/build-cache-dirty/target/new_dep",
+  "tests/script-based-pre/verify_std_cmd/tmp_dir/target/kani_verify_std",
 ]
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index ebf61e153c46..a1d976d73150 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -57,6 +57,8 @@ impl KaniSession {
         let mut rustc_args = self.kani_rustc_flags(LibConfig::new_no_core(lib_path));
         rustc_args.push(to_rustc_arg(self.kani_compiler_flags()).into());
         rustc_args.push(self.reachability_arg().into());
+        // Ignore global assembly, since `compiler_builtins` has some.
+        rustc_args.push(to_rustc_arg(vec!["--ignore-global-asm".to_string()]).into());
 
         let mut cargo_args: Vec<OsString> = vec!["build".into()];
         cargo_args.append(&mut cargo_config_args());
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index dcced313ce0b..d3bb0f7efb45 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -49,7 +49,6 @@ RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-trai
 
 # Declare testing suite information (suite and mode)
 TESTS=(
-    "script-based-pre exec"
     "kani kani"
     "expected expected"
     "ui expected"
@@ -59,6 +58,7 @@ TESTS=(
     "smack kani"
     "cargo-kani cargo-kani"
     "cargo-ui cargo-kani"
+    "script-based-pre exec"
     "coverage coverage-based"
     "kani-docs cargo-kani"
     "kani-fixme kani-fixme"
diff --git a/tests/script-based-pre/verify_std_cmd/config.yml b/tests/script-based-pre/verify_std_cmd/config.yml
new file mode 100644
index 000000000000..f6e398303b79
--- /dev/null
+++ b/tests/script-based-pre/verify_std_cmd/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: verify_std.sh
+expected: verify_std.expected
diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected
new file mode 100644
index 000000000000..aa965f50cdf2
--- /dev/null
+++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected
@@ -0,0 +1,11 @@
+[TEST] Run kani verify-std
+Checking harness kani::check_success...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness kani::check_panic...
+VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+
+Checking harness num::verify::check_non_zero...
+VERIFICATION:- SUCCESSFUL
+
+Complete - 3 successfully verified harnesses, 0 failures, 3 total.
diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh
new file mode 100755
index 000000000000..9e18ed72ca2a
--- /dev/null
+++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh
@@ -0,0 +1,91 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Test `kani verify-std` subcommand.
+# 1. Make a copy of the rust standard library.
+# 2. Add a few Kani definitions to it + a few harnesses
+# 3. Execute Kani
+
+set +e
+
+TMP_DIR="tmp_dir"
+
+rm -rf ${TMP_DIR}
+mkdir ${TMP_DIR}
+
+# Create a custom standard library.
+echo "[TEST] Copy standard library from the current toolchain"
+SYSROOT=$(rustc --print sysroot)
+STD_PATH="${SYSROOT}/lib/rustlib/src/rust/library"
+cp -r "${STD_PATH}" "${TMP_DIR}"
+
+# Insert a small harness in one of the standard library modules.
+CORE_CODE='
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod kani {
+    pub use kani_core::proof;
+
+    #[rustc_diagnostic_item = "KaniAnyRaw"]
+    #[inline(never)]
+    pub fn any_raw_inner<T>() -> T {
+        loop {}
+    }
+
+    #[inline(never)]
+    #[rustc_diagnostic_item = "KaniAssert"]
+    pub const fn assert(cond: bool, msg: &'\''static str) {
+        let _ = cond;
+        let _ = msg;
+    }
+
+    #[kani_core::proof]
+    #[kani_core::should_panic]
+    fn check_panic() {
+        let num: u8 = any_raw_inner();
+        assert!(num != 0, "Found zero");
+    }
+
+    #[kani_core::proof]
+    fn check_success() {
+        let orig: u8 = any_raw_inner();
+        let mid = orig as i8;
+        let new = mid as u8;
+        assert!(orig == new, "Conversion round trip works");
+    }
+}
+'
+
+STD_CODE='
+#[cfg(kani)]
+mod verify {
+    use core::kani;
+    #[kani::proof]
+    fn check_non_zero() {
+        let orig: u32 = kani::any_raw_inner();
+        if let Some(val) = core::num::NonZeroU32::new(orig) {
+            assert!(orig == val.into());
+        } else {
+            assert!(orig == 0);
+        };
+    }
+}
+'
+
+echo "[TEST] Modify library"
+echo "${CORE_CODE}" >> ${TMP_DIR}/library/core/src/lib.rs
+echo "${STD_CODE}" >> ${TMP_DIR}/library/std/src/num.rs
+
+# Note: Prepending with sed doesn't work on MacOs the same way it does in linux.
+# sed -i '1s/^/#![cfg_attr(kani, feature(kani))]\n/' ${TMP_DIR}/library/std/src/lib.rs
+cp ${TMP_DIR}/library/std/src/lib.rs ${TMP_DIR}/std_lib.rs
+echo '#![cfg_attr(kani, feature(kani))]' > ${TMP_DIR}/library/std/src/lib.rs
+cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs
+
+echo "[TEST] Run kani verify-std"
+export RUST_BACKTRACE=1
+kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target"
+
+# Cleanup
+rm -r ${TMP_DIR}