`HashMap::clone` allows to prove false facts with a non-standard `Clone` implementation

[gewitternacht]

As described in this issue, if the Clone implementation of a HashMap's key produces a key with a different hash, or if key.clone() == key does not hold, then this can result in a broken HashMap after map.clone(). These assumptions are not documented anywhere, which is why I made a pull request to update the Clone trait documentation.

In Verus, the requirement of key.clone() == key for the keys of a HashMap/HashSet is (as far as I can tell) also not documented anywhere. HashMap::clone is specified to return a map equal to the original one, which is not true if key.clone() != key. Due to this, it is possible to prove false facts about a cloned HashMap, as shown here in the playground.

To my understanding, simply updating the HashMap::clone specification would not be enough to fix this issue: A Clone implementation that does not respect key.clone() == key can break very basic invariants of a HashMap, like every key occurring at most once in the map, so that afterwards, the specification of, e.g., HashMap::remove does not hold anymore. So maybe the requirement that key.clone() == key should be part of obeys_key_model<Key>, or be modelled similarly?

[jaylorch]

Thanks for pointing this out! I'm working on a PR to address this. It'll just be an update to the documentation of obeys_key_model, as you suggest.

[gewitternacht]

Thanks for the documentation update!
I'm just wondering: Should the HashMap::clone specification be updated too, to have obeys_key_model as a "precondition" for guaranteeing other@ == this@ (e.g., like insert, where the specification is ensures obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> { [actual postconditions] })? I'm not really sure for which HashMap functions this "precondition" is present and for which it isn't, so I might be wrong, but it seems appropriate for clone to me, as clone's behaviour directly depends on the newly added part (3) of obeys_key_model.

[jaylorch]

I don't think we need those assumptions for HashMap::clone, because they're on HashMap::insert. If you don't have the assumptions, you stop knowing anything about the view once it becomes non-empty, until you clear it, in which case it becomes empty again. And cloning an empty HashMap will give an empty one even if Key::clone has strange behavior.

[gewitternacht]

Ooh okay, I see, I think I now understand better why these assumptions are where they are. Thanks a lot for the explanation!

[gewitternacht]

I only now realised that the specification other@ == this@ of HashMap::clone is still unsound, as the values of the HashMap could also have a clone implementation that does not respect val.clone() == val. This playground link shows how this can lead to false facts being verified.
In contrast to keys with a weird clone implementation, this does not break the HashMap itself, but really is a problem with the specification other@ == this@, I think. It should probably say something like "other@ has the same domain as this@, and each new value is the result of cloning the old value" instead.

[jaylorch]

Could you please post a version of that with ensures false somewhere? I don't see how one gets to false from your example.

[tjhance]

I think @gewitternacht is correct, this specification:

pub assume_specification<K: Clone, V: Clone, S: Clone>[ <HashMap::<K, V, S> as Clone>::clone ](
    this: &HashMap<K, V, S>,
) -> (other: HashMap<K, V, S>)
    ensures
        other@ == this@,
;

assumes that V::clone will always returns an identical value (i.e., a spec-equal value). Generally we should be using cloned to specify the behavior of Clone for generic containers (see this page for an example).

I doubt you'll be able to actually "ensure" false, but it seems like a case where the spec doesn't match the executable code.

[gewitternacht]

a case where the spec doesn't match the executable code

Yes, this was what I was trying to say, and trying to show with the print_fake_one function: from the specification, it looks like the only thing that can ever be printed is FakeInt(1), but in the real word FakeInt(0) is printed. There are probably better ways to get this point across in a code example, but I don't know how to do that.

To actually reach a point where you can prove false, I think you would have to verify the actual HashMap::clone implementation, showing that there are cases where other@ != this@, and by this reach a contradiction with the assumed specification.