Getting Prusti internal error related to while loop condition

[atgeller]

Hi there, I'm getting the following error:

error: [Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Pred(Field(FieldExpr { base: Local(Local { variable: _9: Ref(tuple2$usize$bool), position: Position { line: 0, column: 0, id: 51 } }), field: tuple_0: Ref(usize), position: Position { line: 0, column: 0, id: 51 } }), write)))
  --> ex4_kmp.rs:90:1
   |
90 | / fn test(p:&VecWrapperUSize) {
91 | |     let mut x = 0;
92 | |     while x <= p.len() - 1 {
93 | |     }
94 | | }
   | |_^

while trying to verify the following function (as a minimal example). The definition of VecWrapperUSize is basically copied from the user guide, and I've included it at the bottom here as well.

fn test(p:&VecWrapperUSize) {
    let mut x = 0;
    while x <= p.len() - 1 {
    }
}

I'm also getting a similar error trying to verify a more complicated file, also using a vec wrapper in a while loop condition.

Interestingly enough, the same code verifies from above works with no problem using the following while loop condition instead:

fn test(p:&VecWrapperUSize) {
    let mut x = 0;
    while x < p.len() {
    }
}

VecWrapperUSize definition:

pub struct VecWrapperUSize {
    v: Vec<usize>
}

/// Need this because Prusti doesn't seem to be able to handle polymorphic types
impl VecWrapperUSize {
    /// A ghost function for getting the length of the vector
    #[trusted]
    #[pure]
    pub fn len(&self) -> usize {
        self.v.len()
    }

    /// A ghost function for specifying values stored in the vector.
    #[trusted]
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> usize {
        self.v[index]
    }

    /// A ghost function for specifying values stored in the vector.
    #[trusted]
    #[requires(index < self.len())]
    #[ensures(self.len() == old(self.len()) && forall(
        |i: usize| (i < self.len() && i != index) ==>
        self.lookup(i) == old(self.lookup(i))
    ) && self.lookup(index) == value)]
    pub fn store(&mut self, index: usize, value: usize) {
        self.v[index] = value;
    }
}

[fpoli]

Thanks for the report! This is the same issue as https://github.com/viperproject/prusti-dev/issues/389; there is an overflow check generated by the compiler that breaks the encoding of the loop.

[atgeller]

Would the same problem possibly arise for other sorts of checks as well? Or just overflow checks? I'm getting a similar error in a loop condition without any addition or subtraction, but using a VecWrapper lookup, so there would be a bounds check. (Quickly checking, this appears to be the case since pulling the lookup function into a local variable makes the issue go away)

[fpoli]

Yes, the general issue is not specific to overflow checks. See https://github.com/viperproject/prusti-dev/issues/389#issuecomment-984449062. Feel free to post any such example.

[JonasAlaif]

Duplicate of #389