vstd::std_specs::hash

Function lemma_hashmap_deepview_properties

Source 
pub broadcast proof fn lemma_hashmap_deepview_properties<K: DeepView, V: DeepView>(
    m: HashMap<K, V>,
)
Expand description
requires
crate::relations::injective(|k: K| k.deep_view()),
ensures
forall |k: K| (
    #[trigger] m@.contains_key(k)
        ==> m.deep_view().contains_key(k.deep_view())
            && m.deep_view()[k.deep_view()] == m@[k].deep_view()
),
forall |dk: <K as DeepView>::V| {
    #[trigger] m.deep_view().contains_key(dk)
        ==> exists |k: K| k.deep_view() == dk && #[trigger] m@.contains_key(k)
},