"not yet implemented: action fold" error

[fpoli]

The following program makes Prusti crash with

thread 'main' panicked at 'not yet implemented: action fold acc(m_20200615_225658$$Locator$opensqu$0$closesqu$$_beg_$_end_:None(_16.val_ref), read)', prusti-viper/src/encoder/foldunfold/action.rs:44:17

The error happens during the encoding of the delete method. Deleting or changing the contract of remove (called by delete) makes the crash disappear.

Actions to close this issue:

• [x] Make Prusti report the error without crashing, pointing to the method that was being encoded.
• [ ] Make Prusti verify the given program.

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: MIT-0

// This version will compile with prusti-rustc but uses various partially
// supported features. Attempting to verify anything might crash Prusti.

extern crate prusti_contracts;

use std::collections::HashMap;
use std::hash::Hash;

#[derive(Copy, Clone, PartialEq, Eq, Hash)]
pub struct Locator(usize);

const NUM_PAGES: usize = 512usize;

#[derive(Clone)]
pub struct Page<T>
    where T: Clone
{
    data: T,
    next:  Option<usize>,
}

// PRUSTI START: trusted wrappers
#[derive(Clone)] // partially supported due to internal usage of raw pointers
pub struct VecWrapper<T> 
    where T: Clone
{
    v: Vec<T>,
}

impl<T> VecWrapper<T>
    where T: Clone
{

}

pub struct HashMapLocatorWrapper
{
    m: HashMap<Locator, Locator>,
}

impl HashMapLocatorWrapper
{

    //Option<&Locator>
    #[trusted]
    pub fn get(&self, k: &Locator) -> Option<Locator>{
        unimplemented!()
    }

    #[trusted]
    #[pure]
    pub fn contains_kv(&self, k: &Locator, v: usize) -> bool {
       unimplemented!()
    }

    #[trusted]
    //#[ensures="old(self.contains_kv(k,0)) == false ==> self.existsZero() == true"] // original
    #[ensures="old(self.contains_kv(k, 0))"] // minimized
    pub fn remove(&mut self, k: &Locator) -> Option<Locator> {
        //self.m.remove(k)
        unimplemented!()
    }

    #[trusted]
    #[pure]
    pub fn existsZero(&self) -> bool{
        unimplemented!()
    }

}
// PRUSTI END

struct Disk<T>
    where T:Clone
{
    pages: VecWrapper<Page<T>>,
}

impl<T> Disk<T>
    where T: Clone
{
    //#[requires="p < self.pages.len()"]
    fn read(&self, p: usize) -> Page<T> {
        unimplemented!()
    }
}

pub struct KeyStore<T>
    where T: Clone
{
    disk: Disk<T>,
    predecessor: HashMapLocatorWrapper,
}

impl<T> KeyStore<T>
    where T: Eq + Hash + Clone
{
    // The crash happens during the encoding of this method:
    pub fn delete(&mut self, locator: Locator) {
        if let Some(loc) = self.predecessor.get(&locator) {
            let this_page = self.disk.read(locator.0);
            self.predecessor.remove(&locator);
        }
    }
}

fn main() {}

[fpoli]

PR #64 makes Prusti report the error without crashing, pointing to the method that was being encoded.