Imandra encoding of UBS dark pool (Form ATS)

In this notebook, we model the order priority logic of the UBS ATS dark pool as described in UBS's June 1st 2015 Form ATS submission to the SEC and analyse it using Imandra.

We observe that as described, the order priority logic suffers from a fundamental flaw: the order ranking function is not transitive.

This type of subtle issue in matching logic strongly motivates the use of formal, machine reasonable disclosures.

Some relevant references:

UBS Future of Finance Challenge - First Place Winner

This analysis was part of Aesthetic Integration's entry in the 2015 UBS Future of Finance Challenge, for which we won first place (out of 620 companies from 52 countries!). This analysis is based purely on publicly available documents, and is based on our interpretation of the English prose written in the Form ATS.

An Imandra Formal Model of UBS ATS Order Priority Logic

We begin our model by defining a record type corresponding to the current NBB/O and relevant market data signals.

In [1]:
type mkt_data = {
  nbb : real;
  nbo : real;
  l_up : real;
  l_down : real;
}
Out[1]:
type mkt_data = { nbb : real; nbo : real; l_up : real; l_down : real; }

Let us now introduce some useful functions on mkt_data.

In [2]:
type mkt_cond = MKT_NORMAL | MKT_CROSSED | MKT_LOCKED

let which_mkt mkt =
  if mkt.nbo = mkt.nbb then MKT_LOCKED
  else if mkt.nbo <. mkt.nbb then MKT_CROSSED
  else MKT_NORMAL

let mid_point mkt = (mkt.nbb +. mkt.nbo) /. 2.0
Out[2]:
type mkt_cond = MKT_NORMAL | MKT_CROSSED | MKT_LOCKED
val which_mkt : mkt_data -> mkt_cond = <fun>
val mid_point : mkt_data -> real = <fun>

Because our model is executable, we can compute with various mkt_data values:

In [3]:
{nbb=42.11; nbo=42.10; l_up=3. ; l_down= 2.5}
Out[3]:
- : mkt_data = {nbb = 4211/100; nbo = 421/10; l_up = 3; l_down = 5/2}
In [4]:
which_mkt {nbb=42.11; nbo=42.10; l_up=3. ; l_down= 2.5}
Out[4]:
- : mkt_cond = MKT_CROSSED

Aside: Custom Document Printers

Imandra has a powerful structured document system for making custom views and interfaces for your algorithm analysis tasks.

To make our Imandra notebooks and analysis toolchains user-friendly, we can define and install our own custom Imandra document printer that will render our market data type in a table in our notebook.

For example, we can define a simple table-based document printer for our mkt_data type as follows.

We use the [@@program] attribute on our pretty-printer definition, to tell Imandra to only define this function in #program mode (not in #logic mode, i.e., not within our formal logic). Arbitrary OCaml functions can be defined in #program mode, the basis for much custom Imandra interfaces and proof automation:

In [5]:
let doc_of_mkt_data m =
  let module D = Document in
  D.indent "mkt_data" @@ D.record [
           "nbb", D.s @@ Real.to_string_approx m.nbb;
           "nbo", D.s @@ Real.to_string_approx m.nbo;
           "l_up", D.s @@ Real.to_string_approx m.l_up;
           "l_down", D.s @@ Real.to_string_approx m.l_down;
  ]
[@@program]

#install_doc doc_of_mkt_data
Out[5]:
val doc_of_mkt_data : mkt_data -> Imandra_surface__Document.t = <fun>

If we view the same mkt_data value as above, we'll now see it rendered with our custom pretty-printer:

In [6]:
{nbb=42.11; nbo=42.10; l_up=3. ; l_down= 2.5}
Out[6]:
- : mkt_data = <document>

mkt_data

nbb42.11
nbo42.1
l_up3.
l_down2.5

Time, Price and Static Data

We now define some types and functions for representing time, price and static_data. We use int for time and real for price, as it is sufficient for this analysis, but custom types (e.g., decs with price bands) can be easily defined.

In [7]:
type time = int
Out[7]:
type time = int
In [8]:
type price = real
Out[8]:
type price = real
In [9]:
type static_data = { round_lot : int;
                     tick_size : float }
Out[9]:
type static_data = { round_lot : int; tick_size : float; }

Order types

We now define the order types supported by the dark pool.

Section 2 of the Form ATS defines the order types as follows:

Order Types:

  • Pegged Orders (both Resident and IOC TimeInForce).
    Pegging can be to the near, midpoint, or far
    side of the NBBO. Pegged Orders may have a limit price.
  • Limit Orders (both Resident and IOC TimeInForce)
  • Market Orders (both Resident and IOC TimeInForce)

Conditional Indication Types:

  • Pegged Conditional Indications (Resident T)
  • Limit Conditional Indications (Resident TimeInForce only)
In [10]:
type order_side = BUY | SELL | SELL_SHORT

type order_peg = NEAR | MID | FAR | NO_PEG

type order_type =
    MARKET
  | LIMIT
  | PEGGED
  | PEGGED_CI
  | LIMIT_CI
  | FIRM_UP_PEGGED
  | FIRM_UP_LIMIT
Out[10]:
type order_side = BUY | SELL | SELL_SHORT
type order_peg = NEAR | MID | FAR | NO_PEG
type order_type =
    MARKET
  | LIMIT
  | PEGGED
  | PEGGED_CI
  | LIMIT_CI
  | FIRM_UP_PEGGED
  | FIRM_UP_LIMIT

Source Categories are defined in the Form ATS as follows:

  • Source Category 1: Retail orders routed by broker - dealer clients of the UBS Retail Market Making business.
  • Source Category 2: Certain orders received from UBS algorithms, where the underlying client is an institutional client of UBS.
  • Source Category 3: Orders received from Order Originators that are determined by UBS to exhibit lowto - neutral reversion.
  • Source Category 4: All other orders not originating from Source Categories 1, 2 or 3.
In [11]:
type order_attr = RESIDENT | IOC

type category = C_ONE | C_TWO | C_THREE | C_FOUR
Out[11]:
type order_attr = RESIDENT | IOC
type category = C_ONE | C_TWO | C_THREE | C_FOUR

Capacity, Eligibilities and Crossing Restrictions

In [12]:
type capacity = Principal | Agency

(* ID of the order source *)

type order_source = int

(* UBS's ID in the model *)

let ubs_id = 12

(* Category crossing constraints *)

type category_elig = {
  c_one_elig : bool;
  c_two_elig : bool;
  c_three_elig : bool;
  c_four_elig : bool;
}

let default_cat_elig = {
  c_one_elig = true;
  c_two_elig = true;
  c_three_elig = true;
  c_four_elig = true;
}

(* Type for crossing restrictions *)

type cross_restrict = {
  cr_self_cross : bool;
  cr_ubs_principal : bool;
  cr_round_lot_only : bool;
  cr_no_locked_nbbo : bool;
  cr_pegged_mid_point_mode : int;

  (* From the examples, we understand that: 0 - no constraint 1 - mid      *)
  (* constraint 2 - limit constraint                                       *)

  cr_enable_conditionals : bool;
  cr_min_qty : bool;
  cr_cat_elig : category_elig;
}

let default_cross_restrict = {
  cr_self_cross = false;
  cr_ubs_principal = false;
  cr_round_lot_only = false;
  cr_no_locked_nbbo = false;
  cr_pegged_mid_point_mode = 0;
  cr_enable_conditionals = false;
  cr_min_qty = false;
  cr_cat_elig = default_cat_elig;
}
Out[12]:
type capacity = Principal | Agency
type order_source = int
val ubs_id : Z.t = 12
type category_elig = {
  c_one_elig : bool;
  c_two_elig : bool;
  c_three_elig : bool;
  c_four_elig : bool;
}
val default_cat_elig : category_elig =
  {c_one_elig = true; c_two_elig = true; c_three_elig = true;
   c_four_elig = true}
type cross_restrict = {
  cr_self_cross : bool;
  cr_ubs_principal : bool;
  cr_round_lot_only : bool;
  cr_no_locked_nbbo : bool;
  cr_pegged_mid_point_mode : int;
  cr_enable_conditionals : bool;
  cr_min_qty : bool;
  cr_cat_elig : category_elig;
}
val default_cross_restrict : cross_restrict =
  {cr_self_cross = false; cr_ubs_principal = false;
   cr_round_lot_only = false; cr_no_locked_nbbo = false;
   cr_pegged_mid_point_mode = 0; cr_enable_conditionals = false;
   cr_min_qty = false;
   cr_cat_elig =
    {c_one_elig = true; c_two_elig = true; c_three_elig = true;
     c_four_elig = true}}

Orders

We now define the type order, representing all data associated with a given order.

In [13]:
(* Note: there's both the quantity of the order and the current filled quantity. *)

type order =
    { id : int;                        (* Order ID *)
      peg : order_peg;                 (* Near, Mid, Far or NoPeg *)
      client_id : int;                 (* Client ID *)
      order_type : order_type;         (* Market, Limit or Pegged order + Conditional Indications *)
      qty : int;                       (* Original quantity of the order (updated after cancel/replace) *)
      min_qty : int;                   (* Minimum acceptible quantity to trade *)
      leaves_qty : int;                (* Remaining quantity of the order *)
      price : price;                   (* Limit price (Not used if the order *)
      time : time;                     (* time of order entry (reset on update)) *)
      src : order_source;              (* ID of the order source *)
      order_attr : order_attr;         (* Resident or Immediate Or Cancel (IOC) *)
      capacity : capacity;             (* Principal or agency *)
      category : category;             (* Client category *)
      cross_restrict : cross_restrict; (* Crossing restrictions *)
      locate_found : bool;             (* A sell-short order without a locate would be rejected *)
      expiry_time : int;               (* When will the order expire? *)
    }
Out[13]:
type order = {
  id : int;
  peg : order_peg;
  client_id : int;
  order_type : order_type;
  qty : int;
  min_qty : int;
  leaves_qty : int;
  price : price;
  time : time;
  src : order_source;
  order_attr : order_attr;
  capacity : capacity;
  category : category;
  cross_restrict : cross_restrict;
  locate_found : bool;
  expiry_time : int;
}

Determining how much and at what price two orders may trade

In [14]:
(** Uses two orders' timestamps to determin the older price of the two *)
let older_price (o1, o2) =
  if o1.time > o2.time then o2.price else o1.price

type fill_price =
  | Known of price
  | Unknown
  | TOP of price

(* Functions for categorisations  *)

let cat_priority (o1, o2) =
  if o1.category = C_ONE then false
  else if o1.category = C_TWO &&
            (o2.category = C_THREE || o2.category = C_FOUR)
  then false
  else if o1.category = C_THREE && (o2.category = C_FOUR) then false
  else true

let eff_min_qty (o) = min o.min_qty o.leaves_qty

let effective_size (o, should_round, round_lot) =
  if should_round = true then
    ( if round_lot > 0 then ( (o.leaves_qty / round_lot) * round_lot )
      else o.leaves_qty )
  else
    o.leaves_qty

(* The pricing functions *)

let lessAggressive (side, lim_price, far_price) =
  if lim_price <. 0.0 then far_price else
    (if side = BUY then Real.min lim_price far_price
     else Real.max lim_price far_price)

(** This function is used to calculate the priority price *)
let priority_price (side, o, mkt) =
  let calc_pegged_price =
    ( match o.peg with
      | FAR -> lessAggressive(side, o.price,
                              (if side = BUY then mkt.nbo else mkt.nbb))
      | MID -> lessAggressive(side, o.price, (mid_point mkt))
      | NEAR -> lessAggressive(side, o.price,
                               (if side = BUY then mkt.nbb else mkt.nbo))
      | NO_PEG -> o.price )
  in
  let calc_nbbo_capped_limit =
    ( if side = BUY then lessAggressive (BUY, o.price, mkt.nbo)
      else lessAggressive (SELL, o.price, mkt.nbb ) )
  in
  match o.order_type with
  | LIMIT -> calc_nbbo_capped_limit
  | MARKET -> if side = BUY then mkt.nbo else mkt.nbb
  | PEGGED -> calc_pegged_price
  | PEGGED_CI -> calc_pegged_price
  | LIMIT_CI -> calc_nbbo_capped_limit
  | FIRM_UP_PEGGED -> calc_pegged_price
  | FIRM_UP_LIMIT -> calc_nbbo_capped_limit

(** This is used to calculate the actual price at which the order would trade   *)
let exec_price (side, o, mkt) =
  priority_price (side, o, mkt)
Out[14]:
val older_price : order * order -> price = <fun>
type fill_price = Known of price | Unknown | TOP of price
val cat_priority : order * order -> bool = <fun>
val eff_min_qty : order -> int = <fun>
val effective_size : order * bool * int -> int = <fun>
val lessAggressive : order_side * real * real -> real = <fun>
val priority_price : order_side * order * mkt_data -> real = <fun>
val exec_price : order_side * order * mkt_data -> real = <fun>

Crossing Restrictions

The UBS ATS allows all Order Originators to use the following optional crossing restrictions, on a per - order or configured basis:

  • No Self Cross: To prevent crossing against 'own orders' (orders sent with the same client ID).
  • No UBS Principal: To prevent crossing against UBS BD Principal Orders, or UBS affiliate Principal orders.
  • Round Lot Only: To prevent crossing in other than round lot orders.
  • No Locked: To prevent crossing on a pegged order when the NBBO is locked. (Bid = Offer)
  • PeggedMidPointMode: To prevent a Mid - point Pegged Order from being executed at its limit price if (i) in the case of a buy order, its limit price is less than the mid - point of the spread between the NBB and NBO and (ii) in the case of a sell order, its limit price is greater than the mid - point of the spread between the NBB and NBO. In the event this restriction is not elected, a Mid - Point Pegged Order with a specified limit price may be executed at the limit price even if the price is not equal to the mid - point of the spread between the NBB and the NBBO.
  • Enable Conditionals: To enable a Resident Order to interact with Conditional Indicators.
  • Minimum Quantity: Orders may be routed to the UBS ATS with a minimum quantity value specified. UBS ATS will only cross where at least this number of shares is available from a single eligible contra side order.
In [15]:
(* Note that these are order-level constraints. There are members of this  *)
(* structure, like cr_min_qty and cr_round_lot_only that are used in       *)
(* calculating the effective minimum price.                                *)

let get_cat_eligibility (cat_elig, c) =
  match c with
  | C_ONE -> cat_elig.c_one_elig
  | C_TWO -> cat_elig.c_two_elig
  | C_THREE -> cat_elig.c_three_elig
  | C_FOUR -> cat_elig.c_four_elig

let can_orders_cross (o1, o2) =
  let o1_cr = o1.cross_restrict in
  let o2_cr = o2.cross_restrict in
  if (o1_cr.cr_self_cross || o2_cr.cr_self_cross) && (o1.client_id = o2.client_id)
  then false
  else if (o1_cr.cr_ubs_principal || o2_cr.cr_ubs_principal) &&
            (o1.client_id = ubs_id || o2.client_id = ubs_id) then false
  else if (o1_cr.cr_enable_conditionals || o2_cr.cr_enable_conditionals) &&
            (o1.order_type = LIMIT_CI || o1.order_type = PEGGED_CI) then false
  else true
Out[15]:
val get_cat_eligibility : category_elig * category -> bool = <fun>
val can_orders_cross : order * order -> bool = <fun>

Order Book

The Order Book is used to match buy orders against sell orders.

In [16]:
type order_book = {
  buys  : order list;
  sells : order list;
}

let empty_book = { buys = []; sells = [] }

type fill = { order_buy : order;
              order_sell : order;
              fill_qty : int;
              fill_price : fill_price;
              fill_time : time;
            }
Out[16]:
type order_book = { buys : order list; sells : order list; }
val empty_book : order_book = {buys = []; sells = []}
type fill = {
  order_buy : order;
  order_sell : order;
  fill_qty : int;
  fill_price : fill_price;
  fill_time : time;
}

Ranking functions for orders

From Section 4.1 of UBS's June, 2015 Form ATS:

Eligible Resident Orders and IOC Orders are given priority
based first on price and second on the time of their receipt by the UBS ATS.
Eligibility is determined based on the crossing restrictions associated with
the orders on both sides of the potential cross.

Invites are sent to the Order Originators of Conditional Indications on a
priority based first on price, second on the quantity and third on the time of
receipt by UBS ATS. For orders with the same price and time, priority is given
to Resident and IOC Orders over Conditional Indications.

All marketable limit orders (i.e., buy orders with limit prices at or above the
NBO or sell orders with limit prices at or below the NBB) will be treated as
though they are at equivalent prices for priority purposes. As such, they will
be handled based strictly on time priority, as if they were market orders. If a
marketable limit order becomes non - marketable before execution, it will be treated
as a limit order and will receive price / time priority, with time based upon the
original time of receipt of the order by the UBS ATS.

Let us formalise this logic below.

In [17]:
let non_ci (ot) = not(ot = PEGGED_CI || ot = LIMIT_CI);;

let order_higher_ranked (side, o1, o2, mkt) =
  let ot1 = o1.order_type in
  let ot2 = o2.order_type in

  let p_price1 = priority_price (side, o1, mkt) in
  let p_price2 = priority_price (side, o2, mkt) in

  let wins_price = (
    if side = BUY then
      ( if p_price1 >. p_price2 then 1
        else if p_price1 = p_price2 then 0
        else -1)
    else
      ( if p_price1 <. p_price2 then 1
        else if p_price1 = p_price2 then 0
        else -1) ) in

  let wins_time = (
    if o1.time < o2.time then 1
    else if o1.time = o2.time then 0
    else -1
  ) in

  (* Note that the CI priority is price, quantity and then time *)
  if wins_price = 1 then true
  else if wins_price = -1 then false
  else (
    (* Same price level - first check to see whether we're comparing two   *)
    (* CI orders here                                                      *)
    if not (non_ci (ot1)) && not (non_ci (ot2)) then
      o1.leaves_qty > o2.leaves_qty
    else ( if wins_time = 1 then true
           else if wins_time = -1 then false
           else (
             if non_ci(ot1) then true
             else if (not(non_ci(ot1)) && non_ci(ot2)) then false
             else
               o1.leaves_qty > o2.leaves_qty)
         )
  )
Out[17]:
val non_ci : order_type -> bool = <fun>
val order_higher_ranked : order_side * order * order * mkt_data -> bool =
  <fun>

The property we're interested in is whether this ranking predicate is transitive (a necessary condition for being a proper ordering relation that can be used for sorting, e.g., orders in the book):

In [18]:
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)
Out[18]:
val rank_transitivity :
  order_side -> order -> order -> order -> mkt_data -> bool = <fun>

Now we can check whether this property of being transitive holds:

In [19]:
verify (fun side o1 o2 o3 mkt -> rank_transitivity side o1 o2 o3 mkt)
Out[19]:
- : order_side -> order -> order -> order -> mkt_data -> bool = <fun>
module CX :
  sig
    val side : order_side
    val o1 : order
    val o2 : order
    val o3 : order
    val mkt : mkt_data
  end
Counterexample (after 0 steps, 0.054s):
 let side = BUY
 let o1 =
   {id = 3; peg = NEAR; client_id = 4; order_type = PEGGED_CI; qty = 5;
    min_qty = 6; leaves_qty = 1236; price = 0.; time = 0; src = 7;
    order_attr = IOC; capacity = Principal; category = C_TWO;
    cross_restrict =
     {cr_self_cross = false; cr_ubs_principal = false;
      cr_round_lot_only = false; cr_no_locked_nbbo = false;
      cr_pegged_mid_point_mode = 2; cr_enable_conditionals = false;
      cr_min_qty = false;
      cr_cat_elig =
       {c_one_elig = false; c_two_elig = false; c_three_elig = false;
        c_four_elig = false}};
    locate_found = false; expiry_time = 8}
 let o2 =
   {id = 9; peg = MID; client_id = 10; order_type = PEGGED_CI; qty = 11;
    min_qty = 12; leaves_qty = 1235; price = 0.; time = (-1); src = 13;
    order_attr = IOC; capacity = Principal; category = C_TWO;
    cross_restrict =
     {cr_self_cross = false; cr_ubs_principal = false;
      cr_round_lot_only = false; cr_no_locked_nbbo = false;
      cr_pegged_mid_point_mode = 15; cr_enable_conditionals = false;
      cr_min_qty = false;
      cr_cat_elig =
       {c_one_elig = false; c_two_elig = false; c_three_elig = false;
        c_four_elig = false}};
    locate_found = false; expiry_time = 14}
 let o3 =
   {id = 19; peg = MID; client_id = 20; order_type = FIRM_UP_LIMIT; qty = 21;
    min_qty = 22; leaves_qty = 2437; price = 8856.; time = 0; src = 23;
    order_attr = IOC; capacity = Principal; category = C_TWO;
    cross_restrict =
     {cr_self_cross = false; cr_ubs_principal = false;
      cr_round_lot_only = false; cr_no_locked_nbbo = false;
      cr_pegged_mid_point_mode = 18; cr_enable_conditionals = false;
      cr_min_qty = false;
      cr_cat_elig =
       {c_one_elig = false; c_two_elig = false; c_three_elig = false;
        c_four_elig = false}};
    locate_found = false; expiry_time = 24}
 let mkt = {nbb = 1.; nbo = 0.; l_up = 2.; l_down = 3.}
Refuted
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.054s
details
Expand
smt_stats
arith offset eqs8
num checks1
arith assert lower172
arith pivots23
rlimit count47777
mk clause707
datatype occurs check17
mk bool var1204
arith assert upper185
datatype splits72
decisions2741
arith add rows192
arith bound prop4
propagations2511
interface eqs1
conflicts52
arith fixed eqs97
datatype accessor ax101
minimized lits4
arith conflicts2
arith assert diseq126
datatype constructor ax428
num allocs1424269982
final checks2
added eqs4308
del clause231
arith eq adapter85
memory16.660000
max memory18.750000
Expand
  • start[0.054s]
      (if (if :var_0: = BUY
           then
             if (if ….order_type = LIMIT
                 then
                   if :var_0: = BUY then if ….1 <. 0 then … else …
                   else if ….1 <. 0 then … else …
                 else
                 if ….order_type = MARKET
                 then if :var_0: = BUY then … else …
                 else if ….order_type = PEGGED then … else …)
                >.
                (if ….order_type = LIMIT
                 then
                   if :var_0: = BUY then if ….1 <. 0 then … else …
                   else if … then … else …
                 else …)
             then 1 else …
           else …)
          = 1
       then true else …)
      && … ==> …
  • simplify

    into
    (not
     (((if :var_0: = BUY
        then
          if (if :var_1:.order_type = LIMIT
              then
                if :var_0: = BUY then if 0 <=. :var_1:.price then … else …
                else if 0 <=. :var_1:.price then … else …
              else
              if :var_1:.order_type = MARKET
              then if :var_0: = BUY then … else …
              else if :var_1:.order_type = PEGGED then … else …)
             <=.
             (if :var_2:.order_type = LIMIT
              then
                if :var_0: = BUY then if 0 <=. :var_2:.price then … else …
                else if 0 <=. :var_2:.price then … else …
              else
              if :var_2:.order_type = MARKET
              then if :var_0: = BUY then … else …
              else if :var_2:.order_type = PEGGED then … else …)
          then if … then 0 else -1 else 1
        else …)
       = 1 || …)
      && …)
     || …)
    || …
    expansions
    []
    rewrite_steps
      forward_chaining
      • Sat (Some let side = BUY let o1 = {id = 3; peg = NEAR; client_id = 4; order_type = PEGGED_CI; qty = 5; min_qty = 6; leaves_qty = 1236; price = 0.; time = 0; src = 7; order_attr = IOC; capacity = Principal; category = C_TWO; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 2; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 8} let o2 = {id = 9; peg = MID; client_id = 10; order_type = PEGGED_CI; qty = 11; min_qty = 12; leaves_qty = 1235; price = 0.; time = (-1); src = 13; order_attr = IOC; capacity = Principal; category = C_TWO; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 15; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 14} let o3 = {id = 19; peg = MID; client_id = 20; order_type = FIRM_UP_LIMIT; qty = 21; min_qty = 22; leaves_qty = 2437; price = 8856.; time = 0; src = 23; order_attr = IOC; capacity = Principal; category = C_TWO; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 18; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 24} let mkt = {nbb = 1.; nbo = 0.; l_up = 2.; l_down = 3.} )

      We just showed that the ranking function is not transitive! As always, the components of the counterexample are automatically reflected into a module called CX and can be computed with, just as any other value in our runtime:

      In [20]:
      CX.o1
      
      Out[20]:
      - : order =
      {id = 3; peg = NEAR; client_id = 4; order_type = PEGGED_CI; qty = 5;
       min_qty = 6; leaves_qty = 1236; price = 0; time = 0; src = 7;
       order_attr = IOC; capacity = Principal; category = C_TWO;
       cross_restrict =
        {cr_self_cross = false; cr_ubs_principal = false;
         cr_round_lot_only = false; cr_no_locked_nbbo = false;
         cr_pegged_mid_point_mode = 2; cr_enable_conditionals = false;
         cr_min_qty = false;
         cr_cat_elig =
          {c_one_elig = false; c_two_elig = false; c_three_elig = false;
           c_four_elig = false}};
       locate_found = false; expiry_time = 8}
      

      Let's verify this counterexample to transitivity by computation!

      In [21]:
      order_higher_ranked CX.(side, o1, o2, mkt)
      
      Out[21]:
      - : bool = true
      
      In [22]:
      order_higher_ranked CX.(side, o2, o3, mkt)
      
      Out[22]:
      - : bool = true
      
      In [23]:
      order_higher_ranked CX.(side, o1, o3, mkt)
      
      Out[23]:
      - : bool = false
      

      Let us add some additional constraints to help make our counterexample "pretty":

      In [24]:
      let pretty mkt o1 o2 o3 =
          o1.leaves_qty <= o1.qty &&
          o2.leaves_qty <= o2.qty &&
          o3.leaves_qty <= o3.qty &&
          o1.time >= 0 &&
          o2.time >= 0 &&
          o3.time >= 0 &&
          o1.price >. 0.0 &&
          o2.price >. 0.0 &&
          o3.price >. 0.0 &&
          o1.qty > 0 &&
          o2.qty > 0 &&
          o3.qty > 0 &&
          o1.leaves_qty >= 0 &&
          o2.leaves_qty >= 0 &&
          o3.leaves_qty >= 0 &&
          mkt.l_down >. 0.0 &&
          mkt.nbb >. mkt.l_down &&
          mkt.nbo >. mkt.nbb &&
          mkt.l_up >. mkt.nbo
      
      Out[24]:
      val pretty : mkt_data -> order -> order -> order -> bool = <fun>
      
      In [25]:
      verify (fun side o1 o2 o3 mkt -> pretty mkt o1 o2 o3 ==> rank_transitivity side o1 o2 o3 mkt)
      
      Out[25]:
      - : order_side -> order -> order -> order -> mkt_data -> bool = <fun>
      module CX :
        sig
          val side : order_side
          val o1 : order
          val o2 : order
          val o3 : order
          val mkt : mkt_data
        end
      
      Counterexample (after 0 steps, 0.045s):
       let side = SELL
       let o1 =
         {id = 3; peg = MID; client_id = 4; order_type = PEGGED_CI; qty = 39;
          min_qty = 5; leaves_qty = 2; price = 3.; time = 8366; src = 6;
          order_attr = IOC; capacity = Principal; category = C_TWO;
          cross_restrict =
           {cr_self_cross = false; cr_ubs_principal = false;
            cr_round_lot_only = false; cr_no_locked_nbbo = false;
            cr_pegged_mid_point_mode = 8; cr_enable_conditionals = false;
            cr_min_qty = false;
            cr_cat_elig =
             {c_one_elig = false; c_two_elig = false; c_three_elig = false;
              c_four_elig = false}};
          locate_found = false; expiry_time = 7}
       let o2 =
         {id = 11; peg = MID; client_id = 12; order_type = PEGGED_CI; qty = 7720;
          min_qty = 13; leaves_qty = 1; price = 3.; time = 8365; src = 14;
          order_attr = IOC; capacity = Principal; category = C_TWO;
          cross_restrict =
           {cr_self_cross = false; cr_ubs_principal = false;
            cr_round_lot_only = false; cr_no_locked_nbbo = false;
            cr_pegged_mid_point_mode = 10; cr_enable_conditionals = false;
            cr_min_qty = false;
            cr_cat_elig =
             {c_one_elig = false; c_two_elig = false; c_three_elig = false;
              c_four_elig = false}};
          locate_found = false; expiry_time = 15}
       let o3 =
         {id = 18; peg = MID; client_id = 19; order_type = LIMIT; qty = 2438;
          min_qty = 20; leaves_qty = 0; price = 3.; time = 8366; src = 21;
          order_attr = IOC; capacity = Principal; category = C_TWO;
          cross_restrict =
           {cr_self_cross = false; cr_ubs_principal = false;
            cr_round_lot_only = false; cr_no_locked_nbbo = false;
            cr_pegged_mid_point_mode = 17; cr_enable_conditionals = false;
            cr_min_qty = false;
            cr_cat_elig =
             {c_one_elig = false; c_two_elig = false; c_three_elig = false;
              c_four_elig = false}};
          locate_found = false; expiry_time = 22}
       let mkt =
         {nbb = 2.; nbo = (Real.mk_of_string "18859/5000");
          l_up = (Real.mk_of_string "23859/5000"); l_down = 1.}
      
      Refuted
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.045s
      details
      Expand
      smt_stats
      arith offset eqs23
      num checks1
      arith assert lower106
      arith pivots31
      rlimit count32962
      mk clause600
      datatype occurs check13
      mk bool var897
      arith assert upper91
      datatype splits36
      decisions1443
      arith add rows195
      arith bound prop14
      propagations1341
      interface eqs1
      conflicts29
      arith fixed eqs46
      datatype accessor ax58
      minimized lits1
      arith conflicts2
      arith assert diseq26
      datatype constructor ax230
      num allocs1527666821
      final checks2
      added eqs2056
      del clause169
      arith eq adapter49
      memory20.100000
      max memory21.210000
      Expand
      • start[0.045s]
          :var_0:.leaves_qty <= :var_0:.qty
          && :var_1:.leaves_qty <= :var_1:.qty
             && :var_2:.leaves_qty <= :var_2:.qty
                && :var_0:.time >= 0
                   && :var_1:.time >= 0
                      && :var_2:.time >= 0
                         && :var_0:.price >. 0
                            && :var_1:.price >. 0
                               && :var_2:.price >. 0
                                  && :var_0:.qty > 0
                                     && :var_1:.qty > 0
                                        && :var_2:.qty > 0
                                           && :var_0:.leaves_qty >= 0
                                              && :var_1:.leaves_qty >= 0
                                                 && :var_2:.leaves_qty >= 0
                                                    && :var_3:.l_down >. 0
                                                       && :var_3:.nbb >.
                                                          :var_3:.l_down
                                                          && :var_3:.nbo >.
                                                             :var_3:.nbb
                                                             && :var_3:.l_up >.
                                                                :var_3:.nbo
          ==> (if (if :var_4: = BUY
                   then
                     if (if ….order_type = LIMIT
                         then
                           if :var_4: = BUY then if ….1 <. 0 then … else …
                           else if ….1 <. 0 then … else …
                         else
                         if ….order_type = MARKET
                         then if :var_4: = BUY then … else …
                         else if ….order_type = PEGGED then … else …)
                        >.
                        (if ….order_type = LIMIT
                         then
                           if :var_4: = BUY then if ….1 <. 0 then … else …
                           else if … then … else …
                         else …)
                     then 1 else …
                   else …)
                  = 1
               then true else …)
              && … ==> …
      • simplify

        into
        ((not
          ((((((((((((((((((:var_0:.leaves_qty <= :var_0:.qty
                            && :var_1:.leaves_qty <= :var_1:.qty)
                           && :var_2:.leaves_qty <= :var_2:.qty)
                          && :var_0:.time >= 0)
                         && :var_1:.time >= 0)
                        && :var_2:.time >= 0)
                       && not (:var_0:.price <=. 0))
                      && not (:var_1:.price <=. 0))
                     && not (:var_2:.price <=. 0))
                    && not (:var_0:.qty <= 0))
                   && not (:var_1:.qty <= 0))
                  && not (:var_2:.qty <= 0))
                 && :var_0:.leaves_qty >= 0)
                && :var_1:.leaves_qty >= 0)
               && :var_2:.leaves_qty >= 0)
              && not (:var_3:.l_down <=. 0))
             && not (:var_3:.nbb <=. :var_3:.l_down))
            && not (:var_3:.nbo <=. :var_3:.nbb))
           && not (:var_3:.l_up <=. :var_3:.nbo))
          || not
             (((if :var_4: = BUY
                then
                  if (if :var_0:.order_type = LIMIT
                      then
                        if :var_4: = BUY
                        then if 0 <=. :var_0:.price then … else :var_3:.nbo
                        else if 0 <=. :var_0:.price then … else :var_3:.nbb
                      else
                      if :var_0:.order_type = MARKET
                      then if :var_4: = BUY then :var_3:.nbo else :var_3:.nbb
                      else if :var_0:.order_type = PEGGED then … else …)
                     <=.
                     (if :var_1:.order_type = LIMIT
                      then
                        if :var_4: = BUY
                        then if 0 <=. :var_1:.price then … else :var_3:.nbo
                        else if 0 <=. :var_1:.price then … else :var_3:.nbb
                      else
                      if :var_1:.order_type = MARKET
                      then if :var_4: = BUY then :var_3:.nbo else :var_3:.nbb
                      else if :var_1:.order_type = PEGGED then … else …)
                  then if … then 0 else -1 else 1
                else …)
               = 1 || …)
              && …))
         || …)
        || …
        expansions
        []
        rewrite_steps
          forward_chaining
          • Sat (Some let side = SELL let o1 = {id = 3; peg = MID; client_id = 4; order_type = PEGGED_CI; qty = 39; min_qty = 5; leaves_qty = 2; price = 3.; time = 8366; src = 6; order_attr = IOC; capacity = Principal; category = C_TWO; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 8; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 7} let o2 = {id = 11; peg = MID; client_id = 12; order_type = PEGGED_CI; qty = 7720; min_qty = 13; leaves_qty = 1; price = 3.; time = 8365; src = 14; order_attr = IOC; capacity = Principal; category = C_TWO; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 10; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 15} let o3 = {id = 18; peg = MID; client_id = 19; order_type = LIMIT; qty = 2438; min_qty = 20; leaves_qty = 0; price = 3.; time = 8366; src = 21; order_attr = IOC; capacity = Principal; category = C_TWO; cross_restrict = {cr_self_cross = false; cr_ubs_principal = false; cr_round_lot_only = false; cr_no_locked_nbbo = false; cr_pegged_mid_point_mode = 17; cr_enable_conditionals = false; cr_min_qty = false; cr_cat_elig = {c_one_elig = false; c_two_elig = false; c_three_elig = false; c_four_elig = false}}; locate_found = false; expiry_time = 22} let mkt = {nbb = 2.; nbo = (Real.mk_of_string "18859/5000"); l_up = (Real.mk_of_string "23859/5000"); l_down = 1.} )

          Extending the model with Document printers

          Let's define a few more custom document printers to make these (complex!) counterexamples easier to understand.

          In [26]:
          (* We can generate string printers for our types automatically using `Genpp` *)
          Genpp.eval ~quiet:true ();;
          
          let doc_of_order_type o =
            Document.s @@ Pp.pp_order_type o
          [@@program];;
          
          #install_doc doc_of_order_type;;
          
          let doc_of_order o =
            let module D = Document in
            D.indent "order" @@ D.record [
                "id", D.bigint o.id;
                "peg", D.s @@ Pp.pp_order_peg o.peg;
                "client_id", D.bigint o.client_id;
                "order_type", D.s @@ Pp.pp_order_type o.order_type;
                "qty", D.bigint o.qty;
                "min_qty", D.bigint o.min_qty;
                "leaves_qty", D.bigint o.leaves_qty;
                "price", D.s @@ Real.to_string_approx o.price;
                "time", D.s @@ Pp.pp_time o.time;
                "src", D.s @@ Pp.pp_order_source o.src;
                "order_attr", D.s @@ Pp.pp_order_attr o.order_attr;
                "capacity", D.s @@ Pp.pp_capacity o.capacity;
                "category", D.s @@ Pp.pp_category o.category;
                (* "cross_restrict", D.s @@ Pp.pp_cross_restrict o.cross_restrict; *)
                "locate_found", D.s_f "%B" o.locate_found;
                "expiry_time", D.bigint o.expiry_time;
            ]
          [@@program];;
          
          #install_doc doc_of_order;;
          
          let doc_of_side side = Document.s @@ Pp.pp_order_side side
          [@@program];;
          
          #install_doc doc_of_side;;
          
          let doc_of_mkt mkt =
            let module D = Document in
            D.indent "mkt" @@ D.record [
                "nbb", D.s @@ Real.to_string_approx mkt.nbb;
                "nbo", D.s @@ Real.to_string_approx mkt.nbo;
                "l_up", D.s @@ Real.to_string_approx mkt.l_up;
                "l_down", D.s @@ Real.to_string_approx mkt.l_down;
            ]
          [@@program];;
          
          let pp_rank (side, o1, o2, o3, mkt) =
            Document.(tbl ~headers:["side";"order1";"order2";"order3";"mkt"] 
              @@ [[doc_of_side side; doc_of_order o1; doc_of_order o2; doc_of_order o3; doc_of_mkt mkt]]) 
           [@@program];;
          
          #install_doc pp_rank
          
          Out[26]:
          - : unit = ()
          val doc_of_order_type : order_type -> Imandra_surface.Document.t = <fun>
          val doc_of_order : order -> Imandra_surface__Document.t = <fun>
          val doc_of_side : order_side -> Imandra_surface.Document.t = <fun>
          val doc_of_mkt : mkt_data -> Imandra_surface__Document.t = <fun>
          val pp_rank :
            order_side * order * order * order * mkt_data -> Imandra_surface.Document.t =
            <fun>
          

          Now, let's view our latest counterexample again:

          In [27]:
          CX.(side, o1, o2, o3, mkt)
          
          Out[27]:
          - : order_side * order * order * order * mkt_data = <document>
          
          sideorder1order2order3mkt
          SELL
          order
          id3
          pegMID
          client_id4
          order_typePEGGED_CI
          qty39
          min_qty5
          leaves_qty2
          price3.
          time8366
          src6
          order_attrIOC
          capacityPrincipal
          categoryC_TWO
          locate_foundfalse
          expiry_time7
          order
          id11
          pegMID
          client_id12
          order_typePEGGED_CI
          qty7720
          min_qty13
          leaves_qty1
          price3.
          time8365
          src14
          order_attrIOC
          capacityPrincipal
          categoryC_TWO
          locate_foundfalse
          expiry_time15
          order
          id18
          pegMID
          client_id19
          order_typeLIMIT
          qty2438
          min_qty20
          leaves_qty0
          price3.
          time8366
          src21
          order_attrIOC
          capacityPrincipal
          categoryC_TWO
          locate_foundfalse
          expiry_time22
          mkt
          nbb2.
          nbo3.7718
          l_up4.7718
          l_down1.