unsoundness when verifying reference-typed fields with quantifiers

[nokunish]

It may somewhat be related to #1029, but I am having trouble verifying a universal statement that accesses reference type fields, specifically when we use HashMap::get(..).

For the external specifications, I provided

    #[ensures(result.is_none() ==> !old(self.contains_key(&k)))]
    #[ensures(result.is_some() ==> 
        old(self.contains_key(&k)) && old(snap(self.get(&k).unwrap())) === result.unwrap()
    )]
    #[ensures(forall( |u: K| old(self.contains_key(&u)) && u != k 
        ==> self.contains_key(&u) && *self.get(&u).unwrap() === old(snap(self.get(&u).unwrap()))
    , triggers = [(self.contains_key(&u), )]
    ))]
    #[ensures(
        self.contains_key(&k) && *self.get(&k).unwrap() === v
    )]
    pub fn insert(&mut self, k: K, v: V) -> Option<V>;  

So that HashMap::insert(..) wouldn't make unnecessary changes.

In the following code, the first post-condition gets verified, however the second one fails:

#[requires(forall(
        |u: usize| map.contains_key(&u) ==> *map.get(&u).unwrap() < 10
        , triggers = [(map.contains_key(&u), )]
    ))]
#[ensures(
    map.contains_key(&i) && *map.get(&i).unwrap() == 6
)]
#[ensures(forall(
        |u: usize| map.contains_key(&u) ==> *map.get(&u).unwrap() < 10
        , triggers = [(map.contains_key(&u), )]
    ))]
fn modify_map(map: &mut HashMap<usize, usize>, i: usize) {
    map.insert(i, 6);
}

I tried using

#[pure]
#[trusted]
#[requires(map.contains_key(&u))]
fn getter(map: &HashMap<usize, usize>, u: usize) -> usize
{
    *map.get(&u).unwrap()       
}

and it causes the same error (changing to map.get(&u).unwrap() and returning &usize didn't help).

On the other hand, the existential statement got verified if we call map.get(&u).unwrap() directly

#[requires(exists(
        |u: usize| map.contains_key(&u) ==> *map.get(&u).unwrap() < 10
        , triggers = [(map.contains_key(&u), )]
    ))]
#[ensures(exists(
        |u: usize| map.contains_key(&u) ==> *map.get(&u).unwrap() < 10
        , triggers = [(map.contains_key(&u), )]
    ))]

But if we use the wrapper getter(..) function,

#[requires(exists(
        |u: usize| map.contains_key(&u) ==>  getter(&map, u) < 10
        , triggers = [(map.contains_key(&u), )]
    ))]
#[ensures(exists(
        |u: usize| map.contains_key(&u) ==>  getter(&map, u) < 10
        , triggers = [(map.contains_key(&u), )]
    ))]

then Prusti highlights the function modify_map and reports that the post-condition might not hold, rather than highlighting the failing condition.