Fold/unfold failure for `Option::unwrap` specification

[Aurel300]

An extern specced Option with a postcondition like this fails fold/unfold:

#[requires(o.is_some())]
#[ensures(match o {
    Option::Some(v) => result == v,
    Option::None => false,
})]
fn unwrap<T>(o: Option<T>) -> T;

error: [Prusti internal error] cannot generate fold-unfold Viper statements. The required permission Acc(_13[enum_Some].f$0, read) cannot be obtained.

[fpoli]

Full example:

use prusti_contracts::*;

#[extern_spec]
impl<T: PartialEq> Option<T> {
    #[pure]
    #[ensures(result == match self {
        Option::Some(_) => true,
        Option::None => false,
    })]
    fn is_some(&self) -> bool;

    #[requires(self.is_some())]
    #[ensures(match self{
        Option::Some(v) => result == v,
        Option::None => false,
    })]
    fn unwrap(self) -> T;
}

fn main() {
    let x = Some(123);
    let y = x.unwrap();
    assert!(y == 123);
}

Error:

error: [Prusti internal error] cannot generate fold-unfold Viper statements. The required permission Acc(_3[enum_Some].f$0, read) cannot be obtained.
  --> tmp/program.rs:20:1
   |
20 | / fn main() {
21 | |     let x = Some(123);
22 | |     let y = x.unwrap();
23 | |     assert!(y == 123);
24 | | }
   | |_^

[fpoli]

Given this encoding

    // [mir] _2 = std::option::Option::<i32>::unwrap(move _3) -> [return: bb1, unwind: bb4]
    label l1
    assert (m_is_some<Snapshot(m_Option$_beg_$i32$_end_),Bool>(_3)) && (true)
    ...
    inhale (((old[l1](_3.discriminant)) == (0))?(false):((downcast _3 to enum_Some in (snap(_2)) == (snap(old[l1](_3[enum_Some].f$0)))))) && (true)

before label l1 the algorithm tries to obtain _3[enum_Some].f$0 because it's later used in an old[l1](...) expression. This is done to avoid having to fold inside old-expressions, which is not possible in Viper:

https://github.com/viperproject/prusti-dev/blob/705e79d808a81a99f2d0ad329d85305a48f6fa19/prusti-viper/src/encoder/foldunfold/requirements.rs#L66-L74

The algorithm fails to obtain the expression because before the label the variant of the enum is unknown. The correct thing to do would be to only fold to obtain the permissions required by old[l1](...) expressions, ignoring the rest.

[fpoli]

Adding old(..) in the postcondition around the argument of unwrap avoids the error:

use prusti_contracts::*;

#[extern_spec]
impl<T: PartialEq> Option<T> {
    #[pure]
    #[ensures(result == match self {
        Option::Some(_) => true,
        Option::None => false,
    })]
    fn is_some(&self) -> bool;

    #[requires(self.is_some())]
    #[ensures(match old(self) {
        Option::Some(v) => result == v,
        Option::None => false,
    })]
    fn unwrap(self) -> T;
}

fn main() {
    let x = Some(123);
    let y = x.unwrap();
    assert!(y == 123);
}

This might be related to https://github.com/viperproject/prusti-dev/issues/651