Issues with verifying the result is None

[nokunish]

Hi, calling a function that always returns None from the pre/post-condition/ prusti assertions, i.e.,

#[pure]
fn test(u: u32) -> Option<u32> {
     return None    
}

#[requires(test(10).is_none())]
fn main() {
}

produces errors: Error 1:

Details: consistency error in prusti_test::test_v1::code::debug::debug::main: Consistency error: No domain function named cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_ found in the program. (<no position>)

Error 2:

Details: consistency error in prusti_test::test_v1::code::debug::debug::main: Consistency error: No matching identifier cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_ found of type DomainFunc. (<no position>)

If test(..) returns an Option of type tuple (i.e., Option<(u32, u32)>), then it additionally produces:

Details: consistency error in prusti_test::test_v1::code::debug::debug::main: Consistency error: DomainType references non-existent domain Snap$tuple2$u32$u32. (<no position>)

In this simple example, returning Some from a branch fixes the issue

// this doesn't produce the error msgs 

#[pure]
fn test(u: u32) -> Option<u32> {
    if u < 10 {
        return Some(u)
    }
    return None    
}

However, say we have a struct struct S1(Option<usize>) with the following two methods

impl S1 {

    #[ensures(self.filter(7).is_none())]                    // P1
    fn new(&self) -> Self {
        Self{0: None}
    }

    #[pure]
    #[ensures(u <= 10 ==> result.is_none())]         // P2
    pub fn filter(&self, u: u32) -> Option<u32> {
        if u > 10 {
            return Some(u)
    }  
        return None
    }  
} 

Prusti crashes if we compile as shown above, but it wouldn't if

• the post-condition of filter(..) doesn't guarantee P1 (i.e., omit P2 entirely, or modify it such that #[ensures(u <= 4 ==> result.is_none())]. This fails normally
• change input u for filter to usize and output to Option<usize> (to match the field type of S1). But in this case, P1 always gets verified (regardless of the strength / presence of post-condition for filter)

The same issue is observed when we convert the post-condition to a Prusti assertion instead. Most interestingly, if we try to verify that the result is some (i.e., #[ensures(self.filter(10).is_some())]), then Prusti doesn't crash.

As reference, I defined the external specifications as follows, although this doesn't seem to be the problem

#[extern_spec]
impl <T> Option<T> 
{
    #[pure]
    #[ensures(matches!(*self, Some(_)) <==> result)]
    #[ensures(!result <==> self.is_none())]
    pub fn is_some(&self) -> bool;

    #[pure]
    #[ensures(matches!(*self, None) <==> result)]
    #[ensures(!result <==> self.is_some())]
    pub fn is_none(&self) -> bool;
}

[Aurel300]

(I can't test this atm, but) does it make a difference if you remove these two postconditions from the extern spec?

    #[ensures(!result <==> self.is_none())]
    #[ensures(!result <==> self.is_some())]

[nokunish]

It does not seem to make any difference... I've commented both/either one of them out, and they crash. I've also tried changing to #[ensures(!result == self.is_none())],#[ensures(result != self.is_none())], as well as annotating is_none(..) as trusted, but none of these seem to work either

If I comment out both post-conditions for None

#[pure]
    pub fn is_none(&self) -> bool;

then, Prusti does not crash, but then it wouldn't be very helpful since we can't verify

#[pure]
    #[ensures(u <= 10 ==> result.is_none())]                   // this fails 
    pub fn filter(&self, u: u32) -> Option<u32> {
        if u > 10 {
            return Some(u)
    }  
        return None
    }

[jscissr]

This bug happens for the same reason as #1391. The problem is that for enums which are only used in specifications (pre- and postconditions, assertions) of a function but not in its body, some functions and axioms are not generated in the viper domain of the snapshot type. In particular, some constructors and the discriminant axioms are missing. In this case, the injectivity axiom is still present and refers to a missing constructor:

domain Snap$m_std$$option$$Option$_beg_$u32$_end_  {

  function discriminant$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$(self: Snap$m_std$$option$$Option$_beg_$u32$_end_): Int 

  function cons$0$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$Snap$m_std$$option$$Option$_beg_$u32$_end_(): Snap$m_std$$option$$Option$_beg_$u32$_end_ 

  axiom Snap$m_std$$option$$Option$_beg_$u32$_end_$1$injectivity {
    (forall _l_0: Int, _r_0: Int ::
      { cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_(_l_0),
      cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_(_r_0) }
      cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_(_l_0) ==
      cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_(_r_0) ==>
      _l_0 == _r_0)
  }
}

We can work around this bug by explicitly mentioning the type in the function body, which causes everything in the snapshot domain to be generated:

#[pure]
fn test(u: u32) -> Option<u32> {
     return None
}

#[requires(test(10).is_none())]
fn main() {
    let _: Option<u32> = None;
}

[nokunish]

Hi,

There seems to be a similar bug with Option::Some(..) as well. For instance, if we have a function that always returns Some(usize),

    #[pure]
    pub fn some_obj(&self) -> Option<usize> {
        Some(10)
    }

    #[pure]                                                     // does not affect results
    #[ensures(result <==> self.some_obj().is_some())]      
    pub fn is_true(&self) -> bool {
        let _: Option<usize> = None;                           
        true
    }

Prusti crashes if the post-condition for is_true(..) is imposed, even if we mention the type explicitly and remove the pure annotation. On the other hand when a similar tactic is used for some_obj(..), i.e.,

    #[pure]
    pub fn some_obj(&self) -> Option<usize> {
        let obj: Option<usize> = Some(10);
        obj
    }

the explicit mentioning of the type makes Prusti crash, only if the fuction is marked as pure.