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.

Try this!
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.

Try this!
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:

Try this!
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}
Try this!
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:

Try this!
In [5]:
#program;;
(* #require "tyxml";; *)

let html elt =
  let module H = Tyxml.Html in
  Document.html (Document.Unsafe_.html_of_string @@ CCFormat.sprintf "%a" (H.pp_elt ()) elt);;

let html_of_mkt_data (m : mkt_data) =
  let module H = Tyxml.Html in
  H.table
  [ H.tr [ H.td [H.txt "nbb"]; H.td [H.txt (Real.to_string_approx m.nbb)] ]
  ; H.tr [ H.td [H.txt "nbo"]; H.td [H.txt (Real.to_string_approx m.nbo)] ]
  ; H.tr [ H.td [H.txt "l_up"]; H.td [H.txt (Real.to_string_approx m.l_up)] ]
  ; H.tr [ H.td [H.txt "l_down"]; H.td [H.txt (Real.to_string_approx m.l_down)] ]
  ];;

let doc_of_mkt_data m =
  let module D = Document in
  let module H = Tyxml.Html in
  D.indent "mkt_data" @@ (html (html_of_mkt_data m))
[@@program]

#install_doc doc_of_mkt_data;;

#logic;;
Out[5]:
val html : 'a Tyxml_html.elt -> Document.t = <fun>
val html_of_mkt_data : mkt_data -> [> Html_types.table ] Tyxml_html.elt =
  <fun>
val doc_of_mkt_data : mkt_data -> Document.t = <fun>

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

Try this!
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.

Try this!
In [7]:
type time = int
Out[7]:
type time = Z.t
Try this!
In [8]:
type price = real
Out[8]:
type price = real
Try this!
In [9]:
type static_data = { round_lot : int;
                     tick_size : float }
Out[9]:
type static_data = { round_lot : time; 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)
Try this!
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.
Try this!
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

Try this!
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 = time
val ubs_id : order_source = 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 : order_source;
  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.

Try this!
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 : order_source;
  peg : order_peg;
  client_id : order_source;
  order_type : order_type;
  qty : order_source;
  min_qty : order_source;
  leaves_qty : order_source;
  price : price;
  time : order_source;
  src : order_source;
  order_attr : order_attr;
  capacity : capacity;
  category : category;
  cross_restrict : cross_restrict;
  locate_found : bool;
  expiry_time : order_source;
}

Determining how much and at what price two orders may trade

Try this!
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 -> order_source = <fun>
val effective_size : order * bool * order_source -> order_source = <fun>
val lessAggressive : order_side * price * price -> price = <fun>
val priority_price : order_side * order * mkt_data -> price = <fun>
val exec_price : order_side * order * mkt_data -> price = <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.
Try this!
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.

Try this!
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 : order_source;
  fill_price : fill_price;
  fill_time : order_source;
}

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.

Try this!
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):

Try this!
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:

Try this!
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.034s):
let side : order_side = BUY
let o1 : order =
  {id = 1; peg = MID; client_id = 2; order_type = PEGGED; qty = 3;
   min_qty = 4; leaves_qty = 8367; price = 2; time = 1797; src = 5;
   order_attr = RESIDENT; capacity = Principal; category = C_ONE;
   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 = 7; 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 = 6}
let o2 : order =
  {id = 17; peg = NEAR; client_id = 18; order_type = PEGGED_CI; qty = 19;
   min_qty = 20; leaves_qty = 8366; price = 1; time = 1797; src = 21;
   order_attr = RESIDENT; capacity = Principal; category = C_ONE;
   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 = 16; 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 o3 : order =
  {id = 11; peg = MID; client_id = 8; order_type = PEGGED_CI; qty = 12;
   min_qty = 13; leaves_qty = 8365; price = (-1); time = 1796; src = 9;
   order_attr = RESIDENT; capacity = Principal; category = C_ONE;
   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 = 14}
let mkt : mkt_data = {nbb = 2439; nbo = (-2437); l_up = 3; l_down = 4}
Refuted
proof attempt
ground_instances:0
definitions:0
inductions:0
search_time:
0.034s
details:
Expand
smt_stats:
arith offset eqs:55
num checks:1
arith assert lower:106
arith tableau max rows:31
arith tableau max columns:54
arith pivots:33
rlimit count:66208
mk clause:796
datatype occurs check:11
mk bool var:892
arith assert upper:129
datatype splits:53
decisions:980
arith row summations:318
arith bound prop:43
propagations:1689
interface eqs:1
conflicts:55
arith fixed eqs:39
arith assume eqs:1
datatype accessor ax:64
minimized lits:35
arith conflicts:9
arith num rows:31
arith assert diseq:160
datatype constructor ax:154
num allocs:14018604
final checks:2
added eqs:1830
del clause:243
arith eq adapter:89
time:0.019000
memory:22.060000
max memory:23.270000
Expand
  • start[0.034s]
  let (_x_0 : order) = ….1 in
  let (_x_1 : int) = ….time in
  let (_x_2 : int) = ….leaves_qty in
  let (_x_3 : order_type) = _x_0.order_type in
  let (_x_4 : order_type) = ….order_type in
  let (_x_5 : bool) = (_x_4 = PEGGED_CI) || (_x_4 = LIMIT_CI) in
  let (_x_6 : bool) = _x_4 = MARKET in
  let (_x_7 : real) = if _x_6 then … else … in
  let (_x_8 : bool) = ….0 = BUY in
  let (_x_9 : real) = if _x_8 then … else … in
  let (_x_10 : bool) = _x_4 = LIMIT in
  let (_x_11 : bool) = … = BUY in
  let (_x_12 : real) = if _x_11 then … else … in
  let (_x_13 : int)
      = if (if _x_10 then _x_9 else _x_7) = (if _x_10 then _x_12 else _x_7)
        then 0 else (-1)
  in
  let (_x_14 : real) = if _x_4 = PEGGED then … else … in
  let (_x_15 : real) = if ….1 < 0 then … else … in
  let (_x_16 : real)
      = if _x_10 then if _x_11 then _x_15 else _x_15
        else if _x_6 then _x_12 else _x_14
  in
  let (_x_17 : int)
      = if (if _x_10 then if _x_8 then _x_15 else _x_15
            else if _x_6 then _x_9 else _x_14)
           < _x_16
        then 1 else _x_13
  in
  let (_x_18 : bool) = ( :var_0: ) = BUY in
  let (_x_19 : real)
      = if _x_10 then if _x_18 then _x_15 else _x_15
        else if _x_6 then if _x_18 then … else … else _x_14
  in
  let (_x_20 : int) = if _x_19 > _x_16 then 1 else _x_13 in
  let (_x_21 : int)
      = if _x_18 then if _x_19 > _x_19 then 1 else 0
        else if _x_19 < _x_19 then 1 else 0
  in
  let (_x_22 : bool)
      = if _x_21 = 1 then true
        else
        if _x_21 = (-1) then false
        else
        if _x_5 && _x_5 then _x_2 > _x_2
        else if (if _x_1 < _x_1 then 1 else …) = 1 then true else …
  in
  (if (if _x_18 then _x_20 else _x_17) = 1 then true
   else
   if (if _x_11 then _x_20 else _x_17) = (-1) then false
   else
   if ((_x_3 = PEGGED_CI) || (_x_3 = LIMIT_CI)) && _x_5
   then _x_0.leaves_qty > _x_2
   else if (if _x_0.time < _x_1 then 1 else …) = 1 then true else …)
  && _x_22 ==> _x_22

  • simplify

    into:
    let (_x_0 : order_type) = ( :var_1: ).order_type in
let (_x_1 : bool) = _x_0 = MARKET in
let (_x_2 : bool) = ( :var_0: ) = BUY in
let (_x_3 : real) = if _x_2 then … else … in
let (_x_4 : bool) = _x_0 = LIMIT in
let (_x_5 : real) = if _x_4 then _x_3 else if _x_1 then … else … in
let (_x_6 : order_type) = ( :var_4: ).order_type in
let (_x_7 : bool) = _x_6 = MARKET in
let (_x_8 : bool) = _x_6 = LIMIT in
let (_x_9 : real) = if _x_8 then _x_3 else if _x_7 then … else … in
let (_x_10 : int) = if _x_5 = _x_9 then 0 else (-1) in
let (_x_11 : bool) = _x_6 = PEGGED_CI in
let (_x_12 : real) = if 0 <= ( :var_4: ).price then … else … in
let (_x_13 : real)
    = if _x_8 then if _x_2 then _x_12 else _x_12
      else
      if _x_7 then _x_3 else if (_x_6 = PEGGED) || _x_11 then … else …
in
let (_x_14 : bool) = _x_0 = PEGGED_CI in
let (_x_15 : real) = if 0 <= ( :var_1: ).price then … else … in
let (_x_16 : real)
    = if _x_4 then if _x_2 then _x_15 else _x_15
      else
      if _x_1 then _x_3 else if (_x_0 = PEGGED) || _x_14 then … else …
in
let (_x_17 : int)
    = if _x_2 then if _x_16 <= _x_13 then _x_10 else 1
      else if _x_13 <= _x_16 then _x_10 else 1
in
let (_x_18 : int) = ( :var_4: ).time in
let (_x_19 : int) = ( :var_1: ).time in
let (_x_20 : bool) = _x_18 <= _x_19 in
let (_x_21 : bool) = _x_14 || (_x_0 = LIMIT_CI) in
let (_x_22 : bool) = not _x_21 in
let (_x_23 : bool) = _x_11 || (_x_6 = LIMIT_CI) in
let (_x_24 : bool) = not _x_23 in
let (_x_25 : int) = ( :var_1: ).leaves_qty in
let (_x_26 : int) = ( :var_4: ).leaves_qty in
let (_x_27 : bool) = not (_x_25 <= _x_26) in
let (_x_28 : order_type) = ( :var_2: ).order_type in
let (_x_29 : bool) = _x_28 = MARKET in
let (_x_30 : bool) = _x_28 = LIMIT in
let (_x_31 : real) = if _x_30 then _x_3 else if _x_29 then … else … in
let (_x_32 : int) = if _x_5 = _x_31 then 0 else (-1) in
let (_x_33 : bool) = _x_28 = PEGGED_CI in
let (_x_34 : real) = if 0 <= ( :var_2: ).price then … else … in
let (_x_35 : real)
    = if _x_30 then if _x_2 then _x_34 else _x_34
      else
      if _x_29 then _x_3 else if (_x_28 = PEGGED) || _x_33 then … else …
in
let (_x_36 : int)
    = if _x_2 then if _x_16 <= _x_35 then _x_32 else 1
      else if _x_35 <= _x_16 then _x_32 else 1
in
let (_x_37 : int) = ( :var_2: ).time in
let (_x_38 : bool) = _x_37 <= _x_19 in
let (_x_39 : bool) = _x_33 || (_x_28 = LIMIT_CI) in
let (_x_40 : bool) = not _x_39 in
let (_x_41 : int) = ( :var_2: ).leaves_qty in
let (_x_42 : bool) = not (_x_25 <= _x_41) in
let (_x_43 : int) = if _x_31 = _x_9 then 0 else (-1) in
let (_x_44 : int)
    = if _x_2 then if _x_35 <= _x_13 then _x_43 else 1
      else if _x_13 <= _x_35 then _x_43 else 1
in
let (_x_45 : bool) = _x_18 <= _x_37 in
let (_x_46 : bool) = not (_x_41 <= _x_26) in
(_x_17 = 1)
|| (not (_x_17 = (-1))
    && (if _x_21 && _x_23 then _x_27
        else
          (not _x_20
           || (not (_x_20 && not (_x_19 = _x_18))
               && (_x_22 || (not (_x_21 && _x_24) && _x_27))))))
|| not
   (((_x_36 = 1)
     || (not (_x_36 = (-1))
         && (if _x_21 && _x_39 then _x_42
             else
               (not _x_38
                || (not (_x_38 && not (_x_19 = _x_37))
                    && (_x_22 || (not (_x_21 && _x_40) && _x_42)))))))
    && ((_x_44 = 1)
        || (not (_x_44 = (-1))
            && (if _x_39 && _x_23 then _x_46
                else
                  (not _x_45
                   || (not (_x_45 && not (_x_37 = _x_18))
                       && (_x_40 || (not (_x_39 && _x_24) && _x_46))))))))
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • Sat (Some let side : order_side = BUY let o1 : order = {id = (Z.of_nativeint (1n)); peg = MID; client_id = (Z.of_nativeint (2n)); order_type = PEGGED; qty = (Z.of_nativeint (3n)); min_qty = (Z.of_nativeint (4n)); leaves_qty = (Z.of_nativeint (8367n)); price = (Q.of_nativeint (2n)); time = (Z.of_nativeint (1797n)); src = (Z.of_nativeint (5n)); order_attr = RESIDENT; capacity = Principal; category = C_ONE; 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 = (Z.of_nativeint (7n)); 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 = (Z.of_nativeint (6n))} let o2 : order = {id = (Z.of_nativeint (17n)); peg = NEAR; client_id = (Z.of_nativeint (18n)); order_type = PEGGED_CI; qty = (Z.of_nativeint (19n)); min_qty = (Z.of_nativeint (20n)); leaves_qty = (Z.of_nativeint (8366n)); price = (Q.of_nativeint (1n)); time = (Z.of_nativeint (1797n)); src = (Z.of_nativeint (21n)); order_attr = RESIDENT; capacity = Principal; category = C_ONE; 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 = (Z.of_nativeint (16n)); 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 = (Z.of_nativeint (22n))} let o3 : order = {id = (Z.of_nativeint (11n)); peg = MID; client_id = (Z.of_nativeint (8n)); order_type = PEGGED_CI; qty = (Z.of_nativeint (12n)); min_qty = (Z.of_nativeint (13n)); leaves_qty = (Z.of_nativeint (8365n)); price = (Q.of_nativeint (-1n)); time = (Z.of_nativeint (1796n)); src = (Z.of_nativeint (9n)); order_attr = RESIDENT; capacity = Principal; category = C_ONE; 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 = (Z.of_nativeint (10n)); 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 = (Z.of_nativeint (14n))} let mkt : mkt_data = {nbb = (Q.of_nativeint (2439n)); nbo = (Q.of_nativeint (-2437n)); l_up = (Q.of_nativeint (3n)); l_down = (Q.of_nativeint (4n))} )

      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:

      Try this!
      In [20]:
      CX.o1
      Out[20]:
      - : order =
{id = 1; peg = MID; client_id = 2; order_type = PEGGED; qty = 3; min_qty = 4;
 leaves_qty = 8367; price = 2; time = 1797; src = 5; order_attr = RESIDENT;
 capacity = Principal; category = C_ONE;
 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 = 7; 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 = 6}

      Let's verify this counterexample to transitivity by computation!

      Try this!
      In [21]:
      order_higher_ranked CX.(side, o1, o2, mkt)
      Out[21]:
      - : bool = true
      Try this!
      In [22]:
      order_higher_ranked CX.(side, o2, o3, mkt)
      Out[22]:
      - : bool = true
      Try this!
      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":

      Try this!
      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>
      Try this!
      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.033s):
let side : order_side = BUY
let o1 : order =
  {id = 3; peg = FAR; client_id = 5; order_type = LIMIT; qty = 7720;
   min_qty = 6; leaves_qty = 1; price = 1; time = 1; src = 7;
   order_attr = RESIDENT; capacity = Principal; category = C_ONE;
   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 = 4; 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 : order =
  {id = 18; peg = FAR; client_id = 19; order_type = PEGGED_CI; qty = 1237;
   min_qty = 20; leaves_qty = 1; price = 1; time = 2; src = 21;
   order_attr = RESIDENT; capacity = Principal; category = C_ONE;
   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 o3 : order =
  {id = 13; peg = NEAR; client_id = 9; order_type = LIMIT_CI; qty = 2438;
   min_qty = 10; leaves_qty = 0; price = 1; time = 0; src = 14;
   order_attr = RESIDENT; capacity = Principal; category = C_ONE;
   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 = 12; 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 = 11}
let mkt : mkt_data = {nbb = 8857; nbo = 8858; l_up = 8859; l_down = 8856}
      Refuted
      proof attempt
      ground_instances:0
      definitions:0
      inductions:0
      search_time:
      0.033s
      details:
      Expand
      smt_stats:
      arith offset eqs:24
      num checks:1
      arith assert lower:96
      arith tableau max rows:34
      arith tableau max columns:62
      arith pivots:17
      rlimit count:58801
      mk clause:588
      datatype occurs check:30
      mk bool var:727
      arith assert upper:54
      datatype splits:31
      decisions:781
      arith row summations:73
      arith bound prop:1
      propagations:879
      interface eqs:3
      conflicts:15
      arith fixed eqs:17
      arith assume eqs:3
      datatype accessor ax:49
      minimized lits:1
      arith conflicts:1
      arith num rows:34
      arith assert diseq:42
      datatype constructor ax:133
      num allocs:26812891
      final checks:4
      added eqs:1125
      del clause:166
      arith eq adapter:32
      time:0.019000
      memory:23.000000
      max memory:24.010000
      Expand
      • start[0.033s]
  let (_x_0 : int) = ( :var_0: ).leaves_qty in
  let (_x_1 : int) = ( :var_0: ).qty in
  let (_x_2 : int) = ( :var_1: ).leaves_qty in
  let (_x_3 : int) = ( :var_1: ).qty in
  let (_x_4 : int) = ( :var_2: ).leaves_qty in
  let (_x_5 : int) = ( :var_2: ).qty in
  let (_x_6 : real) = ( :var_3: ).l_down in
  let (_x_7 : real) = ( :var_3: ).nbb in
  let (_x_8 : real) = ( :var_3: ).nbo in
  let (_x_9 : int) = ….time in
  let (_x_10 : int) = ….leaves_qty in
  let (_x_11 : order_type) = ….order_type in
  let (_x_12 : bool) = (_x_11 = PEGGED_CI) || (_x_11 = LIMIT_CI) in
  let (_x_13 : bool) = ( :var_4: ) = BUY in
  let (_x_14 : real) = if ….1 < 0 then … else … in
  let (_x_15 : real)
      = if _x_11 = LIMIT then if _x_13 then _x_14 else _x_14
        else
        if _x_11 = MARKET then if _x_13 then … else …
        else if _x_11 = PEGGED then … else …
  in
  let (_x_16 : int)
      = if _x_13 then if _x_15 > _x_15 then 1 else 0
        else if _x_15 < _x_15 then 1 else 0
  in
  let (_x_17 : bool)
      = if _x_16 = 1 then true
        else
        if _x_16 = (-1) then false
        else
        if _x_12 && _x_12 then _x_10 > _x_10
        else if (if _x_9 < _x_9 then 1 else …) = 1 then true else …
  in
  (_x_0 <= _x_1)
  && ((_x_2 <= _x_3)
      && ((_x_4 <= _x_5)
          && ((( :var_0: ).time >= 0)
              && ((( :var_1: ).time >= 0)
                  && ((( :var_2: ).time >= 0)
                      && ((( :var_0: ).price > 0)
                          && ((( :var_1: ).price > 0)
                              && ((( :var_2: ).price > 0)
                                  && ((_x_1 > 0)
                                      && ((_x_3 > 0)
                                          && ((_x_5 > 0)
                                              && ((_x_0 >= 0)
                                                  && ((_x_2 >= 0)
                                                      && ((_x_4 >= 0)
                                                          && ((_x_6 > 0)
                                                              && ((_x_7
                                                                   > _x_6)
                                                                  && (
                                                                  (_x_8
                                                                   > _x_7)
                                                                  && (
                                                                  ( :var_3: ).l_up
                                                                  > _x_8))))))))))))))))))
  ==> _x_17 && _x_17 ==> _x_17

      • simplify

        into:
        let (_x_0 : order_type) = ( :var_0: ).order_type in
let (_x_1 : bool) = _x_0 = MARKET in
let (_x_2 : bool) = ( :var_4: ) = BUY in
let (_x_3 : real) = if _x_2 then … else … in
let (_x_4 : bool) = _x_0 = LIMIT in
let (_x_5 : real) = if _x_4 then _x_3 else if _x_1 then … else … in
let (_x_6 : order_type) = ( :var_2: ).order_type in
let (_x_7 : bool) = _x_6 = MARKET in
let (_x_8 : bool) = _x_6 = LIMIT in
let (_x_9 : real) = if _x_8 then _x_3 else if _x_7 then … else … in
let (_x_10 : int) = if _x_5 = _x_9 then 0 else (-1) in
let (_x_11 : bool) = _x_6 = PEGGED_CI in
let (_x_12 : real) = ( :var_2: ).price in
let (_x_13 : real) = if 0 <= _x_12 then … else … in
let (_x_14 : real)
    = if _x_8 then if _x_2 then _x_13 else _x_13
      else
      if _x_7 then _x_3 else if (_x_6 = PEGGED) || _x_11 then … else …
in
let (_x_15 : bool) = _x_0 = PEGGED_CI in
let (_x_16 : real) = ( :var_0: ).price in
let (_x_17 : real) = if 0 <= _x_16 then … else … in
let (_x_18 : real)
    = if _x_4 then if _x_2 then _x_17 else _x_17
      else
      if _x_1 then _x_3 else if (_x_0 = PEGGED) || _x_15 then … else …
in
let (_x_19 : int)
    = if _x_2 then if _x_18 <= _x_14 then _x_10 else 1
      else if _x_14 <= _x_18 then _x_10 else 1
in
let (_x_20 : int) = ( :var_2: ).time in
let (_x_21 : int) = ( :var_0: ).time in
let (_x_22 : bool) = _x_20 <= _x_21 in
let (_x_23 : bool) = _x_15 || (_x_0 = LIMIT_CI) in
let (_x_24 : bool) = not _x_23 in
let (_x_25 : bool) = _x_11 || (_x_6 = LIMIT_CI) in
let (_x_26 : bool) = not _x_25 in
let (_x_27 : int) = ( :var_0: ).leaves_qty in
let (_x_28 : int) = ( :var_2: ).leaves_qty in
let (_x_29 : bool) = not (_x_27 <= _x_28) in
let (_x_30 : order_type) = ( :var_1: ).order_type in
let (_x_31 : bool) = _x_30 = MARKET in
let (_x_32 : bool) = _x_30 = LIMIT in
let (_x_33 : real) = if _x_32 then _x_3 else if _x_31 then … else … in
let (_x_34 : int) = if _x_5 = _x_33 then 0 else (-1) in
let (_x_35 : bool) = _x_30 = PEGGED_CI in
let (_x_36 : real) = ( :var_1: ).price in
let (_x_37 : real) = if 0 <= _x_36 then … else … in
let (_x_38 : real)
    = if _x_32 then if _x_2 then _x_37 else _x_37
      else
      if _x_31 then _x_3 else if (_x_30 = PEGGED) || _x_35 then … else …
in
let (_x_39 : int)
    = if _x_2 then if _x_18 <= _x_38 then _x_34 else 1
      else if _x_38 <= _x_18 then _x_34 else 1
in
let (_x_40 : int) = ( :var_1: ).time in
let (_x_41 : bool) = _x_40 <= _x_21 in
let (_x_42 : bool) = _x_35 || (_x_30 = LIMIT_CI) in
let (_x_43 : bool) = not _x_42 in
let (_x_44 : int) = ( :var_1: ).leaves_qty in
let (_x_45 : bool) = not (_x_27 <= _x_44) in
let (_x_46 : int) = if _x_33 = _x_9 then 0 else (-1) in
let (_x_47 : int)
    = if _x_2 then if _x_38 <= _x_14 then _x_46 else 1
      else if _x_14 <= _x_38 then _x_46 else 1
in
let (_x_48 : bool) = _x_20 <= _x_40 in
let (_x_49 : bool) = not (_x_44 <= _x_28) in
let (_x_50 : int) = ( :var_0: ).qty in
let (_x_51 : int) = ( :var_1: ).qty in
let (_x_52 : int) = ( :var_2: ).qty in
let (_x_53 : real) = ( :var_3: ).l_down in
(_x_19 = 1)
|| (not (_x_19 = (-1))
    && (if _x_23 && _x_25 then _x_29
        else
          (not _x_22
           || (not (_x_22 && not (_x_21 = _x_20))
               && (_x_24 || (not (_x_23 && _x_26) && _x_29))))))
|| not
   (((_x_39 = 1)
     || (not (_x_39 = (-1))
         && (if _x_23 && _x_42 then _x_45
             else
               (not _x_41
                || (not (_x_41 && not (_x_21 = _x_40))
                    && (_x_24 || (not (_x_23 && _x_43) && _x_45)))))))
    && ((_x_47 = 1)
        || (not (_x_47 = (-1))
            && (if _x_42 && _x_25 then _x_49
                else
                  (not _x_48
                   || (not (_x_48 && not (_x_40 = _x_20))
                       && (_x_43 || (not (_x_42 && _x_26) && _x_49))))))))
|| not
   ((_x_27 <= _x_50) && (_x_44 <= _x_51) && (_x_28 <= _x_52) && (_x_21 >= 0)
    && (_x_40 >= 0) && (_x_20 >= 0) && not (_x_16 <= 0) && not (_x_36 <= 0)
    && not (_x_12 <= 0) && not (_x_50 <= 0) && not (_x_51 <= 0)
    && not (_x_52 <= 0) && (_x_27 >= 0) && (_x_44 >= 0) && (_x_28 >= 0)
    && not (_x_53 <= 0) && not (… <= _x_53) && not (… <= …)
    && not (( :var_3: ).l_up <= …))
        expansions:
        []
        rewrite_steps:
          forward_chaining:
          • Sat (Some let side : order_side = BUY let o1 : order = {id = (Z.of_nativeint (3n)); peg = FAR; client_id = (Z.of_nativeint (5n)); order_type = LIMIT; qty = (Z.of_nativeint (7720n)); min_qty = (Z.of_nativeint (6n)); leaves_qty = (Z.of_nativeint (1n)); price = (Q.of_nativeint (1n)); time = (Z.of_nativeint (1n)); src = (Z.of_nativeint (7n)); order_attr = RESIDENT; capacity = Principal; category = C_ONE; 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 = (Z.of_nativeint (4n)); 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 = (Z.of_nativeint (8n))} let o2 : order = {id = (Z.of_nativeint (18n)); peg = FAR; client_id = (Z.of_nativeint (19n)); order_type = PEGGED_CI; qty = (Z.of_nativeint (1237n)); min_qty = (Z.of_nativeint (20n)); leaves_qty = (Z.of_nativeint (1n)); price = (Q.of_nativeint (1n)); time = (Z.of_nativeint (2n)); src = (Z.of_nativeint (21n)); order_attr = RESIDENT; capacity = Principal; category = C_ONE; 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 = (Z.of_nativeint (17n)); 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 = (Z.of_nativeint (22n))} let o3 : order = {id = (Z.of_nativeint (13n)); peg = NEAR; client_id = (Z.of_nativeint (9n)); order_type = LIMIT_CI; qty = (Z.of_nativeint (2438n)); min_qty = (Z.of_nativeint (10n)); leaves_qty = (Z.of_nativeint (0n)); price = (Q.of_nativeint (1n)); time = (Z.of_nativeint (0n)); src = (Z.of_nativeint (14n)); order_attr = RESIDENT; capacity = Principal; category = C_ONE; 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 = (Z.of_nativeint (12n)); 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 = (Z.of_nativeint (11n))} let mkt : mkt_data = {nbb = (Q.of_nativeint (8857n)); nbo = (Q.of_nativeint (8858n)); l_up = (Q.of_nativeint (8859n)); l_down = (Q.of_nativeint (8856n))} )

          Extending the model with Document printers

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

          Try this!
          In [26]:
          (* We can generate string printers for our types automatically using the pp plugin *)
Imandra.add_plugin_pp ();;

let doc_of_order o =
  let module D = Document in
  let module H = Tyxml.Html in
  D.indent "order" @@ html (H.table
      [ H.tr [ H.td [ H.txt "id"]; H.td [ H.txt (Z.to_string o.id)]]
      ; H.tr [ H.td [ H.txt "peg"]; H.td [ H.txt ( CCFormat.to_string pp_order_peg o.peg)]]
      ; H.tr [ H.td [ H.txt "client_id"]; H.td [ H.txt (Z.to_string o.client_id)]]
      ; H.tr [ H.td [ H.txt "order_type"]; H.td [ H.txt ( CCFormat.to_string pp_order_type o.order_type)]]
      ; H.tr [ H.td [ H.txt "qty"]; H.td [ H.txt (Z.to_string o.qty)]]
      ; H.tr [ H.td [ H.txt "min_qty"]; H.td [ H.txt (Z.to_string o.min_qty)]]
      ; H.tr [ H.td [ H.txt "leaves_qty"]; H.td [ H.txt (Z.to_string o.leaves_qty)]]
      ; H.tr [ H.td [ H.txt "price"]; H.td [ H.txt ( Real.to_string_approx o.price)]]
      ; H.tr [ H.td [ H.txt "time"]; H.td [ H.txt ( CCFormat.to_string pp_time o.time)]]
      ; H.tr [ H.td [ H.txt "src"]; H.td [ H.txt ( CCFormat.to_string pp_order_source o.src)]]
      ; H.tr [ H.td [ H.txt "order_attr"]; H.td [ H.txt ( CCFormat.to_string pp_order_attr o.order_attr)]]
      ; H.tr [ H.td [ H.txt "capacity"]; H.td [ H.txt ( CCFormat.to_string pp_capacity o.capacity)]]
      ; H.tr [ H.td [ H.txt "category"]; H.td [ H.txt ( CCFormat.to_string pp_category o.category)]]
      ; H.tr [ H.td [ H.txt "locate_found"]; H.td [ H.txt (CCFormat.sprintf "%B" o.locate_found)]]
      ; H.tr [ H.td [ H.txt "expiry_time"]; H.td [ H.txt (Z.to_string o.expiry_time)]]
      ])
[@@program];;

#install_doc doc_of_order;;

let doc_of_side side = Document.s @@ CCFormat.to_string pp_order_side side
[@@program];;

#install_doc doc_of_side;;

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_data mkt]])
 [@@program];;

#install_doc pp_rank
          Out[26]:
          - : unit = ()
val doc_of_order : order -> Document.t = <fun>
val doc_of_side : order_side -> Document.t = <fun>
val pp_rank : order_side * order * order * order * mkt_data -> Document.t =
  <fun>

          Now, let's view our latest counterexample again:

          Try this!
          In [27]:
          CX.(side, o1, o2, o3, mkt)
          Out[27]:
          - : order_side * order * order * order * mkt_data = <document>
          sideorder1order2order3mkt
          BUY
          order
          id3
          pegFAR
          client_id5
          order_typeLIMIT
          qty7720
          min_qty6
          leaves_qty1
          price1.
          time1
          src7
          order_attrRESIDENT
          capacityPrincipal
          categoryC_ONE
          locate_foundfalse
          expiry_time8
          order
          id18
          pegFAR
          client_id19
          order_typePEGGED_CI
          qty1237
          min_qty20
          leaves_qty1
          price1.
          time2
          src21
          order_attrRESIDENT
          capacityPrincipal
          categoryC_ONE
          locate_foundfalse
          expiry_time22
          order
          id13
          pegNEAR
          client_id9
          order_typeLIMIT_CI
          qty2438
          min_qty10
          leaves_qty0
          price1.
          time0
          src14
          order_attrRESIDENT
          capacityPrincipal
          categoryC_ONE
          locate_foundfalse
          expiry_time11
          mkt_data
          nbb8857.
          nbo8858.
          l_up8859.
          l_down8856.