pub broadcast proof fn axiom_spec_hash_map_iter<'a, Key, Value, S>(
m: &'a HashMap<Key, Value, S>,
)Expand description
ensures
({
let v = #[trigger] spec_hash_map_iter(m).remaining();
&&& v.len() == m@.dom().len()
&&& forall |i: int| {
0 <= i < v.len() ==> m@.contains_key(*v[i].0) && m@[*v[i].0] == *v[i].1
}
&&& forall |k: Key| #[trigger] m@.contains_key(k) ==> v.contains((&k, &m@[k]))
&&& v.unref().to_set() == m@.kv_pairs()
}),