From 03b4cf30bfd4596f85d08769dbad8bb6f7192530 Mon Sep 17 00:00:00 2001
From: Matias Scharager <matias.scharager@gmail.com>
Date: Tue, 28 May 2024 14:40:30 -0400
Subject: [PATCH 01/12] rename_result

---
 .../src/sysroot/contracts/bootstrap.rs        |  4 +-
 .../src/sysroot/contracts/check.rs            |  8 +--
 .../src/sysroot/contracts/initialize.rs       | 50 +++++++++++++++++--
 .../src/sysroot/contracts/replace.rs          | 10 ++--
 .../src/sysroot/contracts/shared.rs           |  2 +-
 5 files changed, 59 insertions(+), 15 deletions(-)

diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
index 8d930fdebda9..aea0c33ad77e 100644
--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -89,9 +89,9 @@ impl<'a> ContractConditionsHandler<'a> {
                     #call_replace(#(#args),*)
                 } else {
                     unsafe { REENTRY = true };
-                    let result = #call_check(#(#also_args),*);
+                    let result_kani_internal = #call_check(#(#also_args),*);
                     unsafe { REENTRY = false };
-                    result
+                    result_kani_internal
                 }
             }
         ));
diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs
index 516bd187ba7f..9a7c54eb13cb 100644
--- a/library/kani_macros/src/sysroot/contracts/check.rs
+++ b/library/kani_macros/src/sysroot/contracts/check.rs
@@ -46,14 +46,14 @@ 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 == "result_kani_internal")
                 ));
 
                 quote!(
                     #arg_copies
                     #(#inner)*
                     #exec_postconditions
-                    result
+                    result_kani_internal
                 )
             }
             ContractConditionsData::Modifies { attr } => {
@@ -96,8 +96,8 @@ impl<'a> ContractConditionsHandler<'a> {
                 quote!(#wrapper_name)
             };
             syn::parse_quote!(
-                let result : #return_type = #wrapper_call(#(#args),*);
-                result
+                let result_kani_internal : #return_type = #wrapper_call(#(#args),*);
+                result_kani_internal
             )
         } 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..344df57cfe5d 100644
--- a/library/kani_macros/src/sysroot/contracts/initialize.rs
+++ b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -7,7 +7,7 @@ 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 syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ItemFn, Signature, parse::ParseStream, parse::Parse, Token};
 
 use super::{
     helpers::{chunks_by, is_token_stream_2_comma, matches_path},
@@ -64,6 +64,22 @@ impl ContractFunctionState {
     }
 }
 
+struct EnsuresParseResult {
+    result_name: Ident,
+    attr: Expr,
+}
+
+impl Parse for EnsuresParseResult {
+    fn parse(input: ParseStream) -> syn::Result<Self> {
+        let mut result_name : Ident = Ident::new("result",Span::call_site());
+        if input.peek2(Token![=>]) {
+            result_name = input.parse()?;
+            let _arrow: Token![=>] = input.parse()?;
+        }
+        Ok(EnsuresParseResult{result_name:result_name, attr:input.parse()?,})
+    }
+}
+
 impl<'a> ContractConditionsHandler<'a> {
     /// Initialize the handler. Constructs the required
     /// [`ContractConditionsType`] depending on `is_requires`.
@@ -81,7 +97,8 @@ impl<'a> ContractConditionsHandler<'a> {
                 ContractConditionsData::Requires { attr: syn::parse(attr)? }
             }
             ContractConditionsType::Ensures => {
-                ContractConditionsData::new_ensures(&annotated_fn.sig, syn::parse(attr)?)
+                let data : EnsuresParseResult = syn::parse(attr)?;
+                ContractConditionsData::new_ensures(&annotated_fn.sig, data.attr, data.result_name)
             }
             ContractConditionsType::Modifies => {
                 ContractConditionsData::new_modifies(attr, &mut output)
@@ -97,8 +114,12 @@ impl ContractConditionsData {
     ///
     /// Renames the [`Ident`]s used in `attr` and stores the translation map in
     /// `argument_names`.
-    fn new_ensures(sig: &Signature, mut attr: Expr) -> Self {
+    fn new_ensures(sig: &Signature, mut attr: Expr, result_name: Ident) -> Self {
         let argument_names = rename_argument_occurrences(sig, &mut attr);
+        
+        let mut ident_rewriter = RenamerResult(&result_name);
+        ident_rewriter.visit_expr_mut(&mut attr);
+
         ContractConditionsData::Ensures { argument_names, attr }
     }
 
@@ -167,6 +188,29 @@ impl<'ast> Visit<'ast> for ArgumentIdentCollector {
     }
 }
 
+/// renames the ident to the internal result variable
+struct RenamerResult<'a>(&'a Ident);
+
+impl<'a> VisitMut for RenamerResult<'a> {
+    fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) {
+        if i.path.segments.len() == 1 {
+            i.path
+                .segments
+                .first_mut()
+                .map(|p| if p.ident == *self.0 {p.ident = Ident::new("result_kani_internal",Span::call_site())});
+        }
+    }
+
+    /// This restores shadowing. Without this we would rename all ident
+    /// occurrences, but not rebinding location. This is because our
+    /// [`Self::visit_expr_path_mut`] is scope-unaware.
+    fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) {
+        if i.ident == *self.0 {
+            i.ident = Ident::new("result_kani_internal",Span::call_site())
+        }
+    }
+}
+
 /// Applies the contained renaming (key renamed to value) to every ident pattern
 /// and ident expr visited.
 struct Renamer<'a>(&'a HashMap<Ident, Ident>);
diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs
index 28e401c22d48..7c298bfd3d36 100644
--- a/library/kani_macros/src/sysroot/contracts/replace.rs
+++ b/library/kani_macros/src/sysroot/contracts/replace.rs
@@ -39,7 +39,7 @@ 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![])
+            (vec![syn::parse_quote!(let result_kani_internal : #return_type = kani::any_modifies();)], vec![])
         } else {
             let stmts = &self.annotated_fn.block.stmts;
             let idx = stmts
@@ -74,7 +74,7 @@ impl<'a> ContractConditionsHandler<'a> {
                     kani::assert(#attr, stringify!(#attr_copy));
                     #(#before)*
                     #(#after)*
-                    result
+                    result_kani_internal
                 )
             }
             ContractConditionsData::Ensures { attr, argument_names } => {
@@ -85,7 +85,7 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#after)*
                     kani::assume(#attr);
                     #copy_clean
-                    result
+                    result_kani_internal
                 )
             }
             ContractConditionsData::Modifies { attr } => {
@@ -93,7 +93,7 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#before)*
                     #(*unsafe { kani::internal::Pointer::assignable(#attr) } = kani::any_modifies();)*
                     #(#after)*
-                    result
+                    result_kani_internal
                 )
             }
         }
@@ -126,7 +126,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..0a4612202a50 100644
--- a/library/kani_macros/src/sysroot/contracts/shared.rs
+++ b/library/kani_macros/src/sysroot/contracts/shared.rs
@@ -114,7 +114,7 @@ macro_rules! try_as_result_assign_pat {
                     ident: result_ident,
                     subpat: None,
                     ..
-                }) if result_ident == "result"
+                }) if result_ident == "result_kani_internal"
             ) => init.$convert(),
             _ => None,
         }

From 6403650ab5846888e4361ef613e1a1155031e461 Mon Sep 17 00:00:00 2001
From: Matias Scharager <matias.scharager@gmail.com>
Date: Tue, 28 May 2024 15:08:13 -0400
Subject: [PATCH 02/12] globalize result name

---
 .../src/sysroot/contracts/bootstrap.rs           |  9 +++++----
 .../kani_macros/src/sysroot/contracts/check.rs   | 12 +++++++-----
 .../src/sysroot/contracts/initialize.rs          |  6 +++---
 library/kani_macros/src/sysroot/contracts/mod.rs |  2 ++
 .../kani_macros/src/sysroot/contracts/replace.rs | 16 ++++++++++------
 .../kani_macros/src/sysroot/contracts/shared.rs  |  4 ++--
 6 files changed, 29 insertions(+), 20 deletions(-)

diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
index aea0c33ad77e..141b04c7afa3 100644
--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -4,11 +4,11 @@
 //! 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 +80,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 +90,9 @@ impl<'a> ContractConditionsHandler<'a> {
                     #call_replace(#(#args),*)
                 } else {
                     unsafe { REENTRY = true };
-                    let result_kani_internal = #call_check(#(#also_args),*);
+                    let #result = #call_check(#(#also_args),*);
                     unsafe { REENTRY = false };
-                    result_kani_internal
+                    #result
                 }
             }
         ));
diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs
index 9a7c54eb13cb..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_kani_internal")
+                        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_kani_internal
+                    #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_kani_internal : #return_type = #wrapper_call(#(#args),*);
-                result_kani_internal
+                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 344df57cfe5d..49bc20de6361 100644
--- a/library/kani_macros/src/sysroot/contracts/initialize.rs
+++ b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -12,7 +12,7 @@ use syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ItemFn, Sig
 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 {
@@ -197,7 +197,7 @@ impl<'a> VisitMut for RenamerResult<'a> {
             i.path
                 .segments
                 .first_mut()
-                .map(|p| if p.ident == *self.0 {p.ident = Ident::new("result_kani_internal",Span::call_site())});
+                .map(|p| if p.ident == *self.0 {p.ident = Ident::new(INTERNAL_RESULT_IDENT,Span::call_site())});
         }
     }
 
@@ -206,7 +206,7 @@ impl<'a> VisitMut for RenamerResult<'a> {
     /// [`Self::visit_expr_path_mut`] is scope-unaware.
     fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) {
         if i.ident == *self.0 {
-            i.ident = Ident::new("result_kani_internal",Span::call_site())
+            i.ident = Ident::new(INTERNAL_RESULT_IDENT,Span::call_site())
         }
     }
 }
diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index 02d2b98eb8db..001d6225dc7b 100644
--- a/library/kani_macros/src/sysroot/contracts/mod.rs
+++ b/library/kani_macros/src/sysroot/contracts/mod.rs
@@ -243,6 +243,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 7c298bfd3d36..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_kani_internal : #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_kani_internal
+                    #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_kani_internal
+                    #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_kani_internal
+                    #result
                 )
             }
         }
diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs
index 0a4612202a50..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_kani_internal"
+                }) if result_ident == INTERNAL_RESULT_IDENT
             ) => init.$convert(),
             _ => None,
         }

From 679c39e1f20e5010ed468e6725747ae03649407a Mon Sep 17 00:00:00 2001
From: Matias Scharager <matias.scharager@gmail.com>
Date: Wed, 29 May 2024 20:03:35 -0400
Subject: [PATCH 03/12] closure syntax

---
 .../src/sysroot/contracts/initialize.rs       | 54 +++----------------
 1 file changed, 7 insertions(+), 47 deletions(-)

diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs
index 49bc20de6361..f4d9f57901fd 100644
--- a/library/kani_macros/src/sysroot/contracts/initialize.rs
+++ b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -7,7 +7,8 @@ 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, parse::ParseStream, parse::Parse, Token};
+use syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ExprClosure, ItemFn, Signature};
+use quote::quote;
 
 use super::{
     helpers::{chunks_by, is_token_stream_2_comma, matches_path},
@@ -64,22 +65,6 @@ impl ContractFunctionState {
     }
 }
 
-struct EnsuresParseResult {
-    result_name: Ident,
-    attr: Expr,
-}
-
-impl Parse for EnsuresParseResult {
-    fn parse(input: ParseStream) -> syn::Result<Self> {
-        let mut result_name : Ident = Ident::new("result",Span::call_site());
-        if input.peek2(Token![=>]) {
-            result_name = input.parse()?;
-            let _arrow: Token![=>] = input.parse()?;
-        }
-        Ok(EnsuresParseResult{result_name:result_name, attr:input.parse()?,})
-    }
-}
-
 impl<'a> ContractConditionsHandler<'a> {
     /// Initialize the handler. Constructs the required
     /// [`ContractConditionsType`] depending on `is_requires`.
@@ -97,8 +82,10 @@ impl<'a> ContractConditionsHandler<'a> {
                 ContractConditionsData::Requires { attr: syn::parse(attr)? }
             }
             ContractConditionsType::Ensures => {
-                let data : EnsuresParseResult = syn::parse(attr)?;
-                ContractConditionsData::new_ensures(&annotated_fn.sig, data.attr, data.result_name)
+                let data : ExprClosure = syn::parse(attr)?;
+                let result : Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+                let attr : Expr = Expr::Verbatim(quote!((#data)(#result)));
+                ContractConditionsData::new_ensures(&annotated_fn.sig, attr)
             }
             ContractConditionsType::Modifies => {
                 ContractConditionsData::new_modifies(attr, &mut output)
@@ -114,12 +101,8 @@ impl ContractConditionsData {
     ///
     /// Renames the [`Ident`]s used in `attr` and stores the translation map in
     /// `argument_names`.
-    fn new_ensures(sig: &Signature, mut attr: Expr, result_name: Ident) -> Self {
+    fn new_ensures(sig: &Signature, mut attr: Expr) -> Self {
         let argument_names = rename_argument_occurrences(sig, &mut attr);
-        
-        let mut ident_rewriter = RenamerResult(&result_name);
-        ident_rewriter.visit_expr_mut(&mut attr);
-
         ContractConditionsData::Ensures { argument_names, attr }
     }
 
@@ -188,29 +171,6 @@ impl<'ast> Visit<'ast> for ArgumentIdentCollector {
     }
 }
 
-/// renames the ident to the internal result variable
-struct RenamerResult<'a>(&'a Ident);
-
-impl<'a> VisitMut for RenamerResult<'a> {
-    fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) {
-        if i.path.segments.len() == 1 {
-            i.path
-                .segments
-                .first_mut()
-                .map(|p| if p.ident == *self.0 {p.ident = Ident::new(INTERNAL_RESULT_IDENT,Span::call_site())});
-        }
-    }
-
-    /// This restores shadowing. Without this we would rename all ident
-    /// occurrences, but not rebinding location. This is because our
-    /// [`Self::visit_expr_path_mut`] is scope-unaware.
-    fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) {
-        if i.ident == *self.0 {
-            i.ident = Ident::new(INTERNAL_RESULT_IDENT,Span::call_site())
-        }
-    }
-}
-
 /// Applies the contained renaming (key renamed to value) to every ident pattern
 /// and ident expr visited.
 struct Renamer<'a>(&'a HashMap<Ident, Ident>);

From 713f4124edd7b7e9bb83367618348236b8aeb07c Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Thu, 30 May 2024 16:09:18 -0400
Subject: [PATCH 04/12] attempting to fix tests

---
 library/kani_macros/src/sysroot/contracts/bootstrap.rs |  5 ++++-
 .../kani_macros/src/sysroot/contracts/initialize.rs    | 10 ++++++----
 library/kani_macros/src/sysroot/contracts/mod.rs       |  2 +-
 .../function-contract/arbitrary_ensures_fail.rs        |  2 +-
 .../function-contract/arbitrary_ensures_pass.rs        |  2 +-
 .../function-contract/arbitrary_requires_fail.rs       |  2 +-
 tests/expected/function-contract/attribute_complain.rs |  2 +-
 .../function-contract/attribute_no_complain.rs         |  2 +-
 .../function-contract/checking_from_external_mod.rs    |  2 +-
 tests/expected/function-contract/checking_in_impl.rs   |  2 +-
 tests/expected/function-contract/fail_on_two.rs        |  4 ++--
 tests/expected/function-contract/gcd_failure_code.rs   |  2 +-
 .../expected/function-contract/gcd_failure_contract.rs |  2 +-
 tests/expected/function-contract/gcd_rec_code_fail.rs  |  2 +-
 .../function-contract/gcd_rec_comparison_pass.rs       |  2 +-
 .../function-contract/gcd_rec_contract_fail.rs         |  2 +-
 .../function-contract/gcd_rec_replacement_pass.rs      |  2 +-
 .../expected/function-contract/gcd_rec_simple_pass.rs  |  2 +-
 .../expected/function-contract/gcd_replacement_fail.rs |  2 +-
 .../expected/function-contract/gcd_replacement_pass.rs |  2 +-
 tests/expected/function-contract/gcd_success.rs        |  2 +-
 .../modifies/check_only_verification.rs                |  2 +-
 tests/expected/function-contract/modifies/expr_pass.rs |  2 +-
 .../function-contract/modifies/expr_replace_pass.rs    |  2 +-
 .../modifies/fail_missing_recursion_attr.rs            |  2 +-
 .../function-contract/modifies/field_replace_pass.rs   |  2 +-
 .../function-contract/modifies/global_replace_pass.rs  |  2 +-
 .../expected/function-contract/modifies/havoc_pass.rs  |  2 +-
 .../function-contract/modifies/havoc_pass_reordered.rs |  2 +-
 .../modifies/mistake_condition_return.rs               |  4 ++--
 .../function-contract/modifies/unique_arguments.rs     |  4 ++--
 tests/expected/function-contract/modifies/vec_pass.rs  |  2 +-
 tests/expected/function-contract/pattern_use.rs        |  2 +-
 .../prohibit-pointers/allowed_const_ptr.rs             |  2 +-
 .../prohibit-pointers/allowed_mut_ref.rs               |  2 +-
 .../prohibit-pointers/allowed_mut_return_ref.rs        |  2 +-
 .../function-contract/prohibit-pointers/allowed_ref.rs |  2 +-
 .../function-contract/prohibit-pointers/hidden.rs      |  2 +-
 .../prohibit-pointers/plain_pointer.rs                 |  2 +-
 .../prohibit-pointers/return_pointer.rs                |  2 +-
 .../expected/function-contract/simple_ensures_fail.rs  |  2 +-
 .../expected/function-contract/simple_ensures_pass.rs  |  2 +-
 .../expected/function-contract/simple_replace_fail.rs  |  2 +-
 .../expected/function-contract/simple_replace_pass.rs  |  2 +-
 .../function-contract/type_annotation_needed.rs        |  2 +-
 45 files changed, 56 insertions(+), 51 deletions(-)

diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
index 141b04c7afa3..7c35cc469254 100644
--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -8,7 +8,10 @@ use proc_macro2::{Ident, Span};
 use quote::quote;
 use syn::ItemFn;
 
-use super::{helpers::*, shared::identifier_for_generated_function, ContractConditionsHandler, INTERNAL_RESULT_IDENT};
+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
diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs
index f4d9f57901fd..4f72730ba458 100644
--- a/library/kani_macros/src/sysroot/contracts/initialize.rs
+++ b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -7,8 +7,10 @@ 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, ExprClosure, ItemFn, Signature};
 use quote::quote;
+use syn::{
+    spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ExprClosure, ItemFn, Signature,
+};
 
 use super::{
     helpers::{chunks_by, is_token_stream_2_comma, matches_path},
@@ -82,9 +84,9 @@ impl<'a> ContractConditionsHandler<'a> {
                 ContractConditionsData::Requires { attr: syn::parse(attr)? }
             }
             ContractConditionsType::Ensures => {
-                let data : ExprClosure = syn::parse(attr)?;
-                let result : Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-                let attr : Expr = Expr::Verbatim(quote!((#data)(#result)));
+                let data: ExprClosure = syn::parse(attr)?;
+                let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+                let attr: Expr = Expr::Verbatim(quote!((#data)(#result)));
                 ContractConditionsData::new_ensures(&annotated_fn.sig, attr)
             }
             ContractConditionsType::Modifies => {
diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index 001d6225dc7b..fd6a772dda02 100644
--- a/library/kani_macros/src/sysroot/contracts/mod.rs
+++ b/library/kani_macros/src/sysroot/contracts/mod.rs
@@ -243,7 +243,7 @@ mod initialize;
 mod replace;
 mod shared;
 
-const INTERNAL_RESULT_IDENT : &str = "result_kani_internal";
+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/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs
index 91638b1cc037..d85a6d39c415 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| 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.rs b/tests/expected/function-contract/arbitrary_ensures_pass.rs
index df8d3a2361fb..13972a13105a 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| 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..466914544eb3 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| 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.rs b/tests/expected/function-contract/checking_from_external_mod.rs
index 43d1551f9aef..0f2a752a5c81 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| (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.rs b/tests/expected/function-contract/checking_in_impl.rs
index 7d5c0506d9df..a157d393b4cb 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| (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.rs b/tests/expected/function-contract/fail_on_two.rs
index 605065449194..c8870a2b2fe6 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| 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| 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.rs b/tests/expected/function-contract/gcd_failure_code.rs
index f76e04b75fee..33aa739902f9 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| 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.rs b/tests/expected/function-contract/gcd_failure_contract.rs
index 6b835466c5a0..6ebc65423f4b 100644
--- a/tests/expected/function-contract/gcd_failure_contract.rs
+++ b/tests/expected/function-contract/gcd_failure_contract.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| 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.rs b/tests/expected/function-contract/gcd_rec_code_fail.rs
index da38318e2a66..c859236f91da 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| 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.rs b/tests/expected/function-contract/gcd_rec_comparison_pass.rs
index 1db9691ae8e4..e228abcd2eea 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| 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.rs b/tests/expected/function-contract/gcd_rec_contract_fail.rs
index 3fe34cb2effc..08140b9fc861 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| 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..73a34bfd1142 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| 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.rs b/tests/expected/function-contract/gcd_rec_simple_pass.rs
index 464e3d8bbea1..de474203d12e 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| 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..46831f8f026d 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| 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..2fe4d2205f46 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| 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.rs b/tests/expected/function-contract/gcd_success.rs
index d3a2c75b7d20..1517e1098531 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| 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..820e29e4ac72 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| 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..6eca25458a1c 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| 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.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..a3ab34c031ec 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| 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..9b075ea779d6 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| unsafe{ *result == *input })]
 fn return_pointer(input: *const usize) -> *const usize {
     input
 }
diff --git a/tests/expected/function-contract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs
index 687853612dcc..5ea7e21a0cfb 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| 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.rs b/tests/expected/function-contract/simple_ensures_pass.rs
index 2d36f5c96e88..5c7d9450f013 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| (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..d994efea2350 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| 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..baf688c31755 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| 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..a52a998f423f 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| result.is_some())]
 fn or_default<T: Default>(opt: Option<T>) -> Option<T> {
     opt.or(Some(T::default()))
 }

From aa4278710c72d90c8d0f545ef96cec14f754672a Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Thu, 30 May 2024 18:37:55 -0400
Subject: [PATCH 05/12] more tests pass

---
 .../function-contract/arbitrary_ensures_fail.expected         | 2 +-
 .../function-contract/arbitrary_ensures_pass.expected         | 2 +-
 .../function-contract/checking_from_external_mod.expected     | 2 +-
 tests/expected/function-contract/checking_in_impl.expected    | 2 +-
 tests/expected/function-contract/fail_on_two.expected         | 4 ++--
 tests/expected/function-contract/gcd_failure_code.expected    | 4 ++--
 .../expected/function-contract/gcd_failure_contract.expected  | 4 ++--
 tests/expected/function-contract/gcd_rec_code_fail.expected   | 2 +-
 .../function-contract/gcd_rec_comparison_pass.expected        | 4 ++--
 .../expected/function-contract/gcd_rec_contract_fail.expected | 2 +-
 tests/expected/function-contract/gcd_rec_simple_pass.expected | 4 ++--
 tests/expected/function-contract/gcd_success.expected         | 2 +-
 .../modifies/mistake_condition_return.expected                | 2 +-
 tests/expected/function-contract/simple_ensures_fail.expected | 4 ++--
 tests/expected/function-contract/simple_ensures_pass.expected | 2 +-
 tests/expected/function-contract/type_annotation_needed.rs    | 2 +-
 16 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected
index 0a59d2cea5eb..f64564e93e6c 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| result == x"\
 in function max 
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected
index 85619fa84c22..a052491634be 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| result == x || result == y"\
 in function max
      
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected
index c31b5c389fc8..19ed8ad69217 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| (result == x) | (result == y)"\
 in function max
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/checking_in_impl.expected b/tests/expected/function-contract/checking_in_impl.expected
index d5a390be8425..dbaf6e00e4fb 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| (result == self) | (result == y)"\
 in function WrappedInt::max
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/fail_on_two.expected b/tests/expected/function-contract/fail_on_two.expected
index 32fc28012d3a..02955e7b2c12 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| result < 3"
 
-Failed Checks: result < 3
+Failed Checks: |result| result < 3
diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected
index c7fe5a721abb..5fc363b8155d 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| result != 0 && x % result == 0 && y % result == 0"\
 in function gcd
 
-Failed Checks: result != 0 && x % result == 0 && y % result == 0
+Failed Checks: |result| result != 0 && x % result == 0 && y % result == 0
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/gcd_failure_contract.expected b/tests/expected/function-contract/gcd_failure_contract.expected
index aeadfb563ab9..9b8f12315907 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| result != 0 && x % result == 1 && y % result == 0"\
 in function gcd\
 	 
-Failed Checks: result != 0 && x % result == 1 && y % result == 0
+Failed Checks: |result| result != 0 && x % result == 1 && y % result == 0
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/gcd_rec_code_fail.expected b/tests/expected/function-contract/gcd_rec_code_fail.expected
index 80dbaadbf4c7..a83e6e3cd014 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| result != 0 && x % result == 0 && y % result == 0
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.expected b/tests/expected/function-contract/gcd_rec_comparison_pass.expected
index da647dfd40aa..eeae918e0e14 100644
--- a/tests/expected/function-contract/gcd_rec_comparison_pass.expected
+++ b/tests/expected/function-contract/gcd_rec_comparison_pass.expected
@@ -1,9 +1,9 @@
 assertion\
 - Status: SUCCESS\
-- Description: "x != 0 && y != 0"
+- Description: "|result| x != 0 && y != 0"
 
 assertion\
 - Status: SUCCESS\
-- Description: "result != 0 && x % result == 0 && y % result == 0"
+- Description: "|result| result != 0 && x % result == 0 && y % result == 0"
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.expected b/tests/expected/function-contract/gcd_rec_contract_fail.expected
index bfb470192a39..5c305fe85e89 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| result != 0 && x % result == 1 && y % result == 0
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.expected b/tests/expected/function-contract/gcd_rec_simple_pass.expected
index da647dfd40aa..eeae918e0e14 100644
--- a/tests/expected/function-contract/gcd_rec_simple_pass.expected
+++ b/tests/expected/function-contract/gcd_rec_simple_pass.expected
@@ -1,9 +1,9 @@
 assertion\
 - Status: SUCCESS\
-- Description: "x != 0 && y != 0"
+- Description: "|result| x != 0 && y != 0"
 
 assertion\
 - Status: SUCCESS\
-- Description: "result != 0 && x % result == 0 && y % result == 0"
+- Description: "|result| result != 0 && x % result == 0 && y % result == 0"
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/gcd_success.expected b/tests/expected/function-contract/gcd_success.expected
index 73b531d424b9..1dd1ecd35858 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| result != 0 && x % result == 0 && y % result == 0"\
 in function gcd
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/modifies/mistake_condition_return.expected b/tests/expected/function-contract/modifies/mistake_condition_return.expected
index ad1cbf4f72d2..f5843de7cc63 100644
--- a/tests/expected/function-contract/modifies/mistake_condition_return.expected
+++ b/tests/expected/function-contract/modifies/mistake_condition_return.expected
@@ -1,3 +1,3 @@
-Failed Checks: assertion failed: res == 100
+Failed Checks: assertion failed: |result| res == 100
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected
index 8e9b42d42640..26f40fd49fd6 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| result == x"\
 in function max
 
-Failed Checks: result == x
+Failed Checks: |result| result == x
 
 VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected
index 5a7874964413..8f35e680b75f 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| (result == x) | (result == y)"\
 in function max
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/type_annotation_needed.rs b/tests/expected/function-contract/type_annotation_needed.rs
index a52a998f423f..6e19a1127196 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| 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()))
 }

From d00b2290a9ef1f1819f6e495bf0e6a06af084bff Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Fri, 31 May 2024 11:05:16 -0400
Subject: [PATCH 06/12] change rewriter

---
 .../src/sysroot/contracts/initialize.rs       | 28 +++++++------------
 1 file changed, 10 insertions(+), 18 deletions(-)

diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs
index 4f72730ba458..063604e4e84b 100644
--- a/library/kani_macros/src/sysroot/contracts/initialize.rs
+++ b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -8,9 +8,7 @@ use std::collections::{HashMap, HashSet};
 use proc_macro::{Diagnostic, TokenStream};
 use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
 use quote::quote;
-use syn::{
-    spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ExprClosure, ItemFn, Signature,
-};
+use syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ExprClosure, ItemFn};
 
 use super::{
     helpers::{chunks_by, is_token_stream_2_comma, matches_path},
@@ -84,10 +82,11 @@ impl<'a> ContractConditionsHandler<'a> {
                 ContractConditionsData::Requires { attr: syn::parse(attr)? }
             }
             ContractConditionsType::Ensures => {
-                let data: ExprClosure = 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 attr: Expr = Expr::Verbatim(quote!((#data)(#result)));
-                ContractConditionsData::new_ensures(&annotated_fn.sig, attr)
+                let app: Expr = Expr::Verbatim(quote!((#data)(#result)));
+                ContractConditionsData::Ensures { argument_names, attr: app }
             }
             ContractConditionsType::Modifies => {
                 ContractConditionsData::new_modifies(attr, &mut output)
@@ -98,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.
@@ -135,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);
 
@@ -150,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
 }
 

From e063b850defd9822cbd2ce3148330cf6655e5d2b Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Fri, 31 May 2024 11:42:03 -0400
Subject: [PATCH 07/12] more tests pass

---
 .../expected/function-contract/gcd_rec_comparison_pass.expected | 2 +-
 tests/expected/function-contract/gcd_rec_simple_pass.expected   | 2 +-
 .../modifies/mistake_condition_return.expected                  | 2 +-
 tests/expected/function-contract/modifies/vec_pass.expected     | 2 +-
 .../function-contract/prohibit-pointers/return_pointer.rs       | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.expected b/tests/expected/function-contract/gcd_rec_comparison_pass.expected
index eeae918e0e14..ba314f45b4aa 100644
--- a/tests/expected/function-contract/gcd_rec_comparison_pass.expected
+++ b/tests/expected/function-contract/gcd_rec_comparison_pass.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|result| x != 0 && y != 0"
+- Description: "x != 0 && y != 0"
 
 assertion\
 - Status: SUCCESS\
diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.expected b/tests/expected/function-contract/gcd_rec_simple_pass.expected
index eeae918e0e14..ba314f45b4aa 100644
--- a/tests/expected/function-contract/gcd_rec_simple_pass.expected
+++ b/tests/expected/function-contract/gcd_rec_simple_pass.expected
@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|result| x != 0 && y != 0"
+- Description: "x != 0 && y != 0"
 
 assertion\
 - Status: SUCCESS\
diff --git a/tests/expected/function-contract/modifies/mistake_condition_return.expected b/tests/expected/function-contract/modifies/mistake_condition_return.expected
index f5843de7cc63..ad1cbf4f72d2 100644
--- a/tests/expected/function-contract/modifies/mistake_condition_return.expected
+++ b/tests/expected/function-contract/modifies/mistake_condition_return.expected
@@ -1,3 +1,3 @@
-Failed Checks: assertion failed: |result| res == 100
+Failed Checks: assertion failed: res == 100
 
 VERIFICATION:- FAILED
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/prohibit-pointers/return_pointer.rs b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs
index 9b075ea779d6..4efe044cdc28 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(|result| unsafe{ *result == *input })]
+#[kani::ensures(|result : *const usize| unsafe{ *result == *input })]
 fn return_pointer(input: *const usize) -> *const usize {
     input
 }

From 8e2e6104637a4c8105d01590987cf1e20c9caea0 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Fri, 31 May 2024 12:24:49 -0400
Subject: [PATCH 08/12] change to pass by reference

---
 library/kani_macros/src/sysroot/contracts/initialize.rs       | 2 +-
 .../function-contract/arbitrary_ensures_fail.expected         | 2 +-
 tests/expected/function-contract/arbitrary_ensures_fail.rs    | 2 +-
 .../function-contract/arbitrary_ensures_pass.expected         | 2 +-
 tests/expected/function-contract/arbitrary_ensures_pass.rs    | 2 +-
 tests/expected/function-contract/arbitrary_requires_fail.rs   | 2 +-
 .../function-contract/checking_from_external_mod.expected     | 2 +-
 .../expected/function-contract/checking_from_external_mod.rs  | 2 +-
 tests/expected/function-contract/checking_in_impl.expected    | 2 +-
 tests/expected/function-contract/checking_in_impl.rs          | 2 +-
 tests/expected/function-contract/fail_on_two.expected         | 4 ++--
 tests/expected/function-contract/fail_on_two.rs               | 4 ++--
 tests/expected/function-contract/gcd_failure_code.expected    | 4 ++--
 tests/expected/function-contract/gcd_failure_code.rs          | 2 +-
 .../expected/function-contract/gcd_failure_contract.expected  | 4 ++--
 tests/expected/function-contract/gcd_failure_contract.rs      | 4 ++--
 tests/expected/function-contract/gcd_rec_code_fail.expected   | 2 +-
 tests/expected/function-contract/gcd_rec_code_fail.rs         | 2 +-
 .../function-contract/gcd_rec_comparison_pass.expected        | 2 +-
 tests/expected/function-contract/gcd_rec_comparison_pass.rs   | 2 +-
 .../expected/function-contract/gcd_rec_contract_fail.expected | 2 +-
 tests/expected/function-contract/gcd_rec_contract_fail.rs     | 2 +-
 tests/expected/function-contract/gcd_rec_replacement_pass.rs  | 2 +-
 tests/expected/function-contract/gcd_rec_simple_pass.expected | 2 +-
 tests/expected/function-contract/gcd_rec_simple_pass.rs       | 2 +-
 tests/expected/function-contract/gcd_replacement_fail.rs      | 2 +-
 tests/expected/function-contract/gcd_replacement_pass.rs      | 2 +-
 tests/expected/function-contract/gcd_success.expected         | 2 +-
 tests/expected/function-contract/gcd_success.rs               | 2 +-
 .../function-contract/modifies/check_only_verification.rs     | 2 +-
 .../function-contract/modifies/fail_missing_recursion_attr.rs | 2 +-
 tests/expected/function-contract/pattern_use.rs               | 2 +-
 .../function-contract/prohibit-pointers/return_pointer.rs     | 2 +-
 tests/expected/function-contract/simple_ensures_fail.expected | 4 ++--
 tests/expected/function-contract/simple_ensures_fail.rs       | 2 +-
 tests/expected/function-contract/simple_ensures_pass.expected | 2 +-
 tests/expected/function-contract/simple_ensures_pass.rs       | 2 +-
 tests/expected/function-contract/simple_replace_fail.rs       | 2 +-
 tests/expected/function-contract/simple_replace_pass.rs       | 2 +-
 tests/expected/function-contract/type_annotation_needed.rs    | 2 +-
 40 files changed, 46 insertions(+), 46 deletions(-)

diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs
index 063604e4e84b..aee0c21bc82d 100644
--- a/library/kani_macros/src/sysroot/contracts/initialize.rs
+++ b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -85,7 +85,7 @@ impl<'a> ContractConditionsHandler<'a> {
                 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)));
+                let app: Expr = Expr::Verbatim(quote!((#data)(&#result)));
                 ContractConditionsData::Ensures { argument_names, attr: app }
             }
             ContractConditionsType::Modifies => {
diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected
index f64564e93e6c..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| 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 d85a6d39c415..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| 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 a052491634be..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| 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 13972a13105a..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| 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 466914544eb3..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| result <= dividend)]
+#[kani::ensures(|result : &u32| *result <= dividend)]
 fn div(dividend: u32, divisor: u32) -> u32 {
     dividend / divisor
 }
diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected
index 19ed8ad69217..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| (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 0f2a752a5c81..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| (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 dbaf6e00e4fb..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| (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 a157d393b4cb..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| (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 02955e7b2c12..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| result < 3"
+- Description: "|result : &i32| *result < 3"
 
-Failed Checks: |result| 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 c8870a2b2fe6..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| 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| 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 5fc363b8155d..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| 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| 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 33aa739902f9..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| 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 9b8f12315907..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| 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| 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 6ebc65423f4b..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| 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 a83e6e3cd014..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| 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 c859236f91da..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| 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 ba314f45b4aa..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| 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 e228abcd2eea..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| 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 5c305fe85e89..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| 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 08140b9fc861..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| 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 73a34bfd1142..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| 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 ba314f45b4aa..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| 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 de474203d12e..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| 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 46831f8f026d..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| 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 2fe4d2205f46..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| 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 1dd1ecd35858..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| 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 1517e1098531..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| 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 820e29e4ac72..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| 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/fail_missing_recursion_attr.rs b/tests/expected/function-contract/modifies/fail_missing_recursion_attr.rs
index 6eca25458a1c..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| 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/pattern_use.rs b/tests/expected/function-contract/pattern_use.rs
index a3ab34c031ec..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| 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/return_pointer.rs b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs
index 4efe044cdc28..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(|result : *const usize| 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 26f40fd49fd6..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| result == x"\
+- Description: "|result : &u32| *result == x"\
 in function max
 
-Failed Checks: |result| 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 5ea7e21a0cfb..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| 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 8f35e680b75f..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| (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 5c7d9450f013..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| (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 d994efea2350..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| 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 baf688c31755..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| 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 6e19a1127196..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 : Option<T>| 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()))
 }

From 895cd3525d2eacd8179b22625704710336afa3fc Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Fri, 31 May 2024 13:15:02 -0400
Subject: [PATCH 09/12] fix more tests

---
 tests/std-checks/core/src/ptr.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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 ddb6f9c0ac373b7244bdc70b139e76a661740ffa Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Mon, 3 Jun 2024 10:07:13 -0400
Subject: [PATCH 10/12] comments

---
 library/kani/src/contracts.rs                 | 10 ++--
 library/kani_macros/src/lib.rs                | 10 ++--
 .../kani_macros/src/sysroot/contracts/mod.rs  | 56 ++++++++++---------
 3 files changed, 40 insertions(+), 36 deletions(-)

diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs
index 4f963038cab9..c50da7325351 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/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index fd6a772dda02..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
 //!     }
 //! }
 //! ```

From 4518865f031de26de78d48473fa2c78e30c33caf Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Mon, 3 Jun 2024 10:24:30 -0400
Subject: [PATCH 11/12] format

---
 library/kani/src/contracts.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs
index c50da7325351..65b9ec7c01cc 100644
--- a/library/kani/src/contracts.rs
+++ b/library/kani/src/contracts.rs
@@ -57,7 +57,7 @@
 //! 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 postcondition is expressed
-//! as a closure where the value returned from the function is passed to this 
+//! 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

From 5f5fb8a149acd702cdde2498d80f7f9843f82031 Mon Sep 17 00:00:00 2001
From: Matias Scharager <mscharag@amazon.com>
Date: Wed, 5 Jun 2024 13:37:26 -0400
Subject: [PATCH 12/12] updated rfc

---
 rfc/src/rfcs/0009-function-contracts.md | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

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]) {
     ...
   }