Gentle Introduction to ImandraX

ImandraX is the latest version of the Imandra automated reasoning engine. Its input language is Imandra Modeling Language (IML), a pure subset of OCaml (www.ocaml.org) with some added directives to interact with the engine (e.g. verify command). At the same time, IML models can be used as ordinary OCaml programs. At Imandra, we’ve created mechanized formal semantics for this subset of OCaml which ImandraX uses under-the-hood to automatically translate IML models into mathematics, allowing it to use myriad of techniques to analyze them. CodeLogician uses ImandraX to construct the models and reason about them, so understanding ImandraX even at a high-level is very useful to effectively using CodeLogician.

Our documentation page contains many examples, but for our purposes - we’ll do a high-level overview of writing models in ImandraX and look at the two major features that CodeLogician relies upon: (dis)proving verification goals and performing model state-space region decomposition. This section makes no assumptions about your background in formal methods, automated reasoning but that you have written some code before.

If you want to use ImandraX directly, you should go through the installation details listed in ImandraX docs. Your Imandra Universe API key will be required (there’s a free tier) - you can get one at the Universe page.

Writing formal models

When we talk about models, we simply refer to programs written in Imandra Modeling Language, a which is effectively a “pure” subset (no side effects) of the open source language OCaml (www.ocaml.org) with some added directives for reasoning. OCaml is a great functional programming language that’s used both in academia and in industry (e.g. JaneStreet). These programs are also models because we’ve created a mechanized formal semantics for this fragment of OCaml, which means that when you submit such program into ImandraX, it is automatically coverted into mathematical logic - but all of this is done “under the hood.”

A natural question is: “What can you model in ImandraX/IML?” The answer is quite a lot, effectively everything that you can express as a program. We have lots of examples in our gallery page: https://www.imandra.ai/demos. Later in this tutorial we’ll discuss “abstraction” and whether directly modeling your program in IML is the right approach (as opposed to using a domain-specific language, or DSL, that ultimately translates into IML).

Formal verification

Formal verification (FV) refers to mathematically verifying properties of programs - in our case, IML models. FV is different from traditional testing as it requires logically reasoning about (typically) infinitely many possible scenarios and the evidence, when you have successfully proved a property, comes in the form of a mathematical proof. From the perspective of a developer, writing out the properties to verify is much more natural to the way that humans think than thinking of concrete test cases. For example, if

We ask ImandraX to formally verify properties of models by writing Verification Goals (VG), boolean valued (returns a True or a False) functions also written in IML that encodes a property you wish to verify of the model. This is much more powerful than simply writing tests - where you would need to come up with specific inputs and outputs, because here you can express properties that must hold true for effectively infinitely many possible inputs. Such symbolic description of the type of property you wish to verify is much closer to “human thinking” and it’s much easier (you don’t have to come up with concrete instances!). In our industrial applications of automated reasoning - for example in financial services - we work with operators of complex systems and often encode the statements that they make to the regulators as verification goals.

Let’s now revisit the UBS example. The demo code (not listed here for brevity) contains the following:

  • Background type definitions and helper functions (e.g. order type which contains information about an order like quantity, side (Buy or Sell), order type and limit price (if applicable))
  • order_priority function that takes as input side of the order, orders o1 and o2, current market conditions (e.g. national best bid and offer) mkt and returns True when o1 is higher ranked than o2 and False for the opposite
  • Transitivity VG checking that order_priority function is, in fact, transitive.

Let’s see how we encode transitivity:

let rank_transitivity side o1 o2 o3 mkt =
  order_higher_ranked(side,o1,o2,mkt) &&
  order_higher_ranked(side,o2,o3,mkt)
  ==>
  order_higher_ranked(side,o1,o3,mkt)

That simply states that if (for the same side (Buy or Sell) and market conditions mkt), if an order 1 (o1) is higher ranked than order 2 (o2) and order 2 (o2) is higher ranked than order 3 (o3), then ALWAYS order 1 (o1) must be higher ranked than order 3 (o3). The VG rank_transitivity simply encodes that.

Once you have admitted those into ImandraX and asked to verify it, you would typically get either:

  • A counterexample demonstrating where the VG fails
  • Or, a proof that the VG is True for all possible inputs

In the case of our rank_transitivity, verify (rank_transditivity) will fail and you can explicitly extract the counter-example with instance (rank_transitivity). Typically you would use the counterexample to refine the model (the function doing the comparison) or the property you wish to verify, or both! In our experience of applying formal methods in industrial settings (with very complex models) you rarely get verification goals correct the first time!

Region decomposition

Region decomposition refers to the automated analysis of the model’s state-space by dividing it up into a finite number of symbolic “regions.” No doubt you’ve heard of developers wanting to “cover all the edge cases” when testing code - well, this is the mathematical way of thinking about edge cases. The algorithm itself comes,

Each region contains:

  • a set of constrains (expressed in IML) on the inputs such that the code goes into this direction
  • invariant result refers to the outcome of running the model on inputs that satisfy the constraints
  • sample points these refer to a sample set of inputs that satisfy the constraints (what we use to generate test cases)

Let’s start with a basic example by defining and decomposing a simple function:

let g x =
  if x > 22 then 9
  else 100 + x

let f x =
  if x > 99 then
    100
  else if x < 70 && x > 23
  then 89 + x
  else if x > 20
  then g x + 20
  else if x > -2 then
    103
  else 99
[@@decomp top ()];;

Let’s now revisit the more complicated example we touched upon in the introduction section pertaining to SIX Swiss.

let match_price (ob : order_book) (ref_price : real) = 
 ... (* omitted for brevity *)
[@@decomp top ()];;

Region 1.1.1.1.1.1.1.1:

  • ob.sells <> []
  • ob.buys <> []
  • (List.hd ob.buys).order_qty = (List.hd ob.sells).order_qty
  • (List.hd ob.buys).order_type = Market
  • (List.hd ob.sells).order_type = Market
  • (List.tl ob.buys) <> []
  • (List.tl ob.sells) <> []
  • not ((List.hd (List.tl ob.buys)).order_type = Market)
  • not ((List.hd (List.tl ob.sells)).order_type = Market)
  • not ((List.hd (List.tl ob.buys)).order_price >. ref_price)
  • not ((List.hd (List.tl ob.sells)).order_price <. ref_price) and the invariant result is this:
  • F = Known (List.hd (List.tl ob.sells)).order_price

While Region *.2 has all of the same constraints except for the last one which is negated (notice the added not at the front):

  • not ((List.hd (List.tl ob.sells)).order_price <. ref_price)

This seemingly small difference leads to a fundmanetal change in the resulting price (output of the function):

  • F = Known ref_price Which now becomes the ref_price, which is one of the two inputs into the function. Without going into market microstructure specifics, this means that there’s not enough “priced” liquidity available, so the trading price is determined to be something more “stable”, in this case it’s the reference price of the book (which may be yesterday’s “close” or a moving average, depending on the time of day).

Adding side-conditions

This is where things get really interesting… Imagine you have a large model, but you really only care about specific sub-regions of the state space? Well, by adding a side condition to the decomposition request, you can do just that.

A side condition is an IML boolean-valued function (so must return either True or False) that has the same signature (same types and order of inputs) as the function you’re looking to decompose. After adding side-condition you will only see regions where that side condition function returns True.

Let’s now add a side condition function to our simple running example - notice that it also takes in an int as input (this is inferred since the value is being compared to an integer).

let side_condition x = x > 23;;

let f x =
  if x > 99 then
    100
  else if x < 70 && x > 23
  then 89 + x
  else if x > 20
  then g x + 20
  else if x > -2 then
    103
  else 99
[@@decomp top ~assuming:[%id side_condition]()];;

When ImandraX decomposes function f, it’s now only considering those regions that satisfy side_condition. So, as the result we only now see the following regions:

  • Region 1:
    • constraints: []
    • invariant: []
  • Region 2:
    • constraints: []
    • invariant: []

This ability to consider only certain regions of the state-space is particularly useful as models become more and more complex.

Working with the basis

There are times when you don’t want to think about all the possible edge cases. For example, consider a model that has code that compares values of a datetime type (including year, month, day, hour, etc…).

(* Let's create a datetime type that we'll soon use *)
type datetime = {
    year    : int
  ; month   : int
  ; day     : int
  ; hour    : int
  ; minute  : int
  ; second  : int
}

(* is dt1 less thantg dt2 *)
let dt_less_than dt1 dt2 = 
  if dt1.year   < dt2.year    then true else if dt1.year    > dt2.year    then false else
  if dt1.month  < dt2.month   then true else if dt1.month   > dt2.month   then false else
  if dt1.day    < dt2.day     then true else if dt1.day     > dt2.day     then false else
  if dt1.hour   < dt2.hour    then true else if dt1.hour    > dt2.hour    then false else
  if dt1.minute < dt2.minute  then true else if dt1.minute  > dt2.minute  then false else
  if dt1.second < dt2.second  then true else if dt1.second  > dt2.second  then false else
  true
[@@decomp top ()];;

This function has 12 regions - all the different ways that two values can be different. What if that function is called from another function? Let’s now add more code that calls dt_less_than.

type transaction = {
    date    : datetime
  ; amount  : int 
  ; price   : int
}

(* Let's now add some logic that makes use of `dt_less_than` function  *)
let is_more_important t1 t2 = 
  if (t1.amount * t1.price) > (2 * t2.amount * t2.price) then true else
  dt_less_than t1.date t2.date
[@@decomp top ()];;

When we decompose is_more_important - we get (predictably) get 13 regions. But what if you didn’t really care to consider all the ways dt_less_than “behaves”? Well, then you can add dt_less_than function into the basis - which means that ImandraX will “not go into” the function and explore its edge cases. You can do this by adding ~basis:[[%id dt_less_than] into the decomposition call.

let is_more_important t1 t2 = 
  if (t1.amount * t1.price) > (2 * t2.amount * t2.price) then true else
  dt_less_than t1.date t2.date
[@@decomp top ~basis:[[%id dt_less_than]] ()];;

And just like that, instead of the original 14 regions - we now only have 2!

  • Region 1:
    • constraints [t1.amount * t1.price > 2 * t2.amount * t2.price]
    • invariant true
  • Region 2:
    • constraints [not t1.amount * t1.price > 2 * t2.amount * t2.price]
    • invariant dt_less_than t1.date t2.date

This feature, like adding side conditions, is particularly useful when you deal with really complex models (sometimes they may contain many thousands of lines of IML!).

Generating test cases

TODO: Explain how to extract test cases from regions.