A simple and effective way to reduce the complexity of reasoning about a system is to use abstract datatypes. An abstract datatype uses a service specification to hide the implementation of the type and provide only properties of the type that we require.

When programming, we often use types provided by a programming language, such as integers or lists, without much concern for whether we actually require the properties of these types for our application. For example, we might use the integer type when all we require is a totally ordered range of values, or a list type when all we need is a representation of a set.

Abstract datatypes can provide just the properties we need for a given application. For example, suppose we need a datatype to represent clock values in a protocol. The protocol doesn’t care about the quantitative values of the clocks. It only needs to be able to compare the values. Here is a possible specification of this type in IVy:

#lang ivy1.7

object clock = {
    type t
    relation (X:t < Y:t)
    
    object spec = {
        property [transitivity] X:t < Y & Y < Z -> X < Z
        property [antisymmetry] ~(X:t < Y & Y < X)
    }
}

We begin with the interface. Our datatype clock provides a type clock.t equipped with a binary relation <. The we give the specification of this interface. The specification is a sub-object containing two properties. The spec says that the type clock.t respects the axioms of a partial order. We can rely on the declared properties of clock.t in proving correctness of our protocol.

Of course, our new datatype isn’t very useful, since it provides no actual operations. Suppose, for example, that our protocol requires an operation incr that can add some amount to a clock value. We don’t care how much is added, so long as the clock value increases. Let’s add this operation to the interface and specify it:

object clock = {
    type t
    relation (X:t < Y:t)
    action incr(inp:t) returns (out:t)

    object spec = {
        property [transitivity] X:t < Y & Y < Z -> X < Z
        property [antisymmetry] ~(X:t < Y & Y < X)

        after incr {
            assert inp < out
        }
    }
}

We’ve added an action incr that takes a clock value and returns a clock value. In addition, we’ve added a monitor to object spec. It requires that the output value y be greater than the input value x. Notice the new keyword after. It specifies that a given action be inserted after the execution of action incr. We need an after specification to make statements about the output values of actions.

Using an abstract datatype

As an example of using an abstract datatype, let’s make our ping-pong game a little more interesting by attaching a clock value to the ball. Here is the new interface definition:

object intf = {
    action ping(x:clock.t)
    action pong(x:clock.t)
}

To the specification, we add the requirement that the ball’s clock value must always increase:

type side_t = {left,right}

object spec = {
    individual side : side_t
    individual time : clock.t
    after init {
        side := left;
        time = 0
    }

    before intf.ping {
        assert side = left & time < x;
        side := right;
        time := x
    }

    before intf.pong {
        assert side = right & time < x;
        side := left;
        time := x
    }
}

Now, using our abstract datatype clock, we can implement the left player like this:

object left_player = {
    individual ball : bool
    individual time : clock.t
    after init {
        ball := true;
        time := 0
    }

    action hit = {
        if ball {
            call intf.ping(clock.incr(time));
            ball := false
        }
    }

    implement intf.pong {
        ball := true;
        time := x
    }

    conjecture ball -> (spec.side = left & spec.time <= time)
}

Notice that when we send the ball using intf.ping, we increment the clock value using our incr operation. The right player is similar:

object right_player = {
    individual ball : bool
    individual time : clock.t
    after init {
        ball := false
    }

    action hit = {
        if ball {
            call intf.pong(clock.incr(time));
            ball := false
        }
    }

    implement intf.ping {
        ball := true;
        time := x
    }

    conjecture ball -> (spec.side = right & spec.time <= time)
}

As before, we export some actions to the environment, and set up our assume-guarantee proof:

export left_player.hit
export right_player.hit

isolate iso_l = left_player with spec, clock
isolate iso_r = right_player with spec, clock

Notice that in our isolates, we use the clock datatype. Without the specification of clock, we couldn’t verify the interface specifications in spec. Now let’s try to use IVy to verify this program:

$ ivy_check coverage=false pingpongclock.ivy
...
OK

The command line option coverage=false tells IVy that we know some assertions are not checked (that is, the ones in clock). What we have proved is that the protocol only depends on the specifications we provided for clock: that it is a partial order and that incr is increasing.

As an experiment, see what happens when you remove the transitivity property from clock (hint: use the command line option diagnose=true to see the counterexample) . What happens when you remove antisymmetry?

Implementing an abstract datatype

To make a program we can actually run, we need to provide an implementation of the abstract datatype clock. We will do this using IVy’s built-in type int that represents the integers. Here is the implementation:

object clock = {
    ...

    object impl = {
        interpret clock.t -> int

        implement incr {
            out := in + 1
        }
    }
}

The interpret declaration tells IVy that the type clock.t should be interpreted as the integers. This also gives an interpretation to certain symbols in the signature of the integer theory, for example +, <, 0 and 1. With this interpretation, we can write an implementation of clock.incr that simply adds one to its argument.

Now let’s apply assume-guarantee reasoning to our abstract datatype:

isolate iso_ci = clock

First, let’s see what we’re actually verifying:

$ ivy_show isolate=iso_ci pingpongclock.ivy

type clock.t
type side_t = {left,right}
relation (V0:clock.t < V1:clock.t)

property [clock.transitivity] (X:clock.t < Y:clock.t & Y:clock.t < Z:clock.t) -> X:clock.t < Z:clock.t
property [clock.antisymmetry] ~(X:clock.t < Y:clock.t & Y:clock.t < X:clock.t)
interp clock.t -> int

action ext:clock.incr(inp:clock.t) returns(out:clock.t) = {
    out := inp + 1;
    assert inp < out
}

Notice that the after specification for clock.incr has been inserted at the end of the implemention and is a guarantee for object clock. In general, after specifications for actions are guarantees for the objects that define them.

Now let’s verify this isolate using IVy:

$ ivy_check isolate=iso_ci pingpongclock.ivy

Isolate iso_ci:

The following properties are to be checked:
    pingpongclock.ivy: line 7: clock.transitivity ... PASS
    pingpongclock.ivy: line 8: clock.antisymmetry ... PASS

...

The following program assertions are treated as guarantees:
    in action clock.incr when called from the environment:
        pingpongclock.ivy: line 14: guarantee ... PASS

...
OK

IVy used the built-in theory of integer arithmetic of the Z3 theorem prover to prove the assertion, and also to prove the two properties of clocks. As an experiment, try taking out the interpret declaration to see what happens.

Now that we have a full implementation, we can verify the full program:

$ ivy_check pingpongclock.ivy
...
OK

Is this useful?

Specifying and verifying an abstract datatype might seem to be a lot of work just to avoid making unnecesary assumptions about the integers. However, it is worth observing the effect of this approach on the proof. When verifying the protocol, IVy didn’t have to make use of the integer theory. It only used the properties that we provided. This will be a significant advantage when doing proofs about systems of many processes, or other systems that require quantifiers in the proofs. When we mix quantifiers, relations and integers, the verification problems become undecidable. This makes the theorem prover unreliable. Abstract datatypes give us a way to segregate theory reasoning into isolates that use do not require quantifiers, or generally speaking fall into decidable fragments. In this way, we obtain more reliable performance from the prover, and also make sure that the prover can generate correct counterexamples when we make a mistake.