The Wolf, Goat and Cabbage Exchange
Our last article introduced the notion of Machine Reasonable APIs and Regulations. Here, we give an example of such an API and regulation in the context of the FIX protocol. In order to demonstrate what we mean, we encode a fictional exchange which accepts FIX messages and analyse its functionality using the Imandra Protocol Language.
In our exchange, we want to be able to trade with three objects — a wolf, a cabbage and a goat. Initially, the exchange has all three. Let us assume it is a regulatory requirement that no client can be in ownership of all three objects.
The exchange implements a trading logic which attempts to provide functionality to trade in these objects while adhering to the regulatory requirement. In order to trade a client can
- send a message asking to pick up or drop an object belonging to the client;
- explicitly do nothing and wait for an action from the exchange;
- send an object to the exchange.
The exchange performs fill actions, which can
- pick up or drop an object belonging to the exchange;
- explicitly do nothing and wait for another message;
- send an object to the client.
The exchange explicitly forbids the following pairs of objects from existing alone either at the exchange when it is the client’s turn to send a message, or with a client when it is the exchange’s turn to send a message:
Note that it is valid for all three to exist together at the exchange. The exchange thinks that this constraint is enough to satisfy the regulatory requirement and has conducted some testing with hundreds of thousands of test cases, none of which break the regulatory requirement, which gives some confidence that the requirement will not be broken.
Let us now describe this venue using the Imandra Protocol Language (IPL). We begin by defining the types of messages that the exchange accepts and sends out. We are notionally importing the FIX 4.4 dictionary here, but we want to add our own special fields and associated enumeration types, which we can do using the custom functionality in IPL:
What this means is that the exchange accepts a
NewOrderSingle message with an optional field
obj with given field tag
“2001”, and a field
act with given field tag
“2002”. The exchange also sends out an
ExecutionReport message with the same fields. The acceptable values are given by the associated enumeration types.
Now we have defined a message interface for the exchange we can consider adding some validation requirements, which dictate the acceptable behaviour of the fields of the incoming messages. In order to do this let us first introduce a new local enumeration type named
location, and the notion of a
state — a ubiquitous and canonical notion in any IPL model:
state records the location of the objects, and where the objects can be picked up or dropped off — represented by the
We refer to messages as “events”. We can add a constrained event called an
action, which we name
fill that records any objects transferred from the exchange to the client. We can also add validation statements to events which ensure specified properties are true when receiving an event. These validation statements ensure that should an object be eaten an event is not accepted, and that should the event be to simply move the
transit element then there should be no object contained therein. We also ensure that the
transit element is at the correct location to pick or drop at the client.
Now we can write logic which acts upon the
state when a message or an action is received:
As this full model is machine reasonable we can now set about analysing the possible states. We can try to determine if the model satisfies the regulation by writing a verification goal. In this case, because this is a demonstration example, we tailor the verification goal to the problem, but in general verification goals can be automatically generated.
In IPL we can define the machine reasonable regulation, by writing for example:
!(state.cabbage = Client &&
state.goat = Client &&
state.wolf = Client)
then use Imandra to verify whether this regulation holds. In this case, Imandra quickly discovers that the regulation is broken giving back an example FIX log of
This log can be validated by pasting the contents here for example, and corresponds to the following sequence of messages and actions:
The regulatory requirement of this problem — that no client should be in the possession of all three objects — is only broken at message sequence lengths of 18 or greater. The number of possible paths that can be found with message sequences of length 18 is 3,200,668. The total number of paths at less than or equal to 18 is 5,816,112. Out of all of these possible sequences of events, there are only 2 sequences which break the regulatory requirement.
Even with a bounded message sequence length for testing, and tens of thousands of tests, the probability that one of the 2 sequences is found via classical testing techniques is extremely low. This is why formal analysis of the model is so vital. Imandra can not only find the sequence where the regulatory requirement is broken but can also perform a region decomposition which provides a static analysis of all the feasible paths through the model. For example below is a graph showing the distinct paths through the model sufficient to cover all possible scenarios in this model — please click on the image to see the full decomposition graph.
This decomposition of the state-space is automatically produced by Imandra, and produces a set of possible regions which we can explore and use both in formal verification and in the automatic creation of high-coverage test suites. Below is an image of the generated interactive region explorer — soon publicly available for browsing!
We’re very excited to bring the rigour of machine reasonable APIs and regulations to finance, significantly upping the game when it comes to algorithm governance and transparency.
Join us at www.imandra.ai to learn more!