Support for encapsulated mutability in `modifies` clauses

[JustusAdam]

Data structures like RefCell mutate internal state on methods like borrow and borrow_mut. This state is not part of the public API and therefore cannot be mentioned in the modifies clause without breaking encapsulation.

Consider the following example that shows a simple function modifying a RefCell with a modifies clause that should be valid given the body of the function. It overapproximates the function (as the result will be an arbitrary value rather than the concrete 100 but this is not the point).

#[kani::modifies(cell.borrow())]
fn modifies_ref_cell(cell: &RefCell<u32>) {
    *cell.try_borrow_mut().map(|r| *r = 100);
}

However running this with kani creates the error:

Check 60: std::ptr::write::<isize>.assigns.3
     - Status: FAILURE
     - Description: "Check that *dst is assignable"

The reason is that as cell is borrowed it internally mutably sets the BorrowFlag (which is an isize) stored in the RefCell.

In Rust's encapsulation fields (like borrow) in the RefCell should not be used or referenced by a user of RefCell. because they are considered potentially unstable implementation details. It would be breaking the encapsulation if the modifies clause needed to reference the internal fields of the cell for the contract to pass. At the same time we can't simply assume that all private fields may be modified because that would cause them to be havocked which will break the invariants wrt the borrow field. For instance in this example cell.borrow == old(cell.borrow) (instead of kani::any()).

In contrast if we had the function

#[kani::modifies(cell.borrow())]
fn modifies_ref_cell_2(cell: &'a RefCell<u32>) -> Option<RefMut<'a, u32>> {
    *cell.try_borrow_mut().ok().map(|r| {
        *r = 100;
        r
    });
}

Then if return.is_some() { cell.borrow == 1 } else { cell.borrow == old(cell.borrow) }.

This is to illustrate that what it means to be assignable or assigned to is different for some types, such as RefCell. An additional issue is that structures such as RefCell, Rc, Arc etc also perform assignment even when not used mutably. A call to RefCell::borrow or Rc::clone while nominally being immutable operations at the surface will perform assignment to internal fields.

[celinval]

Is your concern here related to stubbing or contract verification?

I'm asking because I am not convinced that contracts should require access to internal fields of dependencies. If a function does not have access to a field, neither should its contract.

Looking at the first example, the contract should be:

#[kani::modifies(cell)]
#[kani::ensures(|_| cell.into_inner() == 100 || cell.into_inner() == old(cell.into_inner()))]
fn modifies_ref_cell(cell: &RefCell<u32>) {
    *cell.try_borrow_mut().map(|r| *r = 100);
}

I believe this should be enough check the behavior of this function.

For your second example, I am not so sure the contract should mention the state of cell. However, if the user does want to specify this behavior, they should use the public interface of cell, e.g.:

#[kani::modifies(cell)]
#[kani::ensures(|res| if res.is_some() { cell.try_borrow().is_err() } else { true })]
fn modifies_ref_cell_2(cell: &'a RefCell<u32>) -> Option<RefMut<'a, u32>> {
    *cell.try_borrow_mut().ok().map(|r| {
        *r = 100;
        r
    });
}

I agree that this will limit the stubbing functionality though, and a plain stub or a wrapper that extends the contract may be more suitable.

[celinval]

BTW, I think the encapsulation plays an important role when it comes to transitive modifies. I created a separate issue for that: https://github.com/model-checking/kani/issues/3372