Our server needs to keep track of ranges of keys that are delegated to other servers. We will call this the delegation map. In the abstract, the delegation map is just a map from keys to server id’s. Here’s its specification as an abstract datatype:

module delegation_map(key,id) = {

    action set(lo:key.iter.t,hi:key.iter.t,dst:id)
    action get(k:key.t) returns (val:id)

    # The delegation map is a relation, since as a function it might
    # not be stratified.

    relation map(K:key.t, X:id)
    after init {
        map(K,X) := X = 0
    }

    object spec = {
        before set {
            map(K,X) := (X = dst) & key.iter.between(lo,K,hi)
                        | map(K,X) & ~key.iter.between(lo,K,hi)
        }
        after get {
            assert map(k,val)
        }
    }

    conjecture map(K,V) & map(K,W) -> V = W
    ...

The delegation map provides an action set that maps a range of keys [lo,hi) to a given id dst. Notice that lo and hi are key iterators, so hi can be end, meaning all keys from lo up are mapped. The get action returns the destination id for a given ‘key’.

The abstract state is a relation map between keys and id’s. Initially, all keys map to the default server with if 0. By making map a relation rather than a function, we avoid creating a function cycles in case the client of the delegation map has a finction from id’s to keys.

THe specification of set says that all keys between lo and hi are mapped to dst and all other keys keep their value. The get action just returns an id associated to a given key. Of course, we won’t be able to actually prove this post-condition unless map is actually total (has at least one id for each key). As it turns out, though, we never have to explicitly state this.

Finally, delegation_map provides an invariant that map is injective. This is an object invariant that is implied by the spec, but we have to provide it as a conjecture to be proved, since IVy doesn’t have object invariants yet.

Implementation

We implement the delegation map with an ordered_map from keys to id’s. If k1,k2 is a successive pair of keys in thhis map, all the keys in the range [k1,k2) are delegated to the id valu8e assicated with k1. This gives us an efficient way to represent a map over a large range of keys.

Here is the implementation:

    object impl = {

        instance imap : ordered_map(key,id)

        after init {
            call imap.set(0,0)
        }

        implement set(lo:key.iter.t,hi:key.iter.t,dst:id)  {
            if lo < hi {
                if ~key.iter.is_end(hi) {
                    local nid:id {
                        nid := imap.get(key.iter.val(imap.glb(hi)));
                        call imap.set(key.iter.val(hi),nid)
                    }
                };
                call imap.erase(lo,hi);
                call imap.set(key.iter.val(lo),dst)
            }
        }

        implement get(k:key.t) returns (val:id)  {
            val := imap.get(key.iter.val(imap.glb(key.iter.create(k))))
        }
    ...
     }

The implmentation map is called imap. Notice the use of after init to set value of key 0 to 0. Since 0 is the minimal key, this means that initially all keys are delegated to the default server 0, as in the abstract state.

The implmenation of get is quite simple. We call imap to get the greates lower bound (glb) of the requested key. This is as iterator to the greates key in the map that is less than or equal to k. This action has a precondition that there exists some key in the map less than or equal to key. This is needed because there is no iterator value reprenenting “before the begining”. Fortunately, this precondition is met becuase key 0 is always in the map. We return the id associated the the glb.

The set action is a little more complicated. First, we have to check that the given interval actually contains some keys (lo < hi). If so, we will set the value of lo to point to dst. We must also clear out all the keys in the range [lo,hi) so that the whole ranges is covered by lo. In addition though, we must be careful no to disturb the values above hi. This means that if hi is not end, we have to map hi to its current value, which we obtain by calling get.

Proof

To prove the the implementation of get satisfies its postcondition, we need to know that if the glb if key L is K, then key K has the correct value for L according to the abstract map. To state this invariant directly would invold a quantifier alternation, since the definition of glb as a function would look something like this:

definition glb(L) = some K. K <= L & contains(K) 
                            & ~exists M. K < M & M <= L & contains(M)

Fortunately, the ordered_map module has an alternative specification in terms of a relation gap on iterators. The predicate gap(X,Y) is true when there are no keys in the map in the open interval (X,Y). Both specifications are equivalent in terms of the input and output of actions, but they are useful for different purposes.

The gap specification allows us to state our invariant as follows:

conjecture imap.maps(key.iter.val(I),V) & imap.gap(I,J)
                              & key.iter.between(I,K,J) -> map(K,V)

That is, if a key K lies in the gap between I and J, and I maps to V, then in the abstract map I maps to V. We need one more invariant to make sure all keys are mapped:

conjecture imap.contains(0)

Because the map always contains key 0, all keys have a glb. With these two invariants, IVy can prove that the implementation satisfies its specification.

Reasoning with alternate specifications

We’ll do that shortly. First, though, we should understand the limitations of reasoning with different specifications of the same interface. Here is how IVy defines gap:

function gap(k:key.iter.t, m:key.iter.t) =
          forall L. ~(key.iter.ahead(L,k) & key.iter.done(L,m) & contains(L))

This definition gives the relation between the contains specification state and the gap specification state. It should be fairly easy to convince yourself that the keys in the map (i.e., contains) can in turn be derived from the gaps, apart from the annoying exception of 0. The difficulty is that the relation between contains and gaps can only be expressed with a quantifier alternation.

The upshot if this is that, as long we we write our invariant only using the gaps specification or only using the contains specification, IVy can decide reliably whether our invariant is inductive. If we try mixing the two, we might get a counterexample in which gaps and contains are inconsistent. There is a small proviso to this, however: we can always write contains(0) since this is independent of gaps.

Using alternate specifications can be a very useful tactic for keeping the proof of invariants within a decidable fragment. It is sometimes a bit tricky to come up with an alternate encoding that on the one hand can be specified in the logic and on the other hand is useful for writing invariants. Some examples are provided in the standard libarary, however, that are generically useful.

Checking the proof

Let’s test the delegation_map module by instantiating it:

#lang ivy1.6

include key
include delmap

type id

instance dmap : delegation_map(key,id)

export dmap.set
export dmap.get

object impl = {
    interpret id -> bv[1]
}

isolate iso_dmap = dmap with key
extract iso_impl = dmap, key, impl

We need our key module. In addition, we need a type of process id’s.

$ ivy_check diagnose=true delmap_test.ivy 
Checking isolate iso_dmap...
trying ext:dmap.get...
checking consecution...
trying ext:dmap.set...
checking consecution...
Checking isolate key.iso...
trying ext:key.iter.create...
checking consecution...
trying ext:key.iter.end...
checking consecution...
OK

As an excersize, you might try changin or removing some lines in the implementation to see what breaks, or try compiling this module to a REPL and running it.