Implementing Clone

As a finishing touch, let’s implement Clone for TreeMap<K, V>. The main trick here will be in figuring out the correct specification for TreeMap::<K, V>::Clone.

Naturally, such an implementation will require both K: Clone and V: Clone. However, to write a sensible clone implementation for the tree, we have to consider what the implementations of K::clone and V::clone actually do.

Generally speaking, Verus imposes no constraints on the implementations of the Clone, so it is not necessarily true that a clone() call will return a value that is spec-equal to its inputs.

With this in mind, we’re going to prove the following signature for TreeMap<K, V>::clone:

impl<K: Copy + TotalOrdered, V: Clone> Clone for TreeMap<K, V> {
    fn clone(&self) -> (res: Self)
        ensures self@.dom() =~= res@.dom(),
            forall |key| #[trigger] res@.dom().contains(key) ==>
                call_ensures(V::clone, (&self@[key],), res@[key])
    {
        ...
    }
}

Dealing with K::clone

In order to clone all the keys, we need K::clone to respect the ordering of elements; otherwise, we’d need to resort all the keys on clone in order for the resulting tree to be valid. However, it’s not likely that is desirable behavior. If Clone doesn’t respect the TotalOrdered implementation, it’s likely a user bug.

A general way to handle this would be to require that Clone actually be compatible with the total-ordering in some sense. However, you’ll recall from the previous section that we’re already simplifying the “total ordered” specification a bit. Likewise, we’re going to continue to keep things simple here by also requiring that K: Copy.

As a result, we’ll be able to prove that our TreeMap clone implementation can preserve all keys exactly, even when compared via spec equality. That is, we’ll be able to ensure that self@.dom() =~= res@.dom().

Dealing with V::clone

So what about V? Again, we don’t know a priori what V::clone does. It might return values unequal to the imput; it might even be nondeterminstic. Therefore, a cloned TreeMap may have different values than the original.

In order to specify TreeMap::<K, V>::clone as generically as possible, we choose to write its ensures clause in terms of the ensures clause for V::clone. This can be done using [call_ensures](./exec_funs_as_values.md). The predicate call_ensures(V::clone, (&self@[key],), res@[key]) effectively says “self@[key] and res@[key] are a possible input-output pair for V::clone”.

Understanding the implications of the signature

Let’s do a few examples.

First, consider cloning a TreeMap::<u64, u32>. The Verus standard library provides a specification for u32::clone; it’s the same as a copy, i.e., a cloned u32 always equals the input. As a result, we can deduce that cloning a TreeMap::<u64, u32> will preserve its view exactly. We can prove this using extensional equality.

fn test_clone_u32(tree_map: TreeMap<u64, u32>) {
    let tree_map2 = tree_map.clone();
    assert(tree_map2@ =~= tree_map@);
}

We can do the same for any type where clone guarantees spec-equality. Here’s another example with a user-defined type.

struct IntWrapper {
    pub int_value: u32,
}

impl Clone for IntWrapper {
    fn clone(&self) -> (s: Self)
        ensures s == *self
    {
        IntWrapper { int_value: self.int_value }
    }
}

fn test_clone_int_wrapper(tree_map: TreeMap<u64, IntWrapper>) {
    let tree_map2 = tree_map.clone();
    assert(tree_map2@ =~= tree_map@);
}

This works because of the postcondition on IntWrapper::clone, that is, ensures *s == self. If you’re new to this style, it might seem initially surprising that IntWrapper::clone has any effect on the verification of test_clone_int_wrapper, since it doesn’t directly call IntWrapper::clone. In this case, the postcondition is referenced indirectly via TreeMap<u64, IntWrapper>:clone.

Let’s do one more example, this time with a less precise clone function.

struct WeirdInt {
    pub int_value: u32,
    pub other: u32,
}

impl Clone for WeirdInt {
    fn clone(&self) -> (s: Self)
        ensures s.int_value == self.int_value
    {
        WeirdInt { int_value: self.int_value, other: 0 }
    }
}

fn test_clone_weird_int(tree_map: TreeMap<u64, WeirdInt>) {
    let tree_map2 = tree_map.clone();

    // assert(tree_map2@ =~= tree_map@); // this would fail

    assert(tree_map2@.dom() == tree_map@.dom());
    assert(forall |k| tree_map@.dom().contains(k) ==>
        tree_map2@[k].int_value == tree_map@[k].int_value);
}

This example is a bit pathological; our struct, WeirdInt, has an extra field that doesn’t get cloned. You could imagine real-life scenarios that have this property (for example, if every struct needs to have a unique identifier). Anyway, the postcondition of WeirdInt::clone doesn’t say both objects are equal, only that the int_value fields are equal. This postcondition can then be inferred for each value in the map, as shown.

Implementing TreeMap::<K, V>::Clone.

As usual, we write the implementation as a recursive function.

It’s not necessary to implement Node::Clone; one could instead just implement a normal recursive function as a helper for TreeMap::Clone; but it’s more Rust-idiomatic to do it this way. This lets us call Option<Node<K, V>>::Clone in the implementation of TreeMap::clone (the spec for Option::clone is provided by vstd). However, you can see that there are a few ‘gotchas’ that need to be worked around.

impl<K: Copy + TotalOrdered, V: Clone> Clone for Node<K, V> {
    fn clone(&self) -> (res: Self)
        ensures
            self.well_formed() ==> res.well_formed(),
            self.as_map().dom() =~= res.as_map().dom(),
            forall |key| #[trigger] res.as_map().dom().contains(key) ==>
                call_ensures(V::clone, (&self.as_map()[key],), res.as_map()[key])
    {
        // TODO(fixme): Assigning V::clone to a variable is a hack needed to work around
        // this issue: https://github.com/verus-lang/verus/issues/1348
        let v_clone = V::clone;

        let res = Node {
            key: self.key,
            value: v_clone(&self.value),
            // Ordinarily, we would use Option<Node>::clone rather than inlining
            // the case statement here; we write it this way to work around
            // this issue: https://github.com/verus-lang/verus/issues/1346
            left: (match &self.left {
                Some(node) => Some(Box::new((&**node).clone())),
                None => None,
            }),
            right: (match &self.right {
                Some(node) => Some(Box::new((&**node).clone())),
                None => None,
            }),
        };

        proof {
            assert(Node::optional_as_map(res.left).dom() =~= 
                Node::optional_as_map(self.left).dom());
            assert(Node::optional_as_map(res.right).dom() =~= 
                Node::optional_as_map(self.right).dom());
        }

        return res;
    }
}

impl<K: Copy + TotalOrdered, V: Clone> Clone for TreeMap<K, V> {
    fn clone(&self) -> (res: Self)
        ensures self@.dom() =~= res@.dom(),
            forall |key| #[trigger] res@.dom().contains(key) ==>
                call_ensures(V::clone, (&self@[key],), res@[key])
    {
        proof {
            use_type_invariant(self);
        }

        TreeMap {
            // This calls Option<Node<K, V>>::Clone
            root: self.root.clone(),
        }
    }
}

Full source

The full source for this example can be found here.