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 Clone, so it is not necessarily true that a clone() call will return a value that is spec-equal to its input.

With this in mind, to simplify this example, 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) ==>
                cloned::<V>(self@[key], res@[key])
    {
        ...
    }
}

We explain the details of this signature below.

Dealing with K::clone

In order to clone all the keys, we need K::clone to respect the ordering of elements; otherwise during a clone operation, we’d need to re-sort all the keys so that the resulting tree would be valid. However, it’s unlikely that is desirable behavior. If K::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 a value 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. 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”. This predicate is a mouthful, so vstd provides a helper function: cloned::<V>(self@[key], res@[key])

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.

pub 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) ==>
                cloned::<V>(self.as_map()[key], res.as_map()[key])
    {
        let res = Node {
            key: self.key,
            value: self.value.clone(),
            // 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) ==>
                cloned::<V>(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.