Treatment of Clone, and of Hash and HashMap

[utaal]

We need to determine the design and encoding of Clone, Hash, etc. to be able to support HashMap and HashSet.

Related pull requests with previous attempts:

#174

#308

Related archived branch: https://github.com/verus-lang/verus/tree/archive/implement_dict

[tjhance]

We need to consider how Clone should interact with view().

When I implemented Rc (see https://github.com/verus-lang/verus/blob/main/source/rust_verify/example/state_machines/tutorial/rc.rs) I had to make the spec for clone using view():

fn clone(&self) -> (other: Self)
  ensures self@ === other@

Proving the stronger self === other turned out to be infeasible. The reason was somewhat technical, and it's possible it could be worked around. But my feeling is that in general, we'll frequently want the postcondition self@ === other@.

It seems kind of tricky to have a condition like that generically, though.
Maybe we need some kind of ClonePreservesView trait or some such?