Contracts: History Expressions via "old" monad

library/kani/src/contracts.rs

@@ -225,4 +225,27 @@
 //! Rust pointer type (`&T`, `&mut T`, `*const T` or `*mut T`). In addition `T`
 //! must implement [`Arbitrary`](super::Arbitrary). This is used to assign
 //! `kani::any()` to the location when the function is used in a `stub_verified`.
+//!
+//! ## History Variables
+//!
+//! Additionally, an ensures clause is allowed to refer to history computations
+//! via an `old` monad. Any instance of `old(computation)` will evaluate the
+//! computation before the function is called. It is required that this computation
+//! is effect free and closed with respect to the function arguments.
+//!
+//! For example, the following code passes kani tests:
+//!
+//! ```
+//! #[kani::modifies(a)]
+//! #[kani::ensures(|result| old(*a).wrapping_add(1) == *a)]
+//! #[kani::ensures(|result : &u32| old(*a).wrapping_add(1) == *result)]
+//! fn add1(a : &mut u32) -> u32 {
+//!     *a=a.wrapping_add(1);
+//!     *a
+//! }
+//! ```
+//!
+//! Here, the value stored in `a` is precomputed and remembered after the function
+//! is called, even though the contents of `a` changed during the function execution.
+//!
 pub use super::{ensures, modifies, proof_for_contract, requires, stub_verified};

library/kani_macros/src/sysroot/contracts/check.rs

@@ -9,7 +9,9 @@ use syn::{Expr, FnArg, ItemFn, Token};
 
 use super::{
     helpers::*,
-    shared::{make_unsafe_argument_copies, try_as_result_assign_mut},
+    shared::{
+        build_ensures, count_remembers, make_unsafe_argument_copies, try_as_result_assign_mut,
+    },
     ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
@@ -25,6 +27,7 @@ impl<'a> ContractConditionsHandler<'a> {
     pub fn make_check_body(&mut self) -> TokenStream2 {
         let mut inner = self.ensure_bootstrapped_check_body();
         let Self { attr_copy, .. } = self;
+        let remember_count: usize = count_remembers(&inner);
 
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
@@ -35,11 +38,12 @@ impl<'a> ContractConditionsHandler<'a> {
             }
             ContractConditionsData::Ensures { argument_names, attr } => {
                 let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names);
+                let (remembers_stmts, ensures_clause) = build_ensures(attr, remember_count);
 
                 // The code that enforces the postconditions and cleans up the shallow
                 // argument copies (with `mem::forget`).
                 let exec_postconditions = quote!(
-                    kani::assert(#attr, stringify!(#attr_copy));
+                    kani::assert(#ensures_clause, stringify!(#attr_copy));
                     #copy_clean
                 );
 
@@ -52,6 +56,7 @@ impl<'a> ContractConditionsHandler<'a> {
                 let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
                 quote!(
                     #arg_copies
+                    #remembers_stmts
                     #(#inner)*
                     #exec_postconditions
                     #result

library/kani_macros/src/sysroot/contracts/helpers.rs

@@ -268,3 +268,21 @@ pub fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 {
     let long_hash = hasher.finish();
     long_hash % SIX_HEX_DIGITS_MASK
 }
+
+macro_rules! assert_spanned_err {
+    ($condition:expr, $span_source:expr, $msg:expr, $($args:expr),+) => {
+        if !$condition {
+            $span_source.span().unwrap().error(format!($msg, $($args),*)).emit();
+            assert!(false);
+        }
+    };
+    ($condition:expr, $span_source:expr, $msg:expr $(,)?) => {
+        if !$condition {
+            $span_source.span().unwrap().error($msg).emit();
+            assert!(false);
+        }
+    };
+    ($condition:expr, $span_source:expr) => {
+        assert_spanned_err!($condition, $span_source, concat!("Failed assertion ", stringify!($condition)))
+    };
+}

library/kani_macros/src/sysroot/contracts/initialize.rs

@@ -7,13 +7,12 @@ 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};
+use syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, ExprClosure, ItemFn};
 
 use super::{
     helpers::{chunks_by, is_token_stream_2_comma, matches_path},
     ContractConditionsData, ContractConditionsHandler, ContractConditionsType,
-    ContractFunctionState, INTERNAL_RESULT_IDENT,
+    ContractFunctionState,
 };
 
 impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState {
@@ -84,9 +83,7 @@ impl<'a> ContractConditionsHandler<'a> {
             ContractConditionsType::Ensures => {
                 let mut data: ExprClosure = syn::parse(attr)?;
                 let argument_names = rename_argument_occurrences(&annotated_fn.sig, &mut data);
-                let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-                let app: Expr = Expr::Verbatim(quote!((#data)(&#result)));
-                ContractConditionsData::Ensures { argument_names, attr: app }
+                ContractConditionsData::Ensures { argument_names, attr: data }
             }
             ContractConditionsType::Modifies => {
                 ContractConditionsData::new_modifies(attr, &mut output)

library/kani_macros/src/sysroot/contracts/mod.rs

@@ -233,15 +233,81 @@
 //!     }
 //! }
 //! ```
+//!
+//! Additionally, there is functionality that allows the referencing of
+//! history values within the ensures statement. This means we can
+//! precompute a value before the function is called and have access to
+//! this value in the later ensures statement. This is done via the
+//! `old` monad which lets you access the old state within the present
+//! state. Each occurance of old is lifted, so is is necessary that
+//! each lifted occurance is closed with respect to the function arguments.
+//! The results of these old computations are placed into
+//! `remember_kani_internal_XXX` variables of incrementing index to avoid
+//! collisions of variable names. Consider the following example:
+//!
+//! ```
+//! #[kani::modifies(a)]
+//! #[kani::ensures(|result| old(*a).wrapping_add(1) == *a)]
+//! #[kani::ensures(|result : &u32| old(*a).wrapping_add(1) == *result)]
+//! fn add1(a : &mut u32) -> u32 {
+//!     *a=a.wrapping_add(1);
+//!     *a
+//! }
+//!
+//! #[kani::proof_for_contract(add1)]
+//! fn verify_success() {
+//!     let a : &mut u32 = &mut kani::any();
+//!     add1(a);
+//! }
+//! ```
+//!
+//! This expands to
+//!
+//! ```
+//! #[allow(dead_code, unused_variables)]
+//! #[kanitool :: is_contract_generated(check)]
+//! fn add1_check_86e6df(a : & mut u32) -> u32 {
+//!     let a_renamed = kani::internal::untracked_deref(& a);
+//!     let remember_kani_internal_1 = *a_renamed;
+//!     let a_renamed = kani::internal::untracked_deref(& a);
+//!     let remember_kani_internal_0 = * a_renamed;
+//!     let _wrapper_arg_1 = unsafe { kani :: internal :: Pointer :: decouple_lifetime(& a) };
+//!     let result_kani_internal : u32 = add1_wrapper_86e6df(a, _wrapper_arg_1);
+//!     kani::assert((| result | (remember_kani_internal_0).wrapping_add(1) == *a_renamed) (& result_kani_internal),
+//!         stringify! (|result| old(*a).wrapping_add(1) == *a));
+//!     std::mem::forget(a_renamed);
+//!     kani::assert((| result : & u32 | (remember_kani_internal_1).wrapping_add(1) == *result) (& result_kani_internal),
+//!         stringify!(|result : &u32| old(*a).wrapping_add(1) == *result));
+//!     std::mem::forget(a_renamed);
+//!     result_kani_internal
+//! }
+//!
+//! #[allow(dead_code, unused_variables)]
+//! #[kanitool :: is_contract_generated(replace)]
+//! fn add1_replace_86e6df(a : & mut u32) -> u32 {
+//!     let a_renamed = kani::internal::untracked_deref(& a);
+//!     let remember_kani_internal_1 = *a_renamed;
+//!     let a_renamed = kani::internal::untracked_deref(& a);
+//!     let remember_kani_internal_0 = *a_renamed;
+//!     let result_kani_internal : u32 = kani::any_modifies();
+//!     *unsafe{ kani :: internal :: Pointer :: assignable(a) } = kani::any_modifies();
+//!     kani ::assume((| result | (remember_kani_internal_0).wrapping_add(1) == *a_renamed) (& result_kani_internal));
+//!     std :: mem :: forget(a_renamed);
+//!     kani ::assume((| result : & u32 | (remember_kani_internal_1).wrapping_add(1) == *result) (& result_kani_internal));
+//!     std :: mem :: forget(a_renamed);
+//!     result_kani_internal
+//! }
+//! ```
 
 use proc_macro::TokenStream;
 use proc_macro2::{Ident, TokenStream as TokenStream2};
 use quote::{quote, ToTokens};
 use std::collections::HashMap;
-use syn::{parse_macro_input, Expr, ItemFn};
+use syn::{parse_macro_input, Expr, ExprClosure, ItemFn};
 
 mod bootstrap;
 mod check;
+#[macro_use]
 mod helpers;
 mod initialize;
 mod replace;
@@ -356,7 +422,7 @@ enum ContractConditionsData {
         /// we will be emitting.
         argument_names: HashMap<Ident, Ident>,
         /// The contents of the attribute.
-        attr: Expr,
+        attr: ExprClosure,
     },
     Modifies {
         attr: Vec<Expr>,

library/kani_macros/src/sysroot/contracts/replace.rs

@@ -8,7 +8,7 @@ use quote::quote;
 
 use super::{
     helpers::*,
-    shared::{make_unsafe_argument_copies, try_as_result_assign},
+    shared::{build_ensures, count_remembers, make_unsafe_argument_copies, try_as_result_assign},
     ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
@@ -67,6 +67,7 @@ impl<'a> ContractConditionsHandler<'a> {
     /// generating a replace function.
     fn make_replace_body(&self) -> TokenStream2 {
         let (before, after) = self.ensure_bootstrapped_replace_body();
+        let remember_count = count_remembers(&before);
 
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
@@ -82,11 +83,13 @@ impl<'a> ContractConditionsHandler<'a> {
             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());
+                let (remembers_stmts, ensures_clause) = build_ensures(attr, remember_count);
                 quote!(
                     #arg_copies
+                    #remembers_stmts
                     #(#before)*
                     #(#after)*
-                    kani::assume(#attr);
+                    kani::assume(#ensures_clause);
                     #copy_clean
                     #result
                 )