Implement old() function for contracts

[JustusAdam]

As part of the function contracts implementation we require a notion of history variables, aka old.

As a running example we shall use this simple function (modify) and harness (main):

fn modify(ptr: &mut u32) {
    *ptr += 1
}

#[kani::proof]
fn main() {
    let _ = Box::new(());
    let mut i = kani::any();
    modify(&mut i);
}

Prereqs

We have access to history variables in CBMC, via __CPROVER_old.

Attempt 1: Rewrite a kani::old function via GotoHook

This method exposes the function below as part of the kani library and installs a hook in the code generation that implements this function call as __CPROVER_old(*t).

#[inline(never)]
#[rustc_diagnostic_item = "KaniOld"]
pub fn old<T>(t: &T) -> T { todo!() }

This would make a contract for our example be #[kani::ensures(kani::old(ptr) == *ptr - 1)]

This approach did not work, because the following constraints cannot be (easily) unified.

1. Contracts in Kani generate a new function. In the example that is

   fn modify_ensures_1(ptr: &mut u32, result: &()) -> bool { 
     kani::old(ptr) == *ptr - 1 
   }

   We do this so we can support arbitrary code in the condition and Rust deals with parsing, type checking etc for us. The CBMC level contract we then generate is __CPROVER_ensures(modify_ensures_1(ptr, &__CPROVER_return_value)). We need to use this encoding, because our generated function may contain control flow, which is generated if the contract calls functions or uses the short circuiting && or ||. Control flow is not allowed directly in the CBMC contract, but is allowed in the called function which is why we can't (easily) inline the body of modify_ensures_1.
2. __CPROVER_old is only allowed to be called directly inside __CPROVER_ensures, not anywhere else and thus also illegal in modify_ensures_1. See __CPROVER_old is ignored when called form a spec function diffblue/cbmc#7775

We would need to inline the generated function directly into the call to __CPROVER_ensures and rewrite all control flow to eliminate jumps.

Attempt 2: Pass all old arguments to the generated function

In the second attempt we instead always provide all history values as old_<var name>. In the example this would change the contract to #[kani::ensures(*old_ptr == *ptr - 1)] and generate the following function

fn modify_ensures_1(ptr: &mut u32, old_ptr: &mut 32, result: &()) -> bool { 
  *old_ptr == *ptr - 1 
}

And the CBMC contract __CPROVER_ensures(modify_ensures_1(ptr, __CPROVER_old(ptr), &__CPROVER_return_value)).

This also does not work, because unfortunately __CPROVER_old makes shallow copies. In this case it would copy the value of the pointer, but not the value behind the pointer and making this contract fail.

Proposal 1: Expression extraction

We could expand the idea from Attempt 2, but instead of always working on the arguments work on arbitrary (lvalue) expressions we extract during the macro invocation.

The contract would look more similar to Attempt 1: #[kani::ensures(old(ptr) == *ptr - 1)], but this time the expression in the old() call is extracted, stored and replaced by a generated_variable. We then generate a function that expects the result of that old() call to be passed in addition to the function arguments.

fn modify_ensures_1(ptr: &mut u32, old_1: u32, result: &()) -> bool { 
  old_1 == *ptr - 1 
}

And generate the CBMC contract __CPROVER_ensures(modify_ensures_1(ptr, __CPROVER_old(*ptr), &__CPROVER_return_value).

This has a couple of problems actually. The first one is types. While I just gave old_1 u32 here, when this function is generated (in a macro) we don't actually have access to the type of *ptr. We could get around this by instead generating a function that wraps a closure which closes over the old expressions to get type inference, e.g.

fn modify_ensures_1<'a>(ptr: &'a mut u32, result: &'a ()) -> impl Fn() -> bool + 'a {
  let old_1 = *ptr;
  || old_1 == *ptr - 1
}

This will cause Rustc to generate code for a closure for us like so:

struct [modify_ensures_1_closure_1] {
  old_1: u32,
  ptr: &mut u32
}

fn modify_ensures_1_closure_1(closure: &[modify_ensures_1_closure_1]) -> bool {
  closure.old_1 == *closure.ptr - 1
}

fn modify_ensures_1(ptr: &mut u32, result: &()) -> [modify_ensures_1_closure_1] {
  let old_1 = *ptr;
  [modify_ensures_1_closure_1] {
    ptr, old_1
  }
}

We can then ignore modify_ensures_1 and generate a CBMC contract from the closure like so

__CPROVER_ensures(
  modify_ensures_1_closure_1(&{ ptr = ptr, old_1 = __CPROVER_old(*ptr) })
)

The second drawback is that we can only support simple expressions inside of old. In particular we cannot support function calls easily as they require type inference, monomorphization etc. But they are needed because for instance our vec-map example always uses function call conditions, e.g. !old(self.contains_key(&key)).

Proposal 2: Inlining spec functions

Straightforward: Just do what I said before is hard and transform the body of modify_ensures_1 into an expression and inline it.

This is actually still not enough to enable function calls in old, because CBMC does not allow it, see diffblue/cbmc#7802

Proposal 3: Abandon CBMC

Instead of using CBMC we can solve this issue on the Kani side but that means we need to reimplement contract enforcement. The easiest way to achieve it is through lots of code generation plus function replacement in the compiler. When we encounter a contract instead of just generating a function for the contract, we can instead generate a new function that implements the contract's enforcement (or substitution). old is handled by parsing the condition with syn and then replacing all invocations of old with a temporary variable. The enforcement function has the same signature as the function on which the contract is placed. In its body we first discharge all assumes, then evaluate the old expressions and store them in the aforementioned variables, then we call the original function, then check all asserts. Finally we link the enforcement function to the original function using a kanitool attribute that carries the name of the replacement function. Example below for the contract #[kani::ensures(old(*ptr) == *ptr - 1)]

fn modify_copy_1(ptr: &mut u32) {
    *ptr += 1
}


fn modify_check_1(ptr: &mut u32) {
  let old_1 = *ptr;
  let result = modify_copy_1(ptr);
  kani::assert(old_1 == *ptr - 1);
  result
}

#[kanitool::checked_with = "modify_check_1"]
fn modify(ptr: &mut u32) {
    *ptr += 1
}

The benefit of this approach is that this supports arbitrary expressions inside old though they must respect borrowing rules. That however is fine, as users can simply use clone if they want to avoid references.

The easiest way to make implement the enforcement in a harness then is to add a kani::for_contract(modify) attribute for harnesses that instructs the compiler to replace occurrences of modify with the function mentioned in checked_by on modify. This way we need no additional enforcement mechanism and the driver can simply invoke the harness.

The only exception here is assigns clauses. I see no easy way to handle them in Kani, but they can simply be substituted and dispatched to CBMC as before.

Note: I have actually already implemented this last option and it works well for contract checking on vec-map, including supporting arbitrary old expressions.