[Internal Error] Prusti crashes when moving a mutable reference inside a loop

[lynae99]

Prusti encounters an unexpected internal error when a mutable reference is moved to a new local variable inside a nested loop. The reference is obtained from a function annotated with #[after_expiry].

use prusti_contracts::*;

pub struct VecWrapper<T>{
    v: Vec<T>
}
impl<T: Clone> VecWrapper<T> {
    #[trusted]
    #[ensures(result.len() == size)]
    pub fn new(value: T, size: usize) -> Self {
        VecWrapper { v: vec![value; size] }
    }
    #[trusted]
    #[pure]
    pub fn len(&self) -> usize {
        self.v.len()
    }
    #[trusted]
    #[requires(0 <= index && index < self.len())]
    pub fn index(&self, index: usize) -> &T {
        &self.v[index]
    }
    #[trusted]
    #[requires(0 <= index && index < self.len())]
    #[after_expiry(self.len() == old(self.len()))]
    pub fn index_mut(&mut self, index: usize) -> &mut T {
        &mut self.v[index]
    }
}

fn doors1() {
    let mut door_open = VecWrapper::new(false, 100);
    let mut pass = 1;
    while pass < 100 {
        body_invariant!(pass < 100);
        body_invariant!(1 <= pass);
        body_invariant!(door_open.len() == 100);
        let mut door = pass;
        while door <= 100 {
            body_invariant!(door <= 100);
            body_invariant!(1 <= door);
            body_invariant!(door_open.len() == 100);
            let door_state = !door_open.index(door - 1);
            let new_door_state = door_open.index_mut(door - 1);
            let _new_new_door_state = new_door_state;
            *_new_new_door_state = door_state;
            door += pass;
        }
        pass += 1;
    }
}

fn main() {}

Actual Behavior
Prusti reports an internal error:

error: [Prusti: internal error] Prusti encountered an unexpected internal error
  |
  = help: This could be caused by too small assertion timeout. Try increasing it by setting the configuration parameter ASSERT_TIMEOUT to a larger value.
  = note: This is likely to be a bug in Prusti. We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: unregistered verification error: [fold.failed:insufficient.permission; 0] Folding bool(_old$l27$0) might fail. There might be insufficient permission to access self.val_bool (@0.0)

Expected Behavior
The code is valid Rust and should be verified successfully