diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 65b9ec7c01cc..beddd7cc580e 100644 --- a/library/kani/src/contracts.rs +++ b/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 Expressions +//! +//! Additionally, an ensures clause is allowed to refer to the state of the function arguments before function execution and perform simple computations on them +//! 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}; diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index dbe2126d0458..e0c79a39c105 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -15,7 +15,7 @@ proc-macro = true proc-macro2 = "1.0" proc-macro-error = "1.0.4" quote = "1.0.20" -syn = { version = "2.0.18", features = ["full", "visit-mut", "visit"] } +syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-traits"] } [package.metadata.rust-analyzer] # This package uses rustc crates. diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index bd4c09b07796..e76286b398cb 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -9,7 +9,7 @@ use syn::{Expr, FnArg, ItemFn, Token}; use super::{ helpers::*, - shared::{make_unsafe_argument_copies, try_as_result_assign_mut}, + shared::{build_ensures, try_as_result_assign_mut}, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, }; @@ -33,14 +33,13 @@ impl<'a> ContractConditionsHandler<'a> { #(#inner)* ) } - ContractConditionsData::Ensures { argument_names, attr } => { - let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); + ContractConditionsData::Ensures { attr } => { + let (remembers, ensures_clause) = build_ensures(attr); // 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)); - #copy_clean + kani::assert(#ensures_clause, stringify!(#attr_copy)); ); assert!(matches!( @@ -51,7 +50,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( - #arg_copies + #remembers #(#inner)* #exec_postconditions #result diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index baa25b8104e8..174f0f9483d7 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/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))) + }; +} diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index aee0c21bc82d..73621b2aeec5 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -3,17 +3,14 @@ //! Initialization routine for the contract handler -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 proc_macro2::{Ident, TokenStream as TokenStream2}; +use syn::{spanned::Spanned, 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 { @@ -82,11 +79,7 @@ impl<'a> ContractConditionsHandler<'a> { ContractConditionsData::Requires { attr: syn::parse(attr)? } } 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 { attr: syn::parse(attr)? } } ContractConditionsType::Modifies => { ContractConditionsData::new_modifies(attr, &mut output) @@ -115,76 +108,3 @@ impl ContractConditionsData { ContractConditionsData::Modifies { attr } } } - -/// A supporting function for creating shallow, unsafe copies of the arguments -/// for the postconditions. -/// -/// This function: -/// - Collects all [`Ident`]s found in the argument patterns; -/// - 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 ExprClosure, -) -> HashMap { - let mut arg_ident_collector = ArgumentIdentCollector::new(); - arg_ident_collector.visit_signature(&sig); - - let mk_new_ident_for = |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); - let arg_idents = arg_ident_collector - .0 - .into_iter() - .map(|i| { - let new = mk_new_ident_for(&i); - (i, new) - }) - .collect::>(); - - let mut ident_rewriter = Renamer(&arg_idents); - ident_rewriter.visit_expr_closure_mut(attr); - arg_idents -} - -/// Collect all named identifiers used in the argument patterns of a function. -struct ArgumentIdentCollector(HashSet); - -impl ArgumentIdentCollector { - fn new() -> Self { - Self(HashSet::new()) - } -} - -impl<'ast> Visit<'ast> for ArgumentIdentCollector { - fn visit_pat_ident(&mut self, i: &'ast syn::PatIdent) { - self.0.insert(i.ident.clone()); - syn::visit::visit_pat_ident(self, i) - } - fn visit_receiver(&mut self, _: &'ast syn::Receiver) { - self.0.insert(Ident::new("self", proc_macro2::Span::call_site())); - } -} - -/// Applies the contained renaming (key renamed to value) to every ident pattern -/// and ident expr visited. -struct Renamer<'a>(&'a HashMap); - -impl<'a> VisitMut for Renamer<'a> { - fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) { - if i.path.segments.len() == 1 { - i.path - .segments - .first_mut() - .and_then(|p| self.0.get(&p.ident).map(|new| p.ident = new.clone())); - } - } - - /// 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 let Some(new) = self.0.get(&i.ident) { - i.ident = new.clone(); - } - } -} diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 7a25cc390100..defcd9dae1b4 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -233,15 +233,114 @@ //! } //! } //! ``` +//! +//! 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 occurrence of `old` is lifted, so is is necessary that +//! each lifted occurrence is closed with respect to the function arguments. +//! The results of these old computations are placed into +//! `remember_kani_internal_XXX` variables which are hashed. Consider the following example: +//! +//! ``` +//! #[kani::ensures(|result| old(*ptr + 1) == *ptr)] +//! #[kani::ensures(|result| old(*ptr + 1) == *ptr)] +//! #[kani::requires(*ptr < 100)] +//! #[kani::modifies(ptr)] +//! fn modify(ptr: &mut u32) { +//! *ptr += 1; +//! } +//! +//! #[kani::proof_for_contract(modify)] +//! fn main() { +//! let mut i = kani::any(); +//! modify(&mut i); +//! } +//! +//! ``` +//! +//! This expands to +//! +//! ``` +//! #[kanitool::checked_with = "modify_recursion_wrapper_633496"] +//! #[kanitool::replaced_with = "modify_replace_633496"] +//! #[kanitool::inner_check = "modify_wrapper_633496"] +//! fn modify(ptr: &mut u32) { { *ptr += 1; } } +//! #[allow(dead_code, unused_variables, unused_mut)] +//! #[kanitool::is_contract_generated(recursion_wrapper)] +//! fn modify_recursion_wrapper_633496(arg0: &mut u32) { +//! static mut REENTRY: bool = false; +//! if unsafe { REENTRY } { +//! modify_replace_633496(arg0) +//! } else { +//! unsafe { REENTRY = true }; +//! let result_kani_internal = modify_check_633496(arg0); +//! unsafe { REENTRY = false }; +//! result_kani_internal +//! } +//! } +//! #[allow(dead_code, unused_variables, unused_mut)] +//! #[kanitool::is_contract_generated(check)] +//! fn modify_check_633496(ptr: &mut u32) { +//! let _wrapper_arg_1 = +//! unsafe { kani::internal::Pointer::decouple_lifetime(&ptr) }; +//! kani::assume(*ptr < 100); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let result_kani_internal: () = modify_wrapper_633496(ptr, _wrapper_arg_1); +//! kani::assert((|result| +//! (remember_kani_internal_92cc419d8aca576c) == +//! *ptr)(&result_kani_internal), +//! "|result| old(*ptr + 1) == *ptr"); +//! kani::assert((|result| +//! (remember_kani_internal_92cc419d8aca576c) == +//! *ptr)(&result_kani_internal), +//! "|result| old(*ptr + 1) == *ptr"); +//! result_kani_internal +//! } +//! #[allow(dead_code, unused_variables, unused_mut)] +//! #[kanitool::is_contract_generated(replace)] +//! fn modify_replace_633496(ptr: &mut u32) { +//! kani::assert(*ptr < 100, "*ptr < 100"); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let result_kani_internal: () = kani::any_modifies(); +//! *unsafe { +//! kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr))) +//! } = kani::any_modifies(); +//! kani::assume((|result| +//! (remember_kani_internal_92cc419d8aca576c) == +//! *ptr)(&result_kani_internal)); +//! kani::assume((|result| +//! (remember_kani_internal_92cc419d8aca576c) == +//! *ptr)(&result_kani_internal)); +//! result_kani_internal +//! } +//! #[kanitool::modifies(_wrapper_arg_1)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! #[kanitool::is_contract_generated(wrapper)] +//! fn modify_wrapper_633496<'_wrapper_arg_1, +//! WrapperArgType1>(ptr: &mut u32, _wrapper_arg_1: &WrapperArgType1) { +//! *ptr += 1; +//! } +//! #[allow(dead_code)] +//! #[kanitool::proof_for_contract = "modify"] +//! fn main() { +//! kani::internal::init_contracts(); +//! { let mut i = kani::any(); modify(&mut i); } +//! } +//! ``` 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; @@ -352,11 +451,8 @@ enum ContractConditionsData { attr: Expr, }, Ensures { - /// Translation map from original argument names to names of the copies - /// we will be emitting. - argument_names: HashMap, /// The contents of the attribute. - attr: Expr, + attr: ExprClosure, }, Modifies { attr: Vec, diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 1a84e40523c2..7a522ea98e08 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/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, try_as_result_assign}, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, }; @@ -79,15 +79,14 @@ impl<'a> ContractConditionsHandler<'a> { #result ) } - ContractConditionsData::Ensures { attr, argument_names } => { - let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); + ContractConditionsData::Ensures { attr } => { + let (remembers, ensures_clause) = build_ensures(attr); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( - #arg_copies + #remembers #(#before)* #(#after)* - kani::assume(#attr); - #copy_clean + kani::assume(#ensures_clause); #result ) } @@ -95,7 +94,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #(#before)* - #(*unsafe { kani::internal::Pointer::assignable(#attr) } = kani::any_modifies();)* + #(*unsafe { kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(#attr))) } = kani::any_modifies();)* #(#after)* #result ) diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index bf204e6bca32..2682c0781661 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -11,7 +11,10 @@ use std::collections::HashMap; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::{quote, ToTokens}; -use syn::Attribute; +use std::hash::{DefaultHasher, Hash, Hasher}; +use syn::{ + spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, Path, +}; use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT}; @@ -98,26 +101,6 @@ pub fn identifier_for_generated_function( Ident::new(&identifier, proc_macro2::Span::mixed_site()) } -/// We make shallow copies of the argument for the postconditions in both -/// `requires` and `ensures` clauses and later clean them up. -/// -/// This function creates the code necessary to both make the copies (first -/// tuple elem) and to clean them (second tuple elem). -pub fn make_unsafe_argument_copies( - renaming_map: &HashMap, -) -> (TokenStream2, TokenStream2) { - let arg_names = renaming_map.values(); - let also_arg_names = renaming_map.values(); - let arg_values = renaming_map.keys(); - ( - quote!(#(let #arg_names = kani::internal::untracked_deref(&#arg_values);)*), - #[cfg(not(feature = "no_core"))] - quote!(#(std::mem::forget(#also_arg_names);)*), - #[cfg(feature = "no_core")] - quote!(#(core::mem::forget(#also_arg_names);)*), - ) -} - /// Used as the "single source of truth" for [`try_as_result_assign`] and [`try_as_result_assign_mut`] /// since we can't abstract over mutability. Input is the object to match on and the name of the /// function used to convert an `Option` into the result type (e.g. `as_ref` and `as_mut` @@ -176,3 +159,119 @@ pub fn try_as_result_assign(stmt: &syn::Stmt) -> Option<&syn::LocalInit> { pub fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalInit> { try_as_result_assign_pat!(stmt, as_mut) } + +/// When a `#[kani::ensures(|result|expr)]` is expanded, this function is called on with `build_ensures(|result|expr)`. +/// This function goes through the expr and extracts out all the `old` expressions and creates a sequence +/// of statements that instantiate these expressions as `let remember_kani_internal_x = old_expr;` +/// where x is a unique hash. This is returned as the first return parameter. The second +/// return parameter is the expression formed by passing in the result variable into the input closure. +pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) { + let mut remembers_exprs = HashMap::new(); + let mut vis = OldVisitor { t: OldLifter::new(), remembers_exprs: &mut remembers_exprs }; + let mut expr = &mut data.clone(); + vis.visit_expr_closure_mut(&mut expr); + + let remembers_stmts: TokenStream2 = remembers_exprs + .iter() + .fold(quote!(), |collect, (ident, expr)| quote!(let #ident = #expr; #collect)); + + let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + (remembers_stmts, Expr::Verbatim(quote!((#expr)(&#result)))) +} + +trait OldTrigger { + /// You are provided with the expression that is the first argument of the + /// `old()` call. You may modify it as you see fit. The return value + /// indicates whether the entire `old()` call should be replaced by the + /// (potentially altered) first argument. + /// + /// The second argument is the span of the original `old` expression. + /// + /// The third argument is a collection of all the expressions that need to be lifted + /// into the past environment as new remember variables. + fn trigger(&mut self, e: &mut Expr, s: Span, output: &mut HashMap) -> bool; +} + +struct OldLifter; + +impl OldLifter { + fn new() -> Self { + Self + } +} + +struct OldDenier; + +impl OldTrigger for OldDenier { + fn trigger(&mut self, _: &mut Expr, s: Span, _: &mut HashMap) -> bool { + s.unwrap().error("Nested calls to `old` are prohibited").emit(); + false + } +} + +struct OldVisitor<'a, T> { + t: T, + remembers_exprs: &'a mut HashMap, +} + +impl syn::visit_mut::VisitMut for OldVisitor<'_, T> { + fn visit_expr_mut(&mut self, ex: &mut Expr) { + let trigger = match &*ex { + Expr::Call(call @ ExprCall { func, attrs, args, .. }) => match func.as_ref() { + Expr::Path(ExprPath { + attrs: func_attrs, + qself: None, + path: Path { leading_colon: None, segments }, + }) if segments.len() == 1 + && segments.first().map_or(false, |sgm| sgm.ident == "old") => + { + let first_segment = segments.first().unwrap(); + assert_spanned_err!(first_segment.arguments.is_empty(), first_segment); + assert_spanned_err!(attrs.is_empty(), call); + assert_spanned_err!(func_attrs.is_empty(), func); + assert_spanned_err!(args.len() == 1, call); + true + } + _ => false, + }, + _ => false, + }; + if trigger { + let span = ex.span(); + let new_expr = if let Expr::Call(ExprCall { ref mut args, .. }) = ex { + self.t + .trigger(args.iter_mut().next().unwrap(), span, self.remembers_exprs) + .then(|| args.pop().unwrap().into_value()) + } else { + unreachable!() + }; + if let Some(new) = new_expr { + let _ = std::mem::replace(ex, new); + } + } else { + syn::visit_mut::visit_expr_mut(self, ex) + } + } +} + +impl OldTrigger for OldLifter { + fn trigger( + &mut self, + e: &mut Expr, + _: Span, + remembers_exprs: &mut HashMap, + ) -> bool { + let mut denier = OldVisitor { t: OldDenier, remembers_exprs }; + // This ensures there are no nested calls to `old` + denier.visit_expr_mut(e); + let mut hasher = DefaultHasher::new(); + e.hash(&mut hasher); + let ident = + Ident::new(&format!("remember_kani_internal_{:x}", hasher.finish()), Span::call_site()); + // save the original expression to be lifted into the past remember environment + remembers_exprs.insert(ident.clone(), (*e).clone()); + // change the expression to refer to the new remember variable + let _ = std::mem::replace(e, Expr::Verbatim(quote!((#ident)))); + true + } +} diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index deeeca66ab7a..a8bd7bf66041 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -549,6 +549,49 @@ This is the technical portion of the RFC. Please provide high level details of t +We developed the `old` contract for history expressions via understanding it as a [modality](https://en.wikipedia.org/wiki/Monad_(functional_programming)) originating from [Moggi 1991](https://www.sciencedirect.com/science/article/pii/0890540191900524). +The `old` monad links the "language of the past" to the "language of the present". +Implementing the full generality of the monad is rather difficult, so we focus on a particular usage of the monad. + +We have an external syntax representation which is what the user inputs. We then parse this and logically manipulate it as a monad, prefixing all the `bind` operations. We then output the final compiled macro output as Rust code. + +In particular, if we have an ensures statement like +```rust +#[kani::ensures(old(*ptr)+1==*ptr)] +``` +Then we comprehend this as syntax for the statement (not within Rust) +``` +bind (*ptr : O(u32)) (|remember : u32| remember + 1 == *ptr) +``` +Here, the `O(u32)` is taking the type of the past `u32` and converting it into a type in the present `O(u32)` while the bind operation lets you use the value of the past `u32` to express a type in the present `bool`. + +This then gets compiled to (within Rust) +```rust +let remember = *ptr; +let result = ...; +kani::assert(remember + 1 == *ptr) +``` +This means that the underlying principle of the monad is there, but external syntax appears to be less like a monad because otherwise it would be too difficult to implement, and the user most likely only cares about this particular construction of prefixing all the `bind` operations. + +This construction requires that `old` expressions are closed with resprect to the input parameters. This is due to the lifting into the prefixed `bind` operations. + +A major drawback is that eta expansion fails. If we eta expand a function f, it becomes |x|f(x). Note that eta expansions guarantee that the original f and the |x|f(x) are equivalent which makes a lot of sense since you’re just calling the same function. However, we have that `old(y)` is not equivalent to `(|x|old(x))(y)`. `y` is a closed expression, so the first statement works. `x` is a bound variable, so it is an open expression, so compilation will fail. + +The reason for this restriction is that the user will most likely only want to use this particular prefixed `bind` structure for their code, so exposing the concept of monads to the user level would only confuse the user. It is also simpler from an implementation perspective to limit the monad to this particular usage. + +As for nested old, such as `old(old(*ptr)+*ptr)`, it is reasonable to interpret this as syntax representing +``` +bind (bind(*ptr)(|remember_1| remember_1 + *ptr)) (|remember_0| ...) +``` +which compiles to +```rust +let remember_1 = *ptr; +let remember_0 = remember_1 + *ptr; +let result = ...; +... +``` +so the restriction is just a matter of there not being implementation support for this kind of statement rather than the theory itself. It is not particularly useful to implement this because we claim that there should be no effectful computation within the contracts, so you can substitute the `remember_1` into the second line without worrying about the effects. Hence, we opt for simply restricting this behavior instead of implementing it. (Note: it can be implemented by changing `denier.visit_expr_mut(e);` into `self.visit_expr_mut(e);`) +