Help with HashMap / get_and_unwrap specification

[pinzaghi]

I am trying to use the function get_and_unwrap which has the precondition requires(map.contains_key(key)).

My HashMap spec looks like this:

#[extern_spec]
impl<K, V, S> HashMap<K, V, S>
where
    K: Eq + Hash,
    S: BuildHasher,
{
    #[trusted]
    #[pure]
    #[ensures(result ==> matches!(self.get(k), Some(_)))]
    pub fn contains_key<Q: ?Sized>(&self, k: &Q) -> bool
    where
        K: Borrow<Q>,
        Q: Hash + Eq;
}

My problem happens when I call get_and_unwrap(&self.next_index, &key), I get a precondition might not hold.

#[requires(self.is_initialized())]
#[requires(self.is_leader())]
#[requires(self.is_valid_id(destid))]
pub fn append_entries(&self, destid: &NodeId) -> Message {

    let m_prev_log_index = get_and_unwrap(&self.next_index, &destid)-1;
...

The important thing here is that requires(self.is_initialized()) should be enough for get_and_unwrap, because if that's true, indexing the map next_index should be safe.

This is where I don't know how to proceed:

#[pure]
#[ensures(forall(|i: usize| (0 <= i) ==> self.next_index.contains_key(&i) ))]
pub fn is_initialized(&self) -> bool{
    matches!(self.initialized,true)
}

I tried this but it causes an internal error. Any help is appreciated.

[vakaras]

What is the internal error?

[Aurel300]

Can you assert!(...) the .contains_key precondition before the get_and_unwrap call, and does it succeed? A minimal, reproducible example program would help us identify the problem. Finally, (especially if the internal error turns out to be a duplicate of an existing one,) issues like this might be better suited for our Zulip chat.

[pinzaghi]

It's a little difficult for me to slice a minimal example because they are several things working together, this is the repo with the problem: https://github.com/pinzaghi/rusty-raft

It only has 2 important files, raft.rs and log.rs, the latter was took from the user guide example, I'm using it as a list structure.

The contains_key precondition does not hold, here I try to add an ensures that would prove the precondition, but it generates internal errors.

If you want to reproduce the error, just clone the repo and execute:

cargo +nightly build
cargo-prusti

[pinzaghi]

I tried to obtain a minimal example:

#![feature(allocator_api)]

use std::hash::Hash;
use std::hash::BuildHasher;
use std::collections::{HashSet, HashMap};
use std::borrow::Borrow;
use core::alloc::Allocator;
use fxhash::{FxHashSet, FxHashMap, FxHasher};

use prusti_contracts::*;

#[extern_spec]
impl<K, V, S> HashMap<K, V, S> {
    #[pure]
    pub fn len(&self) -> usize;
}

#[extern_spec]
impl<T, A: Allocator> Vec<T, A> {
    #[pure]
    pub fn len(&self) -> usize;
}

#[extern_spec]
impl<K, V, S> HashMap<K, V, S>
where
    K: Eq + Hash,
    S: BuildHasher,
{
    #[trusted]
    #[pure]
    #[ensures(result ==> matches!(self.get(k), Some(_)))]
    pub fn contains_key<Q: ?Sized>(&self, k: &Q) -> bool
    where
        K: Borrow<Q>,
        Q: Hash + Eq;

    #[trusted]
    #[pure]
    pub fn get<Q: ?Sized>(&self, k: &Q) -> Option<&V>
    where
        K: Borrow<Q>,
        Q: Hash + Eq;
}

#[trusted]
#[ensures(is_initialized(map, list))]
pub fn init(map: &mut FxHashMap::<usize, usize>, list: Vec<usize>){
    for i in &list {
        map.insert(*i, 1);
    }
}

#[pure]
#[ensures((forall(|i: usize| (0 <= i && i < list.len()) ==> map.contains_key(&i))))]
pub fn is_initialized(map: &mut FxHashMap::<usize, usize>, list: Vec<usize>) -> bool{
    map.len() == list.len()
}

#[trusted]
#[requires(map.contains_key(key))]
fn get_and_unwrap<'a, K: Eq + Hash, V>(map: &'a FxHashMap<K, V>, key: &'a K) -> &'a V {
    map.get(key).unwrap()
}

#[requires(is_initialized(map, list))]
fn last_entry(map: &mut FxHashMap::<usize, usize>, list: Vec<usize>, index: usize) -> usize {
    assert!(map.contains_key(&index));

    *get_and_unwrap(map, &index)
}

maybe it's easier to see my problem. I have an internal error but also other problems not related to the original one:

error: [Prusti: invalid specification] pure function parameters must be Copy
  --> src/lib.rs:56:23
   |
56 | pub fn is_initialized(map: &mut FxHashMap::<usize, usize>, list: Vec<usize>) -> bool{
   |                       ^^^

error: [Prusti internal error] Prusti encountered an unexpected internal error
  --> src/lib.rs:56:1
   |
56 | / pub fn is_initialized(map: &mut FxHashMap::<usize, usize>, list: Vec<usize>) -> bool{
57 | |     map.len() == list.len()
58 | | }
   | |_^
   |
   = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
   = note: Details: cannot generate fold-unfold Viper statements. The required permission Acc(_2.val_int, read) cannot be obtained.
           

error: [Prusti: invalid specification] pure function parameters must be Copy
  --> src/lib.rs:66:12
   |
66 | #[requires(is_initialized(map, list))]
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^

[Aurel300]

There are several problems and the Prusti errors are not all internal (so you should read them):

• pure function parameters must be Copy - you are trying to pass a mutable reference to a hashmap and an owned vector to is_initialized, neither of these are Copy types. In pure functions you generally want to take shared references to complex data structures, so &FxHashMap and &Vec. The calls to is_initialized need to be updated accordingly.
• Once the above is fixed, the error is postcondition might not hold for is_initialized: and this makes sense, the function does nothing to make sure that quantifier holds. What you are looking for is a predicate, i.e. predicate! { pub fn is_initialized(..) -> bool { map.len() == list.len() && forall(..) } }.
• Once that is fixed, then the first assertion in last_entry (map.contains_key(&index)) does not have to pass because index may be >= list.len(). I guess you want to add #[requires(index < list.len())] to last_entry.

Then the example verifies.

[pinzaghi]

Thanks for your feedback. I updated the code like this:

#![feature(allocator_api)]

use std::hash::Hash;
use std::hash::BuildHasher;
use std::collections::{HashSet, HashMap};
use std::borrow::Borrow;
use core::alloc::Allocator;
use fxhash::{FxHashSet, FxHashMap, FxHasher};

use prusti_contracts::*;

#[extern_spec]
impl<K, V, S> HashMap<K, V, S> {
    #[pure]
    pub fn len(&self) -> usize;
}

#[extern_spec]
impl<T, A: Allocator> Vec<T, A> {
    #[pure]
    pub fn len(&self) -> usize;
}

#[extern_spec]
impl<K, V, S> HashMap<K, V, S>
where
    K: Eq + Hash,
    S: BuildHasher,
{
    #[trusted]
    #[pure]
    #[ensures(result ==> matches!(self.get(k), Some(_)))]
    pub fn contains_key<Q: ?Sized>(&self, k: &Q) -> bool
    where
        K: Borrow<Q>,
        Q: Hash + Eq;
}

predicate! { pub fn is_initialized(map: &FxHashMap::<usize, usize>, list: &Vec<usize>) -> bool { map.len() == list.len() && forall(|i: usize| (0 <= i && i < list.len()) ==> map.contains_key(&list[i])) } }

#[trusted]
#[ensures(is_initialized(&map, &list))]
pub fn init(map: &mut FxHashMap::<usize, usize>, list: Vec<usize>){
    for i in &list {
        map.insert(*i, 1);
    }
}

#[trusted]
#[requires(map.contains_key(key))]
fn get_and_unwrap<'a, K: Eq + Hash, V>(map: &'a FxHashMap<K, V>, key: &'a K) -> &'a V {
    map.get(key).unwrap()
}

#[requires(is_initialized(&map, &list))]
#[requires(index < list.len())]
fn last_entry(map: &mut FxHashMap::<usize, usize>, list: Vec<usize>, index: usize) -> usize {
    let key = list[index];
    assert!(map.contains_key(&key));

    *get_and_unwrap(map, &index)
}

and I'm having:

error: [Prusti: unsupported feature] Non-slice LHS type '&usize' not supported yet
  --> src/lib.rs:65:15
   |
65 |     let key = list[index];
   |               ^^^^^^^^^^^

did I miss something?

[pinzaghi]

Following up with this @Aurel300, I don't want to bother, but maybe this last error is something simple for you to see. Thanks again.

[hiroki-chen]

Following up with this @Aurel300, I don't want to bother, but maybe this last error is something simple for you to see. Thanks again.

@pinzaghi Prusti cannot fully support std::vec::Vec type, so it would be better for you to wrap the vector into another struct, say VecWrapper<T> and give pure function specifications on that type. You can follow the example here. Also this thread may be enlightening for you.