Abstract dataypes allow us to hide the representation of data behind interfaces. To pass information across interfaces, however, we still need a sufficiently rich class of concrete datatypes whose representation is not hidden. This is particularly relevant when communicating across a network. In this case, we can’t efficiently pass a reference to an abstract object – we have to represent the contents of the object in a concrete way.

To facilitate exchange of data across interfaces, Ivy provides a set of standard concrete datatypes.

Structs

A struct is an aggregate of named components. Structs are declared like this:

type point = struct {
    x : coord,
    y : coord
}

This defines a type point whose elements are structures consisting of members x and y of type coord. Two destructor functions x and y are defined that respectively extract the x and y coordinates of the point. Thus, if p is a point, then x(p) is the x coordinate of p and y(p) is the y coordinate.

The members of a structure can be assigned. For example, to assign 0 to the x coordinate of point p, we would write:

x(p) := 0

This mutates not the destructor function x, which is immutable, but rather the value of p. The value of y(p) remains unchanged by this assignment.

Members of a struct can also be functions and relations. For example:

type point = struct {
    coords(X:dimension) : nat
}

Our points now have one coordinate value for each dimension defined by some arbitrary type dimension. Suppose we declare:

type dimension = {x,y,z}

We could then refer to the x coordinate of a point p as coord(p,x), and we could assign 0 to it like this:

coord(p,x) := 0

This would be written in many programming languages as something like p.coord[x] = 0. The type dimension need not be an enumerated type, however. It could be an uninterpreted type, or an interpreted type (for example, an integer type) or even another structure type.

Structs can also contain structs. For example:

type line = {
    begin : point,
    end : point
}

To set the x coordinate of the begin point of a line l, we could write:

coord(begin(l),x) := 0

This mutates l and not the immutable destructor functions coord and begin.

Arrays

An array type represents a map from an interval [0,end) of some type (the index type) to some other type (that value type). Usually the index type is interpreted as int.

Here is an example of a simple program that tabulates the function f(X) = X * X from 0 to max-1:

#lang ivy1.7

include collections

type t

instance arr : array(t,t)

action tabulate(max : t) returns (res:arr.t) {
    local i:index {
        i := 0;
        res := arr.create(max,0);
        while i < max {
            res := arr.set(res,i,i*i);
            i := i + 1
        }
    }
}

The array module provides an action create that returns an array mapping values in the range [0,end) to some given value (in the example, 0). The set action takes a array, an index and a value. It sets the value of the array at the given index to the value and returns the resulting array. Keep in mind, because of IVy’s call-by-value convention, an action can’t have a side effect on its input parameters. The set action returns a copy of its input array with one value changed.

This program seems inefficient, since it copies the array each time it modifies one element. In fact it isn’t. The compiler recognizes that the array can be modified “in place”. Lets run this program to see what we get. First, we have to give a concrete interpretation for type t and define an extract:

interpret t -> int
export tabulate
extract iso_impl = tabulate, arr

Compile and run:

$ make array1
ivy_to_cpp target=repl isolate=iso_impl array1.ivy
g++ -g -o array1 array1.cpp
$ ./array1
> tabulate(4)
[0,1,4,9]

Here is a part of the interface definition for array types, from the collections module in the standard library:

module array(domain,range) = {

    type t

    action create(s:domain,y:range) returns (a:t)
    action set(a:t,x:domain,y:range) returns (a:t)
    action get(a:t,x:domain) returns (y:range) 
    action size(a:t) returns (s:domain)
    action resize(a:t,s:domain,v:range) returns (a:t)

    function end(A:t) : domain
    function value(A:t,X:domain) : range

    object spec = {
        before create {
            assert 0 <= s
        }
        after create {
            assert end(a) = s & value(a,X) = y
        }
        before set {
            assert 0 <= x & x < end(a)
        }                        
        after set {
            assert value(a,X) = y if X = x else value(old a,X)
        }
        before get {
            assert 0 <= x & x < end(a)
        }
        after get {
            assert value(a,x) = y
        }
        after size {
            assert s = end(a)
        }
        after resize {
            assert end(a) = s;
            assert 0 <= X & X < end(old a) -> value(a,X) = value(old a,X);
            assert end(old a) <= X & X < s -> value(a,X) = v
        }
        ...
    }
    ...
}

In addition to create and set, array types provide an action get to get the value at a given index, size to get the end index, and resize to change the end index. The resize action takes an addition parameter that gives the value of the new elements in case the size is increased.

Notice that in the set method, both the input and the output parameter are called a. This indicates to the compiler that we intend to modify the array a in place if possible. When writing the after specification for set, we need a way to refer to the input value of a. For this, we use old a. We can refer to the original value of any component that is mutated by an action using old. You can also see the use of old in the specification of resize. The expression old x always referes to the value of symbol x at the time the action was called.

In the next section, we’ll see a more interesting application of arrays.

Representation functions

Often, we use concrete dataypes as representations of abstract values. This gives us an efficient way of passing these values across interfaces.

As an example, consider using an array as a representation of a set. Here is the start of a module that accomplishes that:

#lang ivy1.7
module set(elem) = {

    type this
    alias t = this

    relation contains(X:t,Y:elem)
    action emptyset returns(s:t)
    action add(s:t,e:elem) returns (s:t)
    ...    

Notice something new here: type this. This declares a type with the same name as the object we are declaring (which won’t be known until we instantiate this module). For convenience, we create an alias t for this type. This interface of our abstact set type contains a relation and two actions.

The relation contains acts as a representation function. This tells us what abstract set a given value of type set represents. The representation function allows us write specifications using the abstract value that is represented. This means we can can pass around values of type set as if they were actually abstract sets instead of arrays.

Now let’s specify the semantics of our two set operations in terms of the contains relation.

module set(elem) = {
    ...

    object spec = {
        after emptyset {
            assert ~contains(s,X)
        }
        after add {
            assert contains(s,X) <-> (contains(old s,X) | X = e)
        }
    }

The action emptyset returns a representation of the empty set, while add returns set s with element e added. Notice that the set parameter of add is both input and output. This indiciates to the compiler that we wish to avoid copying if possible. In most cases, this will allowed the compiled code of add to modify the set in place.

Let’s have a hack at implementing these operations. The implementation usually provides a concrete data representation, a definition for each function or relation in the interface, and code for each action. Typically it instantiates some modules to provide the concrete representation. Here’s one way we could implement set:

include collections
include order

module set(index,elem) = {
    ...

    instance index : unbounded_sequence
    instance arr : array(index.t,elem)
    destructor repr(X:t) : arr
    
    definition contains(X:t,y:elem) = exists Z. 0 <= Z & Z < repr(X).end & repr(X).value(Z) = y
    
implement emptyset {
    repr(s) := arr.create(0,0)
}

implement add {
    if ~contains(s,e) {
            repr(s) := arr.resize(repr(s),index.next(arr.end(repr(s))),e)
    }
    }

isolate iso = this
}

This implementation uses an unbounded array as a representation. The concrete type is usually provide by giving the abstract type a private destructor, in this case the function repr from type t to the array type. Giving the destructor in this way is equivalent to writing:

type t = struct {
    repr : arr
}

except the that field repr, being a component of the implementation, is not visible to users of set (it’s similar to a private member in C++). We use the function repr to access the internal representation of a set.

Next, we give the definition of contains in terms of repr. This definition is also private. We say that contains(x,y) is true if a given elem y can be found somewhere in the array representing set x.

The implementation of emptyset returns an empty array. To add an element to a set, we test whether the element is already present. If not, we resize the array to make it one value larger, where the added value is e, the new element.

Finally, we create an isolate containing our object so it will be verified separately.

Notice that in the implementation of add, we evaluate the predicate contains. IVy recognizes that contains is executable because the quantifier in the definition of contains is bounded. This means it can compile the quantifier into a loop from 0 to arr.end(X). If you try to compile an unbounded quantifier into executable code, IVy will complain.

Also notice that instead of arr.end(s) + 1, we wrote index.next(arr.end(s)). That is, we are treating index as an abstract datatype, assuming only that it provides an order < and an action next. From a software engineering point of view, this is probably useless abstraction. However, from a verification point of view, it is useful – it allows us to verify set without using the theory or arithmetic.

The implementation is moderately efficient. That is, if the caller of add writes:

s := set.add(s,e)

the compiler will recognize that the array s can be modified in place. On the other hand, evaluating contains will still be linear time in the array size, since it loops over the array. This approach is only practical for small sets.

To try out our sets, we instantiate a set type:

type elem
instance s : set(elem)

We export our two actions:

export s.emptyset
export s.add

Then we verify:

$ivy_check arrayset.ivy
ivy_check arrayset.ivy 
Checking isolate s.impl.index.iso...
trying ext:s.impl.index.next...
checking consecution...
Checking isolate s.iso...
trying ext:s.add...
checking consecution...
trying ext:s.emptyset...
checking consecution...
OK

Notice that even though the object index was instantiated from the standard library, IVy still verified it. Generally speaking, even trusted modules have properties that need to be verified when instantiated in a particular environment.

Representation invariants

Now let’s try adding an action to our set module that removes an element:

 module set(index,elem) = {
     ...
     action remove(s:t,e:elem) returns (s:t)

     object spec = {
         ...
         after remove {
             assert contains(s,X) <-> (contains(old s,X) & X ~= e);
         }
    }

    object impl = {
        ...
        implement remove {
            if some (i:index.t) 0 <= i & i < repr(s).end & repr(s).value(i) = e {
                var last := repr(s).end.prev;
                repr(s) := repr(s).set(i,repr(s).get(last));
                repr(s) := repr(s).resize(last,0)
            }
        }
    }
}

This implementation of remove scans the array for some index i whose value is e. If such an i exists, the value e is removed by replacing it with the last value in the array and then resizing the array to make it one element smaller.

Unfortunately, this implementation doesn’t work: if the input array contains two copies of the element e, one copy will remain. One solution to this problem is to use a representation invariant. This is a predicate a predicate that must be true of a value for it to be a valid representation. The representation invariant is assumed to be true of input values and must hold of output values.

In the case of our sets, the representation invariant is that no value occurs twice in the array. It is part of the interface, and like contains, its definition is private:

    relation valid(X:t)

We have to specify our interface to make the appropriate assumptions and guarantees:

object spec = {
    after emptyset {
        assert ~contains(s,X)
    }
    before add {
        assert valid(s)
    }
    after add {
        assert contains(s,X) <-> (contains(old s,X) | X = e);
        assert valid(s)
    }
    before remove {
        assert valid(s)
    }
    after remove {
        assert contains(s,X) <-> (contains(old s,X) & X ~= e);
        assert valid(s)
    }
}

We give the definition of valid in the implementation:

object impl = {
    ...
    definition valid(X:t) =
        forall Y,Z. (0 <= Y & Y < repr(X).end & 0 <= Z & Z < repr(X).end
                      & repr(X).value(Y) = repr(X).value(Z) -> Y = Z)
}

Now we can verify that our implementation of remove works (try verifying arrayset2.ivy). There is a disadvantage to this approach, however. Users of our set module now have to keep track of the invariant that set values are valid. This could lead to many “boilerplate” invariant conjectures. One day, IVy will solve this problem using predicate subtypes.

Array and loops

For now, it might be best to just implement remove in a way that doesn’t rely on a representation invariant. We can do this using a while loop. Here is the implementation we have in mind:

action remove(s:t,e:elem) returns (res:t)

object impl = {
    ...

    implement remove {
        local i:index.t, end:index.t {
            i := 0;
            res := emptyset;
            end := arr.end(s);
            while i < end
            {
                local f:elem {
                    f := arr.get(s,i);
                    if  f ~= e {
                        res := add(res,f)
                    }
                };
                i := index.next(i)
            }
        }
    }
}

That is, we scan the input array s. When we encounter a value not equal to the output set res. This is easy enough to write, but Ivy can’t prove it correct because of the loop. We’re going to need an inductive invariant.

Before diving in to the proof, let’s consider the general schema of inductive proofs of loops. We think of the loop as computing an approximation to a desired function that approaches the correct result with each iteration. We’ll call this function step(i), where i is the loop index. Suppose we want our loop to compute the “or” of the bits in an array a, that is:

 function or = exists X. 0 <= X & X < arr.end(a) & arr.value(a,X)

Then our step function would be:

 function step(i) = exists X. 0 <= X & X < i & arr.value(a,X)

That is, our approximation is the “or” of all the bits up to (but not including) the index i.

Now we need to give an inductive characterization of step. That is, we need to know how to compute the value of step at the next iteration. It looks like this:

property 0 <= I & index.succ(I,J) -> step(J) = (step(I) | arr.value(a,I))

That is, to compute approximation for the successor of index I, we “or” step(I) with the bit in the array at index I. Ivy can prove this property from the definition of step. It just unfolds the definition of step for I and J and uses its EPR decision procedure. Notice we use the successor relation succ provided by the index type to represent the fact that J is next after I. This is because we can’t call the action next in a property of function definition.

Now we need to know that when we get to the and of the array, we have the desired result. Here is how we write this condition:

property I = arr.end(a) -> step(I) = or

Again, Ivy can easily prove this from the definitions of step and or. If you squint at these two properties a bit, you’ll see that they are very close to a logic program for computing or (in fact, we could easily recast them in the form of Horn clauses). A logic programming system could execute them directly to compute our result. We have have in mind, however, to do the computation using a loop:

i := 0;
res := false;
while i < arr.end(a)
    invariant 0 <= i & i <= arr.end(a)
    invariant res = step(i)
{
    res := res | arr.value(a,i);
    i := index.next(i)
} 
assert res = or

Notice the two invariants decorating the loop. IVy can prove that that they are inductive and that the assertion is true. This can be done using only our two properties, without reference to the actual definition definition of step. This is the general approach for writing a loop in IVy: first characterize the loop inductively, then write the loop with two invariants as above.

Now let’s get back to the remove method. We start with the step function:

function remove_step (s:t,e:elem,i:index.t,y:elem)
        = (exists Z. 0 <= Z & Z < i & arr.value(s,Z) = y) & y ~= e

This is an approximation of the representation function contains. Here, s is the input set, e is the element to remove, i is the loop index and y is an element to test for membership. The function yields true if y is not the removed element e and if it occurs before index i in the input set. In other words, this function gives us the output set accumulated up to index i.

Now we need an inductive charaterization. Basically, we add an element of the array to the output set if it is not the removed element:

property I >= 0 & index.succ(I,J) ->
    (remove_step(X,E,J,Y) <-> (remove_step(X,E,I,Y) | arr.value(X,I) = Y & Y ~= E))

The exit condition tells us when we have completed the computation:

property I = arr.end(X) ->
    (remove_step(X,E,I,Y) <-> (contains(X,Y) & Y~=E))

That is, when we reach the end of the array, we have accumulated all the elements of the input set except e.

Now here’s the remove action, decorated with invariants:

implement remove {
    local i:index.t, end:index.t {
        i := 0;
        res := arr.create(0,0);
        end := arr.end(s);
        while i < end
            invariant 0 <= i & i <= end
            invariant contains(res,Y) = remove_step(s,e,i,Y)
        {
            local f:elem {
                f := arr.get(s,i);
                if  f ~= e {
                    res := add(res,f)
                }
            };
            i := index.next(i)
        }
    }
}

Notice that the invariant is universally quantified on Y, the test element. The invariant says that our loop computes exactly what our inductive characterization computes. Ivy can easily verify that this version of remove satisfies its specification.

Of course, this might seem like a lot of work for around ten lines of code. This style of proof has a big advantage, though, from the point of view of automating the proof. That is, the places in the Horn clauses where definitions need to be unfolded are clear. We don’t need fragile quantifier instantiation heuristics to make the proof go through.

In general, though, it’s best to avoid this kind of painstaking construction of loops by using higher-level operations on containers.