Specification refinement on `Cell<T>` with trait bounds

[Pointerbender]

When feeding the following Rust program to Prusti:

use prusti_contracts::*;
use core::cell::Cell;
fn main() {
    let foo = Cell::new(1);
    assert!(foo.get() == 1);
}

#[extern_spec]
impl<T: Copy> Cell<T> {
    #[pure]
    pub fn get(&self) -> T;
}

#[extern_spec]
impl<T: Copy + PartialEq> Cell<T> {
    #[ensures(result.get() == old(value))]
    pub fn new(value: T) -> Cell<T>;
}

Prusti warns warning: [Prusti: unsupported feature] T$0 type is not supported for the second #[extern_spec], but not for the first #[extern_spec]. I suspect this is because of the extra PartialEq trait bound on that impl block. Unfortunately, the PartialEq trait bound is needed in this case, otherwise Prusti won't allow the #[ensures(result.get() == old(value))] specification.

Since this warning comes from the vir high encoding which recently had some refactoring, I just wanted to check if this is purposely unsupported for now, or if there would be a way to only support PartialEq on trait bounds for external specifications just like in the pure encoding and procedure encoding. Would this be possible?

[vakaras]

This is clearly a regression introduced during the refactoring; I will look into it once I have some free time (currently is an exam period and I have to supervise and grade exams).

By the way, putting #[pure] on Cell methods is unsound because pure functions assume that data referenced via shared references cannot be changed. However, since Cell internally uses internal mutability, this assumption is violated.

[Pointerbender]

Thanks for the feedback and good luck with the exams!

By the way, putting #[pure] on Cell methods is unsound because pure functions assume that data referenced via shared references cannot be changed. However, since Cell internally uses internal mutability, this assumption is violated.

Is that also unsound in this case:

#[extern_spec]
impl<T: Copy> Cell<T> {
    #[pure]
    pub fn get(&self) -> T;
}

Due to that Cell is !Sync and get() copies the value out of Cell<T> without modifying the inner T: Copy, it is true that this method call is pure for the duration of the method call to get(), because the same thread nor other threads can change the contents of &self during get(). As long as there is no #[pure] on methods like Cell::replace, Cell::set, Cell::take, I would expect this is sound, but I'm not sure now if Prusti reasons along the same lines :)

[vakaras]

Consider the following example:

struct A { f: i32 }

#[trusted]
#[pure]
fn get(a: &A) -> i32 { unimplemented!{} }

fn do_something(x: &A) { }

fn test(a: A) {
  let x = &a;
  let t = get(x);
  do_something(x);
  assert!(t == get(x));  // Verifies.
}

The assert on the last line verifies. However, if you replace A with Cell, it is clear that it should not because do_something(x: &Cell<i32>) could call x.set(5). The problem is that adding #[pure] on get makes it assume that its result does not change as long as it is called with the same shared reference.

[Pointerbender]

I see! This even happens despite the fact that do_something is not marked as #[pure]. Thinking deeper about it, I believe part of the reason must be because do_something gets passed a copy of x: &A. The effects of do_something only affect the copy of x, not x itself. Thanks for the clarification :)

As a thought-experiment, I tried to see what happens when working with a single shared reference which can not be copied:

struct NonCopyRef<'a> {
    ptr: NonNull<A>, // to silence error related to unsupported struct field lifetimes
    _a: PhantomData<&'a A>,
}
impl<'a> NonCopyRef<'a> {
    pub fn new(a: &'a A) -> Self {
        Self {
            ptr: NonNull::from(a),
            _a: PhantomData
        }
    }
    #[pure]
    #[trusted]
    pub fn get(&self) -> i32 { unimplemented!()}
}
struct A { f: i32 }

#[trusted]
fn do_something(x: NonCopyRef) -> NonCopyRef { x }

fn test(a: A) {
  let x = NonCopyRef::new(&a);
  let t = x.get();
  let x = do_something(x);
  assert!(t == x.get()); // Should not verify
}

but then hit a wall because of a new error error: [Prusti internal error] cannot generate fold-unfold Viper statements. Failed to subtract fractional permissions: invalid substraction: read - write during the encoding of fn test. Assuming this worked in Prusti, would this be sound? Or does Prusti currently assume that once passed to a #[pure] function, a shared reference can never be internally mutated regardless of being copied or not, even when passed to non-pure functions afterwards?

[vakaras]

Prusti assumes that everything reachable from a shared reference is immutable as long as that reference is alive. This assumption holds for any code that does not use UnsafeCell and raw pointers. Since using them directly requires unsafe (which is not supported at the moment), you cannot run into problems by using shared references directly. However, you can run into problems if you use pure functions: pure functions are required to be deterministic, but you can violate this property by using internal mutability like your get function in the first example.

Or does Prusti currently assume that once passed to a #[pure] function, a shared reference can never be internally mutated regardless of being copied or not, even when passed to non-pure functions afterwards?

Yes, exactly.